Balanced predicate

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

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)

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.

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

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_zero : BalancedAtRoot 0 0

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_one : BalancedAtRoot 0 1

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_zero : BalancedAtRoot 1 0

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_one : BalancedAtRoot 1 1

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_two_one : BalancedAtRoot 2 1

@[simp]

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_one_two : BalancedAtRoot 1 2

theorem Std.DTreeMap.Internal.Impl.balanced_one_leaf_leaf {α : Type u} {β : α → Type v} {k : α} {v : β k} : (inner 1 k v leaf leaf).Balanced

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff {n : Nat} : BalancedAtRoot 0 n ↔ n ≤ 1

theorem Std.DTreeMap.Internal.Impl.balancedAtRoot_zero_iff' {n : Nat} : BalancedAtRoot n 0 ↔ n ≤ 1

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

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

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

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

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

theorem Std.DTreeMap.Internal.Impl.BalancedAtRoot.symm {l r : Nat} (h : BalancedAtRoot l r) : BalancedAtRoot r l