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. It now also exposes reader-facing wrappers for successor/predecessor existence, Boolean search after insertion/deletion, and successor/predecessor queries after deletion.

Sections

• 12.1 Binary search trees: partial, with the functional BST theorem boundary 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.

Current Gaps

Functional successor/predecessor queries and functional deletion are formalized. Parent-pointer successor/predecessor procedures, transplant, and pointer-level mutation are not yet formalized. The pointer-transplant algorithm from CLRS needs an imperative tree model or a refinement from the functional deletion theorem.