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 : ¬rep 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 : ¬rep 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 instDecidableEqPathIn {Hist✝ : History} {X✝ : Sequent} {a✝ : Tableau Hist✝ X✝} : DecidableEq (PathIn a✝)

Equations

• instDecidableEqPathIn = decEqPathIn✝

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

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

@[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 {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: Hist✝) 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 {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {bas : X✝.basic} {Δ✝ : Sequent} {r : PdlRule X✝ Δ✝} {next : Tableau (X✝ :: Hist✝) Δ✝} {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 {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: Hist✝) 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 {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {bas : X✝.basic} {Δ✝ : Sequent} {r : PdlRule X✝ Δ✝} {next : Tableau (X✝ :: Hist✝) Δ✝} {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

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 : ¬rep 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 : ¬rep (tabAt s).fst (tabAt s).snd.fst} {bas : (tabAt s).snd.fst.basic} {Δ✝ : Sequent} {r : PdlRule (tabAt s).snd.fst Δ✝} {next : Tableau ((tabAt s).snd.fst :: (tabAt s).fst) Δ✝} (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.

@[simp]

theorem nil_edge_loc_nil {X Y : Sequent} {Hist : List Sequent} {nrep : ¬rep 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 : ¬rep 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 : ¬rep 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 : ¬rep 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 : ¬rep 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 : ¬rep Hist X} {bas : X.basic} (child : Tableau (X :: Hist) Y) (r : PdlRule X Y) : nodeAt PathIn.nil.pdl = Y

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✝¹} : IsAsymm (PathIn tab) edge

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 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✝¹} : IsAsymm (PathIn tab) (Relation.TransGen edge)

The "<" in a tableau is antisymmetric.

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?)

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 : ¬rep 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 : ¬rep 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

From Path to History

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]

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 : ¬rep 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 : ¬rep 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

theorem PathIn.prefix_toList_eq_toList_take {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (t.length + 1)) : (t.prefix k).toList = List.take (↑k + 1) t.toList

The list of a prefix of a path is the same as the prefix of the list of the path.

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.

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_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).length < t.length

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

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.

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

Finiteness and Wellfoundedness -

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 nrep 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 {Hist✝ : History} {X✝ : Sequent} {nrep : ¬rep Hist✝ X✝} {nbas : ¬X✝.basic} {lt : LocalTableau X✝} {next : (Y : Sequent) → Y ∈ endNodesOf lt → Tableau (X✝ :: Hist✝) 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 : { x : PathIn (next Y Y_in) // x ∈ 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 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 : IsIrrefl α (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

theorem PathIn.mem_history_setEqTo_then_lrep {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : (∃ Y ∈ (tabAt p).fst, Y.setEqTo (nodeAt p)) → (tabAt p).snd.snd.isLrep

theorem single_of_transgen {α : Sort u_1} {r : α → α → Prop} {a c : α} : Relation.TransGen r a c → ∃ (b : α), r a b

instance flipEdge.instIsIrrefl {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : IsIrrefl (PathIn tab) (Relation.TransGen (flip edge))

theorem flipEdge.wellFounded {a✝ : History} {a✝¹ : Sequent} {tab : Tableau a✝ a✝¹} : 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.