Documentation

Std.Data.DHashMap.Internal.WF

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) = []
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 #

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) :
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.valStd.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) :
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)

Access operations #

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} :
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} :
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} :
theorem Std.DHashMap.Internal.Raw₀.getKeyₘ_eq_getKey {α : Type u} {β : αType v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
theorem Std.DHashMap.Internal.Raw₀.getKey_eq_getKey {α : Type u} {β : αType v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {h : m.contains a = true} :
theorem Std.DHashMap.Internal.Raw₀.getKeyDₘ_eq_getKeyD {α : Type u} {β : αType v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {fallback : α} :
m.getKeyDₘ a fallback = Std.DHashMap.Internal.List.getKeyD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback
theorem Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyD {α : Type u} {β : αType v} [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {fallback : α} :
m.getKeyD a fallback = Std.DHashMap.Internal.List.getKeyD a (Std.DHashMap.Internal.toListModel m.val.buckets) fallback

replaceₘ #

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) :
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₀.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} :

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₀.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₀.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? #

eraseₘ #

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

erase #

filterMapₘ #

theorem Std.DHashMap.Internal.Raw₀.toListModel_filterMapₘ {α : Type u} {β : αType v} {δ : αType w} {m : Std.DHashMap.Internal.Raw₀ α β} {f : (a : α) → β aOption (δ 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 : α) → β aOption (δ 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 : α) → β aOption (δ 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 : α) → β aOption (δ 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))

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) :

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 : α) → β aBool} :
(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 : α) → β aBool} (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 : α) → β aBool} (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 : α) → β aBool} :
(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.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