Canonical pinned API for the upstream CLL cut-elimination port

DefinitionEquivalence of source and pinned cut-free proof bundles#✓fully proved

Source and pinned cut-free proof bundles contain the same proof values.

def CF.Proof.equivCutFreeProof : CF.Proof Γ ≃ CutFreeProof Γ where
  toFun p := ⟨p.val, (Proof.isCutFree_iff_cutFree p.val).mp p.property⟩
  invFun p := ⟨p.val, (Proof.isCutFree_iff_cutFree p.val).mpr p.property⟩
  left_inv _ := Subtype.ext rfl
  right_inv _ := Subtype.ext rfl

Uses 3 · Used by 3

Statement usesProofs of the cut-free inference system · Cut-freeness of a proof · Cut-freeness predicate agrees with the Boolean check

Used byCut admissibility in the pinned bundle with list tails · Cut elimination for original classical linear logic proofs · Cut-free original proof from an explicit list presentation

DefinitionCut-free original proof from an explicit list presentation#✓fully proved

Compute a cut-free original CLL proof using an explicit list presentation.

def Proof.cut_elim_list [DecidableEq Atom]
    {Γ : List (Proposition Atom)} (p : Proof (Γ : Sequent Atom)) :
    CutFreeProof (Γ : Sequent Atom) :=
  CF.Proof.equivCutFreeProof (Proof.cutElimList p)

Uses 3

Statement usesProofs of the cut-free inference system · Equivalence of source and pinned cut-free proof bundles · List-based cut elimination in the source calculus

DefinitionCut elimination for original classical linear logic proofs#✓fully proved

Every original CLL proof has a cut-free original proof of the same sequent. This wrapper uses classical atom equality and a classical list representative.

noncomputable def Proof.cut_elim (p : Proof Γ) : CutFreeProof Γ := by
  classical
  exact CF.Proof.equivCutFreeProof (Proof.cutElim p)

Uses 3

Statement usesProofs of the cut-free inference system · Equivalence of source and pinned cut-free proof bundles · Cut elimination with a noncomputable list presentation

DefinitionCut admissibility in the pinned bundle with list tails#✓fully proved

Cut admissibility in the existing pinned bundle, with explicit list tails.

def CutFreeProof.cutAdmList [DecidableEq Atom] {a : Proposition Atom}
    {Γ Δ : List (Proposition Atom)} (p : CutFreeProof (a ::ₘ Γ))
    (q : CutFreeProof (a⫠ ::ₘ Δ)) :
    CutFreeProof ((Γ : Sequent Atom) + (Δ : Sequent Atom)) :=
  CF.Proof.equivCutFreeProof (Proof.cutAdm
    (CF.Proof.equivCutFreeProof.symm p)
    (CF.Proof.equivCutFreeProof.symm q))

Uses 3

Statement usesProofs of the cut-free inference system · Equivalence of source and pinned cut-free proof bundles · Cut admissibility for cut-free classical linear logic proofs

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.