feat: verify insertMany method for adding lists to HashMaps

src/Std/Data/DHashMap/Internal/Model.lean

@@ -188,7 +188,7 @@ theorem toListModel_updateAllBuckets {m : Raw₀ α β} {f : AssocList α β →
     omega
   rw [updateAllBuckets, toListModel, Array.toList_map, List.flatMap_eq_foldl, List.foldl_map,
     toListModel, List.flatMap_eq_foldl]
-  suffices ∀ (l : List (AssocList α β)) (l' : List ((a: α) × δ a)) (l'' : List ((a : α) × β a)),
+  suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) × δ a)) (l'' : List ((a : α) × β a)),
       Perm (g l'') l' →
       Perm (l.foldl (fun acc a => acc ++ (f a).toList) l')
         (g (l.foldl (fun acc a => acc ++ a.toList) l'')) by
@@ -322,6 +322,12 @@ def mapₘ (m : Raw₀ α β) (f : (a : α) → β a → δ a) : Raw₀ α δ :=
 def filterₘ (m : Raw₀ α β) (f : (a : α) → β a → Bool) : Raw₀ α β :=
   ⟨withComputedSize (updateAllBuckets m.1.buckets fun l => l.filter f), by simpa using m.2⟩
 
+/-- Internal implementation detail of the hash map -/
+def insertListₘ [BEq α] [Hashable α](m : Raw₀ α β) (l : List ((a : α) × β a)) : Raw₀ α β :=
+  match l with
+  | .nil => m
+  | .cons hd tl => insertListₘ (m.insert hd.1 hd.2) tl
+
 section
 
 variable {β : Type v}
@@ -342,6 +348,17 @@ def Const.getDₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α)
 def Const.get!ₘ [BEq α] [Hashable α] [Inhabited β] (m : Raw₀ α (fun _ => β)) (a : α) : β :=
   (Const.get?ₘ m a).get!
 
+/-- Internal implementation detail of the hash map -/
+def Const.insertListₘ [BEq α] [Hashable α](m : Raw₀ α (fun _ => β)) (l: List (α × β)): Raw₀ α (fun _ => β) :=
+  match l with
+  | .nil => m
+  | .cons hd tl => insertListₘ (m.insert hd.1 hd.2) tl
+
+/-- Internal implementation detail of the hash map -/
+def Const.insertListIfNewUnitₘ [BEq α] [Hashable α](m : Raw₀ α (fun _ => Unit)) (l: List α): Raw₀ α (fun _ => Unit) :=
+  match l with
+  | .nil => m
+  | .cons hd tl => insertListIfNewUnitₘ (m.insertIfNew hd ()) tl
 end
 
 /-! # Equivalence between model functions and real implementations -/
@@ -455,6 +472,19 @@ theorem map_eq_mapₘ (m : Raw₀ α β) (f : (a : α) → β a → δ a) :
 theorem filter_eq_filterₘ (m : Raw₀ α β) (f : (a : α) → β a → Bool) :
     m.filter f = m.filterₘ f := rfl
 
+theorem insertMany_eq_insertListₘ [BEq α] [Hashable α](m : Raw₀ α β) (l : List ((a : α) × β a)) : insertMany m l = insertListₘ m l := by
+  simp only [insertMany, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
+  suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop),
+    (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' }),
+      (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val =
+    t.val.insertListₘ l from this _
+  intro t
+  induction l generalizing m with
+  | nil => simp[insertListₘ]
+  | cons hd tl ih =>
+    simp only [List.foldl_cons,insertListₘ]
+    apply ih
+
 section
 
 variable {β : Type v}
@@ -485,6 +515,33 @@ theorem Const.getThenInsertIfNew?_eq_get?ₘ [BEq α] [Hashable α] (m : Raw₀
   dsimp only [Array.ugetElem_eq_getElem, Array.uset]
   split <;> simp_all [-getValue?_eq_none]
 
+theorem Const.insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (l: List (α × β)):
+    (Const.insertMany m l).1 = Const.insertListₘ m l := by
+  simp only [insertMany, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
+  suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => β) → Prop),
+    (∀ {m'' : Raw₀ α (fun _ => β)} {a : α} {b : β}, P m'' → P (m''.insert a b)) → P m → P m' }),
+      (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val =
+    Const.insertListₘ t.val l from this _
+  intro t
+  induction l generalizing m with
+  | nil => simp[insertListₘ]
+  | cons hd tl ih =>
+    simp only [List.foldl_cons,insertListₘ]
+    apply ih
+
+theorem Const.insertManyIfNewUnit_eq_insertListIfNewUnitₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => Unit)) (l: List α):
+    (Const.insertManyIfNewUnit m l).1 = Const.insertListIfNewUnitₘ m l := by
+  simp only [insertManyIfNewUnit, Id.run, Id.pure_eq, Id.bind_eq, List.forIn_yield_eq_foldl]
+  suffices ∀ (t : { m' // ∀ (P : Raw₀ α (fun _ => Unit) → Prop),
+      (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m'}),
+      (List.foldl (fun m' p => ⟨m'.val.insertIfNew p (), fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val =
+    Const.insertListIfNewUnitₘ t.val l from this _
+  intro t
+  induction l generalizing m with
+  | nil => simp[insertListIfNewUnitₘ]
+  | cons hd tl ih =>
+    simp only [List.foldl_cons,insertListIfNewUnitₘ]
+    apply ih
 end
 
 end Raw₀

src/Std/Data/DHashMap/Internal/Raw.lean

@@ -199,6 +199,14 @@ theorem filter_val [BEq α] [Hashable α] {m : Raw₀ α β} {f : (a : α) → 
     m.val.filter f = m.filter f := by
   simp [Raw.filter, m.2]
 
+theorem insertMany_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
+    m.insertMany l = Raw₀.insertMany ⟨m, h.size_buckets_pos⟩ l := by
+  simp[Raw.insertMany, h.size_buckets_pos]
+
+theorem insertMany_val [BEq α][Hashable α] {m : Raw₀ α β} {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] {l : ρ} :
+    m.val.insertMany l = m.insertMany l := by
+  simp[Raw.insertMany, m.2]
+
 section
 
 variable {β : Type v}