From fea55533d9c87b10edac3afde88e8e99b58711f8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= <wojciech@lean-fro.org>
Date: Wed, 26 Nov 2025 17:24:40 +0000
Subject: [PATCH] feat: add `ofArray` to `DHashMap`/`HashMap`/`HashSet`
 (#11243)

This PR adds `ofArray` to `DHashMap`/`HashMap`/`HashSet` and proves a
simp lemma allowing to rewrite `ofArray` to `ofList`.

---------

Co-authored-by: Markus Himmel <markus@himmel-villmar.de>
---
 src/Std/Data/DHashMap/Basic.lean        |  8 ++++++++
 src/Std/Data/DHashMap/Internal/Raw.lean | 16 ++++++++++++++++
 src/Std/Data/DHashMap/Internal/WF.lean  | 12 ++++++++++++
 src/Std/Data/DHashMap/Lemmas.lean       | 15 +++++++++++++++
 src/Std/Data/DHashMap/Raw.lean          | 21 +++++++++++++++++++++
 src/Std/Data/DHashMap/RawLemmas.lean    | 22 ++++++++++++++++++++--
 src/Std/Data/HashMap/Basic.lean         |  4 ++++
 src/Std/Data/HashMap/Lemmas.lean        | 12 ++++++++++++
 src/Std/Data/HashMap/Raw.lean           | 10 ++++++++++
 src/Std/Data/HashMap/RawLemmas.lean     | 12 ++++++++++++
 src/Std/Data/HashSet/Lemmas.lean        |  6 ++++++
 src/Std/Data/HashSet/RawLemmas.lean     |  6 ++++++
 12 files changed, 142 insertions(+), 2 deletions(-)

diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean
index 9094436568..421b1f31ed 100644
--- a/src/Std/Data/DHashMap/Basic.lean
+++ b/src/Std/Data/DHashMap/Basic.lean
@@ -387,10 +387,18 @@ end Unverified
     DHashMap α β :=
   insertMany ∅ l
 
+@[inline, inherit_doc Raw.ofArray] def ofArray [BEq α] [Hashable α] (l : Array ((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.ofArray] def Const.ofArray {β : Type v} [BEq α] [Hashable α]
+    (l : Array (α × β)) : DHashMap α (fun _ => β) :=
+  Const.insertMany ∅ l
+
 @[inline, inherit_doc Raw.Const.unitOfList] def Const.unitOfList [BEq α] [Hashable α] (l : List α) :
     DHashMap α (fun _ => Unit) :=
   Const.insertManyIfNewUnit ∅ l
diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean
index b421e0f6ca..2ec025c701 100644
--- a/src/Std/Data/DHashMap/Internal/Raw.lean
+++ b/src/Std/Data/DHashMap/Internal/Raw.lean
@@ -133,6 +133,11 @@ theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} :
   simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
   congr
 
+theorem ofArray_eq [BEq α] [Hashable α] {a : Array ((a : α) × β a)} :
+    Raw.ofArray a = Raw₀.insertMany Raw₀.emptyWithCapacity a := by
+  simp only [Raw.ofArray, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
+  congr
+
 theorem alter_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} :
     m.alter k f = Raw₀.alter ⟨m, h.size_buckets_pos⟩ k f := by
   simp [Raw.alter, h.size_buckets_pos]
@@ -162,6 +167,11 @@ theorem Const.ofList_eq [BEq α] [Hashable α] {l : List (α × β)} :
   simp only [Raw.Const.ofList, Raw.Const.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte]
   congr
 
+theorem Const.ofArray_eq [BEq α] [Hashable α] {a : Array (α × β)} :
+    Raw.Const.ofArray a = Raw₀.Const.insertMany Raw₀.emptyWithCapacity a := by
+  simp only [Raw.Const.ofArray, 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
@@ -173,6 +183,12 @@ theorem Const.unitOfList_eq [BEq α] [Hashable α] {l : List α} :
     ↓reduceDIte]
   congr
 
+theorem Const.unitOfArray_eq [BEq α] [Hashable α] {a : Array α} :
+    Raw.Const.unitOfArray a = Raw₀.Const.insertManyIfNewUnit Raw₀.emptyWithCapacity a := by
+  simp only [Raw.Const.unitOfArray, 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]
diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean
index 9d7db379b4..1ab1d44292 100644
--- a/src/Std/Data/DHashMap/Internal/WF.lean
+++ b/src/Std/Data/DHashMap/Internal/WF.lean
@@ -1124,6 +1124,18 @@ theorem insertMany_eq_insertListₘ_toListModel [BEq α] [Hashable α] (m m₂ :
     simp only [List.foldl_cons, insertListₘ]
     apply ih
 
+theorem insertMany_array_eq_insertMany_toList [BEq α] [Hashable α] (m : Raw₀ α β) (a : Array ((k : α) × (β k))) :
+    insertMany m a = insertMany m a.toList := by
+  simp only [insertMany, bind_pure_comp, map_pure, bind_pure, ← Array.forIn_toList, forIn_pure_yield_eq_foldl, Array.foldl_toList, Id.run_pure]
+
+theorem Const.insertMany_array_eq_insertMany_toList [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α fun _ => β) (a : Array (α × β)) :
+    Const.insertMany m a = Const.insertMany m a.toList := by
+  simp only [insertMany, bind_pure_comp, map_pure, bind_pure, ← Array.forIn_toList, forIn_pure_yield_eq_foldl, Array.foldl_toList, Id.run_pure]
+
+theorem Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList [BEq α] [Hashable α] (m : Raw₀ α fun _ => Unit) (a : Array α) :
+    Const.insertManyIfNewUnit m a = Const.insertManyIfNewUnit m a.toList := by
+  simp only [insertManyIfNewUnit, bind_pure_comp, map_pure, bind_pure, ← Array.forIn_toList, forIn_pure_yield_eq_foldl, Array.foldl_toList, Id.run_pure]
+
 theorem insertManyIfNew_eq_insertListIfNewₘ_toListModel [BEq α] [Hashable α] (m m₂ : Raw₀ α β) :
     insertManyIfNew m m₂.1 = insertListIfNewₘ m (toListModel m₂.1.buckets) := by
   simp only [insertManyIfNew, bind_pure_comp, map_pure, bind_pure]
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
index 811747c8d6..b9f77346ee 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -2888,6 +2888,11 @@ end DHashMap
 
 namespace DHashMap
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array ((a : α) × (β a))) :
+    ofArray a = ofList a.toList :=
+  ext <| congrArg Subtype.val <| congrArg Subtype.val (Raw₀.insertMany_array_eq_insertMany_toList (α := α) _ a)
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ :=
@@ -3037,6 +3042,11 @@ namespace Const
 
 variable {β : Type v}
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array (α × β)) :
+    ofArray a = ofList a.toList :=
+  ext <| congrArg Subtype.val <| congrArg Subtype.val (Raw₀.Const.insertMany_array_eq_insertMany_toList (α := α) _ a)
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ :=
@@ -3182,6 +3192,11 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     (ofList l).isEmpty = l.isEmpty :=
   Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list
 
+@[simp, grind =]
+theorem unitOfArray_eq_unitOfList (a : Array α) :
+    unitOfArray a = unitOfList a.toList :=
+  ext <| congrArg Subtype.val <| congrArg Subtype.val (Raw₀.Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList (α := α) _ a)
+
 @[simp]
 theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ :=
diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean
index 466558a556..7ae49ace1a 100644
--- a/src/Std/Data/DHashMap/Raw.lean
+++ b/src/Std/Data/DHashMap/Raw.lean
@@ -607,10 +607,19 @@ occurrence takes precedence. -/
 @[inline] def ofList [BEq α] [Hashable α] (l : List ((a : α) × β a)) : Raw α β :=
   insertMany ∅ l
 
+/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
+occurrence takes precedence. -/
+@[inline] def ofArray [BEq α] [Hashable α] (l : Array ((a : α) × β a)) : Raw α β :=
+  insertMany ∅ l
+
 @[inline, inherit_doc Raw.ofList] def Const.ofList {β : Type v} [BEq α] [Hashable α]
     (l : List (α × β)) : Raw α (fun _ => β) :=
   Const.insertMany ∅ l
 
+@[inline, inherit_doc Raw.ofArray] def Const.ofArray {β : Type v} [BEq α] [Hashable α]
+    (l : Array (α × β)) : Raw α (fun _ => β) :=
+  Const.insertMany ∅ l
+
 /-- Creates a hash map from a list of keys, associating the value `()` with each key.
 
 This is mainly useful to implement `HashSet.ofList`, so if you are considering using this,
@@ -760,6 +769,18 @@ theorem WF.Const.unitOfList [BEq α] [Hashable α] {l : List α} :
     (Const.unitOfList l : Raw α (fun _ => Unit)).WF :=
   Const.insertManyIfNewUnit WF.empty
 
+theorem WF.ofArray [BEq α] [Hashable α] {a : Array ((a : α) × β a)} :
+    (ofArray a : Raw α β).WF :=
+  .insertMany WF.empty
+
+theorem WF.Const.ofArray {β : Type v} [BEq α] [Hashable α] {a : Array (α × β)} :
+    (Const.ofArray a : Raw α (fun _ => β)).WF :=
+  Const.insertMany WF.empty
+
+theorem WF.Const.unitOfArray [BEq α] [Hashable α] {a : Array α} :
+    (Const.unitOfArray a : Raw α (fun _ => Unit)).WF :=
+  Const.insertManyIfNewUnit WF.empty
+
 theorem WF.union₀ [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (Raw₀.union ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩).val.WF := by
   simp only [Raw₀.union]
   split
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
index 2ab88c7a43..c868425c5c 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -46,8 +46,8 @@ private meta def baseNames : Array Name :=
     ``get?_eq, ``get_eq, ``get!_eq, ``getD_eq,
     ``Const.get?_eq, ``Const.get_eq, ``Const.getD_eq, ``Const.get!_eq,
     ``getKey?_eq, ``getKey_eq, ``getKey!_eq, ``getKeyD_eq,
-    ``insertMany_eq, ``Const.insertMany_eq, ``Const.insertManyIfNewUnit_eq,
-    ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq,
+    ``insertMany_eq, ``Const.insertMany_eq, ``Const.insertManyIfNewUnit_eq, ``ofArray_eq, ``Const.ofArray_eq,
+    ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq, ``Const.unitOfArray_eq,
     ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq, ``inter_eq]
 
 /-- Internal implementation detail of the hash map -/
@@ -3340,6 +3340,12 @@ variable [BEq α] [Hashable α]
 
 open Internal.Raw Internal.Raw₀
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array ((a : α) × (β a))) :
+    ofArray a = ofList a.toList := by
+  simp_to_raw
+  rw [Raw₀.insertMany_array_eq_insertMany_toList]
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List ((a : α) × (β a))) = ∅ := by
@@ -3492,6 +3498,12 @@ namespace Const
 
 variable {β : Type v}
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array (α × β)) :
+    ofArray a = ofList a.toList := by
+  simp_to_raw
+  rw [Const.insertMany_array_eq_insertMany_toList]
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List (α × β)) = ∅ := by
@@ -3640,6 +3652,12 @@ theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     (ofList l).isEmpty = l.isEmpty := by
   simp_to_raw using Raw₀.Const.isEmpty_insertMany_emptyWithCapacity_list
 
+@[simp, grind =]
+theorem unitOfArray_eq_unitOfList (a : Array α) :
+    unitOfArray a = unitOfList a.toList := by
+  simp_to_raw
+  rw [Raw₀.Const.insertManyIfNewUnit_array_eq_insertManyIfNewUnit_toList]
+
 @[simp]
 theorem unitOfList_nil :
     unitOfList ([] : List α) = ∅ := by
diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean
index 9c0ca3906f..5c96bfd419 100644
--- a/src/Std/Data/HashMap/Basic.lean
+++ b/src/Std/Data/HashMap/Basic.lean
@@ -198,6 +198,10 @@ instance [BEq α] [Hashable α] : GetElem? (HashMap α β) α β (fun m a => a 
     HashMap α Unit :=
   ⟨DHashMap.Const.unitOfList l⟩
 
+@[inline, inherit_doc DHashMap.Const.ofArray] def ofArray [BEq α] [Hashable α] (a : Array (α × β)) :
+    HashMap α β :=
+  ⟨DHashMap.Const.ofArray a⟩
+
 @[inline, inherit_doc DHashMap.Const.toList] def toList (m : HashMap α β) :
     List (α × β) :=
   DHashMap.Const.toList m.inner
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
index 78bb300e15..119f0d6205 100644
--- a/src/Std/Data/HashMap/Lemmas.lean
+++ b/src/Std/Data/HashMap/Lemmas.lean
@@ -2105,6 +2105,12 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
 
 grind_pattern size_ofList_le => (ofList l).size
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array (α × β)) :
+    ofArray a = ofList a.toList := by
+  apply ext
+  apply DHashMap.Const.ofArray_eq_ofList
+
 @[simp, grind =]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
@@ -2222,6 +2228,12 @@ theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α]
     (unitOfList l).size ≤ l.length :=
   DHashMap.Const.size_unitOfList_le
 
+@[simp, grind =]
+theorem unitOfArray_eq_unitOfList (a : Array α) :
+    unitOfArray a = unitOfList a.toList := by
+  apply ext
+  apply DHashMap.Const.unitOfArray_eq_unitOfList
+
 @[simp]
 theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean
index 5d5983455c..69c068caec 100644
--- a/src/Std/Data/HashMap/Raw.lean
+++ b/src/Std/Data/HashMap/Raw.lean
@@ -192,6 +192,10 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m
     (l : List α) : Raw α Unit :=
   ⟨DHashMap.Raw.Const.unitOfList l⟩
 
+@[inline, inherit_doc DHashMap.Raw.Const.ofList] def ofArray [BEq α] [Hashable α]
+    (a : Array (α × β)) : Raw α β :=
+  ⟨DHashMap.Raw.Const.ofArray a⟩
+
 @[inline, inherit_doc DHashMap.Raw.Const.alter] def alter [BEq α] [EquivBEq α] [Hashable α]
     (m : Raw α β) (a : α) (f : Option β → Option β) : Raw α β :=
   ⟨DHashMap.Raw.Const.alter m.inner a f⟩
@@ -342,9 +346,15 @@ theorem WF.insertManyIfNewUnit [BEq α] [Hashable α] {ρ : Type w} [ForIn Id ρ
 theorem WF.ofList [BEq α] [Hashable α] {l : List (α × β)} : (ofList l).WF :=
   ⟨DHashMap.Raw.WF.Const.ofList⟩
 
+theorem WF.ofArray [BEq α] [Hashable α] {a : Array (α × β)} : (ofArray a).WF :=
+  ⟨DHashMap.Raw.WF.Const.ofArray⟩
+
 theorem WF.unitOfList [BEq α] [Hashable α] {l : List α} : (unitOfList l).WF :=
   ⟨DHashMap.Raw.WF.Const.unitOfList⟩
 
+theorem WF.unitOfArray [BEq α] [Hashable α] {a : Array α} : (unitOfArray a).WF :=
+  ⟨DHashMap.Raw.WF.Const.unitOfArray⟩
+
 theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ m₂).WF :=
   ⟨DHashMap.Raw.WF.union h₁.out h₂.out⟩
 
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
index 24f43169ab..ec42aba0de 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -2156,6 +2156,12 @@ theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
 
 grind_pattern size_ofList_le => (ofList l).size
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array (α × β)) :
+    ofArray a = ofList a.toList := by
+  apply ext
+  apply DHashMap.Raw.Const.ofArray_eq_ofList
+
 @[simp, grind =]
 theorem isEmpty_ofList [EquivBEq α] [LawfulHashable α]
     {l : List (α × β)} :
@@ -2244,6 +2250,12 @@ theorem size_unitOfList_le [EquivBEq α] [LawfulHashable α]
     (unitOfList l).size ≤ l.length :=
   DHashMap.Raw.Const.size_unitOfList_le
 
+@[simp, grind =]
+theorem unitOfArray_eq_unitOfList (a : Array α) :
+    unitOfArray a = unitOfList a.toList := by
+  apply ext
+  apply DHashMap.Raw.Const.unitOfArray_eq_unitOfList
+
 @[simp]
 theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α]
     {l : List α} :
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
index 5404567e88..0dfc0ab2b1 100644
--- a/src/Std/Data/HashSet/Lemmas.lean
+++ b/src/Std/Data/HashSet/Lemmas.lean
@@ -1086,6 +1086,12 @@ end Inter
 
 section
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array α) :
+    ofArray a = ofList a.toList := by
+  apply ext
+  apply HashMap.unitOfArray_eq_unitOfList
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List α) = ∅ :=
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
index a780c965bf..26252658a1 100644
--- a/src/Std/Data/HashSet/RawLemmas.lean
+++ b/src/Std/Data/HashSet/RawLemmas.lean
@@ -1150,6 +1150,12 @@ theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h
 
 end Inter
 
+@[simp, grind =]
+theorem ofArray_eq_ofList (a : Array α) :
+    ofArray a = ofList a.toList := by
+  apply ext
+  apply HashMap.Raw.unitOfArray_eq_unitOfList
+
 @[simp, grind =]
 theorem ofList_nil :
     ofList ([] : List α) = ∅ :=