laziness, booleans

adlib/booleans.lp

+require open
+  personoj.encodings.lhol
+  personoj.encodings.pvs_cert
+
+definition false ≔ forall {bool} (λx, x)
+definition true ≔ impd {false} (λ_, false)
+
+definition imp P Q ≔ impd {P} (λ_, Q)
+
+definition bnot P ≔ impd {P} (λ_, false)
+definition band P Q ≔ bnot (imp P (bnot Q))
+definition bor P Q ≔ imp (bnot P) Q
+set prefix 5 "¬" ≔ bnot
+set infix 6 "∧" ≔ band
+set infix 5 "∨" ≔ bor
+
+definition biff P Q ≔ (imp P Q) ∧ (imp Q P)
+set infix 7 "⇔" ≔ biff
+
+definition when P Q ≔ imp Q P
+
+set builtin "bot" ≔ false
+set builtin "top" ≔ true
+set builtin "imp" ≔ imp
+set builtin "not" ≔ bnot
+set builtin "and" ≔ band
+set builtin "or"  ≔ bor

encodings/lazy.lp

@@ -2,32 +2,15 @@ require open
   personoj.encodings.lhol
   personoj.encodings.pvs_cert
 
-definition false ≔ forall {bool} (λx, x)
-definition true ≔ impd {false} (λ_, false)
+constant symbol delayed: Set ⇒ TYPE
+constant symbol quote {T: Set}: η T ⇒ delayed T
 
-definition imp P Q ≔ impd {P} (λ_, Q)
+constant symbol s_app: Set ⇒ Set ⇒ Set
 
-definition bnot P ≔ impd {P} (λ_, false)
-definition band P Q ≔ bnot (imp P (bnot Q))
-definition bor P Q ≔ imp (bnot P) Q
-set prefix 5 "¬" ≔ bnot
-set infix 6 "∧" ≔ band
-set infix 5 "∨" ≔ bor
+constant symbol app {T: Set} {S: Set}
+: delayed T ⇒ delayed S ⇒ delayed (s_app T S)
 
-definition biff P Q ≔ (imp P Q) ∧ (imp Q P)
-set infix 7 "⇔" ≔ biff
+symbol unquote {T: Set}: delayed T ⇒ η T
 
-definition when P Q ≔ imp Q P
-
-set builtin "bot" ≔ false
-set builtin "top" ≔ true
-set builtin "imp" ≔ imp
-set builtin "not" ≔ bnot
-set builtin "and" ≔ band
-set builtin "or"  ≔ bor
-
-// Lazy reduction rules
-//rule bor true → λ_, true
-//rule bor false → λx, x
-//rule band true → λx, x
-//rule band false → λ_, false
+rule unquote (quote &x) → &x
+rule unquote {&S} (app {&T ~> &S} {&T} &t &u) → (unquote &t) (unquote &u)

encodings/subtype.lp

@@ -4,13 +4,13 @@ require open personoj.encodings.pvs_cert
 symbol subtype : Set ⇒ Set ⇒ Bool
 set infix left 6 "⊑" ≔ subtype
 
-symbol Refl (a: Set): ε (a ⊑ a)
-symbol Trans (s t u: Set): ε (s ⊑ t) ⇒ ε (t ⊑ u) ⇒ ε (s ⊑ u)
+symbol S_Refl (a: Set): ε (a ⊑ a)
+symbol S_Trans (s t u: Set): ε (s ⊑ t) ⇒ ε (t ⊑ u) ⇒ ε (s ⊑ u)
 
-symbol Restr {a: Set} (p: η a ⇒ Bool): ε (psub p ⊑ a)
+symbol S_Restr {a: Set} (p: η a ⇒ Bool): ε (psub p ⊑ a)
 
-symbol Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
-symbol Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
+symbol S_Arr (t u1 u2: Set): ε (u1 ⊑ u2) ⇒ ε ((t ~> u1) ⊑ (t ~> u2))
+symbol S_Darr (d: Set) (r1: η d ⇒ Set) (r2: η d ⇒ Set)
 : ε (forall (λx, (r1 x) ⊑ (r2 x))) ⇒ ε ((arrd r1) ⊑ (arrd r2))
 
 symbol upcast {A: Set} {B: Set}: ε (A ⊑ B) ⇒ η A ⇒ η B

prelude/logic2.lp

@@ -4,7 +4,7 @@ require open
   personoj.encodings.equality
   personoj.encodings.prenex
   personoj.encodings.if
-  personoj.encodings.lazy
+  personoj.adlib.booleans
   personoj.encodings.subtype
 
 definition neq {T: Set} (x y: η T) ≔ bnot (eq x y)
@@ -35,7 +35,7 @@ theorem xor_def
       (forall {bool} (λb, eq {bool}
                              (xor a b)
                              (if {bool} {bool} bool
-                              (Refl bool) (Refl bool)
+                              (S_Refl bool) (S_Refl bool)
                               a (bnot b) b)))))
 proof
   simpl
@@ -91,7 +91,7 @@ theorem lift_if1
                            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)))))))))))
+                                (f (if s (S_Refl s) (S_Refl s) a x y))
+                                (if t (S_Refl t) (S_Refl t) a (f x) (f y)))))))))))
 proof
 admit