pisigma-0.1.0.1: examples/Streams.pi

Unit : Type;
Unit = { unit };

Empty : Type;
Empty = { };

Bool : Type;
Bool = { true false };

T : Bool -> Type;
T = \ b -> case b of {
             true -> Unit
	   | false -> Empty };


Nat : Type;
Nat = (l : { z s }) * case l of {
                           z -> Unit
			 | s -> [Nat] };

zero : Nat;
zero = ('z,'unit);

succ : Nat -> Nat;
succ = \ n -> ('s,n);

one : Nat;
one = succ zero;

two : Nat;
two = succ one;

add : Nat -> Nat -> Nat;
add = \ m n -> split m with (lm , m') ->
                 ! case lm of {
		     z -> [n]
 		   | s -> [succ (add m' n)] };

eqbNat : Nat -> Nat -> Bool;
eqbNat = \ m n -> split m with (lm , m') ->
                  split n with (ln , n') ->
                  ! case lm of {
		     z -> case ln of { 
		             z -> ['true]
			   | s -> ['false] }
	           | s -> case ln of {
		             z -> ['false]
			   | s -> [eqbNat m' n'] } };

eqNat : Nat -> Nat -> Type;
eqNat = \ m n -> T (eqbNat m n);

reflNat : (n:Nat) -> eqNat n n;
reflNat = \ n -> split n with (ln , n') ->
       	        ! case ln of {
		     z -> ['unit]
		   | s -> [reflNat n'] };


Stream : Type -> Type;
Stream = \ a -> a * [^ (Stream a)];

put : (a : Type) -> a -> Stream a -> Stream a;
put = \ a x xs -> (x,[xs]);

from : Nat -> Stream Nat;
from = \ n -> (n, [from (succ n)]);

tail : (a:Type) -> Stream a -> Stream a;
tail = \ a xs -> split xs with (x , xs') -> ! xs';

head : (a:Type) -> Stream a -> a;
head = \ a xs -> split xs with (x , xs') -> x;

map : (a : Type) -> (b : Type) -> (a -> b) -> Stream a -> Stream b;
map = \ a b f xs -> split xs with (x , xs') -> (f x, [map a b f (! xs')]);

eqStream : (a : Type) -> (a -> a -> Type) -> Stream a -> Stream a -> Type;
eqStream = \ a eq xs ys -> split xs with (x , xs') ->
	                   split ys with (y , ys') ->
			   	 (eq x y) * [^ (eqStream a eq (! xs') (! ys'))];

reflStream :  (a : Type) -> (eq : a -> a -> Type) 
	   -> ((x : a) -> eq x x)
	   -> (xs : Stream a) -> eqStream a eq xs xs;
reflStream = \ a eq refl xs -> split xs with (x , xs') -> 
	       	    	         ((refl x), [reflStream a eq refl (! xs')]);

lemma : (n : Nat) -> eqStream Nat eqNat (from (succ n)) 
                                        (map Nat Nat succ (from n));
lemma = \ n -> ((reflNat (succ n)),[lemma (succ n)]);