Documentation

Batteries.Data.RBMap.WF

Lemmas for Red-black trees #

The main theorem in this file is WF_def, which shows that the RBNode.WF.mk constructor subsumes the others, by showing that insert and erase satisfy the red-black invariants.

theorem Batteries.RBNode.All.trivial {α : Type u_1} {p : αProp} (H : ∀ {x : α}, p x) {t : Batteries.RBNode α} :
theorem Batteries.RBNode.All_and {α : Type u_1} {p : αProp} {q : αProp} {t : Batteries.RBNode α} :
theorem Batteries.RBNode.cmpLT.flip :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y : α}, Batteries.RBNode.cmpLT cmp x yBatteries.RBNode.cmpLT (flip cmp) y x
theorem Batteries.RBNode.cmpLT.trans :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y z : α}, Batteries.RBNode.cmpLT cmp x yBatteries.RBNode.cmpLT cmp y zBatteries.RBNode.cmpLT cmp x z
theorem Batteries.RBNode.cmpLT.trans_l {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} (H : Batteries.RBNode.cmpLT cmp x y) {t : Batteries.RBNode α} (h : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp y x) t) :
Batteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x x_1) t
theorem Batteries.RBNode.cmpLT.trans_r {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} (H : Batteries.RBNode.cmpLT cmp x y) {a : Batteries.RBNode α} (h : Batteries.RBNode.All (fun (x_1 : α) => Batteries.RBNode.cmpLT cmp x_1 x) a) :
Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x y) a
theorem Batteries.RBNode.cmpEq.lt_congr_left :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y z : α}, Batteries.RBNode.cmpEq cmp x y(Batteries.RBNode.cmpLT cmp x z Batteries.RBNode.cmpLT cmp y z)
theorem Batteries.RBNode.cmpEq.lt_congr_right :
∀ {α : Sort u_1} {cmp : ααOrdering} {y z x : α}, Batteries.RBNode.cmpEq cmp y z(Batteries.RBNode.cmpLT cmp x y Batteries.RBNode.cmpLT cmp x z)
@[simp]
theorem Batteries.RBNode.reverse_reverse {α : Type u_1} (t : Batteries.RBNode α) :
t.reverse.reverse = t
theorem Batteries.RBNode.reverse_eq_iff {α : Type u_1} {t : Batteries.RBNode α} {t' : Batteries.RBNode α} :
t.reverse = t' t = t'.reverse
@[simp]
theorem Batteries.RBNode.reverse_balance1 {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balance1 v r).reverse = r.reverse.balance2 v l.reverse
@[simp]
theorem Batteries.RBNode.reverse_balance2 {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
(l.balance2 v r).reverse = r.reverse.balance1 v l.reverse
@[simp]
theorem Batteries.RBNode.All.reverse {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} :
theorem Batteries.RBNode.Ordered.reverse {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} :

The reverse function reverses the ordering invariants.

theorem Batteries.RBNode.Balanced.reverse {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {t : Batteries.RBNode α} :
t.Balanced c nt.reverse.Balanced c n
theorem Batteries.RBNode.Ordered.balance1 {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.Ordered cmp (l.balance1 v r)

The balance1 function preserves the ordering invariants.

@[simp]
theorem Batteries.RBNode.balance1_All {α : Type u_1} {p : αProp} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
theorem Batteries.RBNode.Ordered.balance2 {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
Batteries.RBNode.Ordered cmp (l.balance2 v r)

The balance2 function preserves the ordering invariants.

@[simp]
theorem Batteries.RBNode.balance2_All {α : Type u_1} {p : αProp} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} :
@[simp]
theorem Batteries.RBNode.reverse_setBlack {α : Type u_1} {t : Batteries.RBNode α} :
t.setBlack.reverse = t.reverse.setBlack
theorem Batteries.RBNode.Balanced.setBlack :
∀ {α : Type u_1} {t : Batteries.RBNode α} {c : Batteries.RBColor} {n : Nat}, t.Balanced c n∃ (n' : Nat), t.setBlack.Balanced Batteries.RBColor.black n'
theorem Batteries.RBNode.setBlack_idem {α : Type u_1} {t : Batteries.RBNode α} :
t.setBlack.setBlack = t.setBlack
@[simp]
theorem Batteries.RBNode.reverse_ins {α : Type u_1} {cmp : ααOrdering} {x : α} [inst : Batteries.OrientedCmp cmp] {t : Batteries.RBNode α} :
(Batteries.RBNode.ins cmp x t).reverse = Batteries.RBNode.ins (flip cmp) x t.reverse
theorem Batteries.RBNode.All.ins {α : Type u_1} {p : αProp} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α} (h₁ : p x) (h₂ : Batteries.RBNode.All p t) :
theorem Batteries.RBNode.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Batteries.RBNode α} :

The ins function preserves the ordering invariants.

@[simp]
theorem Batteries.RBNode.isRed_reverse {α : Type u_1} {t : Batteries.RBNode α} :
t.reverse.isRed = t.isRed
@[simp]
theorem Batteries.RBNode.reverse_insert {α : Type u_1} {cmp : ααOrdering} {x : α} [inst : Batteries.OrientedCmp cmp] {t : Batteries.RBNode α} :
(Batteries.RBNode.insert cmp t x).reverse = Batteries.RBNode.insert (flip cmp) t.reverse x
theorem Batteries.RBNode.insert_setBlack {α : Type u_1} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} :
(Batteries.RBNode.insert cmp t v).setBlack = (Batteries.RBNode.ins cmp v t).setBlack
theorem Batteries.RBNode.Ordered.insert :
∀ {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} {v : α}, Batteries.RBNode.Ordered cmp tBatteries.RBNode.Ordered cmp (Batteries.RBNode.insert cmp t v)

The insert function preserves the ordering invariants.

inductive Batteries.RBNode.RedRed (p : Prop) {α : Type u_1} :

The red-red invariant is a weakening of the red-black balance invariant which allows the root to be red with red children, but does not allow any other violations. It occurs as a temporary condition in the insert and erase functions.

The p parameter allows the .redred case to be dependent on an additional condition. If it is false, then this is equivalent to the usual red-black invariant.

Instances For
    theorem Batteries.RBNode.RedRed.of_false {p : Prop} :
    ∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, ¬pBatteries.RBNode.RedRed p t n∃ (c : Batteries.RBColor), t.Balanced c n

    When p is false, the red-red case is impossible so the tree is balanced.

    theorem Batteries.RBNode.RedRed.of_red {p : Prop} :
    ∀ {α : Type u_1} {a : Batteries.RBNode α} {x : α} {b : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.RedRed p (Batteries.RBNode.node Batteries.RBColor.red a x b) n∃ (c₁ : Batteries.RBColor), ∃ (c₂ : Batteries.RBColor), a.Balanced c₁ n b.Balanced c₂ n

    A red node with the red-red invariant has balanced children.

    theorem Batteries.RBNode.RedRed.imp {p : Prop} {q : Prop} :
    ∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, (pq)Batteries.RBNode.RedRed p t nBatteries.RBNode.RedRed q t n

    The red-red invariant is monotonic in p.

    theorem Batteries.RBNode.RedRed.reverse {p : Prop} :
    ∀ {α : Type u_1} {t : Batteries.RBNode α} {n : Nat}, Batteries.RBNode.RedRed p t nBatteries.RBNode.RedRed p t.reverse n
    theorem Batteries.RBNode.RedRed.setBlack :
    ∀ {α : Type u_1} {t : Batteries.RBNode α} {p : Prop} {n : Nat}, Batteries.RBNode.RedRed p t n∃ (n' : Nat), t.setBlack.Balanced Batteries.RBColor.black n'

    If t has the red-red invariant, then setting the root to black yields a balanced tree.

    theorem Batteries.RBNode.RedRed.balance1 {α : Type u_1} {p : Prop} {n : Nat} {c : Batteries.RBColor} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : Batteries.RBNode.RedRed p l n) (hr : r.Balanced c n) :
    ∃ (c : Batteries.RBColor), (l.balance1 v r).Balanced c (n + 1)

    The balance1 function repairs the balance invariant when the first argument is red-red.

    theorem Batteries.RBNode.RedRed.balance2 {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {p : Prop} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : l.Balanced c n) (hr : Batteries.RBNode.RedRed p r n) :
    ∃ (c : Batteries.RBColor), (l.balance2 v r).Balanced c (n + 1)

    The balance2 function repairs the balance invariant when the second argument is red-red.

    theorem Batteries.RBNode.balance1_eq {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hl : l.Balanced c n) :

    The balance1 function does nothing if the first argument is already balanced.

    theorem Batteries.RBNode.balance2_eq {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (hr : r.Balanced c n) :

    The balance2 function does nothing if the second argument is already balanced.

    insert #

    theorem Batteries.RBNode.Balanced.ins {α : Type u_1} {c : Batteries.RBColor} {n : Nat} (cmp : ααOrdering) (v : α) {t : Batteries.RBNode α} (h : t.Balanced c n) :

    The balance invariant of the ins function. The result of inserting into the tree either yields a balanced tree, or a tree which is almost balanced except that it has a red-red violation at the root.

    theorem Batteries.RBNode.Balanced.insert {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cmp : ααOrdering} {v : α} {t : Batteries.RBNode α} (h : t.Balanced c n) :
    ∃ (c' : Batteries.RBColor), ∃ (n' : Nat), (Batteries.RBNode.insert cmp t v).Balanced c' n'

    The insert function is balanced if the input is balanced. (We lose track of both the color and the black-height of the result, so this is only suitable for use on the root of the tree.)

    @[simp]
    theorem Batteries.RBNode.reverse_setRed {α : Type u_1} {t : Batteries.RBNode α} :
    t.setRed.reverse = t.reverse.setRed
    theorem Batteries.RBNode.All.setRed {α : Type u_1} {p : αProp} {t : Batteries.RBNode α} (h : Batteries.RBNode.All p t) :
    theorem Batteries.RBNode.Ordered.setRed {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} :

    The setRed function preserves the ordering invariants.

    @[simp]
    theorem Batteries.RBNode.reverse_balLeft {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
    (l.balLeft v r).reverse = r.reverse.balRight v l.reverse
    @[simp]
    theorem Batteries.RBNode.reverse_balRight {α : Type u_1} (l : Batteries.RBNode α) (v : α) (r : Batteries.RBNode α) :
    (l.balRight v r).reverse = r.reverse.balLeft v l.reverse
    theorem Batteries.RBNode.All.balLeft :
    ∀ {α : Type u_1} {p : αProp} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α}, Batteries.RBNode.All p lp vBatteries.RBNode.All p rBatteries.RBNode.All p (l.balLeft v r)
    theorem Batteries.RBNode.Ordered.balLeft {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
    Batteries.RBNode.Ordered cmp (l.balLeft v r)

    The balLeft function preserves the ordering invariants.

    theorem Batteries.RBNode.Balanced.balLeft :
    ∀ {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} {cr : Batteries.RBColor} {n : Nat}, Batteries.RBNode.RedRed True l nr.Balanced cr (n + 1)Batteries.RBNode.RedRed (cr = Batteries.RBColor.red) (l.balLeft v r) (n + 1)

    The balancing properties of the balLeft function.

    theorem Batteries.RBNode.All.balRight :
    ∀ {α : Type u_1} {p : αProp} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α}, Batteries.RBNode.All p lp vBatteries.RBNode.All p rBatteries.RBNode.All p (l.balRight v r)
    theorem Batteries.RBNode.Ordered.balRight {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
    Batteries.RBNode.Ordered cmp (l.balRight v r)

    The balRight function preserves the ordering invariants.

    theorem Batteries.RBNode.Balanced.balRight :
    ∀ {α : Type u_1} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} {cl : Batteries.RBColor} {n : Nat}, l.Balanced cl (n + 1)Batteries.RBNode.RedRed True r nBatteries.RBNode.RedRed (cl = Batteries.RBColor.red) (l.balRight v r) (n + 1)

    The balancing properties of the balRight function.

    @[irreducible]
    theorem Batteries.RBNode.All.append :
    ∀ {α : Type u_1} {l r : Batteries.RBNode α} {p : αProp}, Batteries.RBNode.All p lBatteries.RBNode.All p rBatteries.RBNode.All p (l.append r)
    @[irreducible]
    theorem Batteries.RBNode.Ordered.append {α : Type u_1} {cmp : ααOrdering} {l : Batteries.RBNode α} {v : α} {r : Batteries.RBNode α} (lv : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp x v) l) (vr : Batteries.RBNode.All (fun (x : α) => Batteries.RBNode.cmpLT cmp v x) r) (hl : Batteries.RBNode.Ordered cmp l) (hr : Batteries.RBNode.Ordered cmp r) :
    Batteries.RBNode.Ordered cmp (l.append r)

    The append function preserves the ordering invariants.

    @[irreducible]
    theorem Batteries.RBNode.Balanced.append {α : Type u_1} {c₁ : Batteries.RBColor} {n : Nat} {c₂ : Batteries.RBColor} {l : Batteries.RBNode α} {r : Batteries.RBNode α} (hl : l.Balanced c₁ n) (hr : r.Balanced c₂ n) :

    The balance properties of the append function.

    erase #

    The invariant of the del function.

    • If the input tree is black, then the result of deletion is a red-red tree with black-height lowered by 1.
    • If the input tree is red or nil, then the result of deletion is a balanced tree with some color and the same black-height.
    Equations
    Instances For

      The DelProp property is a strengthened version of the red-red invariant.

      theorem Batteries.RBNode.All.del {α : Type u_1} {p : αProp} {cut : αOrdering} {t : Batteries.RBNode α} :
      theorem Batteries.RBNode.Ordered.del {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} :

      The del function preserves the ordering invariants.

      theorem Batteries.RBNode.Balanced.del {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cut : αOrdering} {t : Batteries.RBNode α} (h : t.Balanced c n) :

      The del function has the DelProp property.

      theorem Batteries.RBNode.Ordered.erase {α : Type u_1} {cmp : ααOrdering} {cut : αOrdering} {t : Batteries.RBNode α} (h : Batteries.RBNode.Ordered cmp t) :

      The erase function preserves the ordering invariants.

      theorem Batteries.RBNode.Balanced.erase {α : Type u_1} {c : Batteries.RBColor} {n : Nat} {cut : αOrdering} {t : Batteries.RBNode α} (h : t.Balanced c n) :
      ∃ (n : Nat), (Batteries.RBNode.erase cut t).Balanced Batteries.RBColor.black n

      The erase function preserves the balance invariants.

      theorem Batteries.RBNode.WF.out {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} (h : Batteries.RBNode.WF cmp t) :
      Batteries.RBNode.Ordered cmp t ∃ (c : Batteries.RBColor), ∃ (n : Nat), t.Balanced c n

      The well-formedness invariant implies the ordering and balance properties.

      @[simp]
      theorem Batteries.RBNode.WF_iff {α : Type u_1} {cmp : ααOrdering} {t : Batteries.RBNode α} :
      Batteries.RBNode.WF cmp t Batteries.RBNode.Ordered cmp t ∃ (c : Batteries.RBColor), ∃ (n : Nat), t.Balanced c n

      The well-formedness invariant for a red-black tree is exactly the mk constructor, because the other constructors of WF are redundant.

      theorem Batteries.RBNode.Balanced.map {α : Type u_1} {c : Batteries.RBColor} {n : Nat} :
      ∀ {α_1 : Type u_2} {f : αα_1} {t : Batteries.RBNode α}, t.Balanced c n(Batteries.RBNode.map f t).Balanced c n

      The map function preserves the balance invariants.

      class Batteries.RBNode.IsMonotone {α : Sort u_1} {β : Sort u_2} (cmpα : ααOrdering) (cmpβ : ββOrdering) (f : αβ) :

      The property of a map function f which ensures the map operation is valid.

      Instances
        theorem Batteries.RBNode.IsMonotone.lt_mono {α : Sort u_1} {β : Sort u_2} {cmpα : ααOrdering} {cmpβ : ββOrdering} {f : αβ} [self : Batteries.RBSet.IsMonotone cmpα cmpβ f] {x : α} {y : α} :
        Batteries.RBNode.cmpLT cmpα x yBatteries.RBNode.cmpLT cmpβ (f x) (f y)

        If x < y then f x < f y.

        theorem Batteries.RBNode.All.map {α : Type u_1} {β : Type u_2} {p : αProp} {q : βProp} {f : αβ} (H : ∀ {x : α}, p xq (f x)) {t : Batteries.RBNode α} :

        Sufficient condition for map to preserve an All quantifier.

        theorem Batteries.RBNode.Ordered.map {α : Type u_1} {β : Type u_2} {cmpα : ααOrdering} {cmpβ : ββOrdering} (f : αβ) [Batteries.RBSet.IsMonotone cmpα cmpβ f] {t : Batteries.RBNode α} :

        The map function preserves the order invariants if f is monotone.

        @[inline]
        def Batteries.RBSet.mapMonotone {α : Type u_1} {β : Type u_2} {cmpα : ααOrdering} {cmpβ : ββOrdering} (f : αβ) [Batteries.RBSet.IsMonotone cmpα cmpβ f] (t : Batteries.RBSet α cmpα) :

        O(n). Map a function on every value in the set. This requires IsMonotone on the function in order to preserve the order invariant. If the function is not monotone, use RBSet.map instead.

        Equations
        Instances For
          @[inline]
          def Batteries.RBMap.Imp.mapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : αβγ) :
          α × βα × γ

          Applies f to the second component. We extract this as a function so that IsMonotone (mapSnd f) can be an instance.

          Equations
          Instances For
            instance Batteries.RBMap.Imp.instIsMonotoneProdByKeyFstMapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : ααOrdering) (f : αβγ) :
            Equations
            • =
            def Batteries.RBMap.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : ααOrdering} (f : αβγ) (t : Batteries.RBMap α β cmp) :
            Batteries.RBMap α γ cmp

            O(n). Map a function on the values in the map.

            Equations
            Instances For