feat: verify insertMany method for adding lists to HashMaps (#6211)

This PR verifies the `insertMany` method on `HashMap`s for the special
case of inserting lists.

---------

Co-authored-by: jt0202 <[email protected]>
Co-authored-by: monsterkrampe <[email protected]>
Co-authored-by: Johannes Tantow <[email protected]>

src/Std/Data/DHashMap/Basic.lean

@@ -290,24 +290,12 @@ This function ensures that the value is used linearly.
   ⟨(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
    (Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insertIfNew₀ m.2⟩
 
-@[inline, inherit_doc Raw.ofList] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
-    DHashMap α β :=
-  insertMany ∅ l
-
 /-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/
 @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β :=
   m₂.fold (init := m₁) fun acc x => acc.insert x
 
 instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩
 
-@[inline, inherit_doc Raw.Const.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
-    (l : List (α × β)) : DHashMap α (fun _ => β) :=
-  Const.insertMany ∅ l
-
-@[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
-    DHashMap α (fun _ => Unit) :=
-  Const.insertManyIfNewUnit ∅ l
-
 @[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) :
     DHashMap α (fun _ => Unit) :=
   Const.insertManyIfNewUnit ∅ l
@@ -321,4 +309,16 @@ instance [BEq α] [Hashable α] [Repr α] [(a : α) → Repr (β a)] : Repr (DHa
 
 end Unverified
 
+@[inline, inherit_doc Raw.ofList] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) :
+    DHashMap α β :=
+  insertMany ∅ l
+
+@[inline, inherit_doc Raw.Const.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
+    (l : List (α × β)) : DHashMap α (fun _ => β) :=
+  Const.insertMany ∅ l
+
+@[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
+    DHashMap α (fun _ => Unit) :=
+  Const.insertManyIfNewUnit ∅ l
+
 end Std.DHashMap

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

@@ -201,7 +201,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
@@ -378,6 +378,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}
@@ -398,6 +404,20 @@ 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 -/
@@ -569,6 +589,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}
@@ -599,6 +632,36 @@ 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,10 +199,52 @@ 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]
+
+theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
+    Raw.ofList l = Raw₀.insertMany Raw₀.empty l := by
+  simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
+  congr
+
 section
 
 variable {β : Type v}
 
+theorem Const.insertMany_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} :
+    Raw.Const.insertMany m l = Raw₀.Const.insertMany ⟨m, h.size_buckets_pos⟩ l := by
+  simp [Raw.Const.insertMany, h.size_buckets_pos]
+
+theorem Const.insertMany_val [BEq α][Hashable α] {m : Raw₀ α (fun _ => β)} {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} :
+    Raw.Const.insertMany m.val l = Raw₀.Const.insertMany m l := by
+  simp [Raw.Const.insertMany, m.2]
+
+theorem Const.ofList_eq [BEq α] [Hashable α] {l : List (α × β)} :
+    Raw.Const.ofList l = Raw₀.Const.insertMany Raw₀.empty l := by
+  simp only [Raw.Const.ofList, Raw.Const.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
+  congr
+
+theorem Const.insertManyIfNewUnit_eq {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α]
+    {m : Raw α (fun _ => Unit)} {l : ρ} (h : m.WF):
+    Raw.Const.insertManyIfNewUnit m l = Raw₀.Const.insertManyIfNewUnit ⟨m, h.size_buckets_pos⟩ l := by
+  simp [Raw.Const.insertManyIfNewUnit, h.size_buckets_pos]
+
+theorem Const.insertManyIfNewUnit_val {ρ : Type w} [ForIn Id ρ α] [BEq α] [Hashable α]
+    {m : Raw₀ α (fun _ => Unit)} {l : ρ} :
+    Raw.Const.insertManyIfNewUnit m.val l = Raw₀.Const.insertManyIfNewUnit m l := by
+  simp [Raw.Const.insertManyIfNewUnit, m.2]
+
+theorem Const.unitOfList_eq [BEq α] [Hashable α] {l : List α} :
+    Raw.Const.unitOfList l = Raw₀.Const.insertManyIfNewUnit Raw₀.empty l := by
+  simp only [Raw.Const.unitOfList, Raw.Const.insertManyIfNewUnit, (Raw.WF.empty).size_buckets_pos ∅,
+    ↓reduceDIte]
+  congr
+
 theorem Const.get?_eq [BEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {a : α} :
     Raw.Const.get? m a = Raw₀.Const.get? ⟨m, h.size_buckets_pos⟩ a := by
   simp [Raw.Const.get?, h.size_buckets_pos]