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 CustomBasicDatastructures.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 CustomBasicDatastructures.FiniteTree.rec' {α : Type u} {β : Type v} {motive : FiniteTree α β → Sort w} (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

• One or more equations did not get rendered due to their size.
• CustomBasicDatastructures.FiniteTree.rec' leaf inner (CustomBasicDatastructures.FiniteTree.leaf l) = ⋯ ▸ ⋯ ▸ leaf l

def CustomBasicDatastructures.finiteTreeEq {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a b : FiniteTree α β) : Decidable (a = b)

Equations

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

def CustomBasicDatastructures.finiteTreeListEq {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a b : List (FiniteTree α β)) : Decidable (a = b)

Equations

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

@[instance_reducible]

instance CustomBasicDatastructures.instDecidableEqFiniteTreeOfDecidableEq {α : Type u} {β : Type v} [DecidableEq α] [DecidableEq β] (a b : FiniteTree α β) : Decidable (a = b)

Equations

• CustomBasicDatastructures.instDecidableEqFiniteTreeOfDecidableEq a b = CustomBasicDatastructures.finiteTreeEq a b

@[irreducible]

def CustomBasicDatastructures.FiniteTree.depth {α : Type u} {β : Type v} : FiniteTree α β → Nat

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

Equations

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

@[irreducible]

def CustomBasicDatastructures.FiniteTree.leaves {α : Type u} {β : Type v} : FiniteTree α β → List β

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

Equations

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

@[irreducible]

def CustomBasicDatastructures.FiniteTree.innerLabels {α : Type u} {β : Type v} : 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

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

@[irreducible]

def CustomBasicDatastructures.FiniteTree.subtrees {α : Type u} {β : Type v} : FiniteTree α β → List (FiniteTree α β)

Returns all subtrees, i.e. the tree itself and all subtrees of its immediate children.

Equations

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

@[irreducible]

def CustomBasicDatastructures.FiniteTree.mapLeaves {α : Type u} {β : Type v} {γ : Type v'} (f : β → FiniteTree α γ) : FiniteTree α β → FiniteTree α γ

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

Equations

• One or more equations did not get rendered due to their size.
• CustomBasicDatastructures.FiniteTree.mapLeaves f (CustomBasicDatastructures.FiniteTree.leaf a) = f a

theorem CustomBasicDatastructures.FiniteTree.mapLeaves_eq_of_map_leaves_eq {α : Type u} {β : Type v} {γ : Type v'} {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 CustomBasicDatastructures.FiniteTree.nodeLabel {α : Type u} : FiniteTree α α → α

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

Equations

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

theorem CustomBasicDatastructures.FiniteTree.tree_eq_while_contained_is_impossible {α : Type u} {β : Type v} [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.