# `Balanced` predicate #

This file defines what it means for a tree map to be balanced. This definition is encoded in the `Balanced` predicate.

source
def Std.DTreeMap.Internal.Impl.BalancedAtRoot (left right : Nat) :
Prop

Predicate for local balance at a node of the tree. We don't provide API for this, preferring instead to use automation to dispatch goals about balance.

Equations

- Std.DTreeMap.Internal.Impl.BalancedAtRoot left right = (left + right ≤ 1 ∨ left ≤ Std.DTreeMap.Internal.delta * right ∧ right ≤ Std.DTreeMap.Internal.delta * left)

Instances For

source
inductive Std.DTreeMap.Internal.Impl.Balanced {α : Type u} {β : α → Type v} :
Impl α β → Prop

Predicate that states that the stored size information in a tree is correct and that it is balanced.

- leaf {α : Type u} {β : α → Type v} : Impl.leaf.Balanced

  Leaf is balanced.

- inner {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} : l.Balanced → r.Balanced → BalancedAtRoot l.size r.size → sz = l.size + 1 + r.size → (Impl.inner sz k v l r).Balanced

  Inner node is balanced if it is locally balanced, both children are balanced and size information is correct.

Instances For

source
theorem Std.DTreeMap.Internal.Impl.balanced_inner_iff {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
(inner sz k v l r).Balanced ↔ l.Balanced ∧ r.Balanced ∧ BalancedAtRoot l.size r.size ∧ sz = l.size + 1 + r.size
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_zero :
BalancedAtRoot 0 0
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_one :
BalancedAtRoot 0 1
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_zero :
BalancedAtRoot 1 0
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_one :
BalancedAtRoot 1 1
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_two_one :
BalancedAtRoot 2 1
source
@[simp]
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_two :
BalancedAtRoot 1 2
source
theorem Std.DTreeMap.Internal.Impl.balanced_one_leaf_leaf {α : Type u} {β : α → Type v} {k : α} {v : β k} :
(inner 1 k v leaf leaf).Balanced
source
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff {n : Nat} :
BalancedAtRoot 0 n ↔ n ≤ 1
source
theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff' {n : Nat} :
BalancedAtRoot n 0 ↔ n ≤ 1
source
theorem Std.DTreeMap.Internal.Impl.Balanced.one_le {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} (h : (Impl.inner sz k v l r).Balanced) :
1 ≤ sz
source
theorem Std.DTreeMap.Internal.Impl.Balanced.eq {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
(Impl.inner sz k v l r).Balanced → sz = l.size + 1 + r.size
source
theorem Std.DTreeMap.Internal.Impl.Balanced.left {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
(Impl.inner sz k v l r).Balanced → l.Balanced
source
theorem Std.DTreeMap.Internal.Impl.Balanced.right {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
(Impl.inner sz k v l r).Balanced → r.Balanced
source
theorem Std.DTreeMap.Internal.Impl.Balanced.at_root {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} :
(Impl.inner sz k v l r).Balanced → BalancedAtRoot l.size r.size
source
theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.symm {l r : Nat} (h : BalancedAtRoot l r) :
BalancedAtRoot r l