Add System F-style Polymorphism

.gitignore

@@ -1 +1,4 @@
 *.agdai
+debruijn/no-positivity-core-type.agda
+debruijn/no-positivity-core-exp.agda
+debruijn/no-positivity-core.agda

Dockerfile

@@ -3,5 +3,6 @@ run cabal update
 run cabal install alex
 run cabal install happy
 run cabal install Agda-2.5.4.2
+# Warning: Agda version may be out of date
 copy . .
 cmd ["agda" , "-v", "2" , "all.agda"]

Nat.agda

@@ -22,3 +22,115 @@ module Nat where
   natEQ (1+ x) (1+ y) with natEQ x y
   natEQ (1+ x) (1+ .x) | Inl refl = Inl refl
   ... | Inr b = Inr (λ x₁ → b (1+inj x y x₁))
+
+  natEQrefl : {x : Nat} -> natEQ x x == Inl refl
+  natEQrefl {x} with natEQ x x
+  ... | Inl refl = refl
+  ... | Inr neq = abort (neq refl)
+
+  natEQneq : {x y : Nat} -> (neq : ((x == y) → ⊥)) -> natEQ x y == Inr neq
+  natEQneq {x} {y} neq with natEQ x y
+  ... | Inl refl = abort (neq refl)
+  ... | Inr neq' = inr-inj (funext (λ eq → abort (neq eq)))
+    where
+      inr-inj : ∀{a a'} -> a == a' -> Inr a == Inr a'
+      inr-inj eq rewrite eq = refl
+
+  data _<_ : Nat → Nat → Set where
+    LTZ : ∀{n} -> Z < 1+ n
+    LTS : ∀{n m} -> n < m -> 1+ n < 1+ m
+
+  natLT : (n m : Nat) -> ((n < m) + ¬(n < m))
+  natLT Z Z = Inr (λ ())
+  natLT Z (1+ n) = Inl LTZ
+  natLT (1+ n) Z = Inr (λ ())
+  natLT (1+ n) (1+ m) with natLT n m
+  ... | Inl p = Inl (LTS p)
+  ... | Inr p = Inr (\{(LTS p') -> p p'})
+
+  lt-1+ : {x : Nat} -> x < 1+ x
+  lt-1+ {Z} = LTZ
+  lt-1+ {1+ x'} = LTS lt-1+
+
+  lt-ne : {x y : Nat} -> x < y -> (x == y) → ⊥
+  lt-ne LTZ = \ ()
+  lt-ne (LTS {n} {m} p) = \eq -> lt-ne p ((1+inj n m eq))
+
+  lt-antisym : {x y : Nat} -> x < y -> y < x -> ⊥
+  lt-antisym LTZ = λ ()
+  lt-antisym (LTS p) (LTS p') = lt-antisym p p'
+
+  lt-gtz : {x y : Nat} -> y < x -> Σ[ z ∈ Nat ] (x == 1+ z)
+  lt-gtz (LTZ {n}) = n , refl
+  lt-gtz (LTS {n} {m} p) = let p1 , p2 = lt-gtz p in 1+ p1 , foo p2
+    where
+      foo : {x y : Nat} -> x == y -> 1+ x == 1+ y
+      foo eq rewrite eq = refl
+
+  lt-1+-inj : {x y : Nat} -> 1+ x < 1+ y -> x < y
+  lt-1+-inj (LTS p) = p
+
+  lt-trans-1+ : {x y z : Nat} -> x < y -> y < z -> 1+ x < z
+  lt-trans-1+ LTZ (LTS LTZ) = LTS LTZ
+  lt-trans-1+ LTZ (LTS (LTS p)) = LTS LTZ
+  lt-trans-1+ (LTS p) (LTS p') = LTS (lt-trans-1+ p p')
+
+  lt-right-incr : {x y : Nat} -> x < y -> x < 1+ y
+  lt-right-incr LTZ = LTZ
+  lt-right-incr (LTS p) = LTS (lt-right-incr p)
+
+  lt-trans : {x y z : Nat} -> x < y -> y < z -> x < z
+  lt-trans LTZ (LTS p) = LTZ
+  lt-trans (LTS p) (LTS p') = lt-right-incr (lt-trans-1+ p p')
+
+  lt-right-incr-neq : {x y : Nat} -> x < 1+ y -> ((x == y) -> ⊥) -> x < y
+  lt-right-incr-neq {y = 0} LTZ d = abort (d refl)
+  lt-right-incr-neq {y = (1+ y')} LTZ d = LTZ
+  lt-right-incr-neq {y = 0} (LTS ()) d 
+  lt-right-incr-neq {x = (1+ x')} {y = (1+ y')} (LTS a) d = LTS (lt-right-incr-neq {x = x'} {y = y'} a λ x → d (foo x))
+    where 
+      foo : {a b : Nat} -> a == b -> (1+ a) == (1+ b)
+      foo eq rewrite eq = refl
+
+  lt-lte-is-lt : {a b c : Nat} -> (a < b) -> (b < (1+ c)) -> (a < c)
+  lt-lte-is-lt {a = Z} {c = Z} lt LTZ = lt
+  lt-lte-is-lt {a = Z} {c = Z} lt (LTS ())
+  lt-lte-is-lt {a = Z} {c = 1+ c} lt lte = LTZ
+  lt-lte-is-lt {a = 1+ a} {c = Z} lt LTZ = lt
+  lt-lte-is-lt {a = 1+ a} {c = Z} lt (LTS ())
+  lt-lte-is-lt {a = 1+ a} {b = 1+ b} {c = 1+ c} (LTS lt) (LTS lte) = LTS (lt-lte-is-lt lt lte)
+
+  trichotomy : (a b : Nat) -> (a < b + b < a + a == b)
+  trichotomy Z Z = Inr (Inr refl)
+  trichotomy (1+ a) Z = Inr (Inl LTZ)
+  trichotomy Z (1+ b) = Inl LTZ
+  trichotomy (1+ a) (1+ b) with trichotomy a b  
+  ... | Inl x = Inl (LTS x)
+  ... | Inr (Inl x) = Inr (Inl (LTS x))
+  ... | Inr (Inr x) rewrite x = Inr (Inr refl)
+
+  trichotomy-lemma : {a b : Nat} -> (a == b → ⊥) -> (a < b → ⊥) -> (b < a)
+  trichotomy-lemma {a = a} {b = b} neq nlt with trichotomy a b 
+  ... | Inl x = abort (nlt x)
+  ... | Inr (Inl x) = x
+  ... | Inr (Inr x) = abort (neq x)
+
+  _nat+_ : (n m : Nat) → Nat 
+  Z nat+ n = n 
+  (1+ n) nat+ m = 1+ (n nat+ m)
+
+  nat+Z : (n : Nat) → n nat+ Z == n
+  nat+Z Z = refl
+  nat+Z (1+ n) rewrite nat+Z n = refl
+
+  nat+1+ : (n m : Nat) → n nat+ 1+ m == 1+ (n nat+ m)
+  nat+1+ Z m = refl
+  nat+1+ (1+ n) m rewrite nat+1+ n m = refl
+
+  nat+assoc : (n m l : Nat) → n nat+ (m nat+ l) == (n nat+ m) nat+ l
+  nat+assoc Z m l = refl
+  nat+assoc (1+ n) m l rewrite nat+assoc n m l = refl
+
+  nat+comm : (n m : Nat) → n nat+ m == m nat+ n
+  nat+comm Z m rewrite nat+Z m = refl
+  nat+comm (1+ n) m rewrite nat+1+ m n rewrite nat+comm n m = refl

Prelude.agda

@@ -8,6 +8,11 @@ module Prelude where
   abort : ∀ {C : Set} → ⊥ → C
   abort ()
 
+  -- negation 
+  open import Agda.Primitive using (Level)
+  ¬_ : ∀ {ℓ : Level} → Set ℓ → Set ℓ
+  ¬ A = A → ⊥
+
   -- unit
   data ⊤ : Set where
     <> : ⊤
@@ -43,7 +48,7 @@ module Prelude where
 
   -- disequality
   _≠_ : {l : Level} {A : Set l} → (a b : A) → Set l
-  a ≠ b = (a == b) → ⊥
+  a ≠ b = ¬ (a == b)
 
   {-# BUILTIN EQUALITY _==_ #-}
 
@@ -91,3 +96,11 @@ module Prelude where
   -- non-equality is commutative
   flip : {A : Set} {x y : A} → (x == y → ⊥) → (y == x → ⊥)
   flip neq eq = neq (! eq)
+
+    -- equality is symmetric
+  sym : {A : Set} {x y : A} → (x == y) → (y == x)
+  sym refl = refl
+
+  -- bi-implication
+  _↔_ : {l1 : Level} {l2 : Level} → (Set l1) → (Set l2) → Set (lmax l1 l2)
+  a ↔ b = (a → b) × (b → a)