use Stdlib instead of Logics.U (#2)

.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: |

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;

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 ϵ ≔ π;

README.md

@@ -17,7 +17,7 @@ Usage in Lambdapi
 -----------------
 
 ```
-require Logic.Zenon.Main;
+require open Logic.Zenon.Main;
 ```
 
 Compilation from the sources

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"}
 ]