feat: verify toList for hash maps (#6954)

This PR verifies the `toList`function for hash maps and dependent hash
maps.

src/Std/Data/DHashMap/Basic.lean

@@ -180,6 +180,14 @@ end
 @[inline, inherit_doc Raw.keys] def keys (m : DHashMap α β) : List α :=
   m.1.keys
 
+@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
+    List ((a : α) × β a) :=
+  m.1.toList
+
+@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
+    (m : DHashMap α (fun _ => β)) : List (α × β) :=
+  Raw.Const.toList m.1
+
 section Unverified
 
 /-! We currently do not provide lemmas for the functions below. -/
@@ -219,18 +227,10 @@ instance [BEq α] [Hashable α] : ForM m (DHashMap α β) ((a : α) × β a) whe
 instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
-@[inline, inherit_doc Raw.toList] def toList (m : DHashMap α β) :
-    List ((a : α) × β a) :=
-  m.1.toList
-
 @[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
     Array ((a : α) × β a) :=
   m.1.toArray
 
-@[inline, inherit_doc Raw.Const.toList] def Const.toList {β : Type v}
-    (m : DHashMap α (fun _ => β)) : List (α × β) :=
-  Raw.Const.toList m.1
-
 @[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
     (m : DHashMap α (fun _ => β)) : Array (α × β) :=
   Raw.Const.toArray m.1

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

@@ -89,9 +89,8 @@ private def queryNames : Array Name :=
     ``Const.get_eq_getValue, ``get!_eq_getValueCast!, ``getD_eq_getValueCastD,
     ``Const.get!_eq_getValue!, ``Const.getD_eq_getValueD, ``getKey?_eq_getKey?,
     ``getKey_eq_getKey, ``getKeyD_eq_getKeyD, ``getKey!_eq_getKey!,
-    ``Raw.length_keys_eq_length_keys, ``Raw.isEmpty_keys_eq_isEmpty_keys,
-    ``Raw.contains_keys_eq_contains_keys, ``Raw.mem_keys_iff_contains_keys,
-    ``Raw.pairwise_keys_iff_pairwise_keys]
+    ``Raw.toList_eq_toListModel, ``Raw.keys_eq_keys_toListModel,
+    ``Raw.Const.toList_eq_toListModel_map]
 
 private def modifyMap : Std.DHashMap Name (fun _ => Name) :=
   .ofList
@@ -848,13 +847,95 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
 @[simp]
 theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
+  rw [← List.contains_iff]
   simp_to_model
   rw [List.containsKey_eq_keys_contains]
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.Pairwise (fun a b => (a == b) = false) := by
   simp_to_model using (Raw.WF.out h).distinct.distinct
 
+theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
+    m.1.toList.map Sigma.fst = m.1.keys := by
+  simp_to_model
+  rw [List.keys_eq_map]
+
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.length = m.1.size := by
+  simp_to_model
+
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.isEmpty = m.1.isEmpty := by
+  simp_to_model
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.1.toList ↔ m.get? k = some v := by
+  simp_to_model using List.mem_iff_getValueCast?_eq_some
+
+theorem find?_toList_eq_some_iff_get?_eq_some [LawfulBEq α]
+    (h : m.1.WF) {k : α} {v : β k} :
+    m.1.toList.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
+  simp_to_model using List.find?_eq_some_iff_getValueCast?_eq_some
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    m.1.toList.find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_model using List.find?_eq_none_iff_containsKey_eq_false
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.toList.Pairwise (fun a b => (a.1 == b.1) = false) := by
+  simp_to_model using List.pairwise_fst_eq_false
+
+namespace Const
+
+variable {β : Type v} (m : Raw₀ α (fun _ => β))
+
+theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
+    (Raw.Const.toList m.1).map Prod.fst = m.1.keys := by
+  simp_to_model using List.map_prod_fst_map_toProd_eq_keys
+
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).length = m.1.size := by
+  simp_to_model using List.length_map
+
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).isEmpty = m.1.isEmpty := by
+  simp_to_model
+  rw [Bool.eq_iff_iff, List.isEmpty_iff,List.isEmpty_iff, List.map_eq_nil_iff]
+
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
+    {k : α} {v : β} :
+    (k, v) ∈ Raw.Const.toList m.1 ↔ get? m k = some v := by
+  simp_to_model using List.mem_map_toProd_iff_getValue?_eq_some
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toList m.1 := by
+  simp_to_model using getValue?_eq_some_iff_exists_beq_and_mem_toList
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} {v : β} :
+    (Raw.Const.toList m.1).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v := by
+  simp_to_model using List.find?_map_toProd_eq_some_iff_getKey?_eq_some_and_getValue?_eq_some
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k : α} :
+    (Raw.Const.toList m.1).find? (·.1 == k) = none ↔ m.contains k = false := by
+  simp_to_model using List.find?_map_eq_none_iff_containsKey_eq_false
+
+theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    (h : m.1.WF) {k: α} {v : β} :
+    (k, v) ∈ (Raw.Const.toList m.1) ↔ m.getKey? k = some k ∧ get? m k = some v := by
+  simp_to_model using List.mem_map_toProd_iff_getKey?_eq_some_and_getValue?_eq_some
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    (Raw.Const.toList m.1).Pairwise (fun a b => (a.1 == b.1) = false) := by
+  simp_to_model using List.pairwise_fst_eq_false_map_toProd
+
+end Const
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m := by
@@ -1230,7 +1311,7 @@ theorem getKey?_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashab
   simp_to_model [Const.insertManyIfNewUnit] using List.getKey?_insertListIfNewUnit_of_contains
 
 theorem getKey_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α]
-    (h : m.1.WF) {l : List α} {k : α} {h'} (contains : m.contains k):
+    (h : m.1.WF) {l : List α} {k : α} {h'} (contains : m.contains k) :
     getKey (insertManyIfNewUnit m l).1 k h' = getKey m k contains := by
   simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains
 

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

@@ -104,37 +104,25 @@ theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
     l.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc = toListModel l.buckets ++ acc := by
   simp [foldRev_cons_apply]
 
+theorem foldRev_cons_mk {β : Type v} {l : Raw α (fun _ => β)} {acc : List (α × β)} :
+    l.foldRev (fun acc k v => (k, v) :: acc) acc =
+      (toListModel l.buckets).map (fun ⟨k, v⟩ => (k, v)) ++ acc := by
+  simp [foldRev_cons_apply]
+
 theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
     l.foldRev (fun acc k _ => k :: acc) acc = List.keys (toListModel l.buckets) ++ acc := by
   rw [foldRev_cons_apply, keys_eq_map]
 
-theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
+theorem toList_eq_toListModel {m : Raw α β} : m.toList = toListModel m.buckets := by
   simp [Raw.toList, foldRev_cons]
 
-theorem keys_perm_keys_toListModel {m : Raw α β} :
-    Perm m.keys (List.keys (toListModel m.buckets)) := by
-  simp [Raw.keys, foldRev_cons_key, keys_eq_map]
-
-theorem length_keys_eq_length_keys {m : Raw α β} :
-    m.keys.length = (List.keys (toListModel m.buckets)).length :=
-  keys_perm_keys_toListModel.length_eq
+theorem Const.toList_eq_toListModel_map {β : Type v} {m : Raw α (fun _ => β)} :
+    Raw.Const.toList m = (toListModel m.buckets).map (fun ⟨k, v⟩ => ⟨k, v⟩) := by
+  simp [Raw.Const.toList, foldRev_cons_mk]
 
-theorem isEmpty_keys_eq_isEmpty_keys {m : Raw α β} :
-    m.keys.isEmpty = (List.keys (toListModel m.buckets)).isEmpty :=
-  keys_perm_keys_toListModel.isEmpty_eq
-
-theorem contains_keys_eq_contains_keys [BEq α] {m : Raw α β} {k : α} :
-    m.keys.contains k = (List.keys (toListModel m.buckets)).contains k :=
-  keys_perm_keys_toListModel.contains_eq
-
-theorem mem_keys_iff_contains_keys [BEq α] [LawfulBEq α] {m : Raw α β} {k : α} :
-    k ∈ m.keys ↔ (List.keys (toListModel m.buckets)).contains k := by
-  rw [← List.contains_iff_mem, contains_keys_eq_contains_keys]
-
-theorem pairwise_keys_iff_pairwise_keys [BEq α] [PartialEquivBEq α] {m : Raw α β} :
-    m.keys.Pairwise (fun a b => (a == b) = false) ↔
-      (List.keys (toListModel m.buckets)).Pairwise (fun a b => (a == b) = false) :=
-  keys_perm_keys_toListModel.pairwise_iff BEq.symm_false
+theorem keys_eq_keys_toListModel {m : Raw α β }:
+    m.keys = List.keys (toListModel m.buckets) := by
+  simp [Raw.keys, foldRev_cons_key, keys_eq_map]
 
 end Raw
 

src/Std/Data/DHashMap/Lemmas.lean

@@ -963,6 +963,109 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+@[simp]
+theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
+    m.1.toList.map Sigma.fst = m.1.keys  :=
+  Raw₀.map_sigma_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.length = m.size :=
+  Raw₀.length_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  Raw₀.isEmpty_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    ⟨k, v⟩ ∈ m.toList ↔ m.get? k = some v :=
+  Raw₀.mem_toList_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_some_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β k} :
+    m.toList.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v :=
+  Raw₀.find?_toList_eq_some_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    m.toList.find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  apply Raw₀.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
+  Raw₀.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+namespace Const
+
+variable {β : Type v} {m : DHashMap α (fun _ => β)}
+
+@[simp]
+theorem map_prod_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
+    (toList m).map Prod.fst = m.keys :=
+  Raw₀.Const.map_prod_fst_toList_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
+
+@[simp]
+theorem length_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).length = m.size :=
+  Raw₀.Const.length_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).isEmpty = m.isEmpty :=
+  Raw₀.Const.isEmpty_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem mem_toList_iff_get?_eq_some [LawfulBEq α]
+    {k : α} {v : β} :
+    (k, v) ∈ toList m ↔ get? m k = some v :=
+  Raw₀.Const.mem_toList_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem mem_toList_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    (k, v) ∈ toList m ↔ m.getKey? k = some k ∧ get? m k = some v :=
+  Raw₀.Const.mem_toList_iff_getKey?_eq_some_and_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem get?_eq_some_iff_exists_beq_and_mem_toList [EquivBEq α] [LawfulHashable α]
+    {k : α} {v : β} :
+    get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ toList m :=
+  Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    [EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
+    (toList m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
+      m.getKey? k = some k' ∧ get? m k = some v :=
+  Raw₀.Const.find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some
+    ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem find?_toList_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    (toList m).find? (·.1 == k) = none ↔ m.contains k = false :=
+  Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem find?_toList_eq_none_iff_not_mem [EquivBEq α] [LawfulHashable α]
+    {k : α} :
+    (toList m).find? (·.1 == k) = none ↔ ¬ k ∈ m := by
+  simp only [Bool.not_eq_true, mem_iff_contains]
+  apply Raw₀.Const.find?_toList_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
+    (toList m).Pairwise (fun a b => (a.1 == b.1) = false) :=
+  Raw₀.Const.distinct_keys_toList ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+end Const
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m :=

src/Std/Data/DHashMap/Raw.lean

@@ -399,18 +399,10 @@ instance : ForM m (Raw α β) ((a : α) × β a) where
 instance : ForIn m (Raw α β) ((a : α) × β a) where
   forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init
 
-/-- Transforms the hash map into a list of mappings in some order. -/
-@[inline] def toList (m : Raw α β) : List ((a : α) × β a) :=
-  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
-
 /-- Transforms the hash map into an array of mappings in some order. -/
 @[inline] def toArray (m : Raw α β) : Array ((a : α) × β a) :=
   m.fold (fun acc k v => acc.push ⟨k, v⟩) #[]
 
-@[inline, inherit_doc Raw.toList] def Const.toList {β : Type v} (m : Raw α (fun _ => β)) :
-    List (α × β) :=
-  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
-
 @[inline, inherit_doc Raw.toArray] def Const.toArray {β : Type v} (m : Raw α (fun _ => β)) :
     Array (α × β) :=
   m.fold (fun acc k v => acc.push ⟨k, v⟩) #[]
@@ -483,11 +475,19 @@ implementation detail.
 def Internal.numBuckets (m : Raw α β) : Nat :=
   m.buckets.size
 
+end Unverified
+
+/-- Transforms the hash map into a list of mappings in some order. -/
+@[inline] def toList (m : Raw α β) : List ((a : α) × β a) :=
+  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
+
+@[inline, inherit_doc Raw.toList] def Const.toList {β : Type v} (m : Raw α (fun _ => β)) :
+    List (α × β) :=
+  m.foldRev (fun acc k v => ⟨k, v⟩ :: acc) []
+
 instance [Repr α] [(a : α) → Repr (β a)] : Repr (Raw α β) where
   reprPrec m prec := Repr.addAppParen ("Std.DHashMap.Raw.ofList " ++ reprArg m.toList) prec
 
-end Unverified
-
 /-- Returns a list of all keys present in the hash map in some order. -/
 @[inline] def keys (m : Raw α β) : List α :=
   m.foldRev (fun acc k _ => k :: acc) []