From c43bd6dcc515851c9d447467d0b656b52191f6f3 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Mon, 10 Aug 2026 10:50:44 +0200
Subject: [PATCH 01/42] IsAxiom and axiom L

---
 Cslib/Logics/Modal/Basic.lean | 103 +++++++++++++++++++++++-----------
 Cslib/Logics/Modal/Cube.lean  |   6 +-
 CslibTests/Modal.lean         |  18 +++---
 3 files changed, 85 insertions(+), 42 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index b00710b46..063bbab2b 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -16,7 +16,7 @@ public import Mathlib.Logic.Nonempty
 /-! # Modal Logic
 
 Modal logic is a logic for reasoning about relational structures, studying statements about
-necessity (`□φ`) and possibility `◇φ`.
+necessity (`□φ`) and possibility (`◇φ`).
 
 ## References
 
@@ -47,6 +47,9 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
+/-- Utility to coerce atoms into atomic propositions. -/
+instance : Coe Atom (Proposition Atom) := ⟨.atom⟩
+
 instance : HasNot (Proposition Atom) := ⟨.not⟩
 instance : HasAnd (Proposition Atom) := ⟨.and⟩
 instance : HasDiamond (Proposition Atom) := ⟨.diamond⟩
@@ -203,27 +206,40 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
   apply TheoryEq.ext_iff.1 at h
   exact (h φ).mp hs
 
+/-- A proposition `φ` is an axiom under the relation `r` (the 'frame') if it holds for all
+valuations and worlds. -/
+abbrev IsAxiom (r : World → World → Prop) (φ : Proposition Atom) := ∀ v w, ⇓Modal[⟨r, v⟩,w ⊨ φ]
+
+/-- If a proposition is an axiom under the relation of a model, it is satisfied by every world. -/
+@[scoped grind .]
+theorem Satisfies.of_isAxiom (m : Model World Atom) (φ : Proposition Atom) (h : IsAxiom m.r φ)
+    (w : World) : ⇓Modal[m,w ⊨ φ] := h m.v w
+
 /-- The K axiom, valid for all models. -/
-theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
+theorem Satisfies.k (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    IsAxiom r <| □(φ₁ → φ₂) → (□φ₁ → □φ₂) := by grind
 
 /-- The dual axiom, valid for all models. -/
-theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
+theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
+    IsAxiom r <| ◇φ ↔ ¬□¬φ := by
+  intro _ w
   simp only [Satisfies.iff_iff_iff]
   constructor
   · grind
   · grind only [= not_iff_not, = diamond_iff_exists, = box_iff_forall]
 
 /-- The T axiom, valid for all reflexive models. -/
-theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
-    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → ◇φ] := by grind [instRefl.refl w]
+theorem Satisfies.t (r : World → World → Prop) [instRefl : Std.Refl r] (φ : Proposition Atom)
+    : IsAxiom r <| φ → ◇φ := by
+  grind [instRefl.refl]
 
 /-- Any model that admits the axiom T is reflexive. -/
-theorem Satisfies.t_refl {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → ◇φ]) : Std.Refl r where
+theorem Satisfies.t_refl (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, IsAxiom r <| φ → ◇φ) : Std.Refl r where
   refl w := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w
-    let h' := h (v := v) (w := w) (φ := .atom a)
+    let h' := h (v := v) (w := w) (φ := a)
     grind
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/
@@ -232,70 +248,93 @@ theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ]
   grind
 
 /-- The B axiom, valid for all symmetric models. -/
-theorem Satisfies.b {m : Model World Atom} [Std.Symm m.r] {w : World} (φ : Proposition Atom) :
-    ⇓Modal[m,w ⊨ φ → □◇φ] := by
-  have := Std.Symm.symm (r := m.r) w
+theorem Satisfies.b (r : World → World → Prop) [Std.Symm r] (φ : Proposition Atom) :
+    IsAxiom r <| φ → □◇φ := by
+  intro _ w
+  have := Std.Symm.symm (r := r) w
   grind
 
 /-- Any model that admits the axiom B is symmetric. -/
-theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ φ → □◇φ]) : Std.Symm r where
+theorem Satisfies.b_symm (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, IsAxiom r <| φ → □◇φ) : Std.Symm r where
   symm w₁ := by
     have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
-    let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
+    let h₁ := h (v := v₁) (w := w₁) (φ := a)
     simp [imp_iff_imp] at h₁
     grind
 
 /-- The 4 axiom, valid for all transitive models. -/
-theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World}
-    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by
+theorem Satisfies.four (r : World → World → Prop) [IsTrans World r]
+    (φ : Proposition Atom) : IsAxiom r <| ◇◇φ → ◇φ := by
+  intro _ _
   simp only [imp_iff_imp]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
   exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩
 
 /-- Any model that admits 4 is transitive. -/
-theorem Satisfies.four_trans {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇◇φ → ◇φ]) : IsTrans World r where
+theorem Satisfies.four_trans (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ (φ : Proposition Atom), IsAxiom r <| ◇◇φ → ◇φ) : IsTrans World r where
   trans w₁ w₂ w₃ h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
 /-- The 5 axiom, valid for all Euclidean models. -/
-theorem Satisfies.five {m : Model World Atom} [Relation.RightEuclidean m.r]
-    {w : World}
-    (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇φ → □◇φ] := by
-  have := @Relation.RightEuclidean.rightEuclidean (r := m.r)
+theorem Satisfies.five (r : World → World → Prop) [Relation.RightEuclidean r]
+    (φ : Proposition Atom) : IsAxiom r <| ◇φ → □◇φ := by
+  have := @Relation.RightEuclidean.rightEuclidean (r := r)
   grind
 
 /-- Any model that admits 5 is Euclidean. -/
-theorem Satisfies.five_rightEuclidean {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w : World} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇φ → □◇φ]) :
+theorem Satisfies.five_rightEuclidean (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, IsAxiom r <| ◇φ → □◇φ) :
     Relation.RightEuclidean r where
   rightEuclidean {w₁ w₂ w₃} h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
 /-- The D axiom, valid for all serial models. -/
-theorem Satisfies.d {m : Model World Atom} [Relation.Serial m.r] {w} (φ : Proposition Atom) :
-    ⇓Modal[m,w ⊨ □φ → ◇φ] := by
-  have : ∃ w', m.r w w' := Relation.Serial.serial w
+theorem Satisfies.d (r : World → World → Prop) [Relation.Serial r] (φ : Proposition Atom) :
+    IsAxiom r <| □φ → ◇φ := by
+  intro _ w
+  have : ∃ w', r w w' := Relation.Serial.serial w
   grind
 
 /-- Any model that admits D is serial. -/
-theorem Satisfies.d_serial {r : World → World → Prop} [Nonempty Atom]
-    (h : ∀ {v} {w} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ □φ → ◇φ]) : Relation.Serial r where
+theorem Satisfies.d_serial (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, IsAxiom r <| □φ → ◇φ) : Relation.Serial r where
   serial w₁ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₁
-    let h' := h (v := v) (w := w₁) (φ := .atom a)
+    let h' := h (v := v) (w := w₁) (φ := a)
     grind
 
+/-- The L axiom, or Löb's theorem, valid for all transitive and converse well-founded models. -/
+theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
+    (hwf : WellFounded (flip r)) (φ : Proposition Atom) : IsAxiom r <| □(□φ → φ) → □φ := by
+  intro v w
+  let m := Model.mk r v
+  rw [Satisfies.imp_iff_imp]
+  intro h
+  rw [Satisfies.box_iff_forall] at h ⊢
+  intro w' hw'
+  have h' : ∀ w', r w w' → ⇓Modal[m, w' ⊨ φ] := by
+    intro w'
+    refine (WellFounded.induction (C := fun w' => m.r w w' → ⇓Modal[m,w' ⊨ φ]) hwf w' ?_)
+    intro w' ih hww'
+    have hImp : ⇓Modal[m, w' ⊨ □φ → φ] := h _ hww'
+    rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall] at hImp
+    apply hImp
+    intro w'' hw'w''
+    apply ih _ hw'w''
+    exact IsTrans.trans _ _ _ hww' hw'w''
+  exact h' w' hw'
+
 /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under
 all models in `S` for all worlds. -/
 @[simp, scoped grind =]
diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 765193ac0..57c7dc46f 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -135,6 +135,10 @@ section Validity
 This section showcases how to prove the expected validities in the different modal logics.
 -/
 
+open InferenceSystem
+
+open scoped Satisfies
+
 /-- The axiom K is valid in the logic K. -/
 theorem K.k_valid : (□(φ₁ → φ₂) → (□φ₁ → □φ₂) : Proposition Atom) ∈ K World Atom := by
   open scoped Proposition in grind [Satisfies.k]
@@ -142,7 +146,7 @@ theorem K.k_valid : (□(φ₁ → φ₂) → (□φ₁ → □φ₂) : Proposit
 /-- The axiom T is valid in the logic T. -/
 theorem T.t_valid : (φ → ◇φ : Proposition Atom) ∈ T World Atom := by
   intro _ h
-  grind [Satisfies.t (instRefl := (by assumption))]
+  grind [Satisfies.t (instRefl := h)]
 
 end Validity
 
diff --git a/CslibTests/Modal.lean b/CslibTests/Modal.lean
index be9f5b880..e9a2bdb61 100644
--- a/CslibTests/Modal.lean
+++ b/CslibTests/Modal.lean
@@ -19,19 +19,19 @@ example : ((◇◇φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈
   intro m h w
   let : IsTrans World m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ D4 World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : IsTrans World m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.four φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.four _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ D5 World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example :
     Proposition.and (□φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈
@@ -40,31 +40,31 @@ example :
   let : Relation.Serial m.r := h.1
   let : IsTrans World m.r := h.2.1
   let : Relation.RightEuclidean m.r := h.2.2
-  exact ⟨Satisfies.d φ, Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((□φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ DB World Atom := by
   intro m h w
   let : Relation.Serial m.r := h.1
   let : Std.Symm m.r := h.2
-  exact ⟨Satisfies.d φ, Satisfies.b φ⟩
+  exact ⟨Satisfies.d _ φ _ _, Satisfies.b _ φ _ _⟩
 
 example : ((φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ TB World Atom := by
   intro m h w
   let : Std.Refl m.r := h.1
   let : Std.Symm m.r := h.2
-  exact ⟨Satisfies.t φ, Satisfies.b φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.b _ φ _ _⟩
 
 example : ((φ → □◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ KB5 World Atom := by
   intro m h w
   let : Std.Symm m.r := h.1
   let : Relation.RightEuclidean m.r := h.2
-  exact ⟨Satisfies.b φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.b _ φ _ _, Satisfies.five _ φ _ _⟩
 
 example : ((φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ S4 World Atom := by
   intro m h w
   let : Std.Refl m.r := h.1
   let : IsTrans World m.r := h.2
-  exact ⟨Satisfies.t φ, Satisfies.four φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.four _ φ _ _⟩
 
 example :
     Proposition.and (φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈
@@ -73,6 +73,6 @@ example :
   let : Std.Refl m.r := h.1
   let : IsTrans World m.r := h.2.1
   let : Relation.RightEuclidean m.r := h.2.2
-  exact ⟨Satisfies.t φ, Satisfies.four φ, Satisfies.five φ⟩
+  exact ⟨Satisfies.t _ φ _ _, Satisfies.four _ φ _ _, Satisfies.five _ φ _ _⟩
 
 end Cslib.Logic.Modal

From 7ab403b93e7f60383da88968423b3a451a032a7b Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Fri, 14 Aug 2026 13:53:38 +0200
Subject: [PATCH 02/42] Lean modal model and refactoring of modal logical
 equivalence

---
 Cslib.lean                                 |   2 +
 Cslib/Foundations/Relation/Defs.lean       |   3 +
 Cslib/Foundations/Syntax/Congruence.lean   |   6 +-
 Cslib/Languages/CCS/BehaviouralTheory.lean |   7 +-
 Cslib/Logics/Modal/Basic.lean              |  51 ++++++
 Cslib/Logics/Modal/Denotation.lean         |  18 ++
 Cslib/Logics/Modal/Lean/Basic.lean         | 123 ++++++++++++++
 Cslib/Logics/Modal/Lean/SMul.lean          | 101 ++++++++++++
 Cslib/Logics/Modal/LogicalEquivalence.lean | 182 +++++++++++++++++----
 CslibTests.lean                            |   1 +
 CslibTests/Modal/Ideal.lean                | 116 +++++++++++++
 11 files changed, 573 insertions(+), 37 deletions(-)
 create mode 100644 Cslib/Logics/Modal/Lean/Basic.lean
 create mode 100644 Cslib/Logics/Modal/Lean/SMul.lean
 create mode 100644 CslibTests/Modal/Ideal.lean

diff --git a/Cslib.lean b/Cslib.lean
index a4da6b124..149a0a9b1 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -169,6 +169,8 @@ public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic
 public import Cslib.Logics.Modal.Basic
 public import Cslib.Logics.Modal.Cube
 public import Cslib.Logics.Modal.Denotation
+public import Cslib.Logics.Modal.Lean.Basic
+public import Cslib.Logics.Modal.Lean.SMul
 public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Propositional.Defs
 public import Cslib.Logics.Propositional.NaturalDeduction.Basic
diff --git a/Cslib/Foundations/Relation/Defs.lean b/Cslib/Foundations/Relation/Defs.lean
index 4901f785d..51e0729a0 100644
--- a/Cslib/Foundations/Relation/Defs.lean
+++ b/Cslib/Foundations/Relation/Defs.lean
@@ -67,6 +67,9 @@ abbrev SemiConfluent (r : α → α → Prop) :=
 /-- A relation has the Church Rosser property when equivalence implies multi-joinability. -/
 abbrev ChurchRosser (r : α → α → Prop) := ∀ {x y}, EqvGen r x y → Join (ReflTransGen r) x y
 
+/-- Relation `r` preserves predicate `P`. -/
+def Preserves (r : α → α → Prop) (P : α → Prop) : Prop := ∀ ⦃a b⦄, r a b → P a → P b
+
 /-- An element is reducible with respect to a relation if there is a value it is related to. -/
 abbrev Reducible (r : α → α → Prop) (x : α) : Prop := ∃ y, r x y
 
diff --git a/Cslib/Foundations/Syntax/Congruence.lean b/Cslib/Foundations/Syntax/Congruence.lean
index 25c954c2d..51ce37eae 100644
--- a/Cslib/Foundations/Syntax/Congruence.lean
+++ b/Cslib/Foundations/Syntax/Congruence.lean
@@ -24,7 +24,7 @@ class Congruence (r : α → α → Prop)
 
 /-- `a ≡[r] b` means that the `a` and `b` are related by the congruence `r`. -/
 @[nolint unusedArguments]
-def Congruence.r (r : α → α → Prop) [Congruence r] := r
+abbrev Congruence.r (r : α → α → Prop) [Congruence r] := r
 
 @[inherit_doc]
 scoped notation:29 a " ≡[" r "] " b => Congruence.r r a b
@@ -35,7 +35,7 @@ class DefaultCongruence (α : Type*) (r : outParam (α → α → Prop))
 /-- `a ≡ b` means that `a` and `b` are related by the canonical congruence relation for their
 type. -/
 @[nolint unusedArguments]
-def DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
+abbrev DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
 
 @[inherit_doc]
 scoped infix:29 " ≡ " => DefaultCongruence.r
@@ -45,6 +45,6 @@ instance (α : Type*) (r : α → α → Prop) [DefaultCongruence α r] : Congru
 
 /-- An equivalence relation on `α` preserved by all contexts. -/
 class LawfulCongruence (r : α → α → Prop) [Congruence r] [HasContext α] extends
-  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) (· ≡[r] ·)
+  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
 
 end Cslib
diff --git a/Cslib/Languages/CCS/BehaviouralTheory.lean b/Cslib/Languages/CCS/BehaviouralTheory.lean
index cd5a00f9d..b8770c350 100644
--- a/Cslib/Languages/CCS/BehaviouralTheory.lean
+++ b/Cslib/Languages/CCS/BehaviouralTheory.lean
@@ -444,11 +444,8 @@ theorem bisimilarity_is_congruence
 instance : Congruence (HomBisimilarity (lts (defs := defs))) := ⟨⟩
 
 /-- Bisimilarity is a congruence in CCS. -/
-instance bisimilarityCongruence :
-    LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
-  elim := by
-    dsimp [Congruence.r]
-    grind [Covariant, bisimilarity_is_congruence]
+instance bisimilarityCongruence : LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
+  elim := by grind [Covariant, bisimilarity_is_congruence]
 
 end CCS
 
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 063bbab2b..62aa37941 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -228,6 +228,14 @@ theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
   · grind
   · grind only [= not_iff_not, = diamond_iff_exists, = box_iff_forall]
 
+/-- Possibility preserves conjunction in all models. -/
+theorem Satisfies.diamond_and (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    IsAxiom r <| ◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂) := by grind
+
+/-- Possibility can be combined with necessity. -/
+theorem Satisfies.diamond_and_box (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    IsAxiom r <| (◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂) := by grind
+
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t (r : World → World → Prop) [instRefl : Std.Refl r] (φ : Proposition Atom)
     : IsAxiom r <| φ → ◇φ := by
@@ -335,6 +343,30 @@ theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
     exact IsTrans.trans _ _ _ hww' hw'w''
   exact h' w' hw'
 
+open Relation in
+/-- Axiom .2, valid for all frames with the diamond property. -/
+theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
+    (φ : Proposition Atom) : IsAxiom r <| ◇□φ → □◇φ := by
+  intro v w
+  rw [Satisfies.imp_iff_imp]
+  intro h₁
+  rw [Satisfies.diamond_iff_exists] at h₁
+  rcases h₁ with ⟨_, hww₁, _⟩
+  rw [Satisfies.box_iff_forall]
+  intro _ hww₂
+  obtain ⟨w₃, hww₃⟩ := h hww₁ hww₂
+  grind
+
+open Relation in
+/-- Any model that admits axiom .2 has the diamond property. -/
+theorem Satisfies.pointTwo_diamond (r : World → World → Prop) [Nonempty Atom]
+    (h : ∀ φ : Proposition Atom, IsAxiom r <| ◇□φ → □◇φ) : Diamond r := by
+  intro w w₁ w₂ hww₁ hww₂
+  have a := Classical.arbitrary Atom
+  let v := fun (w' : World) (a : Atom) => r w₁ w'
+  have h' := h a v w
+  grind [Join]
+
 /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under
 all models in `S` for all worlds. -/
 @[simp, scoped grind =]
@@ -346,4 +378,23 @@ def Proposition.valid (S : Set (Model World Atom)) (φ : Proposition Atom) : Pro
 def logic (S : Set (Model World Atom)) : Set (Proposition Atom) :=
   {φ | φ.valid S}
 
+/-- Modal logic is antitone (wrt the class of models). -/
+theorem logic_antitone : Antitone (logic (World := World) (Atom := Atom)) :=
+  fun _ _ hS₁S₂ _ hφ m hm w => hφ m (hS₁S₂ hm) w
+
+/-- The class of all models generated by a frame (relation). -/
+abbrev modelsOfRelation (r : World → World → Prop) : Set (Model World Atom) :=
+  {m | m.r = r}
+
+/-- A proposition is an axiom of a frame exactly when it belongs to the logic of all models over
+that frame. -/
+theorem isAxiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
+    IsAxiom r φ ↔ φ ∈ logic (modelsOfRelation r) := by
+  apply Iff.intro
+  case mp =>
+    intro h m hm w
+    subst hm
+    exact h m.v w
+  case mpr => grind
+
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 4b3415b33..7f64b6f91 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi
 module
 
 public import Cslib.Logics.Modal.Basic
+public import Cslib.Logics.Modal.LogicalEquivalence
 
 /-! # Denotational semantics for Modal Logic
 
@@ -48,4 +49,21 @@ theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} :
     (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by
   apply Iff.intro <;> grind [_=_ satisfies_mem_denotation]
 
+/-- Logically equivalent propositions under a model have the same denotation. -/
+theorem Proposition.equiv_iff_denotation_eq :
+    (φ₁ ≡[Equiv m] φ₂) ↔ φ₁.denotation m = φ₂.denotation m := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    ext w
+    grind [h w]
+  case mpr =>
+    intro w
+    rw [Set.ext_iff] at h
+    grind [h w]
+
+/-- `grind`-friendly first part of `Proposition.equiv_iff_denotation_eq`. -/
+@[scoped grind ⇒]
+theorem Proposition.denotation_eq_of_equiv (h : φ₁ ≡[Equiv m] φ₂) :
+    φ₁.denotation m = φ₂.denotation m := equiv_iff_denotation_eq.1 h
+
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
new file mode 100644
index 000000000..6e79b160a
--- /dev/null
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -0,0 +1,123 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Logics.Modal.Basic
+public import Cslib.Logics.Modal.LogicalEquivalence
+public import Cslib.Logics.Modal.Denotation
+
+/-! # Modal Logic for Lean
+
+This module develops the interplay between modal logic and Lean's propositional language, in order
+to enable the use of modal logic to reason about standard Lean relations using `Prop`.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+namespace Model
+
+/-- Given a relation `r` on `α`, constructs the modal model whose worlds are elements of `α`
+and whose atoms are Lean predicates on `α` (`α → Prop`).
+
+Valuation checks that a world satisfies a predicate. For example, under `Model.ofPredicates r`, `□P`
+at `a : α` means that `P a'` holds at every `a'` such that `r a a'`. -/
+abbrev ofPredicates (r : α → α → Prop) : Model α (α → Prop) where
+  r := r
+  v w P := P w
+
+/-- Given a relation `r` on `α` and a container type `β` for `α` (`Membership α β`), constructs the
+modal model whose worlds are elements of `α` and whose atoms are of type `β`.
+
+Valuation is membership. For example, under `Model.ofContainers r`, `□b` at `a : α` means that
+`a' ∈ b` holds for every `a'` such that `r a a'`. -/
+abbrev ofContainers [Membership α β] (r : α → α → Prop) : Model α β where
+  r := r
+  v w p := w ∈ p
+
+/-- Abbreviation for `Model.ofContainers` where the container type is a `Set`. -/
+abbrev ofSets (r : α → α → Prop) : Model α (Set α) := ofContainers r
+
+/-- The set model and predicate model of a relation are definitionally equal. -/
+theorem ofSets_eq_ofPredicates (r : α → α → Prop) :
+    ofSets r = ofPredicates r := rfl
+
+end Model
+
+open Model Relation
+open scoped InferenceSystem Satisfies
+
+/-! ## Models of Lean predicates -/
+
+/-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
+@[scoped grind =]
+theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
+    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind
+
+/-- Under `Model.ofPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/
+@[scoped grind ⇒]
+theorem Satisfies.ofPredicates_preserves_iff {P : α → Prop} (r : α → α → Prop) :
+    (∀ a, ⇓Modal[ofPredicates r, a ⊨ P → □P]) ↔ Preserves r P := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    intro a₁ a₂ hr hPa₁
+    grind [h a₁]
+  case mpr =>
+    grind [Preserves]
+
+/-- Logical equivalence under `Model.ofPredicates r`. -/
+abbrev Proposition.Equiv.OfPredicates (r : α → α → Prop) := Proposition.Equiv (ofPredicates r)
+
+/-- Logical equivalence under `Model.ofContainers r`. -/
+abbrev Proposition.Equiv.OfContainers [Membership α β] (r : α → α → Prop) :=
+  Proposition.Equiv (ofContainers (β := β) r)
+
+/-- Logically equivalent propositions under `Equiv.OfPredicates r` have the same denotation in the
+Lean modal model induced by `ofPredicates r`. -/
+@[scoped grind ⇒]
+theorem Proposition.equivOfPredicates_denotation_eq {r : α → α → Prop}
+    {φ₁ φ₂ : Proposition (α → Prop)} :
+    (φ₁ ≡[Equiv.OfPredicates r] φ₂) ↔
+      φ₁.denotation (ofPredicates r) = φ₂.denotation (ofPredicates r) := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    apply denotation_eq_of_equiv h
+  case mpr =>
+    apply equiv_iff_denotation_eq.2
+    grind
+
+/-- Logically equivalent propositions under `Equiv.OfContainers r` have the same denotation in the
+Lean modal model induced by `ofContainers r`. -/
+@[scoped grind ⇒]
+theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r : α → α → Prop}
+    {φ₁ φ₂ : Proposition β} :
+    (φ₁ ≡[Equiv.OfContainers (β := β) r] φ₂) ↔
+      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    apply denotation_eq_of_equiv h
+  case mpr =>
+    apply equiv_iff_denotation_eq.2
+    grind
+
+/-- Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in
+the Lean modal model induced by `r`. -/
+theorem Proposition.equivOfPredicates_and {r : α → α → Prop} {P Q : α → Prop} :
+    (fun a => P a ∧ Q a) ≡[Equiv.OfPredicates r] (P ∧ Q) := by
+  simp only [← Proposition.equiv_def]
+  grind [Proposition.Equiv]
+
+/-- Under `Equiv.OfContainers r`, if membership in the infimum of two containers is equivalent to
+membership in both containers, then atomic infimum is logically equivalent to modal conjunction. -/
+theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α → α → Prop) (p q : β)
+    (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
+    (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by
+  intro
+  grind
+
+end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
new file mode 100644
index 000000000..5b1c6e07b
--- /dev/null
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Mathlib.Algebra.Group.Defs
+public import Mathlib.GroupTheory.GroupAction.SubMulAction
+public import Cslib.Foundations.Relation.Defs
+public import Cslib.Logics.Modal.LogicalEquivalence
+public import Cslib.Logics.Modal.Lean.Basic
+
+/-! # Modal Logic for scalar multiplication (SMul)
+
+Any scalar multiplication operation `•` induces an accessibility relation where two elements are
+related if the latter is the result of applying a scalar multiplication to the former.
+
+Properties of the operator translate to properties of the relation, for example a semigroup action
+on a commutative semigroup yields a relation with the `Diamond` property. This bridge allows for
+studying properties of the operation using modal logic.
+-/
+
+@[expose] public section
+
+namespace Relation
+
+/-- The accessibility relation induced by a scalar multiplication operation: `x` is related to `y`
+when there exists `m` such that `m • x = y`. -/
+def ofSMul (M α : Type*) [SMul M α] (x y : α) : Prop := ∃ m : M, m • x = y
+
+/-- The relation induced by a monoid action is reflexive. -/
+instance [Monoid M] [MulAction M α] : Std.Refl (ofSMul M α) where
+  refl x := by
+    use 1
+    simp
+
+/-- The relation induced by a semigroup action is transitive. -/
+instance [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α) where
+  trans x y z hxy hyz := by
+    rcases hxy with ⟨m, rfl⟩
+    rcases hyz with ⟨n, rfl⟩
+    use n * m
+    rw [mul_smul]
+
+/-- The relation induced by a semigroup action of a commutative semigroup has the diamond property.
+-/
+@[scoped grind .]
+theorem ofSMul_diamond [CommSemigroup M] [SemigroupAction M α] : Diamond (ofSMul M α) := by
+  intro x y z hxy hxz
+  rcases hxy with ⟨m, rfl⟩
+  rcases hxz with ⟨n, rfl⟩
+  refine ⟨n • (m • x), ?_, ?_⟩
+  · use n
+  · use m
+    grind only [=_ mul_smul]
+
+/-- Preservation by an action-induced relation is exactly closure under the action. -/
+@[scoped grind =]
+theorem ofSMul_preserves_iff [SMul M α] {P : α → Prop} :
+    Preserves (ofSMul M α) P ↔ ∀ m : M, ∀ x, P x → P (m • x) := by
+  apply Iff.intro
+  case mp =>
+    intro h m x hx
+    exact h ⟨m, rfl⟩ hx
+  case mpr =>
+    intro h x y hxy hx
+    rcases hxy with ⟨m, rfl⟩
+    exact h m x hx
+
+/-- Membership in a type closed under a scalar action is preserved by the relation induced by the
+action. -/
+@[scoped grind .]
+theorem ofSMul_preserves_mem [SMul M α] [SetLike S α] [SMulMemClass S M α]
+    (s : S) : Preserves (ofSMul M α) (· ∈ s) := by
+  rw [Relation.ofSMul_preserves_iff]
+  apply SMulMemClass.smul_mem
+
+end Relation
+
+namespace Cslib.Logic.Modal.Proposition
+
+/-- Characterisation of the denotation of a `◇p` under `ofSMul`. -/
+theorem ofSMul_diamond_denotation [SMul M α] [Membership α β] (p : β) :
+    (◇p : Proposition β).denotation (Model.ofContainers (Relation.ofSMul M α)) =
+      {x | ∃ m : M, m • x ∈ p} := by
+  ext x
+  change (∃ y, (∃ m : M, m • x = y) ∧ y ∈ p) ↔ ∃ m : M, m • x ∈ p
+  grind
+
+/-- For `SetLike` objects closed under a commutative semigroup action, simultaneous reachability is
+equivalent to separate reachability. -/
+theorem ofSMul_diamond_and_equiv [CommSemigroup M] [SemigroupAction M α] [SetLike S α]
+    [SMulMemClass S M α] (p q : S) :
+    ◇(p ∧ q : Proposition S) ≡[Equiv.OfContainers (Relation.ofSMul M α)] (◇p ∧ ◇q) :=
+  diamond_and_equiv_of_preserves Relation.ofSMul_diamond
+    (Relation.ofSMul_preserves_mem p)
+    (Relation.ofSMul_preserves_mem q)
+
+end Cslib.Logic.Modal.Proposition
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 092ff00e6..b0008858b 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -24,43 +24,89 @@ namespace Cslib.Logic.Modal
 
 open scoped InferenceSystem Proposition Satisfies
 
-/-- The modal propositions `φ₁` and `φ₂` are equivalent in the class of models `S`. -/
-def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    : Prop :=
-  ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]
+/-- The modal propositions `φ₁` and `φ₂` are equivalent in the model `m`. -/
+def Proposition.Equiv (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Prop :=
+  ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]
 
-instance : Congruence (Proposition.Equiv S) := ⟨⟩
+instance : Congruence (Proposition.Equiv m) := ⟨⟩
 
 @[scoped grind =]
-theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) :
-    φ₁.Equiv S φ₂ ↔ (φ₁ ≡[Equiv S] φ₂) := by rfl
+theorem Proposition.equiv_def (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) :
+    (φ₁.Equiv m φ₂) ↔ φ₁ ≡[Equiv m] φ₂ := by rfl
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_forall_der (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[Equiv S] φ₂) : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
+theorem Proposition.equiv_forall_der (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
+    (h : φ₁ ≡[Equiv m] φ₂) : ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
   intro s
   specialize h s
   assumption
 
-theorem Proposition.forall_der_equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[Equiv S] φ₂ := by
+theorem Proposition.forall_der_equiv (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
+    (h : ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[Equiv m] φ₂ := by
   intro s
   specialize h s
   assumption
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[Equiv S] φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) :
-    ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
+theorem Proposition.equiv_iff {m : Model World Atom} {φ₁ φ₂ : Proposition Atom}
+    (h : φ₁ ≡[Equiv m] φ₂) (w : World) : ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
   grind [=_ Satisfies.iff_iff_iff]
 
+/-- A class of models, defined as a set. -/
+abbrev ModelClass World Atom := Set (Model World Atom)
+
+/-- Every class of models induces an inference system tag for reasoning within that class. -/
+inductive Within (S : ModelClass World Atom)
+
+instance (S : ModelClass World Atom) : InferenceSystem (Within S) (Judgement World Atom) where
+  derivation j := j.m ∈ S → ⇓j
+
+@[scoped grind =_]
+theorem derivation_within_def {S : ModelClass World Atom} {m : Model World Atom} :
+    (m ∈ S → ⇓Modal[m, w ⊨ φ]) = Within S⇓Modal[m,w ⊨ φ] := rfl
+
+@[scoped grind .]
+theorem Satisfies.within_subset {S₁ S₂ : ModelClass World Atom} {m : Model World Atom}
+    (hs : S₂ ⊆ S₁) (h : Within S₁⇓Modal[m,w ⊨ φ]) : Within S₂⇓Modal[m, w ⊨ φ] := by grind
+
+@[scoped grind =]
+theorem Satisfies.within_univ {m : Model World Atom} :
+    Within (Set.univ (α := Model World Atom))⇓Modal[m,w ⊨ φ] = ⇓Modal[m, w ⊨ φ] := by grind
+
+/-- The modal propositions `φ₁` and `φ₂` are equivalent in the model class `S`. -/
+def Proposition.EquivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) :=
+  ∀ m ∈ S, φ₁ ≡[Equiv m] φ₂
+
+instance : Congruence (Proposition.EquivWithin S) := ⟨⟩
+
+@[scoped grind =]
+theorem Proposition.equivWithin_def (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) :
+    φ₁.EquivWithin S φ₂ ↔ (φ₁ ≡[EquivWithin S] φ₂) := by rfl
+
+@[scoped grind ⇒]
+theorem Proposition.equiv_of_EquivWithin {S : ModelClass World Atom} (h : φ₁ ≡[EquivWithin S] φ₂)
+    (m : Model World Atom) (hm : m ∈ S) : φ₁ ≡[Equiv m] φ₂ := h m hm
+
+theorem Proposition.equivWithin_forall_der (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
+    (h : φ₁ ≡[EquivWithin S] φ₂) : ∀ m ∈ S, ∀ (w : World), Within S⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
+  intro m
+  grind [h m]
+
+theorem Proposition.forall_der_equivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
+    (h : ∀ m ∈ S, ∀ (w : World), Within S⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[EquivWithin S] φ₂ := by
+  intro m hm w
+  grind [h m hm]
+
+theorem Proposition.equivWithin_iff (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
+    (h : φ₁ ≡[EquivWithin S] φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) :
+    Within S⇓Modal[m,w ⊨ φ₁] ↔ Within S⇓Modal[m,w ⊨ φ₂] := by
+  grind [h _ hm w]
+
 /-- Logical equivalence preserves validity. -/
-theorem Proposition.equiv_valid (S : Set (Model World Atom))
-    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[Equiv S] φ₂) :
+theorem Proposition.equivWithin_valid (S : ModelClass World Atom)
+    (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[EquivWithin S] φ₂) :
     (φ₁.valid S ↔ φ₂.valid S) := by
-  apply Proposition.equiv_forall_der at h
-  simp only [Satisfies.iff_iff_iff] at h
-  grind
+  apply Iff.intro <;> intro h' m hm w <;> grind [h m hm w]
 
 /-- Propositional contexts. -/
 inductive Proposition.Context (Atom : Type u) : Type u where
@@ -89,17 +135,38 @@ lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} :
 open scoped Proposition Proposition.Context
 
 /-- Logical equivalence is an equivalence relation. -/
-instance {World Atom} (S : Set (Model World Atom)) :
-    IsEquiv (Proposition Atom) (Proposition.Equiv S) := by
+instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv m) := by
+  rw [← equivalence_iff_isEquiv]
+  constructor
+  case refl => grind [Proposition.Equiv]
+  case symm =>
+    intro φ₁ φ₂ h w
+    grind
+  case trans =>
+    intro φ₁ φ₂ φ₃ h₁ h₂ w
+    grind
+
+/-- Logical equivalence within a class is an equivalence relation. -/
+instance {World Atom} (S : ModelClass World Atom) :
+    IsEquiv (Proposition Atom) (Proposition.EquivWithin S) := by
   rw [← equivalence_iff_isEquiv]
-  grind [Equivalence, Proposition.Equiv]
+  unfold Proposition.EquivWithin
+  constructor
+  case refl =>
+    intro φ m hm w
+    grind [Proposition.Equiv]
+  case symm =>
+    intro φ₁ φ₂ h m hm w
+    grind [h m hm w]
+  case trans =>
+    intro φ₁ φ₂ φ₃ h₁ h₂ m hm w
+    grind [h₁ m hm w, h₂ m hm w]
 
 /-- Logical equivalence is a congruence. -/
-instance {World Atom} (S : Set (Model World Atom)) :
-    LawfulCongruence (Proposition.Equiv S) where
-  elim ctx φ₁ φ₂ heqv m hₘ w := by
+instance (m : Model World Atom) : LawfulCongruence (Proposition.Equiv m) where
+  elim ctx φ₁ φ₂ heqv w := by
     induction ctx generalizing w
-    case hole => grind [=_ Proposition.Context.fill_def]
+    case hole => apply heqv
     case not c ih | andL c ih | andR c ih =>
       specialize ih w
       grind [=_ Proposition.Context.fill_def]
@@ -111,6 +178,12 @@ instance {World Atom} (S : Set (Model World Atom)) :
         specialize ih w'
         grind [=_ Proposition.Context.fill_def]
 
+/-- Logical equivalence within a class is a congruence. -/
+instance (S : ModelClass World Atom) :
+    LawfulCongruence (Proposition.EquivWithin S) where
+  elim ctx _ _ h m hm :=
+    LawfulCongruence.covariant.elim ctx (h m hm)
+
 /-- Judgemental contexts. -/
 structure Satisfies.Context (World Atom : Type*) where
   /-- The model to consider. -/
@@ -122,8 +195,7 @@ structure Satisfies.Context (World Atom : Type*) where
 def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) :
     Judgement World Atom := Modal[c.m, c.w ⊨ φ]
 
-instance : HasHContext (Judgement World Atom) (Proposition Atom) :=
-  ⟨Satisfies.Context.fill⟩
+instance : HasHContext (Judgement World Atom) (Proposition Atom) := ⟨Satisfies.Context.fill⟩
 
 @[scoped grind =]
 lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
@@ -131,13 +203,65 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
 
 open scoped Satisfies.Context
 
+/-- Logical equivalence for Modal Logic within a class of models `S`. -/
+instance (S : ModelClass World Atom) : LogicalEquivalence
+    (α := Proposition Atom)
+    (Judgement := Judgement World Atom) (Within S)
+    (Proposition.EquivWithin S) where
+  eqvFillValid heqv c h := by
+    specialize heqv c.m
+    grind [=_ Satisfies.Context.fill_def]
+
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
 instance : LogicalEquivalence
     (α := Proposition Atom)
     (Judgement := Judgement World Atom) InferenceSystem.Default
-    (Proposition.Equiv (Set.univ (α := Model World Atom))) where
+    (Proposition.EquivWithin (Set.univ (α := Model World Atom))) where
   eqvFillValid heqv c h := by
     specialize heqv c.m
     grind [=_ Satisfies.Context.fill_def]
 
+/-- Correspondence of equivalence and axiom validity. -/
+theorem Proposition.isAxiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) :
+    (IsAxiom r (φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := by
+  apply Iff.intro <;> intro h
+  case mp =>
+    intro v w
+    exact h v w
+  case mpr =>
+    intro v w
+    exact h v w
+
+open Relation in
+/-- In a transitive diamond model, possibility distributes over conjunction for propositions
+whose satisfaction is preserved along accessibility. -/
+@[scoped grind ⇒]
+theorem Proposition.diamond_and_equiv_of_preserves {m : Model World Atom} [IsTrans World m.r]
+    {φ₁ φ₂ : Proposition Atom} (hd : Diamond m.r) (h₁ : Preserves m.r (⇓Modal[m,· ⊨ φ₁]))
+    (h₂ : Preserves m.r (⇓Modal[m,· ⊨ φ₂])) :
+    ◇(φ₁ ∧ φ₂) ≡[Equiv m] (◇φ₁ ∧ ◇φ₂) := by
+  intro a
+  rw [Satisfies.iff_iff_iff]
+  apply Iff.intro
+  case mp => grind
+  case mpr =>
+    intro h
+    rw [Satisfies.and_iff_and] at h
+    rcases h with ⟨hφ₁, hφ₂⟩
+    rw [Satisfies.diamond_iff_exists] at hφ₁ hφ₂ ⊢
+    rcases hφ₁ with ⟨b, hab, hb⟩
+    rcases hφ₂ with ⟨c, hac, hc⟩
+    rcases hd hab hac with ⟨d, hbd, hcd⟩
+    use d, IsTrans.trans _ _ _ hab hbd
+    exact ⟨h₁ hbd hb, h₂ hcd hc⟩
+
+/-- In a reflexive and transitive model, diamond absorbs itself (idempotency). -/
+theorem Proposition.diamond_diamond_equiv {m : Model World Atom} [Std.Refl m.r] [IsTrans World m.r]
+    (φ : Proposition Atom) : ◇◇φ ≡[Equiv m] ◇φ := by
+  intro w
+  rw [Satisfies.iff_iff_iff]
+  apply Iff.intro <;> rw [← Satisfies.imp_iff_imp]
+  · grind [Satisfies.four]
+  · grind [Satisfies.t]
+
 end Cslib.Logic.Modal
diff --git a/CslibTests.lean b/CslibTests.lean
index 99f1d31f5..d5103dbcb 100644
--- a/CslibTests.lean
+++ b/CslibTests.lean
@@ -15,5 +15,6 @@ import CslibTests.LTS
 import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Modal
+import CslibTests.Modal.Ideal
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses
diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
new file mode 100644
index 000000000..be8782caf
--- /dev/null
+++ b/CslibTests/Modal/Ideal.lean
@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Logics.Modal.Denotation
+import Cslib.Logics.Modal.Lean.Basic
+import Cslib.Logics.Modal.Lean.SMul
+import Cslib.Foundations.Relation.Defs
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Algebra.Ring.Defs
+import Mathlib.RingTheory.Ideal.Defs
+import Mathlib.RingTheory.Ideal.Operations
+
+/-! # Example: radicals of ideals with modal logic
+
+We leverage the accessibility relation induced by scalar multiplication to exemplify how laws of
+radicals of ideals can be derived from modal logic laws.
+-/
+
+namespace CslibTests
+
+open Cslib Logic Modal Proposition Model Relation
+
+/-! ## Relational view of radicals of ideals
+
+We interpret positive exponentiation as an action and hence as an accessibility relation.
+Ideals are invariant under this action, while radical membership corresponds to reachability.
+-/
+
+/-- Positive naturals act on a monoid by exponentiation. -/
+@[instance_reducible]
+def posPowAction [Monoid α] : MulAction ℕ+ α where
+  smul n x := x ^ (n : ℕ)
+  one_smul x := pow_one x
+  mul_smul m n x := by
+    dsimp [HSMul.hSMul]
+    grind [pow_mul, mul_comm]
+
+local instance [Monoid α] : MulAction ℕ+ α := posPowAction
+
+/-- Ideals are invariant under positive exponentiation. -/
+theorem Ideal.posPowSMulMemClass [Semiring R] : SMulMemClass (Ideal R) ℕ+ R where
+  smul_mem n x hx := by
+    change _ ^ (n : ℕ) ∈ _
+    exact Ideal.pow_mem_of_mem _ hx n n.prop
+
+local instance [Semiring R] : SMulMemClass (Ideal R) ℕ+ R := Ideal.posPowSMulMemClass
+
+/-- Accessibility by positive natural exponentiation. -/
+abbrev PosPow α [Monoid α] := Relation.ofSMul ℕ+ α
+
+/-- The modal model of ideals under positive-power accessibility. -/
+abbrev idealPowerModel [Semiring R] : Model R (Ideal R) := Model.ofContainers (PosPow R)
+
+/-- Logical equivalence under `idealPowerModel`. -/
+abbrev IdealEquiv [Semiring R] := Proposition.Equiv (idealPowerModel (R := R))
+
+/-- An ideal atom denotes its underlying set in `idealPowerModel`. -/
+example [Semiring R] (I : Ideal R) : (I : Set R) = Proposition.denotation idealPowerModel I := rfl
+
+/-- Characterisation of radicals as modal denotations. This is the key bridge that enables reasoning
+about membership of radicals with modal logic. -/
+@[local grind =]
+theorem Ideal.radical_eq_modal_denotation [CommSemiring R] (I : Ideal R) :
+    (I.radical : Set R) = Proposition.denotation idealPowerModel (◇I) := by
+  rw [Proposition.ofSMul_diamond_denotation]
+  ext x
+  apply Iff.intro
+  · rintro ⟨n, hn⟩
+    refine ⟨⟨n + 1, Nat.succ_pos _⟩, ?_⟩
+    exact I.pow_mem_of_pow_mem hn (Nat.le_succ n)
+  · rintro ⟨n, hn⟩
+    exact ⟨(n : ℕ), hn⟩
+
+/-- In `idealPowerModel`, the radical of an ideal is logically equivalent to possibility. -/
+theorem Ideal.radical_equiv_diamond [CommSemiring R] (I : Ideal R) :
+    (I.radical : Proposition (Ideal R)) ≡[IdealEquiv] ◇I :=
+  Proposition.equiv_iff_denotation_eq.mpr (Ideal.radical_eq_modal_denotation I)
+
+open scoped Satisfies
+
+/-- Radical is idempotent, as a consequence of modal idempotence of `◇`. -/
+theorem Ideal.radical_idem [CommSemiring R] (I : Ideal R) : I.radical.radical = I.radical := by
+  apply SetLike.ext'
+  simp only [Ideal.radical_eq_modal_denotation]
+  apply Proposition.denotation_eq_of_equiv
+  calc
+    (◇(I.radical : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] ◇◇I := by
+      let pc : HasContext.Context (Proposition (Ideal R)) := Context.diamond .hole
+      apply LawfulCongruence.covariant.elim pc (Ideal.radical_equiv_diamond I)
+    _ ≡[IdealEquiv] ◇I := by apply Proposition.diamond_diamond_equiv
+
+/-- In `idealPowerModel`, possibility of membership in an infimum is equivalent to simultaneous
+possibility of membership in both ideals. -/
+theorem Ideal.inf_modelEquiv [Semiring R] (I J : Ideal R) :
+    (◇(I ⊓ J : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] (◇I ∧ ◇J) := by
+  calc
+    (◇(I ⊓ J : Ideal R) : Proposition (Ideal R)) ≡[IdealEquiv] ◇(I ∧ J) := by
+      let pc : HasContext.Context (Proposition (Ideal R)) := Context.diamond .hole
+      exact LawfulCongruence.covariant.elim pc
+        (Proposition.ofContainers_inf_equiv (PosPow R) I J (by simp))
+    _ ≡[IdealEquiv] (◇I ∧ ◇J) := Proposition.ofSMul_diamond_and_equiv I J
+
+/-- Radicals of ideals distribute over intersection, as a consequence that `◇(I ⊓ J)` is logically
+equivalent to `◇I ∧ ◇J`. -/
+theorem Ideal.radical_inf [CommSemiring R] (I J : Ideal R) :
+    (I ⊓ J).radical = I.radical ⊓ J.radical := by
+  apply SetLike.ext'
+  rw [Submodule.coe_inf]
+  simp only [Ideal.radical_eq_modal_denotation]
+  rw [Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]
+  rfl
+
+end CslibTests

From 34074f300d2229753dc4f54e293ad6c6aebca053 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:07:47 +0200
Subject: [PATCH 03/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 6e79b160a..a68a7ab63 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -83,13 +83,8 @@ Lean modal model induced by `ofPredicates r`. -/
 theorem Proposition.equivOfPredicates_denotation_eq {r : α → α → Prop}
     {φ₁ φ₂ : Proposition (α → Prop)} :
     (φ₁ ≡[Equiv.OfPredicates r] φ₂) ↔
-      φ₁.denotation (ofPredicates r) = φ₂.denotation (ofPredicates r) := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    apply denotation_eq_of_equiv h
-  case mpr =>
-    apply equiv_iff_denotation_eq.2
-    grind
+      φ₁.denotation (ofPredicates r) = φ₂.denotation (ofPredicates r) :=
+  equiv_iff_denotation_eq  
 
 /-- Logically equivalent propositions under `Equiv.OfContainers r` have the same denotation in the
 Lean modal model induced by `ofContainers r`. -/

From 67a5cec2aba08a79113ec38af9cd01fad34db391 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:07:58 +0200
Subject: [PATCH 04/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index a68a7ab63..ad056920d 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -92,13 +92,8 @@ Lean modal model induced by `ofContainers r`. -/
 theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r : α → α → Prop}
     {φ₁ φ₂ : Proposition β} :
     (φ₁ ≡[Equiv.OfContainers (β := β) r] φ₂) ↔
-      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    apply denotation_eq_of_equiv h
-  case mpr =>
-    apply equiv_iff_denotation_eq.2
-    grind
+      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) := 
+  equiv_iff_denotation_eq
 
 /-- Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in
 the Lean modal model induced by `r`. -/

From b77de1017474f154eb22358da602598ae8664e01 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:08:19 +0200
Subject: [PATCH 05/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 23 +++++++++--------------
 1 file changed, 9 insertions(+), 14 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 62aa37941..95134414b 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -327,21 +327,16 @@ theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
     (hwf : WellFounded (flip r)) (φ : Proposition Atom) : IsAxiom r <| □(□φ → φ) → □φ := by
   intro v w
   let m := Model.mk r v
-  rw [Satisfies.imp_iff_imp]
+  simp_rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall]
   intro h
-  rw [Satisfies.box_iff_forall] at h ⊢
-  intro w' hw'
-  have h' : ∀ w', r w w' → ⇓Modal[m, w' ⊨ φ] := by
-    intro w'
-    refine (WellFounded.induction (C := fun w' => m.r w w' → ⇓Modal[m,w' ⊨ φ]) hwf w' ?_)
-    intro w' ih hww'
-    have hImp : ⇓Modal[m, w' ⊨ □φ → φ] := h _ hww'
-    rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall] at hImp
-    apply hImp
-    intro w'' hw'w''
-    apply ih _ hw'w''
-    exact IsTrans.trans _ _ _ hww' hw'w''
-  exact h' w' hw'
+  refine (hwf.induction (C := fun w' => m.r w w' → ⇓Modal[m,w' ⊨ φ]) · ?_)
+  intro w' ih hww'
+  have hImp : ⇓Modal[m, w' ⊨ □φ → φ] := h _ hww'
+  rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall] at hImp
+  apply hImp
+  intro w'' hw'w''
+  apply ih _ hw'w''
+  exact IsTrans.trans _ _ _ hww' hw'w''
 
 open Relation in
 /-- Axiom .2, valid for all frames with the diamond property. -/

From 5c4207f4b7de2b55fe499b95ce76d587457da9e9 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:08:33 +0200
Subject: [PATCH 06/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 95134414b..4432862f5 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -342,13 +342,8 @@ open Relation in
 /-- Axiom .2, valid for all frames with the diamond property. -/
 theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
     (φ : Proposition Atom) : IsAxiom r <| ◇□φ → □◇φ := by
-  intro v w
-  rw [Satisfies.imp_iff_imp]
-  intro h₁
-  rw [Satisfies.diamond_iff_exists] at h₁
-  rcases h₁ with ⟨_, hww₁, _⟩
-  rw [Satisfies.box_iff_forall]
-  intro _ hww₂
+  simp_rw [IsAxiom, Satisfies.imp_iff_imp, Satisfies.diamond_iff_exists, Satisfies.box_iff_forall]
+  rintro v w ⟨_, hww₁, _⟩ _ hww₂
   obtain ⟨w₃, hww₃⟩ := h hww₁ hww₂
   grind
 

From 315358a1d9413efdbd19b5c151103147b304a5d1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:08:41 +0200
Subject: [PATCH 07/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 4432862f5..407c207f7 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -352,9 +352,7 @@ open Relation in
 theorem Satisfies.pointTwo_diamond (r : World → World → Prop) [Nonempty Atom]
     (h : ∀ φ : Proposition Atom, IsAxiom r <| ◇□φ → □◇φ) : Diamond r := by
   intro w w₁ w₂ hww₁ hww₂
-  have a := Classical.arbitrary Atom
-  let v := fun (w' : World) (a : Atom) => r w₁ w'
-  have h' := h a v w
+  specialize h (Classical.arbitrary Atom) (fun w' _ => r w₁ w') w
   grind [Join]
 
 /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under

From a86d6386bdcd5bb1b2cb3f7e3093402d1277679c Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:08:51 +0200
Subject: [PATCH 08/42] Update Cslib/Logics/Modal/Denotation.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Denotation.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 7f64b6f91..26b1b9658 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -52,7 +52,7 @@ theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} :
 /-- Logically equivalent propositions under a model have the same denotation. -/
 theorem Proposition.equiv_iff_denotation_eq :
     (φ₁ ≡[Equiv m] φ₂) ↔ φ₁.denotation m = φ₂.denotation m := by
-  apply Iff.intro <;> intro h
+  constructor <;> intro h
   case mp =>
     ext w
     grind [h w]

From af3e9ba24fa6d822e068cb66cd26e97aa181f009 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Fri, 14 Aug 2026 18:09:34 +0200
Subject: [PATCH 09/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 407c207f7..4868781c8 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -378,7 +378,7 @@ abbrev modelsOfRelation (r : World → World → Prop) : Set (Model World Atom)
 that frame. -/
 theorem isAxiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
     IsAxiom r φ ↔ φ ∈ logic (modelsOfRelation r) := by
-  apply Iff.intro
+  constructor
   case mp =>
     intro h m hm w
     subst hm

From f260ad26719889c13ec88858e0d6b2f0ece07f9a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Fri, 14 Aug 2026 18:33:48 +0200
Subject: [PATCH 10/42] fix whitespacing

---
 Cslib/Logics/Modal/Lean/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index ad056920d..535a3b5c9 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -84,7 +84,7 @@ theorem Proposition.equivOfPredicates_denotation_eq {r : α → α → Prop}
     {φ₁ φ₂ : Proposition (α → Prop)} :
     (φ₁ ≡[Equiv.OfPredicates r] φ₂) ↔
       φ₁.denotation (ofPredicates r) = φ₂.denotation (ofPredicates r) :=
-  equiv_iff_denotation_eq  
+  equiv_iff_denotation_eq
 
 /-- Logically equivalent propositions under `Equiv.OfContainers r` have the same denotation in the
 Lean modal model induced by `ofContainers r`. -/
@@ -92,7 +92,7 @@ Lean modal model induced by `ofContainers r`. -/
 theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r : α → α → Prop}
     {φ₁ φ₂ : Proposition β} :
     (φ₁ ≡[Equiv.OfContainers (β := β) r] φ₂) ↔
-      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) := 
+      φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) :=
   equiv_iff_denotation_eq
 
 /-- Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in

From 542f6e2aebfed07c5f92bcaf98e8fb5929d8decf Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Fri, 14 Aug 2026 19:26:32 +0200
Subject: [PATCH 11/42] Axiom derivation system

---
 Cslib/Logics/HML/Basic.lean                |  6 --
 Cslib/Logics/Modal/Basic.lean              | 74 ++++++++++++----------
 Cslib/Logics/Modal/Denotation.lean         |  2 +-
 Cslib/Logics/Modal/Lean/Basic.lean         |  4 +-
 Cslib/Logics/Modal/LogicalEquivalence.lean |  4 +-
 5 files changed, 47 insertions(+), 43 deletions(-)

diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean
index 1bba83dd3..00c8f74e3 100644
--- a/Cslib/Logics/HML/Basic.lean
+++ b/Cslib/Logics/HML/Basic.lean
@@ -259,12 +259,6 @@ theorem mem_denotation_iff_satisfies {φ : Proposition Label} :
 theorem mem_theory_iff_satisfies : φ ∈ theory lts s ↔ ⇓HML[lts,s ⊨ φ] := by
   grind
 
-/- A state satisfies a proposition iff it does not satisfy the negation of the proposition. -/
--- @[simp, scoped grind =]
--- theorem Satisfies.not_not_iff {lts : LTS State Label} :
---   ¬⇓HML[lts,s ⊨ ¬φ] ↔ ⇓HML[lts,s ⊨ φ] := by
---   grind
-
 open scoped Satisfies
 
 /-- A state is in the denotation of a proposition iff it is not in the denotation of the negation
diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 4868781c8..7712cc995 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -126,7 +126,7 @@ instance : HasInferenceSystem (Judgement World Atom) := ⟨Satisfies.Bundled⟩
 
 open scoped InferenceSystem Proposition
 
-@[scoped grind =_]
+@[scoped grind =]
 theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} :
   Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl
 
@@ -169,7 +169,7 @@ This result proves that the definition is correct. -/
 theorem Satisfies.iff_iff_iff {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
   simp only [HasIff.iff, Proposition.iff]
-  grind [= derivation_def]
+  grind
 
 /-- Characterisation of the `□` modality.
 
@@ -193,7 +193,7 @@ theorem TheoryEq.ext_iff : TheoryEq m w₁ w₂ ↔ (∀ φ, φ ∈ theory m w
 
 /-- Any proposition satisfied by a world is in the theory of that world. -/
 @[scoped grind →]
-theorem satisfies_theory (h : Satisfies m w φ) : φ ∈ theory m w := by grind
+theorem satisfies_theory (h : ⇓Modal[m,w ⊨ φ]) : φ ∈ theory m w := by grind
 
 /-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/
 lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) :
@@ -206,22 +206,31 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
   apply TheoryEq.ext_iff.1 at h
   exact (h φ).mp hs
 
+/-- Every accessibility relation induces an inference system tag for proving valid axioms under
+the relation. -/
+inductive Axiom (r : World → World → Prop)
+
 /-- A proposition `φ` is an axiom under the relation `r` (the 'frame') if it holds for all
 valuations and worlds. -/
-abbrev IsAxiom (r : World → World → Prop) (φ : Proposition Atom) := ∀ v w, ⇓Modal[⟨r, v⟩,w ⊨ φ]
+instance (r : World → World → Prop) : InferenceSystem (Axiom r) (Proposition Atom) where
+  derivation φ := ∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]
+
+@[scoped grind ⇒]
+theorem Satisfies.axiom_def (r : World → World → Prop) :
+    (∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]) ↔ Axiom r⇓φ := by rfl
 
 /-- If a proposition is an axiom under the relation of a model, it is satisfied by every world. -/
 @[scoped grind .]
-theorem Satisfies.of_isAxiom (m : Model World Atom) (φ : Proposition Atom) (h : IsAxiom m.r φ)
+theorem Satisfies.of_axiom (m : Model World Atom) (φ : Proposition Atom) (h : Axiom m.r⇓φ)
     (w : World) : ⇓Modal[m,w ⊨ φ] := h m.v w
 
 /-- The K axiom, valid for all models. -/
 theorem Satisfies.k (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
-    IsAxiom r <| □(φ₁ → φ₂) → (□φ₁ → □φ₂) := by grind
+    Axiom r⇓(□(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind
 
 /-- The dual axiom, valid for all models. -/
 theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
-    IsAxiom r <| ◇φ ↔ ¬□¬φ := by
+    Axiom r⇓(◇φ ↔ ¬□¬φ) := by
   intro _ w
   simp only [Satisfies.iff_iff_iff]
   constructor
@@ -230,25 +239,25 @@ theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
 
 /-- Possibility preserves conjunction in all models. -/
 theorem Satisfies.diamond_and (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
-    IsAxiom r <| ◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂) := by grind
+    Axiom r⇓(◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂)) := by grind
 
 /-- Possibility can be combined with necessity. -/
 theorem Satisfies.diamond_and_box (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
-    IsAxiom r <| (◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂) := by grind
+    Axiom r⇓((◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂)) := by grind
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t (r : World → World → Prop) [instRefl : Std.Refl r] (φ : Proposition Atom)
-    : IsAxiom r <| φ → ◇φ := by
+    : Axiom r⇓(φ → ◇φ) := by
   grind [instRefl.refl]
 
 /-- Any model that admits the axiom T is reflexive. -/
 theorem Satisfies.t_refl (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ φ : Proposition Atom, IsAxiom r <| φ → ◇φ) : Std.Refl r where
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(φ → ◇φ)) : Std.Refl r where
   refl w := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w
     let h' := h (v := v) (w := w) (φ := a)
-    grind
+    grind [=_ derivation_def]
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/
 theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by
@@ -257,24 +266,24 @@ theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ]
 
 /-- The B axiom, valid for all symmetric models. -/
 theorem Satisfies.b (r : World → World → Prop) [Std.Symm r] (φ : Proposition Atom) :
-    IsAxiom r <| φ → □◇φ := by
+    Axiom r⇓(φ → □◇φ) := by
   intro _ w
   have := Std.Symm.symm (r := r) w
-  grind
+  grind [=_ derivation_def]
 
 /-- Any model that admits the axiom B is symmetric. -/
 theorem Satisfies.b_symm (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ φ : Proposition Atom, IsAxiom r <| φ → □◇φ) : Std.Symm r where
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(φ → □◇φ)) : Std.Symm r where
   symm w₁ := by
     have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
     let h₁ := h (v := v₁) (w := w₁) (φ := a)
     simp [imp_iff_imp] at h₁
-    grind
+    grind [=_ derivation_def]
 
 /-- The 4 axiom, valid for all transitive models. -/
 theorem Satisfies.four (r : World → World → Prop) [IsTrans World r]
-    (φ : Proposition Atom) : IsAxiom r <| ◇◇φ → ◇φ := by
+    (φ : Proposition Atom) : Axiom r⇓(◇◇φ → ◇φ) := by
   intro _ _
   simp only [imp_iff_imp]
   intro h
@@ -283,39 +292,39 @@ theorem Satisfies.four (r : World → World → Prop) [IsTrans World r]
 
 /-- Any model that admits 4 is transitive. -/
 theorem Satisfies.four_trans (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ (φ : Proposition Atom), IsAxiom r <| ◇◇φ → ◇φ) : IsTrans World r where
+    (h : ∀ (φ : Proposition Atom), Axiom r⇓(◇◇φ → ◇φ)) : IsTrans World r where
   trans w₁ w₂ w₃ h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := a)
-    grind
+    grind [=_ derivation_def]
 
 /-- The 5 axiom, valid for all Euclidean models. -/
 theorem Satisfies.five (r : World → World → Prop) [Relation.RightEuclidean r]
-    (φ : Proposition Atom) : IsAxiom r <| ◇φ → □◇φ := by
+    (φ : Proposition Atom) : Axiom r⇓(◇φ → □◇φ) := by
   have := @Relation.RightEuclidean.rightEuclidean (r := r)
   grind
 
 /-- Any model that admits 5 is Euclidean. -/
 theorem Satisfies.five_rightEuclidean (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ φ : Proposition Atom, IsAxiom r <| ◇φ → □◇φ) :
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(◇φ → □◇φ)) :
     Relation.RightEuclidean r where
   rightEuclidean {w₁ w₂ w₃} h₁ h₂ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := a)
-    grind
+    grind [=_ derivation_def]
 
 /-- The D axiom, valid for all serial models. -/
 theorem Satisfies.d (r : World → World → Prop) [Relation.Serial r] (φ : Proposition Atom) :
-    IsAxiom r <| □φ → ◇φ := by
+    Axiom r⇓(□φ → ◇φ) := by
   intro _ w
   have : ∃ w', r w w' := Relation.Serial.serial w
   grind
 
 /-- Any model that admits D is serial. -/
 theorem Satisfies.d_serial (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ φ : Proposition Atom, IsAxiom r <| □φ → ◇φ) : Relation.Serial r where
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(□φ → ◇φ)) : Relation.Serial r where
   serial w₁ := by
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₁
@@ -324,7 +333,7 @@ theorem Satisfies.d_serial (r : World → World → Prop) [Nonempty Atom]
 
 /-- The L axiom, or Löb's theorem, valid for all transitive and converse well-founded models. -/
 theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
-    (hwf : WellFounded (flip r)) (φ : Proposition Atom) : IsAxiom r <| □(□φ → φ) → □φ := by
+    (hwf : WellFounded (flip r)) (φ : Proposition Atom) : Axiom r⇓(□(□φ → φ) → □φ) := by
   intro v w
   let m := Model.mk r v
   simp_rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall]
@@ -341,8 +350,9 @@ theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
 open Relation in
 /-- Axiom .2, valid for all frames with the diamond property. -/
 theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
-    (φ : Proposition Atom) : IsAxiom r <| ◇□φ → □◇φ := by
-  simp_rw [IsAxiom, Satisfies.imp_iff_imp, Satisfies.diamond_iff_exists, Satisfies.box_iff_forall]
+    (φ : Proposition Atom) : Axiom r⇓(◇□φ → □◇φ) := by
+  simp_rw [← Satisfies.axiom_def, Satisfies.imp_iff_imp, Satisfies.diamond_iff_exists,
+    Satisfies.box_iff_forall]
   rintro v w ⟨_, hww₁, _⟩ _ hww₂
   obtain ⟨w₃, hww₃⟩ := h hww₁ hww₂
   grind
@@ -350,10 +360,10 @@ theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
 open Relation in
 /-- Any model that admits axiom .2 has the diamond property. -/
 theorem Satisfies.pointTwo_diamond (r : World → World → Prop) [Nonempty Atom]
-    (h : ∀ φ : Proposition Atom, IsAxiom r <| ◇□φ → □◇φ) : Diamond r := by
+    (h : ∀ φ : Proposition Atom, Axiom r⇓(◇□φ → □◇φ)) : Diamond r := by
   intro w w₁ w₂ hww₁ hww₂
   specialize h (Classical.arbitrary Atom) (fun w' _ => r w₁ w') w
-  grind [Join]
+  grind [Join, =_ derivation_def]
 
 /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under
 all models in `S` for all worlds. -/
@@ -376,13 +386,13 @@ abbrev modelsOfRelation (r : World → World → Prop) : Set (Model World Atom)
 
 /-- A proposition is an axiom of a frame exactly when it belongs to the logic of all models over
 that frame. -/
-theorem isAxiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
-    IsAxiom r φ ↔ φ ∈ logic (modelsOfRelation r) := by
+theorem axiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
+    Axiom r⇓φ ↔ φ ∈ logic (modelsOfRelation r) := by
   constructor
   case mp =>
     intro h m hm w
     subst hm
     exact h m.v w
-  case mpr => grind
+  case mpr => grind [Satisfies.axiom_def]
 
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 26b1b9658..9def7b078 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -34,7 +34,7 @@ def Proposition.denotation (m : Model World Atom) :
 @[scoped grind =]
 theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} :
     w ∈ φ.denotation m ↔ ⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind
+  induction φ generalizing w <;> grind [=_ derivation_def]
 
 /-- A world is in the denotation of a proposition iff it is not in the denotation of the negation
 of the proposition. -/
diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 535a3b5c9..9e4311bed 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -57,7 +57,7 @@ open scoped InferenceSystem Satisfies
 /-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
 @[scoped grind =]
 theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
-    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind
+    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind [=_ derivation_def]
 
 /-- Under `Model.ofPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/
 @[scoped grind ⇒]
@@ -108,6 +108,6 @@ theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α 
     (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
     (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by
   intro
-  grind
+  grind [=_ derivation_def]
 
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index b0008858b..a9252163a 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -222,8 +222,8 @@ instance : LogicalEquivalence
     grind [=_ Satisfies.Context.fill_def]
 
 /-- Correspondence of equivalence and axiom validity. -/
-theorem Proposition.isAxiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) :
-    (IsAxiom r (φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := by
+theorem Proposition.axiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) :
+    (Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := by
   apply Iff.intro <;> intro h
   case mp =>
     intro v w

From 9ae560791b8648fd943ea1dbe7152d18cb43687a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:18:31 +0200
Subject: [PATCH 12/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 5b1c6e07b..956c7d2d5 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -43,6 +43,16 @@ instance [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α) where
     rcases hyz with ⟨n, rfl⟩
     use n * m
     rw [mul_smul]
+/-- The relation induced by a group action is symmetric. -/
+instance [Group G] [MulAction G α] : Std.Symm (ofSMul G α) where
+  symm := by
+    rintro x _ ⟨g, rfl⟩
+    use g⁻¹
+    simp
+
+/-- The relation induced by an action of a nonempty type is serial. -/
+instance [SMul M α] [Nonempty M] : Serial (ofSMul M α) where
+  serial x := ⟨Classical.arbitrary M • x, Classical.arbitrary M, rfl⟩
 
 /-- The relation induced by a semigroup action of a commutative semigroup has the diamond property.
 -/

From 387b5f1bc982643126c2312935dc766b3fb2505c Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:19:02 +0200
Subject: [PATCH 13/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 956c7d2d5..bd96ec255 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -54,17 +54,16 @@ instance [Group G] [MulAction G α] : Std.Symm (ofSMul G α) where
 instance [SMul M α] [Nonempty M] : Serial (ofSMul M α) where
   serial x := ⟨Classical.arbitrary M • x, Classical.arbitrary M, rfl⟩
 
-/-- The relation induced by a semigroup action of a commutative semigroup has the diamond property.
--/
+/-- TODO: upstream this generalisation of Mathlib's `smulCommClass_self`, which applies only to
+monoids `M`. -/
+instance {M α} [CommSemigroup M] [SemigroupAction M α] : SMulCommClass M M α where
+  smul_comm m n a := by rw [←mul_smul, mul_comm, mul_smul]
+
+/-- The relation induced by an action commuting with itself has the diamond property. -/
 @[scoped grind .]
-theorem ofSMul_diamond [CommSemigroup M] [SemigroupAction M α] : Diamond (ofSMul M α) := by
-  intro x y z hxy hxz
-  rcases hxy with ⟨m, rfl⟩
-  rcases hxz with ⟨n, rfl⟩
-  refine ⟨n • (m • x), ?_, ?_⟩
-  · use n
-  · use m
-    grind only [=_ mul_smul]
+theorem ofSMul_diamond [SMul M α] [SMulCommClass M M α] : Diamond (ofSMul M α) := by
+  rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
+  use! n • m • x, n, m, smul_comm ..
 
 /-- Preservation by an action-induced relation is exactly closure under the action. -/
 @[scoped grind =]

From 62c81e565da64e365f19a7b0e865f81552009285 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:19:20 +0200
Subject: [PATCH 14/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index bd96ec255..221c2430e 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -69,7 +69,7 @@ theorem ofSMul_diamond [SMul M α] [SMulCommClass M M α] : Diamond (ofSMul M α
 @[scoped grind =]
 theorem ofSMul_preserves_iff [SMul M α] {P : α → Prop} :
     Preserves (ofSMul M α) P ↔ ∀ m : M, ∀ x, P x → P (m • x) := by
-  apply Iff.intro
+  constructor
   case mp =>
     intro h m x hx
     exact h ⟨m, rfl⟩ hx

From 8b44b375108ca8ca969bdf0c7299d3d44cc7a5f3 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:19:36 +0200
Subject: [PATCH 15/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 221c2430e..816ef2aab 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -38,9 +38,8 @@ instance [Monoid M] [MulAction M α] : Std.Refl (ofSMul M α) where
 
 /-- The relation induced by a semigroup action is transitive. -/
 instance [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α) where
-  trans x y z hxy hyz := by
-    rcases hxy with ⟨m, rfl⟩
-    rcases hyz with ⟨n, rfl⟩
+  trans := by
+    rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
     use n * m
     rw [mul_smul]
 /-- The relation induced by a group action is symmetric. -/

From 9048d783d2a4cd67530bbfc62b322d02334b604a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:20:30 +0200
Subject: [PATCH 16/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 816ef2aab..58f459783 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -73,8 +73,7 @@ theorem ofSMul_preserves_iff [SMul M α] {P : α → Prop} :
     intro h m x hx
     exact h ⟨m, rfl⟩ hx
   case mpr =>
-    intro h x y hxy hx
-    rcases hxy with ⟨m, rfl⟩
+    rintro h x y ⟨m, rfl⟩ hx
     exact h m x hx
 
 /-- Membership in a type closed under a scalar action is preserved by the relation induced by the

From 3faeef471d57193be17cc28e366e196c0788ae1a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:20:48 +0200
Subject: [PATCH 17/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 9e4311bed..9bd0d9cbb 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -63,9 +63,9 @@ theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Pro
 @[scoped grind ⇒]
 theorem Satisfies.ofPredicates_preserves_iff {P : α → Prop} (r : α → α → Prop) :
     (∀ a, ⇓Modal[ofPredicates r, a ⊨ P → □P]) ↔ Preserves r P := by
-  apply Iff.intro <;> intro h
+  constructor
   case mp =>
-    intro a₁ a₂ hr hPa₁
+    intro h a₁ a₂ hr hPa₁
     grind [h a₁]
   case mpr =>
     grind [Preserves]

From 54bdef9a1bbdeb39b0ff8a4cc15388def0d8dfb1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:06 +0200
Subject: [PATCH 18/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 9bd0d9cbb..92e3d874b 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -107,7 +107,6 @@ membership in both containers, then atomic infimum is logically equivalent to mo
 theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α → α → Prop) (p q : β)
     (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
     (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by
-  intro
   grind [=_ derivation_def]
 
 end Cslib.Logic.Modal

From ab3a482afaf958bd9b6cb984cc022f4e52ae3beb Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:21 +0200
Subject: [PATCH 19/42] Update CslibTests/Modal/Ideal.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 CslibTests/Modal/Ideal.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
index be8782caf..18ca04fca 100644
--- a/CslibTests/Modal/Ideal.lean
+++ b/CslibTests/Modal/Ideal.lean
@@ -43,7 +43,6 @@ local instance [Monoid α] : MulAction ℕ+ α := posPowAction
 /-- Ideals are invariant under positive exponentiation. -/
 theorem Ideal.posPowSMulMemClass [Semiring R] : SMulMemClass (Ideal R) ℕ+ R where
   smul_mem n x hx := by
-    change _ ^ (n : ℕ) ∈ _
     exact Ideal.pow_mem_of_mem _ hx n n.prop
 
 local instance [Semiring R] : SMulMemClass (Ideal R) ℕ+ R := Ideal.posPowSMulMemClass

From f759698c0618b10d7f7c22846626074338362a6e Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:28 +0200
Subject: [PATCH 20/42] Update CslibTests/Modal/Ideal.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 CslibTests/Modal/Ideal.lean | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
index 18ca04fca..183a213e8 100644
--- a/CslibTests/Modal/Ideal.lean
+++ b/CslibTests/Modal/Ideal.lean
@@ -107,9 +107,8 @@ equivalent to `◇I ∧ ◇J`. -/
 theorem Ideal.radical_inf [CommSemiring R] (I J : Ideal R) :
     (I ⊓ J).radical = I.radical ⊓ J.radical := by
   apply SetLike.ext'
-  rw [Submodule.coe_inf]
-  simp only [Ideal.radical_eq_modal_denotation]
-  rw [Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]
+  simp_rw [Submodule.coe_inf, Ideal.radical_eq_modal_denotation,
+    Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)]
   rfl
 
 end CslibTests

From 78544711e84ff36083c60dbc8c21a94c57b05197 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:42 +0200
Subject: [PATCH 21/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 9 +--------
 1 file changed, 1 insertion(+), 8 deletions(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index a9252163a..6fd5992fa 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -223,14 +223,7 @@ instance : LogicalEquivalence
 
 /-- Correspondence of equivalence and axiom validity. -/
 theorem Proposition.axiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) :
-    (Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := by
-  apply Iff.intro <;> intro h
-  case mp =>
-    intro v w
-    exact h v w
-  case mpr =>
-    intro v w
-    exact h v w
+    (Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := Iff.rfl
 
 open Relation in
 /-- In a transitive diamond model, possibility distributes over conjunction for propositions

From b06cb9307cd7c929aa4e7ecd5e5a2920c7c479db Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:49 +0200
Subject: [PATCH 22/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 6fd5992fa..7883a6fb9 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -238,12 +238,8 @@ theorem Proposition.diamond_and_equiv_of_preserves {m : Model World Atom} [IsTra
   apply Iff.intro
   case mp => grind
   case mpr =>
-    intro h
-    rw [Satisfies.and_iff_and] at h
-    rcases h with ⟨hφ₁, hφ₂⟩
-    rw [Satisfies.diamond_iff_exists] at hφ₁ hφ₂ ⊢
-    rcases hφ₁ with ⟨b, hab, hb⟩
-    rcases hφ₂ with ⟨c, hac, hc⟩
+    rw [Satisfies.and_iff_and, Satisfies.diamond_iff_exists]
+    rintro ⟨⟨b, hab, hb⟩, ⟨c, hac, hc⟩⟩
     rcases hd hab hac with ⟨d, hbd, hcd⟩
     use d, IsTrans.trans _ _ _ hab hbd
     exact ⟨h₁ hbd hb, h₂ hcd hc⟩

From b56bd3f22272c2fc799d4614ae3bddd6f04d12a1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:21:58 +0200
Subject: [PATCH 23/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 7712cc995..9193bcc99 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -390,8 +390,7 @@ theorem axiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ
     Axiom r⇓φ ↔ φ ∈ logic (modelsOfRelation r) := by
   constructor
   case mp =>
-    intro h m hm w
-    subst hm
+    rintro h m rfl w
     exact h m.v w
   case mpr => grind [Satisfies.axiom_def]
 

From 09c052461b8ddd1fdabefcc76ffaac6151de6162 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Mon, 17 Aug 2026 08:22:23 +0200
Subject: [PATCH 24/42] Update CslibTests/Modal/Ideal.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 CslibTests/Modal/Ideal.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
index 183a213e8..d62da1775 100644
--- a/CslibTests/Modal/Ideal.lean
+++ b/CslibTests/Modal/Ideal.lean
@@ -35,8 +35,7 @@ def posPowAction [Monoid α] : MulAction ℕ+ α where
   smul n x := x ^ (n : ℕ)
   one_smul x := pow_one x
   mul_smul m n x := by
-    dsimp [HSMul.hSMul]
-    grind [pow_mul, mul_comm]
+    simp [HSMul.hSMul, ←pow_mul, mul_comm]
 
 local instance [Monoid α] : MulAction ℕ+ α := posPowAction
 

From 359b30085f60421c44fd1750f1f9a730e6de44e4 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Mon, 17 Aug 2026 08:51:22 +0200
Subject: [PATCH 25/42] review comments

---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 26 +++++++---------------
 1 file changed, 8 insertions(+), 18 deletions(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 7883a6fb9..a269a7aa3 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -35,21 +35,12 @@ theorem Proposition.equiv_def (m : Model World Atom) (φ₁ φ₂ : Proposition
     (φ₁.Equiv m φ₂) ↔ φ₁ ≡[Equiv m] φ₂ := by rfl
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_forall_der (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[Equiv m] φ₂) : ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
-  intro s
-  specialize h s
-  assumption
-
-theorem Proposition.forall_der_equiv (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
-    (h : ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[Equiv m] φ₂ := by
-  intro s
-  specialize h s
-  assumption
+theorem Proposition.equiv_iff_forall_der (m : Model World Atom) (φ₁ φ₂ : Proposition Atom)
+    : (φ₁ ≡[Equiv m] φ₂) ↔ ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by rfl
 
 @[scoped grind ⇒]
-theorem Proposition.equiv_iff {m : Model World Atom} {φ₁ φ₂ : Proposition Atom}
-    (h : φ₁ ≡[Equiv m] φ₂) (w : World) : ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
+theorem Proposition.equiv_iff_forall_iff {m : Model World Atom} {φ₁ φ₂ : Proposition Atom} :
+    (φ₁ ≡[Equiv m] φ₂) ↔ ∀ (w : World), ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := by
   grind [=_ Satisfies.iff_iff_iff]
 
 /-- A class of models, defined as a set. -/
@@ -233,12 +224,11 @@ theorem Proposition.diamond_and_equiv_of_preserves {m : Model World Atom} [IsTra
     {φ₁ φ₂ : Proposition Atom} (hd : Diamond m.r) (h₁ : Preserves m.r (⇓Modal[m,· ⊨ φ₁]))
     (h₂ : Preserves m.r (⇓Modal[m,· ⊨ φ₂])) :
     ◇(φ₁ ∧ φ₂) ≡[Equiv m] (◇φ₁ ∧ ◇φ₂) := by
+  rw [equiv_iff_forall_iff]
   intro a
-  rw [Satisfies.iff_iff_iff]
-  apply Iff.intro
+  constructor
   case mp => grind
   case mpr =>
-    rw [Satisfies.and_iff_and, Satisfies.diamond_iff_exists]
     rintro ⟨⟨b, hab, hb⟩, ⟨c, hac, hc⟩⟩
     rcases hd hab hac with ⟨d, hbd, hcd⟩
     use d, IsTrans.trans _ _ _ hab hbd
@@ -247,9 +237,9 @@ theorem Proposition.diamond_and_equiv_of_preserves {m : Model World Atom} [IsTra
 /-- In a reflexive and transitive model, diamond absorbs itself (idempotency). -/
 theorem Proposition.diamond_diamond_equiv {m : Model World Atom} [Std.Refl m.r] [IsTrans World m.r]
     (φ : Proposition Atom) : ◇◇φ ≡[Equiv m] ◇φ := by
+  rw [equiv_iff_forall_iff]
   intro w
-  rw [Satisfies.iff_iff_iff]
-  apply Iff.intro <;> rw [← Satisfies.imp_iff_imp]
+  constructor <;> rw [← Satisfies.imp_iff_imp]
   · grind [Satisfies.four]
   · grind [Satisfies.t]
 

From 1f50aea73c889f79796a15617bad0974e51319a1 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Mon, 17 Aug 2026 08:52:33 +0200
Subject: [PATCH 26/42] spacing

---
 Cslib/Logics/Modal/Lean/SMul.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 58f459783..52dd4f7c4 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -42,6 +42,7 @@ instance [Semigroup M] [SemigroupAction M α] : IsTrans α (ofSMul M α) where
     rintro x _ _ ⟨m, rfl⟩ ⟨n, rfl⟩
     use n * m
     rw [mul_smul]
+
 /-- The relation induced by a group action is symmetric. -/
 instance [Group G] [MulAction G α] : Std.Symm (ofSMul G α) where
   symm := by

From d25e3937fb0e36e0c0b7d37a00452fa14f62b28c Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 18 Aug 2026 12:19:06 +0200
Subject: [PATCH 27/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index a269a7aa3..973aa5503 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -131,7 +131,6 @@ instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv
   constructor
   case refl => grind [Proposition.Equiv]
   case symm =>
-    intro φ₁ φ₂ h w
     grind
   case trans =>
     intro φ₁ φ₂ φ₃ h₁ h₂ w

From 3eccaa24d24ec250fcd87974057344a6b93b5a80 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 18 Aug 2026 12:19:18 +0200
Subject: [PATCH 28/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 973aa5503..7b2df7231 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -133,7 +133,6 @@ instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv
   case symm =>
     grind
   case trans =>
-    intro φ₁ φ₂ φ₃ h₁ h₂ w
     grind
 
 /-- Logical equivalence within a class is an equivalence relation. -/

From 460578e0297f5299022d4aa726ee0ab8699cbd73 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Tue, 18 Aug 2026 12:20:49 +0200
Subject: [PATCH 29/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 7b2df7231..2c648fa25 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -142,14 +142,11 @@ instance {World Atom} (S : ModelClass World Atom) :
   unfold Proposition.EquivWithin
   constructor
   case refl =>
-    intro φ m hm w
     grind [Proposition.Equiv]
   case symm =>
-    intro φ₁ φ₂ h m hm w
-    grind [h m hm w]
+    grind
   case trans =>
-    intro φ₁ φ₂ φ₃ h₁ h₂ m hm w
-    grind [h₁ m hm w, h₂ m hm w]
+    grind
 
 /-- Logical equivalence is a congruence. -/
 instance (m : Model World Atom) : LawfulCongruence (Proposition.Equiv m) where

From a2a5933e14292f37c2bae76d53ad5c210ac50c36 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 19 Aug 2026 11:33:13 +0200
Subject: [PATCH 30/42] review comments

---
 Cslib/Logics/Modal/Basic.lean              | 15 ++++----
 Cslib/Logics/Modal/Denotation.lean         |  2 +-
 Cslib/Logics/Modal/Lean/Basic.lean         |  4 +--
 Cslib/Logics/Modal/LogicalEquivalence.lean | 42 ----------------------
 4 files changed, 12 insertions(+), 51 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 9193bcc99..6206672f9 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -130,6 +130,9 @@ open scoped InferenceSystem Proposition
 theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} :
   Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl
 
+@[simp, scoped grind =]
+theorem Satisfies.atom_iff {a : Atom} : ⇓Modal[m,w ⊨ a] ↔ m.v w a := by rfl
+
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
 theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
@@ -257,7 +260,7 @@ theorem Satisfies.t_refl (r : World → World → Prop) [Nonempty Atom]
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w
     let h' := h (v := v) (w := w) (φ := a)
-    grind [=_ derivation_def]
+    grind
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/
 theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by
@@ -269,7 +272,7 @@ theorem Satisfies.b (r : World → World → Prop) [Std.Symm r] (φ : Propositio
     Axiom r⇓(φ → □◇φ) := by
   intro _ w
   have := Std.Symm.symm (r := r) w
-  grind [=_ derivation_def]
+  grind
 
 /-- Any model that admits the axiom B is symmetric. -/
 theorem Satisfies.b_symm (r : World → World → Prop) [Nonempty Atom]
@@ -279,7 +282,7 @@ theorem Satisfies.b_symm (r : World → World → Prop) [Nonempty Atom]
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
     let h₁ := h (v := v₁) (w := w₁) (φ := a)
     simp [imp_iff_imp] at h₁
-    grind [=_ derivation_def]
+    grind
 
 /-- The 4 axiom, valid for all transitive models. -/
 theorem Satisfies.four (r : World → World → Prop) [IsTrans World r]
@@ -297,7 +300,7 @@ theorem Satisfies.four_trans (r : World → World → Prop) [Nonempty Atom]
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := a)
-    grind [=_ derivation_def]
+    grind
 
 /-- The 5 axiom, valid for all Euclidean models. -/
 theorem Satisfies.five (r : World → World → Prop) [Relation.RightEuclidean r]
@@ -313,7 +316,7 @@ theorem Satisfies.five_rightEuclidean (r : World → World → Prop) [Nonempty A
     have a := Classical.arbitrary Atom
     let v := fun (w' : World) (a : Atom) => w' = w₃
     let h' := h (v := v) (w := w₁) (φ := a)
-    grind [=_ derivation_def]
+    grind
 
 /-- The D axiom, valid for all serial models. -/
 theorem Satisfies.d (r : World → World → Prop) [Relation.Serial r] (φ : Proposition Atom) :
@@ -363,7 +366,7 @@ theorem Satisfies.pointTwo_diamond (r : World → World → Prop) [Nonempty Atom
     (h : ∀ φ : Proposition Atom, Axiom r⇓(◇□φ → □◇φ)) : Diamond r := by
   intro w w₁ w₂ hww₁ hww₂
   specialize h (Classical.arbitrary Atom) (fun w' _ => r w₁ w') w
-  grind [Join, =_ derivation_def]
+  grind [Join]
 
 /-- A proposition is valid in a class of models `S` (modelled as a set) if it is satisfied under
 all models in `S` for all worlds. -/
diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 9def7b078..26b1b9658 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -34,7 +34,7 @@ def Proposition.denotation (m : Model World Atom) :
 @[scoped grind =]
 theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} :
     w ∈ φ.denotation m ↔ ⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind [=_ derivation_def]
+  induction φ generalizing w <;> grind
 
 /-- A world is in the denotation of a proposition iff it is not in the denotation of the negation
 of the proposition. -/
diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 92e3d874b..7b04d61ce 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -57,7 +57,7 @@ open scoped InferenceSystem Satisfies
 /-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
 @[scoped grind =]
 theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
-    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind [=_ derivation_def]
+    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind
 
 /-- Under `Model.ofPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/
 @[scoped grind ⇒]
@@ -107,6 +107,6 @@ membership in both containers, then atomic infimum is logically equivalent to mo
 theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α → α → Prop) (p q : β)
     (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
     (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by
-  grind [=_ derivation_def]
+  grind
 
 end Cslib.Logic.Modal
diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 2c648fa25..834d2b070 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -46,24 +46,6 @@ theorem Proposition.equiv_iff_forall_iff {m : Model World Atom} {φ₁ φ₂ : P
 /-- A class of models, defined as a set. -/
 abbrev ModelClass World Atom := Set (Model World Atom)
 
-/-- Every class of models induces an inference system tag for reasoning within that class. -/
-inductive Within (S : ModelClass World Atom)
-
-instance (S : ModelClass World Atom) : InferenceSystem (Within S) (Judgement World Atom) where
-  derivation j := j.m ∈ S → ⇓j
-
-@[scoped grind =_]
-theorem derivation_within_def {S : ModelClass World Atom} {m : Model World Atom} :
-    (m ∈ S → ⇓Modal[m, w ⊨ φ]) = Within S⇓Modal[m,w ⊨ φ] := rfl
-
-@[scoped grind .]
-theorem Satisfies.within_subset {S₁ S₂ : ModelClass World Atom} {m : Model World Atom}
-    (hs : S₂ ⊆ S₁) (h : Within S₁⇓Modal[m,w ⊨ φ]) : Within S₂⇓Modal[m, w ⊨ φ] := by grind
-
-@[scoped grind =]
-theorem Satisfies.within_univ {m : Model World Atom} :
-    Within (Set.univ (α := Model World Atom))⇓Modal[m,w ⊨ φ] = ⇓Modal[m, w ⊨ φ] := by grind
-
 /-- The modal propositions `φ₁` and `φ₂` are equivalent in the model class `S`. -/
 def Proposition.EquivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) :=
   ∀ m ∈ S, φ₁ ≡[Equiv m] φ₂
@@ -78,21 +60,6 @@ theorem Proposition.equivWithin_def (S : ModelClass World Atom) (φ₁ φ₂ : P
 theorem Proposition.equiv_of_EquivWithin {S : ModelClass World Atom} (h : φ₁ ≡[EquivWithin S] φ₂)
     (m : Model World Atom) (hm : m ∈ S) : φ₁ ≡[Equiv m] φ₂ := h m hm
 
-theorem Proposition.equivWithin_forall_der (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[EquivWithin S] φ₂) : ∀ m ∈ S, ∀ (w : World), Within S⇓Modal[m,w ⊨ φ₁ ↔ φ₂] := by
-  intro m
-  grind [h m]
-
-theorem Proposition.forall_der_equivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
-    (h : ∀ m ∈ S, ∀ (w : World), Within S⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) : φ₁ ≡[EquivWithin S] φ₂ := by
-  intro m hm w
-  grind [h m hm]
-
-theorem Proposition.equivWithin_iff (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom)
-    (h : φ₁ ≡[EquivWithin S] φ₂) (m : Model World Atom) (hm : m ∈ S) (w : World) :
-    Within S⇓Modal[m,w ⊨ φ₁] ↔ Within S⇓Modal[m,w ⊨ φ₂] := by
-  grind [h _ hm w]
-
 /-- Logical equivalence preserves validity. -/
 theorem Proposition.equivWithin_valid (S : ModelClass World Atom)
     (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[EquivWithin S] φ₂) :
@@ -189,15 +156,6 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
 
 open scoped Satisfies.Context
 
-/-- Logical equivalence for Modal Logic within a class of models `S`. -/
-instance (S : ModelClass World Atom) : LogicalEquivalence
-    (α := Proposition Atom)
-    (Judgement := Judgement World Atom) (Within S)
-    (Proposition.EquivWithin S) where
-  eqvFillValid heqv c h := by
-    specialize heqv c.m
-    grind [=_ Satisfies.Context.fill_def]
-
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
 instance : LogicalEquivalence
     (α := Proposition Atom)

From 0c808418b6be7c6fe9c46fdfddfd58d08b9955d2 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 19 Aug 2026 11:34:51 +0200
Subject: [PATCH 31/42] more simplifications

---
 Cslib/Logics/Modal/Lean/Basic.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 7b04d61ce..9d92d01df 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -98,15 +98,12 @@ theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r :
 /-- Pointwise conjunction of Lean predicates is logically equivalent to their modal conjunction in
 the Lean modal model induced by `r`. -/
 theorem Proposition.equivOfPredicates_and {r : α → α → Prop} {P Q : α → Prop} :
-    (fun a => P a ∧ Q a) ≡[Equiv.OfPredicates r] (P ∧ Q) := by
-  simp only [← Proposition.equiv_def]
-  grind [Proposition.Equiv]
+    (fun a => P a ∧ Q a) ≡[Equiv.OfPredicates r] (P ∧ Q) := by grind
 
 /-- Under `Equiv.OfContainers r`, if membership in the infimum of two containers is equivalent to
 membership in both containers, then atomic infimum is logically equivalent to modal conjunction. -/
 theorem Proposition.ofContainers_inf_equiv [Membership α β] [Min β] (r : α → α → Prop) (p q : β)
     (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) :
-    (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by
-  grind
+    (↑(p ⊓ q) : Proposition β) ≡[Equiv.OfContainers r] (p ∧ q) := by grind
 
 end Cslib.Logic.Modal

From 9dbc6728be3d95a30296c242c4046011da1752c0 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:03 +0200
Subject: [PATCH 32/42] Update Cslib/Logics/Modal/LogicalEquivalence.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/LogicalEquivalence.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean
index 834d2b070..afd4cd798 100644
--- a/Cslib/Logics/Modal/LogicalEquivalence.lean
+++ b/Cslib/Logics/Modal/LogicalEquivalence.lean
@@ -64,7 +64,7 @@ theorem Proposition.equiv_of_EquivWithin {S : ModelClass World Atom} (h : φ₁
 theorem Proposition.equivWithin_valid (S : ModelClass World Atom)
     (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[EquivWithin S] φ₂) :
     (φ₁.valid S ↔ φ₂.valid S) := by
-  apply Iff.intro <;> intro h' m hm w <;> grind [h m hm w]
+  grind
 
 /-- Propositional contexts. -/
 inductive Proposition.Context (Atom : Type u) : Type u where

From 9d18b7e98e36bf5def04f74cd8356c33d00af309 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:18 +0200
Subject: [PATCH 33/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 9d92d01df..75d23d50f 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -57,7 +57,7 @@ open scoped InferenceSystem Satisfies
 /-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
 @[scoped grind =]
 theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
-    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := by grind
+    ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := Iff.rfl
 
 /-- Under `Model.ofPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/
 @[scoped grind ⇒]

From 168792aacf768cab69d822b6eebf945a6c34147a Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:31 +0200
Subject: [PATCH 34/42] Update CslibTests/Modal/Ideal.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 CslibTests/Modal/Ideal.lean | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
index d62da1775..6b689688c 100644
--- a/CslibTests/Modal/Ideal.lean
+++ b/CslibTests/Modal/Ideal.lean
@@ -4,13 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Fabrizio Montesi
 -/
 
-import Cslib.Logics.Modal.Denotation
-import Cslib.Logics.Modal.Lean.Basic
 import Cslib.Logics.Modal.Lean.SMul
-import Cslib.Foundations.Relation.Defs
-import Mathlib.Algebra.Group.Defs
-import Mathlib.Algebra.Ring.Defs
-import Mathlib.RingTheory.Ideal.Defs
 import Mathlib.RingTheory.Ideal.Operations
 
 /-! # Example: radicals of ideals with modal logic

From 083ff883442e61b4834d7d2c9475a61fe02994cd Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:39 +0200
Subject: [PATCH 35/42] Update Cslib/Logics/Modal/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Basic.lean | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 6206672f9..b44694be0 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -11,7 +11,10 @@ public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
 public import Cslib.Foundations.Relation.Euclidean
-public import Mathlib.Logic.Nonempty
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.Operators
+public import Cslib.Foundations.Relation.Defs
+public import Mathlib.Order.BooleanAlgebra.Set
 
 /-! # Modal Logic
 

From 6e71bea677ebfe17cc91c518bfce090a96d77e79 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:48 +0200
Subject: [PATCH 36/42] Update Cslib/Logics/Modal/Cube.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Cube.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Cube.lean
index 57c7dc46f..8eb2dc385 100644
--- a/Cslib/Logics/Modal/Cube.lean
+++ b/Cslib/Logics/Modal/Cube.lean
@@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Marianna Girlando
 module
 
 public import Cslib.Logics.Modal.Basic
+public import Cslib.Foundations.Relation.Euclidean
 
 /-! # Modal Logic Cube
 

From 46e9b79ef3e58fd09703e80002409054f21ed7fe Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:39:58 +0200
Subject: [PATCH 37/42] Update Cslib/Logics/Modal/Denotation.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Denotation.lean | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean
index 26b1b9658..f4982e270 100644
--- a/Cslib/Logics/Modal/Denotation.lean
+++ b/Cslib/Logics/Modal/Denotation.lean
@@ -6,7 +6,6 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Logics.Modal.Basic
 public import Cslib.Logics.Modal.LogicalEquivalence
 
 /-! # Denotational semantics for Modal Logic

From 0eb1b48661aafd2e402dfea8e029259475044c72 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:40:07 +0200
Subject: [PATCH 38/42] Update Cslib/Logics/Modal/Lean/SMul.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/SMul.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Lean/SMul.lean
index 52dd4f7c4..06b7a9f29 100644
--- a/Cslib/Logics/Modal/Lean/SMul.lean
+++ b/Cslib/Logics/Modal/Lean/SMul.lean
@@ -6,10 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Mathlib.Algebra.Group.Defs
 public import Mathlib.GroupTheory.GroupAction.SubMulAction
-public import Cslib.Foundations.Relation.Defs
-public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Modal.Lean.Basic
 
 /-! # Modal Logic for scalar multiplication (SMul)

From a357deae22124510bc591e2fc119b2d6a8e9fc97 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:40:16 +0200
Subject: [PATCH 39/42] Update Cslib/Logics/Modal/Lean/Basic.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 Cslib/Logics/Modal/Lean/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean
index 75d23d50f..9c0e11b06 100644
--- a/Cslib/Logics/Modal/Lean/Basic.lean
+++ b/Cslib/Logics/Modal/Lean/Basic.lean
@@ -6,8 +6,6 @@ Authors: Fabrizio Montesi
 
 module
 
-public import Cslib.Logics.Modal.Basic
-public import Cslib.Logics.Modal.LogicalEquivalence
 public import Cslib.Logics.Modal.Denotation
 
 /-! # Modal Logic for Lean

From 82c71c071a3c4fbab36e04d81299c7746c00c161 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <famontesi@gmail.com>
Date: Wed, 19 Aug 2026 18:40:24 +0200
Subject: [PATCH 40/42] Update CslibTests/Modal/Ideal.lean

Co-authored-by: Thomas Krishna Waring <51426330+thomaskwaring@users.noreply.github.com>
---
 CslibTests/Modal/Ideal.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean
index 6b689688c..f9cb8ee2a 100644
--- a/CslibTests/Modal/Ideal.lean
+++ b/CslibTests/Modal/Ideal.lean
@@ -35,8 +35,7 @@ local instance [Monoid α] : MulAction ℕ+ α := posPowAction
 
 /-- Ideals are invariant under positive exponentiation. -/
 theorem Ideal.posPowSMulMemClass [Semiring R] : SMulMemClass (Ideal R) ℕ+ R where
-  smul_mem n x hx := by
-    exact Ideal.pow_mem_of_mem _ hx n n.prop
+  smul_mem n _ hx := Ideal.pow_mem_of_mem _ hx n n.prop
 
 local instance [Semiring R] : SMulMemClass (Ideal R) ℕ+ R := Ideal.posPowSMulMemClass
 

From 1efc4d7c72afe19903d95957ada6278fcf641057 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 19 Aug 2026 18:40:53 +0200
Subject: [PATCH 41/42] grind

---
 Cslib/Logics/Modal/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index b44694be0..12ba1f1da 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -101,7 +101,6 @@ lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl
 
 /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies
 the proposition `φ`. -/
-@[scoped grind]
 def Satisfies (m : Model World Atom) (w : World) : Proposition Atom → Prop
   | .atom p => m.v w p
   | .not φ => ¬Satisfies m w φ
@@ -122,7 +121,6 @@ structure Judgement World Atom where
 @[inherit_doc] scoped notation "Modal[" m "," w " ⊨ " φ "]" => Judgement.mk m w φ
 
 /-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/
-@[simp, scoped grind =]
 def Satisfies.Bundled (j : Judgement World Atom) : Prop := Satisfies j.m j.w j.φ
 
 instance : HasInferenceSystem (Judgement World Atom) := ⟨Satisfies.Bundled⟩

From a3953dc8bfcaf847a04ff721fffbde442eb578e8 Mon Sep 17 00:00:00 2001
From: Fabrizio Montesi <fm@fabriziomontesi.com>
Date: Wed, 19 Aug 2026 18:41:36 +0200
Subject: [PATCH 42/42] imports

---
 Cslib/Logics/Modal/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean
index 12ba1f1da..f397edb4d 100644
--- a/Cslib/Logics/Modal/Basic.lean
+++ b/Cslib/Logics/Modal/Basic.lean
@@ -6,8 +6,6 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Foundations.Logic.Operators
-public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
 public import Cslib.Foundations.Relation.Euclidean