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 ⋯

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 lb).depth = 1
• (FiniteTree.inner a a_1).depth = 1 + (List.map FiniteTree.depth a_1).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 lb).leaves = [lb]
• (FiniteTree.inner a a_1).leaves = List.flatMap FiniteTree.leaves a_1

@[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 lb).innerLabels = []
• (FiniteTree.inner a a_1).innerLabels = a :: List.flatMap FiniteTree.innerLabels a_1

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

def FiniteTree.forEach {α : Type u_1} {β : Type u_2} (f : FiniteTree α β → Prop) : FiniteTree α β → Prop

Check that f holds for each subtree of a given tree.

Equations

• FiniteTree.forEach f (FiniteTree.leaf lb) = f (FiniteTree.leaf lb)
• FiniteTree.forEach f (FiniteTree.inner a a_1) = (f (FiniteTree.inner a a_1) ∧ ∀ (t : FiniteTree α β), t ∈ a_1 → f t)

def FiniteTree.treesInDepth {α : Type u_1} {β : Type u_2} (t : FiniteTree α β) (depth : Nat) : List (FiniteTree α β)

For a given depth, returns all subtrees of the given tree t that have their root at this depth in t.

Equations

• t.treesInDepth depth = FiniteTree.privateTreesInDepth✝ t depth 0

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.