Updated to lambdapi

encodings/bool_plus.lp

@@ -3,16 +3,18 @@ require open personoj.encodings.prenex
 require open personoj.encodings.logical
 
 // It may be generalisable to dependent propositions
-theorem and_intro:
+opaque
+symbol and_intro:
   Prf
   (∀ {prop} (λa,
    ∀ {prop} (λb,
-   a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b))))))
-proof
+   a ⊃ (λ_, b ⊃ (λ_, a ∧ (λ_, b)))))) ≔
+begin
   assume A B h0 h1 f
   refine f h0 h1
-qed
+end
 
-theorem and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a
-proof
+opaque
+symbol and_elim_1 a b (_: Prf (a ∧ (λ_, b))): Prf a ≔
+begin
 admit

encodings/builtins.lp

@@ -24,11 +24,11 @@ constant symbol str_empty: El {|!String!|}
 constant symbol str_cons: El {|!Number!|} → El {|!String!|} → El {|!String!|}
 
 set declared "∃"
-definition ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λx, ¬ (P x)))
+symbol ∃ {T: Set} (P: El T → El prop) ≔ ¬ (∀ (λx, ¬ (P x)))
 
 symbol propositional_extensionality:
   Prf (∀ {prop} (λp, (∀ {prop} (λq, (iff p q) ⊃ (λ_, eq {prop} p q)))))
 
-definition neq {t} x y ≔ ¬ (eq {t} x y)
+symbol neq {t} x y ≔ ¬ (eq {t} x y)
 set infix left 2 "/=" ≔ neq
 set infix left 2 "≠" ≔ neq

encodings/equality.lp

@@ -8,23 +8,25 @@ symbol eq {T: Set}: El T → El T → Prop
 set infix left 2 "=" ≔ eq
 set builtin "eq" ≔ eq
 
-definition neq {s: Set} (x y: El s) ≔ ¬ (x = y)
+symbol neq {s: Set} (x y: El s) ≔ ¬ (x = y)
 set infix 2 "≠" ≔ neq
 
 // Leibniz equality
 rule Prf ($x = $y) ↪ Πp: El (_ ~> prop), Prf (p $x) → Prf (p $y)
 
 // Some theorems for equality
-theorem eq_refl {a: Set} (x: El a): Prf (x = x)
-proof
+opaque
+symbol eq_refl {a: Set} (x: El a): Prf (x = x) ≔
+begin
   assume a x p h
   apply h
-qed
+end
 set builtin "refl" ≔ eq_refl
 
-theorem eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
-      : Prf (x = z)
-proof
+opaque
+symbol eq_trans {a: Set} (x y z: El a) (_: Prf (x = y)) (_: Prf (y = z))
+      : Prf (x = z) ≔
+begin
   assume a x y z hxy hyz p px
   refine hyz p (hxy p px)
-qed
+end

encodings/equality_tup.lp

@@ -7,4 +7,4 @@ require open personoj.encodings.logical
 // Equality operates on the maximal supertype. It allows to profit
 // from predicate subtyping for free in the propositional equality.
 symbol eq {t: Set} (_: El (T.t (μ t) (μ t))): Prop
-definition neq {t} m ≔ ¬ (@eq t m)
+symbol neq {t} m ≔ ¬ (@eq t m)

encodings/if.lp

@@ -3,22 +3,22 @@
 require open personoj.encodings.lhol
 require open personoj.encodings.pvs_cert
 
-definition false ≔ ∀ {prop} (λx, x)
-definition true ≔ impd {false} (λ_, false)
+symbol false ≔ ∀ {prop} (λx, x)
+symbol true ≔ impd {false} (λ_, false)
 
 symbol eq {s: Set}: El s → El s → El prop
 set infix left 6 "=" ≔ eq
 
-definition not p ≔ eq {prop} p false
+symbol not p ≔ eq {prop} p false
 set prefix 5 "¬" ≔ not
 
 constant symbol if {s: Set} p: (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule Prf (if $p $then $else)
    ↪ (Πh: Prf $p, Prf ($then h)) → Πh: Prf (¬ $p), Prf ($else h)
 
-definition and p q ≔ if {prop} p q (λ_, false)
-definition or p q ≔ if {prop} p (λ_, true) q
-definition imp p q ≔ if {prop} p q (λ_, true)
+symbol and p q ≔ if {prop} p q (λ_, false)
+symbol or p q ≔ if {prop} p (λ_, true) q
+symbol imp p q ≔ if {prop} p q (λ_, true)
 set infix left 4 "∧" ≔ and
 set infix left 3 "∨" ≔ or
 set infix left 2 "⊃" ≔ imp

encodings/logical.lp

 // Definition based on implication
 require open personoj.encodings.lhol
 
-definition false ≔ ∀ {prop} (λx, x)
-definition true ≔ impd {false} (λ_, false)
+symbol false ≔ ∀ {prop} (λx, x)
+symbol true ≔ impd {false} (λ_, false)
 
-definition not P ≔ impd {P} (λ_, false)
+symbol not P ≔ impd {P} (λ_, false)
 set prefix 5 "¬" ≔ not
 
-definition imp P Q ≔ impd {P} Q
+symbol imp P Q ≔ impd {P} Q
 set infix 2 "⊃" ≔ imp
 
-definition and P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
+symbol and P Q ≔ ¬ (P ⊃ (λh, ¬ (Q h)))
 set infix 4 "∧" ≔ and
-definition or P Q ≔ (¬ P) ⊃ Q
+symbol or P Q ≔ (¬ P) ⊃ Q
 set infix 3 "∨" ≔ or
 
 set builtin "bot" ≔ false
@@ -25,4 +25,4 @@ set builtin "or"  ≔ or
 symbol if {s: Set} (p: Prop): (Prf p → El s) → (Prf (¬ p) → El s) → El s
 rule if {prop} $p $then $else ↪ ($p ⊃ $then) ⊃ (λ_, (¬ $p) ⊃ $else)
 
-definition iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))
+symbol iff P Q ≔ (P ⊃ (λ_, Q)) ∧ ((λ_, Q ⊃ (λ_, P)))

encodings/pvs_cert.lp

@@ -10,8 +10,8 @@ symbol fst: Π{t: Set} {p: El t → Prop}, El (psub p) → El t
 symbol snd {t: Set}{p: El t → Prop} (m: El (psub p)): Prf (p (fst m))
 
 // Proof irrelevance
-definition pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
-         ≔ pair' t p m
+symbol pair {t: Set} {p: El t → Prop} (m: El t) (_: Prf (p m))
+     ≔ pair' t p m
 
 rule fst (pair' _ _ $M) ↪ $M
 

prelude/logic.lp

@@ -33,25 +33,25 @@ constant symbol prop_exclusive: Prf (neq {prop} false true)
 constant symbol prop_inclusive:
   Prf (∀ {prop} (λa, ((eq {prop} a false) ∨ (λ_, eq {prop} a true))))
 
-theorem excluded_middle: Prf (∀ {prop} (λa, a ∨ (λ_, ¬ a)))
-proof
+opaque
+symbol excluded_middle: Prf (∀ {prop} (λa, a ∨ (λ_, ¬ a)))
+≔ begin
   assume x f
   refine f
-qed
+end
 
 //
 // xor_def
 //
-definition xor (a b: El prop) ≔ neq {prop} a b
+symbol xor (a b: El prop) ≔ neq {prop} a b
 
 // PVS solves that kind of things thanks to the (bddsimp) tactic which uses an
 // external C program
-theorem xor_def:
+opaque
+symbol xor_def:
   Prf (∀ {prop} (λa, ∀ {prop} (λb, eq {prop} (xor a b)
                                     (if {prop} a (λ_, ¬ b) (λ_, b)))))
-proof
-  set prover "Alt-Ergo"
-  set prover_timeout 12
+≔ begin
   assume a b p
   simpl
   assume hxor
@@ -61,12 +61,12 @@ admit
 //
 // Defined types
 //
-definition pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> prop
-definition PRED ≔ pred
-definition predicate ≔ pred
-definition PREDICATE ≔ pred
-definition setof ≔ pred
-definition SETOF ≔ pred
+symbol pred: El_k (∀K (λ_, scheme_k {|set|})) ≔ λt, t ~> prop
+symbol PRED ≔ pred
+symbol predicate ≔ pred
+symbol PREDICATE ≔ pred
+symbol setof ≔ pred
+symbol SETOF ≔ pred
 
 //
 // exists1
@@ -82,9 +82,11 @@ constant
 symbol If_false
      : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
 
-theorem if_same
+opaque
+symbol if_same
       : Prf (∀B (λt, ∀ {prop} (λb, ∀ (λx: El t, if b (λ_, x) (λ_, x) = x))))
-proof
+      ≔
+begin
 admit
 
 constant symbol reflexivity_of_equals: Prf (∀B (λt, ∀ (λx: El t, x = x)))
@@ -101,18 +103,20 @@ symbol symmetry_of_equals
      : Prf (∀B (λt, ∀ (λx: El t, (∀ (λy: El t, (x = y) ⊃ (λ_, y = x))))))
 
 // Not in prelude!
-theorem eqind {t} x y: Prf (x = y) → Πp: El t → Prop, Prf (p y) → Prf (p x)
-proof
+opaque
+symbol eqind {t} x y: Prf (x = y) → Πp: El t → Prop, Prf (p y) → Prf (p x)
+≔ begin
   assume t x y heq
   apply symmetry_of_equals t x y heq
-qed
+end
 set builtin "eqind" ≔ eqind
 
 //
 // if_props
 //
 
-theorem lift_if1:
+opaque
+symbol lift_if1:
   Prf (∀B (λs: Ty {|set|},
            ∀B (λt: Ty {|set|},
                  ∀ {prop}
@@ -122,10 +126,11 @@ theorem lift_if1:
                                 ∀ (λf: El (s ~> t),
                                      f (if a (λ_, x) (λ_, y))
                                      = if a (λ_, f x) (λ_, f y))))))))
-proof
+≔ begin
 admit
 
-theorem lift_if2:
+opaque
+symbol lift_if2:
   Prf (∀B (λs,
            ∀ {prop}
              (λa,
@@ -141,5 +146,5 @@ theorem lift_if2:
                                      = if a
                                        (λ_, if b (λ_, x) (λ_, y))
                                        (λ_, if c (λ_, x) (λ_, y)))))))))
-proof
+≔ begin
 admit