English
O(log n). Split a tree at x into three parts: the left part with elements < x, an optional element equal to x, and the right part with elements > x.
Русский
O(log n). Разделить дерево по x на три части: элементы < x слева, возможный элемент = x, и элементы > x справа.
LaTeX
$$$$ \mathrm{split3}: (x: \alpha) \to \ Ordnode\; \alpha \to \ Ordnode\; \alpha \times \mathrm{Option}\; \alpha \times \ Ordnode\; \alpha, \quad \text{определение по рекурсии} $$$$
Lean4
/-- O(log n). Split the tree into those smaller than `x` and those greater than it.
If an element equivalent to `x` is in the set, it is discarded.
split 2 {1, 2, 4} = ({1}, {4})
split 3 {1, 2, 4} = ({1, 2}, {4})
split 4 {1, 2, 4} = ({1, 2}, ∅)
Using a preorder on `ℕ × ℕ` that only compares the first coordinate:
split (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, ∅)
split (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, ∅) -/
def split (x : α) : Ordnode α → Ordnode α × Ordnode α
| nil => (nil, nil)
| node _ l y r =>
match cmpLE x y with
| Ordering.lt =>
let (lt, gt) := split x l
(lt, link gt y r)
| Ordering.eq => (l, r)
| Ordering.gt =>
let (lt, gt) := split x r
(link l y lt, gt)
