theorem
Batteries.HashMap.Imp.Buckets.ext
{α : Type u_1}
{β : Type u_2}
{b₁ b₂ : Batteries.HashMap.Imp.Buckets α β}
:
theorem
Batteries.HashMap.Imp.Buckets.toList_update
{α : Type u_1}
{β : Type u_2}
(self : Batteries.HashMap.Imp.Buckets α β)
(i : USize)
(d : Batteries.AssocList α β)
(h : i.toNat < self.val.size)
:
(self.update i d h).val.toList = self.val.toList.set i.toNat d
@[deprecated Batteries.HashMap.Imp.Buckets.toList_update]
theorem
Batteries.HashMap.Imp.Buckets.update_data
{α : Type u_1}
{β : Type u_2}
(self : Batteries.HashMap.Imp.Buckets α β)
(i : USize)
(d : Batteries.AssocList α β)
(h : i.toNat < self.val.size)
:
(self.update i d h).val.toList = self.val.toList.set i.toNat d
theorem
Batteries.HashMap.Imp.Buckets.exists_of_update
{α : Type u_1}
{β : Type u_2}
(self : Batteries.HashMap.Imp.Buckets α β)
(i : USize)
(d : Batteries.AssocList α β)
(h : i.toNat < self.val.size)
:
theorem
Batteries.HashMap.Imp.Buckets.update_update
{α : Type u_1}
{β : Type u_2}
(self : Batteries.HashMap.Imp.Buckets α β)
(i : USize)
(d d' : Batteries.AssocList α β)
(h : i.toNat < self.val.size)
(h' : i.toNat < (self.update i d h).val.size)
:
(self.update i d h).update i d' h' = self.update i d' h
theorem
Batteries.HashMap.Imp.Buckets.size_eq
{α : Type u_1}
{β : Type u_2}
(data : Batteries.HashMap.Imp.Buckets α β)
:
data.size = (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) data.val.toList).sum
theorem
Batteries.HashMap.Imp.Buckets.mk_size
{α : Type u_1}
{β : Type u_2}
{n : Nat}
(h : 0 < n)
:
(Batteries.HashMap.Imp.Buckets.mk n h).size = 0
theorem
Batteries.HashMap.Imp.Buckets.WF.mk'
{α : Type u_1}
{β : Type u_2}
{n : Nat}
[BEq α]
[Hashable α]
(h : 0 < n)
:
(Batteries.HashMap.Imp.Buckets.mk n h).WF
theorem
Batteries.HashMap.Imp.Buckets.WF.update
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{buckets : Batteries.HashMap.Imp.Buckets α β}
{i : USize}
{d : Batteries.AssocList α β}
{h : i.toNat < buckets.val.size}
(H : buckets.WF)
(h₁ :
∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α],
List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) buckets.val[i].toList →
List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) d.toList)
(h₂ :
Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat)
buckets.val[i] →
Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % USize.ofNat buckets.val.size).toNat = i.toNat)
d)
:
(buckets.update i d h).WF
theorem
Batteries.HashMap.Imp.reinsertAux_size
{α : Type u_1}
{β : Type u_2}
[Hashable α]
(data : Batteries.HashMap.Imp.Buckets α β)
(a : α)
(b : β)
:
(Batteries.HashMap.Imp.reinsertAux data a b).size = data.size.succ
theorem
Batteries.HashMap.Imp.reinsertAux_WF
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{data : Batteries.HashMap.Imp.Buckets α β}
{a : α}
{b : β}
(H : data.WF)
(h₁ :
∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α],
Batteries.AssocList.All (fun (x : α) (x_1 : β) => ¬(a == x) = true)
data.val[(Batteries.HashMap.Imp.mkIdx ⋯ (hash a).toUSize).val])
:
(Batteries.HashMap.Imp.reinsertAux data a b).WF
theorem
Batteries.HashMap.Imp.expand_size
{α : Type u_1}
{β : Type u_2}
{sz : Nat}
[Hashable α]
{buckets : Batteries.HashMap.Imp.Buckets α β}
:
(Batteries.HashMap.Imp.expand sz buckets).buckets.size = buckets.size
@[irreducible]
theorem
Batteries.HashMap.Imp.expand_size.go
{α : Type u_1}
{β : Type u_2}
[Hashable α]
(i : Nat)
(source : Array (Batteries.AssocList α β))
(target : Batteries.HashMap.Imp.Buckets α β)
(hs : ∀ (j : Nat), j < i → source.toList[j]?.getD Batteries.AssocList.nil = Batteries.AssocList.nil)
:
(Batteries.HashMap.Imp.expand.go i source target).size = (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) source.toList).sum + target.size
theorem
Batteries.HashMap.Imp.expand_WF.foldl
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
(rank : α → Nat)
{l : List (α × β)}
{i : Nat}
(hl₁ :
∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α],
List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) l)
(hl₂ : ∀ (x : α × β), x ∈ l → rank x.fst = i)
{target : Batteries.HashMap.Imp.Buckets α β}
(ht₁ : target.WF)
(ht₂ :
∀ (bucket : Batteries.AssocList α β),
bucket ∈ target.val.toList →
Batteries.AssocList.All
(fun (k : α) (x : β) =>
rank k ≤ i ∧ ∀ [inst : PartialEquivBEq α] [inst : Batteries.HashMap.LawfulHashable α] (x : α × β),
x ∈ l → ¬(x.fst == k) = true)
bucket)
:
(List.foldl (fun (d : Batteries.HashMap.Imp.Buckets α β) (x : α × β) => Batteries.HashMap.Imp.reinsertAux d x.fst x.snd)
target l).WF ∧ ∀ (bucket : Batteries.AssocList α β),
bucket ∈ (List.foldl
(fun (d : Batteries.HashMap.Imp.Buckets α β) (x : α × β) =>
Batteries.HashMap.Imp.reinsertAux d x.fst x.snd)
target l).val.toList →
Batteries.AssocList.All (fun (k : α) (x : β) => rank k ≤ i) bucket
theorem
Batteries.HashMap.Imp.expand_WF
{α : Type u_1}
{β : Type u_2}
{sz : Nat}
[BEq α]
[Hashable α]
{buckets : Batteries.HashMap.Imp.Buckets α β}
(H : buckets.WF)
:
(Batteries.HashMap.Imp.expand sz buckets).buckets.WF
@[irreducible]
theorem
Batteries.HashMap.Imp.expand_WF.go
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
(i : Nat)
{source : Array (Batteries.AssocList α β)}
(hs₁ :
∀ [inst : Batteries.HashMap.LawfulHashable α] [inst : PartialEquivBEq α] (bucket : Batteries.AssocList α β),
bucket ∈ source.toList → List.Pairwise (fun (a b : α × β) => ¬(a.fst == b.fst) = true) bucket.toList)
(hs₂ :
∀ (j : Nat) (h : j < source.size),
Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % USize.ofNat source.size).toNat = j) source[j])
{target : Batteries.HashMap.Imp.Buckets α β}
(ht :
target.WF ∧ ∀ (bucket : Batteries.AssocList α β),
bucket ∈ target.val.toList →
Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % USize.ofNat source.size).toNat < i) bucket)
:
(Batteries.HashMap.Imp.expand.go i source target).WF
theorem
Batteries.HashMap.Imp.insert_size
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
{v : β}
(h : m.size = m.buckets.size)
:
(m.insert k v).size = (m.insert k v).buckets.size
theorem
Batteries.HashMap.Imp.insert_WF
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
{v : β}
(h : m.buckets.WF)
:
(m.insert k v).buckets.WF
theorem
Batteries.HashMap.Imp.erase_size
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
(h : m.size = m.buckets.size)
:
(m.erase k).size = (m.erase k).buckets.size
theorem
Batteries.HashMap.Imp.erase_WF
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
(h : m.buckets.WF)
:
(m.erase k).buckets.WF
theorem
Batteries.HashMap.Imp.modify_size
{α : Type u_1}
{β : Type u_2}
{f : α → β → β}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
(h : m.size = m.buckets.size)
:
(m.modify k f).size = (m.modify k f).buckets.size
theorem
Batteries.HashMap.Imp.modify_WF
{α : Type u_1}
{β : Type u_2}
{f : α → β → β}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
{k : α}
(h : m.buckets.WF)
:
(m.modify k f).buckets.WF
theorem
Batteries.HashMap.Imp.WF.out
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
(h : m.WF)
:
theorem
Batteries.HashMap.Imp.WF_iff
{α : Type u_1}
{β : Type u_2}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
:
theorem
Batteries.HashMap.Imp.WF.mapVal
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → γ}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
(H : m.WF)
:
(Batteries.HashMap.Imp.mapVal f m).WF
theorem
Batteries.HashMap.Imp.WF.filterMap
{α : Type u_1}
{β : Type u_2}
{γ : Type u_3}
{f : α → β → Option γ}
[BEq α]
[Hashable α]
{m : Batteries.HashMap.Imp α β}
(H : m.WF)
:
(Batteries.HashMap.Imp.filterMap f m).WF
@[inline]
def
Batteries.HashMap.mapVal
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → γ)
(self : Batteries.HashMap α β)
:
Map a function over the values in the map.
Equations
- Batteries.HashMap.mapVal f self = ⟨Batteries.HashMap.Imp.mapVal f self.val, ⋯⟩
Instances For
@[inline]
def
Batteries.HashMap.filterMap
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type u_2}
{γ : Type u_3}
(f : α → β → Option γ)
(self : Batteries.HashMap α β)
:
Applies f to each key-value pair a, b in the map. If it returns some c then
a, c is pushed into the new map; else the key is removed from the map.
Equations
- Batteries.HashMap.filterMap f self = ⟨Batteries.HashMap.Imp.filterMap f self.val, ⋯⟩
Instances For
@[inline]
def
Batteries.HashMap.filter
{α : Type u_1}
{x✝ : BEq α}
{x✝¹ : Hashable α}
{β : Type u_2}
(f : α → β → Bool)
(self : Batteries.HashMap α β)
:
Constructs a map with the set of all pairs a, b such that f returns true.
Equations
- Batteries.HashMap.filter f self = Batteries.HashMap.filterMap (fun (a : α) (b : β) => bif f a b then some b else none) self