Lemmas for Red-black trees

The main theorem in this file is WF_def, which shows that the RBNode.WF.mk constructor subsumes the others, by showing that insert and erase satisfy the red-black invariants.

theorem Std.RBNode.All.trivial {α : Type u_1} {p : α → Prop} (H : {x : α} → p x) {t : Std.RBNode α} : Std.RBNode.All p t

theorem Std.RBNode.All_and {α : Type u_1} {p : α → Prop} {q : α → Prop} {t : Std.RBNode α} : Std.RBNode.All (fun a => p a ∧ q a) t ↔ Std.RBNode.All p t ∧ Std.RBNode.All q t

theorem Std.RBNode.cmpLT.trans : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y z : α}, Std.RBNode.cmpLT cmp x y → Std.RBNode.cmpLT cmp y z → Std.RBNode.cmpLT cmp x z

theorem Std.RBNode.cmpLT.trans_l {α : Type u_1} {cmp : α → α → Ordering} {x : α} {y : α} (H : Std.RBNode.cmpLT cmp x y) {t : Std.RBNode α} (h : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp y x) t) : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x x) t

theorem Std.RBNode.cmpLT.trans_r {α : Type u_1} {cmp : α → α → Ordering} {x : α} {y : α} (H : Std.RBNode.cmpLT cmp x y) {a : Std.RBNode α} (h : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x x) a) : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x y) a

theorem Std.RBNode.cmpEq.lt_congr_left : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y z : α}, Std.RBNode.cmpEq cmp x y → (Std.RBNode.cmpLT cmp x z ↔ Std.RBNode.cmpLT cmp y z)

theorem Std.RBNode.cmpEq.lt_congr_right : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {y z x : α}, Std.RBNode.cmpEq cmp y z → (Std.RBNode.cmpLT cmp x y ↔ Std.RBNode.cmpLT cmp x z)

theorem Std.RBNode.Ordered.balance1 {α : Type u_1} {cmp : α → α → Ordering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) : Std.RBNode.Ordered cmp (Std.RBNode.balance1 l v r)

The balance1 function preserves the ordering invariants.

@[simp]

theorem Std.RBNode.balance1_All {α : Type u_1} {p : α → Prop} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} : Std.RBNode.All p (Std.RBNode.balance1 l v r) ↔ p v ∧ Std.RBNode.All p l ∧ Std.RBNode.All p r

theorem Std.RBNode.Ordered.balance2 {α : Type u_1} {cmp : α → α → Ordering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) : Std.RBNode.Ordered cmp (Std.RBNode.balance2 l v r)

The balance2 function preserves the ordering invariants.

@[simp]

theorem Std.RBNode.balance2_All {α : Type u_1} {p : α → Prop} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} : Std.RBNode.All p (Std.RBNode.balance2 l v r) ↔ p v ∧ Std.RBNode.All p l ∧ Std.RBNode.All p r

theorem Std.RBNode.Ordered.setBlack {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} : Std.RBNode.Ordered cmp (Std.RBNode.setBlack t) ↔ Std.RBNode.Ordered cmp t

theorem Std.RBNode.Balanced.setBlack : ∀ {α : Type u_1} {t : Std.RBNode α} {c : Std.RBColor} {n : Nat}, Std.RBNode.Balanced t c n → ∃ n', Std.RBNode.Balanced (Std.RBNode.setBlack t) Std.RBColor.black n'

theorem Std.RBNode.setBlack_idem {α : Type u_1} {t : Std.RBNode α} : Std.RBNode.setBlack (Std.RBNode.setBlack t) = Std.RBNode.setBlack t

theorem Std.RBNode.insert_setBlack {α : Type u_1} {cmp : α → α → Ordering} {v : α} {t : Std.RBNode α} : Std.RBNode.setBlack (Std.RBNode.insert cmp t v) = Std.RBNode.setBlack (Std.RBNode.ins cmp v t)

theorem Std.RBNode.All.ins {α : Type u_1} {p : α → Prop} {cmp : α → α → Ordering} {x : α} {t : Std.RBNode α} (h₁ : p x) (h₂ : Std.RBNode.All p t) : Std.RBNode.All p (Std.RBNode.ins cmp x t)

theorem Std.RBNode.Ordered.ins {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : Std.RBNode α} : Std.RBNode.Ordered cmp t → Std.RBNode.Ordered cmp (Std.RBNode.ins cmp x t)

The ins function preserves the ordering invariants.

theorem Std.RBNode.Ordered.insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} {v : α}, Std.RBNode.Ordered cmp t → Std.RBNode.Ordered cmp (Std.RBNode.insert cmp t v)

The insert function preserves the ordering invariants.

inductive Std.RBNode.RedRed (p : Prop) {α : Type u_1} : Std.RBNode α → Nat → Prop

• balanced: ∀ {p : Prop} {x : Type u_1} {t : Std.RBNode x} {c : Std.RBColor} {n : Nat}, Std.RBNode.Balanced t c n → Std.RBNode.RedRed p t n

  A balanced tree has the red-red invariant.

• redred: ∀ {p : Prop} {x : Type u_1} {a : Std.RBNode x} {c₁ : Std.RBColor} {n : Nat} {b : Std.RBNode x} {c₂ : Std.RBColor} {x_1 : x}, p → Std.RBNode.Balanced a c₁ n → Std.RBNode.Balanced b c₂ n → Std.RBNode.RedRed p (Std.RBNode.node Std.RBColor.red a x_1 b) n

  A red node with balanced red children has the red-red invariant (if p is true).

The red-red invariant is a weakening of the red-black balance invariant which allows the root to be red with red children, but does not allow any other violations. It occurs as a temporary condition in the insert and erase functions.

The p parameter allows the .redred case to be dependent on an additional condition. If it is false, then this is equivalent to the usual red-black invariant.

theorem Std.RBNode.RedRed.of_false {p : Prop} : ∀ {α : Type u_1} {t : Std.RBNode α} {n : Nat}, ¬p → Std.RBNode.RedRed p t n → ∃ c, Std.RBNode.Balanced t c n

When p is false, the red-red case is impossible so the tree is balanced.

theorem Std.RBNode.RedRed.of_red {p : Prop} : ∀ {α : Type u_1} {a : Std.RBNode α} {x : α} {b : Std.RBNode α} {n : Nat}, Std.RBNode.RedRed p (Std.RBNode.node Std.RBColor.red a x b) n → ∃ c₁ c₂, Std.RBNode.Balanced a c₁ n ∧ Std.RBNode.Balanced b c₂ n

A red node with the red-red invariant has balanced children.

theorem Std.RBNode.RedRed.imp {p : Prop} {q : Prop} : ∀ {α : Type u_1} {t : Std.RBNode α} {n : Nat}, (p → q) → Std.RBNode.RedRed p t n → Std.RBNode.RedRed q t n

The red-red invariant is monotonic in p.

theorem Std.RBNode.RedRed.setBlack : ∀ {α : Type u_1} {t : Std.RBNode α} {p : Prop} {n : Nat}, Std.RBNode.RedRed p t n → ∃ n', Std.RBNode.Balanced (Std.RBNode.setBlack t) Std.RBColor.black n'

If t has the red-red invariant, then setting the root to black yields a balanced tree.

theorem Std.RBNode.RedRed.balance1 {α : Type u_1} {p : Prop} {n : Nat} {c : Std.RBColor} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (hl : Std.RBNode.RedRed p l n) (hr : Std.RBNode.Balanced r c n) : ∃ c, Std.RBNode.Balanced (Std.RBNode.balance1 l v r) c (n + 1)

The balance1 function repairs the balance invariant when the first argument is red-red.

theorem Std.RBNode.RedRed.balance2 {α : Type u_1} {c : Std.RBColor} {n : Nat} {p : Prop} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (hl : Std.RBNode.Balanced l c n) (hr : Std.RBNode.RedRed p r n) : ∃ c, Std.RBNode.Balanced (Std.RBNode.balance2 l v r) c (n + 1)

The balance2 function repairs the balance invariant when the second argument is red-red.

theorem Std.RBNode.balance1_eq {α : Type u_1} {c : Std.RBColor} {n : Nat} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (hl : Std.RBNode.Balanced l c n) : Std.RBNode.balance1 l v r = Std.RBNode.node Std.RBColor.black l v r

The balance1 function does nothing if the first argument is already balanced.

theorem Std.RBNode.balance2_eq {α : Type u_1} {c : Std.RBColor} {n : Nat} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (hr : Std.RBNode.Balanced r c n) : Std.RBNode.balance2 l v r = Std.RBNode.node Std.RBColor.black l v r

The balance2 function does nothing if the second argument is already balanced.

insert

theorem Std.RBNode.Balanced.ins {α : Type u_1} {c : Std.RBColor} {n : Nat} (cmp : α → α → Ordering) (v : α) {t : Std.RBNode α} (h : Std.RBNode.Balanced t c n) : Std.RBNode.RedRed (Std.RBNode.isRed t = Std.RBColor.red) (Std.RBNode.ins cmp v t) n

The balance invariant of the ins function. The result of inserting into the tree either yields a balanced tree, or a tree which is almost balanced except that it has a red-red violation at the root.

theorem Std.RBNode.Balanced.insert {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : α → α → Ordering} {v : α} {t : Std.RBNode α} (h : Std.RBNode.Balanced t c n) : ∃ c' n', Std.RBNode.Balanced (Std.RBNode.insert cmp t v) c' n'

The insert function is balanced if the input is balanced. (We lose track of both the color and the black-height of the result, so this is only suitable for use on the root of the tree.)

theorem Std.RBNode.All.setRed {α : Type u_1} {p : α → Prop} {t : Std.RBNode α} (h : Std.RBNode.All p t) : Std.RBNode.All p (Std.RBNode.setRed t)

theorem Std.RBNode.Ordered.setRed {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} : Std.RBNode.Ordered cmp (Std.RBNode.setRed t) ↔ Std.RBNode.Ordered cmp t

The setRed function preserves the ordering invariants.

theorem Std.RBNode.All.balLeft : ∀ {α : Type u_1} {p : α → Prop} {l : Std.RBNode α} {v : α} {r : Std.RBNode α}, Std.RBNode.All p l → p v → Std.RBNode.All p r → Std.RBNode.All p (Std.RBNode.balLeft l v r)

theorem Std.RBNode.Ordered.balLeft {α : Type u_1} {cmp : α → α → Ordering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) : Std.RBNode.Ordered cmp (Std.RBNode.balLeft l v r)

The balLeft function preserves the ordering invariants.

theorem Std.RBNode.Balanced.balLeft : ∀ {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} {cr : Std.RBColor} {n : Nat}, Std.RBNode.RedRed True l n → Std.RBNode.Balanced r cr (n + 1) → Std.RBNode.RedRed (cr = Std.RBColor.red) (Std.RBNode.balLeft l v r) (n + 1)

The balancing properties of the balLeft function.

theorem Std.RBNode.All.balRight : ∀ {α : Type u_1} {p : α → Prop} {l : Std.RBNode α} {v : α} {r : Std.RBNode α}, Std.RBNode.All p l → p v → Std.RBNode.All p r → Std.RBNode.All p (Std.RBNode.balRight l v r)

theorem Std.RBNode.Ordered.balRight {α : Type u_1} {cmp : α → α → Ordering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) : Std.RBNode.Ordered cmp (Std.RBNode.balRight l v r)

The balRight function preserves the ordering invariants.

theorem Std.RBNode.Balanced.balRight : ∀ {α : Type u_1} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} {cl : Std.RBColor} {n : Nat}, Std.RBNode.Balanced l cl (n + 1) → Std.RBNode.RedRed True r n → Std.RBNode.RedRed (cl = Std.RBColor.red) (Std.RBNode.balRight l v r) (n + 1)

The balancing properties of the balRight function.

theorem Std.RBNode.All.append : ∀ {α : Type u_1} {l r : Std.RBNode α} {p : α → Prop}, Std.RBNode.All p l → Std.RBNode.All p r → Std.RBNode.All p (Std.RBNode.append l r)

theorem Std.RBNode.Ordered.append {α : Type u_1} {cmp : α → α → Ordering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun x => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) : Std.RBNode.Ordered cmp (Std.RBNode.append l r)

The append function preserves the ordering invariants.

theorem Std.RBNode.Balanced.append {α : Type u_1} {c₁ : Std.RBColor} {n : Nat} {c₂ : Std.RBColor} {l : Std.RBNode α} {r : Std.RBNode α} (hl : Std.RBNode.Balanced l c₁ n) (hr : Std.RBNode.Balanced r c₂ n) : Std.RBNode.RedRed (c₁ = Std.RBColor.black → c₂ ≠ Std.RBColor.black) (Std.RBNode.append l r) n

The balance properties of the append function.

erase

def Std.RBNode.DelProp {α : Type u_1} (p : Std.RBColor) (t : Std.RBNode α) (n : Nat) : Prop

The invariant of the del function.

• If the input tree is black, then the result of deletion is a red-red tree with black-height lowered by 1.
• If the input tree is red or nil, then the result of deletion is a balanced tree with some color and the same black-height.

Equations

• Std.RBNode.DelProp p t n = match p with | Std.RBColor.black => ∃ n', n = n' + 1 ∧ Std.RBNode.RedRed True t n' | Std.RBColor.red => ∃ c, Std.RBNode.Balanced t c n

theorem Std.RBNode.DelProp.redred {c : Std.RBColor} : ∀ {α : Type u_1} {t : Std.RBNode α} {n : Nat}, Std.RBNode.DelProp c t n → ∃ n', Std.RBNode.RedRed (c = Std.RBColor.black) t n'

The DelProp property is a strengthened version of the red-red invariant.

theorem Std.RBNode.All.del {α : Type u_1} {p : α → Prop} {cut : α → Ordering} {t : Std.RBNode α} : Std.RBNode.All p t → Std.RBNode.All p (Std.RBNode.del cut t)

theorem Std.RBNode.Ordered.del {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} : Std.RBNode.Ordered cmp t → Std.RBNode.Ordered cmp (Std.RBNode.del cut t)

The del function preserves the ordering invariants.

theorem Std.RBNode.Balanced.del {α : Type u_1} {c : Std.RBColor} {n : Nat} {cut : α → Ordering} {t : Std.RBNode α} (h : Std.RBNode.Balanced t c n) : Std.RBNode.DelProp (Std.RBNode.isBlack t) (Std.RBNode.del cut t) n

The del function has the DelProp property.

theorem Std.RBNode.Ordered.erase {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t : Std.RBNode α} (h : Std.RBNode.Ordered cmp t) : Std.RBNode.Ordered cmp (Std.RBNode.erase cut t)

The erase function preserves the ordering invariants.

theorem Std.RBNode.Balanced.erase {α : Type u_1} {c : Std.RBColor} {n : Nat} {cut : α → Ordering} {t : Std.RBNode α} (h : Std.RBNode.Balanced t c n) : ∃ n, Std.RBNode.Balanced (Std.RBNode.erase cut t) Std.RBColor.black n

The erase function preserves the balance invariants.

theorem Std.RBNode.WF.out {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} (h : Std.RBNode.WF cmp t) : Std.RBNode.Ordered cmp t ∧ ∃ c n, Std.RBNode.Balanced t c n

The well-formedness invariant implies the ordering and balance properties.

@[simp]

theorem Std.RBNode.WF_iff {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} : Std.RBNode.WF cmp t ↔ Std.RBNode.Ordered cmp t ∧ ∃ c n, Std.RBNode.Balanced t c n

The well-formedness invariant for a red-black tree is exactly the mk constructor, because the other constructors of WF are redundant.

theorem Std.RBNode.Balanced.map {α : Type u_1} {c : Std.RBColor} {n : Nat} : ∀ {α : Type u_2} {f : α → α} {t : Std.RBNode α}, Std.RBNode.Balanced t c n → Std.RBNode.Balanced (Std.RBNode.map f t) c n

The map function preserves the balance invariants.

class Std.RBNode.IsMonotone {α : Sort u_1} {β : Sort u_2} (cmpα : α → α → Ordering) (cmpβ : β → β → Ordering) (f : α → β) : Prop

• lt_mono : ∀ {x y : α}, Std.RBNode.cmpLT cmpα x y → Std.RBNode.cmpLT cmpβ (f x) (f y)

  If x < y then f x < f y.

The property of a map function f which ensures the map operation is valid.

theorem Std.RBNode.All.map {α : Type u_1} {β : Type u_2} {p : α → Prop} {q : β → Prop} {f : α → β} (H : {x : α} → p x → q (f x)) {t : Std.RBNode α} : Std.RBNode.All p t → Std.RBNode.All q (Std.RBNode.map f t)

Sufficient condition for map to preserve an All quantifier.

theorem Std.RBNode.Ordered.map {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} (f : α → β) [Std.RBSet.IsMonotone cmpα cmpβ f] {t : Std.RBNode α} : Std.RBNode.Ordered cmpα t → Std.RBNode.Ordered cmpβ (Std.RBNode.map f t)

The map function preserves the order invariants if f is monotone.

@[inline]

def Std.RBSet.map {α : Type u_1} {β : Type u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} (f : α → β) [Std.RBSet.IsMonotone cmpα cmpβ f] (t : Std.RBSet α cmpα) : Std.RBSet β cmpβ

O(n). Map a function on every value in the tree. This requires IsMonotone on the function in order to preserve the order invariant.

Equations

• Std.RBSet.map f t = { val := Std.RBNode.map f t.val, property := (_ : Std.RBNode.WF cmpβ (Std.RBNode.map f t.val)) }

@[inline]

def Std.RBMap.Imp.mapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) : α × β → α × γ

Applies f to the second component. We extract this as a function so that IsMonotone (mapSnd f) can be an instance.

Equations

• Std.RBMap.Imp.mapSnd f x = match x with | (a, b) => (a, f a b)

instance Std.RBMap.Imp.instIsMonotoneProdProdByKeyFstByKeyFstMapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : α → α → Ordering) (f : α → β → γ) : Std.RBSet.IsMonotone (Std.byKey Prod.fst cmp) (Std.byKey Prod.fst cmp) (Std.RBMap.Imp.mapSnd f)

Equations

• @Std.RBMap.Imp.instIsMonotoneProdProdByKeyFstByKeyFstMapSnd = @Std.RBMap.Imp.instIsMonotoneProdProdByKeyFstByKeyFstMapSnd.proof_1

def Std.RBMap.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : α → α → Ordering} (f : α → β → γ) (t : Std.RBMap α β cmp) : Std.RBMap α γ cmp

O(n). Map a function on the values in the map.

Equations

• Std.RBMap.mapVal f t = Std.RBSet.map (Std.RBMap.Imp.mapSnd f) t