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.

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.

O(1). Construct a singleton set containing value a.

singleton 3 = {3}

O(1). Get the size of the set.

size {2, 1, 1, 4} = 3

O(1). Is the set empty?

empty ∅ = tt
empty {1, 2, 3} = ff

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.

Internal use only

O(1). Construct a node with the correct size information, without rebalancing.

Basic pretty printing for ordnode α that shows the structure of the tree.

repr {3, 1, 2, 4} = ((∅ 1 ∅) 2 ((∅ 3 ∅) 4 ∅))

Internal use only

O(1). Rebalance a tree which was previously balanced but has had its left side grow by 1, or its right side shrink by 1.

Internal use only

O(1). Rebalance a tree which was previously balanced but has had its right side grow by 1, or its left side shrink by 1.

Internal use only

O(1). Rebalance a tree which was previously balanced but has had one side change by at most 1.

O(n). Does every element of the map satisfy property P?

all (λ x, x < 5) {1, 2, 3} = true
all (λ x, x < 5) {1, 2, 3, 5} = false

O(n). Does any element of the map satisfy property P?

any (λ x, x < 2) {1, 2, 3} = true
any (λ x, x < 2) {2, 3, 5} = false

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

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:

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.

O(log n). Return the minimum element of the tree, or the provided default value.

find_min' 37 {1, 2, 3} = 1
find_min' 37 ∅ = 37

O(log n). Return the minimum element of the tree, if it exists.

find_min {1, 2, 3} = some 1
find_min ∅ = none

O(log n). Return the maximum element of the tree, or the provided default value.

find_max' 37 {1, 2, 3} = 3
find_max' 37 ∅ = 37

O(log n). Return the maximum element of the tree, if it exists.

find_max {1, 2, 3} = some 3
find_max ∅ = none

O(log n). Remove the minimum element from the tree, or do nothing if it is already empty.

erase_min {1, 2, 3} = {2, 3}
erase_min ∅ = ∅

O(log n). Remove the maximum element from the tree, or do nothing if it is already empty.

erase_max {1, 2, 3} = {1, 2}
erase_max ∅ = ∅

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

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

Internal use only

O(log(m+n)). Concatenate two trees that are balanced and ordered with respect to each other.

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

O(log n). Insert an element above all the others, without any comparisons. (Assumes that the element is in fact above all the others).

insert_max {1, 2} 4 = {1, 2, 4}
insert_max {1, 2} 0 = precondition violation

O(log n). Insert an element below all the others, without any comparisons. (Assumes that the element is in fact below all the others).

insert_min {1, 2} 0 = {0, 1, 2}
insert_min {1, 2} 4 = precondition violation

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

O(n). Filter the elements of a tree satisfying a predicate.

filter (λ x, x < 3) {1, 2, 4} = {1, 2}
filter (λ x, x > 5) {1, 2, 4} = ∅

O(n). Split the elements of a tree into those satisfying, and not satisfying, a predicate.

partition (λ x, x < 3) {1, 2, 4} = ({1, 2}, {3})

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 (λ x, x + 2) {1, 2, 4} = {2, 3, 6}
 partition (λ x : ℕ, x - 2) {1, 2, 4} = precondition violation

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.

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

O(n). Fold a function from right to left (in decreasing order) across the tree.

foldl f {1, 2, 4} z = f 1 (f 2 (f 4 z))

O(n). Build a list of elements in ascending order from the tree.

to_list {1, 2, 4} = [1, 2, 4]
to_list {2, 1, 1, 4} = [1, 2, 4]

O(n). Build a list of elements in descending order from the tree.

to_rev_list {1, 2, 4} = [4, 2, 1]
to_rev_list {2, 1, 1, 4} = [4, 2, 1]

O(n). True if the trees have the same elements, ignoring structural differences.

equiv {1, 2, 4} {2, 1, 1, 4} = true
equiv {1, 2, 4} {1, 2, 3} = false

O(2^n). Constructs the powerset of a given set, that is, the set of all subsets.

powerset {1, 2, 3} = {∅, {1}, {2}, {3}, {1,2}, {1,3}, {2,3}, {1,2,3}}

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)}

O(m+n). Build a set on the disjoint union by combining sets on the factors. inl a ∈ s.copair t iff a ∈ s, and inr b ∈ s.copair t iff b ∈ t.

copair {1, 2} {2, 3} = {inl 1, inl 2, inr 2, inr 3}

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)}

O(n). "Attach" the information that every element of t satisfies property P to these elements inside the set, producing a set in the subtype.

attach' (λ x, x < 4) {1, 2} H = ({1, 2} : ordnode {x // x<4})

O(log n). Get the ith 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 ith 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 take. (Can also be used in lieu of take if you know the index is within the range of the data structure.)

take_aux {a, b, c, d} 2 = {a, b}
take_aux {a, b, c, d} 5 = {a, b, c, d}

O(log n). Get the first i elements of the set, counted from the left.

take 2 {a, b, c, d} = {a, b}
take 5 {a, b, c, d} = {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 = ∅

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} = ∅

Auxiliary definition for split_at. (Can also be used in lieu of split_at if you know the index is within the range of the data structure.)

split_at_aux {a, b, c, d} 2 = ({a, b}, {c, d})
split_at_aux {a, b, c, d} 5 = ({a, b, c, d}, ∅)

O(log n). Split a set at the ith element, getting the first i and everything else.

split_at 2 {a, b, c, d} = ({a, b}, {c, d})
split_at 5 {a, b, c, d} = ({a, b, c, d}, ∅)

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.

take_while (λ x, x < 4) {1, 2, 3, 4, 5} = {1, 2, 3}
take_while (λ x, x > 4) {1, 2, 3, 4, 5} = precondition violation

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.

drop_while (λ x, x < 4) {1, 2, 3, 4, 5} = {4, 5}
drop_while (λ x, x > 4) {1, 2, 3, 4, 5} = precondition violation

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 (λ x, x < 4) {1, 2, 3, 4, 5} = ({1, 2, 3}, {4, 5})
span (λ x, x > 4) {1, 2, 3, 4, 5} = precondition violation

Auxiliary definition for of_asc_list.

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 of_asc_list [1, 2, 3] = {1, 2, 3} by rfl. This implementation is optimized for VM evaluation.

Auxiliary definition for of_asc_list.

O(n). Build a set from a list which is already sorted. Performs no comparisons.

of_asc_list [1, 2, 3] = {1, 2, 3}
of_asc_list [3, 2, 1] = precondition violation

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

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

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).

insert_with f 0 {1, 2, 3} = {0, 1, 2, 3}
insert_with f 1 {1, 2, 3} = {f 1, 2, 3}

Using a preorder on ℕ × ℕ that only compares the first coordinate:

insert_with f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
insert_with f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2), (3, 1)}

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.

adjust_with f 0 {1, 2, 3} = {1, 2, 3}
adjust_with f 1 {1, 2, 3} = {f 1, 2, 3}

Using a preorder on ℕ × ℕ that only compares the first coordinate:

adjust_with f (1, 1) {(0, 1), (1, 2)} = {(0, 1), f (1, 2)}
adjust_with f (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}

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.

update_with f 0 {1, 2, 3} = {1, 2, 3}
update_with f 1 {1, 2, 3} = {2, 3}     if f 1 = none
                          = {a, 2, 3}  if f 1 = some a