Positions of a rose tree

The positions of a rose tree t form RoseTree.Positions t, a subtype of TreePath. Since validPaths t is prefix-closed, the positions inherit the order structure of TreePath: the root is the least position, the parent of a position and the meet of two positions are again positions, and strict dominance is well founded, so Positions t is a rooted tree in the sense of Mathlib/Order/SuccPred/Tree.lean. Covering in Positions t is covering in TreePath (Positions.covBy_iff), so the daughters of a position are its valid daughters, and the subtree at a position (Positions.subtree) has the subtrees at its covers as daughters (Positions.mem_children_subtree) and the subtrees at the positions below it as subtrees (Positions.isSubtree_subtree).

The positions whose subtree satisfies a predicate form RoseTree.positionsWhere P t, decidable when the predicate is, which picks out the positions of a label, of a branching node, or of any other condition on a node and what it dominates. Replacing the subtree at a position leaves the positions outside it where they were, for a predicate that does not look below the root (mem_positionsWhere_replaceAt). The topmost and bottommost of the positions are their Minimal and Maximal members, the root being least, and both are decidable: the positions above one are its prefixes, and those below it in the tree are among vertices.

Main declarations

• RoseTree.Positions: the positions of a tree, a rooted tree under the prefix order.
• RoseTree.Positions.subtree: the subtree at a position.
• RoseTree.positionsWhere: the positions whose subtree satisfies a predicate.

@[reducible, inline]

abbrev RoseTree.Positions {α : Type u_1} (t : RoseTree α) : Type

The valid positions of t, as a subtype of TreePath, form a rooted tree under the prefix order.

Equations

• t.Positions = { p : Core.Order.TreePath // p ∈ t.validPaths }

@[instance_reducible]

instance RoseTree.Positions.instOrderBot {α : Type u_1} {t : RoseTree α} : OrderBot t.Positions

The root is the least position.

Equations

• RoseTree.Positions.instOrderBot = { bot := ⟨⊥, ⋯⟩, bot_le := ⋯ }

@[simp]

theorem RoseTree.Positions.bot_val {α : Type u_1} {t : RoseTree α} : ↑⊥ = ⊥

@[instance_reducible]

instance RoseTree.Positions.instSemilatticeInf {α : Type u_1} {t : RoseTree α} : SemilatticeInf t.Positions

The meet of two positions, their longest common prefix, is a position, since it dominates either.

Equations

• RoseTree.Positions.instSemilatticeInf = Subtype.semilatticeInf ⋯

@[simp]

theorem RoseTree.Positions.inf_val {α : Type u_1} {t : RoseTree α} (p q : t.Positions) : ↑(p ⊓ q) = ↑p ⊓ ↑q

@[instance_reducible]

instance RoseTree.Positions.instPredOrder {α : Type u_1} {t : RoseTree α} : PredOrder t.Positions

The parent of a position is a position.

Equations

• RoseTree.Positions.instPredOrder = { pred := fun (p : t.Positions) => ⟨(↑p).parent, ⋯⟩, pred_le := ⋯, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }

@[simp]

theorem RoseTree.Positions.pred_val {α : Type u_1} {t : RoseTree α} (p : t.Positions) : ↑(Order.pred p) = (↑p).parent

theorem RoseTree.Positions.covBy_iff {α : Type u_1} {t : RoseTree α} {p q : t.Positions} : p ⋖ q ↔ ↑p ⋖ ↑q

Covering in the positions of t is covering in TreePath, so the daughters of a position are its valid daughters.

def RoseTree.Positions.subtree {α : Type u_1} {t : RoseTree α} (p : t.Positions) : RoseTree α

The subtree of t at a position.

Equations

• p.subtree = (t.subtreeAt (↑p).toList).get ⋯

theorem RoseTree.Positions.subtreeAt_eq {α : Type u_1} {t : RoseTree α} (p : t.Positions) : t.subtreeAt (↑p).toList = some p.subtree

@[simp]

theorem RoseTree.Positions.subtree_bot {α : Type u_1} {t : RoseTree α} : ⊥.subtree = t

theorem RoseTree.Positions.subtree_eq_iff {α : Type u_1} {t : RoseTree α} {p : t.Positions} {s : RoseTree α} : p.subtree = s ↔ t.subtreeAt (↑p).toList = some s

theorem RoseTree.Positions.isSubtree_subtree {α : Type u_1} {t : RoseTree α} {p : t.Positions} {s : RoseTree α} : s.IsSubtree p.subtree ↔ ∃ (q : t.Positions), p ≤ q ∧ q.subtree = s

The subtrees of the subtree at a position are the subtrees at the positions below it.

theorem RoseTree.Positions.mem_children_subtree {α : Type u_1} {t : RoseTree α} {p : t.Positions} {c : RoseTree α} : c ∈ p.subtree.children ↔ ∃ (q : t.Positions), p ⋖ q ∧ q.subtree = c

The daughters of the subtree at a position are the subtrees at its covers.

Positions satisfying a predicate

def RoseTree.positionsWhere {α : Type u_1} (P : RoseTree α → Prop) (t : RoseTree α) : Set Core.Order.TreePath

The positions of t whose subtree satisfies P.

Equations

• RoseTree.positionsWhere P t = {p : Core.Order.TreePath | ∃ s ∈ t.subtreeAt p.toList, P s}

theorem RoseTree.mem_positionsWhere {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} : p ∈ positionsWhere P t ↔ ∃ s ∈ t.subtreeAt p.toList, P s

@[instance_reducible]

instance RoseTree.instDecidablePredTreePathMemSetPositionsWhere {α : Type u_1} {P : RoseTree α → Prop} [DecidablePred P] (t : RoseTree α) : DecidablePred fun (x : Core.Order.TreePath) => x ∈ positionsWhere P t

Equations

• t.instDecidablePredTreePathMemSetPositionsWhere x✝ = RoseTree.instDecidablePredTreePathMemSetPositionsWhere._aux_1 t x✝

theorem RoseTree.positionsWhere_subset_validPaths {α : Type u_1} (P : RoseTree α → Prop) (t : RoseTree α) : positionsWhere P t ⊆ t.validPaths

theorem RoseTree.positionsWhere_mono {α : Type u_1} {P Q : RoseTree α → Prop} (h : ∀ (s : RoseTree α), P s → Q s) (t : RoseTree α) : positionsWhere P t ⊆ positionsWhere Q t

theorem RoseTree.positionsWhere_or {α : Type u_1} (P Q : RoseTree α → Prop) (t : RoseTree α) : positionsWhere (fun (s : RoseTree α) => P s ∨ Q s) t = positionsWhere P t ∪ positionsWhere Q t

theorem RoseTree.positionsWhere_and {α : Type u_1} (P Q : RoseTree α → Prop) (t : RoseTree α) : positionsWhere (fun (s : RoseTree α) => P s ∧ Q s) t = positionsWhere P t ∩ positionsWhere Q t

theorem RoseTree.positionsWhere_map {α : Type u_1} {β : Type u_2} (f : α → β) (P : RoseTree β → Prop) (t : RoseTree α) : positionsWhere P (map f t) = positionsWhere (fun (s : RoseTree α) => P (map f s)) t

Relabelling moves the predicate onto the relabelled subtrees.

theorem RoseTree.mem_positionsWhere_replaceAt {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} (hP : ∀ (s : RoseTree α) (i : ℕ) (q : List ℕ) (new : RoseTree α), P (s.replaceAt (i :: q) new) ↔ P s) {c : Core.Order.TreePath} (h : ¬c ≤ p) (new : RoseTree α) : p ∈ positionsWhere P (t.replaceAt c.toList new) ↔ p ∈ positionsWhere P t

Outside the replaced subtree, a position satisfies a predicate that ignores what lies below the root exactly as before the replacement.

theorem RoseTree.minimal_mem_positionsWhere_iff {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} : Minimal (fun (x : Core.Order.TreePath) => x ∈ positionsWhere P t) p ↔ p ∈ positionsWhere P t ∧ ∀ q ∈ p.toList.inits, { toList := q } ≠ p → { toList := q } ∉ positionsWhere P t

@[instance_reducible]

instance RoseTree.instDecidableMinimalTreePathMemSetPositionsWhereOfDecidablePred {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} [DecidablePred P] : Decidable (Minimal (fun (x : Core.Order.TreePath) => x ∈ positionsWhere P t) p)

Equations

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

theorem RoseTree.maximal_mem_positionsWhere_iff {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} : Maximal (fun (x : Core.Order.TreePath) => x ∈ positionsWhere P t) p ↔ p ∈ positionsWhere P t ∧ ∀ q ∈ t.vertices, p < { toList := q } → { toList := q } ∉ positionsWhere P t

@[instance_reducible]

instance RoseTree.instDecidableMaximalTreePathMemSetPositionsWhereOfDecidablePred {α : Type u_1} {P : RoseTree α → Prop} {t : RoseTree α} {p : Core.Order.TreePath} [DecidablePred P] : Decidable (Maximal (fun (x : Core.Order.TreePath) => x ∈ positionsWhere P t) p)

Equations

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