Documentation

Std.Data.DTreeMap.Internal.Balancing

Balancing operations #

This file contains the implementation of internal balancing operations used by the modification operations of the tree map and proves that these operations produce balanced trees.

Implementation #

Although it is desirable to separate the implementation from the balancedness proofs as much as possible, we want the Lean to optimize away some impossible case distinctions. Therefore, we need to prove them impossible in the implementation itself. Most proofs are automated using a custom tactic tree_tac, but the proof terms tend to be large, so we should be cautious.

Implementations marked with an exclamation mark do not rely on balancing proofs and just panic when a case occurs that is impossible for balanced trees. These implementations are slower because the impossible cases need to be checked for.

Implementation #

@[reducible, inline]

Precondition for balanceL: at most one element was added to left subtree.

Equations
    Instances For
      @[reducible, inline]

      Precondition for balanceLErase. As Breitner et al. remark, "not very educational".

      Equations
        Instances For

          Internal implementation detail of the tree map

          Equations
            Instances For

              Internal implementation detail of the tree map

              Equations
                Instances For

                  balanceL variants #

                  @[inline]
                  def Std.DTreeMap.Internal.Impl.balanceL {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond l.size r.size) :
                  Impl α β

                  Rebalances a tree after at most one element was added to the left subtree. Uses balancing information to show that some cases are impossible.

                  Equations
                    Instances For
                      @[inline]
                      def Std.DTreeMap.Internal.Impl.balanceLErase {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                      Impl α β

                      Slower version of balanceL with weaker balancing assumptions that hold after erasing from the right side of the tree.

                      Equations
                        Instances For
                          @[inline]
                          def Std.DTreeMap.Internal.Impl.balanceL! {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                          Impl α β

                          Slower version of balanceL which can be used in the complete absence of balancing information but still assumes that the preconditions of balanceL or balanceL are satisfied (otherwise panics).

                          Equations
                            Instances For

                              balanceR variants #

                              @[inline]
                              def Std.DTreeMap.Internal.Impl.balanceR {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond r.size l.size) :
                              Impl α β

                              Rebalances a tree after at most one element was added to the right subtree. Uses balancing information to show that some cases are impossible.

                              Equations
                                Instances For
                                  @[inline]
                                  def Std.DTreeMap.Internal.Impl.balanceRErase {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                  Impl α β

                                  Slower version of balanceR with weaker balancing assumptions that hold after erasing from the left side of the tree.

                                  Equations
                                    Instances For
                                      @[inline]
                                      def Std.DTreeMap.Internal.Impl.balanceR! {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                                      Impl α β

                                      Slower version of balanceR which can be used in the complete absence of balancing information but still assumes that the preconditions of balanceR or balanceRErase are satisfied (otherwise panics).

                                      Equations
                                        Instances For

                                          balance variants #

                                          def Std.DTreeMap.Internal.Impl.balance {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) (hl : l.Balanced) (hr : r.Balanced) (h : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                          Impl α β

                                          Rebalances a tree after at most one element was added or removed from either subtree.

                                          Equations
                                            Instances For
                                              def Std.DTreeMap.Internal.Impl.balance! {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                                              Impl α β

                                              Slower version of balance which can be used in the complete absence of balancing information but still assumes that the preconditions of balance are satisfied (otherwise panics).

                                              Equations
                                                Instances For

                                                  Lemmas about balancing operations #

                                                  The following definitions are not actually used by the tree map implementation. They are only used in the model function balanceₘ, which exists for proof purposes only.

                                                  The terminology is consistent with the comment above the balance implementation in Haskell.

                                                  def Std.DTreeMap.Internal.Impl.bin {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                                                  Impl α β

                                                  Constructor for an inner node with the correct size.

                                                  Equations
                                                    Instances For
                                                      theorem Std.DTreeMap.Internal.Impl.size_bin {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                                                      (bin k v l r).size = l.size + 1 + r.size
                                                      def Std.DTreeMap.Internal.Impl.singleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rk : α) (rv : β rk) (rl rr : Impl α β) :
                                                      Impl α β

                                                      A single left rotation.

                                                      Equations
                                                        Instances For
                                                          theorem Std.DTreeMap.Internal.Impl.size_singleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rk : α) (rv : β rk) (rl rr : Impl α β) :
                                                          (singleL k v l rk rv rl rr).size = (bin k v l (bin rk rv rl rr)).size
                                                          def Std.DTreeMap.Internal.Impl.singleR {α : Type u} {β : αType v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Impl α β) :
                                                          Impl α β

                                                          A single right rotation.

                                                          Equations
                                                            Instances For
                                                              theorem Std.DTreeMap.Internal.Impl.size_singleR {α : Type u} {β : αType v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Impl α β) :
                                                              (singleR k v lk lv ll lr r).size = (bin k v (bin lk lv ll lr) r).size
                                                              def Std.DTreeMap.Internal.Impl.doubleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rk : α) (rv : β rk) (rlk : α) (rlv : β rlk) (rll rlr rr : Impl α β) :
                                                              Impl α β

                                                              A double left rotation.

                                                              Equations
                                                                Instances For
                                                                  theorem Std.DTreeMap.Internal.Impl.size_doubleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rk : α) (rv : β rk) (rlk : α) (rlv : β rlk) (rll rlr rr : Impl α β) :
                                                                  (doubleL k v l rk rv rlk rlv rll rlr rr).size = (bin k v l (bin rk rv (bin rlk rlv rll rlr) rr)).size
                                                                  def Std.DTreeMap.Internal.Impl.doubleR {α : Type u} {β : αType v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll : Impl α β) (lrk : α) (lrv : β lrk) (lrl lrr r : Impl α β) :
                                                                  Impl α β

                                                                  A double right rotation.

                                                                  Equations
                                                                    Instances For
                                                                      theorem Std.DTreeMap.Internal.Impl.size_doubleR {α : Type u} {β : αType v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll : Impl α β) (lrk : α) (lrv : β lrk) (lrl lrr r : Impl α β) :
                                                                      (doubleR k v lk lv ll lrk lrv lrl lrr r).size = (bin k v (bin lk lv ll (bin lrk lrv lrl lrr)) r).size
                                                                      def Std.DTreeMap.Internal.Impl.rotateL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rk : α) (rv : β rk) (rl rr : Impl α β) :
                                                                      Impl α β

                                                                      Internal implementation detail of the tree map

                                                                      Equations
                                                                        Instances For
                                                                          theorem Std.DTreeMap.Internal.Impl.size_rotateL {α : Type u} {β : αType v} {k : α} {v : β k} {l : Impl α β} {rk : α} {rv : β rk} {rl rr : Impl α β} (h : rl.Balanced) :
                                                                          (rotateL k v l rk rv rl rr).size = (bin k v l (bin rk rv rl rr)).size
                                                                          def Std.DTreeMap.Internal.Impl.rotateR {α : Type u} {β : αType v} (k : α) (v : β k) (lk : α) (lv : β lk) (ll lr r : Impl α β) :
                                                                          Impl α β

                                                                          Internal implementation detail of the tree map

                                                                          Equations
                                                                            Instances For
                                                                              theorem Std.DTreeMap.Internal.Impl.size_rotateR {α : Type u} {β : αType v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Impl α β} (h : lr.Balanced) :
                                                                              (rotateR k v lk lv ll lr r).size = (bin k v (bin lk lv ll lr) r).size
                                                                              def Std.DTreeMap.Internal.Impl.balanceₘ {α : Type u} {β : αType v} (k : α) (v : β k) (l r : Impl α β) :
                                                                              Impl α β

                                                                              Internal implementation detail of the tree map

                                                                              Equations
                                                                                Instances For
                                                                                  theorem Std.DTreeMap.Internal.Impl.balance!_eq_balanceₘ {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  balance! k v l r = balanceₘ k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.Balanced.map {α : Type u} {β : αType v} {t₁ t₂ : Impl α β} :
                                                                                  t₁.Balancedt₁ = t₂t₂.Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_singleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rs : Nat) (rk : α) (rv : β rk) (rl rr : Impl α β) (hl : l.Balanced) (hr : (inner rs rk rv rl rr).Balanced) (hlr : BalanceLErasePrecond l.size rs BalanceLErasePrecond rs l.size) (hh : rs > delta * l.size) (hx : rl.size < ratio * rr.size) :
                                                                                  (singleL k v l rk rv rl rr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_singleR {α : Type u} {β : αType v} (k : α) (v : β k) (ls : Nat) (lk : α) (lv : β lk) (ll lr r : Impl α β) (hl : (inner ls lk lv ll lr).Balanced) (hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size BalanceLErasePrecond r.size ls) (hh : ls > delta * r.size) (hx : lr.size < ratio * ll.size) :
                                                                                  (singleR k v lk lv ll lr r).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_doubleL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rs : Nat) (rk : α) (rv : β rk) (rls : Nat) (rlk : α) (rlv : β rlk) (rll rlr rr : Impl α β) (hl : l.Balanced) (hr : (inner rs rk rv (inner rls rlk rlv rll rlr) rr).Balanced) (hlr : BalanceLErasePrecond l.size rs BalanceLErasePrecond rs l.size) (hh : rs > delta * l.size) (hx : ¬rls < ratio * rr.size) :
                                                                                  (doubleL k v l rk rv rlk rlv rll rlr rr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_doubleR {α : Type u} {β : αType v} (k : α) (v : β k) (ls : Nat) (lk : α) (lv : β lk) (ll : Impl α β) (lrs : Nat) (lrk : α) (lrv : β lrk) (lrl lrr r : Impl α β) (hl : (inner ls lk lv ll (inner lrs lrk lrv lrl lrr)).Balanced) (hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size BalanceLErasePrecond r.size ls) (hh : ls > delta * r.size) (hx : ¬lrs < ratio * ll.size) :
                                                                                  (doubleR k v lk lv ll lrk lrv lrl lrr r).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_rotateL {α : Type u} {β : αType v} (k : α) (v : β k) (l : Impl α β) (rs : Nat) (rk : α) (rv : β rk) (rl rr : Impl α β) (hl : l.Balanced) (hr : (inner rs rk rv rl rr).Balanced) (hlr : BalanceLErasePrecond l.size rs BalanceLErasePrecond rs l.size) (hh : rs > delta * l.size) :
                                                                                  (rotateL k v l rk rv rl rr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_rotateR {α : Type u} {β : αType v} (k : α) (v : β k) (ls : Nat) (lk : α) (lv : β lk) (ll lr r : Impl α β) (hl : (inner ls lk lv ll lr).Balanced) (hr : r.Balanced) (hlr : BalanceLErasePrecond ls r.size BalanceLErasePrecond r.size ls) (hh : ls > delta * r.size) :
                                                                                  (rotateR k v lk lv ll lr r).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceL_eq_balanceLErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond l.size r.size} :
                                                                                  balanceL k v l r hlb hrb hlr = balanceLErase k v l r hlb hrb
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceLErase_eq_balanceL! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size} :
                                                                                  balanceLErase k v l r hlb hrb hlr = balanceL! k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceL!_eq_balance! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                                                                                  balanceL! k v l r = balance! k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceR_eq_balanceRErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLPrecond r.size l.size} :
                                                                                  balanceR k v l r hlb hrb hlr = balanceRErase k v l r hlb hrb
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceRErase_eq_balanceR! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond r.size l.size} :
                                                                                  balanceRErase k v l r hlb hrb hlr = balanceR! k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanceR!_eq_balance! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                                                                  balanceR! k v l r = balance! k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balance_eq_balance! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} {hlb : l.Balanced} {hrb : r.Balanced} {hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size} :
                                                                                  balance k v l r hlb hrb hlr = balance! k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balance_eq_inner {α : Type u} {β : αType v} [Ord α] {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (hl : (inner sz k v l r).Balanced) {h : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size} :
                                                                                  balance k v l r h = inner sz k v l r
                                                                                  theorem Std.DTreeMap.Internal.Impl.balance!_desc {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  (balance! k v l r).size = l.size + 1 + r.size (balance! k v l r).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balance! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  (balance! k v l r).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balance! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  (balance! k v l r).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  (balance k v l r hlb hrb hlr).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balance_balance {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size BalanceLErasePrecond r.size l.size) :
                                                                                  (balance k v l r hlb hrb hlr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceL! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                                                                                  (balanceL! k v l r).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceL! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceLErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                                                                                  (balanceLErase k v l r hlb hrb hlr).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceLErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond l.size r.size) :
                                                                                  (balanceLErase k v l r hlb hrb hlr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceL {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond l.size r.size) :
                                                                                  (balanceL k v l r hlb hrb hlr).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceL {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond l.size r.size) :
                                                                                  (balanceL k v l r hlb hrb hlr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceR! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                                                                  (balanceR! k v l r).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceR! {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceRErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                                                                  (balanceRErase k v l r hlb hrb hlr).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceRErase {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLErasePrecond r.size l.size) :
                                                                                  (balanceRErase k v l r hlb hrb hlr).Balanced
                                                                                  theorem Std.DTreeMap.Internal.Impl.size_balanceR {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond r.size l.size) :
                                                                                  (balanceR k v l r hlb hrb hlr).size = l.size + 1 + r.size
                                                                                  theorem Std.DTreeMap.Internal.Impl.balanced_balanceR {α : Type u} {β : αType v} {k : α} {v : β k} {l r : Impl α β} (hlb : l.Balanced) (hrb : r.Balanced) (hlr : BalanceLPrecond r.size l.size) :
                                                                                  (balanceR k v l r hlb hrb hlr).Balanced