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.
Instances for ordnode
Equations
Equations
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
O(1). Get the size of the set.
size {2, 1, 1, 4} = 3
Equations
- (ordnode.node sz _x _x_1 _x_2).size = sz
- ordnode.nil.size = 0
O(1). Is the set empty?
Equations
- (ordnode.node _x _x_1 _x_2 _x_3).empty = bool.ff
- ordnode.nil.empty = bool.tt
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.node s l x r).dual = ordnode.node s r.dual x l.dual
- ordnode.nil.dual = ordnode.nil
Equations
- ordnode.has_repr = {repr := ordnode.repr _inst_1}
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.
Equations
- l.balance_l x r = r.cases_on (l.cases_on (ordnode.singleton x) (λ (ls : ℕ) (ll : ordnode α) (lx : α) (lr : ordnode α), ll.cases_on (lr.cases_on (ordnode.node 2 l x ordnode.nil) (λ (lr_size : ℕ) (lr_l : ordnode α) (lrx : α) (lr_r : ordnode α), ordnode.node 3 (ordnode.singleton lx) lrx (ordnode.singleton x))) (λ (lls : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), lr.cases_on (ordnode.node 3 ll lx (ordnode.singleton x)) (λ (lrs : ℕ) (lrl : ordnode α) (lrx : α) (lrr : ordnode α), ite (lrs < ordnode.ratio * lls) (ordnode.node (ls + 1) ll lx (ordnode.node (lrs + 1) lr x ordnode.nil)) (ordnode.node (ls + 1) (ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx (ordnode.node (lrr.size + 1) lrr x ordnode.nil)))))) (λ (rs : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), l.cases_on (ordnode.node (rs + 1) ordnode.nil x r) (λ (ls : ℕ) (ll : ordnode α) (lx : α) (lr : ordnode α), ite (ls > ordnode.delta * rs) (ll.cases_on ordnode.nil (λ (lls : ℕ) (l_2 : ordnode α) (x_2 : α) (r_2 : ordnode α), lr.cases_on ordnode.nil (λ (lrs : ℕ) (lrl : ordnode α) (lrx : α) (lrr : ordnode α), ite (lrs < ordnode.ratio * lls) (ordnode.node (ls + rs + 1) ll lx (ordnode.node (rs + lrs + 1) lr x r)) (ordnode.node (ls + rs + 1) (ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx (ordnode.node (lrr.size + rs + 1) lrr x r))))) (ordnode.node (ls + rs + 1) l x r)))
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.
Equations
- l.balance_r x r = l.cases_on (r.cases_on (ordnode.singleton x) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr : ordnode α), rr.cases_on (rl.cases_on (ordnode.node 2 ordnode.nil x r) (λ (rl_size : ℕ) (rl_l : ordnode α) (rlx : α) (rl_r : ordnode α), ordnode.node 3 (ordnode.singleton x) rlx (ordnode.singleton rx))) (λ (rrs : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), rl.cases_on (ordnode.node 3 (ordnode.singleton x) rx rr) (λ (rls : ℕ) (rll : ordnode α) (rlx : α) (rlr : ordnode α), ite (rls < ordnode.ratio * rrs) (ordnode.node (rs + 1) (ordnode.node (rls + 1) ordnode.nil x rl) rx rr) (ordnode.node (rs + 1) (ordnode.node (rll.size + 1) ordnode.nil x rll) rlx (ordnode.node (rlr.size + rrs + 1) rlr rx rr)))))) (λ (ls : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), r.cases_on (ordnode.node (ls + 1) l x ordnode.nil) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr : ordnode α), ite (rs > ordnode.delta * ls) (rr.cases_on ordnode.nil (λ (rrs : ℕ) (l_2 : ordnode α) (x_2 : α) (r_2 : ordnode α), rl.cases_on ordnode.nil (λ (rls : ℕ) (rll : ordnode α) (rlx : α) (rlr : ordnode α), ite (rls < ordnode.ratio * rrs) (ordnode.node (ls + rs + 1) (ordnode.node (ls + rls + 1) l x rl) rx rr) (ordnode.node (ls + rs + 1) (ordnode.node (ls + rll.size + 1) l x rll) rlx (ordnode.node (rlr.size + rrs + 1) rlr rx rr))))) (ordnode.node (ls + rs + 1) l x r)))
Internal use only
O(1). Rebalance a tree which was previously balanced but has had one side change by at most 1.
Equations
- l.balance x r = l.cases_on (r.cases_on (ordnode.singleton x) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr : ordnode α), rl.cases_on (rr.cases_on (ordnode.node 2 ordnode.nil x r) (λ (size : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), ordnode.node 3 (ordnode.singleton x) rx rr)) (λ (rls : ℕ) (rll : ordnode α) (rlx : α) (rlr : ordnode α), rr.cases_on (ordnode.node 3 (ordnode.singleton x) rlx (ordnode.singleton rx)) (λ (rrs : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), ite (rls < ordnode.ratio * rrs) (ordnode.node (rs + 1) (ordnode.node (rls + 1) ordnode.nil x rl) rx rr) (ordnode.node (rs + 1) (ordnode.node (rll.size + 1) ordnode.nil x rll) rlx (ordnode.node (rlr.size + rrs + 1) rlr rx rr)))))) (λ (ls : ℕ) (ll : ordnode α) (lx : α) (lr : ordnode α), r.cases_on (ll.cases_on (lr.cases_on (ordnode.node 2 l x ordnode.nil) (λ (lr_size : ℕ) (lr_l : ordnode α) (lrx : α) (lr_r : ordnode α), ordnode.node 3 (ordnode.singleton lx) lrx (ordnode.singleton x))) (λ (lls : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), lr.cases_on (ordnode.node 3 ll lx (ordnode.singleton x)) (λ (lrs : ℕ) (lrl : ordnode α) (lrx : α) (lrr : ordnode α), ite (lrs < ordnode.ratio * lls) (ordnode.node (ls + 1) ll lx (ordnode.node (lrs + 1) lr x ordnode.nil)) (ordnode.node (ls + 1) (ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx (ordnode.node (lrr.size + 1) lrr x ordnode.nil))))) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr : ordnode α), ite (ordnode.delta * ls < rs) (rl.cases_on ordnode.nil (λ (rls : ℕ) (rll : ordnode α) (rlx : α) (rlr : ordnode α), rr.cases_on ordnode.nil (λ (rrs : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), ite (rls < ordnode.ratio * rrs) (ordnode.node (ls + rs + 1) (ordnode.node (ls + rls + 1) l x rl) rx rr) (ordnode.node (ls + rs + 1) (ordnode.node (ls + rll.size + 1) l x rll) rlx (ordnode.node (rlr.size + rrs + 1) rlr rx rr))))) (ite (ordnode.delta * rs < ls) (ll.cases_on ordnode.nil (λ (lls : ℕ) (l_1 : ordnode α) (x_1 : α) (r_1 : ordnode α), lr.cases_on ordnode.nil (λ (lrs : ℕ) (lrl : ordnode α) (lrx : α) (lrr : ordnode α), ite (lrs < ordnode.ratio * lls) (ordnode.node (ls + rs + 1) ll lx (ordnode.node (lrs + rs + 1) lr x r)) (ordnode.node (ls + rs + 1) (ordnode.node (lls + lrl.size + 1) ll lx lrl) lrx (ordnode.node (lrr.size + rs + 1) lrr x r))))) (ordnode.node (ls + rs + 1) l x r))))
O(n). Does every element of the map satisfy property P
?
Equations
- ordnode.all P (ordnode.node _x l x r) = (ordnode.all P l ∧ P x ∧ ordnode.all P r)
- ordnode.all P ordnode.nil = true
Instances for ordnode.all
Equations
- ordnode.all.decidable t = ordnode.rec (id decidable.true) (λ (t_size : ℕ) (t_l : ordnode α) (t_x : α) (t_r : ordnode α) (t_ih_l : decidable (ordnode.all P t_l)) (t_ih_r : decidable (ordnode.all P t_r)), id and.decidable) t
O(n). Does any element of the map satisfy property P
?
Equations
- ordnode.any P (ordnode.node _x l x r) = (ordnode.any P l ∨ P x ∨ ordnode.any P r)
- ordnode.any P ordnode.nil = false
Instances for ordnode.any
Equations
- ordnode.any.decidable t = ordnode.rec (id decidable.false) (λ (t_size : ℕ) (t_l : ordnode α) (t_x : α) (t_r : ordnode α) (t_ih_l : decidable (ordnode.any P t_l)) (t_ih_r : decidable (ordnode.any P t_r)), id or.decidable) t
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.
Equations
- ordnode.emem x = ordnode.any (eq x)
Instances for ordnode.emem
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.
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
.
Equations
- ordnode.amem x = ordnode.any (λ (y : α), x ≤ y ∧ y ≤ x)
Instances for ordnode.amem
Equations
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
Equations
- (ordnode.node _x l x r).find_min' _x_1 = l.find_min' x
- ordnode.nil.find_min' x = x
O(log n). Return the minimum element of the tree, if it exists.
find_min {1, 2, 3} = some 1
find_min ∅ = none
Equations
- (ordnode.node _x l x r).find_min = option.some (l.find_min' x)
- ordnode.nil.find_min = option.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
Equations
- ordnode.find_max' _x (ordnode.node _x_1 l x r) = ordnode.find_max' x r
- ordnode.find_max' x ordnode.nil = x
O(log n). Return the maximum element of the tree, if it exists.
find_max {1, 2, 3} = some 3
find_max ∅ = none
Equations
- (ordnode.node _x l x r).find_max = option.some (ordnode.find_max' x r)
- ordnode.nil.find_max = option.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 ∅ = ∅
Equations
- (ordnode.node _x (ordnode.node size l x r) x_1 r_1).erase_min = (ordnode.node size l x r).erase_min.balance_r x_1 r_1
- (ordnode.node _x ordnode.nil x r).erase_min = r
- ordnode.nil.erase_min = ordnode.nil
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 ∅ = ∅
Equations
- (ordnode.node _x l x (ordnode.node size l_1 x_1 r)).erase_max = l.balance_l x (ordnode.node size l_1 x_1 r).erase_max
- (ordnode.node _x l x ordnode.nil).erase_max = l
- ordnode.nil.erase_max = ordnode.nil
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.
Equations
- (ordnode.node _x ll lx lr).split_min' x r = ordnode.split_min'._match_1 x r (ll.split_min' lx lr)
- ordnode.nil.split_min' x r = (x, r)
- ordnode.split_min'._match_1 x r (xm, l') = (xm, l'.balance_r x r)
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.node _x l x r).split_min = ↑(l.split_min' x r)
- ordnode.nil.split_min = option.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.
Equations
- l.split_max' x (ordnode.node _x rl rx rr) = ordnode.split_max'._match_1 l x (rl.split_max' rx rr)
- l.split_max' x ordnode.nil = (l, x)
- ordnode.split_max'._match_1 l x (r', xm) = (l.balance_l x r', xm)
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.node _x x l r).split_max = ↑(x.split_max' l r)
- ordnode.nil.split_max = option.none
Internal use only
O(log(m+n)). Concatenate two trees that are balanced and ordered with respect to each other.
Equations
- (ordnode.node sl ll lx lr).glue (ordnode.node sr rl rx rr) = ite (sl > sr) (ordnode.glue._match_1 sr rl rx rr (ll.split_max' lx lr)) (ordnode.glue._match_2 sl ll lx lr (rl.split_min' rx rr))
- (ordnode.node _x _x_1 _x_2 _x_3).glue ordnode.nil = ordnode.node _x _x_1 _x_2 _x_3
- ordnode.nil.glue r = r
- ordnode.glue._match_1 sr rl rx rr (l', m) = l'.balance_r m (ordnode.node sr rl rx rr)
- ordnode.glue._match_2 sl ll lx lr (m, r') = (ordnode.node sl ll lx lr).balance_l m 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
- l.merge = l.rec_on (λ (r : ordnode α), r) (λ (ls : ℕ) (ll : ordnode α) (lx : α) (lr : ordnode α) (IHll IHlr : ordnode α → ordnode α) (r : ordnode α), r.rec_on (ordnode.node ls ll lx lr) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr IHrl IHrr : ordnode α), ite (ordnode.delta * ls < rs) (IHrl.balance_l rx rr) (ite (ordnode.delta * rs < ls) (ll.balance_r lx (IHlr (ordnode.node rs rl rx rr))) ((ordnode.node ls ll lx lr).glue (ordnode.node rs rl rx rr)))))
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
Equations
- (ordnode.node _x l y r).insert_max x = l.balance_r y (r.insert_max x)
- ordnode.nil.insert_max x = ordnode.singleton 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).
insert_min {1, 2} 0 = {0, 1, 2}
insert_min {1, 2} 4 = precondition violation
Equations
- ordnode.insert_min x (ordnode.node _x l y r) = (ordnode.insert_min x l).balance_r y r
- ordnode.insert_min x ordnode.nil = ordnode.singleton x
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
- l.link x = l.rec_on (ordnode.insert_min x) (λ (ls : ℕ) (ll : ordnode α) (lx : α) (lr : ordnode α) (IHll IHlr : ordnode α → ordnode α) (r : ordnode α), r.rec_on (l.insert_max x) (λ (rs : ℕ) (rl : ordnode α) (rx : α) (rr IHrl IHrr : ordnode α), ite (ordnode.delta * ls < rs) (IHrl.balance_l rx rr) (ite (ordnode.delta * rs < ls) (ll.balance_r lx (IHlr r)) (l.node' x r))))
O(n). Filter the elements of a tree satisfying a predicate.
Equations
- ordnode.filter p (ordnode.node _x l x r) = ite (p x) ((ordnode.filter p l).link x (ordnode.filter p r)) ((ordnode.filter p l).merge (ordnode.filter p r))
- ordnode.filter p ordnode.nil = ordnode.nil
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})
Equations
- ordnode.partition p (ordnode.node _x l x r) = ordnode.partition._match_2 p x (ordnode.partition p r) (ordnode.partition p l)
- ordnode.partition p ordnode.nil = (ordnode.nil α, ordnode.nil α)
- ordnode.partition._match_2 p x _f_1 (l₁, l₂) = ordnode.partition._match_1 p x l₁ l₂ _f_1
- ordnode.partition._match_1 p x l₁ l₂ (r₁, r₂) = ite (p x) (l₁.link x r₁, l₂.merge r₂) (l₁.merge r₁, l₂.link x r₂)
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
Equations
- ordnode.map f (ordnode.node s l x r) = ordnode.node s (ordnode.map f l) (f x) (ordnode.map f r)
- ordnode.map f ordnode.nil = ordnode.nil
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.node _x l x r) = f (ordnode.fold z f l) x (ordnode.fold z f r)
- ordnode.fold z f ordnode.nil = z
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 z (ordnode.node _x l x r) = ordnode.foldl f (f (ordnode.foldl f z l) x) r
- ordnode.foldl f z ordnode.nil = z
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))
Equations
- ordnode.foldr f (ordnode.node _x l x r) z = ordnode.foldr f l (f x (ordnode.foldr f r z))
- ordnode.foldr f ordnode.nil z = 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]
Equations
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]
Equations
O(n). True if the trees have the same elements, ignoring structural differences.
Instances for ordnode.equiv
Equations
- ordnode.equiv.decidable_rel = λ (t₁ t₂ : ordnode α), and.decidable
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}}
Equations
- t.powerset = ordnode.insert_min ordnode.nil (ordnode.foldr (λ (x : α) (ts : ordnode (ordnode α)), (ordnode.insert_min (ordnode.singleton x) (ordnode.map (ordnode.insert_min x) ts)).glue ts) t ordnode.nil)
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 (λ (s₁ : ordnode (α × β)) (a : α) (s₂ : ordnode (α × β)), s₁.merge ((ordnode.map (prod.mk a) t₂).merge s₂)) t₁
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}
Equations
- t₁.copair t₂ = (ordnode.map sum.inl t₁).merge (ordnode.map sum.inr 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.
Equations
- ordnode.pmap f (ordnode.node s l x r) _ = ordnode.node s (ordnode.pmap f l hl) (f x hx) (ordnode.pmap f r hr)
- ordnode.pmap f ordnode.nil _x = ordnode.nil
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})
Equations
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
Equations
- (ordnode.node _x l x r).nth i = ordnode.nth._match_1 x (l.nth i) (λ (j : ℕ), r.nth j) (i.psub' l.size)
- ordnode.nil.nth i = option.none
- ordnode.nth._match_1 x _f_1 _f_2 (option.some (j + 1)) = _f_2 j
- ordnode.nth._match_1 x _f_1 _f_2 (option.some 0) = option.some x
- ordnode.nth._match_1 x _f_1 _f_2 option.none = _f_1
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}
Equations
- (ordnode.node _x l x r).remove_nth i = ordnode.remove_nth._match_1 l x r (l.remove_nth i) (λ (j : ℕ), r.remove_nth j) (i.psub' l.size)
- ordnode.nil.remove_nth i = ordnode.nil
- ordnode.remove_nth._match_1 l x r _f_1 _f_2 (option.some (j + 1)) = l.balance_l x (_f_2 j)
- ordnode.remove_nth._match_1 l x r _f_1 _f_2 (option.some 0) = l.glue r
- ordnode.remove_nth._match_1 l x r _f_1 _f_2 option.none = _f_1.balance_r x r
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}
Equations
- (ordnode.node _x l x r).take_aux i = ite (i = 0) ordnode.nil (ordnode.take_aux._match_1 l x (l.take_aux i) (λ (j : ℕ), r.take_aux j) (i.psub' l.size))
- ordnode.nil.take_aux i = ordnode.nil
- ordnode.take_aux._match_1 l x _f_1 _f_2 (option.some (j + 1)) = l.link x (_f_2 j)
- ordnode.take_aux._match_1 l x _f_1 _f_2 (option.some 0) = l
- ordnode.take_aux._match_1 l x _f_1 _f_2 option.none = _f_1
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
- (ordnode.node _x l x r).drop_aux i = ite (i = 0) (ordnode.node _x l x r) (ordnode.drop_aux._match_1 x r (l.drop_aux i) (λ (j : ℕ), r.drop_aux j) (i.psub' l.size))
- ordnode.nil.drop_aux i = ordnode.nil
- ordnode.drop_aux._match_1 x r _f_1 _f_2 (option.some (j + 1)) = _f_2 j
- ordnode.drop_aux._match_1 x r _f_1 _f_2 (option.some 0) = ordnode.insert_min x r
- ordnode.drop_aux._match_1 x r _f_1 _f_2 option.none = _f_1.link x r
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 = ite (t.size ≤ i) ordnode.nil (t.drop_aux i)
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}, ∅)
Equations
- (ordnode.node _x l x r).split_at_aux i = ite (i = 0) (ordnode.nil α, ordnode.node _x l x r) (ordnode.split_at_aux._match_1 l x r (l.split_at_aux i) (λ (j : ℕ), r.split_at_aux j) (i.psub' l.size))
- ordnode.nil.split_at_aux i = (ordnode.nil α, ordnode.nil α)
- ordnode.split_at_aux._match_1 l x r _f_1 _f_2 (option.some (j + 1)) = ordnode.split_at_aux._match_3 l x (_f_2 j)
- ordnode.split_at_aux._match_1 l x r _f_1 _f_2 (option.some 0) = (l.glue r, ordnode.insert_min x r)
- ordnode.split_at_aux._match_1 l x r _f_1 _f_2 option.none = ordnode.split_at_aux._match_2 x r _f_1
- ordnode.split_at_aux._match_3 l x (r₁, r₂) = (l.link x r₁, r₂)
- ordnode.split_at_aux._match_2 x r (l₁, l₂) = (l₁, l₂.link x r)
O(log n). Split a set at the i
th 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}, ∅)
Equations
- ordnode.split_at i t = ite (t.size ≤ i) (t, ordnode.nil α) (t.split_at_aux 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
.
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
Equations
- ordnode.take_while p (ordnode.node _x l x r) = ite (p x) (l.link x (ordnode.take_while p r)) (ordnode.take_while p l)
- ordnode.take_while p ordnode.nil = ordnode.nil
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
Equations
- ordnode.drop_while p (ordnode.node _x l x r) = ite (p x) (ordnode.drop_while p r) ((ordnode.drop_while p l).link x r)
- ordnode.drop_while p ordnode.nil = ordnode.nil
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
Equations
- ordnode.span p (ordnode.node _x l x r) = ite (p x) (ordnode.span._match_1 l x (ordnode.span p r)) (ordnode.span._match_2 x r (ordnode.span p l))
- ordnode.span p ordnode.nil = (ordnode.nil α, ordnode.nil α)
- ordnode.span._match_1 l x (r₁, r₂) = (l.link x r₁, r₂)
- ordnode.span._match_2 x r (l₁, l₂) = (l₁, l₂.link x r)
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.
Equations
- ordnode.of_asc_list_aux₁ (x :: xs) = λ (s : ℕ), ite (s = 1) (ordnode.singleton x, ⟨xs, _⟩) (ordnode.of_asc_list_aux₁._match_1 x xs (λ (y : α) (ys : list α) (h : (y :: ys).length ≤ xs.length) (this : (y :: ys).length ≤ xs.length.succ), ordnode.of_asc_list_aux₁ ys (s.shiftl 1)) (ordnode.of_asc_list_aux₁ xs (s.shiftl 1)))
- ordnode.of_asc_list_aux₁ list.nil = λ (s : ℕ), (ordnode.nil α, ⟨list.nil α, _⟩)
- ordnode.of_asc_list_aux₁._match_1 x xs _f_1 (l, ⟨y :: ys, h⟩) = have this : (y :: ys).length ≤ xs.length.succ, from _, ordnode.of_asc_list_aux₁._match_2 x xs l y ys this (_f_1 y ys h this)
- ordnode.of_asc_list_aux₁._match_1 x xs _f_1 (t, ⟨list.nil α, h⟩) = (t, ⟨list.nil α, _⟩)
- ordnode.of_asc_list_aux₁._match_2 x xs l y ys this (r, ⟨zs, h'⟩) = (l.link y r, ⟨zs, _⟩)
Auxiliary definition for of_asc_list
.
Equations
- ordnode.of_asc_list_aux₂ (x :: xs) = λ (l : ordnode α) (s : ℕ), ordnode.of_asc_list_aux₂._match_1 xs (λ (r : ordnode α) (ys : list α) (h : ys.length ≤ xs.length) (this : ys.length < xs.length.succ), ordnode.of_asc_list_aux₂ ys (l.link x r) (s.shiftl 1)) (ordnode.of_asc_list_aux₁ xs s)
- ordnode.of_asc_list_aux₂ list.nil = λ (t : ordnode α) (s : ℕ), t
- ordnode.of_asc_list_aux₂._match_1 xs _f_1 (r, ⟨ys, h⟩) = have this : ys.length < xs.length.succ, from _, _f_1 r ys h this
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
Equations
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?
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
Equations
- ordnode.mem x (ordnode.node _x l y r) = ordnode.mem._match_1 (ordnode.mem x l) (ordnode.mem x r) (cmp_le x y)
- ordnode.mem x ordnode.nil = bool.ff
- ordnode.mem._match_1 _f_1 _f_2 ordering.gt = _f_2
- ordnode.mem._match_1 _f_1 _f_2 ordering.eq = bool.tt
- ordnode.mem._match_1 _f_1 _f_2 ordering.lt = _f_1
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.node _x l y r) = ordnode.find._match_1 y (ordnode.find x l) (ordnode.find x r) (cmp_le x y)
- ordnode.find x ordnode.nil = option.none
- ordnode.find._match_1 y _f_1 _f_2 ordering.gt = _f_2
- ordnode.find._match_1 y _f_1 _f_2 ordering.eq = option.some y
- ordnode.find._match_1 y _f_1 _f_2 ordering.lt = _f_1
Equations
- ordnode.has_mem = {mem := λ (x : α) (t : ordnode α), ↥(ordnode.mem x t)}
Equations
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)}
Equations
- ordnode.insert_with f x (ordnode.node sz l y r) = ordnode.insert_with._match_1 f sz l y r (ordnode.insert_with f x l) (ordnode.insert_with f x r) (cmp_le x y)
- ordnode.insert_with f x ordnode.nil = ordnode.singleton x
- ordnode.insert_with._match_1 f sz l y r _f_1 _f_2 ordering.gt = l.balance_r y _f_2
- ordnode.insert_with._match_1 f sz l y r _f_1 _f_2 ordering.eq = ordnode.node sz l (f y) r
- ordnode.insert_with._match_1 f sz l y r _f_1 _f_2 ordering.lt = _f_1.balance_l y r
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)}
Equations
- ordnode.adjust_with f x (ordnode.node sz l y r) = ordnode.adjust_with._match_1 f sz l y r (ordnode.adjust_with f x l) (ordnode.adjust_with f x r) (cmp_le x y)
- ordnode.adjust_with f x ordnode.nil = ordnode.nil
- ordnode.adjust_with._match_1 f sz l y r _f_1 _f_2 ordering.gt = ordnode.node sz l y _f_2
- ordnode.adjust_with._match_1 f sz l y r _f_1 _f_2 ordering.eq = ordnode.node sz l (f y) r
- ordnode.adjust_with._match_1 f sz l y r _f_1 _f_2 ordering.lt = ordnode.node sz _f_1 y r
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
Equations
- ordnode.update_with f x (ordnode.node sz l y r) = ordnode.update_with._match_1 f sz l y r (ordnode.update_with f x l) (ordnode.update_with f x r) (cmp_le x y)
- ordnode.update_with f x ordnode.nil = ordnode.nil
- ordnode.update_with._match_1 f sz l y r _f_1 _f_2 ordering.gt = l.balance_l y _f_2
- ordnode.update_with._match_1 f sz l y r _f_1 _f_2 ordering.eq = ordnode.update_with._match_2 sz l r (f y)
- ordnode.update_with._match_1 f sz l y r _f_1 _f_2 ordering.lt = _f_1.balance_r y r
- ordnode.update_with._match_2 sz l r (option.some a) = ordnode.node sz l a r
- ordnode.update_with._match_2 sz l r option.none = l.glue r
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
- ordnode.alter f x (ordnode.node sz l y r) = ordnode.alter._match_1 f sz l y r (ordnode.alter f x l) (ordnode.alter f x r) (cmp_le x y)
- ordnode.alter f x ordnode.nil = (f option.none).rec_on ordnode.nil ordnode.singleton
- ordnode.alter._match_1 f sz l y r _f_1 _f_2 ordering.gt = l.balance y _f_2
- ordnode.alter._match_1 f sz l y r _f_1 _f_2 ordering.eq = ordnode.alter._match_2 sz l r (f (option.some y))
- ordnode.alter._match_1 f sz l y r _f_1 _f_2 ordering.lt = _f_1.balance y r
- ordnode.alter._match_2 sz l r (option.some a) = ordnode.node sz l a r
- ordnode.alter._match_2 sz l r option.none = l.glue r
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
- ordnode.insert x (ordnode.node sz l y r) = ordnode.insert._match_1 x sz l y r (ordnode.insert x l) (ordnode.insert x r) (cmp_le x y)
- ordnode.insert x ordnode.nil = ordnode.singleton x
- ordnode.insert._match_1 x sz l y r _f_1 _f_2 ordering.gt = l.balance_r y _f_2
- ordnode.insert._match_1 x sz l y r _f_1 _f_2 ordering.eq = ordnode.node sz l x r
- ordnode.insert._match_1 x sz l y r _f_1 _f_2 ordering.lt = _f_1.balance_l y r
Equations
- ordnode.has_insert = {insert := ordnode.insert (λ (a b : α), _inst_2 a b)}
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
- ordnode.insert' x (ordnode.node sz l y r) = ordnode.insert'._match_1 sz l y r (ordnode.insert' x l) (ordnode.insert' x r) (cmp_le x y)
- ordnode.insert' x ordnode.nil = ordnode.singleton x
- ordnode.insert'._match_1 sz l y r _f_1 _f_2 ordering.gt = l.balance_r y _f_2
- ordnode.insert'._match_1 sz l y r _f_1 _f_2 ordering.eq = ordnode.node sz l y r
- ordnode.insert'._match_1 sz l y r _f_1 _f_2 ordering.lt = _f_1.balance_l y r
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
- ordnode.split x (ordnode.node sz l y r) = ordnode.split._match_1 l y r (ordnode.split x l) (ordnode.split x r) (cmp_le x y)
- ordnode.split x ordnode.nil = (ordnode.nil α, ordnode.nil α)
- ordnode.split._match_1 l y r _f_1 _f_2 ordering.gt = ordnode.split._match_3 l y _f_2
- ordnode.split._match_1 l y r _f_1 _f_2 ordering.eq = (l, r)
- ordnode.split._match_1 l y r _f_1 _f_2 ordering.lt = ordnode.split._match_2 y r _f_1
- ordnode.split._match_3 l y (lt, gt) = (l.link y lt, gt)
- ordnode.split._match_2 y r (lt, gt) = (lt, gt.link y r)
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.
split 2 {1, 2, 4} = ({1}, some 2, {4})
split 3 {1, 2, 4} = ({1, 2}, none, {4})
split 4 {1, 2, 4} = ({1, 2}, some 4, ∅)
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
split (1, 1) {(0, 1), (1, 2)} = ({(0, 1)}, some (1, 2), ∅)
split (3, 1) {(0, 1), (1, 2)} = ({(0, 1), (1, 2)}, none, ∅)
Equations
- ordnode.split3 x (ordnode.node sz l y r) = ordnode.split3._match_1 l y r (ordnode.split3 x l) (ordnode.split3 x r) (cmp_le x y)
- ordnode.split3 x ordnode.nil = (ordnode.nil α, option.none α, ordnode.nil α)
- ordnode.split3._match_1 l y r _f_1 _f_2 ordering.gt = ordnode.split3._match_3 l y _f_2
- ordnode.split3._match_1 l y r _f_1 _f_2 ordering.eq = (l, option.some y, r)
- ordnode.split3._match_1 l y r _f_1 _f_2 ordering.lt = ordnode.split3._match_2 y r _f_1
- ordnode.split3._match_3 l y (lt, f, gt) = (l.link y lt, f, gt)
- ordnode.split3._match_2 y r (lt, f, gt) = (lt, f, gt.link y r)
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.node sz l y r) = ordnode.erase._match_1 l y r (ordnode.erase x l) (ordnode.erase x r) (cmp_le x y)
- ordnode.erase x ordnode.nil = ordnode.nil
- ordnode.erase._match_1 l y r _f_1 _f_2 ordering.gt = l.balance_l y _f_2
- ordnode.erase._match_1 l y r _f_1 _f_2 ordering.eq = l.glue r
- ordnode.erase._match_1 l y r _f_1 _f_2 ordering.lt = _f_1.balance_r y r
Auxiliary definition for find_lt
.
Equations
- ordnode.find_lt_aux x (ordnode.node _x l y r) best = ite (x ≤ y) (ordnode.find_lt_aux x l best) (ordnode.find_lt_aux x r y)
- ordnode.find_lt_aux x ordnode.nil best = best
O(log n). Get the largest element in the tree that is < x
.
find_lt 2 {1, 2, 4} = some 1
find_lt 3 {1, 2, 4} = some 2
find_lt 0 {1, 2, 4} = none
Equations
- ordnode.find_lt x (ordnode.node _x l y r) = ite (x ≤ y) (ordnode.find_lt x l) (option.some (ordnode.find_lt_aux x r y))
- ordnode.find_lt x ordnode.nil = option.none
Auxiliary definition for find_gt
.
Equations
- ordnode.find_gt_aux x (ordnode.node _x l y r) best = ite (y ≤ x) (ordnode.find_gt_aux x r best) (ordnode.find_gt_aux x l y)
- ordnode.find_gt_aux x ordnode.nil best = best
O(log n). Get the smallest element in the tree that is > x
.
find_lt 2 {1, 2, 4} = some 4
find_lt 3 {1, 2, 4} = some 4
find_lt 4 {1, 2, 4} = none
Equations
- ordnode.find_gt x (ordnode.node _x l y r) = ite (y ≤ x) (ordnode.find_gt x r) (option.some (ordnode.find_gt_aux x l y))
- ordnode.find_gt x ordnode.nil = option.none
Auxiliary definition for find_le
.
Equations
- ordnode.find_le_aux x (ordnode.node _x l y r) best = ordnode.find_le_aux._match_1 y (ordnode.find_le_aux x l best) (ordnode.find_le_aux x r y) (cmp_le x y)
- ordnode.find_le_aux x ordnode.nil best = best
- ordnode.find_le_aux._match_1 y _f_1 _f_2 ordering.gt = _f_2
- ordnode.find_le_aux._match_1 y _f_1 _f_2 ordering.eq = y
- ordnode.find_le_aux._match_1 y _f_1 _f_2 ordering.lt = _f_1
O(log n). Get the largest element in the tree that is ≤ x
.
find_le 2 {1, 2, 4} = some 2
find_le 3 {1, 2, 4} = some 2
find_le 0 {1, 2, 4} = none
Equations
- ordnode.find_le x (ordnode.node _x l y r) = ordnode.find_le._match_1 x y r (ordnode.find_le x l) (cmp_le x y)
- ordnode.find_le x ordnode.nil = option.none
- ordnode.find_le._match_1 x y r _f_1 ordering.gt = option.some (ordnode.find_le_aux x r y)
- ordnode.find_le._match_1 x y r _f_1 ordering.eq = option.some y
- ordnode.find_le._match_1 x y r _f_1 ordering.lt = _f_1
Auxiliary definition for find_ge
.
Equations
- ordnode.find_ge_aux x (ordnode.node _x l y r) best = ordnode.find_ge_aux._match_1 y (ordnode.find_ge_aux x l y) (ordnode.find_ge_aux x r best) (cmp_le x y)
- ordnode.find_ge_aux x ordnode.nil best = best
- ordnode.find_ge_aux._match_1 y _f_1 _f_2 ordering.gt = _f_2
- ordnode.find_ge_aux._match_1 y _f_1 _f_2 ordering.eq = y
- ordnode.find_ge_aux._match_1 y _f_1 _f_2 ordering.lt = _f_1
O(log n). Get the smallest element in the tree that is ≥ x
.
find_le 2 {1, 2, 4} = some 2
find_le 3 {1, 2, 4} = some 4
find_le 5 {1, 2, 4} = none
Equations
- ordnode.find_ge x (ordnode.node _x l y r) = ordnode.find_ge._match_1 x l y (ordnode.find_ge x r) (cmp_le x y)
- ordnode.find_ge x ordnode.nil = option.none
- ordnode.find_ge._match_1 x l y _f_1 ordering.gt = _f_1
- ordnode.find_ge._match_1 x l y _f_1 ordering.eq = option.some y
- ordnode.find_ge._match_1 x l y _f_1 ordering.lt = option.some (ordnode.find_ge_aux x l y)
Auxiliary definition for find_index
.
Equations
- ordnode.find_index_aux x (ordnode.node _x l y r) i = ordnode.find_index_aux._match_1 l i (ordnode.find_index_aux x l i) (ordnode.find_index_aux x r (i + l.size + 1)) (cmp_le x y)
- ordnode.find_index_aux x ordnode.nil i = option.none
- ordnode.find_index_aux._match_1 l i _f_1 _f_2 ordering.gt = _f_2
- ordnode.find_index_aux._match_1 l i _f_1 _f_2 ordering.eq = option.some (i + l.size)
- ordnode.find_index_aux._match_1 l i _f_1 _f_2 ordering.lt = _f_1
O(log n). Get the index, counting from the left,
of an element equivalent to x
if it exists.
find_index 2 {1, 2, 4} = some 1
find_index 4 {1, 2, 4} = some 2
find_index 5 {1, 2, 4} = none
Equations
- ordnode.find_index x t = ordnode.find_index_aux x t 0
Auxiliary definition for is_subset
.
Equations
- (ordnode.node _x l x r).is_subset_aux (ordnode.node size l_1 x_1 r_1) = ordnode.is_subset_aux._match_1 (λ (lt : ordnode α), l.is_subset_aux lt) (λ (gt : ordnode α), r.is_subset_aux gt) (ordnode.split3 x (ordnode.node size l_1 x_1 r_1))
- (ordnode.node size l x r).is_subset_aux ordnode.nil = bool.ff
- ordnode.nil.is_subset_aux (ordnode.node size l x r) = bool.tt
- ordnode.nil.is_subset_aux ordnode.nil = bool.tt
- ordnode.is_subset_aux._match_1 _f_1 _f_2 (lt, found, gt) = found.is_some && _f_1 lt && _f_2 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
Equations
- t₁.is_subset t₂ = decidable.to_bool (t₁.size ≤ t₂.size) && t₁.is_subset_aux t₂
O(m+n). Is every element of t₁
not equivalent to any element of t₂
?
Equations
- (ordnode.node _x l x r).disjoint (ordnode.node size l_1 x_1 r_1) = ordnode.disjoint._match_1 (λ (lt : ordnode α), l.disjoint lt) (λ (gt : ordnode α), r.disjoint gt) (ordnode.split3 x (ordnode.node size l_1 x_1 r_1))
- (ordnode.node size l x r).disjoint ordnode.nil = bool.tt
- ordnode.nil.disjoint (ordnode.node size l x r) = bool.tt
- ordnode.nil.disjoint ordnode.nil = bool.tt
- ordnode.disjoint._match_1 _f_1 _f_2 (lt, found, gt) = found.is_none && _f_1 lt && _f_2 gt
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
- (ordnode.node s₁ l₁ x₁ r₁).union (ordnode.node s₂ l₂ x₂ r₂) = ite (s₂ = 1) (ordnode.insert' x₂ (ordnode.node s₁ l₁ x₁ r₁)) (ite (s₁ = 1) (has_insert.insert x₁ (ordnode.node s₂ l₂ x₂ r₂)) (ordnode.union._match_1 x₁ (λ (l₂' : ordnode α), l₁.union l₂') (λ (r₂' : ordnode α), r₁.union r₂') (ordnode.split x₁ (ordnode.node s₂ l₂ x₂ r₂))))
- (ordnode.node size l x r).union ordnode.nil = ordnode.node size l x r
- ordnode.nil.union (ordnode.node size l x r) = ordnode.node size l x r
- ordnode.nil.union ordnode.nil = ordnode.nil
- ordnode.union._match_1 x₁ _f_1 _f_2 (l₂', r₂') = (_f_1 l₂').link x₁ (_f_2 r₂')
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
- t₁.diff (ordnode.node _x l₂ x r₂) = cond t₁.empty (ordnode.node _x l₂ x r₂) (ordnode.diff._match_1 t₁ (λ (l₁ : ordnode α), l₁.diff l₂) (λ (r₁ : ordnode α), r₁.diff r₂) (ordnode.split x t₁))
- t₁.diff ordnode.nil = t₁
- ordnode.diff._match_1 t₁ _f_1 _f_2 (l₁, r₁) = let l₁₂ : ordnode α := _f_1 l₁, r₁₂ : ordnode α := _f_2 r₁ in ite (l₁₂.size + r₁₂.size = t₁.size) t₁ (l₁₂.merge r₁₂)
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
- (ordnode.node _x l₁ x r₁).inter t₂ = cond t₂.empty (ordnode.node _x l₁ x r₁) (ordnode.inter._match_1 x (λ (l₂ : ordnode α), l₁.inter l₂) (λ (r₂ : ordnode α), r₁.inter r₂) (ordnode.split3 x t₂))
- ordnode.nil.inter t₂ = ordnode.nil
- ordnode.inter._match_1 x _f_1 _f_2 (l₂, y, r₂) = let l₁₂ : ordnode α := _f_1 l₂, r₁₂ : ordnode α := _f_2 r₂ in cond y.is_some (l₁₂.link x r₁₂) (l₁₂.merge r₁₂)
O(n * log n). Build a set from a list, preferring elements that appear earlier in the list in the case of equivalent elements.
of_list [1, 2, 3] = {1, 2, 3}
of_list [2, 1, 1, 3] = {1, 2, 3}
Using a preorder on ℕ × ℕ
that only compares the first coordinate:
of_list [(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.
of_list' [1, 2, 3] = {1, 2, 3} of_list' [2, 1, 1, 3] = {1, 2, 3}
Equations
- ordnode.of_list' (x :: xs) = ite (list.chain (λ (a b : α), ¬b ≤ a) x xs) (ordnode.of_asc_list (x :: xs)) (ordnode.of_list (x :: xs))
- ordnode.of_list' list.nil = ordnode.nil
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 (λ x, x + 2) {1, 2, 4} = {3, 4, 6}
image (λ x : ℕ, x - 2) {1, 2, 4} = {0, 2}
Equations
- ordnode.image f t = ordnode.of_list (list.map f t.to_list)