From 54d0e2d3d3e81fa4a1839a45ce13fba671c48ffc Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 29 Jan 2020 08:45:24 +0100
Subject: [PATCH] pvs cert proofs

---
 explicit/booleans.lp       | 14 ++++++++++++++
 prelude/booleans.lp        | 10 +++++-----
 prelude/rat_exp.lp         | 22 ++++++++++++++++++++++
 pvs-cert.lp => pvs_cert.lp | 10 +++++-----
 pvs_core.lp                |  5 ++---
 5 files changed, 48 insertions(+), 13 deletions(-)
 create mode 100644 explicit/booleans.lp
 create mode 100644 prelude/rat_exp.lp
 rename pvs-cert.lp => pvs_cert.lp (93%)

diff --git a/explicit/booleans.lp b/explicit/booleans.lp
new file mode 100644
index 0000000..bab760c
--- /dev/null
+++ b/explicit/booleans.lp
@@ -0,0 +1,14 @@
+require open pvs_cert
+
+definition bool ≔ Prop
+
+symbol r : Rule Type Prop Prop
+symbol a : Axiom Prop Type
+
+definition uProp ≔ univ Prop Type I
+
+compute Term Type uProp
+type uProp
+
+definition false ≔ prod Type Prop Prop uProp r (λ x : Term Type uProp, x)
+definition true ≔ Term Prop false ⇒ Term Prop false
diff --git a/prelude/booleans.lp b/prelude/booleans.lp
index 46ee42d..3fee8c9 100644
--- a/prelude/booleans.lp
+++ b/prelude/booleans.lp
@@ -7,13 +7,13 @@ set builtin "P" ≔ eps
 definition bool ≔ Prop
 
 // Minimal definitions, only the implication is primitive
-definition false ≔ all bool (λ p : eta bool, p)
+definition false ≔ all bool (λ p : η bool, p)
 definition true ≔ imp false false
 
-definition bnot (P: eta bool) ≔ imp P false
+definition bnot (P: η bool) ≔ imp P false
 set prefix 5 "¬" ≔ bnot
-definition band (P Q: eta bool) ≔ ¬ (imp P (¬ Q))
-definition bor (P Q: eta bool) ≔ (imp (¬ P) Q)
+definition band (P Q: η bool) ≔ ¬ (imp P (¬ Q))
+definition bor (P Q: η bool) ≔ (imp (¬ P) Q)
 set infix 6 "∧" ≔ band
 set infix 5 "∨" ≔ bor
-definition biff (P Q: eta bool) ≔ (imp P Q) ∧ (imp Q P)
+definition biff (P Q: η bool) ≔ (imp P Q) ∧ (imp Q P)
diff --git a/prelude/rat_exp.lp b/prelude/rat_exp.lp
new file mode 100644
index 0000000..94fb232
--- /dev/null
+++ b/prelude/rat_exp.lp
@@ -0,0 +1,22 @@
+require open pvs_core prelude.booleans prelude.equalities prelude.notequal
+require open prelude.nat
+require prelude.nat_ops as N
+
+constant symbol rat : Type
+constant symbol zrat : η rat
+
+definition intnz ≔ psub int (λ x, neq 0 x)
+
+symbol frac : η int ⇒ η intnz ⇒ η rat
+
+symbol times : η rat ⇒ η rat ⇒ η rat
+set infix 5 "*" ≔ times
+rule times (frac &a &b) (frac &c &d) → frac (N.times &a &c) (N.times &b &d)
+
+symbol rateq : η rat ⇒ η rat ⇒ η bool
+rule rateq (frac &a &b) (frac &c &d) → eq (N.times &a &d) (N.times &b &c)
+
+theorem right_cancellation (a : η int) (b : η intnz) :
+  ε (rateq ((frac a b) * (frac b 1)) (frac a 1))
+  proof
+  admit
diff --git a/pvs-cert.lp b/pvs_cert.lp
similarity index 93%
rename from pvs-cert.lp
rename to pvs_cert.lp
index de007d5..0030dbf 100644
--- a/pvs-cert.lp
+++ b/pvs_cert.lp
@@ -20,13 +20,13 @@ rule Rule Prop Prop Prop → True
  and Rule Type Prop Prop → True
  and Rule Type Prop Type → True  // Dependent pairs
 
-injective symbol Term : ∀ s : Sort, Univ s ⇒ TYPE
-constant symbol univ : ∀ s1 s2 : Sort, (Axiom s1 s2) ⇒ Univ s2
+injective symbol Term (s : Sort): Univ s ⇒ TYPE
+
+constant symbol univ (s1 s2 : Sort): (Axiom s1 s2) ⇒ Univ s2
+
 rule Term &s2 (univ &s1 &s2 I) → Univ &s1
 
-symbol prod :
-  ∀ s1 s2 s3 : Sort,
-  ∀ A : Univ s1,
+symbol prod (s1 s2 s3 : Sort) (A : Univ s1):
   (Rule s1 s2 s3) ⇒ (Term s1 A ⇒ Univ s2) ⇒ Univ s3
 
 rule Term &s3 (prod &s1 &s2 &s3 &A I &B) →
diff --git a/pvs_core.lp b/pvs_core.lp
index f710a0c..c54b8bb 100644
--- a/pvs_core.lp
+++ b/pvs_core.lp
@@ -38,7 +38,6 @@ symbol allIntro (A: Type) (p: eta (A ~> Prop)) (x: eta A):
 symbol allElim (A: Type) (t: eta A) (p: eta (A ~> Prop)):
   eps (all A p) ⇒ eps (p t)
 
-
 // Subtype elim 2
-symbol psubElim (A: Type) (p: eta (A ~> Prop)) (t: eta (cast (psub A p))):
-  eps (p t)
+symbol psubElim (A: Type) (p: η (A ~> Prop)) (t: η (cast (psub A p))):
+  ε (p t)
-- 
GitLab