max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: verify toArray for hash maps (#9685)

Browse source 
This PR verifies `toArray` and related functions for hashmaps.
This commit is contained in:
Johannes Tantow 2025-08-18 11:39:44 +02:00 • committed by GitHub
parent 2e6c1a74e5
commit 19301f83eb
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
16 changed files with 1081 additions and 43 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Init/Data/Array/Lemmas.lean
View file

@ -838,9 +838,10 @@ theorem mem_of_contains_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α}
cases as
simp
theorem contains_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : as.contains a = true := by
theorem contains_eq_true_of_mem [BEq α] [ReflBEq α] {a : α} {as : Array α} (h : a ∈ as) :
as.contains a = true := by
cases as
simpa using h
simpa using List.elem_eq_true_of_mem (Array.mem_toList_iff.mpr h)
@[simp] theorem elem_eq_contains [BEq α] {a : α} {xs : Array α} :
elem a xs = xs.contains a := by

24
src/Std/Data/DHashMap/Basic.lean
View file

@ -298,6 +298,18 @@ This function ensures that the value is used linearly.
⟨(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).1,
(Raw₀.Const.insertManyIfNewUnit ⟨m.1, m.2.size_buckets_pos⟩ l).2 _ Raw.WF.insertIfNew₀ m.2⟩
@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
Array ((a : α) × β a) :=
m.1.toArray
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
(m : DHashMap α (fun _ => β)) : Array (α × β) :=
Raw.Const.toArray m.1
@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
Array α :=
m.1.keysArray
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
@ -311,18 +323,6 @@ section Unverified
else
(l, r.insert a b)
@[inline, inherit_doc Raw.toArray] def toArray (m : DHashMap α β) :
Array ((a : α) × β a) :=
m.1.toArray
@[inline, inherit_doc Raw.Const.toArray] def Const.toArray {β : Type v}
(m : DHashMap α (fun _ => β)) : Array (α × β) :=
Raw.Const.toArray m.1
@[inline, inherit_doc Raw.keysArray] def keysArray (m : DHashMap α β) :
Array α :=
m.1.keysArray
@[inline, inherit_doc Raw.values] def values {β : Type v}
(m : DHashMap α (fun _ => β)) : List β :=
m.1.values

9
src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean
View file

@ -271,4 +271,13 @@ 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]
theorem foldl_push_apply {l : AssocList α β} {acc : Array δ} (f : (a : α) → β a → δ) :
l.foldl (fun acc k v => acc.push (f k v)) acc =
acc ++ (l.toList.toArray.map (fun p => f p.1 p.2)) := by
simp [foldl]
induction l generalizing acc with
| nil => simp [foldlM]
| cons k v tl ih =>
simp [foldlM, ih]
end Std.DHashMap.Internal.AssocList

227
src/Std/Data/DHashMap/Internal/RawLemmas.lean
View file

@ -163,6 +163,9 @@ private def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (TSynta
⟨`foldRev, (``Raw.foldRev_eq_foldr_toListModel, #[])⟩,
⟨`forIn, (``Raw.forIn_eq_forIn_toListModel, #[])⟩,
⟨`forM, (``Raw.forM_eq_forM_toListModel, #[])⟩,
⟨`toArray, (``Raw.toArray_eq_toArray_toListModel, #[])⟩,
⟨`keysArray, (``Raw.keysArray_eq_toArray_keys_toListModel, #[])⟩,
⟨`Const.toArray, (``Raw.Const.toArray_eq_toArray_map_toListModel, #[])⟩,
⟨`Equiv, (``Raw.equiv_iff_toListModel_perm,
#[`(_root_.List.Perm.congr_left), `(_root_.List.Perm.congr_right)])⟩]
@ -1108,6 +1111,137 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
end Const
omit [Hashable α] [BEq α] in
theorem toArray_keys_eq_keysArray :
m.1.keys.toArray = m.1.keysArray := by
simp_to_model
omit [Hashable α] [BEq α] in
theorem toList_keysArray_eq_keys :
m.1.keysArray.toList = m.1.keys := by
simp_to_model
@[simp]
theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
m.1.keysArray.size = m.1.size := by
simp [← toArray_keys_eq_keysArray, h]
@[simp]
theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
m.1.keysArray.isEmpty = m.1.isEmpty := by
simp [← toArray_keys_eq_keysArray, h]
@[simp]
theorem contains_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
m.1.keysArray.contains k = m.contains k := by
simp [← toArray_keys_eq_keysArray, h]
@[simp]
theorem mem_keysArray [LawfulBEq α] (h : m.1.WF) {k : α} :
k ∈ m.1.keysArray ↔ m.contains k := by
simp [← toArray_keys_eq_keysArray, h]
theorem forall_mem_keysArray_iff_forall_contains_getKey [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {p : α → Prop} :
(∀ k ∈ m.1.keysArray, p k) ↔ ∀ (k : α) (h : m.contains k), p (m.getKey k h) := by
simp [← toArray_keys_eq_keysArray, h, forall_mem_keys_iff_forall_contains_getKey]
theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α}
(h' : k ∈ m.1.keysArray) : m.contains k :=
(contains_keysArray m h).symm.trans (Array.contains_eq_true_of_mem h')
omit [Hashable α] [BEq α] in
theorem toArray_toList_eq_toArray :
m.1.toList.toArray = m.1.toArray := by
simp_to_model
omit [Hashable α] [BEq α] in
theorem toList_toArray_eq_toList :
m.1.toArray.toList = m.1.toList := by
simp_to_model
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
m.1.toArray.map Sigma.fst = m.1.keysArray := by
simp [← toArray_keys_eq_keysArray, ← toArray_toList_eq_toArray, map_fst_toList_eq_keys]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
m.1.toArray.size = m.1.size := by
simp [← toArray_toList_eq_toArray, length_toList, h]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
m.1.toArray.isEmpty = m.1.isEmpty := by
simp [← toArray_toList_eq_toArray, isEmpty_toList, h]
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
{k : α} {v : β k} :
⟨k, v⟩ ∈ m.1.toArray ↔ m.get? k = some v := by
simp [← toArray_toList_eq_toArray, mem_toList_iff_get?_eq_some, h]
theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
(h : m.1.WF) {k : α} {v : β k} :
m.1.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
simp [← toArray_toList_eq_toArray, find?_toList_eq_some_iff_get?_eq_some, h]
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {k : α} :
m.1.toArray.find? (·.1 == k) = none ↔ m.contains k = false := by
-- does not work if removing the only because it rewrites it away
simp only [← toArray_toList_eq_toArray, List.find?_toArray, find?_toList_eq_none_iff_contains_eq_false, h]
namespace Const
variable {β : Type v} (m : Raw₀ α (fun _ => β))
omit [Hashable α] [BEq α] in
theorem toArray_toList_eq_toArray :
(Raw.Const.toList m.1).toArray = Raw.Const.toArray m.1 := by
simp_to_model
omit [Hashable α] [BEq α] in
theorem toList_toArray_eq_toList :
(Raw.Const.toArray m.1).toList = Raw.Const.toList m.1 := by
simp_to_model
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
(Raw.Const.toArray m.1).map Prod.fst = m.1.keysArray := by
simp [← toArray_toList_eq_toArray, List.map_toArray, ← toArray_keys_eq_keysArray, map_fst_toList_eq_keys]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
(Raw.Const.toArray m.1).size = m.1.size := by
simp [← toArray_toList_eq_toArray, length_toList, h]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
(Raw.Const.toArray m.1).isEmpty = m.1.isEmpty := by
simp [← toArray_toList_eq_toArray, isEmpty_toList, h]
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α] (h : m.1.WF)
{k : α} {v : β} :
(k, v) ∈ Raw.Const.toArray m.1 ↔ get? m k = some v := by
simp [← toArray_toList_eq_toArray, mem_toList_iff_get?_eq_some, h]
theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
{k : α} {v : β} :
get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toArray m.1 := by
simp [← toArray_toList_eq_toArray, get?_eq_some_iff_exists_beq_and_mem_toList, h]
theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
[EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k k' : α} {v : β} :
(Raw.Const.toArray m.1).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
m.getKey? k = some k' ∧ get? m k = some v := by
simp [← toArray_toList_eq_toArray, List.find?_toArray, find?_toList_eq_some_iff_getKey?_eq_some_and_get?_eq_some, h]
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {k : α} :
(Raw.Const.toArray m.1).find? (·.1 == k) = none ↔ m.contains k = false := by
simp only [← toArray_toList_eq_toArray, List.find?_toArray, h, find?_toList_eq_none_iff_contains_eq_false]
theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
(h : m.1.WF) {k: α} {v : β} :
(k, v) ∈ (Raw.Const.toArray m.1) ↔ m.getKey? k = some k ∧ get? m k = some v := by
simp [← toArray_toList_eq_toArray, h, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
end Const
section monadic
-- The types are redefined because fold/for does not need BEq/Hashable
@ -1203,6 +1337,99 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
end Const
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → (a : α) → β a → m' δ} {init : δ} :
m.1.foldM f init = m.1.toArray.foldlM (fun a b => f a b.1 b.2) init := by
simp [← toArray_toList_eq_toArray, foldM_eq_foldlM_toList]
theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
m.1.fold f init = m.1.toArray.foldl (fun a b => f a b.1 b.2) init := by
simp [← toArray_toList_eq_toArray, fold_eq_foldl_toList]
theorem foldRevM_eq_foldrM_toArray [Monad m'] [LawfulMonad m']
{f : δ → (a : α) → β a → m' δ} {init : δ} :
Raw.Internal.foldRevM f init m.1 = m.1.toArray.foldrM (fun a b => f b a.1 a.2) init := by
simp [← toArray_toList_eq_toArray, foldRevM_eq_foldrM_toList]
theorem foldRev_eq_foldr_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
Raw.Internal.foldRev f init m.1 = m.1.toArray.foldr (fun a b => f b a.1 a.2) init := by
simp [← toArray_toList_eq_toArray, foldRev_eq_foldr_toList]
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
m.1.forM f = m.1.toArray.forM (fun a => f a.1 a.2) := by
rw [← toArray_toList_eq_toArray, List.forM_toArray', forM_eq_forM_toList]
rfl
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
m.1.forIn f init = ForIn.forIn m.1.toArray init (fun a b => f a.1 a.2 b) := by
simp [← toArray_toList_eq_toArray, forIn_eq_forIn_toList]
theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} :
m.1.foldM (fun d a _ => f d a) init = m.1.keysArray.foldlM f init := by
simp [← toArray_keys_eq_keysArray, foldM_eq_foldlM_keys]
theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
m.1.fold (fun d a _ => f d a) init = m.1.keysArray.foldl f init := by
simp [← toArray_keys_eq_keysArray, fold_eq_foldl_keys]
theorem foldRevM_eq_foldrM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → (a : α) → m' δ} {init : δ} :
Raw.Internal.foldRevM (fun d a _ => f d a) init m.1 =
m.1.keysArray.foldrM (fun a b => f b a) init := by
simp [← toArray_keys_eq_keysArray, foldRevM_eq_foldrM_keys]
theorem foldRev_eq_foldr_keysArray {f : δ → (a : α) → δ} {init : δ} :
Raw.Internal.foldRev (fun d a _ => f d a) init m.1 =
m.1.keysArray.foldr (fun a b => f b a) init := by
simp [← toArray_keys_eq_keysArray, foldRev_eq_foldr_keys]
theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
m.1.forM (fun a _ => f a) = m.1.keysArray.forM f := by
rw [← toArray_keys_eq_keysArray, List.forM_toArray', forM_eq_forM_keys]
rfl
theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} :
m.1.forIn (fun a _ d => f a d) init = ForIn.forIn m.1.keysArray init f := by
simp [← toArray_keys_eq_keysArray, forIn_eq_forIn_keys]
namespace Const
variable {β : Type v} (m : Raw₀ α (fun _ => β))
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} :
m.1.foldM f init = (Raw.Const.toArray m.1).foldlM (fun a b => f a b.1 b.2) init := by
simp [← toArray_toList_eq_toArray, foldM_eq_foldlM_toList]
theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
m.1.fold f init = (Raw.Const.toArray m.1).foldl (fun a b => f a b.1 b.2) init := by
simp [← toArray_toList_eq_toArray, fold_eq_foldl_toList]
theorem foldRevM_eq_foldrM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} :
Raw.Internal.foldRevM f init m.1 =
(Raw.Const.toArray m.1).foldrM (fun a b => f b a.1 a.2) init := by
simp [← toArray_toList_eq_toArray, foldRevM_eq_foldrM_toList]
theorem foldRev_eq_foldr_toArray {f : δ → α → β → δ} {init : δ} :
Raw.Internal.foldRev f init m.1 = (Raw.Const.toArray m.1).foldr (fun a b => f b a.1 a.2) init := by
simp [← toArray_toList_eq_toArray, foldRev_eq_foldr_toList]
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
m.1.forM f = (Raw.Const.toArray m.1).forM (fun a => f a.1 a.2) := by
rw [← toArray_toList_eq_toArray, List.forM_toArray', forM_eq_forM_toList]
rfl
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)} {init : δ} :
m.1.forIn f init = ForIn.forIn (Raw.Const.toArray m.1) init (fun a b => f a.1 a.2 b) := by
simp [← toArray_toList_eq_toArray, forIn_eq_forIn_toList]
end Const
end monadic
section insertMany

37
src/Std/Data/DHashMap/Internal/WF.lean
View file

@ -112,6 +112,16 @@ theorem foldRev_cons_apply {l : Raw α β} {acc : List γ} (f : (a : α) → β
rw [foldr_cons, ih, AssocList.foldr_apply]
simp
theorem fold_push_apply {l : Raw α β} {acc : Array γ} (f : (a : α) → β a → γ) :
Raw.fold (fun acc k v => acc.push (f k v)) acc l =
acc ++ ((toListModel l.buckets).toArray.map (fun p => f p.1 p.2)) := by
rw [fold_eq, ← Array.foldl_toList, toListModel]
induction l.buckets.toList generalizing acc with
| nil => simp
| cons x xs ih =>
rw [foldl_cons, ih, AssocList.foldl_push_apply]
simp
theorem foldRev_cons {l : Raw α β} {acc : List ((a : α) × β a)} :
Raw.Internal.foldRev (fun acc k v => ⟨k, v⟩ :: acc) acc l = toListModel l.buckets ++ acc := by
simp [foldRev_cons_apply]
@ -126,6 +136,20 @@ theorem foldRev_cons_key {l : Raw α β} {acc : List α} :
List.keys (toListModel l.buckets) ++ acc := by
rw [foldRev_cons_apply, keys_eq_map]
theorem fold_push {l : Raw α β} {acc : Array ((a : α) × β a)} :
Raw.fold (fun acc k v => acc.push ⟨k, v⟩) acc l = acc ++ (toListModel l.buckets).toArray := by
simp [fold_push_apply]
theorem fold_push_mk {β : Type v} {l : Raw α (fun _ => β)} {acc : Array (α × β)} :
Raw.fold (fun acc k v => acc.push (k, v)) acc l =
acc ++ ((toListModel l.buckets).map (fun ⟨k, v⟩ => (k, v))).toArray := by
simp [fold_push_apply]
theorem fold_push_key {l : Raw α β} {acc : Array α} :
Raw.fold (fun acc k _ => acc.push k) acc l =
acc ++ (List.keys (toListModel l.buckets)).toArray := by
simp [fold_push_apply, keys_eq_map]
theorem foldM_eq_foldlM_toListModel {δ : Type w} {m : Type w → Type w } [Monad m] [LawfulMonad m]
{f : δ → (a : α) → β a → m δ} {init : δ} {b : Raw α β} :
b.foldM f init = (toListModel b.buckets).foldlM (fun a b => f a b.1 b.2) init := by
@ -177,10 +201,21 @@ 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 keys_eq_keys_toListModel {m : Raw α β }:
theorem toArray_eq_toArray_toListModel {m : Raw α β} : m.toArray = (toListModel m.buckets).toArray := by
simp [Raw.toArray, fold_push]
theorem Const.toArray_eq_toArray_map_toListModel {β : Type v} {m : Raw α (fun _ => β)} :
Raw.Const.toArray m = ((toListModel m.buckets).map (fun ⟨k, v⟩ => (k,v))).toArray := by
simp [Raw.Const.toArray, fold_push_mk]
theorem keys_eq_keys_toListModel {m : Raw α β} :
m.keys = List.keys (toListModel m.buckets) := by
simp [Raw.keys, foldRev_cons_key, keys_eq_map]
theorem keysArray_eq_toArray_keys_toListModel {m : Raw α β} :
m.keysArray = (List.keys (toListModel m.buckets)).toArray := by
simp [Raw.keysArray, fold_push_key]
theorem forM_eq_forM_toListModel {l: Raw α β} {m : Type w → Type w} [Monad m] [LawfulMonad m]
{f : (a : α) → β a → m PUnit} :
l.forM f = (toListModel l.buckets).forM (fun a => f a.1 a.2) := by

197
src/Std/Data/DHashMap/Lemmas.lean
View file

@ -1166,6 +1166,46 @@ 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 toArray_keys :
m.keys.toArray = m.keysArray :=
Raw₀.toArray_keys_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem toList_keysArray :
m.keysArray.toList = m.keys :=
Raw₀.toList_keysArray_eq_keys ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem size_keysArray [EquivBEq α] [LawfulHashable α] :
m.keysArray.size = m.size :=
Raw₀.size_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
@[simp]
theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] :
m.keysArray.isEmpty = m.isEmpty :=
Raw₀.isEmpty_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
@[simp]
theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
{k : α} :
m.keysArray.contains k = m.contains k :=
Raw₀.contains_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
@[simp]
theorem mem_keysArray [LawfulBEq α] {k : α} :
k ∈ m.keysArray ↔ k ∈ m :=
Raw₀.mem_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
{p : α → Prop} :
(∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
Raw₀.forall_mem_keysArray_iff_forall_contains_getKey ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] {k : α}
(h' : k ∈ m.keysArray) : m.contains k :=
Raw₀.contains_of_mem_keysArray ⟨m.1, m.2.size_buckets_pos⟩ m.2 h'
@[simp, grind _=_]
theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.toList.map Sigma.fst = m.keys :=
@ -1279,6 +1319,103 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
end Const
@[simp]
theorem toArray_toList :
m.toList.toArray = m.toArray :=
Raw₀.toArray_toList_eq_toArray ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem toList_toArray :
m.toArray.toList = m.toList :=
Raw₀.toList_toArray_eq_toList ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
m.toArray.map Sigma.fst = m.keysArray :=
Raw₀.map_fst_toArray_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.size = m.size :=
Raw₀.size_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.isEmpty = m.isEmpty :=
Raw₀.isEmpty_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β k} :
⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v :=
Raw₀.mem_toArray_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β k} :
m.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v :=
Raw₀.find?_toArray_eq_some_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} :
m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
Raw₀.find?_toArray_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}
@[simp]
theorem toArray_toList :
(DHashMap.Const.toList m).toArray = DHashMap.Const.toArray m :=
Raw₀.Const.toArray_toList_eq_toArray ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem toList_toArray :
(DHashMap.Const.toArray m).toList = DHashMap.Const.toList m :=
Raw₀.Const.toList_toArray_eq_toList ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
(DHashMap.Const.toArray m).map Prod.fst = m.keysArray :=
Raw₀.Const.map_fst_toArray_eq_keysArray ⟨m.1, m.2.size_buckets_pos⟩
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] :
(DHashMap.Const.toArray m).size = m.size :=
Raw₀.Const.size_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
(DHashMap.Const.toArray m).isEmpty = m.isEmpty :=
Raw₀.Const.isEmpty_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β} :
(k, v) ∈ DHashMap.Const.toArray m ↔ get? m k = some v :=
Raw₀.Const.mem_toArray_iff_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
{k : α} {v : β} :
get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ DHashMap.Const.toArray m :=
Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
[EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
(DHashMap.Const.toArray m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
m.getKey? k = some k' ∧ get? m k = some v :=
Raw₀.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} :
(DHashMap.Const.toArray m).find? (·.1 == k) = none ↔ m.contains k = false :=
Raw₀.Const.find?_toArray_eq_none_iff_contains_eq_false ⟨m.1, m.2.size_buckets_pos⟩ m.2
theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
{k: α} {v : β} :
(k, v) ∈ DHashMap.Const.toArray m ↔ m.getKey? k = some k ∧ get? m k = some v := by
simp [← toArray_toList, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
end Const
section monadic
variable {m : DHashMap α β} {δ : Type w} {m' : Type w → Type w}
@ -1399,6 +1536,66 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
end Const
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → (a : α) → β a → m' δ} {init : δ} :
m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
Raw₀.foldM_eq_foldlM_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} :
m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
Raw₀.fold_eq_foldl_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} :
m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
Raw₀.forM_eq_forM_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} :
m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
Raw₀.forIn_eq_forIn_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} :
m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
Raw₀.foldM_eq_foldlM_keysArray ⟨m.1, m.2.size_buckets_pos⟩
theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
Raw₀.fold_eq_foldl_keysArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
m.forM (fun a _ => f a) = m.keysArray.forM f :=
Raw₀.forM_eq_forM_keysArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} :
m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
Raw₀.forIn_eq_forIn_keysArray ⟨m.1, m.2.size_buckets_pos⟩
namespace Const
variable {β : Type v} {m : DHashMap α (fun _ => β)}
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} :
m.foldM f init = (DHashMap.Const.toArray m).foldlM (fun a b => f a b.1 b.2) init :=
Raw₀.Const.foldM_eq_foldlM_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
m.fold f init = (DHashMap.Const.toArray m).foldl (fun a b => f a b.1 b.2) init :=
Raw₀.Const.fold_eq_foldl_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
m.forM f = (DHashMap.Const.toArray m).forM (fun a => f a.1 a.2) :=
Raw₀.Const.forM_eq_forM_toArray ⟨m.1, m.2.size_buckets_pos⟩
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)} {init : δ} :
m.forIn f init = ForIn.forIn (DHashMap.Const.toArray m) init (fun a b => f a.1 a.2 b) :=
Raw₀.Const.forIn_eq_forIn_toArray ⟨m.1, m.2.size_buckets_pos⟩
end Const
end monadic
variable {ρ : Type w} [ForIn Id ρ ((a : α) × β a)]

8
src/Std/Data/DHashMap/Raw.lean
View file

@ -435,10 +435,6 @@ define the `ForM` and `ForIn` instances for `HashMap.Raw`.
end Const
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
/--
Updates the values of the hash map by applying the given function to all mappings, keeping
only those mappings where the function returns `some` value.
@ -473,6 +469,10 @@ only those mappings where the function returns `some` value.
@[inline] def keysArray (m : Raw α β) : Array α :=
m.fold (fun acc k _ => acc.push k) (.emptyWithCapacity m.size)
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
/-- Returns a list of all values present in the hash map in some order. -/
@[inline] def values {β : Type v} (m : Raw α (fun _ => β)) : List β :=
Internal.foldRev (fun acc _ v => v :: acc) [] m

202
src/Std/Data/DHashMap/RawLemmas.lean
View file

@ -1241,6 +1241,49 @@ theorem map_sigma_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF
m.toList.map Sigma.fst = m.keys := by
apply Raw₀.map_fst_toList_eq_keys ⟨m, h.size_buckets_pos⟩
@[simp]
theorem toArray_keys (h : m.WF) :
m.keys.toArray = m.keysArray :=
Raw₀.toArray_keys_eq_keysArray ⟨m, h.size_buckets_pos⟩
@[simp]
theorem toList_keysArray (h : m.WF) :
m.keysArray.toList = m.keys :=
Raw₀.toList_keysArray_eq_keys ⟨m, h.size_buckets_pos⟩
@[simp]
theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysArray.size = m.size :=
Raw₀.size_keysArray ⟨m, h.size_buckets_pos⟩ h
@[simp]
theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysArray.isEmpty = m.isEmpty :=
Raw₀.isEmpty_keysArray ⟨m, h.size_buckets_pos⟩ h
@[simp]
theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
m.keysArray.contains k = m.contains k := by
simp_to_raw using Raw₀.contains_keysArray ⟨m, h.size_buckets_pos⟩ h
@[simp]
theorem mem_keysArray [LawfulBEq α] {k : α} (h : m.WF) :
k ∈ m.keysArray ↔ k ∈ m := by
rw [mem_iff_contains]
simp_to_raw using Raw₀.mem_keysArray ⟨m, h.size_buckets_pos⟩ h
theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
{p : α → Prop} (h : m.WF) :
(∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) := by
simp only [mem_iff_contains]
simp_to_raw using
Raw₀.forall_mem_keysArray_iff_forall_contains_getKey ⟨m, h.size_buckets_pos⟩ h
theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
(h' : k ∈ m.keysArray) : m.contains k := by
simp_to_raw using Raw₀.contains_of_mem_keysArray ⟨m, h.size_buckets_pos⟩ h h'
@[simp, grind =]
theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.length = m.size := by
@ -1347,6 +1390,105 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
end Const
@[simp]
theorem toArray_toList (h : m.WF) :
m.toList.toArray = m.toArray :=
Raw₀.toArray_toList_eq_toArray ⟨m, h.size_buckets_pos⟩
@[simp]
theorem toList_toArray (h : m.WF) :
m.toArray.toList = m.toList :=
Raw₀.toList_toArray_eq_toList ⟨m, h.size_buckets_pos⟩
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.map Sigma.fst = m.keysArray :=
Raw₀.map_fst_toArray_eq_keysArray ⟨m, h.size_buckets_pos⟩
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.size = m.size :=
Raw₀.size_toArray ⟨m, h.size_buckets_pos⟩ h
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.isEmpty = m.isEmpty :=
Raw₀.isEmpty_toArray ⟨m, h.size_buckets_pos⟩ h
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β k} (h : m.WF) :
⟨k, v⟩ ∈ m.toArray ↔ m.get? k = some v := by
simp_to_raw using Raw₀.mem_toArray_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
theorem find?_toArray_eq_some_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β k} (h : m.WF) :
m.toArray.find? (·.1 == k) = some ⟨k, v⟩ ↔ m.get? k = some v := by
simp_to_raw using
Raw₀.find?_toArray_eq_some_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
m.toArray.find? (·.1 == k) = none ↔ m.contains k = false := by
simp_to_raw using Raw₀.find?_toArray_eq_none_iff_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
namespace Const
variable {β : Type v} {m : Raw α (fun _ => β)}
@[simp]
theorem toArray_toList (h : m.WF) :
(Raw.Const.toList m).toArray = Raw.Const.toArray m :=
Raw₀.Const.toArray_toList_eq_toArray ⟨m, h.size_buckets_pos⟩
@[simp]
theorem toList_toArray (h : m.WF) :
(Raw.Const.toArray m).toList = Raw.Const.toList m :=
Raw₀.Const.toList_toArray_eq_toList ⟨m, h.size_buckets_pos⟩
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
(Raw.Const.toArray m).map Prod.fst = m.keysArray :=
Raw₀.Const.map_fst_toArray_eq_keysArray ⟨m, h.size_buckets_pos⟩
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
(Raw.Const.toArray m).size = m.size :=
Raw₀.Const.size_toArray ⟨m, h.size_buckets_pos⟩ h
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
(Raw.Const.toArray m).isEmpty = m.isEmpty :=
Raw₀.Const.isEmpty_toArray ⟨m, h.size_buckets_pos⟩ h
theorem mem_toArray_iff_get?_eq_some [LawfulBEq α]
{k : α} {v : β} (h : m.WF) :
(k, v) ∈ Raw.Const.toArray m ↔ get? m k = some v := by
simp_to_raw using Raw₀.Const.mem_toArray_iff_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
{k : α} {v : β} (h : m.WF) :
get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ Raw.Const.toArray m := by
simp_to_raw using Raw₀.Const.get?_eq_some_iff_exists_beq_and_mem_toArray ⟨m, h.size_buckets_pos⟩ h
theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
[EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
(Raw.Const.toArray m).find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
m.getKey? k = some k' ∧ get? m k = some v := by
simp_to_raw using
Raw₀.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some ⟨m, h.size_buckets_pos⟩ h
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
(Raw.Const.toArray m).find? (·.1 == k) = none ↔ m.contains k = false := by
simp_to_raw using Raw₀.Const.find?_toArray_eq_none_iff_contains_eq_false ⟨m, h.size_buckets_pos⟩ h
theorem mem_toArray_iff_getKey?_eq_some_and_get?_eq_some [EquivBEq α] [LawfulHashable α]
(h : m.WF) {k: α} {v : β} :
(k, v) ∈ Raw.Const.toArray m ↔ m.getKey? k = some k ∧ get? m k = some v := by
simp [← toArray_toList, h, mem_toList_iff_getKey?_eq_some_and_get?_eq_some]
end Const
section monadic
variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
@ -1476,6 +1618,66 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
end Const
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → (a : α) → β a → m' δ} {init : δ} (h : m.WF) :
m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
Raw₀.foldM_eq_foldlM_toArray ⟨m, h.size_buckets_pos⟩
theorem fold_eq_foldl_toArray {f : δ → (a : α) → β a → δ} {init : δ} (h : m.WF) :
m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
Raw₀.fold_eq_foldl_toArray ⟨m, h.size_buckets_pos⟩
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : (a : α) → β a → m' PUnit} (h : m.WF) :
m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
Raw₀.forM_eq_forM_toArray ⟨m, h.size_buckets_pos⟩
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : (a : α) → β a → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
Raw₀.forIn_eq_forIn_toArray ⟨m, h.size_buckets_pos⟩
theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} (h : m.WF) :
m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
Raw₀.foldM_eq_foldlM_keysArray ⟨m, h.size_buckets_pos⟩
theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} (h : m.WF) :
m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
Raw₀.fold_eq_foldl_keysArray ⟨m, h.size_buckets_pos⟩
theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
m.forM (fun a _ => f a) = m.keysArray.forM f :=
Raw₀.forM_eq_forM_keysArray ⟨m, h.size_buckets_pos⟩
theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
Raw₀.forIn_eq_forIn_keysArray ⟨m, h.size_buckets_pos⟩
namespace Const
variable {β : Type v} {m : Raw α (fun _ => β)}
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} (h : m.WF) :
m.foldM f init = (Raw.Const.toArray m).foldlM (fun a b => f a b.1 b.2) init :=
Raw₀.Const.foldM_eq_foldlM_toArray ⟨m, h.size_buckets_pos⟩
theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} (h : m.WF) :
m.fold f init = (Raw.Const.toArray m).foldl (fun a b => f a b.1 b.2) init :=
Raw₀.Const.fold_eq_foldl_toArray ⟨m, h.size_buckets_pos⟩
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} (h : m.WF) :
m.forM f = (Raw.Const.toArray m).forM (fun a => f a.1 a.2) :=
Raw₀.Const.forM_eq_forM_toArray ⟨m, h.size_buckets_pos⟩
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn f init = ForIn.forIn (Raw.Const.toArray m) init (fun a b => f a.1 a.2 b) :=
Raw₀.Const.forIn_eq_forIn_toArray ⟨m, h.size_buckets_pos⟩
end Const
end monadic
section insertMany

15
src/Std/Data/HashMap/Basic.lean
View file

@ -247,6 +247,13 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β
{ρ : Type w} [ForIn Id ρ α] (m : HashMap α Unit) (l : ρ) : HashMap α Unit :=
⟨DHashMap.Const.insertManyIfNewUnit m.inner l⟩
@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
Array (α × β) :=
DHashMap.Const.toArray m.inner
@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
Array α :=
m.inner.keysArray
section Unverified
@ -257,14 +264,6 @@ section Unverified
let ⟨l, r⟩ := m.inner.partition f
⟨⟨l⟩, ⟨r⟩⟩
@[inline, inherit_doc DHashMap.Const.toArray] def toArray (m : HashMap α β) :
Array (α × β) :=
DHashMap.Const.toArray m.inner
@[inline, inherit_doc DHashMap.keysArray] def keysArray (m : HashMap α β) :
Array α :=
m.inner.keysArray
@[inline, inherit_doc DHashMap.values] def values (m : HashMap α β) : List β :=
m.inner.values

127
src/Std/Data/HashMap/Lemmas.lean
View file

@ -859,6 +859,46 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
m.keys.Pairwise (fun a b => (a == b) = false) :=
DHashMap.distinct_keys
@[simp]
theorem toArray_keys :
m.keys.toArray = m.keysArray :=
DHashMap.toArray_keys
@[simp]
theorem toList_keysArray :
m.keysArray.toList = m.keys :=
DHashMap.toList_keysArray
@[simp]
theorem size_keysArray [EquivBEq α] [LawfulHashable α] :
m.keysArray.size = m.size :=
DHashMap.size_keysArray
@[simp]
theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] :
m.keysArray.isEmpty = m.isEmpty :=
DHashMap.isEmpty_keysArray
@[simp]
theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
{k : α} :
m.keysArray.contains k = m.contains k :=
DHashMap.contains_keysArray
@[simp]
theorem mem_keysArray [LawfulBEq α] {k : α} :
k ∈ m.keysArray ↔ k ∈ m :=
DHashMap.mem_keysArray
theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
{p : α → Prop} :
(∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
DHashMap.forall_mem_keysArray_iff_forall_mem_getKey
theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] {k : α}
(h' : k ∈ m.keysArray) : m.contains k :=
DHashMap.contains_of_mem_keysArray h'
@[simp, grind _=_]
theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] :
m.toList.map Prod.fst = m.keys :=
@ -921,6 +961,57 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] :
m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
DHashMap.Const.distinct_keys_toList
@[simp]
theorem toArray_toList :
m.toList.toArray = m.toArray :=
DHashMap.Const.toArray_toList
@[simp]
theorem toList_toArray :
m.toArray.toList = m.toList :=
DHashMap.Const.toList_toArray
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] :
m.toArray.map Prod.fst = m.keysArray :=
DHashMap.Const.map_fst_toArray_eq_keysArray
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.size = m.size :=
DHashMap.Const.size_toArray
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.isEmpty = m.isEmpty :=
DHashMap.Const.isEmpty_toArray
theorem mem_toArray_iff_getElem?_eq_some [LawfulBEq α]
{k : α} {v : β} :
(k, v) ∈ m.toArray ↔ m[k]? = some v :=
DHashMap.Const.mem_toArray_iff_get?_eq_some
theorem getElem?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
{k : α} {v : β} :
m[k]? = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
DHashMap.Const.get?_eq_some_iff_exists_beq_and_mem_toArray
theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
[EquivBEq α] [LawfulHashable α] {k k' : α} {v : β} :
m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
m.getKey? k = some k' ∧ get? m k = some v :=
DHashMap.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} :
m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
DHashMap.Const.find?_toArray_eq_none_iff_contains_eq_false
theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α]
{k: α} {v : β} :
(k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v := by
simp [← toArray_toList, mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some]
section monadic
variable {m : HashMap α β} {δ : Type w} {m' : Type w → Type w}
@ -970,6 +1061,42 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m']
ForIn.forIn m init (fun a d => f a.1 d) = ForIn.forIn m.keys init f :=
DHashMap.forIn_eq_forIn_keys
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} :
m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
DHashMap.Const.foldM_eq_foldlM_toArray
theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} :
m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
DHashMap.Const.fold_eq_foldl_toArray
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} :
m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
DHashMap.Const.forM_eq_forM_toArray
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)} {init : δ} :
m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
DHashMap.Const.forIn_eq_forIn_toArray
theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} :
m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
DHashMap.foldM_eq_foldlM_keysArray
theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} :
m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
DHashMap.fold_eq_foldl_keysArray
theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
m.forM (fun a _ => f a) = m.keysArray.forM f :=
DHashMap.forM_eq_forM_keysArray
theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} :
m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
DHashMap.forIn_eq_forIn_keysArray
end monadic
variable {ρ : Type w} [ForIn Id ρ (α × β)]

4
src/Std/Data/HashMap/Raw.lean
View file

@ -230,8 +230,6 @@ instance {m : Type w → Type w} : ForIn m (Raw α β) (α × β) where
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
@[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ)
(m : Raw α β) : Raw α γ :=
⟨m.inner.filterMap f⟩
@ -249,6 +247,8 @@ section Unverified
@[inline, inherit_doc DHashMap.Raw.keysArray] def keysArray (m : Raw α β) : Array α :=
m.inner.keysArray
/-! We currently do not provide lemmas for the functions below. -/
@[inline, inherit_doc DHashMap.Raw.values] def values (m : Raw α β) : List β :=
m.inner.values

127
src/Std/Data/HashMap/RawLemmas.lean
View file

@ -874,6 +874,46 @@ theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keys.Pairwise (fun a b => (a == b) = false) :=
DHashMap.Raw.distinct_keys h.out
@[simp]
theorem toArray_keys (h : m.WF) :
m.keys.toArray = m.keysArray :=
DHashMap.Raw.toArray_keys h.out
@[simp]
theorem toList_keysArray (h : m.WF) :
m.keysArray.toList = m.keys :=
DHashMap.Raw.toList_keysArray h.out
@[simp]
theorem size_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysArray.size = m.size :=
DHashMap.Raw.size_keysArray h.out
@[simp]
theorem isEmpty_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.keysArray.isEmpty = m.isEmpty :=
DHashMap.Raw.isEmpty_keysArray h.out
@[simp]
theorem contains_keysArray [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
m.keysArray.contains k = m.contains k :=
DHashMap.Raw.contains_keysArray h.out
@[simp]
theorem mem_keysArray [LawfulBEq α] {k : α} (h : m.WF) :
k ∈ m.keysArray ↔ k ∈ m :=
DHashMap.Raw.mem_keysArray h.out
theorem forall_mem_keysArray_iff_forall_mem_getKey [EquivBEq α] [LawfulHashable α]
{p : α → Prop} (h : m.WF) :
(∀ k ∈ m.keysArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.getKey k h) :=
DHashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey h.out
theorem contains_of_mem_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
(h' : k ∈ m.keysArray) : m.contains k :=
DHashMap.Raw.contains_of_mem_keysArray h.out h'
@[simp, grind _=_]
theorem map_fst_toList_eq_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.map Prod.fst = m.keys :=
@ -937,6 +977,57 @@ theorem distinct_keys_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.Pairwise (fun a b => (a.1 == b.1) = false) :=
DHashMap.Raw.Const.distinct_keys_toList h.out
@[simp]
theorem toArray_toList (h : m.WF) :
m.toList.toArray = m.toArray :=
DHashMap.Raw.Const.toArray_toList h.out
@[simp]
theorem toList_toArray (h : m.WF) :
m.toArray.toList = m.toList :=
DHashMap.Raw.Const.toList_toArray h.out
@[simp]
theorem map_fst_toArray_eq_keysArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.map Prod.fst = m.keysArray :=
DHashMap.Raw.Const.map_fst_toArray_eq_keysArray h.out
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.size = m.size :=
DHashMap.Raw.Const.size_toArray h.out
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.isEmpty = m.isEmpty :=
DHashMap.Raw.Const.isEmpty_toArray h.out
theorem mem_toArray_iff_getElem?_eq_some [LawfulBEq α]
{k : α} {v : β} (h : m.WF) :
(k, v) ∈ m.toArray ↔ m[k]? = some v :=
DHashMap.Raw.Const.mem_toArray_iff_get?_eq_some h.out
theorem get?_eq_some_iff_exists_beq_and_mem_toArray [EquivBEq α] [LawfulHashable α]
{k : α} {v : β} (h : m.WF) :
get? m k = some v ↔ ∃ (k' : α), k == k' ∧ (k', v) ∈ m.toArray :=
DHashMap.Raw.Const.get?_eq_some_iff_exists_beq_and_mem_toArray h.out
theorem find?_toArray_eq_some_iff_getKey?_eq_some_and_getElem?_eq_some
[EquivBEq α] [LawfulHashable α] (h : m.WF) {k k' : α} {v : β} :
m.toArray.find? (fun a => a.1 == k) = some ⟨k', v⟩ ↔
m.getKey? k = some k' ∧ m[k]? = some v :=
DHashMap.Raw.Const.find?_toArray_eq_some_iff_getKey?_eq_some_and_get?_eq_some h.out
theorem find?_toArray_eq_none_iff_contains_eq_false [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
m.toArray.find? (·.1 == k) = none ↔ m.contains k = false :=
DHashMap.Raw.Const.find?_toArray_eq_none_iff_contains_eq_false h.out
theorem mem_toArray_iff_getKey?_eq_some_and_getElem?_eq_some [EquivBEq α] [LawfulHashable α]
(h : m.WF) {k: α} {v : β} :
(k, v) ∈ m.toArray ↔ m.getKey? k = some k ∧ m[k]? = some v := by
simp [← toArray_toList, h, mem_toList_iff_getKey?_eq_some_and_getElem?_eq_some]
section monadic
variable {m : Raw α β} {δ : Type w} {m' : Type w → Type w}
@ -988,6 +1079,42 @@ theorem forIn_eq_forIn_keys [Monad m'] [LawfulMonad m'] (h : m.WF)
ForIn.forIn m init (fun a d => f a.1 d) = ForIn.forIn m.keys init f :=
DHashMap.Raw.forIn_eq_forIn_keys h.out
theorem foldM_eq_foldlM_keysArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} (h : m.WF) :
m.foldM (fun d a _ => f d a) init = m.keysArray.foldlM f init :=
DHashMap.Raw.foldM_eq_foldlM_keysArray h.out
theorem fold_eq_foldl_keysArray {f : δ → α → δ} {init : δ} (h : m.WF) :
m.fold (fun d a _ => f d a) init = m.keysArray.foldl f init :=
DHashMap.Raw.fold_eq_foldl_keysArray h.out
theorem forM_eq_forM_keysArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
m.forM (fun a _ => f a) = m.keysArray.forM f :=
DHashMap.Raw.forM_eq_forM_keysArray h.out
theorem forIn_eq_forIn_keysArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn (fun a _ d => f a d) init = ForIn.forIn m.keysArray init f :=
DHashMap.Raw.forIn_eq_forIn_keysArray h.out
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → β → m' δ} {init : δ} (h : m.WF) :
m.foldM f init = m.toArray.foldlM (fun a b => f a b.1 b.2) init :=
DHashMap.Raw.Const.foldM_eq_foldlM_toArray h.out
theorem fold_eq_foldl_toArray {f : δ → α → β → δ} {init : δ} (h : m.WF) :
m.fold f init = m.toArray.foldl (fun a b => f a b.1 b.2) init :=
DHashMap.Raw.Const.fold_eq_foldl_toArray h.out
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → β → m' PUnit} (h : m.WF) :
m.forM f = m.toArray.forM (fun a => f a.1 a.2) :=
DHashMap.Raw.Const.forM_eq_forM_toArray h.out
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → β → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn f init = ForIn.forIn m.toArray init (fun a b => f a.1 a.2 b) :=
DHashMap.Raw.Const.forIn_eq_forIn_toArray h.out
end monadic
variable {ρ : Type w} [ForIn Id ρ (α × β)]

9
src/Std/Data/HashSet/Basic.lean
View file

@ -231,6 +231,10 @@ appearance.
HashSet α :=
⟨m.inner.insertManyIfNewUnit l⟩
/-- Transforms the hash set into an array of elements in some order. -/
@[inline] def toArray (m : HashSet α) : Array α :=
m.inner.keysArray
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
@ -252,11 +256,6 @@ section Unverified
if p a then return true
return false
/-- Transforms the hash set into an array of elements in some order. -/
@[inline] def toArray (m : HashSet α) : Array α :=
m.inner.keysArray
/--
Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the
collection contains multiple elements that are equal (with regard to `==`), then the last element

58
src/Std/Data/HashSet/Lemmas.lean
View file

@ -482,6 +482,46 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
m.toList.Pairwise (fun a b => (a == b) = false) :=
HashMap.distinct_keys
@[simp]
theorem toArray_toList :
m.toList.toArray = m.toArray :=
HashMap.toArray_keys
@[simp]
theorem toList_toArray :
m.toArray.toList = m.toList :=
HashMap.toList_keysArray
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.size = m.size :=
HashMap.size_keysArray
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] :
m.toArray.isEmpty = m.isEmpty :=
HashMap.isEmpty_keysArray
@[simp]
theorem contains_toArray [EquivBEq α] [LawfulHashable α]
{k : α} :
m.toArray.contains k = m.contains k :=
HashMap.contains_keysArray
@[simp]
theorem mem_toArray [LawfulBEq α] {k : α} :
k ∈ m.toArray ↔ k ∈ m :=
HashMap.mem_keysArray
theorem forall_mem_toArray_iff_forall_mem_get [EquivBEq α] [LawfulHashable α]
{p : α → Prop} :
(∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h) :=
HashMap.forall_mem_keysArray_iff_forall_mem_getKey
theorem contains_of_mem_toArray [EquivBEq α] [LawfulHashable α] {k : α}
(h' : k ∈ m.toArray) : m.contains k :=
HashMap.contains_of_mem_keysArray h'
section monadic
variable {δ : Type v} {m' : Type v → Type v}
@ -513,6 +553,24 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m']
ForIn.forIn m init f = ForIn.forIn m.toList init f :=
HashMap.forIn_eq_forIn_keys
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} :
m.foldM (fun d a => f d a) init = m.toArray.foldlM f init :=
HashMap.foldM_eq_foldlM_keysArray
theorem fold_eq_foldl_toArray {f : δ → α → δ} {init : δ} :
m.fold (fun d a => f d a) init = m.toArray.foldl f init :=
HashMap.fold_eq_foldl_keysArray
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} :
m.forM (fun a => f a) = m.toArray.forM f :=
HashMap.forM_eq_forM_keysArray
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} :
m.forIn (fun a d => f a d) init = ForIn.forIn m.toArray init f :=
HashMap.forIn_eq_forIn_keysArray
end monadic
variable {ρ : Type v} [ForIn Id ρ α]

17
src/Std/Data/HashSet/Raw.lean
View file

@ -216,14 +216,18 @@ instance {m : Type v → Type v} : ForM m (Raw α) α where
instance {m : Type v → Type v} : ForIn m (Raw α) α where
forIn m init f := m.forIn f init
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
/-- Removes all elements from the hash set for which the given function returns `false`. -/
@[inline] def filter [BEq α] [Hashable α] (f : α → Bool) (m : Raw α) : Raw α :=
⟨m.inner.filter fun a _ => f a⟩
/-- Transforms the hash set into an array of elements in some order. -/
@[inline] def toArray (m : Raw α) : Array α :=
m.inner.keysArray
section Unverified
/-! We currently do not provide lemmas for the functions below. -/
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/
@[inline] def all (m : Raw α) (p : α → Bool) : Bool := Id.run do
for a in m do
@ -236,11 +240,6 @@ section Unverified
if p a then return true
return false
/-- Transforms the hash set into an array of elements in some order. -/
@[inline] def toArray (m : Raw α) : Array α :=
m.inner.keysArray
/--
Inserts multiple mappings into the hash set by iterating over the given collection and calling
`insert`. If the same key appears multiple times, the first occurrence takes precedence.

58
src/Std/Data/HashSet/RawLemmas.lean
View file

@ -506,6 +506,46 @@ theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toList.Pairwise (fun a b => (a == b) = false) :=
HashMap.Raw.distinct_keys h.1
@[simp]
theorem toArray_toList (h : m.WF) :
m.toList.toArray = m.toArray :=
HashMap.Raw.toArray_keys h.out
@[simp]
theorem toList_toArray (h : m.WF) :
m.toArray.toList = m.toList :=
HashMap.Raw.toList_keysArray h.out
@[simp]
theorem size_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.size = m.size :=
HashMap.Raw.size_keysArray h.out
@[simp]
theorem isEmpty_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) :
m.toArray.isEmpty = m.isEmpty :=
HashMap.Raw.isEmpty_keysArray h.out
@[simp]
theorem contains_toArray [EquivBEq α] [LawfulHashable α]
{k : α} (h : m.WF) :
m.toArray.contains k = m.contains k :=
HashMap.Raw.contains_keysArray h.out
@[simp]
theorem mem_toArray [LawfulBEq α] {k : α} (h : m.WF) :
k ∈ m.toArray ↔ k ∈ m :=
HashMap.Raw.mem_keysArray h.out
theorem forall_mem_toArray_iff_forall_mem_get [EquivBEq α] [LawfulHashable α]
{p : α → Prop} (h : m.WF) :
(∀ k ∈ m.toArray, p k) ↔ ∀ (k : α) (h : k ∈ m), p (m.get k h) :=
HashMap.Raw.forall_mem_keysArray_iff_forall_mem_getKey h.out
theorem contains_of_mem_toArray [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α}
(h' : k ∈ m.toArray) : m.contains k :=
HashMap.Raw.contains_of_mem_keysArray h.out h'
section monadic
variable {m : Raw α} {δ : Type v} {m' : Type v → Type v}
@ -539,6 +579,24 @@ theorem forIn_eq_forIn_toList [Monad m'] [LawfulMonad m'] (h : m.WF)
ForIn.forIn m init f = ForIn.forIn m.toList init f :=
HashMap.Raw.forIn_eq_forIn_keys h.out
theorem foldM_eq_foldlM_toArray [Monad m'] [LawfulMonad m']
{f : δ → α → m' δ} {init : δ} (h : m.WF) :
m.foldM (fun d a => f d a) init = m.toArray.foldlM f init :=
HashMap.Raw.foldM_eq_foldlM_keysArray h.out
theorem fold_eq_foldl_toArray {f : δ → α → δ} {init : δ} (h : m.WF) :
m.fold (fun d a => f d a) init = m.toArray.foldl f init :=
HashMap.Raw.fold_eq_foldl_keysArray h.out
theorem forM_eq_forM_toArray [Monad m'] [LawfulMonad m'] {f : α → m' PUnit} (h : m.WF) :
m.forM (fun a => f a) = m.toArray.forM f :=
HashMap.Raw.forM_eq_forM_keysArray h.out
theorem forIn_eq_forIn_toArray [Monad m'] [LawfulMonad m']
{f : α → δ → m' (ForInStep δ)} {init : δ} (h : m.WF) :
m.forIn (fun a d => f a d) init = ForIn.forIn m.toArray init f :=
HashMap.Raw.forIn_eq_forIn_keysArray h.out
end monadic
variable {ρ : Type v} [ForIn Id ρ α]