From 69a2fc208b2eab0c4936103d2ee3065bd2c88a4e Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Fri, 1 May 2026 03:22:43 +0200
Subject: [PATCH 1/7] refactor IsIntuitionistic IsClassical

---
 Cslib/Logics/Propositional/Defs.lean          | 63 +++++++------------
 .../Propositional/NaturalDeduction/Basic.lean |  6 +-
 .../NaturalDeduction/Theory.lean              | 57 +++++++++++++++++
 lake-manifest.json                            |  2 +-
 4 files changed, 83 insertions(+), 45 deletions(-)
 create mode 100644 Cslib/Logics/Propositional/NaturalDeduction/Theory.lean

diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index fa3caf53e..51ff3a9ba 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -6,7 +6,7 @@ Authors: Thomas Waring
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Data.Set.Image
 public import Mathlib.Order.TypeTags
@@ -99,56 +99,37 @@ instance : Functor Theory where
   map f := Set.image (f <$> ·)
 
 /-- The empty theory corresponds to minimal propositional logic. -/
-abbrev MPL : Theory (Atom) := ∅
+abbrev MPL (Atom : Type u) : Theory (Atom) := ∅
 
 /-- Intuitionistic propositional logic adds the principle of explosion (ex falso quodlibet). -/
-abbrev IPL [Bot Atom] : Theory Atom :=
-  Set.range (⊥ → ·)
-
-/-- Classical logic further adds double negation elimination. -/
-abbrev CPL [Bot Atom] : Theory Atom :=
-  Set.range (fun (A : Proposition Atom) ↦ ¬¬A → A)
-
-/-- A theory is intuitionistic if it validates ex falso quodlibet. -/
-@[scoped grind]
-class IsIntuitionistic [Bot Atom] (T : Theory Atom) where
-  efq (A : Proposition Atom) : (⊥ → A) ∈ T
+abbrev IPL (Atom : Type u) [Bot Atom] : Theory Atom := {⊥ → A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-@[scoped grind =]
-theorem isIntuitionisticIff [Bot Atom] (T : Theory Atom) : IsIntuitionistic T ↔ IPL ⊆ T := by grind
+lemma efq_mem_ipl [Bot Atom] (A : Proposition Atom) : (⊥ → A) ∈ IPL Atom := ⟨A, rfl⟩
 
-/-- A theory is classical if it validates double-negation elimination. -/
-@[scoped grind]
-class IsClassical [Bot Atom] (T : Theory Atom) where
-  dne (A : Proposition Atom) : (¬¬A → A) ∈ T
-
-omit [DecidableEq Atom] in
-@[scoped grind =]
-theorem isClassicalIff [Bot Atom] (T : Theory Atom) : IsClassical T ↔ CPL ⊆ T := by grind
-
-instance instIsIntuitionisticIPL [Bot Atom] : IsIntuitionistic (Atom := Atom) IPL where
-  efq A := Set.mem_range.mpr ⟨A, rfl⟩
+/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
+@[reducible]
+def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
+  (WithBot.some <$> T) ∪ IPL (WithBot Atom)
 
-instance instIsClassicalCPL [Bot Atom] : IsClassical (Atom := Atom) CPL where
-  dne A := Set.mem_range.mpr ⟨A, rfl⟩
+/-- Classical logic further adds double negation elimination. -/
+abbrev CPL (Atom : Type u) [Bot Atom] : Theory Atom := {¬¬A → A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
-@[scoped grind →]
-theorem instIsIntuitionisticExtention [Bot Atom] {T T' : Theory Atom} [IsIntuitionistic T]
-    (h : T ⊆ T') : IsIntuitionistic T' := by grind
+lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom := ⟨A, rfl⟩
 
-omit [DecidableEq Atom] in
-@[scoped grind →]
-theorem instIsClassicalExtention [Bot Atom] {T T' : Theory Atom} [IsClassical T] (h : T ⊆ T') :
-    IsClassical T' := by grind
+open InferenceSystem
 
-/-- Attach a bottom element to a theory `T`, and the principle of explosion for that bottom. -/
-@[reducible]
-def intuitionisticCompletion (T : Theory Atom) : Theory (WithBot Atom) :=
-  (WithBot.some <$> T) ∪ IPL
+/-- An inference system is intuitionistic if it derives ex falso quodlibet. -/
+@[scoped grind]
+class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
+    [InferenceSystem S (Proposition Atom)] where
+  efq (A : Proposition Atom) : S⇓(⊥ → A)
 
-instance instIsIntuitionisticIntuitionisticCompletion (T : Theory Atom) :
-    IsIntuitionistic T.intuitionisticCompletion := by grind
+/-- An inference system is classical if it validates double-negation elimination. -/
+@[scoped grind]
+class IsClassical (Atom : Type u) [Bot Atom] (S : Type*)
+    [InferenceSystem S (Proposition Atom)] where
+  dne (A : Proposition Atom) : S⇓(¬¬A → A)
 
 end Cslib.Logic.PL.Theory
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
index ba3f5bbac..8bf3b1273 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Basic.lean
@@ -11,8 +11,6 @@ public import Mathlib.Data.Finset.Insert
 public import Mathlib.Data.Finset.SDiff
 public import Mathlib.Data.Finset.Image
 
-@[expose] public section
-
 /-! # Natural deduction for propositional logic
 
 We define, for minimal logic, deduction trees (a `Type`) and derivability (a `Prop`) relative to a
@@ -61,6 +59,8 @@ in §2.2 of Sorensen & Urzyczyn's *Lectures on the Curry-Howard Isomorphism*. (S
 references welcome!)
 -/
 
+@[expose] public section
+
 universe u
 
 namespace Cslib.Logic.PL
@@ -156,7 +156,7 @@ theorem Theory.equiv_iff {A B : Proposition Atom} :
     exact ⟨D, E⟩
 
 /-- Minimally equivalent propositions. -/
-abbrev Equiv : Proposition Atom → Proposition Atom → Prop := MPL.Equiv
+abbrev Equiv : Proposition Atom → Proposition Atom → Prop := (MPL Atom).Equiv
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => Equiv
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
new file mode 100644
index 000000000..94c4fdb29
--- /dev/null
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -0,0 +1,57 @@
+/-
+Copyright (c) 2025 Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas Waring
+-/
+module
+
+public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+
+/-! # Results on propositional theories -/
+
+@[expose] public section
+
+universe u
+
+namespace Cslib.Logic.PL
+
+open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical
+
+variable {Atom : Type u} [DecidableEq Atom] [Bot Atom]
+
+namespace Theory
+
+instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where
+  efq A := ax (efq_mem_ipl A)
+
+instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
+  dne A := ax (dne_mem_cpl A)
+
+def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
+
+omit [DecidableEq Atom] in
+lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩
+
+def Pierce (Atom : Type u) [Bot Atom] : Theory Atom :=
+  {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)}
+
+omit [DecidableEq Atom] in
+lemma pierce_mem_pierce (A B : Proposition Atom) : (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩
+
+instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where
+  dne A := by
+    apply implI
+    apply orE (ax <| Set.mem_union_left _ <| lem_mem_lem A)
+    · exact ass (Finset.mem_insert_self A _)
+    · apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+      apply implE (A := ¬ A) <;> exact ass (by grind)
+
+instance instIsClassicalPierce : IsClassical Atom (Pierce Atom ∪ IPL Atom : Theory Atom) where
+  dne A := by
+    apply implI
+    apply implE (A := (A → ⊥) → A) (ax <| Set.mem_union_left _ <| pierce_mem_pierce A ⊥)
+    apply implI
+    apply implE (A := ⊥) (ax <| Set.mem_union_right _ (efq_mem_ipl A))
+    apply implE (A := ¬ A) <;> exact ass (by grind)
+
+end Cslib.Logic.PL.Theory
diff --git a/lake-manifest.json b/lake-manifest.json
index 3dcdfeb38..64919030b 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2d59066e04cb90e9fa4d1393a8cd1ee8ace8daa7",
+   "rev": "69c8a067c87c2bb6ba583f03fbf46090564be370",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

From 08119c23472d58ffa2720fd29b42f41e7c17b04d Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Sat, 2 May 2026 17:32:21 +0200
Subject: [PATCH 2/7] derived rules

---
 Cslib/Logics/Propositional/Defs.lean          |  8 +++--
 .../NaturalDeduction/Theory.lean              | 33 ++++++++++++++++++-
 lake-manifest.json                            |  2 +-
 3 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index 51ff3a9ba..e53855b6f 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -120,13 +120,17 @@ lemma dne_mem_cpl [Bot Atom] (A : Proposition Atom) : (¬¬A → A) ∈ CPL Atom
 
 open InferenceSystem
 
-/-- An inference system is intuitionistic if it derives ex falso quodlibet. -/
+/-- An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be
+generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
+implication connective. -/
 @[scoped grind]
 class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
   efq (A : Proposition Atom) : S⇓(⊥ → A)
 
-/-- An inference system is classical if it validates double-negation elimination. -/
+/-- An inference system is classical if it validates double-negation elimination. TODO: this should
+be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an
+implication connective. -/
 @[scoped grind]
 class IsClassical (Atom : Type u) [Bot Atom] (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index 94c4fdb29..c2c72c9b0 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -17,16 +17,47 @@ namespace Cslib.Logic.PL
 
 open Proposition Theory InferenceSystem DerivableIn Derivation IsIntuitionistic IsClassical
 
-variable {Atom : Type u} [DecidableEq Atom] [Bot Atom]
+variable {Atom : Type u} [DecidableEq Atom] [Bot Atom] {T : Theory Atom}
 
 namespace Theory
 
 instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where
   efq A := ax (efq_mem_ipl A)
 
+def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
+    : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weak_ctx (Finset.empty_subset Γ)
+
+def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
+    (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
+  implE (A := ⊥) (efqCtx Γ A) D
+
+def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Proposition Atom)
+    (hΓ : A ∈ Γ) (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) :=
+  efqRule Γ B <| implE (ass hΓ') (ass hΓ)
+
 instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
   dne A := ax (dne_mem_cpl A)
 
+def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition Atom}
+    (D : T⇓(insert (¬ A) Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
+  implE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weak_ctx <| Finset.empty_subset ..) D.implI
+
+instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where
+  efq A := implI _ <| byContra <| ass (by grind)
+
+def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by
+  apply byContra
+  apply implE (ass <| Finset.mem_insert_self ..)
+  apply orI₂; apply implI
+  apply implE (A := A ∨ ¬ A) (ass <| by grind)
+  exact orI₁ <| ass <| Finset.mem_insert_self ..
+
+def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A → B) → A) → A) := by
+  apply implI; apply byContra
+  apply implE (ass <| Finset.mem_insert_self ..)
+  apply implE (A := A → B) (ass <| by grind); apply implI
+  apply contra A B <;> grind
+
 def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
diff --git a/lake-manifest.json b/lake-manifest.json
index 64919030b..499d98946 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "69c8a067c87c2bb6ba583f03fbf46090564be370",
+   "rev": "d9874e4268b90436f38b811922d5aff6af138197",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",

From 656ae2a941c346d48448493e557d8ca3813d1cc5 Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Sat, 2 May 2026 17:41:12 +0200
Subject: [PATCH 3/7] docs

---
 .../Propositional/NaturalDeduction/Theory.lean       | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index c2c72c9b0..47e7c99e4 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -24,13 +24,16 @@ namespace Theory
 instance instIsIntuitionisticIPL : IsIntuitionistic Atom (IPL Atom) where
   efq A := ax (efq_mem_ipl A)
 
+/-- Derivation of efq in an arbitrary context. -/
 def IsIntuitionistic.efqCtx [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
     : T⇓(Γ ⊢ ⊥ → A) := (efq A : T⇓(⊥ → A)).weak_ctx (Finset.empty_subset Γ)
 
+/-- Efq as a derived rule. -/
 def IsIntuitionistic.efqRule [IsIntuitionistic Atom T] (Γ : Ctx Atom) (A : Proposition Atom)
     (D : T⇓(Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
   implE (A := ⊥) (efqCtx Γ A) D
 
+/-- Prove any proposition from contradictory hypotheses. -/
 def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Proposition Atom)
     (hΓ : A ∈ Γ) (hΓ' : (¬A) ∈ Γ) : T⇓(Γ ⊢ B) :=
   efqRule Γ B <| implE (ass hΓ') (ass hΓ)
@@ -38,6 +41,7 @@ def IsIntuitionistic.contra [IsIntuitionistic Atom T] {Γ : Ctx Atom} (A B : Pro
 instance instIsClassicalCPL : IsClassical Atom (CPL Atom) where
   dne A := ax (dne_mem_cpl A)
 
+/-- Proof by contradiction as a derived rule. -/
 def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition Atom}
     (D : T⇓(insert (¬ A) Γ ⊢ ⊥)) : T⇓(Γ ⊢ A) :=
   implE (A := ¬¬A) ((dne A : T⇓(¬¬A → A)) |>.weak_ctx <| Finset.empty_subset ..) D.implI
@@ -45,6 +49,7 @@ def IsClassical.byContra [IsClassical Atom T] {Γ : Ctx Atom} {A : Proposition A
 instance instIsIntuitionisticOfIsClassical [IsClassical Atom T] : IsIntuitionistic Atom T where
   efq A := implI _ <| byContra <| ass (by grind)
 
+/-- Law of excluded middle in a classical theory. -/
 def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬ A) := by
   apply byContra
   apply implE (ass <| Finset.mem_insert_self ..)
@@ -52,21 +57,24 @@ def IsClassical.lem [IsClassical Atom T] (A : Proposition Atom) : T⇓(A ∨ ¬
   apply implE (A := A ∨ ¬ A) (ass <| by grind)
   exact orI₁ <| ass <| Finset.mem_insert_self ..
 
+/-- Pierce's law in a classical theory. -/
 def IsClassical.pierce [IsClassical Atom T] (A B : Proposition Atom) : T⇓(((A → B) → A) → A) := by
   apply implI; apply byContra
   apply implE (ass <| Finset.mem_insert_self ..)
   apply implE (A := A → B) (ass <| by grind); apply implI
   apply contra A B <;> grind
 
+/-- The axiom system consisting of instances of LEM. -/
 def LEM (Atom : Type u) [Bot Atom] : Theory Atom := {A ∨ ¬ A | A : Proposition Atom}
 
 omit [DecidableEq Atom] in
 lemma lem_mem_lem (A : Proposition Atom) : (A ∨ ¬ A) ∈ LEM Atom := ⟨A, rfl⟩
 
-def Pierce (Atom : Type u) [Bot Atom] : Theory Atom :=
+/-- The axiom system consisting of instances of Pierce's law. -/
+def Pierce (Atom : Type u) : Theory Atom :=
   {((A → B) → A) → A | (A : Proposition Atom) (B : Proposition Atom)}
 
-omit [DecidableEq Atom] in
+omit [DecidableEq Atom] [Bot Atom] in
 lemma pierce_mem_pierce (A B : Proposition Atom) : (((A → B) → A) → A) ∈ Pierce Atom := ⟨A, B, rfl⟩
 
 instance instIsClassicalLEM : IsClassical Atom (LEM Atom ∪ IPL Atom : Theory Atom) where

From c97855a37d34ce7c8bd6ac1fbf4e98df4f62fd6d Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Sat, 2 May 2026 17:50:17 +0200
Subject: [PATCH 4/7] fix build Computability.Automata.NA.Concat

---
 Cslib/Computability/Automata/NA/Concat.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Computability/Automata/NA/Concat.lean b/Cslib/Computability/Automata/NA/Concat.lean
index 0b2c10d3e..7cc7c1c18 100644
--- a/Cslib/Computability/Automata/NA/Concat.lean
+++ b/Cslib/Computability/Automata/NA/Concat.lean
@@ -177,7 +177,7 @@ theorem finConcat_language_eq [Inhabited Symbol] :
     obtain ⟨ss, ⟨_, h_ωtr⟩, _⟩ := concat_run_exists h_xl1 h_run2
     #adaptation_note
     /-- A grind regression found moving to nightly-2026-03-31 (changes from lean#13166) -/
-    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (xl1.length + xl2.length))
+    have h_mtr := LTS.OmegaExecution.extract_mTr h_ωtr (zero_le (a := xl1.length + xl2.length))
     simp [← append_append_ωSequence, extract_eq_drop_take,
       take_append_of_le_length, ← List.length_append] at h_mtr
     have : ss (xl1.length + xl2.length) = (ss.drop xl1.length) xl2.length := by grind

From 95044bb3e25520d4f18b0da4ce62afed535f2187 Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Sat, 2 May 2026 21:13:01 +0200
Subject: [PATCH 5/7] docs

---
 Cslib/Logics/Propositional/Defs.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/Cslib/Logics/Propositional/Defs.lean b/Cslib/Logics/Propositional/Defs.lean
index e53855b6f..e9c603d91 100644
--- a/Cslib/Logics/Propositional/Defs.lean
+++ b/Cslib/Logics/Propositional/Defs.lean
@@ -126,6 +126,7 @@ implication connective. -/
 @[scoped grind]
 class IsIntuitionistic (Atom : Type u) [Bot Atom] (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
+  /-- The principle of explosion (ex falso quolibet). -/
   efq (A : Proposition Atom) : S⇓(⊥ → A)
 
 /-- An inference system is classical if it validates double-negation elimination. TODO: this should
@@ -134,6 +135,7 @@ implication connective. -/
 @[scoped grind]
 class IsClassical (Atom : Type u) [Bot Atom] (S : Type*)
     [InferenceSystem S (Proposition Atom)] where
+  /-- Double-negation elimination. -/
   dne (A : Proposition Atom) : S⇓(¬¬A → A)
 
 end Cslib.Logic.PL.Theory

From 723b9df4cc52d8f0202762ae6cd05a33b69aeb0a Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Sat, 2 May 2026 21:24:24 +0200
Subject: [PATCH 6/7] init

---
 Cslib.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib.lean b/Cslib.lean
index 37a038ee4..d525304b6 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -131,3 +131,4 @@ public import Cslib.Logics.LinearLogic.CLL.MLL
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
+public import Cslib.Logics.Propositional.NaturalDeduction.Theory

From f8615dde2f73b9062430ae83127043bf3fd3b30f Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Mon, 4 May 2026 10:24:32 +0200
Subject: [PATCH 7/7] header docstring

---
 Cslib/Logics/Propositional/NaturalDeduction/Theory.lean | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
index 47e7c99e4..7ba28cca6 100644
--- a/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
+++ b/Cslib/Logics/Propositional/NaturalDeduction/Theory.lean
@@ -7,7 +7,12 @@ module
 
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
 
-/-! # Results on propositional theories -/
+/-! # Results on propositional theories
+
+In this file we prove the expected results that `IPL Atom` is an intuitionistic theory, and
+`CPL Atom` is a classical theory. We provide derived rules for common intuitionistic and classical
+proof patterns.
+-/
 
 @[expose] public section