Equality separated from logic, equality on pairs

encodings/builtins.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 require open personoj.encodings.prenex
 
 constant symbol {|!Number!|}: Set

encodings/equality.lp

+// Usual prenex polymorphic equaltiy, with two arguments
 require open personoj.encodings.lhol
+require open personoj.encodings.logical
+require open personoj.encodings.prenex
 
+// We don't use prenex encoding to have implicit arguments.
 symbol eq {T: Set}: El T → El T → Bool
-set infix left 6 "=" ≔ eq
+set infix left 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)
+
+// Some theorems for equality
+theorem eq_refl {a: Set} (x: El a): Prf (x = x)
+proof
+  assume a x p h
+  apply h
+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)
+proof
+  assume a x y z hxy hyz p px
+  refine hyz p (hxy p px)
+qed

encodings/logical.lp

 // Definition based on implication
 require open personoj.encodings.lhol
+require open personoj.encodings.pairs
 
 definition false ≔ ∀ {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
@@ -26,27 +27,3 @@ 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
-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)
-
-// Some theorems for equality
-theorem eq_refl {a: Set} (x: El a): Prf (x = x)
-proof
-  assume a x p h
-  apply h
-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)
-proof
-  assume a x y z hxy hyz p px
-  refine hyz p (hxy p px)
-qed

encodings/pair_equality.lp

+require open personoj.encodings.lhol
+require open personoj.encodings.pairs
+require open personoj.encodings.logical
+
+symbol peq {t: Set} (_: El (σ t t)): Bool
+definition pneq  {t: Set} (m: El (σ t t)) ≔ ¬ (@peq t m)

encodings/pvs_cert.lp

 // PVS-Cert
 require open personoj.encodings.lhol
 
+set declared "μ"
+
 constant symbol psub {x: Set}: (El x → Bool) → Set
 protected symbol pair': Π(t: Set) (p: El t → Bool), El t → El (psub p)
 symbol fst: Π{t: Set} {p: El t → Bool}, El (psub p) → El t
@@ -12,3 +14,7 @@ definition pair {t: Set} {p: El t → Bool} (m: El t) (_: Prf (p m))
          ≔ pair' t p m
 
 rule fst (pair' _ _ $M) ↪ $M
+
+symbol μ (_: Set): Set
+rule μ (@psub $t _) ↪ μ $t
+with μ bool ↪ bool

prelude/functions.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 require open personoj.encodings.prenex
 require open personoj.prelude.logic
 //

prelude/logic.lp

 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 require open personoj.encodings.logical
+require open personoj.encodings.equality
 require open personoj.encodings.prenex
 require open personoj.encodings.builtins
 //