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) : RBNode α → Prop

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

@[inline]

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

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

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

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

inductive Batteries.RBNode.Path.Balanced (c₀ : RBColor) (n₀ : Nat) {α : Type u_1} : Path α → 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₀ : RBColor} {n₀ : Nat} {α : Type u_1} : Path.Balanced c₀ n₀ root c₀ n₀

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

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

  Descend into the left subtree of a red node.

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

  Descend into the right subtree of a red node.

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

  Descend into the left subtree of a black node.

• blackR {c₀ : RBColor} {n₀ : Nat} {α : Type u_1} {x : RBNode α} {c₁ : RBColor} {n : Nat} {v : α} {parent : Path α} {c₂ : RBColor} : x.Balanced c₁ n → Path.Balanced c₀ n₀ parent RBColor.black (n + 1) → Path.Balanced c₀ n₀ (right 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₀ : RBColor} {n₀ : Nat} {c : RBColor} {n : Nat} {path : Path α} {t : 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 : RBNode α✝} {path : Path α✝} {t' : RBNode α✝} {path' : Path α✝} {c₀ : RBColor} {n₀ : Nat} {c : RBColor} {n : Nat} : t.Balanced c n → Path.Balanced c₀ n₀ path c n → zoom cut t path = (t', path') → ∃ (c : RBColor), ∃ (n : Nat), t'.Balanced c n ∧ Path.Balanced c₀ n₀ path' c n

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

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

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

def Batteries.RBNode.Path.Zoomed {α : Type u_1} (cut : α → Ordering) : 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.

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

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

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

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

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

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

The ordering invariant for a Path.

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

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

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

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

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

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

alter

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

The alter function preserves the ordering invariants.

theorem Batteries.RBNode.Balanced.alter {α : Type u_1} {c : RBColor} {n : Nat} {cut : α → Ordering} {f : Option α → Option α} {t : RBNode α} (h : t.Balanced c n) : ∃ (c : RBColor), ∃ (n : Nat), (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 : RBNode α) : modify cut f t = alter cut (Option.map f) t

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

The modify function preserves the ordering invariants.

theorem Batteries.RBNode.Balanced.modify {α : Type u_1} {c : RBColor} {n : Nat} {cut : α → Ordering} {f : α → α} {t : RBNode α} (h : t.Balanced c n) : ∃ (c : RBColor), ∃ (n : Nat), (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 : RBNode α} (H : ∀ {x : α} {t' : RBNode α} {p : Path α}, zoom cut t = (t', p) → f t'.root? = some x → Path.RootOrdered cmp p x ∧ OnRoot (cmpEq cmp x) t') (h : WF cmp t) : WF cmp (RBNode.alter cut f t)

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

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

theorem Batteries.RBSet.ModifyWF.of_eq {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {f : α → α} {t : RBSet α cmp} (H : ∀ {x : α}, RBNode.find? cut t.val = some x → 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 : RBMap α β cmp) (k : α) (f : β → β) : 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.

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

Auxiliary definition for alter.

@[specialize #[]]

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