Tree Positions: TreePath and the Rooted-Tree Order Stack

A TreePath is a position in a rose tree, encoded as a list of child indices (a Gorn address). Under the prefix order (dominance), TreePath instantiates mathlib's order-theoretic rooted-tree stack (Mathlib.Order.SuccPred.Tree):

instance	linguistic reading
OrderBot	the root position ⟨[]⟩
PredOrder	parent (mother-of): drop the last index
IsPredArchimedean	finite ancestor chains
SemilatticeInf	least common ancestor — the smallest
	constituent position containing both

TreePath itself is the full ℕ-branching tree of positions; a concrete tree's valid positions form a prefix-closed subset (see Core/Order/Branching.lean), which inherits the stack.

Moved here from Syntax/Tree/Basic.lean: positions are pure combinatorics, instantiable by any rose-tree carrier (CFG derivation trees via Gorn addresses, Hopf-algebra rooted trees, constituency trees) without importing linguistic theory.

Generic list API: longest common prefix

Upstream-shaped for Mathlib/Data/List/Prefix.lean (no commonPrefix exists in mathlib or Batteries as of 2026-06).

def List.commonPrefix {α : Type u_1} [DecidableEq α] : List α → List α → List α

Longest common prefix of two lists.

Equations

• (a :: as).commonPrefix (b :: bs) = if a = b then a :: as.commonPrefix bs else []
• x✝¹.commonPrefix x✝ = []

theorem List.commonPrefix_prefix_left {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.commonPrefix l₂ <+: l₁

theorem List.commonPrefix_prefix_right {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.commonPrefix l₂ <+: l₂

theorem List.prefix_commonPrefix {α : Type u_1} [DecidableEq α] {r l₁ l₂ : List α} : r <+: l₁ → r <+: l₂ → r <+: l₁.commonPrefix l₂

theorem List.commonPrefix_comm {α : Type u_1} [DecidableEq α] (l₁ l₂ : List α) : l₁.commonPrefix l₂ = l₂.commonPrefix l₁

theorem List.IsPrefix.getElem?_eq_of_lt {α : Type u_1} {l₁ l₂ : List α} (h : l₁ <+: l₂) {i : ℕ} (hi : i < l₁.length) : l₂[i]? = l₁[i]?

A prefix agrees with its extension below its length.

theorem List.append_singleton_prefix_of_getElem? {α : Type u_1} {cp l : List α} (h : cp <+: l) {i : α} (hi : l[cp.length]? = some i) : cp ++ [i] <+: l

A prefix extends by the element sitting at its length.

theorem List.getElem?_commonPrefix_ne {α : Type u_1} [DecidableEq α] {l₁ l₂ : List α} {i j : α} : l₁[(l₁.commonPrefix l₂).length]? = some i → l₂[(l₁.commonPrefix l₂).length]? = some j → i ≠ j

The lists genuinely diverge just past their common prefix.

structure Core.Order.TreePath : Type

A position (Gorn address) in a rose tree: a list of child indices. The empty path is the root.

• toList : List ℕ

  The underlying list of child indices.

def Core.Order.instDecidableEqTreePath.decEq (x✝ x✝¹ : TreePath) : Decidable (x✝ = x✝¹)

Equations

• Core.Order.instDecidableEqTreePath.decEq { toList := a } { toList := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Order.instDecidableEqTreePath : DecidableEq TreePath

Equations

• Core.Order.instDecidableEqTreePath = Core.Order.instDecidableEqTreePath.decEq

def Core.Order.instReprTreePath.repr : TreePath → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.Order.instReprTreePath : Repr TreePath

Equations

• Core.Order.instReprTreePath = { reprPrec := Core.Order.instReprTreePath.repr }

@[implicit_reducible]

instance Core.Order.TreePath.instLE : LE TreePath

Dominance order: p ≤ q iff p is a prefix of q (p dominates q).

Equations

• Core.Order.TreePath.instLE = { le := fun (p q : Core.Order.TreePath) => p.toList <+: q.toList }

theorem Core.Order.TreePath.le_def {p q : TreePath} : p ≤ q ↔ p.toList <+: q.toList

@[implicit_reducible]

instance Core.Order.TreePath.instPartialOrder : PartialOrder TreePath

Equations

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

theorem Core.Order.TreePath.prefix_or_prefix {p q r : TreePath} (hp : p ≤ r) (hq : q ≤ r) : p ≤ q ∨ q ≤ p

Two prefixes of the same list are comparable: the Connected Ancestor Condition (CAC) for the prefix order ([BP90]'s Definition 15). Delegates to List.prefix_or_prefix_of_prefix.

The root: OrderBot

@[implicit_reducible]

instance Core.Order.TreePath.instOrderBot : OrderBot TreePath

Equations

• Core.Order.TreePath.instOrderBot = { bot := { toList := [] }, bot_le := Core.Order.TreePath.instOrderBot._proof_1 }

@[simp]

theorem Core.Order.TreePath.bot_toList : ⊥.toList = []

theorem Core.Order.TreePath.length_strictMono {p q : TreePath} (h : p < q) : p.toList.length < q.toList.length

Parent: PredOrder

Order.pred is mother-of: drop the last child index. The root is its own predecessor (pred ⊥ = ⊥), matching mathlib's convention that pred of a minimal element is itself.

def Core.Order.TreePath.parent (p : TreePath) : TreePath

The parent position: drop the last index. Root's parent is itself.

Equations

• p.parent = { toList := p.toList.dropLast }

@[simp]

theorem Core.Order.TreePath.parent_toList (p : TreePath) : p.parent.toList = p.toList.dropLast

theorem Core.Order.TreePath.parent_le (p : TreePath) : p.parent ≤ p

theorem Core.Order.TreePath.parent_lt_of_ne_bot {p : TreePath} (hp : p ≠ ⊥) : p.parent < p

A non-root position is properly dominated by its parent — the Single Mother Condition reading: every node except the root has a mother that is a proper ancestor. (Order.pred ⊥ = ⊥ is mathlib's convention; linguistic axioms quantifying over mothers need this ≠ ⊥ guard.)

theorem Core.Order.TreePath.le_parent_of_lt {p q : TreePath} (h : p < q) : p ≤ q.parent

@[implicit_reducible]

instance Core.Order.TreePath.instPredOrder : PredOrder TreePath

Equations

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

@[simp]

theorem Core.Order.TreePath.pred_eq_parent (p : TreePath) : Order.pred p = p.parent

Finite depth: IsPredArchimedean

instance Core.Order.TreePath.instIsPredArchimedean : IsPredArchimedean TreePath

Least common ancestor: SemilatticeInf

p ⊓ q is the longest common prefix — the deepest position dominating both, i.e. the smallest constituent position containing both. (List.commonPrefix and its lemmas live in the _root_.List namespace at the top of this file; they are generic list API, upstream-shaped for Mathlib/Data/List/Prefix.lean.)

@[implicit_reducible]

instance Core.Order.TreePath.instSemilatticeInf : SemilatticeInf TreePath

Equations

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

@[reducible, inline]

abbrev Core.Order.TreePath.lca (p q : TreePath) : TreePath

Least common ancestor, by its linguistic name. lca p q is the deepest position dominating both p and q — the smallest constituent position containing both.

Equations

• p.lca q = p ⊓ q

Sisterhood

def Core.Order.TreePath.IsSister (p q : TreePath) : Prop

Sisters: distinct positions with the same parent.

Equations

• p.IsSister q = (p ≠ q ∧ p.parent = q.parent)

theorem Core.Order.TreePath.isSister_symm {p q : TreePath} (h : p.IsSister q) : q.IsSister p

Linear precedence

The PF-side order that dominance forgets: p precedes q iff their paths diverge at some common prefix with p taking an earlier branch. Defined only between dominance-incomparable positions (Precedes.not_le, Precedes.not_ge) — a node neither precedes nor follows its ancestors, the ID/LP division of labor.

def Core.Order.TreePath.Precedes (p q : TreePath) : Prop

p linearly precedes q: at some shared position r, p continues into an earlier child than q.

Equations

• p.Precedes q = ∃ (r : List ℕ) (i : ℕ) (j : ℕ), i < j ∧ r ++ [i] <+: p.toList ∧ r ++ [j] <+: q.toList

theorem Core.Order.TreePath.Precedes.irrefl (p : TreePath) : ¬p.Precedes p

theorem Core.Order.TreePath.Precedes.not_le {p q : TreePath} (h : p.Precedes q) : ¬p ≤ q

Precedence excludes dominance.

theorem Core.Order.TreePath.Precedes.not_ge {p q : TreePath} (h : p.Precedes q) : ¬q ≤ p

Precedence excludes being dominated.

theorem Core.Order.TreePath.Precedes.mono {p q p' q' : TreePath} (h : p.Precedes q) (hp : p ≤ p') (hq : q ≤ q') : p'.Precedes q'

Nontangling (downward inheritance; the third clause of Wall's tree definition, [BP90] Definition 1): precedence is inherited by descendants.

theorem Core.Order.TreePath.Precedes.precedes_iff {p q : TreePath} : p.Precedes q ↔ ∃ (i : ℕ) (j : ℕ), p.toList[(p.toList.commonPrefix q.toList).length]? = some i ∧ q.toList[(p.toList.commonPrefix q.toList).length]? = some j ∧ i < j

The divergence index of Precedes is exactly the common-prefix length: p precedes q iff at index (commonPrefix p q).length both paths continue and p's branch index is smaller. The computable characterization behind Decidable (Precedes p q).

@[implicit_reducible]

instance Core.Order.TreePath.Precedes.instDecidable (p q : TreePath) : Decidable (p.Precedes q)

Equations

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

theorem Core.Order.TreePath.Precedes.asymm {p q : TreePath} (h : p.Precedes q) : ¬q.Precedes p

Precedence is asymmetric.

theorem Core.Order.TreePath.Precedes.cons {p q : TreePath} (i : ℕ) (h : p.Precedes q) : { toList := i :: p.toList }.Precedes { toList := i :: q.toList }

Prepending a shared child index preserves precedence.

theorem Core.Order.TreePath.Precedes.of_index_lt {i j : ℕ} (hij : i < j) (p q : TreePath) : { toList := i :: p.toList }.Precedes { toList := j :: q.toList }

Positions under distinct child indices are precedence-ordered by those indices (divergence at the root).

theorem Core.Order.TreePath.Precedes.trichotomy (p q : TreePath) : p ≤ q ∨ q ≤ p ∨ p.Precedes q ∨ q.Precedes p

Totality over the dominance remainder: any two positions are dominance-comparable or precedence-ordered — the exhaustiveness that linear-precedence statements need.

The bundled mathlib rooted tree

TreePath carries all four classes of Mathlib.Order.SuccPred.Tree's RootedTree; the bundling makes the alignment true by construction and opens mathlib's findAtom/subtree API.

def Core.Order.TreePath.rootedTree : RootedTree

TreePath as a mathlib RootedTree.

Equations

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