English
O(n). Split the elements of a tree into those satisfying a predicate p and those that do not satisfy p. The resulting pair consists of two trees: the first contains all elements with p true, the second contains those with p false.
Русский
O(n). Разбить элементы дерева на те, которые удовлетворяют предикату p, и те, которые не удовлетворяют его. Результат — пара деревьев: первое содержит элементы с p истинно, второе — остальные.
LaTeX
$$$$ \mathrm{partition}: (p: \alpha \to \mathrm{Prop}) \to \mathrm Ordnode\; \alpha \to (Ordnode\; \alpha) \times (Ordnode\; \alpha), \\ \mathrm{partition}(p)(\mathrm nil)=(nil, nil), \\ \mathrm{partition}(p)(\mathrm node\; _\; l\; x\; r) = \begin{cases} (\mathrm{link}\; l_1\; x\; r_1, \mathrm{merge}\; l_2\; r_2) & \text{if } p(x) \\ (\mathrm{merge}\; l_1\; r_1, \mathrm{link}\; l_2\; x\; r_2) & \text{otherwise} \end{cases} $$$$
Lean4
/-- O(n). Split the elements of a tree into those satisfying, and not satisfying, a predicate.
partition (fun x ↦ x < 3) {1, 2, 4} = ({1, 2}, {3}) -/
def partition (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α × Ordnode α
| nil => (nil, nil)
| node _ l x r =>
let (l₁, l₂) := partition p l
let (r₁, r₂) := partition p r
if p x then (link l₁ x r₁, merge l₂ r₂) else (merge l₁ r₁, link l₂ x r₂)
