From 136041e3f5e1860f6b9ca6bb8f91d4bd19cd4f61 Mon Sep 17 00:00:00 2001
From: hondet <gabrielhondet@gmail.com>
Date: Tue, 9 Feb 2021 15:35:38 +0100
Subject: [PATCH] Updated to new lambdapi
---
.github/workflows/type_check.yml | 9 +-
Makefile | 11 +--
README.md | 12 ++-
paper/rat.lp | 140 +++++++++++++++--------------
prelude/functions.lp | 67 --------------
prelude/logic.lp | 150 -------------------------------
6 files changed, 91 insertions(+), 298 deletions(-)
delete mode 100644 prelude/functions.lp
delete mode 100644 prelude/logic.lp
diff --git a/.github/workflows/type_check.yml b/.github/workflows/type_check.yml
index 79055bb..5887ef6 100644
--- a/.github/workflows/type_check.yml
+++ b/.github/workflows/type_check.yml
@@ -40,6 +40,7 @@ jobs:
opam pin add alt-ergo 2.3.1
git clone https://github.com/Deducteam/lambdapi.git lambdapi
(cd lambdapi || exit 1
+ git checkout 3e5c7ee2388d233fdca05776009b5cb158e48d97
opam pin add lambdapi .)
opam install lambdapi
eval $(opam env)
@@ -50,10 +51,10 @@ jobs:
eval $(opam env)
lambdapi check encodings/*.lp
- # - name: check paper
- # run: |
- # eval $(opam env)
- # lambdapi check paper/*.lp
+ - name: check paper
+ run: |
+ eval $(opam env)
+ lambdapi check paper/*.lp
# - name: check prelude
# run: |
diff --git a/Makefile b/Makefile
index 5c656bc..ff9c3c7 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,6 @@
LP = lambdapi
-LP_SRC != find encodings -type f -name "*.lp"
+LP_FLAGS = -v0 -w
+LP_SRC != find encodings paper -type f -name "*.lp"
LP_OBJ = ${LP_SRC:S/.lp$/.lpo/}
.SUFFIXES: .lpo .lp
@@ -7,15 +8,15 @@ LP_OBJ = ${LP_SRC:S/.lp$/.lpo/}
all: ${LP_OBJ}
.lp.lpo:
- ${LP} check --gen-obj $<
+ ${LP} check ${LP_FLAGS} --gen-obj $<
.PHONY: install
-install: ${LP_OBJ} lambdapi.pkg
- ${LP} install lambdapi.pkg ${LP_SRC}
+install: lambdapi.pkg
+ ${LP} install ${LP_FLAGS} lambdapi.pkg ${LP_SRC}
.PHONY: uninstall
uninstall:
- ${LP} uninstall lambdapi.pkg
+ ${LP} uninstall ${LP_FLAGS} lambdapi.pkg
.PHONY: clean
clean:
diff --git a/README.md b/README.md
index 50c7be9..c3d6f59 100644
--- a/README.md
+++ b/README.md
@@ -15,13 +15,19 @@ library, also known as _Prelude_. The prelude is available
## Requirements
[`lambdapi`](https://github.com/Deducteam/lambdapi.git) later than
-fda8752584af52cdc8158a7a80bbe7fce5720616
+3e5c7ee2388d233fdca05776009b5cb158e48d97,
+
+``` sh
+git clone github.com/Deducteam/lambdapi.git
+git checkout 3e5c7ee2388d233fdca05776009b5cb158e48d97
+make
+make install
+```
## Structure
-- `adlib`: additional libraries not in the prelude
- `encodings`: encoding of PVS into Dedukti
-- `prelude`: parts of the PVS prelude
+- `paper`: some specifications presented in papers
- `sandbox`: miscellaneous experiments
- `tools`: some additional scripts and utilities
diff --git a/paper/rat.lp b/paper/rat.lp
index f9c78a8..4d8af9d 100644
--- a/paper/rat.lp
+++ b/paper/rat.lp
@@ -1,100 +1,102 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
+require open personoj.encodings.lhol;
+require open personoj.encodings.pvs_cert;
// Prelude with some logics operator
-definition imp P Q ≔ impd {P} (λ_, Q)
-set infix right 6 "⇒" ≔ imp
-definition false ≔ ∀ {prop} (λx, x)
-definition true ≔ false ⇒ false
-symbol not: Prop → Prop
-set prefix 8 "¬" ≔ not
-rule Prf (¬ $x) ↪ Prf $x → Π(z: Prop), Prf z
+symbol imp P Q ≔ impd {P} (λ _, Q);
+set infix right 6 "⇒" ≔ imp;
+symbol false ≔ ∀ {prop} (λ x, x);
+symbol true ≔ false ⇒ false;
+symbol not: Prop → Prop;
+set prefix 8 "¬" ≔ not;
+rule Prf (¬ $x) ↪ Prf $x → Π(z: Prop), Prf z;
// Nat top type
-constant symbol nat: Set
+constant symbol nat: Set;
// Presburger arithmetics
-constant symbol s: El (nat ~> nat)
-constant symbol z: El nat
-constant symbol eqnat: El (nat ~> nat ~> prop)
-symbol plus_nat: El (nat ~> nat ~> nat)
-set infix left 4 "+" ≔ plus_nat
-constant symbol s_not_z: Prf (∀ (λx, ¬ (eqnat z (s x))))
-rule Prf (eqnat (s $n) (s $m)) ↪ Prf (eqnat $n $m) with Prf (eqnat z z) ↪ Prf true
-rule $n + z ↪ $n with $n + s $m ↪ s ($n + $m)
+constant symbol s: El (nat ~> nat);
+constant symbol z: El nat;
+constant symbol eqnat: El (nat ~> nat ~> prop);
+symbol plus_nat: El (nat ~> nat ~> nat);
+set infix left 4 "+" ≔ plus_nat;
+constant symbol s_not_z: Prf (∀ (λ x, ¬ (eqnat z (s x))));
+rule Prf (eqnat (s $n) (s $m)) ↪ Prf (eqnat $n $m) with Prf (eqnat z z) ↪ Prf true;
+rule $n + z ↪ $n with $n + s $m ↪ s ($n + $m);
symbol nat_ind:
- Prf (∀ {nat ~> prop} (λp, (p z) ⇒ (∀ (λn, p n ⇒ p (s n))) ⇒ (∀ (λn, p n))))
+ Prf (∀ {nat ~> prop} (λ p, (p z) ⇒ (∀ (λ n, p n ⇒ p (s n))) ⇒ (∀ (λ n, p n))));
// System T
-symbol rec_nat: El nat → El nat → (El nat → El nat → El nat) → El nat
-rule rec_nat z $t0 _ ↪ $t0
-rule rec_nat (s $u) $t0 $ts ↪ $ts $u (rec_nat $u $t0 $ts)
+symbol rec_nat: El nat → El nat → (El nat → El nat → El nat) → El nat;
+rule rec_nat z $t0 _ ↪ $t0;
+rule rec_nat (s $u) $t0 $ts ↪ $ts $u (rec_nat $u $t0 $ts);
-definition mult a b ≔ rec_nat a z (λ_ r, b + r)
+symbol mult a b ≔ rec_nat a z (λ _ r, b + r);
-symbol times_nat: El (nat ~> nat ~> nat)
-set infix left 5 "*" ≔ times_nat
+symbol times_nat: El (nat ~> nat ~> nat);
+set infix left 5 "*" ≔ times_nat;
rule z * _ ↪ z
with $n * (s $m) ↪ $n + ($n * $m)
-with _ * z ↪ z // (times_z_left)
+with _ * z ↪ z; // (times_z_left)
// Declaration of a top type
-constant symbol frac: Set
+constant symbol frac: Set;
-symbol eqfrac: El (frac ~> frac ~> prop)
+symbol eqfrac: El (frac ~> frac ~> prop);
-theorem z_plus_n_n: Prf (∀ (λn, eqnat (z + n) n))
-proof
- assume n
- refine nat_ind (λn, eqnat (z + n) n) _ _ n
- refine λx: Prf false, x
- assume n0 Hn
- apply Hn
-qed
+opaque symbol z_plus_n_n: Prf (∀ (λ n, eqnat (z + n) n)) ≔
+begin
+ assume n;
+ refine nat_ind (λ n, eqnat (z + n) n) _ _ n;
+ refine λ x: Prf false, x;
+ assume n0 Hn;
+ apply Hn;
+end;
// The following theorem allows to remove rule (times_z_left)
// but doing so would require to have eqnat transitivity, which requires some
// more work. So it is left for now.
-theorem n_times_z_z: Prf (∀ (λn, eqnat (z * n) z))
-proof
- assume n
- refine nat_ind (λn, eqnat (z * n) z) _ _ n
- refine λx: Prf false, x
- assume n0 Hn
- refine Hn
-qed
-
-theorem times_comm: Prf (∀ (λa, ∀ (λb, eqnat (a * b) (b * a))))
-proof
-admit
-
-definition nznat_p ≔ λn, ¬ (eqnat z n)
-definition nznat ≔ psub nznat_p
-
-theorem nzprod: Prf (∀ {nznat} (λx, ∀ {nznat} (λy, nznat_p (fst x * fst y))))
-proof
-admit
+opaque symbol n_times_z_z: Prf (∀ (λ n, eqnat (z * n) z)) ≔
+begin
+ assume n;
+ refine nat_ind (λ n, eqnat (z * n) z) _ _ n;
+ refine λ x: Prf false, x;
+ assume n0 Hn;
+ refine Hn;
+end;
+
+opaque symbol times_comm: Prf (∀ (λ a, ∀ (λ b, eqnat (a * b) (b * a)))) ≔
+begin
+admit;
+
+symbol nznat_p ≔ λ n, ¬ (eqnat z n);
+symbol nznat ≔ psub nznat_p;
+
+opaque symbol nzprod: Prf (∀ {nznat} (λ x, ∀ {nznat} (λ y, nznat_p (fst x * fst y)))) ≔
+begin
+admit;
// Building rationals from natural numbers
-symbol div: El (nat ~> nznat ~> frac)
-set infix left 6 "/" ≔ div
-rule eqfrac ($a / $b) ($c / $d) ↪ eqnat ($a * (fst $d)) ((fst $b) * $c)
+symbol div: El (nat ~> nznat ~> frac);
+set infix left 6 "÷" ≔ div;
+rule eqfrac ($a ÷ $b) ($c ÷ $d) ↪ eqnat ($a * (fst $d)) ((fst $b) * $c);
// rule Prf (nat_p ($n / pair $n _)) ↪ Prf true
// Non linear rules break confluence
-symbol times_frac: El (frac ~> frac ~> frac)
-rule times_frac ($a / $b) ($c / $d)
+symbol times_frac: El (frac ~> frac ~> frac);
+rule times_frac ($a ÷ $b) ($c ÷ $d)
↪ let denom ≔ fst $b * (fst $d) in
let prf ≔ nzprod $b $d in
- ($a * $c) / (pair denom prf)
+ ($a * $c) ÷ (pair denom prf);
-definition one_nz ≔ pair {nat} {nznat_p} (s z) (s_not_z z)
+symbol one_nz ≔ pair {nat} {nznat_p} (s z) (s_not_z z);
-theorem right_cancel:
- Prf (∀ (λa, ∀ (λb, eqfrac (times_frac (a / b) (fst b / one_nz)) (a / one_nz))))
-proof
- assume x y
- simpl
- apply times_comm x (fst y)
-qed
+opaque
+symbol right_cancel:
+ Prf (∀ (λ a, ∀ (λ b, eqfrac (times_frac (a ÷ b) (fst b ÷ one_nz)) (a ÷ one_nz))))
+ ≔
+begin
+ assume x y;
+ simpl;
+ apply times_comm x (fst y);
+end;
diff --git a/prelude/functions.lp b/prelude/functions.lp
deleted file mode 100644
index e088d05..0000000
--- a/prelude/functions.lp
+++ /dev/null
@@ -1,67 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.logical
-require open personoj.encodings.equality
-require open personoj.encodings.prenex
-require open personoj.prelude.logic
-//
-// functions [D, R: TYPE]
-//
-
-symbol extensionality_postulate:
- Prf (∀B (λD, ∀B (λR,
- ∀ (λf: El (D ~> R),
- ∀ (λg: El (D ~> R), iff (∀ (λx, f x = g x)) (f = g))))))
-
-// definition {|injective?|} {D} {R} (f: Term (D ~> R)) ≔
-// forall (λx1, forall (λx2, imp (f x1 = f x2) (x1 = x2)))
-
-// definition {|surjective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R)) ≔
-// forall (λy, ∃ (λx, (f x) = y))
-
-// definition {|bijective?|} {D: Term uType} {R: Term uType} (f: Term (D ~> R)) ≔
-// ({|injective?|} f) ∧ ({|surjective?|} f)
-
-// theorem bij_is_inj {D: Term uType} {R: Term uType}:
-// Term (Psub {D ~> R} {|bijective?|} ⊑ Psub {D ~> R} {|injective?|})
-// proof
-// admit
-
-// theorem bij_is_surj {D: Term uType} {R: Term uType}:
-// Term (Psub {D ~> R} {|bijective?|} ⊑ Psub {D ~> R} {|surjective?|})
-// proof
-// admit
-
-// symbol domain {D: Term uType} {R: Term uType} (f: Term (D ~> R)): Term uType
-// rule domain {$D} {_} _ ↪ $D
-
-// //
-// // restrict[T: TYPE, S: TYPE FROM T, R: TYPE]
-// //
-// symbol restrict {T: Term uType} (S: Term uType) {R: Term uType}
-// (f: Term (T ~> R)) (_: Term (S ⊑ T)) (s: Term S):
-// Term R
-// rule restrict {$T} _ {_} $f $pr $s ↪ $f (↑ $T $pr $s)
-
-// theorem injective_restrict {T} S {R} (f: Term (T ~> R)) (pr: Term (S ⊑ T)):
-// Term ({|injective?|} f) → Term ({|injective?|} (restrict S f pr))
-// proof
-// admit
-
-// //
-// // restrict_props[T: TYPE, R: TYPE]
-// //
-
-// theorem restrict_full {T: Term uType} {R: Term uType} (f: Term (T ~> R)):
-// Term (eq {T ~> R} (restrict {T} T {R} f (S.refl T)) f)
-// proof
-// admit
-
-// //
-// // extend[T: TYPE, S: TYPE FROM T, R: TYPE, d: R]
-// //
-
-// definition extend {T: Term uType}
-// (s_pred: Term (pred T)) {R: Term uType} (d: Term R)
-// (f: Term (Psub s_pred ~> R)) (t: Term T) (pr: Term (s_pred t)) ≔
-// if (s_pred t) (f (↓ s_pred t pr)) d
diff --git a/prelude/logic.lp b/prelude/logic.lp
deleted file mode 100644
index 1834626..0000000
--- a/prelude/logic.lp
+++ /dev/null
@@ -1,150 +0,0 @@
-require open personoj.encodings.lhol
-require open personoj.encodings.pvs_cert
-require open personoj.encodings.logical
-require open personoj.encodings.equality
-require open personoj.encodings.prenex
-require open personoj.encodings.builtins
-//
-// Propeans
-// In [adlib.cert_f.bootstrap]
-
-//
-// Equalities
-//
-
-//
-// Notequal
-//
-// definition neq {T: Set} (x y: El T) ≔ ¬ (x = y)
-// symbol neq: χ (∀S (λt, scheme (t ~> t ~> prop)))
-// rule neq _ $x $y ↪ ¬ ($x = $y)
-// set infix left 2 "/=" ≔ neq
-// set infix left 2 "≠" ≔ neq
-/// Defined in builtins
-
-//
-// if_def
-//
-
-//
-// propean_props
-// Slightly modified from the prelude
-constant symbol prop_exclusive: Prf (neq {prop} false true)
-constant symbol prop_inclusive:
- Prf (∀ {prop} (λa, ((eq {prop} a false) ∨ (λ_, eq {prop} a true))))
-
-opaque
-symbol excluded_middle: Prf (∀ {prop} (λa, a ∨ (λ_, ¬ a)))
-≔ begin
- assume x f
- refine f
-end
-
-//
-// xor_def
-//
-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
-opaque
-symbol xor_def:
- Prf (∀ {prop} (λa, ∀ {prop} (λb, eq {prop} (xor a b)
- (if {prop} a (λ_, ¬ b) (λ_, b)))))
-≔ begin
- assume a b p
- simpl
- assume hxor
-admit
-//
-// Quantifier props[t: TYPE], built in
-//
-// Defined types
-//
-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
-//
-
-//
-// equality_props
-//
-constant
-symbol If_true
- : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if true (λ_, x) (λ_, y) = x))))
-constant
-symbol If_false
- : Prf (∀B (λt, ∀ (λx, ∀ {t} (λy, if false (λ_, x) (λ_, y) = y))))
-
-opaque
-symbol if_same
- : Prf (∀B (λt, ∀ {prop} (λb, ∀ (λx: El t, if b (λ_, x) (λ_, x) = x))))
- ≔
-begin
-admit
-
-constant symbol reflexivity_of_equals: Prf (∀B (λt, ∀ (λx: El t, x = x)))
-
-constant
-symbol transitivity_of_equals
- : Prf (∀B (λt,
- ∀(λx: El t,
- ∀(λy: El t,
- ∀(λz: El t, (x = y) ∧ (λ_, y = z) ⊃ (λ_, x = z))))))
-
-constant
-symbol symmetry_of_equals
- : Prf (∀B (λt, ∀ (λx: El t, (∀ (λy: El t, (x = y) ⊃ (λ_, y = x))))))
-
-// Not in prelude!
-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
-end
-set builtin "eqind" ≔ eqind
-
-//
-// if_props
-//
-
-opaque
-symbol lift_if1:
- Prf (∀B (λs: Ty {|set|},
- ∀B (λt: Ty {|set|},
- ∀ {prop}
- (λa,
- ∀ (λx: El s,
- ∀ (λy: El s,
- ∀ (λf: El (s ~> t),
- f (if a (λ_, x) (λ_, y))
- = if a (λ_, f x) (λ_, f y))))))))
-≔ begin
-admit
-
-opaque
-symbol lift_if2:
- Prf (∀B (λs,
- ∀ {prop}
- (λa,
- ∀ {prop}
- (λb,
- ∀ {prop}
- (λc,
- ∀ (λx: El s,
- ∀ (λy: El s,
- if (if {prop} a (λ_, b) (λ_, c))
- (λ_, x)
- (λ_, y)
- = if a
- (λ_, if b (λ_, x) (λ_, y))
- (λ_, if c (λ_, x) (λ_, y)))))))))
-≔ begin
-admit
--
GitLab