Rose trees

A rose tree over α is a root carrying a value in α with an ordered list of child subtrees, the n-ary counterpart of mathlib's BinaryTree. A leaf is node a []. The children are a List, which keeps the type computable. The unordered rooted tree, whose children form a multiset, is the quotient of this type by RoseTree.Perm (UnorderedTree).

The type is nested through List, so its recursor takes one motive for trees and one for lists. RoseTree.rec' is the induction principle with the single hypothesis ∀ c ∈ cs, motive c, and RoseTree.fold is the catamorphism from which map, the counts and the frontier are defined.

Main definitions

• RoseTree, RoseTree.value, RoseTree.children, RoseTree.leaf: the type, its projections and its leaves.
• RoseTree.rec', RoseTree.fold: induction and the catamorphism.
• RoseTree.map: relabelling.
• RoseTree.numNodes, RoseTree.numLeaves, RoseTree.height, RoseTree.arity: the counts.
• RoseTree.values, RoseTree.localTrees, RoseTree.leafList: the node values in preorder, each node's value with the values of its children, and the frontier.

inductive RoseTree (α : Type u_1) : Type u_1

A rose tree has a root value : α and an ordered list of child subtrees. A leaf is node a [].

• node {α : Type u_1} (value : α) (children : List (RoseTree α)) : RoseTree α

partial def instReprRoseTree.repr {α✝ : Type u_1} [Repr α✝] : RoseTree α✝ → ℕ → Std.Format

@[instance_reducible]

instance instReprRoseTree {α✝ : Type u_1} [Repr α✝] : Repr (RoseTree α✝)

Equations

• instReprRoseTree = { reprPrec := instReprRoseTree.repr }

Projections

def RoseTree.value {α : Type u_1} : RoseTree α → α

The value at the root.

Equations

• (RoseTree.node a children).value = a

def RoseTree.children {α : Type u_1} : RoseTree α → List (RoseTree α)

The ordered list of child subtrees at the root.

Equations

• (RoseTree.node a children).children = children

@[simp]

theorem RoseTree.value_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).value = a

@[simp]

theorem RoseTree.children_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).children = cs

@[reducible, inline]

abbrev RoseTree.leaf {α : Type u_1} (a : α) : RoseTree α

A leaf is a root with no children.

Equations

• RoseTree.leaf a = RoseTree.node a []

Decidable equality

deriving DecidableEq does not fire through the nested List occurrence (as of Lean v4.35.0), so the instance is built by mutual recursion on the tree and its child list.

def RoseTree.decEq {α : Type u_1} [DecidableEq α] (t s : RoseTree α) : Decidable (t = s)

Decidable equality on trees (mutual with the child-list case).

Equations

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

def RoseTree.decEqList {α : Type u_1} [DecidableEq α] (ts ss : List (RoseTree α)) : Decidable (ts = ss)

Decidable equality on child lists (mutual with the tree case).

Equations

• One or more equations did not get rendered due to their size.
• RoseTree.decEqList [] [] = isTrue ⋯
• RoseTree.decEqList [] (head :: tail) = isFalse ⋯
• RoseTree.decEqList (head :: tail) [] = isFalse ⋯

@[instance_reducible]

instance RoseTree.instDecidableEq {α : Type u_1} [DecidableEq α] : DecidableEq (RoseTree α)

Equations

• RoseTree.instDecidableEq = RoseTree.decEq

Size

theorem RoseTree.sizeOf_lt_of_mem {α : Type u_1} [SizeOf α] {a : α} {cs : List (RoseTree α)} {c : RoseTree α} (hc : c ∈ cs) : sizeOf c < sizeOf (node a cs)

A child of a node is strictly smaller than the node in the generated SizeOf, the measure behind rec' and the well-founded recursions over RoseTree.

The recursion principle

@[irreducible]

def RoseTree.rec' {α : Type u_1} {motive : RoseTree α → Sort u_4} (node : (a : α) → (cs : List (RoseTree α)) → ((c : RoseTree α) → c ∈ cs → motive c) → motive (node a cs)) (t : RoseTree α) : motive t

Induction on a rose tree proves motive t for all t from motive (node a cs) given motive c for every child c ∈ cs.

Equations

• RoseTree.rec' node (RoseTree.node a children) = node a children fun (c : RoseTree α) (_hc : c ∈ children) => RoseTree.rec' node c

Catamorphism

The structural operations (map, numNodes, height, …) are folds, and their equations at a node come from fold_node.

def RoseTree.fold {α : Type u_1} {β : Type u_2} (f : α → List β → β) : RoseTree α → β

The catamorphism replaces each node a cs by f a (folded children).

Equations

• RoseTree.fold f (RoseTree.node a children) = f a (RoseTree.foldList f children)

def RoseTree.foldList {α : Type u_1} {β : Type u_2} (f : α → List β → β) : List (RoseTree α) → List β

foldList folds across a list of children.

Equations

• RoseTree.foldList f [] = []
• RoseTree.foldList f (c :: cs) = RoseTree.fold f c :: RoseTree.foldList f cs

theorem RoseTree.foldList_eq {α : Type u_1} {β : Type u_2} (f : α → List β → β) (cs : List (RoseTree α)) : foldList f cs = List.map (fold f) cs

@[simp]

theorem RoseTree.fold_node {α : Type u_1} {β : Type u_2} (f : α → List β → β) (a : α) (cs : List (RoseTree α)) : fold f (node a cs) = f a (List.map (fold f) cs)

theorem RoseTree.fold_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} (h : β → γ) {f : α → List β → β} {g : α → List γ → γ} (hfg : ∀ (a : α) (ps : List β), h (f a ps) = g a (List.map h ps)) (t : RoseTree α) : h (fold f t) = fold g t

Postcomposing a fold with h gives the fold of the pushed-forward algebra, the RoseTree sibling of List.foldr_hom.

Functoriality

def RoseTree.map {α : Type u_1} {β : Type u_2} (f : α → β) : RoseTree α → RoseTree β

Relabel every node by f, preserving shape.

Equations

• RoseTree.map f = RoseTree.fold fun (a : α) (cs : List (RoseTree β)) => RoseTree.node (f a) cs

@[simp]

theorem RoseTree.map_node {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) (cs : List (RoseTree α)) : map f (node a cs) = node (f a) (List.map (map f) cs)

theorem RoseTree.id_map {α : Type u_1} (t : RoseTree α) : map id t = t

theorem RoseTree.comp_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ) (t : RoseTree α) : map (g ∘ f) t = map g (map f t)

Counting

def RoseTree.numNodes {α : Type u_1} : RoseTree α → ℕ

The number of nodes. A leaf counts as 1.

Equations

• RoseTree.numNodes = RoseTree.fold fun (x : α) (ns : List ℕ) => ns.sum + 1

@[simp]

theorem RoseTree.numNodes_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).numNodes = (List.map numNodes cs).sum + 1

theorem RoseTree.numNodes_pos {α : Type u_1} (t : RoseTree α) : 0 < t.numNodes

def RoseTree.values {α : Type u_1} : RoseTree α → List α

The node values in preorder list the root first, then each child's values left to right.

Equations

• RoseTree.values = RoseTree.fold fun (a : α) (ls : List (List α)) => a :: ls.flatten

@[simp]

theorem RoseTree.values_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).values = a :: (List.map values cs).flatten

theorem RoseTree.length_values {α : Type u_1} (t : RoseTree α) : t.values.length = t.numNodes

def RoseTree.localTrees {α : Type u_1} : RoseTree α → List (α × List α)

The local trees of a tree pair each node's value with the values of its children, one entry per node in preorder.

Equations

• (RoseTree.node a children).localTrees = (a, List.map RoseTree.value children) :: RoseTree.localTreesList children

def RoseTree.localTreesList {α : Type u_1} : List (RoseTree α) → List (α × List α)

localTreesList concatenates the local trees of a list of trees.

Equations

• RoseTree.localTreesList [] = []
• RoseTree.localTreesList (c :: cs) = c.localTrees ++ RoseTree.localTreesList cs

theorem RoseTree.localTreesList_eq {α : Type u_1} (cs : List (RoseTree α)) : localTreesList cs = (List.map localTrees cs).flatten

@[simp]

theorem RoseTree.localTrees_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).localTrees = (a, List.map value cs) :: (List.map localTrees cs).flatten

theorem RoseTree.length_localTrees {α : Type u_1} (t : RoseTree α) : t.localTrees.length = t.numNodes

def RoseTree.leafList {α : Type u_1} : RoseTree α → List α

The ordered frontier lists the leaf values from left to right.

Equations

• RoseTree.leafList = RoseTree.fold fun (a : α) (ls : List (List α)) => match ls with | [] => [a] | ls => ls.flatten

@[simp]

theorem RoseTree.leafList_leaf {α : Type u_1} (a : α) : (node a []).leafList = [a]

theorem RoseTree.leafList_node_of_ne_nil {α : Type u_1} (a : α) {cs : List (RoseTree α)} (h : cs ≠ []) : (node a cs).leafList = (List.map leafList cs).flatten

@[simp]

theorem RoseTree.leafList_node_cons {α : Type u_1} (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : (node a (c :: cs)).leafList = (List.map leafList (c :: cs)).flatten

theorem RoseTree.leafList_ne_nil {α : Type u_1} (t : RoseTree α) : t.leafList ≠ []

def RoseTree.numLeaves {α : Type u_1} : RoseTree α → ℕ

The number of leaves. A single leaf counts as 1.

Equations

• RoseTree.numLeaves = RoseTree.fold fun (x : α) (ns : List ℕ) => max 1 ns.sum

@[simp]

theorem RoseTree.numLeaves_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).numLeaves = max 1 (List.map numLeaves cs).sum

@[simp]

theorem RoseTree.numLeaves_leaf {α : Type u_1} (a : α) : (leaf a).numLeaves = 1

theorem RoseTree.numLeaves_pos {α : Type u_1} (t : RoseTree α) : 0 < t.numLeaves

theorem RoseTree.numLeaves_node_of_ne_nil {α : Type u_1} (a : α) {cs : List (RoseTree α)} (h : cs ≠ []) : (node a cs).numLeaves = (List.map numLeaves cs).sum

theorem RoseTree.length_leafList {α : Type u_1} (t : RoseTree α) : t.leafList.length = t.numLeaves

The frontier has one entry for each leaf.

Height

def RoseTree.height {α : Type u_1} : RoseTree α → ℕ

The height is the number of nodes on a longest path from the root to a leaf, so a leaf has height 1. This is the convention of BinaryTree.height, where nil has height 0.

Equations

• RoseTree.height = RoseTree.fold fun (x : α) (hs : List ℕ) => List.foldr max 0 hs + 1

@[simp]

theorem RoseTree.height_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).height = List.foldr max 0 (List.map height cs) + 1

theorem RoseTree.height_pos {α : Type u_1} (t : RoseTree α) : 0 < t.height

theorem RoseTree.height_lt_of_mem {α : Type u_1} {t c : RoseTree α} (h : c ∈ t.children) : c.height < t.height

Arity

def RoseTree.arity {α : Type u_1} (t : RoseTree α) : ℕ

The arity of the root is its number of children. A leaf has arity 0.

Equations

• t.arity = t.children.length

@[simp]

theorem RoseTree.arity_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).arity = cs.length

@[simp]

theorem RoseTree.arity_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).arity = t.arity

map preserves the counts

@[simp]

theorem RoseTree.map_leaf {α : Type u_1} {β : Type u_2} (f : α → β) (a : α) : map f (leaf a) = leaf (f a)

@[simp]

theorem RoseTree.numNodes_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).numNodes = t.numNodes

@[simp]

theorem RoseTree.numLeaves_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).numLeaves = t.numLeaves

@[simp]

theorem RoseTree.height_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).height = t.height

@[simp]

theorem RoseTree.localTrees_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).localTrees = List.map (fun (p : α × List α) => (f p.1, List.map f p.2)) t.localTrees

@[simp]

theorem RoseTree.leafList_map {α : Type u_1} {β : Type u_2} (f : α → β) (t : RoseTree α) : (map f t).leafList = List.map f t.leafList

Instances

@[instance_reducible]

instance RoseTree.instInhabited {α : Type u_1} [Inhabited α] : Inhabited (RoseTree α)

Equations

• RoseTree.instInhabited = { default := RoseTree.leaf default }