feat: API about HashMap

Algorithm.lean

@@ -17,6 +17,8 @@ import Algorithm.Data.DFinsupp'.Fintype
 import Algorithm.Data.Forest
 import Algorithm.Data.Graph.AdjList
 import Algorithm.Data.Graph.IsDFSForest
+import Algorithm.Data.HashMap
+import Algorithm.Data.HashSet
 import Algorithm.Data.MutableQuotient
 import Algorithm.Data.PairingHeap
 import Algorithm.Data.UnionFind

Algorithm/Data/Classes/Size.lean

@@ -11,20 +11,20 @@ variable {C α : Type _}
 class Size (C : Type _) where
   size : C → Nat
   isEmpty : C → Bool
-  isEmpty_iff_size_eq_zero c : isEmpty c ↔ size c = 0
+  isEmpty_iff_size_eq_zero {c} : isEmpty c ↔ size c = 0
 export Size (size isEmpty isEmpty_iff_size_eq_zero)
 
 attribute [simp] isEmpty_iff_size_eq_zero
 
 instance : Size (List α) where
   size := List.length
   isEmpty := List.isEmpty
-  isEmpty_iff_size_eq_zero l := by cases l <;> simp
+  isEmpty_iff_size_eq_zero := by simp
 
 instance : Size (Array α) where
   size := Array.size
   isEmpty := Array.isEmpty
-  isEmpty_iff_size_eq_zero l := by simp
+  isEmpty_iff_size_eq_zero := by simp
 
 variable [Size C] (c : C)
 

Algorithm/Data/HashMap.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2024 Yuyang Zhao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuyang Zhao
+-/
+import Algorithm.Data.Classes.Dict
+
+namespace Std.HashMap
+variable {ι α : Type*} [BEq ι] [Hashable ι]
+
+instance : Size (HashMap ι α) where
+  size := size
+  isEmpty := isEmpty
+  isEmpty_iff_size_eq_zero := beq_iff_eq
+
+instance : LawfulEmptyCollection (HashMap ι α) ι where
+  not_mem_empty _ := not_mem_empty
+
+variable [LawfulBEq ι]
+
+instance : ToFinset (HashMap ι α) ι where
+  toFinset c := ⟨c.keys, by simpa [List.Nodup] using c.distinct_keys⟩
+  mem_toFinset := by simp
+  size_eq_card_toFinset := by simp [Size.size]
+
+instance : Dict (HashMap ι α) ι α where
+  setElem := insert
+  valid_setElem := by simp
+  getElem_setElem_self := by simp
+  getElem_setElem_of_ne _ _ _ _ hij := by simp [getElem_insert, hij]
+  erase := erase
+  valid_erase := by simp
+  getElem_erase_of_ne := by simp
+
+end Std.HashMap

Algorithm/Data/HashSet.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2024 Yuyang Zhao. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yuyang Zhao
+-/
+import Algorithm.Data.HashMap
+
+variable {α : Type*} [BEq α] [Hashable α]
+
+namespace Std.HashSet
+
+instance : Size (HashSet α) where
+  size := size
+  isEmpty := isEmpty
+  isEmpty_iff_size_eq_zero := beq_iff_eq
+
+instance : LawfulEmptyCollection (HashSet α) α where
+  not_mem_empty _ := not_mem_empty
+
+variable [LawfulBEq α]
+
+instance : ToFinset (HashSet α) α where
+  toFinset c := ⟨c.toList, by simpa [List.Nodup] using c.inner.distinct_keys⟩
+  mem_toFinset := by simp [toList]; rfl
+  size_eq_card_toFinset := by simp [Size.size, toList, size]
+
+instance : Erase (HashSet α) α where
+  erase := erase
+
+instance : LawfulErase (HashSet α) α := lawfulErase_iff_toFinset.mpr fun _ a ↦ by
+  ext; simp [Erase.erase, mem_erase, eq_comm (a := a)]
+
+instance : Bag (HashSet α) α where
+  toFinset_insert a c {_} := by
+    ext; simp [mem_insert, eq_comm (a := a)]
+
+end Std.HashSet

Algorithm/Data/PairingHeap.lean

@@ -170,7 +170,7 @@ lemma coe_toListUnordered_singleton (a : α) :
 instance : ToMultiset (PairingHeap α le) α where
   size x := x.size
   isEmpty x := x.isEmpty
-  isEmpty_iff_size_eq_zero x :=
+  isEmpty_iff_size_eq_zero {x} :=
     match x with
     | ⟨.nil, _⟩ | ⟨.node _ _ _, _⟩ => by
       simp [isEmpty, size, PairingHeapImp.Heap.isEmpty, PairingHeapImp.Heap.size]