Classical Linear Logic

TODO

• First-order polymorphism.
• Cut elimination.

References

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

inductive Cslib.Logic.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

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

@[instance_reducible]

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

Equations

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

def Cslib.Logic.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_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

The multiplicative conjunction connective.

Equations

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

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

The additive disjunction connective.

Equations

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

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

The multiplicative disjunction connective.

Equations

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

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

The additive conjunction connective.

Equations

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

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

The "of course" exponential.

Equations

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

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

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

Equations

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

inductive Cslib.Logic.CLL.Proposition.Context (Atom : Type u) : Type u

Propositional contexts (single-hole contexts for propositions).

• hole {Atom : Type u} : Context Atom
• tensorL {Atom : Type u} (c : Context Atom) (b : Proposition Atom) : Context Atom
• tensorR {Atom : Type u} (a : Proposition Atom) (c : Context Atom) : Context Atom
• parrL {Atom : Type u} (c : Context Atom) (b : Proposition Atom) : Context Atom
• parrR {Atom : Type u} (a : Proposition Atom) (c : Context Atom) : Context Atom
• oplusL {Atom : Type u} (c : Context Atom) (b : Proposition Atom) : Context Atom
• oplusR {Atom : Type u} (a : Proposition Atom) (c : Context Atom) : Context Atom
• withL {Atom : Type u} (c : Context Atom) (b : Proposition Atom) : Context Atom
• withR {Atom : Type u} (a : Proposition Atom) (c : Context Atom) : Context Atom
• bang {Atom : Type u} (c : Context Atom) : Context Atom
• quest {Atom : Type u} (c : Context Atom) : Context Atom

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

Equations

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

@[instance_reducible]

instance Cslib.Logic.CLL.Proposition.instDecidableEqContext {Atom✝ : Type u_1} [DecidableEq Atom✝] : DecidableEq (Context Atom✝)

Equations

• Cslib.Logic.CLL.Proposition.instDecidableEqContext = Cslib.Logic.CLL.Proposition.instDecidableEqContext.decEq

@[instance_reducible]

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

Equations

• Cslib.Logic.CLL.Proposition.instBEqContext = { beq := Cslib.Logic.CLL.Proposition.instBEqContext.beq }

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

Equations

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

def Cslib.Logic.CLL.Proposition.Context.fill {Atom : Type u_1} (c : Context Atom) (a : Proposition Atom) : Proposition Atom

Replaces the hole in a propositional context with a propositions.

Equations

• Cslib.Logic.CLL.Proposition.Context.hole.fill a = a
• (c_2.tensorL b).fill a = (c_2.fill a).tensor b
• (Cslib.Logic.CLL.Proposition.Context.tensorR b c_2).fill a = b.tensor (c_2.fill a)
• (c_2.parrL b).fill a = (c_2.fill a).parr b
• (Cslib.Logic.CLL.Proposition.Context.parrR b c_2).fill a = b.parr (c_2.fill a)
• (c_2.oplusL b).fill a = (c_2.fill a).oplus b
• (Cslib.Logic.CLL.Proposition.Context.oplusR b c_2).fill a = b.oplus (c_2.fill a)
• (c_2.withL b).fill a = (c_2.fill a).with b
• (Cslib.Logic.CLL.Proposition.Context.withR b c_2).fill a = b.with (c_2.fill a)
• c_2.bang.fill a = (c_2.fill a).bang
• c_2.quest.fill a = (c_2.fill a).quest

@[instance_reducible]

instance Cslib.Logic.CLL.instHasContextProposition {Atom : Type u_1} : HasContext (Proposition Atom)

Equations

• Cslib.Logic.CLL.instHasContextProposition = { Context := Cslib.Logic.CLL.Proposition.Context Atom, fill := Cslib.Logic.CLL.Proposition.Context.fill }

theorem Cslib.Logic.CLL.Proposition.context_fill_def {Atom : Type u_1} (c : Context Atom) (a : Proposition Atom) : c<[a] = c.fill a

Definition of context filling.

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

Positive propositions.

Equations

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

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

Negative propositions.

Equations

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

@[instance_reducible]

instance Cslib.Logic.CLL.Proposition.positiveDecidable {Atom : Type u_1} (a : Proposition Atom) : Decidable (a.positive = true)

Whether a Proposition is positive is decidable.

Equations

• a.positiveDecidable = a.positive.decEq true

@[instance_reducible]

instance Cslib.Logic.CLL.Proposition.negativeDecidable {Atom : Type u_1} (a : Proposition Atom) : Decidable (a.negative = true)

Whether a Proposition is negative is decidable.

Equations

• a.negativeDecidable = a.negative.decEq true

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

Propositional duality.

Equations

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

Propositional duality.

Equations

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

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

@[simp]

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

Duality preserves size.

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

No proposition is equal to its dual.

@[simp]

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

Two propositions are equal iff their respective duals are equal.

@[simp]

theorem Cslib.Logic.CLL.Proposition.dual_involution {Atom : Type u_1} (a : Proposition Atom) : a.dual.dual = a

Duality is an involution.

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

Linear implication.

Equations

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

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

Linear implication.

Equations

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

@[reducible, inline]

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

A sequent in CLL is a multiset of propositions.

Equations

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

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

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

Equations

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

def Cslib.Logic.CLL.Sequent.Context (Atom : Type u_1) : Type u_1

Judgemental contexts for CLL.

Equations

• Cslib.Logic.CLL.Sequent.Context Atom = Cslib.Logic.CLL.Sequent Atom

def Cslib.Logic.CLL.Sequent.Context.fill {Atom : Type u_1} (Γc : Context Atom) (a : Proposition Atom) : Multiset (Proposition Atom)

Filling a judgemental context returns a sequent.

Equations

• Γc.fill a = a ::ₘ Γc

@[instance_reducible]

instance Cslib.Logic.CLL.instHasHContextSequentProposition {Atom : Type u_1} : HasHContext (Sequent Atom) (Proposition Atom)

Equations

• Cslib.Logic.CLL.instHasHContextSequentProposition = { Context := Cslib.Logic.CLL.Sequent.Context Atom, fill := Cslib.Logic.CLL.Sequent.Context.fill }

inductive Cslib.Logic.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 ::ₘ Γ)

@[instance_reducible]

instance Cslib.Logic.CLL.instHasInferenceSystemSequent {Atom : Type u_1} : HasInferenceSystem (Sequent Atom)

Equations

• Cslib.Logic.CLL.instHasInferenceSystemSequent = { derivation := Cslib.Logic.CLL.Proof }

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

Convenience definition for rewriting conclusions in proofs.

Equations

• Cslib.Logic.CLL.Proof.rwConclusion h p = Cslib.Logic.InferenceSystem.rwConclusion h p

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

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

Equations

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

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

Cut, but where the premises are reversed.

Equations

• Cslib.Logic.CLL.Proof.cut' p q = Cslib.Logic.CLL.Proof.cut p (⋯ ▸ q)

def Cslib.Logic.CLL.Proof.parrInversion {Atom : Type u_1} {a b : Proposition Atom} {Γ : Sequent Atom} (h : ⇓(a.parr b ::ₘ Γ)) : ⇓(a ::ₘ b ::ₘ Γ)

Inversion of the ⅋ rule.

Equations

• Cslib.Logic.CLL.Proof.parrInversion h = ⋯ ▸ Cslib.Logic.CLL.Proof.cut' (⋯ ▸ Cslib.Logic.CLL.Proof.tensor Cslib.Logic.CLL.Proof.ax' Cslib.Logic.CLL.Proof.ax') h

def Cslib.Logic.CLL.Proof.botInversion {Atom : Type u_1} {Γ : Sequent Atom} (h : ⇓(⊥ ::ₘ Γ)) : ⇓Γ

Inversion of the ⊥ rule.

Equations

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

def Cslib.Logic.CLL.Proof.withInversion₁ {Atom : Type u_1} {a b : Proposition Atom} {Γ : Sequent Atom} (h : ⇓(a.with b ::ₘ Γ)) : ⇓(a ::ₘ Γ)

Inversion of the & rule, first component.

Equations

• Cslib.Logic.CLL.Proof.withInversion₁ h = (Cslib.Logic.CLL.Proof.oplus₁ Cslib.Logic.CLL.Proof.ax').cut' h

def Cslib.Logic.CLL.Proof.withInversion₂ {Atom : Type u_1} {a b : Proposition Atom} {Γ : Sequent Atom} (h : ⇓(a.with b ::ₘ Γ)) : ⇓(b ::ₘ Γ)

Inversion of the & rule, second component.

Equations

• Cslib.Logic.CLL.Proof.withInversion₂ h = (Cslib.Logic.CLL.Proof.oplus₂ Cslib.Logic.CLL.Proof.ax').cut' h

Logical equivalences

def Cslib.Logic.CLL.Proposition.equiv {Atom : Type u_1} (a b : Proposition Atom) : Type u_1

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

Equations

• a.equiv b = (⇓{a.dual, b} × ⇓{b.dual, a})

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

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

Equations

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

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

Propositional equivalence, proof-irrelevant version (Prop).

Equations

• a.Equiv b = (Cslib.Logic.InferenceSystem.Derivable {a.dual, b} ∧ Cslib.Logic.InferenceSystem.Derivable {b.dual, a})

@[instance_reducible]

instance Cslib.Logic.CLL.instDefaultCongruencePropositionEquiv {Atom : Type u_1} : DefaultCongruence (Proposition Atom) Proposition.Equiv

Equations

• Cslib.Logic.CLL.instDefaultCongruencePropositionEquiv = { }

theorem Cslib.Logic.CLL.Proposition.prop_equiv_def {Atom : Type u_1} {a b : Proposition Atom} : a.Equiv b ↔ DefaultCongruence.r a b

theorem Cslib.Logic.CLL.Proposition.equiv.toProp {Atom✝ : Type u_1} {a b : Proposition Atom✝} (h : a.equiv b) : DefaultCongruence.r a b

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

@[instance_reducible]

instance Cslib.Logic.CLL.instCoeEquivRPropositionEquiv {Atom✝ : Type u_1} {a b : Proposition Atom✝} : Coe (a.equiv b) (DefaultCongruence.r a b)

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

Equations

• Cslib.Logic.CLL.instCoeEquivRPropositionEquiv = { coe := ⋯ }

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

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

Equations

• Cslib.Logic.CLL.chooseEquiv h = (Cslib.Logic.InferenceSystem.DerivableIn.toDerivation ⋯, Cslib.Logic.InferenceSystem.DerivableIn.toDerivation ⋯)

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

Proof-relevant equivalence is reflexive.

Equations

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

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

Proof-relevant equivalence is symmetric.

Equations

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

def Cslib.Logic.CLL.Proposition.equiv.trans {Atom : Type u_1} {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 = (Cslib.Logic.CLL.Proof.cut (⋯ ▸ hab.1) hbc.1, Cslib.Logic.CLL.Proof.cut (⋯ ▸ hbc.2) hab.2)

theorem Cslib.Logic.CLL.Proposition.Equiv.refl {Atom : Type u_1} (a : Proposition Atom) : DefaultCongruence.r a a

Proof-irrelevant equivalence is reflexive.

theorem Cslib.Logic.CLL.Proposition.Equiv.symm {Atom : Type u_1} {a b : Proposition Atom} (h : DefaultCongruence.r a b) : DefaultCongruence.r b a

Proof-irrelevant equivalence is symmetric.

theorem Cslib.Logic.CLL.Proposition.Equiv.trans {Atom : Type u_1} {a b c : Proposition Atom} (hab : DefaultCongruence.r a b) (hbc : DefaultCongruence.r b c) : DefaultCongruence.r a c

Proof-irrelevant equivalence is transitive.

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

The canonical equivalence relation for propositions.

Equations

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

instance Cslib.Logic.CLL.Proposition.instIsEquivEquiv {Atom : Type u_1} : IsEquiv (Proposition Atom) Equiv

def Cslib.Logic.CLL.Proposition.bangTopEqvOne {Atom : Type u_1} : ⊤.bang.equiv 1

!⊤ ≡⇓ 1

Equations

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

def Cslib.Logic.CLL.Proposition.questZeroEqvBot {Atom : Type u_1} : (quest 0).equiv ⊥

ʔ0 ≡⇓ ⊥

Equations

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

def Cslib.Logic.CLL.Proposition.tensorZeroEqvZero {Atom : Type u_1} (a : Proposition Atom) : (a.tensor 0).equiv 0

a ⊗ 0 ≡⇓ 0

Equations

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

def Cslib.Logic.CLL.Proposition.parrTopEqvTop {Atom : Type u_1} (a : Proposition Atom) : (a.parr ⊤).equiv ⊤

a ⅋ ⊤ ≡⇓ ⊤

Equations

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

def Cslib.Logic.CLL.Proposition.tensorDistribOplus {Atom : Type u_1} (a b c : Proposition Atom) : (a.tensor (b.oplus c)).equiv ((a.tensor b).oplus (a.tensor c))

⊗ distributes over ⊕.

Equations

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

def Cslib.Logic.CLL.Proposition.substEqvHead {Atom : Type u_1} {a b : Proposition Atom} {Γ : Sequent Atom} (heqv : a.equiv b) (p : ⇓(a ::ₘ Γ)) : ⇓(b ::ₘ Γ)

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

Equations

• Cslib.Logic.CLL.Proposition.substEqvHead heqv p = ⋯ ▸ Cslib.Logic.CLL.Proof.cut p heqv.1

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

def Cslib.Logic.CLL.Proposition.substEqv {Atom : Type u_1} {a b : Proposition Atom} {Γ Δ : Sequent Atom} (heqv : a.equiv b) (p : ⇓(Γ + {a} + Δ)) : ⇓(Γ + {b} + Δ)

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

Equations

• Cslib.Logic.CLL.Proposition.substEqv heqv p = ⋯ ▸ Cslib.Logic.CLL.Proposition.substEqvHead heqv (⋯ ▸ p)

instance Cslib.Logic.CLL.Proposition.instLawfulCongruenceEquiv {Atom : Type u_1} : LawfulCongruence Equiv

@[instance_reducible]

noncomputable instance Cslib.Logic.CLL.Proposition.instLogicalEquivalenceSequentDefaultEquiv {Atom : Type u_1} : LogicalEquivalence InferenceSystem.Default Equiv

Equations

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

def Cslib.Logic.CLL.Proposition.tensorSymm {Atom : Type u_1} {a b : Proposition Atom} : (a.tensor b).equiv (b.tensor a)

Tensor is commutative.

Equations

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

def Cslib.Logic.CLL.Proposition.tensorAssoc {Atom : Type u_1} {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.Logic.CLL.Proposition.instSymmDerivableMultisetConsTensor {Atom : Type u_1} {Γ : Sequent Atom} : Std.Symm fun (a b : Proposition Atom) => InferenceSystem.Derivable (a.tensor b ::ₘ Γ)

def Cslib.Logic.CLL.Proposition.oplusIdem {Atom : Type u_1} {a : Proposition Atom} : (a.oplus a).equiv a

⊕ is idempotent.

Equations

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

def Cslib.Logic.CLL.Proposition.withIdem {Atom : Type u_1} {a : Proposition Atom} : (a.with a).equiv a

& is idempotent.

Equations

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

def Cslib.Logic.CLL.Proof.cutFree {Atom : Type u_1} {Γ : Sequent Atom} : ⇓Γ → Bool

A proof is cut-free if it does not contain any applications of rule cut.

Equations

• Cslib.Logic.CLL.Proof.ax.cutFree = true
• Cslib.Logic.CLL.Proof.one.cutFree = true
• Cslib.Logic.CLL.Proof.top.cutFree = true
• p.bot.cutFree = p.cutFree
• p.parr.cutFree = p.cutFree
• p.oplus₁.cutFree = p.cutFree
• p.oplus₂.cutFree = p.cutFree
• p.quest.cutFree = p.cutFree
• p.weaken.cutFree = p.cutFree
• p.contract.cutFree = p.cutFree
• (Cslib.Logic.CLL.Proof.bang a_1 p).cutFree = p.cutFree
• (p.tensor q).cutFree = (p.cutFree && q.cutFree)
• (p.with q).cutFree = (p.cutFree && q.cutFree)
• (a_1.cut a_2).cutFree = false