feat: classes for inference systems and logical equivalence

Cslib.lean

@@ -54,6 +54,8 @@ public import Cslib.Foundations.Data.Relation
 public import Cslib.Foundations.Data.Set.Saturation
 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.Semantics.FLTS.Basic
 public import Cslib.Foundations.Semantics.FLTS.FLTSToLTS
 public import Cslib.Foundations.Semantics.FLTS.LTSToFLTS
@@ -94,6 +96,7 @@ public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.LcAt
 public import Cslib.Languages.LambdaCalculus.LocallyNameless.Untyped.Properties
 public import Cslib.Languages.LambdaCalculus.Named.Untyped.Basic
 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

Cslib/Foundations/Logic/InferenceSystem.lean

@@ -0,0 +1,52 @@
+/-
+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
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+/--
+The notation typeclass for inference systems.
+This enables the notation `⇓a`, where `a : α` is a derivable value.
+-/
+class InferenceSystem (α : Type u) where
+  /--
+  `⇓a` is a derivation of `a`, that is, a witness that `a` is derivable.
+  The meaning of this notation is type-dependent.
+  -/
+  derivation (s : α) : Sort v
+
+namespace InferenceSystem
+
+@[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation a
+
+/-- Rewrites the conclusion of a proof into an equal one. -/
+@[scoped grind =]
+def rwConclusion [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p
+
+/-- `a` is derivable if it is the conclusion of some derivation. -/
+def Derivable [InferenceSystem α] (a : α) := Nonempty (⇓a)
+
+/-- Shows derivability from a derivation. -/
+theorem Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a :=
+  Nonempty.intro d
+
+instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩
+
+/-- Extracts (noncomputably) a derivation from the fact that a conclusion is derivable. -/
+noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a :=
+  Classical.choice d
+
+noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) :=
+  ⟨Derivable.toDerivation⟩
+
+end InferenceSystem
+
+end Cslib.Logic

Cslib/Foundations/Logic/LogicalEquivalence.lean

@@ -0,0 +1,33 @@
+/-
+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.Foundations.Syntax.Context
+public import Cslib.Foundations.Syntax.Congruence
+
+@[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. -/
+  eqv_fill_valid (heqv : eqv a b) (c : HasHContext.Context Judgement Proposition)
+    (h : Valid (c<[a])) : Valid (c<[b])
+
+@[inherit_doc]
+scoped infix:29 " ≡ " => LogicalEquivalence.eqv
+
+end Cslib.Logic

Cslib/Foundations/Syntax/Congruence.lean

@@ -13,7 +13,7 @@ public import Mathlib.Algebra.Order.Monoid.Unbundled.Defs
 
 namespace Cslib
 
-/-- An equivalence relation preserved by all contexts. -/
+/-- An equivalence relation on `α` preserved by all contexts `Ctx`. -/
 class Congruence (α : Type*) [HasContext α] (r : α → α → Prop) extends
   IsEquiv α r, covariant : CovariantClass (HasContext.Context α) α (·<[·]) r
 

Cslib/Foundations/Syntax/Context.lean

@@ -12,13 +12,20 @@ public import Cslib.Init
 
 namespace Cslib
 
-/-- Class for types (`Term`) that have a notion of (single-hole) contexts (`Context`). -/
-class HasContext (Term : Sort*) where
+/-- Class for types with a canonical notion of heterogeneous single-hole contexts. -/
+class HasHContext (α β : Type*) where
   /-- The type of contexts. -/
-  Context : Sort*
-  /-- Replaces the hole in the context with a term. -/
-  fill (c : Context) (t : Term) : Term
+  Context : Type*
+  /-- Replaces the hole in the context with a value, resulting in a new value. -/
+  fill (c : Context) (b : β) : α
 
-@[inherit_doc] notation:max c "<[" t "]" => HasContext.fill c t
+@[inherit_doc] notation:max c "<[" t "]" => HasHContext.fill c t
+
+/-- Class for types (`α`) that have a canonical notion of homogeneous single-hole contexts
+(`Context`). -/
+abbrev HasContext (α : Type*) := HasHContext α α
+
+@[inherit_doc HasHContext.Context]
+def HasContext.Context (α : Type*) [HasContext α] : Type* := HasHContext.Context α α
 
 end Cslib

Cslib/Languages/CCS/Basic.lean

@@ -123,14 +123,14 @@ instance : HasContext (Process Name Constant) := ⟨Context Name Constant, Conte
 
 /-- Definition of context filling. -/
 @[scoped grind =]
-theorem hasContext_def (c : Context Name Constant) (p : Process Name Constant) :
+theorem context_fill_def (c : Context Name Constant) (p : Process Name Constant) :
   c<[p] = c.fill p := rfl
 
 /-- Any `Process` can be obtained by filling a `Context` with an atom. This proves that `Context`
 is a complete formalisation of syntactic contexts for CCS. -/
 theorem Context.complete (p : Process Name Constant) :
-    ∃ c : Context Name Constant, p = c<[Process.nil] ∨
-    ∃ k : Constant, p = c<[Process.const k] := by
+    ∃ c : Context Name Constant, p = c<[(Process.nil : Process Name Constant)] ∨
+    ∃ k : Constant, p = c<[(Process.const k : Process Name Constant)] := by
   induction p
   case nil =>
     exists hole

Cslib/Logics/HML/LogicalEquivalence.lean

@@ -0,0 +1,115 @@
+/-
+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.Logics.HML.Basic
+public import Cslib.Foundations.Logic.LogicalEquivalence
+
+@[expose] public section
+
+/-! # Logical Equivalence in HML
+
+This module defines logical equivalence for HML propositions and instantiates `LogicalEquivalence`.
+-/
+
+namespace Cslib.Logic.HML
+
+/-- Logical equivalence for HML propositions. -/
+def Proposition.Equiv {State : Type u} {Label : Type v} (a b : Proposition Label) : Prop :=
+  ∀ lts : LTS State Label, a.denotation lts = b.denotation lts
+
+@[scoped grind =]
+theorem Proposition.equiv_def {State : Type u} {Label : Type v} (a b : Proposition Label) :
+    Equiv (State := State) a b ↔
+    (∀ lts : LTS State Label, a.denotation lts = b.denotation lts) := by rfl
+
+/-- Propositional contexts. -/
+inductive Proposition.Context (Label : Type u) : Type u where
+  | hole
+  | andL (c : Context Label) (φ : Proposition Label)
+  | andR (φ : Proposition Label) (c : Context Label)
+  | orL (c : Context Label) (φ : Proposition Label)
+  | orR (φ : Proposition Label) (c : Context Label)
+  | diamond (μ : Label) (c : Context Label)
+  | box (μ : Label) (c : Context Label)
+
+/-- Replaces a hole in a propositional context with a proposition. -/
+@[scoped grind =]
+def Proposition.Context.fill (c : Context Label) (φ : Proposition Label) :=
+  match c with
+  | hole => φ
+  | andL c φ' => (c.fill φ).and φ'
+  | andR φ' c => φ'.and (c.fill φ)
+  | orL c φ' => (c.fill φ).or φ'
+  | orR φ' c => φ'.or (c.fill φ)
+  | diamond μ c => .diamond μ (c.fill φ)
+  | box μ c => .box μ (c.fill φ)
+
+instance : HasContext (Proposition Label) := ⟨Proposition.Context Label, Proposition.Context.fill⟩
+
+open scoped Proposition Proposition.Context
+
+instance : IsEquiv (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where
+  refl := by grind
+  symm := by grind
+  trans := by grind
+
+instance {State : Type u} {Label : Type v} :
+    Congruence (Proposition Label) (Proposition.Equiv (State := State) (Label := Label)) where
+  elim :
+      Covariant (Proposition.Context Label) (Proposition Label) (Proposition.Context.fill)
+      Proposition.Equiv := by
+    intro ctx a b hab lts
+    specialize hab lts
+    induction ctx
+      <;> simp only [Proposition.Context.fill, Proposition.denotation]
+      <;> grind
+
+/-- Bundled version of a judgement for `Satisfy`. -/
+structure Satisfies.Judgement (State : Type u) (Label : Type v) where
+  /-- The state transition system to consider. -/
+  lts : LTS State Label
+  /-- The state to check the proposition against. -/
+  state : State
+  /-- The proposition to check. -/
+  φ : Proposition Label
+
+/-- `Satisfies` variant using bundled judgements. -/
+def Satisfies.Bundled (j : Satisfies.Judgement State Label) := Satisfies j.lts j.state j.φ
+
+@[scoped grind =]
+theorem Satisfies.bundled_char : Satisfies.Bundled j ↔ Satisfies j.lts j.state j.φ := by rfl
+
+/-- Judgemental contexts. -/
+structure Satisfies.Context (State : Type u) (Label : Type v) where
+  /-- The state transition system to consider. -/
+  lts : LTS State Label
+  /-- The state to check propositions against. -/
+  state : State
+
+/-- Fills a judgemental context with a proposition. -/
+def Satisfies.Context.fill (c : Satisfies.Context State Label) (φ : Proposition Label) :
+    Satisfies.Judgement State Label where
+  lts := c.lts
+  state := c.state
+  φ := φ
+
+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
+  eqv := Proposition.Equiv
+  eqv_fill_valid {a b : Proposition Label} (heqv : a.Equiv (State := State) b)
+      (c : HasHContext.Context (Satisfies.Judgement State Label) (Proposition Label))
+      (h : Satisfies.Bundled c<[a]) : Satisfies.Bundled c<[b] := by
+    simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill]
+    simp only [Satisfies.bundled_char, HasHContext.fill, Satisfies.Context.fill] at h
+    grind
+
+end Cslib.Logic.HML