# Documentation

Std.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 Std.RBNode.All.trivial {α : Type u_1} {p : αProp} (H : {x : α} → p x) {t : } :
theorem Std.RBNode.All_and {α : Type u_1} {p : αProp} {q : αProp} {t : } :
Std.RBNode.All (fun a => p a q a) t
theorem Std.RBNode.cmpLT.trans :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y z : α}, Std.RBNode.cmpLT cmp x yStd.RBNode.cmpLT cmp y zStd.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 : } (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 : } (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 : } {v : α} {r : } (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 : ) (hr : ) :

The balance1 function preserves the ordering invariants.

@[simp]
theorem Std.RBNode.balance1_All {α : Type u_1} {p : αProp} {l : } {v : α} {r : } :
theorem Std.RBNode.Ordered.balance2 {α : Type u_1} {cmp : ααOrdering} {l : } {v : α} {r : } (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 : ) (hr : ) :

The balance2 function preserves the ordering invariants.

@[simp]
theorem Std.RBNode.balance2_All {α : Type u_1} {p : αProp} {l : } {v : α} {r : } :
theorem Std.RBNode.Ordered.setBlack {α : Type u_1} {cmp : ααOrdering} {t : } :
theorem Std.RBNode.Balanced.setBlack :
∀ {α : Type u_1} {t : } {c : Std.RBColor} {n : Nat},
theorem Std.RBNode.setBlack_idem {α : Type u_1} {t : } :
theorem Std.RBNode.insert_setBlack {α : Type u_1} {cmp : ααOrdering} {v : α} {t : } :
theorem Std.RBNode.All.ins {α : Type u_1} {p : αProp} {cmp : ααOrdering} {x : α} {t : } (h₁ : p x) (h₂ : ) :
theorem Std.RBNode.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {x : α} {t : } :

The ins function preserves the ordering invariants.

theorem Std.RBNode.Ordered.insert :
∀ {α : Type u_1} {cmp : ααOrdering} {t : } {v : α}, 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} :
• balanced: ∀ {p : Prop} {x : Type u_1} {t : } {c : Std.RBColor} {n : Nat},

A balanced tree has the red-red invariant.

• redred: ∀ {p : Prop} {x : Type u_1} {a : } {c₁ : Std.RBColor} {n : Nat} {b : } {c₂ : Std.RBColor} {x_1 : x}, pStd.RBNode.RedRed p () 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.

Instances For
theorem Std.RBNode.RedRed.of_false {p : Prop} :
∀ {α : Type u_1} {t : } {n : Nat}, ¬pc,

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 : } {x : α} {b : } {n : Nat}, c₁ c₂,

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

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

The red-red invariant is monotonic in p.

theorem Std.RBNode.RedRed.setBlack :
∀ {α : Type u_1} {t : } {p : Prop} {n : Nat},

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 : } {v : α} {r : } (hl : ) (hr : ) :
c, Std.RBNode.Balanced () 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 : } {v : α} {r : } (hl : ) (hr : ) :
c, Std.RBNode.Balanced () 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 : } {v : α} {r : } (hl : ) :
=

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 : } {v : α} {r : } (hr : ) :
=

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 : } (h : ) :

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 : } (h : ) :
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 : } (h : ) :
theorem Std.RBNode.Ordered.setRed {α : Type u_1} {cmp : ααOrdering} {t : } :

The setRed function preserves the ordering invariants.

theorem Std.RBNode.All.balLeft :
∀ {α : Type u_1} {p : αProp} {l : } {v : α} {r : }, p vStd.RBNode.All p ()
theorem Std.RBNode.Ordered.balLeft {α : Type u_1} {cmp : ααOrdering} {l : } {v : α} {r : } (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 : ) (hr : ) :

The balLeft function preserves the ordering invariants.

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

The balancing properties of the balLeft function.

theorem Std.RBNode.All.balRight :
∀ {α : Type u_1} {p : αProp} {l : } {v : α} {r : }, p vStd.RBNode.All p ()
theorem Std.RBNode.Ordered.balRight {α : Type u_1} {cmp : ααOrdering} {l : } {v : α} {r : } (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 : ) (hr : ) :

The balRight function preserves the ordering invariants.

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

The balancing properties of the balRight function.

theorem Std.RBNode.All.append :
∀ {α : Type u_1} {l r : } {p : αProp},
theorem Std.RBNode.Ordered.append {α : Type u_1} {cmp : ααOrdering} {l : } {v : α} {r : } (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 : ) (hr : ) :

The append function preserves the ordering invariants.

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

The balance properties of the append function.

## erase #

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

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.
Instances For
theorem Std.RBNode.DelProp.redred {c : Std.RBColor} :
∀ {α : Type u_1} {t : } {n : Nat}, 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 : } :
theorem Std.RBNode.Ordered.del {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : } :

The del function preserves the ordering invariants.

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

The del function has the DelProp property.

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

The erase function preserves the ordering invariants.

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

The erase function preserves the balance invariants.

theorem Std.RBNode.WF.out {α : Type u_1} {cmp : ααOrdering} {t : } (h : Std.RBNode.WF cmp 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.WF cmp 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 : },

The map function preserves the balance invariants.

class Std.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 Std.RBNode.All.map {α : Type u_1} {β : Type u_2} {p : αProp} {q : βProp} {f : αβ} (H : {x : α} → p xq (f x)) {t : } :
Std.RBNode.All q ()

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 : } :

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.

Instances For
@[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.

Instances For
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) ()
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.

Instances For