Documentation

Std.Data.RBMap.Alter

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

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

Equations
Instances For
    def Std.RBNode.setRoot {α : Type u_1} (v : α) :

    Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

    Equations
    Instances For
      def Std.RBNode.delRoot {α : Type u_1} :

      Auxiliary definition for zoom_ins: set the root of the tree to v, creating a node if necessary.

      Equations
      Instances For
        @[inline]

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

        Equations
        Instances For
          theorem Std.RBNode.Path.zoom_fill' {α : Type u_1} (cut : αOrdering) (t : Std.RBNode α) (path : Std.RBNode.Path α) :
          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.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} :

          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 nStd.RBNode.Balanced t c nStd.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 nStd.RBNode.Path.Balanced c₀ n₀ path c nStd.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.ins_eq_fill {α : Type u_1} {c₀ : Std.RBColor} {n₀ : Nat} {c : Std.RBColor} {n : Nat} {path : Std.RBNode.Path α} {t : Std.RBNode α} :
            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) :
            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 : Std.RBColor), ∃ (n : Nat), 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 = (t', path)) :
            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.blackc' Std.RBColor.red) :
            def Std.RBNode.Path.AllL {α : Type u_1} (p : αProp) :

            Asserts that p holds on all elements to the left of the hole.

            Equations
            Instances For
              def Std.RBNode.Path.AllR {α : Type u_1} (p : αProp) :

              Asserts that p holds on all elements to the right of the hole.

              Equations
              Instances For
                def Std.RBNode.Path.Zoomed {α : Type u_1} (cut : αOrdering) :

                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
                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 pathStd.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
                  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 α} :
                    theorem Std.RBNode.Path.Zoomed.toRootOrdered {α : Type u_1} {v : α} {cmp : ααOrdering} {path : Std.RBNode.Path α} :
                    def Std.RBNode.Path.Ordered {α : Type u_1} (cmp : ααOrdering) :

                    The ordering invariant for a Path.

                    Equations
                    Instances For
                      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')) :
                      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')) :
                      theorem Std.RBNode.Path.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {path : Std.RBNode.Path α} {t : Std.RBNode α} :
                      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) :
                      theorem Std.RBNode.Path.Ordered.del {α : Type u_1} {cmp : ααOrdering} {path : Std.RBNode.Path α} {t : Std.RBNode α} {c : Std.RBColor} :

                      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 xStd.RBNode.Path.RootOrdered cmp p x Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t') (h : Std.RBNode.Ordered cmp 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 α) :
                      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) :

                      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 xStd.RBNode.Path.RootOrdered cmp p x Std.RBNode.OnRoot (Std.RBNode.cmpEq cmp x) t') (h : Std.RBNode.WF cmp 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) :
                      theorem Std.RBNode.find?_eq_zoom {α : Type u_1} {cut : αOrdering} {t : Std.RBNode α} (p : optParam (Std.RBNode.Path α) Std.RBNode.Path.root) :
                      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 xStd.RBNode.cmpEq cmp (f x) x) :

                      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
                      Instances For
                        def Std.RBMap.alter.adapt {α : Type u_1} {β : Type u_2} (k : α) (f : Option βOption β) :
                        Option (α × β)Option (α × β)

                        Auxiliary definition for alter.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        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
                          Instances For