simple examples on nat and list

diff --git a/examples/add.ctt b/examples/add.ctt
new file mode 100644 (file)
index 0000000..e55cb9f
--- /dev/null
+++ b/examples/add.ctt
@@ -0,0 +1,52 @@
+module add where
+
+import nat
+
+add (a : nat) : nat -> nat = split
+  zero  -> a
+  suc n -> suc (add a n)
+
+add_zero : (n : nat) -> Id nat (add zero n) n = split
+  zero  -> <i> zero
+  suc n -> <i> suc (add_zero n @ i)
+
+add_suc (a:nat) : (n : nat) -> Id nat (add (suc a) n) (suc (add a n)) = split
+  zero  ->  <i> suc a
+  suc m -> <i> suc (add_suc a m @ i)
+
+add_comm (a : nat) : (n : nat) -> Id nat (add a n) (add n a) = split
+  zero  -> <i> add_zero a @ -i
+  suc m -> <i> comp nat (suc (add_comm a m @ i)) [ (i = 1) -> <j> add_suc m a @ -j]
+
+assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = split
+ zero -> <i>add a b
+ suc c1 -> <i>suc (assocAdd a b c1@i)
+
+
+test (A:U) (a b c d e : A) (p:Id A a b) (q:Id A b c) (r:Id A c d) (s:Id A d e) : Id A a e =
+ <i>comp A (p@i) [ (i=1) -> <i>comp A (q@i) [ (i=1) -> <i>comp A (r@i) [ (i=1) -> s]]]
+
+data tree = leaf | bin (t0 t1:tree)
+
+swap : tree -> tree = split
+ leaf -> leaf
+ bin t0 t1 -> bin (swap t1) (swap t0)
+
+lem : (t:tree) -> Id tree (swap (swap t)) t = split
+ leaf -> <i>leaf
+ bin t0 t1 -> <i>bin (lem t0@i) (lem t1@i)
+
+pred : nat -> nat = split
+ zero -> zero
+ suc n -> n
+
+simplAdd (b c :nat) : (a : nat) -> Id nat (add b a) (add c a) -> Id nat b c = split
+ zero -> \ (h:Id nat b c) -> h
+ suc a1 -> \ (h : Id nat (suc (add b a1)) (suc (add c a1))) -> simplAdd b c a1 (<i>pred (h@i))
+
+corSimplAdd (b c a :nat) (h: Id nat (add a b) (add a c)) : Id nat b c =  simplAdd b c a rem
+ where rem : Id nat (add b a) (add c a) = 
+          <i>comp nat ((add_comm b a)@i) [(i=1) -> <i>comp nat (h@i) [(i=1) -> add_comm a c]]
+ 
+
+leq (b c:nat) : U = (a : nat) * Id nat (add a b) c
\ No newline at end of file

diff --git a/examples/list.ctt b/examples/list.ctt
index 64584a40e5d03327178b1070946055165dc46d6e..da6b6ce50813abc6afcb1460ec166ccb1d23f3f0 100644 (file)
--- a/examples/list.ctt
+++ b/examples/list.ctt
@@ -11,3 +11,40 @@ append (A : U) : list A -> list A -> list A = split
 reverse (A : U) : list A -> list A = split
   nil -> nil
   cons x xs -> append A (reverse A xs) (cons x nil)
+
+map (A B:U) (f:A->B) : list A -> list B = split
+ nil -> nil
+ cons x xs -> cons (f x) (map A B f xs)
+
+lem (A B C:U) (f:A->B) (g:B -> C) : 
+ (xs:list A) -> Id (list C) (map B C g (map A B f xs)) (map A C (\ (x:A) -> g (f x)) xs) = split
+ nil -> <i>nil
+ cons x xs -> <i>cons (g (f x)) (lem A B C f g xs@i)
+
+funId (A:U) (x:A) : A = x
+
+lem1 (A:U) : (xs:list A) -> Id (list A) (map A A (funId A) xs) xs = split
+ nil -> <i>nil
+ cons x xs -> <i>cons x (lem1 A xs@i)
+
+reverse (A : U) : list A -> list A = split
+  nil -> nil
+  cons x xs -> append A (reverse A xs) (cons x nil)
+
+lem2 (A:U) : (xs:list A) -> Id (list A) (append A xs nil) xs = split
+ nil -> <i>nil
+ cons x xs -> <i>cons x (lem2 A xs@i)
+
+assoc (A:U) : (xs ys zs : list A) -> Id (list A) (append A (append A xs ys) zs) (append A xs (append A ys zs)) = split
+ nil -> \ (ys zs:list A) -> <i>append A ys zs
+ cons x xs -> \ (ys zs:list A) -> <i>cons x (assoc A xs ys zs@i)
+
+lem4 (A:U) : (xs ys:list A) -> Id (list A) (reverse A (append A xs ys)) (append A (reverse A ys) (reverse A xs)) = split
+ nil -> \ (ys:list A) -> <i>lem2 A (reverse A ys)@-i
+ cons x xs -> \ (ys:list A) -> <i>comp (list A) (append A (lem4 A xs ys@i) (cons x nil))
+                                                [(i=1) -> assoc A (reverse A ys) (reverse A xs) (cons x nil)]
+
+lem5 (A:U) : (xs:list A) -> Id (list A) (reverse A (reverse A xs)) xs = split
+ nil -> <i>nil
+ cons x xs -> <i>comp (list A) (lem4 A (reverse A xs) (cons x nil)@i) [(i=1) -> <j>cons x (lem5 A xs@j)]
+