Invariants for the verification of Ordnode

An Ordnode, defined in Mathlib/Data/Ordmap/Ordnode.lean, is an inductive type which describes a tree which stores the size at internal nodes.

In this file we define the correctness invariant of an Ordnode, comprising:

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

This whole file is in the Ordnode namespace, because we first have to prove the correctness of all the operations (and defining what correctness means here is somewhat subtle). The actual Ordset operations are in Mathlib/Data/Ordmap/Ordset.lean.

TODO

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 ≤ delta * 0

theorem Ordnode.delta_lt_false {a b : ℕ} (h₁ : delta * a < b) (h₂ : 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.

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.

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 : (node s l x r).Sized) : node s l x r = l.node' x r

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

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

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

@[simp]

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

theorem Ordnode.Sized.pos {α : Type u_1} {s : ℕ} {l : Ordnode α} {x : α} {r : Ordnode α} (h : (node s 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 α) : t.dual.size = t.size

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 BalancedSz

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

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

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

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

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

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

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

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

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 α) : l.rotateL x (node sz m y r) = if m.size < ratio * r.size then l.node3L x m y r else l.node4L x m y r

theorem Ordnode.rotateL_nil {α : Type u_1} (l : Ordnode α) (x : α) : l.rotateL x nil = l.node' x 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 α) : (node sz l x m).rotateR y r = if m.size < ratio * l.size then l.node3R x m y r else l.node4R x m y r

theorem Ordnode.rotateR_nil {α : Type u_1} (y : α) (r : Ordnode α) : nil.rotateR y r = nil.node' 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 α) : (l.node' x r).dual = r.dual.node' x l.dual

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem Ordnode.Sized.rotateR_size {α : Type u_1} {l : Ordnode α} {x : α} {r : Ordnode α} (hl : l.Sized) : (l.rotateR 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 α} : All P t → All Q t

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

toList

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

@[simp]

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

@[simp]

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

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

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

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

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

mem

theorem Ordnode.pos_size_of_mem {α : Type u_1} [LE α] [DecidableLE α] {x : α} {t : Ordnode α} (h : t.Sized) (h_mem : x ∈ t) : 0 < t.size

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

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

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

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

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

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

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

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

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

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

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

glue

merge

@[simp]

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

@[simp]

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

@[simp]

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

insert

theorem Ordnode.dual_insert {α : Type u_1} [LE α] [IsTotal α fun (x1 x2 : α) => x1 ≤ x2] [DecidableLE α] (x : α) (t : Ordnode α) : (Ordnode.insert x t).dual = Ordnode.insert x 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.balanceL_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 ≤ delta * l.size) : l.balanceL 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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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₁ : WithBot α} {o₂ : WithTop α} : t.Bounded o₁ o₂ → nil.Bounded o₁ o₂

theorem Ordnode.Bounded.trans_left {α : Type u_1} [Preorder α] {t₁ t₂ : Ordnode α} {x : α} {o₁ : WithBot α} {o₂ : WithTop α} : 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₁ : WithBot α} {o₂ : WithTop α} : t₁.Bounded o₁ ↑x → t₂.Bounded (↑x) o₂ → t₁.Bounded o₁ o₂

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

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

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

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

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