English
An auxiliary drop function removes the i-th element in-order from an ordered tree, with explicit behavior depending on the position relative to the left subtree size.
Русский
Вспомогательная функция dropAux удаляет i-й элемент слева направо в упорядоченном дереве, поведение зависит от позиции относительно размера левого поддерева.
LaTeX
$$$\\text{dropAux} : \\mathrm{Ordnode}\\,\\alpha \\to \\mathbb{N} \\to \\mathrm{Ordnode}\\,\\alpha\\quad;\\quad\n\\begin{cases} \\text{dropAux}({\\rm nil}, i) = {\\rm nil}, \\\\ \\\\ \\\\ \\text{dropAux}(\\mathrm{node}\\ sz\\ L\\ x\\ R, i) = \\begin{cases} \\mathrm{node}\\ sz\\ L\\ x\\ R, & i=0, \\\\ \\quad \\text{if } i=0 \\\\ \\text{link}(\\text{dropAux}(L,i))\\ x\\ R, & \\text{none} = \\mathrm{Nat.psub}'(i,|L|), \\\\ \\text{insertMin } x \\ R, & \\mathrm{some}\\ 0 = \\mathrm{Nat.psub}'(i,|L|), \\\\ \\text{dropAux}(R, j), & \\mathrm{some}(j+1) = \\mathrm{Nat.psub}'(i,|L|) \end{cases} \end{cases}$$$
Lean4
/-- Auxiliary definition for `drop`. (Can also be used in lieu of `drop` if you know the
index is within the range of the data structure.)
drop_aux {a, b, c, d} 2 = {c, d}
drop_aux {a, b, c, d} 5 = ∅ -/
def dropAux : Ordnode α → ℕ → Ordnode α
| nil, _ => nil
| t@(node _ l x r), i =>
if i = 0 then t
else
match Nat.psub' i (size l) with
| none => link (dropAux l i) x r
| some 0 => insertMin x r
| some (j + 1) => dropAux r j
