Classical Linear Logic

TODO

• First-order polymorphism.
• Cut elimination.

References

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

inductive Cslib.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 Cslib.CLL.instDecidableEqProposition {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Proposition Atom✝)

Equations

• Cslib.CLL.instDecidableEqProposition = Cslib.CLL.instDecidableEqProposition.decEq

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

The multiplicative conjunction connective.

Equations

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

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

The additive disjunction connective.

Equations

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

def Cslib.CLL.term_⅋_ : Lean.TrailingParserDescr

The multiplicative disjunction connective.

Equations

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

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

The additive conjunction connective.

Equations

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

def Cslib.CLL.term!_ : Lean.ParserDescr

The "of course" exponential.

Equations

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

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

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

Equations

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

def Cslib.CLL.Proposition.positive {Atom : Type u} : Proposition Atom → Bool

Positive propositions.

Equations

• (Cslib.CLL.Proposition.atom x_1).positive = true
• Cslib.CLL.Proposition.one.positive = true
• Cslib.CLL.Proposition.zero.positive = true
• (a.tensor b).positive = true
• (a.oplus b).positive = true
• a.bang.positive = true
• x✝.positive = false

def Cslib.CLL.Proposition.negative {Atom : Type u} : Proposition Atom → Bool

Negative propositions.

Equations

• (Cslib.CLL.Proposition.atomDual x_1).negative = true
• Cslib.CLL.Proposition.bot.negative = true
• Cslib.CLL.Proposition.top.negative = true
• (a.parr b).negative = true
• (a.with b).negative = true
• a.quest.negative = true
• x✝.negative = false

instance Cslib.CLL.Proposition.positive_decidable {Atom : Type u} (a : Proposition Atom) : Decidable (a.positive = true)

Whether a Proposition is positive is decidable.

Equations

• a.positive_decidable = a.positive.decEq true

instance Cslib.CLL.Proposition.negative_decidable {Atom : Type u} (a : Proposition Atom) : Decidable (a.negative = true)

Whether a Proposition is negative is decidable.

Equations

• a.negative_decidable = a.negative.decEq true

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

Propositional duality.

Equations

• (Cslib.CLL.Proposition.atom x_1).dual = Cslib.CLL.Proposition.atomDual x_1
• (Cslib.CLL.Proposition.atomDual x_1).dual = Cslib.CLL.Proposition.atom x_1
• Cslib.CLL.Proposition.one.dual = Cslib.CLL.Proposition.bot
• Cslib.CLL.Proposition.bot.dual = Cslib.CLL.Proposition.one
• Cslib.CLL.Proposition.zero.dual = Cslib.CLL.Proposition.top
• Cslib.CLL.Proposition.top.dual = Cslib.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 Cslib.CLL.«term_⫠» : Lean.TrailingParserDescr

Propositional duality.

Equations

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

theorem Cslib.CLL.Proposition.top_eq_zero_dual {Atom : Type u} : ⊤ = dual 0

theorem Cslib.CLL.Proposition.dual_sizeOf {Atom : Type u} (a : Proposition Atom) : sizeOf a = sizeOf a.dual

Duality preserves size.

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

No proposition is equal to its dual.

@[simp]

theorem Cslib.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 Cslib.CLL.Proposition.dual_involution {Atom : Type u} (a : Proposition Atom) : a.dual.dual = a

Duality is an involution.

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

Linear implication.

Equations

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

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

Linear implication.

Equations

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

@[reducible, inline]

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

A sequent in CLL is a multiset of propositions.

Equations

• Cslib.CLL.Sequent Atom = Multiset (Cslib.CLL.Proposition Atom)

def Cslib.CLL.Sequent.allQuest {Atom : Type u} (Γ : Sequent Atom) : Bool

Checks that all propositions in a sequent Γ are question marks.

Equations

• Γ.allQuest = Multiset.fold and true (Multiset.map (fun (x : Cslib.CLL.Proposition Atom) => match x with | a.quest => true | x => false) Γ)

inductive Cslib.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} {Γ Δ : Multiset (Proposition Atom)} : Proof (a ::ₘ Γ) → Proof (a.dual ::ₘ Δ) → Proof (Γ + Δ)
• one {Atom : Type u} : Proof {1}
• bot {Atom : Type u} {Γ : Sequent Atom} : Proof Γ → Proof (⊥ ::ₘ Γ)
• parr {Atom : Type u} {a b : Proposition Atom} {Γ : Multiset (Proposition Atom)} : Proof (a ::ₘ b ::ₘ Γ) → Proof (a.parr b ::ₘ Γ)
• tensor {Atom : Type u} {a : Proposition Atom} {Γ : Multiset (Proposition Atom)} {b : Proposition Atom} {Δ : Multiset (Proposition Atom)} : Proof (a ::ₘ Γ) → Proof (b ::ₘ Δ) → Proof (a.tensor b ::ₘ (Γ + Δ))
• oplus₁ {Atom : Type u} {a : Proposition Atom} {Γ : Multiset (Proposition Atom)} {b : Proposition Atom} : Proof (a ::ₘ Γ) → Proof (a.oplus b ::ₘ Γ)
• oplus₂ {Atom : Type u} {b : Proposition Atom} {Γ : Multiset (Proposition Atom)} {a : Proposition Atom} : Proof (b ::ₘ Γ) → Proof (a.oplus b ::ₘ Γ)
• with {Atom : Type u} {a : Proposition Atom} {Γ : Multiset (Proposition Atom)} {b : Proposition Atom} : Proof (a ::ₘ Γ) → Proof (b ::ₘ Γ) → Proof (a.with b ::ₘ Γ)
• top {Atom : Type u} {Γ : Multiset (Proposition Atom)} : Proof (⊤ ::ₘ Γ)
• quest {Atom : Type u} {a : Proposition Atom} {Γ : Multiset (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} {Γ : Multiset (Proposition Atom)} : Proof (a.quest ::ₘ a.quest ::ₘ Γ) → Proof (a.quest ::ₘ Γ)
• bang {Atom : Type u} {Γ : Sequent Atom} {a : Proposition Atom} : Γ.allQuest = true → Proof (a ::ₘ Γ) → Proof (a.bang ::ₘ Γ)

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

A proof in the sequent calculus for classical linear logic.

Equations

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

def Cslib.CLL.Proof.rwConclusion {Atom✝ : Type u_1} {Γ Δ : Sequent Atom✝} (h : Γ = Δ) (p : Proof Γ) : Proof Δ

Rewrites the conclusion of a proof into an equal one.

Equations

• Cslib.CLL.Proof.rwConclusion h p = h ▸ p

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

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

Equations

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

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

Having a proof of Γ shows that it is provable.

noncomputable def Cslib.CLL.Sequent.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 Cslib.CLL.instCoeProofProvable {Atom✝ : Type u_1} {Γ : Sequent Atom✝} : Coe (Proof Γ) Γ.Provable

Equations

• Cslib.CLL.instCoeProofProvable = { coe := ⋯ }

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

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

Equations

• Cslib.CLL.Proof.ax' = ⋯ ▸ Cslib.CLL.Proof.ax

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

Cut, but where the premises are reversed.

Equations

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

def Cslib.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 = ⋯ ▸ (⋯ ▸ Cslib.CLL.Proof.ax'.tensor Cslib.CLL.Proof.ax').cut' h

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

Inversion of the ⊥ rule.

Equations

• h.bot_inversion = ⋯.mpr (Cslib.CLL.Proof.one.cut' h)

def Cslib.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₁ = Cslib.CLL.Proof.ax'.oplus₁.cut' h

def Cslib.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₂ = Cslib.CLL.Proof.ax'.oplus₂.cut' h

Logical equivalences

def Cslib.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 = (Cslib.CLL.Proof {a.dual, b} × Cslib.CLL.Proof {b.dual, a})

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

Propositional equivalence, proof-irrelevant version (Prop).

Equations

• a.Equiv b = ({a.dual, b}.Provable ∧ {b.dual, a}.Provable)

theorem Cslib.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.

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

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

Equations

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

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

Propositional equivalence, proof-irrelevant version (Prop).

Equations

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

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

Proof-relevant equivalence is coerciable into proof-irrelevant equivalence.

Equations

• Cslib.CLL.instCoeEquivEquiv = { coe := ⋯ }

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

Proof-relevant equivalence is reflexive.

Equations

• Cslib.CLL.Proposition.equiv.refl a = (Cslib.CLL.Proof.ax', Cslib.CLL.Proof.ax')

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

Proof-relevant equivalence is symmetric.

Equations

• Cslib.CLL.Proposition.equiv.symm a h = (h.2, h.1)

def Cslib.CLL.Proposition.equiv.trans {Atom : Type u} {a b c : Proposition Atom} (hab : a.equiv b) (hbc : b.equiv c) : a.equiv c

Proof-relevant equivalence is transitive.

Equations

• hab.trans hbc = ((⋯ ▸ hab.1).cut hbc.1, (⋯ ▸ hbc.2).cut hab.2)

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

Proof-irrelevant equivalence is reflexive.

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

Proof-irrelevant equivalence is symmetric.

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

Proof-irrelevant equivalence is transitive.

noncomputable def Cslib.CLL.Proposition.chooseEquiv {Atom✝ : Type u_1} {a b : Proposition Atom✝} (h : a.Equiv b) : a.equiv b

Transforms a proof-irrelevant equivalence into a proof-relevant one (this is not computable).

Equations

• Cslib.CLL.Proposition.chooseEquiv h = (⋯.toProof, ⋯.toProof)

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

The canonical equivalence relation for propositions.

Equations

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

def Cslib.CLL.Proposition.bang_top_eqv_one {Atom : Type u} : ⊤.bang.equiv 1

!⊤ ≡⇓ 1

Equations

• Cslib.CLL.Proposition.bang_top_eqv_one = (Cslib.CLL.Proof.one.weaken, (Cslib.CLL.Proof.bang ⋯ Cslib.CLL.Proof.top).bot)

def Cslib.CLL.Proposition.quest_zero_eqv_bot {Atom : Type u} : (quest 0).equiv ⊥

ʔ0 ≡⇓ ⊥

Equations

• Cslib.CLL.Proposition.quest_zero_eqv_bot = (Cslib.CLL.Proof.rwConclusion ⋯ (Cslib.CLL.Proof.bang ⋯ Cslib.CLL.Proof.top).bot, Cslib.CLL.Proof.rwConclusion ⋯ Cslib.CLL.Proof.one.weaken)

def Cslib.CLL.Proposition.tensor_zero_eqv_zero {Atom : Type u} (a : Proposition Atom) : (a.tensor 0).equiv 0

a ⊗ 0 ≡⇓ 0

Equations

• a.tensor_zero_eqv_zero = ((Cslib.CLL.Proof.rwConclusion ⋯ Cslib.CLL.Proof.top).parr, Cslib.CLL.Proof.top)

def Cslib.CLL.Proposition.parr_top_eqv_top {Atom : Type u} (a : Proposition Atom) : (a.parr ⊤).equiv ⊤

a ⅋ ⊤ ≡⇓ ⊤

Equations

• a.parr_top_eqv_top = (Cslib.CLL.Proof.rwConclusion ⋯ Cslib.CLL.Proof.top, Cslib.CLL.Proof.rwConclusion ⋯ (Cslib.CLL.Proof.rwConclusion ⋯ Cslib.CLL.Proof.top).parr)

def Cslib.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))

⊗ distributed over ⊕.

Equations

• One or more equations did not get rendered due to their size.

def Cslib.CLL.Proposition.subst_eqv_head {Atom : Type u} {a b : Proposition Atom} {Γ : Sequent Atom} (heqv : a.equiv b) (p : Proof (a ::ₘ Γ)) : Proof (b ::ₘ Γ)

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

Equations

• Cslib.CLL.Proposition.subst_eqv_head heqv p = ⋯ ▸ p.cut heqv.1

theorem Cslib.CLL.Proposition.add_middle_eq_cons {Atom : Type u} {Γ Δ : Multiset (Proposition Atom)} {a : Proposition Atom} : Γ + {a} + Δ = a ::ₘ (Γ + Δ)

def Cslib.CLL.Proposition.subst_eqv {Atom : Type u} {a b : Proposition Atom} {Γ Δ : Sequent Atom} (heqv : a.equiv b) (p : Proof (Γ + {a} + Δ)) : Proof (Γ + {b} + Δ)

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

Equations

• Cslib.CLL.Proposition.subst_eqv heqv p = ⋯ ▸ Cslib.CLL.Proposition.subst_eqv_head heqv (⋯ ▸ p)

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

Tensor is commutative.

Equations

• Cslib.CLL.Proposition.tensor_symm = ((⋯ ▸ Cslib.CLL.Proof.ax.tensor Cslib.CLL.Proof.ax).parr, (⋯ ▸ Cslib.CLL.Proof.ax.tensor Cslib.CLL.Proof.ax).parr)

def Cslib.CLL.Proposition.tensor_assoc {Atom : Type u} {a b c : Proposition Atom} : (a.tensor (b.tensor c)).equiv ((a.tensor b).tensor c)

⊗ is associative.

Equations

• One or more equations did not get rendered due to their size.

instance Cslib.CLL.Proposition.instSymmProvableConsTensor {Atom : Type u} {Γ : Sequent Atom} : Std.Symm fun (a b : Proposition Atom) => Sequent.Provable (a.tensor b ::ₘ Γ)

def Cslib.CLL.Proposition.oplus_idem {Atom : Type u} {a : Proposition Atom} : (a.oplus a).equiv a

⊕ is idempotent.

Equations

• Cslib.CLL.Proposition.oplus_idem = (Cslib.CLL.Proof.ax'.with Cslib.CLL.Proof.ax', ⋯ ▸ Cslib.CLL.Proof.ax.oplus₁)

def Cslib.CLL.Proposition.with_idem {Atom : Type u} {a : Proposition Atom} : (a.with a).equiv a

& is idempotent.

Equations

• Cslib.CLL.Proposition.with_idem = (Cslib.CLL.Proof.ax'.oplus₁, ⋯ ▸ Cslib.CLL.Proof.ax.with Cslib.CLL.Proof.ax)