N-ary rooted trees (rose trees)

An n-ary rooted tree (rose tree) over α: a distinguished root carrying a value in α, and an ordered list of child subtrees. A leaf is node a []. This is the n-ary generalization of BinaryTree (Mathlib.Data.Tree.Basic), matching Haskell's Data.RoseTree (Node a [RoseTree a]).

The children are an ordered List, not a Multiset or a WType branching family: List-valued children are positivity-clean, keep the type computable, and give the ergonomic map/traversal API that the unordered (Multiset) and WType encodings do not. The unordered rooted tree — the carrier of the free pre-Lie algebra and the Connes–Kreimer Hopf algebra — is a quotient of this type by child permutation, built downstream; it does not belong at this data-structure layer.

The recursion principle

The type is nested through List, so the auto-generated recursor hands a per-List motive rather than a ∀ c ∈ children, motive c hypothesis. The RoseTree.rec' eliminator (registered @[induction_eliminator]) packages the (tree, list-of-trees) shape once, so downstream map/depth/numNodes recurse and prove with a single List-shaped induction hypothesis instead of a hand-written mutual block per operation.

Upstreaming

Intended shape for the reserved Mathlib.Data.Tree n-ary Tree slot (freed by mathlib's Tree → BinaryTree rename). Self-contained: no linguistics, no order/command imports. Dependency-light, sorry-free, no noncomputable.

inductive RoseTree (α : Type u_1) : Type u_1

An n-ary rooted tree (rose tree): 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

@[implicit_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 a_1).value = a

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

The ordered list of child subtrees at the root.

Equations

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

@[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

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

A leaf: a root with no children.

Equations

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

@[simp]

theorem RoseTree.children_leaf {α : Type u_1} (a : α) : (leaf a).children = []

Decidable equality

deriving DecidableEq does not fire through the nested List occurrence (still true as of Lean v4.32.0-rc1), 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

• (RoseTree.node a cs).decEq (RoseTree.node b ds) = if hab : a = b then match RoseTree.decEqList cs ds with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯ else isFalse ⋯

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 ⋯

@[implicit_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} {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 auto-generated SizeOf. This is the measure behind rec' and downstream 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

Structural induction for RoseTree: to prove motive t for all t, prove it for node a cs given motive c for every child c ∈ cs. Packages the nested-List recursion so downstream defs/proofs use a single List-shaped hypothesis.

Equations

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

Catamorphism

fold f is the workhorse: every structural operation (map, numNodes, height, …) is a one-line fold specialization, and their reduction lemmas fall out of fold_node.

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

Catamorphism: replace each node a cs by f a (folded children).

Equations

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

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

Auxiliary: fold 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)

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)

Traversal

Effectful traversal: act on the root, then the children left-to-right — the Traversable action for RoseTree.

def RoseTree.traverse {m : Type u → Type u} [Applicative m] {α β : Type u} (f : α → m β) : RoseTree α → m (RoseTree β)

Traverse a tree with an applicative action, root then children in order.

Equations

• RoseTree.traverse f (RoseTree.node a a_1) = RoseTree.node <$> f a <*> RoseTree.traverseList f a_1

def RoseTree.traverseList {m : Type u → Type u} [Applicative m] {α β : Type u} (f : α → m β) : List (RoseTree α) → m (List (RoseTree β))

Auxiliary: traverse a list of child subtrees.

Equations

• RoseTree.traverseList f [] = pure []
• RoseTree.traverseList f (c :: cs) = (fun (x1 : RoseTree β) (x2 : List (RoseTree β)) => x1 :: x2) <$> RoseTree.traverse f c <*> RoseTree.traverseList f cs

@[simp]

theorem RoseTree.traverse_node {m : Type u → Type u} [Applicative m] {α β : Type u} (f : α → m β) (a : α) (cs : List (RoseTree α)) : traverse f (node a cs) = node <$> f a <*> traverseList f cs

theorem RoseTree.traverse_pure {m : Type u → Type u} [Applicative m] [LawfulApplicative m] {α : Type u} (t : RoseTree α) : traverse pure t = pure t

Counting

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

The total number of nodes (vertices). A leaf counts as 1.

Equations

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

@[simp]

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

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

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

The number of leaves (childless nodes). A single leaf counts as 1.

Equations

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

@[simp]

theorem RoseTree.numLeaves_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) : (node a cs).numLeaves = 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

def RoseTree.spansOf {α : Type u_1} (p : α → Bool) (t : RoseTree α) : List (ℕ × ℕ)

The (offset, size) leaf-spans of the nodes satisfying p, in left-to-right traversal order: the offset counts leaves strictly to the node's left, the size its own leaves.

Equations

• RoseTree.spansOf p t = RoseTree.spansOf.go p 0 t

def RoseTree.spansOf.go {α : Type u_1} (p : α → Bool) (off : ℕ) : RoseTree α → List (ℕ × ℕ)

Equations

• RoseTree.spansOf.go p off (RoseTree.node a a_1) = (if p a = true then [(off, (RoseTree.node a a_1).numLeaves)] else []) ++ RoseTree.spansOf.goList p off a_1

def RoseTree.spansOf.goList {α : Type u_1} (p : α → Bool) (off : ℕ) : List (RoseTree α) → List (ℕ × ℕ)

Equations

• RoseTree.spansOf.goList p off [] = []
• RoseTree.spansOf.goList p off (c :: cs) = RoseTree.spansOf.go p off c ++ RoseTree.spansOf.goList p (off + c.numLeaves) cs

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

The height (length of the longest root-to-leaf path in edges): a leaf has height 0, an internal node is one more than the maximum child height.

Equations

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

@[simp]

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

Arity and the leaf test

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

The arity of the root: 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

def RoseTree.isLeaf {α : Type u_1} (t : RoseTree α) : Bool

Whether the root is a leaf (has no children).

Equations

• t.isLeaf = t.children.isEmpty

@[simp]

theorem RoseTree.isLeaf_node_nil {α : Type u_1} (a : α) : (node a []).isLeaf = true

@[simp]

theorem RoseTree.isLeaf_node_cons {α : Type u_1} (a : α) (c : RoseTree α) (cs : List (RoseTree α)) : (node a (c :: cs)).isLeaf = false

@[simp]

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

Smart constructors

def RoseTree.unary {α : Type u_1} (a : α) (c : RoseTree α) : RoseTree α

A unary node: a single child.

Equations

• RoseTree.unary a c = RoseTree.node a [c]

def RoseTree.binary {α : Type u_1} (a : α) (l r : RoseTree α) : RoseTree α

A binary node: two ordered children.

Equations

• RoseTree.binary a l r = RoseTree.node a [l, r]

def RoseTree.nary {α : Type u_1} (a : α) (cs : List (RoseTree α)) : RoseTree α

An n-ary node: a list of children.

Equations

• RoseTree.nary a cs = RoseTree.node a cs

@[simp]

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

@[simp]

theorem RoseTree.unary_def {α : Type u_1} (a : α) (c : RoseTree α) : unary a c = node a [c]

@[simp]

theorem RoseTree.binary_def {α : Type u_1} (a : α) (l r : RoseTree α) : binary a l r = node a [l, r]

@[simp]

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

depth — longest root-to-leaf path in vertices

depth = height + 1: a leaf has depth 1 (height counts edges, depth counts the vertices on the longest path).

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

Equations

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

@[simp]

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

@[simp]

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

theorem RoseTree.depth_le_foldr_max {α : Type u_1} {c : RoseTree α} {cs : List (RoseTree α)} (h : c ∈ cs) : c.depth ≤ List.foldr max 0 (List.map depth cs)

Each child's depth is at most the children's max depth.

theorem RoseTree.foldr_max_depth_le {α : Type u_1} {cs : List (RoseTree α)} {n : ℕ} (h : ∀ (c : RoseTree α), c ∈ cs → c.depth ≤ n) : List.foldr max 0 (List.map depth cs) ≤ n

The children's max depth is at most any common bound on the children.

map preserves the counts

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

Instances

@[implicit_reducible]

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

Equations

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

Sanity checks