feat: verify toList for hash maps

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

@@ -248,4 +248,86 @@ 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
+
+theorem foldr_foldr_toProd_eq_map_toProd_flatMap_toList
+    {β : Type v} {l : List (AssocList α (fun _ => β))} :
+    List.foldr (fun x y => AssocList.foldr (fun a b d => (a, b) :: d) y x) [] l =
+    List.map (fun x => (x.fst, x.snd)) (List.flatMap AssocList.toList l) := by
+  suffices ∀ (l : List (AssocList α (fun _ => β))) (l' : List (α × β)),
+    List.foldr (fun x y => AssocList.foldr (fun a b d => (a, b) :: d) y x) l' l =
+    List.map (fun x => (x.fst, x.snd)) (List.flatMap AssocList.toList l) ++ l' by
+    specialize this l []
+    simp only [List.append_nil] at this
+    exact this
+  intro l
+  induction l with
+  | nil => simp
+  | cons hd tl ih =>
+    intro l'
+    simp only [List.foldr_cons, List.flatMap_cons, List.map_append, List.append_assoc]
+    rw [ih]
+    suffices ∀ {l : AssocList α (fun _ => β)} {l' : List (α × β)},
+      foldr (fun a b d => (a, b) :: d) l' l = List.map (fun x => (x.fst, x.snd)) l.toList ++ l' by
+      apply this
+    intro l
+    induction l with
+    | nil => simp [foldr, foldrM, Id.run]
+    | cons hda hdb tl ih =>
+      intro l'
+      simp only [foldr, Id.run, foldrM, Id.bind_eq, toList_cons, List.map_cons, List.cons_append,
+        List.cons.injEq, true_and]
+      apply ih
+
 end Std.DHashMap.Internal.AssocList