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
- Std.DHashMap.Internal.bucket self h k = match Std.DHashMap.Internal.mkIdx self.size h (hash k) with | ⟨i, h⟩ => self[i]
Instances For
def
Std.DHashMap.Internal.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 α β)
:
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.updateBucket self h k f = match Std.DHashMap.Internal.mkIdx self.size h (hash k) with | ⟨i, h⟩ => self.uset i (f self[i]) h
Instances For
def
Std.DHashMap.Internal.updateAllBuckets
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
(self : Array (Std.DHashMap.Internal.AssocList α β))
(f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ)
:
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.updateAllBuckets self f = Array.map f self
Instances For
def
Std.DHashMap.Internal.withComputedSize
{α : Type u}
{β : α → Type v}
(self : Array (Std.DHashMap.Internal.AssocList α β))
:
Std.DHashMap.Raw α β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.withComputedSize self = { size := Std.DHashMap.Internal.computeSize self, buckets := self }
Instances For
@[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.size_updateAllBuckets
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
{self : Array (Std.DHashMap.Internal.AssocList α β)}
{f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ}
:
(Std.DHashMap.Internal.updateAllBuckets self f).size = self.size
@[simp]
theorem
Std.DHashMap.Internal.buckets_size_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (Std.DHashMap.Internal.AssocList α β)}
:
(Std.DHashMap.Internal.withComputedSize self).buckets.size = self.size
@[simp]
theorem
Std.DHashMap.Internal.size_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (Std.DHashMap.Internal.AssocList α β)}
:
(Std.DHashMap.Internal.withComputedSize self).size = Std.DHashMap.Internal.computeSize self
@[simp]
theorem
Std.DHashMap.Internal.buckets_withComputedSize
{α : Type u}
{β : α → Type v}
{self : Array (Std.DHashMap.Internal.AssocList α β)}
:
(Std.DHashMap.Internal.withComputedSize self).buckets = self
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.toNat →
Std.DHashMap.Internal.List.containsKey k l = false
theorem
Std.DHashMap.Internal.exists_bucket_of_update
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Array (Std.DHashMap.Internal.AssocList α β))
(h : 0 < m.size)
(k : α)
(f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β)
:
∃ (l : List ((a : α) × β a)),
(Std.DHashMap.Internal.toListModel m).Perm ((Std.DHashMap.Internal.bucket m h k).toList ++ l) ∧ (Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateBucket m h k f)).Perm
((f (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.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.data.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.toNat →
Std.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 l → l.Perm l' → g l = g l')
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.containsKey a l' = false → g (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 l → l.Perm l' → (g l).Perm (g l'))
(hg₂ : ∀ {l l' : List ((a : α) × β a)}, Std.DHashMap.Internal.List.containsKey a l' = false → g (l ++ l') = g l ++ l')
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateBucket m.val.buckets ⋯ a f)).Perm
(g (Std.DHashMap.Internal.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 : 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'))
:
(Std.DHashMap.Internal.toListModel (Std.DHashMap.Internal.updateAllBuckets m.val.buckets f)).Perm
(g (Std.DHashMap.Internal.toListModel m.val.buckets))
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.size →
Std.DHashMap.Internal.List.HashesTo d.toList i.toNat m.size)
(hm : Std.DHashMap.Internal.IsHashSelf m)
:
Std.DHashMap.Internal.IsHashSelf (m.uset i d h)
theorem
Std.DHashMap.Internal.IsHashSelf.updateBucket
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
[PartialEquivBEq α]
[LawfulHashable α]
{m : Array (Std.DHashMap.Internal.AssocList α β)}
{h : 0 < m.size}
{a : α}
{f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α β}
(hf : ∀ (l : Std.DHashMap.Internal.AssocList α β) (p : (a : α) × β a),
p ∈ (f l).toList → Std.DHashMap.Internal.List.containsKey p.fst l.toList = true ∨ hash p.fst = hash a)
(hm : Std.DHashMap.Internal.IsHashSelf m)
:
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 (Std.DHashMap.Internal.AssocList α β)}
{f : Std.DHashMap.Internal.AssocList α β → Std.DHashMap.Internal.AssocList α δ}
(hf : ∀ (l : Std.DHashMap.Internal.AssocList α β) (p : (a : α) × δ a),
p ∈ (f l).toList → Std.DHashMap.Internal.List.containsKey p.fst l.toList = true)
(hm : Std.DHashMap.Internal.IsHashSelf m)
:
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.
Instances For
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.
Instances For
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
- m.get?ₘ a = Std.DHashMap.Internal.AssocList.getCast? a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a)
Instances For
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
- m.containsₘ a = Std.DHashMap.Internal.AssocList.contains a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a)
Instances For
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
- m.getₘ a h = Std.DHashMap.Internal.AssocList.getCast a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a) h
Instances For
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
Instances For
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!
Instances For
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
Instances For
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
Instances For
def
Std.DHashMap.Internal.Raw₀.eraseₘaux
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
:
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₀.eraseₘ
{α : Type u}
{β : α → Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α β)
(a : α)
:
Internal implementation detail of the hash map
Instances For
def
Std.DHashMap.Internal.Raw₀.filterMapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
(m : Std.DHashMap.Internal.Raw₀ α β)
(f : (a : α) → β a → Option (δ a))
:
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 : Std.DHashMap.Internal.Raw₀ α β)
(f : (a : α) → β a → δ a)
:
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₀.filterₘ
{α : Type u}
{β : α → Type v}
(m : Std.DHashMap.Internal.Raw₀ α β)
(f : (a : α) → β a → Bool)
:
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₀.Const.get?ₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
:
Option β
Internal implementation detail of the hash map
Equations
- Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a = Std.DHashMap.Internal.AssocList.get? a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a)
Instances For
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
- Std.DHashMap.Internal.Raw₀.Const.getₘ m a h = Std.DHashMap.Internal.AssocList.get a (Std.DHashMap.Internal.bucket m.val.buckets ⋯ a) h
Instances For
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
- Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback = (Std.DHashMap.Internal.Raw₀.Const.get?ₘ m a).getD fallback
Instances For
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
Instances For
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)
:
(Std.DHashMap.Internal.Raw₀.reinsertAux hash data a b).val = Std.DHashMap.Internal.updateBucket data.val ⋯ a fun (l : Std.DHashMap.Internal.AssocList α β) =>
Std.DHashMap.Internal.AssocList.cons a b l
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₀.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₀.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 : α) → β a → Option (δ a))
:
Std.DHashMap.Internal.Raw₀.filterMap f m = m.filterMapₘ f
theorem
Std.DHashMap.Internal.Raw₀.map_eq_mapₘ
{α : Type u}
{β : α → Type v}
{δ : α → Type w}
(m : Std.DHashMap.Internal.Raw₀ α β)
(f : (a : α) → β a → δ a)
:
Std.DHashMap.Internal.Raw₀.map f m = m.mapₘ f
theorem
Std.DHashMap.Internal.Raw₀.filter_eq_filterₘ
{α : Type u}
{β : α → Type v}
(m : Std.DHashMap.Internal.Raw₀ α β)
(f : (a : α) → β a → Bool)
:
Std.DHashMap.Internal.Raw₀.filter f m = m.filterₘ f
theorem
Std.DHashMap.Internal.Raw₀.Const.get?_eq_get?ₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.get_eq_getₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
(h : m.contains a = true)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getD_eq_getDₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
(fallback : β)
:
Std.DHashMap.Internal.Raw₀.Const.getD m a fallback = Std.DHashMap.Internal.Raw₀.Const.getDₘ m a fallback
theorem
Std.DHashMap.Internal.Raw₀.Const.get!_eq_get!ₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
[Inhabited β]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
:
theorem
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_eq_insertIfNewₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
(b : β)
:
(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).snd = m.insertIfNewₘ a b
theorem
Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew?_eq_get?ₘ
{α : Type u}
{β : Type v}
[BEq α]
[Hashable α]
(m : Std.DHashMap.Internal.Raw₀ α fun (x : α) => β)
(a : α)
(b : β)
: