feat(Logic): logical operators

Cslib.lean

@@ -77,6 +77,7 @@ public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
+public import Cslib.Foundations.Logic.Operators
 public import Cslib.Foundations.Relation.Attr
 public import Cslib.Foundations.Relation.Confluence
 public import Cslib.Foundations.Relation.Defs

Cslib/Foundations/Logic/LogicalEquivalence.lean

@@ -8,28 +8,41 @@ module
 
 public import Cslib.Foundations.Syntax.Context
 public import Cslib.Foundations.Syntax.Congruence
+public import Cslib.Foundations.Logic.InferenceSystem
 
 /-! Typeclass and notation for logical equivalence. -/
 
 @[expose] public section
 
 namespace Cslib.Logic
 
+open scoped InferenceSystem
+
 /-- A logical equivalence for a given type of `Judgement`s is a congruence on propositions that
 preserves validity of judgements under any judgemental context. -/
-class LogicalEquivalence
+class LogicalEquivalence S
     (Proposition : Type u) [HasContext Proposition]
     (Judgement : Type v) [HasHContext Judgement Proposition]
-    (Valid : Judgement → Sort w) where
-  /-- The logical equivalence relation. -/
+    [InferenceSystem S Judgement] where
+  /-- `a ≡[S] b` means that `a` and `b` are logically equivalent in the inference system `S`. -/
   eqv (a b : Proposition) : Prop
   /-- Proof that `eqv` is a congruence. -/
   [congruence : Congruence Proposition eqv]
   /-- Validity is preserved for any judgemental context. -/
   eqvFillValid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
-    (h : Valid (c<[a])) : Valid (c<[b])
+    (h : S⇓(c<[a])) : S⇓(c<[b])
 
 @[inherit_doc]
-scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+scoped notation a " ≡[" S "]" b => LogicalEquivalence.eqv S a b
+
+/-- Class for types (`α`) that have a canonical logical equivalence (under a canonical, default
+inference system). -/
+abbrev HasLogicalEquivalence (Proposition : Type u) [HasContext Proposition]
+    (Judgement : Type v) [HasHContext Judgement Proposition]
+    [HasInferenceSystem Judgement] :=
+  LogicalEquivalence InferenceSystem.Default Proposition Judgement
+
+/-- `a ≡ b` means that `a` and `b` are logically equivalent. -/
+scoped infix:29 " ≡ " => LogicalEquivalence.eqv InferenceSystem.Default
 
 end Cslib.Logic

Cslib/Foundations/Logic/Operators.lean

@@ -0,0 +1,118 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi, Thomas Waring
+-/
+
+module
+
+public import Cslib.Init
+
+/-! # Logical operators
+
+This module contains typeclasses and associated notation for common logical operators: propositional
+connectives (like `∧` and `→`), modalities (like `◇`, plain and indexed), linear connectives (like
+`⊗`), etc.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+section Propositional
+
+/-! ## Propositional connectives -/
+
+/-- The type `α` has an and connective (`∧`). -/
+class HasAnd (α : Type*) where
+  /-- `a ∧ b` is the conjunction of `a` and `b`. -/
+  and (a b : α) : α
+
+@[inherit_doc] scoped infixr:36 " ∧ " => HasAnd.and
+
+/-- The type `α` has an or connective (`∨`). -/
+class HasOr (α : Type*) where
+  /-- `a ∨ b` is the disjunction of `a` and `b`. -/
+  or (a b : α) : α
+
+@[inherit_doc] scoped infixr:30 " ∨ " => HasOr.or
+
+/-- The type `α` has an implication connective (`→`). -/
+class HasImp (α : Type*) where
+  /-- `a → b` denotes `a` implies `b`. -/
+  imp (a b : α) : α
+
+@[inherit_doc] scoped infixr:25 " → " => HasImp.imp
+
+/-- The type `α` has a bi-implication connective (`↔`). -/
+class HasIff (α : Type*) where
+  /-- `a ↔ b` denotes `a` implies `b` and vice-versa. -/
+  iff (a b : α) : α
+
+@[inherit_doc] scoped infixr:20 " ↔ " => HasIff.iff
+
+/-- The type `α` has a negation connective (`¬`). -/
+class HasNot (α : Type*) where
+  /-- `¬a` is the negation of `a`. -/
+  not (a : α) : α
+
+@[inherit_doc] scoped notation:max "¬" p:40 => HasNot.not p
+
+end Propositional
+
+section Modal
+
+/-! ## Basic modalities -/
+
+/-- 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
+
+end Modal
+
+/-
+section Dynamic
+
+/-! ## Dynamic modalities  -/
+
+/-- The type `α` has a dynamic box modality with action type `β` (`[a]φ`). -/
+class HasDynamicBox (α β : Type*) where
+  /-- `b` is necessarily valid after `a`. -/
+  dynBox (a : β) (b : α) : α
+
+@[inherit_doc] scoped notation "[" a "]" φ => HasDynamicBox.dynBox a φ
+
+/-- The type `α` has a dynamic diamond modality with action type `β` (`[a]φ`). -/
+class HasDynamicDiamond (α β : Type*) where
+  /-- `b` is possibly valid after `a`. -/
+  dynDiamond (a : β) (b : α) : α
+
+@[inherit_doc] scoped notation "⟨" a "⟩" φ => HasDynamicDiamond.dynDiamond a φ
+
+end Dynamic
+-/
+
+section Linear
+
+/-! ## Linear connectives -/
+
+/-- The type `α` has a tensor connective (⊗). -/
+class HasTensor (α : Type*) where
+  /-- `a ⊗ b` is the multiplicative conjunction of `a` and `b`. -/
+  tensor (a b : α) : α
+
+@[inherit_doc] scoped infixr:35 " ⊗ " => HasTensor.tensor
+
+end Linear
+
+end Cslib.Logic

Cslib/Logics/HML/LogicalEquivalence.lean

@@ -81,6 +81,8 @@ structure Satisfies.Judgement (State : Type u) (Label : Type v) where
 /-- `Satisfies` variant using bundled judgements. -/
 def Satisfies.Bundled (j : Satisfies.Judgement State Label) := Satisfies j.lts j.state j.φ
 
+instance : HasInferenceSystem (Satisfies.Judgement World Atom) := ⟨Satisfies.Bundled⟩
+
 @[scoped grind =]
 theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl
 
@@ -102,8 +104,8 @@ instance judgementalContext :
     HasHContext (Satisfies.Judgement State Label) (Proposition Label) :=
   ⟨Satisfies.Context State Label, Satisfies.Context.fill⟩
 
-instance : LogicalEquivalence
-    (Proposition Label) (Satisfies.Judgement State Label) (Satisfies.Bundled) where
+instance : HasLogicalEquivalence
+    (Proposition Label) (Satisfies.Judgement State Label) where
   eqv := Proposition.Equiv
   eqvFillValid {a b : Proposition Label} (heqv : a.Equiv (State := State) b)
       (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label))

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -650,7 +650,7 @@ instance : Congruence (Proposition Atom) Proposition.Equiv where
     intro ctx a b hab
     induction ctx <;> grind [= Context.fill]
 
-noncomputable instance : LogicalEquivalence (Proposition Atom) (Sequent Atom) Proof where
+noncomputable instance : HasLogicalEquivalence (Proposition Atom) (Sequent Atom) where
   eqv := Proposition.Equiv
   eqvFillValid {a b : Proposition Atom} (heqv : a.Equiv b)
       (c : HasHContext.Context (Sequent Atom) (Proposition Atom))

Cslib/Logics/Modal/Basic.lean

@@ -6,7 +6,7 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
@@ -47,29 +47,51 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
-@[inherit_doc] scoped prefix:40 "¬" => Proposition.not
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond
+instance : HasNot (Proposition Atom) := {not := Proposition.not}
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond}
+
+@[scoped grind =]
+lemma Proposition.not_def (φ : Proposition Atom) : φ.not = ¬φ := rfl
+
+@[scoped grind =]
+lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : φ₁.and φ₂ = (φ₁ ∧ φ₂) := rfl
+
+@[scoped grind =]
+lemma Proposition.diamond_def (φ : Proposition Atom) : φ.diamond = (◇φ) := rfl
 
 /-- Disjunction. -/
 def Proposition.or (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬(¬φ₁ ∧ ¬φ₂)
 
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+
+@[scoped grind =]
+lemma Proposition.or_def (φ₁ φ₂ : Proposition Atom) : φ₁.or φ₂ = (φ₁ ∨ φ₂) := rfl
 
 /-- Implication. -/
-def Proposition.impl (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
+def Proposition.imp (φ₁ φ₂ : Proposition Atom) : Proposition Atom := ¬φ₁ ∨ φ₂
+
+instance : HasImp (Proposition Atom) := {imp := Proposition.imp}
 
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+@[scoped grind =]
+lemma Proposition.imp_def (φ₁ φ₂ : Proposition Atom) : φ₁.imp φ₂ = (φ₁ → φ₂) := rfl
 
 /-- Bi-implication. -/
 def Proposition.iff (φ₁ φ₂ : Proposition Atom) : Proposition Atom := (φ₁ → φ₂) ∧ (φ₂ → φ₁)
 
-@[inherit_doc] scoped infix:30 " ↔ " => Proposition.iff
+instance : HasIff (Proposition Atom) := {iff := Proposition.iff}
+
+@[scoped grind =]
+lemma Proposition.iff_def (φ₁ φ₂ : Proposition Atom) :
+    φ₁.iff φ₂ = (φ₁ ↔ φ₂) := rfl
 
 /-- Necessity. -/
 def Proposition.box (φ : Proposition Atom) : Proposition Atom := ¬◇¬φ
 
-@[inherit_doc] scoped prefix:40 "□" => Proposition.box
+instance : HasBox (Proposition Atom) := {box := Proposition.box}
+
+@[scoped grind =]
+lemma Proposition.box_def (φ : Proposition Atom) : φ.box = (□φ) := rfl
 
 /-- Satisfaction relation. `Satisfies m w φ` means that, in the model `m`, the world `w` satisfies
 the proposition `φ`. -/
@@ -107,25 +129,34 @@ theorem derivation_def {m : Model World Atom} {w : World} {φ : Proposition Atom
 
 /-- A world satisfies a proposition iff it does not satisfy the negation of the proposition. -/
 @[scoped grind =]
-theorem not_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind
+theorem Satisfies.not_iff_not : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
+
+@[scoped grind =]
+theorem Satisfies.and_iff_and {m : Model World Atom} :
+    ⇓Modal[m,w ⊨ φ₁ ∧ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∧ ⇓Modal[m,w ⊨ φ₂] := by 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
 
 /-- Characterisation of the `∨` connective.
 
 Disjunction is defined in terms of the more primitive connectives given in `Proposition`.
 This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.or_iff_or {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by grind [Proposition.or]
+    ⇓Modal[m,w ⊨ φ₁ ∨ φ₂] ↔ ⇓Modal[m,w ⊨ φ₁] ∨ ⇓Modal[m,w ⊨ φ₂] := by
+  grind [=_ Proposition.or_def, Proposition.or]
 
 /-- 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.impl_iff_impl {m : Model World Atom} :
-    ⇓Modal[m,w ⊨ φ₁ → φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] → ⇓Modal[m,w ⊨ φ₂]) := by grind [Proposition.impl]
+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.
 
@@ -134,7 +165,7 @@ This result proves that the definition is correct. -/
 @[scoped grind =]
 theorem Satisfies.iff_iff_iff {m : Model World Atom} :
     ⇓Modal[m,w ⊨ φ₁ ↔ φ₂] ↔ (⇓Modal[m,w ⊨ φ₁] ↔ ⇓Modal[m,w ⊨ φ₂]) := by
-  simp only [Proposition.iff]
+  simp only [HasIff.iff, Proposition.iff]
   grind [= derivation_def]
 
 /-- Characterisation of the `□` modality.
@@ -143,7 +174,8 @@ Necessity is defined in terms of the more primitive connectives given in `Propos
 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]
+    ⇓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 satifies. -/
 abbrev theory (m : Model World Atom) (w : World) : Set (Proposition Atom) :=
@@ -162,7 +194,7 @@ theorem satisfies_theory (h : Satisfies 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 [=_ not_satisfies]
+    ∃ φ, (⇓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. -/
@@ -174,11 +206,13 @@ theorem theoryEq_satisfies {m : Model World Atom} (h : TheoryEq m w₁ w₂)
 /-- The K axiom, valid for all models. -/
 theorem Satisfies.k : ⇓Modal[m,w ⊨ □(φ₁ → φ₂) → (□φ₁ → □φ₂)] := by grind
 
-set_option linter.tacticAnalysis.verifyGrindOnly false in
 /-- The dual axiom, valid for all models. -/
 theorem Satisfies.dual : ⇓Modal[m,w ⊨ ◇φ ↔ ¬□¬φ] := by
-  grind only [Satisfies.iff_iff_iff.mpr, → satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl,
-    =_ derivation_def, = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
+  constructor
+  · grind
+  · grind
+    --  only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def,
+    -- = not_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}
@@ -211,13 +245,13 @@ theorem Satisfies.b_symm {World Atom} {r : World → World → Prop} [Nonempty A
     have a := Classical.arbitrary Atom
     let v₁ := fun (w' : World) (a : Atom) => w' = w₁
     let h₁ := h (v := v₁) (w := w₁) (φ := .atom a)
-    simp [impl_iff_impl] at h₁
+    simp [imp_iff_imp] at h₁
     grind
 
 /-- The 4 axiom, valid for all transitive models. -/
 theorem Satisfies.four {m : Model World Atom} [IsTrans World m.r] {w : World}
     (φ : Proposition Atom) : ⇓Modal[m,w ⊨ ◇◇φ → ◇φ] := by
-  simp only [impl_iff_impl]
+  simp only [imp_iff_imp]
   intro h
   rcases h with ⟨w', h₁, w'', h₂, hs⟩
   exact ⟨w'', IsTrans.trans _ _ _ h₁ h₂, hs⟩

Cslib/Logics/Modal/Denotation.lean

@@ -18,7 +18,7 @@ A denotational semantics for modal logic, inspired by the one for Hennessy-Milne
 
 namespace Cslib.Logic.Modal
 
-open scoped Proposition InferenceSystem
+open scoped Proposition InferenceSystem Satisfies
 
 /-- Denotation of a proposition. -/
 @[simp, scoped grind =]

Cslib/Logics/Modal/LogicalEquivalence.lean

@@ -122,8 +122,8 @@ lemma Satisfies.Context.fill_def {c : Satisfies.Context World Atom} :
 open scoped Satisfies.Context
 
 /-- Logical equivalence for Modal Logic K. That is, no assumptions on models are made. -/
-instance : LogicalEquivalence
-    (Proposition Atom) (Judgement World Atom) Satisfies.Bundled where
+instance : HasLogicalEquivalence
+    (Proposition Atom) (Judgement World Atom) where
   eqv := Proposition.Equiv Set.univ
   eqvFillValid heqv c h := by
     specialize heqv c.m