feat(Logic): General Modal Logic

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

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

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 -/

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

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