From 1984d0fabf6bfb799fb8fae33cb5b02425144e0b Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Mon, 30 Nov 2020 12:01:55 +0100
Subject: [PATCH] Equality separated from logic, equality on pairs

---
 encodings/builtins.lp      |  1 +
 encodings/equality.lp      | 27 ++++++++++++++++++++++++++-
 encodings/logical.lp       | 25 +------------------------
 encodings/pair_equality.lp |  6 ++++++
 encodings/pvs_cert.lp      |  6 ++++++
 prelude/functions.lp       |  1 +
 prelude/logic.lp           |  1 +
 7 files changed, 42 insertions(+), 25 deletions(-)
 create mode 100644 encodings/pair_equality.lp

diff --git a/encodings/builtins.lp b/encodings/builtins.lp
index 5d46955..c09bdab 100644
--- a/encodings/builtins.lp
+++ b/encodings/builtins.lp
@@ -1,6 +1,7 @@
 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
diff --git a/encodings/equality.lp b/encodings/equality.lp
index c3a1e70..488f666 100644
--- a/encodings/equality.lp
+++ b/encodings/equality.lp
@@ -1,5 +1,30 @@
+// 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
diff --git a/encodings/logical.lp b/encodings/logical.lp
index 559ae07..161a017 100644
--- a/encodings/logical.lp
+++ b/encodings/logical.lp
@@ -1,5 +1,6 @@
 // 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
diff --git a/encodings/pair_equality.lp b/encodings/pair_equality.lp
new file mode 100644
index 0000000..976d5b3
--- /dev/null
+++ b/encodings/pair_equality.lp
@@ -0,0 +1,6 @@
+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)
diff --git a/encodings/pvs_cert.lp b/encodings/pvs_cert.lp
index bedc420..cfa4d10 100644
--- a/encodings/pvs_cert.lp
+++ b/encodings/pvs_cert.lp
@@ -1,6 +1,8 @@
 // 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
diff --git a/prelude/functions.lp b/prelude/functions.lp
index c0d6db2..e088d05 100644
--- a/prelude/functions.lp
+++ b/prelude/functions.lp
@@ -1,6 +1,7 @@
 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
 //
diff --git a/prelude/logic.lp b/prelude/logic.lp
index cd351e4..d74831b 100644
--- a/prelude/logic.lp
+++ b/prelude/logic.lp
@@ -1,6 +1,7 @@
 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
 //
-- 
GitLab