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 #
@[simp]
@[simp]
theorem
Std.DHashMap.Internal.size_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (AssocList α β)}
:
@[simp]
theorem
Std.DHashMap.Internal.buckets_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (AssocList α β)}
:
theorem
Std.DHashMap.Internal.apply_bucket
{α : Type u}
{β : α → Type v}
{γ : Type w}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Raw₀ α β}
(hm : Raw.WFImp m.val)
{a : α}
{f : AssocList α β → γ}
{g : List ((a : α) × β a) → γ}
(hfg : ∀ {l : AssocList α β}, f l = g l.toList)
(hg₁ : ∀ {l l' : List ((a : α) × β a)}, List.DistinctKeys l → l.Perm l' → g l = g l')
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, List.containsKey a l' = false → g (l ++ l') = g l)
:
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 : Raw₀ α β}
(hm : Raw.WFImp m.val)
(a : α)
(f : (a : α) → (l : AssocList α β) → AssocList.contains a l = true → γ a)
(g : (a : α) → (l : List ((a : α) × β a)) → List.containsKey a l = true → γ a)
(hfg : ∀ {a : α} {l : AssocList α β} {h : AssocList.contains a l = true}, f a l h = g a l.toList ⋯)
(hg₁ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : List.containsKey a l = true},
List.DistinctKeys l → ∀ (hl' : l.Perm l'), g a l h = g a l' ⋯)
{h : AssocList.contains a (bucket m.val.buckets ⋯ a) = true}
{h' : List.containsKey a (toListModel m.val.buckets) = true}
(hg₂ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : List.containsKey a (l ++ l') = true}
(hl' : List.containsKey a l' = false), g a (l ++ l') h = g a l ⋯)
:
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 : Raw₀ α β}
(hm : Raw.WFImp m.val)
{a : α}
{f : AssocList α β → AssocList α β}
{g : List ((a : α) × β a) → List ((a : α) × β a)}
(hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList))
(hg₁ : ∀ {l l' : List ((a : α) × β a)}, List.DistinctKeys l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, List.containsKey a l' = false → g (l ++ l') = g l ++ l')
:
(toListModel (updateBucket m.val.buckets ⋯ a f)).Perm (g (toListModel m.val.buckets))
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 : Raw₀ α β}
{f : AssocList α β → AssocList α δ}
{g : List ((a : α) × β a) → List ((a : α) × δ a)}
(hfg : ∀ {l : AssocList α β}, (f l).toList.Perm (g l.toList))
(hg : ∀ {l l' : List ((a : α) × β a)}, (g (l ++ l')).Perm (g l ++ g l'))
:
(toListModel (updateAllBuckets m.val.buckets f)).Perm (g (toListModel m.val.buckets))
This is the general theorem to show that mapping operations (like map and filter) are
correct.
IsHashSelf #
theorem
Std.DHashMap.Internal.IsHashSelf.uset
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
{m : Array (AssocList α β)}
{i : USize}
{h : i.toNat < m.size}
{d : AssocList α β}
(hd : List.HashesTo m[i].toList i.toNat m.size → List.HashesTo d.toList i.toNat m.size)
(hm : IsHashSelf m)
:
IsHashSelf (m.uset i d h)
theorem
Std.DHashMap.Internal.IsHashSelf.updateBucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Array (AssocList α β)}
{h : 0 < m.size}
{a : α}
{f : AssocList α β → AssocList α β}
(hf :
∀ (l : AssocList α β) (p : (a : α) × β a),
p ∈ (f l).toList → List.containsKey p.fst l.toList = true ∨ hash p.fst = hash a)
(hm : IsHashSelf m)
:
IsHashSelf (Internal.updateBucket m h a f)
This is the general theorem to show that modification operations preserve well-formedness of buckets.
theorem
Std.DHashMap.Internal.IsHashSelf.updateAllBuckets
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
[BEq α]
[Hashable α]
[LawfulHashable α]
{m : Array (AssocList α β)}
{f : AssocList α β → AssocList α δ}
(hf : ∀ (l : AssocList α β) (p : (a : α) × δ a), p ∈ (f l).toList → List.containsKey p.fst l.toList = true)
(hm : IsHashSelf m)
:
Definition of model functions #
def
Std.DHashMap.Internal.Raw₀.getKeyₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(h : m.containsₘ a = true)
:
α
Internal implementation detail of the hash map
Equations
Instances For
def
Std.DHashMap.Internal.Raw₀.modifyₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[LawfulBEq α]
(m : Raw₀ α β)
(a : α)
(f : β a → β a)
:
Raw₀ α β
Internal implementation detail of the hash map
Equations
- m.modifyₘ a f = m.alterₘ a fun (x : Option (β a)) => Option.map f x
Instances For
def
Std.DHashMap.Internal.Raw₀.Const.alterₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => β)
(a : α)
(f : Option β → Option β)
:
Raw₀ α fun (x : α) => β
Internal implementation detail of the hash map
Equations
- One or more equations did not get rendered due to their size.
Instances For
def
Std.DHashMap.Internal.Raw₀.mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
(m : Raw₀ α β)
(f : (a : α) → β a → δ a)
:
Raw₀ α δ
Internal implementation detail of the hash map
Equations
- m.mapₘ f = ⟨{ size := m.val.size, buckets := Std.DHashMap.Internal.updateAllBuckets m.val.buckets (Std.DHashMap.Internal.AssocList.map f) }, ⋯⟩
Instances For
def
Std.DHashMap.Internal.Raw₀.Const.getₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α fun (x : α) => β)
(a : α)
(h : m.containsₘ a = true)
:
β
Internal implementation detail of the hash map
Equations
Instances For
Equivalence between model functions and real implementations #
theorem
Std.DHashMap.Internal.Raw₀.getKey_eq_getKeyₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Raw₀ α β)
(a : α)
(h : m.contains a = true)
:
theorem
Std.DHashMap.Internal.Raw₀.filter_eq_filterₘ
{α : Type u}
{β : α → Type v}
(m : Raw₀ α β)
(f : (a : α) → β a → Bool)
: