Lemmas relating operations on well-formed size-bounded trees to operations on lists #
This file contains lemmas that relate Impl.toListModel to the queries and operations on Impl.
The Impl.Ordered property, being defined in terms of Impl.toListModel, is then shown to be
preserved by all of the operations.
However, this file does not contain lemmas that relate operations besides Impl.toListModel to
each other or themselves. Such proofs crucially build on top of the lemmas in this file and
can be found in Std.Data.Internal.Lemmas.
toListModel for balancing operations #
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_balance
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLErasePrecond l.size r.size ∨ BalanceLErasePrecond r.size l.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_balanceL
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLPrecond l.size r.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_balanceLErase
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLErasePrecond l.size r.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_balanceR
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLPrecond r.size l.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_balanceRErase
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hlb : l.Balanced}
{hrb : r.Balanced}
{hlr : BalanceLErasePrecond r.size l.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_minView
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hl : l.Balanced}
{hr : r.Balanced}
{hlr : BalancedAtRoot l.size r.size}
:
⟨(minView k v l r hl hr hlr).k, (minView k v l r hl hr hlr).v⟩ :: (minView k v l r hl hr hlr).tree.impl.toListModel = l.toListModel ++ ⟨k, v⟩ :: r.toListModel
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_maxView
{α : Type u}
{β : α → Type v}
{k : α}
{v : β k}
{l r : Impl α β}
{hl : l.Balanced}
{hr : r.Balanced}
{hlr : BalancedAtRoot l.size r.size}
:
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_glue
{α : Type u}
{β : α → Type v}
{l r : Impl α β}
{hl : l.Balanced}
{hr : r.Balanced}
{hlr : BalancedAtRoot l.size r.size}
:
Verification of model functions #
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_gt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.gt)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel ++ ⟨k', v'⟩ :: List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) r.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_eq
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.eq)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = l.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_gt_of_lt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.lt)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_find?_of_gt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.gt)
(ho : (inner sz k' v' l r).Ordered)
:
List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) r.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_find?_of_eq
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.eq)
(ho : (inner sz k' v' l r).Ordered)
:
List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = some ⟨k', v'⟩
theorem
Std.DTreeMap.Internal.Impl.toListModel_find?_of_lt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.lt)
(ho : (inner sz k' v' l r).Ordered)
:
List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) (inner sz k' v' l r).toListModel = List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_gt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.gt)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) r.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_eq
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.eq)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = r.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_filter_lt_of_lt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.lt)
(ho : (inner sz k' v' l r).Ordered)
:
List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) (inner sz k' v' l r).toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel ++ ⟨k', v'⟩ :: r.toListModel
instance
Std.DTreeMap.Internal.Impl.instIsStrictCutCompare
{α : Type u}
[Ord α]
[TransOrd α]
{k : α}
:
theorem
Std.DTreeMap.Internal.Impl.findCell_of_gt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.gt)
(ho : (inner sz k' v' l r).Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.findCell_of_eq
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.eq)
(ho : (inner sz k' v' l r).Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.findCell_of_lt
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsCut compare k]
{sz : Nat}
{k' : α}
{v' : β k'}
{l r : Impl α β}
(hcmp : k k' = Ordering.lt)
(ho : (inner sz k' v' l r).Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.toListModel_updateCell
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{f : Cell α β (compare k) → Cell α β (compare k)}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(updateCell k f l hlb).impl.toListModel = List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.gt) l.toListModel ++ (f (List.findCell l.toListModel (compare k))).inner.toList ++ List.filter (fun (x : (a : α) × β a) => compare k x.fst == Ordering.lt) l.toListModel
theorem
Std.DTreeMap.Internal.Impl.toListModel_eq_append
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
(k : α → Ordering)
[Internal.IsStrictCut compare k]
{l : Impl α β}
(ho : l.Ordered)
:
l.toListModel = List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel ++ (List.find? (fun (x : (a : α) × β a) => k x.fst == Ordering.eq) l.toListModel).toList ++ List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel
Connecting the tree maps machinery to the hash map machinery #
theorem
Std.DTreeMap.Internal.Impl.exists_cell_of_updateAtKey
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
(l : Impl α β)
(hlb : l.Balanced)
(hlo : l.Ordered)
(k : α)
(f : Cell α β (compare k) → Cell α β (compare k))
:
∃ (l' : List ((a : α) × β a)), l.toListModel.Perm
((List.find? (fun (x : (a : α) × β a) => compare k x.fst == Ordering.eq) l.toListModel).toList ++ l') ∧ (updateCell k f l hlb).impl.toListModel.Perm ((f (List.findCell l.toListModel (compare k))).inner.toList ++ l') ∧ Internal.List.containsKey k l' = false
theorem
Std.DTreeMap.Internal.Impl.toListModel_updateAtKey_perm
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
{k : α}
{f : Cell α β (compare k) → Cell α β (compare k)}
{g : List ((a : α) × β a) → List ((a : α) × β a)}
(hfg : ∀ {c : Cell α β (compare k)}, (f c).inner.toList = g c.inner.toList)
(hg₁ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.List.containsKey k l' = false → g (l ++ l') = g l ++ l')
:
(updateCell k f l hlb).impl.toListModel.Perm (g l.toListModel)
This is the general theorem to show that modification operations are correct.
theorem
Std.DTreeMap.Internal.Impl.applyPartition_eq
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{l : Impl α β}
{f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ}
(hlo : l.Ordered)
:
applyPartition k l f = f (List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.gt) l.toListModel) (List.findCell l.toListModel k) ⋯
(List.filter (fun (x : (a : α) × β a) => k x.fst == Ordering.lt) l.toListModel)
theorem
Std.DTreeMap.Internal.Impl.containsKey_toListModel
{α : Type u}
{β : α → Type v}
[Ord α]
[OrientedOrd α]
{k : α}
{l : Impl α β}
(h : contains' (compare k) l = true)
:
theorem
Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
[TransOrd α]
{k : α}
{l : Impl α β}
(hlo : l.Ordered)
{f :
List ((a : α) × β a) →
(c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → List ((a : α) × β a) → δ}
(g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ)
(h :
∀ {ll rr : List ((a : α) × β a)} {c : Cell α β (compare k)} {h₁ : contains' (compare k) l = true → c.contains = true},
List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) →
(∀ (p : (a : α) × β a), p ∈ ll → compare k p.fst = Ordering.gt) →
(∀ (p : (a : α) × β a), p ∈ rr → compare k p.fst = Ordering.lt) →
f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr) ⋯)
:
theorem
Std.DTreeMap.Internal.Impl.applyPartition_eq_apply_toListModel'
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
[TransOrd α]
{k : α → Ordering}
[Internal.IsStrictCut compare k]
{l : Impl α β}
(hlo : l.Ordered)
{f : List ((a : α) × β a) → (c : Cell α β k) → (contains' k l = true → c.contains = true) → List ((a : α) × β a) → δ}
(g : List ((a : α) × β a) → δ)
(h :
∀ {ll rr : List ((a : α) × β a)} {c : Cell α β k} {h₁ : contains' k l = true → c.contains = true},
List.Pairwise (fun (a b : (a : α) × β a) => compare a.fst b.fst = Ordering.lt) (ll ++ c.inner.toList ++ rr) →
(∀ (p : (a : α) × β a), p ∈ ll → k p.fst = Ordering.gt) →
(∀ (p : (a : α) × β a), p ∈ rr → k p.fst = Ordering.lt) → f ll c h₁ rr = g (ll ++ c.inner.toList ++ rr))
:
theorem
Std.DTreeMap.Internal.Impl.applyCell_eq_apply_toListModel
{α : Type u}
{β : α → Type v}
{δ : Type w}
[Ord α]
[TransOrd α]
{k : α}
{l : Impl α β}
(hlo : l.Ordered)
{f : (c : Cell α β (compare k)) → (contains' (compare k) l = true → c.contains = true) → δ}
(g : (ll : List ((a : α) × β a)) → (contains' (compare k) l = true → Internal.List.containsKey k ll = true) → δ)
(hfg :
∀ (c : Cell α β (compare k)) (hc : contains' (compare k) l = true → c.contains = true), f c hc = g c.inner.toList ⋯)
(hg₁ :
∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k l₁ = true),
Internal.List.DistinctKeys l₁ → ∀ (hP : l₁.Perm l₂), g l₁ h = g l₂ ⋯)
(hg :
∀ (l₁ l₂ : List ((a : α) × β a)) (h : contains' (compare k) l = true → Internal.List.containsKey k (l₁ ++ l₂) = true)
(h' : Internal.List.containsKey k l₂ = false), g (l₁ ++ l₂) h = g l₁ ⋯)
:
Verification of access operations #
isEmpty #
theorem
Std.DTreeMap.Internal.Impl.isEmpty_eq_isEmpty
{α : Type u}
{β : α → Type v}
{t : Impl α β}
:
size #
theorem
Std.DTreeMap.Internal.Impl.size_eq_length
{α : Type u}
{β : α → Type v}
(t : Impl α β)
(htb : t.Balanced)
:
contains #
get? #
theorem
Std.DTreeMap.Internal.Impl.get?ₘ_eq_getValueCast?
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{t : Impl α β}
(hto : t.Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.get?_eq_getValueCast?
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{t : Impl α β}
(hto : t.Ordered)
:
get #
theorem
Std.DTreeMap.Internal.Impl.getₘ_eq_getValueCast
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{t : Impl α β}
(h : Internal.List.containsKey k t.toListModel = true)
{h' : (t.get?ₘ k).isSome = true}
(hto : t.Ordered)
:
get! #
theorem
Std.DTreeMap.Internal.Impl.get!ₘ_eq_getValueCast!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
[Inhabited (β k)]
{t : Impl α β}
(hto : t.Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.get!_eq_getValueCast!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
[Inhabited (β k)]
{t : Impl α β}
(hto : t.Ordered)
:
getD #
theorem
Std.DTreeMap.Internal.Impl.getDₘ_eq_getValueCastD
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{t : Impl α β}
{fallback : β k}
(hto : t.Ordered)
:
theorem
Std.DTreeMap.Internal.Impl.getD_eq_getValueCastD
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{t : Impl α β}
{fallback : β k}
(hto : t.Ordered)
:
getKey? #
getKey #
theorem
Std.DTreeMap.Internal.Impl.getKeyₘ_eq_getKey
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{t : Impl α β}
(h : Internal.List.containsKey k t.toListModel = true)
{h' : (t.getKey?ₘ k).isSome = true}
(hto : t.Ordered)
:
getKey! #
getKeyD #
get? #
get #
theorem
Std.DTreeMap.Internal.Impl.Const.getₘ_eq_getValue
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{k : α}
{t : Impl α fun (x : α) => β}
(h : Internal.List.containsKey k t.toListModel = true)
{h' : (get?ₘ t k).isSome = true}
(hto : t.Ordered)
:
get! #
getD #
Verification of modification operations #
empty #
@[simp]
insertₘ #
theorem
Std.DTreeMap.Internal.Impl.toListModel_insertₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(insertₘ k v l hlb).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)
insert #
theorem
Std.DTreeMap.Internal.Impl.toListModel_insert
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(insert k v l hlb).impl.toListModel.Perm (Internal.List.insertEntry k v l.toListModel)
theorem
Std.DTreeMap.Internal.Impl.WF.insert!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(h : l.WF)
:
(Impl.insert! k v l).WF
theorem
Std.DTreeMap.Internal.Impl.toListModel_insert!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(insert! k v l).toListModel.Perm (Internal.List.insertEntry k v l.toListModel)
eraseₘ #
theorem
Std.DTreeMap.Internal.Impl.toListModel_eraseₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(eraseₘ k t htb).toListModel.Perm (Internal.List.eraseKey k t.toListModel)
erase #
theorem
Std.DTreeMap.Internal.Impl.toListModel_erase
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(erase k t htb).impl.toListModel.Perm (Internal.List.eraseKey k t.toListModel)
theorem
Std.DTreeMap.Internal.Impl.WF.erase!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[TransOrd α]
{k : α}
{l : Impl α β}
(h : l.WF)
:
(Impl.erase! k l).WF
theorem
Std.DTreeMap.Internal.Impl.toListModel_erase!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(erase! k l).toListModel.Perm (Internal.List.eraseKey k l.toListModel)
containsThenInsert #
theorem
Std.DTreeMap.Internal.Impl.size_containsThenInsert_eq_size
{α : Type u}
{β : α → Type v}
[Ord α]
(t : Impl α β)
:
theorem
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(containsThenInsert k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)
containsThenInsert! #
theorem
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsert!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(containsThenInsert! k v t).snd.toListModel.Perm (Internal.List.insertEntry k v t.toListModel)
insertIfNew #
theorem
Std.DTreeMap.Internal.Impl.toListModel_insertIfNew
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(insertIfNew k v l hlb).impl.toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)
theorem
Std.DTreeMap.Internal.Impl.WF.insertIfNew!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(h : l.WF)
:
(Impl.insertIfNew! k v l).WF
theorem
Std.DTreeMap.Internal.Impl.toListModel_insertIfNew!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{l : Impl α β}
(hlb : l.Balanced)
(hlo : l.Ordered)
:
(insertIfNew! k v l).toListModel.Perm (Internal.List.insertEntryIfNew k v l.toListModel)
containsThenInsertIfNew #
theorem
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntryIfNew k v t.toListModel)
containsThenInsertIfNew! #
theorem
Std.DTreeMap.Internal.Impl.toListModel_containsThenInsertIfNew!
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
{k : α}
{v : β k}
{t : Impl α β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(containsThenInsertIfNew k v t htb).snd.impl.toListModel.Perm (Internal.List.insertEntryIfNew k v t.toListModel)
filterMap #
@[simp]
theorem
Std.DTreeMap.Internal.Impl.toListModel_filterMap
{α : Type u}
{β : α → Type v}
{γ : α → Type w}
[Ord α]
{t : Impl α β}
{h : t.Balanced}
{f : (a : α) → β a → Option (γ a)}
:
(filterMap f t h).impl.toListModel = List.filterMap (fun (x : (a : α) × β a) => Option.map (fun (x_1 : γ x.fst) => ⟨x.fst, x_1⟩) (f x.fst x.snd))
t.toListModel
filter #
alter #
theorem
Std.DTreeMap.Internal.Impl.toListModel_alterₘ
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{t : Impl α β}
{a : α}
{f : Option (β a) → Option (β a)}
(htb : t.Balanced)
(hto : t.Ordered)
:
(alterₘ a f t htb).toListModel.Perm (Internal.List.alterKey a f t.toListModel)
theorem
Std.DTreeMap.Internal.Impl.toListModel_alter
{α : Type u}
{β : α → Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{t : Impl α β}
{a : α}
{f : Option (β a) → Option (β a)}
(htb : t.Balanced)
(hto : t.Ordered)
:
(alter a f t htb).impl.toListModel.Perm (Internal.List.alterKey a f t.toListModel)
alter! #
modify #
theorem
Std.DTreeMap.Internal.Impl.modify_eq_alter
{α : Type u}
{β : α → Type v}
[Ord α]
[LawfulEqOrd α]
{t : Impl α β}
{a : α}
{f : β a → β a}
(htb : t.Balanced)
:
mergeWith #
foldlM #
theorem
Std.DTreeMap.Internal.Impl.foldlM_eq_foldlM
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{m : Type u_1 → Type u_2}
{δ : Type u_1}
[Monad m]
[LawfulMonad m]
{f : δ → (a : α) → β a → m δ}
{init : δ}
:
foldlM f init t = List.foldlM (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel
foldl #
theorem
Std.DTreeMap.Internal.Impl.foldl_eq_foldl
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type u_1}
{f : δ → (a : α) → β a → δ}
{init : δ}
:
foldl f init t = List.foldl (fun (acc : δ) (p : (a : α) × β a) => f acc p.fst p.snd) init t.toListModel
foldrM #
theorem
Std.DTreeMap.Internal.Impl.foldrM_eq_foldrM
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{m : Type u_1 → Type u_2}
{δ : Type u_1}
[Monad m]
[LawfulMonad m]
{f : (a : α) → β a → δ → m δ}
{init : δ}
:
foldrM f init t = List.foldrM (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel
foldr #
theorem
Std.DTreeMap.Internal.Impl.foldr_eq_foldr
{α : Type u}
{β : α → Type v}
{t : Impl α β}
{δ : Type u_1}
{f : (a : α) → β a → δ → δ}
{init : δ}
:
foldr f init t = List.foldr (fun (p : (a : α) × β a) (acc : δ) => f p.fst p.snd acc) init t.toListModel
toList #
theorem
Std.DTreeMap.Internal.Impl.toList_eq_toListModel
{α : Type u}
{β : α → Type v}
{t : Impl α β}
:
keys #
getThenInsertIfNew?! #
theorem
Std.DTreeMap.Internal.Impl.Const.WF.getThenInsertIfNew?!
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{v : β}
{t : Impl α fun (x : α) => β}
(h : t.WF)
:
(Const.getThenInsertIfNew?! t k v).snd.WF
alter #
theorem
Std.DTreeMap.Internal.Impl.Const.toListModel_alterₘ
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : Impl α fun (x : α) => β}
{a : α}
{f : Option β → Option β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(alterₘ a f t htb).toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)
theorem
Std.DTreeMap.Internal.Impl.Const.toListModel_alter
{α : Type u}
{β : Type v}
[Ord α]
[TransOrd α]
{t : Impl α fun (x : α) => β}
{a : α}
{f : Option β → Option β}
(htb : t.Balanced)
(hto : t.Ordered)
:
(alter a f t htb).impl.toListModel.Perm (Internal.List.Const.alterKey a f t.toListModel)
alter! #
modify #
mergeWith #
toList #
Deducing that well-formed trees are ordered #
Deducing that additional operations are well-formed #
Internal implementation detail of the tree map
- leaf
{α : Type u}
{β : α → Type v}
{β' : α → Type u_1}
: Impl.leaf.SameKeys Impl.leaf
Internal implementation detail of the tree map
- inner
{α : Type u}
{β : α → Type v}
{β' : α → Type u_1}
(sz : Nat)
(k : α)
(v : β k)
(v' : β' k)
(r : Impl α β)
(r' : Impl α β')
(l : Impl α β)
(l' : Impl α β')
: r.SameKeys r' → l.SameKeys l' → (Impl.inner sz k v l r).SameKeys (Impl.inner sz k v' l' r')
Internal implementation detail of the tree map
Instances For
theorem
Std.DTreeMap.Internal.Impl.SameKeys.ordered_iff_pairwise_keys
{α : Type u}
{β : α → Type v}
[Ord α]
{t : Impl α β}
:
t.Ordered ↔ List.Pairwise (fun (x1 x2 : α) => compare x1 x2 = Ordering.lt)
(List.map (fun (x : (a : α) × β a) => x.fst) t.toListModel)
getThenInsertIfNew?! #
theorem
Std.DTreeMap.Internal.Impl.WF.getThenInsertIfNew?!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[TransOrd α]
[LawfulEqOrd α]
{k : α}
{v : β k}
{t : Impl α β}
(h : t.WF)
:
(t.getThenInsertIfNew?! k v).snd.WF
alter! #
theorem
Std.DTreeMap.Internal.Impl.WF.alter!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[LawfulEqOrd α]
{t : Impl α β}
{a : α}
{f : Option (β a) → Option (β a)}
(h : t.WF)
:
(Impl.alter! a f t).WF
mergeWith! #
theorem
Std.DTreeMap.Internal.Impl.mergeWith_eq_mergeWith!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[LawfulEqOrd α]
{mergeFn : (a : α) → β a → β a → β a}
{t₁ t₂ : Impl α β}
(h : t₁.Balanced)
:
theorem
Std.DTreeMap.Internal.Impl.WF.mergeWith!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
[LawfulEqOrd α]
{mergeFn : (a : α) → β a → β a → β a}
{t₁ t₂ : Impl α β}
(h : t₁.WF)
:
(Impl.mergeWith! mergeFn t₁ t₂).WF
theorem
Std.DTreeMap.Internal.Impl.WF.constMergeWith!
{α : Type u}
{β : Type v}
{x✝ : Ord α}
{mergeFn : α → β → β → β}
{t₁ t₂ : Impl α fun (x : α) => β}
(h : t₁.WF)
:
(Const.mergeWith! mergeFn t₁ t₂).WF
filterMap #
filterMap! #
filter! #
theorem
Std.DTreeMap.Internal.Impl.WF.filter!
{α : Type u}
{β : α → Type v}
{x✝ : Ord α}
{t : Impl α β}
{f : (a : α) → β a → Bool}
(h : t.WF)
:
(Impl.filter! f t).WF