Multiplicative Classical Linear Logic (MLL)

Multiplicative classical linear logic, defined as a fragment of classical linear logic by means of a predicate (unbundled style) and Subtype (bundled style).

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). 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'.

def Cslib.Logic.CLL.Proposition.IsMLL {Atom : Type u_1} : Proposition Atom → Prop

A proposition is in the multiplicative fragment of CLL.

Equations

• (Cslib.Logic.CLL.Proposition.atom x_1).IsMLL = True
• (Cslib.Logic.CLL.Proposition.atomDual x_1).IsMLL = True
• Cslib.Logic.CLL.Proposition.one.IsMLL = True
• Cslib.Logic.CLL.Proposition.bot.IsMLL = True
• (a.tensor b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• (a.parr b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• x✝.IsMLL = False

def Cslib.Logic.CLL.Proposition.IsMLL.rec {Atom : Type u_1} {motive : {a : Proposition Atom} → a.IsMLL → Sort u} (atom : (x : Atom) → motive ⋯) (atomDual : (x : Atom) → motive ⋯) (one : motive ⋯) (bot : motive ⋯) (tensor : (a b : Proposition Atom) → {ha : a.IsMLL} → {hb : b.IsMLL} → motive ha → motive hb → motive ⋯) (parr : (a b : Proposition Atom) → {ha : a.IsMLL} → {hb : b.IsMLL} → motive ha → motive hb → motive ⋯) {a : Proposition Atom} (h : a.IsMLL) : motive h

Recursor for MLL propositions.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.CLL.Proposition.IsMLL.rec atom atomDual one bot tensor parr x_1 = atom x
• Cslib.Logic.CLL.Proposition.IsMLL.rec atom atomDual one bot tensor parr x_1 = atomDual x
• Cslib.Logic.CLL.Proposition.IsMLL.rec atom atomDual one bot tensor parr x = one
• Cslib.Logic.CLL.Proposition.IsMLL.rec atom atomDual one bot tensor parr x = bot

theorem Cslib.Logic.CLL.Proposition.isMLL_dual {Atom : Type u_1} {a : Proposition Atom} (ha : a.IsMLL) : a.dual.IsMLL

Duality in MLL stays in MLL.

def Cslib.Logic.CLL.Proposition.Context.IsMLL {Atom : Type u_1} : Context Atom → Prop

A multiplicative propositional context.

Equations

• Cslib.Logic.CLL.Proposition.Context.hole.IsMLL = True
• (a.tensorL b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• (Cslib.Logic.CLL.Proposition.Context.tensorR a b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• (a.parrL b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• (Cslib.Logic.CLL.Proposition.Context.parrR a b).IsMLL = (a.IsMLL ∧ b.IsMLL)
• x✝.IsMLL = False

theorem Cslib.Logic.CLL.Proposition.Context.isMLL_fill {Atom : Type u_1} {c : Context Atom} {a : Proposition Atom} (hc : c.IsMLL) : (c.fill a).IsMLL ↔ a.IsMLL

Filling a multiplicative propositional context with a multiplicative proposition stays in MLL.

def Cslib.Logic.CLL.Sequent.IsMLL {Atom : Type u_1} (Γ : Sequent Atom) : Prop

A multiplicative sequent.

Equations

• Γ.IsMLL = ∀ (a : Cslib.Logic.CLL.Proposition Atom), a ∈ Γ → a.IsMLL

def Cslib.Logic.CLL.Proof.IsMLL {Atom : Type u_1} {Γ : Sequent Atom} : InferenceSystem.derivation InferenceSystem.Default Γ → Prop

A proof is in MLL.

Equations

• Cslib.Logic.CLL.Proof.ax.IsMLL = a.IsMLL
• a.bot.IsMLL = a.IsMLL
• a_1.parr.IsMLL = a_1.IsMLL
• (p.cut q).IsMLL = (p.IsMLL ∧ q.IsMLL)
• (p.tensor q).IsMLL = (p.IsMLL ∧ q.IsMLL)
• Cslib.Logic.CLL.Proof.one.IsMLL = True
• Cslib.Logic.CLL.Proof.IsMLL x✝ = False

def Cslib.Logic.CLL.Proof.IsMLL.rec {Atom : Type u_1} {motive : {Γ : Sequent Atom} → {p : Proof Γ} → p.IsMLL → Sort u} (ax : {a : Proposition Atom} → {ha : a.IsMLL} → motive ha) (one : motive ⋯) (bot : {Γ : Sequent Atom} → (p : Proof Γ) → {hp : p.IsMLL} → motive hp → motive hp) (tensor : {a b : Proposition Atom} → {Γ Δ : Sequent Atom} → (p : Proof (a ::ₘ Γ)) → (q : Proof (b ::ₘ Δ)) → {hp : p.IsMLL} → {hq : q.IsMLL} → motive hp → motive hq → motive ⋯) (parr : {a b : Proposition Atom} → {Γ : Sequent Atom} → (p : Proof (a ::ₘ b ::ₘ Γ)) → {hp : p.IsMLL} → motive hp → motive hp) (cut : {a : Proposition Atom} → {Γ Δ : Sequent Atom} → (p : Proof (a ::ₘ Γ)) → (q : Proof (a.dual ::ₘ Δ)) → {hp : p.IsMLL} → {hq : q.IsMLL} → motive hp → motive hq → motive ⋯) {Γ : Sequent Atom} {p : Proof Γ} (h : p.IsMLL) : motive h

Recursor for MLL derivations.

Equations

• One or more equations did not get rendered due to their size.
• Cslib.Logic.CLL.Proof.IsMLL.rec ax one bot tensor parr cut hp = ax
• Cslib.Logic.CLL.Proof.IsMLL.rec ax one bot tensor parr cut x = one

theorem Cslib.Logic.CLL.Proof.isMLL_sequent {Atom : Type u_1} {Γ : Sequent Atom} {p : InferenceSystem.derivation InferenceSystem.Default Γ} (h : IsMLL p) : Γ.IsMLL

A proof in the MLL fragment can only prove MLL sequents.

theorem Cslib.Logic.CLL.Proof.isMLL_cutFree {Atom : Type u_1} {Γ : Sequent Atom} (p : InferenceSystem.derivation InferenceSystem.Default Γ) (hΓ : Γ.IsMLL) (hp : cutFree p = true) : IsMLL p

If a CLL derivation is cut-free and concludes an MLL sequent, then it is an MLL derivation.

@[reducible, inline]

abbrev Cslib.Logic.CLL.MLL.Proof {Atom : Type u_1} (Γ : Sequent Atom) : Type u_1

MLL derivations.

Equations

• Cslib.Logic.CLL.MLL.Proof Γ = { p : Cslib.Logic.InferenceSystem.derivation Cslib.Logic.InferenceSystem.Default Γ // Cslib.Logic.CLL.Proof.IsMLL p }

opaque Cslib.Logic.CLL.MLL : Type

Tag for the MLL inference system.

@[implicit_reducible]

instance Cslib.Logic.CLL.instInferenceSystemMLLSequent {Atom : Type u_1} : InferenceSystem MLL (Sequent Atom)

MLL inference system.

Equations

• Cslib.Logic.CLL.instInferenceSystemMLLSequent = { derivation := Cslib.Logic.CLL.MLL.Proof }

theorem Cslib.Logic.CLL.MLL.Proof.isMLL_sequent {Atom : Type u_1} {Γ : Sequent Atom} (p : InferenceSystem.derivation MLL Γ) : Γ.IsMLL

MLL proofs derive only MLL sequents.

def Cslib.Logic.CLL.Proof.cutFreeToMLL {Atom : Type u_1} {Γ : Sequent Atom} (p : InferenceSystem.derivation InferenceSystem.Default Γ) (hΓ : Γ.IsMLL) (hp : cutFree p = true) : InferenceSystem.derivation MLL Γ

Downcasting of cut-free CLL proofs of multiplicative sequents into MLL proofs.

Equations

• Cslib.Logic.CLL.Proof.cutFreeToMLL p hΓ hp = ⟨p, ⋯⟩

@[implicit_reducible]

instance Cslib.Logic.CLL.instCoeDerivationMLLSequentDefault {Atom : Type u_1} {Γ : Sequent Atom} : Coe (InferenceSystem.derivation MLL Γ) (InferenceSystem.derivation InferenceSystem.Default Γ)

Equations

• Cslib.Logic.CLL.instCoeDerivationMLLSequentDefault = { coe := fun (p : Cslib.Logic.InferenceSystem.derivation Cslib.Logic.CLL.MLL Γ) => ↑p }