foo

[bitonic-mengthesis.git] / itt.ka

diff --git a/itt.ka b/itt.ka
index e9decf6bb4a19d72bdfd3de644adc9827246afa4..c30ffc4fa69a36133dd7f14b79e134237185f575 100644 (file)
--- a/itt.ka
+++ b/itt.ka
@@ -1,3 +1,6 @@
+------------------------------------------------------------
+-- Core ITT (minus W)
+
 data Empty : * => { }
 
 absurd [A : *] [x : Empty] : A => (
@@ -15,3 +18,72 @@ data Bool : * => { true : Bool | false : Bool }
 
 -- The if_then_else_ is provided by Bool-Elim
 
+-- A large eliminator, for convenience
+ITE [b : Bool] [A B : *] : * => (
+  Bool-Elim b (\_ => *) A B
+)
+
+------------------------------------------------------------
+-- Examples →
+
+data Nat : * => { zero : Nat | suc : Nat -> Nat }
+
+gt [n : Nat] : Nat -> * => (
+  Nat-Elim
+    n
+    (\_ => Nat -> *)
+    (\_ => Empty)
+    (\n f m => Nat-Elim m (\_ => *) Unit (\m' _ => f m'))
+)
+
+data List : [A : *] -> * =>
+  { nil : List A | cons : A -> List A -> List A }
+
+length [A : *] [xs : List A] : Nat => (
+    List-Elim xs (\_ => Nat) zero (\_ _ n => suc n)
+)
+
+head [A : *] [xs : List A] : gt (length A xs) zero -> A => (
+    List-Elim
+      xs
+      (\xs => gt (length A xs) zero -> A)
+      (\p => absurd A p)
+      (\x _ _ _ => x)
+)
+
+------------------------------------------------------------
+-- Examples ×
+
+data Parity : * => { even : Parity | odd : Parity }
+
+flip [p : Parity] : Parity => (
+  Parity-Elim p (\_ => Parity) odd even
+)
+
+parity [n : Nat] : Parity => (
+  Nat-Elim n (\_ => Parity) even (\_ => flip)
+)
+
+even [n : Nat] : * => (Parity-Elim (parity n) (\_ => *) Unit Empty)
+
+one   : Nat => (suc zero)
+two   : Nat => (suc one)
+three : Nat => (suc two)
+four  : Nat => (suc three)
+five  : Nat => (suc four)
+six   : Nat => (suc five)
+
+even-6 : even six => tt
+
+even-5-neg : neg (even five) => (\z => z)
+
+there-is-an-even-number : Prod Nat even => (prod six even-6)
+
+Or [A B : *] : * => (Prod Bool (\b => ITE b A B))
+
+left  [A B : *] [x : A] : Or A B => (prod true  x)
+right [A B : *] [x : B] : Or A B => (prod false x)
+
+case [A B C : *] [f : A -> C] [g : B -> C] [x : Or A B] : C => (
+  (Bool-Elim (fst x) (\b => ITE b A B -> C) f g) (snd x)
+)
\ No newline at end of file