Deletion from unbalanced binary search trees

Deletion follows the search path to the key. A matching node with an empty right subtree is replaced by its left subtree; otherwise its key is replaced by the leftmost key of the right subtree, which is detached from there. This is the successor-splicing deletion of Cormen et al., Chapter 12, except that a node with an empty left subtree is also rebuilt around its successor rather than replaced by its right subtree. Deleting an absent key leaves the tree unchanged.

Main definitions

• splitMin: detach the leftmost key of a nonempty tree.
• glue: join the two subtrees of a deleted node.
• erase: delete a key.
• eraseVisits: internal-node visits of deletion, in the model of the companion cost module.

Main results

• elements_erase, ordered_erase: deletion has set semantics and preserves the invariant.
• erase_eq_of_notMem: deleting an absent key preserves the entire tree.
• searchVisits_le_eraseVisits: deletion walks the search path of contains and insert, and then at most the left spine of the matched node's right subtree (minimumVisits).
• eraseVisits_le_height, height_erase_le: deletion visits at most the initial height and never increases the height.

References

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

def Cslib.Algorithms.Lean.SearchTree.splitMin {α : Type u_1} (a : α) : BinaryTree α → BinaryTree α → α × BinaryTree α

Detach the leftmost key of the nonempty tree .node a l r, returning it with the rest.

def Cslib.Algorithms.Lean.SearchTree.glue {α : Type u_1} (l : BinaryTree α) : BinaryTree α → BinaryTree α

Join the subtrees of a deleted node, promoting the leftmost key of the right subtree.

theorem Cslib.Algorithms.Lean.SearchTree.height_splitMin_le {α : Type u_1} (a : α) (l r : BinaryTree α) : (splitMin a l r).2.height ≤ (BinaryTree.node a l r).height

theorem Cslib.Algorithms.Lean.SearchTree.height_glue_le {α : Type u_1} (a : α) (l r : BinaryTree α) : (glue l r).height ≤ (BinaryTree.node a l r).height

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

Delete x along its search path; a matching node is replaced by glue of its subtrees.

theorem Cslib.Algorithms.Lean.SearchTree.elements_splitMin {α : Type u_1} [LinearOrder α] (a : α) (l r : BinaryTree α) : elements (BinaryTree.node a l r) = Insert.insert (splitMin a l r).1 (elements (splitMin a l r).2)

The detached key together with the remaining tree represents the original set.

theorem Cslib.Algorithms.Lean.SearchTree.elements_glue {α : Type u_1} [LinearOrder α] (l r : BinaryTree α) : elements (glue l r) = elements l ∪ elements r

Gluing loses only the key of the deleted node.

theorem Cslib.Algorithms.Lean.SearchTree.ordered_splitMin {α : Type u_1} [LinearOrder α] {a : α} {l r : BinaryTree α} (ht : Ordered (BinaryTree.node a l r)) : Ordered (splitMin a l r).2 ∧ ∀ y ∈ elements (splitMin a l r).2, (splitMin a l r).1 < y

In an ordered tree the detached key is the least, and the remaining tree stays ordered.

theorem Cslib.Algorithms.Lean.SearchTree.ordered_glue {α : Type u_1} [LinearOrder α] {a : α} {l r : BinaryTree α} (ht : Ordered (BinaryTree.node a l r)) : Ordered (glue l r)

Gluing the subtrees of an ordered node yields an ordered tree.

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

Deletion removes exactly the requested key, even when it was absent.

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

The binary-search-tree invariant survives deletion.

theorem Cslib.Algorithms.Lean.SearchTree.erase_eq_of_notMem {α : Type u_1} [LinearOrder α] {t : BinaryTree α} {x : α} (hx : x ∉ elements t) : erase x t = t

Deleting an absent key preserves the entire tree, not just its represented set.

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

Internal-node visits of deletion: the search path, then leftmost descent in the right subtree of a matching node.

theorem Cslib.Algorithms.Lean.SearchTree.searchVisits_le_eraseVisits {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : searchVisits x t ≤ eraseVisits x t

Deletion pays for the full search path and possibly a successor descent on top.

theorem Cslib.Algorithms.Lean.SearchTree.eraseVisits_le_height {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : eraseVisits x t ≤ t.height

theorem Cslib.Algorithms.Lean.SearchTree.height_erase_le {α : Type u_1} [LinearOrder α] (x : α) (t : BinaryTree α) : (erase x t).height ≤ t.height

Unlike insertion, deletion never increases the height.