Forests are binary trees

A forest, a list of rose trees, is either empty or a first tree followed by a forest, and the first tree is a value over the forest of its children. A binary tree is either nil or a value with a left and a right subtree. Reading the left subtree as the children of the first tree and the right subtree as the rest of the forest identifies the two: this is the natural correspondence between forests and binary trees of [Knu97], the left-child right-sibling representation. A rose tree is a value together with the forest of its children, hence a value together with a binary tree, and rose trees over an encodable type are encodable.

Main declarations

• BinaryTree.ofForest, BinaryTree.toForest: the natural correspondence and its inverse, bundled as BinaryTree.equivForest; BinaryTree.cons is the list cons transported along it.
• RoseTree.equivProdBinaryTree: a rose tree is a value together with a binary tree.
• RoseTree.encodable, RoseTree.countable: the instances transported along it.

Main results

• BinaryTree.numNodes_ofForest, BinaryTree.numNodes_cons: the correspondence preserves the number of nodes.

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

The natural correspondence sends a forest to the binary tree obtained by consing its trees, in order, onto nil.

Equations

• BinaryTree.ofForest [] = BinaryTree.nil
• BinaryTree.ofForest (t :: rest) = BinaryTree.cons t (BinaryTree.ofForest rest)

def BinaryTree.cons {α : Type u_1} : RoseTree α → BinaryTree α → BinaryTree α

The list cons transported along the natural correspondence makes a tree a node whose left subtree is the forest of its children and whose right subtree is the rest of the forest.

Equations

• BinaryTree.cons (RoseTree.node a cs) x✝ = BinaryTree.node a (BinaryTree.ofForest cs) x✝

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

The inverse of the natural correspondence BinaryTree.ofForest.

Equations

• BinaryTree.nil.toForest = []
• (BinaryTree.node a l r).toForest = RoseTree.node a l.toForest :: r.toForest

@[simp]

theorem BinaryTree.ofForest_nil {α : Type u_1} : ofForest [] = nil

@[simp]

theorem BinaryTree.ofForest_cons {α : Type u_1} (t : RoseTree α) (rest : List (RoseTree α)) : ofForest (t :: rest) = cons t (ofForest rest)

@[simp]

theorem BinaryTree.cons_node {α : Type u_1} (a : α) (cs : List (RoseTree α)) (r : BinaryTree α) : cons (RoseTree.node a cs) r = node a (ofForest cs) r

@[simp]

theorem BinaryTree.toForest_nil {α : Type u_1} : nil.toForest = []

@[simp]

theorem BinaryTree.toForest_node {α : Type u_1} (a : α) (l r : BinaryTree α) : (node a l r).toForest = RoseTree.node a l.toForest :: r.toForest

@[simp]

theorem BinaryTree.toForest_ofForest {α : Type u_1} (cs : List (RoseTree α)) : (ofForest cs).toForest = cs

@[simp]

theorem BinaryTree.toForest_cons {α : Type u_1} (t : RoseTree α) (r : BinaryTree α) : (cons t r).toForest = t :: r.toForest

@[simp]

theorem BinaryTree.ofForest_toForest {α : Type u_1} (t : BinaryTree α) : ofForest t.toForest = t

def BinaryTree.equivForest {α : Type u_1} : BinaryTree α ≃ List (RoseTree α)

The natural correspondence between binary trees and forests.

Equations

• BinaryTree.equivForest = { toFun := BinaryTree.toForest, invFun := BinaryTree.ofForest, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem BinaryTree.equivForest_symm_apply {α : Type u_1} (a✝ : List (RoseTree α)) : equivForest.symm a✝ = ofForest a✝

@[simp]

theorem BinaryTree.equivForest_apply {α : Type u_1} (a✝ : BinaryTree α) : equivForest a✝ = a✝.toForest

theorem BinaryTree.numNodes_ofForest {α : Type u_1} (cs : List (RoseTree α)) : (ofForest cs).numNodes = (List.map RoseTree.numNodes cs).sum

theorem BinaryTree.numNodes_cons {α : Type u_1} (t : RoseTree α) (r : BinaryTree α) : (cons t r).numNodes = t.numNodes + r.numNodes

def RoseTree.equivProdBinaryTree {α : Type u_1} : RoseTree α ≃ α × BinaryTree α

A rose tree is its root value together with the binary tree of the forest of its children.

Equations

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

@[simp]

theorem RoseTree.equivProdBinaryTree_apply {α : Type u_1} (t : RoseTree α) : equivProdBinaryTree t = (t.value, BinaryTree.ofForest t.children)

@[simp]

theorem RoseTree.equivProdBinaryTree_symm_apply {α : Type u_1} (p : α × BinaryTree α) : equivProdBinaryTree.symm p = node p.1 p.2.toForest

@[instance_reducible]

instance RoseTree.encodable {α : Type u_1} [Encodable α] : Encodable (RoseTree α)

Equations

• RoseTree.encodable = Encodable.ofEquiv (α × BinaryTree α) RoseTree.equivProdBinaryTree

instance RoseTree.countable {α : Type u_1} [Countable α] : Countable (RoseTree α)