Repository navigation
feat(search-tree): verified deletion for unbalanced binary search trees #359
Description
Scope
ROADMAP.md (stateful algorithms prototype) lists deletion for the
unbalanced binary search tree as open.
Add the textbook deletion algorithm [CLRS2009, Chapter 12] to the pure search-tree layer:
popMin: detach the leftmost key of a nonempty tree;erase: delete a key, replacing a
two-child (or right-child) node by its successor from the right subtree.- Semantics:
elements_erase(elements (erase x t) = (elements t).erase xfor orderedt),
ordered_erase, anderase_eq_self(absent keys leave the tree unchanged). - Costs in the existing node-visit model:
eraseVisitswitheraseVisits_le_height, and
height_erase_le(deletion never increases height). - Checked examples in
ComplexityTests/SearchTree.lean; ROADMAP/paper update.
Out of scope
Extending the shared Cslib.OrderedSet stateful interface with deletion (this would also affect
other realizations), balancing, RAM representations. These stay recorded in the roadmap.
Completion criteria
scripts/check.sh passes; independent review; PR linked here.
Activity
chris-ai1 commentedon Oct 22, 2026
Agent/session:
worker-crei-dc679113(Claude Code, acting for Christian Reitwiessner)Role: worker
State:
activeBranch:
feat/search-tree-eraseon forkchris-ai1/complexitylibScope: as in the issue description (pure
erase/popMin, set semantics, invariant preservation, node-visit and height bounds, tests, docs).Next step: implement in
Complexity/Algorithms/Lean/SearchTree/{Basic,Cost}.lean.chris-ai1 commentedon Oct 22, 2026
Status:
active— agent/sessionworker-crei-dc679113chris-ai1has read-only access); this comment and the claim above record ownership.Complexity/Algorithms/Lean/SearchTree/Erase.lean(splitMin,glue,erase,elements_erase,ordered_erase,erase_eq_self,eraseVisits_le_height,height_erase_le),ComplexityTests/SearchTreeErase.lean, ROADMAP/UPSTREAM updates. Commitf4b5694aonchris-ai1:feat/search-tree-erase.scripts/check.sh— all six gates ok.chris-ai1 commentedon Oct 22, 2026
Status:
awaiting review— agent/sessionworker-crei-dc679113820d9446, branchchris-ai1:feat/search-tree-erase)scripts/check.shok atf4b5694a; targeted builds after; CI pending.SamuelSchlesinger commentedon Oct 30, 2026
The previously out-of-scope shared-interface follow-up has landed in #1756: total erase and adaptive minimum extraction now reuse the representation-independent semantics and node-visit certificates. Integration and validation record.
This preserves the pure-deletion milestone completed here. Balancing and heap/RAM representations remain open in ROADMAP; allocation, comparison implementation and pure client computation are still excluded from these node-visit bounds. Agent coordination by
codex-ordered-set-integrate-20261030.