From f46c17fa1ddd249c244e3cff331f47f526417826 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Tue, 18 Nov 2025 08:17:16 +0000 Subject: [PATCH] feat: add lemmas for `DHashMap`/`HashMap`/`HashSet` about `emptyWithCapacity`/`empty` (#11223) This PR adds missing lemmas relating `emptyWithCapacity`/`empty` and `toList`/`keys`/`values` for `DHashMap`/`HashMap`/`HashSet`. --- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 16 ++++++++++ src/Std/Data/DHashMap/Internal/WF.lean | 9 ++++++ src/Std/Data/DHashMap/Lemmas.lean | 32 +++++++++++++++++++ src/Std/Data/DHashMap/RawLemmas.lean | 32 +++++++++++++++++++ src/Std/Data/HashMap/Lemmas.lean | 24 ++++++++++++++ src/Std/Data/HashMap/RawLemmas.lean | 24 ++++++++++++++ src/Std/Data/HashSet/Lemmas.lean | 8 +++++ src/Std/Data/HashSet/RawLemmas.lean | 8 +++++ src/Std/Data/Internal/List/Associative.lean | 7 ++++ 9 files changed, 160 insertions(+) diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 22998c97ce..936b237de4 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -75,6 +75,22 @@ theorem size_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.size theorem isEmpty_eq_size_eq_zero : m.1.isEmpty = (m.1.size == 0) := by simp [Raw.isEmpty] +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.toList = [] := by + rw [Raw.toList_eq_toListModel, toListModel_buckets_emptyWithCapacity] + +@[simp] +theorem Const.toList_emptyWithCapacity {c} {β : Type v} : Raw.Const.toList (emptyWithCapacity c : Raw₀ α (fun _ => β)).1 = [] := by + rw [Raw.Const.toList_eq_toListModel_map, toListModel_buckets_emptyWithCapacity, List.map_nil] + +@[simp] +theorem keys_emptyWithCapacity {c} : (emptyWithCapacity c : Raw₀ α β).1.keys = [] := by + rw [Raw.keys_eq_keys_toListModel, toListModel_buckets_emptyWithCapacity, List.keys_nil] + +@[simp] +theorem Const.values_emptyWithCapacity {c} {β : Type v} : (emptyWithCapacity c : Raw₀ α (fun _ => β)).1.values = [] := by + rw [Raw.values_eq_values_toListModel, toListModel_buckets_emptyWithCapacity, List.values_nil] + variable [BEq α] [Hashable α] /-- Internal implementation detail of the hash map -/ diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 57b8293e9a..e602222273 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -131,6 +131,11 @@ theorem foldRev_cons_key {l : Raw α β} {acc : List α} : List.keys (toListModel l.buckets) ++ acc := by rw [foldRev_cons_apply, keys_eq_map] +theorem foldRev_cons_value {β : Type v} {l : Raw α (fun _ => β)} {acc : List β} : + Raw.Internal.foldRev (fun acc _ v => v :: acc) acc l = + List.values (toListModel l.buckets) ++ acc := by + rw [foldRev_cons_apply, values_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] @@ -207,6 +212,10 @@ 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 values_eq_values_toListModel {β : Type v} {m : Raw α (fun _ => β)} : + m.values = List.values (toListModel m.buckets) := by + simp [Raw.values, foldRev_cons_value, values_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] diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 9e730c6342..cd6f020e20 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -148,6 +148,38 @@ theorem size_empty : (∅ : DHashMap α β).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := (rfl) +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).toList = [] := + Raw₀.toList_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : DHashMap α β).toList = [] := + toList_emptyWithCapacity + +@[simp] +theorem Const.toList_emptyWithCapacity {c} {β : Type v}: Const.toList (emptyWithCapacity c : DHashMap α (fun _ => β)) = [] := + Raw₀.Const.toList_emptyWithCapacity + +@[simp] +theorem Const.toList_empty {β : Type v} : Const.toList (∅ : DHashMap α (fun _ => β)) = [] := + Const.toList_emptyWithCapacity + +@[simp] +theorem keys_emptyWithCapacity {c} : (emptyWithCapacity c : DHashMap α β).keys = [] := + Raw₀.keys_emptyWithCapacity + +@[simp] +theorem keys_empty : (∅ : DHashMap α β).keys = [] := + keys_emptyWithCapacity + +@[simp] +theorem Const.values_emptyWithCapacity {c} {β : Type v} : (emptyWithCapacity c : DHashMap α (fun _ => β)).values = [] := + Raw₀.Const.values_emptyWithCapacity + +@[simp] +theorem Const.values_empty {β : Type v} : (∅ : DHashMap α (fun _ => β)).values = [] := + Const.values_emptyWithCapacity + @[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β k} : (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := Raw₀.size_insert ⟨m.1, _⟩ m.2 diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 43e4d2fc06..342318b057 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -81,6 +81,38 @@ theorem size_empty : (∅ : Raw α β).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := by simp [isEmpty] +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).toList = [] := by + simp_to_raw using Raw₀.toList_emptyWithCapacity + +@[simp] +theorem Const.toList_emptyWithCapacity {β : Type v} {c} : Const.toList (emptyWithCapacity c : Raw α (fun _ => β)) = [] := by + simp_to_raw using Raw₀.Const.toList_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : Raw α β).toList = [] := + toList_emptyWithCapacity + +@[simp] +theorem Const.toList_empty {β : Type v} : Const.toList (∅ : Raw α (fun _ => β)) = [] := + Const.toList_emptyWithCapacity + +@[simp] +theorem keys_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).keys = [] := by + simp_to_raw using Raw₀.keys_emptyWithCapacity + +@[simp] +theorem keys_empty : (∅ : Raw α β).keys = [] := + keys_emptyWithCapacity + +@[simp] +theorem Const.values_emptyWithCapacity {c} {β : Type v} : (emptyWithCapacity c : Raw α (fun _ => β)).values = [] := by + simp_to_raw using Raw₀.Const.values_emptyWithCapacity + +@[simp] +theorem Const.values_empty {β : Type v} : (∅ : Raw α (fun _ => β)).values = [] := + Const.values_emptyWithCapacity + variable [BEq α] [Hashable α] @[simp, grind =] diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index b02952d7c5..ac02146d60 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -147,6 +147,30 @@ theorem size_empty : (∅ : HashMap α β).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.isEmpty_eq_size_eq_zero +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).toList = [] := + DHashMap.Const.toList_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : HashMap α β).toList = [] := + toList_emptyWithCapacity + +@[simp] +theorem keys_emptyWithCapacity {c} : (emptyWithCapacity c : HashMap α β).keys = [] := + DHashMap.keys_emptyWithCapacity + +@[simp] +theorem keys_empty : (∅ : HashMap α β).keys = [] := + keys_emptyWithCapacity + +@[simp] +theorem values_emptyWithCapacity {c} {β : Type v} : (emptyWithCapacity c : HashMap α β).values = [] := + DHashMap.Const.values_emptyWithCapacity + +@[simp] +theorem values_empty {β : Type v} : (∅ : HashMap α β).values = [] := + values_emptyWithCapacity + @[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} {v : β} : (m.insert k v).size = if k ∈ m then m.size else m.size + 1 := DHashMap.size_insert diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 9f30b6a852..0680e00f53 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -44,6 +44,30 @@ theorem size_empty : (∅ : Raw α β).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := DHashMap.Raw.isEmpty_eq_size_eq_zero +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).toList = [] := + DHashMap.Raw.Const.toList_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : Raw α β).toList = [] := + toList_emptyWithCapacity + +@[simp] +theorem keys_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α β).keys = [] := + DHashMap.Raw.keys_emptyWithCapacity + +@[simp] +theorem keys_empty : (∅ : Raw α β).keys = [] := + keys_emptyWithCapacity + +@[simp] +theorem values_emptyWithCapacity {c} {β : Type v} : (emptyWithCapacity c : Raw α β).values = [] := + DHashMap.Raw.Const.values_emptyWithCapacity + +@[simp] +theorem values_empty {β : Type v} : (∅ : Raw α β).values = [] := + values_emptyWithCapacity + private theorem ext {m m' : Raw α β} : m.inner = m'.inner → m = m' := by cases m; cases m'; rintro rfl; rfl diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 3674dd6a6a..2e0224782b 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -151,6 +151,14 @@ theorem size_empty : (∅ : HashSet α).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.isEmpty_eq_size_eq_zero +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : HashSet α).toList = [] := + HashMap.keys_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : HashSet α).toList = [] := + toList_emptyWithCapacity + @[grind =] theorem size_insert [EquivBEq α] [LawfulHashable α] {k : α} : (m.insert k).size = if k ∈ m then m.size else m.size + 1 := HashMap.size_insertIfNew diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 72ebdb546e..649f84cee3 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -46,6 +46,14 @@ theorem size_empty : (∅ : Raw α).size = 0 := theorem isEmpty_eq_size_eq_zero : m.isEmpty = (m.size == 0) := HashMap.Raw.isEmpty_eq_size_eq_zero +@[simp] +theorem toList_emptyWithCapacity {c} : (emptyWithCapacity c : Raw α).toList = [] := + HashMap.Raw.keys_emptyWithCapacity + +@[simp] +theorem toList_empty : (∅ : Raw α).toList = [] := + toList_emptyWithCapacity + variable [BEq α] [Hashable α] @[simp, grind =] diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index c0e3e75aba..d2de3e3b1d 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -162,6 +162,12 @@ theorem keys_eq_map {l : List ((a : α) × β a)} : | nil => rfl | cons => simp [keys, *] +theorem values_eq_map {β : Type v} {l : List ((_ : α) × β)} : + values l = l.map (·.2) := by + induction l with + | nil => rfl + | cons => simp [values, *] + theorem getEntry?_eq_some_iff [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {e} {k} (hd : DistinctKeys l) : getEntry? k l = some e ↔ k == e.1 ∧ e ∈ l := by @@ -393,6 +399,7 @@ theorem containsKey_eq_contains_map_fst [BEq α] [PartialEquivBEq α] {l : List rw [BEq.comm] @[simp] theorem keys_nil : keys ([] : List ((a : α) × β a)) = [] := (rfl) +@[simp] theorem values_nil {β : Type v} : values ([] : List ((_ : α) × β )) = [] := (rfl) @[simp] theorem keys_cons {l : List ((a : α) × β a)} {k : α} {v : β k} : keys (⟨k, v⟩ :: l) = k :: keys l := (rfl)