Chapter 12 - Binary Search Trees

Chapter 12 studies binary search trees and the operations that preserve their ordering invariant. The current CLRS-Lean pass uses an inductive tree of natural keys and proves search, minimum/maximum, insertion, functional successor/predecessor, and functional deletion correctness for membership and ordering. A zipper refinement represents the path to the current node as a functional parent-pointer context and proves iterative search, subtree transplant, deletion through that transplant interface, and parent-ascent successor/predecessor equivalent to the established functional operations.

Sections

• 12.1 Binary search trees: partial, with the functional BST theorem and zipper-based parent-navigation boundaries complete for the current inductive-tree model. Main results: CLRS.Chapter12.BSTree.search_eq_true_iff, CLRS.Chapter12.BSTree.minimum?_le_of_ordered, CLRS.Chapter12.BSTree.le_maximum?_of_ordered, CLRS.Chapter12.BSTree.successor?_least_greater, CLRS.Chapter12.BSTree.successor?_eq_some_iff, CLRS.Chapter12.BSTree.successor?_eq_none_iff, CLRS.Chapter12.BSTree.successor?_isSome_iff_exists_greater, CLRS.Chapter12.BSTree.predecessor?_greatest_less, CLRS.Chapter12.BSTree.predecessor?_eq_some_iff, CLRS.Chapter12.BSTree.predecessor?_eq_none_iff, CLRS.Chapter12.BSTree.predecessor?_isSome_iff_exists_less, CLRS.Chapter12.BSTree.inTree_insert_iff, CLRS.Chapter12.BSTree.search_insert_eq_true_iff, CLRS.Chapter12.BSTree.insert_ordered, CLRS.Chapter12.BSTree.inTree_delete_iff, CLRS.Chapter12.BSTree.not_inTree_delete_self, CLRS.Chapter12.BSTree.delete_eq_self_of_not_inTree, CLRS.Chapter12.BSTree.search_delete_self_eq_false, CLRS.Chapter12.BSTree.search_delete_eq_true_iff, CLRS.Chapter12.BSTree.successor?_delete_eq_some_iff, CLRS.Chapter12.BSTree.successor?_delete_eq_none_iff, CLRS.Chapter12.BSTree.predecessor?_delete_eq_some_iff, CLRS.Chapter12.BSTree.predecessor?_delete_eq_none_iff, CLRS.Chapter12.BSTree.delete_ordered, CLRS.Chapter12.BSTree.searchZipper_toTree, CLRS.Chapter12.BSTree.searchIter_eq_search, CLRS.Chapter12.BSTree.transplant_preserves_ordered, CLRS.Chapter12.BSTree.deleteViaTransplant_eq_delete, CLRS.Chapter12.BSTree.successorZipper_eq_successor?, CLRS.Chapter12.BSTree.predecessorZipper_eq_predecessor?, CLRS.Chapter12.BSTree.RepresentsW.tree_unique, CLRS.Chapter12.BSTree.transplantChild_left_representsW, CLRS.Chapter12.BSTree.transplantChild_right_representsW, CLRS.Chapter12.BSTree.transplantChild_left_refines_transplant, CLRS.Chapter12.BSTree.transplantChild_right_refines_transplant, and CLRS.Chapter12.BSTree.insertPointer_right_representsW.

The running-time / cost layer adds the tree height and branch-faithful cost functions with their O(h) bounds (searchCost_le_height, minimumCost_le_height, maximumCost_le_height, successorCost_le_height, predecessorCost_le_height, insertCost_le_height, minKeyCost_le_height, deleteMinCost_le_height, deleteRootCost_le, deleteCost_le), and the randomly-built-BST ancestor characterization CLRS.Chapter12.BSTree.isAncestorOf_iff_firstInInterval (CLRS Lemma 12.3).

Current Gaps

The zipper layer formalizes parent-oriented navigation and subtree replacement without changing the inductive tree representation. Building on it, an imperative pointer-heap layer models nodes as records with mutable left/right/parent cells over a Std.HashMap store, and proves that in-place TRANSPLANT and leaf TREE-INSERT refine the functional subtree-replacement specification through the RepresentsW heap-to-tree abstraction. An explicit RAM-cost model connecting these pointer operations to concrete running times remains future work, as does the probability P(i is an ancestor of j) = 1/(|i-j|+1) and the O(log n) expected-depth bound of a randomly built BST.