Model implementations of tree map functions #
General infrastructure #
def
Std.DTreeMap.Internal.Impl.contains'
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α → Ordering)
(l : Impl α β)
:
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
- Std.DTreeMap.Internal.Impl.contains' k Std.DTreeMap.Internal.Impl.leaf = false
def
Std.DTreeMap.Internal.Impl.applyPartition
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
(k : α → Ordering)
(l : Impl α β)
(f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ)
:
δ
General tree-traversal function. Internal implementation detail of the tree map
Equations
def
Std.DTreeMap.Internal.Impl.applyPartition.go
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
(k : α → Ordering)
(l : Impl α β)
(f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ)
(ll : List ((a : α) × β a))
(m : Impl α β)
(hm : contains' k l = true → contains' k m = true)
(rr : List ((a : α) × β a))
:
δ
Equations
- One or more equations did not get rendered due to their size.
- Std.DTreeMap.Internal.Impl.applyPartition.go k l f ll Std.DTreeMap.Internal.Impl.leaf hm_2 rr = f ll Std.DTreeMap.Internal.Cell.empty ⋯ rr
def
Std.DTreeMap.Internal.Impl.applyCell
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
(k : α)
(l : Impl α β)
(f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ)
:
δ
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
- Std.DTreeMap.Internal.Impl.applyCell k Std.DTreeMap.Internal.Impl.leaf f_2 = f_2 Std.DTreeMap.Internal.Cell.empty Std.DTreeMap.Internal.Impl.applyCell.proof_5
inductive
Std.DTreeMap.Internal.Impl.ExplorationStep
(α : Type u)
(β : α → Type v)
[Ord α]
(k : α → Ordering)
:
Type (max u v)
Data structure used by the general tree-traversal function explore.
Internal implementation detail of the tree map
- lt
{α : Type u}
{β : α → Type v}
[Ord α]
{k : α → Ordering}
(a : α)
: k a = Ordering.lt → β a → List ((a : α) × β a) → ExplorationStep α β k
Needle was less than key at this node: return key-value pair and unexplored right subtree, recusion will continue in left subtree.
- eq
{α : Type u}
{β : α → Type v}
[Ord α]
{k : α → Ordering}
: List ((a : α) × β a) → Cell α β k → List ((a : α) × β a) → ExplorationStep α β k
Needle was equal to key at this node: return key-value pair and both unexplored subtrees, recursion will terminate.
- gt
{α : Type u}
{β : α → Type v}
[Ord α]
{k : α → Ordering}
: List ((a : α) × β a) → (a : α) → k a = Ordering.gt → β a → ExplorationStep α β k
Needle was larger than key at this node: return key-value pair and unexplored left subtree, recusion will containue in right subtree.
def
Std.DTreeMap.Internal.Impl.explore
{α : Type u}
{β : α → Type v}
{γ : Type w}
[Ord α]
(k : α → Ordering)
(init : γ)
(inner : γ → ExplorationStep α β k → γ)
(l : Impl α β)
:
γ
General tree-traversal function. Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
- Std.DTreeMap.Internal.Impl.explore k init inner Std.DTreeMap.Internal.Impl.leaf = inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq [] Std.DTreeMap.Internal.Cell.empty [])
theorem
Std.DTreeMap.Internal.Impl.applyPartition_go_step
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
{k : α → Ordering}
{init : δ}
(l₁ l₂ : List ((a : α) × β a))
(l l' : Impl α β)
(h : contains' k l' = true → contains' k l = true)
(f : δ → ExplorationStep α β k → δ)
:
applyPartition.go k l'
(fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = true → c.contains = true)
(r' : List ((a : α) × β a)) =>
f init (ExplorationStep.eq l'_1 c r'))
l₁ l h l₂ = applyPartition.go k l'
(fun (l'_1 : List ((a : α) × β a)) (c : Cell α β k) (x : contains' k l' = true → c.contains = true)
(r' : List ((a : α) × β a)) =>
f init (ExplorationStep.eq (l₁ ++ l'_1) c (r' ++ l₂)))
[] l h []
theorem
Std.DTreeMap.Internal.Impl.explore_eq_applyPartition
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
{k : α → Ordering}
(init : δ)
(l : Impl α β)
(f : δ → ExplorationStep α β k → δ)
(hfr :
∀ {k_1 : α} {hk : k k_1 = Ordering.lt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k}
{rr r : List ((a : α) × β a)} {init : δ},
f (f init (ExplorationStep.lt k_1 hk v r)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq ll c (rr ++ ⟨k_1, v⟩ :: r)))
(hfl :
∀ {k_1 : α} {hk : k k_1 = Ordering.gt} {v : β k_1} {ll : List ((a : α) × β a)} {c : Cell α β k}
{rr l : List ((a : α) × β a)} {init : δ},
f (f init (ExplorationStep.gt l k_1 hk v)) (ExplorationStep.eq ll c rr) = f init (ExplorationStep.eq (l ++ ⟨k_1, v⟩ :: ll) c rr))
:
noncomputable def
Std.DTreeMap.Internal.Impl.updateCell
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α)
(f : Cell α β (compare k) → Cell α β (compare k))
(l : Impl α β)
(hl : l.Balanced)
:
SizedBalancedTree α β (l.size - 1) (l.size + 1)
General "update the mapping for a given key" function. Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
Model functions #
def
Std.DTreeMap.Internal.Impl.get?ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(l : Impl α β)
(k : α)
:
Option (β k)
Model implementation of the get? function.
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
def
Std.DTreeMap.Internal.Impl.get!ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(l : Impl α β)
(k : α)
[Inhabited (β k)]
:
β k
Model implementation of the get! function.
Internal implementation detail of the tree map
def
Std.DTreeMap.Internal.Impl.getDₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
(l : Impl α β)
(fallback : β k)
:
β k
Model implementation of the getD function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.getDₘ k l fallback = (l.get?ₘ k).getD fallback
def
Std.DTreeMap.Internal.Impl.getKeyDₘ
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α)
(l : Impl α β)
(fallback : α)
:
α
Model implementation of the getKeyD function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.getKeyDₘ k l fallback = (l.getKey?ₘ k).getD fallback
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.leaf.reverse = Std.DTreeMap.Internal.Impl.leaf
- (Std.DTreeMap.Internal.Impl.inner size k' v l_1 r).reverse = Std.DTreeMap.Internal.Impl.inner size k' v r.reverse l_1.reverse
noncomputable def
Std.DTreeMap.Internal.Impl.insertₘ
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α)
(v : β k)
(l : Impl α β)
(h : l.Balanced)
:
Impl α β
Model implementation of the insert function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.insertₘ k v l h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.of k v) l h).impl
noncomputable def
Std.DTreeMap.Internal.Impl.eraseₘ
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α)
(t : Impl α β)
(h : t.Balanced)
:
Impl α β
Model implementation of the erase function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.eraseₘ k t h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.empty) t h).impl
noncomputable def
Std.DTreeMap.Internal.Impl.insertIfNewₘ
{α : Type u}
{β : α → Type v}
[Ord α]
(k : α)
(v : β k)
(l : Impl α β)
(h : l.Balanced)
:
Impl α β
Model implementation of the insertIfNew function.
Internal implementation detail of the tree map
Equations
- One or more equations did not get rendered due to their size.
noncomputable def
Std.DTreeMap.Internal.Impl.alterₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
(f : Option (β k) → Option (β k))
(t : Impl α β)
(h : t.Balanced)
:
Impl α β
Model implementation of the alter function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.alterₘ k f t h = (Std.DTreeMap.Internal.Impl.updateCell k (fun (x : Std.DTreeMap.Internal.Cell α β (compare k)) => Std.DTreeMap.Internal.Cell.alter f x) t h).impl
def
Std.DTreeMap.Internal.Impl.Const.getDₘ
{α : Type u}
{β : Type v}
[Ord α]
(l : Impl α fun (x : α) => β)
(k : α)
(fallback : β)
:
β
Model implementation of the getD function.
Internal implementation detail of the tree map
Equations
- Std.DTreeMap.Internal.Impl.Const.getDₘ l k fallback = (Std.DTreeMap.Internal.Impl.Const.get?ₘ l k).getD fallback
noncomputable def
Std.DTreeMap.Internal.Impl.Const.alterₘ
{α : Type u}
{β : Type v}
[Ord α]
[OrientedOrd α]
(k : α)
(f : Option β → Option β)
(t : Impl α fun (x : α) => β)
(h : t.Balanced)
:
Impl α fun (x : α) => β
Model implementation of the alter function.
Internal implementation detail of the tree map
Equations
Helper theorems for reasoning with key-value pairs #
Equivalence of function to model functions #
theorem
Std.DTreeMap.Internal.Impl.get?_eq_get?ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
(l : Impl α β)
:
theorem
Std.DTreeMap.Internal.Impl.get_eq_get?
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
(l : Impl α β)
{h : k ∈ l}
:
theorem
Std.DTreeMap.Internal.Impl.get!_eq_get!ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
[Inhabited (β k)]
(l : Impl α β)
:
theorem
Std.DTreeMap.Internal.Impl.getD_eq_getDₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
[LawfulEqOrd α]
(k : α)
(l : Impl α β)
(fallback : β k)
:
theorem
Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ'
{α : Type u}
{β : α → Type v}
[Ord α]
{l : Impl α β}
:
theorem
Std.DTreeMap.Internal.Impl.minEntry?ₘ'_eq_minEntry?ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
{l : Impl α β}
:
theorem
Std.DTreeMap.Internal.Impl.minEntry?_eq_minEntry?ₘ
{α : Type u}
{β : α → Type v}
[Ord α]
{l : Impl α β}
:
theorem
Std.DTreeMap.Internal.Impl.balanceLErase_eq_balance
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLErasePrecond l.size r.size}
:
theorem
Std.DTreeMap.Internal.Impl.balanceRErase_eq_balance
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLErasePrecond r.size l.size}
:
theorem
Std.DTreeMap.Internal.Impl.minView_kv_eq_minView!
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hl : l.Balanced}
{hr : r.Balanced}
{hlr : BalancedAtRoot l.size r.size}
:
theorem
Std.DTreeMap.Internal.Impl.maxView_kv_eq_maxView!
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hl : l.Balanced}
{hr : r.Balanced}
{hlr : BalancedAtRoot l.size r.size}
:
theorem
Std.DTreeMap.Internal.Impl.containsThenInsertIfNew!_snd_eq_insertIfNew!
{α : Type u}
{β : α → Type v}
[Ord α]
(t : Impl α β)
(a : α)
(b : β a)
: