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
Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.
Equations
- Std.RBNode.setRoot v x = match x with | Std.RBNode.nil => Std.RBNode.node Std.RBColor.red Std.RBNode.nil v Std.RBNode.nil | Std.RBNode.node c a v b => Std.RBNode.node c a v b
Instances For
Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.
Equations
- Std.RBNode.delRoot x = match x with | Std.RBNode.nil => Std.RBNode.nil | Std.RBNode.node c a v b => Std.RBNode.append a b
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'
theorem
Std.RBNode.Path.zoom_ins
{α : Type u_1}
{v : α}
{path : Std.RBNode.Path α}
{t' : Std.RBNode α}
{path' : Std.RBNode.Path α}
{t : Std.RBNode α}
{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' (Std.RBNode.setRoot v t')
theorem
Std.RBNode.Path.insertNew_eq_insert :
∀ {α : Type u_1} {cmp : α → α → Ordering} {t : Std.RBNode α} {path : Std.RBNode.Path α} {v : α},
Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (Std.RBNode.nil, path) →
Std.RBNode.Path.insertNew path v = Std.RBNode.setBlack (Std.RBNode.insert cmp t v)
theorem
Std.RBNode.Path.zoom_del
{α : Type u_1}
{cut : α → Ordering}
{path : Std.RBNode.Path α}
{t' : Std.RBNode α}
{path' : Std.RBNode.Path α}
{t : Std.RBNode α}
:
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' (Std.RBNode.delRoot t')
(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}
:
Std.RBNode.Path α → Std.RBColor → Nat → Prop
- 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.
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 : 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 n, Std.RBNode.Balanced t' 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 : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Path.Balanced c₀ n₀ path c n →
Std.RBNode.Balanced t c n → Std.RBNode.Path.ins path t = Std.RBNode.setBlack (Std.RBNode.Path.fill path t)
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, 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, Std.RBNode.Balanced (Std.RBNode.Path.insertNew path v) Std.RBColor.black n
theorem
Std.RBNode.Path.Balanced.insert
{α : Type u_1}
{c₀ : Std.RBColor}
{n₀ : Nat}
{c : Std.RBColor}
{n : Nat}
{t : Std.RBNode α}
{v : α}
{path : Std.RBNode.Path α}
(hp : Std.RBNode.Path.Balanced c₀ n₀ path c n)
:
Std.RBNode.Balanced t 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' : Std.RBNode α}
{v : α}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
(ht : Std.RBNode.Balanced t c n)
(H : Std.RBNode.zoom (cmp v) t Std.RBNode.Path.root = (t', path))
:
Std.RBNode.setBlack (Std.RBNode.Path.insert path t' v) = Std.RBNode.setBlack (Std.RBNode.insert cmp t v)
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, Std.RBNode.Balanced (Std.RBNode.Path.del path t c') Std.RBColor.black n
Asserts that p holds on all elements to the left of the hole.
Equations
- Std.RBNode.Path.AllL p Std.RBNode.Path.root = True
- Std.RBNode.Path.AllL p (Std.RBNode.Path.left c parent v r) = Std.RBNode.Path.AllL p parent
- Std.RBNode.Path.AllL p (Std.RBNode.Path.right c a x_1 parent) = (Std.RBNode.All p a ∧ p x_1 ∧ Std.RBNode.Path.AllL p parent)
Instances For
Asserts that p holds on all elements to the right of the hole.
Equations
- Std.RBNode.Path.AllR p Std.RBNode.Path.root = True
- Std.RBNode.Path.AllR p (Std.RBNode.Path.left c parent v r) = (Std.RBNode.Path.AllR p parent ∧ p v ∧ Std.RBNode.All p r)
- Std.RBNode.Path.AllR p (Std.RBNode.Path.right c a x_1 parent) = Std.RBNode.Path.AllR p parent
Instances For
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 v r) = (cut v = Ordering.lt ∧ Std.RBNode.Path.Zoomed cut parent)
- Std.RBNode.Path.Zoomed cut (Std.RBNode.Path.right c a 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.OnRoot (fun x => cut x = Ordering.eq) t'
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 Std.RBNode.Path.root = (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.insert
{α : Type u_1}
{cmp : α → α → Ordering}
{v : α}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Path.Ordered cmp path →
Std.RBNode.Ordered cmp t →
Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t →
Std.RBNode.Path.RootOrdered cmp path v →
Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp v) t → Std.RBNode.Ordered cmp (Std.RBNode.Path.insert path t 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)
theorem
Std.RBNode.Path.Ordered.erase
{α : Type u_1}
{cmp : α → α → Ordering}
{path : Std.RBNode.Path α}
{t : Std.RBNode α}
:
Std.RBNode.Path.Ordered cmp path →
Std.RBNode.Ordered cmp t →
Std.RBNode.All (Std.RBNode.Path.RootOrdered cmp path) t → Std.RBNode.Ordered cmp (Std.RBNode.Path.erase path t)
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 Std.RBNode.Path.root = (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 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 : 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 Std.RBNode.Path.root).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 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 : Option α → Option α}
{cmp : α → α → Ordering}
{t : Std.RBNode α}
(H : ∀ {x : α} {t' : Std.RBNode α} {p : Std.RBNode.Path α},
Std.RBNode.zoom cut t Std.RBNode.Path.root = (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 Std.RBNode.Path.root).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)