Fine paths in local tableaux and in tableaux

This file collects helper definitions and lemmas that are used in Pdl.InterpolationCluster to define interpolants for proper clusters (Section 9 of the paper).

The two main definitions are LocalPathIn, for paths to arbitrary (also intermediate) nodes of a LocalTableau, and FinePathIn, for the nodes of a whole Tableau in the fine sense, i.e. including those nodes inside a local tableau that a loc step jumps over.

Paths inside a local tableau

The Tableau type applies a whole LocalTableau in one loc step, and thus the PathIn type — and with it the edge relation ⋖_ and the clusters defined via ◃ — "jumps over" the intermediate nodes inside a local tableau. For the quasi-tableau in Definition 9.8 we need those intermediate nodes, because it is only there that each rule application is either a left or a right rule.

We therefore first define LocalPathIn, the analogue of PathIn for local tableaux, in the same spirit as LocalTableau.paths which is used for the completeness proof. Note that in contrast to LocalTableau.paths we here keep the nodes themselves and not only the sequents labelling them, so that we can still connect them to PathIn.

inductive LocalPathIn {X : Sequent} : LocalTableau X → Type

A path inside a LocalTableau, pointing at an arbitrary node of it — in contrast to LocalTableau.paths which only goes to the end nodes.

• nil {X : Sequent} {lt : LocalTableau X} : LocalPathIn lt
• cons {X : Sequent} {lra : LocalRuleApp} {X_def : X = lra.X} {next : (Y : Sequent) → Y ∈ lra.C → LocalTableau Y} {Y : Sequent} (Y_in : Y ∈ lra.C) (tail : LocalPathIn (next Y Y_in)) : LocalPathIn (LocalTableau.byLocalRule lra X_def next)

@[instance_reducible]

instance instDecidableEqLocalPathIn {X✝ : Sequent} {a✝ : LocalTableau X✝} : DecidableEq (LocalPathIn a✝)

Equations

• instDecidableEqLocalPathIn = instDecidableEqLocalPathIn.decEq

def instDecidableEqLocalPathIn.decEq {X✝ : Sequent} {a✝ : LocalTableau X✝} (x✝ x✝¹ : LocalPathIn a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqLocalPathIn.decEq LocalPathIn.nil LocalPathIn.nil = isTrue ⋯
• instDecidableEqLocalPathIn.decEq LocalPathIn.nil (LocalPathIn.cons Y_in tail) = isFalse ⋯
• instDecidableEqLocalPathIn.decEq (LocalPathIn.cons Y_in tail) LocalPathIn.nil = isFalse ⋯

def LocalPathIn.last {X : Sequent} {lt : LocalTableau X} : LocalPathIn lt → Sequent

The sequent at the node a local path is pointing at.

Equations

• LocalPathIn.nil.last = X
• (LocalPathIn.cons Y_in tail).last = tail.last

def LocalPathIn.ltAt {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : LocalTableau lp.last

The local tableau rooted at the node a local path is pointing at.

Equations

• LocalPathIn.nil.ltAt = lt
• (LocalPathIn.cons Y_in tail).ltAt = tail.ltAt

def LocalPathIn.isNilB {X : Sequent} {lt : LocalTableau X} : LocalPathIn lt → Bool

Is this the empty local path, i.e. does it point at the root of the local tableau?

Equations

• LocalPathIn.nil.isNilB = true
• (LocalPathIn.cons Y_in tail).isNilB = false

def LocalTableau.hasRule {X : Sequent} : LocalTableau X → Prop

Is a local rule applied at the root of this local tableau?

Equations

• (LocalTableau.byLocalRule lra X_def next).hasRule = True
• (LocalTableau.sim a).hasRule = False

@[instance_reducible]

instance LocalTableau.instDecidableHasRule {X : Sequent} (lt : LocalTableau X) : Decidable lt.hasRule

Equations

• One or more equations did not get rendered due to their size.

def LocalPathIn.isInternal {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : Prop

A local path is internal iff a local rule is applied at the node it points at, i.e. iff that node is not a leaf of the local tableau.

Equations

• lp.isInternal = lp.ltAt.hasRule

@[instance_reducible]

instance LocalPathIn.instDecidableIsInternal {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : Decidable lp.isInternal

Equations

• lp.instDecidableIsInternal = id inferInstance

def LocalPathIn.endNodeAt? {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : Option ↥(endNodesOf lt)

If the local path points at a leaf then this gives the end node it reaches.

Equations

• LocalPathIn.nil.endNodeAt? = none
• LocalPathIn.nil.endNodeAt? = some ⟨X, ⋯⟩
• (LocalPathIn.cons Y_in tail).endNodeAt? = Option.map (fun (x : ↥(endNodesOf (next Y Y_in))) => match x with | ⟨Z, hZ⟩ => ⟨Z, ⋯⟩) tail.endNodeAt?

theorem LocalPathIn.isInternal_iff_endNodeAt?_eq_none {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp.isInternal ↔ lp.endNodeAt? = none

theorem LocalPathIn.last_of_endNodeAt? {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) {Yh : ↥(endNodesOf lt)} (h : lp.endNodeAt? = some Yh) : lp.last = ↑Yh

def LocalPathIn.children {X : Sequent} {lt : LocalTableau X} : LocalPathIn lt → Finset (LocalPathIn lt)

The children of the node a local path points at, inside the same local tableau.

Equations

• LocalPathIn.nil.children = Finset.image (fun (x : ↥lra.C) => match x with | ⟨val, Y_in⟩ => LocalPathIn.cons Y_in LocalPathIn.nil) lra.C.attach
• LocalPathIn.nil.children = ∅
• (LocalPathIn.cons Y_in tail).children = Finset.image (LocalPathIn.cons Y_in) tail.children

def LocalTableau.childLabels {X : Sequent} : LocalTableau X → Finset Sequent

The sequents labelling the children of the root of a local tableau.

Equations

• (LocalTableau.byLocalRule lra X_def next).childLabels = lra.C
• (LocalTableau.sim a).childLabels = ∅

theorem LocalPathIn.map_last_children {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : Finset.image last lp.children = lp.ltAt.childLabels

noncomputable def LocalPathIn.endNodesBelow {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : List ↥(endNodesOf lt)

The end nodes of the whole local tableau that are below a given local path.

Equations

• LocalPathIn.nil.endNodesBelow = (endNodesOf lt).attachList
• (LocalPathIn.cons Y_in tail).endNodesBelow = List.map (fun (x : ↥(endNodesOf (next Y Y_in))) => match x with | ⟨Z, hZ⟩ => ⟨Z, ⋯⟩) tail.endNodesBelow

theorem LocalPathIn.endNodesBelow_eq_of_endNodeAt? {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) {Yh : ↥(endNodesOf lt)} : lp.endNodeAt? = some Yh → ∀ Yh' ∈ lp.endNodesBelow, Yh' = Yh

A leaf of a local tableau is the only end node below itself.

theorem LocalPathIn.exists_child_endNodesBelow {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp.isInternal → ∀ Yh ∈ lp.endNodesBelow, ∃ c ∈ lp.children, Yh ∈ c.endNodesBelow

If an end node is below an internal node of a local tableau, then it is below one of the children of that node.

noncomputable def internalLocalPaths {X : Sequent} (lt : LocalTableau X) : List (LocalPathIn lt)

All internal nodes of a local tableau, i.e. those where a local rule is applied. Compare allPaths for PathIn.

Equations

• One or more equations did not get rendered due to their size.
• internalLocalPaths (LocalTableau.sim a) = []

theorem internalLocalPaths_isInternal {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp ∈ internalLocalPaths lt → lp.isInternal

theorem LocalPathIn.mem_internalLocalPaths {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) (h : lp.isInternal) : lp ∈ internalLocalPaths lt

Fine paths: all nodes of a tableau

A FinePathIn points at a node of the tableau in the fine sense: it may also point at an intermediate node inside a local tableau. Note that the end nodes of a local tableau are not fine nodes of their own: in the Tableau type they are the roots of the tableaux given by next, and that is where they show up here.

Hence a fine node is either

• an internal node of the local tableau applied at a Tableau.loc node (inLoc),
• a Tableau.pdl node (pdlHere), or
• a Tableau.lrep node, i.e. a loaded-path repeat leaf (lrepHere), possibly below some loc and pdl steps. Every node has exactly one representation as a FinePathIn.

inductive FinePathIn {Hist : History} {X : Sequent} : Tableau Hist X → Type

A path in a tableau that may also stop at an intermediate node inside a LocalTableau.

• inLoc {Hist : History} {X : Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} (lp : LocalPathIn lt) (lp_int : lp.isInternal) : FinePathIn (Tableau.loc nrep nbas lt next)
• pdlHere {Hist : History} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {next : Tableau (X :: Hist) Y} : FinePathIn (Tableau.pdl nrep bas r next)
• lrepHere {Hist : History} {X : Sequent} {lpr : LoadedPathRepeat Hist X} : FinePathIn (Tableau.lrep lpr)
• loc {Hist : History} {X : Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} {Y : Sequent} (Y_in : Y ∈ endNodesOf lt) (tail : FinePathIn (next Y Y_in)) : FinePathIn (Tableau.loc nrep nbas lt next)
• pdl {Hist : History} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {next : Tableau (X :: Hist) Y} (tail : FinePathIn next) : FinePathIn (Tableau.pdl nrep bas r next)

@[instance_reducible]

instance instDecidableEqFinePathIn {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} : DecidableEq (FinePathIn a✝)

Equations

• instDecidableEqFinePathIn = instDecidableEqFinePathIn.decEq

def instDecidableEqFinePathIn.decEq {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} (x✝ x✝¹ : FinePathIn a✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqFinePathIn.decEq (FinePathIn.inLoc lp lp_int) (FinePathIn.loc Y_in tail) = isFalse ⋯
• instDecidableEqFinePathIn.decEq FinePathIn.pdlHere FinePathIn.pdlHere = isTrue ⋯
• instDecidableEqFinePathIn.decEq FinePathIn.pdlHere tail.pdl = isFalse ⋯
• instDecidableEqFinePathIn.decEq FinePathIn.lrepHere FinePathIn.lrepHere = isTrue ⋯
• instDecidableEqFinePathIn.decEq (FinePathIn.loc Y_in tail) (FinePathIn.inLoc lp lp_int) = isFalse ⋯
• instDecidableEqFinePathIn.decEq tail.pdl FinePathIn.pdlHere = isFalse ⋯
• instDecidableEqFinePathIn.decEq a_8.pdl b.pdl = if h : a_8 = b then h ▸ have inst := instDecidableEqFinePathIn.decEq a_8 a_8; isTrue ⋯ else isFalse ⋯

def rootFine {H : History} {X : Sequent} (tab : Tableau H X) : FinePathIn tab

The fine path pointing at the root of a tableau.

Equations

• rootFine (Tableau.loc nflprep nbas (LocalTableau.byLocalRule lra X_def next_2) next_3) = FinePathIn.inLoc LocalPathIn.nil True.intro
• rootFine (Tableau.loc nflprep nbas (LocalTableau.sim bas) next_2) = absurd bas nbas
• rootFine (Tableau.pdl nflprep bas r next) = FinePathIn.pdlHere
• rootFine (Tableau.lrep lpr) = FinePathIn.lrepHere

def FinePathIn.label {Hist : History} {X : Sequent} {tab : Tableau Hist X} : FinePathIn tab → Sequent

The sequent at the node a fine path points at, i.e. Λ(t) for fine nodes t.

Equations

• (FinePathIn.inLoc lp lp_int).label = lp.last
• FinePathIn.pdlHere.label = x✝
• FinePathIn.lrepHere.label = x✝
• (FinePathIn.loc Y_in tail).label = tail.label
• tail.pdl.label = tail.label

def FinePathIn.base {Hist : History} {X : Sequent} {tab : Tableau Hist X} : FinePathIn tab → PathIn tab

The PathIn node in whose local tableau the given fine node lies.

Equations

• (FinePathIn.inLoc lp lp_int).base = PathIn.nil
• FinePathIn.pdlHere.base = PathIn.nil
• FinePathIn.lrepHere.base = PathIn.nil
• (FinePathIn.loc Y_in tail).base = PathIn.loc Y_in tail.base
• tail.pdl.base = tail.base.pdl

def FinePathIn.children {Hist : History} {X : Sequent} {tab : Tableau Hist X} : FinePathIn tab → Finset (FinePathIn tab)

The children of a fine node. Note that a child of an internal node of a local tableau may be a node of the tableau in the coarse PathIn sense, namely when it is an end node of that local tableau.

Equations

• One or more equations did not get rendered due to their size.
• FinePathIn.pdlHere.children = {(rootFine next).pdl}
• FinePathIn.lrepHere.children = ∅
• (FinePathIn.loc Y_in tail).children = Finset.image (FinePathIn.loc Y_in) tail.children
• tail.pdl.children = Finset.image FinePathIn.pdl tail.children

def PathIn.toFine {Hist : History} {X : Sequent} {tab : Tableau Hist X} : PathIn tab → FinePathIn tab

Any node in the coarse sense is also a node in the fine sense.

Equations

• PathIn.nil.toFine = rootFine x✝
• (PathIn.loc Y_in tail).toFine = FinePathIn.loc Y_in tail.toFine
• tail.pdl.toFine = tail.toFine.pdl

noncomputable def allFinePaths {H : History} {X : Sequent} (tab : Tableau H X) : List (FinePathIn tab)

All fine nodes of a tableau. Compare allPaths.

Equations

• One or more equations did not get rendered due to their size.
• allFinePaths (Tableau.pdl nflprep bas r next) = FinePathIn.pdlHere :: List.map FinePathIn.pdl (allFinePaths next)
• allFinePaths (Tableau.lrep lpr) = [FinePathIn.lrepHere]

@[simp]

theorem label_rootFine {H : History} {X : Sequent} (tab : Tableau H X) : (rootFine tab).label = X

@[simp]

theorem base_rootFine {H : History} {X : Sequent} (tab : Tableau H X) : (rootFine tab).base = PathIn.nil

@[simp]

theorem PathIn.base_toFine {H : History} {X : Sequent} {tab : Tableau H X} (p : PathIn tab) : p.toFine.base = p

@[simp]

theorem PathIn.label_toFine {H : History} {X : Sequent} {tab : Tableau H X} (p : PathIn tab) : p.toFine.label = nodeAt p

theorem FinePathIn.mem_allFinePaths {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) : f ∈ allFinePaths tab

theorem FinePathIn.base_of_mem_children {H : History} {X : Sequent} {tab : Tableau H X} (f g : FinePathIn tab) : g ∈ f.children → g.base = f.base ∨ f.base ⋖_ g.base

Fine children either stay at the same node in the coarse sense, or they are a child of it. This connects the fine children with the edge relation ⋖_.

theorem FinePathIn.map_label_children_inLoc {Hist : History} {X : Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} (lp : LocalPathIn lt) (h : lp.isInternal) : Finset.image label (inLoc lp h).children = Finset.image LocalPathIn.last lp.children

def FinePathIn.lra? {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → Option LocalRuleApp

The local rule applied at a fine node, if any.

Equations

• (FinePathIn.inLoc lp lp_int).lra? = match lp.ltAt with | LocalTableau.byLocalRule lra X_def next => some lra | LocalTableau.sim a => none
• FinePathIn.pdlHere.lra? = none
• FinePathIn.lrepHere.lra? = none
• (FinePathIn.loc Y_in tail).lra? = tail.lra?
• tail.pdl.lra? = tail.lra?

theorem FinePathIn.lra?_spec {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) {lra : LocalRuleApp} (h : f.lra? = some lra) : f.label = lra.X ∧ Finset.image label f.children = lra.C

If a local rule is applied at a fine node then that node is labelled with the premise and its children are labelled with the conclusions of that rule.

theorem FinePathIn.locally_sound {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) {lra : LocalRuleApp} (h : f.lra? = some lra) {W : Type} (M : KripkeModel W) (w : W) : (M, w) ⊨ f.label ↔ ∃ g ∈ f.children, (M, w) ⊨ g.label

Local soundness and invertibility at the fine level: whenever a local rule is applied at a fine node, its label is satisfied exactly if the label of one of its children is. This is the property of the fine tableau that makes the quasi-tableau work.

Left and right rules

At the fine level each rule application is a left rule or a right rule or neither (the latter for closing rules and loaded-path repeats), but never both. This is what Lemma 9.7 (a) is about, and it is the reason why we needed the fine nodes: on the Tableau level a loc step is in general a mix of left and right rules.

def LocalRule.isRightRule {X : Sequent} {YS : Finset Sequent} : LocalRule X YS → Bool

Is this a local rule applied to the right component?

Equations

• (LocalRule.oneSidedR orule YS_def).isRightRule = true
• (LocalRule.loadedR χ lrule YS_def).isRightRule = true
• x✝.isRightRule = false

def LocalRule.isLeftRule {X : Sequent} {YS : Finset Sequent} : LocalRule X YS → Bool

Is this a local rule applied to the left component?

Equations

• (LocalRule.oneSidedL orule YS_def).isLeftRule = true
• (LocalRule.loadedL χ lrule YS_def).isLeftRule = true
• x✝.isLeftRule = false

def LocalRuleApp.isRightRule (lra : LocalRuleApp) : Bool

Equations

• lra.isRightRule = lra.lr.isRightRule

def LocalRuleApp.isLeftRule (lra : LocalRuleApp) : Bool

Equations

• lra.isLeftRule = lra.lr.isLeftRule

theorem LocalRuleApp.not_left_and_right (lra : LocalRuleApp) : ¬(lra.isLeftRule = true ∧ lra.isRightRule = true)

def PdlRule.isRightRule {X Y : Sequent} : PdlRule X Y → Bool

The (M), (L+) and (L-) rules acting on the right component.

Equations

• (PdlRule.loadR a a_1 a_2).isRightRule = true
• (PdlRule.freeR a a_1).isRightRule = true
• (PdlRule.modR a a_1).isRightRule = true
• x✝.isRightRule = false

def PdlRule.isLeftRule {X Y : Sequent} : PdlRule X Y → Bool

The (M), (L+) and (L-) rules acting on the left component.

Equations

• (PdlRule.loadL a a_1 a_2).isLeftRule = true
• (PdlRule.freeL a a_1).isLeftRule = true
• (PdlRule.modL a a_1).isLeftRule = true
• x✝.isLeftRule = false

def FinePathIn.usesRightRule {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → Bool

Is a right rule applied at this fine node?

Equations

• (FinePathIn.inLoc lp lp_int).usesRightRule = match lp.ltAt with | LocalTableau.byLocalRule lra X_def next => lra.isRightRule | LocalTableau.sim a => false
• FinePathIn.pdlHere.usesRightRule = r.isRightRule
• FinePathIn.lrepHere.usesRightRule = false
• (FinePathIn.loc Y_in tail).usesRightRule = tail.usesRightRule
• tail.pdl.usesRightRule = tail.usesRightRule

def FinePathIn.usesLeftRule {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → Bool

Is a left rule applied at this fine node?

Equations

• (FinePathIn.inLoc lp lp_int).usesLeftRule = match lp.ltAt with | LocalTableau.byLocalRule lra X_def next => lra.isLeftRule | LocalTableau.sim a => false
• FinePathIn.pdlHere.usesLeftRule = r.isLeftRule
• FinePathIn.lrepHere.usesLeftRule = false
• (FinePathIn.loc Y_in tail).usesLeftRule = tail.usesLeftRule
• tail.pdl.usesLeftRule = tail.usesLeftRule

theorem FinePathIn.not_left_and_right {H : History} {Y : Sequent} {tab : Tableau H Y} (f : FinePathIn tab) : ¬(f.usesLeftRule = true ∧ f.usesRightRule = true)

No node uses a left and a right rule at the same time.

theorem FinePathIn.not_isLrep_base_of_usesRightRule {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) (h : f.usesRightRule = true) : ¬f.base.isLrep

A node where a right rule is applied is not a loaded-path repeat, and neither is the coarse node it belongs to.

def FinePathIn.atBigRoot {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → Bool

Is this fine node also a node in the coarse sense, i.e. the root of the local tableau at its base?

Equations

• (FinePathIn.inLoc lp lp_int).atBigRoot = lp.isNilB
• FinePathIn.pdlHere.atBigRoot = true
• FinePathIn.lrepHere.atBigRoot = true
• (FinePathIn.loc Y_in tail).atBigRoot = tail.atBigRoot
• tail.pdl.atBigRoot = tail.atBigRoot

@[simp]

theorem atBigRoot_rootFine {H : History} {X : Sequent} (tab : Tableau H X) : (rootFine tab).atBigRoot = true

@[simp]

theorem PathIn.atBigRoot_toFine {H : History} {X : Sequent} {tab : Tableau H X} (p : PathIn tab) : p.toFine.atBigRoot = true

def FinePathIn.endLabelsBelow {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → Finset Sequent

The labels of those end nodes of the local tableau at f.base that are below f. These are the labels of the children of f.base that can be reached from f.

Equations

• (FinePathIn.inLoc lp lp_int).endLabelsBelow = endNodesOf lp.ltAt
• FinePathIn.pdlHere.endLabelsBelow = ∅
• FinePathIn.lrepHere.endLabelsBelow = ∅
• (FinePathIn.loc Y_in tail).endLabelsBelow = tail.endLabelsBelow
• tail.pdl.endLabelsBelow = tail.endLabelsBelow

noncomputable def FinePathIn.coarseChildrenBelow {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → List (PathIn tab)

The children of f.base in the coarse sense that are below the fine node f. Note that when f is a coarse node itself, i.e. f.atBigRoot, then these are all children of f.base, and that they get further restricted the deeper f sits inside the local tableau at f.base.

Equations

• (FinePathIn.inLoc lp lp_int).coarseChildrenBelow = List.map (fun (x : ↥(endNodesOf lt)) => match x with | ⟨val, Y_in⟩ => PathIn.loc Y_in PathIn.nil) lp.endNodesBelow
• FinePathIn.pdlHere.coarseChildrenBelow = [PathIn.nil.pdl]
• FinePathIn.lrepHere.coarseChildrenBelow = []
• (FinePathIn.loc Y_in tail).coarseChildrenBelow = List.map (PathIn.loc Y_in) tail.coarseChildrenBelow
• tail.pdl.coarseChildrenBelow = List.map PathIn.pdl tail.coarseChildrenBelow

theorem FinePathIn.exists_child_coarseChildrenBelow {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) (q : PathIn tab) (hq : q ∈ f.coarseChildrenBelow) : ∃ g ∈ f.children, g.base = f.base ∧ q ∈ g.coarseChildrenBelow ∨ g.base = q ∧ g.atBigRoot = true

If a coarse child q is below the fine node f, then f has a fine child g that is either still at the same coarse node and has q below it, or g is q.

theorem FinePathIn.eq_toFine_base_of_atBigRoot {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) (h : f.atBigRoot = true) : f = f.base.toFine

A fine node that is a coarse node is the image of that coarse node under toFine.

theorem PathIn.mem_coarseChildrenBelow_toFine {H : History} {X : Sequent} {tab : Tableau H X} (p q : PathIn tab) : p ⋖_ q → q ∈ p.toFine.coarseChildrenBelow

All children of a coarse node are below it in the fine sense. This is the converse of FinePathIn.base_of_mem_children for coarse nodes.

def Sequent.rightOnly (X : Sequent) : Sequent

The right component of a sequent, again as a sequent but with empty left component. This is Λ₂ from the paper; we use it to label the nodes of the quasi-tableau.

Equations

• X.rightOnly = (∅, X.2.1, X.2.2)

Well-founded descent for fine paths

The children of a fine node (FinePathIn.children) are not structurally smaller than the node itself: a child of an internal node of a local tableau is again a path in the same local tableau, and a child of the last internal node is a FinePathIn.loc step, hence even structurally bigger. So there is no induction principle for FinePathIn that follows the child relation for free.

Below we provide one, in the same way as PathIn.strong_upwards_inductionOn is obtained from flipEdge.wellFounded for the coarse PathIn nodes: we equip fine paths with a FinePathIn.length, bound it by a size measure Tableau.fineSize of the tableau, and conclude that there is no infinite chain of fine children — the child relation fineEdge has a well-founded flip. From that we get

• FinePathIn.edge_upwards_inductionOn — induction from the leaves to the root, and
• FinePathIn.strong_upwards_inductionOn — its strong version, where the inductive hypothesis is available at all fine descendants, not only at the children.

Dually, FinePathIn.descent states the descent principle in the contrapositive form in which it is used: if a property holds somewhere and always propagates to some child, then it holds at a node without children.

A length for local paths

def LocalPathIn.length {X : Sequent} {lt : LocalTableau X} : LocalPathIn lt → ℕ

The number of steps of a local path.

Equations

• LocalPathIn.nil.length = 0
• (LocalPathIn.cons Y_in tail).length = tail.length + 1

noncomputable def LocalTableau.nodeCount {X : Sequent} : LocalTableau X → ℕ

The number of nodes of a local tableau.

Equations

• One or more equations did not get rendered due to their size.
• (LocalTableau.sim a).nodeCount = 1

theorem LocalTableau.nodeCount_pos {X : Sequent} (lt : LocalTableau X) : 0 < lt.nodeCount

theorem LocalPathIn.length_lt_nodeCount {X : Sequent} {lt : LocalTableau X} (lp : LocalPathIn lt) : lp.length < lt.nodeCount

theorem LocalPathIn.length_lt_of_mem_children {X : Sequent} {lt : LocalTableau X} (lp lp' : LocalPathIn lt) : lp' ∈ lp.children → lp.length < lp'.length

Going to a child inside a local tableau increases the length.

A length for fine paths

noncomputable def Tableau.fineSize {H : History} {X : Sequent} : Tableau H X → ℕ

A size measure for tableaux that also counts the intermediate nodes of the local tableaux, i.e. an upper bound for the length of any FinePathIn.

Equations

• One or more equations did not get rendered due to their size.
• (Tableau.pdl nflprep bas r next).fineSize = 1 + next.fineSize
• (Tableau.lrep lpr).fineSize = 1

noncomputable def FinePathIn.length {H : History} {X : Sequent} {tab : Tableau H X} : FinePathIn tab → ℕ

The number of steps of a fine path, where a whole local tableau counts with its LocalTableau.nodeCount so that leaving it strictly increases the length.

Equations

• (FinePathIn.inLoc lp lp_int).length = lp.length
• FinePathIn.pdlHere.length = 0
• FinePathIn.lrepHere.length = 0
• (FinePathIn.loc Y_in tail).length = lt.nodeCount + tail.length
• tail.pdl.length = 1 + tail.length

theorem FinePathIn.length_lt_fineSize {H : History} {X : Sequent} {tab : Tableau H X} (f : FinePathIn tab) : f.length < tab.fineSize

theorem FinePathIn.length_lt_of_mem_children {H : History} {X : Sequent} {tab : Tableau H X} (f g : FinePathIn tab) : g ∈ f.children → f.length < g.length

Going to a fine child strictly increases the length of a fine path.

The child relation on fine nodes and its well-founded flip

def fineEdge {H : History} {X : Sequent} {tab : Tableau H X} (f g : FinePathIn tab) : Prop

The child relation on fine nodes, the fine analogue of edge.

Equations

• (f ⋖f g) = (g ∈ f.children)

def «term_⋖f_» : Lean.TrailingParserDescr

The child relation on fine nodes, the fine analogue of edge.

Equations

• «term_⋖f_» = Lean.ParserDescr.trailingNode `«term_⋖f_» 50 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋖f ") (Lean.ParserDescr.cat `term 51))

theorem fineEdge_then_length_lt {H : History} {X : Sequent} {tab : Tableau H X} {f g : FinePathIn tab} (h : f ⋖f g) : f.length < g.length

theorem flipFineEdge.wellFounded {H : History} {X : Sequent} {tab : Tableau H X} : WellFounded (flip fineEdge)

The flipped child relation on fine nodes is well-founded. Compare flipEdge.wellFounded.

The induction principles

theorem FinePathIn.edge_upwards_inductionOn {H : History} {X : Sequent} {tab : Tableau H X} {motive : FinePathIn tab → Prop} (up : ∀ {u : FinePathIn tab}, (∀ {s : FinePathIn tab}, u ⋖f s → motive s) → motive u) (t : FinePathIn tab) : motive t

Induction on fine nodes going from the leaves (= childless fine nodes) to the root. Compare PathIn.edge_upwards_inductionOn.

theorem FinePathIn.strong_upwards_inductionOn {H : History} {X : Sequent} {tab : Tableau H X} {motive : FinePathIn tab → Prop} (ups : ∀ {u : FinePathIn tab}, (∀ {s : FinePathIn tab}, Relation.TransGen fineEdge u s → motive s) → motive u) (t : FinePathIn tab) : motive t

Strong induction on fine nodes going from the leaves to the root: the motive may be assumed at all fine descendants. Compare PathIn.strong_upwards_inductionOn.

theorem FinePathIn.descent {H : History} {X : Sequent} {tab : Tableau H X} {P : FinePathIn tab → Prop} (down : ∀ (u : FinePathIn tab), P u → u.children ≠ ∅ → ∃ g ∈ u.children, P g) (t : FinePathIn tab) (ht : P t) : ∃ (u : FinePathIn tab), P u ∧ u.children = ∅

The descent principle for fine nodes: if a property holds at some fine node and, at every fine node where it holds and which has a child, it also holds at some child, then it holds at some childless fine node.

This is the form in which the well-foundedness is used when following a path downwards in the fine sense, cf. Lemma 9.7 (d) of the paper.

theorem FinePathIn.strong_descent {H : History} {X : Sequent} {tab : Tableau H X} {P : FinePathIn tab → Prop} (down : ∀ (u : FinePathIn tab), P u → u.children ≠ ∅ → ∃ (g : FinePathIn tab), Relation.TransGen fineEdge u g ∧ P g) (t : FinePathIn tab) (ht : P t) : ∃ (u : FinePathIn tab), P u ∧ u.children = ∅

The descent principle in the strong form: the property is only required to propagate to some fine descendant (not necessarily a child) as long as the node is not childless.