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]
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.exists_bucket_of_update
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Array (AssocList α β))
(h : 0 < m.size)
(k : α)
(f : AssocList α β → AssocList α β)
:
∃ (l : List ((a : α) × β a)), (toListModel m).Perm ((bucket m h k).toList ++ l) ∧ (toListModel (updateBucket m h k f)).Perm ((f (bucket m h k)).toList ++ l) ∧ ∀ [LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → Internal.List.containsKey k' l = false
theorem
Std.DHashMap.Internal.exists_bucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Array (AssocList α β))
(h : 0 < m.size)
(k : α)
:
∃ (l : List ((a : α) × β a)), (toListModel m).Perm ((bucket m h k).toList ++ l) ∧ ∀ [LawfulHashable α], IsHashSelf m → ∀ (k' : α), hash k = hash k' → Internal.List.containsKey k' l = false
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)}, Internal.List.DistinctKeys l → l.Perm l' → g l = g l')
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.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)) → Internal.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 : Internal.List.containsKey a l = true},
Internal.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' : Internal.List.containsKey a (toListModel m.val.buckets) = true}
(hg₂ :
∀ {l l' : List ((a : α) × β a)} {a : α} {h : Internal.List.containsKey a (l ++ l') = true}
(hl' : Internal.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)}, Internal.List.DistinctKeys l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Internal.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 → Internal.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 → Internal.List.containsKey p.fst l.toList = true)
(hm : IsHashSelf m)
: