boolops tests

encodings/boolops_if.lp

+// 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

encodings/boolops_imp.lp

+// 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

sandbox/boolops.lp

+// 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)