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

inductive Ordnode (α : Type u) : Type u

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.

• nil {α : Type u} : Ordnode α
• node {α : Type u} (size : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α

instance Ordnode.instEmptyCollection {α : Type u_1} : EmptyCollection (Ordnode α)

Equations

• Ordnode.instEmptyCollection = { emptyCollection := Ordnode.nil }

instance Ordnode.instInhabited {α : Type u_1} : Inhabited (Ordnode α)

Equations

• Ordnode.instInhabited = { default := Ordnode.nil }

@[inline]

def Ordnode.delta : ℕ

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

• Ordnode.delta = 3

@[inline]

def Ordnode.ratio : ℕ

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

• Ordnode.ratio = 2

@[inline]

def Ordnode.singleton {α : Type u_1} (a : α) : Ordnode α

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

singleton 3 = {3}

Equations

• Ordnode.singleton a = Ordnode.node 1 Ordnode.nil a Ordnode.nil

instance Ordnode.instSingleton {α : Type u_1} : Singleton α (Ordnode α)

Equations

• Ordnode.instSingleton = { singleton := Ordnode.singleton }

@[inline]

def Ordnode.size {α : Type u_1} : Ordnode α → ℕ

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

@[simp]

theorem Ordnode.size_nil {α : Type u_1} : nil.size = 0

@[simp]

theorem Ordnode.size_node {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : (node sz l x r).size = sz

@[inline]

def Ordnode.empty {α : Type u_1} : Ordnode α → Bool

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

def Ordnode.dual {α : Type u_1} : Ordnode α → Ordnode α

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

@[reducible, inline]

def Ordnode.node' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α

Internal use only

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

Equations

• l.node' x r = Ordnode.node (l.size + r.size + 1) l x r

def Ordnode.repr {α : Type u_2} [Repr α] (o : Ordnode α) (n : ℕ) : Std.Format

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

instance Ordnode.instRepr {α : Type u_2} [Repr α] : Repr (Ordnode α)

Equations

• Ordnode.instRepr = { reprPrec := Ordnode.repr }

def Ordnode.balanceL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α

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

• One or more equations did not get rendered due to their size.

def Ordnode.balanceR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α

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

• One or more equations did not get rendered due to their size.

def Ordnode.balance {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode α

Internal use only

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

Equations

• One or more equations did not get rendered due to their size.

def Ordnode.All {α : Type u_1} (P : α → Prop) : Ordnode α → Prop

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)

instance Ordnode.All.decidable {α : Type u_1} {P : α → Prop} (t : Ordnode α) [DecidablePred P] : Decidable (All P t)

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

def Ordnode.Any {α : Type u_1} (P : α → Prop) : Ordnode α → Prop

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)

instance Ordnode.Any.decidable {α : Type u_1} {P : α → Prop} (t : Ordnode α) [DecidablePred P] : Decidable (Any P t)

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

def Ordnode.Emem {α : Type u_1} (x : α) : Ordnode α → Prop

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)

instance Ordnode.Emem.decidable {α : Type u_1} (x : α) [DecidableEq α] (t : Ordnode α) : Decidable (Emem x t)

Equations

• Ordnode.Emem.decidable x = id inferInstance

def Ordnode.Amem {α : Type u_1} [LE α] (x : α) : Ordnode α → Prop

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

instance Ordnode.Amem.decidable {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) (t : Ordnode α) : Decidable (Amem x t)

Equations

• Ordnode.Amem.decidable x = id inferInstance

def Ordnode.findMin' {α : Type u_1} : Ordnode α → α → α

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

def Ordnode.findMin {α : Type u_1} : Ordnode α → Option α

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)

def Ordnode.findMax' {α : Type u_1} : α → Ordnode α → α

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

def Ordnode.findMax {α : Type u_1} : Ordnode α → Option α

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)

def Ordnode.eraseMin {α : Type u_1} : Ordnode α → Ordnode α

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

def Ordnode.eraseMax {α : Type u_1} : Ordnode α → Ordnode α

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

def Ordnode.splitMin' {α : Type u_1} : Ordnode α → α → Ordnode α → α × Ordnode α

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.nil.splitMin' x✝¹ x✝ = (x✝¹, x✝)
• (Ordnode.node size ll lx lr).splitMin' x✝¹ x✝ = match ll.splitMin' lx lr with | (xm, l') => (xm, l'.balanceR x✝¹ x✝)

def Ordnode.splitMin {α : Type u_1} : Ordnode α → Option (α × Ordnode α)

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)

def Ordnode.splitMax' {α : Type u_1} : Ordnode α → α → Ordnode α → Ordnode α × α

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

• x✝¹.splitMax' x✝ Ordnode.nil = (x✝¹, x✝)
• x✝¹.splitMax' x✝ (Ordnode.node size rl rx rr) = match rl.splitMax' rx rr with | (r', xm) => (x✝¹.balanceL x✝ r', xm)

def Ordnode.splitMax {α : Type u_1} : Ordnode α → Option (Ordnode α × α)

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)

def Ordnode.glue {α : Type u_1} : Ordnode α → Ordnode α → Ordnode α

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

def Ordnode.merge {α : Type u_1} (l : Ordnode α) : Ordnode α → Ordnode α

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.

def Ordnode.insertMax {α : Type u_1} : Ordnode α → α → Ordnode α

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

def Ordnode.insertMin {α : Type u_1} (x : α) : Ordnode α → Ordnode α

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

def Ordnode.link {α : Type u_1} (l : Ordnode α) (x : α) : Ordnode α → Ordnode α

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

def Ordnode.filter {α : Type u_1} (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α

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)

def Ordnode.partition {α : Type u_1} (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α × Ordnode α

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)

def Ordnode.map {α : Type u_1} {β : Type u_2} (f : α → β) : Ordnode α → Ordnode β

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)

def Ordnode.fold {α : Type u_1} {β : Sort u_2} (z : β) (f : β → α → β → β) : Ordnode α → β

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)

def Ordnode.foldl {α : Type u_1} {β : Sort u_2} (f : β → α → β) : β → Ordnode α → β

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

def Ordnode.foldr {α : Type u_1} {β : Sort u_2} (f : α → β → β) : Ordnode α → β → β

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

def Ordnode.toList {α : Type u_1} (t : Ordnode α) : List α

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

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

Equations

• t.toList = Ordnode.foldr List.cons t []

def Ordnode.toRevList {α : Type u_1} (t : Ordnode α) : List α

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

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

Equations

• t.toRevList = Ordnode.foldl (flip List.cons) [] t

instance Ordnode.instToString {α : Type u_1} [ToString α] : ToString (Ordnode α)

Equations

• Ordnode.instToString = { toString := fun (t : Ordnode α) => "{" ++ ", ".intercalate (List.map toString t.toList) ++ "}" }

instance Ordnode.instToFormat {α : Type u_1} [Std.ToFormat α] : Std.ToFormat (Ordnode α)

Equations

• Ordnode.instToFormat = { format := fun (t : Ordnode α) => Std.Format.joinSep (List.map Std.format t.toList) (Std.Format.text ", ") }

def Ordnode.Equiv {α : Type u_1} (t₁ t₂ : Ordnode α) : Prop

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

Equations

• t₁.Equiv t₂ = (t₁.size = t₂.size ∧ t₁.toList = t₂.toList)

instance Ordnode.instDecidableRelEquivOfDecidableEq {α : Type u_1} [DecidableEq α] : DecidableRel Equiv

Equations

• x.instDecidableRelEquivOfDecidableEq y = inferInstanceAs (Decidable (x.size = y.size ∧ x.toList = y.toList))

def Ordnode.powerset {α : Type u_1} (t : Ordnode α) : Ordnode (Ordnode α)

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

• One or more equations did not get rendered due to their size.

def Ordnode.prod {α : Type u_1} {β : Type u_2} (t₁ : Ordnode α) (t₂ : Ordnode β) : Ordnode (α × β)

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₁

def Ordnode.copair {α : Type u_1} {β : Type u_2} (t₁ : Ordnode α) (t₂ : Ordnode β) : Ordnode (α ⊕ β)

O(m + n). Build a set on the disjoint union by combining sets on the factors. Or.inl a ∈ s.copair t iff a ∈ s, and Or.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₂)

def Ordnode.pmap {α : Type u_1} {P : α → Prop} {β : Type u_2} (f : (a : α) → P a → β) (t : Ordnode α) : All P t → Ordnode β

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)

def Ordnode.attach' {α : Type u_1} {P : α → Prop} (t : Ordnode α) : All P t → Ordnode { a : α // P a }

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' (fun x ↦ x < 4) {1, 2} H = ({1, 2} : Ordnode {x // x<4}) 

Equations

• Ordnode.attach' = Ordnode.pmap Subtype.mk

def Ordnode.nth {α : Type u_1} : Ordnode α → ℕ → Option α

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

Equations

• Ordnode.nil.nth x✝ = none
• (Ordnode.node size l x_2 r).nth x✝ = match x✝.psub' l.size with | none => l.nth x✝ | some 0 => some x_2 | some j.succ => r.nth j

def Ordnode.removeNth {α : Type u_1} : Ordnode α → ℕ → Ordnode α

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}

Equations

• Ordnode.nil.removeNth x✝ = Ordnode.nil
• (Ordnode.node size l x_2 r).removeNth x✝ = match x✝.psub' l.size with | none => (l.removeNth x✝).balanceR x_2 r | some 0 => l.glue r | some j.succ => l.balanceL x_2 (r.removeNth j)

def Ordnode.takeAux {α : Type u_1} : Ordnode α → ℕ → Ordnode α

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

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

Equations

• Ordnode.nil.takeAux x✝ = Ordnode.nil
• (Ordnode.node size l x_2 r).takeAux x✝ = if x✝ = 0 then Ordnode.nil else match x✝.psub' l.size with | none => l.takeAux x✝ | some 0 => l | some j.succ => l.link x_2 (r.takeAux j)

def Ordnode.take {α : Type u_1} (i : ℕ) (t : Ordnode α) : Ordnode α

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}

Equations

• Ordnode.take i t = if t.size ≤ i then t else t.takeAux i

def Ordnode.dropAux {α : Type u_1} : Ordnode α → ℕ → Ordnode α

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

def Ordnode.drop {α : Type u_1} (i : ℕ) (t : Ordnode α) : Ordnode α

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

def Ordnode.splitAtAux {α : Type u_1} : Ordnode α → ℕ → Ordnode α × Ordnode α

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)

def Ordnode.splitAt {α : Type u_1} (i : ℕ) (t : Ordnode α) : Ordnode α × Ordnode α

O(log n). Split a set at the ith 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

def Ordnode.takeWhile {α : Type u_1} (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α

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

def Ordnode.dropWhile {α : Type u_1} (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α

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

def Ordnode.span {α : Type u_1} (p : α → Prop) [DecidablePred p] : Ordnode α → Ordnode α × Ordnode α

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)

@[irreducible]

def Ordnode.ofAscListAux₁ {α : Type u_1} (l : List α) : ℕ → Ordnode α × { l' : List α // l'.length ≤ l.length }

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.

Equations

• One or more equations did not get rendered due to their size.
• Ordnode.ofAscListAux₁ [] = fun (x : ℕ) => (Ordnode.nil, ⟨[], ⋯⟩)

@[irreducible]

def Ordnode.ofAscListAux₂ {α : Type u_1} : List α → Ordnode α → ℕ → Ordnode α

Auxiliary definition for ofAscList.

Equations

• One or more equations did not get rendered due to their size.
• Ordnode.ofAscListAux₂ [] = fun (t : Ordnode α) (x : ℕ) => t

def Ordnode.ofAscList {α : Type u_1} : List α → Ordnode α

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

def Ordnode.mem {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Bool

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

def Ordnode.find {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Option α

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

instance Ordnode.instMembership {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Membership α (Ordnode α)

Equations

• Ordnode.instMembership = { mem := fun (t : Ordnode α) (x : α) => Ordnode.mem x t = true }

instance Ordnode.mem.decidable {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) (t : Ordnode α) : Decidable (x ∈ t)

Equations

• Ordnode.mem.decidable x t = (Ordnode.mem x t).decEq true

def Ordnode.insertWith {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (f : α → α) (x : α) : Ordnode α → Ordnode α

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

def Ordnode.adjustWith {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (f : α → α) (x : α) : Ordnode α → Ordnode α

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

def Ordnode.updateWith {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (f : α → Option α) (x : α) : Ordnode α → Ordnode α

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

def Ordnode.alter {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (f : Option α → Option α) (x : α) : Ordnode α → Ordnode α

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

def Ordnode.insert {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Ordnode α

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

instance Ordnode.instInsert {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Insert α (Ordnode α)

Equations

• Ordnode.instInsert = { insert := Ordnode.insert }

def Ordnode.insert' {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Ordnode α

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

def Ordnode.split {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Ordnode α × Ordnode α

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)

def Ordnode.split3 {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Ordnode α × Option α × Ordnode α

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)

def Ordnode.erase {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Ordnode α

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)

def Ordnode.findLtAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → α → α

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

def Ordnode.findLt {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Option α

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)

def Ordnode.findGtAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → α → α

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

def Ordnode.findGt {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Option α

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)

def Ordnode.findLeAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → α → α

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

def Ordnode.findLe {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Option α

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)

def Ordnode.findGeAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → α → α

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✝

def Ordnode.findGe {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → Option α

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

def Ordnode.findIndexAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) : Ordnode α → ℕ → Option ℕ

Auxiliary definition for findIndex.

Equations

• One or more equations did not get rendered due to their size.
• Ordnode.findIndexAux x Ordnode.nil x✝ = none

def Ordnode.findIndex {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (x : α) (t : Ordnode α) : Option ℕ

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

def Ordnode.isSubsetAux {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Ordnode α → Ordnode α → Bool

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

def Ordnode.isSubset {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (t₁ t₂ : Ordnode α) : Bool

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₁.isSubset t₂ = (decide (t₁.size ≤ t₂.size) && t₁.isSubsetAux t₂)

def Ordnode.disjoint {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Ordnode α → Ordnode α → Bool

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

Equations

• Ordnode.nil.disjoint x✝ = true
• x✝.disjoint Ordnode.nil = true
• (Ordnode.node size l x_2 r).disjoint x✝ = match Ordnode.split3 x_2 x✝ with | (lt, found, gt) => found.isNone && l.disjoint lt && r.disjoint gt

def Ordnode.union {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Ordnode α → Ordnode α → Ordnode α

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✝

def Ordnode.diff {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Ordnode α → Ordnode α → Ordnode α

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✝

def Ordnode.inter {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : Ordnode α → Ordnode α → Ordnode α

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

def Ordnode.ofList {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] (l : List α) : Ordnode α

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

• Ordnode.ofList l = List.foldr insert Ordnode.nil l

def Ordnode.ofList' {α : Type u_1} [LE α] [DecidableRel fun (x1 x2 : α) => x1 ≤ x2] : List α → Ordnode α

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)

def Ordnode.image {α : Type u_2} {β : Type u_3} [LE β] [DecidableRel fun (x1 x2 : β) => x1 ≤ x2] (f : α → β) (t : Ordnode α) : Ordnode β

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)