From 493112d5dfc227c5ec534206d6b1372888644470 Mon Sep 17 00:00:00 2001
From: gabrielhdt <gabrielhondet@gmail.com>
Date: Wed, 29 Jan 2020 10:35:25 +0100
Subject: [PATCH] readme and things

---
 README.md                |  9 +++++++++
 explicit/booleans.lp     | 12 +++---------
 explicit/equalities.lp   |  3 +++
 explicit/nat.lp          |  8 ++++++++
 explicit/nat_ops.lp      | 12 ++++++++++++
 explicit/notequal.lp     |  4 ++++
 explicit/pts_bindings.lp |  7 +++++++
 explicit/rat.lp          | 17 +++++++++++++++++
 pvs_cert.lp              |  2 +-
 9 files changed, 64 insertions(+), 10 deletions(-)
 create mode 100644 README.md
 create mode 100644 explicit/equalities.lp
 create mode 100644 explicit/nat.lp
 create mode 100644 explicit/nat_ops.lp
 create mode 100644 explicit/notequal.lp
 create mode 100644 explicit/pts_bindings.lp
 create mode 100644 explicit/rat.lp

diff --git a/README.md b/README.md
new file mode 100644
index 0000000..df8b4a6
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# PVS proofs
+
+Encodings of PVS and manual translations of PVS prelude. Use with `lambdapi`.
+
+## TODO
+- simplify PVS cert encoding:
+  - no `Rule` since PTS is functional,
+  - no `Type Prop Type` rule since it does not concern products but only
+    predicate subtyping.
diff --git a/explicit/booleans.lp b/explicit/booleans.lp
index bab760c..2d023db 100644
--- a/explicit/booleans.lp
+++ b/explicit/booleans.lp
@@ -1,14 +1,8 @@
-require open pvs_cert
+require open pvs_cert explicit.pts_bindings
 
 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
+
+definition bnot (P : Term Type uProp) ≔ Term Prop P ⇒ Term Prop false
diff --git a/explicit/equalities.lp b/explicit/equalities.lp
new file mode 100644
index 0000000..ad267c7
--- /dev/null
+++ b/explicit/equalities.lp
@@ -0,0 +1,3 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans
+
+symbol eq (T : Term Kind uType) : Term Type T ⇒ Term Type T ⇒ Term Type uProp
diff --git a/explicit/nat.lp b/explicit/nat.lp
new file mode 100644
index 0000000..dd2e3bc
--- /dev/null
+++ b/explicit/nat.lp
@@ -0,0 +1,8 @@
+require open pvs_cert explicit.pts_bindings
+
+constant symbol int : Term Kind uType
+symbol zero : Term Type int
+injective symbol succ : Term Type int ⇒ Term Type int
+
+set builtin "0" ≔ zero
+set builtin "+1" ≔ succ
diff --git a/explicit/nat_ops.lp b/explicit/nat_ops.lp
new file mode 100644
index 0000000..9ac3516
--- /dev/null
+++ b/explicit/nat_ops.lp
@@ -0,0 +1,12 @@
+require open pvs_cert explicit.pts_bindings explicit.nat explicit.notequal
+
+symbol times : Term Type int ⇒ Term Type int ⇒ Term Type int
+rule times &n 1 → &n
+
+set infix left 6 "*" ≔ times
+
+type λ x : Term Type int, neq int x 0
+
+symbol prod_not_zero (x y : Term Type int) :
+  Term Prop (neq int x 0) ⇒ Term Prop (neq int y 0) ⇒
+  Term Prop (neq int (x * y) 0)
diff --git a/explicit/notequal.lp b/explicit/notequal.lp
new file mode 100644
index 0000000..24df8b5
--- /dev/null
+++ b/explicit/notequal.lp
@@ -0,0 +1,4 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans
+require open explicit.equalities
+
+definition neq (T : Term Kind uType) (x y : Term Type T) ≔ bnot (eq T x y)
diff --git a/explicit/pts_bindings.lp b/explicit/pts_bindings.lp
new file mode 100644
index 0000000..9d4351a
--- /dev/null
+++ b/explicit/pts_bindings.lp
@@ -0,0 +1,7 @@
+require open pvs_cert
+
+symbol r : Rule Type Prop Prop
+symbol a : Axiom Prop Type
+
+definition uProp ≔ univ Prop Type I
+definition uType ≔ univ Type Kind I
diff --git a/explicit/rat.lp b/explicit/rat.lp
new file mode 100644
index 0000000..6088674
--- /dev/null
+++ b/explicit/rat.lp
@@ -0,0 +1,17 @@
+require open pvs_cert explicit.pts_bindings explicit.booleans explicit.equalities explicit.notequal
+
+constant symbol Nat : Term Kind uType
+symbol Nz : Term Type Nat
+symbol Nsuc : Term Type Nat ⇒ Term Type Nat
+
+constant symbol rat : Term Kind uType
+constant symbol Qz : Term Type rat
+
+definition notzero ≔ psub uProp (λ x : Term Type uProp, x)
+
+symbol frac : Term Type Nat ⇒ ∀ m : Term Type notzero, Term Type rat
+
+symbol times : Term Type rat ⇒ Term Type rat ⇒ Term Type rat
+
+rule times (frac &A (pair &B &P)) (frac &C (pair &D &Q)) →
+  frac (Nat_times &A &C) (pair (Nat_times &B &D) (Nat_prod_not_zero &B &D &P &Q))
diff --git a/pvs_cert.lp b/pvs_cert.lp
index 0030dbf..768c156 100644
--- a/pvs_cert.lp
+++ b/pvs_cert.lp
@@ -20,7 +20,7 @@ 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
+symbol Term (s : Sort): Univ s ⇒ TYPE
 
 constant symbol univ (s1 s2 : Sort): (Axiom s1 s2) ⇒ Univ s2
 
-- 
GitLab