true encoding of prelude

encodings/equality.lp

 require open personoj.encodings.lhol
 
-symbol equal {T: Set}: η T ⇒ η T ⇒ Bool
-set infix left 6 "=" ≔ equal
-set builtin "T" ≔ η
-set builtin "P" ≔ ε
-set builtin "eq" ≔ equal
+symbol eq {T: Set}: η T ⇒ η T ⇒ Bool
+set infix left 6 "=" ≔ eq
+set builtin "eq" ≔ eq

encodings/if.lp

+require open personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.subtype
+
+symbol if {U: Set} {V: Set} (S: Set)
+: ε (U ⊑ S) ⇒ ε (V ⊑ S) ⇒ Bool ⇒ η U ⇒ η V ⇒ η S

encodings/lazy.lp

@@ -2,9 +2,6 @@ require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
 
-symbol or: Bool ⇒ Bool ⇒ Bool
-symbol {|and|}: Bool ⇒ Bool ⇒ Bool
-
 definition false ≔ forall {bool} (λx, x)
 definition true ≔ impd {false} (λ_, false)
 
@@ -30,7 +27,7 @@ set builtin "and" ≔ band
 set builtin "or"  ≔ bor
 
 // Lazy reduction rules
-rule or true → λ_, true
-rule or false → λx, x
-rule {|and|} true → λx, x
-rule {|and|} false → λ_, false
+//rule bor true → λ_, true
+//rule bor false → λx, x
+//rule band true → λx, x
+//rule band false → λ_, false

encodings/prenex.lp

@@ -7,5 +7,8 @@ symbol χ: Scheme ⇒ TYPE
 symbol ∇: Set ⇒ Scheme
 rule χ (∇ &X) → η &X
 
-symbol forall_pt: (Set ⇒ Scheme) ⇒ Scheme
-rule χ (forall_pt &p) → ∀T: Set, χ (&p T)
+symbol forallp_scheme: (Set ⇒ Scheme) ⇒ Scheme
+rule χ (forallp_scheme &p) → ∀T: Set, χ (&p T)
+
+symbol forallp_bool: (Set ⇒ Bool) ⇒ Bool
+rule ε (forallp_bool &P) → ∀x: Set, ε (&P x)

prelude/logic2.lp

+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+  personoj.encodings.equality
+  personoj.encodings.prenex
+  personoj.encodings.if
+  personoj.encodings.lazy
+  personoj.encodings.subtype
+
+definition neq {T: Set} (x y: η T) ≔ bnot (eq x y)
+set infix left 6 "/=" ≔ neq
+set infix left 6 "≠" ≔ neq
+
+
+//
+// boolean_props
+//
+constant symbol bool_exclusive: ε (neq {bool} false true)
+constant symbol bool_inclusive
+: ε (forall {bool} (λx, ((eq {bool} x false) ∨ (eq {bool} x true))))
+
+compute ε (forall {bool} (λx, ((eq {bool} x false) ∨ (eq {bool} x true))))
+
+theorem excluded_middle: ε (forall {bool} (λx, x ∨ ¬ x))
+proof
+admit
+
+//
+// xor_def
+//
+definition xor (a b: η bool) ≔ neq {bool} a b
+theorem xor_def
+: ε (forall {bool}
+     (λa,
+      (forall {bool} (λb, eq {bool}
+                             (xor a b)
+                             (if {bool} {bool} bool
+                              (Refl bool) (Refl bool)
+                              a (bnot b) b)))))
+proof
+  simpl
+admit
+
+//
+// Quantifier props
+//
+set declared "∃"
+// Declared as a lemma in the prelude
+definition ∃ {T: Set} (P: η T ⇒ η bool) ≔ ¬ (forall (λx, ¬ (P x)))
+
+//
+// Defined types
+//
+definition pred (T: Set) ≔ arrd {T} (λ_, bool)
+definition PRED ≔ pred
+definition predicate ≔ pred
+definition PREDICATE ≔ pred
+definition setof ≔ pred
+definition SETOF ≔ pred
+
+symbol reflexivity_of_equal: ε (forallp_bool (λT, forall {T} (λx, eq x x)))
+set builtin "refl" ≔ reflexivity_of_equal
+
+symbol transitivity_of_equal
+: ε (forallp_bool
+     (λT, forall
+          {T} (λx, forall
+                   {T} (λy, forall
+                            {T} (λz, (imp ((x = y) ∧ (y = z)) (x = z)))))))
+
+symbol symmetry_of_equal
+: ε (forallp_bool
+     (λT, forall
+          {T} (λx, forall
+                   {T} (λy, (imp (x = y) (y = x))))))
+
+//
+// if_props
+//
+theorem lift_if1
+: ε (forallp_bool
+     (λs,
+      (forallp_bool
+       (λt,
+        (forall
+         {bool} (λa,
+                 forall
+                 {s} (λx,
+                      forall
+                      {s} (λy,
+                           forall
+                           {s ~> t}
+                           (λf, eq
+                                (f (if s (Refl s) (Refl s) a x y))
+                                (if t (Refl t) (Refl t) a (f x) (f y)))))))))))
+proof
+admit