Path-based vertex addressing for Planar α

@cite{foissy-typed-decorated-rooted-trees-2018} @cite{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 RootedTree.Planar.Pathed to coexist with the old Vertex.lean (also RootedTree.Planar-scoped) during the migration. Once consumers move over, the Pathed sub-namespace will be hoisted up.

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 RootedTree.Planar.Pathed.Path : Type

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

Equations

• RootedTree.Planar.Pathed.Path = List ℕ

def RootedTree.Planar.Pathed.IsValidPath {α : Type u_1} : Path → Planar α → 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

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

@[simp]

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

@[simp]

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

def RootedTree.Planar.Pathed.decValidPath {α : Type u_1} (p : Path) (T : Planar α) : 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.
• RootedTree.Planar.Pathed.decValidPath [] x✝ = isTrue trivial

@[implicit_reducible]

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

Equations

• RootedTree.Planar.Pathed.instDecidableIsValidPath p T = RootedTree.Planar.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 RootedTree.Planar.Pathed.vertices {α : Type u_1} : Planar α → List Path

All valid paths into T in root-first order.

Equations

• RootedTree.Planar.Pathed.vertices (RootedTree.Planar.node a cs) = [] :: RootedTree.Planar.Pathed.verticesAux 0 cs

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem RootedTree.Planar.Pathed.verticesAux_append {α : Type u_1} (i : ℕ) (xs ys : List (Planar α)) : 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 weight (total vertex count). Mirrors length_vertices_eq_weight in the dependent-typed substrate.

theorem RootedTree.Planar.Pathed.length_vertices_eq_weight {α : Type u_1} (T : Planar α) : (vertices T).length = T.weight

theorem RootedTree.Planar.Pathed.length_verticesAux_eq_weightList {α : Type u_1} (i : ℕ) (cs : List (Planar α)) : (verticesAux i cs).length = weightList cs

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 RootedTree.Planar.Pathed.forall_isValidPath {α : Type u_1} (T : Planar α) {p : Path} : p ∈ vertices T → IsValidPath p T

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