From: Anders Mörtberg <mortberg@chalmers.se>
Date: Tue, 14 Apr 2015 20:19:49 +0000 (+0200)
Subject: Start defining integers as a HIT and proving that they are a set
X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=4c15428ba96acdc47fc2e1349e1aebcd0a3c36fc;p=cubicaltt.git

Start defining integers as a HIT and proving that they are a set
---

diff --git a/examples/int.ctt b/examples/int.ctt
index 3d12f32..dc4ccc0 100644
--- a/examples/int.ctt
+++ b/examples/int.ctt
@@ -3,9 +3,10 @@ module int where
 import nat
 import discor
 
+-- inl = neg, inr = pos
 Z : U = or nat nat
 
-zeroZ : Z =  inr zero
+zeroZ : Z = inr zero
 
 sucZ : Z -> Z = split
   inl u -> auxsucZ u
diff --git a/examples/integer.ctt b/examples/integer.ctt
index e8b6ba9..da9b4b3 100644
--- a/examples/integer.ctt
+++ b/examples/integer.ctt
@@ -1,42 +1,67 @@
 module integer where
 
-import nat
-
-data Z = zeroZ | posZ (n : nat) | negZ (n : nat)
-
-caseNat (A : U) (a : A) (f : nat -> A) : nat -> A = split
-  zero -> a
-  suc n -> f n
-
-sucZ : Z -> Z = split
-  zeroZ -> posZ zero
-  posZ n -> posZ (suc n)
-  negZ n -> caseNat Z zeroZ (\(x : nat) -> negZ x) n
-
-predZ : Z -> Z = split
-  zeroZ -> negZ zero
-  posZ n -> caseNat Z zeroZ (\(x : nat) -> posZ x) n
-  negZ n -> negZ (suc n)
-
-sucpredZ : (n : Z) -> Id Z (sucZ (predZ n)) n = split
-  zeroZ  -> refl Z zeroZ
-  posZ n -> lem n
-   where
-    lem : (n : nat) -> Id Z (sucZ (predZ (posZ n))) (posZ n) = split
-      zero  -> refl Z (posZ zero)
-      suc n -> refl Z (posZ (suc n))
-  negZ n -> refl Z (negZ n)
-
-predsucZ : (n : Z) -> Id Z (predZ (sucZ n)) n = split
-  zeroZ -> refl Z zeroZ
-  posZ n -> refl Z (posZ n)
-  negZ n -> lem n
-   where
-    lem : (n : nat) -> Id Z (predZ (sucZ (negZ n))) (negZ n) = split
-      zero  -> refl Z (negZ zero)
-      suc n -> refl Z (negZ (suc n))
-
-sucIdZ : Id U Z Z = isoId Z Z sucZ predZ sucpredZ predsucZ
-
-sucIdZ2 : Id U Z Z = compId U Z Z Z sucIdZ sucIdZ
-test : Z = predZ (transport sucIdZ2 zeroZ)
\ No newline at end of file
+import int
+
+data int = pos (n : nat)
+         | neg (n : nat)
+         | zeroP @ pos zero ~ neg zero
+
+zeroP' : Id int (pos zero) (neg zero) = <i> zeroP {int} @ i
+
+sucInt : int -> int = split
+  pos n -> pos (suc n)
+  neg n -> sucNat n
+    where sucNat : nat -> int = split
+            zero -> pos one
+            suc n -> neg n
+  zeroP @ i -> pos one
+
+predInt : int -> int = split
+  pos n -> predNat n
+    where predNat : nat -> int = split
+	    zero -> neg one
+	    suc n -> pos n
+  neg n -> neg (suc n)
+  zeroP @ i -> neg one
+
+toZ : int -> Z = split
+  pos n -> inr n
+  neg n -> fun n
+    where fun : nat -> Z = split
+      zero -> zeroZ
+      suc n -> inl n
+  zeroP @ i -> zeroZ
+
+fromZ : Z -> int = split
+  inl n -> neg (suc n)
+  inr n -> pos n
+
+toZK : (a : Z) -> Id Z (toZ (fromZ a)) a = split
+  inl n -> refl Z (inl n)
+  inr n -> refl Z (inr n)
+
+-- fromZ (toZ (neg zero)) = fromZ (fun zero)
+--                        = fromZ zeroZ
+--			  = fromZ (inr zero)
+--			  = pos zero
+
+-- fromZ (toZ (neg (suc n)) = fromZ (fun (suc n))
+-- 	      	   	    = fromZ (inl n)
+--			    = neg (suc n)
+
+sq : Square int (pos zero) (pos zero) (refl int (pos zero))
+                (pos zero) (neg zero) zeroP'
+		(refl int (pos zero)) zeroP' = undefined
+		
+fromZK : (a : int) -> Id int (fromZ (toZ a)) a = split
+  pos n -> refl int (pos n)
+  neg n -> rem n
+    where rem : (n : nat) -> Id int (fromZ (toZ (neg n))) (neg n) = split
+      zero -> zeroP'
+      suc n -> refl int (neg (suc n))
+  zeroP @ i -> temp
+    where temp : Id int (pos zero) (zeroP{int} @ i) = undefined
+
+isoIntZ : Id U Z int = isoId Z int fromZ toZ fromZK toZK
+
+intSet : set int = subst U set Z int isoIntZ ZSet