Rose tree indexing by Gorn address

Navigation into an n-ary RoseTree by a Gorn address: a List ℕ path of child indices. subtreeAt returns the subtree reached by descending along the path, get? its root value, getD with a fallback.

Unlike BinaryTree.get (indexed by a PosNum left/right path) there is no indexOf: that is a binary-search-tree lookup, which has no analogue for a general (unordered-search) rose tree. The Gorn path replaces the PosNum path, so this file needs no Num dependency.

def RoseTree.subtreeAt {α : Type u_1} (t : RoseTree α) : List ℕ → Option (RoseTree α)

The subtree at a Gorn address (a path of child indices); none if the path steps outside the tree.

Equations

• t.subtreeAt [] = some t
• t.subtreeAt (i :: rest) = t.children[i]?.bind fun (c : RoseTree α) => c.subtreeAt rest

@[simp]

theorem RoseTree.subtreeAt_nil {α : Type u_1} (t : RoseTree α) : t.subtreeAt [] = some t

@[simp]

theorem RoseTree.subtreeAt_cons {α : Type u_1} (t : RoseTree α) (i : ℕ) (rest : List ℕ) : t.subtreeAt (i :: rest) = t.children[i]?.bind fun (c : RoseTree α) => c.subtreeAt rest

theorem RoseTree.subtreeAt_append {α : Type u_1} (t : RoseTree α) (p q : List ℕ) : t.subtreeAt (p ++ q) = (t.subtreeAt p).bind fun (x : RoseTree α) => x.subtreeAt q

Gorn composition: descending along p ++ q is descending along p, then along q from the result.

def RoseTree.get? {α : Type u_1} (t : RoseTree α) (path : List ℕ) : Option α

The root value at a Gorn address; none if the path steps outside the tree.

Equations

• t.get? path = Option.map RoseTree.value (t.subtreeAt path)

def RoseTree.getD {α : Type u_1} (t : RoseTree α) (path : List ℕ) (v : α) : α

The root value at a Gorn address, or v if the path is invalid.

Equations

• t.getD path v = (t.get? path).getD v

@[simp]

theorem RoseTree.get?_nil {α : Type u_1} (t : RoseTree α) : t.get? [] = some t.value

@[simp]

theorem RoseTree.getD_nil {α : Type u_1} (t : RoseTree α) (v : α) : t.getD [] v = t.value