# Documentation

Std.Data.RBMap.Alter

# Path operations; modify and alter#

This develops the necessary theorems to construct the modify and alter functions on RBSet using path operations for in-place modification of an RBTree.

## path balance #

def Std.RBNode.OnRoot {α : Type u_1} (p : αProp) :

Asserts that property p holds on the root of the tree, if any.

Equations
def Std.RBNode.setRoot {α : Type u_1} (v : α) :

Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

Equations
def Std.RBNode.delRoot {α : Type u_1} :

Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

Equations
• = match x with | Std.RBNode.nil => Std.RBNode.nil | Std.RBNode.node c a v b =>
@[inline]
def Std.RBNode.Path.fill' {α : Type u_1} :

Same as fill but taking its arguments in a pair for easier composition with zoom.

Equations
theorem Std.RBNode.Path.zoom_fill' {α : Type u_1} (cut : αOrdering) (t : ) (path : ) :
theorem Std.RBNode.Path.zoom_fill :
∀ {α : Type u_1} {cut : αOrdering} {t : } {path : } {t' : } {path' : }, Std.RBNode.zoom cut t path = (t', path')Std.RBNode.Path.fill path t = Std.RBNode.Path.fill path' t'
theorem Std.RBNode.Path.zoom_ins {α : Type u_1} {v : α} {path : } {t' : } {path' : } {t : } {cmp : ααOrdering} :
Std.RBNode.zoom (cmp v) t path = (t', path')Std.RBNode.Path.ins path (Std.RBNode.ins cmp v t) = Std.RBNode.Path.ins path' ()
theorem Std.RBNode.Path.insertNew_eq_insert :
∀ {α : Type u_1} {cmp : ααOrdering} {t : } {path : } {v : α}, Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, path) = Std.RBNode.setBlack (Std.RBNode.insert cmp t v)
theorem Std.RBNode.Path.zoom_del {α : Type u_1} {cut : αOrdering} {path : } {t' : } {path' : } {t : } :
Std.RBNode.zoom cut t path = (t', path')Std.RBNode.Path.del path (Std.RBNode.del cut t) (match t with | Std.RBNode.node c l v r => c | x => Std.RBColor.red) = Std.RBNode.Path.del path' () (match t' with | Std.RBNode.node c l v r => c | x => Std.RBColor.red)
inductive Std.RBNode.Path.Balanced (c₀ : Std.RBColor) (n₀ : Nat) {α : Type u_1} :

The balance invariant for a path. path.Balanced c₀ n₀ c n means that path is a red-black tree with balance invariant c₀, n₀, but it has a "hole" where a tree with balance invariant c, n has been removed. The defining property is Balanced.fill: if path.Balanced c₀ n₀ c n and you fill the hole with a tree satisfying t.Balanced c n, then (path.fill t).Balanced c₀ n₀ .

Instances For
theorem Std.RBNode.Path.Balanced.fill {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {path : } {t : } :
Std.RBNode.Path.Balanced c₀ n₀ path c nStd.RBNode.Balanced (Std.RBNode.Path.fill path t) c₀ n₀

The defining property of a balanced path: If path is a c₀,n₀ tree with a c,n hole, then filling the hole with a c,n tree yields a c₀,n₀ tree.

theorem Std.RBNode.Balanced.zoom :
∀ {α : Type u_1} {cut : αOrdering} {t : } {path : } {t' : } {path' : } {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat}, Std.RBNode.Path.Balanced c₀ n₀ path c nStd.RBNode.zoom cut t path = (t', path')c n, Std.RBNode.Path.Balanced c₀ n₀ path' c n
theorem Std.RBNode.Path.ins_eq_fill {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {path : } {t : } :
Std.RBNode.Path.Balanced c₀ n₀ path c nStd.RBNode.Path.ins path t =
theorem Std.RBNode.Path.Balanced.ins {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {t : } {path : } (hp : Std.RBNode.Path.Balanced c₀ n₀ path c n) (ht : ) :
n,
theorem Std.RBNode.Path.Balanced.insertNew {α : Type u_1} {c : Std.RBColor} {n : Nat} {v : α} {path : } (H : ) :
n,
theorem Std.RBNode.Path.Balanced.insert {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {t : } {v : α} {path : } (hp : Std.RBNode.Path.Balanced c₀ n₀ path c n) :
c n, Std.RBNode.Balanced (Std.RBNode.Path.insert path t v) c n
theorem Std.RBNode.Path.zoom_insert {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {t' : } {v : α} {path : } {t : } (ht : ) (H : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (t', path)) :
theorem Std.RBNode.Path.Balanced.del {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {c' : Std.RBColor} {t : } {path : } (hp : Std.RBNode.Path.Balanced c₀ n₀ path c n) (ht : ) (hc : ) :
n,
def Std.RBNode.Path.AllL {α : Type u_1} (p : αProp) :

Asserts that p holds on all elements to the left of the hole.

Equations
def Std.RBNode.Path.AllR {α : Type u_1} (p : αProp) :

Asserts that p holds on all elements to the right of the hole.

Equations
def Std.RBNode.Path.Zoomed {α : Type u_1} (cut : αOrdering) :

The property of a path returned by t.zoom cut. Each of the parents visited along the path have the appropriate ordering relation to the cut.

Equations
theorem Std.RBNode.Path.zoom_zoomed₁ :
∀ {α : Type u_1} {cut : αOrdering} {t : } {path : } {t' : } {path' : }, Std.RBNode.zoom cut t path = (t', path')Std.RBNode.OnRoot (fun x => cut x = Ordering.eq) t'
theorem Std.RBNode.Path.zoom_zoomed₂ :
∀ {α : Type u_1} {cut : αOrdering} {t : } {path : } {t' : } {path' : }, Std.RBNode.zoom cut t path = (t', path')Std.RBNode.Path.Zoomed cut pathStd.RBNode.Path.Zoomed cut path'
def Std.RBNode.Path.RootOrdered {α : Type u_1} (cmp : ααOrdering) :
αProp

path.RootOrdered cmp v is true if v would be able to fit into the hole without violating the ordering invariant.

Equations
theorem Std.RBNode.cmpEq.RootOrdered_congr {α : Type u_1} {a : α} {b : α} {cmp : ααOrdering} (h : Std.RBNode.cmpEq cmp a b) {t : } :
theorem Std.RBNode.Path.Zoomed.toRootOrdered {α : Type u_1} {v : α} {cmp : ααOrdering} {path : } :
def Std.RBNode.Path.Ordered {α : Type u_1} (cmp : ααOrdering) :

The ordering invariant for a Path.

Equations
theorem Std.RBNode.Ordered.zoom' {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t' : } {path' : } {t : } {path : } (ht : ) (hp : Std.RBNode.Path.Ordered cmp path) (tp : Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t) (pz : Std.RBNode.Path.Zoomed cut path) (eq : Std.RBNode.zoom cut t path = (t', path')) :
theorem Std.RBNode.Ordered.zoom {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t' : } {path' : } {t : } (ht : ) (eq : Std.RBNode.zoom cut t Std.RBNode.Path.root = (t', path')) :
theorem Std.RBNode.Path.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {path : } {t : } :
theorem Std.RBNode.Path.Ordered.insertNew {α : Type u_1} {cmp : ααOrdering} {v : α} {path : } (hp : Std.RBNode.Path.Ordered cmp path) (vp : Std.RBNode.Path.RootOrdered cmp path v) :
theorem Std.RBNode.Path.Ordered.insert {α : Type u_1} {cmp : ααOrdering} {v : α} {path : } {t : } :
theorem Std.RBNode.Path.Ordered.del {α : Type u_1} {cmp : ααOrdering} {path : } {t : } {c : Std.RBColor} :
theorem Std.RBNode.Path.Ordered.erase {α : Type u_1} {cmp : ααOrdering} {path : } {t : } :

## alter #

theorem Std.RBNode.Ordered.alter {α : Type u_1} {cut : αOrdering} {f : } {cmp : ααOrdering} {t : } (H : ∀ {x : α} {t' : } {p : }, Std.RBNode.zoom cut t Std.RBNode.Path.root = (t', p)f () = some x Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t') (h : ) :

The alter function preserves the ordering invariants.

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

The alter function preserves the balance invariants.

theorem Std.RBNode.modify_eq_alter {α : Type u_1} {cut : αOrdering} {f : αα} (t : ) :
theorem Std.RBNode.Ordered.modify {α : Type u_1} {cut : αOrdering} {cmp : ααOrdering} {f : αα} {t : } (H : Std.RBNode.OnRoot (fun x => Std.RBNode.cmpEq cmp (f x) x) (Std.RBNode.zoom cut t Std.RBNode.Path.root).fst) (h : ) :

The modify function preserves the ordering invariants.

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

The modify function preserves the balance invariants.

theorem Std.RBNode.WF.alter {α : Type u_1} {cut : αOrdering} {f : } {cmp : ααOrdering} {t : } (H : ∀ {x : α} {t' : } {p : }, Std.RBNode.zoom cut t Std.RBNode.Path.root = (t', p)f () = some x Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t') (h : Std.RBNode.WF cmp t) :
theorem Std.RBNode.WF.modify {α : Type u_1} {cut : αOrdering} {cmp : ααOrdering} {f : αα} {t : } (H : Std.RBNode.OnRoot (fun x => Std.RBNode.cmpEq cmp (f x) x) (Std.RBNode.zoom cut t Std.RBNode.Path.root).fst) (h : Std.RBNode.WF cmp t) :
theorem Std.RBNode.find?_eq_zoom {α : Type u_1} {cut : αOrdering} {t : } (p : optParam () Std.RBNode.Path.root) :
theorem Std.RBSet.ModifyWF.of_eq {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {f : αα} {t : Std.RBSet α cmp} (H : ∀ {x : α}, Std.RBNode.find? cut t.val = some xStd.RBNode.cmpEq cmp (f x) x) :

A sufficient condition for ModifyWF is that the new element compares equal to the original.

def Std.RBMap.modify {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Std.RBMap α β cmp) (k : α) (f : ββ) :
Std.RBMap α β cmp

O(log n). In-place replace the corresponding to key k. This takes the element out of the tree while f runs, so it uses the element linearly if t is unshared.

Equations
def Std.RBMap.alter.adapt {α : Type u_1} {β : Type u_2} (k : α) (f : ) :
Option (α × β)Option (α × β)

Auxiliary definition for alter.

Equations
• One or more equations did not get rendered due to their size.
@[specialize #[]]
def Std.RBMap.alter {α : Type u_1} {β : Type u_2} {cmp : ααOrdering} (t : Std.RBMap α β cmp) (k : α) (f : ) :
Std.RBMap α β cmp

O(log n). alterP cut f t simultaneously handles inserting, erasing and replacing an element using a function f : Option α → Option α. It is passed the result of t.findP? cut and can either return none to remove the element or some a to replace/insert the element with a (which must have the same ordering properties as the original element).

The element is used linearly if t is unshared.

The AlterWF assumption is required because f may change the ordering properties of the element, which would break the invariants.

Equations