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 Batteries.RBNode.OnRoot {α : Type u_1} (p : α → Prop) : Batteries.RBNode α → Prop

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

Equations

• Batteries.RBNode.OnRoot p Batteries.RBNode.nil = True
• Batteries.RBNode.OnRoot p (Batteries.RBNode.node c l x_1 r) = p x_1

@[inline]

def Batteries.RBNode.Path.fill' {α : Type u_1} : Batteries.RBNode α × Batteries.RBNode.Path α → Batteries.RBNode α

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

Equations

• Batteries.RBNode.Path.fill' (t, path) = path.fill t

theorem Batteries.RBNode.Path.zoom_fill' {α : Type u_1} (cut : α → Ordering) (t : Batteries.RBNode α) (path : Batteries.RBNode.Path α) : Batteries.RBNode.Path.fill' (Batteries.RBNode.zoom cut t path) = path.fill t

theorem Batteries.RBNode.Path.zoom_fill {α✝ : Type u_1} {cut : α✝ → Ordering} {t : Batteries.RBNode α✝} {path : Batteries.RBNode.Path α✝} {t' : Batteries.RBNode α✝} {path' : Batteries.RBNode.Path α✝} (H : Batteries.RBNode.zoom cut t path = (t', path')) : path.fill t = path'.fill t'

inductive Batteries.RBNode.Path.Balanced (c₀ : Batteries.RBColor) (n₀ : Nat) {α : Type u_1} : Batteries.RBNode.Path α → Batteries.RBColor → Nat → Prop

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₀ .

• root: ∀ {c₀ : Batteries.RBColor} {n₀ : Nat} {α : Type u_1}, Batteries.RBNode.Path.Balanced c₀ n₀ Batteries.RBNode.Path.root c₀ n₀

  The root of the tree is c₀, n₀-balanced by assumption.

• redL: ∀ {c₀ : Batteries.RBColor} {n₀ : Nat} {α : Type u_1} {y : Batteries.RBNode α} {n : Nat} {parent : Batteries.RBNode.Path α} {v : α}, y.Balanced Batteries.RBColor.black n → Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n → Batteries.RBNode.Path.Balanced c₀ n₀ (Batteries.RBNode.Path.left Batteries.RBColor.red parent v y) Batteries.RBColor.black n

  Descend into the left subtree of a red node.

• redR: ∀ {c₀ : Batteries.RBColor} {n₀ : Nat} {α : Type u_1} {x : Batteries.RBNode α} {n : Nat} {v : α} {parent : Batteries.RBNode.Path α}, x.Balanced Batteries.RBColor.black n → Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.red n → Batteries.RBNode.Path.Balanced c₀ n₀ (Batteries.RBNode.Path.right Batteries.RBColor.red x v parent) Batteries.RBColor.black n

  Descend into the right subtree of a red node.

• blackL: ∀ {c₀ : Batteries.RBColor} {n₀ : Nat} {α : Type u_1} {y : Batteries.RBNode α} {c₂ : Batteries.RBColor} {n : Nat} {parent : Batteries.RBNode.Path α} {v : α} {c₁ : Batteries.RBColor}, y.Balanced c₂ n → Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.black (n + 1) → Batteries.RBNode.Path.Balanced c₀ n₀ (Batteries.RBNode.Path.left Batteries.RBColor.black parent v y) c₁ n

  Descend into the left subtree of a black node.

• blackR: ∀ {c₀ : Batteries.RBColor} {n₀ : Nat} {α : Type u_1} {x : Batteries.RBNode α} {c₁ : Batteries.RBColor} {n : Nat} {v : α} {parent : Batteries.RBNode.Path α} {c₂ : Batteries.RBColor}, x.Balanced c₁ n → Batteries.RBNode.Path.Balanced c₀ n₀ parent Batteries.RBColor.black (n + 1) → Batteries.RBNode.Path.Balanced c₀ n₀ (Batteries.RBNode.Path.right Batteries.RBColor.black x v parent) c₂ n

  Descend into the right subtree of a black node.

theorem Batteries.RBNode.Path.Balanced.fill {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} : Batteries.RBNode.Path.Balanced c₀ n₀ path c n → t.Balanced c n → (path.fill t).Balanced 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 Batteries.RBNode.Balanced.zoom {α✝ : Type u_1} {cut : α✝ → Ordering} {t : Batteries.RBNode α✝} {path : Batteries.RBNode.Path α✝} {t' : Batteries.RBNode α✝} {path' : Batteries.RBNode.Path α✝} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} : t.Balanced c n → Batteries.RBNode.Path.Balanced c₀ n₀ path c n → Batteries.RBNode.zoom cut t path = (t', path') → ∃ (c : Batteries.RBColor), ∃ (n : Nat), t'.Balanced c n ∧ Batteries.RBNode.Path.Balanced c₀ n₀ path' c n

theorem Batteries.RBNode.Path.Balanced.ins {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path c n) (ht : Batteries.RBNode.RedRed (c = Batteries.RBColor.red) t n) : ∃ (n : Nat), (path.ins t).Balanced Batteries.RBColor.black n

theorem Batteries.RBNode.Path.Balanced.insertNew {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {v : α} {path : Batteries.RBNode.Path α} (H : Batteries.RBNode.Path.Balanced c n path Batteries.RBColor.black 0) : ∃ (n : Nat), (path.insertNew v).Balanced Batteries.RBColor.black n

theorem Batteries.RBNode.Path.Balanced.del {α : Type u_1} {c₀ : Batteries.RBColor} {n₀ : Nat} {c : Batteries.RBColor} {n : Nat} {c' : Batteries.RBColor} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} (hp : Batteries.RBNode.Path.Balanced c₀ n₀ path c n) (ht : Batteries.RBNode.DelProp c' t n) (hc : c = Batteries.RBColor.black → c' ≠ Batteries.RBColor.red) : ∃ (n : Nat), (path.del t c').Balanced Batteries.RBColor.black n

def Batteries.RBNode.Path.Zoomed {α : Type u_1} (cut : α → Ordering) : Batteries.RBNode.Path α → Prop

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

• Batteries.RBNode.Path.Zoomed cut Batteries.RBNode.Path.root = True
• Batteries.RBNode.Path.Zoomed cut (Batteries.RBNode.Path.left c parent x_1 r) = (cut x_1 = Ordering.lt ∧ Batteries.RBNode.Path.Zoomed cut parent)
• Batteries.RBNode.Path.Zoomed cut (Batteries.RBNode.Path.right c l x_1 parent) = (cut x_1 = Ordering.gt ∧ Batteries.RBNode.Path.Zoomed cut parent)

theorem Batteries.RBNode.Path.zoom_zoomed₂ {α✝ : Type u_1} {cut : α✝ → Ordering} {t : Batteries.RBNode α✝} {path : Batteries.RBNode.Path α✝} {t' : Batteries.RBNode α✝} {path' : Batteries.RBNode.Path α✝} (e : Batteries.RBNode.zoom cut t path = (t', path')) (hp : Batteries.RBNode.Path.Zoomed cut path) : Batteries.RBNode.Path.Zoomed cut path'

def Batteries.RBNode.Path.RootOrdered {α : Type u_1} (cmp : α → α → Ordering) : Batteries.RBNode.Path α → α → Prop

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

Equations

• Batteries.RBNode.Path.RootOrdered cmp Batteries.RBNode.Path.root x = True
• Batteries.RBNode.Path.RootOrdered cmp (Batteries.RBNode.Path.left c parent x_2 r) x = (Batteries.RBNode.cmpLT cmp x x_2 ∧ Batteries.RBNode.Path.RootOrdered cmp parent x)
• Batteries.RBNode.Path.RootOrdered cmp (Batteries.RBNode.Path.right c l x_2 parent) x = (Batteries.RBNode.cmpLT cmp x_2 x ∧ Batteries.RBNode.Path.RootOrdered cmp parent x)

theorem Batteries.RBNode.cmpEq.RootOrdered_congr {α : Type u_1} {a b : α} {cmp : α → α → Ordering} (h : Batteries.RBNode.cmpEq cmp a b) {t : Batteries.RBNode.Path α} : Batteries.RBNode.Path.RootOrdered cmp t a ↔ Batteries.RBNode.Path.RootOrdered cmp t b

theorem Batteries.RBNode.Path.Zoomed.toRootOrdered {α : Type u_1} {v : α} {cmp : α → α → Ordering} {path : Batteries.RBNode.Path α} : Batteries.RBNode.Path.Zoomed (cmp v) path → Batteries.RBNode.Path.RootOrdered cmp path v

def Batteries.RBNode.Path.Ordered {α : Type u_1} (cmp : α → α → Ordering) : Batteries.RBNode.Path α → Prop

The ordering invariant for a Path.

Equations

• One or more equations did not get rendered due to their size.
• Batteries.RBNode.Path.Ordered cmp Batteries.RBNode.Path.root = True

theorem Batteries.RBNode.Path.Ordered.fill {α : Type u_1} {cmp : α → α → Ordering} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} : Batteries.RBNode.Ordered cmp (path.fill t) ↔ Batteries.RBNode.Path.Ordered cmp path ∧ Batteries.RBNode.Ordered cmp t ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t

theorem Batteries.RBNode.Ordered.zoom' {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α} {t : Batteries.RBNode α} {path : Batteries.RBNode.Path α} (ht : Batteries.RBNode.Ordered cmp t) (hp : Batteries.RBNode.Path.Ordered cmp path) (tp : Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t) (pz : Batteries.RBNode.Path.Zoomed cut path) (eq : Batteries.RBNode.zoom cut t path = (t', path')) : Batteries.RBNode.Ordered cmp t' ∧ Batteries.RBNode.Path.Ordered cmp path' ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path') t' ∧ Batteries.RBNode.Path.Zoomed cut path'

theorem Batteries.RBNode.Ordered.zoom {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {t' : Batteries.RBNode α} {path' : Batteries.RBNode.Path α} {t : Batteries.RBNode α} (ht : Batteries.RBNode.Ordered cmp t) (eq : Batteries.RBNode.zoom cut t = (t', path')) : Batteries.RBNode.Ordered cmp t' ∧ Batteries.RBNode.Path.Ordered cmp path' ∧ Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path') t' ∧ Batteries.RBNode.Path.Zoomed cut path'

theorem Batteries.RBNode.Path.Ordered.ins {α : Type u_1} {cmp : α → α → Ordering} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} : Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Path.Ordered cmp path → Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t → Batteries.RBNode.Ordered cmp (path.ins t)

theorem Batteries.RBNode.Path.Ordered.insertNew {α : Type u_1} {cmp : α → α → Ordering} {v : α} {path : Batteries.RBNode.Path α} (hp : Batteries.RBNode.Path.Ordered cmp path) (vp : Batteries.RBNode.Path.RootOrdered cmp path v) : Batteries.RBNode.Ordered cmp (path.insertNew v)

theorem Batteries.RBNode.Path.Ordered.del {α : Type u_1} {cmp : α → α → Ordering} {path : Batteries.RBNode.Path α} {t : Batteries.RBNode α} {c : Batteries.RBColor} : Batteries.RBNode.Ordered cmp t → Batteries.RBNode.Path.Ordered cmp path → Batteries.RBNode.All (Batteries.RBNode.Path.RootOrdered cmp path) t → Batteries.RBNode.Ordered cmp (path.del t c)

alter

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

The alter function preserves the ordering invariants.

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

The alter function preserves the balance invariants.

theorem Batteries.RBNode.modify_eq_alter {α : Type u_1} {cut : α → Ordering} {f : α → α} (t : Batteries.RBNode α) : Batteries.RBNode.modify cut f t = Batteries.RBNode.alter cut (Option.map f) t

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

The modify function preserves the ordering invariants.

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

The modify function preserves the balance invariants.

theorem Batteries.RBNode.WF.alter {α : Type u_1} {cut : α → Ordering} {f : Option α → Option α} {cmp : α → α → Ordering} {t : Batteries.RBNode α} (H : ∀ {x : α} {t' : Batteries.RBNode α} {p : Batteries.RBNode.Path α}, Batteries.RBNode.zoom cut t = (t', p) → f t'.root? = some x → Batteries.RBNode.Path.RootOrdered cmp p x ∧ Batteries.RBNode.OnRoot (Batteries.RBNode.cmpEq cmp x) t') (h : Batteries.RBNode.WF cmp t) : Batteries.RBNode.WF cmp (Batteries.RBNode.alter cut f t)

theorem Batteries.RBNode.WF.modify {α : Type u_1} {cut : α → Ordering} {cmp : α → α → Ordering} {f : α → α} {t : Batteries.RBNode α} (H : Batteries.RBNode.OnRoot (fun (x : α) => Batteries.RBNode.cmpEq cmp (f x) x) (Batteries.RBNode.zoom cut t).fst) (h : Batteries.RBNode.WF cmp t) : Batteries.RBNode.WF cmp (Batteries.RBNode.modify cut f t)

theorem Batteries.RBNode.find?_eq_zoom {α : Type u_1} {cut : α → Ordering} {t : Batteries.RBNode α} (p : Batteries.RBNode.Path α := Batteries.RBNode.Path.root) : Batteries.RBNode.find? cut t = (Batteries.RBNode.zoom cut t p).fst.root?

theorem Batteries.RBSet.ModifyWF.of_eq {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {f : α → α} {t : Batteries.RBSet α cmp} (H : ∀ {x : α}, Batteries.RBNode.find? cut t.val = some x → Batteries.RBNode.cmpEq cmp (f x) x) : t.ModifyWF cut f

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

def Batteries.RBMap.modify {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Batteries.RBMap α β cmp) (k : α) (f : β → β) : Batteries.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

• t.modify k f = Batteries.RBSet.modifyP t (fun (x : α × β) => cmp k x.fst) fun (x : α × β) => match x with | (a, b) => (a, f b)

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

Auxiliary definition for alter.

Equations

• Batteries.RBMap.alter.adapt k f none = match f none with | none => none | some v => some (k, v)
• Batteries.RBMap.alter.adapt k f (some (k', v')) = match f (some v') with | none => none | some v => some (k', v)

@[specialize #[]]

def Batteries.RBMap.alter {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} (t : Batteries.RBMap α β cmp) (k : α) (f : Option β → Option β) : Batteries.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

• t.alter k f = Batteries.RBSet.alterP t (fun (x : α × β) => cmp k x.fst) (Batteries.RBMap.alter.adapt k f)