From f9e396ba2ac89c6b4a5f0eb61f226f6d2f2d6b76 Mon Sep 17 00:00:00 2001
From: KonjacSource <1435771606@qq.com>
Date: Fri, 30 Aug 2024 12:19:15 +0800
Subject: [PATCH] update Example.shitt

---
 Example.shitt | 29 ++++++++++++++++++++++++++---
 1 file changed, 26 insertions(+), 3 deletions(-)

diff --git a/Example.shitt b/Example.shitt
index 2422709..1d4455b 100644
--- a/Example.shitt
+++ b/Example.shitt
@@ -4,7 +4,6 @@ data Id {A : U} : (_ _ : A) -> U where
 fun uip {A : U} {x y : A} (p q : Id x y) : Id p q where 
 | (refl _) (refl x) = refl (refl _)
 
-
 data N : U where  
 | zero : ...  
 | succ : (pre : N) -> ...  
@@ -17,13 +16,37 @@ data Vec (A : U) : (_ : N) -> U where
 | nil : ... zero 
 | cons : {n : N} (x : A) (xs : Vec A n) -> ... (succ n)
 
+#infer Vec
+
 fun append {A : U} {m n : N} (v : Vec A m) (w : Vec A n) : Vec A (add m n) 
 | nil w = w 
 | (cons x xs) w = cons x (append xs w)
 
+#eval append (cons zero (cons (succ zero) nil)) nil
+
+-- Some theorems.
+
+fun sym {A : U} {x y : A} (p : Id x y) : Id y x where 
+| (refl _) = refl _
+
+fun trans {A : U} {x y z : A} (_ : Id x y) (_ : Id y z) : Id x z where 
+| (refl _) (refl _) = refl _ 
+
 fun cong {A B : U} {x y : A} (f : A -> B) (p : Id x y) : Id (f x) (f y) where 
 | f (refl x) = refl _
 
+fun addAssoc (x y z : N) : Id (add (add x y) z) (add x (add y z)) where 
+| zero y z = refl _
+| (succ x) y z = cong succ (addAssoc x y z) 
 
-#eval append (cons zero (cons (succ zero) nil)) nil
-#infer Vec
\ No newline at end of file
+fun addIdR (x : N) : Id (add x zero) x where 
+| zero = refl _ 
+| (succ x) = cong succ (addIdR x)
+
+fun addSucc (x y : N) : Id (add (succ x) y) (add x (succ y)) where 
+| zero y = refl _ 
+| (succ x) y = cong succ (addSucc x y)
+
+fun addComm (x y : N) : Id (add x y) (add y x) where 
+| zero y = sym (addIdR _)
+| (succ x) y = trans (cong succ (addComm x y)) (addSucc y x)
\ No newline at end of file