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
- Std.RBNode.OnRoot p x = match x with | Std.RBNode.nil => True | Std.RBNode.node c l x r => p x
Instances For
@[inline]
Same as fill but taking its arguments in a pair for easier composition with zoom.
Equations
- Std.RBNode.Path.fill' x = match x with | (t, path) => Std.RBNode.Path.fill path t
Instances For
theorem
Std.RBNode.Path.zoom_fill'
{α : Type u_1}
(cut : α → Ordering)
(t : Std.RBNode α)
(path : Std.RBNode.Path α)
:
Std.RBNode.Path.fill' (Std.RBNode.zoom cut t path) = Std.RBNode.Path.fill path t
theorem
Std.RBNode.Path.zoom_fill :
∀ {α : Type u_1} {cut : α → Ordering} {t : Std.RBNode α} {path : Std.RBNode.Path α} {t' : Std.RBNode α}
{path' : Std.RBNode.Path α},
Std.RBNode.zoom cut t path = (t', path') → Std.RBNode.Path.fill path t = Std.RBNode.Path.fill path' t'
inductive
Std.RBNode.Path.Balanced
(c₀ : Std.RBColor)
(n₀ : Nat)
{α : Type u_1}
:
Std.RBNode.Path α → Std.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₀ : Std.RBColor} {n₀ : Nat} {α : Type u_1}, Std.RBNode.Path.Balanced c₀ n₀ Std.RBNode.Path.root c₀ n₀
The root of the tree is
c₀, n₀-balanced by assumption. - redL: ∀ {c₀ : Std.RBColor} {n₀ : Nat} {α : Type u_1} {y : Std.RBNode α} {n : Nat} {parent : Std.RBNode.Path α} {v : α},
Std.RBNode.Balanced y Std.RBColor.black n →
Std.RBNode.Path.Balanced c₀ n₀ parent Std.RBColor.red n →
Std.RBNode.Path.Balanced c₀ n₀ (Std.RBNode.Path.left Std.RBColor.red parent v y) Std.RBColor.black n
Descend into the left subtree of a red node.
- redR: ∀ {c₀ : Std.RBColor} {n₀ : Nat} {α : Type u_1} {x : Std.RBNode α} {n : Nat} {v : α} {parent : Std.RBNode.Path α},
Std.RBNode.Balanced x Std.RBColor.black n →
Std.RBNode.Path.Balanced c₀ n₀ parent Std.RBColor.red n →
Std.RBNode.Path.Balanced c₀ n₀ (Std.RBNode.Path.right Std.RBColor.red x v parent) Std.RBColor.black n
Descend into the right subtree of a red node.
- blackL: ∀ {c₀ : Std.RBColor} {n₀ : Nat} {α : Type u_1} {y : Std.RBNode α} {c₂ : Std.RBColor} {n : Nat}
{parent : Std.RBNode.Path α} {v : α} {c₁ : Std.RBColor},
Std.RBNode.Balanced y c₂ n →
Std.RBNode.Path.Balanced c₀ n₀ parent Std.RBColor.black (n + 1) →
Std.RBNode.Path.Balanced c₀ n₀ (Std.RBNode.Path.left Std.RBColor.black parent v y) c₁ n
Descend into the left subtree of a black node.
- blackR: ∀ {c₀ : Std.RBColor} {n₀ : Nat} {α : Type u_1} {x : Std.RBNode α} {c₁ : Std.RBColor} {n : Nat} {v : α}
{parent : Std.RBNode.Path α} {c₂ : Std.RBColor},
Std.RBNode.Balanced x c₁ n →
Std.RBNode.Path.Balanced c₀ n₀ parent Std.RBColor.black (n + 1) →
Std.RBNode.Path.Balanced c₀ n₀ (Std.RBNode.Path.right Std.RBColor.black x v parent) c₂ n
Descend into the right subtree of a black node.
Instances For
theorem
Std.RBNode.Path.Balanced.fill
{α : Type u_1}
{c₀ : Std.RBColor}
{n₀ : Nat}
{c : Std.RBColor}
{n : Nat}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Path.Balanced c₀ n₀ path c n →
Std.RBNode.Balanced t c n → Std.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 : Std.RBNode α} {path : Std.RBNode.Path α} {t' : Std.RBNode α}
{path' : Std.RBNode.Path α} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat},
Std.RBNode.Balanced t c n →
Std.RBNode.Path.Balanced c₀ n₀ path c n →
Std.RBNode.zoom cut t path = (t', path') →
∃ (c : Std.RBColor), ∃ (n : Nat), Std.RBNode.Balanced t' c n ∧ Std.RBNode.Path.Balanced c₀ n₀ path' c n
theorem
Std.RBNode.Path.Balanced.ins
{α : Type u_1}
{c₀ : Std.RBColor}
{n₀ : Nat}
{c : Std.RBColor}
{n : Nat}
{t : Std.RBNode α}
{path : Std.RBNode.Path α}
(hp : Std.RBNode.Path.Balanced c₀ n₀ path c n)
(ht : Std.RBNode.RedRed (c = Std.RBColor.red) t n)
:
∃ (n : Nat), Std.RBNode.Balanced (Std.RBNode.Path.ins path t) Std.RBColor.black n
theorem
Std.RBNode.Path.Balanced.insertNew
{α : Type u_1}
{c : Std.RBColor}
{n : Nat}
{v : α}
{path : Std.RBNode.Path α}
(H : Std.RBNode.Path.Balanced c n path Std.RBColor.black 0)
:
∃ (n : Nat), Std.RBNode.Balanced (Std.RBNode.Path.insertNew path v) Std.RBColor.black n
theorem
Std.RBNode.Path.Balanced.del
{α : Type u_1}
{c₀ : Std.RBColor}
{n₀ : Nat}
{c : Std.RBColor}
{n : Nat}
{c' : Std.RBColor}
{t : Std.RBNode α}
{path : Std.RBNode.Path α}
(hp : Std.RBNode.Path.Balanced c₀ n₀ path c n)
(ht : Std.RBNode.DelProp c' t n)
(hc : c = Std.RBColor.black → c' ≠ Std.RBColor.red)
:
∃ (n : Nat), Std.RBNode.Balanced (Std.RBNode.Path.del path t c') Std.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
- Std.RBNode.Path.Zoomed cut Std.RBNode.Path.root = True
- Std.RBNode.Path.Zoomed cut (Std.RBNode.Path.left c parent x_1 r) = (cut x_1 = Ordering.lt ∧ Std.RBNode.Path.Zoomed cut parent)
- Std.RBNode.Path.Zoomed cut (Std.RBNode.Path.right c l x_1 parent) = (cut x_1 = Ordering.gt ∧ Std.RBNode.Path.Zoomed cut parent)
Instances For
theorem
Std.RBNode.Path.zoom_zoomed₂ :
∀ {α : Type u_1} {cut : α → Ordering} {t : Std.RBNode α} {path : Std.RBNode.Path α} {t' : Std.RBNode α}
{path' : Std.RBNode.Path α},
Std.RBNode.zoom cut t path = (t', path') → Std.RBNode.Path.Zoomed cut path → Std.RBNode.Path.Zoomed cut path'
def
Std.RBNode.Path.RootOrdered
{α : Type u_1}
(cmp : α → α → Ordering)
:
Std.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
- Std.RBNode.Path.RootOrdered cmp Std.RBNode.Path.root x = True
- Std.RBNode.Path.RootOrdered cmp (Std.RBNode.Path.left c parent x_2 r) x = (Std.RBNode.cmpLT cmp x x_2 ∧ Std.RBNode.Path.RootOrdered cmp parent x)
- Std.RBNode.Path.RootOrdered cmp (Std.RBNode.Path.right c l x_2 parent) x = (Std.RBNode.cmpLT cmp x_2 x ∧ Std.RBNode.Path.RootOrdered cmp parent x)
Instances For
theorem
Std.RBNode.cmpEq.RootOrdered_congr
{α : Type u_1}
{a : α}
{b : α}
{cmp : α → α → Ordering}
(h : Std.RBNode.cmpEq cmp a b)
{t : Std.RBNode.Path α}
:
Std.RBNode.Path.RootOrdered cmp t a ↔ Std.RBNode.Path.RootOrdered cmp t b
theorem
Std.RBNode.Path.Zoomed.toRootOrdered
{α : Type u_1}
{v : α}
{cmp : α → α → Ordering}
{path : Std.RBNode.Path α}
:
Std.RBNode.Path.Zoomed (cmp v) path → Std.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.
- Std.RBNode.Path.Ordered cmp Std.RBNode.Path.root = True
Instances For
theorem
Std.RBNode.Path.Ordered.fill
{α : Type u_1}
{cmp : α → α → Ordering}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Ordered cmp (Std.RBNode.Path.fill path t) ↔ Std.RBNode.Path.Ordered cmp path ∧ Std.RBNode.Ordered cmp t ∧ Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t
theorem
Std.RBNode.Ordered.zoom'
{α : Type u_1}
{cmp : α → α → Ordering}
{cut : α → Ordering}
{t' : Std.RBNode α}
{path' : Std.RBNode.Path α}
{t : Std.RBNode α}
{path : Std.RBNode.Path α}
(ht : Std.RBNode.Ordered cmp t)
(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'))
:
Std.RBNode.Ordered cmp t' ∧ Std.RBNode.Path.Ordered cmp path' ∧ Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path') t' ∧ Std.RBNode.Path.Zoomed cut path'
theorem
Std.RBNode.Ordered.zoom
{α : Type u_1}
{cmp : α → α → Ordering}
{cut : α → Ordering}
{t' : Std.RBNode α}
{path' : Std.RBNode.Path α}
{t : Std.RBNode α}
(ht : Std.RBNode.Ordered cmp t)
(eq : Std.RBNode.zoom cut t = (t', path'))
:
Std.RBNode.Ordered cmp t' ∧ Std.RBNode.Path.Ordered cmp path' ∧ Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path') t' ∧ Std.RBNode.Path.Zoomed cut path'
theorem
Std.RBNode.Path.Ordered.ins
{α : Type u_1}
{cmp : α → α → Ordering}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Ordered cmp t →
Std.RBNode.Path.Ordered cmp path →
Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t → Std.RBNode.Ordered cmp (Std.RBNode.Path.ins path t)
theorem
Std.RBNode.Path.Ordered.insertNew
{α : Type u_1}
{cmp : α → α → Ordering}
{v : α}
{path : Std.RBNode.Path α}
(hp : Std.RBNode.Path.Ordered cmp path)
(vp : Std.RBNode.Path.RootOrdered cmp path v)
:
Std.RBNode.Ordered cmp (Std.RBNode.Path.insertNew path v)
theorem
Std.RBNode.Path.Ordered.del
{α : Type u_1}
{cmp : α → α → Ordering}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
{c : Std.RBColor}
:
Std.RBNode.Ordered cmp t →
Std.RBNode.Path.Ordered cmp path →
Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t → Std.RBNode.Ordered cmp (Std.RBNode.Path.del path t c)
alter #
theorem
Std.RBNode.Ordered.alter
{α : Type u_1}
{cut : α → Ordering}
{f : Option α → Option α}
{cmp : α → α → Ordering}
{t : Std.RBNode α}
(H : ∀ {x : α} {t' : Std.RBNode α} {p : Std.RBNode.Path α},
Std.RBNode.zoom cut t = (t', p) →
f (Std.RBNode.root? t') = some x →
Std.RBNode.Path.RootOrdered cmp p x ∧ Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t')
(h : Std.RBNode.Ordered cmp t)
:
Std.RBNode.Ordered cmp (Std.RBNode.alter cut f t)
The alter function preserves the ordering invariants.
theorem
Std.RBNode.Balanced.alter
{α : Type u_1}
{c : Std.RBColor}
{n : Nat}
{cut : α → Ordering}
{f : Option α → Option α}
{t : Std.RBNode α}
(h : Std.RBNode.Balanced t c n)
:
∃ (c : Std.RBColor), ∃ (n : Nat), 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 : Std.RBNode α)
:
Std.RBNode.modify cut f t = Std.RBNode.alter cut (Option.map f) t
theorem
Std.RBNode.Ordered.modify
{α : Type u_1}
{cut : α → Ordering}
{cmp : α → α → Ordering}
{f : α → α}
{t : Std.RBNode α}
(H : Std.RBNode.OnRoot (fun (x : α) => Std.RBNode.cmpEq cmp (f x) x) (Std.RBNode.zoom cut t).fst)
(h : Std.RBNode.Ordered cmp t)
:
Std.RBNode.Ordered cmp (Std.RBNode.modify cut f t)
The modify function preserves the ordering invariants.
theorem
Std.RBNode.Balanced.modify
{α : Type u_1}
{c : Std.RBColor}
{n : Nat}
{cut : α → Ordering}
{f : α → α}
{t : Std.RBNode α}
(h : Std.RBNode.Balanced t c n)
:
∃ (c : Std.RBColor), ∃ (n : Nat), 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 : Option α → Option α}
{cmp : α → α → Ordering}
{t : Std.RBNode α}
(H : ∀ {x : α} {t' : Std.RBNode α} {p : Std.RBNode.Path α},
Std.RBNode.zoom cut t = (t', p) →
f (Std.RBNode.root? t') = some x →
Std.RBNode.Path.RootOrdered cmp p x ∧ Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t')
(h : Std.RBNode.WF cmp t)
:
Std.RBNode.WF cmp (Std.RBNode.alter cut f t)
theorem
Std.RBNode.WF.modify
{α : Type u_1}
{cut : α → Ordering}
{cmp : α → α → Ordering}
{f : α → α}
{t : Std.RBNode α}
(H : Std.RBNode.OnRoot (fun (x : α) => Std.RBNode.cmpEq cmp (f x) x) (Std.RBNode.zoom cut t).fst)
(h : Std.RBNode.WF cmp t)
:
Std.RBNode.WF cmp (Std.RBNode.modify cut f t)
theorem
Std.RBNode.find?_eq_zoom
{α : Type u_1}
{cut : α → Ordering}
{t : Std.RBNode α}
(p : optParam (Std.RBNode.Path α) Std.RBNode.Path.root)
:
Std.RBNode.find? cut t = Std.RBNode.root? (Std.RBNode.zoom cut t p).fst
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 x → Std.RBNode.cmpEq cmp (f x) x)
:
Std.RBSet.ModifyWF t cut f
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
- Std.RBMap.modify t k f = Std.RBSet.modifyP t (fun (x : α × β) => cmp k x.fst) fun (x : α × β) => match x with | (a, b) => (a, f b)
Instances For
@[specialize #[]]
def
Std.RBMap.alter
{α : Type u_1}
{β : Type u_2}
{cmp : α → α → Ordering}
(t : Std.RBMap α β cmp)
(k : α)
(f : Option β → Option β)
:
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
- Std.RBMap.alter t k f = Std.RBSet.alterP t (fun (x : α × β) => cmp k x.fst) (Std.RBMap.alter.adapt k f)