# mathlib3documentation

data.ordmap.ordset

# Verification of the `ordnode α` datatype #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file proves the correctness of the operations in `data.ordmap.ordnode`. The public facing version is the type `ordset α`, which is a wrapper around `ordnode α` which includes the correctness invariant of the type, and it exposes parallel operations like `insert` as functions on `ordset` that do the same thing but bundle the correctness proofs. The advantage is that it is possible to, for example, prove that the result of `find` on `insert` will actually find the element, while `ordnode` cannot guarantee this if the input tree did not satisfy the type invariants.

## Main definitions #

• `ordset α`: A well formed set of values of type `α`

## Implementation notes #

The majority of this file is actually in the `ordnode` namespace, because we first have to prove the correctness of all the operations (and defining what correctness means here is actually somewhat subtle). So all the actual `ordset` operations are at the very end, once we have all the theorems.

An `ordnode α` is an inductive type which describes a tree which stores the `size` at internal nodes. The correctness invariant of an `ordnode α` is:

• `ordnode.sized t`: All internal `size` fields must match the actual measured size of the tree. (This is not hard to satisfy.)
• `ordnode.balanced t`: Unless the tree has the form `()` or `((a) b)` or `(a (b))` (that is, nil or a single singleton subtree), the two subtrees must satisfy `size l ≤ δ * size r` and `size r ≤ δ * size l`, where `δ := 3` is a global parameter of the data structure (and this property must hold recursively at subtrees). This is why we say this is a "size balanced tree" data structure.
• `ordnode.bounded lo hi t`: The members of the tree must be in strictly increasing order, meaning that if `a` is in the left subtree and `b` is the root, then `a ≤ b` and `¬ (b ≤ a)`. We enforce this using `ordnode.bounded` which includes also a global upper and lower bound.

Because the `ordnode` file was ported from Haskell, the correctness invariants of some of the functions have not been spelled out, and some theorems like `ordnode.valid'.balance_l_aux` show very intricate assumptions on the sizes, which may need to be revised if it turns out some operations violate these assumptions, because there is a decent amount of slop in the actual data structure invariants, so the theorem will go through with multiple choices of assumption.

Note: This file is incomplete, in the sense that the intent is to have verified versions and lemmas about all the definitions in `ordnode.lean`, but at the moment only a few operations are verified (the hard part should be out of the way, but still). Contributors are encouraged to pick this up and finish the job, if it appeals to you.

## Tags #

ordered map, ordered set, data structure, verified programming

### delta and ratio #

theorem ordnode.not_le_delta {s : } (H : 1 s) :
theorem ordnode.delta_lt_false {a b : } (h₁ : < b) (h₂ : < a) :

### `size` and `empty`#

def ordnode.real_size {α : Type u_1} :

O(n). Computes the actual number of elements in the set, ignoring the cached `size` field.

Equations

### `sized`#

def ordnode.sized {α : Type u_1} :
Prop

The `sized` property asserts that all the `size` fields in nodes match the actual size of the respective subtrees.

Equations
theorem ordnode.sized.node' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) (hr : r.sized) :
(l.node' x r).sized
theorem ordnode.sized.eq_node' {α : Type u_1} {s : } {l : ordnode α} {x : α} {r : ordnode α} (h : l x r).sized) :
l x r = l.node' x r
theorem ordnode.sized.size_eq {α : Type u_1} {s : } {l : ordnode α} {x : α} {r : ordnode α} (H : l x r).sized) :
l x r).size = l.size + r.size + 1
theorem ordnode.sized.induction {α : Type u_1} {t : ordnode α} (hl : t.sized) {C : Prop} (H0 : C ordnode.nil) (H1 : (l : ordnode α) (x : α) (r : ordnode α), C l C r C (l.node' x r)) :
C t
theorem ordnode.size_eq_real_size {α : Type u_1} {t : ordnode α} :
@[simp]
theorem ordnode.sized.size_eq_zero {α : Type u_1} {t : ordnode α} (ht : t.sized) :
t.size = 0
theorem ordnode.sized.pos {α : Type u_1} {s : } {l : ordnode α} {x : α} {r : ordnode α} (h : l x r).sized) :
0 < s

`dual`

theorem ordnode.dual_dual {α : Type u_1} (t : ordnode α) :
t.dual.dual = t
@[simp]
theorem ordnode.size_dual {α : Type u_1} (t : ordnode α) :

`balanced`

def ordnode.balanced_sz (l r : ) :
Prop

The `balanced_sz l r` asserts that a hypothetical tree with children of sizes `l` and `r` is balanced: either `l ≤ δ * r` and `r ≤ δ * r`, or the tree is trivial with a singleton on one side and nothing on the other.

Equations
Instances for `ordnode.balanced_sz`
@[protected, instance]
Equations
def ordnode.balanced {α : Type u_1} :
Prop

The `balanced t` asserts that the tree `t` satisfies the balance invariants (at every level).

Equations
Instances for `ordnode.balanced`
@[protected, instance]
def ordnode.balanced.dec {α : Type u_1} :
Equations
theorem ordnode.balanced_sz.symm {l r : } :
theorem ordnode.balanced_sz_zero {l : } :
l 1
theorem ordnode.balanced_sz_up {l r₁ r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 r₂ ) (H : r₁) :
theorem ordnode.balanced_sz_down {l r₁ r₂ : } (h₁ : r₁ r₂) (h₂ : l + r₂ 1 l ) (H : r₂) :
theorem ordnode.balanced.dual {α : Type u_1} {t : ordnode α} :

### `rotate` and `balance`#

def ordnode.node3_l {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

Build a tree from three nodes, left associated (ignores the invariants).

Equations
def ordnode.node3_r {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :

Build a tree from three nodes, right associated (ignores the invariants).

Equations
def ordnode.node4_l {α : Type u_1} :
α α

Build a tree from three nodes, with `a () b -> (a ()) b` and `a (b c) d -> ((a b) (c d))`.

Equations
def ordnode.node4_r {α : Type u_1} :
α α

Build a tree from three nodes, with `a () b -> a (() b)` and `a (b c) d -> ((a b) (c d))`.

Equations
def ordnode.rotate_l {α : Type u_1} :
α

Concatenate two nodes, performing a left rotation `x (y z) -> ((x y) z)` if balance is upset.

Equations
def ordnode.rotate_r {α : Type u_1} :
α

Concatenate two nodes, performing a right rotation `(x y) z -> (x (y z))` if balance is upset.

Equations
def ordnode.balance_l' {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :

A left balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

Equations
def ordnode.balance_r' {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :

A right balance operation. This will rebalance a concatenation, assuming the original nodes are not too far from balanced.

Equations
def ordnode.balance' {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :

The full balance operation. This is the same as `balance`, but with less manual inlining. It is somewhat easier to work with this version in proofs.

Equations
theorem ordnode.dual_node' {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
(l.node' x r).dual = r.dual.node' x l.dual
theorem ordnode.dual_node3_l {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :
(l.node3_l x m y r).dual = r.dual.node3_r y m.dual x l.dual
theorem ordnode.dual_node3_r {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :
(l.node3_r x m y r).dual = r.dual.node3_l y m.dual x l.dual
theorem ordnode.dual_node4_l {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :
(l.node4_l x m y r).dual = r.dual.node4_r y m.dual x l.dual
theorem ordnode.dual_node4_r {α : Type u_1} (l : ordnode α) (x : α) (m : ordnode α) (y : α) (r : ordnode α) :
(l.node4_r x m y r).dual = r.dual.node4_l y m.dual x l.dual
theorem ordnode.dual_rotate_l {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
theorem ordnode.dual_rotate_r {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
theorem ordnode.dual_balance' {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
theorem ordnode.dual_balance_l {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
theorem ordnode.dual_balance_r {α : Type u_1} (l : ordnode α) (x : α) (r : ordnode α) :
theorem ordnode.sized.node3_l {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} (hl : l.sized) (hm : m.sized) (hr : r.sized) :
(l.node3_l x m y r).sized
theorem ordnode.sized.node3_r {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} (hl : l.sized) (hm : m.sized) (hr : r.sized) :
(l.node3_r x m y r).sized
theorem ordnode.sized.node4_l {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} (hl : l.sized) (hm : m.sized) (hr : r.sized) :
(l.node4_l x m y r).sized
theorem ordnode.node3_l_size {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node3_l x m y r).size = l.size + m.size + r.size + 2
theorem ordnode.node3_r_size {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node3_r x m y r).size = l.size + m.size + r.size + 2
theorem ordnode.node4_l_size {α : Type u_1} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} (hm : m.sized) :
(l.node4_l x m y r).size = l.size + m.size + r.size + 2
theorem ordnode.sized.dual {α : Type u_1} {t : ordnode α} (h : t.sized) :
theorem ordnode.sized.dual_iff {α : Type u_1} {t : ordnode α} :
theorem ordnode.sized.rotate_l {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) (hr : r.sized) :
(l.rotate_l x r).sized
theorem ordnode.sized.rotate_r {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) (hr : r.sized) :
(l.rotate_r x r).sized
theorem ordnode.sized.rotate_l_size {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hm : r.sized) :
(l.rotate_l x r).size = l.size + r.size + 1
theorem ordnode.sized.rotate_r_size {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) :
(l.rotate_r x r).size = l.size + r.size + 1
theorem ordnode.sized.balance' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) (hr : r.sized) :
(l.balance' x r).sized
theorem ordnode.size_balance' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.sized) (hr : r.sized) :
(l.balance' x r).size = l.size + r.size + 1

## `all`, `any`, `emem`, `amem`#

theorem ordnode.all.imp {α : Type u_1} {P Q : α Prop} (H : (a : α), P a Q a) {t : ordnode α} :
t t
theorem ordnode.any.imp {α : Type u_1} {P Q : α Prop} (H : (a : α), P a Q a) {t : ordnode α} :
t t
theorem ordnode.all_singleton {α : Type u_1} {P : α Prop} {x : α} :
{x} P x
theorem ordnode.any_singleton {α : Type u_1} {P : α Prop} {x : α} :
{x} P x
theorem ordnode.all_dual {α : Type u_1} {P : α Prop} {t : ordnode α} :
t.dual t
theorem ordnode.all_iff_forall {α : Type u_1} {P : α Prop} {t : ordnode α} :
t (x : α), t P x
theorem ordnode.any_iff_exists {α : Type u_1} {P : α Prop} {t : ordnode α} :
t (x : α), t P x
theorem ordnode.emem_iff_all {α : Type u_1} {x : α} {t : ordnode α} :
t (P : α Prop), t P x
theorem ordnode.all_node' {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} :
(l.node' x r) l P x r
theorem ordnode.all_node3_l {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node3_l x m y r) l P x m P y r
theorem ordnode.all_node3_r {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node3_r x m y r) l P x m P y r
theorem ordnode.all_node4_l {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node4_l x m y r) l P x m P y r
theorem ordnode.all_node4_r {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} :
(l.node4_r x m y r) l P x m P y r
theorem ordnode.all_rotate_l {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} :
(l.rotate_l x r) l P x r
theorem ordnode.all_rotate_r {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} :
(l.rotate_r x r) l P x r
theorem ordnode.all_balance' {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} :
(l.balance' x r) l P x r

### `to_list`#

theorem ordnode.foldr_cons_eq_to_list {α : Type u_1} (t : ordnode α) (r : list α) :
= t.to_list ++ r
@[simp]
theorem ordnode.to_list_nil {α : Type u_1} :
@[simp]
theorem ordnode.to_list_node {α : Type u_1} (s : ) (l : ordnode α) (x : α) (r : ordnode α) :
l x r).to_list = l.to_list ++ x :: r.to_list
theorem ordnode.emem_iff_mem_to_list {α : Type u_1} {x : α} {t : ordnode α} :
t x t.to_list
theorem ordnode.length_to_list' {α : Type u_1} (t : ordnode α) :
theorem ordnode.length_to_list {α : Type u_1} {t : ordnode α} (h : t.sized) :
theorem ordnode.equiv_iff {α : Type u_1} {t₁ t₂ : ordnode α} (h₁ : t₁.sized) (h₂ : t₂.sized) :
t₁.equiv t₂ t₁.to_list = t₂.to_list

### `mem`#

theorem ordnode.pos_size_of_mem {α : Type u_1} [has_le α] {x : α} {t : ordnode α} (h : t.sized) (h_mem : x t) :
0 < t.size

### `(find/erase/split)_(min/max)`#

theorem ordnode.find_min'_dual {α : Type u_1} (t : ordnode α) (x : α) :
theorem ordnode.find_max'_dual {α : Type u_1} (t : ordnode α) (x : α) :
theorem ordnode.find_min_dual {α : Type u_1} (t : ordnode α) :
theorem ordnode.find_max_dual {α : Type u_1} (t : ordnode α) :
theorem ordnode.dual_erase_min {α : Type u_1} (t : ordnode α) :
theorem ordnode.dual_erase_max {α : Type u_1} (t : ordnode α) :
theorem ordnode.split_min_eq {α : Type u_1} (s : ) (l : ordnode α) (x : α) (r : ordnode α) :
l.split_min' x r = (l.find_min' x, l x r).erase_min)
theorem ordnode.split_max_eq {α : Type u_1} (s : ) (l : ordnode α) (x : α) (r : ordnode α) :
l.split_max' x r = ((ordnode.node s l x r).erase_max,
theorem ordnode.find_min'_all {α : Type u_1} {P : α Prop} (t : ordnode α) (x : α) :
t P x P (t.find_min' x)
theorem ordnode.find_max'_all {α : Type u_1} {P : α Prop} (x : α) (t : ordnode α) :
P x t P t)

### `merge`#

@[simp]
theorem ordnode.merge_nil_left {α : Type u_1} (t : ordnode α) :
@[simp]
theorem ordnode.merge_nil_right {α : Type u_1} (t : ordnode α) :
@[simp]
theorem ordnode.merge_node {α : Type u_1} {ls : } {ll : ordnode α} {lx : α} {lr : ordnode α} {rs : } {rl : ordnode α} {rx : α} {rr : ordnode α} :
(ordnode.node ls ll lx lr).merge (ordnode.node rs rl rx rr) = ite < rs) (((ordnode.node ls ll lx lr).merge rl).balance_l rx rr) (ite < ls) (ll.balance_r lx (lr.merge (ordnode.node rs rl rx rr))) ((ordnode.node ls ll lx lr).glue (ordnode.node rs rl rx rr)))

### `insert`#

theorem ordnode.dual_insert {α : Type u_1} [preorder α] (x : α) (t : ordnode α) :
t).dual =

### `balance` properties #

theorem ordnode.balance_eq_balance' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) :
l.balance x r = l.balance' x r
theorem ordnode.balance_l_eq_balance {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (sl : l.sized) (sr : r.sized) (H1 : l.size = 0 r.size 1) (H2 : 1 l.size 1 r.size r.size ) :
l.balance_l x r = l.balance x r
def ordnode.raised (n m : ) :
Prop

`raised n m` means `m` is either equal or one up from `n`.

Equations
theorem ordnode.raised_iff {n m : } :
n m m n + 1
theorem ordnode.raised.dist_le {n m : } (H : m) :
n.dist m 1
theorem ordnode.raised.dist_le' {n m : } (H : m) :
m.dist n 1
theorem ordnode.raised.add_left (k : ) {n m : } (H : m) :
ordnode.raised (k + n) (k + m)
theorem ordnode.raised.add_right (k : ) {n m : } (H : m) :
ordnode.raised (n + k) (m + k)
theorem ordnode.raised.right {α : Type u_1} {l : ordnode α} {x₁ x₂ : α} {r₁ r₂ : ordnode α} (H : r₂.size) :
ordnode.raised (l.node' x₁ r₁).size (l.node' x₂ r₂).size
theorem ordnode.balance_l_eq_balance' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l.size r.size) (r' : ), r' ) :
l.balance_l x r = l.balance' x r
theorem ordnode.balance_sz_dual {α : Type u_1} {l r : ordnode α} (H : ( (l' : ), l' r.size) (r' : ), r.size ) :
( (l' : ), r.dual.size l.dual.size) (r' : ), r'
theorem ordnode.size_balance_l {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l.size r.size) (r' : ), r' ) :
(l.balance_l x r).size = l.size + r.size + 1
theorem ordnode.all_balance_l {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l.size r.size) (r' : ), r' ) :
(l.balance_l x r) l P x r
theorem ordnode.balance_r_eq_balance' {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l' r.size) (r' : ), r.size ) :
l.balance_r x r = l.balance' x r
theorem ordnode.size_balance_r {α : Type u_1} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l' r.size) (r' : ), r.size ) :
(l.balance_r x r).size = l.size + r.size + 1
theorem ordnode.all_balance_r {α : Type u_1} {P : α Prop} {l : ordnode α} {x : α} {r : ordnode α} (hl : l.balanced) (hr : r.balanced) (sl : l.sized) (sr : r.sized) (H : ( (l' : ), l' r.size) (r' : ), r.size ) :
(l.balance_r x r) l P x r

### `bounded`#

def ordnode.bounded {α : Type u_1} [preorder α] :
Prop

`bounded t lo hi` says that every element `x ∈ t` is in the range `lo < x < hi`, and also this property holds recursively in subtrees, making the full tree a BST. The bounds can be set to `lo = ⊥` and `hi = ⊤` if we care only about the internal ordering constraints.

Equations
theorem ordnode.bounded.dual {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (h : t.bounded o₁ o₂) :
t.dual.bounded o₂ o₁
theorem ordnode.bounded.dual_iff {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t.bounded o₁ o₂ t.dual.bounded o₂ o₁
theorem ordnode.bounded.weak_left {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t.bounded o₁ o₂ t.bounded o₂
theorem ordnode.bounded.weak_right {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t.bounded o₁ o₂ t.bounded o₁
theorem ordnode.bounded.weak {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (h : t.bounded o₁ o₂) :
theorem ordnode.bounded.mono_left {α : Type u_1} [preorder α] {x y : α} (xy : x y) {t : ordnode α} {o : with_top α} :
theorem ordnode.bounded.mono_right {α : Type u_1} [preorder α] {x y : α} (xy : x y) {t : ordnode α} {o : with_bot α} :
theorem ordnode.bounded.to_lt {α : Type u_1} [preorder α] {t : ordnode α} {x y : α} :
t.bounded x y x < y
theorem ordnode.bounded.to_nil {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t.bounded o₁ o₂ o₂
theorem ordnode.bounded.trans_left {α : Type u_1} [preorder α] {t₁ t₂ : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} :
t₁.bounded o₁ x t₂.bounded x o₂ t₂.bounded o₁ o₂
theorem ordnode.bounded.trans_right {α : Type u_1} [preorder α] {t₁ t₂ : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} :
t₁.bounded o₁ x t₂.bounded x o₂ t₁.bounded o₁ o₂
theorem ordnode.bounded.mem_lt {α : Type u_1} [preorder α] {t : ordnode α} {o : with_bot α} {x : α} :
t.bounded o x ordnode.all (λ (_x : α), _x < x) t
theorem ordnode.bounded.mem_gt {α : Type u_1} [preorder α] {t : ordnode α} {o : with_top α} {x : α} :
t.bounded x o ordnode.all (λ (_x : α), _x > x) t
theorem ordnode.bounded.of_lt {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} {x : α} :
t.bounded o₁ o₂ x ordnode.all (λ (_x : α), _x < x) t t.bounded o₁ x
theorem ordnode.bounded.of_gt {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} {x : α} :
t.bounded o₁ o₂ o₂ ordnode.all (λ (_x : α), _x > x) t t.bounded x o₂
theorem ordnode.bounded.to_sep {α : Type u_1} [preorder α] {t₁ t₂ : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} {x : α} (h₁ : t₁.bounded o₁ x) (h₂ : t₂.bounded x o₂) :
ordnode.all (λ (y : α), ordnode.all (λ (z : α), y < z) t₂) t₁

### `valid`#

structure ordnode.valid' {α : Type u_1} [preorder α] (lo : with_bot α) (t : ordnode α) (hi : with_top α) :
Prop

The validity predicate for an `ordnode` subtree. This asserts that the `size` fields are correct, the tree is balanced, and the elements of the tree are organized according to the ordering. This version of `valid` also puts all elements in the tree in the interval `(lo, hi)`.

def ordnode.valid {α : Type u_1} [preorder α] (t : ordnode α) :
Prop

The validity predicate for an `ordnode` subtree. This asserts that the `size` fields are correct, the tree is balanced, and the elements of the tree are organized according to the ordering.

Equations
theorem ordnode.valid'.mono_left {α : Type u_1} [preorder α] {x y : α} (xy : x y) {t : ordnode α} {o : with_top α} (h : o) :
o
theorem ordnode.valid'.mono_right {α : Type u_1} [preorder α] {x y : α} (xy : x y) {t : ordnode α} {o : with_bot α} (h : x) :
y
theorem ordnode.valid'.trans_left {α : Type u_1} [preorder α] {t₁ t₂ : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} (h : t₁.bounded o₁ x) (H : t₂ o₂) :
t₂ o₂
theorem ordnode.valid'.trans_right {α : Type u_1} [preorder α] {t₁ t₂ : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} (H : t₁ x) (h : t₂.bounded x o₂) :
t₁ o₂
theorem ordnode.valid'.of_lt {α : Type u_1} [preorder α] {t : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} (H : t o₂) (h₁ : x) (h₂ : ordnode.all (λ (_x : α), _x < x) t) :
t x
theorem ordnode.valid'.of_gt {α : Type u_1} [preorder α] {t : ordnode α} {x : α} {o₁ : with_bot α} {o₂ : with_top α} (H : t o₂) (h₁ : o₂) (h₂ : ordnode.all (λ (_x : α), _x > x) t) :
o₂
theorem ordnode.valid'.valid {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (h : t o₂) :
theorem ordnode.valid'_nil {α : Type u_1} [preorder α] {o₁ : with_bot α} {o₂ : with_top α} (h : o₂) :
theorem ordnode.valid_nil {α : Type u_1} [preorder α] :
theorem ordnode.valid'.node {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : r.size) (hs : s = l.size + r.size + 1) :
l x r) o₂
theorem ordnode.valid'.dual {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (h : t o₂) :
t.dual o₁
theorem ordnode.valid'.dual_iff {α : Type u_1} [preorder α] {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t o₂ t.dual o₁
theorem ordnode.valid.dual {α : Type u_1} [preorder α] {t : ordnode α} :
theorem ordnode.valid.dual_iff {α : Type u_1} [preorder α] {t : ordnode α} :
theorem ordnode.valid'.left {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (H : l x r) o₂) :
l x
theorem ordnode.valid'.right {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (H : l x r) o₂) :
o₂
theorem ordnode.valid.left {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} (H : l x r).valid) :
theorem ordnode.valid.right {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} (H : l x r).valid) :
theorem ordnode.valid.size_eq {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} (H : l x r).valid) :
l x r).size = l.size + r.size + 1
theorem ordnode.valid'.node' {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : r.size) :
(l.node' x r) o₂
theorem ordnode.valid'_singleton {α : Type u_1} [preorder α] {x : α} {o₁ : with_bot α} {o₂ : with_top α} (h₁ : x) (h₂ : o₂) :
{x} o₂
theorem ordnode.valid_singleton {α : Type u_1} [preorder α] {x : α} :
{x}.valid
theorem ordnode.valid'.node3_l {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hm : y) (hr : o₂) (H1 : m.size) (H2 : ordnode.balanced_sz (l.size + m.size + 1) r.size) :
(l.node3_l x m y r) o₂
theorem ordnode.valid'.node3_r {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hm : y) (hr : o₂) (H1 : (m.size + r.size + 1)) (H2 : r.size) :
(l.node3_r x m y r) o₂
theorem ordnode.valid'.node4_l_lemma₁ {a b c d : } (lr₂ : 3 * (b + c + 1 + d) 16 * a + 9) (mr₂ : b + c + 1 3 * d) (mm₁ : b 3 * c) :
b < 3 * a + 1
theorem ordnode.valid'.node4_l_lemma₂ {b c d : } (mr₂ : b + c + 1 3 * d) :
c 3 * d
theorem ordnode.valid'.node4_l_lemma₃ {b c d : } (mr₁ : 2 * d b + c + 1) (mm₁ : b 3 * c) :
d 3 * c
theorem ordnode.valid'.node4_l_lemma₄ {a b c d : } (lr₁ : 3 * a b + c + 1 + d) (mr₂ : b + c + 1 3 * d) (mm₁ : b 3 * c) :
a + b + 1 3 * (c + d + 1)
theorem ordnode.valid'.node4_l_lemma₅ {a b c d : } (lr₂ : 3 * (b + c + 1 + d) 16 * a + 9) (mr₁ : 2 * d b + c + 1) (mm₂ : c 3 * b) :
c + d + 1 3 * (a + b + 1)
theorem ordnode.valid'.node4_l {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {m : ordnode α} {y : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hm : y) (hr : o₂) (Hm : 0 < m.size) (H : l.size = 0 m.size = 1 r.size 1 0 < l.size m.size m.size + r.size 3 * (m.size + r.size) 16 * l.size + 9 m.size ) :
(l.node4_l x m y r) o₂
theorem ordnode.valid'.rotate_l_lemma₁ {a b c : } (H2 : 3 * a b + c) (hb₂ : c 3 * b) :
a 3 * b
theorem ordnode.valid'.rotate_l_lemma₂ {a b c : } (H3 : 2 * (b + c) 9 * a + 3) (h : b < 2 * c) :
b < 3 * a + 1
theorem ordnode.valid'.rotate_l_lemma₃ {a b c : } (H2 : 3 * a b + c) (h : b < 2 * c) :
a + b < 3 * c
theorem ordnode.valid'.rotate_l_lemma₄ {a b : } (H3 : 2 * b 9 * a + 3) :
3 * b 16 * a + 9
theorem ordnode.valid'.rotate_l {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H1 : ¬l.size + r.size 1) (H2 : < r.size) (H3 : 2 * r.size 9 * l.size + 5 r.size 3) :
(l.rotate_l x r) o₂
theorem ordnode.valid'.rotate_r {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H1 : ¬l.size + r.size 1) (H2 : < l.size) (H3 : 2 * l.size 9 * r.size + 5 l.size 3) :
(l.rotate_r x r) o₂
theorem ordnode.valid'.balance'_aux {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H₁ : 2 * r.size 9 * l.size + 5 r.size 3) (H₂ : 2 * l.size 9 * r.size + 5 l.size 3) :
(l.balance' x r) o₂
theorem ordnode.valid'.balance'_lemma {α : Type u_1} {l : ordnode α} {l' : } {r : ordnode α} {r' : } (H1 : r') (H2 : l.size.dist l' 1 r.size = r' r.size.dist r' 1 l.size = l') :
2 * r.size 9 * l.size + 5 r.size 3
theorem ordnode.valid'.balance' {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : (l' r' : ), r' (l.size.dist l' 1 r.size = r' r.size.dist r' 1 l.size = l')) :
(l.balance' x r) o₂
theorem ordnode.valid'.balance {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : (l' r' : ), r' (l.size.dist l' 1 r.size = r' r.size.dist r' 1 l.size = l')) :
(l.balance x r) o₂
theorem ordnode.valid'.balance_l_aux {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H₁ : l.size = 0 r.size 1) (H₂ : 1 l.size 1 r.size r.size ) (H₃ : 2 * l.size 9 * r.size + 5 l.size 3) :
(l.balance_l x r) o₂
theorem ordnode.valid'.balance_l {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : ( (l' : ), l.size r.size) (r' : ), r' ) :
(l.balance_l x r) o₂
theorem ordnode.valid'.balance_r_aux {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H₁ : r.size = 0 l.size 1) (H₂ : 1 r.size 1 l.size l.size ) (H₃ : 2 * r.size 9 * l.size + 5 r.size 3) :
(l.balance_r x r) o₂
theorem ordnode.valid'.balance_r {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) (H : ( (l' : ), l' r.size) (r' : ), r.size ) :
(l.balance_r x r) o₂
theorem ordnode.valid'.erase_max_aux {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (H : l x r) o₂) :
(l.node' x r).erase_max r) (l.node' x r).size = (l.node' x r).erase_max.size + 1
theorem ordnode.valid'.erase_min_aux {α : Type u_1} [preorder α] {s : } {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (H : l x r) o₂) :
ordnode.valid' (l.find_min' x) (l.node' x r).erase_min o₂ (l.node' x r).size = (l.node' x r).erase_min.size + 1
theorem ordnode.erase_min.valid {α : Type u_1} [preorder α] {t : ordnode α} (h : t.valid) :
theorem ordnode.erase_max.valid {α : Type u_1} [preorder α] {t : ordnode α} (h : t.valid) :
theorem ordnode.valid'.glue_aux {α : Type u_1} [preorder α] {l r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l o₂) (hr : r o₂) (sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l) (bal : r.size) :
(l.glue r) o₂ (l.glue r).size = l.size + r.size
theorem ordnode.valid'.glue {α : Type u_1} [preorder α] {l : ordnode α} {x : α} {r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l x) (hr : o₂) :
(l.glue r) o₂ (l.glue r).size = l.size + r.size
theorem ordnode.valid'.merge_lemma {a b c : } (h₁ : 3 * a < b + c + 1) (h₂ : b 3 * c) :
2 * (a + b) 9 * c + 5
theorem ordnode.valid'.merge_aux₁ {α : Type u_1} [preorder α] {o₁ : with_bot α} {o₂ : with_top α} {ls : } {ll : ordnode α} {lx : α} {lr : ordnode α} {rs : } {rl : ordnode α} {rx : α} {rr t : ordnode α} (hl : (ordnode.node ls ll lx lr) o₂) (hr : (ordnode.node rs rl rx rr) o₂) (h : < rs) (v : t rx) (e : t.size = ls + rl.size) :
(t.balance_l rx rr) o₂ (t.balance_l rx rr).size = ls + rs
theorem ordnode.valid'.merge_aux {α : Type u_1} [preorder α] {l r : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} (hl : l o₂) (hr : r o₂) (sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l) :
(l.merge r) o₂ (l.merge r).size = l.size + r.size
theorem ordnode.valid.merge {α : Type u_1} [preorder α] {l r : ordnode α} (hl : l.valid) (hr : r.valid) (sep : ordnode.all (λ (x : α), ordnode.all (λ (y : α), x < y) r) l) :
(l.merge r).valid
theorem ordnode.insert_with.valid_aux {α : Type u_1} [preorder α] (f : α α) (x : α) (hf : (y : α), x y y x x f y f y x) {t : ordnode α} {o₁ : with_bot α} {o₂ : with_top α} :
t o₂ x o₂ t) o₂ t).size
theorem ordnode.insert_with.valid {α : Type u_1} [preorder α] (f : α α) (x : α) (hf : (y : α), x y y x x f y f y x) {t : ordnode α} (h : t.valid) :
t).valid
theorem ordnode.insert_eq_insert_with {α : Type u_1} [preorder α] (x : α) (t : ordnode α) :
= ordnode.insert_with (λ (_x : α), x) x t
theorem ordnode.insert.valid {α : Type u_1} [preorder α] (x : α) {t : ordnode α} (h : t.valid) :
t).valid
theorem ordnode.insert'_eq_insert_with {α : Type u_1} [preorder α] (x : α) (t : ordnode α) :
theorem ordnode.insert'.valid {α : Type u_1} [preorder α] (x : α) {t : ordnode α} (h : t.valid) :
t).valid
theorem ordnode.valid'.map_aux {α : Type u_1} [preorder α] {β : Type u_2} [preorder β] {f : α β} (f_strict_mono : strict_mono f) {t : ordnode α} {a₁ : with_bot α} {a₂ : with_top α} (h : t a₂) :
ordnode.valid' a₁) t) a₂) t).size = t.size
theorem ordnode.map.valid {α : Type u_1} [preorder α] {β : Type u_2} [preorder β] {f : α β} (f_strict_mono : strict_mono f) {t : ordnode α} (h : t.valid) :
t).valid
theorem ordnode.valid'.erase_aux {α : Type u_1} [preorder α] (x : α) {t : ordnode α} {a₁ : with_bot α} {a₂ : with_top α} (h : t a₂) :
t) a₂ t.size
theorem ordnode.erase.valid {α : Type u_1} [preorder α] (x : α) {t : ordnode α} (h : t.valid) :
t).valid
theorem ordnode.size_erase_of_mem {α : Type u_1} [preorder α] {x : α} {t : ordnode α} {a₁ : with_bot α} {a₂ : with_top α} (h : t a₂) (h_mem : x t) :
t).size = t.size - 1
def ordset (α : Type u_1) [preorder α] :
Type u_1

An `ordset α` 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. The correctness property of the tree is baked into the type, so all operations on this type are correct by construction.

Equations
Instances for `ordset`
def ordset.nil {α : Type u_1} [preorder α] :

O(1). The empty set.

Equations
def ordset.size {α : Type u_1} [preorder α] (s : ordset α) :

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

Equations
@[protected]
def ordset.singleton {α : Type u_1} [preorder α] (a : α) :

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

Equations
@[protected, instance]
def ordset.has_emptyc {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def ordset.inhabited {α : Type u_1} [preorder α] :
Equations
@[protected, instance]
def ordset.has_singleton {α : Type u_1} [preorder α] :
(ordset α)
Equations
def ordset.empty {α : Type u_1} [preorder α] (s : ordset α) :
Prop

O(1). Is the set empty?

Equations
Instances for `ordset.empty`
theorem ordset.empty_iff {α : Type u_1} [preorder α] {s : ordset α} :
@[protected, instance]
def ordset.empty.decidable_pred {α : Type u_1} [preorder α] :
Equations
@[protected]
def ordset.insert {α : Type u_1} [preorder α] (x : α) (s : ordset α) :

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.

Equations
@[protected, instance]
def ordset.has_insert {α : Type u_1} [preorder α]  :
(ordset α)
Equations
def ordset.insert' {α : Type u_1} [preorder α] (x : α) (s : ordset α) :

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.

Equations
def ordset.mem {α : Type u_1} [preorder α] (x : α) (s : ordset α) :

O(log n). Does the set contain the element `x`? That is, is there an element that is equivalent to `x` in the order?

Equations
def ordset.find {α : Type u_1} [preorder α] (x : α) (s : ordset α) :

O(log n). Retrieve an element in the set that is equivalent to `x` in the order, if it exists.

Equations
@[protected, instance]
def ordset.has_mem {α : Type u_1} [preorder α]  :
(ordset α)
Equations
@[protected, instance]
def ordset.mem.decidable {α : Type u_1} [preorder α] (x : α) (s : ordset α) :
Equations
theorem ordset.pos_size_of_mem {α : Type u_1} [preorder α] {x : α} {t : ordset α} (h_mem : x t) :
0 < t.size
def ordset.erase {α : Type u_1} [preorder α] (x : α) (s : ordset α) :

O(log n). Remove an element from the set equivalent to `x`. Does nothing if there is no such element.

Equations
def ordset.map {α : Type u_1} [preorder α] {β : Type u_2} [preorder β] (f : α β) (f_strict_mono : strict_mono f) (s : ordset α) :

O(n). Map a function across a tree, without changing the structure.

Equations
• f_strict_mono s = s.val, _⟩