From f57f9646a7dd07cb247181c47847231395014eec Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Tue, 14 Apr 2020 17:18:41 +0200
Subject: [PATCH] boolops tests

---
 encodings/boolops_if.lp  | 14 ++++++++++++++
 encodings/boolops_imp.lp | 22 ++++++++++++++++++++++
 sandbox/boolops.lp       | 25 +++++++++++++++++++++++++
 3 files changed, 61 insertions(+)
 create mode 100644 encodings/boolops_if.lp
 create mode 100644 encodings/boolops_imp.lp
 create mode 100644 sandbox/boolops.lp

diff --git a/encodings/boolops_if.lp b/encodings/boolops_if.lp
new file mode 100644
index 0000000..e9faca7
--- /dev/null
+++ b/encodings/boolops_if.lp
@@ -0,0 +1,14 @@
+// Boolean operators defined from if.
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.booleans
+  personoj.encodings.if
+
+// Definition of logical connectors with if3
+definition band p q ≔ if {bool} p q (λ_, false)
+definition bor p q ≔ if {bool} p (λ_, true) q
+definition imp p q ≔ if {bool} p q (λ_, true)
+set infix left 7 "∧" ≔ band
+set infix left 6 "∧" ≔ bor
+set infix left 5 "⊃" ≔ imp
diff --git a/encodings/boolops_imp.lp b/encodings/boolops_imp.lp
new file mode 100644
index 0000000..ed11e1f
--- /dev/null
+++ b/encodings/boolops_imp.lp
@@ -0,0 +1,22 @@
+// Boolean operators defined from dependent implication.
+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.booleans
+
+definition imp P Q ≔ impd {P} (λ_, Q)
+set infix 4 "⊃" ≔ imp
+
+definition band P Q ≔ ¬ (P ⊃ (¬ Q))
+definition bor P Q ≔ (¬ P) ⊃ Q
+set infix 6 "∧" ≔ band
+set infix 5 "∨" ≔ bor
+
+definition biff P Q ≔ (P ⊃ Q) ∧ (Q ⊃ P)
+set infix 7 "⇔" ≔ biff
+
+definition when P Q ≔ Q ⊃ P
+
+set builtin "imp" ≔ imp
+set builtin "and" ≔ band
+set builtin "or"  ≔ bor
diff --git a/sandbox/boolops.lp b/sandbox/boolops.lp
new file mode 100644
index 0000000..7e3f415
--- /dev/null
+++ b/sandbox/boolops.lp
@@ -0,0 +1,25 @@
+// Compute the term [⊥ ⊃ 1 / 0 = 1 / 0]. The principle is that [1/0] is well
+// typed because in the right part of the implication, false is assumed.
+require open personoj.encodings.lhol
+require open personoj.encodings.pvs_cert
+require open personoj.encodings.equality
+require open personoj.encodings.booleans
+
+symbol imp: ∀P: Bool, (ε P ⇒ η bool) ⇒ η bool
+set infix left 6 "⊃" ≔ imp
+
+require personoj.paper.rat as Q
+
+set builtin "0" ≔ Q.Z
+set builtin "+1" ≔ Q.S
+
+theorem zisnotz (h: ε false): ε (Q.{|nznat?|} 0)
+proof
+  assume Hf _
+  refine Hf
+qed
+
+// Computes ⊥ ⊃ (1 / 0) = 1 / 0
+compute false ⊃ (λh,
+                 let ooz ≔ Q.div 1 (pair 0 (zisnotz h)) in
+                 eq ooz ooz)
-- 
GitLab