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 Batteries.RBNode.All.trivial {α : Type u_1} {p : α → Prop} (H : ∀ {x : α}, p x) {t : RBNode α} : All p t

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

theorem Batteries.RBNode.cmpLT.flip {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y : α✝} (h₁ : cmpLT cmp x y) : cmpLT (flip cmp) y x

theorem Batteries.RBNode.cmpLT.trans {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y z : α✝} (h₁ : cmpLT cmp x y) (h₂ : cmpLT cmp y z) : cmpLT cmp x z

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

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

theorem Batteries.RBNode.cmpEq.lt_congr_left {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {x y z : α✝} (H : cmpEq cmp x y) : cmpLT cmp x z ↔ cmpLT cmp y z

theorem Batteries.RBNode.cmpEq.lt_congr_right {α✝ : Sort u_1} {cmp : α✝ → α✝ → Ordering} {y z x : α✝} (H : cmpEq cmp y z) : cmpLT cmp x y ↔ cmpLT cmp x z

@[simp]

theorem Batteries.RBNode.reverse_reverse {α : Type u_1} (t : RBNode α) : t.reverse.reverse = t

theorem Batteries.RBNode.reverse_eq_iff {α : Type u_1} {t t' : RBNode α} : t.reverse = t' ↔ t = t'.reverse

@[simp]

theorem Batteries.RBNode.reverse_balance1 {α : Type u_1} (l : RBNode α) (v : α) (r : RBNode α) : (l.balance1 v r).reverse = r.reverse.balance2 v l.reverse

@[simp]

theorem Batteries.RBNode.reverse_balance2 {α : Type u_1} (l : RBNode α) (v : α) (r : RBNode α) : (l.balance2 v r).reverse = r.reverse.balance1 v l.reverse

@[simp]

theorem Batteries.RBNode.All.reverse {α : Type u_1} {p : α → Prop} {t : RBNode α} : All p t.reverse ↔ All p t

theorem Batteries.RBNode.Ordered.reverse {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} : Ordered cmp t → Ordered (flip cmp) t.reverse

The reverse function reverses the ordering invariants.

theorem Batteries.RBNode.Balanced.reverse {α : Type u_1} {c : RBColor} {n : Nat} {t : RBNode α} : t.Balanced c n → t.reverse.Balanced c n

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

The balance1 function preserves the ordering invariants.

@[simp]

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

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

The balance2 function preserves the ordering invariants.

@[simp]

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

@[simp]

theorem Batteries.RBNode.reverse_setBlack {α : Type u_1} {t : RBNode α} : t.setBlack.reverse = t.reverse.setBlack

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

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

theorem Batteries.RBNode.setBlack_idem {α : Type u_1} {t : RBNode α} : t.setBlack.setBlack = t.setBlack

@[simp]

theorem Batteries.RBNode.reverse_ins {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : OrientedCmp cmp] {t : RBNode α} : (ins cmp x t).reverse = ins (flip cmp) x t.reverse

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

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

The ins function preserves the ordering invariants.

@[simp]

theorem Batteries.RBNode.isRed_reverse {α : Type u_1} {t : RBNode α} : t.reverse.isRed = t.isRed

@[simp]

theorem Batteries.RBNode.reverse_insert {α : Type u_1} {cmp : α → α → Ordering} {x : α} [inst : OrientedCmp cmp] {t : RBNode α} : (insert cmp t x).reverse = insert (flip cmp) t.reverse x

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

theorem Batteries.RBNode.Ordered.insert {α✝ : Type u_1} {cmp : α✝ → α✝ → Ordering} {t : RBNode α✝} {v : α✝} (h : Ordered cmp t) : Ordered cmp (insert cmp t v)

The insert function preserves the ordering invariants.

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

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.

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

  A balanced tree has the red-red invariant.

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

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

theorem Batteries.RBNode.RedRed.of_false {p : Prop} {α✝ : Type u_1} {t : RBNode α✝} {n : Nat} (h : ¬p) : RedRed p t n → ∃ (c : RBColor), t.Balanced c n

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

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

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

theorem Batteries.RBNode.RedRed.imp {p q : Prop} {α✝ : Type u_1} {t : RBNode α✝} {n : Nat} (h : p → q) : RedRed p t n → RedRed q t n

The red-red invariant is monotonic in p.

theorem Batteries.RBNode.RedRed.reverse {p : Prop} {α✝ : Type u_1} {t : RBNode α✝} {n : Nat} : RedRed p t n → RedRed p t.reverse n

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

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

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

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

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

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

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

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

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

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

insert

theorem Batteries.RBNode.Balanced.ins {α : Type u_1} {c : RBColor} {n : Nat} (cmp : α → α → Ordering) (v : α) {t : RBNode α} (h : t.Balanced c n) : RedRed (t.isRed = RBColor.red) (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 Batteries.RBNode.Balanced.insert {α : Type u_1} {c : RBColor} {n : Nat} {cmp : α → α → Ordering} {v : α} {t : RBNode α} (h : t.Balanced c n) : ∃ (c' : RBColor), ∃ (n' : Nat), (RBNode.insert cmp t v).Balanced 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.)

@[simp]

theorem Batteries.RBNode.reverse_setRed {α : Type u_1} {t : RBNode α} : t.setRed.reverse = t.reverse.setRed

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

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

The setRed function preserves the ordering invariants.

@[simp]

theorem Batteries.RBNode.reverse_balLeft {α : Type u_1} (l : RBNode α) (v : α) (r : RBNode α) : (l.balLeft v r).reverse = r.reverse.balRight v l.reverse

@[simp]

theorem Batteries.RBNode.reverse_balRight {α : Type u_1} (l : RBNode α) (v : α) (r : RBNode α) : (l.balRight v r).reverse = r.reverse.balLeft v l.reverse

theorem Batteries.RBNode.All.balLeft {α✝ : Type u_1} {p : α✝ → Prop} {l : RBNode α✝} {v : α✝} {r : RBNode α✝} (hl : All p l) (hv : p v) (hr : All p r) : All p (l.balLeft v r)

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

The balLeft function preserves the ordering invariants.

theorem Batteries.RBNode.Balanced.balLeft {α✝ : Type u_1} {l : RBNode α✝} {v : α✝} {r : RBNode α✝} {cr : RBColor} {n : Nat} (hl : RedRed True l n) (hr : r.Balanced cr (n + 1)) : RedRed (cr = RBColor.red) (l.balLeft v r) (n + 1)

The balancing properties of the balLeft function.

theorem Batteries.RBNode.All.balRight {α✝ : Type u_1} {p : α✝ → Prop} {l : RBNode α✝} {v : α✝} {r : RBNode α✝} (hl : All p l) (hv : p v) (hr : All p r) : All p (l.balRight v r)

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

The balRight function preserves the ordering invariants.

theorem Batteries.RBNode.Balanced.balRight {α✝ : Type u_1} {l : RBNode α✝} {v : α✝} {r : RBNode α✝} {cl : RBColor} {n : Nat} (hl : l.Balanced cl (n + 1)) (hr : RedRed True r n) : RedRed (cl = RBColor.red) (l.balRight v r) (n + 1)

The balancing properties of the balRight function.

@[irreducible]

theorem Batteries.RBNode.All.append {α✝ : Type u_1} {l r : RBNode α✝} {p : α✝ → Prop} (hl : All p l) (hr : All p r) : All p (l.append r)

@[irreducible]

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

The append function preserves the ordering invariants.

@[irreducible]

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

The balance properties of the append function.

erase

def Batteries.RBNode.DelProp {α : Type u_1} (p : RBColor) (t : 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

• Batteries.RBNode.DelProp Batteries.RBColor.black t n = ∃ (n' : Nat), n = n' + 1 ∧ Batteries.RBNode.RedRed True t n'
• Batteries.RBNode.DelProp Batteries.RBColor.red t n = ∃ (c : Batteries.RBColor), t.Balanced c n

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

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

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

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

The del function preserves the ordering invariants.

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

The del function has the DelProp property.

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

The erase function preserves the ordering invariants.

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

The erase function preserves the balance invariants.

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

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

@[simp]

theorem Batteries.RBNode.WF_iff {α : Type u_1} {cmp : α → α → Ordering} {t : RBNode α} : WF cmp t ↔ Ordered cmp t ∧ ∃ (c : RBColor), ∃ (n : Nat), t.Balanced 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 Batteries.RBNode.Balanced.map {α : Type u_1} {c : RBColor} {n : Nat} {α✝ : Type u_2} {f : α → α✝} {t : RBNode α} : t.Balanced c n → (map f t).Balanced c n

The map function preserves the balance invariants.

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

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

• lt_mono {x y : α} : cmpLT cmpα x y → cmpLT cmpβ (f x) (f y)

  If x < y then f x < f y.

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

Sufficient condition for map to preserve an All quantifier.

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

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

@[inline]

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

O(n). Map a function on every value in the set. This requires IsMonotone on the function in order to preserve the order invariant. If the function is not monotone, use RBSet.map instead.

Equations

• Batteries.RBSet.mapMonotone f t = ⟨Batteries.RBNode.map f t.val, ⋯⟩

@[inline]

def Batteries.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

• Batteries.RBMap.Imp.mapSnd f (a, b) = (a, f a b)

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

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

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

Equations

• Batteries.RBMap.mapVal f t = Batteries.RBSet.mapMonotone (Batteries.RBMap.Imp.mapSnd f) t