Documentation

Batteries.Data.RBMap.WF

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 : Batteries.RBNode α} :
theorem Batteries.RBNode.All_and {α : Type u_1} {p q : αProp} {t : Batteries.RBNode α} :
theorem Batteries.RBNode.cmpLT.flip {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y : α✝} (h₁ : Batteries.RBNode.cmpLT cmp x y) :
theorem Batteries.RBNode.cmpLT.trans {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y z : α✝} (h₁ : Batteries.RBNode.cmpLT cmp x y) (h₂ : Batteries.RBNode.cmpLT cmp y z) :
theorem Batteries.RBNode.cmpLT.trans_l {α : Type u_1} {cmp : ααOrdering} {x y : α} (H : Batteries.RBNode.cmpLT cmp x y) {t : Batteries.RBNode α} (h : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp y x) t) :
Batteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x x_1) t
theorem Batteries.RBNode.cmpLT.trans_r {α : Type u_1} {cmp : ααOrdering} {x y : α} (H : Batteries.RBNode.cmpLT cmp x y) {a : Batteries.RBNode α} (h : Batteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x_1 x) a) :
Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x y) a
theorem Batteries.RBNode.cmpEq.lt_congr_left {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {x y z : α✝} (H : Batteries.RBNode.cmpEq cmp x y) :
theorem Batteries.RBNode.cmpEq.lt_congr_right {α✝ : Sort u_1} {cmp : α✝α✝Ordering} {y z x : α✝} (H : Batteries.RBNode.cmpEq cmp y z) :
@[simp]
theorem Batteries.RBNode.reverse_reverse {α : Type u_1} (t : Batteries.RBNode α) :
t.reverse.reverse = t
theorem Batteries.RBNode.reverse_eq_iff {α : Type u_1} {t t' : Batteries.RBNode α} :
t.reverse = t' t = t'.reverse
@[simp]
theorem Batteries.RBNode.reverse_balance1 {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balance1 v r).reverse = r.reverse.balance2 v l.reverse
@[simp]
theorem Batteries.RBNode.reverse_balance2 {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balance2 v r).reverse = r.reverse.balance1 v l.reverse
@[simp]
theorem Batteries.RBNode.All.reverse {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} :
theorem Batteries.RBNode.Ordered.reverse {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} :

The reverse function reverses the ordering invariants.

theorem Batteries.RBNode.Balanced.reverse {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {t : Batteries.RBNode α} :
t.Balanced c nt.reverse.Balanced c n
theorem Batteries.RBNode.Ordered.balance1 {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.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 : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
theorem Batteries.RBNode.Ordered.balance2 {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.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 : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
@[simp]
theorem Batteries.RBNode.reverse_setBlack {α : Type u_1} {t : Batteries.RBNode α} :
t.setBlack.reverse = t.reverse.setBlack
theorem Batteries.RBNode.Balanced.setBlack {α✝ : Type u_1} {t : Batteries.RBNode α✝} {c : Batteries.RBColor} {n : Nat} :
t.Balanced c n∃ (n' : Nat), t.setBlack.Balanced Batteries.RBColor.black n'
theorem Batteries.RBNode.setBlack_idem {α : Type u_1} {t : Batteries.RBNode α} :
t.setBlack.setBlack = t.setBlack
@[simp]
theorem Batteries.RBNode.reverse_ins {α : Type u_1} {cmp : ααOrdering} {x : α} [inst : Batteries.OrientedCmp cmp] {t : Batteries.RBNode α} :
(Batteries.RBNode.ins cmp x t).reverse = Batteries.RBNode.ins (flip cmp) x t.reverse
theorem Batteries.RBNode.All.ins {α : Type u_1} {p : αProp} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α} (h₁ : p x) (h₂ : Batteries.RBNode.All p t) :
theorem Batteries.RBNode.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α} :

The ins function preserves the ordering invariants.

@[simp]
theorem Batteries.RBNode.isRed_reverse {α : Type u_1} {t : Batteries.RBNode α} :
t.reverse.isRed = t.isRed
@[simp]
theorem Batteries.RBNode.reverse_insert {α : Type u_1} {cmp : ααOrdering} {x : α} [inst : Batteries.OrientedCmp cmp] {t : Batteries.RBNode α} :
(Batteries.RBNode.insert cmp t x).reverse = Batteries.RBNode.insert (flip cmp) t.reverse x
theorem Batteries.RBNode.insert_setBlack {α : Type u_1} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} :
(Batteries.RBNode.insert cmp t v).setBlack = (Batteries.RBNode.ins cmp v t).setBlack
theorem Batteries.RBNode.Ordered.insert {α✝ : Type u_1} {cmp : α✝α✝Ordering} {t : Batteries.RBNode α✝} {v : α✝} (h : Batteries.RBNode.Ordered cmp t) :

The insert function preserves the ordering invariants.

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

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 Batteries.RBNode.RedRed.of_false {p : Prop} {α✝ : Type u_1} {t : Batteries.RBNode α✝} {n : Nat} (h : ¬p) :
Batteries.RBNode.RedRed p t n∃ (c : Batteries.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 : Batteries.RBNode α✝} {x : α✝} {b : Batteries.RBNode α✝} {n : Nat} :
Batteries.RBNode.RedRed p (Batteries.RBNode.node Batteries.RBColor.red a x b) n∃ (c₁ : Batteries.RBColor), ∃ (c₂ : Batteries.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 : Batteries.RBNode α✝} {n : Nat} (h : pq) :

The red-red invariant is monotonic in p.

theorem Batteries.RBNode.RedRed.reverse {p : Prop} {α✝ : Type u_1} {t : Batteries.RBNode α✝} {n : Nat} :
theorem Batteries.RBNode.RedRed.setBlack {α✝ : Type u_1} {t : Batteries.RBNode α✝} {p : Prop} {n : Nat} :
Batteries.RBNode.RedRed p t n∃ (n' : Nat), t.setBlack.Balanced Batteries.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 : Batteries.RBColor} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : Batteries.RBNode.RedRed p l n) (hr : r.Balanced c n) :
∃ (c : Batteries.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 : Batteries.RBColor} {n : Nat} {p : Prop} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : l.Balanced c n) (hr : Batteries.RBNode.RedRed p r n) :
∃ (c : Batteries.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 : Batteries.RBColor} {n : Nat} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : l.Balanced c n) :

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

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

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

insert #

theorem Batteries.RBNode.Balanced.ins {α : Type u_1} {c : Batteries.RBColor} {n : Nat} (cmp : ααOrdering) (v : α) {t : Batteries.RBNode α} (h : t.Balanced c 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 : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} (h : t.Balanced c n) :
∃ (c' : Batteries.RBColor), ∃ (n' : Nat), (Batteries.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 : Batteries.RBNode α} :
t.setRed.reverse = t.reverse.setRed
theorem Batteries.RBNode.All.setRed {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} (h : Batteries.RBNode.All p t) :
theorem Batteries.RBNode.Ordered.setRed {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} :

The setRed function preserves the ordering invariants.

@[simp]
theorem Batteries.RBNode.reverse_balLeft {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balLeft v r).reverse = r.reverse.balRight v l.reverse
@[simp]
theorem Batteries.RBNode.reverse_balRight {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balRight v r).reverse = r.reverse.balLeft v l.reverse
theorem Batteries.RBNode.All.balLeft {α✝ : Type u_1} {p : α✝Prop} {l : Batteries.RBNode α✝} {v : α✝} {r : Batteries.RBNode α✝} (hl : Batteries.RBNode.All p l) (hv : p v) (hr : Batteries.RBNode.All p r) :
Batteries.RBNode.All p (l.balLeft v r)
theorem Batteries.RBNode.Ordered.balLeft {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.Ordered cmp (l.balLeft v r)

The balLeft function preserves the ordering invariants.

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

The balancing properties of the balLeft function.

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

The balRight function preserves the ordering invariants.

theorem Batteries.RBNode.Balanced.balRight {α✝ : Type u_1} {l : Batteries.RBNode α✝} {v : α✝} {r : Batteries.RBNode α✝} {cl : Batteries.RBColor} {n : Nat} (hl : l.Balanced cl (n + 1)) (hr : Batteries.RBNode.RedRed True r n) :
Batteries.RBNode.RedRed (cl = Batteries.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 : Batteries.RBNode α✝} {p : α✝Prop} (hl : Batteries.RBNode.All p l) (hr : Batteries.RBNode.All p r) :
Batteries.RBNode.All p (l.append r)
@[irreducible]
theorem Batteries.RBNode.Ordered.append {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.Ordered cmp (l.append r)

The append function preserves the ordering invariants.

@[irreducible]
theorem Batteries.RBNode.Balanced.append {α : Type u_1} {c₁ : Batteries.RBColor} {n : Nat} {c₂ : Batteries.RBColor} {l r : Batteries.RBNode α} (hl : l.Balanced c₁ n) (hr : r.Balanced c₂ n) :

The balance properties of the append function.

erase #

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

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 : Batteries.RBNode α} :
theorem Batteries.RBNode.Ordered.del {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} :

The del function preserves the ordering invariants.

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

The del function has the DelProp property.

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

The erase function preserves the ordering invariants.

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

The erase function preserves the balance invariants.

theorem Batteries.RBNode.WF.out {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} (h : Batteries.RBNode.WF cmp t) :
Batteries.RBNode.Ordered cmp t ∃ (c : Batteries.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 : Batteries.RBNode α} :
Batteries.RBNode.WF cmp t Batteries.RBNode.Ordered cmp t ∃ (c : Batteries.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 : Batteries.RBColor} {n : Nat} {α✝ : Type u_2} {f : αα✝} {t : Batteries.RBNode α} :
t.Balanced c n(Batteries.RBNode.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 : αβ) :

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

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

    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 : αβ) [Batteries.RBSet.IsMonotone cmpα cmpβ f] {t : Batteries.RBNode α} :

    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 : αβ) [Batteries.RBSet.IsMonotone cmpα cmpβ f] (t : Batteries.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
    @[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
    theorem Batteries.RBMap.Imp.instIsMonotoneProdByKeyFstMapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : ααOrdering) (f : αβγ) :
    def Batteries.RBMap.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : ααOrdering} (f : αβγ) (t : Batteries.RBMap α β cmp) :
    Batteries.RBMap α γ cmp

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

    Equations