Documentation

Std.Data.DHashMap.Internal.Model

This is an internal implementation file of the hash map. Users of the hash map should not rely on the contents of this file.

In this file we define functions for manipulating a hash map based on operations defined in terms of their buckets. Then we give "model implementations" of the hash map operations in terms of these basic building blocks and show that the actual operations are equal to the model implementations T his means that later we will be able to prove properties of the operations by proving general facts about the basic building blocks.

Setting up the infrastructure #

def Std.DHashMap.Internal.bucket {α : Type u} {β : αType v} [Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β)) (h : 0 < self.size) (k : α) :

Internal implementation detail of the hash map

Equations

Internal implementation detail of the hash map

Equations

Internal implementation detail of the hash map

Equations

Internal implementation detail of the hash map

Equations
@[simp]
theorem Std.DHashMap.Internal.size_updateBucket {α : Type u} {β : αType v} [Hashable α] {self : Array (Std.DHashMap.Internal.AssocList α β)} {h : 0 < self.size} {k : α} {f : Std.DHashMap.Internal.AssocList α βStd.DHashMap.Internal.AssocList α β} :
(Std.DHashMap.Internal.updateBucket self h k f).size = self.size
@[simp]
theorem Std.DHashMap.Internal.exists_bucket_of_uset {α : Type u} {β : αType v} [BEq α] [Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β)) (i : USize) (hi : i.toNat < self.size) (d : Std.DHashMap.Internal.AssocList α β) :
∃ (l : List ((a : α) × β a)), (Std.DHashMap.Internal.toListModel self).Perm (self[i.toNat].toList ++ l) (Std.DHashMap.Internal.toListModel (self.uset i d hi)).Perm (d.toList ++ l) ∀ [inst : LawfulHashable α], Std.DHashMap.Internal.IsHashSelf self∀ (k : α), (Std.DHashMap.Internal.mkIdx self.size (hash k)).val.toNat = i.toNatStd.DHashMap.Internal.List.containsKey k l = false
theorem Std.DHashMap.Internal.exists_bucket' {α : Type u} {β : αType v} [BEq α] [Hashable α] (self : Array (Std.DHashMap.Internal.AssocList α β)) (i : USize) (hi : i.toNat < self.size) :
∃ (l : List ((a : α) × β a)), (self.toList.bind Std.DHashMap.Internal.AssocList.toList).Perm (self[i.toNat].toList ++ l) ∀ [inst : LawfulHashable α], Std.DHashMap.Internal.IsHashSelf self∀ (k : α), (Std.DHashMap.Internal.mkIdx self.size (hash k)).val.toNat = i.toNatStd.DHashMap.Internal.List.containsKey k l = false
theorem Std.DHashMap.Internal.exists_bucket {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Array (Std.DHashMap.Internal.AssocList α β)) (h : 0 < m.size) (k : α) :
∃ (l : List ((a : α) × β a)), (Std.DHashMap.Internal.toListModel m).Perm ((Std.DHashMap.Internal.bucket m h k).toList ++ l) ∀ [inst : LawfulHashable α], Std.DHashMap.Internal.IsHashSelf m∀ (k' : α), hash k = hash k'Std.DHashMap.Internal.List.containsKey k' l = false
theorem Std.DHashMap.Internal.apply_bucket {α : Type u} {β : αType v} {γ : Type w} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {f : Std.DHashMap.Internal.AssocList α βγ} {g : List ((a : α) × β a)γ} (hfg : ∀ {l : Std.DHashMap.Internal.AssocList α β}, f l = g l.toList) (hg₁ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.DistinctKeys ll.Perm l'g l = g l') (hg₂ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.containsKey a l' = falseg (l ++ l') = g l) :
f (Std.DHashMap.Internal.bucket m.val.buckets a) = g (Std.DHashMap.Internal.toListModel m.val.buckets)

This is the general theorem used to show that access operations are correct.

theorem Std.DHashMap.Internal.apply_bucket_with_proof {α : Type u} {β : αType v} {γ : αType w} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) (a : α) (f : (a : α) → (l : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a l = trueγ a) (g : (a : α) → (l : List ((a : α) × β a)) → Std.DHashMap.Internal.List.containsKey a l = trueγ a) (hfg : ∀ {a : α} {l : Std.DHashMap.Internal.AssocList α β} {h : Std.DHashMap.Internal.AssocList.contains a l = true}, f a l h = g a l.toList ) (hg₁ : ∀ {l l' : List ((a : α) × β a)} {a : α} {h : Std.DHashMap.Internal.List.containsKey a l = true}, Std.DHashMap.Internal.List.DistinctKeys l∀ (hl' : l.Perm l'), g a l h = g a l' ) {h : Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.bucket m.val.buckets a) = true} {h' : Std.DHashMap.Internal.List.containsKey a (Std.DHashMap.Internal.toListModel m.val.buckets) = true} (hg₂ : ∀ {l l' : List ((a : α) × β a)} {a : α} {h : Std.DHashMap.Internal.List.containsKey a (l ++ l') = true} (hl' : Std.DHashMap.Internal.List.containsKey a l' = false), g a (l ++ l') h = g a l ) :
f a (Std.DHashMap.Internal.bucket m.val.buckets a) h = g a (Std.DHashMap.Internal.toListModel m.val.buckets) h'

This is the general theorem used to show that access operations involving a proof (like get) are correct.

theorem Std.DHashMap.Internal.toListModel_updateBucket {α : Type u} {β : αType v} [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp m.val) {a : α} {f : Std.DHashMap.Internal.AssocList α βStd.DHashMap.Internal.AssocList α β} {g : List ((a : α) × β a)List ((a : α) × β a)} (hfg : ∀ {l : Std.DHashMap.Internal.AssocList α β}, (f l).toList = g l.toList) (hg₁ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.DistinctKeys ll.Perm l'(g l).Perm (g l')) (hg₂ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.containsKey a l' = falseg (l ++ l') = g l ++ l') :

This is the general theorem to show that modification operations are correct.

theorem Std.DHashMap.Internal.toListModel_updateAllBuckets {α : Type u} {β : αType v} {δ : αType w} {m : Std.DHashMap.Internal.Raw₀ α β} {f : Std.DHashMap.Internal.AssocList α βStd.DHashMap.Internal.AssocList α δ} {g : List ((a : α) × β a)List ((a : α) × δ a)} (hfg : ∀ {l : Std.DHashMap.Internal.AssocList α β}, (f l).toList.Perm (g l.toList)) (hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l')) :

This is the general theorem to show that mapping operations (like map and filter) are correct.

IsHashSelf #

@[simp]
theorem Std.DHashMap.Internal.IsHashSelf.mkArray {α : Type u} {β : αType v} [BEq α] [Hashable α] {c : Nat} :
Std.DHashMap.Internal.IsHashSelf (mkArray c Std.DHashMap.Internal.AssocList.nil)
theorem Std.DHashMap.Internal.IsHashSelf.uset {α : Type u} {β : αType v} [BEq α] [Hashable α] {m : Array (Std.DHashMap.Internal.AssocList α β)} {i : USize} {h : i.toNat < m.size} {d : Std.DHashMap.Internal.AssocList α β} (hd : Std.DHashMap.Internal.List.HashesTo m[i].toList i.toNat m.sizeStd.DHashMap.Internal.List.HashesTo d.toList i.toNat m.size) (hm : Std.DHashMap.Internal.IsHashSelf m) :

This is the general theorem to show that modification operations preserve well-formedness of buckets.

Definition of model functions #

def Std.DHashMap.Internal.Raw₀.replaceₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DHashMap.Internal.Raw₀.consₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DHashMap.Internal.Raw₀.get?ₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
Option (β a)

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.getKey?ₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.containsₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.getₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (h : m.containsₘ a = true) :
β a

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.getDₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) :
β a

Internal implementation detail of the hash map

Equations
  • m.getDₘ a fallback = (m.get?ₘ a).getD fallback
def Std.DHashMap.Internal.Raw₀.get!ₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) [Inhabited (β a)] :
β a

Internal implementation detail of the hash map

Equations
  • m.get!ₘ a = (m.get?ₘ a).get!
def Std.DHashMap.Internal.Raw₀.getKeyₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (h : m.containsₘ a = true) :
α

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.getKeyDₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : α) :
α

Internal implementation detail of the hash map

Equations
  • m.getKeyDₘ a fallback = (m.getKey?ₘ a).getD fallback
def Std.DHashMap.Internal.Raw₀.getKey!ₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] [Inhabited α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
α

Internal implementation detail of the hash map

Equations
  • m.getKey!ₘ a = (m.getKey?ₘ a).get!
def Std.DHashMap.Internal.Raw₀.insertₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :

Internal implementation detail of the hash map

Equations
  • m.insertₘ a b = if m.containsₘ a = true then m.replaceₘ a b else (m.consₘ a b).expandIfNecessary
def Std.DHashMap.Internal.Raw₀.insertIfNewₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :

Internal implementation detail of the hash map

Equations
  • m.insertIfNewₘ a b = if m.containsₘ a = true then m else (m.consₘ a b).expandIfNecessary

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.

Internal implementation detail of the hash map

Equations
  • m.eraseₘ a = if m.containsₘ a = true then m.eraseₘaux a else m
def Std.DHashMap.Internal.Raw₀.filterMapₘ {α : Type u} {β : αType v} {δ : αType w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aOption (δ a)) :

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DHashMap.Internal.Raw₀.mapₘ {α : Type u} {β : αType v} {δ : αType w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aδ a) :

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.filterₘ {α : Type u} {β : αType v} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aBool) :

Internal implementation detail of the hash map

Equations
  • One or more equations did not get rendered due to their size.
def Std.DHashMap.Internal.Raw₀.Const.get?ₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) :

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.Const.getₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) (h : m.containsₘ a = true) :
β

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.Const.getDₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) (fallback : β) :
β

Internal implementation detail of the hash map

Equations
def Std.DHashMap.Internal.Raw₀.Const.get!ₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] [Inhabited β] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) :
β

Internal implementation detail of the hash map

Equations

Equivalence between model functions and real implementations #

theorem Std.DHashMap.Internal.Raw₀.reinsertAux_eq {α : Type u} {β : αType v} [Hashable α] (data : { d : Array (Std.DHashMap.Internal.AssocList α β) // 0 < d.size }) (a : α) (b : β a) :
theorem Std.DHashMap.Internal.Raw₀.get?_eq_get?ₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
m.get? a = m.get?ₘ a
theorem Std.DHashMap.Internal.Raw₀.get_eq_getₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (h : m.contains a = true) :
m.get a h = m.getₘ a h
theorem Std.DHashMap.Internal.Raw₀.getD_eq_getDₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : β a) :
m.getD a fallback = m.getDₘ a fallback
theorem Std.DHashMap.Internal.Raw₀.get!_eq_get!ₘ {α : Type u} {β : αType v} [BEq α] [LawfulBEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) [Inhabited (β a)] :
m.get! a = m.get!ₘ a
theorem Std.DHashMap.Internal.Raw₀.getKey?_eq_getKey?ₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
m.getKey? a = m.getKey?ₘ a
theorem Std.DHashMap.Internal.Raw₀.getKey_eq_getKeyₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (h : m.contains a = true) :
m.getKey a h = m.getKeyₘ a h
theorem Std.DHashMap.Internal.Raw₀.getKeyD_eq_getKeyDₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (fallback : α) :
m.getKeyD a fallback = m.getKeyDₘ a fallback
theorem Std.DHashMap.Internal.Raw₀.getKey!_eq_getKey!ₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] [Inhabited α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
m.getKey! a = m.getKey!ₘ a
theorem Std.DHashMap.Internal.Raw₀.contains_eq_containsₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
m.contains a = m.containsₘ a
theorem Std.DHashMap.Internal.Raw₀.insert_eq_insertₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
m.insert a b = m.insertₘ a b
theorem Std.DHashMap.Internal.Raw₀.containsThenInsert_eq_insertₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.containsThenInsert a b).snd = m.insertₘ a b
theorem Std.DHashMap.Internal.Raw₀.containsThenInsert_eq_containsₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.containsThenInsert a b).fst = m.containsₘ a
theorem Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_eq_insertIfNewₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.containsThenInsertIfNew a b).snd = m.insertIfNewₘ a b
theorem Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_eq_containsₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.containsThenInsertIfNew a b).fst = m.containsₘ a
theorem Std.DHashMap.Internal.Raw₀.insertIfNew_eq_insertIfNewₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
m.insertIfNew a b = m.insertIfNewₘ a b
theorem Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_eq_insertIfNewₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.getThenInsertIfNew? a b).snd = m.insertIfNewₘ a b
theorem Std.DHashMap.Internal.Raw₀.getThenInsertIfNew?_eq_get?ₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] [LawfulBEq α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) (b : β a) :
(m.getThenInsertIfNew? a b).fst = m.get?ₘ a
theorem Std.DHashMap.Internal.Raw₀.erase_eq_eraseₘ {α : Type u} {β : αType v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α) :
m.erase a = m.eraseₘ a
theorem Std.DHashMap.Internal.Raw₀.filterMap_eq_filterMapₘ {α : Type u} {β : αType v} {δ : αType w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aOption (δ a)) :
theorem Std.DHashMap.Internal.Raw₀.map_eq_mapₘ {α : Type u} {β : αType v} {δ : αType w} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aδ a) :
theorem Std.DHashMap.Internal.Raw₀.filter_eq_filterₘ {α : Type u} {β : αType v} (m : Std.DHashMap.Internal.Raw₀ α β) (f : (a : α) → β aBool) :
theorem Std.DHashMap.Internal.Raw₀.Const.getD_eq_getDₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) (fallback : β) :
theorem Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_eq_insertIfNewₘ {α : Type u} {β : Type v} [BEq α] [Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β) (a : α) (b : β) :