Navigating through tableaux with PathIn

To define relations between nodes in a tableau we need to represent the whole tableau and point to a specific node inside it. This is the PathIn type. Its values say "go to this child, then to this child, ... stop here."

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

A path in a tableau. Three constructors for the empty path, a local step or a pdl step. The loc and pdl steps correspond to two out of three constructors of Tableau. A PathIn only goes downwards, it cannot use LoadedPathRepeats.

• nil {Hist : History} {X : Sequent} {a✝ : Tableau Hist X} : PathIn a✝
• 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 : PathIn (next Y Y_in)) : PathIn (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 : PathIn next) : PathIn (Tableau.pdl nrep bas r next)

@[instance_reducible]

instance instDecidableEqPathIn {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} : DecidableEq (PathIn a✝)

Equations

• instDecidableEqPathIn = instDecidableEqPathIn.decEq

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

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqPathIn.decEq PathIn.nil PathIn.nil = isTrue ⋯
• instDecidableEqPathIn.decEq PathIn.nil (PathIn.loc Y_in tail) = isFalse ⋯
• instDecidableEqPathIn.decEq PathIn.nil tail.pdl = isFalse ⋯
• instDecidableEqPathIn.decEq (PathIn.loc Y_in tail) PathIn.nil = isFalse ⋯
• instDecidableEqPathIn.decEq tail.pdl PathIn.nil = isFalse ⋯
• instDecidableEqPathIn.decEq a_8.pdl b.pdl = if h : a_8 = b then h ▸ have inst := instDecidableEqPathIn.decEq a_8 a_8; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

def tabAt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : PathIn tab → (H : History) × (X : Sequent) × Tableau H X

Equations

• tabAt PathIn.nil = ⟨a✝¹, ⟨a✝, tab⟩⟩
• tabAt (PathIn.loc Y_in tail) = tabAt tail
• tabAt tail.pdl = tabAt tail

theorem tabAt_cast_gen {Hist : History} {X : Sequent} {tab : Tableau Hist X} (s : PathIn tab) (w : (H : History) × (X : Sequent) × Tableau H X) (h : tabAt s = w) (q : PathIn w.snd.snd) : tabAt (⋯ ▸ q) = tabAt q

Transporting a path along an equation about tabAt does not change tabAt. Compare PathIn.tabAt_cast which is about an equation between two tableaux.

def PathIn.append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : PathIn tab

Equations

• PathIn.nil.append q_2 = q_2
• (PathIn.loc Y_in tail).append q_2 = PathIn.loc Y_in (tail.append q_2)
• tail.pdl.append q_2 = (tail.append q_2).pdl

def PathIn.isLrep {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) : Prop

Equations

• p.isLrep = (tabAt p).snd.snd.isLrep

@[instance_reducible]

instance instDecdidablePathInisLrep {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) : Decidable p.isLrep

Equations

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

@[simp]

theorem append_eq_iff_eq {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (s : PathIn tab) (p q : PathIn (tabAt s).snd.snd) : s.append p = s.append q ↔ p = q

@[simp]

theorem PathIn.eq_append_iff_other_eq_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : p = p.append q ↔ q = nil

theorem PathIn.nil_eq_append_iff_both_eq_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : nil = p.append q ↔ p = nil ∧ q = nil

@[simp]

theorem tabAt_append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : tabAt (p.append q) = tabAt q

@[simp]

theorem tabAt_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} : tabAt PathIn.nil = ⟨Hist, ⟨X, tab⟩⟩

@[simp]

theorem tabAt_loc {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: H✝) Y} {a✝ : Sequent} {Y_in : a✝ ∈ endNodesOf lt} {tail : PathIn (next a✝ Y_in)} : tabAt (PathIn.loc Y_in tail) = tabAt tail

@[simp]

theorem tabAt_pdl {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {bas : X✝.basic} {Y✝ : Sequent} {r : PdlRule X✝ Y✝} {next : Tableau (X✝ :: H✝) Y✝} {tail : PathIn next} : tabAt tail.pdl = tabAt tail

def nodeAt {H : History} {X : Sequent} {tab : Tableau H X} (p : PathIn tab) : Sequent

Given a path to node t, this is its label Λ(t).

Equations

• nodeAt p = (tabAt p).snd.fst

@[simp]

theorem nodeAt_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} : nodeAt PathIn.nil = X

@[simp]

theorem nodeAt_loc {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: H✝) Y} {a✝ : Sequent} {Y_in : a✝ ∈ endNodesOf lt} {tail : PathIn (next a✝ Y_in)} : nodeAt (PathIn.loc Y_in tail) = nodeAt tail

@[simp]

theorem nodeAt_pdl {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {bas : X✝.basic} {Y✝ : Sequent} {r : PdlRule X✝ Y✝} {next : Tableau (X✝ :: H✝) Y✝} {tail : PathIn next} : nodeAt tail.pdl = nodeAt tail

@[simp]

theorem nodeAt_append {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : nodeAt (p.append q) = nodeAt q

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

Equations

• x✝.head = X

def PathIn.last {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) : Sequent

Equations

• t.last = (tabAt t).snd.fst

@[implicit_reducible]

def PathIn.length {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) : ℕ

The length of a path is the number of actual steps.

Equations

• PathIn.nil.length = 0
• tail.pdl.length = tail.length + 1
• (PathIn.loc Y_in tail).length = tail.length + 1

theorem append_length {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {p : PathIn tab} (q : PathIn (tabAt p).snd.snd) : (p.append q).length = p.length + q.length

Edge Relation

def edge {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (s t : PathIn tab) : Prop

Relation s ⋖_ t says t is a child of s. Two cases, both defined via append.

Equations

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

def «term_⋖__» : Lean.TrailingParserDescr

Notation ⋖_ for edge (because ⋖ is taken in Mathlib).

Equations

• «term_⋖__» = Lean.ParserDescr.trailingNode `«term_⋖__» 1022 1023 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⋖_ ") (Lean.ParserDescr.cat `term 1023))

theorem edge_append_loc_nil {sX : Sequent} {sHist : List Sequent} {nrep : ¬flprep sHist sX} {nbas : ¬sX.basic} {X : History} {Hist : Sequent} {tab : Tableau X Hist} (s : PathIn tab) {lt : LocalTableau sX} (next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (sX :: sHist) Y) {Y : Sequent} (Y_in : Y ∈ endNodesOf lt) (tabAt_s_def : tabAt s = ⟨sHist, ⟨sX, Tableau.loc nrep nbas lt next⟩⟩) : s ⋖_ (s.append (⋯ ▸ PathIn.loc Y_in PathIn.nil))

Appending a one-step loc path is also a ⋖_ child. When using this, this may be helpful: convert this; rw [← heq_iff_eq, heq_eqRec_iff_heq, eqRec_heq_iff_heq].

@[simp]

theorem edge_append_pdl_nil {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {s : PathIn a✝²} {nrep : ¬flprep (tabAt s).fst (tabAt s).snd.fst} {bas : (tabAt s).snd.fst.basic} {Y✝ : Sequent} {r : PdlRule (tabAt s).snd.fst Y✝} {next : Tableau ((tabAt s).snd.fst :: (tabAt s).fst) Y✝} (h : (tabAt s).snd.snd = Tableau.pdl nrep bas r next) : s ⋖_ (s.append (⋯ ▸ PathIn.nil.pdl))

Appending a one-step pdl path is also a ⋖_ child.

theorem edge_append_pdl_nil' {X : History} {Hist : Sequent} {tab : Tableau X Hist} (s : PathIn tab) {sHist : List Sequent} {sX sY : Sequent} {nrep : ¬flprep sHist sX} {bas : sX.basic} {r : PdlRule sX sY} (next : Tableau (sX :: sHist) sY) (tabAt_s_def : tabAt s = ⟨sHist, ⟨sX, Tableau.pdl nrep bas r next⟩⟩) : s ⋖_ (s.append (⋯ ▸ PathIn.nil.pdl))

Variant of edge_append_pdl_nil where the assumption is about all of tabAt s, analogous to edge_append_loc_nil.

@[simp]

theorem nil_edge_loc_nil {X Y : Sequent} {Hist : List Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {Y_in : Y ∈ endNodesOf lt} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} : PathIn.nil ⋖_ (PathIn.loc Y_in PathIn.nil)

@[simp]

theorem nil_edge_pdl_nil {Hist : List Sequent} {X : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {Y : Sequent} {r : PdlRule X Y} {next : Tableau (X :: Hist) Y} : PathIn.nil ⋖_ PathIn.nil.pdl

@[simp]

theorem loc_edge_loc_iff_edge {Y X : Sequent} {lt : LocalTableau X} {Y_in : Y ∈ endNodesOf lt} {tail : List Sequent} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: tail) Y} {nrep : ¬flprep tail X} {nbas : ¬X.basic} {t s : PathIn (next Y Y_in)} : (PathIn.loc Y_in t) ⋖_ (PathIn.loc Y_in s) ↔ t ⋖_ s

@[simp]

theorem pdl_edge_pdl_iff_edge {X Y : Sequent} {r : PdlRule X Y} {tail : List Sequent} {next : Tableau (X :: tail) Y} {nrep : ¬flprep tail X} {bas : X.basic} {t s : PathIn next} : t.pdl ⋖_ s.pdl ↔ t ⋖_ s

theorem not_edge_nil {Hist : History} {X : Sequent} (tab : Tableau Hist X) (t : PathIn tab) : ¬t ⋖_ PathIn.nil

The root has no parent. Note this holds even when Hist ≠ [].

theorem nodeAt_loc_nil {X Y : Sequent} {H : List Sequent} {lt : LocalTableau X} {nrep : ¬flprep H X} {nbas : ¬X.basic} (next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: H) Y) (Y_in : Y ∈ endNodesOf lt) : nodeAt (PathIn.loc Y_in PathIn.nil) = Y

theorem nodeAt_pdl_nil {X : Sequent} {Hist : List Sequent} {Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} (child : Tableau (X :: Hist) Y) (r : PdlRule X Y) : nodeAt PathIn.nil.pdl = Y

theorem nodeAt_of_edge {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (h : s ⋖_ t) : (∃ (lt : LocalTableau (nodeAt s)), nodeAt t ∈ endNodesOf lt) ∨ Nonempty (PdlRule (nodeAt s) (nodeAt t))

Any ⋖_ step is given by an end node of a local tableau or by a PDL rule.

theorem length_succ_eq_length_of_edge {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} : s ⋖_ t → s.length + 1 = t.length

The length of edge-related paths differs by one.

theorem edge_then_length_lt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} (s_t : s ⋖_ t) : s.length < t.length

def edge_natLT_relHom {Hist : History} {X : Sequent} {tab : Tableau Hist X} : edge →r Nat.lt

Equations

• edge_natLT_relHom = { toFun := PathIn.length, map_rel' := ⋯ }

theorem edge.wellFounded {Hist : History} {X : Sequent} {tab : Tableau Hist X} : WellFounded edge

The ⋖_ relation in a tableau is well-founded. Proven by lifting the relation to the length of histories. That length goes up with ⋖_, so because < is wellfounded on Nat also ⋖_ is well-founded via RelHomClass.wellFounded.

instance edge.isAsymm {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : Std.Asymm edge

theorem edge_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} : s ⋖_ t → s ≠ t

def PathIn.children {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (p : PathIn tab) : Finset { q : PathIn tab // p ⋖_ q }

Equations

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

theorem PathIn.children_spec {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} : p ⋖_ q ↔ q ∈ Finset.image Subtype.val p.children

@[instance_reducible]

instance instDecidableEdge {H : History} {X : Sequent} {tab : Tableau H X} (p q : PathIn tab) : Decidable (p ⋖_ q)

Equations

• instDecidableEdge p q = decidable_of_iff (q ∈ Finset.image Subtype.val p.children) ⋯

theorem PathIn.init_inductionOn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) {motive : PathIn tab → Prop} (root : motive nil) (step : ∀ (t : PathIn tab), motive t → ∀ {s : PathIn tab}, t ⋖_ s → motive s) : motive t

An induction principle for PathIn with a base case at the root of the tableau and an induction step using the edge relation ⋖_.

QUESTIONS:

• Do we need to add any of these attributes? @[induction_eliminator, elab_as_elim]
• Should it be a def or a theorem? (motive to Prop or to Sort u?)

Transitive Closure of the Edge Relation

@[instance_reducible]

instance instLTPathIn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : LT (PathIn tab)

Enable "<" notation for transitive closure of ⋖_.

Equations

• instLTPathIn = { lt := Relation.TransGen edge }

@[instance_reducible]

instance instLEPathIn {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : LE (PathIn tab)

Enable "≤" notation for reflexive transitive closure of ⋖_

Equations

• instLEPathIn = { le := Relation.ReflTransGen edge }

instance edge.TransGen_isAsymm {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : Std.Asymm (Relation.TransGen edge)

The "<" in a tableau is antisymmetric.

theorem not_path_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} : ¬a < PathIn.nil

theorem path_is_strict_ordering {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} : s < t → s ≠ t

theorem PathIn.nil_le_anything {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {t : PathIn a✝²} : nil ≤ t

theorem PathIn.loc_le_loc_of_le {Hist : History} {X : Sequent} {Y : ¬flprep Hist X} {nrep : ¬X.basic} {nbas : LocalTableau X} {lt : (Y : Sequent) → Y ∈ endNodesOf nbas → Tableau (X :: Hist) Y} {next : Sequent} {Z_in : next ∈ endNodesOf nbas} {t1 t2 : PathIn (lt next Z_in)} (h : t1 ≤ t2) : loc Z_in t1 ≤ loc Z_in t2

theorem PathIn.pdl_le_pdl_of_le {Hist : History} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {Z_in : Tableau (X :: Hist) Y} {t1 t2 : PathIn Z_in} (h : t1 ≤ t2) : t1.pdl ≤ t2.pdl

theorem PathIn.length_le_of_le {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (h : s ≤ t) : s.length ≤ t.length

Paths further down are longer.

Path cast and append lemmas

Lemmas developed for tabToIntAt.

@[simp]

theorem PathIn.cast_nil {a✝ : History} {a✝¹ : Sequent} {tab tab2 : Tableau a✝ a✝¹} (h : tab = tab2) : h ▸ nil = nil

@[simp]

theorem PathIn.tabAt_cast_nil {a✝ : History} {a✝¹ : Sequent} {tab tab2 : Tableau a✝ a✝¹} (h : tab = tab2) : tabAt (h ▸ nil) = tabAt nil

@[simp]

theorem PathIn.tabAt_cast_loc {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {nexts : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: H✝) Y} {tab2 : Tableau H✝ X✝} {Y : Sequent} {Y_in : Y ∈ endNodesOf lt} (h : Tableau.loc nrep nbas lt nexts = tab2) (tail : PathIn (nexts Y Y_in)) : tabAt (h ▸ loc Y_in tail) = tabAt tail

@[simp]

theorem PathIn.tabAt_cast_pdl {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {bas : X✝.basic} {Y✝ : Sequent} {r : PdlRule X✝ Y✝} {next : Tableau (X✝ :: H✝) Y✝} {tab2 : Tableau H✝ X✝} {tail : PathIn next} (h : Tableau.pdl nrep bas r next = tab2) : tabAt (h ▸ tail.pdl) = tabAt tail

@[simp]

theorem PathIn.tabAt_cast {a✝ : History} {a✝¹ : Sequent} {tab tab2 : Tableau a✝ a✝¹} (p : PathIn tab) (h : tab = tab2) : tabAt (h ▸ p) = tabAt p

theorem PathIn.append_append {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) (r : PathIn (tabAt (p.append q)).snd.snd) : (p.append q).append r = p.append (q.append (⋯ ▸ r))

(p ++ q) ++ r = p ++ (q ++ r)

@[simp]

theorem PathIn.loc_append {X : Sequent} {Hist : History} {nflprep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {nexts : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} {Y : Sequent} {Y_in : Y ∈ endNodesOf lt} {tail : PathIn (tabAt (loc Y_in nil)).snd.snd} (h : PathIn (nexts Y Y_in) = PathIn (tabAt (loc Y_in nil)).snd.snd) : (loc Y_in nil).append tail = loc Y_in (⋯ ▸ tail)

@[simp]

theorem PathIn.pdl_append {Hist : List Sequent} {X Y : Sequent} {next : Tableau (X :: Hist) Y} {nflprep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {tail : PathIn (tabAt nil.pdl).snd.snd} (h : PathIn next = PathIn (tabAt nil.pdl).snd.snd) : nil.pdl.append tail = (⋯ ▸ tail).pdl

theorem PathIn.lt_append_non_nil {Hist : History} {X : Sequent} {pHist : History} {pX : Sequent} {tabNew : Tableau pHist pX} {tab : Tableau Hist X} (p : PathIn tab) (h : tabAt p = ⟨pHist, ⟨pX, tabNew⟩⟩) (q : PathIn tabNew) : q ≠ nil → p < p.append (⋯ ▸ q)

Used for tabToIntAt.

theorem PathIn.le_append {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : p ≤ p.append q

Appending to a path goes further down.

From Path to History

@[implicit_reducible]

def PathIn.toHistory {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) : History

Convert a path to a History. Does not include the last node. The history of .nil is [] because this will not go into Hist.

Equations

• PathIn.nil.toHistory = []
• tail.pdl.toHistory = tail.toHistory ++ [X]
• (PathIn.loc Y_in tail).toHistory = tail.toHistory ++ [X]

theorem PathIn.toHistory_length_eq_length {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) : List.length t.toHistory = t.length

The history of a path has one entry for each step of the path.

def PathIn.toList {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) : List Sequent

Convert a path to a list of nodes. Reverse of the history and does include the last node. The list of .nil is [X].

Equations

• PathIn.nil.toList = [X]
• tail.pdl.toList = X :: tail.toList
• (PathIn.loc Y_in tail).toList = X :: tail.toList

theorem PathIn.toHistory_eq_Hist {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) : t.toHistory ++ Hist = (tabAt t).fst

A path gives the same list of nodes as the history of its last node.

theorem tabAt_fst_length_eq_toHistory_length {X : Sequent} {tab : Tableau [] X} (s : PathIn tab) : List.length (tabAt s).fst = List.length s.toHistory

@[simp]

theorem PathIn.loc_length_eq {X Y : Sequent} {Hist : List Sequent} {nrep : ¬flprep Hist X} {nbas : ¬X.basic} {lt : LocalTableau X} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X :: Hist) Y} (Y_in : Y ∈ endNodesOf lt) (tail : PathIn (next Y Y_in)) : List.length (loc Y_in tail).toHistory = List.length tail.toHistory + 1

@[simp]

theorem PathIn.pdl_length_eq {X Y : Sequent} {Hist : List Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {next : Tableau (X :: Hist) Y} {r : PdlRule X Y} (tail : PathIn next) : List.length tail.pdl.toHistory = List.length tail.toHistory + 1

def PathIn.prefix {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (t.length + 1)) : PathIn tab

Prefix of a path, taking only the first k steps.

Equations

• PathIn.nil.prefix x_2 = PathIn.nil
• tail.pdl.prefix k = Fin.cases PathIn.nil (fun (j : Fin tail.pdl.length) => (tail.prefix j).pdl) k
• (PathIn.loc Y_in tail).prefix k = Fin.cases PathIn.nil (fun (j : Fin (PathIn.loc Y_in tail).length) => PathIn.loc Y_in (tail.prefix j)) k

Path Rewinding

def PathIn.rewind {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) : PathIn tab

Rewinding a path, removing the last k steps. Cannot go into Hist. Used to go to the companion of a repeat. Returns .nil when k is the length of the whole path. We use +1 in the type because rewind 0 is always possible, even with history []. Defined using Fin.lastCases.

Hint: when proving stuff about rewind k, avoid induction on k, because rewind does not decrease k.

Equations

• PathIn.nil.rewind x_2 = PathIn.nil
• (PathIn.loc Y_in tail).rewind k = Fin.lastCases PathIn.nil (PathIn.loc Y_in ∘ tail.rewind ∘ Fin.cast ⋯) k
• tail.pdl.rewind k = Fin.lastCases PathIn.nil (PathIn.pdl ∘ tail.rewind ∘ Fin.cast ⋯) k

theorem PathIn.rewind_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} {p : PathIn tab} : p.rewind 0 = p

Rewinding 0 steps does nothing.

theorem PathIn.rewind_le {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) : t.rewind k ≤ t

theorem PathIn.rewind_length {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) : (t.rewind k).length + ↑k = t.length

Rewinding a path by k steps makes it k steps shorter.

theorem PathIn.rewind_length_lt_length_of_gt_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) (k_gt_zero : k > 0) : (t.rewind k).length < t.length

If we rewind by k > 0 steps then the length goes down.

theorem PathIn.rewind_lt_of_gt_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) (k_gt_zero : k > 0) : t.rewind k < t

theorem PathIn.nodeAt_rewind_eq_toHistory_get {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) : nodeAt (t.rewind k) = (nodeAt t :: t.toHistory).get k

The node we get from rewinding k steps is element k+1 in the history.

theorem nil_iff_length_zero {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} : a = PathIn.nil ↔ a.toHistory = []

theorem PathIn.loc_injective {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} {ta tb : PathIn (next Y Y_in)} : loc Y_in ta = loc Y_in tb → ta = tb

theorem PathIn.pdl_injective {Hist : History} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {next : Tableau (X :: Hist) Y} (r : PdlRule X Y) (ta tb : PathIn next) : ta.pdl = tb.pdl → ta = tb

theorem edge_is_irreflexive {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} : ¬a ⋖_ a

theorem path_then_length_lt {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {s t : PathIn tab} (s_t : s < t) : s.length < t.length

theorem path_is_irreflexive {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a : PathIn tab} : ¬Relation.TransGen edge a a

theorem rewind_order_reversing {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h : k < k') : t.rewind k' ≤ t.rewind k

theorem PathIn.loc_lt_loc_of_lt {Hist : History} {X : Sequent} {Y : ¬flprep Hist X} {nrep : ¬X.basic} {nbas : LocalTableau X} {lt : (Y : Sequent) → Y ∈ endNodesOf nbas → Tableau (X :: Hist) Y} {next : Sequent} {Z_in : next ∈ endNodesOf nbas} {t1 t2 : PathIn (lt next Z_in)} (h : t1 < t2) : loc Z_in t1 < loc Z_in t2

theorem PathIn.pdl_lt_pdl_of_lt {Hist : History} {X Y : Sequent} {nrep : ¬flprep Hist X} {bas : X.basic} {r : PdlRule X Y} {Z_in : Tableau (X :: Hist) Y} {t1 t2 : PathIn Z_in} (h : t1 < t2) : t1.pdl < t2.pdl

theorem one_is_one_helper {k : ℕ} {h : k > 0} : 1 = ↑1

theorem rewind_of_edge_is_eq {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (a_b : a ⋖_ b) : b.rewind 1 = a

theorem rewind_order_reversing_if_not_nil {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h : k < k') (h' : t ≠ PathIn.nil) : t.rewind k' < t.rewind k

theorem rewind_is_inj {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h1 : t.rewind k = t.rewind k') : k = k'

theorem one_is_one_rewind_helper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {b : PathIn tab} {k : Fin (List.length b.toHistory + 1)} (h : (b.rewind k) ⋖_ b) : k = 1

theorem edge_leftInjective {Hist : History} {X : Sequent} {tab : Tableau Hist X} (a b c : PathIn tab) : a ⋖_ c → b ⋖_ c → a = b

theorem edge_revEuclideanHelper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) : a ⋖_ c → b < c → b ≤ a

theorem path_revEuclidean {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) : a < c → b < c → a < b ∨ b < a ∨ b = a

theorem path_revEuclidean' {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} (a b c : PathIn tab) : a < c → b < c → a ≤ b ∨ b ≤ a

theorem edge_inc_length_by_one {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (a_b : a ⋖_ b) : List.length a.toHistory + 1 + 1 = List.length b.toHistory + 1

theorem rewind_helper {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} {k : Fin (List.length a.toHistory + 1)} (a_b : a ⋖_ b) : b.rewind (Fin.cast ⋯ k.succ) = a.rewind k

theorem exists_rewind_of_le {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b : PathIn tab} (h : a ≤ b) : ∃ (k : Fin (List.length b.toHistory + 1)), b.rewind k = a

theorem exists_rewinds_middle {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} {a b c : PathIn tab} (h : a ≤ b) (h' : b ≤ c) : ∃ (k : Fin (List.length c.toHistory + 1)) (k' : Fin (List.length c.toHistory + 1)), c.rewind k = a ∧ c.rewind k' = b ∧ k' ≤ k

Finiteness and Wellfoundedness

def Finset.join {α : Type u_1} [DecidableEq α] (M : Finset (Finset α)) : Finset α

Equations

• M.join = M.sup id

def allPaths {Hist : History} {X : Sequent} (tab : Tableau Hist X) : Finset (PathIn tab)

Equations

• One or more equations did not get rendered due to their size.
• allPaths (Tableau.pdl nflprep bas r next) = {PathIn.nil} ∪ Finset.image (fun (p : PathIn next) => p.pdl) (allPaths next)
• allPaths (Tableau.lrep lpr) = {PathIn.nil}

theorem allPaths_loc_cases {H✝ : History} {X✝ : Sequent} {nrep : ¬flprep H✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: H✝) Y} (s : PathIn (Tableau.loc nrep nbas lt next)) : s ∈ allPaths (Tableau.loc nrep nbas lt next) ↔ s = PathIn.nil ∨ ∃ (Y : Sequent) (Y_in : Y ∈ endNodesOf lt), ∃ t ∈ allPaths (next Y Y_in), s = PathIn.loc Y_in t

theorem PathIn.elem_allPaths {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : p ∈ allPaths tab

@[instance_reducible]

instance PathIn.instFintype {Hist : History} {X : Sequent} {tab : Tableau Hist X} : Fintype (PathIn tab)

A Tableau is finite. Should be useful to get converse well-foundedness of edge

Equations

• PathIn.instFintype = { elems := allPaths tab, complete := ⋯ }

theorem Finite.wellfounded_of_irrefl_TC {α : Type} [Finite α] (r : α → α → Prop) (h : Std.Irrefl (Relation.TransGen r)) : WellFounded r

theorem nodeAt_mem_History_of_edge {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} : p ⋖_ q → nodeAt p ∈ (tabAt q).fst

theorem mem_History_of_edge {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} {x : Sequent} : p ⋖_ q → x ∈ (tabAt p).fst → x ∈ (tabAt q).fst

theorem mem_History_append {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p : PathIn a✝²} {X : Sequent} {q : PathIn (tabAt p).snd.snd} : X ∈ (tabAt p).fst → X ∈ (tabAt (p.append q)).fst

theorem edge_TransGen_then_mem_History {a✝ : History} {a✝¹ : Sequent} {a✝² : Tableau a✝ a✝¹} {p q : PathIn a✝²} : Relation.TransGen edge p q → nodeAt p ∈ (tabAt q).fst

Wellfoundedness of flip edge

The lemmas and instances here are used for tabToIntAt.

theorem PathIn.length_lt_tab_size {H : History} {X : Sequent} (tab : Tableau H X) (p : PathIn tab) : p.length < tab.size

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

The flip edge relation in a tableau is well-founded.

theorem PathIn.edge_upwards_inductionOn {Hist : History} {X : Sequent} {tab : Tableau Hist X} {motive : PathIn tab → Prop} (up : ∀ {u : PathIn tab}, (∀ {s : PathIn tab}, u ⋖_ s → motive s) → motive u) (t : PathIn tab) : motive t

Induction principle going from the leaves (= childless nodes) to the root. Suppose whenever the motive holds at all children then it holds at the parent. Then it holds at all nodes.

theorem Relation.TransGen_flip_iff {α : Sort u_1} {s t : α} {r : α → α → Prop} : TransGen (flip r) s t ↔ TransGen r t s

theorem PathIn.strong_upwards_inductionOn {Hist : History} {X : Sequent} {tab : Tableau Hist X} {motive : PathIn tab → Prop} (ups : ∀ {u : PathIn tab}, (∀ {s : PathIn tab}, u < s → motive s) → motive u) (t0 : PathIn tab) : motive t0

Strong induction from the leaves (= childless nodes) to the root. Suppose whenever the motive holds at all successors then it holds at the parent. Then it holds at all nodes.

theorem Tableau.lprBounded_of_paths {Hist : History} {X : Sequent} (tab : Tableau Hist X) (n : ℕ) (h : ∀ (q : PathIn tab) (lpr : LoadedPathRepeat (tabAt q).fst (tabAt q).snd.fst), (tabAt q).snd.snd = lrep lpr → ↑↑lpr < n + q.length) : tab.lprBounded n

To show lprBounded it suffices to bound all loaded-path repeats reached by paths.