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

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

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

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

Equations

• instDecidableEqTree = decEqTree✝

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

Equations

• instReprTree = { reprPrec := reprTree✝ }

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

Equations

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

def Tree.ofRBNode {α : Type u} : Std.RBNode α → Tree α

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

Equations

• Tree.ofRBNode Std.RBNode.nil = Tree.nil
• Tree.ofRBNode (Std.RBNode.node _color l key r) = Tree.node key (Tree.ofRBNode l) (Tree.ofRBNode r)

def Tree.indexOf {α : Type u} (lt : α → α → Prop) [DecidableRel lt] (x : α) : Tree α → Option PosNum

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

• One or more equations did not get rendered due to their size.
• Tree.indexOf lt x Tree.nil = none

def Tree.get {α : Type u} : PosNum → Tree α → Option α

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

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

Equations

• Tree.get x Tree.nil = none
• Tree.get PosNum.one (Tree.node a _t₁ _t₂) = some a
• Tree.get (PosNum.bit0 n) (Tree.node _a t₁ _t₂) = Tree.get n t₁
• Tree.get (PosNum.bit1 n) (Tree.node _a _t₁ t₂) = Tree.get n t₂

def Tree.getOrElse {α : Type u} (n : PosNum) (t : Tree α) (v : α) : α

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

Equations

• Tree.getOrElse n t v = Option.getD (Tree.get n t) 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.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)

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

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

Equations

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

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

The number of leaves of a binary tree

Equations

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

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

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

Equations

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

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

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

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

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

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

Equations

• Tree.left x = match x with | Tree.nil => Tree.nil | Tree.node a l _r => l

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

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

Equations

• Tree.right x = match x with | Tree.nil => Tree.nil | Tree.node a _l r => r

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

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 Tree.nil) (ind : (x y : Tree Unit) → motive x → motive y → motive (Tree.node () x y)) : motive t

Equations

• Tree.unitRecOn t base ind = Tree.recOn t base fun _u => ind

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