feat: HashMap.toList_insert_perm_of_not_mem

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

@@ -37,6 +37,17 @@ theorem foldl_eq {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocLis
     l.foldl f init = l.toList.foldl (fun d p => f d p.1 p.2) init := by
   induction l generalizing init <;> simp_all [foldl, Id.run, foldlM]
 
+theorem foldlM_id {f : δ → (a : α) → β a → δ} {init : δ} {l : AssocList α β} :
+    l.foldlM (m := Id) f init = l.foldl f init := rfl
+
+@[simp]
+theorem foldr_eq {f : (a : α) → β a → δ → δ} {init : δ} {l : AssocList α β} :
+    l.foldr f init = l.toList.foldr (fun p d => f p.1 p.2 d) init := by
+  induction l generalizing init <;> simp_all [foldr, Id.run, foldrM]
+
+theorem foldrM_id {f : (a : α) → β a → δ → δ} {init : δ} {l : AssocList α β} :
+    l.foldrM (m := Id) f init = l.foldr f init := rfl
+
 @[simp]
 theorem length_eq {l : AssocList α β} : l.length = l.toList.length := by
   rw [length, foldl_eq]

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

@@ -158,6 +158,10 @@ namespace DHashMap.Internal
 def toListModel (buckets : Array (AssocList α β)) : List ((a : α) × β a) :=
   buckets.toList.flatMap AssocList.toList
 
+/-- Internal implementation detail of the hash map -/
+def Const.toListModel {β} (buckets : Array (AssocList α (fun _ => β))) : List (α × β) :=
+  (Internal.toListModel buckets).map fun ⟨a, b⟩ => (a, b)
+
 /-- Internal implementation detail of the hash map -/
 @[inline] def computeSize (buckets : Array (AssocList α β)) : Nat :=
   buckets.foldl (fun d b => d + b.length) 0

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

@@ -39,4 +39,7 @@ def values {β : Type v} : List ((_ : α) × β) → List β
   | [] => []
   | ⟨_, v⟩ :: l => v :: values l
 
+theorem keys_eq_map_fst {l : List ((a : α) × β a)} : keys l = l.map Sigma.fst := by
+    induction l <;> simp_all [keys]
+
 end Std.DHashMap.Internal.List

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

@@ -85,6 +85,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.keys_eq_keys_toListModel, ``Raw.toList_eq_toListModel,
     ``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]
@@ -821,7 +822,7 @@ theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
 
 @[simp]
 theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
-    m.1.keys.isEmpty = m.1.isEmpty:= by
+    m.1.keys.isEmpty = m.1.isEmpty := by
   simp_to_model using List.isEmpty_keys_eq_isEmpty
 
 @[simp]
@@ -832,13 +833,28 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
 @[simp]
 theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     k ∈ m.1.keys ↔ m.contains k := by
-  simp_to_model 
-  rw [List.containsKey_eq_keys_contains]
+  simp_to_model
+  rw [List.containsKey_eq_keys_contains, List.elem_iff]
 
 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
 
+@[simp]
+theorem toList_map_fst {α β} (m : Raw₀ α β) :
+    m.1.toList.map Sigma.fst = m.1.keys := by
+  simp_to_model
+  simp [List.keys_eq_map_fst]
+
+open _root_.List in
+theorem toList_insert_perm_of_not_contains [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
+    (k : α) (v : β k) (h' : m.contains k = false) :
+    (m.insert k v).1.toList ~ ⟨k, v⟩ :: m.1.toList := by
+  revert h'
+  simp_to_model
+  intro h'
+  exact Perm.trans (toListModel_insert (Raw.WF.out h)) (by simp [insertEntry, h'])
+
 end Raw₀
 
 end Std.DHashMap.Internal

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

@@ -107,12 +107,19 @@ 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_eq_keys_toListModel {m : Raw α β} :
+    m.keys = List.keys (toListModel m.buckets) := by
+  simp [Raw.keys, foldRev_cons_key]
+
+theorem toList_perm_toListModel {m : Raw α β} : Perm m.toList (toListModel m.buckets) :=
+  Perm.of_eq toList_eq_toListModel
+
 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]
+    Perm m.keys (List.keys (toListModel m.buckets)) :=
+  Perm.of_eq keys_eq_keys_toListModel
 
 theorem length_keys_eq_length_keys {m : Raw α β} :
     m.keys.length = (List.keys (toListModel m.buckets)).length :=
@@ -135,6 +142,15 @@ theorem pairwise_keys_iff_pairwise_keys [BEq α] [PartialEquivBEq α] {m : Raw 
       (List.keys (toListModel m.buckets)).Pairwise (fun a b => (a == b) = false) :=
   keys_perm_keys_toListModel.pairwise_iff BEq.symm_false
 
+theorem Const.toList_eq_toListModel {β} {m : Raw α (fun _ => β)} :
+    Raw.Const.toList m = Const.toListModel m.buckets := by
+  simp only [Raw.Const.toList, Const.toListModel, ← Raw.toList_eq_toListModel, Raw.toList,
+    Raw.foldRev, Raw.foldRevM, Array.id_run_foldrM, AssocList.foldrM_id]
+  rw [← Array.foldr_hom (List.map _) _ (g₂ := fun l acc => foldr (fun p d => (p.fst, p.snd) :: d) acc l.toList)]
+  · simp
+  · intro l acc
+    induction l <;> simp_all
+
 end Raw
 
 namespace Raw₀

src/Std/Data/DHashMap/Lemmas.lean

@@ -960,12 +960,24 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
 
 @[simp]
 theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
-    k ∈ m.keys ↔ k ∈ m := by 
+    k ∈ m.keys ↔ k ∈ m := by
   rw [mem_iff_contains]
   exact Raw₀.mem_keys ⟨m.1, _⟩ m.2
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
-    m.keys.Pairwise (fun a b => (a == b) = false) := 
+    m.keys.Pairwise (fun a b => (a == b) = false) :=
   Raw₀.distinct_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
+@[simp]
+theorem toList_map_fst :
+    m.toList.map Sigma.fst = m.keys :=
+  Raw₀.toList_map_fst ⟨m.1, m.2.size_buckets_pos⟩
+
+open List in
+theorem toList_insert_perm_of_not_mem [EquivBEq α] [LawfulHashable α]
+    (k : α) (v : β k) (h' : ¬k ∈ m) :
+    (m.insert k v).toList ~ (⟨k, v⟩ :: m.toList) :=
+  Raw₀.toList_insert_perm_of_not_contains ⟨m.1, m.2.size_buckets_pos⟩ m.2 k v
+    (eq_false_of_ne_true h')
+
 end Std.DHashMap

src/Std/Data/DHashMap/RawLemmas.lean

@@ -1039,14 +1039,28 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
 
 @[simp]
 theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
-    k ∈ m.keys ↔ k ∈ m := by 
+    k ∈ m.keys ↔ k ∈ m := by
   rw [mem_iff_contains]
   simp_to_raw using Raw₀.mem_keys ⟨m, _⟩ h
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := by
   simp_to_raw using Raw₀.distinct_keys ⟨m, h.size_buckets_pos⟩ h
 
+@[simp]
+theorem toList_map_fst (h : m.WF) :
+    m.toList.map Sigma.fst = m.keys := by
+  simp_to_raw using Raw₀.toList_map_fst ⟨m, h.size_buckets_pos⟩
+
+open List in
+theorem toList_insert_perm_of_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    (k : α) (v : β k) (h' : ¬k ∈ m) :
+    (m.insert k v).toList ~ (⟨k, v⟩ :: m.toList) := by
+  rw [mem_iff_contains, Bool.not_eq_true] at h'
+  revert h'
+  simp_to_raw
+  apply Raw₀.toList_insert_perm_of_not_contains _ h
+
 end Raw
 
 end Std.DHashMap

src/Std/Data/HashMap/Lemmas.lean

@@ -701,6 +701,30 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.distinct_keys
 
+@[simp]
+theorem toList_inner :
+    m.inner.toList = m.toList.map fun ⟨k, v⟩ => ⟨k, v⟩ := by
+  simp [DHashMap.toList, toList, DHashMap.Const.toList,
+    DHashMap.Internal.Raw.toList_eq_toListModel, DHashMap.Internal.Raw.Const.toList_eq_toListModel,
+    DHashMap.Internal.Const.toListModel, Function.comp_def]
+
+@[simp]
+theorem toList_map_fst :
+    m.toList.map Prod.fst = m.keys := by
+  simpa using DHashMap.toList_map_fst (m := m.1)
+
+@[simp] theorem insert_inner [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    m.inner.insert k v = (m.insert k v).inner := rfl
+
+open List in
+theorem toList_insert_perm_of_not_mem [EquivBEq α] [LawfulHashable α]
+    (k : α) (v : β) (h' : ¬k ∈ m) :
+    (m.insert k v).toList ~ (k, v) :: m.toList := by
+  have t := DHashMap.toList_insert_perm_of_not_mem (β := fun _ => β) k v h'
+  simp at t
+  replace t := Perm.map (fun x : (_ : α) × β => (x.fst, x.snd)) t
+  simpa [Function.comp_def] using t
+
 end
 
 end Std.HashMap

src/Std/Data/HashMap/RawLemmas.lean

@@ -699,13 +699,37 @@ theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
 
 @[simp]
 theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
-    k ∈ m.keys ↔ k ∈ m := 
+    k ∈ m.keys ↔ k ∈ m :=
   DHashMap.Raw.mem_keys h.out
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
-    m.keys.Pairwise (fun a b => (a == b) = false) := 
+    m.keys.Pairwise (fun a b => (a == b) = false) :=
   DHashMap.Raw.distinct_keys h.out
 
+@[simp]
+theorem toList_inner {α β} (m : Raw α β) :
+    m.inner.toList = m.toList.map fun ⟨k, v⟩ => ⟨k, v⟩ := by
+  simp [toList,
+    DHashMap.Internal.Raw.toList_eq_toListModel, DHashMap.Internal.Raw.Const.toList_eq_toListModel,
+    DHashMap.Internal.Const.toListModel, Function.comp_def]
+
+@[simp]
+theorem toList_map_fst (h : m.WF) :
+    m.toList.map Prod.fst = m.keys := by
+  simpa using DHashMap.Raw.toList_map_fst (m := m.inner) h.out
+
+@[simp] theorem insert_inner [EquivBEq α] [LawfulHashable α] {k : α} {v : β} :
+    m.inner.insert k v = (m.insert k v).inner := rfl
+
+open List in
+theorem toList_insert_perm_of_not_mem [EquivBEq α] [LawfulHashable α] (h : m.WF)
+    (k : α) (v : β) (h' : ¬k ∈ m) :
+    (m.insert k v).toList ~ ((k, v) :: m.toList) := by
+  have t := DHashMap.Raw.toList_insert_perm_of_not_mem h.out k v h'
+  simp only [insert_inner, toList_inner] at t
+  replace t := Perm.map (fun x : (_ : α) × β => (x.fst, x.snd)) t
+  simpa [Function.comp_def] using t
+
 end Raw
 
 end Std.HashMap