Finite Trees

This file defines finite trees as a nested inductive type FiniteTree. The tree can have different types for the contents of its leafs and inner nodes.

inductive FiniteTree (α : Type u) (β : Type v) : Type (max u v)

An InductiveTree is either a leaf or a node that features a list of children that are again trees.

• leaf {α : Type u} {β : Type v} : β → FiniteTree α β
• inner {α : Type u} {β : Type v} : α → List (FiniteTree α β) → FiniteTree α β

@[irreducible]

def FiniteTree.rec' {α : Type u_1} {β : Type u_2} {motive : FiniteTree α β → Sort u} (leaf : (l : β) → motive (leaf l)) (inner : (label : α) → (ts : List (FiniteTree α β)) → ((t : FiniteTree α β) → t ∈ ts → motive t) → motive (inner label ts)) (t : FiniteTree α β) : motive t

A simplified recursor for proving properties of finite trees via induction. (The default recursor generated for the nested inductive type was not very useful for me.)

Equations

• FiniteTree.rec' leaf inner (FiniteTree.leaf l) = ⋯ ▸ ⋯ ▸ leaf l
• FiniteTree.rec' leaf inner (FiniteTree.inner label ts) = ⋯ ▸ ⋯ ▸ inner label ts fun (t : FiniteTree α β) (x : t ∈ ts) => FiniteTree.rec' leaf inner t

def finiteTreeEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (a b : FiniteTree α β) : Decidable (a = b)

Equations

• One or more equations did not get rendered due to their size.
• finiteTreeEq (FiniteTree.leaf lb) (FiniteTree.leaf lb_1) = if eq_ls : lb = lb_1 then isTrue ⋯ else isFalse ⋯
• finiteTreeEq (FiniteTree.leaf lb) (FiniteTree.inner a a_1) = isFalse ⋯
• finiteTreeEq (FiniteTree.inner a_1 a_2) (FiniteTree.leaf lb) = isFalse ⋯

def finiteTreeListEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (a b : List (FiniteTree α β)) : Decidable (a = b)

Equations

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

@[implicit_reducible]

instance instDecidableEqFiniteTreeOfDecidableEq {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (a b : FiniteTree α β) : Decidable (a = b)

Equations

• instDecidableEqFiniteTreeOfDecidableEq a b = finiteTreeEq a b

@[irreducible]

def FiniteTree.depth {α : Type u_1} {β : Type u_2} : FiniteTree α β → Nat

Returns the depth of the tree where a leaf is defined to have depth 1.

Equations

• (FiniteTree.leaf a).depth = 1
• (FiniteTree.inner a ts).depth = 1 + (List.map FiniteTree.depth ts).max?.getD 1

@[irreducible]

def FiniteTree.leaves {α : Type u_1} {β : Type u_2} : FiniteTree α β → List β

Returns all leaf nodes of the tree as a single list. (Intuitively you simply read all leaves from left to right).

Equations

• (FiniteTree.leaf a).leaves = [a]
• (FiniteTree.inner a ts).leaves = List.flatMap FiniteTree.leaves ts

@[irreducible]

def FiniteTree.innerLabels {α : Type u_1} {β : Type u_2} : FiniteTree α β → List α

Returns all nodes that are not leaves as a single list. You can imagine going branch by branch from left to right while avoiding using the same node twice.

Equations

• (FiniteTree.leaf a).innerLabels = []
• (FiniteTree.inner a ts).innerLabels = a :: List.flatMap FiniteTree.innerLabels ts

@[irreducible]

def FiniteTree.mapLeaves {β : Type u_1} {α : Type u_2} {γ : Type u_3} (f : β → FiniteTree α γ) : FiniteTree α β → FiniteTree α γ

Returns the tree there we leaf nodes have been replaced according to the function f.

Equations

• FiniteTree.mapLeaves f (FiniteTree.leaf b) = f b
• FiniteTree.mapLeaves f (FiniteTree.inner a ts) = FiniteTree.inner a (List.map (FiniteTree.mapLeaves f) ts)

theorem FiniteTree.mapLeaves_eq_of_map_leaves_eq {β : Type u_1} {α : Type u_2} {γ : Type u_3} {f g : β → FiniteTree α γ} {t : FiniteTree α β} : List.map f t.leaves = List.map g t.leaves → mapLeaves f t = mapLeaves g t

The trees resulting from two different leaf mappings are the same of applying the functions only on the list of leaves yields the same list.

def FiniteTree.nodeLabel {α : Type u_1} : FiniteTree α α → α

Returns the root label of a given tree. This only works if the types for leaf and inner nodes are the same.

Equations

• (FiniteTree.leaf a).nodeLabel = a
• (FiniteTree.inner a a_1).nodeLabel = a

theorem FiniteTree.tree_eq_while_contained_is_impossible {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] (t : FiniteTree α β) (ts : List (FiniteTree α β)) (a : α) (h_eq : inner a ts = t) (h_contains : t ∈ ts) : False

A tree cannot occur as its own child.