RBNode depth bounds

def Batteries.RBNode.depth {α : Type u_1} : 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 : RBNode α) : t.size < 2 ^ t.depth

def Batteries.RBNode.depthLB : 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 Batteries.RBColor.red x✝ = x✝ + 1
• Batteries.RBNode.depthLB Batteries.RBColor.black x✝ = x✝

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

def Batteries.RBNode.depthUB : 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 Batteries.RBColor.red x✝ = 2 * x✝ + 1
• Batteries.RBNode.depthUB Batteries.RBColor.black x✝ = 2 * x✝

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

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

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

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

theorem Batteries.RBNode.Balanced.depth_bound {α : Type u_1} {t : RBNode α} {c : 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 : RBNode α} (h : 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.