From f18d8e641f34028d5774e10ceafdd5f75c737ac8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= Date: Fri, 21 Jun 2024 20:47:26 +0200 Subject: [PATCH] use Stdlib instead of Logics.U (#2) --- .github/workflows/main.yml | 4 +- Implem.lp | 133 +++++++++++++++++++++++++++++++++++++ Main.lp | 61 ++++++++--------- README.md | 2 +- lambdapi-zenon.opam | 2 +- 5 files changed, 164 insertions(+), 38 deletions(-) create mode 100644 Implem.lp diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index fffc38e..c88b3d5 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -10,7 +10,7 @@ jobs: fail-fast: false matrix: lambdapi-version: [lambdapi, lambdapi.2.5.0, lambdapi.2.4.1, lambdapi.2.4.0, lambdapi.2.3.1, lambdapi.2.3.0, lambdapi.2.2.1, lambdapi.2.2.0, lambdapi.2.1.0, lambdapi.2.0.0] - lambdapi-logics-version: [lambdapi-logics.0.0.1] + lambdapi-stdlib-version: [lambdapi-stdlib.1.1.0] runs-on: ubuntu-latest @@ -37,7 +37,7 @@ jobs: run: opam install ${{ matrix.lambdapi-version }} - name: Install dependencies - run: opam install ${{ matrix.lambdapi-logics-version }} + run: opam install ${{ matrix.lambdapi-stdlib-version }} - name: Check library run: | diff --git a/Implem.lp b/Implem.lp new file mode 100644 index 0000000..9fb6211 --- /dev/null +++ b/Implem.lp @@ -0,0 +1,133 @@ +/* Implementation of Zenon rules in classical FOL. */ + +require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL; + +symbol Rfalse : π ⊥ → π ⊥ ≔ +begin +assume h; apply h +end; + +symbol Rnottrue : π (¬ ⊤) → π ⊥ ≔ +begin +assume h; refine h _; apply ⊤ᵢ +end; + +symbol Raxiom p : π p → π (¬ p) → π ⊥ ≔ +begin +assume p hp hnp; apply hnp hp +end; + +symbol Rnoteq a (t : τ a) : π (¬ (t = t)) → π ⊥ ≔ +begin +assume a t neq; apply neq; reflexivity +end; + +symbol Reqsym a (t u : τ a) : π (t = u) → π (¬ (u = t)) → π ⊥ ≔ +begin +assume a t u eq neq; apply neq; symmetry; apply eq +end; + +symbol Rnotnot p : (π p → π ⊥) → π (¬ ¬ p) → π ⊥ ≔ +begin +assume p np nnp; apply nnp np +end; + +symbol Rand p q : (π p → π q → π ⊥) → π (p ∧ q) → π ⊥ ≔ +begin +assume p q h pq; apply h { apply ∧ₑ₁ pq } { apply ∧ₑ₂ pq } +end; + +symbol Ror p q : (π p → π ⊥) → (π q → π ⊥) → π (p ∨ q) → π ⊥ ≔ +begin +assume p q np nq pq; apply ∨ₑ pq np nq +end; + +symbol Rnotor p q : (π (¬ p) → π (¬ q) → π ⊥) → π (¬ (p ∨ q)) → π ⊥ ≔ +begin +assume p q h npq; apply h +{ assume hp; apply npq; apply ∨ᵢ₁ hp } +{ assume hq; apply npq; apply ∨ᵢ₂ hq } +end; + +symbol Rex a p : (Π t : τ a, π (p t) → π ⊥) → π (∃ p) → π ⊥ ≔ +begin +assume a p h1 h2; apply ∃ₑ h2; assume x px; apply h1 x px +end; + +symbol Rall a p (t : τ a) : (π (p t) → π ⊥) → π (∀ p) → π ⊥ ≔ +begin +assume a p t npt h; apply npt; apply h t +end; + +symbol Rnotex a p (t : τ a) : (π (¬ (p t)) → π ⊥) → π (¬ (∃ p)) → π ⊥ ≔ +begin +assume a p t nnpt h; apply nnpt; assume pt; apply h; apply ∃ᵢ t pt +end; + +symbol Rsubst a p (t1 t2 : τ a) : (π (¬ (t1 = t2)) → π ⊥) → (π (p t2) → π ⊥) → π (p t1) → π ⊥ ≔ +begin +assume a p t1 t2 nneq npt2 pt1; apply nneq; assume eq; apply npt2; +rewrite left eq; refine pt1 +end; + +symbol Rconglr a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t1 = t2) → π ⊥ ≔ +begin +assume a p t1 t2 npt2 pt1 eq; apply npt2; rewrite left eq; refine pt1 +end; + +symbol Rcongrl a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t2 = t1) → π ⊥ ≔ +begin +assume a p t1 t2 npt2 pt1 eq; apply npt2; rewrite eq; refine pt1 +end; + +symbol Rimply p q : (π (¬ p) → π ⊥) → (π q → π ⊥) → π (p ⇒ q) → π ⊥ ≔ +begin +assume p q nnp nq pq; apply nnp; assume hp; apply nq; apply pq; refine hp +end; + +symbol Rnotand p q : (π (¬ p) → π ⊥) → (π (¬ q) → π ⊥) → π (¬ (p ∧ q)) → π ⊥ ≔ +begin +assume p q nnp nnq npq; apply nnp; assume hp; apply nnq; assume hq; apply npq; +apply ∧ᵢ hp hq +end; + +symbol Rnotimply p q : (π p → π (¬ q) → π ⊥) → π (¬ (p ⇒ q)) → π ⊥ ≔ +begin +assume p q h1 h2; apply h2; assume hp; apply ⊥ₑ; apply h1 hp; +assume hq; apply h2; assume hp'; refine hq +end; + +symbol Rnotequiv p q : (π (¬ p) → π q → π ⊥) → (π p → π (¬ q) → π ⊥) → π (¬ (p ⇔ q)) → π ⊥ ≔ +begin +assume p q h1 h2 h3; +have np: π (¬ p) +{ assume hp; apply h2 hp; assume hq; apply h3; apply ∧ᵢ + { assume hp'; refine hq } + { assume hq'; refine hp } +}; +apply h3; apply ∧ᵢ +{ assume hp; apply ⊥ₑ; apply np hp } +{ assume hq; apply ⊥ₑ; apply h1 np hq } +end; + +symbol Requiv p q : (π (¬ p) → π (¬ q) → π ⊥) → (π p → π q → π ⊥) → π (p ⇔ q) → π ⊥ ≔ +begin +assume p q h1 h2 eq; +have pq : π (p ⇒ q) { apply ∧ₑ₁ eq }; +have qp : π (q ⇒ p) { apply ∧ₑ₂ eq }; +have nq: π (¬ q) { assume hq; apply h2 _ hq; apply qp; refine hq }; +have np: π (¬ p) { assume hp; apply h2 hp; apply pq; refine hp }; +apply h1 np nq +end; + +require open Stdlib.Classic; + +symbol nnpp p : π (¬ ¬ p) → π p ≔ +begin +refine ¬¬ₑ +end; + +symbol Rnotall a p : (Π t : τ a, π (¬ (p t)) → π ⊥) → π (¬ (∀ p)) → π ⊥ ≔ +begin +assume a p h1 h2; apply h2; assume t; apply ¬¬ₑ; refine h1 t +end; diff --git a/Main.lp b/Main.lp index 53a7ce0..1963bec 100644 --- a/Main.lp +++ b/Main.lp @@ -1,44 +1,37 @@ /* Logic used by the automated theorem prover ZenonModulo https://github.com/Deducteam/zenon_modulo/tree/modulo */ -require open Logic.U.Prop Logic.U.Set Logic.U.Quant; +require open Stdlib.Prop Stdlib.Set Stdlib.Eq Stdlib.FOL; -// equivalence -symbol ⇔ : Prop → Prop → Prop; notation ⇔ infix right 5; - -// equality -symbol = [a] : El a → El a → Prop; notation = infix 12; - -// Zenon rules -symbol nnpp p : Prf (¬ ¬ p) → Prf p; -symbol Rfalse : Prf ⊥ → Prf ⊥; -symbol Rnottrue : Prf (¬ ⊤) → Prf ⊥; -symbol Raxiom p : Prf p → Prf (¬ p) → Prf ⊥; -symbol Rnoteq a (t : El a) : Prf (¬ (t = t)) → Prf ⊥; -symbol Reqsym a (t u : El a) : Prf (t = u) → Prf (¬ (u = t)) → Prf ⊥; -symbol Rnotnot p : (Prf p → Prf ⊥) → Prf (¬ ¬ p) → Prf ⊥; -symbol Rand p q : (Prf p → Prf q → Prf ⊥) → Prf (p ∧ q) → Prf ⊥; -symbol Ror p q : (Prf p → Prf ⊥) → (Prf q → Prf ⊥) → Prf (p ∨ q) → Prf ⊥; -symbol Rimply p q : (Prf (¬ p) → Prf ⊥) → (Prf q → Prf ⊥) → Prf (p ⇒ q) → Prf ⊥; -symbol Requiv p q : (Prf (¬ p) → Prf (¬ q) → Prf ⊥) → (Prf p → Prf q → Prf ⊥) → Prf (p ⇔ q) → Prf ⊥; -symbol Rnotand p q : (Prf (¬ p) → Prf ⊥) → (Prf (¬ q) → Prf ⊥) → Prf (¬ (p ∧ q)) → Prf ⊥; -symbol Rnotor p q : (Prf (¬ p) → Prf (¬ q) → Prf ⊥) → Prf (¬ (p ∨ q)) → Prf ⊥; -symbol Rnotimply p q : (Prf p → Prf (¬ q) → Prf ⊥) → Prf (¬ (p ⇒ q)) → Prf ⊥; -symbol Rnotequiv p q : (Prf (¬ p) → Prf q → Prf ⊥) → (Prf p → Prf (¬ q) → Prf ⊥) → Prf (¬ (p ⇔ q)) → Prf ⊥; -symbol Rex a p : (Π t : El a, Prf (p t) → Prf ⊥) → Prf (∃ p) → Prf ⊥; -symbol Rall a p (t : El a) : (Prf (p t) → Prf ⊥) → Prf (∀ p) → Prf ⊥; -symbol Rnotex a p (t : El a) : (Prf (¬ (p t)) → Prf ⊥) → Prf (¬ (∃ p)) → Prf ⊥; -symbol Rnotall a p : (Π t : El a, Prf (¬ (p t)) → Prf ⊥) → Prf (¬ (∀ p)) → Prf ⊥; -symbol Rsubst a p (t1 t2 : El a) : (Prf (¬ (t1 = t2)) → Prf ⊥) → (Prf (p t2) → Prf ⊥) → Prf (p t1) → Prf ⊥; -symbol Rconglr a p (t1 t2 : El a) : (Prf (p t2) → Prf ⊥) → Prf (p t1) → Prf (t1 = t2) → Prf ⊥; -symbol Rcongrl a p (t1 t2 : El a) : (Prf (p t2) → Prf ⊥) → Prf (p t1) → Prf (t2 = t1) → Prf ⊥; +symbol nnpp p : π (¬ ¬ p) → π p; +symbol Rfalse : π ⊥ → π ⊥; +symbol Rnottrue : π (¬ ⊤) → π ⊥; +symbol Raxiom p : π p → π (¬ p) → π ⊥; +symbol Rnoteq a (t : τ a) : π (¬ (t = t)) → π ⊥; +symbol Reqsym a (t u : τ a) : π (t = u) → π (¬ (u = t)) → π ⊥; +symbol Rnotnot p : (π p → π ⊥) → π (¬ ¬ p) → π ⊥; +symbol Rand p q : (π p → π q → π ⊥) → π (p ∧ q) → π ⊥; +symbol Ror p q : (π p → π ⊥) → (π q → π ⊥) → π (p ∨ q) → π ⊥; +symbol Rimply p q : (π (¬ p) → π ⊥) → (π q → π ⊥) → π (p ⇒ q) → π ⊥; +symbol Requiv p q : (π (¬ p) → π (¬ q) → π ⊥) → (π p → π q → π ⊥) → π (p ⇔ q) → π ⊥; +symbol Rnotand p q : (π (¬ p) → π ⊥) → (π (¬ q) → π ⊥) → π (¬ (p ∧ q)) → π ⊥; +symbol Rnotor p q : (π (¬ p) → π (¬ q) → π ⊥) → π (¬ (p ∨ q)) → π ⊥; +symbol Rnotimply p q : (π p → π (¬ q) → π ⊥) → π (¬ (p ⇒ q)) → π ⊥; +symbol Rnotequiv p q : (π (¬ p) → π q → π ⊥) → (π p → π (¬ q) → π ⊥) → π (¬ (p ⇔ q)) → π ⊥; +symbol Rex a p : (Π t : τ a, π (p t) → π ⊥) → π (∃ p) → π ⊥; +symbol Rall a p (t : τ a) : (π (p t) → π ⊥) → π (∀ p) → π ⊥; +symbol Rnotex a p (t : τ a) : (π (¬ (p t)) → π ⊥) → π (¬ (∃ p)) → π ⊥; +symbol Rnotall a p : (Π t : τ a, π (¬ (p t)) → π ⊥) → π (¬ (∀ p)) → π ⊥; +symbol Rsubst a p (t1 t2 : τ a) : (π (¬ (t1 = t2)) → π ⊥) → (π (p t2) → π ⊥) → π (p t1) → π ⊥; +symbol Rconglr a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t1 = t2) → π ⊥; +symbol Rcongrl a p (t1 t2 : τ a) : (π (p t2) → π ⊥) → π (p t1) → π (t2 = t1) → π ⊥; // temporary renamings to be removed ultimately symbol Type ≔ Set; -symbol ι ≔ ι; -symbol τ ≔ El; -symbol κ ≔ El ι; +symbol ι : Set; +symbol τ ≔ τ; +symbol κ ≔ τ ι; symbol ∀α [a] ≔ ∀ [a]; symbol ∃α [a] ≔ ∃ [a]; symbol =α [a] ≔ (=) [a]; -symbol ϵ ≔ Prf; +symbol ϵ ≔ π; diff --git a/README.md b/README.md index 8f24721..5f2310b 100644 --- a/README.md +++ b/README.md @@ -17,7 +17,7 @@ Usage in Lambdapi ----------------- ``` -require Logic.Zenon.Main; +require open Logic.Zenon.Main; ``` Compilation from the sources diff --git a/lambdapi-zenon.opam b/lambdapi-zenon.opam index 441d1bf..fdbd902 100644 --- a/lambdapi-zenon.opam +++ b/lambdapi-zenon.opam @@ -12,5 +12,5 @@ dev-repo: "git+https://github.com/Deducteam/lambdapi-zenon.git" install: [ make "install" ] depends: [ "lambdapi" {>= "2.3.0"} - "lambdapi-logics" {>= "0.0.1"} + "lambdapi-stdlib" {>= "1.1.0"} ]