Prerequisite APIs for the frozen cut-elimination source port

10 fully proved

Sequent

DefinitionCheck that every proposition in a list is a why-not proposition#✓fully proved

Checks that all propositions in a list are question marks (ʔ).

def _root_.List.allQuest (as : List (Proposition Atom)) :=
  as.map (· matches ʔ_) |> List.foldr .and true

Used by 9

Used byContraction of a duplicated question-mark context · Weakening by a list of question-mark propositions · Why-not check agrees on a list and its multiset · Cut admissibility for a bang proposition · Principal shapes of a cut-free proof at the cut proposition · Reduction of a cut between matching principal rules · Cut step exposing a principal rule or commuting the cut · Exponential multicut against replicated question marks · Axiom case of the exponential multicut

TheoremWhy-not check agrees on a list and its multiset#✓fully proved

Checking a list context agrees with checking its multiset coercion.

@[simp, scoped grind =]
theorem allQuest_coe (Γ : List (Proposition Atom)) : allQuest (Γ : Sequent Atom) = Γ.allQuest

Uses 1 · Used by 3

Statement usesCheck that every proposition in a list is a why-not proposition

Used byCut step exposing a principal rule or commuting the cut · Exponential multicut against replicated question marks · Axiom case of the exponential multicut

TheoremEmpty sequent consists of question-mark propositions#✓fully proved

The empty sequent consists of ʔ-propositions.

@[simp, scoped grind =]
theorem allQuest_zero : (0 : Sequent Atom).allQuest

Used by 1

Used byA sum of sequents is all question marks iff both summands are

TheoremA cons sequent is all question marks iff its head and tail are#✓fully proved

A cons sequent consists of ʔ-propositions exactly when its head and tail do.

theorem allQuest_cons_iff {Γ : Sequent Atom} : allQuest (a ::ₘ Γ) ↔ (∃ b, a = ʔb) ∧ Γ.allQuest

Used by 1

Used byCut step exposing a principal rule or commuting the cut

TheoremA question-mark head does not change the all-question-mark property#✓fully proved

Adding a ʔ-proposition preserves and reflects allQuest.

@[simp]
theorem allQuest_quest_cons {Γ : Sequent Atom} : allQuest (ʔa ::ₘ Γ) ↔ Γ.allQuest

TheoremA sequent headed by a bang proposition is not all question marks#✓fully proved

A sequent containing a !-proposition cannot satisfy allQuest.

@[simp]
theorem not_allQuest_bang_cons {Γ : Sequent Atom} : ¬allQuest ((!a) ::ₘ Γ)

TheoremA sum of sequents is all question marks iff both summands are#✓fully proved

A sum consists of ʔ-propositions exactly when both summands do.

@[simp, scoped grind .]
theorem allQuest_add {Γ Δ : Sequent Atom} : (Γ + Δ).allQuest ↔ Γ.allQuest ∧ Δ.allQuest

Uses 1 · Used by 2

Proof usesEmpty sequent consists of question-mark propositions

Used byCut step exposing a principal rule or commuting the cut · Exponential multicut against replicated question marks

CLL

DefinitionHeight of a classical linear logic proof#✓fully proved

Height of a proof.

def Proof.height {Γ : Sequent Atom} : ⇓Γ → ℕ
  | .ax | .one | .top => 1
  | .bot p | .parr p | .oplus₁ p | .oplus₂ p
    | .quest p | .weaken p | .contract p | .bang _ p => p.height + 1
  | .cut p q | .tensor p q | .with p q => max p.height q.height + 1

Used by 4

Used byConclusion transport preserves proof height · Cut admissibility for a bang proposition · Cut admissibility for non-exponential propositions · Cut step exposing a principal rule or commuting the cut

TheoremConclusion transport preserves proof height#✓fully proved

Transporting a conclusion preserves proof height.

@[simp, scoped grind =]
theorem Proof.rwConclusion_height {Γ Δ : Sequent Atom} (h : Γ = Δ) (p : ⇓Γ) :
    (p.rwConclusion h).height = p.height

Uses 1 · Used by 1

Statement usesHeight of a classical linear logic proof

Used byCut step exposing a principal rule or commuting the cut

TheoremConclusion transport preserves the Boolean cut-free check#✓fully proved

Conclusion transport preserves the pinned Boolean cut-free check.

@[simp]
theorem Proof.cutFree_rwConclusion {Γ Δ : Sequent Atom}
    (h : Γ = Δ) (p : Proof Γ) :
    (p.rwConclusion h).cutFree = p.cutFree

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.