Binary tree

Provides binary tree storage for values of any type, with O(lg n) retrieval. See also Lean.Data.RBTree for red-black trees - this version allows more operations to be defined and is better suited for in-kernel computation.

We also specialize for Tree Unit, which is a binary tree without any additional data. We provide the notation a △ b for making a Tree Unit with children a and b.

References

https://leanprover-community.github.io/archive/stream/113488-general/topic/tactic.20question.html

inductive Tree (α : Type u) : Type u

A binary tree with values stored in non-leaf nodes.

• nil {α : Type u} : Tree α
• node {α : Type u} : α → Tree α → Tree α → Tree α

instance instDecidableEqTree {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (Tree α✝)

Equations

• instDecidableEqTree = decEqTree✝

instance instReprTree {α✝ : Type u_1} [Repr α✝] : Repr (Tree α✝)

Equations

• instReprTree = { reprPrec := reprTree✝ }

instance Tree.instInhabited {α : Type u} : Inhabited (Tree α)

Equations

• Tree.instInhabited = { default := Tree.nil }

def Tree.traverse {m : Type u_1 → Type u_2} [Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) : Tree α → m (Tree β)

Do an action for every node of the tree. Actions are taken in node -> left subtree -> right subtree recursive order. This function is the traverse function for the Traversable Tree instance.

Equations

• Tree.traverse f Tree.nil = pure Tree.nil
• Tree.traverse f (Tree.node a a_1 a_2) = Tree.node <$> f a <*> Tree.traverse f a_1 <*> Tree.traverse f a_2

def Tree.map {α : Type u} {β : Type u_1} (f : α → β) : Tree α → Tree β

Apply a function to each value in the tree. This is the map function for the Tree functor.

Equations

• Tree.map f Tree.nil = Tree.nil
• Tree.map f (Tree.node a a_1 a_2) = Tree.node (f a) (Tree.map f a_1) (Tree.map f a_2)

theorem Tree.id_map {α : Type u} (t : Tree α) : map id t = t

theorem Tree.comp_map {α : Type u} {β : Type u_1} {γ : Type u_2} (f : α → β) (g : β → γ) (t : Tree α) : map (g ∘ f) t = map g (map f t)

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

def Tree.numNodes {α : Type u} : Tree α → ℕ

The number of internal nodes (i.e. not including leaves) of a binary tree

Equations

• Tree.nil.numNodes = 0
• (Tree.node a a_1 a_2).numNodes = a_1.numNodes + a_2.numNodes + 1

def Tree.numLeaves {α : Type u} : Tree α → ℕ

The number of leaves of a binary tree

Equations

• Tree.nil.numLeaves = 1
• (Tree.node a a_1 a_2).numLeaves = a_1.numLeaves + a_2.numLeaves

def Tree.height {α : Type u} : Tree α → ℕ

The height - length of the longest path from the root - of a binary tree

Equations

• Tree.nil.height = 0
• (Tree.node a a_1 a_2).height = max a_1.height a_2.height + 1

theorem Tree.numLeaves_eq_numNodes_succ {α : Type u} (x : Tree α) : x.numLeaves = x.numNodes + 1

theorem Tree.numLeaves_pos {α : Type u} (x : Tree α) : 0 < x.numLeaves

theorem Tree.height_le_numNodes {α : Type u} (x : Tree α) : x.height ≤ x.numNodes

def Tree.left {α : Type u} : Tree α → Tree α

The left child of the tree, or nil if the tree is nil

Equations

• Tree.nil.left = Tree.nil
• (Tree.node a a_1 a_2).left = a_1

def Tree.right {α : Type u} : Tree α → Tree α

The right child of the tree, or nil if the tree is nil

Equations

• Tree.nil.right = Tree.nil
• (Tree.node a a_1 a_2).right = a_2

def Tree.«term_△_» : Lean.TrailingParserDescr

A node with Unit data

Equations

• Tree.«term_△_» = Lean.ParserDescr.trailingNode `Tree.«term_△_» 65 66 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " △ ") (Lean.ParserDescr.cat `term 65))

def Tree.unitRecOn {motive : Tree Unit → Sort u_1} (t : Tree Unit) (base : motive nil) (ind : (x y : Tree Unit) → motive x → motive y → motive (node () x y)) : motive t

Induction principle for Tree Units

Equations

• Tree.unitRecOn t base ind = Tree.recOn t base fun (_u : Unit) => ind

theorem Tree.left_node_right_eq_self {x : Tree Unit} (_hx : x ≠ nil) : node () x.left x.right = x