feat(Logic): improvements to the inference system and congruence frameworks, with associated refactorings

Cslib.lean

@@ -79,6 +79,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/InferenceSystem.lean

@@ -8,7 +8,15 @@ module
 
 public import Cslib.Init
 
-/-! -/
+/-! # Inference systems
+
+This module defines the basic classes and notation for *inference systems* -- systems for deriving
+conclusions from premises.
+
+We intend inference systems broadly, as in theory of programming languages. In applications to
+logic, for example, we use inference systems to capture both the concepts of satisfiability and
+proof systems.
+-/
 
 @[expose] public section
 
@@ -63,6 +71,17 @@ noncomputable instance [InferenceSystem S α] {a : α} : Coe (DerivableIn S a) (
 
 @[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation Default a
 
+open Lean Elab PrettyPrinter Delaborator SubExpr in
+/-- Delaborator that hides `InferenceSystem.Default` in uses of the `⇓a` notation. -/
+@[app_delab InferenceSystem.derivation]
+meta def delabInferenceSystem : Delab := do
+  let expr ← getExpr
+  if expr.getAppArgs[0]?.any (·.isConstOf `Cslib.Logic.InferenceSystem.Default) then
+    let a ← withAppArg delab
+    `(⇓ $a)
+  else
+    delabApp
+
 end InferenceSystem
 
 end Cslib.Logic

Cslib/Foundations/Logic/LogicalEquivalence.lean

@@ -8,28 +8,23 @@ 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
 
-/-- 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
-    (Proposition : Type u) [HasContext Proposition]
-    (Judgement : Type v) [HasHContext Judgement Proposition]
-    (Valid : Judgement → Sort w) where
-  /-- The logical equivalence relation. -/
-  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])
+open scoped InferenceSystem
 
-@[inherit_doc]
-scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+/-- A logical equivalence `eqv` for an inference system `S` is a congruence on propositions (of type
+`α`) that preserves validity of judgements under any judgemental context. -/
+class LogicalEquivalence S (eqv : α → α → Prop)
+    [HasContext α] [Congruence eqv] [HasHContext Judgement α] [InferenceSystem S Judgement]
+    extends LawfulCongruence eqv where
+  /-- Validity is preserved for any judgemental context. -/
+  eqvFillValid (heqv : a ≡[eqv] b) (c : HasHContext.Context Judgement α)
+    (h : S⇓(c<[a])) : S⇓(c<[b])
 
 end Cslib.Logic

Cslib/Foundations/Logic/Operators.lean

@@ -0,0 +1,120 @@
+/-
+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
+
+Here we need to use the prefix `d` to distinguish our notation from the normal `[·]` and `⟨·⟩`.
+A refactoring that makes this unnecessary would be welcome.
+-/
+
+/-- The type `α` has a dynamic box modality with action type `β` (`d[a]φ`). -/
+class HasDynamicBox (α β : Type*) where
+  /-- `b` is necessarily valid after `a`. -/
+  dynBox (a : β) (b : α) : α
+
+@[inherit_doc] scoped notation "d[" a "]" φ => 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 : α) : α
+
+@[inherit_doc] scoped notation "d⟨" 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/Foundations/Syntax/Congruence.lean

@@ -15,8 +15,36 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 
 namespace Cslib
 
-/-- An equivalence relation on `α` preserved by all contexts `Ctx`. -/
-class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
-  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
+/-- The relation `r` is a congruence on `α`. This class gives access to the `≡[r]` notation.
+To instantiate a canonical congruence for `α`, see `HasCongruence`.
+
+Congruence relations should also instantiate `LawfulCongruence` to prove that the relation respects
+the expected congruence laws. -/
+class Congruence (r : α → α → Prop)
+
+/-- `a ≡[r] b` means that the `a` and `b` are related by the congruence `r`. -/
+@[nolint unusedArguments]
+def Congruence.r (r : α → α → Prop) [Congruence r] := r
+
+@[inherit_doc]
+scoped notation:29 a " ≡[" r "] " b => Congruence.r r a b
+
+/-- The type `α` has a canonical congruence relation. This gives access to the `≡` notation. -/
+class DefaultCongruence (α : Type*) (r : outParam (α → α → Prop))
+
+/-- `a ≡ b` means that `a` and `b` are related by the canonical congruence relation for their
+type. -/
+@[nolint unusedArguments]
+def DefaultCongruence.r {α : Type*} {r : α → α → Prop} [DefaultCongruence α r] (a b : α) := r a b
+
+@[inherit_doc]
+scoped infix:29 " ≡ " => DefaultCongruence.r
+
+@[nolint unusedArguments]
+instance (α : Type*) (r : α → α → Prop) [DefaultCongruence α r] : Congruence r := ⟨⟩
+
+/-- An equivalence relation on `α` preserved by all contexts. -/
+class LawfulCongruence (r : α → α → Prop) [Congruence r] [HasContext α] extends
+  IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) (· ≡[r] ·)
 
 end Cslib

Cslib/Foundations/Syntax/Context.lean

@@ -17,7 +17,7 @@ namespace Cslib
 /-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/
 class HasHContext (α β : Type*) where
   /-- The type of contexts. -/
-  Context : Type*
+  {Context : Type*}
   /-- Replaces the hole in the context with a value, resulting in a new value. -/
   fill (c : Context) (b : β) : α
 

Cslib/Languages/CCS/Basic.lean

@@ -119,7 +119,7 @@ def Context.fill (c : Context Name Constant) (p : Process Name Constant) : Proce
   | choiceR r c => Process.choice r (c.fill p)
   | res a c => Process.res a (c.fill p)
 
-instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Context.fill⟩
+instance : HasContext (Process Name Constant) := ⟨Context.fill⟩
 
 /-- Definition of context filling. -/
 @[scoped grind =]

Cslib/Languages/CCS/BehaviouralTheory.lean

@@ -441,10 +441,14 @@ theorem bisimilarity_is_congruence
   | _ => grind [bisimilarity_congr_pre, bisimilarity_congr_par,
                 bisimilarity_congr_choice, bisimilarity_congr_res]
 
+instance : Congruence (HomBisimilarity (lts (defs := defs))) := ⟨⟩
+
 /-- Bisimilarity is a congruence in CCS. -/
 instance bisimilarityCongruence :
-    Congruence (Process Name Constant) (HomBisimilarity (lts (defs := defs))) where
-  covariant := ⟨by grind [Covariant, bisimilarity_is_congruence]⟩
+    LawfulCongruence (HomBisimilarity (lts (defs := defs))) where
+  elim := by
+    dsimp [Congruence.r]
+    grind [Covariant, bisimilarity_is_congruence]
 
 end CCS