feat(ModalLogic/LambdaCalculus): modal grind set and proof of type safety for simply typed lambda calculus

Cslib.lean

@@ -92,6 +92,7 @@ public import Cslib.Foundations.Relation.Confluence
 public import Cslib.Foundations.Relation.Defs
 public import Cslib.Foundations.Relation.Domain
 public import Cslib.Foundations.Relation.Euclidean
+public import Cslib.Foundations.Relation.Preserves
 public import Cslib.Foundations.Relation.Restriction
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
@@ -184,3 +185,4 @@ public import Cslib.MachineLearning.PACLearning.VCDimension
 public import Cslib.MachineLearning.PACLearning.VersionSpace
 public import Cslib.MachineLearning.PACLearning.VersionSpaceLattice
 public import Cslib.Probability.PMF
+public import Cslib.Tactic.GrindAttrs

Cslib/Foundations/Relation/Confluence.lean

@@ -149,8 +149,7 @@ theorem Confluent.equivalence_join_reflTransGen (h : Confluent r) :
   apply equivalence_join
   grind
 
-set_option linter.tacticAnalysis.verifyGrindOnly false in
-lemma SN_iff_SN_of_rel (x : α) : SN r x ↔ ∀ y, r x y → SN r y := by grind only [Acc]
+lemma SN_iff_SN_of_rel (x : α) : SN r x ↔ ∀ y, r x y → SN r y := by grind [Acc]
 
 lemma SN.intro : (h : ∀ y, r x y → SN r y) → SN r x := (SN_iff_SN_of_rel x).mpr
 

Cslib/Foundations/Relation/Preserves.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi and Thomas Waring. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+module
+
+public import Cslib.Foundations.Relation.Defs
+public import Mathlib.Logic.Function.Defs
+
+/-! # Relations: preservation of properties -/
+
+@[expose] public section
+
+namespace Relation
+
+open scoped Function
+
+/-- A predicate preserved by a relation is also preserved by its reflexive closure. -/
+@[simp, scoped grind =]
+theorem preserves_reflGen_iff : Preserves (ReflGen r) P  ↔ Preserves r P := by grind [Preserves]
+
+/-- A predicate preserved by a relation is also preserved by its transitive closure. -/
+@[simp, scoped grind =]
+theorem preserves_transGen_iff : Preserves (TransGen r) P ↔ Preserves r P := by
+  constructor <;> intro h
+  · grind [Preserves]
+  · intro _ _ hxy
+    induction hxy <;> grind [Preserves]
+
+/-- A predicate is preserved by a relation iff it is preserves by its reflexive and transitive
+closure. -/
+@[simp, scoped grind =]
+theorem preserves_reflTransGen_iff : Preserves (ReflTransGen r) P ↔ Preserves r P := by
+  constructor <;> intro h
+  · intro _ _ hab
+    exact h (ReflTransGen.single hab)
+  · change ReflTransGen r ≤ ((· ≤ ·) on P)
+    exact reflTransGen_le_of_le h
+
+end Relation

Cslib/Init.lean

@@ -9,6 +9,7 @@ module -- shake: keep-downstream, shake: keep-all
 public import Cslib.Foundations.Lint.Basic
 public import Mathlib.Init
 public import Mathlib.Tactic.Common
+public import Cslib.Tactic.GrindAttrs
 
 /-!
 # CSLib Initialization

Cslib/Languages/LambdaCalculus/LocallyNameless/Stlc/Safety.lean

@@ -9,6 +9,7 @@ module
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Basic
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.FullBeta
 public import Cslib.Foundations.Relation.Confluence
+public import Cslib.Foundations.Relation.Preserves
 
 /-! # λ-calculus
 
@@ -31,30 +32,13 @@ universe u v
 
 namespace LambdaCalculus.LocallyNameless.Stlc
 
-open Untyped Typing
+open Untyped Typing Relation
 
 variable {Var : Type u} {Base : Type v} {R : Term Var → Term Var → Prop}
 
 /-- A relation on terms preserves typing if all related terms have the same type. -/
 def PreservesTyping (R : Term Var → Term Var → Prop) (Base : Type v) :=
-  ∀ {Γ t t'} {τ : Ty Base}, Γ ⊢ t ∶ τ → R t t' → Γ ⊢ t' ∶ τ
-
-/-- If a reduction preserves types, so does its reflexive transitive closure. -/
-@[scoped grind →]
-theorem redex_preservesTyping :
-    PreservesTyping R Base → PreservesTyping (Relation.ReflTransGen R) Base := by
-  intros _ _ _ _ _ _ redex
-  induction redex <;> [grind; aesop]
-
-
-open _root_.Relation in
-/-- Confluence preserves type preservation. -/
-theorem confluence_preservesTyping {τ : Ty Base}
-    (con : Confluent R) (p : PreservesTyping R Base) (der : Γ ⊢ a ∶ τ)
-    (ab : ReflTransGen R a b) (ac : ReflTransGen R a c) :
-    ∃ d, ReflTransGen R b d ∧ ReflTransGen R c d ∧ Γ ⊢ d ∶ τ := by
-  have ⟨d, bd, cd⟩ := con ab ac
-  exact ⟨d, bd, cd, redex_preservesTyping p der (ab.trans bd)⟩
+  ∀ ⦃Γ⦄ ⦃τ : Ty Base⦄, Preserves R (Γ ⊢ · ∶ τ)
 
 variable [HasFresh Var] [DecidableEq Var] {Γ : Context Var (Ty Base)}
 
@@ -64,8 +48,9 @@ open LambdaCalculus.LocallyNameless.Untyped.Term FullBeta
 
 set_option linter.unusedDecidableInType false in
 /-- Typing preservation for full beta reduction. -/
-@[scoped grind →]
-theorem preservation (der : Γ ⊢ t ∶ τ) (step : t ⭢βᶠ t') : Γ ⊢ t' ∶ τ := by
+@[scoped grind .]
+theorem preservation : PreservesTyping (Var := Var) (· ⭢βᶠ ·) Base := by
+  intro Γ τ t t' step der
   induction der generalizing t' <;> cases step
   case abs.abs xs _ _ _ xs' _ => apply Typing.abs (free_union Var); grind
   case app.base h der _ _ der_l =>

Cslib/Logics/Modal/Basic.lean

@@ -129,14 +129,14 @@ 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 =]
+@[simp, scoped grind =, modal =]
 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 =]
+@[scoped grind =, modal =]
 theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
 
-@[scoped grind =]
+@[scoped grind =, modal =]
 theorem Satisfies.and_iff_and {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by rfl
 
@@ -148,7 +148,7 @@ theorem Satisfies.diamond_iff_exists {m : Model World Atom} :
 
 Disjunction is defined in terms of the more primitive connectives given in `Proposition`.
 This result proves that the definition is correct. -/
-@[scoped grind =]
+@[scoped grind =, modal =]
 theorem Satisfies.or_iff_or {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by
   grind [=_ Proposition.or_def, Proposition.or]
@@ -158,7 +158,7 @@ theorem Satisfies.or_iff_or {m : Model World Atom} :
 Implication is defined in terms of the more primitive connectives given in `Proposition`.
 This result proves that the definition is correct.
 -/
-@[scoped grind =]
+@[scoped grind =, modal =]
 theorem Satisfies.imp_iff_imp {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by
   grind [=_ Proposition.imp_def, Proposition.imp]
@@ -167,7 +167,7 @@ theorem Satisfies.imp_iff_imp {m : Model World Atom} :
 
 Bi-implication is defined in terms of the more primitive connectives given in `Proposition`.
 This result proves that the definition is correct. -/
-@[scoped grind =]
+@[scoped grind =, modal =]
 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]
@@ -221,12 +221,16 @@ instance (r : World → World → Prop) : InferenceSystem (Axiom r) (Proposition
 theorem Satisfies.axiom_def (r : World → World → Prop) :
     (∀ v w, ⇓Modal[⟨r,v⟩,w ⊨ φ]) ↔ Axiom r⇓φ := by rfl
 
+@[modal .]
+theorem Satisfies.der_of_axiom (h : Axiom m.r⇓φ) : ⇓Modal[m,w ⊨ φ] := h m.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_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. -/
+@[scoped grind ., modal .]
 theorem Satisfies.k (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
     Axiom r⇓(□(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind
 
@@ -240,13 +244,20 @@ theorem Satisfies.dual (r : World → World → Prop) (φ : Proposition Atom) :
   · grind only [= not_iff_not, = diamond_iff_exists, = box_iff_forall]
 
 /-- Possibility preserves conjunction in all models. -/
+@[modal .]
 theorem Satisfies.diamond_and (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
     Axiom r⇓(◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂)) := by grind
 
 /-- Possibility can be combined with necessity. -/
+@[modal .]
 theorem Satisfies.diamond_and_box (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
     Axiom r⇓((◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂)) := by grind
 
+/-- If `φ₁` is necessary and some successor exists, then some successor satisfies `φ₁`. -/
+@[scoped grind ., modal .]
+theorem Satisfies.diamond_of_box {φ₁ φ₂ : Proposition Atom} :
+    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)
     : Axiom r⇓(φ → ◇φ) := by
@@ -334,7 +345,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) : Axiom r⇓(□(□φ → φ) → □φ) := by
+    (hwf : Relation.Terminating 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]
@@ -348,6 +359,15 @@ theorem Satisfies.l (r : World → World → Prop) [IsTrans World r]
   apply ih _ hw'w''
   exact IsTrans.trans _ _ _ hww' hw'w''
 
+/-- Löb induction, via the L axiom. -/
+theorem Satisfies.l_induction (m : Model World Atom) [IsTrans World m.r]
+    (hwf : Relation.Terminating m.r) (hstep : ∀ w, ⇓Modal[m,w ⊨ □φ → φ]) (w : World) :
+    ⇓Modal[m, w ⊨ φ] := by
+  have hl := Satisfies.of_axiom m _ (Satisfies.l m.r hwf φ) w
+  /- We use `grind only` here as a memo and test that the `modal` grind set should be able to derive
+    (the modal part of) this proof. -/
+  grind only [modal, = box_iff_forall]
+
 open Relation in
 /-- Axiom .2, valid for all frames with the diamond property. -/
 theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)

Cslib/Logics/Modal/Cube.lean

@@ -142,7 +142,7 @@ 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]
+  open scoped Proposition in grind
 
 /-- The axiom T is valid in the logic T. -/
 theorem T.t_valid : (φ → ◇φ : Proposition Atom) ∈ T World Atom := by

Cslib/Logics/Modal/Lean/Basic.lean

@@ -6,6 +6,7 @@ Authors: Fabrizio Montesi
 
 module
 
+public import Cslib.Foundations.Relation.Preserves
 public import Cslib.Logics.Modal.Denotation
 
 /-! # Modal Logic for Lean
@@ -53,7 +54,7 @@ open scoped InferenceSystem Satisfies
 /-! ## Models of Lean predicates -/
 
 /-- Under `Model.ofPredicates r`, an atomic proposition `P` holds at `a` iff `P a`. -/
-@[scoped grind =]
+@[scoped grind =, modal =]
 theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) :
     ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := Iff.rfl
 
@@ -104,4 +105,13 @@ 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 grind
 
+/-- Invariants are preserved by the reflexive and transitive closure of the accessibility relation.
+-/
+@[scoped grind ., modal .]
+theorem Satisfies.ofPredicates_preserves_reflTransGen {r : α → α → Prop} {P : α → Prop}
+    (h : ∀ a, ⇓Modal[Model.ofPredicates r,a ⊨ P → □P]) :
+    ∀ a, ⇓Modal[Model.ofPredicates (Relation.ReflTransGen r),a ⊨ P → □P] :=
+  (Satisfies.ofPredicates_preserves_iff (Relation.ReflTransGen r)).mpr
+    (preserves_reflTransGen_iff.mpr ((Satisfies.ofPredicates_preserves_iff r).mp h))
+
 end Cslib.Logic.Modal

Cslib/Tactic/GrindAttrs.lean

@@ -0,0 +1,26 @@
+/-
+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 Lean.Meta.Tactic.Grind.RegisterCommand
+
+/-! # CSLib grind sets
+
+This module registers custom grind sets in CSLib.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Modal
+
+/--
+The `modal` grind set is designed to quickly resolve goals that can be derived from modal reasoning
+without unfolding the underlying Lean semantics of satisfaction for modalities. Use this in
+combination with modal axioms for more powerful proof search. -/
+register_grind_attr modal
+
+end Cslib.Logic.Modal

CslibTests.lean

@@ -17,5 +17,6 @@ import CslibTests.LambdaCalculus
 import CslibTests.MLL
 import CslibTests.Modal
 import CslibTests.Modal.Ideal
+import CslibTests.Modal.Stlc
 import CslibTests.Reduction
 import CslibTests.StatefulProcesses