Balanced
predicate #
This file defines what it means for a tree map to be balanced. This definition is encoded in the
Balanced
predicate.
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
Instances For
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
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)
:
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