Spans of subtrees in the frontier

The frontier of a subtree is a slice of the frontier of the tree. RoseTree.leafIndex t p is where the slice for the subtree at the address p begins, the number of leaves of t to its left, and the slice has as many entries as the subtree has leaves. These are the lemmas List.take_sum_flatten, List.drop_sum_flatten and List.drop_take_succ_flatten_eq_getElem of mathlib one level up: a list of lists is a tree of height two, and the index of its ith member in the flattened list is the sum of the lengths before it.

Dominance and precedence of positions become containment and order of spans. A position below another begins no earlier and ends no later, a position that precedes another ends before the other begins, and two positions are left-aligned (TreePath.LeftAligned) exactly when they begin at the same leaf.

Main definitions

• RoseTree.leafIndex: the number of leaves left of the subtree at an address.

Main results

• RoseTree.drop_take_leafList: the frontier of a subtree is the slice of the frontier that begins at its index.
• RoseTree.leafList_replaceAt: replacing a subtree replaces its slice.
• RoseTree.leafIndex_add_numLeaves_le_of_precedes: a subtree ends before one it precedes begins.
• RoseTree.leftAligned_iff_leafIndex_eq: left-aligned positions are those with one index.

The index of a subtree

def RoseTree.leafIndex {α : Type u_1} : RoseTree α → List ℕ → ℕ

t.leafIndex p is the number of leaves of t to the left of the subtree at the address p, the index in the frontier at which the frontier of that subtree begins.

Equations

• x✝.leafIndex [] = 0
• (RoseTree.node value cs).leafIndex (i :: p) = (List.map RoseTree.numLeaves (List.take i cs)).sum + cs[i]?.elim 0 fun (x : RoseTree α) => x.leafIndex p

@[simp]

theorem RoseTree.leafIndex_nil {α : Type u_1} (t : RoseTree α) : t.leafIndex [] = 0

theorem RoseTree.leafIndex_cons {α : Type u_1} (t : RoseTree α) (i : ℕ) (p : List ℕ) : t.leafIndex (i :: p) = (List.map numLeaves (List.take i t.children)).sum + t.children[i]?.elim 0 fun (x : RoseTree α) => x.leafIndex p

theorem RoseTree.leafIndex_cons_of_getElem? {α : Type u_1} {t c : RoseTree α} {i : ℕ} (hc : t.children[i]? = some c) (p : List ℕ) : t.leafIndex (i :: p) = (List.map numLeaves (List.take i t.children)).sum + c.leafIndex p

theorem RoseTree.leafIndex_append {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) (q : List ℕ) : t.leafIndex (p ++ q) = t.leafIndex p + s.leafIndex q

The index of a position below p is the index of p plus its index in the subtree at p.

The slice of a subtree

theorem RoseTree.leafIndex_add_numLeaves_le {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) : t.leafIndex p + s.numLeaves ≤ t.numLeaves

The frontier of a subtree ends inside the frontier of the tree.

theorem RoseTree.take_append_leafList_append_drop {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) : List.take (t.leafIndex p) t.leafList ++ s.leafList ++ List.drop (t.leafIndex p + s.numLeaves) t.leafList = t.leafList

The frontier of a tree is the leaves left of a subtree, the frontier of the subtree, and the leaves to its right.

theorem RoseTree.drop_take_leafList {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) : List.drop (t.leafIndex p) (List.take (t.leafIndex p + s.numLeaves) t.leafList) = s.leafList

The frontier of the subtree at p is the slice of the frontier of the tree that begins at t.leafIndex p.

theorem RoseTree.leafList_replaceAt {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) (new : RoseTree α) : (t.replaceAt p new).leafList = List.take (t.leafIndex p) t.leafList ++ new.leafList ++ List.drop (t.leafIndex p + s.numLeaves) t.leafList

Replacing the subtree at p replaces its slice of the frontier.

theorem RoseTree.getElem?_leafList_leafIndex {α : Type u_1} {t : RoseTree α} {p : List ℕ} {a : α} (h : t.subtreeAt p = some (leaf a)) : t.leafList[t.leafIndex p]? = some a

A leaf sits in the frontier at its index.

theorem RoseTree.IsSubtree.leafList_isInfix {α : Type u_1} {t s : RoseTree α} (h : s.IsSubtree t) : s.leafList <:+: t.leafList

The frontier of a subtree is an infix of the frontier of the tree.

@[simp]

theorem RoseTree.leafIndex_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) (p : List ℕ) : (map f t).leafIndex p = t.leafIndex p

Dominance and precedence

theorem RoseTree.leafIndex_le_leafIndex_append {α : Type u_1} {t s : RoseTree α} {p : List ℕ} (h : t.subtreeAt p = some s) (q : List ℕ) : t.leafIndex p ≤ t.leafIndex (p ++ q)

A position below p begins no earlier than p.

theorem RoseTree.leafIndex_append_add_numLeaves_le {α : Type u_1} {t s : RoseTree α} {p q : List ℕ} {u : RoseTree α} (h : t.subtreeAt p = some s) (hu : s.subtreeAt q = some u) : t.leafIndex (p ++ q) + u.numLeaves ≤ t.leafIndex p + s.numLeaves

A position below p ends no later than p.

theorem RoseTree.leafIndex_add_numLeaves_le_of_precedes {α : Type u_1} {t s : RoseTree α} {p q : Core.Order.TreePath} (hpq : p.Precedes q) (hp : t.subtreeAt p.toList = some s) (hq : (t.subtreeAt q.toList).isSome = true) : t.leafIndex p.toList + s.numLeaves ≤ t.leafIndex q.toList

The frontier of a subtree ends before the frontier of any subtree it precedes begins.

Left-alignment

theorem RoseTree.leafIndex_replicate_zero {α : Type u_1} (t : RoseTree α) (k : ℕ) : t.leafIndex (List.replicate k 0) = 0

theorem RoseTree.leafIndex_eq_zero_iff {α : Type u_1} {t : RoseTree α} {p : List ℕ} (h : (t.subtreeAt p).isSome = true) : t.leafIndex p = 0 ↔ ∀ i ∈ p, i = 0

A position begins where the tree does exactly when it is reached through first daughters.

theorem RoseTree.leftAligned_iff_leafIndex_eq {α : Type u_1} {t : RoseTree α} {p q : Core.Order.TreePath} (hp : (t.subtreeAt p.toList).isSome = true) (hq : (t.subtreeAt q.toList).isSome = true) : p.LeftAligned q ↔ t.leafIndex p.toList = t.leafIndex q.toList

Two positions of a tree are left-aligned exactly when their frontiers begin at the same leaf.