feat(Logic): logical operators

Cslib.lean

@@ -68,6 +68,14 @@ 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.And
+public import Cslib.Foundations.Logic.Operators.Box
+public import Cslib.Foundations.Logic.Operators.Diamond
+public import Cslib.Foundations.Logic.Operators.Iff
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Tensor
 public import Cslib.Foundations.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS

Cslib/Foundations/Logic/Operators/And.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # And connective (∧) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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
+
+end Cslib.Logic

Cslib/Foundations/Logic/Operators/Box.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Box modality (□) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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
+
+end Cslib.Logic

Cslib/Foundations/Logic/Operators/Diamond.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Diamond modality (◇) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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 Cslib.Logic

Cslib/Foundations/Logic/Operators/Iff.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Iff connective (↔) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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
+
+end Cslib.Logic

Cslib/Foundations/Logic/Operators/Impl.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Impl connective (→) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- The type `α` has an implication connective (`→`). -/
+class HasImpl (α : Type*) where
+  /-- `a → b` denotes `a` implies `b`. -/
+  impl (a b : α) : α
+
+@[inherit_doc] scoped infixr:25 " → " => HasImpl.impl
+
+end Cslib.Logic

Cslib/Foundations/Logic/Operators/Not.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Negation connective (¬) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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 Cslib.Logic

Cslib/Foundations/Logic/Operators/Or.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Or connective (∨) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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
+
+end Cslib.Logic

Cslib/Foundations/Logic/Operators/Tensor.lean

@@ -0,0 +1,24 @@
+/-
+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
+
+/-! # Tensor connective (⊗) -/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/-- 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 Cslib.Logic

Cslib/Logics/Modal/Basic.lean

@@ -6,7 +6,13 @@ Authors: Fabrizio Montesi, Marianna Girlando
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators.And
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
+public import Cslib.Foundations.Logic.Operators.Box
+public import Cslib.Foundations.Logic.Operators.Diamond
+public import Cslib.Foundations.Logic.Operators.Iff
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Mathlib.Data.Set.Basic
 public import Mathlib.Order.Defs.Unbundled
@@ -47,29 +53,51 @@ inductive Proposition (Atom : Type u) : Type u where
   /-- Possibility. -/
   | diamond (φ : Proposition Atom)
 
-@[inherit_doc] scoped prefix:40 "¬" => Proposition.neg
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped prefix:40 "◇" => Proposition.diamond
+instance : HasNot (Proposition Atom) := {not := Proposition.neg}
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasDiamond (Proposition Atom) := {diamond := Proposition.diamond}
+
+@[simp, scoped grind =]
+lemma Proposition.not_def (φ : Proposition Atom) : (¬φ) = φ.neg := rfl
+
+@[simp, scoped grind =]
+lemma Proposition.and_def (φ₁ φ₂ : Proposition Atom) : (φ₁ ∧ φ₂) = φ₁.and φ₂:= rfl
+
+@[simp, 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 := ¬φ₁ ∨ φ₂
 
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
+instance : HasImpl (Proposition Atom) := {impl := Proposition.impl}
+
+@[scoped grind =]
+lemma Proposition.impl_def (φ₁ φ₂ : Proposition Atom) : (φ₁ → φ₂) = φ₁.impl φ₂ := 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,8 +135,7 @@ 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 neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by
-  induction φ generalizing w <;> grind
+theorem neg_satisfies : ⇓Modal[m,w ⊨ ¬φ] ↔ ¬⇓Modal[m,w ⊨ φ] := by rfl
 
 /-- Characterisation of the `∨` connective.
 
@@ -164,13 +191,9 @@ 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
-  constructor
-  · grind
-  · grind only [→ satisfies_theory, usr Set.mem_setOf_eq, = impl_iff_impl, = derivation_def,
-    = neg_satisfies, Satisfies, = box_iff_forall, = Set.setOf_true]
+  constructor <;> grind
 
 /-- The T axiom, valid for all reflexive models. -/
 theorem Satisfies.t {m : Model World Atom} [instRefl : Std.Refl m.r] {w : World}

Cslib/Logics/Propositional/Defs.lean

@@ -6,7 +6,10 @@ Authors: Thomas Waring
 
 module
 
-public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators.And
+public import Cslib.Foundations.Logic.Operators.Or
+public import Cslib.Foundations.Logic.Operators.Impl
+public import Cslib.Foundations.Logic.Operators.Not
 public import Mathlib.Data.FunLike.Basic
 public import Mathlib.Data.Set.Image
 public import Mathlib.Order.TypeTags
@@ -30,8 +33,10 @@ theory.
 
 ## Notation
 
-We introduce notation for the logical connectives: `⊥ ⊤ ∧ ∨ → ¬` for, respectively, falsum, verum,
-conjunction, disjunction, implication and negation.
+We instantiate the notation classes `HasAnd`, `HasOr`, `HasImpl` and `HasNot` for `Proposition Atom`
+to give access to, respectively, the notations `∧, ∨, →` and `¬` for propositional connectives.
+In the case that `Atom` has a bottom element (respectively, is inhabited) we give instances
+`HasBot (Proposition Atom)` and (respectively, `HasTop (Proposition Atom)`).
 -/
 
 @[expose] public section
@@ -67,10 +72,10 @@ instance instTopProposition [Inhabited Atom] : Top (Proposition Atom) := ⟨.top
 
 example [Bot Atom] : (⊤ : Proposition Atom) = Proposition.impl ⊥ ⊥ := rfl
 
-@[inherit_doc] scoped infix:36 " ∧ " => Proposition.and
-@[inherit_doc] scoped infix:35 " ∨ " => Proposition.or
-@[inherit_doc] scoped infix:30 " → " => Proposition.impl
-@[inherit_doc] scoped prefix:40 " ¬ " => Proposition.neg
+instance : HasAnd (Proposition Atom) := {and := Proposition.and}
+instance : HasOr (Proposition Atom) := {or := Proposition.or}
+instance : HasImpl (Proposition Atom) := {impl := Proposition.impl}
+instance [Bot Atom] : HasNot (Proposition Atom) := {not := Proposition.neg}
 
 /-- Substitute each atom in a proposition for a proposition, possibly changing the atomic
 language. -/