feat(Logic): logical operators

Cslib.lean

@@ -71,6 +71,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.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/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/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))