Verification of the Ordnode α datatype

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'.balanceL_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) : ¬s ≤ Ordnode.delta * 0

theorem Ordnode.delta_lt_false {a : ℕ} {b : ℕ} (h₁ : Ordnode.delta * a < b) (h₂ : Ordnode.delta * b < a) : False

singleton

size and empty

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

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

Equations

• Ordnode.realSize Ordnode.nil = 0
• Ordnode.realSize (Ordnode.node size l x_1 r) = Ordnode.realSize l + Ordnode.realSize r + 1

Sized

def Ordnode.Sized {α : Type u_1} : Ordnode α → Prop

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

Equations

• Ordnode.Sized Ordnode.nil = True
• Ordnode.Sized (Ordnode.node size l x_1 r) = (size = Ordnode.size l + Ordnode.size r + 1 ∧ Ordnode.Sized l ∧ Ordnode.Sized r)

theorem Ordnode.Sized.node' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.node' l x r)

theorem Ordnode.Sized.eq_node' {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (h : Ordnode.Sized (Ordnode.node s l x r)) : Ordnode.node s l x r = Ordnode.node' l x r

theorem Ordnode.Sized.size_eq {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : Ordnode.Sized (Ordnode.node s l x r)) : Ordnode.size (Ordnode.node s l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.Sized.induction {α : Type u_1} {t : Ordnode α} (hl : Ordnode.Sized t) {C : Ordnode α → Prop} (H0 : C Ordnode.nil) (H1 : (l : Ordnode α) → (x : α) → (r : Ordnode α) → C l → C r → C (Ordnode.node' l x r)) : C t

theorem Ordnode.size_eq_realSize {α : Type u_1} {t : Ordnode α} : Ordnode.Sized t → Ordnode.size t = Ordnode.realSize t

@[simp]

theorem Ordnode.Sized.size_eq_zero {α : Type u_1} {t : Ordnode α} (ht : Ordnode.Sized t) : Ordnode.size t = 0 ↔ t = Ordnode.nil

theorem Ordnode.Sized.pos {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (h : Ordnode.Sized (Ordnode.node s l x r)) : 0 < s

dual

theorem Ordnode.dual_dual {α : Type u_1} (t : Ordnode α) : Ordnode.dual (Ordnode.dual t) = t

@[simp]

theorem Ordnode.size_dual {α : Type u_1} (t : Ordnode α) : Ordnode.size (Ordnode.dual t) = Ordnode.size t

Balanced

def Ordnode.BalancedSz (l : ℕ) (r : ℕ) : Prop

The BalancedSz 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.

instance Ordnode.BalancedSz.dec : DecidableRel Ordnode.BalancedSz

def Ordnode.Balanced {α : Type u_1} : Ordnode α → Prop

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

Equations

• Ordnode.Balanced Ordnode.nil = True
• Ordnode.Balanced (Ordnode.node size l x_1 r) = (Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size r) ∧ Ordnode.Balanced l ∧ Ordnode.Balanced r)

instance Ordnode.Balanced.dec {α : Type u_1} : DecidablePred Ordnode.Balanced

Equations

• One or more equations did not get rendered due to their size.
• Ordnode.Balanced.dec Ordnode.nil = Eq.mpr (_ : Decidable (Ordnode.Balanced Ordnode.nil) = Decidable True) inferInstance

theorem Ordnode.BalancedSz.symm {l : ℕ} {r : ℕ} : Ordnode.BalancedSz l r → Ordnode.BalancedSz r l

theorem Ordnode.balancedSz_zero {l : ℕ} : Ordnode.BalancedSz l 0 ↔ l ≤ 1

theorem Ordnode.balancedSz_up {l : ℕ} {r₁ : ℕ} {r₂ : ℕ} (h₁ : r₁ ≤ r₂) (h₂ : l + r₂ ≤ 1 ∨ r₂ ≤ Ordnode.delta * l) (H : Ordnode.BalancedSz l r₁) : Ordnode.BalancedSz l r₂

theorem Ordnode.balancedSz_down {l : ℕ} {r₁ : ℕ} {r₂ : ℕ} (h₁ : r₁ ≤ r₂) (h₂ : l + r₂ ≤ 1 ∨ l ≤ Ordnode.delta * r₁) (H : Ordnode.BalancedSz l r₂) : Ordnode.BalancedSz l r₁

theorem Ordnode.Balanced.dual {α : Type u_1} {t : Ordnode α} : Ordnode.Balanced t → Ordnode.Balanced (Ordnode.dual t)

rotate and balance

def Ordnode.node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode α

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

def Ordnode.node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode α

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

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

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

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

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

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

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

theorem Ordnode.rotateL_node {α : Type u_1} (l : Ordnode α) (x : α) (sz : ℕ) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.rotateL l x (Ordnode.node sz m y r) = if Ordnode.size m < Ordnode.ratio * Ordnode.size r then Ordnode.node3L l x m y r else Ordnode.node4L l x m y r

theorem Ordnode.rotateL_nil {α : Type u_1} (l : Ordnode α) (x : α) : Ordnode.rotateL l x Ordnode.nil = Ordnode.node' l x Ordnode.nil

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

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

theorem Ordnode.rotateR_node {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.rotateR (Ordnode.node sz l x m) y r = if Ordnode.size m < Ordnode.ratio * Ordnode.size l then Ordnode.node3R l x m y r else Ordnode.node4R l x m y r

theorem Ordnode.rotateR_nil {α : Type u_1} (y : α) (r : Ordnode α) : Ordnode.rotateR Ordnode.nil y r = Ordnode.node' Ordnode.nil y r

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

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

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

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

def Ordnode.balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : 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.

theorem Ordnode.dual_node' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.node' l x r) = Ordnode.node' (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.dual_node3L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.dual (Ordnode.node3L l x m y r) = Ordnode.node3R (Ordnode.dual r) y (Ordnode.dual m) x (Ordnode.dual l)

theorem Ordnode.dual_node3R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.dual (Ordnode.node3R l x m y r) = Ordnode.node3L (Ordnode.dual r) y (Ordnode.dual m) x (Ordnode.dual l)

theorem Ordnode.dual_node4L {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.dual (Ordnode.node4L l x m y r) = Ordnode.node4R (Ordnode.dual r) y (Ordnode.dual m) x (Ordnode.dual l)

theorem Ordnode.dual_node4R {α : Type u_1} (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) : Ordnode.dual (Ordnode.node4R l x m y r) = Ordnode.node4L (Ordnode.dual r) y (Ordnode.dual m) x (Ordnode.dual l)

theorem Ordnode.dual_rotateL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.rotateL l x r) = Ordnode.rotateR (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.dual_rotateR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.rotateR l x r) = Ordnode.rotateL (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.dual_balance' {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.balance' l x r) = Ordnode.balance' (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.dual_balanceL {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.balanceL l x r) = Ordnode.balanceR (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.dual_balanceR {α : Type u_1} (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.dual (Ordnode.balanceR l x r) = Ordnode.balanceL (Ordnode.dual r) x (Ordnode.dual l)

theorem Ordnode.Sized.node3L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hm : Ordnode.Sized m) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.node3L l x m y r)

theorem Ordnode.Sized.node3R {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hm : Ordnode.Sized m) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.node3R l x m y r)

theorem Ordnode.Sized.node4L {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hm : Ordnode.Sized m) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.node4L l x m y r)

theorem Ordnode.node3L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.size (Ordnode.node3L l x m y r) = Ordnode.size l + Ordnode.size m + Ordnode.size r + 2

theorem Ordnode.node3R_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.size (Ordnode.node3R l x m y r) = Ordnode.size l + Ordnode.size m + Ordnode.size r + 2

theorem Ordnode.node4L_size {α : Type u_1} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} (hm : Ordnode.Sized m) : Ordnode.size (Ordnode.node4L l x m y r) = Ordnode.size l + Ordnode.size m + Ordnode.size r + 2

theorem Ordnode.Sized.dual {α : Type u_1} {t : Ordnode α} : Ordnode.Sized t → Ordnode.Sized (Ordnode.dual t)

theorem Ordnode.Sized.dual_iff {α : Type u_1} {t : Ordnode α} : Ordnode.Sized (Ordnode.dual t) ↔ Ordnode.Sized t

theorem Ordnode.Sized.rotateL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.rotateL l x r)

theorem Ordnode.Sized.rotateR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.rotateR l x r)

theorem Ordnode.Sized.rotateL_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hm : Ordnode.Sized r) : Ordnode.size (Ordnode.rotateL l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.Sized.rotateR_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) : Ordnode.size (Ordnode.rotateR l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.Sized.balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hr : Ordnode.Sized r) : Ordnode.Sized (Ordnode.balance' l x r)

theorem Ordnode.size_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Sized l) (hr : Ordnode.Sized r) : Ordnode.size (Ordnode.balance' l x r) = Ordnode.size l + Ordnode.size r + 1

All, Any, Emem, Amem

theorem Ordnode.All.imp {α : Type u_1} {P : α → Prop} {Q : α → Prop} (H : (a : α) → P a → Q a) {t : Ordnode α} : Ordnode.All P t → Ordnode.All Q t

theorem Ordnode.Any.imp {α : Type u_1} {P : α → Prop} {Q : α → Prop} (H : (a : α) → P a → Q a) {t : Ordnode α} : Ordnode.Any P t → Ordnode.Any Q t

theorem Ordnode.all_singleton {α : Type u_1} {P : α → Prop} {x : α} : Ordnode.All P {x} ↔ P x

theorem Ordnode.any_singleton {α : Type u_1} {P : α → Prop} {x : α} : Ordnode.Any P {x} ↔ P x

theorem Ordnode.all_dual {α : Type u_1} {P : α → Prop} {t : Ordnode α} : Ordnode.All P (Ordnode.dual t) ↔ Ordnode.All P t

theorem Ordnode.all_iff_forall {α : Type u_1} {P : α → Prop} {t : Ordnode α} : Ordnode.All P t ↔ (x : α) → Ordnode.Emem x t → P x

theorem Ordnode.any_iff_exists {α : Type u_1} {P : α → Prop} {t : Ordnode α} : Ordnode.Any P t ↔ ∃ x, Ordnode.Emem x t ∧ P x

theorem Ordnode.emem_iff_all {α : Type u_1} {x : α} {t : Ordnode α} : Ordnode.Emem x t ↔ (P : α → Prop) → Ordnode.All P t → P x

theorem Ordnode.all_node' {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} : Ordnode.All P (Ordnode.node' l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

theorem Ordnode.all_node3L {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.All P (Ordnode.node3L l x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r

theorem Ordnode.all_node3R {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.All P (Ordnode.node3R l x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r

theorem Ordnode.all_node4L {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.All P (Ordnode.node4L l x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r

theorem Ordnode.all_node4R {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} : Ordnode.All P (Ordnode.node4R l x m y r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P m ∧ P y ∧ Ordnode.All P r

theorem Ordnode.all_rotateL {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} : Ordnode.All P (Ordnode.rotateL l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

theorem Ordnode.all_rotateR {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} : Ordnode.All P (Ordnode.rotateR l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

theorem Ordnode.all_balance' {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} : Ordnode.All P (Ordnode.balance' l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

toList

theorem Ordnode.foldr_cons_eq_toList {α : Type u_1} (t : Ordnode α) (r : List α) : Ordnode.foldr List.cons t r = Ordnode.toList t ++ r

@[simp]

theorem Ordnode.toList_nil {α : Type u_1} : Ordnode.toList Ordnode.nil = []

@[simp]

theorem Ordnode.toList_node {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.toList (Ordnode.node s l x r) = Ordnode.toList l ++ x :: Ordnode.toList r

theorem Ordnode.emem_iff_mem_toList {α : Type u_1} {x : α} {t : Ordnode α} : Ordnode.Emem x t ↔ x ∈ Ordnode.toList t

theorem Ordnode.length_toList' {α : Type u_1} (t : Ordnode α) : List.length (Ordnode.toList t) = Ordnode.realSize t

theorem Ordnode.length_toList {α : Type u_1} {t : Ordnode α} (h : Ordnode.Sized t) : List.length (Ordnode.toList t) = Ordnode.size t

theorem Ordnode.equiv_iff {α : Type u_1} {t₁ : Ordnode α} {t₂ : Ordnode α} (h₁ : Ordnode.Sized t₁) (h₂ : Ordnode.Sized t₂) : Ordnode.Equiv t₁ t₂ ↔ Ordnode.toList t₁ = Ordnode.toList t₂

mem

theorem Ordnode.pos_size_of_mem {α : Type u_1} [LE α] [DecidableRel fun x x_1 => x ≤ x_1] {x : α} {t : Ordnode α} (h : Ordnode.Sized t) (h_mem : x ∈ t) : 0 < Ordnode.size t

(find/erase/split)(Min/Max)

theorem Ordnode.findMin'_dual {α : Type u_1} (t : Ordnode α) (x : α) : Ordnode.findMin' (Ordnode.dual t) x = Ordnode.findMax' x t

theorem Ordnode.findMax'_dual {α : Type u_1} (t : Ordnode α) (x : α) : Ordnode.findMax' x (Ordnode.dual t) = Ordnode.findMin' t x

theorem Ordnode.findMin_dual {α : Type u_1} (t : Ordnode α) : Ordnode.findMin (Ordnode.dual t) = Ordnode.findMax t

theorem Ordnode.findMax_dual {α : Type u_1} (t : Ordnode α) : Ordnode.findMax (Ordnode.dual t) = Ordnode.findMin t

theorem Ordnode.dual_eraseMin {α : Type u_1} (t : Ordnode α) : Ordnode.dual (Ordnode.eraseMin t) = Ordnode.eraseMax (Ordnode.dual t)

theorem Ordnode.dual_eraseMax {α : Type u_1} (t : Ordnode α) : Ordnode.dual (Ordnode.eraseMax t) = Ordnode.eraseMin (Ordnode.dual t)

theorem Ordnode.splitMin_eq {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.splitMin' l x r = (Ordnode.findMin' l x, Ordnode.eraseMin (Ordnode.node s l x r))

theorem Ordnode.splitMax_eq {α : Type u_1} (s : ℕ) (l : Ordnode α) (x : α) (r : Ordnode α) : Ordnode.splitMax' l x r = (Ordnode.eraseMax (Ordnode.node s l x r), Ordnode.findMax' x r)

theorem Ordnode.findMin'_all {α : Type u_1} {P : α → Prop} (t : Ordnode α) (x : α) : Ordnode.All P t → P x → P (Ordnode.findMin' t x)

theorem Ordnode.findMax'_all {α : Type u_1} {P : α → Prop} (x : α) (t : Ordnode α) : P x → Ordnode.All P t → P (Ordnode.findMax' x t)

glue

merge

@[simp]

theorem Ordnode.merge_nil_left {α : Type u_1} (t : Ordnode α) : Ordnode.merge t Ordnode.nil = t

@[simp]

theorem Ordnode.merge_nil_right {α : Type u_1} (t : Ordnode α) : Ordnode.merge Ordnode.nil t = t

@[simp]

theorem Ordnode.merge_node {α : Type u_1} {ls : ℕ} {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : ℕ} {rl : Ordnode α} {rx : α} {rr : Ordnode α} : Ordnode.merge (Ordnode.node ls ll lx lr) (Ordnode.node rs rl rx rr) = if Ordnode.delta * ls < rs then Ordnode.balanceL (Ordnode.merge (Ordnode.node ls ll lx lr) rl) rx rr else if Ordnode.delta * rs < ls then Ordnode.balanceR ll lx (Ordnode.merge lr (Ordnode.node rs rl rx rr)) else Ordnode.glue (Ordnode.node ls ll lx lr) (Ordnode.node rs rl rx rr)

insert

theorem Ordnode.dual_insert {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (t : Ordnode α) : Ordnode.dual (Ordnode.insert x t) = Ordnode.insert x (Ordnode.dual t)

balance properties

theorem Ordnode.balance_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) : Ordnode.balance l x r = Ordnode.balance' l x r

theorem Ordnode.balanceL_eq_balance {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H1 : Ordnode.size l = 0 → Ordnode.size r ≤ 1) (H2 : 1 ≤ Ordnode.size l → 1 ≤ Ordnode.size r → Ordnode.size r ≤ Ordnode.delta * Ordnode.size l) : Ordnode.balanceL l x r = Ordnode.balance l x r

def Ordnode.Raised (n : ℕ) (m : ℕ) : Prop

Raised n m means m is either equal or one up from n.

theorem Ordnode.raised_iff {n : ℕ} {m : ℕ} : Ordnode.Raised n m ↔ n ≤ m ∧ m ≤ n + 1

theorem Ordnode.Raised.dist_le {n : ℕ} {m : ℕ} (H : Ordnode.Raised n m) : Nat.dist n m ≤ 1

theorem Ordnode.Raised.dist_le' {n : ℕ} {m : ℕ} (H : Ordnode.Raised n m) : Nat.dist m n ≤ 1

theorem Ordnode.Raised.add_left (k : ℕ) {n : ℕ} {m : ℕ} (H : Ordnode.Raised n m) : Ordnode.Raised (k + n) (k + m)

theorem Ordnode.Raised.add_right (k : ℕ) {n : ℕ} {m : ℕ} (H : Ordnode.Raised n m) : Ordnode.Raised (n + k) (m + k)

theorem Ordnode.Raised.right {α : Type u_1} {l : Ordnode α} {x₁ : α} {x₂ : α} {r₁ : Ordnode α} {r₂ : Ordnode α} (H : Ordnode.Raised (Ordnode.size r₁) (Ordnode.size r₂)) : Ordnode.Raised (Ordnode.size (Ordnode.node' l x₁ r₁)) (Ordnode.size (Ordnode.node' l x₂ r₂))

theorem Ordnode.balanceL_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised l' (Ordnode.size l) ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised (Ordnode.size r) r' ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.balanceL l x r = Ordnode.balance' l x r

theorem Ordnode.balance_sz_dual {α : Type u_1} {l : Ordnode α} {r : Ordnode α} (H : (∃ l', Ordnode.Raised (Ordnode.size l) l' ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised r' (Ordnode.size r) ∧ Ordnode.BalancedSz (Ordnode.size l) r') : (∃ l', Ordnode.Raised l' (Ordnode.size (Ordnode.dual r)) ∧ Ordnode.BalancedSz l' (Ordnode.size (Ordnode.dual l))) ∨ ∃ r', Ordnode.Raised (Ordnode.size (Ordnode.dual l)) r' ∧ Ordnode.BalancedSz (Ordnode.size (Ordnode.dual r)) r'

theorem Ordnode.size_balanceL {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised l' (Ordnode.size l) ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised (Ordnode.size r) r' ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.size (Ordnode.balanceL l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.all_balanceL {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised l' (Ordnode.size l) ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised (Ordnode.size r) r' ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.All P (Ordnode.balanceL l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

theorem Ordnode.balanceR_eq_balance' {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised (Ordnode.size l) l' ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised r' (Ordnode.size r) ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.balanceR l x r = Ordnode.balance' l x r

theorem Ordnode.size_balanceR {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised (Ordnode.size l) l' ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised r' (Ordnode.size r) ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.size (Ordnode.balanceR l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.all_balanceR {α : Type u_1} {P : α → Prop} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : Ordnode.Balanced l) (hr : Ordnode.Balanced r) (sl : Ordnode.Sized l) (sr : Ordnode.Sized r) (H : (∃ l', Ordnode.Raised (Ordnode.size l) l' ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised r' (Ordnode.size r) ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.All P (Ordnode.balanceR l x r) ↔ Ordnode.All P l ∧ P x ∧ Ordnode.All P r

bounded

def Ordnode.Bounded {α : Type u_1} [Preorder α] : Ordnode α → WithBot α → WithTop α → 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

• Ordnode.Bounded Ordnode.nil (some a) (some b) = (a < b)
• Ordnode.Bounded Ordnode.nil x x = True
• Ordnode.Bounded (Ordnode.node size l x_3 r) x x = (Ordnode.Bounded l x ↑x_3 ∧ Ordnode.Bounded r (↑x_3) x)

theorem Ordnode.Bounded.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded (Ordnode.dual t) o₂ o₁

theorem Ordnode.Bounded.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t o₁ o₂ ↔ Ordnode.Bounded (Ordnode.dual t) o₂ o₁

theorem Ordnode.Bounded.weak_left {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded t ⊥ o₂

theorem Ordnode.Bounded.weak_right {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded t o₁ ⊤

theorem Ordnode.Bounded.weak {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.Bounded t o₁ o₂) : Ordnode.Bounded t ⊥ ⊤

theorem Ordnode.Bounded.mono_left {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithTop α} : Ordnode.Bounded t (↑y) o → Ordnode.Bounded t (↑x) o

theorem Ordnode.Bounded.mono_right {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithBot α} : Ordnode.Bounded t o ↑x → Ordnode.Bounded t o ↑y

theorem Ordnode.Bounded.to_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {y : α} : Ordnode.Bounded t ↑x ↑y → x < y

theorem Ordnode.Bounded.to_nil {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded Ordnode.nil o₁ o₂

theorem Ordnode.Bounded.trans_left {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t₁ o₁ ↑x → Ordnode.Bounded t₂ (↑x) o₂ → Ordnode.Bounded t₂ o₁ o₂

theorem Ordnode.Bounded.trans_right {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Bounded t₁ o₁ ↑x → Ordnode.Bounded t₂ (↑x) o₂ → Ordnode.Bounded t₁ o₁ o₂

theorem Ordnode.Bounded.mem_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithBot α} {x : α} : Ordnode.Bounded t o ↑x → Ordnode.All (fun x => x < x) t

theorem Ordnode.Bounded.mem_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o : WithTop α} {x : α} : Ordnode.Bounded t (↑x) o → Ordnode.All (fun x => x > x) t

theorem Ordnode.Bounded.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded Ordnode.nil o₁ ↑x → Ordnode.All (fun x => x < x) t → Ordnode.Bounded t o₁ ↑x

theorem Ordnode.Bounded.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} : Ordnode.Bounded t o₁ o₂ → Ordnode.Bounded Ordnode.nil (↑x) o₂ → Ordnode.All (fun x => x > x) t → Ordnode.Bounded t (↑x) o₂

theorem Ordnode.Bounded.to_sep {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} {x : α} (h₁ : Ordnode.Bounded t₁ o₁ ↑x) (h₂ : Ordnode.Bounded t₂ (↑x) o₂) : Ordnode.All (fun y => Ordnode.All (fun z => y < z) t₂) t₁

Valid

structure Ordnode.Valid' {α : Type u_1} [Preorder α] (lo : WithBot α) (t : Ordnode α) (hi : WithTop α) : Prop

• ord : Ordnode.Bounded t lo hi
• sz : Ordnode.Sized t
• bal : Ordnode.Balanced t

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.

theorem Ordnode.Valid'.mono_left {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithTop α} (h : Ordnode.Valid' (↑y) t o) : Ordnode.Valid' (↑x) t o

theorem Ordnode.Valid'.mono_right {α : Type u_1} [Preorder α] {x : α} {y : α} (xy : x ≤ y) {t : Ordnode α} {o : WithBot α} (h : Ordnode.Valid' o t ↑x) : Ordnode.Valid' o t ↑y

theorem Ordnode.Valid'.trans_left {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.Bounded t₁ o₁ ↑x) (H : Ordnode.Valid' (↑x) t₂ o₂) : Ordnode.Valid' o₁ t₂ o₂

theorem Ordnode.Valid'.trans_right {α : Type u_1} [Preorder α] {t₁ : Ordnode α} {t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t₁ ↑x) (h : Ordnode.Bounded t₂ (↑x) o₂) : Ordnode.Valid' o₁ t₁ o₂

theorem Ordnode.Valid'.of_lt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t o₂) (h₁ : Ordnode.Bounded Ordnode.nil o₁ ↑x) (h₂ : Ordnode.All (fun x => x < x) t) : Ordnode.Valid' o₁ t ↑x

theorem Ordnode.Valid'.of_gt {α : Type u_1} [Preorder α] {t : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ t o₂) (h₁ : Ordnode.Bounded Ordnode.nil (↑x) o₂) (h₂ : Ordnode.All (fun x => x > x) t) : Ordnode.Valid' (↑x) t o₂

theorem Ordnode.Valid'.valid {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.Valid' o₁ t o₂) : Ordnode.Valid t

theorem Ordnode.valid'_nil {α : Type u_1} [Preorder α] {o₁ : WithBot α} {o₂ : WithTop α} (h : Ordnode.Bounded Ordnode.nil o₁ o₂) : Ordnode.Valid' o₁ Ordnode.nil o₂

theorem Ordnode.valid_nil {α : Type u_1} [Preorder α] : Ordnode.Valid Ordnode.nil

theorem Ordnode.Valid'.node {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size r)) (hs : s = Ordnode.size l + Ordnode.size r + 1) : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂

theorem Ordnode.Valid'.dual {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Valid' o₁ t o₂ → Ordnode.Valid' o₂ (Ordnode.dual t) o₁

theorem Ordnode.Valid'.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Valid' o₁ t o₂ ↔ Ordnode.Valid' o₂ (Ordnode.dual t) o₁

theorem Ordnode.Valid.dual {α : Type u_1} [Preorder α] {t : Ordnode α} : Ordnode.Valid t → Ordnode.Valid (Ordnode.dual t)

theorem Ordnode.Valid.dual_iff {α : Type u_1} [Preorder α] {t : Ordnode α} : Ordnode.Valid t ↔ Ordnode.Valid (Ordnode.dual t)

theorem Ordnode.Valid'.left {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) : Ordnode.Valid' o₁ l ↑x

theorem Ordnode.Valid'.right {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) : Ordnode.Valid' (↑x) r o₂

theorem Ordnode.Valid.left {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : Ordnode.Valid (Ordnode.node s l x r)) : Ordnode.Valid l

theorem Ordnode.Valid.right {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : Ordnode.Valid (Ordnode.node s l x r)) : Ordnode.Valid r

theorem Ordnode.Valid.size_eq {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (H : Ordnode.Valid (Ordnode.node s l x r)) : Ordnode.size (Ordnode.node s l x r) = Ordnode.size l + Ordnode.size r + 1

theorem Ordnode.Valid'.node' {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size r)) : Ordnode.Valid' o₁ (Ordnode.node' l x r) o₂

theorem Ordnode.valid'_singleton {α : Type u_1} [Preorder α] {x : α} {o₁ : WithBot α} {o₂ : WithTop α} (h₁ : Ordnode.Bounded Ordnode.nil o₁ ↑x) (h₂ : Ordnode.Bounded Ordnode.nil (↑x) o₂) : Ordnode.Valid' o₁ {x} o₂

theorem Ordnode.valid_singleton {α : Type u_1} [Preorder α] {x : α} : Ordnode.Valid {x}

theorem Ordnode.Valid'.node3L {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hm : Ordnode.Valid' (↑x) m ↑y) (hr : Ordnode.Valid' (↑y) r o₂) (H1 : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size m)) (H2 : Ordnode.BalancedSz (Ordnode.size l + Ordnode.size m + 1) (Ordnode.size r)) : Ordnode.Valid' o₁ (Ordnode.node3L l x m y r) o₂

theorem Ordnode.Valid'.node3R {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hm : Ordnode.Valid' (↑x) m ↑y) (hr : Ordnode.Valid' (↑y) r o₂) (H1 : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size m + Ordnode.size r + 1)) (H2 : Ordnode.BalancedSz (Ordnode.size m) (Ordnode.size r)) : Ordnode.Valid' o₁ (Ordnode.node3R l x m y r) o₂

theorem Ordnode.Valid'.node4L_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'.node4L_lemma₂ {b : ℕ} {c : ℕ} {d : ℕ} (mr₂ : b + c + 1 ≤ 3 * d) : c ≤ 3 * d

theorem Ordnode.Valid'.node4L_lemma₃ {b : ℕ} {c : ℕ} {d : ℕ} (mr₁ : 2 * d ≤ b + c + 1) (mm₁ : b ≤ 3 * c) : d ≤ 3 * c

theorem Ordnode.Valid'.node4L_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'.node4L_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'.node4L {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {m : Ordnode α} {y : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hm : Ordnode.Valid' (↑x) m ↑y) (hr : Ordnode.Valid' (↑y) r o₂) (Hm : 0 < Ordnode.size m) (H : Ordnode.size l = 0 ∧ Ordnode.size m = 1 ∧ Ordnode.size r ≤ 1 ∨ 0 < Ordnode.size l ∧ Ordnode.ratio * Ordnode.size r ≤ Ordnode.size m ∧ Ordnode.delta * Ordnode.size l ≤ Ordnode.size m + Ordnode.size r ∧ 3 * (Ordnode.size m + Ordnode.size r) ≤ 16 * Ordnode.size l + 9 ∧ Ordnode.size m ≤ Ordnode.delta * Ordnode.size r) : Ordnode.Valid' o₁ (Ordnode.node4L l x m y r) o₂

theorem Ordnode.Valid'.rotateL_lemma₁ {a : ℕ} {b : ℕ} {c : ℕ} (H2 : 3 * a ≤ b + c) (hb₂ : c ≤ 3 * b) : a ≤ 3 * b

theorem Ordnode.Valid'.rotateL_lemma₂ {a : ℕ} {b : ℕ} {c : ℕ} (H3 : 2 * (b + c) ≤ 9 * a + 3) (h : b < 2 * c) : b < 3 * a + 1

theorem Ordnode.Valid'.rotateL_lemma₃ {a : ℕ} {b : ℕ} {c : ℕ} (H2 : 3 * a ≤ b + c) (h : b < 2 * c) : a + b < 3 * c

theorem Ordnode.Valid'.rotateL_lemma₄ {a : ℕ} {b : ℕ} (H3 : 2 * b ≤ 9 * a + 3) : 3 * b ≤ 16 * a + 9

theorem Ordnode.Valid'.rotateL {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H1 : ¬Ordnode.size l + Ordnode.size r ≤ 1) (H2 : Ordnode.delta * Ordnode.size l < Ordnode.size r) (H3 : 2 * Ordnode.size r ≤ 9 * Ordnode.size l + 5 ∨ Ordnode.size r ≤ 3) : Ordnode.Valid' o₁ (Ordnode.rotateL l x r) o₂

theorem Ordnode.Valid'.rotateR {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H1 : ¬Ordnode.size l + Ordnode.size r ≤ 1) (H2 : Ordnode.delta * Ordnode.size r < Ordnode.size l) (H3 : 2 * Ordnode.size l ≤ 9 * Ordnode.size r + 5 ∨ Ordnode.size l ≤ 3) : Ordnode.Valid' o₁ (Ordnode.rotateR l x r) o₂

theorem Ordnode.Valid'.balance'_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H₁ : 2 * Ordnode.size r ≤ 9 * Ordnode.size l + 5 ∨ Ordnode.size r ≤ 3) (H₂ : 2 * Ordnode.size l ≤ 9 * Ordnode.size r + 5 ∨ Ordnode.size l ≤ 3) : Ordnode.Valid' o₁ (Ordnode.balance' l x r) o₂

theorem Ordnode.Valid'.balance'_lemma {α : Type u_2} {l : Ordnode α} {l' : ℕ} {r : Ordnode α} {r' : ℕ} (H1 : Ordnode.BalancedSz l' r') (H2 : Nat.dist (Ordnode.size l) l' ≤ 1 ∧ Ordnode.size r = r' ∨ Nat.dist (Ordnode.size r) r' ≤ 1 ∧ Ordnode.size l = l') : 2 * Ordnode.size r ≤ 9 * Ordnode.size l + 5 ∨ Ordnode.size r ≤ 3

theorem Ordnode.Valid'.balance' {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : ∃ l' r', Ordnode.BalancedSz l' r' ∧ (Nat.dist (Ordnode.size l) l' ≤ 1 ∧ Ordnode.size r = r' ∨ Nat.dist (Ordnode.size r) r' ≤ 1 ∧ Ordnode.size l = l')) : Ordnode.Valid' o₁ (Ordnode.balance' l x r) o₂

theorem Ordnode.Valid'.balance {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : ∃ l' r', Ordnode.BalancedSz l' r' ∧ (Nat.dist (Ordnode.size l) l' ≤ 1 ∧ Ordnode.size r = r' ∨ Nat.dist (Ordnode.size r) r' ≤ 1 ∧ Ordnode.size l = l')) : Ordnode.Valid' o₁ (Ordnode.balance l x r) o₂

theorem Ordnode.Valid'.balanceL_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H₁ : Ordnode.size l = 0 → Ordnode.size r ≤ 1) (H₂ : 1 ≤ Ordnode.size l → 1 ≤ Ordnode.size r → Ordnode.size r ≤ Ordnode.delta * Ordnode.size l) (H₃ : 2 * Ordnode.size l ≤ 9 * Ordnode.size r + 5 ∨ Ordnode.size l ≤ 3) : Ordnode.Valid' o₁ (Ordnode.balanceL l x r) o₂

theorem Ordnode.Valid'.balanceL {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : (∃ l', Ordnode.Raised l' (Ordnode.size l) ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised (Ordnode.size r) r' ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.Valid' o₁ (Ordnode.balanceL l x r) o₂

theorem Ordnode.Valid'.balanceR_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H₁ : Ordnode.size r = 0 → Ordnode.size l ≤ 1) (H₂ : 1 ≤ Ordnode.size r → 1 ≤ Ordnode.size l → Ordnode.size l ≤ Ordnode.delta * Ordnode.size r) (H₃ : 2 * Ordnode.size r ≤ 9 * Ordnode.size l + 5 ∨ Ordnode.size r ≤ 3) : Ordnode.Valid' o₁ (Ordnode.balanceR l x r) o₂

theorem Ordnode.Valid'.balanceR {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) (H : (∃ l', Ordnode.Raised (Ordnode.size l) l' ∧ Ordnode.BalancedSz l' (Ordnode.size r)) ∨ ∃ r', Ordnode.Raised r' (Ordnode.size r) ∧ Ordnode.BalancedSz (Ordnode.size l) r') : Ordnode.Valid' o₁ (Ordnode.balanceR l x r) o₂

theorem Ordnode.Valid'.eraseMax_aux {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) : Ordnode.Valid' o₁ (Ordnode.eraseMax (Ordnode.node' l x r)) ↑(Ordnode.findMax' x r) ∧ Ordnode.size (Ordnode.node' l x r) = Ordnode.size (Ordnode.eraseMax (Ordnode.node' l x r)) + 1

theorem Ordnode.Valid'.eraseMin_aux {α : Type u_1} [Preorder α] {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (H : Ordnode.Valid' o₁ (Ordnode.node s l x r) o₂) : Ordnode.Valid' (↑(Ordnode.findMin' l x)) (Ordnode.eraseMin (Ordnode.node' l x r)) o₂ ∧ Ordnode.size (Ordnode.node' l x r) = Ordnode.size (Ordnode.eraseMin (Ordnode.node' l x r)) + 1

theorem Ordnode.eraseMin.valid {α : Type u_1} [Preorder α] {t : Ordnode α} : Ordnode.Valid t → Ordnode.Valid (Ordnode.eraseMin t)

theorem Ordnode.eraseMax.valid {α : Type u_1} [Preorder α] {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.eraseMax t)

theorem Ordnode.Valid'.glue_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l o₂) (hr : Ordnode.Valid' o₁ r o₂) (sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l) (bal : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size r)) : Ordnode.Valid' o₁ (Ordnode.glue l r) o₂ ∧ Ordnode.size (Ordnode.glue l r) = Ordnode.size l + Ordnode.size r

theorem Ordnode.Valid'.glue {α : Type u_1} [Preorder α] {l : Ordnode α} {x : α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l ↑x) (hr : Ordnode.Valid' (↑x) r o₂) : Ordnode.BalancedSz (Ordnode.size l) (Ordnode.size r) → Ordnode.Valid' o₁ (Ordnode.glue l r) o₂ ∧ Ordnode.size (Ordnode.glue l r) = Ordnode.size l + Ordnode.size r

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₁ : WithBot α} {o₂ : WithTop α} {ls : ℕ} {ll : Ordnode α} {lx : α} {lr : Ordnode α} {rs : ℕ} {rl : Ordnode α} {rx : α} {rr : Ordnode α} {t : Ordnode α} (hl : Ordnode.Valid' o₁ (Ordnode.node ls ll lx lr) o₂) (hr : Ordnode.Valid' o₁ (Ordnode.node rs rl rx rr) o₂) (h : Ordnode.delta * ls < rs) (v : Ordnode.Valid' o₁ t ↑rx) (e : Ordnode.size t = ls + Ordnode.size rl) : Ordnode.Valid' o₁ (Ordnode.balanceL t rx rr) o₂ ∧ Ordnode.size (Ordnode.balanceL t rx rr) = ls + rs

theorem Ordnode.Valid'.merge_aux {α : Type u_1} [Preorder α] {l : Ordnode α} {r : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} (hl : Ordnode.Valid' o₁ l o₂) (hr : Ordnode.Valid' o₁ r o₂) (sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l) : Ordnode.Valid' o₁ (Ordnode.merge l r) o₂ ∧ Ordnode.size (Ordnode.merge l r) = Ordnode.size l + Ordnode.size r

theorem Ordnode.Valid.merge {α : Type u_1} [Preorder α] {l : Ordnode α} {r : Ordnode α} (hl : Ordnode.Valid l) (hr : Ordnode.Valid r) (sep : Ordnode.All (fun x => Ordnode.All (fun y => x < y) r) l) : Ordnode.Valid (Ordnode.merge l r)

theorem Ordnode.insertWith.valid_aux {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (f : α → α) (x : α) (hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t : Ordnode α} {o₁ : WithBot α} {o₂ : WithTop α} : Ordnode.Valid' o₁ t o₂ → Ordnode.Bounded Ordnode.nil o₁ ↑x → Ordnode.Bounded Ordnode.nil (↑x) o₂ → Ordnode.Valid' o₁ (Ordnode.insertWith f x t) o₂ ∧ Ordnode.Raised (Ordnode.size t) (Ordnode.size (Ordnode.insertWith f x t))

theorem Ordnode.insertWith.valid {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (f : α → α) (x : α) (hf : ∀ (y : α), x ≤ y ∧ y ≤ x → x ≤ f y ∧ f y ≤ x) {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.insertWith f x t)

theorem Ordnode.insert_eq_insertWith {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (t : Ordnode α) : Ordnode.insert x t = Ordnode.insertWith (fun x => x) x t

theorem Ordnode.insert.valid {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.insert x t)

theorem Ordnode.insert'_eq_insertWith {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (t : Ordnode α) : Ordnode.insert' x t = Ordnode.insertWith id x t

theorem Ordnode.insert'.valid {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.insert' x t)

theorem Ordnode.Valid'.map_aux {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Ordnode.Valid' a₁ t a₂) : Ordnode.Valid' (Option.map f a₁) (Ordnode.map f t) (Option.map f a₂) ∧ Ordnode.size (Ordnode.map f t) = Ordnode.size t

theorem Ordnode.map.valid {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] {f : α → β} (f_strict_mono : StrictMono f) {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.map f t)

theorem Ordnode.Valid'.erase_aux {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Ordnode.Valid' a₁ t a₂) : Ordnode.Valid' a₁ (Ordnode.erase x t) a₂ ∧ Ordnode.Raised (Ordnode.size (Ordnode.erase x t)) (Ordnode.size t)

theorem Ordnode.erase.valid {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) {t : Ordnode α} (h : Ordnode.Valid t) : Ordnode.Valid (Ordnode.erase x t)

theorem Ordnode.size_erase_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] {x : α} {t : Ordnode α} {a₁ : WithBot α} {a₂ : WithTop α} (h : Ordnode.Valid' a₁ t a₂) (h_mem : x ∈ t) : Ordnode.size (Ordnode.erase x t) = Ordnode.size t - 1

def Ordset (α : Type u_2) [Preorder α] : Type u_2

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.

def Ordset.nil {α : Type u_1} [Preorder α] : Ordset α

O(1). The empty set.

def Ordset.size {α : Type u_1} [Preorder α] (s : Ordset α) : ℕ

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

def Ordset.singleton {α : Type u_1} [Preorder α] (a : α) : Ordset α

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

instance Ordset.instEmptyCollection {α : Type u_1} [Preorder α] : EmptyCollection (Ordset α)

instance Ordset.instInhabited {α : Type u_1} [Preorder α] : Inhabited (Ordset α)

instance Ordset.instSingleton {α : Type u_1} [Preorder α] : Singleton α (Ordset α)

def Ordset.Empty {α : Type u_1} [Preorder α] (s : Ordset α) : Prop

O(1). Is the set empty?

theorem Ordset.empty_iff {α : Type u_1} [Preorder α] {s : Ordset α} : s = ∅ ↔ Ordnode.empty ↑s = true

instance Ordset.Empty.instDecidablePred {α : Type u_1} [Preorder α] : DecidablePred Ordset.Empty

def Ordset.insert {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : 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.

instance Ordset.instInsert {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] : Insert α (Ordset α)

def Ordset.insert' {α : Type u_1} [Preorder α] [IsTotal α fun x x_1 => x ≤ x_1] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : 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.

def Ordset.mem {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : Bool

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

def Ordset.find {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : Option α

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

instance Ordset.instMembership {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] : Membership α (Ordset α)

instance Ordset.mem.decidable {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : Decidable (x ∈ s)

theorem Ordset.pos_size_of_mem {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] {x : α} {t : Ordset α} (h_mem : x ∈ t) : 0 < Ordset.size t

def Ordset.erase {α : Type u_1} [Preorder α] [DecidableRel fun x x_1 => x ≤ x_1] (x : α) (s : Ordset α) : Ordset α

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

def Ordset.map {α : Type u_1} [Preorder α] {β : Type u_2} [Preorder β] (f : α → β) (f_strict_mono : StrictMono f) (s : Ordset α) : Ordset β

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