Path-based vertex addressing for RoseTree α

[foissy-typed-decorated-rooted-trees-2018] [chapoton-livernet-2001]

Path-based replacement for the indexed-inductive Vertex T / VertexList cs machinery in Vertex.lean. A vertex is addressed by a Path = List ℕ of child indices from the root. The non-dependent representation lets List.map_append, List.Perm, and related mathlib API fire directly on vertices outputs without the have h := List.map_append; rw [h] workarounds that the dependent-typed version forced.

Lives under namespace RoseTree.Pathed; the Pathed sub-namespace keeps the path-addressing API from colliding with the core RoseTree surface and will be hoisted up once the old dependent Vertex machinery is retired.

File scope

• §1: Path, IsValidPath, Decidable instance.
• §2: vertices enumeration + length theorem + validity sanity check.

Path-based code uses Path and IsValidPath directly. A subtype wrapper { p : Path // IsValidPath p T } can be inlined at use sites that need it; no global Vertex def is needed.

Status

[UPSTREAM] candidate. Sorry-free, no noncomputable.

§1: Path and validity

@[reducible, inline]

abbrev RoseTree.Pathed.Path : Type

A path from the root: list of child indices. [] addresses the root.

Equations

• RoseTree.Pathed.Path = List ℕ

def RoseTree.Pathed.IsValidPath {α : Type u_1} : Path → RoseTree α → Prop

IsValidPath p T means p addresses an existing vertex in T. Recurses on the path: empty path is always valid; i :: rest requires i to be in bounds and rest to be valid in the i-th child.

Equations

• RoseTree.Pathed.IsValidPath [] x✝ = True
• RoseTree.Pathed.IsValidPath (i :: rest) (RoseTree.node value cs) = ∃ (h : i < cs.length), RoseTree.Pathed.IsValidPath rest cs[i]

@[simp]

theorem RoseTree.Pathed.isValidPath_nil {α : Type u_1} (T : RoseTree α) : IsValidPath [] T

@[simp]

theorem RoseTree.Pathed.isValidPath_cons {α : Type u_1} (i : ℕ) (rest : Path) (a : α) (cs : List (RoseTree α)) : IsValidPath (i :: rest) (node a cs) ↔ ∃ (h : i < cs.length), IsValidPath rest cs[i]

def RoseTree.Pathed.decValidPath {α : Type u_1} (p : Path) (T : RoseTree α) : Decidable (IsValidPath p T)

Decidability of IsValidPath, by recursion on the path.

Equations

• One or more equations did not get rendered due to their size.
• RoseTree.Pathed.decValidPath [] x✝ = isTrue trivial

@[implicit_reducible]

instance RoseTree.Pathed.instDecidableIsValidPath {α : Type u_1} (p : Path) (T : RoseTree α) : Decidable (IsValidPath p T)

Equations

• RoseTree.Pathed.instDecidableIsValidPath p T = RoseTree.Pathed.decValidPath p T

§2: Vertex enumeration

vertices T : List Path lists the valid paths into T in DFS root-first order: the empty path, then for each child cs[i] the i-prepended recursion. Mutual with an aux running over the children list paired with an offset index.

The mutual style is the same shape as vertices / verticesList in the old Vertex.lean — exchange of the dependent inductive for a path list.

def RoseTree.Pathed.vertices {α : Type u_1} : RoseTree α → List Path

All valid paths into T in root-first order.

Equations

• RoseTree.Pathed.vertices (RoseTree.node value cs) = [] :: RoseTree.Pathed.verticesAux 0 cs

def RoseTree.Pathed.verticesAux {α : Type u_1} : ℕ → List (RoseTree α) → List Path

Auxiliary: paths into a children list, with a starting index. The paths returned are already prefixed with the corresponding child index.

Equations

• RoseTree.Pathed.verticesAux x✝ [] = []
• RoseTree.Pathed.verticesAux x✝ (c :: cs) = List.map (fun (x : List ℕ) => x✝ :: x) (RoseTree.Pathed.vertices c) ++ RoseTree.Pathed.verticesAux (x✝ + 1) cs

@[simp]

theorem RoseTree.Pathed.vertices_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : vertices (node a cs) = [] :: verticesAux 0 cs

@[simp]

theorem RoseTree.Pathed.verticesAux_nil {α : Type u_1} (i : ℕ) : verticesAux i [] = []

@[simp]

theorem RoseTree.Pathed.verticesAux_cons {α : Type u_1} (i : ℕ) (c : RoseTree α) (cs : List (RoseTree α)) : verticesAux i (c :: cs) = List.map (fun (x : List ℕ) => i :: x) (vertices c) ++ verticesAux (i + 1) cs

theorem RoseTree.Pathed.verticesAux_append {α : Type u_1} (i : ℕ) (xs ys : List (RoseTree α)) : verticesAux i (xs ++ ys) = verticesAux i xs ++ verticesAux (i + xs.length) ys

verticesAux distributes over list ++. The right summand's start index shifts by the left list's length.

Length theorem

The total number of enumerated paths equals the tree's node count (numNodes). Mirrors the dependent-typed substrate's length_vertices result, now stated directly against numNodes — no weightList aux-twin is needed, the child sum is (cs.map numNodes).sum.

theorem RoseTree.Pathed.length_vertices_eq_numNodes {α : Type u_1} (T : RoseTree α) : (vertices T).length = T.numNodes

theorem RoseTree.Pathed.length_verticesAux {α : Type u_1} (i : ℕ) (cs : List (RoseTree α)) : (verticesAux i cs).length = (List.map numNodes cs).sum

Validity sanity check

Every path enumerated by vertices T is in fact valid in T. Proved via a mutual recursion through an aux that decomposes paths in verticesAux i₀ cs as (i₀ + k) :: rest with rest ∈ vertices cs[k].

theorem RoseTree.Pathed.forall_isValidPath {α : Type u_1} (T : RoseTree α) {p : Path} : p ∈ vertices T → IsValidPath p T

theorem RoseTree.Pathed.forall_isValidPath_aux {α : Type u_1} (cs : List (RoseTree α)) (i₀ : ℕ) {p : Path} : p ∈ verticesAux i₀ cs → ∃ (k : ℕ), ∃ (rest : Path), p = (i₀ + k) :: rest ∧ ∃ (h : k < cs.length), IsValidPath rest cs[k]