From 7e231a3e2af4042a0510e95935c5565c89874785 Mon Sep 17 00:00:00 2001
From: jt0202 <johannes.tantow@gmail.com>
Date: Tue, 5 Nov 2024 18:22:39 +0100
Subject: [PATCH] Add keys_isEmpty to HashMap

---
 src/Std/Data/DHashMap/Internal/RawLemmas.lean | 11 +++++++++--
 src/Std/Data/DHashMap/Lemmas.lean             |  9 +++++++--
 src/Std/Data/DHashMap/RawLemmas.lean          |  8 ++++++--
 src/Std/Data/HashMap/Lemmas.lean              | 11 ++++++++---
 src/Std/Data/HashMap/RawLemmas.lean           |  9 +++++++--
 5 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
index eecfe6c0e2f0..59e8bf65e081 100644
--- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,8 +815,8 @@ 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]
@@ -824,6 +824,13 @@ 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
index 31b2974a80b3..fd0c20302d63 100644
--- a/src/Std/Data/DHashMap/Lemmas.lean
+++ b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,8 +944,8 @@ 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]
@@ -953,4 +953,9 @@ 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
index 132e0ce1b618..16a4885b4121 100644
--- a/src/Std/Data/DHashMap/RawLemmas.lean
+++ b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,8 +1023,8 @@ 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]
@@ -1032,6 +1032,10 @@ 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
index bfd4fe9e04d5..bcea7b07de89 100644
--- 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
index edadac99d224..e1ebe2dd7105 100644
--- a/src/Std/Data/HashMap/RawLemmas.lean
+++ b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,8 +683,8 @@ 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]
@@ -692,6 +692,11 @@ 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