feat: verify toList for hash maps

src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean

@@ -248,4 +248,57 @@ theorem foldr_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a
       (l.toList.map (fun p => f p.1 p.2)) ++ acc := by
   induction l generalizing acc <;> simp_all [AssocList.foldr, AssocList.foldrM, Id.run]
 
+theorem foldr_foldr_cons_eq_flatMap_toList {l: List (AssocList α β)}:
+    List.foldr (fun x y => AssocList.foldr (fun a b d => ⟨a, b⟩ :: d) y x) [] l
+    = List.flatMap AssocList.toList l := by
+  suffices ∀ (l : List (AssocList α β)) (l' : List ((a : α) ×  β a)),
+    List.foldr (fun x y => AssocList.foldr (fun a b d => ⟨a, b⟩ :: d) y x) l' l
+    = (List.flatMap AssocList.toList l) ++ l'
+  by
+    rw [← List.append_nil (List.flatMap AssocList.toList l)]
+    apply this
+  intro l
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    intro l'
+    simp only [List.foldr_cons, ih, List.flatMap_cons, List.append_assoc]
+    suffices ∀ {l : AssocList α β} {l' : List ((a : α) × β a)},
+      AssocList.foldr (fun a b d => ⟨a, b⟩ :: d) l' l = l.toList ++ l' from this
+    intro l
+    induction l with
+    | nil => simp [AssocList.foldr, AssocList.foldrM, Id.run]
+    | cons hda hdb tl ih =>
+      intro l'
+      simp only [foldr, Id.run, foldrM, Id.bind_eq, toList_cons, List.cons_append, List.cons.injEq,
+        true_and]
+      apply ih
+
+theorem foldr_foldr_eq_sigma_fst_flatMap_toList {l: List (AssocList α β)}:
+    List.foldr (fun x y => AssocList.foldr (fun a _ d => a :: d) y x) [] l
+    = List.map Sigma.fst (List.flatMap AssocList.toList l) := by
+  suffices ∀ (l: List (AssocList α β)) (l': List ((a : α) ×  β a)),
+    (List.foldr (fun x y => AssocList.foldr (fun a b d => a :: d) y x) (l'.map Sigma.fst) l)
+    = (List.foldr (fun x y => AssocList.foldr (fun a b d => ⟨a, b⟩ :: d) y x) l' l).map Sigma.fst
+  by
+    specialize this l []
+    simp only [List.map_nil] at this
+    rw [this, foldr_foldr_cons_eq_flatMap_toList]
+  intro l
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    intro l'
+    simp [ih]
+    suffices ∀ {l : AssocList α β} {l' : List ((a : α) × β a)},
+      AssocList.foldr (fun a b d => a :: d) (l'.map Sigma.fst) l
+      = List.map Sigma.fst (foldr (fun a b d => ⟨a, b⟩ :: d) l' l) from this
+    intro l
+    induction l with
+    | nil => simp [AssocList.foldr, AssocList.foldrM, Id.run]
+    | cons hda hdb tl ih =>
+      intro l'
+      simp only [foldr, Id.run, foldrM, Id.bind_eq, List.map_cons, List.cons.injEq, true_and]
+      apply ih
+
 end Std.DHashMap.Internal.AssocList

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -1942,6 +1942,49 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a
     · rw [cond_false, cond_false, ih, List.cons_append]
     · rw [cond_true, cond_true]
 
+theorem mem_iff_getValueCast?_eq_some [BEq α] [LawfulBEq α] {k : α} {v : β k}
+    {l : List ((a : α) × β a)} (h : DistinctKeys l):
+    ⟨k, v⟩ ∈ l ↔ getValueCast? k l = some v := by
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    simp only [List.mem_cons]
+    by_cases kv_hd: ⟨k, v⟩ = hd
+    · rw [← kv_hd]
+      simp
+    · simp only [kv_hd, false_or]
+      rw [distinctKeys_cons_iff] at h
+      by_cases k_hdfst: k == hd.fst
+      · simp only [beq_iff_eq] at k_hdfst
+        have : ∃ (v' : β k), ⟨k, v'⟩ = hd := by
+          exists cast (by congr;symm;exact k_hdfst) hd.snd
+          refine Sigma.ext k_hdfst ?_
+          simp
+        rcases this with ⟨v', h'⟩
+        rw [← h']
+        simp only [getValueCast?_cons_self, Option.some.injEq]
+        have h₁ : ¬ ⟨k,v⟩ ∈ tl := by
+          rw [containsKey_eq_false_iff] at h
+          false_or_by_contra
+          rename_i p
+          rcases h with ⟨_, h⟩
+          specialize h ⟨k, v⟩ p
+          simp [k_hdfst] at h
+        have h₂ : ¬ v' = v := by
+          false_or_by_contra
+          rename_i p
+          rw [← p, h'] at kv_hd
+          contradiction
+        simp [h₁, h₂]
+      · simp only [getValueCast?, beq_iff_eq]
+        split
+        · rename_i h
+          simp only [beq_iff_eq] at k_hdfst
+          simp only [beq_iff_eq] at h
+          rw [h] at k_hdfst
+          simp at k_hdfst
+        · apply ih (And.left h)
+
 /-- Internal implementation detail of the hash map -/
 def insertList [BEq α] (l toInsert : List ((a : α) × β a)) : List ((a : α) × β a) :=
   match toInsert with

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

@@ -88,9 +88,7 @@ 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]
 
 private def modifyMap : Std.DHashMap Name (fun _ => Name) :=
   .ofList
@@ -829,6 +827,10 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 
 end Const
 
+theorem keys_def [EquivBEq α] [LawfulHashable α] :
+    m.1.keys = m.1.toList.map Sigma.fst := by
+  simp_to_model using List.keys_eq_map
+
 @[simp]
 theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
     m.1.keys.length = m.1.size := by
@@ -847,13 +849,27 @@ 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 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
+
 @[simp]
 theorem insertMany_nil :
     m.insertMany [] = m := by

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

@@ -107,9 +107,20 @@ 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_eq_toListModel {m : Raw α β} : m.toList = toListModel m.buckets := by
+  simp only [Raw.toList, Raw.foldRev, Raw.foldRevM, Array.id_run_foldrM, ← Array.foldr_toList,
+    toListModel]
+  apply AssocList.foldr_foldr_cons_eq_flatMap_toList
+
 theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) := by
   simp [Raw.toList, foldRev_cons]
 
+theorem keys_eq_keys_toListModel {m : Raw α β }:
+    m.keys = List.keys (toListModel m.buckets) := by
+  simp only [Raw.keys, Raw.foldRev, Raw.foldRevM, Array.id_run_foldrM, ← Array.foldr_toList,
+    toListModel, keys_eq_map]
+  apply AssocList.foldr_foldr_eq_sigma_fst_flatMap_toList
+
 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]