Add keys_isEmpty to HashMap

leanprover · Nov 5, 2024 · 7e231a3 · 7e231a3
1 parent d9cac0c
commit 7e231a3
Show file tree

Hide file tree

Showing 5 changed files with 37 additions and 11 deletions.
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,15 +815,22 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) : 
-    m.1.keys.length = m.1.size := by 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+    m.1.keys.length = m.1.size := by
   simp_to_model using List.length_keys_eq_length
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
     m.1.keys.contains k = m.contains k := by
   simp_to_model using List.containsKey_eq_keys_contains.symm
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+    m.1.keys.isEmpty = m.1.isEmpty:= by
+  rw [Bool.eq_iff_iff, List.isEmpty_iff_length_eq_zero, isEmpty_eq_size_eq_zero, length_keys_eq_size m h]
+  simp
+
+
 end Raw₀
 
 end Std.DHashMap.Internal
diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,13 +944,18 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+    m.keys.length = m.size :=
   Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
   Raw₀.contains_keys ⟨m.1, _⟩ m.2
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty  :=
+  Raw₀.keys_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
 end Std.DHashMap
diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,15 +1023,19 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
-    m.keys.length = m.size := by 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys.length = m.size := by
   simp_to_raw using Raw₀.length_keys_eq_size ⟨m, h.size_buckets_pos⟩ h
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k := by
   simp_to_raw using Raw₀.contains_keys ⟨m, _⟩ h
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty := by
+  simp_to_raw using Raw₀.keys_isEmpty ⟨m, h.size_buckets_pos⟩
 end Raw
 
 end Std.DHashMap
diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,15 +678,20 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+    m.keys.length = m.size :=
   DHashMap.length_keys_eq_size
 
 @[simp]
-theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} : 
+theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
   DHashMap.contains_keys
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.keys_isEmpty
+
 end
 
 end Std.HashMap
diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,15 +683,20 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
   ext (DHashMap.Raw.Const.getThenInsertIfNew?_snd h.out)
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) : 
-    m.keys.length = m.size := 
+theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.keys.length = m.size :=
   DHashMap.Raw.length_keys_eq_size h.out
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     m.keys.contains k = m.contains k :=
   DHashMap.Raw.contains_keys h.out
 
+@[simp]
+theorem keys_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.Raw.keys_isEmpty h.out
+
 end Raw
 
 end Std.HashMap