English
O(log n). Split a set into those elements satisfying, and not satisfying, a predicate p, where p is antitone (if x<y and p(y) then p(x)).
Русский
O(log n). Разделить множество на элементы, удовлетворяющие и не удовлетворяющие предикату p, где p антотонен (если x<y и p(y), то p(x)).
LaTeX
$$$$ \\mathrm{span}: (p: \\alpha \\to \\mathrm{Prop}) \\to [\\mathrm{DecidablePred}\ p] \\to \\ Ordnode\\; \\alpha \\to \\ Ordnode\\; \\alpha \\times \\ Ordnode\\; \\alpha, \\quad \\text{определение по рекурсии:} $$$
Lean4
/-- O(log n). Split the set into those satisfying and not satisfying the predicate `p`.
`p` is required to be antitone, that is, `x < y → p y → p x`.
span (fun x ↦ x < 4) {1, 2, 3, 4, 5} = ({1, 2, 3}, {4, 5})
span (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation -/
def span (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α × Ordnode α
| nil => (nil, nil)
| node _ l x r =>
if p x then
let (r₁, r₂) := span p r
(link l x r₁, r₂)
else
let (l₁, l₂) := span p l
(l₁, link l₂ x r)
