feat: Tagged InferenceSystem

Cslib/Foundations/Logic/InferenceSystem.lean

@@ -14,38 +14,52 @@ namespace Cslib.Logic
 
 /--
 The notation typeclass for inference systems.
-This enables the notation `⇓a`, where `a : α` is a derivable value.
+This enables the notation `S⇓a`, where `S` is a tag for the inference system and `a : α`
+is a derivable value.
 -/
-class InferenceSystem (α : Type u) where
+class InferenceSystem (S : Type*) (α : Type*) where
   /--
-  `⇓a` is a derivation of `a`, that is, a witness that `a` is derivable.
+  `S⇓a` is a derivation of `a`, that is, a witness that `a` is derivable in the system `S`.
   The meaning of this notation is type-dependent.
   -/
-  derivation (s : α) : Sort v
+  derivation (a : α) : Sort v
+
+/-- Default tag for inference system instances. `⇓a` is short for `Default⇓a`. -/
+opaque InferenceSystem.Default : Type := Empty
+
+/-- Class for types (`α`) that have a canonical inference system. -/
+abbrev HasInferenceSystem := InferenceSystem InferenceSystem.Default
 
 namespace InferenceSystem
 
-@[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation a
+@[inherit_doc] scoped notation S:90 "⇓" a:90 => InferenceSystem.derivation S a
 
 /-- Rewrites the conclusion of a proof into an equal one. -/
 @[scoped grind =]
-def rwConclusion [InferenceSystem α] {Γ Δ : α} (h : Γ = Δ) (p : ⇓Γ) : ⇓Δ := h ▸ p
+def rwConclusion [InferenceSystem S α] {Γ Δ : α} (h : Γ = Δ) (p : S⇓Γ) : S⇓Δ :=
+  h ▸ p
 
-/-- `a` is derivable if it is the conclusion of some derivation. -/
-def Derivable [InferenceSystem α] (a : α) := Nonempty (⇓a)
+/-- `a` is derivable in `S` if it is the conclusion of some derivation. -/
+def DerivableIn S [InferenceSystem S α] (a : α) := Nonempty (S⇓a)
+
+/-- `a : α` is derivable in the default inference system for `α`. -/
+abbrev Derivable [InferenceSystem Default α] := DerivableIn Default (α := α)
 
 /-- Shows derivability from a derivation. -/
-theorem Derivable.fromDerivation [InferenceSystem α] {a : α} (d : ⇓a) : Derivable a :=
+theorem DerivableIn.fromDerivation [InferenceSystem S α] {a : α} (d : S⇓a) : DerivableIn S a :=
   Nonempty.intro d
 
-instance [InferenceSystem α] {a : α} : Coe (⇓a) (Derivable a) := ⟨Derivable.fromDerivation⟩
+instance [InferenceSystem S α] {a : α} : Coe (S⇓a) (DerivableIn S a) := ⟨DerivableIn.fromDerivation⟩
 
 /-- Extracts (noncomputably) a derivation from the fact that a conclusion is derivable. -/
-noncomputable def Derivable.toDerivation [InferenceSystem α] {a : α} (d : Derivable a) : ⇓a :=
+noncomputable def DerivableIn.toDerivation [InferenceSystem S α] {a : α} (d : DerivableIn S a) :
+    S⇓a :=
   Classical.choice d
 
-noncomputable instance [InferenceSystem α] {a : α} : Coe (Derivable a) (⇓a) :=
-  ⟨Derivable.toDerivation⟩
+noncomputable instance [InferenceSystem S α] {a : α} : Coe (DerivableIn S a) (S⇓a) :=
+  ⟨DerivableIn.toDerivation⟩
+
+@[inherit_doc] scoped notation "⇓" a:90 => InferenceSystem.derivation Default a
 
 end InferenceSystem
 

Cslib/Logics/LinearLogic/CLL/Basic.lean

@@ -205,11 +205,9 @@ inductive Proof : Sequent Atom → Type u where
   | bang {Γ : Sequent Atom} {a} : Γ.allQuest → Proof (a ::ₘ Γ) → Proof ((!a) ::ₘ Γ)
   -- No rule for zero.
 
-open Logic
+open Logic InferenceSystem
 
-instance : InferenceSystem (Sequent Atom) := ⟨Proof⟩
-
-open InferenceSystem
+instance : HasInferenceSystem (Sequent Atom) := ⟨Proof⟩
 
 /-- Convenience definition for rewriting conclusions in proofs. -/
 @[scoped grind =]
@@ -681,7 +679,7 @@ def tensor_assoc {a b c : Proposition Atom} : a ⊗ (b ⊗ c) ≡⇓ (a ⊗ b) 
      (.tensor .ax <| .tensor .ax .ax)⟩
 
 instance {Γ : Sequent Atom} : Std.Symm (fun a b => Derivable ((a ⊗ b) ::ₘ Γ)) where
-  symm _ _ h := Derivable.fromDerivation (subst_eqv_head tensor_symm (Derivable.toDerivation h))
+  symm _ _ h := DerivableIn.fromDerivation (subst_eqv_head tensor_symm (DerivableIn.toDerivation h))
 
 /-- ⊕ is idempotent. -/
 @[scoped grind ←]
@@ -699,4 +697,12 @@ 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

Cslib/Logics/LinearLogic/CLL/CutElimination.lean

@@ -14,24 +14,6 @@ namespace Cslib.Logic.CLL
 
 open Cslib.Logic.InferenceSystem
 
-/-- A proof is cut-free if it does not contain any applications of rule cut. -/
-def Proof.cutFree {Γ : Sequent Atom} (p : ⇓Γ) : Bool :=
-  match p with
-  | ax => true
-  | one => true
-  | bot p => p.cutFree
-  | parr p => p.cutFree
-  | tensor p q => p.cutFree && q.cutFree
-  | oplus₁ p => p.cutFree
-  | oplus₂ p => p.cutFree
-  | .with p q => p.cutFree && q.cutFree
-  | top => true
-  | quest p => p.cutFree
-  | weaken p => p.cutFree
-  | contract p => p.cutFree
-  | bang _ p => p.cutFree
-  | cut _ _ => false
-
 /-- A `CutFreeProof` is a `Proof` without cuts (applications of `Proof.cut`). -/
 abbrev CutFreeProof (Γ : Sequent Atom) := { q : ⇓Γ // q.cutFree }
 

Cslib/Logics/LinearLogic/CLL/MLL.lean

@@ -14,41 +14,21 @@ public import Cslib.Foundations.Logic.InferenceSystem
 /-! # Multiplicative Classical Linear Logic (MLL)
 
 Multiplicative classical linear logic, defined as a fragment of classical linear logic by means of
-`Subtype`.
+a predicate (unbundled style) and `Subtype` (bundled style).
 
-This file also serves as the reference example of how to define a fragment of an inference system
-through `Subtype`, following the next recipe.
+This file serves as the reference example of how to define a fragment of an inference system
+through tagging of `InferenceSystem` and `Subtype`, following the next recipe. It is a work in
+progress: the recipe will evolve together with how the Lean and CSLib ecosystems can
+deal with this general problem.
 
 1. Define predicates for restricting relevant types to the fragment, here `IsMLL` for propositions
 (`CLL.Proposition`) and proofs (`CLL.Proof`). This part lives under the namespace of the original
-system (here `Cslib.Logic.CLL`).
-2. Define the types in the fragment -- here `MLL.Proposition` and `MLL.Proof` -- as abbreviations of
-subtypes. This part lives under the namespace of the fragment (here `Cslib.Logic.MLL`).
+system (here `Cslib.Logic.CLL`). Custom recursors can be defined for convenient case analysis that
+automatically discharges irrelevant cases (those not in the fragment).
+2. Define the inference system in the fragment -- here `MLL.Proof` -- as an abbreviation of
+a subtype. This part lives under the namespace of the fragment (here `Cslib.Logic.CLL.MLL`).
 
 We also call the first part the 'unbundled part' and the second the 'bundled part'.
-
-This recipe has the advantage that any value (propositions, proofs, etc.) in the fragment is
-coerciable into the original system for free through `Subtype`.
-
-The main disadvantage is that the fragment does not have its own inductives, so case analysis
-requires carrying around the restricting predicate(s) as parameters to discharge irrelevant cases
-from the original system.
-This can be elegantly managed by unbundling the predicate right away, so that `match` (or similar)
-can automatically eliminate irrelevant cases.
-For example, the following definition checks that an MLL proof is cut-free:
-
-```
-/-- A proof is cut-free if it does not contain any applications of rule cut. -/
-def Proof.cutFree {Γ : Sequent Atom} (p : ⇓Γ) : Bool :=
-  go p.val p.property
-where go {Γ : CLL.Sequent Atom} (p : ⇓Γ) (hp : p.IsMLL) : Bool :=
-  match p, hp with
-  | .ax, _ => true
-  | .bot p, hp | .parr p, hp => go p hp
-  | .one, _ => true
-  | .cut _ _, _ => false
-  | .tensor p q, hp => go p hp.left && go q hp.right
-```
 -/
 
 namespace Cslib.Logic.CLL
@@ -60,12 +40,39 @@ def Proposition.IsMLL : Proposition Atom → Prop
   | tensor a b | parr a b => a.IsMLL ∧ b.IsMLL
   | _ => False
 
+/-- Recursor for MLL propositions. -/
+@[induction_eliminator, cases_eliminator, elab_as_elim]
+def Proposition.IsMLL.rec
+    {motive : {a : Proposition Atom} → (h : a.IsMLL) → Sort u}
+    (atom : ∀ x : Atom, motive (a := .atom x) (by simp))
+    (atomDual : ∀ x : Atom, motive (a := .atomDual x) (by simp))
+    (one : motive (a := .one) (by simp))
+    (bot : motive (a := .bot) (by simp))
+    (tensor : ∀ (a b : Proposition Atom) {ha : a.IsMLL} {hb : b.IsMLL},
+      motive ha → motive hb → motive (a :=.tensor a b) (by simp [ha,hb]))
+    (parr : ∀ (a b : Proposition Atom) {ha : a.IsMLL} {hb : b.IsMLL},
+      motive ha → motive hb → motive (a := .parr a b) (by simp [ha,hb]))
+    {a : Proposition Atom} (h : a.IsMLL) : motive (a := a) h :=
+  match a, h with
+  | .atom x, _ => atom x
+  | .atomDual x, _ => atomDual x
+  | .one, _ => one
+  | .bot, _ => bot
+  | .tensor a b, ⟨ha, hb⟩ =>
+    tensor a b (ha := ha) (hb := hb)
+      (Proposition.IsMLL.rec atom atomDual one bot tensor parr ha)
+      (Proposition.IsMLL.rec atom atomDual one bot tensor parr hb)
+  | .parr a b, ⟨ha, hb⟩ =>
+      parr a b
+        (Proposition.IsMLL.rec atom atomDual one bot tensor parr ha)
+        (Proposition.IsMLL.rec atom atomDual one bot tensor parr hb)
+  | .zero, h | .top, h | .oplus _ _, h | .with _ _, h
+    | .bang _, h | .quest _, h => nomatch h
+
 /-- Duality in MLL stays in MLL. -/
 @[scoped grind →]
 theorem Proposition.isMLL_dual {a : Proposition Atom} (ha : a.IsMLL) : a⫠.IsMLL := by
-  induction a with
-  | atom | atomDual | one | bot | tensor | parr => grind [dual, IsMLL]
-  | _ => grind [IsMLL]
+  induction ha <;> grind [dual, IsMLL]
 
 /-- A multiplicative propositional context. -/
 @[simp]
@@ -97,11 +104,47 @@ def Proof.IsMLL {Γ : Sequent Atom} : ⇓Γ → Prop
   | one => True
   | _ => False
 
+/-- Recursor for MLL derivations. -/
+@[induction_eliminator, cases_eliminator, elab_as_elim]
+def Proof.IsMLL.rec
+    {motive : {Γ : Sequent Atom} → {p : Proof Γ} → (h : p.IsMLL) → Sort u}
+    (ax : ∀ {a : Proposition Atom} {ha : a.IsMLL}, @motive {a, a⫠} .ax (by simp [ha]))
+    (one : @motive {Proposition.one} .one (by simp))
+    (bot : ∀ {Γ : Sequent Atom} (p : Proof Γ) {hp : p.IsMLL},
+      @motive Γ p hp → @motive (.bot ::ₘ Γ) (.bot p) (by simp [hp]))
+    (tensor : ∀ {a b : Proposition Atom} {Γ Δ : Sequent Atom}
+      (p : Proof (a ::ₘ Γ)) (q : Proof (b ::ₘ Δ)) {hp : p.IsMLL} {hq : q.IsMLL},
+      @motive (a ::ₘ Γ) p hp → @motive (b ::ₘ Δ) q hq →
+      @motive ((a ⊗ b) ::ₘ (Γ + Δ)) (.tensor p q) (by simp [hp, hq]))
+    (parr : ∀ {a b : Proposition Atom} {Γ : Sequent Atom}
+      (p : Proof (a ::ₘ b ::ₘ Γ)) {hp : p.IsMLL},
+      @motive (a ::ₘ b ::ₘ Γ) p hp → @motive ((a ⅋ b) ::ₘ Γ) (.parr p) (by simp [hp]))
+    (cut : ∀ {a : Proposition Atom} {Γ Δ : Sequent Atom}
+      (p : Proof (a ::ₘ Γ)) (q : Proof (a⫠ ::ₘ Δ)) {hp : p.IsMLL} {hq : q.IsMLL},
+      @motive (a ::ₘ Γ) p hp → @motive (a⫠ ::ₘ Δ) q hq →
+      @motive (Γ + Δ) (.cut p q) (by simp [hp, hq]))
+    {Γ : Sequent Atom} {p : Proof Γ} (h : p.IsMLL) : @motive Γ p h :=
+  match p, h with
+  | .ax (a := a), hp => @ax a (by simpa)
+  | .one, _ => one
+  | .bot p (Γ := Γ), hp => @bot Γ p hp (IsMLL.rec ax one bot tensor parr cut (p := p) hp)
+  | .tensor (a := a) (b := b) (Γ := Γ) (Δ := Δ) p q, h =>
+    @tensor a b Γ Δ p q h.left h.right
+      (IsMLL.rec ax one bot tensor parr cut h.left)
+      (IsMLL.rec ax one bot tensor parr cut h.right)
+  | .parr (a := a) (b := b) (Γ := Γ) p, hp =>
+    @parr a b Γ p hp
+      (IsMLL.rec ax one bot tensor parr cut (p := p) hp)
+  | .cut (a := a) (Γ := Γ) (Δ := Δ) p q, h =>
+    @cut a Γ Δ p q h.left h.right
+      (IsMLL.rec ax one bot tensor parr cut h.left)
+      (IsMLL.rec ax one bot tensor parr cut h.right)
+
 open scoped Sequent Proposition in
-/-- An MLL proof can only prove MLL sequents. -/
-theorem Proof.isMLL_sequent {Γ : Sequent Atom} (p : ⇓Γ) (hp : p.IsMLL) : Γ.IsMLL := by
+/-- A proof in the MLL fragment can only prove MLL sequents. -/
+theorem Proof.isMLL_sequent {Γ : Sequent Atom} {p : ⇓Γ} (h : p.IsMLL) : Γ.IsMLL := by
   -- This should be simpler, grind seems to have some trouble.
-  induction p
+  induction h
   case ax =>
     grind [Proof.IsMLL, Multiset.insert_eq_cons, Multiset.mem_singleton]
   case one =>
@@ -110,31 +153,52 @@ theorem Proof.isMLL_sequent {Γ : Sequent Atom} (p : ⇓Γ) (hp : p.IsMLL) : Γ.
   case bot Γ p ih =>
     simp
     grind [Proof.IsMLL]
-  case oplus₁ | oplus₂ | «with» | top | quest | weaken | contract | bang => contradiction
 
-end Cslib.Logic.CLL
+/-- If a CLL derivation is cut-free and concludes an MLL sequent, then it is an MLL derivation. -/
+theorem Proof.isMLL_cutFree {Γ : Sequent Atom} (p : ⇓Γ) (hΓ : Γ.IsMLL)
+    (hp : p.cutFree) : p.IsMLL := by
+  induction p
+  case ax => simp_all
+  case one => simp
+  case bot _ _ ih =>
+    refine ih ?_ hp
+    simpa using hΓ
+  case parr a b Γ p ih =>
+    refine ih ?_ hp
+    simp at hΓ
+    grind [Sequent.IsMLL]
+  case tensor a b Γ Δ p q ihp ihq =>
+    simp at hΓ
+    refine ⟨ihp ?mll.p ?cut.p, ihq ?mll.q ?cut.q⟩
+    case mll | mll => grind [Sequent.IsMLL]
+    case cut | cut => grind [cutFree]
+  case oplus₁ | oplus₂ | «with» | top | quest | contract | weaken | bang => simp at hΓ
+  case cut => simp [cutFree] at hp
 
-namespace Cslib.Logic.MLL
+/-- MLL derivations. -/
+abbrev MLL.Proof (Γ : CLL.Sequent Atom) := {p : ⇓Γ // p.IsMLL}
 
-/-- MLL propositions. -/
-abbrev Proposition (Atom : Type u) := {a : CLL.Proposition Atom // a.IsMLL}
+/-- Tag for the MLL inference system. -/
+opaque MLL : Type := Empty
 
-/-- MLL propositional contexts. -/
-abbrev Proposition.Context (Atom : Type u) := {c : CLL.Proposition.Context Atom // c.IsMLL}
+/-- MLL inference system. -/
+instance : InferenceSystem MLL (Sequent Atom) := ⟨MLL.Proof⟩
 
-/-- Filling of an MLL propositional context. -/
-def Proposition.Context.fill (c : Proposition.Context Atom) (a : Proposition Atom) :
-    Proposition Atom where
-  val := CLL.Proposition.Context.fill c a
-  property := (CLL.Proposition.Context.isMLL_fill c.property).mpr a.property
+namespace MLL
 
-/-- MLL sequents. -/
-abbrev Sequent (Atom : Type u) := {Γ : CLL.Sequent Atom // Γ.IsMLL}
+open InferenceSystem
 
-/-- MLL derivations. -/
-abbrev Proof {Atom : Type u} (Γ : Sequent Atom) := {p : CLL.Proof (Atom := Atom) Γ // p.IsMLL}
+/-- MLL proofs derive only MLL sequents. -/
+theorem Proof.isMLL_sequent {Γ : Sequent Atom} (p : MLL⇓Γ) : Γ.IsMLL :=
+  CLL.Proof.isMLL_sequent p.property
 
-/-- The sequent calculus of MLL. -/
-instance : Logic.InferenceSystem (Sequent Atom) := ⟨Proof⟩
+end MLL
 
-end Cslib.Logic.MLL
+/-- Downcasting of cut-free CLL proofs of multiplicative sequents into MLL proofs. -/
+def Proof.cutFreeToMLL {Γ : Sequent Atom} (p : ⇓Γ) (hΓ : Γ.IsMLL) (hp : p.cutFree) : MLL⇓Γ :=
+  ⟨p, CLL.Proof.isMLL_cutFree p hΓ hp⟩
+
+instance {Γ : Sequent Atom} : Coe (MLL⇓Γ) (⇓Γ) where
+  coe p := p.val
+
+end Cslib.Logic.CLL

CslibTests.lean

@@ -11,4 +11,5 @@ public import CslibTests.HasFresh
 public import CslibTests.ImportWithMathlib
 public import CslibTests.LTS
 public import CslibTests.LambdaCalculus
+public import CslibTests.MLL
 public import CslibTests.Reduction

CslibTests/MLL.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2026 Fabrizio Montesi. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Fabrizio Montesi
+-/
+
+import Cslib.Logics.LinearLogic.CLL.MLL
+
+namespace CslibTests
+
+/-! # Tests for Multiplicative Classical Linear Logic -/
+
+open Cslib.Logic.CLL Cslib.Logic.InferenceSystem
+
+open Proposition Proof Sequent
+
+-- Test the custom Proof.IsMLL recursor with induction.
+example {Γ : Sequent Atom} (p : ⇓Γ) (h : p.IsMLL) : Γ.IsMLL := by
+  induction h with
+  | ax =>
+    grind [Proof.IsMLL, Multiset.insert_eq_cons, Multiset.mem_singleton]
+  | one =>
+    simp [Sequent.IsMLL, Proposition.IsMLL]
+  | parr | tensor | cut => grind [Proposition.IsMLL, Proof.IsMLL]
+  | bot p h =>
+    simp
+    grind [Proof.IsMLL]
+
+-- Induction on a bundled MLL proof.
+example {Γ : Sequent Atom} (p : MLL⇓Γ) : Γ.IsMLL := by
+  rcases p with ⟨p, h⟩
+  induction h with
+  | ax =>
+    grind [Proof.IsMLL, Multiset.insert_eq_cons, Multiset.mem_singleton]
+  | one =>
+    simp [Sequent.IsMLL, Proposition.IsMLL]
+  | parr | tensor | cut =>
+    grind [Proposition.IsMLL, Proof.IsMLL]
+  | bot p h =>
+    simp
+    grind [Proof.IsMLL]
+
+-- Test that MLL proofs can be coerced into CLL proofs.
+example {Γ : Sequent Atom} (p : MLL⇓Γ) : ⇓Γ := (p : ⇓Γ)
+
+end CslibTests