feat: add decidable equality to DHashMap/HashMap/HashSet and their extensional variants (#11421)

This PR adds decidable equality to `DHashMap`/`HashMap`/`HashSet` and
their extensional variants.

Stacked on top of #11266.

src/Std/Data.lean

@@ -23,8 +23,11 @@ public import Std.Data.ExtTreeSet
 -- the well-formedness invariant, so we need to additionally import the files that deal with the
 -- unbundled version
 public import Std.Data.DHashMap.RawLemmas
+public import Std.Data.DHashMap.RawDecidableEquiv
 public import Std.Data.HashMap.RawLemmas
+public import Std.Data.HashMap.RawDecidableEquiv
 public import Std.Data.HashSet.RawLemmas
+public import Std.Data.HashSet.RawDecidableEquiv
 public import Std.Data.DTreeMap.Raw
 public import Std.Data.TreeMap.Raw
 public import Std.Data.TreeSet.Raw

src/Std/Data/DHashMap.lean

@@ -11,3 +11,4 @@ public import Std.Data.DHashMap.AdditionalOperations
 public import Std.Data.DHashMap.Iterator
 public import Std.Data.DHashMap.Lemmas
 public import Std.Data.DHashMap.IteratorLemmas
+public import Std.Data.DHashMap.DecidableEquiv

src/Std/Data/DHashMap/DecidableEquiv.lean

@@ -0,0 +1,25 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.DHashMap.Internal.RawLemmas
+
+public section
+
+/-!
+# Decidable equivalence for `DHashMap`
+-/
+
+open Std.DHashMap.Internal
+
+namespace Std.DHashMap
+
+instance {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] (m₁ m₂ : DHashMap α β) : Decidable (m₁ ~m m₂) :=
+  let : Decidable (m₁.1.Equiv m₂.1) := Raw₀.decidableEquiv ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ m₁.2 m₂.2;
+  decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+end Std.DHashMap

src/Std/Data/DHashMap/Internal/RawLemmas.lean

@@ -5158,4 +5158,12 @@ end map
 
 end Raw₀
 
+namespace Raw₀
+
+/-- Internal implementation detail -/
+def decidableEquiv [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] (m₁ m₂ : Raw₀ α β) (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : Decidable (m₁.1.Equiv m₂.1) :=
+  decidable_of_iff _ ⟨Raw₀.equiv_of_beq h₁ h₂, Raw₀.Equiv.beq h₁ h₂⟩
+
+end Raw₀
+
 end Std.DHashMap.Internal

src/Std/Data/DHashMap/RawDecidableEquiv.lean

@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.DHashMap.Internal.RawLemmas
+
+public section
+
+/-!
+# Decidable equivalence for `DHashMap.Raw`
+-/
+
+open Std.DHashMap.Internal
+
+namespace Std.DHashMap.Raw
+
+instance instDecidableEquiv {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+  Raw₀.decidableEquiv ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ h₁ h₂
+
+end Std.DHashMap.Raw

src/Std/Data/ExtDHashMap/Basic.lean

@@ -371,6 +371,9 @@ instance [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] : ReflBEq (E
 instance [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] : LawfulBEq (ExtDHashMap α β) where
   eq_of_beq {m₁} {m₂} := m₁.inductionOn₂ m₂ fun _ _ hyp => sound <| DHashMap.equiv_of_beq hyp
 
+instance {α : Type u} {β : α → Type v} [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] : DecidableEq (ExtDHashMap α β) :=
+  fun _ _ => decidable_of_iff _ beq_iff_eq
+
 namespace Const
 
 variable {β : Type v}

src/Std/Data/ExtHashMap/Basic.lean

@@ -262,6 +262,9 @@ instance [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (ExtHashMap α β) w
     simp only [mk.injEq] at |- hyp
     exact ExtDHashMap.Const.eq_of_beq _ _ hyp
 
+instance {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] : DecidableEq (ExtHashMap α β) :=
+  fun _ _ => decidable_of_iff _ beq_iff_eq
+
 @[inline, inherit_doc ExtDHashMap.inter]
 def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : ExtHashMap α β := ⟨ExtDHashMap.inter m₁.inner m₂.inner⟩
 

src/Std/Data/ExtHashSet/Basic.lean

@@ -217,6 +217,9 @@ instance [LawfulBEq α] : LawfulBEq (ExtHashSet α) where
     simp only [mk.injEq, ExtHashMap.mk.injEq] at |- hyp
     exact ExtDHashMap.Const.eq_of_beq _ _ hyp
 
+instance {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] : DecidableEq (ExtHashSet α) :=
+  fun _ _ => decidable_of_iff _ beq_iff_eq
+
 /--
 Computes the intersection of the given hash sets.
 

src/Std/Data/HashMap.lean

@@ -11,3 +11,4 @@ public import Std.Data.HashMap.AdditionalOperations
 public import Std.Data.HashMap.Iterator
 public import Std.Data.HashMap.Lemmas
 public import Std.Data.HashMap.IteratorLemmas
+public import Std.Data.HashMap.DecidableEquiv

src/Std/Data/HashMap/DecidableEquiv.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.DHashMap.DecidableEquiv
+public import Std.Data.HashMap.Basic
+
+public section
+
+/-!
+# Decidable equivalence for `HashMap`
+-/
+
+namespace Std.HashMap
+
+instance {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] (m₁ m₂ : HashMap α β) : Decidable (m₁ ~m m₂) :=
+  decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+end Std.HashMap

src/Std/Data/HashMap/RawDecidableEquiv.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.DHashMap.RawDecidableEquiv
+public import Std.Data.HashMap.Raw
+
+public section
+
+/-!
+# Decidable equivalence for `HashMap.Raw`
+-/
+
+open Std.DHashMap.Raw
+
+namespace Std.HashMap.Raw
+
+instance instDecidableEquiv {α : Type u} {β : Type v} [BEq α] [LawfulBEq α] [Hashable α] [BEq β] [LawfulBEq β] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+  let : Decidable (m₁.1 ~m m₂.1) := DHashMap.Raw.instDecidableEquiv h₁.out h₂.out;
+  decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+end Std.HashMap.Raw

src/Std/Data/HashSet.lean

@@ -10,3 +10,4 @@ public import Std.Data.HashSet.Basic
 public import Std.Data.HashSet.Iterator
 public import Std.Data.HashSet.Lemmas
 public import Std.Data.HashSet.IteratorLemmas
+public import Std.Data.HashSet.DecidableEquiv

src/Std/Data/HashSet/DecidableEquiv.lean

@@ -0,0 +1,23 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.HashMap.DecidableEquiv
+public import Std.Data.HashSet.Basic
+
+public section
+
+/-!
+# Decidable equivalence for `HashSet`
+-/
+
+namespace Std.HashSet
+
+instance {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] (m₁ m₂ : HashSet α) : Decidable (m₁ ~m m₂) :=
+  decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+end Std.HashSet

src/Std/Data/HashSet/RawDecidableEquiv.lean

@@ -0,0 +1,26 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Różowski
+-/
+module
+
+prelude
+public import Std.Data.HashMap.RawDecidableEquiv
+public import Std.Data.HashSet.Raw
+
+public section
+
+/-!
+# Decidable equivalence for `HashSet.Raw`
+-/
+
+open Std.HashMap.Raw
+
+namespace Std.HashSet.Raw
+
+instance instDecidableEquiv {α : Type u} [BEq α] [LawfulBEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : Decidable (m₁ ~m m₂) :=
+  let : Decidable (m₁.1 ~m m₂.1) := HashMap.Raw.instDecidableEquiv h₁.out h₂.out;
+  decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩
+
+end Std.HashSet.Raw

tests/lean/run/exthashset_deceq.lean

@@ -0,0 +1,24 @@
+import Std.Data.ExtHashSet
+open Std
+
+@[ext]
+structure A where
+  a : Nat
+  b : Nat
+deriving Hashable
+
+instance : BEq A where
+  beq x y := x.b == y.b && x.a == y.a
+
+@[simp]
+theorem A.beq_eq {x y : A} : (x == y) = (x.b == y.b && x.a == y.a) := rfl
+
+instance : LawfulBEq A where
+  rfl {x} := by simp
+  eq_of_beq {x y} := by grind [A.beq_eq, A.ext]
+
+instance : DecidableEq A :=
+  fun x y => by simp [A.ext_iff]; infer_instance
+
+example : Decidable (ExtHashSet.ofList [A.mk 1 2] = ExtHashSet.ofList [A.mk 1 2]) := by
+  infer_instance