mathlib3 documentation

data.tree

Binary tree #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Provides binary tree storage for values of any type, with O(lg n) retrieval. See also 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

@[protected, instance]

def tree.decidable_eq (α : Type u) [a : decidable_eq α] :

decidable_eq (tree α)

@[protected, instance]

meta def tree.has_reflect (α : Type) [a : has_reflect α] [a_1 : reflected Type α] :

has_reflect (tree α)

inductive tree (α : Type u) :

nil : Π {α : Type u}, tree α
node : Π {α : Type u}, α → tree α → tree α → tree α

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

Instances for tree

def tree.repr {α : Type u} [has_repr α] :

tree α → string

Construct a string representation of a tree. Provides a has_repr instance.

Equations

(tree.node a t1 t2).repr = "tree.node " ++ has_repr.repr a ++ " (" ++ t1.repr ++ ") (" ++ t2.repr ++ ")"
tree.nil.repr = "nil"

@[protected, instance]

def tree.has_repr {α : Type u} [has_repr α] :

has_repr (tree α)

Equations

tree.has_repr = {repr := tree.repr _inst_1}

@[protected, instance]

def tree.inhabited {α : Type u} :

inhabited (tree α)

Equations

tree.inhabited = {default := tree.nil α}

def tree.of_rbnode {α : Type u} :

rbnode α → tree α

Makes a tree α out of a red-black tree.

Equations

tree.of_rbnode (l.black_node a r) = tree.node a (tree.of_rbnode l) (tree.of_rbnode r)
tree.of_rbnode (l.red_node a r) = tree.node a (tree.of_rbnode l) (tree.of_rbnode r)
tree.of_rbnode rbnode.leaf = tree.nil

def tree.index_of {α : Type u} (lt : α → α → Prop) [decidable_rel lt] (x : α) :

tree α → option pos_num

Finds the index of an element in the tree assuming the tree has been constructed according to the provided decidable order on its elements. If it hasn't, the result will be incorrect. If it has, but the element is not in the tree, returns none.

Equations

tree.index_of lt x (tree.node a t₁ t₂) = tree.index_of._match_1 (tree.index_of lt x t₁) (tree.index_of lt x t₂) (cmp_using lt x a)
tree.index_of lt x tree.nil = option.none
tree.index_of._match_1 _f_1 _f_2 ordering.gt = pos_num.bit1 <$> _f_2
tree.index_of._match_1 _f_1 _f_2 ordering.eq = option.some pos_num.one
tree.index_of._match_1 _f_1 _f_2 ordering.lt = pos_num.bit0 <$> _f_1

def tree.get {α : Type u} :

pos_num → tree α → option α

Retrieves an element uniquely determined by a pos_num from the tree, taking the following path to get to the element:

bit0 - go to left child
bit1 - go to right child
pos_num.one - retrieve from here

Equations

tree.get n.bit0 (tree.node a t₁ t₂) = tree.get n t₁
tree.get ᾰ.bit0 tree.nil = option.none
tree.get n.bit1 (tree.node a t₁ t₂) = tree.get n t₂
tree.get ᾰ.bit1 tree.nil = option.none
tree.get pos_num.one (tree.node a t₁ t₂) = option.some a
tree.get pos_num.one tree.nil = option.none

def tree.get_or_else {α : Type u} (n : pos_num) (t : tree α) (v : α) :

α

Retrieves an element from the tree, or the provided default value if the index is invalid. See tree.get.

Equations

tree.get_or_else n t v = (tree.get n t).get_or_else v

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. TODO: implement traversable tree.

Equations

tree.map f (tree.node a l r) = tree.node (f a) (tree.map f l) (tree.map f r)
tree.map f tree.nil = tree.nil

@[simp]

def tree.num_nodes {α : Type u} :

tree α → ℕ

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

Equations

(tree.node _x a b).num_nodes = a.num_nodes + b.num_nodes + 1
tree.nil.num_nodes = 0

@[simp]

def tree.num_leaves {α : Type u} :

tree α → ℕ

The number of leaves of a binary tree

Equations

(tree.node _x a b).num_leaves = a.num_leaves + b.num_leaves
tree.nil.num_leaves = 1

@[simp]

def tree.height {α : Type u} :

tree α → ℕ

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

Equations

(tree.node _x a b).height = linear_order.max a.height b.height + 1
tree.nil.height = 0

theorem tree.num_leaves_eq_num_nodes_succ {α : Type u} (x : tree α) :

x.num_leaves = x.num_nodes + 1

theorem tree.num_leaves_pos {α : Type u} (x : tree α) :

0 < x.num_leaves

theorem tree.height_le_num_nodes {α : Type u} (x : tree α) :

x.height ≤ x.num_nodes

@[simp]

def tree.left {α : Type u} :

tree α → tree α

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

Equations

(tree.node _x l r).left = l
tree.nil.left = tree.nil

@[simp]

def tree.right {α : Type u} :

tree α → tree α

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

Equations

(tree.node _x l r).right = r
tree.nil.right = tree.nil

def tree.unit_rec_on {motive : tree unit → Sort u_1} (t : tree unit) (base : motive tree.nil) (ind : Π (x y : tree unit), motive x → motive y → motive (tree.node unit.star() x y)) :

motive t

Recursion on tree unit; allows for a better induction which does not have to worry about the element of type α = unit

Equations

t.unit_rec_on base ind = t.rec_on base (λ (u : unit), punit.rec_on u ind)

theorem tree.left_node_right_eq_self {x : tree unit} (hx : x ≠ tree.nil) :

tree.node unit.star() x.left x.right = x