Tree positions

A TreePath is a position in a rose tree, written as its Gorn address: the list of child indices on the way down from the root. Under the prefix order, with p ≤ q when p dominates q, the positions form the rooted tree in which every node has a child for each natural number. It carries the order structure of Mathlib/Order/SuccPred/Tree.lean: the root ⊥ is the empty address, Order.pred drops the last index, p ⊓ q is the longest common prefix, and strict dominance is well founded, so ancestor chains are finite. The positions of a concrete tree form a prefix-closed subset (RoseTree.validPaths).

p precedes q when the two part at some position with p taking the earlier child. Precedence is lexicographic order between positions neither of which dominates the other. It is a decidable strict order, it passes to dominated positions, and any two positions are related by dominance or by precedence.

Two positions are left-aligned when their addresses differ only in trailing first-daughter steps, so that the subtrees at them begin with the same leaf. Left-alignment is a decidable equivalence relation, and left-aligned positions lie on one branch.

Main definitions

• Core.Order.TreePath: Gorn addresses under the prefix order.
• Core.Order.TreePath.Precedes: linear precedence of positions.
• Core.Order.TreePath.LeftAligned: positions sharing a left edge.

Main results

• TreePath.covBy_iff: q covers p exactly when q extends p by one index.
• TreePath.precedes_iff_lt_and_not_le: precedence is lexicographic order minus dominance.
• TreePath.Precedes.trichotomy: two positions are related by dominance or by precedence.
• TreePath.leftAligned_iff_exists: positions are left-aligned exactly when descending through first daughters from each reaches a common position.

structure Core.Order.TreePath : Type

A position in a rose tree is given by its Gorn address, the child indices on the path from the root. The empty address is the root.

• toList : List ℕ

  The child indices, from the root down.

theorem Core.Order.TreePath.ext {x y : TreePath} (toList : x.toList = y.toList) : x = y

theorem Core.Order.TreePath.ext_iff {x y : TreePath} : x = y ↔ x.toList = y.toList

@[instance_reducible]

instance Core.Order.instDecidableEqTreePath : DecidableEq TreePath

Equations

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

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 ⋯

@[instance_reducible]

instance Core.Order.instReprTreePath : Repr TreePath

Equations

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

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

Equations

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

@[instance_reducible]

instance Core.Order.TreePath.instLE : LE TreePath

A position dominates another when its address is a prefix of the other's.

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

@[simp]

theorem Core.Order.TreePath.mk_le_mk {l m : List ℕ} : { toList := l } ≤ { toList := m } ↔ l <+: m

@[instance_reducible]

instance Core.Order.TreePath.instDecidableLE : DecidableLE TreePath

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff (x✝¹.toList <+: x✝.toList) ⋯

@[instance_reducible]

instance Core.Order.TreePath.instPartialOrder : PartialOrder TreePath

Equations

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

@[instance_reducible]

instance Core.Order.TreePath.instDecidableLT : DecidableLT TreePath

Equations

• x✝¹.instDecidableLT x✝ = decidable_of_iff (x✝¹ ≤ x✝ ∧ ¬x✝ ≤ x✝¹) ⋯

@[instance_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 : StrictMono fun (p : TreePath) => p.toList.length

instance Core.Order.TreePath.instWellFoundedLT : WellFoundedLT TreePath

Parents

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

The parent of a position drops its last index. The root is its own parent.

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.le_parent_of_lt {p q : TreePath} (h : p < q) : p ≤ q.parent

@[instance_reducible]

instance Core.Order.TreePath.instPredOrder : PredOrder TreePath

Equations

• Core.Order.TreePath.instPredOrder = { pred := Core.Order.TreePath.parent, pred_le := Core.Order.TreePath.parent_le, min_of_le_pred := ⋯, le_pred_of_lt := ⋯ }

@[simp]

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

theorem Core.Order.TreePath.covBy_iff {p q : TreePath} : p ⋖ q ↔ ∃ (i : ℕ), q.toList = p.toList ++ [i]

A position is covered exactly by its daughters, the extensions by one index.

Least common ancestors

@[instance_reducible]

instance Core.Order.TreePath.instSemilatticeInf : SemilatticeInf TreePath

The meet of two positions is their longest common prefix, the deepest position dominating both.

Equations

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

Linear precedence

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

p precedes q when, at some common position, 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.lt {p q : TreePath} (h : p.Precedes q) : p.toList < q.toList

A position comes lexicographically before every position it precedes.

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

A position precedes no position it dominates.

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

A position precedes no position that dominates it.

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

Precedence passes to the positions each relatum dominates.

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

Prefixing a common index preserves precedence.

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

Positions under distinct daughters of the root are ordered as the daughters are.

theorem Core.Order.TreePath.precedes_iff_lt_and_not_le {p q : TreePath} : p.Precedes q ↔ p.toList < q.toList ∧ ¬p ≤ q

p precedes q exactly when p comes lexicographically before q without dominating it.

@[instance_reducible]

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

Equations

• p.instDecidablePrecedes q = decidable_of_iff (p.toList < q.toList ∧ ¬p ≤ q) ⋯

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

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

theorem Core.Order.TreePath.Precedes.trans {p q r : TreePath} (h₁ : p.Precedes q) (h₂ : q.Precedes r) : p.Precedes r

instance Core.Order.TreePath.Precedes.instIsStrictOrder : IsStrictOrder TreePath Precedes

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

Any two positions are related by dominance or by precedence.

Left edges

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

Two positions are left-aligned when their addresses agree once trailing first-daughter steps are dropped, so that the subtrees at them begin with the same leaf.

Equations

• p.LeftAligned q = (List.dropWhile (fun (x : ℕ) => x == 0) p.toList.reverse = List.dropWhile (fun (x : ℕ) => x == 0) q.toList.reverse)

@[instance_reducible]

instance Core.Order.TreePath.instDecidableRelLeftAligned : DecidableRel LeftAligned

Equations

• x✝¹.instDecidableRelLeftAligned x✝ = Core.Order.TreePath.instDecidableRelLeftAligned._aux_1 x✝¹ x✝

theorem Core.Order.TreePath.LeftAligned.refl (p : TreePath) : p.LeftAligned p

theorem Core.Order.TreePath.LeftAligned.symm {p q : TreePath} (h : p.LeftAligned q) : q.LeftAligned p

theorem Core.Order.TreePath.LeftAligned.trans {p q r : TreePath} (h₁ : p.LeftAligned q) (h₂ : q.LeftAligned r) : p.LeftAligned r

theorem Core.Order.TreePath.leftAligned_iff_exists {p q : TreePath} : p.LeftAligned q ↔ ∃ (j : ℕ) (k : ℕ), p.toList ++ List.replicate j 0 = q.toList ++ List.replicate k 0

Positions are left-aligned exactly when descending through first daughters from each reaches a common position.

theorem Core.Order.TreePath.LeftAligned.le_or_ge {p q : TreePath} (h : p.LeftAligned q) : p ≤ q ∨ q ≤ p

Left-aligned positions lie on one branch.