Documentation

Cslib.Logics.LinearLogic.CLL.EtaExpansion

η-expansion for Classical Linear Logic (CLL) #

source
@[irreducible]
def Cslib.CLL.Proposition.expand {Atom : Type u} (a : Proposition Atom) :
Proof {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.CLL.Proof.onlyAtomicAxioms {Atom✝ : Type u_1} {Γ : Sequent Atom✝} (p : Proof Γ) :
    Bool

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

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

      Proof.onlyAtomicAxioms is preserved by Proof.rwConclusion.

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

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