Elimination

Difficulty: hard — 2 definitions, 0 abbreviations, 1 lemmas, 5 theorems, 0 examples.

definition lemma theorem
legend

Pasting is never needed when the rules are schematic.

A deduction may paste other deductions into the statements it draws on. Where the rules are schemata, that is a convenience rather than a necessity: everything obtained by pasting can be obtained without it, by pushing the pasted deductions out to the leaves.

Source: Hiep, New Foundations for Separation Logic (PhD thesis, 2024), appendix A.3.

Enlarging the premises of a cut-free deduction gives a cut-free deduction: the schemata are read against the larger list instead, and the leaves point into it.

def Logic.ProofTheory.CutFree.mono {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop}
  {P P' : List Obj} {a : Obj} :
  (∀ x ∈ P, x ∈ P') → Logic.ProofTheory.CutFree S P a → Logic.ProofTheory.CutFree S P' a
Show details 
| Logic.ProofTheory.CutFree.mono x_3 (Logic.ProofTheory.CutFree.assumption ha) =
  Logic.ProofTheory.CutFree.assumption ⋯
| Logic.ProofTheory.CutFree.mono x_2 (Logic.ProofTheory.CutFree.apply s hs es) =
  Logic.ProofTheory.CutFree.apply s hs (Logic.ProofTheory.CutFree.DerivationsOf.mono x_2 es)

Complexity: 225 (size of the value term)

Outer dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.Schema

Inner dependencies: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.CutFree.DerivationsOf.mono

Lean core dependencies: Eq, Eq.symm, HEq, List, Prod, eq_of_heq

Used by: Logic.ProofTheory.CutFree.DerivationsOf.graft, Logic.ProofTheory.CutFree.DerivationsOf.mono

The same, branch by branch.

def Logic.ProofTheory.CutFree.DerivationsOf.mono {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop}
  {P P' : List Obj} {ps : List (List Obj × Obj)} :
  (∀ x ∈ P, x ∈ P') →
    Logic.ProofTheory.CutFree.DerivationsOf S P ps → Logic.ProofTheory.CutFree.DerivationsOf S P' ps
Show details 
| Logic.ProofTheory.CutFree.DerivationsOf.mono x_2 Logic.ProofTheory.CutFree.DerivationsOf.nil =
  Logic.ProofTheory.CutFree.DerivationsOf.nil
| Logic.ProofTheory.CutFree.DerivationsOf.mono x_2
    (Logic.ProofTheory.CutFree.DerivationsOf.cons d es) =
  Logic.ProofTheory.CutFree.DerivationsOf.cons (Logic.ProofTheory.CutFree.mono ⋯ d)
    (Logic.ProofTheory.CutFree.DerivationsOf.mono x_2 es)

Complexity: 233 (size of the value term)

Outer dependencies: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.Schema

Inner dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.mono, instToSeqList

Lean core dependencies: Eq, Eq.mp, Eq.mpr, Eq.symm, HEq, List, List.mem_append, Or, Or.elim, Prod, eq_of_heq, id

Used by: Logic.ProofTheory.CutFree.mono

Pasting, for cut-free deductions: the result is again cut-free.

theorem Logic.ProofTheory.DerivableCutFree.graft {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop}
  {P Q : List Obj} {a : Obj} :
  (∀ b ∈ Q, Logic.ProofTheory.DerivableCutFree S P b) →
    ∀ (a✝ : Logic.ProofTheory.CutFree S Q a), Logic.ProofTheory.DerivableCutFree S P a
Show details 
fun {Obj} {S} x x_1 x_2 x_3 x_4 =>
  Logic.ProofTheory.CutFree.brecOn x_4 Logic.ProofTheory.DerivableCutFree.graft._f
    Logic.ProofTheory.CutFree.DerivationsOf.graft._f x x_3

Complexity: 209 (size of the value term)

Dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.Schema

Proof dependencies: Logic.ProofTheory.CutFree.DerivationsOf

Lean core dependencies: Eq, Eq.symm, HEq, List, Nonempty, Nonempty.elim, Prod, eq_of_heq

Used by: Logic.ProofTheory.Derivation.toCutFree

The same, branch by branch.

theorem Logic.ProofTheory.CutFree.DerivationsOf.graft {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop}
  {P Q : List Obj} {ps : List (List Obj × Obj)} :
  (∀ b ∈ Q, Logic.ProofTheory.DerivableCutFree S P b) →
    ∀ (a✝ : Logic.ProofTheory.CutFree.DerivationsOf S Q ps),
      Nonempty (Logic.ProofTheory.CutFree.DerivationsOf S P ps)
Show details 
fun {Obj} {S} x x_1 x_2 x_3 x_4 =>
  Logic.ProofTheory.CutFree.DerivationsOf.brecOn x_4 Logic.ProofTheory.DerivableCutFree.graft._f
    Logic.ProofTheory.CutFree.DerivationsOf.graft._f x x_3

Complexity: 217 (size of the value term)

Dependencies: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.Schema

Proof dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.mono, instToSeqList

Lean core dependencies: Eq, Eq.mp, Eq.symm, HEq, List, List.mem_append, Nonempty, Nonempty.elim, Or, Or.elim, Prod, eq_of_heq

Used by: (none)

Establishing every branch of a schema, one at a time, establishes them all.

theorem Logic.ProofTheory.CutFree.DerivationsOf.of_forall {Obj : Type}
  {S : Logic.ProofTheory.Schema Obj → Prop} {Γ : List Obj} {ps : List (List Obj × Obj)} :
  (∀ p ∈ ps, Logic.ProofTheory.DerivableCutFree S ⟪p.1, Γ⟫ p.2) →
    Nonempty (Logic.ProofTheory.CutFree.DerivationsOf S Γ ps)
Show details 
fun {Obj} {S} {Γ} x x_1 =>
  List.brecOn (motive := fun x =>
    (∀ p ∈ x, Logic.ProofTheory.DerivableCutFree S ⟪p.1, Γ⟫ p.2) →
      Nonempty (Logic.ProofTheory.CutFree.DerivationsOf S Γ x))
    x Logic.ProofTheory.CutFree.DerivationsOf.of_forall._f x_1

Complexity: 301 (size of the value term)

Dependencies: Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.Schema, instToSeqList

Proof dependencies: Logic.ProofTheory.CutFree

Lean core dependencies: Eq, Eq.trans, List, Nonempty, Nonempty.elim, Or, Prod, True, congrArg, congrFun', eq_self, eq_true, of_eq_true, or_true, true_or

Used by: Logic.ProofTheory.Derivation.toCutFree

Every deduction in a system generated by schemata can be replaced by a direct one.

theorem Logic.ProofTheory.Derivation.toCutFree {Obj : Type} {S : Logic.ProofTheory.Schema Obj → Prop}
  {P : List Obj} {a : Obj} :
  ∀ (a✝ : Logic.ProofTheory.Derivation (Logic.ProofTheory.Schema.system S) P a),
    Logic.ProofTheory.DerivableCutFree S P a
Show details 
fun {Obj} {S} {P} {a} a_1 => Logic.ProofTheory.Derivation.toCutFree._mutual (PSum.inl ⟨P, ⟨a, a_1⟩⟩)

Complexity: 221 (size of the value term)

Dependencies: Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.Derivation, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.system

Proof dependencies: Logic.ProofTheory.Application, Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.DerivationsOf, Logic.ProofTheory.CutFree.DerivationsOf.of_forall, Logic.ProofTheory.DerivableCutFree.graft, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.Schema.instance, instToSeqList

Mathlib dependencies: Nonempty.some

Lean core dependencies: And, Bool, Decidable.byContradiction, Decidable.decide, Eq, Eq.mpr, Eq.symm, Eq.trans, Exists, False, HEq, Int, Int.natCast_add, Int.natCast_nonneg, Int.sub_nonneg_of_le, InvImage, Lean.Omega.Coeffs.ofList, Lean.Omega.Constraint.addInequality_sat, Lean.Omega.Constraint.combine_sat', Lean.Omega.Constraint.isImpossible, Lean.Omega.Constraint.not_sat'_of_isImpossible, Lean.Omega.Int.add_congr, Lean.Omega.Int.ofNat_le_of_le, Lean.Omega.Int.sub_congr, Lean.Omega.LinearCombo, Lean.Omega.LinearCombo.add_eval, Lean.Omega.LinearCombo.coordinate, Lean.Omega.LinearCombo.coordinate_eval_0, Lean.Omega.LinearCombo.coordinate_eval_1, Lean.Omega.LinearCombo.coordinate_eval_2, Lean.Omega.LinearCombo.coordinate_eval_3, Lean.Omega.LinearCombo.eval, Lean.Omega.LinearCombo.sub_eval, Lean.Omega.combo_sat', Lean.Omega.tidy_sat, List, List.map, List.mem_cons, List.mem_map_of_mem, Nat, Nat.cast, Nat.le_of_not_lt, Nonempty.elim, Not, Or, PSigma, PSum, Prod, True, WellFounded.Nat.fix, absurd, congrArg, eq_of_heq, id, le_of_le_of_eq, not_false_eq_true, of_decide_eq_true, of_eq_true

Used by: Logic.ProofTheory.derivable_iff_derivableCutFree

The same, claim by claim.

theorem Logic.ProofTheory.DerivationsOf.forall_toCutFree {Obj : Type}
  {S : Logic.ProofTheory.Schema Obj → Prop} {ps : List (List Obj × Obj)} :
  ∀ (a : Logic.ProofTheory.DerivationsOf (Logic.ProofTheory.Schema.system S) ps),
    ∀ q ∈ ps, Logic.ProofTheory.DerivableCutFree S q.1 q.2
Show details 
fun {Obj} {S} {ps} a q a_1 =>
  Logic.ProofTheory.Derivation.toCutFree._mutual (PSum.inr ⟨ps, ⟨a, ⟨q, a_1⟩⟩⟩)

Complexity: 447 (size of the value term)

Dependencies: Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.DerivationsOf, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.system

Proof dependencies: Logic.ProofTheory.Derivation

Lean core dependencies: Eq, Eq.symm, HEq, List, PSigma, Prod, eq_of_heq

Used by: (none)

Pasting is eliminable. Where the rules are schemata, a conclusion is deducible exactly when it is deducible without pasting. Deducibility is unchanged, so a certificate never needs a node that carries no rule of its own.

cut-elimination
theorem Logic.ProofTheory.derivable_iff_derivableCutFree {Obj : Type}
  {S : Logic.ProofTheory.Schema Obj → Prop} {P : List Obj} {a : Obj} :
  Logic.ProofTheory.Derivable (Logic.ProofTheory.Schema.system S) P a ↔
    Logic.ProofTheory.DerivableCutFree S P a
Show details 
fun {Obj} {S} {P} {a} =>
  { mp := fun h => Logic.ProofTheory.Derivation.toCutFree (Nonempty.some h),
    mpr := fun h => Nonempty.intro (Nonempty.some h).toDerivation }

Complexity: 131 (size of the value term)

Dependencies: Logic.ProofTheory.Derivable, Logic.ProofTheory.DerivableCutFree, Logic.ProofTheory.Schema, Logic.ProofTheory.Schema.system

Proof dependencies: Logic.ProofTheory.CutFree, Logic.ProofTheory.CutFree.toDerivation, Logic.ProofTheory.Derivation, Logic.ProofTheory.Derivation.toCutFree

Mathlib dependencies: Nonempty.some

Lean core dependencies: Iff, List

Used by: (none)

Dependency diagram

Drag to pan, Ctrl+scroll (or Cmd+scroll, or pinch on a touch screen) to zoom, click a node to jump to it.

definitionlemmatheoremdeclared elsewheredependencyproof dependency
legend