From 2bd35f8f0b1c575eafc20a041dfb5d5dd07fe485 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 8 Apr 2020 17:26:45 +0200
Subject: [PATCH] laziness, booleans

---
 adlib/booleans.lp    | 27 +++++++++++++++++++++++++++
 encodings/lazy.lp    | 33 ++++++++-------------------------
 encodings/subtype.lp | 10 +++++-----
 prelude/logic2.lp    |  8 ++++----
 4 files changed, 44 insertions(+), 34 deletions(-)
 create mode 100644 adlib/booleans.lp

diff --git a/adlib/booleans.lp b/adlib/booleans.lp
new file mode 100644
index 0000000..528c4cc
--- /dev/null
+++ b/adlib/booleans.lp
@@ -0,0 +1,27 @@
+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
diff --git a/encodings/lazy.lp b/encodings/lazy.lp
index 067cbfa..80b424b 100644
--- a/encodings/lazy.lp
+++ b/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)
diff --git a/encodings/subtype.lp b/encodings/subtype.lp
index 7fa435b..6f27ed9 100644
--- a/encodings/subtype.lp
+++ b/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
diff --git a/prelude/logic2.lp b/prelude/logic2.lp
index d0a1d7e..d2803a3 100644
--- a/prelude/logic2.lp
+++ 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
-- 
GitLab