This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.
File contents: proof that all hash map operations preserve WFImp to show WF.out : WF → WFImp
@[simp]
theorem
Std.DHashMap.Internal.toListModel_mkArray_nil
{α : Type u}
{β : α → Type v}
{c : Nat}
:
Std.DHashMap.Internal.toListModel (mkArray c Std.DHashMap.Internal.AssocList.nil) = []
@[simp]
theorem
Std.DHashMap.Internal.computeSize_eq
{α : Type u}
{β : α → Type v}
{buckets : Array (Std.DHashMap.Internal.AssocList α β)}
:
Std.DHashMap.Internal.computeSize buckets = (Std.DHashMap.Internal.toListModel buckets).length
theorem
Std.DHashMap.Internal.Raw.size_eq_length
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : Std.DHashMap.Internal.Raw.WFImp m)
:
m.size = (Std.DHashMap.Internal.toListModel m.buckets).length
theorem
Std.DHashMap.Internal.Raw.isEmpty_eq_isEmpty
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Std.DHashMap.Raw α β}
(h : Std.DHashMap.Internal.Raw.WFImp m)
:
m.isEmpty = (Std.DHashMap.Internal.toListModel m.buckets).isEmpty
Raw₀.empty #
@[simp]
theorem
Std.DHashMap.Internal.Raw₀.toListModel_buckets_empty
{α : Type u}
{β : α → Type v}
{c : Nat}
:
Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.empty c).val.buckets = []
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_reinsertAux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(data : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size })
(a : α)
(b : β a)
(h : Std.DHashMap.Internal.IsHashSelf data.val)
:
Std.DHashMap.Internal.IsHashSelf (Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b).val
expandIfNecessary #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_reinsertAux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
(data : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size })
(a : α)
(b : β a)
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b).val).Perm
(⟨a, b⟩ :: Std.DHashMap.Internal.toListModel data.val)
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_foldl_reinsertAux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(l : List ((a : α) × β a))
(target : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size })
:
Std.DHashMap.Internal.IsHashSelf target.val →
Std.DHashMap.Internal.IsHashSelf
(List.foldl
(fun (acc : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }) (p : (a : α) × β a) =>
Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd)
target l).val
theorem
Std.DHashMap.Internal.Raw₀.toListModel_foldl_reinsertAux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
(l : List ((a : α) × β a))
(target : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size })
:
(Std.DHashMap.Internal.toListModel
(List.foldl
(fun (acc : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }) (p : (a : α) × β a) =>
Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd)
target l).val).Perm
(l ++ Std.DHashMap.Internal.toListModel target.val)
theorem
Std.DHashMap.Internal.Raw₀.expand.go_pos
{α : Type u}
{β : α → Type v}
[Hashable α]
{i : Nat}
{source : Array (Std.DHashMap.Internal.AssocList α β)}
{target : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }}
(h : i < source.size)
:
Std.DHashMap.Internal.Raw₀.expand.go i source target = Std.DHashMap.Internal.Raw₀.expand.go (i + 1) (source.set ⟨i, h⟩ Std.DHashMap.Internal.AssocList.nil)
(Std.DHashMap.Internal.AssocList.foldl (Std.DHashMap.Internal.Raw₀.reinsertAux hash) target (source.get ⟨i, h⟩))
theorem
Std.DHashMap.Internal.Raw₀.expand.go_neg
{α : Type u}
{β : α → Type v}
[Hashable α]
{i : Nat}
{source : Array (Std.DHashMap.Internal.AssocList α β)}
{target : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }}
(h : ¬i < source.size)
:
Std.DHashMap.Internal.Raw₀.expand.go i source target = target
theorem
Std.DHashMap.Internal.Raw₀.expand.go_eq
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
(source : Array (Std.DHashMap.Internal.AssocList α β))
(target : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size })
:
Std.DHashMap.Internal.Raw₀.expand.go 0 source target = List.foldl
(fun (acc : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }) (p : (a : α) × β a) =>
Std.DHashMap.Internal.Raw₀.reinsertAux hash acc p.fst p.snd)
target (Std.DHashMap.Internal.toListModel source)
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_expand
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulHashable α]
[EquivBEq α]
{buckets : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }}
:
theorem
Std.DHashMap.Internal.Raw₀.toListModel_expand
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
{buckets : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }}
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.expand buckets).val).Perm
(Std.DHashMap.Internal.toListModel buckets.val)
theorem
Std.DHashMap.Internal.Raw₀.toListModel_expandIfNecessary
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
(m : Std.DHashMap.Internal.Raw₀ α β)
:
(Std.DHashMap.Internal.toListModel m.expandIfNecessary.val.buckets).Perm
(Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.wfImp_expandIfNecessary
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp m.expandIfNecessary.val
Access operations #
theorem
Std.DHashMap.Internal.Raw₀.containsₘ_eq_containsKey
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
m.containsₘ a = Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.contains_eq_containsKey
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
m.contains a = Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.get?ₘ_eq_getValueCast?
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
m.get?ₘ a = Std.DHashMap.Internal.List.getValueCast? a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.get?_eq_getValueCast?
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
m.get? a = Std.DHashMap.Internal.List.getValueCast? a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.getₘ_eq_getValue
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{h : m.containsₘ a = true}
:
m.getₘ a h = Std.DHashMap.Internal.List.getValueCast a (Std.DHashMap.Internal.toListModel m.val.buckets) ⋯
theorem
Std.DHashMap.Internal.Raw₀.get_eq_getValueCast
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{h : m.contains a = true}
:
m.get a h = Std.DHashMap.Internal.List.getValueCast a (Std.DHashMap.Internal.toListModel m.val.buckets) ⋯
theorem
Std.DHashMap.Internal.Raw₀.get!ₘ_eq_getValueCast!
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
[Inhabited (β a)]
:
m.get!ₘ a = Std.DHashMap.Internal.List.getValueCast! a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.get!_eq_getValueCast!
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
[Inhabited (β a)]
:
m.get! a = Std.DHashMap.Internal.List.getValueCast! a (Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.getDₘ_eq_getValueCastD
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{fallback : β a}
:
m.getDₘ a fallback = Std.DHashMap.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback
theorem
Std.DHashMap.Internal.Raw₀.getD_eq_getValueCastD
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{fallback : β a}
:
m.getD a fallback = Std.DHashMap.Internal.List.getValueCastD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback
theorem
Std.DHashMap.Internal.Raw₀.Const.get?ₘ_eq_getValue?
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get?_eq_getValue?
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getₘ_eq_getValue
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{h : m.containsₘ a = true}
:
Std.DHashMap.Internal.Raw₀.Const.getₘ m a h = Std.DHashMap.Internal.List.getValue a (Std.DHashMap.Internal.toListModel m.val.buckets) ⋯
theorem
Std.DHashMap.Internal.Raw₀.Const.get_eq_getValue
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{h : m.contains a = true}
:
Std.DHashMap.Internal.Raw₀.Const.get m a h = Std.DHashMap.Internal.List.getValue a (Std.DHashMap.Internal.toListModel m.val.buckets) ⋯
theorem
Std.DHashMap.Internal.Raw₀.Const.get!ₘ_eq_getValue!
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
[Inhabited β]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get!_eq_getValue!
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
[Inhabited β]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getDₘ_eq_getValueD
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{fallback : β}
:
Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = Std.DHashMap.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback
theorem
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getValueD
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
(hm : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{fallback : β}
:
Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.List.getValueD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback
replaceₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_replaceₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
:
(Std.DHashMap.Internal.toListModel (m.replaceₘ a b).val.buckets).Perm
(Std.DHashMap.Internal.List.replaceEntry a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_replaceₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
:
Std.DHashMap.Internal.IsHashSelf (m.replaceₘ a b).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_replaceₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
:
Std.DHashMap.Internal.Raw.WFImp (m.replaceₘ a b).val
insertₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_consₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
:
(Std.DHashMap.Internal.toListModel (m.consₘ a b).val.buckets).Perm
(⟨a, b⟩ :: Std.DHashMap.Internal.toListModel m.val.buckets)
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_consₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
:
Std.DHashMap.Internal.IsHashSelf (m.consₘ a b).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_consₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(a : α)
(b : β a)
(hc : m.containsₘ a = false)
:
Std.DHashMap.Internal.Raw.WFImp (m.consₘ a b).val
theorem
Std.DHashMap.Internal.Raw₀.toListModel_insertₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.insertₘ a b).val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_insertₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.insertₘ a b).val
insert #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_insert
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.insert a b).val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_insert
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.insert a b).val
containsThenInsert #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsert
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.containsThenInsert a b).snd.val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntry a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsert
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.containsThenInsert a b).snd.val
insertIfNewₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_insertIfNewₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.insertIfNewₘ a b).val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_insertIfNewₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.insertIfNewₘ a b).val
insertIfNew #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_insertIfNew
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.insertIfNew a b).val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_insertIfNew
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.insertIfNew a b).val
containsThenInsertIfNew #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_containsThenInsertIfNew
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
(Std.DHashMap.Internal.toListModel (m.containsThenInsertIfNew a b).snd.val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_containsThenInsertIfNew
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
{a : α}
{b : β a}
:
Std.DHashMap.Internal.Raw.WFImp (m.containsThenInsertIfNew a b).snd.val
getThenInsertIfNew? #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_getThenInsertIfNew?
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
(Std.DHashMap.Internal.toListModel (m.getThenInsertIfNew? a b).snd.val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_getThenInsertIfNew?
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
{b : β a}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.getThenInsertIfNew? a b).snd.val
Const.getThenInsertIfNew? #
theorem
Std.DHashMap.Internal.Raw₀.Const.toListModel_getThenInsertIfNew?
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).snd.val.buckets).Perm
(Std.DHashMap.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.Const.wfImp_getThenInsertIfNew?
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{a : α}
{b : β}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
eraseₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_eraseₘaux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
(Std.DHashMap.Internal.toListModel (m.eraseₘaux a).val.buckets).Perm
(Std.DHashMap.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_eraseₘaux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.IsHashSelf (m.eraseₘaux a).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_eraseₘaux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(h' : m.containsₘ a = true)
:
Std.DHashMap.Internal.Raw.WFImp (m.eraseₘaux a).val
theorem
Std.DHashMap.Internal.Raw₀.toListModel_perm_eraseKey_of_containsₘ_eq_false
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
(h' : m.containsₘ a = false)
:
(Std.DHashMap.Internal.toListModel m.val.buckets).Perm
(Std.DHashMap.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.toListModel_eraseₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
(Std.DHashMap.Internal.toListModel (m.eraseₘ a).val.buckets).Perm
(Std.DHashMap.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_eraseₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.eraseₘ a).val
erase #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_erase
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
(Std.DHashMap.Internal.toListModel (m.erase a).val.buckets).Perm
(Std.DHashMap.Internal.List.eraseKey a (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_erase
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{a : α}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.erase a).val
filterMapₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_filterMapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
:
(Std.DHashMap.Internal.toListModel (m.filterMapₘ f).val.buckets).Perm
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd))
(Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_filterMapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[ReflBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.IsHashSelf (m.filterMapₘ f).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_filterMapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.filterMapₘ f).val
filterMap #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_filterMap
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.filterMap f m).val.buckets).Perm
(List.filterMap (fun (p : (a : α) × β a) => Option.map (fun (x : δ p.fst) => ⟨p.fst, x⟩) (f p.fst p.snd))
(Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_filterMap
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Option (δ a)}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
mapₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
:
(Std.DHashMap.Internal.toListModel (m.mapₘ f).val.buckets).Perm
(List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[ReflBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.IsHashSelf (m.mapₘ f).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.mapₘ f).val
map #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_map
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.map f m).val.buckets).Perm
(List.map (fun (p : (a : α) × β a) => ⟨p.fst, f p.fst p.snd⟩) (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_map
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → δ a}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
filterₘ #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_filterₘ
{α : Type u}
{β : α → Type v}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
:
(Std.DHashMap.Internal.toListModel (m.filterₘ f).val.buckets).Perm
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.isHashSelf_filterₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[ReflBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.IsHashSelf (m.filterₘ f).val.buckets
theorem
Std.DHashMap.Internal.Raw₀.wfImp_filterₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.filterₘ f).val
filter #
theorem
Std.DHashMap.Internal.Raw₀.toListModel_filter
{α : Type u}
{β : α → Type v}
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.Raw₀.filter f m).val.buckets).Perm
(List.filter (fun (p : (a : α) × β a) => f p.fst p.snd) (Std.DHashMap.Internal.toListModel m.val.buckets))
theorem
Std.DHashMap.Internal.Raw₀.wfImp_filter
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{m : Std.DHashMap.Internal.Raw₀ α β}
{f : (a : α) → β a → Bool}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
theorem
Std.DHashMap.Internal.Raw.WF.out
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[i₁ : EquivBEq α]
[i₂ : LawfulHashable α]
{m : Std.DHashMap.Raw α β}
(h : m.WF)
:
theorem
Std.DHashMap.Internal.Raw₀.wfImp_insertMany
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{ρ : Type w}
[ForIn Id ρ ((a : α) × β a)]
{m : Std.DHashMap.Internal.Raw₀ α β}
{l : ρ}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
Std.DHashMap.Internal.Raw.WFImp (m.insertMany l).val.val
theorem
Std.DHashMap.Internal.Raw₀.Const.wfImp_insertMany
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{ρ : Type w}
[ForIn Id ρ (α × β)]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β}
{l : ρ}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.wfImp_insertManyUnit
{α : Type u}
[BEq α]
[Hashable α]
[EquivBEq α]
[LawfulHashable α]
{ρ : Type w}
[ForIn Id ρ α]
{m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => Unit}
{l : ρ}
(h : Std.DHashMap.Internal.Raw.WFImp m.val)
: