Classical Linear Logic

TODO

• First-order polymorphism.
• Cut elimination.

References

• J.-Y. Girard, Linear Logic: its syntax and semantics

inductive CLL.Proposition (Atom : Type u) : Type u

Propositions.

• atom {Atom : Type u} (x : Atom) : Proposition Atom
• atomDual {Atom : Type u} (x : Atom) : Proposition Atom
• one {Atom : Type u} : Proposition Atom
• zero {Atom : Type u} : Proposition Atom
• top {Atom : Type u} : Proposition Atom
• bot {Atom : Type u} : Proposition Atom
• tensor {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  The multiplicative conjunction connective.

• parr {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  The multiplicative disjunction connective.

• oplus {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  The additive disjunction connective.

• with {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

  The additive conjunction connective.

• bang {Atom : Type u} (a : Proposition Atom) : Proposition Atom

  The "of course" exponential.

• quest {Atom : Type u} (a : Proposition Atom) : Proposition Atom

  The "why not" exponential. This is written as ʔ, or _?, to distinguish itself from the lean syntatical hole ? syntax

instance CLL.instDecidableEqProposition {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Proposition Atom✝)

Equations

• CLL.instDecidableEqProposition = CLL.instDecidableEqProposition.decEq

def CLL.instDecidableEqProposition.decEq {Atom✝ : Type u_1} [DecidableEq Atom✝] (x✝ x✝¹ : Proposition Atom✝) : Decidable (x✝ = x✝¹)

instance CLL.instBEqProposition {Atom✝ : Type u_1} [BEq Atom✝] : BEq (Proposition Atom✝)

Equations

• CLL.instBEqProposition = { beq := CLL.instBEqProposition.beq }

def CLL.instBEqProposition.beq {Atom✝ : Type u_1} [BEq Atom✝] : Proposition Atom✝ → Proposition Atom✝ → Bool

Equations

• CLL.instBEqProposition.beq (CLL.Proposition.atom a) (CLL.Proposition.atom b) = (a == b)
• CLL.instBEqProposition.beq (CLL.Proposition.atomDual a) (CLL.Proposition.atomDual b) = (a == b)
• CLL.instBEqProposition.beq CLL.Proposition.one CLL.Proposition.one = true
• CLL.instBEqProposition.beq CLL.Proposition.zero CLL.Proposition.zero = true
• CLL.instBEqProposition.beq CLL.Proposition.top CLL.Proposition.top = true
• CLL.instBEqProposition.beq CLL.Proposition.bot CLL.Proposition.bot = true
• CLL.instBEqProposition.beq (a.tensor a_1) (b.tensor b_1) = (CLL.instBEqProposition.beq a b && CLL.instBEqProposition.beq a_1 b_1)
• CLL.instBEqProposition.beq (a.parr a_1) (b.parr b_1) = (CLL.instBEqProposition.beq a b && CLL.instBEqProposition.beq a_1 b_1)
• CLL.instBEqProposition.beq (a.oplus a_1) (b.oplus b_1) = (CLL.instBEqProposition.beq a b && CLL.instBEqProposition.beq a_1 b_1)
• CLL.instBEqProposition.beq (a.with a_1) (b.with b_1) = (CLL.instBEqProposition.beq a b && CLL.instBEqProposition.beq a_1 b_1)
• CLL.instBEqProposition.beq a.bang b.bang = CLL.instBEqProposition.beq a b
• CLL.instBEqProposition.beq a.quest b.quest = CLL.instBEqProposition.beq a b
• CLL.instBEqProposition.beq x✝¹ x✝ = false

instance CLL.instZeroProposition {Atom : Type u} : Zero (Proposition Atom)

Equations

• CLL.instZeroProposition = { zero := CLL.Proposition.zero }

instance CLL.instOneProposition {Atom : Type u} : One (Proposition Atom)

Equations

• CLL.instOneProposition = { one := CLL.Proposition.one }

instance CLL.instTopProposition {Atom : Type u} : Top (Proposition Atom)

Equations

• CLL.instTopProposition = { top := CLL.Proposition.top }

instance CLL.instBotProposition {Atom : Type u} : Bot (Proposition Atom)

Equations

• CLL.instBotProposition = { bot := CLL.Proposition.bot }

def CLL.«term_⊗_» : Lean.TrailingParserDescr

The multiplicative conjunction connective.

Equations

• CLL.«term_⊗_» = Lean.ParserDescr.trailingNode `CLL.«term_⊗_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊗ ") (Lean.ParserDescr.cat `term 36))

def CLL.«term_⊕_» : Lean.TrailingParserDescr

The additive disjunction connective.

Equations

• CLL.«term_⊕_» = Lean.ParserDescr.trailingNode `CLL.«term_⊕_» 35 36 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊕ ") (Lean.ParserDescr.cat `term 36))

def CLL.term_⅋_ : Lean.TrailingParserDescr

The multiplicative disjunction connective.

Equations

• CLL.term_⅋_ = Lean.ParserDescr.trailingNode `CLL.term_⅋_ 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⅋ ") (Lean.ParserDescr.cat `term 31))

def CLL.«term_&_» : Lean.TrailingParserDescr

The additive conjunction connective.

Equations

• CLL.«term_&_» = Lean.ParserDescr.trailingNode `CLL.«term_&_» 30 31 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " & ") (Lean.ParserDescr.cat `term 31))

def CLL.term!_ : Lean.ParserDescr

The "of course" exponential.

Equations

• CLL.term!_ = Lean.ParserDescr.node `CLL.term!_ 95 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "!") (Lean.ParserDescr.cat `term 95))

def CLL.«termʔ_» : Lean.ParserDescr

The "why not" exponential. This is written as ʔ, or _?, to distinguish itself from the lean syntatical hole ? syntax

Equations

• CLL.«termʔ_» = Lean.ParserDescr.node `CLL.«termʔ_» 95 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "ʔ") (Lean.ParserDescr.cat `term 95))

def CLL.Proposition.Pos {Atom : Type u} : Proposition Atom → Prop

Positive propositions.

Equations

• (CLL.Proposition.atom x_1).Pos = True
• CLL.Proposition.one.Pos = True
• CLL.Proposition.zero.Pos = True
• (a.tensor b).Pos = True
• (a.oplus b).Pos = True
• a.bang.Pos = True
• x✝.Pos = False

def CLL.Proposition.Neg {Atom : Type u} : Proposition Atom → Prop

Negative propositions.

Equations

• (CLL.Proposition.atomDual x_1).Neg = True
• CLL.Proposition.bot.Neg = True
• CLL.Proposition.top.Neg = True
• (a.parr b).Neg = True
• (a.with b).Neg = True
• a.quest.Neg = True
• x✝.Neg = False

def CLL.Proposition.dual {Atom : Type u} : Proposition Atom → Proposition Atom

Propositional duality.

Equations

• (CLL.Proposition.atom x_1).dual = CLL.Proposition.atomDual x_1
• (CLL.Proposition.atomDual x_1).dual = CLL.Proposition.atom x_1
• CLL.Proposition.one.dual = CLL.Proposition.bot
• CLL.Proposition.bot.dual = CLL.Proposition.one
• CLL.Proposition.zero.dual = CLL.Proposition.top
• CLL.Proposition.top.dual = CLL.Proposition.zero
• (a.tensor b).dual = a.dual.parr b.dual
• (a.parr b).dual = a.dual.tensor b.dual
• (a.oplus b).dual = a.dual.with b.dual
• (a.with b).dual = a.dual.oplus b.dual
• a.bang.dual = a.dual.quest
• a.quest.dual = a.dual.bang

def CLL.«term_⫠» : Lean.TrailingParserDescr

Propositional duality.

Equations

• CLL.«term_⫠» = Lean.ParserDescr.trailingNode `CLL.«term_⫠» 1024 1024 (Lean.ParserDescr.symbol "⫠")

theorem CLL.Proposition.dual.neq {Atom : Type u} (a : Proposition Atom) : a ≠ a.dual

No proposition is equal to its dual.

@[simp]

theorem CLL.Proposition.dual_inj {Atom : Type u} (a b : Proposition Atom) : a.dual = b.dual ↔ a = b

Two propositions are equal iff their respective duals are equal.

@[simp]

theorem CLL.Proposition.dual.involution {Atom : Type u} (a : Proposition Atom) : a.dual.dual = a

Duality is an involution.

def CLL.Proposition.linImpl {Atom : Type u} (a b : Proposition Atom) : Proposition Atom

Linear implication.

Equations

• a.linImpl b = a.dual.parr b

def CLL.«term_⊸_» : Lean.TrailingParserDescr

Linear implication.

Equations

• CLL.«term_⊸_» = Lean.ParserDescr.trailingNode `CLL.«term_⊸_» 25 26 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊸ ") (Lean.ParserDescr.cat `term 26))

@[reducible, inline]

abbrev CLL.Sequent (Atom : Type u_1) : Type u_1

A sequent in CLL is a list of propositions.

Equations

• CLL.Sequent Atom = List (CLL.Proposition Atom)

def CLL.Sequent.AllQuest {Atom : Type u} (Γ : Sequent Atom) : Prop

Checks that all propositions in Γ are question marks.

Equations

• Γ.AllQuest = ∀ (a : CLL.Proposition Atom), a ∈ Γ → ∃ (b : CLL.Proposition Atom), a = b.quest

inductive CLL.Proof {Atom : Type u} : Sequent Atom → Type u

A proof in the sequent calculus for classical linear logic.

• ax {Atom : Type u} {a : Proposition Atom} : Proof [a, a.dual]
• cut {Atom : Type u} {a : Proposition Atom} {Γ Δ : List (Proposition Atom)} : Proof (a :: Γ) → Proof (a.dual :: Δ) → Proof (Γ ++ Δ)
• exchange {Atom : Type u} {Γ Δ : List (Proposition Atom)} : Γ.Perm Δ → Proof Γ → Proof Δ
• one {Atom : Type u} : Proof [1]
• bot {Atom : Type u} {Γ : Sequent Atom} : Proof Γ → Proof (⊥ :: Γ)
• parr {Atom : Type u} {a b : Proposition Atom} {Γ : List (Proposition Atom)} : Proof (a :: b :: Γ) → Proof (a.parr b :: Γ)
• tensor {Atom : Type u} {a : Proposition Atom} {Γ : List (Proposition Atom)} {b : Proposition Atom} {Δ : List (Proposition Atom)} : Proof (a :: Γ) → Proof (b :: Δ) → Proof (a.tensor b :: (Γ ++ Δ))
• oplus₁ {Atom : Type u} {a : Proposition Atom} {Γ : List (Proposition Atom)} {b : Proposition Atom} : Proof (a :: Γ) → Proof (a.oplus b :: Γ)
• oplus₂ {Atom : Type u} {b : Proposition Atom} {Γ : List (Proposition Atom)} {a : Proposition Atom} : Proof (b :: Γ) → Proof (a.oplus b :: Γ)
• with {Atom : Type u} {a : Proposition Atom} {Γ : List (Proposition Atom)} {b : Proposition Atom} : Proof (a :: Γ) → Proof (b :: Γ) → Proof (a.with b :: Γ)
• top {Atom : Type u} {Γ : List (Proposition Atom)} : Proof (⊤ :: Γ)
• quest {Atom : Type u} {a : Proposition Atom} {Γ : List (Proposition Atom)} : Proof (a :: Γ) → Proof (a.quest :: Γ)
• weaken {Atom : Type u} {Γ : Sequent Atom} {a : Proposition Atom} : Proof Γ → Proof (a.quest :: Γ)
• contract {Atom : Type u} {a : Proposition Atom} {Γ : List (Proposition Atom)} : Proof (a.quest :: a.quest :: Γ) → Proof (a.quest :: Γ)
• bang {Atom : Type u} {Γ : Sequent Atom} {a : Proposition Atom} : Γ.AllQuest → Proof (a :: Γ) → Proof (a.bang :: Γ)

def CLL.Provable {Atom : Type u} (Γ : Sequent Atom) : Prop

A sequent is provable if there exists a proof that concludes it.

Equations

• CLL.Provable Γ = Nonempty (CLL.Proof Γ)

def CLL.«term⇓_» : Lean.ParserDescr

A proof in the sequent calculus for classical linear logic.

Equations

• CLL.«term⇓_» = Lean.ParserDescr.node `CLL.«term⇓_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⇓") (Lean.ParserDescr.cat `term 90))

def CLL.«term⊢_» : Lean.ParserDescr

A sequent is provable if there exists a proof that concludes it.

Equations

• CLL.«term⊢_» = Lean.ParserDescr.node `CLL.«term⊢_» 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊢") (Lean.ParserDescr.cat `term 90))

def CLL.Provable.fromProof {Atom : Type u} {Γ : Sequent Atom} (p : Proof Γ) : Provable Γ

Having a proof of Γ shows that it is provable.

Equations

• ⋯ = ⋯

noncomputable def CLL.Provable.toProof {Atom : Type u} {Γ : Sequent Atom} (p : Provable Γ) : Proof Γ

Having a proof of Γ shows that it is provable.

Equations

• p.toProof = Classical.choice p

instance CLL.instCoeProofProvable {Atom✝ : Type u_1} {Γ : Sequent Atom✝} : Coe (Proof Γ) (Provable Γ)

Equations

• CLL.instCoeProofProvable = { coe := ⋯ }

noncomputable instance CLL.instCoeProvableProof {Atom✝ : Type u_1} {Γ : Sequent Atom✝} : Coe (Provable Γ) (Proof Γ)

Equations

• CLL.instCoeProvableProof = { coe := fun (p : CLL.Provable Γ) => p.toProof }

def CLL.Proof.ax' {Atom : Type u} {a : Proposition Atom} : Proof [a.dual, a]

The axiom, but where the order of propositions is reversed.

Equations

• CLL.Proof.ax' = CLL.Proof.exchange ⋯ CLL.Proof.ax

def CLL.Proof.cut' {Atom✝ : Type u_1} {a : Proposition Atom✝} {Γ Δ : List (Proposition Atom✝)} (p : Proof (a.dual :: Γ)) (q : Proof (a :: Δ)) : Proof (Γ ++ Δ)

Cut, but where the premises are reversed.

Equations

• p.cut' q = p.cut (⋯.mp q)

def CLL.Proof.parr_inversion {Atom : Type u} {a b : Proposition Atom} {Γ : Sequent Atom} (h : Proof (a.parr b :: Γ)) : Proof (a :: b :: Γ)

Inversion of the ⅋ rule.

Equations

• h.parr_inversion = (CLL.Proof.ax'.tensor CLL.Proof.ax').cut' h

def CLL.Proof.bot_inversion {Atom : Type u} {Γ : Sequent Atom} (h : Proof (⊥ :: Γ)) : Proof Γ

Inversion of the ⊥ rule.

Equations

• h.bot_inversion = CLL.Proof.one.cut' h

def CLL.Proof.with_inversion₁ {Atom : Type u} {a b : Proposition Atom} {Γ : Sequent Atom} (h : Proof (a.with b :: Γ)) : Proof (a :: Γ)

Inversion of the & rule, first component.

Equations

• h.with_inversion₁ = CLL.Proof.ax'.oplus₁.cut' h

def CLL.Proof.with_inversion₂ {Atom : Type u} {a b : Proposition Atom} {Γ : Sequent Atom} (h : Proof (a.with b :: Γ)) : Proof (b :: Γ)

Inversion of the & rule, second component.

Equations

• h.with_inversion₂ = CLL.Proof.ax'.oplus₂.cut' h

Logical equivalences

def CLL.Proposition.equiv {Atom : Type u} (a b : Proposition Atom) : Type u

Two propositions are equivalent if one implies the other and vice versa. Proof-relevant version.

Equations

• a.equiv b = (CLL.Proof [a.dual, b] × CLL.Proof [b.dual, a])

def CLL.Proposition.Equiv {Atom : Type u} (a b : Proposition Atom) : Prop

Propositional equivalence, proof-irrelevant version (Prop).

Equations

• a.Equiv b = (CLL.Provable [a.dual, b] ∧ CLL.Provable [b.dual, a])

theorem CLL.Proposition.equiv.toProp {Atom✝ : Type u_1} {a b : Proposition Atom✝} (h : a.equiv b) : a.Equiv b

Conversion from proof-relevant to proof-irrelevant versions of propositional equivalence.

instance CLL.instCoeEquivEquiv {Atom : Type u} {a b : Proposition Atom} : Coe (a.equiv b) (a.Equiv b)

Equations

• CLL.instCoeEquivEquiv = { coe := ⋯ }

def CLL.«term_≡_» : Lean.TrailingParserDescr

Equations

• CLL.«term_≡_» = Lean.ParserDescr.trailingNode `CLL.«term_≡_» 29 30 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≡ ") (Lean.ParserDescr.cat `term 30))

def CLL.Proposition.equiv.refl {Atom : Type u} (a : Proposition Atom) : a.equiv a

Equations

• CLL.Proposition.equiv.refl a = (CLL.Proof.exchange ⋯ CLL.Proof.ax, CLL.Proof.exchange ⋯ CLL.Proof.ax)

theorem CLL.Proposition.Equiv.refl {Atom : Type u} (a : Proposition Atom) : a.Equiv a

theorem CLL.Proposition.Equiv.symm {Atom : Type u} {a b : Proposition Atom} (h : a.Equiv b) : b.Equiv a

theorem CLL.Proposition.Equiv.trans {Atom : Type u} {a b c : Proposition Atom} (hab : a.Equiv b) (hbc : b.Equiv c) : a.Equiv c

def CLL.Proposition.propositionSetoid {Atom : Type u} : Setoid (Proposition Atom)

The canonical equivalence relation for propositions.

Equations

• CLL.Proposition.propositionSetoid = { r := CLL.Proposition.Equiv, iseqv := ⋯ }

theorem CLL.Proposition.bang_top_eqv_one {Atom : Type u} : ⊤.bang.Equiv 1

theorem CLL.Proposition.quest_zero_eqv_bot {Atom : Type u} : (quest 0).Equiv ⊥

theorem CLL.Proposition.tensor_zero_eqv_zero {Atom : Type u} (a : Proposition Atom) : (a.tensor 0).Equiv 0

theorem CLL.Proposition.parr_top_eqv_top {Atom : Type u} (a : Proposition Atom) : (a.parr ⊤).Equiv ⊤

theorem CLL.Proposition.tensor_distrib_oplus {Atom : Type u} (a b c : Proposition Atom) : (a.tensor (b.oplus c)).Equiv ((a.tensor b).oplus (a.tensor c))

theorem CLL.Proposition.subst_eqv_head {Atom : Type u} {Γ : Sequent Atom} {a b : Proposition Atom} (heqv : a.Equiv b) : Provable (a :: Γ) → Provable (b :: Γ)

The proposition at the head of a proof can be substituted by an equivalent proposition.

theorem CLL.Proposition.subst_eqv {Atom : Type u} {Γ Δ : Sequent Atom} {a b : Proposition Atom} (heqv : a.Equiv b) : Provable (Γ ++ [a] ++ Δ) → Provable (Γ ++ [b] ++ Δ)

Any proposition in a proof (regardless of its position) can be substituted by an equivalent proposition.

theorem CLL.Proposition.tensor_symm {Atom : Type u} {a b : Proposition Atom} : (a.tensor b).Equiv (b.tensor a)

theorem CLL.Proposition.tensor_assoc {Atom : Type u} {a b c : Proposition Atom} : (a.tensor (b.tensor c)).Equiv ((a.tensor b).tensor c)

instance CLL.Proposition.instIsSymmProvableConsTensor {Atom : Type u} {Γ : Sequent Atom} : IsSymm (Proposition Atom) fun (a b : Proposition Atom) => Provable (a.tensor b :: Γ)

theorem CLL.Proposition.oplus_idem {Atom : Type u} {a : Proposition Atom} : (a.oplus a).Equiv a

theorem CLL.Proposition.with_idem {Atom : Type u} {a : Proposition Atom} : (a.with a).Equiv a