examples for proof irrelevance, refl eq

encodings/bool_hol.lp

@@ -25,10 +25,15 @@ set builtin "or"  ≔ or
 symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule if {bool} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
+definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
+
 symbol eq {s: Set}: El s → El s → El bool
 set infix 2 "=" ≔ eq
 set builtin "eq" ≔ eq // FIXME emacs indentation
 
 rule Prf ($x = $y) ↪ Πp: El (_ ~> bool), Prf (p $x) → Prf (p $y)
-
-definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
+theorem eq_refl {a: Set} (x: El a): Prf (x = x)
+proof
+  assume a x p h
+  apply h
+qed

paper/proof_irr.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_hol
+
+
+set declared "ℕ"
+constant symbol ℕ: Set
+constant symbol z: El ℕ
+constant symbol s (_: El ℕ): El ℕ
+constant symbol leq: El ℕ → El ℕ → Bool
+set infix left 3 "≤" ≔ leq
+
+// Agda manual
+symbol p1: Prf (z ≤ s z)
+symbol p2: Prf (z ≤ s z)
+definition bounded (k: El ℕ) ≔ psub (λn, n ≤ k)
+
+constant symbol slist (bound: El ℕ): Set
+constant symbol snil (bound: El ℕ): El (slist bound)
+constant symbol scons {bound: El ℕ} (head: El (bounded bound))
+                      (tail: El (slist (fst head)))
+              : El (slist bound)
+
+set declared "l₁"
+set declared "l₂"
+definition l₁: El (slist (s z)) ≔ scons (pair z p1) (snil z)
+definition l₂: El (slist (s z)) ≔ scons (pair z p2) (snil z)
+
+theorem listeq: Prf (l₁ = l₂)
+proof
+  refine eq_refl l₁
+qed
+
+// Proof irrelevance without K
+symbol plus: El ℕ → El ℕ → El ℕ
+set infix left 10 "+" ≔ plus
+
+constant symbol even_p: El ℕ → Bool
+definition even ≔ psub even_p
+
+symbol plus_closed_even (n m: El even): Prf (even_p ((fst n) + (fst m)))
+
+definition add (n m: El even) : El even
+         ≔ pair ((fst n) + (fst m)) (plus_closed_even n m)
+
+symbol app_thm (a b: Set) (f: El (a ~> b))
+               (x y: El a) (_: Prf (x = y))
+     : Prf (f x = f y)
+
+symbol fun_ext (a b: Set) (f g: El (a ~> b)) (_: Prf (∀ (λx, f x = g x))): Prf (f = g)
+
+symbol plus_commutativity (n m: El ℕ): Prf (n + m = m + n)
+
+theorem even_add_commutativity (n m: El even): Prf (add n m = add m n)
+proof
+admit