Documentation

Std.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 Std.RBNode.All.trivial {α : Type u_1} {p : αProp} (H : ∀ {x : α}, p x) {t : Std.RBNode α} :
theorem Std.RBNode.All_and {α : Type u_1} {p : αProp} {q : αProp} {t : Std.RBNode α} :
Std.RBNode.All (fun (a : α) => p a q a) t Std.RBNode.All p t Std.RBNode.All q t
theorem Std.RBNode.cmpLT.trans :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y z : α}, Std.RBNode.cmpLT cmp x yStd.RBNode.cmpLT cmp y zStd.RBNode.cmpLT cmp x z
theorem Std.RBNode.cmpLT.trans_l {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} (H : Std.RBNode.cmpLT cmp x y) {t : Std.RBNode α} (h : Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp y x) t) :
Std.RBNode.All (fun (x_1 : α) => Std.RBNode.cmpLT cmp x x_1) t
theorem Std.RBNode.cmpLT.trans_r {α : Type u_1} {cmp : ααOrdering} {x : α} {y : α} (H : Std.RBNode.cmpLT cmp x y) {a : Std.RBNode α} (h : Std.RBNode.All (fun (x_1 : α) => Std.RBNode.cmpLT cmp x_1 x) a) :
Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp x y) a
theorem Std.RBNode.cmpEq.lt_congr_left :
∀ {α : Sort u_1} {cmp : ααOrdering} {x y z : α}, Std.RBNode.cmpEq cmp x y(Std.RBNode.cmpLT cmp x z Std.RBNode.cmpLT cmp y z)
theorem Std.RBNode.cmpEq.lt_congr_right :
∀ {α : Sort u_1} {cmp : ααOrdering} {y z x : α}, Std.RBNode.cmpEq cmp y z(Std.RBNode.cmpLT cmp x y Std.RBNode.cmpLT cmp x z)
theorem Std.RBNode.Ordered.balance1 {α : Type u_1} {cmp : ααOrdering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) :

The balance1 function preserves the ordering invariants.

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

The balance2 function preserves the ordering invariants.

@[simp]
theorem Std.RBNode.balance2_All {α : Type u_1} {p : αProp} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} :
theorem Std.RBNode.insert_setBlack {α : Type u_1} {cmp : ααOrdering} {v : α} {t : Std.RBNode α} :
theorem Std.RBNode.All.ins {α : Type u_1} {p : αProp} {cmp : ααOrdering} {x : α} {t : Std.RBNode α} (h₁ : p x) (h₂ : Std.RBNode.All p t) :
theorem Std.RBNode.Ordered.ins {α : Type u_1} {cmp : ααOrdering} {x : α} {t : Std.RBNode α} :

The ins function preserves the ordering invariants.

theorem Std.RBNode.Ordered.insert :
∀ {α : Type u_1} {cmp : ααOrdering} {t : Std.RBNode α} {v : α}, Std.RBNode.Ordered cmp tStd.RBNode.Ordered cmp (Std.RBNode.insert cmp t v)

The insert function preserves the ordering invariants.

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

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 Std.RBNode.RedRed.of_false {p : Prop} :
    ∀ {α : Type u_1} {t : Std.RBNode α} {n : Nat}, ¬pStd.RBNode.RedRed p t n∃ (c : Std.RBColor), Std.RBNode.Balanced t c n

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

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

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

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

    The red-red invariant is monotonic in p.

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

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

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

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

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

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

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

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

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

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

    insert #

    theorem Std.RBNode.Balanced.ins {α : Type u_1} {c : Std.RBColor} {n : Nat} (cmp : ααOrdering) (v : α) {t : Std.RBNode α} (h : Std.RBNode.Balanced t 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 Std.RBNode.Balanced.insert {α : Type u_1} {c : Std.RBColor} {n : Nat} {cmp : ααOrdering} {v : α} {t : Std.RBNode α} (h : Std.RBNode.Balanced t c n) :
    ∃ (c' : Std.RBColor), ∃ (n' : Nat), Std.RBNode.Balanced (Std.RBNode.insert cmp t v) 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.)

    theorem Std.RBNode.All.setRed {α : Type u_1} {p : αProp} {t : Std.RBNode α} (h : Std.RBNode.All p t) :
    theorem Std.RBNode.Ordered.setRed {α : Type u_1} {cmp : ααOrdering} {t : Std.RBNode α} :

    The setRed function preserves the ordering invariants.

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

    The balLeft function preserves the ordering invariants.

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

    The balancing properties of the balLeft function.

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

    The balRight function preserves the ordering invariants.

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

    The balancing properties of the balRight function.

    theorem Std.RBNode.All.append :
    ∀ {α : Type u_1} {l r : Std.RBNode α} {p : αProp}, Std.RBNode.All p lStd.RBNode.All p rStd.RBNode.All p (Std.RBNode.append l r)
    theorem Std.RBNode.Ordered.append {α : Type u_1} {cmp : ααOrdering} {l : Std.RBNode α} {v : α} {r : Std.RBNode α} (lv : Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp x v) l) (vr : Std.RBNode.All (fun (x : α) => Std.RBNode.cmpLT cmp v x) r) (hl : Std.RBNode.Ordered cmp l) (hr : Std.RBNode.Ordered cmp r) :

    The append function preserves the ordering invariants.

    theorem Std.RBNode.Balanced.append {α : Type u_1} {c₁ : Std.RBColor} {n : Nat} {c₂ : Std.RBColor} {l : Std.RBNode α} {r : Std.RBNode α} (hl : Std.RBNode.Balanced l c₁ n) (hr : Std.RBNode.Balanced r c₂ n) :

    The balance properties of the append function.

    erase #

    def Std.RBNode.DelProp {α : Type u_1} (p : Std.RBColor) (t : Std.RBNode α) (n : Nat) :

    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
      theorem Std.RBNode.DelProp.redred {c : Std.RBColor} :
      ∀ {α : Type u_1} {t : Std.RBNode α} {n : Nat}, Std.RBNode.DelProp c t n∃ (n' : Nat), Std.RBNode.RedRed (c = Std.RBColor.black) t n'

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

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

      The del function preserves the ordering invariants.

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

      The del function has the DelProp property.

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

      The erase function preserves the ordering invariants.

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

      The erase function preserves the balance invariants.

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

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

      @[simp]
      theorem Std.RBNode.WF_iff {α : Type u_1} {cmp : ααOrdering} {t : Std.RBNode α} :

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

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

      The map function preserves the balance invariants.

      class Std.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 Std.RBNode.All.map {α : Type u_1} {β : Type u_2} {p : αProp} {q : βProp} {f : αβ} (H : ∀ {x : α}, p xq (f x)) {t : Std.RBNode α} :

        Sufficient condition for map to preserve an All quantifier.

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

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

        @[inline]
        def Std.RBSet.mapMonotone {α : Type u_1} {β : Type u_2} {cmpα : ααOrdering} {cmpβ : ββOrdering} (f : αβ) [Std.RBSet.IsMonotone cmpα cmpβ f] (t : Std.RBSet α cmpα) :
        Std.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 Std.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 Std.RBMap.Imp.instIsMonotoneProdProdByKeyFstByKeyFstMapSnd {α : Type u_1} {β : Type u_2} {γ : Type u_3} (cmp : ααOrdering) (f : αβγ) :
            Equations
            • =
            def Std.RBMap.mapVal {α : Type u_1} {β : Type u_2} {γ : Type u_3} {cmp : ααOrdering} (f : αβγ) (t : Std.RBMap α β cmp) :
            Std.RBMap α γ cmp

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

            Equations
            Instances For