readme and things

README.md

+# 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.

explicit/booleans.lp

-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

explicit/equalities.lp

+require open pvs_cert explicit.pts_bindings explicit.booleans
+
+symbol eq (T : Term Kind uType) : Term Type T ⇒ Term Type T ⇒ Term Type uProp

explicit/nat.lp

+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

explicit/nat_ops.lp

+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)

explicit/notequal.lp

+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)

explicit/pts_bindings.lp

+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

explicit/rat.lp

+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))

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