Added toList lemmas for HashSet

leanprover · Nov 6, 2024 · bfebae8 · bfebae8
1 parent dff162b
commit bfebae8
Show file tree

Hide file tree

Showing 2 changed files with 45 additions and 0 deletions.
diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean
@@ -353,6 +353,28 @@ theorem containsThenInsert_fst {k : α} : (m.containsThenInsert k).1 = m.contain
 theorem containsThenInsert_snd {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   ext HashMap.containsThenInsertIfNew_snd
 
+@[simp]
+theorem toList_length_eq_size [EquivBEq α] [LawfulHashable α] : m.toList.length = m.size :=
+  HashMap.length_keys_eq_size
+
+@[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 : α}:
+    k ∈ m.toList ↔ k ∈ m :=
+  HashMap.mem_keys_iff_mem
+
+theorem distinct_toList [EquivBEq α] [LawfulHashable α]:
+    m.toList.Pairwise (fun a b => (a == b) = false) :=
+  HashMap.distinct_keys
 end
 
 end Std.HashSet
diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean
@@ -366,6 +366,29 @@ theorem containsThenInsert_fst (h : m.WF) {k : α} : (m.containsThenInsert k).1
 theorem containsThenInsert_snd (h : m.WF) {k : α} : (m.containsThenInsert k).2 = m.insert k :=
   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
+
+@[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 : α}:
+    k ∈ m.toList ↔ k ∈ m :=
+  HashMap.Raw.mem_keys_iff_mem h.1
+
+theorem distinct_toList [EquivBEq α] [LawfulHashable α] (h : m.WF) :
+    m.toList.Pairwise (fun a b => (a == b) = false) :=
+  HashMap.Raw.distinct_keys h.1
+
 end Raw
 
 end Std.HashSet