diff --git a/Cslib.lean b/Cslib.lean index 34a0d27be..a15e2139e 100644 --- a/Cslib.lean +++ b/Cslib.lean @@ -82,6 +82,7 @@ public import Cslib.Foundations.Data.OmegaSequence.InfOcc public import Cslib.Foundations.Data.OmegaSequence.Init public import Cslib.Foundations.Data.OmegaSequence.Temporal public import Cslib.Foundations.Data.OmegaSequence.Topology +public import Cslib.Foundations.Data.PFunctor.Basic public import Cslib.Foundations.Data.PFunctor.Free public import Cslib.Foundations.Data.RelatesInSteps public import Cslib.Foundations.Data.Set.Saturation @@ -101,6 +102,8 @@ public import Cslib.Foundations.Semantics.FLTS.Basic public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS public import Cslib.Foundations.Semantics.FLTS.Prod +public import Cslib.Foundations.Semantics.Frame.Basic +public import Cslib.Foundations.Semantics.Frame.LTS public import Cslib.Foundations.Semantics.LTS.Basic public import Cslib.Foundations.Semantics.LTS.Bisimulation public import Cslib.Foundations.Semantics.LTS.Divergence @@ -168,18 +171,22 @@ public import Cslib.Languages.Mech.LocalComputation public import Cslib.Languages.StatefulProcesses.Basic public import Cslib.Languages.StatefulProcesses.Network public import Cslib.Logics.HML.Basic -public import Cslib.Logics.HML.LogicalEquivalence public import Cslib.Logics.LinearLogic.CLL.Basic public import Cslib.Logics.LinearLogic.CLL.CutElimination public import Cslib.Logics.LinearLogic.CLL.EtaExpansion public import Cslib.Logics.LinearLogic.CLL.MLL 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.Modal.Semantics +public import Cslib.Logics.Modal.Unary.Basic +public import Cslib.Logics.Modal.Unary.LTS +public import Cslib.Logics.Modal.Unimodal.Basic +public import Cslib.Logics.Modal.Unimodal.Cube +public import Cslib.Logics.Modal.Unimodal.Lean.Basic +public import Cslib.Logics.Modal.Unimodal.Lean.SMul public import Cslib.Logics.Propositional.Defs public import Cslib.Logics.Propositional.NaturalDeduction.Basic public import Cslib.Logics.Propositional.NaturalDeduction.Theory diff --git a/Cslib/Foundations/Data/PFunctor/Basic.lean b/Cslib/Foundations/Data/PFunctor/Basic.lean new file mode 100644 index 000000000..4a36db9c7 --- /dev/null +++ b/Cslib/Foundations/Data/PFunctor/Basic.lean @@ -0,0 +1,59 @@ +/- +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.Init +public import Mathlib.Data.PFunctor.Univariate.Basic + +/-! # Additional basic theory on polynomial functors -/ + +@[expose] public section + +namespace PFunctor + +/-- The constant child map for `a`. -/ +def const {P : PFunctor} (a : P.A) (x : α) : P.B a → α := fun _ => x + +@[simp, scoped grind =] +theorem const_apply {P : PFunctor} (a : P.A) (x : α) (i : P.B a) : PFunctor.const a x i = x := rfl + +section Unary + +/-- A polynomial functor is unary if all child types have exactly one element. -/ +class Unary (P : PFunctor) where + unary (a : P.A) : Unique (P.B a) + +attribute [instance_reducible, instance] PFunctor.Unary.unary + +theorem Unary.fun_eq_const [Unary P] + (a : P.A) (f : P.B a → α) : f = fun _ => f default := by + funext i + exact congrArg f (Subsingleton.elim i default) + +/-- A polynomial functor has children with decidable equality. -/ +class DecidableEqChildren (P : PFunctor) where + decidableEq (a : P.A) : DecidableEq (P.B a) + +attribute [instance_reducible, instance] DecidableEqChildren.decidableEq + +/-- A unary polynomial functor has decidable child equality. -/ +instance (P : PFunctor) [P.Unary] : P.DecidableEqChildren where + decidableEq _ _ _ := isTrue (Subsingleton.elim _ _) + +/-- Constructs a unary polynomial functor. -/ +abbrev mkUnary (A : Type*) : PFunctor where + A := A + B := fun _ => Unit + +instance {A : Type u} : (mkUnary A).Unary where + unary _ := by + change Unique Unit + infer_instance + +end Unary + +end PFunctor diff --git a/Cslib/Foundations/Logic/Operators.lean b/Cslib/Foundations/Logic/Operators.lean index fc9f3bb2a..de1d8e7cc 100644 --- a/Cslib/Foundations/Logic/Operators.lean +++ b/Cslib/Foundations/Logic/Operators.lean @@ -7,6 +7,7 @@ Authors: Fabrizio Montesi, Thomas Waring module public import Cslib.Init +public import Cslib.Foundations.Data.PFunctor.Basic /-! # Logical operators @@ -62,21 +63,22 @@ end Propositional section Modal -/-! ## Basic modalities -/ +/-! ## General modalities from modal similarity types (polynomial functors) -/ -/-- The type `α` has a box modality (`□`). -/ -class HasBox (α : Type*) where - /-- `a` is valid in all immediately reachable states. -/ - box (a : α) : α +/-- The type `α` has a family of triangle operators (`Δ`). -/ +class HasTriangle (α : Type*) (τ : outParam PFunctor) where + /-- `Δ[op](φ₁, ..., φₙ)` means that `φ₁`, ..., `φₙ` are valid at some respective related states. + -/ + triangle (op : τ.A) (arg : τ.B op → α) : α -@[inherit_doc] scoped prefix:40 "□" => HasBox.box +@[inherit_doc] scoped notation:50 "Δ[" op "]" arg:max => HasTriangle.triangle op arg -/-- The type `α` has a diamond modality (`◇`). -/ -class HasDiamond (α : Type*) where - /-- `a` is valid in a reachable state. -/ - diamond (a : α) : α +/-- The type `α` has a family of nabla operators (`∇`). -/ +class HasNabla (α : Type*) (τ : outParam PFunctor) where + /-- `∇[op](φ₁, ..., φₙ)` means that `φ₁`, ..., `φₙ` are valid at all respective related states. -/ + nabla (op : τ.A) (arg : τ.B op → α) : α -@[inherit_doc] scoped prefix:40 "◇" => HasDiamond.diamond +@[inherit_doc] scoped notation:50 "∇[" op "]" arg:max => HasNabla.nabla op arg end Modal @@ -88,22 +90,76 @@ Here we need to use the prefix `d` to distinguish our notation from the normal ` A refactoring that makes this unnecessary would be welcome. -/ +/-- The type `α` has a dynamic diamond modality with action type `β` (`d⟨a⟩φ`). -/ +class HasDynamicDiamond (α : Type*) (β : outParam Type*) where + /-- `b` is possibly valid after `a`. -/ + dynDiamond (a : β) (b : α) : α + +@[inherit_doc] scoped notation "d⟨" a "⟩" φ:max => HasDynamicDiamond.dynDiamond a φ + /-- The type `α` has a dynamic box modality with action type `β` (`d[a]φ`). -/ -class HasDynamicBox (α β : Type*) where +class HasDynamicBox (α : Type*) (β : outParam Type*) where /-- `b` is necessarily valid after `a`. -/ dynBox (a : β) (b : α) : α -@[inherit_doc] scoped notation "d[" a "]" φ => HasDynamicBox.dynBox a φ +@[inherit_doc] scoped notation "d[" a "]" φ:max => HasDynamicBox.dynBox a φ -/-- The type `α` has a dynamic diamond modality with action type `β` (`d⟨a⟩φ`). -/ -class HasDynamicDiamond (α β : Type*) where - /-- `b` is possibly valid after `a`. -/ - dynDiamond (a : β) (b : α) : α +/-- A family of triangle operators over induces dynamic diamond modalities by applying each operator +to the constant argument family. -/ +instance [HasTriangle α τ] : HasDynamicDiamond α τ.A where + dynDiamond op φ := Δ[op](PFunctor.const op φ) + +@[simp, scoped grind =, modal =] +theorem dynDiamond_eq_triangle [HasTriangle α τ] (op : τ.A) (φ : α) : + (d⟨op⟩φ) = (Δ[op](PFunctor.const op φ)) := rfl -@[inherit_doc] scoped notation "d⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ +/-- A family of nabla operators induces dynamic box modalities by applying each operator to the +constant argument family. -/ +instance [HasNabla α τ] : HasDynamicBox α τ.A where + dynBox op φ := ∇[op](PFunctor.const op φ) + +@[simp, scoped grind =, modal =] +theorem dynBox_eq_nabla [HasNabla α τ] (op : τ.A) (φ : α) : + (d[op]φ) = (∇[op](PFunctor.const op φ)) := rfl end Dynamic +section Unimodal + +/-! ## Basic modalities (Unimodal logic operators) -/ + +/-- The type `α` has a box modality (`□`). -/ +class HasBox (α : Type*) where + /-- `a` is valid in all immediately reachable states. -/ + box (a : α) : α + +@[inherit_doc] scoped prefix:40 "□" => HasBox.box + +/-- The type `α` has a diamond modality (`◇`). -/ +class HasDiamond (α : Type*) where + /-- `a` is valid in a reachable state. -/ + diamond (a : α) : α + +@[inherit_doc] scoped prefix:40 "◇" => HasDiamond.diamond + +/-- A dynamic diamond modality with a unique action induces a basic diamond modality. -/ +instance [Unique β] [HasDynamicDiamond α β] : HasDiamond α where + diamond φ := d⟨default⟩φ + +@[simp, scoped grind =, modal =] +theorem diamond_eq_dynDiamond [Unique β] [HasDynamicDiamond α β] {φ : α} : + (◇φ) = (d⟨default⟩φ) := rfl + +/-- A dynamic box modality with a unique action induces a basic box modality. -/ +instance [Unique β] [HasDynamicBox α β] : HasBox α where + box φ := d[default]φ + +@[simp, scoped grind =, modal =] +theorem box_eq_dynBox [Unique β] [HasDynamicBox α β] {φ : α} : + (□φ) = (d[default]φ) := rfl + +end Unimodal + section Linear /-! ## Linear connectives -/ diff --git a/Cslib/Foundations/Semantics/Frame/Basic.lean b/Cslib/Foundations/Semantics/Frame/Basic.lean new file mode 100644 index 000000000..5032be48d --- /dev/null +++ b/Cslib/Foundations/Semantics/Frame/Basic.lean @@ -0,0 +1,105 @@ +/- +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.Init +public import Cslib.Foundations.Data.PFunctor.Basic + +/-! # Modal Frames + +A frame is a structure of relations, each with its own arity. + +## Implementation notes + +Frames for general modal logic were formulated with modal similarity types [Blackburn2001], which +we generalise here to arbitrary polynomial functors. + +## References + +* [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] +-/ + +@[expose] public section + +namespace Cslib + +/-- A frame is an indexed structure of potentially heterogeneous relations. + +Frames are typically used in combination with modal logics or akin concepts. This is why we use +`op` (for operator) to range over relation indexes. +-/ +structure Frame World (τ : PFunctor) where + /-- Accessibility relations. -/ + r : (op : τ.A) → World → (τ.B op → World) → Prop + +namespace Frame + +/-- The binary relation obtained by observing position `i` of the worlds accessible via `op`. -/ +def project (f : Frame World τ) (op : τ.A) (i : τ.B op) : World → World → Prop := + fun w w' => ∃ ws, f.r op w ws ∧ ws i = w' + +/-- The binary relation induced by restricting the accessibility relation of `op` +to constant tuples of worlds. -/ +@[instance_reducible] +def diagonal (f : Frame World τ) (op : τ.A) : World → World → Prop := + fun w w' => f.r op w (fun _ => w') + +@[scoped grind →, modal →] +theorem r_const_of_diagonal {f : Frame World τ} (h : f.diagonal op w w') : + f.r op w (fun _ => w') := by grind [Frame.diagonal] + +@[scoped grind →, modal →] +theorem diagonal_of_r [PFunctor.Unary τ] {f : Frame World τ} (h : f.r op w ws) : + f.diagonal op w (ws default) := by grind [Frame.diagonal, PFunctor.Unary.fun_eq_const op ws] + +/-- A frame is diagonally symmetric at `op` if, whenever `w` accesses `ws`, some component of `ws` +accesses the constant sequence at `w`. -/ +class DiagonalSymm (f : Frame World τ) (op : τ.A) where + symm w ws : f.r op w ws → ∃ i, f.r op (ws i) (fun _ => w) + +/-- A frame is transitive at `op` if accessibility can be composed through any accessible component: +whenever `w` accesses `ws₁` and `ws₁ i` accesses `ws₂`, then `w` accesses `ws₂`. +-/ +class Trans (f : Frame World τ) (op : τ.A) where + trans w ws₁ i ws₂ : f.r op w ws₁ → f.r op (ws₁ i) ws₂ → f.r op w ws₂ + +instance (f : Frame World τ) [f.Trans op] (i : τ.B op) : + IsTrans World (f.project op i) where + trans w₁ w₂ w₃ h₁ h₂ := by + rcases h₁ with ⟨ws₁, hr₁, rfl⟩ + rcases h₂ with ⟨ws₂, hr₂, h⟩ + exact ⟨ws₂, Frame.Trans.trans _ _ _ _ hr₁ hr₂, h⟩ + +/-- A frame is right Euclidean at `op` if, whenever a world `w` accesses two tuples `ws₁` and +`ws₂`, some component of `ws₂` accesses `ws₁`. -/ +class RightEuclidean (f : Frame World τ) (op : τ.A) where + rightEuclidean w ws₁ ws₂ : f.r op w ws₁ → f.r op w ws₂ → ∃ i, f.r op (ws₂ i) ws₁ + +/-- A predicate map `Ps` is preserved from `P` by `op` if, whenever `P` holds at a world `w`, +then for every tuple `ws` accessible from `w` via `op`, each component `ws i` satisfies the +corresponding predicate `Ps i`. -/ +def PreservesMap (f : Frame α τ) (op : τ.A) (P : α → Prop) (Ps : τ.B op → α → Prop) : Prop := + ∀ w ws, f.r op w ws → P w → ∃ i, Ps i (ws i) + +/-- Builds a unary frame from an indexed family of binary relations. -/ +def ofRelations {τ : PFunctor} [τ.Unary] (r : τ.A → World → World → Prop) : + Frame World τ where + r i w ws := r i w (ws default) + +@[scoped grind =, modal =] +lemma ofRelations_iff {τ : PFunctor} [τ.Unary] (r : τ.A → World → World → Prop) (i : τ.A) + (w : World) (ws : τ.B i → World) : (ofRelations r).r i w ws ↔ r i w (ws default) := by rfl + +@[simp, scoped grind =, modal =] +lemma ofRelations_diagonal_iff {τ : PFunctor} [τ.Unary] + (r : τ.A → World → World → Prop) (i : τ.A) (w w' : World) : + (ofRelations r).diagonal i w w' ↔ r i w w' := by + rfl + +end Frame + +end Cslib diff --git a/Cslib/Foundations/Semantics/Frame/LTS.lean b/Cslib/Foundations/Semantics/Frame/LTS.lean new file mode 100644 index 000000000..8954352e7 --- /dev/null +++ b/Cslib/Foundations/Semantics/Frame/LTS.lean @@ -0,0 +1,35 @@ +/- +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.Init +public import Cslib.Foundations.Semantics.Frame.Basic +public import Cslib.Foundations.Semantics.LTS.Basic + +/-! # Modal Frames and LTS -/ + +@[expose] public section + +namespace Cslib.LTS + +open PFunctor + +variable (lts : LTS State Label) + +/-- Transforms `lts` into a corresponding unary `Frame`. -/ +def toFrame : Frame State (mkUnary Label) := + Frame.ofRelations (fun μ s s' => lts.Tr s μ s') + +instance : Coe (LTS State Label) (Frame State (PFunctor.mkUnary Label)) := ⟨LTS.toFrame⟩ + +@[simp] +lemma toFrame_r_iff_tr : lts.toFrame.r μ s f ↔ lts.Tr s μ (f default) := by rfl + +@[simp, modal =] +lemma toFrame_diagonal_iff_tr : lts.toFrame.diagonal μ s s' ↔ lts.Tr s μ s' := by rfl + +end Cslib.LTS diff --git a/Cslib/Logics/HML/Basic.lean b/Cslib/Logics/HML/Basic.lean index 00c8f74e3..3a2db2bd5 100644 --- a/Cslib/Logics/HML/Basic.lean +++ b/Cslib/Logics/HML/Basic.lean @@ -7,8 +7,9 @@ Authors: Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker module public import Cslib.Foundations.Semantics.LTS.Bisimulation -public import Cslib.Foundations.Logic.Operators -public import Cslib.Foundations.Logic.InferenceSystem +public import Cslib.Foundations.Semantics.Frame.LTS +public import Cslib.Logics.Modal.Semantics +public import Cslib.Logics.Modal.Unary.LTS /-! # Hennessy-Milner Logic (HML) @@ -47,252 +48,52 @@ distinguishing proposition that one state satisfies and the other does not. @[expose] public section -namespace Cslib.Logic.HML +namespace Cslib.Logic.Modal -/-- Propositions. -/ -inductive Proposition (Label : Type u) : Type u where - /-- Truth. -/ - | true - /-- Conjunction. -/ - | and (φ₁ φ₂ : Proposition Label) - /-- Negation. -/ - | not (φ : Proposition Label) - /-- Possibility (dynamic diamond modality). -/ - | diamond (μ : Label) (φ : Proposition Label) - -instance : Top (Proposition Label) := ⟨.true⟩ -instance : HasAnd (Proposition Label) := ⟨.and⟩ -instance : HasNot (Proposition Label) := ⟨.not⟩ -instance : HasDynamicDiamond (Proposition Label) Label := ⟨.diamond⟩ - -/-- Falsity, derived from negation and truth. -/ -@[match_pattern] -def Proposition.false : Proposition Label := ¬⊤ - -instance : Bot (Proposition Label) := ⟨.false⟩ - -/-- Disjunction, derived from negation and conjunction. -/ -@[match_pattern] -def Proposition.or (φ₁ φ₂ : Proposition Label) : Proposition Label := ¬(¬φ₁ ∧ ¬φ₂) - -instance : HasOr (Proposition Label) := ⟨Proposition.or⟩ - -/-- Implication. -/ -@[match_pattern] -def Proposition.imp (φ₁ φ₂ : Proposition Label) : Proposition Label := ¬φ₁ ∨ φ₂ - -instance : HasImp (Proposition Label) := ⟨.imp⟩ - -/-- Bi-implication. -/ -@[match_pattern] -def Proposition.iff (φ₁ φ₂ : Proposition Label) : Proposition Label := (φ₁ → φ₂) ∧ (φ₂ → φ₁) - -instance : HasIff (Proposition Label) := ⟨.iff⟩ - -/-- Necessity (dynamic box modality), derived from dynamic diamond and negation. -/ -@[match_pattern] -def Proposition.box (μ : Label) (φ : Proposition Label) : Proposition Label := ¬d⟨μ⟩¬φ - -instance : HasDynamicBox (Proposition Label) Label := ⟨.box⟩ - -@[scoped grind =] -lemma Proposition.top_def : .true = ((⊤ : Proposition Label)) := rfl - -@[scoped grind =] -lemma Proposition.bot_def : .false = ((⊥ : Proposition Label)) := rfl +open PFunctor -@[scoped grind =] -lemma Proposition.and_def (φ₁ φ₂ : Proposition Label) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl - -@[scoped grind =] -lemma Proposition.not_def (φ : Proposition Label) : φ.not = ¬φ := rfl - -@[scoped grind =] -lemma Proposition.diamond_def (μ : Label) (φ : Proposition Label) : - Proposition.diamond μ φ = d⟨μ⟩φ := rfl - -@[scoped grind =] -lemma Proposition.or_def (φ₁ φ₂ : Proposition Label) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl - -@[scoped grind =] -lemma Proposition.imp_def (φ₁ φ₂ : Proposition Label) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl - -@[scoped grind =] -lemma Proposition.iff_def (φ₁ φ₂ : Proposition Label) : - φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl +namespace HML -@[scoped grind =] -lemma Proposition.box_def (μ : Label) (φ : Proposition Label) : Proposition.box μ φ = d[μ]φ := rfl +/-- Propositions. -/ +abbrev Proposition (Label Atom : Type*) := Modal.Proposition (mkUnary Label) Atom /-- Finite conjunction of propositions. -/ @[simp, scoped grind =] -def Proposition.finiteAnd (φs : List (Proposition Label)) : Proposition Label := +def Proposition.finiteAnd (φs : List (Proposition Label Atom)) : Proposition Label Atom := List.foldr (· ∧ ·) ⊤ φs /-- Finite disjunction of propositions. -/ @[simp, scoped grind =] -def Proposition.finiteOr (φs : List (Proposition Label)) : Proposition Label := +def Proposition.finiteOr (φs : List (Proposition Label Atom)) : Proposition Label Atom := List.foldr (· ∨ ·) ⊥ φs -/-- Satisfaction relation. `Satisfies lts s φ` means that, in the LTS `lts`, the state `s` satisfies -the proposition `φ`. -/ -@[scoped grind] -def Satisfies (lts : LTS State Label) (s : State) : Proposition Label → Prop - | .true => True - | .and φ₁ φ₂ => Satisfies lts s φ₁ ∧ Satisfies lts s φ₂ - | .not φ => ¬Satisfies lts s φ - | .diamond μ φ => ∃ s', lts.Tr s μ s' ∧ Satisfies lts s' φ - -/-- Judgement, representing the conclusions one reaches in HML. -/ -structure Judgement State Label where - /-- Constructs a judgement. -/ - mk :: - /-- LTS. -/ - lts : LTS State Label - /-- The state satisfying the proposition `φ`. -/ - state : State - /-- The proposition satisfied by the state `s`. -/ - φ : Proposition Label - -@[inherit_doc] scoped notation "HML[" lts "," s " ⊨ " φ "]" => Judgement.mk lts s φ - -/-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/ -@[simp, scoped grind =] -def Satisfies.Bundled (j : Judgement State Label) : Prop := Satisfies j.lts j.state j.φ - -instance : HasInferenceSystem (Judgement State Label) := ⟨Satisfies.Bundled⟩ - -open scoped InferenceSystem Proposition +end HML -@[scoped grind =] -theorem derivation_def : Satisfies lts s φ = ⇓HML[lts,s ⊨ φ] := rfl - -@[scoped grind =] -theorem Satisfies.not_iff_not : ⇓HML[lts,s ⊨ ¬φ] ↔ ¬⇓HML[lts,s ⊨ φ] := by rfl - -@[scoped grind .] -theorem Satisfies.top : ⇓HML[lts,s ⊨ ⊤] := by - dsimp [Top.top] - grind [=_ derivation_def] - -@[scoped grind .] -theorem Satisfies.bot : ¬⇓HML[lts,s ⊨ ⊥] := by - simp only [Bot.bot] - grind [= Proposition.false] - -@[scoped grind =] -theorem Satisfies.and_iff_and : - ⇓HML[lts,s ⊨ φ₁ ∧ φ₂] ↔ ⇓HML[lts,s ⊨ φ₁] ∧ ⇓HML[lts,s ⊨ φ₂] := by rfl - -@[scoped grind =] -theorem Satisfies.or_iff_or : - ⇓HML[lts,s ⊨ φ₁ ∨ φ₂] ↔ ⇓HML[lts,s ⊨ φ₁] ∨ ⇓HML[lts,s ⊨ φ₂] := by - grind [=_ Proposition.or_def, Proposition.or] - -@[scoped grind =] -theorem Satisfies.diamond_iff_exists : - ⇓HML[lts,s ⊨ d⟨μ⟩φ] ↔ ∃ s', lts.Tr s μ s' ∧ ⇓HML[lts,s' ⊨ φ] := by rfl - -/-- Characterisation of the `→` connective. - -Implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. --/ -@[scoped grind =] -theorem Satisfies.imp_iff_imp : - ⇓HML[lts,s ⊨ φ₁ → φ₂] ↔ (⇓HML[lts,s ⊨ φ₁] → ⇓HML[lts,s ⊨ φ₂]) := by - grind [=_ Proposition.imp_def, Proposition.imp] - -/-- Characterisation of the `↔` connective. +open Model HML LTS +open scoped HML.Proposition Modal.Proposition InferenceSystem Satisfies Frame LTS -Bi-implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ -@[scoped grind =] -theorem Satisfies.iff_iff_iff : - ⇓HML[lts,s ⊨ φ₁ ↔ φ₂] ↔ (⇓HML[lts,s ⊨ φ₁] ↔ ⇓HML[lts,s ⊨ φ₂]) := by - simp only [HasIff.iff, Proposition.iff] - grind - -@[scoped grind =] -theorem Satisfies.box_iff_forall : - ⇓HML[lts,s ⊨ d[μ]φ] ↔ ∀ s', lts.Tr s μ s' → ⇓HML[lts,s' ⊨ φ] := by - grind [=_ Proposition.box_def, Proposition.box] +variable {lts : LTS State Label} {v : State → Atom → Prop} /-- A state satisfies a finite conjunction iff it satisfies all conjuncts. -/ @[scoped grind =] theorem Satisfies.finiteAnd_iff_forall : - ⇓HML[lts,s ⊨ Proposition.finiteAnd φs] ↔ ∀ φ ∈ φs, ⇓HML[lts,s ⊨ φ] := by + ⇓Modal[ofLTS lts v,s ⊨ Proposition.finiteAnd φs] ↔ ∀ φ ∈ φs, ⇓Modal[ofLTS lts v,s ⊨ φ] := by induction φs <;> grind /-- A state satisfies a finite disjunction iff it satisfies some disjunct. -/ @[scoped grind =] theorem Satisfies.finiteOr_iff_exists : - ⇓HML[lts,s ⊨ Proposition.finiteOr φs] ↔ ∃ φ ∈ φs, ⇓HML[lts,s ⊨ φ] := by + ⇓Modal[ofLTS lts v,s ⊨ Proposition.finiteOr φs] ↔ ∃ φ ∈ φs, ⇓Modal[ofLTS lts v,s ⊨ φ] := by induction φs <;> grind -/-- Denotation of a proposition. -/ -@[simp, scoped grind =] -def Proposition.denotation (lts : LTS State Label) - : Proposition Label → Set State - | .true => Set.univ - | .and φ₁ φ₂ => φ₁.denotation lts ∩ φ₂.denotation lts - | .not φ => (φ.denotation lts)ᶜ - | .diamond μ φ => {s | ∃ s', lts.Tr s μ s' ∧ s' ∈ φ.denotation lts} - -/-- The theory of a state is the set of all propositions that it satisfies. -/ -abbrev theory (lts : LTS State Label) (s : State) : Set (Proposition Label) := - {φ | ⇓HML[lts,s ⊨ φ]} - -/-- Two states are theory-equivalent (for a specific LTS) if they have the same theory. -/ -abbrev TheoryEq (lts : LTS State Label) (s1 s2 : State) := - theory lts s1 = theory lts s2 - -open Proposition LTS - -/-- Characterisation theorem for the denotational semantics. -/ -@[scoped grind =] -theorem mem_denotation_iff_satisfies {φ : Proposition Label} : - s ∈ φ.denotation lts ↔ ⇓HML[lts,s ⊨ φ] := by - induction φ generalizing s <;> grind [=_ derivation_def] - -@[scoped grind .] -theorem mem_theory_iff_satisfies : φ ∈ theory 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 -of the proposition. -/ -@[scoped grind =] -theorem not_denotation {lts : LTS State Label} (φ : Proposition Label) : - s ∉ (¬φ).denotation lts ↔ s ∈ φ.denotation lts := by grind - -/-- Two states are theory-equivalent iff they are denotationally equivalent. -/ -theorem theoryEq_denotation_eq {lts : LTS State Label} : - TheoryEq lts s1 s2 ↔ - (∀ φ : Proposition Label, s1 ∈ φ.denotation lts ↔ s2 ∈ φ.denotation lts) := by - grind [=_ mem_theory_iff_satisfies, =_ mem_denotation_iff_satisfies] - -/-- If two states are not theory equivalent, there exists a distinguishing proposition. -/ -lemma not_theoryEq_satisfies (h : ¬TheoryEq lts s1 s2) : - ∃ φ, (⇓HML[lts,s1 ⊨ φ] ∧ ¬⇓HML[lts,s2 ⊨ φ]) := by - grind [=_ Satisfies.not_iff_not] - -/-- If two states are theory equivalent and the former satisfies a proposition, the latter does as -well. -/ -theorem theoryEq_satisfies (h : TheoryEq lts s1 s2) - (hs : ⇓HML[lts,s1 ⊨ φ]) : ⇓HML[lts,s2 ⊨ φ] := by - unfold TheoryEq theory at h - rw [Set.ext_iff] at h - exact (h φ).mp hs - section ImageToPropositions -variable {lts : LTS State Label} (stateMap : lts.image s μ → Proposition Label) -variable [finImage : Fintype (lts.image s μ)] +variable {s : State} {μ : Label} {lts : LTS State Label} + (stateMap : lts.image s μ → HML.Proposition Label Atom) + [finImage : Fintype (lts.image s μ)] /-- The list of propositions over finite μ-derivatives. -/ -noncomputable def propositions : List (Proposition Label) := +noncomputable def propositions : List (HML.Proposition Label Atom) := finImage.elems.toList.map stateMap theorem propositions_complete (s' : lts.image s μ) : stateMap s' ∈ propositions stateMap := by @@ -300,9 +101,9 @@ theorem propositions_complete (s' : lts.image s μ) : stateMap s' ∈ propositio use s', Finset.mem_toList.mpr (Fintype.complete s') theorem propositions_satisfies_conjunction (htr : lts.Tr s1 μ s1') - (hdist_spec : ∀ s2', ⇓HML[lts,s1' ⊨ (stateMap s2')]) : - ⇓HML[lts,s1 ⊨ d⟨μ⟩finiteAnd (propositions stateMap)] := by - rw [Satisfies.diamond_iff_exists] + (hdist_spec : ∀ s2', ⇓Modal[ofLTS lts v,s1' ⊨ (stateMap s2')]) : + ⇓Modal[ofLTS lts v,s1 ⊨ d⟨μ⟩(Proposition.finiteAnd (propositions stateMap))] := by + rw [Satisfies.dynDiamond_iff_exists] use s1', htr rw [Satisfies.finiteAnd_iff_forall] intro φ hφ_mem @@ -311,59 +112,67 @@ theorem propositions_satisfies_conjunction (htr : lts.Tr s1 μ s1') end ImageToPropositions /-- Theory equivalence is a bisimulation. -/ -@[scoped grind ⇒] -theorem theoryEq_isBisimulation (lts : LTS State Label) +theorem theoryEq_isBisimulation [image_finite : ∀ s μ, Finite (lts.image s μ)] : - lts.IsHomBisimulation (TheoryEq lts) := by + lts.IsHomBisimulation (TheoryEq (ofLTS lts v)) := by intro s1 s2 h μ let (s : State) := @Fintype.ofFinite (lts.image s μ) (image_finite s μ) constructor case left => intro s1' htr by_contra - have hdist : ∀ s2' : lts.image s2 μ, ∃ φ, ⇓HML[lts,s1' ⊨ φ] ∧ ¬⇓HML[lts,s2'.val ⊨ φ] := by + have hdist : ∀ s2' : lts.image s2 μ, ∃ φ, ⇓Modal[ofLTS lts v,s1' ⊨ φ] ∧ + ¬⇓Modal[ofLTS lts v,s2'.val ⊨ φ] := by intro ⟨s2', hs2'⟩ apply not_theoryEq_satisfies grind choose dist_formula hdist_spec using hdist let conjunction := Proposition.finiteAnd (propositions dist_formula) - have hs1_diamond : ⇓HML[lts,s1 ⊨ d⟨μ⟩conjunction] := by + have hs1_diamond : ⇓Modal[ofLTS lts v,s1 ⊨ d⟨μ⟩conjunction] := by grind [propositions_satisfies_conjunction] - obtain ⟨s2'', htr2, hsat⟩ := Satisfies.diamond_iff_exists.mp (theoryEq_satisfies h hs1_diamond) + obtain ⟨s2'', htr2, hsat⟩ := Satisfies.dynDiamond_iff_exists.mp + (theoryEq_satisfies h hs1_diamond) grind [propositions_complete dist_formula ⟨s2'', htr2⟩] case right => -- Symmetric to left case intro s2' htr by_contra - have hdist : ∀ s1' : lts.image s1 μ, ∃ a, Satisfies lts s2' a ∧ ¬Satisfies lts s1'.val a := by + have hdist : ∀ s1' : lts.image s1 μ, ∃ a, ⇓Modal[ofLTS lts v, s2' ⊨ a] ∧ + ¬⇓Modal[ofLTS lts v, s1'.val ⊨ a] := by intro ⟨s1', hs1'⟩ apply not_theoryEq_satisfies grind choose dist_formula hdist_spec using hdist let conjunction := Proposition.finiteAnd (propositions dist_formula) - have hs2_diamond : ⇓HML[lts,s2 ⊨ d⟨μ⟩conjunction] := by + have hs2_diamond : ⇓Modal[ofLTS lts v,s2 ⊨ d⟨μ⟩conjunction] := by grind [propositions_satisfies_conjunction] obtain ⟨s1'', htr1, hsat⟩ := - Satisfies.diamond_iff_exists.mp (theoryEq_satisfies h.symm hs2_diamond) + Satisfies.dynDiamond_iff_exists.mp (theoryEq_satisfies h.symm hs2_diamond) grind [propositions_complete dist_formula ⟨s1'', htr1⟩] /-- If two states are in a bisimulation, one satisfies a proposition iff the other does. -/ -@[scoped grind ⇒] lemma bisimulation_satisfies {hrb : lts.IsHomBisimulation r} - (hr : r s1 s2) (φ : Proposition Label) : ⇓HML[lts,s1 ⊨ φ] ↔ ⇓HML[lts,s2 ⊨ φ] := by - induction φ generalizing s1 s2 <;> grind [IsBisimulation] - -lemma bisimulation_theoryEq {hrb : lts.IsHomBisimulation r} (hr : r s1 s2) : - TheoryEq lts s1 s2 := by grind + (hv : ∀ {s1 s2}, r s1 s2 → ∀ p, v s1 p ↔ v s2 p) (hr : r s1 s2) + (φ : HML.Proposition Label Atom) : + ⇓Modal[ofLTS lts v,s1 ⊨ φ] ↔ ⇓Modal[ofLTS lts v,s2 ⊨ φ] := by + induction φ generalizing s1 s2 with + | triangle => + rw [Proposition.triangle_def, Proposition.unary_triangle_eq_dynDiamond] + grind only [IsBisimulation, Satisfies.ofLTS_dynDiamond_iff_exists] + | _ => grind + +lemma bisimulation_theoryEq {hrb : lts.IsHomBisimulation r} + (hv : ∀ {s1 s2}, r s1 s2 → ∀ p, v s1 p ↔ v s2 p) (hr : r s1 s2) : + TheoryEq (ofLTS lts v) s1 s2 := by grind [bisimulation_satisfies] /-- Theory equivalence and bisimilarity coincide for image-finite LTSs. -/ -theorem theoryEq_eq_bisimilarity {lts : LTS State Label} - [image_finite : ∀ s μ, Finite (lts.image s μ)] : - TheoryEq lts = HomBisimilarity lts := by +theorem theoryEq_eq_bisimilarity + [image_finite : ∀ s μ, Finite (lts.image s μ)] + (hv : ∀ {s1 s2}, s1 ~[lts] s2 → ∀ p, v s1 p ↔ v s2 p := by grind) : + TheoryEq (ofLTS lts v) = HomBisimilarity lts := by ext s1 s2 apply Iff.intro <;> intro h - · exists TheoryEq lts - grind - · grind + · exact ⟨TheoryEq (ofLTS lts v), h, theoryEq_isBisimulation⟩ + · grind [bisimulation_satisfies] -end Cslib.Logic.HML +end Cslib.Logic.Modal diff --git a/Cslib/Logics/HML/LogicalEquivalence.lean b/Cslib/Logics/HML/LogicalEquivalence.lean deleted file mode 100644 index 0b251f1e1..000000000 --- a/Cslib/Logics/HML/LogicalEquivalence.lean +++ /dev/null @@ -1,192 +0,0 @@ -/- -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.HML.Basic -public import Cslib.Foundations.Logic.LogicalEquivalence - -/-! # Logical Equivalence in HML - -This module defines logical equivalence for HML propositions and instantiates `LogicalEquivalence`. --/ - -@[expose] public section - -namespace Cslib.Logic.HML - -open scoped InferenceSystem Satisfies - -section Theory - -/-! ## Theory of logical equivalence -/ - -/-- The HML propositions `φ₁` and `φ₂` are logically equivalent under the LTS `lts`. -/ -def Proposition.Equiv (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) : Prop := - ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂] - -instance : Congruence (Proposition.Equiv lts) := ⟨⟩ - -@[scoped grind =] -theorem Proposition.equiv_def (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) : - (φ₁.Equiv lts φ₂) ↔ φ₁ ≡[Equiv lts] φ₂ := by rfl - -@[scoped grind ⇒] -theorem Proposition.equiv_forall_der (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) - (h : φ₁ ≡[Equiv lts] φ₂) : ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂] := by - intro s - specialize h s - assumption - -theorem Proposition.forall_der_equiv (lts : LTS State Label) (φ₁ φ₂ : Proposition Label) - (h : ∀ (s : State), ⇓HML[lts,s ⊨ φ₁ ↔ φ₂]) : - φ₁ ≡[Equiv lts] φ₂ := by - intro s - specialize h s - assumption - -@[scoped grind ⇒] -theorem Proposition.equiv_iff {lts : LTS State Label} {φ₁ φ₂ : Proposition Label} - (h : φ₁ ≡[Equiv lts] φ₂) (s : State) : - ⇓HML[lts,s ⊨ φ₁] ↔ ⇓HML[lts,s ⊨ φ₂] := by - grind [=_ Satisfies.iff_iff_iff] - -/-- Propositional contexts. -/ -inductive Proposition.Context (Label : Type u) : Type u where - | hole - | andL (c : Context Label) (φ : Proposition Label) - | andR (φ : Proposition Label) (c : Context Label) - | not (c : Context Label) - | diamond (μ : Label) (c : Context Label) - -/-- Replaces a hole in a propositional context with a proposition. -/ -@[scoped grind =] -def Proposition.Context.fill (c : Context Label) (φ : Proposition Label) := - match c with - | hole => φ - | andL c φ' => (c.fill φ).and φ' - | andR φ' c => φ'.and (c.fill φ) - | not c => .not (c.fill φ) - | diamond μ c => .diamond μ (c.fill φ) - -instance : HasContext (Proposition Label) := ⟨Proposition.Context.fill⟩ - -@[scoped grind =] -lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} : - c.fill φ = c<[φ] := rfl - -open scoped Proposition Proposition.Context - -/-- Logical equivalence is an equivalence relation. -/ -instance : IsEquiv (Proposition Label) (Proposition.Equiv lts) := by - rw [← equivalence_iff_isEquiv] - grind [Equivalence, Proposition.Equiv] - -/-- Logical equivalence is a lawful congruence. -/ -instance (lts : LTS State Label) : - LawfulCongruence (Proposition.Equiv lts) where - elim ctx φ₁ φ₂ heqv := by - induction ctx - case hole => - grind [=_ Proposition.Context.fill_def] - case not c ih | andL c ih | andR c ih => - intro s - grind [=_ Proposition.Context.fill_def] - case diamond c ih => - intro s - rw [Satisfies.iff_iff_iff] - apply Iff.intro - · grind [=_ Proposition.Context.fill_def] - · rintro ⟨w', h⟩ - specialize ih w' - grind [=_ Proposition.Context.fill_def] - -/-- Judgemental contexts. -/ -structure Judgement.Context State Label where - /-- The labelled transition system to consider. -/ - lts : LTS State Label - /-- The state to check propositions against. -/ - state : State - -/-- Fills a judgemental context with a proposition. -/ -def Judgement.Context.fill (c : Judgement.Context State Label) (φ : Proposition Label) : - Judgement State Label where - lts := c.lts - state := c.state - φ := φ - -instance : HasHContext (Judgement State Label) (Proposition Label) := - ⟨Judgement.Context.fill⟩ - -@[scoped grind =] -lemma Judgement.Context.fill_def {c : Judgement.Context World Atom} {φ : Proposition Atom} : - HML[c.lts,c.state ⊨ φ] = c<[φ] := rfl - -/-- Universal logical equivalence: logical equivalence under all LTSs. -/ -def Proposition.UEquiv.{u, v} {Label : Type v} (φ₁ φ₂ : Proposition Label) : Prop := - ∀ ⦃State : Type u⦄ (lts : LTS State Label), φ₁ ≡[Equiv lts] φ₂ - -instance : DefaultCongruence (Proposition Label) (Proposition.UEquiv (Label := Label)) := ⟨⟩ - -@[scoped grind =] -theorem Proposition.uEquiv_def.{u, v} : UEquiv.{u, v} φ₁ φ₂ ↔ φ₁ ≡[UEquiv.{u, v}] φ₂ := by - simp [Congruence.r] - -@[scoped grind =] -theorem Proposition.uEquiv_iff_forall_equiv.{u, v} {Label : Type v} (φ₁ φ₂ : Proposition Label) : - (φ₁ ≡[UEquiv.{u, v}] φ₂) ↔ ∀ {State : Type u} (lts : LTS State Label), φ₁ ≡[Equiv lts] φ₂ := by - rfl - -/-- Universal logical equivalence is an equivalence relation. -/ -instance : IsEquiv (Proposition Label) Proposition.UEquiv := by - rw [← equivalence_iff_isEquiv] - constructor - · intro φ State lts s - grind - · intro φ₁ φ₂ h State lts s - grind [h lts] - · intro φ₁ φ₂ φ₃ h₁ h₂ State lts - grind [h₁ lts, h₂ lts, Proposition.forall_der_equiv lts] - -/-- Universal logical equivalence is a lawful congruence. -/ -instance {Label} : LawfulCongruence (Proposition.UEquiv (Label := Label)) where - elim : - Covariant (Proposition.Context Label) (Proposition Label) Proposition.Context.fill - Proposition.UEquiv := by - intro ctx φ₁ φ₂ h State lts - induction ctx <;> grind [h lts, Proposition.forall_der_equiv lts] - -instance : LogicalEquivalence (Judgement := Judgement State Label) InferenceSystem.Default - (Proposition.UEquiv (Label := Label)) where - eqvFillValid heqv c h := by - specialize heqv c.lts c.state - grind [=_ Judgement.Context.fill_def, HasHContext.fill, Judgement.Context.fill] - -end Theory - -section Equivalences - -/-! ## Database of logical equivalences -/ - -namespace Proposition - -theorem false_and_false_eqv_false : - (⊥ ∧ ⊥ : Proposition Label) ≡ (⊥ : Proposition Label) := by - intro State lts - have := forall_der_equiv lts - grind - -/-- The dual axiom (reformulated for HML from modal logic). -/ -theorem dual (μ : Label) (φ : Proposition Label) : - (d⟨μ⟩φ) ≡ (¬d[μ]¬φ) := by - intro State lts s - grind - -end Proposition - -end Equivalences - -end Cslib.Logic.HML diff --git a/Cslib/Logics/Modal/Basic.lean b/Cslib/Logics/Modal/Basic.lean index 2c1c5bb59..e4bd82143 100644 --- a/Cslib/Logics/Modal/Basic.lean +++ b/Cslib/Logics/Modal/Basic.lean @@ -1,23 +1,37 @@ /- Copyright (c) 2026 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Fabrizio Montesi, Marianna Girlando +Authors: Fabrizio Montesi -/ module +public import Mathlib.Data.PFunctor.Univariate.Basic public import Mathlib.Data.Set.Basic +public import Mathlib.Order.BooleanAlgebra.Set public import Mathlib.Order.Defs.Unbundled public import Cslib.Foundations.Relation.Euclidean public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Foundations.Logic.Operators public import Cslib.Foundations.Relation.Defs -public import Mathlib.Order.BooleanAlgebra.Set +public import Cslib.Foundations.Syntax.HasSubstitution /-! # Modal Logic -Modal logic is a logic for reasoning about relational structures, studying statements about -necessity (`□φ`) and possibility (`◇φ`). +Modal logic is a logic for reasoning about (possibly polyadic) relational structures, studying +**qualified** statements through the use of **modalities** (like necessity, possibility, knowledge, +belief, permission, etc.). + +This module formalises general modal logic, parameterised over a signature of modal operators. A +signature is formalised as a polynomial functor (`PFunctor`), generalising the concept of modal +similarity types from the literature [Blackburn2001]. + +## Implementation notes + +- Compared to [Blackburn2001], a triangle takes a map of arguments (from the argument type given + by the polynomial functor to propositions), instead of a sequence of arguments. +- The use of `τ` to range over signatures of modal operators comes from the literature + [Blackburn2001]. ## References @@ -28,391 +42,170 @@ necessity (`□φ`) and possibility (`◇φ`). @[expose] public section -namespace Cslib.Logic.Modal +attribute [modal =] PFunctor.const_apply -/-- A model consists of a relation between worlds `r` and a valuation `v`. -/ -structure Model (World : Type*) (Atom : Type*) where - /-- World accessibility relation. -/ - r : World → World → Prop - /-- Valuation of atoms at a world. -/ - v : World → Atom → Prop +namespace Cslib.Logic.Modal -/-- Propositions. -/ -inductive Proposition (Atom : Type u) : Type u where +/-- A modal proposition. -/ +inductive Proposition (τ : PFunctor) Atom where /-- Atomic proposition. -/ | atom (p : Atom) + /-- Falsehood. -/ + | false /-- Negation. -/ - | not (φ : Proposition Atom) - /-- Conjunction. -/ - | and (φ₁ φ₂ : Proposition Atom) - /-- Possibility. -/ - | diamond (φ : Proposition Atom) + | not (φ : Proposition τ Atom) + /-- Disjunction. -/ + | or (φ₁ φ₂ : Proposition τ Atom) + /-- Generalised possibility, or triangle. -/ + | triangle (op : τ.A) (φs : τ.B op → Proposition τ Atom) + +/-- A map of propositions for the operator `op` in the polynomial functor `τ`. -/ +abbrev PropositionMap τ op Atom := τ.B op → Proposition τ Atom /-- Utility to coerce atoms into atomic propositions. -/ -instance : Coe Atom (Proposition Atom) := ⟨.atom⟩ +instance : Coe Atom (Proposition τ Atom) := ⟨.atom⟩ + +instance {τ : PFunctor} {Atom : Type*} : Bot (Proposition τ Atom) := ⟨.false⟩ +instance {τ : PFunctor} {Atom : Type*} : HasNot (Proposition τ Atom) := ⟨.not⟩ +instance {τ : PFunctor} {Atom : Type*} : HasOr (Proposition τ Atom) := ⟨Proposition.or⟩ +instance {τ : PFunctor} {Atom : Type*} : HasTriangle (Proposition τ Atom) τ := ⟨.triangle⟩ -instance : HasNot (Proposition Atom) := ⟨.not⟩ -instance : HasAnd (Proposition Atom) := ⟨.and⟩ -instance : HasDiamond (Proposition Atom) := ⟨.diamond⟩ +@[scoped grind =] +lemma Proposition.false_def : (.false : Proposition (τ := τ) (Atom := Atom)) = ⊥ := rfl + +@[scoped grind =] +lemma Proposition.not_def (φ : Proposition τ Atom) : φ.not = ¬φ := rfl @[scoped grind =] -lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl +lemma Proposition.or_def (φ₁ φ₂ : Proposition τ Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl @[scoped grind =] -lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl +lemma Proposition.triangle_def {τ : PFunctor} (op : τ.A) + (φs : τ.B op → Proposition τ Atom) : Proposition.triangle op φs = (Δ[op]φs) := rfl + +/-- Truth. -/ +@[match_pattern] +def Proposition.true : Proposition τ Atom := ¬⊥ + +instance {τ : PFunctor} {Atom : Type*} : Top (Proposition τ Atom) := ⟨.true⟩ @[scoped grind =] -lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl +lemma Proposition.true_def : Proposition.true (τ := τ) (Atom := Atom) = ⊤ := rfl -/-- Disjunction. -/ -def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂) +/-- Conjunction. -/ +@[match_pattern] +def Proposition.and (φ₁ φ₂ : Proposition τ Atom) := ¬(¬φ₁ ∨ ¬φ₂) -instance : HasOr (Proposition Atom) := ⟨Proposition.or⟩ +instance {τ : PFunctor} {Atom : Type*} : HasAnd (Proposition τ Atom) := ⟨.and⟩ @[scoped grind =] -lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl +lemma Proposition.and_def (φ₁ φ₂ : Proposition τ Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl /-- Implication. -/ -def Proposition.imp (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂ +@[match_pattern] +def Proposition.imp (φ₁ φ₂ : Proposition τ Atom) := ¬φ₁ ∨ φ₂ -instance : HasImp (Proposition Atom) := ⟨.imp⟩ +instance {τ : PFunctor} {Atom : Type*} : HasImp (Proposition τ Atom) := ⟨.imp⟩ @[scoped grind =] -lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl +lemma Proposition.imp_def (φ₁ φ₂ : Proposition τ Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl /-- Bi-implication. -/ -def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁) +@[match_pattern] +def Proposition.iff (φ₁ φ₂ : Proposition τ Atom) := (φ₁ → φ₂) ∧ (φ₂ → φ₁) -instance : HasIff (Proposition Atom) := ⟨.iff⟩ +instance {τ : PFunctor} {Atom : Type*} : HasIff (Proposition τ Atom) := ⟨.iff⟩ @[scoped grind =] -lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) : - φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl +lemma Proposition.iff_def (φ₁ φ₂ : Proposition τ Atom) : φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl -/-- Necessity. -/ -def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ +/-- Point-wise negation of a proposition map. -/ +def PropositionMap.not (φs : PropositionMap τ op Atom) := fun i => ¬φs i -instance : HasBox (Proposition Atom) := ⟨.box⟩ +instance {τ : PFunctor} {op : τ.A} {Atom : Type*} : HasNot (PropositionMap τ op Atom) := ⟨.not⟩ -@[scoped grind =] -lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl +@[simp, scoped grind =, modal =] +theorem PropositionMap.not_apply {φs : PropositionMap τ op Atom} (i : τ.B op) : + (¬φs) i = ¬(φs i) := by simp [HasNot.not, PropositionMap.not] -/-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies -the proposition `φ`. -/ -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' φ +/-- Point-wise conjunction of proposition maps. -/ +def PropositionMap.and (φs₁ φs₂ : PropositionMap τ op Atom) := fun i => φs₁ i ∧ φs₂ i -/-- Judgement, representing the conclusions one reaches in modal logic. -/ -structure Judgement World Atom where - /-- Constructs a judgement. -/ - mk :: - /-- Model. -/ - m : Model World Atom - /-- The world satisfying the proposition `φ`. -/ - w : World - /-- The proposition satisfied by the world `w`. -/ - φ : Proposition Atom +instance {τ : PFunctor} {op : τ.A} {Atom : Type*} : HasAnd (PropositionMap τ op Atom) := ⟨.and⟩ -@[inherit_doc] scoped notation "Modal[" m "," w " ⊨ " φ "]" => Judgement.mk m w φ +@[scoped grind =, modal =] +theorem PropositionMap.and_apply (φs₁ φs₂ : PropositionMap τ op Atom) (i : τ.B op) : + (φs₁ ∧ φs₂) i = (φs₁ i ∧ φs₂ i) := rfl -/-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/ -def Satisfies.Bundled (j : Judgement World Atom) : Prop := Satisfies j.m j.w j.φ +/-- Point-wise disjunction of proposition maps. -/ +def PropositionMap.or (φs₁ φs₂ : PropositionMap τ op Atom) := fun i => φs₁ i ∨ φs₂ i -instance : HasInferenceSystem (Judgement World Atom) := ⟨Satisfies.Bundled⟩ +instance {τ : PFunctor} {op : τ.A} {Atom : Type*} : HasOr (PropositionMap τ op Atom) := ⟨.or⟩ -open scoped InferenceSystem Proposition +/-- Point-wise implication of proposition maps. -/ +def PropositionMap.imp (φs₁ φs₂ : PropositionMap τ op Atom) := fun i => φs₁ i → φs₂ i -@[scoped grind =] -theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom} : - Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl +instance {τ : PFunctor} {op : τ.A} {Atom : Type*} : HasImp (PropositionMap τ op Atom) := ⟨.imp⟩ + +/-- Point-wise bi-implication of proposition maps. -/ +def PropositionMap.iff (φs₁ φs₂ : PropositionMap τ op Atom) := fun i => φs₁ i ↔ φs₂ i + +instance {τ : PFunctor} {op : τ.A} {Atom : Type*} : HasIff (PropositionMap τ op Atom) := ⟨.iff⟩ @[simp, scoped grind =, modal =] -theorem Satisfies.atom_iff {a : Atom} : ⇓Modal[m,w ⊨ a] ↔ m.v w a := by rfl +theorem PropositionMap.or_apply (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : + (φs ∨ ψs) i = (φs i ∨ ψs i) := rfl -/-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/ -@[scoped grind =, modal =] -theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl +@[simp, scoped grind =, modal =] +theorem PropositionMap.imp_apply (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : + (φs → ψs) i = (φs i → ψs i) := rfl -@[scoped grind =, modal =] -theorem Satisfies.and_iff_and {m : Model World Atom} : - ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by rfl +@[simp, scoped grind =, modal =] +theorem PropositionMap.iff_apply (φs ψs : PropositionMap τ op Atom) (i : τ.B op) : + (φs ↔ ψs) i = (φs i ↔ ψs i) := rfl -@[scoped grind =] -theorem Satisfies.diamond_iff_exists {m : Model World Atom} : - ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.r w w' ∧ ⇓Modal[m,w' ⊨ φ] := by rfl +/-- Generalised necessity, or nabla (∇), dual of triangle. -/ +@[match_pattern] +def Proposition.nabla {τ : PFunctor} (op : τ.A) (φs : τ.B op → Proposition τ Atom) := + ¬Δ[op]¬φs -/-- Characterisation of the `∨` connective. +instance {τ : PFunctor} {Atom : Type*} : HasNabla (Proposition τ Atom) τ := ⟨.nabla⟩ -Disjunction is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ -@[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] +@[scoped grind =] +lemma Proposition.nabla_def {τ : PFunctor} (op : τ.A) + (φs : τ.B op → Proposition τ Atom) : Proposition.nabla op φs = (∇[op]φs) := rfl -/-- Characterisation of the `→` connective. +/-- The constant proposition map for `op`. -/ +abbrev PropositionMap.const {τ : PFunctor} (op : τ.A) (φ : Proposition τ Atom) : + PropositionMap τ op Atom := PFunctor.const op φ -Implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. --/ -@[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] +/-- Negation commutes with constant proposition maps. -/ +@[simp, scoped grind =, modal =] +theorem PropositionMap.const_not {τ : PFunctor} (op : τ.A) (φ : Proposition τ Atom) : + PropositionMap.const op (¬φ) = ¬PropositionMap.const op φ := by grind only [modal] -/-- Characterisation of the `↔` connective. +/-- Conjunction commutes with constant proposition maps. -/ +@[simp, scoped grind =, modal =] +theorem PropositionMap.const_and {τ : PFunctor} (op : τ.A) (φ ψ : Proposition τ Atom) : + PropositionMap.const op (φ ∧ ψ) = (PropositionMap.const op φ ∧ PropositionMap.const op ψ) := by + grind only [modal] -Bi-implication is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ -@[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] - grind +/-- Disjunction commutes with constant proposition maps. -/ +@[simp, scoped grind =, modal =] +theorem PropositionMap.const_or {τ : PFunctor} (op : τ.A) (φ ψ : Proposition τ Atom) : + PropositionMap.const op (φ ∨ ψ) = (PropositionMap.const op φ ∨ PropositionMap.const op ψ) := by + grind only [modal] -/-- Characterisation of the `□` modality. +/-- Implication commutes with constant proposition maps. -/ +@[simp, scoped grind =, modal =] +theorem PropositionMap.const_imp {τ : PFunctor} (op : τ.A) (φ ψ : Proposition τ Atom) : + PropositionMap.const op (φ → ψ) = (PropositionMap.const op φ → PropositionMap.const op ψ) := by + grind only [modal] -Necessity is defined in terms of the more primitive connectives given in `Proposition`. -This result proves that the definition is correct. -/ -@[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_def, Proposition.box] - -/-- 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 ⊨ φ]} - -/-- Two worlds are theory-equivalent under a model if they have the same theory. -/ -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 - -/-- Any proposition satisfied by a world is in the theory of that world. -/ -@[scoped 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₂) : - ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ Satisfies.not_iff_not] - -/-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as -well. -/ -theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂) - (hs : Satisfies m w₁ φ) : ⇓Modal[m,w₂ ⊨ φ] := by - 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 - -@[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 - -/-- The dual axiom, valid for all models. -/ -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. -/ -@[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 - 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, 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 - -/-- 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 - -/-- The B axiom, valid for all symmetric models. -/ -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 (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₁) (φ := a) - grind - -/-- The 4 axiom, valid for all transitive models. -/ -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 : ∀ (φ : 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 - -/-- The 5 axiom, valid for all Euclidean models. -/ -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 : ∀ φ : 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 - -/-- The D axiom, valid for all serial models. -/ -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 : ∀ φ : 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₁) (φ := 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 : 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] - 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'' - -/-- 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) - (φ : 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 =] -def Proposition.valid (S : Set (Model World Atom)) (φ : Proposition Atom) : Prop := - ∀ (m : Model World Atom), ∀ (_ : m ∈ S), ∀ (w : World), ⇓Modal[m,w ⊨ φ] - -/-- The modal logic of a class of models `S` is the set of all propositions valid in `S`. -/ -@[simp, scoped grind =] -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] +/-- Bi-implication commutes with constant proposition maps. -/ +@[simp, scoped grind =, modal =] +theorem PropositionMap.const_iff {τ : PFunctor} (op : τ.A) (φ ψ : Proposition τ Atom) : + PropositionMap.const op (φ ↔ ψ) = (PropositionMap.const op φ ↔ PropositionMap.const op ψ) := by + grind only [modal] end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Denotation.lean b/Cslib/Logics/Modal/Denotation.lean index f1ef01c7d..f98fc6df1 100644 --- a/Cslib/Logics/Modal/Denotation.lean +++ b/Cslib/Logics/Modal/Denotation.lean @@ -22,30 +22,31 @@ open scoped Proposition InferenceSystem Satisfies /-- Denotation of a proposition. -/ @[simp, scoped grind =] -def Proposition.denotation (m : Model World Atom) : - Proposition Atom → Set World +def Proposition.denotation (m : Model World τ Atom) : + Proposition τ Atom → Set World | .atom p => {w | m.v w p} + | .false => ∅ | .not φ => (φ.denotation m)ᶜ - | .and φ₁ φ₂ => φ₁.denotation m ∩ φ₂.denotation m - | .diamond φ => {w | ∃ w', m.r w w' ∧ w' ∈ φ.denotation m} + | .or φ₁ φ₂ => φ₁.denotation m ∪ φ₂.denotation m + | .triangle op φs => {w | ∃ ws, m.r op w ws ∧ ∀ i, ws i ∈ (φs i).denotation m} /-- Characterisation theorem for the denotational semantics. -/ @[scoped grind =] -theorem satisfies_mem_denotation {m : Model World Atom} {φ : Proposition Atom} : +theorem satisfies_mem_denotation {m : Model World τ Atom} {φ : Proposition τ Atom} : w ∈ φ.denotation m ↔ ⇓Modal[m,w ⊨ φ] := by 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. -/ @[scoped grind =] -theorem not_denotation {m : Model World Atom} (φ : Proposition Atom) : +theorem not_denotation {m : Model World τ Atom} (φ : Proposition τ Atom) : w ∉ (¬φ).denotation m ↔ w ∈ φ.denotation m := by grind [_=_ satisfies_mem_denotation] /-- Two worlds are theory-equivalent iff they are denotationally equivalent. -/ -theorem theoryEq_denotation_eq {m : Model World Atom} {w₁ w₂ : World} : +theorem theoryEq_denotation_eq {m : Model World τ Atom} {w₁ w₂ : World} : (TheoryEq m w₁ w₂) ↔ - (∀ (φ : Proposition Atom), w₁ ∈ (φ.denotation m) ↔ w₂ ∈ (φ.denotation m)) := by + (∀ (φ : 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. -/ diff --git a/Cslib/Logics/Modal/Lean/Basic.lean b/Cslib/Logics/Modal/Lean/Basic.lean index 59cab25bd..e0eafa16e 100644 --- a/Cslib/Logics/Modal/Lean/Basic.lean +++ b/Cslib/Logics/Modal/Lean/Basic.lean @@ -21,97 +21,107 @@ namespace Cslib.Logic.Modal namespace Model -/-- Given a relation `r` on `α`, constructs the modal model whose worlds are elements of `α` +/-- Given a frame `f` 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 +abbrev ofPredicates (f : Frame α τ) : Model α τ (α → Prop) where + toFrame := f v w P := P w -/-- Given a relation `r` on `α` and a container type `β` for `α` (`Membership α β`), constructs the +/-- Given a frame `f` 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 +abbrev ofContainers [Membership α β] (f : Frame α τ) : Model α τ β where + toFrame := f v w p := w ∈ p /-- Abbreviation for `Model.ofContainers` where the container type is a `Set`. -/ -abbrev ofSets (r : α → α → Prop) : Model α (Set α) := ofContainers r +abbrev ofSets (f : Frame α τ) : Model α τ (Set α) := ofContainers f -/-- The set model and predicate model of a relation are definitionally equal. -/ -theorem ofSets_eq_ofPredicates (r : α → α → Prop) : - ofSets r = ofPredicates r := rfl +/-- The set model and predicate model of a frame are definitionally equal. -/ +theorem ofSets_eq_ofPredicates (f : Frame α τ) : ofSets f = ofPredicates f := 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 =, modal =] -theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (r : α → α → Prop) : - ⇓Modal[ofPredicates r, a ⊨ P] ↔ P a := Iff.rfl +theorem Satisfies.ofPredicates_atom_iff {P : α → Prop} (f : Frame α τ) : + ⇓Modal[ofPredicates f,a ⊨ P] ↔ P a := Iff.rfl -/-- 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 +/-- In the predicate model generated by `f`, `P → ∇[op]Ps` holds everywhere iff `op` +preserves the predicate map `Ps` from `P`. -/ +@[scoped grind ., modal .] +theorem Satisfies.ofPredicates_preservesMap_iff {P : α → Prop} {Ps : τ.B op → α → Prop} + (f : Frame α τ) : + (∀ w, ⇓Modal[ofPredicates f,w ⊨ P → ∇[op](fun i => (Ps i : Proposition τ (α → Prop)))]) ↔ + f.PreservesMap op P Ps := by constructor - case mp => - intro h a₁ a₂ hr hPa₁ - grind [h a₁] - case mpr => - grind [Preserves] + · intro h w ws hr hP + have h' := h w + rw [Satisfies.imp_iff_imp] at h' + specialize h' hP + rw [Satisfies.nabla_iff_forall] at h' + obtain ⟨i, hi⟩ := h' ws hr + exact ⟨i, by simpa using hi⟩ + · intro h w + rw [Satisfies.imp_iff_imp, Satisfies.nabla_iff_forall] + intro hP ws hr + obtain ⟨i, hi⟩ := h w ws hr hP + exact ⟨i, by simpa using hi⟩ -/-- 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) := +@[scoped grind =, modal =] +theorem Satisfies.ofContainers_atom_iff [Membership α β] {f : Frame α τ} {b : β} : + ⇓Modal[Model.ofContainers f,w ⊨ (b : Proposition τ β)] ↔ w ∈ b := + Iff.rfl + +/-- Logical equivalence under `Model.ofPredicates`. -/ +abbrev Proposition.Equiv.OfPredicates (f : Frame α τ) := + Proposition.Equiv (Model.ofPredicates f) + +/-- Logical equivalence under `Model.ofContainers`. -/ +abbrev Proposition.Equiv.OfContainers [Membership α β] (f : Frame α τ) := + Proposition.Equiv (Model.ofContainers (β := β) f) + +/-- Logically equivalent propositions under `Equiv.OfPredicates f` have the same denotation in the +Lean modal model induced by `ofPredicates f`. -/ +@[scoped grind =] +theorem Proposition.equivOfPredicates_denotation_eq {f : Frame α τ} + {φ₁ φ₂ : Proposition τ (α → Prop)} : + (φ₁ ≡[Equiv.OfPredicates f] φ₂) ↔ + φ₁.denotation (ofPredicates f) = φ₂.denotation (ofPredicates f) := equiv_iff_denotation_eq -/-- Logically equivalent propositions under `Equiv.OfContainers r` have the same denotation in the -Lean modal model induced by `ofContainers r`. -/ +/-- Logically equivalent propositions under `Equiv.OfContainers f` have the same denotation in the +modal model induced by `Model.ofContainers f`. -/ @[scoped grind ⇒] -theorem Proposition.equivOfContainers_denotation_eq {α} [Membership α β] {r : α → α → Prop} - {φ₁ φ₂ : Proposition β} : - (φ₁ ≡[Equiv.OfContainers (β := β) r] φ₂) ↔ - φ₁.denotation (ofContainers r) = φ₂.denotation (ofContainers r) := +theorem Proposition.equivOfContainers_denotation_eq + [Membership α β] {f : Frame α τ} {φ₁ φ₂ : Proposition τ β} : + (φ₁ ≡[Equiv.OfContainers (β := β) f] φ₂) ↔ + φ₁.denotation (ofContainers f) = φ₂.denotation (ofContainers f) := equiv_iff_denotation_eq /-- 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 grind +the predicate model induced by `f`. -/ +@[scoped grind ., modal .] +theorem Proposition.equivOfPredicates_and + {f : Frame α τ} {P Q : α → Prop} : + (fun a => P a ∧ Q a) ≡[Equiv.OfPredicates f] (P ∧ Q) := by + grind -/-- Under `Equiv.OfContainers r`, if membership in the infimum of two containers is equivalent to +/-- Under `Equiv.OfContainers f`, 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 - -/-- 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)) +theorem Proposition.ofContainers_inf_equiv + [Membership α β] [Min β] (f : Frame α τ) (p q : β) + (h : ∀ x, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q) : + (↑(p ⊓ q) : Proposition τ β) ≡[Equiv.OfContainers f] (p ∧ q) := by + grind end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/LogicalEquivalence.lean b/Cslib/Logics/Modal/LogicalEquivalence.lean index afd4cd798..6d9529436 100644 --- a/Cslib/Logics/Modal/LogicalEquivalence.lean +++ b/Cslib/Logics/Modal/LogicalEquivalence.lean @@ -6,7 +6,7 @@ Authors: Fabrizio Montesi module -public import Cslib.Logics.Modal.Basic +public import Cslib.Logics.Modal.Semantics public import Cslib.Foundations.Logic.LogicalEquivalence /-! # Logical Equivalence in Modal Logic @@ -25,75 +25,95 @@ namespace Cslib.Logic.Modal open scoped InferenceSystem Proposition Satisfies /-- The modal propositions `φ₁` and `φ₂` are equivalent in the model `m`. -/ -def Proposition.Equiv (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : Prop := +def Proposition.Equiv (m : Model World τ Atom) (φ₁ φ₂ : Proposition τ Atom) : Prop := ∀ (w : World), ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] instance : Congruence (Proposition.Equiv m) := ⟨⟩ @[scoped grind =] -theorem Proposition.equiv_def (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) : +theorem Proposition.equiv_def (m : Model World τ Atom) (φ₁ φ₂ : Proposition τ Atom) : (φ₁.Equiv m φ₂) ↔ φ₁ ≡[Equiv m] φ₂ := by rfl -@[scoped grind ⇒] -theorem Proposition.equiv_iff_forall_der (m : Model World Atom) (φ₁ φ₂ : Proposition Atom) +@[scoped grind ⇒, modal ⇒] +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_forall_iff {m : Model World Atom} {φ₁ φ₂ : Proposition Atom} : +@[scoped grind ⇒, modal ⇒] +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. -/ -abbrev ModelClass World Atom := Set (Model World Atom) +abbrev ModelClass (World : Type*) (τ : PFunctor) (Atom : Type*) := Set (Model World τ Atom) /-- The modal propositions `φ₁` and `φ₂` are equivalent in the model class `S`. -/ -def Proposition.EquivWithin (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) := +def Proposition.EquivWithin (S : ModelClass World τ Atom) (φ₁ φ₂ : Proposition τ Atom) := ∀ m ∈ S, φ₁ ≡[Equiv m] φ₂ instance : Congruence (Proposition.EquivWithin S) := ⟨⟩ +/-- Universal logical equivalence: `φ₁` and `φ₂` are equivalent in the class of all models. -/ +abbrev Proposition.UEquiv {World : Type*} (φ₁ φ₂ : Proposition τ Atom) := + EquivWithin (World := World) Set.univ φ₁ φ₂ + @[scoped grind =] -theorem Proposition.equivWithin_def (S : ModelClass World Atom) (φ₁ φ₂ : Proposition Atom) : +theorem Proposition.equivWithin_def (S : ModelClass World τ Atom) (φ₁ φ₂ : Proposition τ Atom) : φ₁.EquivWithin S φ₂ ↔ (φ₁ ≡[EquivWithin S] φ₂) := by rfl +@[scoped grind ⇒, modal ⇒] +theorem Proposition.equivWithin_iff_forall_iff : + (φ₁ ≡[EquivWithin S] φ₂) ↔ ∀ m ∈ S, φ₁ ≡[Equiv m] φ₂ := 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.equiv_of_EquivWithin {S : ModelClass World τ Atom} (h : φ₁ ≡[EquivWithin S] φ₂) + (m : Model World τ Atom) (hm : m ∈ S) : φ₁ ≡[Equiv m] φ₂ := h m hm /-- Logical equivalence preserves validity. -/ -theorem Proposition.equivWithin_valid (S : ModelClass World Atom) - (φ₁ φ₂ : Proposition Atom) (h : φ₁ ≡[EquivWithin S] φ₂) : +theorem Proposition.equivWithin_valid (S : ModelClass World τ Atom) + (φ₁ φ₂ : Proposition τ Atom) (h : φ₁ ≡[EquivWithin S] φ₂) : (φ₁.valid S ↔ φ₂.valid S) := by grind +/-- A proposition map missing a particular case (index). -/ +abbrev PropositionMap.Without (τ : PFunctor) (Atom : Type*) (op : τ.A) (i : τ.B op) := + {j : τ.B op // j ≠ i} → Proposition τ Atom + /-- Propositional contexts. -/ -inductive Proposition.Context (Atom : Type u) : Type u where +inductive Proposition.Context (τ : PFunctor) (Atom : Type u) where | hole - | not (c : Context Atom) - | andL (c : Context Atom) (φ : Proposition Atom) - | andR (φ : Proposition Atom) (c : Context Atom) - | diamond (c : Context Atom) + | not (c : Context τ Atom) + | andL (c : Context τ Atom) (φ : Proposition τ Atom) + | andR (φ : Proposition τ Atom) (c : Context τ Atom) + | triangle (op : τ.A) (i : τ.B op) (c : Context τ Atom) + (φs : PropositionMap.Without τ Atom op i) /-- Replaces a hole in a propositional context with a proposition. -/ @[scoped grind =] -def Proposition.Context.fill (c : Context Atom) (φ : Proposition Atom) := +def Proposition.Context.fill {τ : PFunctor} [τ.DecidableEqChildren] {Atom : Type*} + (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 φ) + | .triangle op i c φs => .triangle op fun j => + if h : j = i then + c.fill φ + else + φs ⟨j, h⟩ -instance : HasContext (Proposition Atom) := ⟨Proposition.Context.fill⟩ +instance {τ : PFunctor} [τ.DecidableEqChildren] {Atom : Type*} : + HasContext (Proposition τ Atom) := ⟨Proposition.Context.fill⟩ @[scoped grind =] -lemma Proposition.Context.fill_def {c : HasContext.Context (Proposition Atom)} : - c.fill φ = c<[φ] := rfl +lemma Proposition.Context.fill_def {τ : PFunctor} [τ.DecidableEqChildren] {Atom : Type*} + {c : HasContext.Context (Proposition τ Atom)} {φ : Proposition τ Atom} : + c.fill φ = c<[φ] := rfl open scoped Proposition Proposition.Context /-- Logical equivalence is an equivalence relation. -/ -instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv m) := by +instance (m : Model World τ Atom) : IsEquiv (Proposition τ Atom) (Proposition.Equiv m) := by rw [← equivalence_iff_isEquiv] constructor case refl => grind [Proposition.Equiv] @@ -103,8 +123,8 @@ instance (m : Model World Atom) : IsEquiv (Proposition Atom) (Proposition.Equiv grind /-- Logical equivalence within a class is an equivalence relation. -/ -instance {World Atom} (S : ModelClass World Atom) : - IsEquiv (Proposition Atom) (Proposition.EquivWithin S) := by +instance {World Atom} (S : ModelClass World τ Atom) : + IsEquiv (Proposition τ Atom) (Proposition.EquivWithin S) := by rw [← equivalence_iff_isEquiv] unfold Proposition.EquivWithin constructor @@ -116,84 +136,88 @@ instance {World Atom} (S : ModelClass World Atom) : grind /-- Logical equivalence is a congruence. -/ -instance (m : Model World Atom) : LawfulCongruence (Proposition.Equiv m) where +instance {τ : PFunctor} [τ.DecidableEqChildren] {Atom : Type*} (m : Model World τ Atom) : + LawfulCongruence (Proposition.Equiv m) where elim ctx φ₁ φ₂ heqv w := by induction ctx generalizing w case hole => apply heqv case not c ih | andL c ih | andR c ih => specialize ih w grind [=_ Proposition.Context.fill_def] - case diamond c ih => + case triangle op i c φs ih => rw [Satisfies.iff_iff_iff] - apply Iff.intro + constructor all_goals - rintro ⟨w', h⟩ - specialize ih w' - grind [=_ Proposition.Context.fill_def] + intro h + obtain ⟨ws, hr, hs⟩ := h + refine ⟨ws, hr, ?_⟩ + intro j + by_cases j = i + · subst j + specialize ih (ws i) + grind + · grind /-- Logical equivalence within a class is a congruence. -/ -instance (S : ModelClass World Atom) : - LawfulCongruence (Proposition.EquivWithin S) where +instance {τ : PFunctor} [τ.DecidableEqChildren] {Atom : Type*} + (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 +structure Judgement.Context (World : Type*) (τ : PFunctor) (Atom : Type*) where /-- The model to consider. -/ - m : Model World Atom + m : Model World τ Atom /-- The world to check propositions against. -/ w : World /-- Fills a judgemental context with a proposition. -/ -def Satisfies.Context.fill (c : Satisfies.Context World Atom) (φ : Proposition Atom) : - Judgement World Atom := Modal[c.m, c.w ⊨ φ] +def Judgement.Context.fill (c : Judgement.Context World τ Atom) (φ : Proposition τ Atom) : + Judgement World τ Atom := Modal[c.m, c.w ⊨ φ] -instance : HasHContext (Judgement World Atom) (Proposition Atom) := ⟨Satisfies.Context.fill⟩ +instance {World : Type*} {τ : PFunctor} {Atom : Type*} : + HasHContext (Judgement World τ Atom) (Proposition τ Atom) := ⟨Judgement.Context.fill⟩ @[scoped grind =] -lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} : +lemma Judgement.Context.fill_def {c : Judgement.Context World τ Atom} {φ : Proposition τ Atom} : Modal[c.m,c.w ⊨ φ] = c<[φ] := rfl -open scoped Satisfies.Context +open scoped Judgement.Context /-- 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.EquivWithin (Set.univ (α := Model World Atom))) where +instance {τ : PFunctor} [τ.DecidableEqChildren] : LogicalEquivalence + (α := Proposition τ Atom) + (Judgement := Judgement World τ Atom) InferenceSystem.Default + (Proposition.EquivWithin (Set.univ (α := Model World τ Atom))) where eqvFillValid heqv c h := by specialize heqv c.m - grind [=_ Satisfies.Context.fill_def] + grind [=_ Judgement.Context.fill_def] -/-- Correspondence of equivalence and axiom validity. -/ -theorem Proposition.axiom_iff_forall_equiv (r : α → α → Prop) (φ₁ φ₂ : Proposition Atom) : - (Axiom r⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨r, v⟩] φ₂ := Iff.rfl +section Axiom -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 - rw [equiv_iff_forall_iff] - intro a - constructor - case mp => grind - case mpr => - 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⟩ - -/-- 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 - constructor <;> rw [← Satisfies.imp_iff_imp] - · grind [Satisfies.four] - · grind [Satisfies.t] +/-- Correspondence of equivalence and axiom validity. -/ +@[scoped grind =, modal =] +theorem Proposition.axiom_iff_forall_equiv (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + (Axiom f⇓(φ₁ ↔ φ₂)) ↔ ∀ v, φ₁ ≡[Equiv ⟨f, v⟩] φ₂ := Iff.rfl + +/-- A frame-valid bi-implication induces logical equivalence in every model over that frame. -/ +@[scoped grind ., modal .] +theorem Proposition.equiv_of_axiom {f : Frame World τ} {φ₁ φ₂ : Proposition τ Atom} + (h : Axiom f⇓(φ₁ ↔ φ₂)) (v : World → Atom → Prop) : φ₁ ≡[Equiv ⟨f, v⟩] φ₂ := + (Proposition.axiom_iff_forall_equiv f φ₁ φ₂).mp h v + +/-- A bi-implication is an axiom of `f` iff its sides are equivalent in every model over `f`. -/ +@[scoped grind =, modal =] +theorem Proposition.axiom_iff_equivWithin_modelsOfFrame + (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + Axiom f⇓(φ₁ ↔ φ₂) ↔ φ₁ ≡[EquivWithin (modelsOfFrame f)] φ₂ := by grind + +/-- Triangle and the negation of the dual nabla are universally logically equivalent. -/ +theorem Proposition.dual_equiv (φs : PropositionMap τ op Atom) : + Δ[op]φs ≡[UEquiv (World := World)] ¬∇[op]¬φs := by + -- We use `grind only` as a test that `modal` can lift axioms to logical equivalences + grind only [modal, Satisfies.dual] + +end Axiom end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Semantics.lean b/Cslib/Logics/Modal/Semantics.lean new file mode 100644 index 000000000..f08310c11 --- /dev/null +++ b/Cslib/Logics/Modal/Semantics.lean @@ -0,0 +1,357 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi, Marianna Girlando +-/ + +module + +public import Cslib.Logics.Modal.Basic +public import Cslib.Foundations.Semantics.Frame.Basic + +/-! # Semantics of Modal Logic -/ + +@[expose] public section + +namespace Cslib.Logic.Modal + +/-- A model is a frame equipped with a valuation of atoms at worlds. -/ +structure Model World (τ : PFunctor) Atom extends Frame World τ where + /-- Valuation of atoms at a world. -/ + v : World → Atom → Prop + +/-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies +the proposition `φ`. -/ +def Satisfies (m : Model World τ Atom) (w : World) : Proposition τ Atom → Prop + | .atom p => m.v w p + | .false => False + | .not φ => ¬Satisfies m w φ + | .or φ₁ φ₂ => Satisfies m w φ₁ ∨ Satisfies m w φ₂ + | .triangle op φs => ∃ ws : τ.B op → World, m.r op w ws ∧ ∀ i, Satisfies m (ws i) (φs i) + +/-- Judgement, representing the conclusions one reaches in modal logic. -/ +structure Judgement World τ Atom where + /-- Constructs a judgement. -/ + mk :: + /-- Model. -/ + m : Model World τ Atom + /-- The world satisfying the proposition `φ`. -/ + w : World + /-- The proposition satisfied by the world `w`. -/ + φ : Proposition τ Atom + +@[inherit_doc] scoped notation "Modal[" m "," w " ⊨ " φ "]" => Judgement.mk m w φ + +/-- Satisfaction for judgements. This just refers to the unbundled `Satisfies`. -/ +def Satisfies.Bundled (j : Judgement World τ Atom) : Prop := Satisfies j.m j.w j.φ + +instance {World : Type*} {τ : PFunctor} {Atom : Type*} : + HasInferenceSystem (Judgement World τ Atom) := ⟨Satisfies.Bundled⟩ + +open scoped InferenceSystem Proposition PropositionMap Frame PFunctor + +@[scoped grind =] +theorem derivation_def {m : Model World τ Atom} {w : World} {φ : Proposition τ Atom} : + Satisfies m w φ = ⇓Modal[m,w ⊨ φ] := rfl + +@[simp, scoped grind =, modal =] +theorem Satisfies.atom_iff {a : Atom} : ⇓Modal[m,w ⊨ a] ↔ m.v w a := by rfl + +@[simp, scoped grind =, modal =] +theorem Satisfies.false : ⇓Modal[m,w ⊨ ⊥] ↔ False := by rfl + +/-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/ +@[scoped grind =, modal =] +theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl + +@[simp, scoped grind ., modal .] +theorem Satisfies.true : ⇓Modal[m,w ⊨ ⊤] := by + grind [=_ Proposition.true_def, Proposition.true] + +@[scoped grind =, modal =] +theorem Satisfies.or_iff_or {m : Model World τ Atom} : + ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by rfl + +@[scoped grind =] +theorem Satisfies.triangle_iff_exists {m : Model World τ Atom} : + ⇓Modal[m,w ⊨ Δ[op]φs] ↔ ∃ ws, m.r op w ws ∧ ∀ i, ⇓Modal[m,(ws i) ⊨ (φs i)] := by rfl + +@[scoped grind =] +theorem Satisfies.triangle_not_iff_exists_not {φs : τ.B op → Proposition τ Atom} + {m : Model World τ Atom} : ⇓Modal[m,w ⊨ Δ[op]¬φs] ↔ + ∃ ws, m.r op w ws ∧ ∀ i, ¬⇓Modal[m,(ws i) ⊨ (φs i)] := by + have : (¬φs) = (fun i => ¬(φs i)) := rfl + grind + +/-- Characterisation of the `∧` connective. + +Conjunction is defined in terms of the more primitive connectives given in `Proposition`. +This result proves that the definition is correct. -/ +@[scoped grind =, modal =] +theorem Satisfies.and_iff_and {m : Model World τ Atom} : + ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by + grind [=_ Proposition.and_def, Proposition.and] + +/-- Characterisation of the `→` connective. + +Implication is defined in terms of the more primitive connectives given in `Proposition`. +This result proves that the definition is correct. +-/ +@[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] + +/-- Characterisation of the `↔` connective. + +Bi-implication is defined in terms of the more primitive connectives given in `Proposition`. +This result proves that the definition is correct. -/ +@[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] + grind + +/-- Characterisation of `∇`. + +Necessity is defined in terms of the more primitive connectives given in `Proposition`. +This result proves that the definition is correct. -/ +@[scoped grind =] +theorem Satisfies.nabla_iff_forall {m : Model World τ Atom} : + ⇓Modal[m,w ⊨ ∇[op]φs] ↔ ∀ ws, m.r op w ws → ∃ i, ⇓Modal[m,(ws i) ⊨ (φs i)] := by + grind [=_ Proposition.nabla_def, Proposition.nabla] + +/-- The theory of a world in a model is the set of all propositions that it satisfies. -/ +abbrev theory {World : Type*} {τ : PFunctor} {Atom : Type*} (m : Model World τ Atom) + (w : World) : Set (Proposition τ Atom) := {φ | ⇓Modal[m,w ⊨ φ]} + +/-- Two worlds are theory-equivalent under a model if they have the same theory. -/ +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 + +/-- Any proposition satisfied by a world is in the theory of that world. -/ +@[scoped 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₂) : + ∃ φ, (⇓Modal[m,w₁ ⊨ φ] ∧ ¬⇓Modal[m,w₂ ⊨ φ]) := by grind [=_ Satisfies.not_iff_not] + +/-- If two worlds are theory equivalent and the former satisfies a proposition, the latter does as +well. -/ +theorem theoryEq_satisfies {m : Model World τ Atom} (h : TheoryEq m w₁ w₂) + (hs : Satisfies m w₁ φ) : ⇓Modal[m,w₂ ⊨ φ] := by + apply TheoryEq.ext_iff.1 at h + exact (h φ).mp hs + +/-- Every frame induces an inference system tag for proving valid axioms under the frame. -/ +inductive Axiom (f : Frame World τ) + +/-- A proposition `φ` is an axiom under a frame `f` if it holds for all valuations and worlds. -/ +instance {World : Type*} {τ : PFunctor} {Atom : Type*} (f : Frame World τ) : + InferenceSystem (Axiom f) (Proposition τ Atom) where + derivation φ := ∀ v w, ⇓Modal[⟨f,v⟩,w ⊨ φ] + +@[scoped grind ⇒] +theorem Satisfies.axiom_def (f : Frame World τ) : + (∀ v w, ⇓Modal[⟨f,v⟩,w ⊨ φ]) ↔ Axiom f⇓φ := by rfl + +@[modal .] +theorem Satisfies.der_of_axiom (h : Axiom m.toFrame⇓φ) : ⇓Modal[m,w ⊨ φ] := h m.v w + +/-- If a proposition is an axiom under the frame of a model, it is satisfied by every world. -/ +@[scoped grind ., modal .] +theorem Satisfies.of_axiom (m : Model World τ Atom) (φ : Proposition τ Atom) (h : Axiom m.toFrame⇓φ) + (w : World) : ⇓Modal[m,w ⊨ φ] := h m.v w + +@[scoped grind =] +theorem Satisfies.subst_apply_iff [DecidableEq (τ.B op)] {φs : PropositionMap τ op Atom} + {i j : τ.B op} {φ : Proposition τ Atom} : ⇓Modal[m,w ⊨ φs[i := φ] j] ↔ + (j = i ∧ ⇓Modal[m,w ⊨ φ]) ∨ (j ≠ i ∧ ⇓Modal[m,w ⊨ φs j]) := + Function.pred_update (P := fun _ φ' => Satisfies m w φ') φs i φ j + +/-- Axiom K, valid for all frames. -/ +@[scoped grind ., modal .] +theorem Satisfies.k (f : Frame World τ) {φs : PropositionMap τ op Atom} [DecidableEq (τ.B op)] + {i : τ.B op} {φ₁ φ₂ : Proposition τ Atom} (hi : φs i = (φ₁ → φ₂)) : + Axiom f⇓(∇[op]φs → (∇[op]φs[i := φ₁] → ∇[op]φs[i := φ₂])) := by grind + +/-- The dual axiom, valid for all frames. -/ +theorem Satisfies.dual (f : Frame World τ) {φs : PropositionMap τ op Atom} : + Axiom f⇓(Δ[op]φs ↔ ¬∇[op]¬φs) := by grind + +/-- Possibility preserves conjunction. -/ +@[scoped grind ., modal .] +theorem Satisfies.triangle_and (f : Frame World τ) (φs₁ φs₂ : PropositionMap τ op Atom) : + Axiom f⇓(Δ[op](φs₁ ∧ φs₂) → (Δ[op]φs₁ ∧ Δ[op]φs₂)) := by grind + +/-- Possibility can be combined with necessity. -/ +@[modal .] +theorem Satisfies.triangle_and_nabla {m : Model World τ Atom} [DecidableEq (τ.B op)] + (h : ⇓Modal[m,w ⊨ Δ[op]φs₁ ∧ ∇[op]φs₂]) : ∃ i, ⇓Modal[m,w ⊨ Δ[op]φs₁[i := φs₁ i ∧ φs₂ i]] := by + grind + +/-- If `φ₁` is necessary and some successor exists, then some successor satisfies `φ₁`. -/ +@[scoped grind ., modal .] +theorem Satisfies.triangle_of_nabla {φs₁ φs₂ : PropositionMap τ op Atom} + [DecidableEq (τ.B op)] (h : ⇓Modal[m,w ⊨ ∇[op]φs₁ ∧ Δ[op]φs₂]) : + ∃ i, ⇓Modal[m,w ⊨ Δ[op]φs₂[i := φs₁ i]] := by grind + +@[scoped grind .] +theorem Satisfies.triangle_of_diagonal {m : Model World τ Atom} {op : τ.A} {w : World} + {φ : Proposition τ Atom} [instRefl : Std.Refl (m.toFrame.diagonal op)] + (h : ⇓Modal[m,w ⊨ φ]) : ⇓Modal[m,w ⊨ Δ[op](PropositionMap.const op φ)] := + ⟨fun _ => w, instRefl.refl w, by grind⟩ + +/-- Axiom T. -/ +theorem Satisfies.t (f : Frame World τ) [instRefl : Std.Refl (f.diagonal op)] + (φ : Proposition τ Atom) : Axiom f⇓(φ → Δ[op](PropositionMap.const op φ)) := by grind + +/-- Any frame admitting T for `op` has a reflexive diagonal relation. -/ +theorem Satisfies.t_refl (f : Frame World τ) {op : τ.A} [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(φ → Δ[op](PropositionMap.const op φ))) : + Std.Refl (f.diagonal op) where + refl w := by + have a := Classical.arbitrary Atom + let v := fun (w' : World) (_ : Atom) => w' = w + have h' := h (v := v) (w := w) (φ := a) + rw [Satisfies.imp_iff_imp] at h' + specialize h' rfl + obtain ⟨ws, hr, _⟩ := h' + have hws : ws = fun _ => w := by grind + grind [Frame.diagonal] + +/-- In any model whose diagonal relation for `op` is reflexive, `∇[op]φ → φ` is equivalent to +`φ → Δ[op]φ`. -/ +theorem Satisfies.t_nabla_triangle (f : Frame World τ) [Std.Refl (f.diagonal op)] : + Axiom f⇓((∇[op](PropositionMap.const op φ) → φ) ↔ (φ → Δ[op](PropositionMap.const op φ))) := by + intro _ w + have hr : f.r op w (fun _ => w) := by + simpa [Frame.diagonal] using (Std.Refl.refl (r := f.diagonal op) w) + grind + +/-- Axiom B, valid for diagonally symmetric frames. -/ +theorem Satisfies.b (f : Frame World τ) [f.DiagonalSymm op] (φ : Proposition τ Atom) : + Axiom f⇓(φ → ∇[op](PropositionMap.const op (Δ[op](PropositionMap.const op φ)))) := by + intro _ w + have := Frame.DiagonalSymm.symm (f := f) (op := op) + grind + +/-- Any frame that admits B at `op` is diagonally symmetric at `op`. -/ +theorem Satisfies.b_symm (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, + Axiom f⇓(φ → ∇[op](PropositionMap.const op (Δ[op](PropositionMap.const op φ))))) : + f.DiagonalSymm op where + symm w ws hwws := by + have a := Classical.arbitrary Atom + let v := fun (w' : World) (_ : Atom) => w' = w + let h' := h (v := v) (w := w) (φ := a) + rw [Satisfies.imp_iff_imp] at h' + specialize h' (by grind) + rw [Satisfies.nabla_iff_forall] at h' + obtain ⟨i, ws', _⟩ := h' ws hwws + have : ws' = fun _ => w := by grind + grind + +/-- The 4 axiom, valid for transitive frames. -/ +theorem Satisfies.four (f : Frame World τ) [f.Trans op] + (φs ψs : PropositionMap τ op Atom) (i : τ.B op) + (hi : φs i = (Δ[op]ψs)) : + Axiom f⇓(Δ[op]φs → Δ[op]ψs) := by + have ht := Frame.Trans.trans (f := f) (op := op) (i := i) + grind only [modal, =_ axiom_def, = triangle_iff_exists] + +/-- Any frame that admits 4 at `op` is transitive at `op`. -/ +theorem Satisfies.four_trans (f : Frame World τ) [Nonempty Atom] + (e : τ.B op ↪ Atom) (h : ∀ (φs ψs : PropositionMap τ op Atom) (i : τ.B op), + φs i = (Δ[op]ψs) → Axiom f⇓(Δ[op]φs → Δ[op]ψs)) : f.Trans op where + trans w ws i ws' h₁ h₂ := by + classical + let a := Classical.arbitrary Atom + -- Each coordinate gets its own atom. + let ψs : PropositionMap τ op Atom := fun j => e j + -- A tautology for the irrelevant coordinates of the outer triangle. + let top : Proposition τ Atom := a → a + let φs : PropositionMap τ op Atom := + fun j => if j = i then Δ[op]ψs else top + -- Atom `e j` holds exactly at `ws' j`. + let v : World → Atom → Prop := + fun x p => ∃ j, p = e j ∧ x = ws' j + have hi : φs i = (Δ[op]ψs) := by grind only + have h' := h φs ψs i hi (v := v) (w := w) + have hφs : ⇓Modal[⟨f, v⟩,w ⊨ Δ[op]φs] := by + rw [Satisfies.triangle_iff_exists] + refine ⟨ws, h₁, ?_⟩ + grind only [modal, of_axiom, axiom_def, = triangle_iff_exists] + rw [Satisfies.imp_iff_imp] at h' + specialize h' hφs + rw [Satisfies.triangle_iff_exists] at h' + obtain ⟨xs, hr, hs⟩ := h' + have hxs : xs = ws' := by grind + grind only + +/-- Axiom 5, valid for right-Euclidean frames. -/ +theorem Satisfies.five (f : Frame World τ) [f.RightEuclidean op] + (φs : PropositionMap τ op Atom) : + Axiom f⇓(Δ[op]φs → ∇[op](PropositionMap.const op (Δ[op]φs))) := by + have he := Frame.RightEuclidean.rightEuclidean (f := f) (op := op) + grind + +/-- Any frame that admits 5 at `op` is right-Euclidean at `op`. -/ +theorem Satisfies.five_rightEuclidean (f : Frame World τ) (e : τ.B op ↪ Atom) + (h : ∀ φs : PropositionMap τ op Atom, + Axiom f⇓(Δ[op]φs → ∇[op](PropositionMap.const op (Δ[op]φs)))) : f.RightEuclidean op where + rightEuclidean {w ws₁ ws₂} h₁ h₂ := by + let φs : PropositionMap τ op Atom := fun i => e i + let v : World → Atom → Prop := + fun w' a => ∃ i, a = e i ∧ w' = ws₁ i + have h' := h φs (v := v) (w := w) + have hφs : ⇓Modal[⟨f,v⟩,w ⊨ Δ[op]φs] := by grind + rw [Satisfies.imp_iff_imp] at h' + specialize h' hφs + rw [Satisfies.nabla_iff_forall] at h' + obtain ⟨i, hi⟩ := h' ws₂ h₂ + obtain ⟨ws', hr, hs⟩ := hi + have hws : ws' = ws₁ := by + funext j + have hj := hs j + simp only [φs] at hj + rcases hj with ⟨k, hk, hw⟩ + have hjk : j = k := e.injective hk + simpa [hjk] using hw + grind only + +/-- 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 =] +def Proposition.valid {World : Type*} {τ : PFunctor} {Atom : Type*} (S : Set (Model World τ Atom)) + (φ : Proposition τ Atom) : Prop := ∀ m ∈ S, ∀ (w : World), ⇓Modal[m,w ⊨ φ] + +/-- The modal logic of a class of models `S` is the set of all propositions valid in `S`. -/ +@[simp, scoped grind =] +def logic {World : Type*} {τ : PFunctor} {Atom : Type*} (S : Set (Model World τ Atom)) : + Set (Proposition τ Atom) := {φ | φ.valid S} + +/-- Modal logic is antitone (wrt the class of models). -/ +theorem logic_antitone {World : Type*} {τ : PFunctor} {Atom : Type*} : + 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 modelsOfFrame {World : Type*} {τ : PFunctor} {Atom : Type*} (f : Frame World τ) : + Set (Model World τ Atom) := {m | m.toFrame = f} + +/-- 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_modelsOfFrame (f : Frame World τ) (φ : Proposition τ Atom) : + Axiom f⇓φ ↔ φ ∈ logic (modelsOfFrame f) := by + constructor + case mp => + rintro h m rfl w + exact h m.v w + case mpr => grind [Satisfies.axiom_def] + +end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Unary/Basic.lean b/Cslib/Logics/Modal/Unary/Basic.lean new file mode 100644 index 000000000..854e2b903 --- /dev/null +++ b/Cslib/Logics/Modal/Unary/Basic.lean @@ -0,0 +1,53 @@ +/- +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.Foundations.Data.PFunctor.Basic +public import Cslib.Logics.Modal.Basic +public import Cslib.Logics.Modal.Semantics +public import Cslib.Logics.Modal.LogicalEquivalence + +/-! # Unary Modal Logic -/ + +@[expose] public section + +namespace Cslib.Logic.Modal + +open PFunctor +open scoped InferenceSystem Proposition Satisfies Frame + +variable {τ : PFunctor} [τ.Unary] + +/-- Context constructor for the dynamic diamond modality. -/ +@[match_pattern] +def Proposition.Context.dynDiamond (c : Context τ Atom) (a : τ.A) : Context τ Atom := + .triangle a default c fun ⟨i, hi⟩ => (hi (Subsingleton.elim i default)).elim + +@[scoped grind =] +theorem Proposition.unary_triangle_eq_dynDiamond {a : τ.A} + (φs : PropositionMap τ a Atom) : (Δ[a]φs) = d⟨a⟩(φs default) := by + rw [PFunctor.Unary.fun_eq_const a φs] + rfl + +@[modal =] +theorem Satisfies.dynDiamond_iff_exists {m : Model World τ Atom} + {φ : Proposition τ Atom} : ⇓Modal[m,w ⊨ d⟨a⟩φ] ↔ + ∃ w', m.toFrame.diagonal a w w' ∧ ⇓Modal[m,w' ⊨ φ] := by grind + +@[modal =] +theorem Satisfies.dynBox_iff_forall {m : Model World τ Atom} {φ : Proposition τ Atom} : + ⇓Modal[m,w ⊨ d[a]φ] ↔ ∀ w', m.toFrame.diagonal a w w' → ⇓Modal[m,w' ⊨ φ] := by grind + +omit [τ.Unary] in +/-- The dual axiom (reformulated for unary modal logic). -/ +theorem Satisfies.unary_dual (f : Frame World τ) {a : τ.A} {φ : Proposition τ Atom} : + Axiom f⇓(d⟨a⟩φ ↔ ¬d[a]¬φ) := by + /- We use `grind only` on purpose here because this axiom should be derivable from the more + more general `Satisfies.dual`. -/ + grind only [modal, Satisfies.dual] + +end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Unary/LTS.lean b/Cslib/Logics/Modal/Unary/LTS.lean new file mode 100644 index 000000000..1ba849611 --- /dev/null +++ b/Cslib/Logics/Modal/Unary/LTS.lean @@ -0,0 +1,61 @@ +/- +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.Foundations.Data.PFunctor.Basic +public import Cslib.Logics.Modal.Semantics +public import Cslib.Logics.Modal.Unary.Basic +public import Cslib.Foundations.Semantics.LTS.Basic +public import Cslib.Foundations.Semantics.Frame.LTS + +/-! # Unary Modal Logic -/ + +@[expose] public section + +namespace Cslib.Logic.Modal + +open PFunctor + +/-- Constructs a unary model from an `LTS` and a valuation `v`. -/ +def Model.ofLTS (lts : LTS State Label) (v : State → Atom → Prop) : + Model State (mkUnary Label) Atom where + toFrame := lts.toFrame + v := v + +@[simp, scoped grind =, modal =] +theorem Model.ofLTS_toFrame (lts : LTS State Label) (v : State → Atom → Prop) : + (ofLTS lts v).toFrame = lts.toFrame := by + rfl + +open Model +open scoped InferenceSystem + +variable {lts : LTS State Label} {v : State → Atom → Prop} + +@[scoped grind =, modal =] +theorem Satisfies.ofLTS_atom_iff {p : Atom} : ⇓Modal[ofLTS lts v,s ⊨ p] ↔ v s p := by rfl + +theorem Satisfies.ofLTS_dynDiamond_iff_exists : + ⇓Modal[ofLTS lts v,s ⊨ d⟨μ⟩φ] ↔ ∃ s', lts.Tr s μ s' ∧ ⇓Modal[ofLTS lts v,s' ⊨ φ] := by + rw [Satisfies.dynDiamond_iff_exists] + simp [ofLTS] + +theorem Satisfies.ofLTS_dynBox_iff_forall : + ⇓Modal[ofLTS lts v,s ⊨ d[μ]φ] ↔ ∀ s', lts.Tr s μ s' → ⇓Modal[ofLTS lts v,s' ⊨ φ] := by + rw [Satisfies.dynBox_iff_forall] + simp [ofLTS] + +@[modal ⇒] +theorem Satisfies.ofLTS_dynDiamond_intro (htr : lts.Tr s μ s') + (h : ⇓Modal[ofLTS lts v,s' ⊨ φ]) : ⇓Modal[ofLTS lts v,s ⊨ d⟨μ⟩φ] := by + grind [modal] + +@[modal ⇒] +theorem Satisfies.ofLTS_dynBox_elim (hbox : ⇓Modal[ofLTS lts v,s ⊨ d[μ]φ]) + (htr : lts.Tr s μ s') : ⇓Modal[ofLTS lts v,s' ⊨ φ] := by grind [modal] + +end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Unimodal/Basic.lean b/Cslib/Logics/Modal/Unimodal/Basic.lean new file mode 100644 index 000000000..7bcc12d05 --- /dev/null +++ b/Cslib/Logics/Modal/Unimodal/Basic.lean @@ -0,0 +1,324 @@ +/- +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Fabrizio Montesi, Marianna Girlando +-/ + +module + +public import Cslib.Logics.Modal.Unary.Basic +public import Cslib.Logics.Modal.LogicalEquivalence + +/-! # Basic Modal Logic + +Basic modal logic is the modal logic with a single unary modality. + +## References + +* [P. Blackburn, M. de Rijke, Y. Venema, *Modal Logic*][Blackburn2001] +-/ + +@[expose] public section + +namespace Cslib + +section Unimodal + +open PFunctor + +variable {τ : PFunctor} [Unary τ] [Unique τ.A] + +namespace Frame + +/-- The accessibility relation of a unimodal frame. -/ +@[instance_reducible] +def rel (f : Frame World τ) : World → World → Prop := f.diagonal default + +omit [Unary τ] in +@[scoped grind =, modal =] +theorem rel_iff_diagonal (f : Frame World τ) (w w' : World) : + f.rel w w' ↔ f.diagonal default w w' := by rfl + +/-- Builds a unimodal frame out of a binary relation. -/ +@[instance_reducible] +def ofRelation (r : World → World → Prop) : Frame World τ where + r := fun _ w ws => r w (ws default) + +@[simp, scoped grind =, modal =] +theorem ofRelation_rel (r : World → World → Prop) : Frame.rel (Frame.ofRelation (τ := τ) r) = r := + rfl + +instance {r : World → World → Prop} [Std.Refl r] : Std.Refl (ofRelation (τ := τ) r).rel := by + infer_instance + +instance {r : World → World → Prop} [Std.Symm r] : Std.Symm (ofRelation (τ := τ) r).rel := by + infer_instance + +instance {r : World → World → Prop} [IsTrans World r] : + IsTrans World (Frame.ofRelation (τ := τ) r).rel := by + change IsTrans World r + infer_instance + +@[scoped grind =, modal =] +theorem ofRelation_rel_iff (r : World → World → Prop) (w w' : World) : + (ofRelation (τ := τ) r).rel w w' ↔ r w w' := by rfl + +@[scoped grind ., modal .] +theorem ofRelation_rel_of {r : World → World → Prop} {w w' : World} + (h : r w w') : (ofRelation (τ := τ) r).rel w w' := by grind + +open Relation in +@[scoped grind =, modal =] +theorem preservesMap_const_iff_preserves {r : α → α → Prop} {P : α → Prop} : + (ofRelation (τ := τ) r).PreservesMap default P (fun _ => P) ↔ Preserves r P := by + constructor + · intro h a₁ a₂ hr hP + obtain ⟨i, hi⟩ := h a₁ (fun _ => a₂) hr hP + exact hi + · intro h a₁ ws hr hP + refine ⟨default, ?_⟩ + exact h hr hP + +end Frame + +namespace Logic.Modal + +open scoped InferenceSystem Satisfies Proposition Proposition.Context Frame + +@[scoped grind =] +theorem Satisfies.diamond_iff_exists {m : Model World τ Atom} {φ : Proposition τ Atom} : + ⇓Modal[m,w ⊨ ◇φ] ↔ ∃ w', m.rel w w' ∧ ⇓Modal[m,w' ⊨ φ] := by + grind [diamond_eq_dynDiamond (φ := φ)] + +@[scoped grind →, modal →] +theorem Satisfies.diamond_of {m : Model World τ Atom} {φ : Proposition τ Atom} + (hr : m.toFrame.rel w w') (hφ : ⇓Modal[m,w' ⊨ φ]) : ⇓Modal[m,w ⊨ ◇φ] := + Satisfies.diamond_iff_exists.mpr ⟨w', hr, hφ⟩ + +@[scoped grind =] +theorem Satisfies.box_iff_forall {m : Model World τ Atom} {φ : Proposition τ Atom} : + ⇓Modal[m,w ⊨ □φ] ↔ ∀ w', m.rel w w' → ⇓Modal[m,w' ⊨ φ] := + Satisfies.dynBox_iff_forall + +/-- Axiom K for unimodal logic. -/ +@[scoped grind ., modal .] +theorem Satisfies.unimodal_k (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + Axiom f⇓(□(φ₁ → φ₂) → (□φ₁ → □φ₂)) := by grind + +/-- The dual axiom for unimodal logic. -/ +theorem Satisfies.unimodal_dual (f : Frame World τ) (φ : Proposition τ Atom) : + Axiom f⇓(◇φ ↔ ¬□¬φ) := by grind + +@[scoped grind ., modal .] +theorem Satisfies.diamond_and (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + Axiom f⇓(◇(φ₁ ∧ φ₂) → (◇φ₁ ∧ ◇φ₂)) := by grind + +@[modal .] +theorem Satisfies.diamond_and_box (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + Axiom f⇓((◇φ₁ ∧ □φ₂) → ◇(φ₁ ∧ φ₂)) := by grind + +@[scoped grind ., modal .] +theorem Satisfies.diamond_of_box (f : Frame World τ) (φ₁ φ₂ : Proposition τ Atom) : + Axiom f⇓(□φ₁ ∧ ◇φ₂ → ◇φ₁) := by grind + +/-- Axiom T. -/ +theorem Satisfies.unimodal_t (f : Frame World τ) [instRefl : Std.Refl f.rel] + (φ : Proposition τ Atom) : Axiom f⇓(φ → ◇φ) := by grind [instRefl.refl] + +/-- Any frame that admits T is reflexive. -/ +theorem Satisfies.unimodal_t_refl (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(φ → ◇φ)) : Std.Refl f.rel 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 + +/-- In any reflexive model, `□φ → φ` is equivalent to `φ → ◇φ`. -/ +theorem Satisfies.t_box_diamond {m : Model World τ Atom} [Std.Refl m.rel] : + ⇓Modal[m,w ⊨ □φ → φ] ↔ ⇓Modal[m,w ⊨ φ → ◇φ] := by + have := Std.Refl.refl (r := m.rel) w + grind + +/-- Axiom B. -/ +theorem Satisfies.unimodal_b (f : Frame World τ) [Std.Symm f.rel] + (φ : Proposition τ Atom) : Axiom f⇓(φ → □◇φ) := by + intro _ w + have := Std.Symm.symm (r := f.rel) w + grind + +/-- Any frame that admits B is symmetric. -/ +theorem Satisfies.unimodal_b_symm (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(φ → □◇φ)) : Std.Symm f.rel 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) + grind + +/-- Axiom 4, valid for all transitive frames. -/ +theorem Satisfies.unimodal_four (f : Frame World τ) [IsTrans World f.rel] + (φ : Proposition τ Atom) : Axiom f⇓(◇◇φ → ◇φ) := by + intro _ _ + simp only [Satisfies.imp_iff_imp, Satisfies.diamond_iff_exists] + rintro ⟨w', h₁, w'', h₂, hs⟩ + exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩ + +/-- Any frame that admits 4 is transitive. -/ +theorem Satisfies.unimodal_four_trans (f : Frame World τ) [Nonempty Atom] + (h : ∀ (φ : Proposition τ Atom), Axiom f⇓(◇◇φ → ◇φ)) : IsTrans World f.rel 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 + +/-- Axiom 5. -/ +theorem Satisfies.unimodal_five (f : Frame World τ) [Relation.RightEuclidean f.rel] + (φ : Proposition τ Atom) : Axiom f⇓(◇φ → □◇φ) := by + have := @Relation.RightEuclidean.rightEuclidean (r := f.rel) + grind + +/-- Any frame that admits 5 is Euclidean. -/ +theorem Satisfies.unimodal_five_rightEuclidean (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(◇φ → □◇φ)) : + Relation.RightEuclidean f.rel 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 + +/-- Axiom D, valid for all serial frames. -/ +theorem Satisfies.d (f : Frame World τ) [Relation.Serial f.rel] + (φ : Proposition τ Atom) : Axiom f⇓(□φ → ◇φ) := by + intro _ w + have : ∃ w', f.rel w w' := Relation.Serial.serial w + grind + +/-- Any model that admits D is serial. -/ +theorem Satisfies.d_serial (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(□φ → ◇φ)) : Relation.Serial f.rel 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₁) (φ := a) + grind + +/-- The L axiom, or Löb's theorem, valid for all transitive and converse well-founded models. -/ +theorem Satisfies.l (f : Frame World τ) [IsTrans World f.rel] + (hwf : Relation.Terminating f.rel) (φ : Proposition τ Atom) : + Axiom f⇓(□(□φ → φ) → □φ) := by + intro v w + let m : Model World τ Atom := ⟨f, v⟩ + simp_rw [Satisfies.imp_iff_imp, Satisfies.box_iff_forall] + intro h + refine (hwf.induction (C := fun w' : World => f.rel 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'' + +/-- Löb induction, via the L axiom. -/ +theorem Satisfies.l_induction (m : Model World τ Atom) [IsTrans World m.rel] + (hwf : Relation.Terminating m.rel) (hstep : ∀ w, ⇓Modal[m,w ⊨ □φ → φ]) (w : World) : + ⇓Modal[m, w ⊨ φ] := by + have hl := Satisfies.of_axiom m _ (Satisfies.l m.toFrame 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 (f : Frame World τ) (h : Diamond f.rel) + (φ : Proposition τ Atom) : Axiom f⇓(◇□φ → □◇φ) := 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 (f : Frame World τ) [Nonempty Atom] + (h : ∀ φ : Proposition τ Atom, Axiom f⇓(◇□φ → □◇φ)) : Diamond f.rel := by + intro w w₁ w₂ hww₁ hww₂ + specialize h (Classical.arbitrary Atom) (fun w' _ => f.rel w₁ w') w + grind [Join] + +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.rel] {φ₁ φ₂ : Proposition τ Atom} (hd : Diamond m.rel) + (h₁ : Preserves m.rel (⇓Modal[m,· ⊨ φ₁])) (h₂ : Preserves m.rel (⇓Modal[m,· ⊨ φ₂])) : + ◇(φ₁ ∧ φ₂) ≡[Equiv m] (◇φ₁ ∧ ◇φ₂) := by + rw [equiv_iff_forall_iff] + intro a + constructor + case mp => + grind only [modal, Satisfies.diamond_iff_exists] + case mpr => + intro h + simp only [Satisfies.and_iff_and, Satisfies.diamond_iff_exists] at h + obtain ⟨⟨b, hab, hb⟩, ⟨c, hac, hc⟩⟩ := h + obtain ⟨d, hbd, hcd⟩ := hd hab hac + rw [Satisfies.diamond_iff_exists (τ := τ)] + refine ⟨d, IsTrans.trans a b d hab hbd, ?_⟩ + apply Satisfies.and_iff_and.mpr + 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.rel] + [IsTrans World m.rel] (φ : Proposition τ Atom) : ◇◇φ ≡[Equiv m] ◇φ := by + rw [equiv_iff_forall_iff] + intro w + constructor <;> rw [← Satisfies.imp_iff_imp] + · grind [Satisfies.unimodal_four] + · grind [Satisfies.unimodal_t] + +/-- Context constructor for the diamond modality. -/ +@[match_pattern] +def Proposition.Context.diamond (c : Context τ Atom) : Context τ Atom := .dynDiamond c default + +/-- Constructs a signature for basic modal logic at the same universe level of the input type. -/ +def τUnimodal (_ : Type u) : PFunctor.{u,u} where + A := PUnit + B := fun _ => PUnit + +instance : (τUnimodal α).Unary where + unary _ := by + change Unique PUnit + infer_instance + +instance : Unique ((τUnimodal α).A) := by + change Unique PUnit + infer_instance + +instance : (τUnimodal α).DecidableEqChildren := ⟨by infer_instance⟩ + +@[simp, scoped grind =, modal =] +theorem _root_.Cslib.Frame.ofRelation_unimodal_rel_iff + (r : World → World → Prop) (w w' : World) : + (Frame.ofRelation (τ := τUnimodal World) r).rel w w' ↔ r w w' := by + rfl + +namespace Unimodal + +/-- A basic model, constructed on `τUnimodal`. -/ +abbrev Model World Atom := Modal.Model World (τUnimodal Atom) Atom + +/-- The language of modal propositions instantiated for `τUnimodal Atom`. -/ +abbrev Proposition Atom := Modal.Proposition (τUnimodal Atom) Atom + +end Unimodal + +end Logic.Modal + +end Unimodal + +end Cslib diff --git a/Cslib/Logics/Modal/Cube.lean b/Cslib/Logics/Modal/Unimodal/Cube.lean similarity index 73% rename from Cslib/Logics/Modal/Cube.lean rename to Cslib/Logics/Modal/Unimodal/Cube.lean index a56bf81d0..4ab6728e1 100644 --- a/Cslib/Logics/Modal/Cube.lean +++ b/Cslib/Logics/Modal/Unimodal/Cube.lean @@ -6,13 +6,13 @@ Authors: Fabrizio Montesi, Marianna Girlando module -public import Cslib.Logics.Modal.Basic +public import Cslib.Logics.Modal.Unimodal.Basic public import Cslib.Foundations.Relation.Euclidean /-! # Modal Logic Cube -This module formalises the Modal Cube, including all the 15 foundational modal logics and their -relationships. +This module formalises the Modal Cube for basic modal logic, including all the 15 foundational modal +logics and their relationships. ## References @@ -22,7 +22,7 @@ relationships. @[expose] public section -namespace Cslib.Logic.Modal +namespace Cslib.Logic.Modal.Unimodal /-- The modal logic K. -/ @[scoped grind =] @@ -30,70 +30,70 @@ def K World Atom := logic (Set.univ (α := Model World Atom)) /-- The modal logic T. -/ @[scoped grind =] -def T World Atom := logic {m : Model World Atom | Std.Refl m.r} +def T World Atom := logic {m : Model World Atom | Std.Refl m.rel} /-- The modal logic B. -/ @[scoped grind =] -def B World Atom := logic {m : Model World Atom | Std.Symm m.r} +def B World Atom := logic {m : Model World Atom | Std.Symm m.rel} /-- The modal logic 4. -/ @[scoped grind =] -def Four World Atom := logic {m : Model World Atom | IsTrans World m.r} +def Four World Atom := logic {m : Model World Atom | IsTrans World m.rel} /-- The modal logic 5. -/ @[scoped grind =] -def Five World Atom := logic {m : Model World Atom | Relation.RightEuclidean m.r} +def Five World Atom := logic {m : Model World Atom | Relation.RightEuclidean m.rel} /-- The modal logic K45. -/ @[scoped grind =] def K45 World Atom := - logic {m : Model World Atom | IsTrans World m.r ∧ Relation.RightEuclidean m.r} + logic {m : Model World Atom | IsTrans World m.rel ∧ Relation.RightEuclidean m.rel} /-- The modal logic D. -/ @[scoped grind =] -def D World Atom := logic {m : Model World Atom | Relation.Serial m.r} +def D World Atom := logic {m : Model World Atom | Relation.Serial m.rel} /-- The modal logic D4. -/ @[scoped grind =] def D4 World Atom := - logic {m : Model World Atom | Relation.Serial m.r ∧ IsTrans World m.r} + logic {m : Model World Atom | Relation.Serial m.rel ∧ IsTrans World m.rel} /-- The modal logic D5. -/ @[scoped grind =] def D5 World Atom := - logic {m : Model World Atom | Relation.Serial m.r ∧ Relation.RightEuclidean m.r} + logic {m : Model World Atom | Relation.Serial m.rel ∧ Relation.RightEuclidean m.rel} /-- The modal logic D45. -/ @[scoped grind =] def D45 World Atom := logic {m : Model World Atom | - Relation.Serial m.r ∧ IsTrans World m.r ∧ Relation.RightEuclidean m.r} + Relation.Serial m.rel ∧ IsTrans World m.rel ∧ Relation.RightEuclidean m.rel} /-- The modal logic DB. -/ @[scoped grind =] def DB World Atom := - logic {m : Model World Atom | Relation.Serial m.r ∧ Std.Symm m.r} + logic {m : Model World Atom | Relation.Serial m.rel ∧ Std.Symm m.rel} /-- The modal logic TB. -/ @[scoped grind =] def TB World Atom := - logic {m : Model World Atom | Std.Refl m.r ∧ Std.Symm m.r} + logic {m : Model World Atom | Std.Refl m.rel ∧ Std.Symm m.rel} /-- The modal logic KB5. -/ @[scoped grind =] def KB5 World Atom := - logic {m : Model World Atom | Std.Symm m.r ∧ Relation.RightEuclidean m.r} + logic {m : Model World Atom | Std.Symm m.rel ∧ Relation.RightEuclidean m.rel} /-- The modal logic S4. -/ @[scoped grind =] def S4 World Atom := - logic {m : Model World Atom | Std.Refl m.r ∧ IsTrans World m.r} + logic {m : Model World Atom | Std.Refl m.rel ∧ IsTrans World m.rel} /-- The modal logic S5. -/ @[scoped grind =] def S5 World Atom := logic {m : Model World Atom | - Std.Refl m.r ∧ IsTrans World m.r ∧ Relation.RightEuclidean m.r} + Std.Refl m.rel ∧ IsTrans World m.rel ∧ Relation.RightEuclidean m.rel} section Order @@ -147,8 +147,8 @@ 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 := h)] + grind [Satisfies.unimodal_t (instRefl := h)] end Validity -end Cslib.Logic.Modal +end Cslib.Logic.Modal.Unimodal diff --git a/Cslib/Logics/Modal/Unimodal/Lean/Basic.lean b/Cslib/Logics/Modal/Unimodal/Lean/Basic.lean new file mode 100644 index 000000000..ddea0be0d --- /dev/null +++ b/Cslib/Logics/Modal/Unimodal/Lean/Basic.lean @@ -0,0 +1,61 @@ +/- +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.Foundations.Relation.Preserves +public import Cslib.Logics.Modal.Denotation +public import Cslib.Logics.Modal.Lean.Basic +public import Cslib.Logics.Modal.Unimodal.Basic + +/-! # Basic Modal Logic for Lean -/ + +@[expose] public section + +namespace Cslib.Logic.Modal + +variable {τ : PFunctor} [τ.Unary] [Unique τ.A] + +/-- Builds a unimodal predicate model from a binary relation. -/ +abbrev Model.unimodalOfPredicates (r : α → α → Prop) : Model α τ (α → Prop) := + Modal.Model.ofPredicates (Frame.ofRelation r) + +/-- Builds a unimodal container model from a binary relation. -/ +abbrev Model.unimodalOfContainers [Membership α β] (r : α → α → Prop) : Model α τ β := + Modal.Model.ofContainers (Frame.ofRelation r) + +open Model Relation +open scoped InferenceSystem Satisfies Proposition Frame + +/-- Under `Model.unimodalOfPredicates r`, `P → □P` is an axiom iff `r` preserves `P`. -/ +theorem Satisfies.unimodalOfPredicates_preserves_iff {P : α → Prop} (r : α → α → Prop) : + (∀ a, ⇓Modal[Model.unimodalOfPredicates (τ := τ) r,a ⊨ P → □P]) ↔ Preserves r P := by + constructor + case mp => + intro h a₁ a₂ hr hPa₁ + simp only [Satisfies.imp_iff_imp] at h + specialize h a₁ hPa₁ + simp only [Satisfies.box_iff_forall] at h + specialize h a₂ + grind only [modal] + case mpr => + grind [Preserves] + +/-- Invariants are preserved by the reflexive and transitive closure of the accessibility relation. +-/ +@[scoped grind ., modal .] +theorem Satisfies.unimodalOfPredicates_preserves_reflTransGen + {r : α → α → Prop} {P : α → Prop} + (h : ∀ a, ⇓Modal[unimodalOfPredicates (τ := τ) r,a ⊨ P → □P]) : + ∀ a, ⇓Modal[unimodalOfPredicates (τ := τ) (Relation.ReflTransGen r),a ⊨ P → □P] := by + apply (Satisfies.ofPredicates_preservesMap_iff + (Frame.ofRelation (τ := τ) (Relation.ReflTransGen r))).mpr + have hmap : (Frame.ofRelation (τ := τ) r).PreservesMap + default P (fun _ => P) := by + exact (Satisfies.ofPredicates_preservesMap_iff (Frame.ofRelation (τ := τ) r)).mp h + grind + +end Cslib.Logic.Modal diff --git a/Cslib/Logics/Modal/Lean/SMul.lean b/Cslib/Logics/Modal/Unimodal/Lean/SMul.lean similarity index 77% rename from Cslib/Logics/Modal/Lean/SMul.lean rename to Cslib/Logics/Modal/Unimodal/Lean/SMul.lean index 06b7a9f29..72b8646b5 100644 --- a/Cslib/Logics/Modal/Lean/SMul.lean +++ b/Cslib/Logics/Modal/Unimodal/Lean/SMul.lean @@ -7,7 +7,7 @@ Authors: Fabrizio Montesi module public import Mathlib.GroupTheory.GroupAction.SubMulAction -public import Cslib.Logics.Modal.Lean.Basic +public import Cslib.Logics.Modal.Unimodal.Lean.Basic /-! # Modal Logic for scalar multiplication (SMul) @@ -82,25 +82,41 @@ theorem ofSMul_preserves_mem [SMul M α] [SetLike S α] [SMulMemClass S M α] rw [Relation.ofSMul_preserves_iff] apply SMulMemClass.smul_mem +@[scoped grind →] +theorem ofSMul_mem_of_mem [SMul M α] [SetLike S α] [SMulMemClass S M α] + {p : S} {a b : α} (hab : Relation.ofSMul M α a b) (ha : a ∈ p) : b ∈ p := + ofSMul_preserves_mem p hab ha + end Relation namespace Cslib.Logic.Modal.Proposition +variable {τ : PFunctor} [τ.Unary] [Unique τ.A] + +open scoped Satisfies Frame Relation + /-- 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 α)) = + (◇p : Proposition τ β).denotation + (Model.ofContainers (Frame.ofRelation (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 + rw [satisfies_mem_denotation, Satisfies.diamond_iff_exists] + constructor + · grind [Relation.ofSMul] + · rintro ⟨m, hm⟩ + refine ⟨m • x, ?_⟩ + grind [Relation.ofSMul] /-- 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) + ◇(p ∧ q : Proposition τ S) ≡[Equiv.OfContainers + (Frame.ofRelation (τ := τ) (Relation.ofSMul M α)) + ] (◇p ∧ ◇q) := by + have : IsTrans α (Frame.ofRelation (τ := τ) (Relation.ofSMul M α)).rel := by + simpa [Frame.ofRelation_rel] using (inferInstance : IsTrans α (Relation.ofSMul M α)) + apply diamond_and_equiv_of_preserves <;> grind [Relation.Preserves] end Cslib.Logic.Modal.Proposition diff --git a/CslibTests.lean b/CslibTests.lean index 94af0f156..bea9caaab 100644 --- a/CslibTests.lean +++ b/CslibTests.lean @@ -18,5 +18,6 @@ import CslibTests.MLL import CslibTests.Modal import CslibTests.Modal.Ideal import CslibTests.Modal.Stlc +import CslibTests.Modal.UnimodalCube import CslibTests.Reduction import CslibTests.StatefulProcesses diff --git a/CslibTests/GrindLint.lean b/CslibTests/GrindLint.lean index 70cce89a0..896c8467b 100644 --- a/CslibTests/GrindLint.lean +++ b/CslibTests/GrindLint.lean @@ -69,7 +69,8 @@ open_scoped_all Cslib #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.ListFullBeta.step #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.sub #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Fsub.Env.Wf.ty -#grind_lint skip Cslib.Logic.HML.bisimulation_satisfies +#grind_lint skip Cslib.Logic.Modal.Satisfies.iff_iff_iff +#grind_lint skip Cslib.Logic.Modal.Satisfies.triangle_of_diagonal #grind_lint skip Cslib.LambdaCalculus.LocallyNameless.Untyped.Term.step_multiApp_l #adaptation_note /-- (changes from lean#13166) -/ @@ -83,7 +84,6 @@ open_scoped_all Cslib #grind_lint skip Cslib.LTS.IsBisimulation.sup #grind_lint skip Cslib.LTS.IsBisimulation.traceEq #grind_lint skip Cslib.LTS.IsBisimulationUpTo.isBisimulation -#grind_lint skip Cslib.Logic.HML.theoryEq_isBisimulation #guard_msgs in #grind_lint check (min := 20) in Cslib diff --git a/CslibTests/HML.lean b/CslibTests/HML.lean index b1a4fae2f..7325917eb 100644 --- a/CslibTests/HML.lean +++ b/CslibTests/HML.lean @@ -5,17 +5,25 @@ Authors: Fabrizio Montesi -/ import Cslib.Logics.HML.Basic -import Cslib.Logics.HML.LogicalEquivalence +import Cslib.Logics.Modal.LogicalEquivalence import Cslib.Languages.CCS.Semantics namespace CslibTests -open Cslib Logic HML LTS +open Cslib Logic Modal HML LTS Model Proposition Satisfies +open scoped InferenceSystem example [∀ p μ, Finite ((CCS.lts (defs := defs)).image p μ)] : - TheoryEq (CCS.lts (defs := defs)) = HomBisimilarity (CCS.lts (defs := defs)) := + TheoryEq (Atom := Unit) (ofLTS (CCS.lts (defs := defs)) (fun _ _ => True)) = + HomBisimilarity (CCS.lts (defs := defs)) := theoryEq_eq_bisimilarity .. +example (v : State → Atom → Prop) (htr : lts.Tr s μ s') (hφ : ⇓Modal[ofLTS lts v,s' ⊨ φ]) : + ⇓Modal[ofLTS lts v,s ⊨ d⟨μ⟩φ] := by grind only [modal] + +example (v : State → Atom → Prop) (hbox : ⇓Modal[Model.ofLTS lts v,s ⊨ d[μ]φ]) + (htr : lts.Tr s μ s') : ⇓Modal[ofLTS lts v,s' ⊨ φ] := by grind only [modal] + section LogicalEquivalence /- @@ -26,21 +34,23 @@ with grind. Note that the grind proof works because Satisfies.and_iff_and gives principle on the satisfaction relation for the and-connective. -/ -open scoped InferenceSystem -open Proposition +open PFunctor -example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} {φ₁ φ₂ : Proposition Label} - (h : ⇓HML[lts,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂]) - : ⇓HML[lts,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by - let pc : HasContext.Context (Proposition Label) := Context.andL .hole φ₂ +example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} + {φ₁ φ₂ : HML.Proposition Label Atom} (v : State → Atom → Prop) + (h : ⇓Modal[ofLTS lts v,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂]) : ⇓Modal[ofLTS lts v,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by + let pc : HasContext.Context (HML.Proposition Label Atom) := Context.andL .hole φ₂ + have dual a (φ : HML.Proposition Label Atom) : d⟨a⟩φ ≡[UEquiv (World := State)] ¬d[a]¬φ := by + grind only [modal, Satisfies.unary_dual] have eqv := LawfulCongruence.covariant.elim pc (dual μ φ₁) - let jc : HasHContext.Context (Judgement State Label) (Proposition Label) := - Judgement.Context.mk lts s + let jc : HasHContext.Context (Judgement State (mkUnary Label) Atom) + (HML.Proposition Label Atom) := Judgement.Context.mk (ofLTS lts v) s apply LogicalEquivalence.eqvFillValid eqv jc h -example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} {φ₁ φ₂ : Proposition Label} - (h : ⇓HML[lts,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂]) : ⇓HML[lts,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by - grind only [= Satisfies.and_iff_and, => equiv_iff, dual μ φ₁ lts] +example {State : Type u} {lts : LTS State Label} {s : State} {μ : Label} + {φ₁ φ₂ : HML.Proposition Label Atom} (v : State → Atom → Prop) + (h : ⇓Modal[ofLTS lts v,s ⊨ (d⟨μ⟩φ₁) ∧ φ₂]) : + ⇓Modal[ofLTS lts v,s ⊨ (¬d[μ]¬φ₁) ∧ φ₂] := by grind [modal] end LogicalEquivalence diff --git a/CslibTests/Modal.lean b/CslibTests/Modal.lean index e9a2bdb61..b3183ad02 100644 --- a/CslibTests/Modal.lean +++ b/CslibTests/Modal.lean @@ -1,78 +1,97 @@ /- -Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Copyright (c) 2026 Fabrizio Montesi. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Samuel Schlesinger +Authors: Fabrizio Montesi -/ -import Cslib.Logics.Modal.Cube +import Cslib.Logics.Modal.Semantics namespace Cslib.Logic.Modal -open scoped Proposition - -variable {World Atom : Type*} {φ : Proposition Atom} - --- Compound modal logics contain conjunctions of the axioms validated by their combined frame --- conditions. Defining them as unions of the individual logics loses these conjunctions. - -example : ((◇◇φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ K45 World Atom := by - intro m h w - let : IsTrans World m.r := h.1 - let : Relation.RightEuclidean m.r := h.2 - 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 _ φ _ _⟩ - -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 _ φ _ _⟩ - -example : - Proposition.and (□φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ - D45 World Atom := by - intro m h w - 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 _ φ _ _⟩ - -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 _ φ _ _⟩ - -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 _ φ _ _⟩ - -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 _ φ _ _⟩ - -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 _ φ _ _⟩ - -example : - Proposition.and (φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ - S5 World Atom := by - intro m h w - 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 _ φ _ _⟩ +open scoped InferenceSystem Proposition Satisfies + +section Grind + +variable {τ : PFunctor} +variable {World Atom : Type*} +variable {m : Model World τ Atom} + +/-! ## Basic propositional connectives -/ + +example (h : ⇓Modal[m,w ⊨ ¬φ]) : ¬⇓Modal[m,w ⊨ φ] := by grind only [modal] + +example (h : ⇓Modal[m,w ⊨ φ₁ ∧ φ₂]) : ⇓Modal[m,w ⊨ φ₁] := by + grind only [modal] + +example (h₁ : ⇓Modal[m,w ⊨ φ₁]) (h₂ : ⇓Modal[m,w ⊨ φ₂]) : ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] := by + grind only [modal] + +example (h : ⇓Modal[m,w ⊨ φ₁ → φ₂]) (h₁ : ⇓Modal[m,w ⊨ φ₁]) : ⇓Modal[m,w ⊨ φ₂] := by + grind only [modal] + +example (h : ⇓Modal[m,w ⊨ φ₁ ↔ φ₂]) (h₁ : ⇓Modal[m,w ⊨ φ₁]) : ⇓Modal[m,w ⊨ φ₂] := by + grind only [modal] + +/-! ## Triangle -/ + +example (h : ⇓Modal[m,w ⊨ Δ[op]φs]) : ∃ ws, m.r op w ws ∧ ∀ i, ⇓Modal[m,ws i ⊨ φs i] := by grind + +example (hr : m.r op w ws) (hs : ∀ i, ⇓Modal[m,ws i ⊨ φs i]) : ⇓Modal[m,w ⊨ Δ[op]φs] := by grind + +/-! ## Nabla -/ + +example (h : ⇓Modal[m,w ⊨ ∇[op]φs]) (hr : m.r op w ws) : ∃ i, ⇓Modal[m,ws i ⊨ φs i] := by grind + +example (h : ∀ ws, m.r op w ws → ∃ i, ⇓Modal[m,ws i ⊨ φs i]) : ⇓Modal[m,w ⊨ ∇[op]φs] := by grind + +/-! ## Composition of modal and propositional operators -/ + +example (h : ⇓Modal[m,w ⊨ Δ[op]φs]) (himp : ∀ ws i, m.r op w ws → ⇓Modal[m,ws i ⊨ φs i → ψs i]) : + ⇓Modal[m,w ⊨ Δ[op]ψs] := by grind + +example (h : ⇓Modal[m,w ⊨ ∇[op]φs]) (himp : ∀ ws i, m.r op w ws → ⇓Modal[m,ws i ⊨ φs i → ψs i]) : + ⇓Modal[m,w ⊨ ∇[op]ψs] := by grind + +/-! ## Derivable modal laws -/ + +/-- A modal implication should behave as modus ponens. -/ +example {φ ψ : Proposition τ Atom} (himp : ⇓Modal[m,w ⊨ φ → ψ]) (hφ : ⇓Modal[m,w ⊨ φ]) : + ⇓Modal[m,w ⊨ ψ] := by grind only [modal] + +/-- `grind` should instantiate quantified modal implications. -/ +example {φs ψs : PropositionMap τ op Atom} + (himp : ∀ i w, ⇓Modal[m,w ⊨ φs i → ψs i]) + (hφ : ⇓Modal[m,w' ⊨ φs i]) : + ⇓Modal[m,w' ⊨ ψs i] := by + simp only [Satisfies.imp_iff_imp] at himp + grind only [modal] + +/-- Triangle is monotone in every argument. -/ +example {op : τ.A} {φs ψs : PropositionMap τ op Atom} (himp : ∀ i w, ⇓Modal[m,w ⊨ φs i → ψs i]) + (h : ⇓Modal[m,w ⊨ Δ[op]φs]) : ⇓Modal[m,w ⊨ Δ[op]ψs] := by + simp only [Satisfies.imp_iff_imp] at himp + grind [modal] + +/-- Nabla is monotone in every argument. -/ +example {φs ψs : PropositionMap τ op Atom} (himp : ∀ i w, ⇓Modal[m,w ⊨ φs i → ψs i]) + (h : ⇓Modal[m,w ⊨ ∇[op]φs]) : ⇓Modal[m,w ⊨ ∇[op]ψs] := by + simp only [Satisfies.imp_iff_imp] at himp + grind [modal] + +/-- Triangle preserves pointwise conjunction in the forward direction. -/ +example {φs ψs : PropositionMap τ op Atom} + (h : ⇓Modal[m,w ⊨ Δ[op](φs ∧ ψs)]) : ⇓Modal[m,w ⊨ Δ[op]φs ∧ Δ[op]ψs] := by + grind [modal] + +/-- Either nabla condition entails their pointwise disjunction. -/ +example {φs ψs : PropositionMap τ op Atom} + (h : ⇓Modal[m,w ⊨ ∇[op]φs ∨ ∇[op]ψs]) : ⇓Modal[m,w ⊨ ∇[op](φs ∨ ψs)] := by + grind [modal] + +/-- Nabla is the dual of triangle. -/ +example {φs : PropositionMap τ op Atom} : ⇓Modal[m,w ⊨ ∇[op]φs] ↔ ⇓Modal[m,w ⊨ ¬Δ[op](¬φs)] := by + grind + +end Grind end Cslib.Logic.Modal diff --git a/CslibTests/Modal/Ideal.lean b/CslibTests/Modal/Ideal.lean index f9cb8ee2a..424c920a1 100644 --- a/CslibTests/Modal/Ideal.lean +++ b/CslibTests/Modal/Ideal.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Fabrizio Montesi -/ -import Cslib.Logics.Modal.Lean.SMul +import Cslib.Logics.Modal.Unimodal.Lean.SMul import Mathlib.RingTheory.Ideal.Operations /-! # Example: radicals of ideals with modal logic @@ -42,8 +42,12 @@ local instance [Semiring R] : SMulMemClass (Ideal R) ℕ+ R := Ideal.posPowSMulM /-- 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) +/-- The unimodal frame of ideals under positive-power accessibility. -/ +abbrev idealPowerFrame [Semiring R] : Frame R (τUnimodal R) := Frame.ofRelation (PosPow R) + +/-- Container model induced by `idealPowerFrame R` and `Ideal R`. -/ +abbrev idealPowerModel {R : Type u} [Semiring R] : Model R (τUnimodal R) (Ideal R) := + Model.ofContainers idealPowerFrame /-- Logical equivalence under `idealPowerModel`. -/ abbrev IdealEquiv [Semiring R] := Proposition.Equiv (idealPowerModel (R := R)) @@ -56,7 +60,7 @@ 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] + rw [Proposition.ofSMul_diamond_denotation (τ := (τUnimodal R))] ext x apply Iff.intro · rintro ⟨n, hn⟩ @@ -67,7 +71,7 @@ theorem Ideal.radical_eq_modal_denotation [CommSemiring R] (I : Ideal R) : /-- 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 := + (I.radical : Proposition (τUnimodal R) (Ideal R)) ≡[IdealEquiv] ◇I := Proposition.equiv_iff_denotation_eq.mpr (Ideal.radical_eq_modal_denotation I) open scoped Satisfies @@ -75,23 +79,24 @@ 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] + rw [Ideal.radical_eq_modal_denotation (I.radical), Ideal.radical_eq_modal_denotation I] 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 + (◇(I.radical : Ideal R) : Proposition (τUnimodal R) (Ideal R)) ≡[IdealEquiv] ◇◇I := by + let pc : HasContext.Context (Proposition (τUnimodal R) (Ideal R)) := + Context.diamond (τ := (τUnimodal R)) (Atom := Ideal R) .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 +theorem Ideal.inf_modelEquiv {R : Type u} [Semiring R] (I J : Ideal R) : + (◇(I ⊓ J : Ideal R) : Proposition (τUnimodal R) (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 + (◇(I ⊓ J : Ideal R) : Proposition (τUnimodal R) (Ideal R)) ≡[IdealEquiv] ◇(I ∧ J) := by + let pc : HasContext.Context (Proposition (τUnimodal R) (Ideal R)) := Context.diamond .hole exact LawfulCongruence.covariant.elim pc - (Proposition.ofContainers_inf_equiv (PosPow R) I J (by simp)) + (Proposition.ofContainers_inf_equiv idealPowerFrame 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 @@ -101,6 +106,6 @@ theorem Ideal.radical_inf [CommSemiring R] (I J : Ideal R) : apply SetLike.ext' simp_rw [Submodule.coe_inf, Ideal.radical_eq_modal_denotation, Proposition.denotation_eq_of_equiv (Ideal.inf_modelEquiv I J)] - rfl + grind end CslibTests diff --git a/CslibTests/Modal/Stlc.lean b/CslibTests/Modal/Stlc.lean index 1b01ede57..7cc6e4180 100644 --- a/CslibTests/Modal/Stlc.lean +++ b/CslibTests/Modal/Stlc.lean @@ -5,7 +5,7 @@ Authors: Fabrizio Montesi -/ import Cslib.Languages.LambdaCalculus.LocallyNameless.Stlc.Safety -import Cslib.Logics.Modal.Lean.Basic +import Cslib.Logics.Modal.Unimodal.Lean.Basic import Cslib.Foundations.Relation.Preserves /-! # Modal logic for type safety (exemplified on the simply typed λ-calculus) @@ -38,8 +38,8 @@ judgements. full β-reduction). 3. We stratify the multistep model on top of the single step model by means of an atomic proposition, `IsSingleStepSafe τ t`, defined as - `⇓Modal[singleStepModel,t ⊨ IsValue ∨ ◇HasType τ]`. (This would not be necessary with multimodal - logic, as we could use different modalities for single- and multistep reductions.) + `⇓Modal[singleStepModel,t ⊨ IsValue ∨ ◇HasType τ]`. (This is necessary because we use unimodal + logic; alternatively, we could use different modalities for single- and multistep reductions.) 4. Using the above and Axiom K, we derive type safety in the multistep model: `HasType τ → □IsSingleStepSafe τ`. 5. The standard type safety statement is trivially extracted by unfolding the semantics of step (4). @@ -52,7 +52,7 @@ judgements. namespace CslibTests.LambdaCalculus.Stlc.Modal open Cslib Logic Modal LambdaCalculus LocallyNameless Stlc Untyped Term Relation -open scoped Satisfies Term InferenceSystem +open scoped Satisfies Term InferenceSystem Frame variable {Var : Type*} [HasFresh Var] @@ -62,13 +62,27 @@ variable {Var : Type*} [HasFresh Var] abbrev LAtom Var := Term Var → Prop /-- Modal propositions over predicates on λ-terms. -/ -abbrev LProposition Var := Proposition (LAtom Var) +abbrev LProposition (Var : Type u) := Proposition (τUnimodal (Term Var)) (LAtom Var) /-- The single step model of full β-reduction. -/ -abbrev singleStepModel : Model (Term Var) (LAtom Var) := Model.ofPredicates (· ⭢βᶠ ·) +def singleStepModel : Model (Term Var) (τ := τUnimodal (Term Var)) (LAtom Var) := + Model.unimodalOfPredicates (· ⭢βᶠ ·) + +omit [HasFresh Var] in +theorem singleStepModel_rel_iff (t t' : Term Var) : singleStepModel.rel t t' ↔ t ⭢βᶠ t' := by + grind only [singleStepModel, = Frame.ofRelation_rel_iff] + +attribute [local grind _=_] singleStepModel_rel_iff /-- The multistep model of full β-reduction. -/ -abbrev multiStepModel : Model (Term Var) (LAtom Var) := Model.ofPredicates (· ↠βᶠ ·) +def multiStepModel {Var : Type u} : Model (Term Var) (τUnimodal (Term Var)) (LAtom Var) := + Model.unimodalOfPredicates (· ↠βᶠ ·) + +omit [HasFresh Var] in +theorem multiStepModel_rel_iff (t t' : Term Var) : multiStepModel.rel t t' ↔ t ↠βᶠ t' := by + grind only [multiStepModel, = Frame.ofRelation_rel_iff] + +attribute [local grind _=_] multiStepModel_rel_iff /-! ## Atomic modal propositions on terms -/ @@ -95,8 +109,10 @@ Suppose that whenever `φ₁` holds: Then either `φ₃` already holds or some successor satisfies `φ₂`. -/ -theorem safety_of_preservation_progress (hpres : ⇓Modal[m,w ⊨ φ₁ → □φ₂]) - (hprog : ⇓Modal[m,w ⊨ φ₁ → φ₃ ∨ ◇φ₄]) : ⇓Modal[m,w ⊨ φ₁ → φ₃ ∨ ◇φ₂] := by +theorem safety_of_preservation_progress + {φ₁ φ₂ φ₃ φ₄ : Proposition (τUnimodal α) Atom} + (hpres : ⇓Modal[m,w ⊨ φ₁ → □φ₂]) (hprog : ⇓Modal[m,w ⊨ φ₁ → φ₃ ∨ ◇φ₄]) : + ⇓Modal[m,w ⊨ φ₁ → φ₃ ∨ ◇φ₂] := by have : ⇓Modal[m, w ⊨ □φ₂ ∧ ◇φ₄ → ◇φ₂] := by grind only [modal] grind only [modal] @@ -106,15 +122,16 @@ theorem safety_of_preservation_progress (hpres : ⇓Modal[m,w ⊨ φ₁ → □ theorem preservation_singleStepModel_modal (τ : Ty Base) (t : Term Var) : ⇓Modal[singleStepModel, t ⊨ HasType τ → □HasType τ] := by classical - exact ((Satisfies.ofPredicates_preserves_iff (· ⭢βᶠ ·)).mpr (FullBeta.preservation (τ := τ))) t + exact ((Satisfies.unimodalOfPredicates_preserves_iff (τ := (τUnimodal (Term Var))) (· ⭢βᶠ ·)).mpr + (FullBeta.preservation (τ := τ))) t omit [HasFresh Var] in /-- Modal view of single step progress. -/ theorem progress_modal (τ : Ty Base) (t : Term Var) : - ⇓Modal[singleStepModel, t ⊨ HasType τ → IsValue ∨ ◇IsTerm] := by + ⇓Modal[singleStepModel,t ⊨ HasType τ → IsValue ∨ ◇IsTerm] := by rw [Satisfies.imp_iff_imp] intro ht - rcases FullBeta.progress ht <;> grind only [modal, = Satisfies.diamond_iff_exists] + rcases FullBeta.progress ht <;> grind [singleStepModel] /-! ## Modal development of type safety @@ -125,7 +142,7 @@ STLC-specific reasoning is required. /-- Modal view of multistep typing preservation. -/ theorem preservation_multiStep_modal (τ : Ty Base) (t : Term Var) : ⇓Modal[multiStepModel, t ⊨ HasType τ → □HasType τ] := - Satisfies.ofPredicates_preserves_reflTransGen (preservation_singleStepModel_modal τ ·) t + Satisfies.unimodalOfPredicates_preserves_reflTransGen (preservation_singleStepModel_modal τ ·) t /-- Modal view that preservation and progress give single step safety. -/ theorem type_safety_singleStep_modal (τ : Ty Base) (t : Term Var) : @@ -145,20 +162,30 @@ theorem type_safety_modal (τ : Ty Base) (t : Term Var) : ⇓Modal[multiStepModel,t ⊨ HasType τ → □IsSingleStepSafe τ] := by have hpres := preservation_multiStep_modal (Var := Var) τ t have hsafety : ⇓Modal[multiStepModel,t ⊨ □(HasType τ → IsSingleStepSafe τ)] := by - rw [Satisfies.box_iff_forall] + rw [Satisfies.box_iff_forall (τ := τUnimodal (Term Var))] intro t' - grind only [modal, type_safety_singleStep_modal (Var := Var) τ t'] + grind only [singleStepModel, multiStepModel, modal, + type_safety_singleStep_modal (Var := Var) τ t'] -- Axiom K instantiated for single step type safety have hk : ⇓Modal[multiStepModel,t ⊨ □(HasType τ → IsSingleStepSafe τ) → (□HasType τ → □IsSingleStepSafe τ)] := - Satisfies.der_of_axiom (Satisfies.k multiStepModel.r _ _) + Satisfies.der_of_axiom (Satisfies.unimodal_k multiStepModel.toFrame _ _) grind only [modal] /-- Type safety: if a term is well-typed, any term it can reach is either a value or can progress. -/ theorem type_safety {t t' : Term Var} {τ : Ty Base} (ht : [] ⊢ t ∶ τ) (hsteps : t ↠βᶠ t') : t'.Value ∨ ∃ t'', t' ⭢βᶠ t'' ∧ [] ⊢ t'' ∶ τ := by - grind only [modal, type_safety_modal (Var := Var) τ t, Satisfies.box_iff_forall, - Satisfies.diamond_iff_exists] + -- We use `grind only` on purpose to test that the passed theorems are sufficient. + grind only [ + _=_ singleStepModel_rel_iff, + _=_ multiStepModel_rel_iff, + singleStepModel, + multiStepModel, + modal, + type_safety_modal (Var := Var) τ t, + Satisfies.box_iff_forall, + Satisfies.diamond_iff_exists + ] end CslibTests.LambdaCalculus.Stlc.Modal diff --git a/CslibTests/Modal/UnimodalCube.lean b/CslibTests/Modal/UnimodalCube.lean new file mode 100644 index 000000000..bcf077a99 --- /dev/null +++ b/CslibTests/Modal/UnimodalCube.lean @@ -0,0 +1,87 @@ +/- +Copyright (c) 2026 Samuel Schlesinger. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Samuel Schlesinger +-/ + +import Cslib.Logics.Modal.Unimodal.Cube + +namespace Cslib.Logic.Modal.Unimodal + +open scoped Proposition + +variable {World Atom : Type*} {φ : Proposition Atom} + +-- Compound modal logics contain conjunctions of the axioms validated by their combined frame +-- conditions. Defining them as unions of the individual logics loses these conjunctions. + +example : ((◇◇φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ K45 World Atom := by + intro m h w + let : IsTrans World m.rel := h.1 + let : Relation.RightEuclidean m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.unimodal_four _ φ _ _, Satisfies.unimodal_five _ φ _ _⟩ + +example : ((□φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ D4 World Atom := by + intro m h w + let : Relation.Serial m.rel := h.1 + let : IsTrans World m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.d _ φ _ _, Satisfies.unimodal_four _ φ _ _⟩ + +example : ((□φ → ◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ D5 World Atom := by + intro m h w + let : Relation.Serial m.rel := h.1 + let : Relation.RightEuclidean m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.d _ φ _ _, Satisfies.unimodal_five _ φ _ _⟩ + +example : + Proposition.and (□φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ + D45 World Atom := by + intro m h w + let : Relation.Serial m.rel := h.1 + let : IsTrans World m.rel := h.2.1 + let : Relation.RightEuclidean m.rel := h.2.2 + simp only [Proposition.and_def, Satisfies.and_iff_and] + exact ⟨Satisfies.d _ φ _ _, Satisfies.unimodal_four _ φ _ _, Satisfies.unimodal_five _ φ _ _⟩ + +example : ((□φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ DB World Atom := by + intro m h w + let : Relation.Serial m.rel := h.1 + let : Std.Symm m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.d _ φ _ _, Satisfies.unimodal_b _ φ _ _⟩ + +example : ((φ → ◇φ) ∧ (φ → □◇φ) : Proposition Atom) ∈ TB World Atom := by + intro m h w + let : Std.Refl m.rel := h.1 + let : Std.Symm m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.t _ φ _ _, Satisfies.unimodal_b _ φ _ _⟩ + +example : ((φ → □◇φ) ∧ (◇φ → □◇φ) : Proposition Atom) ∈ KB5 World Atom := by + intro m h w + let : Std.Symm m.rel := h.1 + let : Relation.RightEuclidean m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.unimodal_b _ φ _ _, Satisfies.unimodal_five _ φ _ _⟩ + +example : ((φ → ◇φ) ∧ (◇◇φ → ◇φ) : Proposition Atom) ∈ S4 World Atom := by + intro m h w + let : Std.Refl m.rel := h.1 + let : IsTrans World m.rel := h.2 + apply Satisfies.and_iff_and.mpr + exact ⟨Satisfies.t _ φ _ _, Satisfies.unimodal_four _ φ _ _⟩ + +example : + Proposition.and (φ → ◇φ) (Proposition.and (◇◇φ → ◇φ) (◇φ → □◇φ)) ∈ + S5 World Atom := by + intro m h w + let : Std.Refl m.rel := h.1 + let : IsTrans World m.rel := h.2.1 + let : Relation.RightEuclidean m.rel := h.2.2 + simp only [Proposition.and_def, Satisfies.and_iff_and] + exact ⟨Satisfies.t _ φ _ _, Satisfies.unimodal_four _ φ _ _, Satisfies.unimodal_five _ φ _ _⟩ + +end Cslib.Logic.Modal.Unimodal