diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index ee6a6a16e..b30f9006b 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Copyright (c) 2026 Fabrizio Montesi, Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi, Marianna Girlando +Authors: Fabrizio Montesi, Marianna Girlando, Benjamin Brast-McKie -/ module @@ -18,6 +18,11 @@ public import Mathlib.Logic.Nonempty Modal logic is a logic for reasoning about relational structures, studying statements about necessity (`□φ`) and possibility `◇φ`. +## Primitives + +The formula type uses `{atom, bot, imp, box}` as primitive constructors. Negation, conjunction, +disjunction, and diamond (possibility) are derived connectives following the Lukasiewicz convention. + ## References * [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] @@ -36,49 +41,95 @@ structure Model (World : Type*) (Atom : Type*) where /-- Valuation of atoms at a world. -/ v : World → Atom → Prop -/-- Propositions. -/ +/-- Propositions. Primitives are atoms, falsum, implication, and necessity (box). -/ inductive Proposition (Atom : Type u) : Type u where /-- Atomic proposition. -/ | atom (p : Atom) - /-- Negation. -/ - | not (φ : Proposition Atom) - /-- Conjunction. -/ - | and (φ₁ φ₂ : Proposition Atom) - /-- Possibility. -/ - | diamond (φ : Proposition Atom) - -@[inherit_doc] scoped prefix:40 "¬" => Proposition.not -@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and -@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond - -/-- Disjunction. -/ -def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) + /-- Falsum / bottom. -/ + | bot + /-- Implication. -/ + | imp (φ₁ φ₂ : Proposition Atom) + /-- Necessity / box. -/ + | box (φ : Proposition Atom) + deriving DecidableEq, BEq -@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or +/-- Negation as derived connective: ¬φ := φ → ⊥ -/ +abbrev Proposition.neg (φ : Proposition Atom) : Proposition Atom := .imp φ .bot -/-- Implication. -/ -def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ +/-- Verum / top: ⊤ := ⊥ → ⊥ -/ +abbrev Proposition.top : Proposition Atom := .imp .bot .bot -@[inherit_doc] scoped infix:30 " → " => Proposition.impl +/-- Disjunction: φ₁ ∨ φ₂ := ¬φ₁ → φ₂ -/ +abbrev Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .imp (.imp φ₁ .bot) φ₂ -/-- Bi-implication. -/ -def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) +/-- Conjunction: φ₁ ∧ φ₂ := ¬(φ₁ → ¬φ₂) -/ +abbrev Proposition.and (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .imp (.imp φ₁ (.imp φ₂ .bot)) .bot -@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff +/-- Possibility / diamond: ◇φ := ¬□¬φ -/ +abbrev Proposition.diamond (φ : Proposition Atom) : Proposition Atom := + .neg (.box (.neg φ)) -/-- Necessity. -/ -def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ +/-- Bi-implication. -/ +abbrev Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := + .and (.imp φ₁ φ₂) (.imp φ₂ φ₁) +@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg +@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and +@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or +@[inherit_doc] scoped infix:30 " → " => Proposition.imp @[inherit_doc] scoped prefix:40 "□" => Proposition.box +@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond +@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff /-- 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 φ - | .and φ₁ φ₂ => Satisfies m w φ₁ ∧ Satisfies m w φ₂ - | .diamond φ => ∃ w', m.r w w' ∧ Satisfies m w' φ + | .bot => False + | .imp φ₁ φ₂ => Satisfies m w φ₁ → Satisfies m w φ₂ + | .box φ => ∀ w', m.r w w' → Satisfies m w' φ + +/-- Satisfaction of negation. -/ +theorem Satisfies.neg_iff : Satisfies m w (.neg φ) ↔ ¬Satisfies m w φ := + ⟨fun h hs => h hs, fun h hs => absurd hs h⟩ + +/-- Satisfaction of diamond. -/ +theorem Satisfies.diamond_iff : Satisfies m w (.diamond φ) ↔ ∃ w', m.r w w' ∧ Satisfies m w' φ := by + unfold Proposition.diamond Proposition.neg + simp only [Satisfies] + constructor + · intro h + by_contra hc + push Not at hc + exact h fun w' hr hs => absurd hs (hc w' hr) + · intro ⟨w', hr, hs⟩ hbox + exact hbox w' hr hs + +/-- Satisfaction of conjunction. -/ +theorem Satisfies.and_iff : Satisfies m w (.and φ₁ φ₂) ↔ Satisfies m w φ₁ ∧ Satisfies m w φ₂ := by + change ((Satisfies m w φ₁ → Satisfies m w φ₂ → False) → False) ↔ _ + constructor + · intro h + constructor + · by_contra h1; exact h (fun hs => absurd hs h1) + · by_contra h2; exact h (fun _ hs => absurd hs h2) + · intro ⟨h1, h2⟩ hf; exact hf h1 h2 + +/-- Satisfaction of disjunction. -/ +theorem Satisfies.or_iff : Satisfies m w (.or φ₁ φ₂) ↔ Satisfies m w φ₁ ∨ Satisfies m w φ₂ := by + change ((Satisfies m w φ₁ → False) → Satisfies m w φ₂) ↔ _ + constructor + · intro h + rcases Classical.em (Satisfies m w φ₁) with h1 | h1 + · exact Or.inl h1 + · exact Or.inr (h h1) + · intro h hn + cases h with + | inl h => exact absurd h hn + | inr h => exact h /-- Judgement, representing the conclusions one reaches in modal logic. -/ structure Judgement World Atom where @@ -107,45 +158,44 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/ @[scoped grind =] -theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by - induction φ generalizing w <;> grind - -/-- Characterisation of the `∨` connective. +theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := Satisfies.neg_iff -Disjunction is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `∨` connective. -/ @[scoped grind =] theorem Satisfies.or_iff_or {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or] - -/-- Characterisation of the `→` connective. + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := Satisfies.or_iff -Implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. --/ +/-- Characterisation of the `→` connective. -/ @[scoped grind =] theorem Satisfies.impl_iff_impl {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl] + ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := + Iff.rfl -/-- Characterisation of the `↔` connective. +/-- Characterisation of the `□` modality. -/ +@[scoped grind =] +theorem Satisfies.box_iff_forall {m : Model World Atom} : + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := + Iff.rfl -Bi-implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `◇` modality. -/ @[scoped grind =] -theorem Satisfies.iff_iff_iff {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by - simp only [Proposition.iff] - grind [= derivation_def] +theorem Satisfies.diamond_iff_exists {m : Model World Atom} : + ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.r w w' ∧ ⇓Modal[m,w' ⊨ φ] := Satisfies.diamond_iff -/-- Characterisation of the `□` modality. +/-- Characterisation of `∧` in terms of satisfaction. -/ +@[scoped grind =] +theorem Satisfies.and_iff_and {m : Model World Atom} : + ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := Satisfies.and_iff -Necessity is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ +/-- Characterisation of the `↔` connective. -/ @[scoped grind =] -theorem Satisfies.box_iff_forall {m : Model World Atom} : - ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.r w w' → ⇓Modal[m,w' ⊨ φ] := by grind [Proposition.box] +theorem Satisfies.iff_iff_iff {m : Model World Atom} : + ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by + change Satisfies m w (.and (.imp φ₁ φ₂) (.imp φ₂ φ₁)) ↔ _ + rw [Satisfies.and_iff] + exact ⟨fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩, fun ⟨h₁, h₂⟩ => ⟨h₁, h₂⟩⟩ -/-- The theory of a world in a model is the set of all propositions that it satifies. -/ +/-- The theory of a world in a model is the set of all propositions that it satisfies. -/ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := {φ | ⇓Modal[m,w ⊨ φ]} @@ -153,16 +203,22 @@ abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) := abbrev TheoryEq (m : Model World Atom) (w₁ w₂ : World) := theory m w₁ = theory m w₂ -theorem TheoryEq.ext_iff : TheoryEq m w₁ w₂ ↔ (∀ φ, φ ∈ theory m w₁ ↔ φ ∈ theory m w₂) := by - grind +theorem TheoryEq.ext_iff : TheoryEq m w₁ w₂ ↔ (∀ φ, φ ∈ theory m w₁ ↔ φ ∈ theory m w₂) := + Set.ext_iff /-- 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 : Satisfies m w φ) : φ ∈ theory m w := h /-- If two worlds are not theory equivalent, there exists a distinguishing proposition. -/ lemma not_theoryEq_satisfies (h : ¬TheoryEq m w₁ w₂) : - ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ not_satisfies] + ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by + rw [TheoryEq.ext_iff] at h + push Not at h + obtain ⟨φ, h⟩ := h + rcases h with ⟨h1, h2⟩ | ⟨h1, h2⟩ + · exact ⟨φ, h1, h2⟩ + · exact ⟨¬φ, not_satisfies.mpr h1, fun h3 => not_satisfies.mp h3 h2⟩ /-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as well. -/ @@ -172,71 +228,117 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂) exact (h φ).mp hs /-- The K axiom, valid for all models. -/ -theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind +theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by + change Satisfies m w (.imp (.box (.imp φ₁ φ₂)) (.imp (.box φ₁) (.box φ₂))) + simp only [Satisfies] + intro h1 h2 w' hr + exact h1 w' hr (h2 w' hr) -set_option linter.tacticAnalysis.verifyGrindOnly false in /-- The dual axiom, valid for all models. -/ theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by - grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, - =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true] + change Satisfies m w (.iff (.diamond φ) (.neg (.box (.neg φ)))) + rw [and_iff] + exact ⟨id, id⟩ /-- 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] + (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → ◇φ] := by + change Satisfies m w φ → Satisfies m w (.diamond φ) + intro hφ + rw [diamond_iff] + exact ⟨w, instRefl.refl w, hφ⟩ /-- 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 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) - grind + let v : World → Atom → Prop := fun w' _ => w' = w + have h' := h (v := v) (w := w) (φ := .atom a) + simp only [← derivation_def] at h' + have hsat : Satisfies ⟨r, v⟩ w (.atom a) := rfl + have h₂ := h' hsat + rw [diamond_iff] at h₂ + obtain ⟨w', hr, hv⟩ := h₂ + change w' = w at hv + rwa [hv] at hr /-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/ -theorem Satisfies.t_box_diamond [Std.Refl m.r] : ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by - have := Std.Refl.refl (r := m.r) w - grind +theorem Satisfies.t_box_diamond [Std.Refl m.r] : + ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by + have hrefl := Std.Refl.refl (r := m.r) w + change ((∀ w', m.r w w' → Satisfies m w' φ) → Satisfies m w φ) ↔ + (Satisfies m w φ → Satisfies m w (.diamond φ)) + constructor + · intro h hφ + rw [diamond_iff] + exact ⟨w, hrefl, hφ⟩ + · intro h hbox + exact hbox w hrefl /-- The B axiom, valid for all symmetric models. -/ -theorem Satisfies.b {m : Model World Atom} [Std.Symm m.r] {w : World} (φ : Proposition Atom) : +theorem Satisfies.b {m : Model World Atom} [instSymm : Std.Symm m.r] {w : World} + (φ : Proposition Atom) : ⇓Modal[m,w ⊨ φ → □◇φ] := by - have := Std.Symm.symm (r := m.r) w - grind + change Satisfies m w φ → ∀ w', m.r w w' → Satisfies m w' (.diamond φ) + intro hφ w' hr + rw [diamond_iff] + exact ⟨w, instSymm.symm w w' hr, hφ⟩ /-- 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 - symm w₁ := by + symm {w₁ w₂} hr := by have a := Classical.arbitrary Atom - let v₁ := fun (w' : World) (a : Atom) => w' = w₁ - let h₁ := h (v := v₁) (w := w₁) (φ := .atom a) - simp [impl_iff_impl] at h₁ - grind + let v₁ := fun (w' : World) (_ : Atom) => w' = w₁ + have h₁ : Satisfies ⟨r, v₁⟩ w₁ (.atom a) → + ∀ w', r w₁ w' → Satisfies ⟨r, v₁⟩ w' (.diamond (.atom a)) := + h (v := v₁) (w := w₁) (φ := .atom a) + have hsat : Satisfies ⟨r, v₁⟩ w₁ (.atom a) := rfl + have h₂ := h₁ hsat w₂ hr + rw [diamond_iff] at h₂ + obtain ⟨w'', hr', hv⟩ := h₂ + simp only [Satisfies] at hv + rwa [← hv] /-- 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 - simp only [impl_iff_impl] - intro h - rcases h with ⟨w', h₁, w'', h₂, hs⟩ - exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩ + change Satisfies m w (.diamond (.diamond φ)) → Satisfies m w (.diamond φ) + rw [diamond_iff, diamond_iff] + intro ⟨w', hr₁, h'⟩ + rw [diamond_iff] at h' + obtain ⟨w'', hr₂, hs⟩ := h' + exact ⟨w'', IsTrans.trans _ _ _ hr₁ hr₂, 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 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) - grind + let v := fun (w' : World) (_ : Atom) => w' = w₃ + have h' : Satisfies ⟨r, v⟩ w₁ (.diamond (.diamond (.atom a))) → + Satisfies ⟨r, v⟩ w₁ (.diamond (.atom a)) := + h (v := v) (w := w₁) (φ := .atom a) + have hdd : Satisfies ⟨r, v⟩ w₁ (.diamond (.diamond (.atom a))) := by + rw [diamond_iff] + exact ⟨w₂, h₁, by rw [diamond_iff]; exact ⟨w₃, h₂, rfl⟩⟩ + have h₃ := h' hdd + rw [diamond_iff] at h₃ + obtain ⟨w', hr, hv⟩ := h₃ + simp only [Satisfies] at hv + rwa [← hv] /-- 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) - grind + have heuc := @Relation.RightEuclidean.rightEuclidean (r := m.r) + change Satisfies m w (.diamond φ) → ∀ w', m.r w w' → Satisfies m w' (.diamond φ) + intro hdiam w' hr + rw [diamond_iff] at hdiam ⊢ + obtain ⟨w'', hr', hs⟩ := hdiam + exact ⟨w'', heuc hr hr', hs⟩ /-- Any model that admits 5 is Euclidean. -/ theorem Satisfies.five_rightEuclidean {r : World → World → Prop} [Nonempty Atom] @@ -244,24 +346,43 @@ theorem Satisfies.five_rightEuclidean {r : World → World → Prop} [Nonempty A 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) - grind + let v := fun (w' : World) (_ : Atom) => w' = w₃ + have h' : Satisfies ⟨r, v⟩ w₁ (.diamond (.atom a)) → + ∀ w', r w₁ w' → Satisfies ⟨r, v⟩ w' (.diamond (.atom a)) := + h (v := v) (w := w₁) (φ := .atom a) + have hdiam : Satisfies ⟨r, v⟩ w₁ (.diamond (.atom a)) := by + rw [diamond_iff]; exact ⟨w₃, h₂, rfl⟩ + have h₂' := h' hdiam w₂ h₁ + rw [diamond_iff] at h₂' + obtain ⟨w', hr, hv⟩ := h₂' + simp only [Satisfies] at hv + rwa [← hv] /-- The D axiom, valid for all serial models. -/ -theorem Satisfies.d {m : Model World Atom} [Relation.Serial m.r] {w} (φ : Proposition Atom) : +theorem Satisfies.d {m : Model World Atom} [hSer : Relation.Serial m.r] {w} + (φ : Proposition Atom) : ⇓Modal[m,w ⊨ □φ → ◇φ] := by - have : ∃ w', m.r w w' := Relation.Serial.serial w - grind + change (∀ w', m.r w w' → Satisfies m w' φ) → Satisfies m w (.diamond φ) + intro hbox + rw [diamond_iff] + obtain ⟨w', hr⟩ := hSer.serial w + exact ⟨w', hr, hbox w' hr⟩ /-- 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 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) - grind + let v := fun (_ : World) (_ : Atom) => True + have h' : (∀ w', r w₁ w' → Satisfies ⟨r, v⟩ w' (.atom a)) → + Satisfies ⟨r, v⟩ w₁ (.diamond (.atom a)) := + h (v := v) (w := w₁) (φ := .atom a) + have hbox : ∀ w', r w₁ w' → Satisfies ⟨r, v⟩ w' (.atom a) := + fun _ _ => trivial + have h₃ := h' hbox + rw [diamond_iff] at h₃ + obtain ⟨w', hr, _⟩ := h₃ + exact ⟨w', hr⟩ /-- 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 b74e8f3f1..fdcfab934 100644 --- a/Cslib/Logics/Modal/Denotation.lean +++ b/Cslib/Logics/Modal/Denotation.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Copyright (c) 2026 Fabrizio Montesi, Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Benjamin Brast-McKie -/ module @@ -25,27 +25,62 @@ open scoped Proposition InferenceSystem def Proposition.denotation (m : Model World Atom) : Proposition Atom → Set World | .atom p => {w | m.v w p} - | .not φ => (φ.denotation m)ᶜ - | .and φ₁ φ₂ => φ₁.denotation m ∩ φ₂.denotation m - | .diamond φ => {w | ∃ w', m.r w w' ∧ w' ∈ φ.denotation m} + | .bot => ∅ + | .imp φ₁ φ₂ => (φ₁.denotation m)ᶜ ∪ φ₂.denotation m + | .box φ => {w | ∀ w', m.r w w' → w' ∈ φ.denotation m} /-- Characterisation theorem for the denotational semantics. -/ @[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 with + | atom p => simp [Proposition.denotation, ← derivation_def, Satisfies] + | bot => simp [Proposition.denotation, ← derivation_def, Satisfies] + | imp φ₁ φ₂ ih₁ ih₂ => + simp only [Proposition.denotation, Set.mem_union, Set.mem_compl_iff, + ← derivation_def, Satisfies] + constructor + · intro h hs₁ + rcases h with h | h + · exact absurd (ih₁.mpr hs₁) h + · exact ih₂.mp h + · intro h + by_cases hs : w ∈ φ₁.denotation m + · exact Or.inr (ih₂.mpr (h (ih₁.mp hs))) + · exact Or.inl hs + | box φ ih => + simp only [Proposition.denotation, Set.mem_setOf_eq, ← derivation_def, Satisfies] + exact ⟨fun h w' hr => ih.mp (h w' hr), fun h w' hr => ih.mpr (h w' hr)⟩ /-- A world is in the denotation of a proposition iff it is not in the denotation of the negation of the proposition. -/ @[scoped grind =] theorem not_denotation {m : Model World Atom} (φ : Proposition Atom) : w ∉ (¬φ).denotation m ↔ w ∈ φ.denotation m := by - grind [_=_ satisfies_mem_denotation] + simp only [Proposition.denotation, Set.mem_union, Set.mem_compl_iff] + constructor + · intro h + push Not at h + exact h.1 + · intro h hc + rcases hc with hc | hc + · exact hc h + · simp at hc /-- Two worlds are theory-equivalent iff they are denotationally equivalent. -/ theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} : (TheoryEq m w₁ w₂) ↔ (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by - apply Iff.intro <;> grind [_=_ satisfies_mem_denotation] + constructor + · intro h φ + have hext := TheoryEq.ext_iff.mp h φ + exact ⟨fun h₁ => satisfies_mem_denotation.mpr (hext.mp (satisfies_mem_denotation.mp h₁)), + fun h₂ => satisfies_mem_denotation.mpr (hext.mpr (satisfies_mem_denotation.mp h₂))⟩ + · intro h + apply TheoryEq.ext_iff.mpr + intro φ + have hd := h φ + exact ⟨fun h₁ => satisfies_mem_denotation.mp (hd.mp (satisfies_mem_denotation.mpr h₁)), + fun h₂ => satisfies_mem_denotation.mp (hd.mpr (satisfies_mem_denotation.mpr h₂))⟩ end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index 0fc089e4e..0d4cebec0 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Copyright (c) 2026 Fabrizio Montesi, Benjamin Brast-McKie. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi +Authors: Fabrizio Montesi, Benjamin Brast-McKie -/ module @@ -9,124 +9,133 @@ module public import Cslib.Logics.Modal.Basic public import Cslib.Foundations.Logic.LogicalEquivalence -/-! # Logical Equivalence in Modal Logic +/-! # Logical Equivalence for Modal Propositions -This module defines logical equivalence for modal propositions. -The definitions are parametric on the class of models under consideration. +This file defines a one-hole context for `Proposition`, a fill operation that substitutes a +proposition into the hole, and proves that logical equivalence (agreement of satisfaction across all +models and worlds) is a congruence with respect to contexts. -We also instantiate `LogicalEquivalence` for Modal Logic K, i.e., equivalence -for the class of all models. +## Main Definitions + +* `Proposition.Context` -- a one-hole context matching the `Proposition` constructors +* `Proposition.Context.fill` -- substitute a proposition into the hole +* `Proposition.Equiv` -- two propositions are logically equivalent relative to a class of models +* `LogicalEquivalence` -- typeclass instance connecting equivalence, congruence, and validity + +## Design Notes + +The `Context` constructors mirror the recursive positions of `Proposition`: `imp` has two +sub-proposition positions (left and right), and `box` has one. The ground constructors `atom` and +`bot` have no sub-propositions, so they do not appear in `Context`. -/ @[expose] public section namespace Cslib.Logic.Modal -open scoped InferenceSystem Proposition Satisfies +open scoped InferenceSystem Proposition -/-- 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 ⊨ φ₁ ↔ φ₂] +/-- Logical equivalence for modal propositions, parametric on a class of models `S`. +Two propositions are equivalent when they are satisfied by the same model-world pairs in `S`. -/ +def Proposition.Equiv (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : Prop := + ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] @[inherit_doc] scoped notation φ₁ " ≡[" S "] " φ₂ => Proposition.Equiv S φ₁ φ₂ -@[inherit_doc] -scoped notation φ₁ " ≡ " φ₂ => Proposition.Equiv Set.univ φ₁ φ₂ - -@[scoped grind =] -theorem Proposition.equiv_def (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : - (φ₁ ≡[S] φ₂) ↔ - (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) := by rfl - -@[scoped grind =] -theorem Proposition.equiv_iff (S : Set (Model World Atom)) (φ₁ φ₂ : Proposition Atom) : - (φ₁ ≡[S] φ₂) ↔ - (∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by - simp [Proposition.equiv_def, Satisfies.iff_iff_iff] - -theorem Proposition.equiv_valid (S : Set (Model World Atom)) - (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[S] φ₂) : - (φ₁.valid S ↔ φ₂.valid S) := by - grind - -/-- Propositional contexts. -/ +@[simp] +theorem Proposition.equiv_def {S : Set (Model World Atom)} + {φ₁ φ₂ : Proposition Atom} : + (φ₁ ≡[S] φ₂) ↔ ∀ m ∈ S, ∀ w : World, ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := + Iff.rfl + +theorem Proposition.equiv_iff {S : Set (Model World Atom)} + {φ₁ φ₂ : Proposition Atom} + (h : φ₁ ≡[S] φ₂) {m : Model World Atom} (hm : m ∈ S) {w : World} : + ⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂] := + h m hm w + +/-- A one-hole context for `Proposition`. Each constructor corresponds to a recursive position +in `Proposition`: `impL` is the left argument of `imp`, `impR` is the right argument, and `box` +is the argument of `box`. The `hole` constructor marks the position to be filled. -/ inductive Proposition.Context (Atom : Type u) : Type u where + /-- The position to substitute. -/ | hole - | not (c : Context Atom) - | andL (c : Context Atom) (φ : Proposition Atom) - | andR (φ : Proposition Atom) (c : Context Atom) - | diamond (c : Context Atom) - -/-- Replaces a hole in a propositional context with a proposition. -/ + /-- Context in the left argument of `imp`. -/ + | impL (c : Context Atom) (φ : Proposition Atom) + /-- Context in the right argument of `imp`. -/ + | impR (φ : Proposition Atom) (c : Context Atom) + /-- Context under `box`. -/ + | box (c : Context Atom) + +/-- Fill the hole in a context with a proposition. -/ @[scoped grind =] -def Proposition.Context.fill (c : Context Atom) (φ : Proposition Atom) := - match c with - | hole => φ - | not c => .not (c.fill φ) - | andL c φ' => (c.fill φ).and φ' - | andR φ' c => φ'.and (c.fill φ) - | diamond c => .diamond (c.fill φ) - -instance : HasContext (Proposition Atom) := ⟨Proposition.Context Atom, Proposition.Context.fill⟩ - -@[scoped grind =_] -lemma Proposition.Context.fill_def {Γ : HasContext.Context (Proposition Atom)} : - Γ.fill φ = Γ<[φ] := rfl - -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 - rw [← equivalence_iff_isEquiv] - grind [Equivalence] - -/-- Logical equivalence is a congruence. -/ -instance {World Atom} (S : Set (Model World Atom)) : - Congruence (Proposition Atom) (Proposition.Equiv S) where - elim ctx φ₁ φ₂ heqv m hₘ w := by - induction ctx generalizing w - case hole => grind - case not c ih | andL c ih | andR c ih => - specialize ih w - grind - case diamond c ih => - rw [Satisfies.iff_iff_iff] - apply Iff.intro - all_goals - rintro ⟨w', h⟩ - specialize ih w' - grind - -/-- Judgemental contexts. -/ -structure Satisfies.Context (World Atom : Type*) where - /-- The model to consider. -/ +def Proposition.Context.fill : Proposition.Context Atom → Proposition Atom → Proposition Atom + | .hole, φ => φ + | .impL c ψ, φ => .imp (c.fill φ) ψ + | .impR ψ c, φ => .imp ψ (c.fill φ) + | .box c, φ => .box (c.fill φ) + +instance : HasContext (Proposition Atom) := + ⟨Proposition.Context Atom, Proposition.Context.fill⟩ + +@[simp] +theorem Proposition.Context.fill_def (c : Proposition.Context Atom) (φ : Proposition Atom) : + (c : HasContext.Context (Proposition Atom))<[φ] = c.fill φ := rfl + +instance : IsEquiv (Proposition Atom) + (Proposition.Equiv (World := World) (S : Set (Model World Atom))) where + refl _ _ _ _ := Iff.rfl + symm _ _ hab m hm w := (hab m hm w).symm + trans _ _ _ hab hbc m hm w := (hab m hm w).trans (hbc m hm w) + +instance : Congruence (Proposition Atom) + (Proposition.Equiv (World := World) (S : Set (Model World Atom))) where + elim := by + intro ctx a b hab + change Proposition.Equiv S (ctx.fill a) (ctx.fill b) + intro m hm + induction ctx with + | hole => exact hab m hm + | impL c _ ih => + intro w + simp only [Proposition.Context.fill, ← derivation_def, Satisfies] + exact ⟨fun hf ha => hf ((ih w).mpr ha), fun hf ha => hf ((ih w).mp ha)⟩ + | impR _ c ih => + intro w + simp only [Proposition.Context.fill, ← derivation_def, Satisfies] + exact ⟨fun hf ha => (ih w).mp (hf ha), fun hf ha => (ih w).mpr (hf ha)⟩ + | box c ih => + intro w + simp only [Proposition.Context.fill, ← derivation_def, Satisfies] + exact ⟨fun hf w' hr => (ih w').mp (hf w' hr), + fun hf w' hr => (ih w').mpr (hf w' hr)⟩ + +/-- Judgemental contexts for satisfaction. -/ +structure Satisfies.Context (World : Type*) (Atom : Type*) where + /-- The class of models. -/ + S : Set (Model World Atom) + /-- The model. -/ m : Model World Atom - /-- The world to check propositions against. -/ + /-- Evidence that the model belongs to the class. -/ + hm : m ∈ S + /-- The world satisfying the proposition. -/ w : World -/-- Fills a judgemental context with a proposition. -/ +/-- Fills a judgemental context with a proposition to obtain a judgement. -/ def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) : - Judgement World Atom := Modal[c.m, c.w ⊨ φ] + Judgement World Atom := + ⟨c.m, c.w, φ⟩ -instance judgementalContext : - HasHContext (Judgement World Atom) (Proposition Atom) := +instance : HasHContext (Judgement World Atom) (Proposition Atom) := ⟨Satisfies.Context World Atom, Satisfies.Context.fill⟩ -@[scoped grind =_] -lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} : - Modal[c.m,c.w ⊨ φ] = c<[φ] := rfl - -open scoped Satisfies.Context - -/-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/ instance : LogicalEquivalence (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where eqv := Proposition.Equiv Set.univ eqvFillValid heqv c h := by - specialize heqv c.m - grind + change Satisfies c.m c.w _ + have h' : Satisfies c.m c.w _ := h + exact (heqv c.m (Set.mem_univ _) c.w).mp h' end Cslib.Logic.Modal diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index d04527c10..71715e232 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -82,6 +82,10 @@ open_scoped_all Cslib #grind_lint skip Cslib.LTS.IsBisimulation.traceEq #grind_lint skip Cslib.LTS.IsBisimulationUpTo.isBisimulation #grind_lint skip Cslib.Logic.HML.theoryEq_isBisimulation +#grind_lint skip Cslib.Logic.Modal.not_denotation +#grind_lint skip Cslib.Logic.Modal.Satisfies.and_iff_and +#grind_lint skip Cslib.Logic.Modal.Satisfies.iff_iff_iff +#grind_lint skip Cslib.Logic.Modal.Satisfies.or_iff_or #guard_msgs in #grind_lint check (min := 20) in Cslib