From: Anders Mörtberg 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)) = 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)) = assocAdd c b a @ -i - in comp (<_> nat) (rem1 @ i) [ (i = 0) -> 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))) = add a (add_comm3 b c d @ i) in 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 -> add a b suc c1 -> 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 = 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)) = 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)) = assocAdd c b a @ -i + in comp (<_> nat) (rem1 @ i) [ (i = 0) -> 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 - -