RBNode depth bounds

def Batteries.RBNode.depth {α : Type u_1} : Batteries.RBNode α → Nat

O(n). depth t is the maximum number of nodes on any path to a leaf. It is an upper bound on most tree operations.

Equations

• Batteries.RBNode.nil.depth = 0
• (Batteries.RBNode.node c a v b).depth = max a.depth b.depth + 1

theorem Batteries.RBNode.size_lt_depth {α : Type u_1} (t : Batteries.RBNode α) : t.size < 2 ^ t.depth

def Batteries.RBNode.depthLB : Batteries.RBColor → Nat → Nat

depthLB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Equations

• Batteries.RBNode.depthLB x✝ x = match x✝, x with | Batteries.RBColor.red, n => n + 1 | Batteries.RBColor.black, n => n

theorem Batteries.RBNode.depthLB_le (c : Batteries.RBColor) (n : Nat) : n ≤ Batteries.RBNode.depthLB c n

def Batteries.RBNode.depthUB : Batteries.RBColor → Nat → Nat

depthUB c n is the best upper bound on the depth of any balanced red-black tree with root colored c and black-height n.

Equations

• Batteries.RBNode.depthUB x✝ x = match x✝, x with | Batteries.RBColor.red, n => 2 * n + 1 | Batteries.RBColor.black, n => 2 * n

theorem Batteries.RBNode.depthUB_le (c : Batteries.RBColor) (n : Nat) : Batteries.RBNode.depthUB c n ≤ 2 * n + 1

theorem Batteries.RBNode.depthUB_le_two_depthLB (c : Batteries.RBColor) (n : Nat) : Batteries.RBNode.depthUB c n ≤ 2 * Batteries.RBNode.depthLB c n

theorem Batteries.RBNode.Balanced.depth_le {α : Type u_1} {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : Nat} : t.Balanced c n → t.depth ≤ Batteries.RBNode.depthUB c n

theorem Batteries.RBNode.Balanced.le_size {α : Type u_1} {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : Nat} : t.Balanced c n → 2 ^ Batteries.RBNode.depthLB c n ≤ t.size + 1

theorem Batteries.RBNode.Balanced.depth_bound {α : Type u_1} {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : Nat} (h : t.Balanced c n) : t.depth ≤ 2 * (t.size + 1).log2

theorem Batteries.RBNode.WF.depth_bound {α : Type u_1} {cmp : α → α → Ordering} {t : Batteries.RBNode α} (h : Batteries.RBNode.WF cmp t) : t.depth ≤ 2 * (t.size + 1).log2

A well formed tree has t.depth ∈ O(log t.size), that is, it is well balanced. This justifies the O(log n) bounds on most searching operations of RBSet.