Documentation

Cslib.Logics.LinearLogic.CLL.EtaExpansion

η-expansion for Classical Linear Logic (CLL) #

source
@[irreducible]
def Cslib.Logic.CLL.Proposition.expand {Atom : Type u_1} (a : Proposition Atom) :
⇓{a, a.dual}

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

Equations
Instances For
    source
    def Cslib.Logic.CLL.Proof.onlyAtomicAxioms {Atom : Type u_1} {Γ : Sequent Atom} (p : ⇓Γ) :
    Bool

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

    Equations
    Instances For
      source
      theorem Cslib.Logic.CLL.Proof.onlyAtomicAxioms_rwConclusion {Atom : Type u_1} {Γ Δ : Sequent Atom} {heq : Γ = Δ} {p : ⇓Γ} (h : onlyAtomicAxioms p = true) :
      onlyAtomicAxioms (rwConclusion heq p) = true

      Proof.onlyAtomicAxioms is preserved by Proof.rwConclusion.

      source
      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.