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 BinaryTree Unit, which is a binary tree without any additional data. We provide the notation a △ b for making a BinaryTree Unit with children a and b.

References

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

inductive BinaryTree (α : Type u) : Type u

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

• nil {α : Type u} : BinaryTree α
• node {α : Type u} (value : α) (left right : BinaryTree α) : BinaryTree α

@[implicit_reducible]

instance instDecidableEqBinaryTree {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (BinaryTree α✝)

Equations

• instDecidableEqBinaryTree = instDecidableEqBinaryTree.decEq

def instDecidableEqBinaryTree.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : BinaryTree α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqBinaryTree.decEq BinaryTree.nil BinaryTree.nil = isTrue ⋯
• instDecidableEqBinaryTree.decEq BinaryTree.nil (BinaryTree.node value left right) = isFalse ⋯
• instDecidableEqBinaryTree.decEq (BinaryTree.node value left right) BinaryTree.nil = isFalse ⋯

@[implicit_reducible]

instance instReprBinaryTree {α✝ : Type u_1} [Repr α✝] : Repr (BinaryTree α✝)

Equations

• instReprBinaryTree = { reprPrec := instReprBinaryTree.repr }

def instReprBinaryTree.repr {α✝ : Type u_1} [Repr α✝] : BinaryTree α✝ → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprBinaryTree.repr BinaryTree.nil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "BinaryTree.nil")).group prec✝

@[reducible, deprecated BinaryTree (since := "2026-06-07")]

def Tree (α : Type u) : Type u

Alias of BinaryTree.

---

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

Equations

• Tree = BinaryTree

@[reducible, inline, deprecated BinaryTree.nil (since := "2026-06-07")]

abbrev Tree.nil {α : Type u} : Tree α

Alias of BinaryTree.nil.

Equations

• Tree.nil = BinaryTree.nil

@[reducible, inline, deprecated BinaryTree.node (since := "2026-06-07")]

abbrev Tree.node {α : Type u} (value : α) (left right : Tree α) : Tree α

Alias of BinaryTree.node.

Equations

• Tree.node value left right = BinaryTree.node value left right

@[implicit_reducible]

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

Equations

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

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

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 BinaryTree instance.

Equations

• BinaryTree.traverse f BinaryTree.nil = pure BinaryTree.nil
• BinaryTree.traverse f (BinaryTree.node a l r) = BinaryTree.node <$> f a <*> BinaryTree.traverse f l <*> BinaryTree.traverse f r

@[reducible, inline, deprecated BinaryTree.traverse (since := "2026-06-07")]

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

Alias of BinaryTree.traverse.

Equations

• Tree.traverse f t = BinaryTree.traverse f t

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

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

Equations

• BinaryTree.map f BinaryTree.nil = BinaryTree.nil
• BinaryTree.map f (BinaryTree.node a l r) = BinaryTree.node (f a) (BinaryTree.map f l) (BinaryTree.map f r)

@[reducible, inline, deprecated BinaryTree.map (since := "2026-06-07")]

abbrev Tree.map {α : Type u_1} {β : Type u_2} (f : α → β) (t : Tree α) : Tree β

Alias of BinaryTree.map.

Equations

• Tree.map f t = BinaryTree.map f t

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

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

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

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

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

Equations

• BinaryTree.nil.numNodes = 0
• (BinaryTree.node a l r).numNodes = l.numNodes + r.numNodes + 1

@[reducible, inline, deprecated BinaryTree.numNodes (since := "2026-06-07")]

abbrev Tree.numNodes {α : Type u_1} (t : Tree α) : ℕ

Alias of BinaryTree.numNodes.

Equations

• t.numNodes = BinaryTree.numNodes t

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

The number of leaves of a binary tree

Equations

• BinaryTree.nil.numLeaves = 1
• (BinaryTree.node a l r).numLeaves = l.numLeaves + r.numLeaves

@[reducible, inline, deprecated BinaryTree.numLeaves (since := "2026-06-07")]

abbrev Tree.numLeaves {α : Type u_1} (t : Tree α) : ℕ

Alias of BinaryTree.numLeaves.

Equations

• t.numLeaves = BinaryTree.numLeaves t

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

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

Equations

• BinaryTree.nil.height = 0
• (BinaryTree.node a l r).height = max l.height r.height + 1

@[reducible, inline, deprecated BinaryTree.height (since := "2026-06-07")]

abbrev Tree.height {α : Type u_1} (t : Tree α) : ℕ

Alias of BinaryTree.height.

Equations

• t.height = BinaryTree.height t

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

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

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

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

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

Equations

• BinaryTree.nil.left = BinaryTree.nil
• (BinaryTree.node a l r).left = l

@[reducible, inline, deprecated BinaryTree.left (since := "2026-06-07")]

abbrev Tree.left {α : Type u_1} (t : Tree α) : Tree α

Alias of BinaryTree.left.

Equations

• t.left = BinaryTree.left t

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

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

Equations

• BinaryTree.nil.right = BinaryTree.nil
• (BinaryTree.node a l r).right = r

@[reducible, inline, deprecated BinaryTree.right (since := "2026-06-07")]

abbrev Tree.right {α : Type u_1} (t : Tree α) : Tree α

Alias of BinaryTree.right.

Equations

• t.right = BinaryTree.right t

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

A node with Unit data

Equations

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

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

Induction principle for BinaryTree Units

Equations

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

@[reducible, inline, deprecated BinaryTree.unitRecOn (since := "2026-06-07")]

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

Alias of BinaryTree.unitRecOn.

Equations

• Tree.unitRecOn t base ind = BinaryTree.unitRecOn t base ind

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