η-expansion for Classical Linear Logic (CLL)

@[irreducible]

def Cslib.Logic.CLL.Proposition.expand {Atom : Type u_1} (a : Proposition Atom) : InferenceSystem.derivation InferenceSystem.Default {a, a.dual}

The η-expansion of a proposition a is a Proof of {a, a⫠} that applies the axiom only to atomic propositions.

Equations

• One or more equations did not get rendered due to their size.
• (Cslib.Logic.CLL.Proposition.atom x).expand = Cslib.Logic.CLL.Proof.ax
• (Cslib.Logic.CLL.Proposition.atomDual x).expand = Cslib.Logic.CLL.Proof.ax
• Cslib.Logic.CLL.Proposition.one.expand = Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.rwConclusion ⋯ Cslib.Logic.CLL.Proof.one.bot)
• Cslib.Logic.CLL.Proposition.bot.expand = Cslib.Logic.CLL.Proof.one.bot
• Cslib.Logic.CLL.Proposition.top.expand = Cslib.Logic.CLL.Proof.top
• Cslib.Logic.CLL.Proposition.zero.expand = Cslib.Logic.CLL.Proof.rwConclusion ⋯ Cslib.Logic.CLL.Proof.top
• (a_2.tensor b).expand = Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.parr (Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.tensor a_2.expand b.expand)))
• a_2.quest.expand = Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.bang ⋯ (Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.quest a_2.expand)))
• a_2.bang.expand = Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.bang ⋯ (Cslib.Logic.CLL.Proof.rwConclusion ⋯ (Cslib.Logic.CLL.Proof.quest a_2.dual.expand)))

def Cslib.Logic.CLL.Proof.onlyAtomicAxioms {Atom : Type u_1} {Γ : Sequent Atom} (p : InferenceSystem.derivation InferenceSystem.Default Γ) : Bool

A Proof has only atomic axioms if all its instances of the axiom treat atomic propositions.

Equations

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

theorem Cslib.Logic.CLL.Proof.onlyAtomicAxioms_rwConclusion {Atom : Type u_1} {Γ Δ : Sequent Atom} {heq : Γ = Δ} {p : InferenceSystem.derivation InferenceSystem.Default Γ} (h : onlyAtomicAxioms p = true) : onlyAtomicAxioms (rwConclusion heq p) = true

Proof.onlyAtomicAxioms is preserved by Proof.rwConclusion.

theorem Cslib.Logic.CLL.Proof.expand_onlyAtomicAxioms {Atom : Type u_1} (a : Proposition Atom) : onlyAtomicAxioms a.expand = true

η-expansion is correct: the proof returned by η-expansion contains only atomic axioms.