feat(ModalLogic+Congruence): modal reasoning for Lean

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

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
 

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

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
 

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

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⟩
@@ -123,10 +126,13 @@ 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
 
+@[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
@@ -166,7 +172,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.
 
@@ -190,7 +196,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₂) :
@@ -203,27 +209,57 @@ 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. -/
+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_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 : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
+theorem Satisfies.k (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    Axiom 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) :
+    Axiom r⇓(◇φ ↔ ¬□¬φ) := by
+  intro _ w
   simp only [Satisfies.iff_iff_iff]
   constructor
   · 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) :
+    Axiom r⇓(◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂)) := by grind
+
+/-- Possibility can be combined with necessity. -/
+theorem Satisfies.diamond_and_box (r : World → World → Prop) (φ₁ φ₂ : Proposition Atom) :
+    Axiom r⇓((◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂)) := by grind
+
 /-- 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)
+    : 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 : ∀ {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, 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) (φ := .atom a)
+    let h' := h (v := v) (w := w) (φ := a)
     grind
 
 /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/
@@ -232,70 +268,106 @@ 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) :
+    Axiom 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, 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₁) (φ := .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) : Axiom 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), 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₁) (φ := .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) : 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 : ∀ {v} {w : World} {φ : Proposition Atom}, ⇓Modal[⟨r, v⟩,w ⊨ ◇φ → □◇φ]) :
+theorem Satisfies.five_rightEuclidean (r : World → World → Prop) [Nonempty Atom]
+    (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₁) (φ := .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) :
+    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 : ∀ {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, Axiom 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) : Axiom r⇓(□(□φ → φ) → □φ) := by
+  intro v w
+  let m := Model.mk r v
+  simp_rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall]
+  intro h
+  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. -/
+theorem Satisfies.pointTwo (r : World → World → Prop) (h : Diamond r)
+    (φ : 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
+
+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, Axiom r⇓(◇□φ → □◇φ)) : Diamond r := by
+  intro w w₁ w₂ hww₁ hww₂
+  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
 all models in `S` for all worlds. -/
 @[simp, scoped grind =]
@@ -307,4 +379,22 @@ 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 axiom_iff_mem_logic_modelsOfRelation (r : World → World → Prop) (φ : Proposition Atom) :
+    Axiom r⇓φ ↔ φ ∈ logic (modelsOfRelation r) := by
+  constructor
+  case mp =>
+    rintro h m rfl w
+    exact h m.v w
+  case mpr => grind [Satisfies.axiom_def]
+
 end Cslib.Logic.Modal

Cslib/Logics/Modal/Cube.lean

@@ -135,14 +135,18 @@ 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]
 
 /-- 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
 

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
+  constructor <;> 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