app_pair

paper/proof_irr.lp

@@ -32,6 +32,11 @@ proof
 qed
 
 // 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)
+
 symbol plus: El ℕ → El ℕ → El ℕ
 set infix left 10 "+" ≔ plus
 
@@ -52,5 +57,30 @@ symbol fun_ext (a b: Set) (f g: El (a ~> b)) (_: Prf (∀ (λx, f x = g x))): Pr
 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
+  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
+
+// Toy example
+set declared "n₀"
+set declared "n₁"
+symbol n₀: El ℕ
+symbol n₁: El ℕ
+
+symbol nz_eq_no: Prf (n₀ = n₁)
+symbol pred: El ℕ → Bool
+symbol pq0: Prf (pred n₀)
+symbol pq1: Prf (pred n₁)
+
+definition ps ≔ psub pred
+theorem thethm: Prf (@pair ℕ pred n₀ pq0 = @pair ℕ pred n₁ pq1)
 proof
 admit