add classical logic (#14)

AUTHORS.md

@@ -0,0 +1,3 @@
+- Quentin Garchery
+- Quentin Buzet
+- Frédéric Blanqui

Bool.lp

@@ -34,7 +34,7 @@ with istrue false ↪ ⊥;
 
 opaque symbol false≠true : π (false ≠ true) ≔
 begin
-  assume h; refine ind_eq h istrue top
+  assume h; refine ind_eq h istrue ⊤ᵢ
 end;
 
 opaque symbol true≠false : π (true ≠ false) ≔
@@ -61,28 +61,28 @@ with $b    or false ↪ $b;
 opaque symbol ∨_istrue [p q] : π(istrue(p or q)) → π(istrue p ∨ istrue q) ≔
 begin
   induction
-  { assume q h; apply ∨ᵢ₁; apply top; }
+  { assume q h; apply ∨ᵢ₁; apply ⊤ᵢ; }
   { assume q h; apply ∨ᵢ₂; apply h; }
 end;
 
 opaque symbol istrue_or [p q] : π(istrue p ∨ istrue q) → π(istrue(p or q)) ≔
 begin
   induction
-  { assume q h; apply top; }
+  { assume q h; apply ⊤ᵢ; }
   { assume q h; apply ∨ₑ h { assume i; apply ⊥ₑ i; } { assume i; apply i; } }
 end;
 
 opaque symbol orᵢ₁ [p] q : π (istrue p) → π (istrue (p or q)) ≔
 begin
   induction
-  { simplify; assume b h; apply top }
+  { simplify; assume b h; apply ⊤ᵢ }
   { simplify; assume b h; apply ⊥ₑ h }
 end;
 
 opaque symbol orᵢ₂ p [q] : π (istrue q) → π (istrue (p or q)) ≔
 begin
   induction
-  { simplify; assume b h; apply top }
+  { simplify; assume b h; apply ⊤ᵢ }
   { simplify; assume b h; apply h }
 end;
 
@@ -121,7 +121,7 @@ opaque symbol ∧_istrue [p q] : π(istrue (p and q)) → π(istrue p ∧ istrue
 begin
   induction
   { induction
-    { assume h; apply ∧ᵢ { apply top } { apply top } }
+    { assume h; apply ∧ᵢ { apply ⊤ᵢ } { apply ⊤ᵢ } }
     { assume h; apply ⊥ₑ h; }
   }
   { assume q h; apply ⊥ₑ h; }
@@ -143,7 +143,7 @@ end;
 opaque symbol andₑ₁ [p q] : π (istrue (p and q)) → π (istrue p) ≔
 begin
   induction
-  { assume q i; apply top; }
+  { assume q i; apply ⊤ᵢ; }
   { assume q i; apply i; }
 end;
 

CHANGES.md

@@ -0,0 +1,18 @@
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/),
+and this project adheres to [Semantic Versioning](https://semver.org/).
+
+## 1.1.0 (2024-06-21)
+
+- Add classical logic
+- Rename top into ⊤ᵢ
+- Declare more arguments of ∃ᵢ and ∃ₑ implicit
+
+## 1.0.0 (2023-10-19)
+
+- Add integers (Quentin Garchery)
+
+## 0.0.0 (2022-01-27)
+
+- Add natural numbers and lists (Quentin Buzet)

Classic.lp

@@ -0,0 +1,30 @@
+// classical logic
+
+require open Stdlib.Set Stdlib.Prop Stdlib.FOL;
+
+symbol em p : π (p ∨ ¬ p); // excluded middle
+
+opaque symbol ¬¬ₑ p : π (¬ ¬ p) → π p ≔
+begin
+assume p nnp; apply ∨ₑ (em p)
+{ assume h; refine h }
+{ assume np; apply ⊥ₑ; refine nnp np }
+end;
+
+opaque symbol ∨¬ᵢ p q : π (p ⇒ q) → π (¬ p ∨ q) ≔
+begin
+assume p q pq; apply ∨ₑ (em p)
+{ assume hp; refine ∨ᵢ₂ _; refine pq hp }
+{ assume np; refine ∨ᵢ₁ np }
+end;
+
+opaque symbol ∃¬ᵢ a p : π (¬ (∀ p)) → π (`∃ x : τ a, ¬ (p x)) ≔
+begin
+assume a p not_all_p; apply ∨ₑ (em (`∃ x, ¬ (p x)))
+{ assume h; apply h }
+{ assume not_ex_not_p; apply ⊥ₑ; apply not_all_p;
+  have h: π (`∀ x, ¬ ¬ (p x))
+    { refine ¬∃ (λ x, ¬ (p x)) _; refine not_ex_not_p};
+  assume x; apply ¬¬ₑ; refine h x
+}
+end;

Comp.lp

@@ -40,17 +40,17 @@ with isGt Gt ↪ true;
 
 symbol Lt≠Eq : π (Lt ≠ Eq) ≔
 begin
-  assume h; refine ind_eq h (λ n, istrue(isEq n)) top
+  assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ
 end;
 
 symbol Gt≠Eq : π (Gt ≠ Eq) ≔
 begin
-  assume h; refine ind_eq h (λ n, istrue(isEq n)) top
+  assume h; refine ind_eq h (λ n, istrue(isEq n)) ⊤ᵢ
 end;
 
 symbol Gt≠Lt : π (Gt ≠ Lt) ≔
 begin
-  assume h; refine ind_eq h (λ n, istrue(isLt n)) top
+  assume h; refine ind_eq h (λ n, istrue(isLt n)) ⊤ᵢ
 end;
 
 // Opposite of a Comp

FOL.lp

@@ -4,15 +4,27 @@ require open Stdlib.Set Stdlib.Prop;
 
 // Universal quantification
 
-constant symbol ∀ [a] : (τ a → Prop) → Prop; notation ∀ quantifier; // !! or \forall
+constant symbol ∀ [a] : (τ a → Prop) → Prop; // !! or \forall
+
+notation ∀ quantifier;
 
 rule π (∀ $f) ↪ Π x, π ($f x);
 
 // Existential quantification
 
-constant symbol ∃ [a] : (τ a → Prop) → Prop; notation ∃ quantifier; // ?? or \exists
+constant symbol ∃ [a] : (τ a → Prop) → Prop; // ?? or \exists
+
+notation ∃ quantifier;
+
+constant symbol ∃ᵢ [a p] (x:τ a) : π (p x) → π (∃ p);
+
+symbol ∃ₑ [a p] : π (∃ p) → Π [q], (Π x:τ a, π (p x) → π q) → π q;
+
+rule ∃ₑ (∃ᵢ $x $px) $f ↪ $f $x $px;
 
-constant symbol ∃ᵢ [a] p (x:τ a) : π (p x) → π (∃ p);
-symbol ∃ₑ [a] p : π (∃ p) → Π q, (Π x:τ a, π (p x) → π q) → π q;
+// properties
 
-rule ∃ₑ _ (∃ᵢ _ $x $px) _ $f ↪ $f $x $px;
+opaque symbol ¬∃ [a] p : π (¬ (∃ p) ⇒ `∀ x : τ a, ¬ (p x)) ≔
+begin
+assume a p not_ex_p x px; apply not_ex_p; apply ∃ᵢ x px
+end;

List.lp

@@ -220,7 +220,7 @@ with is□ (_ ⸬ _) ↪ false;
 
 opaque symbol ⸬≠□ [a] [x:τ a] [l] : π (x ⸬ l ≠ □) ≔
 begin
-  assume a x l h; refine ind_eq h (λ l, istrue(is□ l)) top
+  assume a x l h; refine ind_eq h (λ l, istrue(is□ l)) ⊤ᵢ
 end;
 
 opaque symbol □≠⸬ [a] [x:τ a] [l] : π (□ ≠ x ⸬ l) ≔
@@ -286,7 +286,7 @@ opaque symbol eql_complete a beq: π(`∀ x:τ a, `∀ y, x = y ⇒ istrue(beq x
 begin
   simplify; //FIXME: remove
   assume a beq beq_complete; induction
-  { assume m i; rewrite left i; apply top; }
+  { assume m i; rewrite left i; apply ⊤ᵢ; }
   { simplify /*FIXME*/; assume x l h; induction
     { assume j; apply ⸬≠□ j; }
     { assume y m i j; simplify;
@@ -1086,7 +1086,7 @@ end;
 opaque symbol mem_head [a] beq (x:τ a) l :
   π (beq x x = true) → π (istrue (∈ beq x (x ⸬ l))) ≔
 begin
-  assume a beq x l hrefl; simplify; rewrite hrefl; apply top;
+  assume a beq x l hrefl; simplify; rewrite hrefl; apply ⊤ᵢ;
 end;
 
 opaque symbol mem_take [a] beq n l (x:τ a) :
@@ -1119,10 +1119,10 @@ opaque symbol index_size [a] beq (x:τ a) l :
   π (istrue (index beq x l ≤ size l)) ≔
 begin
   assume a beq x; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume e l h; simplify;
     refine ind_𝔹 (λ b, istrue (if b 0 (index beq x l +1) ≤ size l +1)) _ _ (beq x e) {
-      apply top;
+      apply ⊤ᵢ;
     } {
       simplify; apply h;
     };
@@ -1169,10 +1169,10 @@ opaque symbol find_size [a] (p:τ a → 𝔹) l :
   π (istrue (find p l ≤ size l)) ≔
 begin
   assume a p; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume e l h;
     refine ind_𝔹 (λ x:𝔹, istrue (if x 0 (find p l +1) ≤ size l +1)) _ _ (p e) {
-      apply top;
+      apply ⊤ᵢ;
     } {
       simplify; apply h;
     };
@@ -1192,7 +1192,7 @@ assert ⊢ count (λ x, eqn (x + 1) 3) (2 ⸬ 2 ⸬ 2 ⸬ 2 ⸬ □) ≡ 4;
 opaque symbol count_size [a] (p:τ a → 𝔹) l : π(istrue (count p l ≤ size l)) ≔
 begin
   assume a p; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x:𝔹, istrue (if x (count p l +1) (count p l) ≤ size l +1)) _ _ (p e) {
       simplify; apply h;
@@ -1378,7 +1378,7 @@ opaque symbol size_undup [a] beq (l:𝕃 a) :
   π (istrue (size (undup beq l) ≤ size l)) ≔
 begin
   assume a beq; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume e l h; simplify;
     refine ind_𝔹 (λ x, istrue (size (if x (undup beq l) (e ⸬ undup beq l)) ≤ size l +1)) _ _ (∈ beq e (undup beq l)) {
       simplify;
@@ -1393,7 +1393,7 @@ opaque symbol undup_uniq [a] beq (l:𝕃 a) :
   π (istrue (uniq beq (undup beq l))) ≔
 begin
   assume a beq; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume e l h; simplify;
     refine ind_𝔹_eq (λ b, (istrue(uniq beq (if b (undup beq l) (e ⸬ (undup beq l)))))) (∈ beq e (undup beq l)) _ _ {
       assume i; rewrite i; simplify; apply h;

Nat.lp

@@ -117,7 +117,7 @@ with is0 (_ +1) ↪ false;
 
 opaque symbol s≠0 [n] : π (n +1 ≠ 0) ≔
 begin
-  assume n h; refine ind_eq h (λ n, istrue(is0 n)) top
+  assume n h; refine ind_eq h (λ n, istrue(is0 n)) ⊤ᵢ
 end;
 
 opaque symbol 0≠s [n] : π (0 ≠ n +1) ≔
@@ -154,7 +154,7 @@ end;
 opaque symbol eqn_complete x y : π(x = y) → π(istrue(eqn x y)) ≔
 begin
   induction
-  { assume y i; rewrite left i; apply top; }
+  { assume y i; rewrite left i; apply ⊤ᵢ; }
   { simplify; assume x h; induction
     { assume i; apply s≠0 i; }
     { assume y i j; simplify; }
@@ -654,7 +654,7 @@ end;
 opaque symbol ≤_refl x : π (istrue (x ≤ x)) ≔
 begin
   induction
-  { simplify; apply top;}
+  { simplify; apply ⊤ᵢ;}
   { assume x h; simplify; apply h; }
 end;
 
@@ -749,14 +749,14 @@ end;
 opaque symbol leq_pred n : π (istrue (n -1 ≤ n)) ≔
 begin
   induction
-  { apply top;}
+  { apply ⊤ᵢ;}
   { assume n h; simplify; apply leqnSn n;} 
 end;
 
 opaque symbol ltnW m n : π (istrue (m < n)) → π (istrue (m ≤ n)) ≔
 begin
   induction
-  { assume m h; apply top;}
+  { assume m h; apply ⊤ᵢ;}
   { assume m h; induction
     { assume i; apply i;}
     { assume n i j; apply h n; apply j;}
@@ -798,9 +798,9 @@ end;
 opaque symbol leq_total x y : π (istrue (x ≤ y) ∨ istrue (y ≤ x)) ≔
 begin
   induction
-  { assume y; simplify; apply ∨ᵢ₁; apply top; }
+  { assume y; simplify; apply ∨ᵢ₁; apply ⊤ᵢ; }
   { assume x h; induction
-    { simplify; apply ∨ᵢ₂; apply top; }
+    { simplify; apply ∨ᵢ₂; apply ⊤ᵢ; }
     { assume y i; simplify; apply h y; }
   }
 end;
@@ -814,7 +814,7 @@ begin
   } {
     generalize n; induction
     { assume h; apply h (eq_refl 0); }
-    { assume n h i; apply top; }
+    { assume n h i; apply ⊤ᵢ; }
   };
 end;
 
@@ -824,7 +824,7 @@ begin
     generalize m; induction
     { induction
       { assume h; apply ∨ᵢ₁ (eq_refl 0) }
-      { assume n h i; apply ∨ᵢ₂ top }
+      { assume n h i; apply ∨ᵢ₂ ⊤ᵢ }
     }
     { assume m h; induction
       { assume i; apply ∨ᵢ₂ i }
@@ -883,7 +883,7 @@ end;
 opaque symbol leq_addl m n : π (istrue (n ≤ m + n)) ≔
 begin
   assume m; induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume n h; apply h; }
 end;
 
@@ -897,7 +897,7 @@ begin
   induction
   { assume n; apply ≤_refl n; }
   { assume m h; induction
-    { apply top; }
+    { apply ⊤ᵢ; }
     { assume n i; simplify; 
       have t: π (istrue (n ≤ n +1)) { apply leqnSn n };
       apply @leq_trans (n - m) n (n +1) (h n) t;
@@ -909,7 +909,7 @@ opaque symbol subn_eq0 m n : π ((m - n = 0) ⇔ istrue (m ≤ n)) ≔
 begin
   assume m n; apply ∧ᵢ {
     generalize m; induction
-    { assume n h; apply top; }
+    { assume n h; apply ⊤ᵢ; }
     { assume m h; induction
       { assume i; apply s≠0 i; }
       { assume n i j; apply h n j; }
@@ -1188,7 +1188,7 @@ rule max $x $x ↪ $x;
 opaque symbol leq_maxl m n : π (istrue (m ≤ max m n)) ≔
 begin
   induction
-  { assume n; apply top; }
+  { assume n; apply ⊤ᵢ; }
   { assume m h; induction
     { simplify; apply ≤_refl m; }
     { assume n i; simplify; apply h n; }
@@ -1352,7 +1352,7 @@ begin
   } {
     generalize m; induction
     { assume h; apply h (eq_refl 0); }
-    { assume m h i; apply top; }
+    { assume m h i; apply ⊤ᵢ; }
   };
 end;
 
@@ -1482,9 +1482,9 @@ rule min $x $x ↪ $x;
 opaque symbol geq_minl m n : π (istrue (min m n ≤ m)) ≔
 begin
   induction
-  { assume n; apply top; }
+  { assume n; apply ⊤ᵢ; }
   { assume m h; induction
-    { apply top; }
+    { apply ⊤ᵢ; }
     { assume n i; simplify; apply h n; }
   }
 end;
@@ -1777,7 +1777,7 @@ end;
 opaque symbol fact_gt0 n : π (istrue (n ! > 0)) ≔
 begin
   induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume n h; rewrite factS n; rewrite mulSnr n (n !);
     apply ltn_addl 0 (n !) (n * n !); apply h; }
 end;
@@ -1790,6 +1790,6 @@ end;
 opaque symbol fact_geq n : π (istrue (n ≤ n !)) ≔
 begin
   induction
-  { apply top; }
+  { apply ⊤ᵢ; }
   { assume n h; rewrite factS n; apply leq_pmulr (n +1) (n !) (fact_gt0 n); }
 end;