feat(Logic/CLL): cut elimination for Classical Linear Logic (CLL)

Cslib.lean

@@ -128,6 +128,7 @@ public import Cslib.Foundations.Data.FinFun.Update
 public import Cslib.Foundations.Data.Finset.Involution
 public import Cslib.Foundations.Data.HasFresh
 public import Cslib.Foundations.Data.List.IsChainFromTo
+public import Cslib.Foundations.Data.Multiset.Grind
 public import Cslib.Foundations.Data.Nat.Asymptotics
 public import Cslib.Foundations.Data.Nat.Factorial
 public import Cslib.Foundations.Data.Nat.Segment
@@ -235,7 +236,7 @@ public import Cslib.Languages.StatefulProcesses.Basic
 public import Cslib.Languages.StatefulProcesses.Network
 public import Cslib.Logics.HML.Basic
 public import Cslib.Logics.LinearLogic.CLL.Basic
-public import Cslib.Logics.LinearLogic.CLL.CutElimination
+public import Cslib.Logics.LinearLogic.CLL.CutFree
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
 public import Cslib.Logics.LinearLogic.CLL.MLL
 public import Cslib.Logics.LinearLogic.CLL.PhaseSemantics.Basic

Cslib/Foundations/Data/Multiset/Grind.lean

@@ -0,0 +1,34 @@
+/-
+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
+public import Mathlib.Data.Multiset.AddSub
+public import Mathlib.Data.Multiset.Replicate
+
+/-! # Grind support for multisets
+
+Use `grind [multiset]` (or `grind only [multiset]`) to reason about multisets or their list
+representations. Importing this module does not add rules to the default `grind` set.
+-/
+
+public section
+
+namespace Cslib
+
+attribute [multiset _=_] Multiset.cons_coe Multiset.coe_add Multiset.singleton_add
+  Multiset.coe_eq_coe
+attribute [multiset =] Multiset.insert_eq_cons Multiset.coe_replicate
+attribute [multiset =] Multiset.cons_add Multiset.add_cons
+attribute [multiset =] Multiset.mem_cons Multiset.mem_add
+attribute [multiset =] Multiset.add_comm Multiset.add_assoc
+attribute [multiset =] Multiset.add_right_inj Multiset.add_left_inj
+attribute [multiset =] Multiset.zero_add Multiset.add_zero
+attribute [multiset .] Multiset.le_add_left Multiset.le_add_right
+attribute [multiset =] Multiset.replicate_succ
+
+end Cslib

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -211,6 +211,18 @@ instance : HasInferenceSystem (Sequent Atom) := ⟨Proof⟩
 @[scoped grind =]
 def Proof.rwConclusion {Γ Δ : Sequent Atom} (h : Γ = Δ) (p : ⇓Γ) := InferenceSystem.rwConclusion h p
 
+/-- Height of a proof. -/
+def Proof.height {Γ : Sequent Atom} : ⇓Γ → ℕ
+  | .ax | .one | .top => 1
+  | .bot p | .parr p | .oplus₁ p | .oplus₂ p
+    | .quest p | .weaken p | .contract p | .bang _ p => p.height + 1
+  | .cut p q | .tensor p q | .with p q => max p.height q.height + 1
+
+/-- Transporting a conclusion preserves proof height. -/
+@[simp, scoped grind =]
+theorem Proof.rwConclusion_height {Γ Δ : Sequent Atom} (h : Γ = Δ) (p : ⇓Γ) :
+    (p.rwConclusion h).height = p.height := by grind
+
 /-- The axiom, but where the order of propositions is reversed. -/
 @[scoped grind <=]
 def Proof.ax' {a : Proposition Atom} : ⇓({a⫠, a} : Sequent Atom) :=
@@ -594,12 +606,4 @@ end Proposition
 
 end LogicalEquiv
 
-/-- A proof is cut-free if it does not contain any applications of rule cut. -/
-def Proof.cutFree {Γ : Sequent Atom} : ⇓Γ → Bool
-  | ax | one | top => true
-  | bot p | parr p | oplus₁ p | oplus₂ p
-    | quest p | weaken p | contract p | bang _ p => p.cutFree
-  | tensor p q | .with p q => p.cutFree && q.cutFree
-  | cut _ _ => false
-
 end Cslib.Logic.CLL