Low-level implementation of the size-bounded tree

This file contains the basic definition implementing the functionality of the size-bounded trees.

inductive Std.DTreeMap.Internal.Impl (α : Type u) (β : α → Type v) : Type (max u v)

(Implementation detail) The actual inductive type for the size-balanced tree data structure.

• inner {α : Type u} {β : α → Type v} (size : Nat) (k : α) (v : β k) (l r : Impl α β) : Impl α β

  (Implementation detail)

• leaf {α : Type u} {β : α → Type v} : Impl α β

  (Implementation detail)

def Std.DTreeMap.Internal.instInhabitedImpl.default {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} : Impl a✝ a✝¹

Equations

• Std.DTreeMap.Internal.instInhabitedImpl.default = Std.DTreeMap.Internal.Impl.leaf

instance Std.DTreeMap.Internal.instInhabitedImpl {a✝ : Type u_1} {a✝¹ : a✝ → Type u_2} : Inhabited (Impl a✝ a✝¹)

Equations

• Std.DTreeMap.Internal.instInhabitedImpl = { default := Std.DTreeMap.Internal.instInhabitedImpl.default }

@[inline]

def Std.DTreeMap.Internal.delta : Nat

The "delta" parameter of the size-bounded tree. Controls how imbalanced the tree can be.

Equations

• Std.DTreeMap.Internal.delta = 3

@[inline]

def Std.DTreeMap.Internal.ratio : Nat

The "ratio" parameter of the size-bounded tree. Controls how aggressive the rebalancing operations are.

Equations

• Std.DTreeMap.Internal.ratio = 2

size

In contrast to other functions, size is defined here because it is required to define the Balanced predicate (see Std.Data.DTreeMap.Internal.Balanced).

@[inline]

def Std.DTreeMap.Internal.Impl.size {α : Type u} {β : α → Type v} : Impl α β → Nat

The size information stored in the tree.

Equations

• (Std.DTreeMap.Internal.Impl.inner sz k v l r).size = sz
• Std.DTreeMap.Internal.Impl.leaf.size = 0

theorem Std.DTreeMap.Internal.Impl.size_leaf {α : Type u} {β : α → Type v} : leaf.size = 0

theorem Std.DTreeMap.Internal.Impl.size_inner {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} : (inner sz k v l r).size = sz

toListModel

toListModel is defined here because it is required to define the Ordered predicate.

def Std.DTreeMap.Internal.Impl.toListModel {α : Type u} {β : α → Type v} : Impl α β → List ((a : α) × β a)

Flattens a tree into a list of key-value pairs. This function is defined for verification purposes and should not be executed because it is very inefficient.

Equations

• Std.DTreeMap.Internal.Impl.leaf.toListModel = []
• (Std.DTreeMap.Internal.Impl.inner size k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_leaf {α : Type u} {β : α → Type v} : leaf.toListModel = []

@[simp]

theorem Std.DTreeMap.Internal.Impl.toListModel_inner {α : Type u} {β : α → Type v} {sz : Nat} {k : α} {v : β k} {l r : Impl α β} : (inner sz k v l r).toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel