Rename results around HashMap keys method

leanprover · Nov 8, 2024 · 01b95c3 · 01b95c3
1 parent 4f4d7aa
commit 01b95c3
Show file tree

Hide file tree

Showing 7 changed files with 63 additions and 61 deletions.
diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean
@@ -815,22 +815,22 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.1.WF) :
+theorem length_keys [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 isEmpty_keys [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
+    m.1.keys.isEmpty = m.1.isEmpty:= by
+  simp_to_model using List.isEmpty_keys_eq_isEmpty
+
 @[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 isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h: m.1.WF):
-    m.1.keys.isEmpty = m.1.isEmpty:= by
-  simp_to_model using List.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_contains [LawfulBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} :
+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]

diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean
@@ -944,25 +944,25 @@ theorem getThenInsertIfNew?_snd {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  Raw₀.length_keys_eq_size ⟨m.1, m.2.size_buckets_pos⟩ m.2
+  Raw₀.length_keys ⟨m.1, m.2.size_buckets_pos⟩ m.2
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty  :=
+  Raw₀.isEmpty_keys ⟨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 isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty  :=
-  Raw₀.isEmpty_keys_eq_isEmpty ⟨m.1, m.2.size_buckets_pos⟩ m.2
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  exact Raw₀.mem_keys_iff_contains ⟨m.1, _⟩ m.2
+  exact Raw₀.mem_keys ⟨m.1, _⟩ m.2
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 

diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean
@@ -1023,25 +1023,25 @@ theorem getThenInsertIfNew?_snd (h : m.WF) {k : α} {v : β} :
 end Const
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+theorem length_keys [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_to_raw using Raw₀.length_keys ⟨m, h.size_buckets_pos⟩ h
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty := by
+  simp_to_raw using Raw₀.isEmpty_keys ⟨m, h.size_buckets_pos⟩
 
 @[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 isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty := by
-  simp_to_raw using Raw₀.isEmpty_keys_eq_isEmpty ⟨m, h.size_buckets_pos⟩
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := by 
   rw [mem_iff_contains]
-  simp_to_raw using Raw₀.mem_keys_iff_contains ⟨m, _⟩ h
+  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

diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean
@@ -678,24 +678,24 @@ instance [EquivBEq α] [LawfulHashable α] : LawfulGetElem (HashMap α β) α β
     split <;> simp_all
 
 @[simp]
-theorem length_keys_eq_size [EquivBEq α] [LawfulHashable α] :
+theorem length_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.length = m.size :=
-  DHashMap.length_keys_eq_size
+  DHashMap.length_keys
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α]:
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.isEmpty_keys
 
 @[simp]
 theorem contains_keys [EquivBEq α] [LawfulHashable α] {k : α} :
     m.keys.contains k = m.contains k :=
   DHashMap.contains_keys
 
 @[simp]
-theorem isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α]:
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.mem_keys_iff_mem
+  DHashMap.mem_keys
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] :
     m.keys.Pairwise (fun a b => (a == b) = false) := 

diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean
@@ -683,24 +683,24 @@ 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) :
+theorem length_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.length = m.size :=
-  DHashMap.Raw.length_keys_eq_size h.out
+  DHashMap.Raw.length_keys h.out
+
+@[simp]
+theorem isEmpty_keys [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.keys.isEmpty = m.isEmpty :=
+  DHashMap.Raw.isEmpty_keys 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 isEmpty_keys_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.keys.isEmpty = m.isEmpty :=
-  DHashMap.Raw.isEmpty_keys_eq_isEmpty h.out
-
-@[simp]
-theorem mem_keys_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
+theorem mem_keys [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
     k ∈ m.keys ↔ k ∈ m := 
-  DHashMap.Raw.mem_keys_iff_mem h.out
+  DHashMap.Raw.mem_keys h.out
 
 theorem distinct_keys [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.keys.Pairwise (fun a b => (a == b) = false) := 

diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
@@ -354,23 +354,24 @@ theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert
   ext HashMap.containsThenInsertIfNew_snd
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size :=
-  HashMap.length_keys_eq_size
+theorem length_toList [EquivBEq α] [LawfulHashable α] : 
+    m.toList.length = m.size :=
+  HashMap.length_keys
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] :
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.isEmpty_keys
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α}:
     m.toList.contains k = m.contains k :=
   HashMap.contains_keys
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] :
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.isEmpty_keys_eq_isEmpty
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α]  {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α]  {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.mem_keys_iff_mem
+  HashMap.mem_keys
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
     m.toList.Pairwise (fun a b => (a == b) = false) :=

diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
@@ -367,23 +367,24 @@ theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2
   ext (HashMap.Raw.containsThenInsertIfNew_snd h.out)
 
 @[simp]
-theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] (h : m.WF): m.toList.length = m.size :=
-  HashMap.Raw.length_keys_eq_size h.1
+theorem length_toList [EquivBEq α] [LawfulHashable α] (h : m.WF): 
+    m.toList.length = m.size :=
+  HashMap.Raw.length_keys h.1
+
+@[simp]
+theorem isEmpty_toList [EquivBEq α] [LawfulHashable α] (h : m.WF):
+    m.toList.isEmpty = m.isEmpty :=
+  HashMap.Raw.isEmpty_keys h.1
 
 @[simp]
 theorem contains_toList [EquivBEq α] [LawfulHashable α] {k : α} (h : m.WF):
     m.toList.contains k = m.contains k :=
   HashMap.Raw.contains_keys h.1
 
 @[simp]
-theorem isEmpty_toList_eq_isEmpty [EquivBEq α] [LawfulHashable α] (h : m.WF):
-    m.toList.isEmpty = m.isEmpty :=
-  HashMap.Raw.isEmpty_keys_eq_isEmpty h.1
-
-@[simp]
-theorem mem_toList_iff_mem [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
+theorem mem_toList [LawfulBEq α] [LawfulHashable α] (h : m.WF) {k : α}:
     k ∈ m.toList ↔ k ∈ m :=
-  HashMap.Raw.mem_keys_iff_mem h.1
+  HashMap.Raw.mem_keys h.1
 
 theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
     m.toList.Pairwise (fun a b => (a == b) = false) :=