From 3ef53c828cadafe4c5d3f4deb943dd273fac9631 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 15 Apr 2020 13:59:36 +0200
Subject: [PATCH] new encodings of booleans, two ways

---
 encodings/bool_hol.lp   | 27 +++++++++++++++++++++++++++
 encodings/bool_pvs.lp   | 31 +++++++++++++++++++++++++++++++
 encodings/boolops_if.lp |  9 ++++-----
 sandbox/boolops_if.lp   |  9 +++++++++
 4 files changed, 71 insertions(+), 5 deletions(-)
 create mode 100644 encodings/bool_hol.lp
 create mode 100644 encodings/bool_pvs.lp
 create mode 100644 sandbox/boolops_if.lp

diff --git a/encodings/bool_hol.lp b/encodings/bool_hol.lp
new file mode 100644
index 0000000..ac2f5c1
--- /dev/null
+++ b/encodings/bool_hol.lp
@@ -0,0 +1,27 @@
+// Definition based on implication
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+definition not P ≔ impd {P} (λ_, false)
+set prefix 5 "¬" ≔ not
+
+definition imp P Q ≔ impd {P} Q
+set infix 2 "⊃" ≔ imp
+
+definition {|and|} P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
+set infix 4 "∧" ≔ {|and|}
+definition or P Q ≔ (¬ P) ⊃ Q
+set infix 3 "∨" ≔ or
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or
+
+symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule if {bool} &p &then &else → (&p ⊃ &then) ⊃ (λ_, ¬ &p ⊃ &else)
diff --git a/encodings/bool_pvs.lp b/encodings/bool_pvs.lp
new file mode 100644
index 0000000..0094145
--- /dev/null
+++ b/encodings/bool_pvs.lp
@@ -0,0 +1,31 @@
+// Close to PVS logic system: native equality,
+// true, false, and if
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+symbol eq {s: Set}: η s ⇒ η s ⇒ η bool
+set infix left 6 "=" ≔ eq
+
+definition not p ≔ eq {bool} p false
+set prefix 5 "¬" ≔ not
+
+constant symbol if {s: Set} p: (ε p ⇒ η s) ⇒ (ε (¬ p) ⇒ η s) ⇒ η s
+rule ε (if &p &then &else)
+   → (∀h: ε &p, ε (&then h)) ⇒ ∀h: ε (¬ &p), ε (&else h)
+
+definition {|and|} p q ≔ if {bool} p q (λ_, false)
+definition or p q ≔ if {bool} p (λ_, true) q
+definition imp p q ≔ if {bool} p q (λ_, true)
+set infix left 4 "∧" ≔ {|and|}
+set infix left 3 "∨" ≔ or
+set infix left 2 "⊃" ≔ imp
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "not" ≔ not
+set builtin "imp" ≔ imp
+set builtin "and" ≔ {|and|}
+set builtin "or"  ≔ or
diff --git a/encodings/boolops_if.lp b/encodings/boolops_if.lp
index e9faca7..ba1b39b 100644
--- a/encodings/boolops_if.lp
+++ b/encodings/boolops_if.lp
@@ -1,9 +1,8 @@
 // Boolean operators defined from if.
-require open
-  personoj.encodings.lhol
-  personoj.encodings.pvs_cert
-  personoj.encodings.booleans
-  personoj.encodings.if
+require open personoj.encodings.lhol
+require open  personoj.encodings.pvs_cert
+require open  personoj.encodings.booleans
+require open  personoj.encodings.if
 
 // Definition of logical connectors with if3
 definition band p q ≔ if {bool} p q (λ_, false)
diff --git a/sandbox/boolops_if.lp b/sandbox/boolops_if.lp
new file mode 100644
index 0000000..735934d
--- /dev/null
+++ b/sandbox/boolops_if.lp
@@ -0,0 +1,9 @@
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.bool_pvs
+
+theorem trivial (P: η bool): ε (P ⊃ (λ_, P))
+proof
+  assume P
+  refine λ_ _ f, f
+qed
-- 
GitLab