Ordered sets #
This file defines a data structure for ordered sets, supporting a variety of useful operations including insertion and deletion, logarithmic time lookup, set operations, folds, and conversion from lists.
The Ordnode α
operations all assume that α
has the structure of
a total preorder, meaning a ≤
operation that is
- Transitive:
x ≤ y → y ≤ z → x ≤ z
- Reflexive:
x ≤ x
- Total:
x ≤ y ∨ y ≤ x
For example, in order to use this data structure as a map type, one
can store pairs (k, v)
where (k, v) ≤ (k', v')
is defined to mean
k ≤ k'
(assuming that the key values are linearly ordered).
Two values x,y
are equivalent if x ≤ y
and y ≤ x
. An Ordnode α
maintains the invariant that it never stores two equivalent nodes;
the insertion operation comes with two variants depending on whether
you want to keep the old value or the new value in case you insert a value
that is equivalent to one in the set.
The operations in this file are not verified, in the sense that they provide
"raw operations" that work for programming purposes but the invariants
are not explicitly in the structure. See Ordset
for a verified version
of this data structure.
Main definitions #
Ordnode α
: A set of values of typeα
Implementation notes #
Based on weight balanced trees:
- Stephen Adams, "Efficient sets: a balancing act", Journal of Functional Programming 3(4):553-562, October 1993, http://www.swiss.ai.mit.edu/~adams/BB/.
- J. Nievergelt and E.M. Reingold, "Binary search trees of bounded balance", SIAM journal of computing 2(1), March 1973.
Ported from Haskell's Data.Set
.
Tags #
ordered map, ordered set, data structure
An Ordnode α
is a finite set of values, represented as a tree.
The operations on this type maintain that the tree is balanced
and correctly stores subtree sizes at each level.
Equations
- Ordnode.instEmptyCollection = { emptyCollection := Ordnode.nil }
Equations
- Ordnode.instInhabited = { default := Ordnode.nil }
Internal use only
The maximal relative difference between the sizes of
two trees, it corresponds with the w
in Adams' paper.
According to the Haskell comment, only (delta, ratio)
settings
of (3, 2)
and (4, 2)
will work, and the proofs in
Ordset.lean
assume delta := 3
and ratio := 2
.
Equations
Internal use only
The ratio between an outer and inner sibling of the
heavier subtree in an unbalanced setting. It determines
whether a double or single rotation should be performed
to restore balance. It is corresponds with the inverse
of α
in Adam's article.
Equations
O(1). Construct a singleton set containing value a
.
singleton 3 = {3}
Equations
Equations
- Ordnode.instSingleton = { singleton := Ordnode.singleton }
O(1). Get the size of the set.
size {2, 1, 1, 4} = 3
Equations
- Ordnode.nil.size = 0
- (Ordnode.node sz l x_1 r).size = sz
O(1). Is the set empty?
empty ∅ = tt empty {1, 2, 3} = ff
Equations
- Ordnode.nil.empty = true
- (Ordnode.node sz l x_1 r).empty = false
Internal use only, because it violates the BST property on the original order.
O(n). The dual of a tree is a tree with its left and right sides reversed throughout. The dual of a valid BST is valid under the dual order. This is convenient for exploiting symmetries in the algorithms.
Equations
- Ordnode.nil.dual = Ordnode.nil
- (Ordnode.node sz l x_1 r).dual = Ordnode.node sz r.dual x_1 l.dual
Basic pretty printing for Ordnode α
that shows the structure of the tree.
repr {3, 1, 2, 4} = ((∅ 1 ∅) 2 ((∅ 3 ∅) 4 ∅))
Equations
- Ordnode.nil.repr n = Std.Format.text "∅"
- (Ordnode.node sz l x_1 r).repr n = (Std.Format.joinSep [l.repr n, reprPrec x_1 n, r.repr n] (Std.Format.text " ")).paren
Equations
- Ordnode.instRepr = { reprPrec := Ordnode.repr }
O(n). Does every element of the map satisfy property P
?
All (fun x ↦ x < 5) {1, 2, 3} = True All (fun x ↦ x < 5) {1, 2, 3, 5} = False
Equations
- Ordnode.All P Ordnode.nil = True
- Ordnode.All P (Ordnode.node sz l x_1 r) = (Ordnode.All P l ∧ P x_1 ∧ Ordnode.All P r)
Equations
- Ordnode.All.decidable Ordnode.nil = isTrue trivial
- Ordnode.All.decidable (Ordnode.node sz l x_1 r) = inferInstanceAs (Decidable (Ordnode.All P l ∧ P x_1 ∧ Ordnode.All P r))
O(n). Does any element of the map satisfy property P
?
Any (fun x ↦ x < 2) {1, 2, 3} = True Any (fun x ↦ x < 2) {2, 3, 5} = False
Equations
- Ordnode.Any P Ordnode.nil = False
- Ordnode.Any P (Ordnode.node sz l x_1 r) = (Ordnode.Any P l ∨ P x_1 ∨ Ordnode.Any P r)
Equations
- Ordnode.Any.decidable Ordnode.nil = isFalse ⋯
- Ordnode.Any.decidable (Ordnode.node sz l x_1 r) = inferInstanceAs (Decidable (Ordnode.Any P l ∨ P x_1 ∨ Ordnode.Any P r))
O(n). Exact membership in the set. This is useful primarily for stating
correctness properties; use ∈
for a version that actually uses the BST property
of the tree.
Emem 2 {1, 2, 3} = true
Emem 4 {1, 2, 3} = false
Equations
- Ordnode.Emem x = Ordnode.Any (Eq x)
Equations
O(n). Approximate membership in the set, that is, whether some element in the
set is equivalent to this one in the preorder. This is useful primarily for stating
correctness properties; use ∈
for a version that actually uses the BST property
of the tree.
Amem 2 {1, 2, 3} = true
Amem 4 {1, 2, 3} = false
To see the difference with Emem
, we need a preorder that is not a partial order.
For example, suppose we compare pairs of numbers using only their first coordinate. Then:
-- Porting note: Verify below example
emem (0, 1) {(0, 0), (1, 2)} = false
amem (0, 1) {(0, 0), (1, 2)} = true
(0, 1) ∈ {(0, 0), (1, 2)} = true
The ∈
relation is equivalent to Amem
as long as the Ordnode
is well formed,
and should always be used instead of Amem
.
Equations
- Ordnode.Amem x = Ordnode.Any fun (y : α) => x ≤ y ∧ y ≤ x
Equations
O(log n). Return the minimum element of the tree, or the provided default value.
findMin' 37 {1, 2, 3} = 1 findMin' 37 ∅ = 37
Equations
- Ordnode.nil.findMin' x✝ = x✝
- (Ordnode.node size l x_2 r).findMin' x✝ = l.findMin' x_2
O(log n). Return the minimum element of the tree, if it exists.
findMin {1, 2, 3} = some 1 findMin ∅ = none
Equations
- Ordnode.nil.findMin = none
- (Ordnode.node sz l x_1 r).findMin = some (l.findMin' x_1)
O(log n). Return the maximum element of the tree, or the provided default value.
findMax' 37 {1, 2, 3} = 3 findMax' 37 ∅ = 37
Equations
- Ordnode.findMax' x✝ Ordnode.nil = x✝
- Ordnode.findMax' x✝ (Ordnode.node size l x_3 r) = Ordnode.findMax' x_3 r
O(log n). Return the maximum element of the tree, if it exists.
findMax {1, 2, 3} = some 3 findMax ∅ = none
Equations
- Ordnode.nil.findMax = none
- (Ordnode.node sz l x_1 r).findMax = some (Ordnode.findMax' x_1 r)
O(log n). Remove the minimum element from the tree, or do nothing if it is already empty.
eraseMin {1, 2, 3} = {2, 3} eraseMin ∅ = ∅
Equations
- Ordnode.nil.eraseMin = Ordnode.nil
- (Ordnode.node size Ordnode.nil x_1 r).eraseMin = r
- (Ordnode.node size (Ordnode.node sz l' y r') x_1 r).eraseMin = (Ordnode.node sz l' y r').eraseMin.balanceR x_1 r
O(log n). Remove the maximum element from the tree, or do nothing if it is already empty.
eraseMax {1, 2, 3} = {1, 2} eraseMax ∅ = ∅
Equations
- Ordnode.nil.eraseMax = Ordnode.nil
- (Ordnode.node size l x_1 Ordnode.nil).eraseMax = l
- (Ordnode.node size l x_1 (Ordnode.node sz l' y r')).eraseMax = l.balanceL x_1 (Ordnode.node sz l' y r').eraseMax
Internal use only, because it requires a balancing constraint on the inputs.
O(log n). Extract and remove the minimum element from a nonempty tree.
O(log n). Extract and remove the minimum element from the tree, if it exists.
split_min {1, 2, 3} = some (1, {2, 3}) split_min ∅ = none
Equations
- Ordnode.nil.splitMin = none
- (Ordnode.node sz l x_1 r).splitMin = some (l.splitMin' x_1 r)
Internal use only, because it requires a balancing constraint on the inputs.
O(log n). Extract and remove the maximum element from a nonempty tree.
O(log n). Extract and remove the maximum element from the tree, if it exists.
split_max {1, 2, 3} = some ({1, 2}, 3) split_max ∅ = none
Equations
- Ordnode.nil.splitMax = none
- (Ordnode.node sz l x_1 r).splitMax = some (l.splitMax' x_1 r)
Internal use only
O(log(m + n)). Concatenate two trees that are balanced and ordered with respect to each other.
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.nil.glue x✝ = x✝
- (Ordnode.node size l x_2 r).glue Ordnode.nil = Ordnode.node size l x_2 r
O(log(m + n)). Concatenate two trees that are ordered with respect to each other.
merge {1, 2} {3, 4} = {1, 2, 3, 4} merge {3, 4} {1, 2} = precondition violation
Equations
- One or more equations did not get rendered due to their size.
O(log n). Insert an element above all the others, without any comparisons. (Assumes that the element is in fact above all the others).
insertMax {1, 2} 4 = {1, 2, 4}
insertMax {1, 2} 0 = precondition violation
Equations
- Ordnode.nil.insertMax x✝ = Ordnode.singleton x✝
- (Ordnode.node size l x_2 r).insertMax x✝ = l.balanceR x_2 (r.insertMax x✝)
O(log n). Insert an element below all the others, without any comparisons. (Assumes that the element is in fact below all the others).
insertMin {1, 2} 0 = {0, 1, 2}
insertMin {1, 2} 4 = precondition violation
Equations
- Ordnode.insertMin x Ordnode.nil = Ordnode.singleton x
- Ordnode.insertMin x (Ordnode.node sz l x_2 r) = (Ordnode.insertMin x l).balanceR x_2 r
O(log(m+n)). Build a tree from an element between two trees, without any assumption on the relative sizes.
link {1, 2} 4 {5, 6} = {1, 2, 4, 5, 6}
link {1, 3} 2 {5} = precondition violation
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.nil.link x = Ordnode.insertMin x
O(n). Filter the elements of a tree satisfying a predicate.
filter (fun x ↦ x < 3) {1, 2, 4} = {1, 2} filter (fun x ↦ x > 5) {1, 2, 4} = ∅
Equations
- Ordnode.filter p Ordnode.nil = Ordnode.nil
- Ordnode.filter p (Ordnode.node sz l x_1 r) = if p x_1 then (Ordnode.filter p l).link x_1 (Ordnode.filter p r) else (Ordnode.filter p l).merge (Ordnode.filter p r)
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})
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.partition p Ordnode.nil = (Ordnode.nil, Ordnode.nil)
O(n). Map a function across a tree, without changing the structure. Only valid when
the function is strictly monotone, i.e. x < y → f x < f y
.
partition (fun x ↦ x + 2) {1, 2, 4} = {2, 3, 6}
partition (fun x : ℕ ↦ x - 2) {1, 2, 4} = precondition violation
Equations
- Ordnode.map f Ordnode.nil = Ordnode.nil
- Ordnode.map f (Ordnode.node sz l x_1 r) = Ordnode.node sz (Ordnode.map f l) (f x_1) (Ordnode.map f r)
O(n). Fold a function across the structure of a tree.
fold z f {1, 2, 4} = f (f z 1 z) 2 (f z 4 z)
The exact structure of function applications depends on the tree and so is unspecified.
Equations
- Ordnode.fold z f Ordnode.nil = z
- Ordnode.fold z f (Ordnode.node sz l x_1 r) = f (Ordnode.fold z f l) x_1 (Ordnode.fold z f r)
O(n). Fold a function from left to right (in increasing order) across the tree.
foldl f z {1, 2, 4} = f (f (f z 1) 2) 4
Equations
- Ordnode.foldl f x✝ Ordnode.nil = x✝
- Ordnode.foldl f x✝ (Ordnode.node size l x_2 r) = Ordnode.foldl f (f (Ordnode.foldl f x✝ l) x_2) r
O(n). Fold a function from right to left (in decreasing order) across the tree.
foldr f {1, 2, 4} z = f 1 (f 2 (f 4 z))
Equations
- Ordnode.foldr f Ordnode.nil x✝ = x✝
- Ordnode.foldr f (Ordnode.node size l x_2 r) x✝ = Ordnode.foldr f l (f x_2 (Ordnode.foldr f r x✝))
Equations
- Ordnode.instToString = { toString := fun (t : Ordnode α) => "{" ++ ", ".intercalate (List.map toString t.toList) ++ "}" }
Equations
- Ordnode.instToFormat = { format := fun (t : Ordnode α) => Std.Format.joinSep (List.map Std.format t.toList) (Std.Format.text ", ") }
O(m * n). The cartesian product of two sets: (a, b) ∈ s.prod t
iff a ∈ s
and b ∈ t
.
prod {1, 2} {2, 3} = {(1, 2), (1, 3), (2, 2), (2, 3)}
Equations
- t₁.prod t₂ = Ordnode.fold Ordnode.nil (fun (s₁ : Ordnode (α × β)) (a : α) (s₂ : Ordnode (α × β)) => s₁.merge ((Ordnode.map (Prod.mk a) t₂).merge s₂)) t₁
O(n). Map a partial function across a set. The result depends on a proof that the function is defined on all members of the set.
pmap (fin.mk : ∀ n, n < 4 → fin 4) {1, 2} H = {(1 : fin 4), (2 : fin 4)}
Equations
- Ordnode.pmap f Ordnode.nil x_2 = Ordnode.nil
- Ordnode.pmap f (Ordnode.node s l x_2 r) ⋯ = Ordnode.node s (Ordnode.pmap f l hl) (f x_2 hx) (Ordnode.pmap f r hr)
O(log n). Get the i
th element of the set, by its index from left to right.
nth {a, b, c, d} 2 = some c nth {a, b, c, d} 5 = none
O(log n). Remove the i
th element of the set, by its index from left to right.
remove_nth {a, b, c, d} 2 = {a, b, d} remove_nth {a, b, c, d} 5 = {a, b, c, d}
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 = ∅
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.nil.dropAux x✝ = Ordnode.nil
O(log n). Remove the first i
elements of the set, counted from the left.
drop 2 {a, b, c, d} = {c, d} drop 5 {a, b, c, d} = ∅
Equations
- Ordnode.drop i t = if t.size ≤ i then Ordnode.nil else t.dropAux i
Auxiliary definition for splitAt
. (Can also be used in lieu of splitAt
if you know the
index is within the range of the data structure.)
splitAtAux {a, b, c, d} 2 = ({a, b}, {c, d})
splitAtAux {a, b, c, d} 5 = ({a, b, c, d}, ∅)
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.nil.splitAtAux x✝ = (Ordnode.nil, Ordnode.nil)
O(log n). Split a set at the i
th element, getting the first i
and everything else.
splitAt 2 {a, b, c, d} = ({a, b}, {c, d}) splitAt 5 {a, b, c, d} = ({a, b, c, d}, ∅)
Equations
- Ordnode.splitAt i t = if t.size ≤ i then (t, Ordnode.nil) else t.splitAtAux i
O(log n). Get an initial segment of the set that satisfies the predicate p
.
p
is required to be antitone, that is, x < y → p y → p x
.
takeWhile (fun x ↦ x < 4) {1, 2, 3, 4, 5} = {1, 2, 3}
takeWhile (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation
Equations
- Ordnode.takeWhile p Ordnode.nil = Ordnode.nil
- Ordnode.takeWhile p (Ordnode.node sz l x_1 r) = if p x_1 then l.link x_1 (Ordnode.takeWhile p r) else Ordnode.takeWhile p l
O(log n). Remove an initial segment of the set that satisfies the predicate p
.
p
is required to be antitone, that is, x < y → p y → p x
.
dropWhile (fun x ↦ x < 4) {1, 2, 3, 4, 5} = {4, 5}
dropWhile (fun x ↦ x > 4) {1, 2, 3, 4, 5} = precondition violation
Equations
- Ordnode.dropWhile p Ordnode.nil = Ordnode.nil
- Ordnode.dropWhile p (Ordnode.node sz l x_1 r) = if p x_1 then Ordnode.dropWhile p r else (Ordnode.dropWhile p l).link x_1 r
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
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.span p Ordnode.nil = (Ordnode.nil, Ordnode.nil)
Auxiliary definition for ofAscList
.
Note: This function is defined by well founded recursion, so it will probably not compute
in the kernel, meaning that you probably can't prove things like
ofAscList [1, 2, 3] = {1, 2, 3}
by rfl
.
This implementation is optimized for VM evaluation.
O(n). Build a set from a list which is already sorted. Performs no comparisons.
ofAscList [1, 2, 3] = {1, 2, 3} ofAscList [3, 2, 1] = precondition violation
Equations
- Ordnode.ofAscList [] = Ordnode.nil
- Ordnode.ofAscList (x_1 :: xs) = Ordnode.ofAscListAux₂ xs (Ordnode.singleton x_1) 1
O(log n). Does the set (approximately) contain the element x
? That is,
is there an element that is equivalent to x
in the order?
1 ∈ {1, 2, 3} = true
4 ∈ {1, 2, 3} = false
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
(1, 1) ∈ {(0, 1), (1, 2)} = true
(3, 1) ∈ {(0, 1), (1, 2)} = false
Equations
- Ordnode.mem x Ordnode.nil = false
- Ordnode.mem x (Ordnode.node sz l x_2 r) = match cmpLE x x_2 with | Ordering.lt => Ordnode.mem x l | Ordering.eq => true | Ordering.gt => Ordnode.mem x r
O(log n). Retrieve an element in the set that is equivalent to x
in the order,
if it exists.
find 1 {1, 2, 3} = some 1
find 4 {1, 2, 3} = none
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
find (1, 1) {(0, 1), (1, 2)} = some (1, 2)
find (3, 1) {(0, 1), (1, 2)} = none
Equations
- Ordnode.find x Ordnode.nil = none
- Ordnode.find x (Ordnode.node sz l x_2 r) = match cmpLE x x_2 with | Ordering.lt => Ordnode.find x l | Ordering.eq => some x_2 | Ordering.gt => Ordnode.find x r
Equations
- Ordnode.instMembership = { mem := fun (t : Ordnode α) (x : α) => Ordnode.mem x t = true }
Equations
- Ordnode.mem.decidable x t = (Ordnode.mem x t).decEq true
O(log n). Insert an element into the set, preserving balance and the BST property.
If an equivalent element is already in the set, the function f
is used to generate
the element to insert (being passed the current value in the set).
insertWith f 0 {1, 2, 3} = {0, 1, 2, 3}
insertWith f 1 {1, 2, 3} = {f 1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
insertWith f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
insertWith f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.insertWith f x Ordnode.nil = Ordnode.singleton x
O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by f
must be equivalent to x
.
adjustWith f 0 {1, 2, 3} = {1, 2, 3}
adjustWith f 1 {1, 2, 3} = {f 1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
adjustWith f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
adjustWith f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.adjustWith f x Ordnode.nil = Ordnode.nil
O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by f
must be equivalent to x
.
updateWith f 0 {1, 2, 3} = {1, 2, 3}
updateWith f 1 {1, 2, 3} = {2, 3} if f 1 = none
= {a, 2, 3} if f 1 = some a
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.updateWith f x Ordnode.nil = Ordnode.nil
O(log n). Modify an element in the set with the given function,
doing nothing if the key is not found.
Note that the element returned by f
must be equivalent to x
.
alter f 0 {1, 2, 3} = {1, 2, 3} if f none = none
= {a, 1, 2, 3} if f none = some a
alter f 1 {1, 2, 3} = {2, 3} if f 1 = none
= {a, 2, 3} if f 1 = some a
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.alter f x Ordnode.nil = Option.recOn (f none) Ordnode.nil Ordnode.singleton
O(log n). Insert an element into the set, preserving balance and the BST property. If an equivalent element is already in the set, this replaces it.
insert 1 {1, 2, 3} = {1, 2, 3}
insert 4 {1, 2, 3} = {1, 2, 3, 4}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
insert (1, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 1)}
insert (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.insert x Ordnode.nil = Ordnode.singleton x
Equations
- Ordnode.instInsert = { insert := Ordnode.insert }
O(log n). Insert an element into the set, preserving balance and the BST property. If an equivalent element is already in the set, the set is returned as is.
insert' 1 {1, 2, 3} = {1, 2, 3}
insert' 4 {1, 2, 3} = {1, 2, 3, 4}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
insert' (1, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
insert' (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.insert' x Ordnode.nil = Ordnode.singleton x
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)}, ∅)
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.split x Ordnode.nil = (Ordnode.nil, Ordnode.nil)
O(log n). Split the tree into those smaller than x
and those greater than it,
plus an element equivalent to x
, if it exists.
split3 2 {1, 2, 4} = ({1}, some 2, {4})
split3 3 {1, 2, 4} = ({1, 2}, none, {4})
split3 4 {1, 2, 4} = ({1, 2}, some 4, ∅)
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
split3 (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, some (1, 2), ∅)
split3 (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, none, ∅)
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.split3 x Ordnode.nil = (Ordnode.nil, none, Ordnode.nil)
O(log n). Remove an element from the set equivalent to x
. Does nothing if there
is no such element.
erase 1 {1, 2, 3} = {2, 3}
erase 4 {1, 2, 3} = {1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
erase (1, 1) {(0, 1), (1, 2)} = {(0, 1)}
erase (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
Equations
- Ordnode.erase x Ordnode.nil = Ordnode.nil
- Ordnode.erase x (Ordnode.node sz l y r) = match cmpLE x y with | Ordering.lt => (Ordnode.erase x l).balanceR y r | Ordering.eq => l.glue r | Ordering.gt => l.balanceL y (Ordnode.erase x r)
Auxiliary definition for findLt
.
Equations
- Ordnode.findLtAux x Ordnode.nil x✝ = x✝
- Ordnode.findLtAux x (Ordnode.node size l x_3 r) x✝ = if x ≤ x_3 then Ordnode.findLtAux x l x✝ else Ordnode.findLtAux x r x_3
O(log n). Get the largest element in the tree that is < x
.
findLt 2 {1, 2, 4} = some 1 findLt 3 {1, 2, 4} = some 2 findLt 0 {1, 2, 4} = none
Equations
- Ordnode.findLt x Ordnode.nil = none
- Ordnode.findLt x (Ordnode.node sz l x_2 r) = if x ≤ x_2 then Ordnode.findLt x l else some (Ordnode.findLtAux x r x_2)
Auxiliary definition for findGt
.
Equations
- Ordnode.findGtAux x Ordnode.nil x✝ = x✝
- Ordnode.findGtAux x (Ordnode.node size l x_3 r) x✝ = if x_3 ≤ x then Ordnode.findGtAux x r x✝ else Ordnode.findGtAux x l x_3
O(log n). Get the smallest element in the tree that is > x
.
findGt 2 {1, 2, 4} = some 4 findGt 3 {1, 2, 4} = some 4 findGt 4 {1, 2, 4} = none
Equations
- Ordnode.findGt x Ordnode.nil = none
- Ordnode.findGt x (Ordnode.node sz l x_2 r) = if x_2 ≤ x then Ordnode.findGt x r else some (Ordnode.findGtAux x l x_2)
Auxiliary definition for findLe
.
Equations
- Ordnode.findLeAux x Ordnode.nil x✝ = x✝
- Ordnode.findLeAux x (Ordnode.node size l x_3 r) x✝ = match cmpLE x x_3 with | Ordering.lt => Ordnode.findLeAux x l x✝ | Ordering.eq => x_3 | Ordering.gt => Ordnode.findLeAux x r x_3
O(log n). Get the largest element in the tree that is ≤ x
.
findLe 2 {1, 2, 4} = some 2 findLe 3 {1, 2, 4} = some 2 findLe 0 {1, 2, 4} = none
Equations
- Ordnode.findLe x Ordnode.nil = none
- Ordnode.findLe x (Ordnode.node sz l x_2 r) = match cmpLE x x_2 with | Ordering.lt => Ordnode.findLe x l | Ordering.eq => some x_2 | Ordering.gt => some (Ordnode.findLeAux x r x_2)
Auxiliary definition for findGe
.
Equations
- Ordnode.findGeAux x Ordnode.nil x✝ = x✝
- Ordnode.findGeAux x (Ordnode.node size l x_3 r) x✝ = match cmpLE x x_3 with | Ordering.lt => Ordnode.findGeAux x l x_3 | Ordering.eq => x_3 | Ordering.gt => Ordnode.findGeAux x r x✝
O(log n). Get the smallest element in the tree that is ≥ x
.
findGe 2 {1, 2, 4} = some 2 findGe 3 {1, 2, 4} = some 4 findGe 5 {1, 2, 4} = none
Equations
- Ordnode.findGe x Ordnode.nil = none
- Ordnode.findGe x (Ordnode.node sz l x_2 r) = match cmpLE x x_2 with | Ordering.lt => some (Ordnode.findGeAux x l x_2) | Ordering.eq => some x_2 | Ordering.gt => Ordnode.findGe x r
Auxiliary definition for findIndex
.
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.findIndexAux x Ordnode.nil x✝ = none
O(log n). Get the index, counting from the left,
of an element equivalent to x
if it exists.
findIndex 2 {1, 2, 4} = some 1
findIndex 4 {1, 2, 4} = some 2
findIndex 5 {1, 2, 4} = none
Equations
- Ordnode.findIndex x t = Ordnode.findIndexAux x t 0
Auxiliary definition for isSubset
.
Equations
- Ordnode.nil.isSubsetAux x✝ = true
- x✝.isSubsetAux Ordnode.nil = false
- (Ordnode.node size l x_2 r).isSubsetAux x✝ = match Ordnode.split3 x_2 x✝ with | (lt, found, gt) => found.isSome && l.isSubsetAux lt && r.isSubsetAux gt
O(m + n). Is every element of t₁
equivalent to some element of t₂
?
is_subset {1, 4} {1, 2, 4} = tt is_subset {1, 3} {1, 2, 4} = ff
O(m + n). Is every element of t₁
not equivalent to any element of t₂
?
disjoint {1, 3} {2, 4} = tt disjoint {1, 2} {2, 4} = ff
O(m * log(|m ∪ n| + 1)), m ≤ n. The union of two sets, preferring members of
t₁
over those of t₂
when equivalent elements are encountered.
union {1, 2} {2, 3} = {1, 2, 3} union {1, 3} {2} = {1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
union {(1, 1)} {(0, 1), (1, 2)} = {(0, 1), (1, 1)}
Equations
- One or more equations did not get rendered due to their size.
- x✝.union Ordnode.nil = x✝
- Ordnode.nil.union x✝ = x✝
O(m * log(|m ∪ n| + 1)), m ≤ n. Difference of two sets.
diff {1, 2} {2, 3} = {1} diff {1, 2, 3} {2} = {1, 3}
Equations
- One or more equations did not get rendered due to their size.
- x✝.diff Ordnode.nil = x✝
O(m * log(|m ∪ n| + 1)), m ≤ n. Intersection of two sets, preferring members of
t₁
over those of t₂
when equivalent elements are encountered.
inter {1, 2} {2, 3} = {2}
inter {1, 3} {2} = ∅
Equations
- One or more equations did not get rendered due to their size.
- Ordnode.nil.inter x✝ = Ordnode.nil
O(n * log n). Build a set from a list, preferring elements that appear earlier in the list in the case of equivalent elements.
ofList [1, 2, 3] = {1, 2, 3}
ofList [2, 1, 1, 3] = {1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
ofList [(1, 1), (0, 1), (1, 2)] = {(0, 1), (1, 1)}
Equations
O(n * log n). Adaptively chooses between the linear and log-linear algorithm depending on whether the input list is already sorted.
ofList' [1, 2, 3] = {1, 2, 3} ofList' [2, 1, 1, 3] = {1, 2, 3}
Equations
- Ordnode.ofList' [] = Ordnode.nil
- Ordnode.ofList' (x_1 :: xs) = if List.Chain (fun (a b : α) => ¬b ≤ a) x_1 xs then Ordnode.ofAscList (x_1 :: xs) else Ordnode.ofList (x_1 :: xs)
O(n * log n). Map a function on a set. Unlike map
this has no requirements on
f
, and the resulting set may be smaller than the input if f
is noninjective.
Equivalent elements are selected with a preference for smaller source elements.
image (fun x ↦ x + 2) {1, 2, 4} = {3, 4, 6}
image (fun x : ℕ ↦ x - 2) {1, 2, 4} = {0, 2}
Equations
- Ordnode.image f t = Ordnode.ofList (List.map f t.toList)