Unbalanced binary search trees

An ordinary binary search tree reuses Mathlib's BinaryTree. Keys strictly smaller than the root occur on the left, larger keys on the right. Inserting a duplicate leaves the tree unchanged. These are the textbook search and insertion algorithms of Cormen et al., Chapter 12.

Main definitions

• elements: the finite set represented by a tree.
• Ordered: the strict binary-search-tree invariant.
• contains, insert, minimum, successor: executable search-tree operations.

Main results

• contains_eq_true: membership is exactly finite-set membership.
• elements_insert, ordered_insert: insertion has set semantics and preserves the invariant.
• minimum_spec, successor_spec: queries return the least eligible key, or none.

Trees are not balanced. Cost bounds in the companion module depend on their actual height.

References

• T. H. Cormen, C. E. Leiserson, R. L. Rivest and C. Stein, Introduction to Algorithms, Chapter 12

def Cslib.Algorithms.Lean.SearchTree.elements {α : Type u_1} [LinearOrder α] : BinaryTree α → Finset α

The finite set of keys stored at internal nodes.

def Cslib.Algorithms.Lean.SearchTree.Ordered {α : Type u_1} [LinearOrder α] : BinaryTree α → Prop

Strict subtree separation rules out duplicate keys.

def Cslib.Algorithms.Lean.SearchTree.contains {α : Type u_1} [LinearOrder α] (x : α) : BinaryTree α → Bool

Follow a single search path; no subtree is scanned.

def Cslib.Algorithms.Lean.SearchTree.insert {α : Type u_1} [LinearOrder α] (x : α) : BinaryTree α → BinaryTree α

Insert at the first empty child on the search path; equality preserves the existing node.

def Cslib.Algorithms.Lean.SearchTree.minimum {α : Type u_1} : BinaryTree α → Option α

Follow left children to find the least key.

def Cslib.Algorithms.Lean.SearchTree.successor {α : Type u_1} [LinearOrder α] (x : α) : BinaryTree α → Option α

The least stored key strictly greater than x, including when x is absent.

@[simp]

theorem Cslib.Algorithms.Lean.SearchTree.mem_elements_node {α : Type u_1} [LinearOrder α] {x a : α} {l r : BinaryTree α} : x ∈ elements (BinaryTree.node a l r) ↔ x = a ∨ x ∈ elements l ∨ x ∈ elements r

Membership in a node's element set splits across the root key and the two subtrees.

theorem Cslib.Algorithms.Lean.SearchTree.contains_eq_true {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) (x : α) : contains x t = true ↔ x ∈ elements t

Search is correct for any shape satisfying the invariant.

theorem Cslib.Algorithms.Lean.SearchTree.elements_insert {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : elements (insert x t) = Insert.insert x (elements t)

Insertion adds exactly the requested key, even when it was already present.

theorem Cslib.Algorithms.Lean.SearchTree.ordered_insert {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) (x : α) : Ordered (insert x t)

The binary-search-tree invariant survives insertion.

theorem Cslib.Algorithms.Lean.SearchTree.insert_eq_self {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) {x : α} (hx : x ∈ elements t) : insert x t = t

Re-inserting a present key preserves the entire tree, not just its represented set.

theorem Cslib.Algorithms.Lean.SearchTree.card_elements {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) : (elements t).card = t.numNodes

A strict search tree stores each represented key in exactly one node.

theorem Cslib.Algorithms.Lean.SearchTree.minimum_spec {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) : OrderedSet.LeastResult (elements t) (minimum t)

Left descent returns the least element, with the empty case accounted for.

theorem Cslib.Algorithms.Lean.SearchTree.successor_spec {α : Type u_1} [LinearOrder α] {t : BinaryTree α} (ht : Ordered t) (x : α) : OrderedSet.LeastResult ({x_1 ∈ elements t | x < x_1}) (successor x t)

Successor is strict and does not require the query itself to belong to the tree.