1. CLRS-Lean
  2. Chapter 12. Binary Search Trees
  3. 12.1. Binary Search Trees
Imports
import Mathlib

CLRS Section 12.1 - Binary search trees

This section gives a first Lean model of binary search trees as inductive trees of natural-number keys. It proves the fundamental search and insertion facts used by the textbook invariant argument: search is correct on ordered trees, minimum and maximum return genuine extremal keys, insertion adds exactly the inserted key to the membership set, and insertion preserves the BST ordering invariant. It also proves functional successor and predecessor queries: the successor is the least key greater than the query, and the predecessor is the greatest key less than the query. Finally, it proves a functional deletion operation that removes exactly the requested key and preserves ordering.

Main results:

  • Theorem search_eq_true_iff: Boolean search is equivalent to tree membership on ordered trees.

  • Theorem minimum?_inTree: a returned minimum key occurs in the tree.

  • Theorem minimum?_le_of_ordered: a returned minimum key is a lower bound on an ordered tree.

  • Theorem maximum?_inTree: a returned maximum key occurs in the tree.

  • Theorem le_maximum?_of_ordered: a returned maximum key is an upper bound on an ordered tree.

  • Theorem successor?_least_greater: a returned successor is the least tree key strictly greater than the query.

  • Theorem successor?_eq_some_iff: complete iff specification for a returned successor.

  • Theorem successor?_eq_none_iff: complete none specification for a missing successor.

  • Theorem successor?_isSome_iff_exists_greater: successor existence is equivalent to the existence of a greater tree key.

  • Theorem predecessor?_greatest_less: a returned predecessor is the greatest tree key strictly less than the query.

  • Theorem predecessor?_eq_some_iff: complete iff specification for a returned predecessor.

  • Theorem predecessor?_eq_none_iff: complete none specification for a missing predecessor.

  • Theorem predecessor?_isSome_iff_exists_less: predecessor existence is equivalent to the existence of a smaller tree key.

  • Theorem inTree_insert_iff: membership after insertion is exactly the old membership relation plus the inserted key.

  • Theorem search_insert_eq_true_iff: searching after insertion succeeds exactly for the inserted key or an old key.

  • Theorem insert_ordered: insertion preserves the BST ordering invariant.

  • Theorem inTree_delete_iff: functional deletion removes exactly the requested key.

  • Theorem delete_ordered: functional deletion preserves the BST ordering invariant.

  • Theorem not_inTree_delete_self: the deleted key is absent afterward.

  • Theorem delete_eq_self_of_not_inTree: deleting a missing key leaves an ordered tree unchanged.

  • Theorem search_delete_self_eq_false: searching for the deleted key after deletion returns false.

  • Theorem search_delete_eq_true_iff: searching after deletion succeeds exactly for old keys different from the deleted key.

  • Theorem successor?_delete_eq_some_iff: after deletion, the returned successor is the least old key above the query and different from the deleted key.

  • Theorem successor?_delete_eq_none_iff: after deletion, no successor is returned exactly when every old key except the deleted key is at most the query.

  • Theorem predecessor?_delete_eq_some_iff: after deletion, the returned predecessor is the greatest old key below the query and different from the deleted key.

  • Theorem predecessor?_delete_eq_none_iff: after deletion, no predecessor is returned exactly when every old key except the deleted key is at least the query.

Current gaps:

  • Parent-pointer successor/predecessor procedures, transplant, and pointer-level tree mutation are future section targets.

namespace CLRSnamespace Chapter12

Tree model and invariant

A binary tree of natural-number keys.

inductive BSTree where | empty : BSTree | node : BSTree → Nat → BSTree → BSTree deriving Repr, DecidableEq
namespace BSTree

Membership of a key in a binary tree.

def InTree (x : Nat) : BSTree → Prop | empty => False | node left key right => x = key ∨ InTree x left ∨ InTree x right

Every key in the tree is strictly less than bound.

def AllLt (bound : Nat) (t : BSTree) : Prop := ∀ x, InTree x t → x < bound

Every key in the tree is strictly greater than bound.

def AllGt (bound : Nat) (t : BSTree) : Prop := ∀ x, InTree x t → bound < x

The binary-search-tree ordering invariant.

def Ordered : BSTree → Prop | empty => True | node left key right => Ordered left ∧ Ordered right ∧ AllLt key left ∧ AllGt key right

Functional insertion into a binary search tree.

def insert (x : Nat) : BSTree → BSTree | empty => node empty x empty | node left key right => if x < key then node (insert x left) key right else if key < x then node left key (insert x right) else node left key right

Search, minimum, and maximum operations

Search for a key using the binary-search-tree ordering decisions.

def search (x : Nat) : BSTree → Bool | empty => false | node left key right => if x = key then true else if x < key then search x left else search x right

The minimum key of a nonempty tree, found by following left children.

def minimum? : BSTree → Option Nat | empty => none | node empty key _right => some key | node left@(node _ _ _) _key _right => minimum? left

The maximum key of a nonempty tree, found by following right children.

def maximum? : BSTree → Option Nat | empty => none | node _left key empty => some key | node _left _key right@(node _ _ _) => maximum? right

The least key in the tree that is strictly greater than x, if such a key exists. This is a functional counterpart of CLRS successor search without parent pointers.

def successor? (x : Nat) : BSTree → Option Nat | empty => none | node left key right => if x < key then match successor? x left with | some y => some y | none => some key else successor? x right

The greatest key in the tree that is strictly less than x, if such a key exists. This is a functional counterpart of CLRS predecessor search without parent pointers.

def predecessor? (x : Nat) : BSTree → Option Nat | empty => none | node left key right => if key < x then match predecessor? x right with | some y => some y | none => some key else predecessor? x left

A total version of the minimum-key operation. The value on an empty tree is a dummy; all public theorems use it only through membership hypotheses or nonempty subtrees.

def minKey : BSTree → Nat | empty => 0 | node empty key _right => key | node left@(node _ _ _) _key _right => minKey left

Delete the minimum key from a tree, leaving empty trees unchanged.

def deleteMin : BSTree → BSTree | empty => empty | node empty _key right => right | node left@(node _ _ _) key right => node (deleteMin left) key right

Delete the root of a tree. When both children are present, the root is replaced by the minimum key of the right subtree, matching the successor-replacement idea from the CLRS deletion proof.

def deleteRoot : BSTree → BSTree | empty => empty | node left _key empty => left | node left _key right@(node _ _ _) => node left (minKey right) (deleteMin right)

Functional deletion from a binary search tree.

def delete (x : Nat) : BSTree → BSTree | empty => empty | node left key right => if x < key then node (delete x left) key right else if key < x then node left key (delete x right) else deleteRoot (node left key right)

Search correctness

On an ordered tree, Boolean search is equivalent to tree membership.

Minimum and maximum correctness

If minimum? returns a key, that key occurs in the tree.

On an ordered tree, the result returned by minimum? is a lower bound.

If maximum? returns a key, that key occurs in the tree.

On an ordered tree, the result returned by maximum? is an upper bound.

Successor and predecessor correctness

If the functional successor query returns none, no tree key is strictly greater than the query key.

Functional successor correctness: if successor? x t = some s on an ordered tree, then s occurs in the tree, x < s, and every tree key greater than x is at least s.

exact ⟨ Or.inr (Or.inr hInRight), hxs, ⟩

If the functional predecessor query returns none, no tree key is strictly less than the query key.

Functional predecessor correctness: if predecessor? x t = some p on an ordered tree, then p occurs in the tree, p < x, and every tree key less than x is at most p.

exact ⟨ Or.inr (Or.inl hInLeft), hpx, ⟩

Complete iff specification for a returned functional successor.

theorem successor?_eq_some_iff {x s : Nat} {t : BSTree} (ht : Ordered t) : successor? x t = some s ↔ InTree s t ∧ x < s ∧ ∀ y, InTree y t → x < y → s ≤ y := cases hs : successor? x t with

Complete none specification for a missing functional successor.

theorem successor?_eq_none_iff {x : Nat} {t : BSTree} (ht : Ordered t) : successor? x t = none ↔ ∀ y, InTree y t → y ≤ x := cases hs : successor? x t with

Complete iff specification for a returned functional predecessor.

theorem predecessor?_eq_some_iff {x p : Nat} {t : BSTree} (ht : Ordered t) : predecessor? x t = some p ↔ InTree p t ∧ p < x ∧ ∀ y, InTree y t → y < x → y ≤ p := cases hp : predecessor? x t with

Complete none specification for a missing functional predecessor.

theorem predecessor?_eq_none_iff {x : Nat} {t : BSTree} (ht : Ordered t) : predecessor? x t = none ↔ ∀ y, InTree y t → x ≤ y := cases hp : predecessor? x t with

A functional successor exists exactly when some tree key is greater.

theorem successor?_isSome_iff_exists_greater {x : Nat} {t : BSTree} (ht : Ordered t) : (successor? x t).isSome ↔ ∃ y, InTree y t ∧ x < y := cases hs : successor? x t with cases hs : successor? x t with

A functional predecessor exists exactly when some tree key is smaller.

theorem predecessor?_isSome_iff_exists_less {x : Nat} {t : BSTree} (ht : Ordered t) : (predecessor? x t).isSome ↔ ∃ y, InTree y t ∧ y < x := cases hp : predecessor? x t with cases hp : predecessor? x t with

Functional deletion correctness

A node is never the empty tree.

theorem node_ne_empty (left : BSTree) (key : Nat) (right : BSTree) : node left key right ≠ empty :=

On nonempty trees, the total minKey agrees with minimum?.

theorem minimum?_eq_some_minKey {t : BSTree} (h : t ≠ empty) : minimum? t = some (minKey t) := induction t with cases left with

The total minimum key of a nonempty tree occurs in that tree.

theorem minKey_inTree {t : BSTree} (h : t ≠ empty) : InTree (minKey t) t :=

On an ordered tree, minKey is a lower bound for all members.

theorem minKey_le_of_ordered {t : BSTree} (ht : Ordered t) : ∀ y, InTree y t → minKey t ≤ y :=

Deleting the minimum key removes exactly that key from an ordered tree. The empty-tree case is harmless because membership is false.

theorem inTree_deleteMin_iff {y : Nat} {t : BSTree} (ht : Ordered t) : InTree y (deleteMin t) ↔ InTree y t ∧ y ≠ minKey t := induction t generalizing y with cases left with

Deleting the minimum key preserves the BST ordering invariant.

Deleting a root removes exactly the old root key from an ordered node.

theorem inTree_deleteRoot_iff {y : Nat} {left right : BSTree} {key : Nat} (ht : Ordered (node left key right)) : InTree y (deleteRoot (node left key right)) ↔ InTree y (node left key right) ∧ y ≠ key := cases right with

Deleting a root preserves the BST ordering invariant.

Functional deletion removes exactly the requested key from an ordered tree.

Functional deletion preserves the binary-search-tree ordering invariant.

The key requested for functional deletion is absent afterward.

theorem not_inTree_delete_self {x : Nat} {t : BSTree} (ht : Ordered t) : ¬ InTree x (delete x t) :=

Keys different from the deleted key are preserved by functional deletion.

theorem inTree_delete_of_ne {x y : Nat} {t : BSTree} (ht : Ordered t) (hy : InTree y t) (hyne : y ≠ x) : InTree y (delete x t) :=

Every key present after functional deletion was already present before it.

theorem inTree_of_inTree_delete {x y : Nat} {t : BSTree} (ht : Ordered t) (hy : InTree y (delete x t)) : InTree y t :=

Deleting a missing key leaves an ordered functional BST unchanged.

Searching for a deleted key in the resulting ordered tree returns false.

theorem search_delete_self_eq_false {x : Nat} {t : BSTree} (ht : Ordered t) : search x (delete x t) = false := cases hsearch : search x (delete x t) with

Searching after deletion succeeds exactly for old keys different from the deleted key.

theorem search_delete_eq_true_iff {x y : Nat} {t : BSTree} (ht : Ordered t) : search y (delete x t) = true ↔ search y t = true ∧ y ≠ x :=

Successor after deletion is the least old key above the query except the deleted key.

theorem successor?_delete_eq_some_iff {x q s : Nat} {t : BSTree} (ht : Ordered t) : successor? q (delete x t) = some s ↔ InTree s t ∧ s ≠ x ∧ q < s ∧ ∀ y, InTree y t → y ≠ x → q < y → s ≤ y := exact ⟨ hsOld, hsNe, hqs, ⟩

No successor remains after deletion exactly when every remaining old key is below the query.

theorem successor?_delete_eq_none_iff {x q : Nat} {t : BSTree} (ht : Ordered t) : successor? q (delete x t) = none ↔ ∀ y, InTree y t → y ≠ x → y ≤ q :=

Predecessor after deletion is the greatest old key below the query except the deleted key.

theorem predecessor?_delete_eq_some_iff {x q p : Nat} {t : BSTree} (ht : Ordered t) : predecessor? q (delete x t) = some p ↔ InTree p t ∧ p ≠ x ∧ p < q ∧ ∀ y, InTree y t → y ≠ x → y < q → y ≤ p := exact ⟨ hpOld, hpNe, hpq, ⟩

No predecessor remains after deletion exactly when every remaining old key is above the query.

theorem predecessor?_delete_eq_none_iff {x q : Nat} {t : BSTree} (ht : Ordered t) : predecessor? q (delete x t) = none ↔ ∀ y, InTree y t → y ≠ x → q ≤ y :=

Membership after insertion

Insertion adds exactly the inserted key to the tree membership relation.

The inserted key is a member of the resulting tree.

theorem inTree_insert_self (x : Nat) (t : BSTree) : InTree x (insert x t) :=

Existing members remain members after insertion.

theorem inTree_insert_of_inTree {x y : Nat} {t : BSTree} (h : InTree y t) : InTree y (insert x t) :=

Ordering after insertion

Insertion preserves an upper-bound invariant when the inserted key satisfies it.

theorem allLt_insert {x bound : Nat} {t : BSTree} (hx : x < bound) (ht : AllLt bound t) : AllLt bound (insert x t) :=

Insertion preserves a lower-bound invariant when the inserted key satisfies it.

theorem allGt_insert {x bound : Nat} {t : BSTree} (hx : bound < x) (ht : AllGt bound t) : AllGt bound (insert x t) :=

Functional BST insertion preserves the binary-search-tree ordering invariant.

theorem insert_ordered {x : Nat} {t : BSTree} (ht : Ordered t) : Ordered (insert x t) := induction t with

Searching after insertion succeeds exactly for the inserted key or an old key.

end BSTreeend Chapter12end CLRS