neq and fix

encodings/bool_hol.lp

@@ -30,6 +30,8 @@ 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
+definition neq {s: Set} (x y: El s) ≔ ¬ (x = y)
+set infix 2 "≠" ≔ neq
 
 // Leibniz equality
 rule Prf ($x = $y) ↪ Πp: El (_ ~> bool), Prf (p $x) → Prf (p $y)
@@ -42,7 +44,8 @@ proof
 qed
 set builtin "refl" ≔ eq_refl
 
-theorem eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z)): Prf (x = z)
+theorem eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
+      : Prf (x = z)
 proof
   assume a x y z hxy hyz p px
   refine hyz p (hxy p px)

paper/proof_irr.lp

@@ -31,18 +31,15 @@ proof
   refine eq_refl l₁
 qed
 
+constant symbol even_p: El ℕ → Bool
+definition even ≔ psub even_p
+
 // Proof irrelevance without K
-// We need the following axiom for pairs
-symbol app_pair {a b: Set} (x y: El a) (p: El a → Bool)
-                (hx: Prf (p x)) (hy: Prf (p y)) (_: Prf (x = y))
-     : Prf (@pair _ p x hx = @pair _ p y hy)
+definition eqEven (e1 e2: El even) ≔ fst e1 = fst e2
 
 symbol plus: El ℕ → El ℕ → El ℕ
 set infix left 10 "+" ≔ plus
 
-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
@@ -50,15 +47,8 @@ definition add (n m: El even) : El even
 
 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)
+theorem even_add_commutativity (n m: El even): Prf (eqEven (add n m) (add m n))
 proof
   assume n m
-  refine app_pair (fst n + fst m) (fst m + fst n) even_p _ _ _
-  refine ℕ
-  // fst n + fst m is even
-  refine plus_closed_even n m
-  // fst m + fst n is even
-  refine plus_closed_even m n
-  // fst n + m = fst m + n
   refine plus_commutativity (fst n) (fst m)
 qed