From: Anders Mörtberg <andersmortberg@gmail.com>
Date: Fri, 15 Jan 2016 21:29:06 +0000 (-0500)
Subject: move two lemmas to nat
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=a9d652db84f5e592afda63b98dc9dae7e50cd055;p=cubicaltt.git

move two lemmas to nat
---

diff --git a/examples/hz.ctt b/examples/hz.ctt
index feabc89..a2d5261 100644
--- a/examples/hz.ctt
+++ b/examples/hz.ctt
@@ -6,23 +6,12 @@ import setquot
 -- shorthand for nat x nat
 nat2 : U = and nat nat
 
-add_comm3 (a b c : nat) : Id nat (add a (add b c)) (add c (add b a)) = 
-  let rem : Id nat (add a (add b c)) (add a (add c b)) = <i> add a (add_comm b c @ i)
-      rem1 : Id nat (add a (add c b)) (add (add c b) a) = add_comm a (add c b)
-      rem2 : Id nat (add (add c b) a) (add c (add b a)) = <i> assocAdd c b a @ -i
-  in <i> comp (<_> nat) (rem1 @ i) [ (i = 0) -> <j> rem @ -j, (i = 1) -> rem2 ]
-
 natlemma (a b c d : nat) : Id nat (add (add a b) (add c d)) (add (add a d) (add c b)) =
   let rem : Id nat (add a (add b (add c d))) (add a (add d (add c b))) =
         <i> add a (add_comm3 b c d @ i)
   in <i> comp (<_> nat) (rem @ i) [ (i = 0) -> assocAdd a b (add c d)
                                   , (i = 1) -> assocAdd a d (add c b) ]
 
-natcancelr (a b : nat) : (x : nat) -> Id nat (add a x) (add b x) -> Id nat a b = split
-  zero -> \(h : Id nat a b) -> h
-  suc x' -> \(h : Id nat (suc (add a x')) (suc (add b x'))) ->
-    natcancelr a b x' (sucInj (add a x') (add b x') h)
-
 rel : eqrel nat2 = (r,rem)
   where
   r : hrel nat2 = \(x y : nat2) -> 
diff --git a/examples/nat.ctt b/examples/nat.ctt
index b76fef7..db26e94 100644
--- a/examples/nat.ctt
+++ b/examples/nat.ctt
@@ -33,7 +33,6 @@ assocAdd (a b:nat) : (c:nat) -> Id nat (add a (add b c)) (add (add a b) c) = spl
  zero -> <i>add a b
  suc c1 -> <i>suc (assocAdd a b c1@i)
 
-
 add' : nat -> nat -> nat = split
   zero -> \(x : nat) -> x
   suc n -> \(x : nat) -> suc (add' n x)
@@ -41,6 +40,17 @@ add' : nat -> nat -> nat = split
 sucInj (n m : nat) (p : Id nat (suc n) (suc m)) : Id nat n m =
  <i> pred (p @ i)
 
+add_comm3 (a b c : nat) : Id nat (add a (add b c)) (add c (add b a)) =
+  let rem : Id nat (add a (add b c)) (add a (add c b)) = <i> add a (add_comm b c @ i)
+      rem1 : Id nat (add a (add c b)) (add (add c b) a) = add_comm a (add c b)
+      rem2 : Id nat (add (add c b) a) (add c (add b a)) = <i> assocAdd c b a @ -i
+  in <i> comp (<_> nat) (rem1 @ i) [ (i = 0) -> <j> rem @ -j, (i = 1) -> rem2 ]
+
+natcancelr (a b : nat) : (x : nat) -> Id nat (add a x) (add b x) -> Id nat a b = split
+  zero -> \(h : Id nat a b) -> h
+  suc x' -> \(h : Id nat (suc (add a x')) (suc (add b x'))) ->
+    natcancelr a b x' (sucInj (add a x') (add b x') h)
+
 idnat : nat -> nat = split
   zero -> zero
   suc n -> suc (idnat n)
@@ -73,5 +83,3 @@ natDec : (n m:nat) -> dec (Id nat n m) = split
                  (sucInj n m) (natDec n m))
 
 natSet : set nat = hedberg nat natDec
-
-