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 #
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]
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'
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
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
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)
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)