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

Equations

• PDL.instDecidableEqPathIn = PDL.instDecidableEqPathIn.decEq

def PDL.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.
• PDL.instDecidableEqPathIn.decEq PDL.PathIn.nil PDL.PathIn.nil = isTrue ⋯
• PDL.instDecidableEqPathIn.decEq PDL.PathIn.nil (PDL.PathIn.loc Y_in tail) = isFalse ⋯
• PDL.instDecidableEqPathIn.decEq PDL.PathIn.nil tail.pdl = isFalse ⋯
• PDL.instDecidableEqPathIn.decEq (PDL.PathIn.loc Y_in tail) PDL.PathIn.nil = isFalse ⋯
• PDL.instDecidableEqPathIn.decEq tail.pdl PDL.PathIn.nil = isFalse ⋯
• PDL.instDecidableEqPathIn.decEq a_8.pdl b.pdl = if h : a_8 = b then h ▸ have inst := PDL.instDecidableEqPathIn.decEq a_8 a_8; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

def PDL.tabAt {Hist : History} {X : Sequent} {tab : Tableau Hist X} : PathIn tab → (H : History) × (X : Sequent) × Tableau H X

The tableau reached by a path, together with its history and root sequent.

Equations

• PDL.tabAt PDL.PathIn.nil = ⟨Hist, ⟨X, tab⟩⟩
• PDL.tabAt (PDL.PathIn.loc Y_in tail) = PDL.tabAt tail
• PDL.tabAt tail.pdl = PDL.tabAt tail

theorem PDL.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 PDL.PathIn.append {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : PathIn tab

Append a path in the reached tableau to an initial path.

Equations

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

def PDL.PathIn.isLrep {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : Prop

Whether the tableau reached by a path is a loaded-path-repeat leaf.

Equations

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

@[instance_reducible]

instance PDL.instDecdidablePathInisLrep {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : Decidable p.isLrep

Equations

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

@[simp]

theorem PDL.append_eq_iff_eq {Hist : History} {X : Sequent} {tab : Tableau Hist X} (s : PathIn tab) (p q : PathIn (tabAt s).snd.snd) : s.append p = s.append q ↔ p = q

@[simp]

theorem PDL.PathIn.eq_append_iff_other_eq_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : p = p.append q ↔ q = nil

theorem PDL.PathIn.nil_eq_append_iff_both_eq_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : nil = p.append q ↔ p = nil ∧ q = nil

@[simp]

theorem PDL.tabAt_append {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : tabAt (p.append q) = tabAt q

@[simp]

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

@[simp]

theorem PDL.tabAt_loc {Hist : History} {X Y : 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)} : tabAt (PathIn.loc Y_in tail) = tabAt tail

@[simp]

theorem PDL.tabAt_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} : tabAt tail.pdl = tabAt tail

def PDL.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

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

@[simp]

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

@[simp]

theorem PDL.nodeAt_loc {Hist : History} {X Y : 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)} : nodeAt (PathIn.loc Y_in tail) = nodeAt tail

@[simp]

theorem PDL.nodeAt_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} : nodeAt tail.pdl = nodeAt tail

@[simp]

theorem PDL.nodeAt_append {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) (q : PathIn (tabAt p).snd.snd) : nodeAt (p.append q) = nodeAt q

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

The root sequent of the tableau containing a path.

Equations

• x✝.head = X

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

The sequent reached at the end of a path.

Equations

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

@[implicit_reducible]

def PDL.PathIn.length {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) : ℕ

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

Equations

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

theorem PDL.append_length {Hist : History} {X : Sequent} {tab : Tableau Hist X} {p : PathIn tab} (q : PathIn (tabAt p).snd.snd) : (p.append q).length = p.length + q.length

Edge Relation

def PDL.edge {Hist : History} {X : Sequent} {tab : Tableau Hist X} (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 PDL.«term_⋖__» : Lean.TrailingParserDescr

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

Equations

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

theorem PDL.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⟩⟩) : edge 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 PDL.edge_append_pdl_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s : PathIn tab} {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) : edge s (s.append (⋯ ▸ PathIn.nil.pdl))

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

theorem PDL.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⟩⟩) : edge 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 PDL.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} : edge PathIn.nil (PathIn.loc Y_in PathIn.nil)

@[simp]

theorem PDL.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} : edge PathIn.nil PathIn.nil.pdl

@[simp]

theorem PDL.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)} : edge (PathIn.loc Y_in t) (PathIn.loc Y_in s) ↔ edge t s

@[simp]

theorem PDL.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} : edge t.pdl s.pdl ↔ edge t s

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

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

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

theorem PDL.nodeAt_of_edge {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (h : edge 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 PDL.length_succ_eq_length_of_edge {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} : edge s t → s.length + 1 = t.length

The length of edge-related paths differs by one.

theorem PDL.edge_then_length_lt {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (s_t : edge s t) : s.length < t.length

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

Map tableau edges to strict increases in path length.

Equations

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

theorem PDL.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 PDL.edge.isAsymm {Hist : History} {X : Sequent} {tab : Tableau Hist X} : Std.Asymm edge

theorem PDL.edge_is_strict_ordering {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} : edge s t → s ≠ t

def PDL.PathIn.children {Hist : History} {X : Sequent} {tab : Tableau Hist X} (p : PathIn tab) : Finset { q : PathIn tab // edge p q }

Enumerate the immediate children of a tableau path.

Equations

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

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

@[instance_reducible]

instance PDL.instDecidableEdge {H : History} {X : Sequent} {tab : Tableau H X} (p q : PathIn tab) : Decidable (edge p q)

Equations

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

theorem PDL.PathIn.init_inductionOn {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) {motive : PathIn tab → Prop} (root : motive nil) (step : ∀ (t : PathIn tab), motive t → ∀ {s : PathIn tab}, edge 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 PDL.instLTPathIn {Hist : History} {X : Sequent} {tab : Tableau Hist X} : LT (PathIn tab)

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

Equations

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

@[instance_reducible]

instance PDL.instLEPathIn {Hist : History} {X : Sequent} {tab : Tableau Hist X} : LE (PathIn tab)

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

Equations

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

instance PDL.edge.TransGen_isAsymm {Hist : History} {X : Sequent} {tab : Tableau Hist X} : Std.Asymm (Relation.TransGen edge)

The "<" in a tableau is antisymmetric.

theorem PDL.not_path_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a : PathIn tab} : ¬a < PathIn.nil

theorem PDL.path_is_strict_ordering {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} : s < t → s ≠ t

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

theorem PDL.PathIn.loc_le_loc_of_le {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} {Z_in : Y ∈ endNodesOf lt} {t1 t2 : PathIn (next Y Z_in)} (h : t1 ≤ t2) : loc Z_in t1 ≤ loc Z_in t2

theorem PDL.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

Path cast and append lemmas

Lemmas developed for tabToIntAt.

@[simp]

theorem PDL.PathIn.cast_nil {Hist : History} {X : Sequent} {tab tab2 : Tableau Hist X} (h : tab = tab2) : h ▸ nil = nil

theorem PDL.PathIn.tabAt_cast_nil {Hist : History} {X : Sequent} {tab tab2 : Tableau Hist X} (h : tab = tab2) : tabAt (h ▸ nil) = tabAt nil

theorem PDL.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

theorem PDL.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 PDL.PathIn.tabAt_cast {Hist : History} {X : Sequent} {tab tab2 : Tableau Hist X} (p : PathIn tab) (h : tab = tab2) : tabAt (h ▸ p) = tabAt p

theorem PDL.PathIn.append_append {X : Sequent} {Hist : History} {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 PDL.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 PDL.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 PDL.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.

From Path to History

@[implicit_reducible]

def PDL.PathIn.toHistory {X : Sequent} {Hist : History} {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

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

def PDL.PathIn.toList {X : Sequent} {Hist : History} {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

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

theorem PDL.PathIn.toHistory_eq_Hist {X : Sequent} {Hist : History} {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 PDL.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 PDL.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 PDL.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 PDL.PathIn.prefix {X : Sequent} {Hist : History} {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

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

theorem PDL.PathIn.prefix_toList_eq_toList_take {X : Sequent} {Hist : History} {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 PDL.PathIn.rewind {Hist : History} {X : Sequent} {tab : Tableau Hist X} (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

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

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

Rewinding 0 steps does nothing.

theorem PDL.PathIn.rewind_le {Hist : History} {X : Sequent} {tab : Tableau Hist X} (t : PathIn tab) (k : Fin (List.length t.toHistory + 1)) : t.rewind k ≤ t

theorem PDL.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 PDL.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 PDL.PathIn.nodeAt_rewind_eq_toHistory_get {X : Sequent} {Hist : History} {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 PDL.nil_iff_length_zero {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a : PathIn tab} : a = PathIn.nil ↔ a.toHistory = []

theorem PDL.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 PDL.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 PDL.edge_is_irreflexive {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a : PathIn tab} : ¬edge a a

theorem PDL.path_then_length_lt {Hist : History} {X : Sequent} {tab : Tableau Hist X} {s t : PathIn tab} (s_t : s < t) : s.length < t.length

theorem PDL.path_is_irreflexive {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a : PathIn tab} : ¬Relation.TransGen edge a a

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

theorem PDL.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 PDL.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 PDL.one_is_one_helper {k : ℕ} {h : k > 0} : 1 = ↑1

theorem PDL.rewind_of_edge_is_eq {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a b : PathIn tab} (a_b : edge a b) : b.rewind 1 = a

theorem PDL.rewind_order_reversing_if_not_nil {Hist : History} {X : Sequent} {tab : Tableau Hist X} {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 PDL.rewind_is_inj {Hist : History} {X : Sequent} {tab : Tableau Hist X} {t : PathIn tab} {k k' : Fin (List.length t.toHistory + 1)} (h1 : t.rewind k = t.rewind k') : k = k'

theorem PDL.one_is_one_rewind_helper {Hist : History} {X : Sequent} {tab : Tableau Hist X} {b : PathIn tab} {k : Fin (List.length b.toHistory + 1)} (h : edge (b.rewind k) b) : k = 1

theorem PDL.edge_leftInjective {X : Sequent} {Hist : History} {tab : Tableau Hist X} (a b c : PathIn tab) : edge a c → edge b c → a = b

theorem PDL.edge_revEuclideanHelper {Hist : History} {X : Sequent} {tab : Tableau Hist X} (a b c : PathIn tab) : edge a c → b < c → b ≤ a

theorem PDL.path_revEuclidean {Hist : History} {X : Sequent} {tab : Tableau Hist X} (a b c : PathIn tab) : a < c → b < c → a < b ∨ b < a ∨ b = a

theorem PDL.path_revEuclidean' {Hist : History} {X : Sequent} {tab : Tableau Hist X} (a b c : PathIn tab) : a < c → b < c → a ≤ b ∨ b ≤ a

theorem PDL.edge_inc_length_by_one {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a b : PathIn tab} (a_b : edge a b) : List.length a.toHistory + 1 + 1 = List.length b.toHistory + 1

theorem PDL.rewind_helper {Hist : History} {X : Sequent} {tab : Tableau Hist X} {a b : PathIn tab} {k : Fin (List.length a.toHistory + 1)} (a_b : edge a b) : b.rewind (Fin.cast ⋯ k.succ) = a.rewind k

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

theorem PDL.exists_rewinds_middle {Hist : History} {X : Sequent} {tab : Tableau Hist X} {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.pdlJoin {α : Type u_1} [DecidableEq α] (M : Finset (Finset α)) : Finset α

The union of a finite family of finsets.

Equations

• M.pdlJoin = M.sup id

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

Enumerate every path in a tableau.

Equations

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

theorem PDL.allPaths_loc_cases {Hist : History} {X : Sequent} {nrep : ¬flprep 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 ∈ allPaths (next Y Y_in), s = PathIn.loc Y_in t

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

@[instance_reducible]

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

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

Equations

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

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

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

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

theorem PDL.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 PDL.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 PDL.PathIn.length_lt_tab_size {H : History} {X : Sequent} (tab : Tableau H X) (p : PathIn tab) : p.length < tab.size

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

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

theorem PDL.PathIn.edge_upwards_inductionOn {Hist : History} {X : Sequent} {tab : Tableau Hist X} {motive : PathIn tab → Prop} (up : ∀ {u : PathIn tab}, (∀ {s : PathIn tab}, edge 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 PDL.Relation.TransGen_flip_iff {α : Sort u_1} {s t : α} {r : α → α → Prop} : Relation.TransGen (flip r) s t ↔ Relation.TransGen r t s

theorem PDL.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.