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 α} : Batteries.RBNode.All p t

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

theorem Batteries.RBNode.cmpLT.flip : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y : α}, Batteries.RBNode.cmpLT cmp x y → Batteries.RBNode.cmpLT (flip cmp) y x

theorem Batteries.RBNode.cmpLT.trans : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {x y z : α}, Batteries.RBNode.cmpLT cmp x y → Batteries.RBNode.cmpLT cmp y z → Batteries.RBNode.cmpLT cmp x 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 : α}, Batteries.RBNode.cmpEq cmp x y → (Batteries.RBNode.cmpLT cmp x z ↔ Batteries.RBNode.cmpLT cmp y z)

theorem Batteries.RBNode.cmpEq.lt_congr_right : ∀ {α : Sort u_1} {cmp : α → α → Ordering} {y z x : α}, Batteries.RBNode.cmpEq cmp y z → (Batteries.RBNode.cmpLT cmp x y ↔ Batteries.RBNode.cmpLT cmp x 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 : Batteries.RBNode α} {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 α} : Batteries.RBNode.All p t.reverse ↔ Batteries.RBNode.All p t

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

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 n → t.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 α} : Batteries.RBNode.All p (l.balance1 v r) ↔ p v ∧ Batteries.RBNode.All p l ∧ Batteries.RBNode.All p r

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 α} : Batteries.RBNode.All p (l.balance2 v r) ↔ p v ∧ Batteries.RBNode.All p l ∧ Batteries.RBNode.All p r

@[simp]

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

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

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) : Batteries.RBNode.All p (Batteries.RBNode.ins cmp x t)

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

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 : α}, Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Ordered cmp (Batteries.RBNode.insert cmp t v)

The insert function preserves the ordering invariants.

inductive Batteries.RBNode.RedRed (p : Prop) {α : Type u_1} : Batteries.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 : Batteries.RBNode x} {c : Batteries.RBColor} {n : Nat}, t.Balanced c n → Batteries.RBNode.RedRed p t n

  A balanced tree has the red-red invariant.

• redred: ∀ {p : Prop} {x : Type u_1} {a : Batteries.RBNode x} {c₁ : Batteries.RBColor} {n : Nat} {b : Batteries.RBNode x} {c₂ : Batteries.RBColor} {x_1 : x}, p → a.Balanced c₁ n → b.Balanced c₂ n → Batteries.RBNode.RedRed p (Batteries.RBNode.node Batteries.RBColor.red a x_1 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 : Batteries.RBNode α} {n : Nat}, ¬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 : Prop} {q : Prop} : ∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, (p → q) → Batteries.RBNode.RedRed p t n → Batteries.RBNode.RedRed q t n

The red-red invariant is monotonic in p.

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

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) : l.balance1 v r = Batteries.RBNode.node Batteries.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 : Batteries.RBColor} {n : Nat} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hr : r.Balanced c n) : l.balance2 v r = Batteries.RBNode.node Batteries.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 : Batteries.RBColor} {n : Nat} (cmp : α → α → Ordering) (v : α) {t : Batteries.RBNode α} (h : t.Balanced c n) : Batteries.RBNode.RedRed (t.isRed = Batteries.RBColor.red) (Batteries.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 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) : Batteries.RBNode.All p t.setRed

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

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 α}, Batteries.RBNode.All p l → p v → 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}, Batteries.RBNode.RedRed True l n → r.Balanced cr (n + 1) → Batteries.RBNode.RedRed (cr = Batteries.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 : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α}, Batteries.RBNode.All p l → p v → 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}, l.Balanced cl (n + 1) → 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}, Batteries.RBNode.All p l → 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 : Batteries.RBNode α} {r : Batteries.RBNode α} (hl : l.Balanced c₁ n) (hr : r.Balanced c₂ n) : Batteries.RBNode.RedRed (c₁ = Batteries.RBColor.black → c₂ ≠ Batteries.RBColor.black) (l.append r) n

The balance properties of the append function.

erase

def Batteries.RBNode.DelProp {α : Type u_1} (p : Batteries.RBColor) (t : Batteries.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 : Batteries.RBColor} : ∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.DelProp c t n → ∃ (n' : Nat), Batteries.RBNode.RedRed (c = Batteries.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 : Batteries.RBNode α} : Batteries.RBNode.All p t → Batteries.RBNode.All p (Batteries.RBNode.del cut t)

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

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) : Batteries.RBNode.DelProp t.isBlack (Batteries.RBNode.del cut t) 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) : Batteries.RBNode.Ordered cmp (Batteries.RBNode.erase cut 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} : ∀ {α_1 : Type u_2} {f : α → α_1} {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 : α → β) : Prop

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

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

  If x < y then f x < f y.

theorem Batteries.RBNode.IsMonotone.lt_mono {α : Sort u_1} {β : Sort u_2} {cmpα : α → α → Ordering} {cmpβ : β → β → Ordering} {f : α → β} [self : Batteries.RBSet.IsMonotone cmpα cmpβ f] {x : α} {y : α} : Batteries.RBNode.cmpLT cmpα x y → Batteries.RBNode.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 : Batteries.RBNode α} : Batteries.RBNode.All p t → Batteries.RBNode.All q (Batteries.RBNode.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 : α → β) [Batteries.RBSet.IsMonotone cmpα cmpβ f] {t : Batteries.RBNode α} : Batteries.RBNode.Ordered cmpα t → Batteries.RBNode.Ordered cmpβ (Batteries.RBNode.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 : α → β) [Batteries.RBSet.IsMonotone cmpα cmpβ f] (t : Batteries.RBSet α cmpα) : 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

• 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 : α → β → γ) : Batteries.RBSet.IsMonotone (Ordering.byKey Prod.fst cmp) (Ordering.byKey Prod.fst cmp) (Batteries.RBMap.Imp.mapSnd f)

Equations

• ⋯ = ⋯

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

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