Documentation

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

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

Equations
Instances For
    @[inline]

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

    Equations
    Instances For
      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 α}, 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₀ .

      Instances For
        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 nt.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 nBatteries.RBNode.Path.Balanced c₀ n₀ path c nBatteries.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.blackc' 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
        Instances For
          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 α}, Batteries.RBNode.zoom cut t path = (t', path')Batteries.RBNode.Path.Zoomed cut pathBatteries.RBNode.Path.Zoomed cut path'
          def Batteries.RBNode.Path.RootOrdered {α : Type u_1} (cmp : ααOrdering) :

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

            The ordering invariant for a Path.

            Equations
            Instances For
              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)

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

              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 xBatteries.RBNode.Path.RootOrdered cmp p x Batteries.RBNode.OnRoot (Batteries.RBNode.cmpEq cmp x) t') (h : Batteries.RBNode.WF cmp 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) :
              theorem Batteries.RBNode.find?_eq_zoom {α : Type u_1} {cut : αOrdering} {t : Batteries.RBNode α} (p : optParam (Batteries.RBNode.Path α) Batteries.RBNode.Path.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 xBatteries.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
              Instances For
                def Batteries.RBMap.alter.adapt {α : Type u_1} {β : Type u_2} (k : α) (f : Option βOption β) :
                Option (α × β)Option (α × β)

                Auxiliary definition for alter.

                Equations
                Instances For
                  @[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
                  Instances For