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]

abbrev Std.DTreeMap.Internal.Impl.BalanceLPrecond (left right : Nat) : Prop

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

@[reducible, inline]

abbrev Std.DTreeMap.Internal.Impl.BalanceLErasePrecond (left right : Nat) : Prop

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

def Std.DTreeMap.Internal.Impl.tacticTree_tac : Lean.ParserDescr

Internal implementation detail of the tree map

def Std.DTreeMap.Internal.Impl.«term✓» : Lean.ParserDescr

Internal implementation detail of the tree map

theorem Std.DTreeMap.Internal.Impl.BalanceLPrecond.erase {left right : Nat} : BalanceLPrecond left right → BalanceLErasePrecond left right

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.

@[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.

@[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).

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.

@[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.

@[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).

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.

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).

Lemmas about balancing operations

theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.erase_left {l l' r : Nat} : BalancedAtRoot l r → l - 1 ≤ l' → l' ≤ l → BalanceLErasePrecond r l'

theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.erase_right {l r r' : Nat} : BalancedAtRoot l r → r - 1 ≤ r' → r' ≤ r → BalanceLErasePrecond l r'

theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.adjust_left {l l' r : Nat} : BalancedAtRoot l r → l - 1 ≤ l' → l' ≤ l + 1 → BalanceLErasePrecond l' r ∨ BalanceLErasePrecond r l'

theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.adjust_right {l r r' : Nat} : BalancedAtRoot l r → r - 1 ≤ r' → r' ≤ r + 1 → BalanceLErasePrecond l r' ∨ BalanceLErasePrecond r' l

theorem Std.DTreeMap.Internal.Impl.balanceLErasePrecond_zero_iff {n : Nat} : BalanceLErasePrecond 0 n ↔ n ≤ 1

theorem Std.DTreeMap.Internal.Impl.balanceLErasePrecond_zero_iff' {n : Nat} : BalanceLErasePrecond n 0 ↔ n ≤ 3

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.

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.

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.

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.

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.

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

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

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

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₁.Balanced → t₁ = 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) : (balanceL! k v l r).Balanced

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) : (balanceR! k v l r).Balanced

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