theorem Batteries.HashMap.Imp.Buckets.ext_iff {α : Type u_1} {β : Type u_2} {b₁ : Batteries.HashMap.Imp.Buckets α β} {b₂ : Batteries.HashMap.Imp.Buckets α β} : b₁ = b₂ ↔ b₁.val.data = b₂.val.data

theorem Batteries.HashMap.Imp.Buckets.ext {α : Type u_1} {β : Type u_2} {b₁ : Batteries.HashMap.Imp.Buckets α β} {b₂ : Batteries.HashMap.Imp.Buckets α β} : b₁.val.data = b₂.val.data → b₁ = b₂

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.data = self.val.data.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) : ∃ (l₁ : List (Batteries.AssocList α β)), ∃ (l₂ : List (Batteries.AssocList α β)), self.val.data = l₁ ++ self.val[i] :: l₂ ∧ l₁.length = i.toNat ∧ (self.update i d h).val.data = l₁ ++ d :: l₂

theorem Batteries.HashMap.Imp.Buckets.update_update {α : Type u_1} {β : Type u_2} (self : Batteries.HashMap.Imp.Buckets α β) (i : USize) (d : Batteries.AssocList α β) (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 = Nat.sum (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) data.val.data)

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 % buckets.val.size).toNat = i.toNat) buckets.val[i] → Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % 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.data[j]?.getD Batteries.AssocList.nil = Batteries.AssocList.nil) : (Batteries.HashMap.Imp.expand.go i source target).size = Nat.sum (List.map (fun (x : Batteries.AssocList α β) => x.toList.length) source.data) + 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.data → 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.data → 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.data → 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 % source.size).toNat = j) source[j]) {target : Batteries.HashMap.Imp.Buckets α β} (ht : target.WF ∧ ∀ (bucket : Batteries.AssocList α β), bucket ∈ target.val.data → Batteries.AssocList.All (fun (k : α) (x : β) => ((hash k).toUSize % 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) : m.size = m.buckets.size ∧ m.buckets.WF

theorem Batteries.HashMap.Imp.WF_iff {α : Type u_1} {β : Type u_2} [BEq α] [Hashable α] {m : Batteries.HashMap.Imp α β} : m.WF ↔ m.size = m.buckets.size ∧ m.buckets.WF

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_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (α → β → γ) → Batteries.HashMap α β → Batteries.HashMap α γ

Map a function over the values in the map.

Equations

• Batteries.HashMap.mapVal f self = ⟨Batteries.HashMap.Imp.mapVal f self.val, ⋯⟩

@[inline]

def Batteries.HashMap.filterMap {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → {γ : Type u_3} → (α → β → Option γ) → Batteries.HashMap α β → 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, ⋯⟩

@[inline]

def Batteries.HashMap.filter {α : Type u_1} : {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → (α → β → Bool) → Batteries.HashMap α β → 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