diff --git a/src/Std/Data.lean b/src/Std/Data.lean index 0479b505e7d3..47f60a9ff28b 100644 --- a/src/Std/Data.lean +++ b/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 diff --git a/src/Std/Data/DHashMap.lean b/src/Std/Data/DHashMap.lean index 03860f758875..a25cddf7ddf6 100644 --- a/src/Std/Data/DHashMap.lean +++ b/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 diff --git a/src/Std/Data/DHashMap/DecidableEquiv.lean b/src/Std/Data/DHashMap/DecidableEquiv.lean new file mode 100644 index 000000000000..64e0419828f8 --- /dev/null +++ b/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} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β 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 diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index db6918675d0a..3ce132c8a833 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -5138,4 +5138,12 @@ end map end Raw₀ +namespace Raw₀ + +/-- Internal implementation detail -/ +def decidableEquiv [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β 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 diff --git a/src/Std/Data/DHashMap/RawDecidableEquiv.lean b/src/Std/Data/DHashMap/RawDecidableEquiv.lean new file mode 100644 index 000000000000..5c8c803ac8bb --- /dev/null +++ b/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} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β 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 diff --git a/src/Std/Data/ExtDHashMap/Basic.lean b/src/Std/Data/ExtDHashMap/Basic.lean index a0b3582fdf23..7984cd8f4ed4 100644 --- a/src/Std/Data/ExtDHashMap/Basic.lean +++ b/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} [DecidableEq α] [Hashable α] [∀ k, DecidableEq (β k)] : DecidableEq (ExtDHashMap α β) := + fun _ _ => decidable_of_iff _ beq_iff_eq + namespace Const variable {β : Type v} diff --git a/src/Std/Data/ExtHashMap/Basic.lean b/src/Std/Data/ExtHashMap/Basic.lean index f17a5b712c2f..226588808ab1 100644 --- a/src/Std/Data/ExtHashMap/Basic.lean +++ b/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} [DecidableEq α] [Hashable α] [DecidableEq β] : 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⟩ diff --git a/src/Std/Data/ExtHashSet/Basic.lean b/src/Std/Data/ExtHashSet/Basic.lean index 6590000bec56..1f2d2f04f456 100644 --- a/src/Std/Data/ExtHashSet/Basic.lean +++ b/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} [DecidableEq α] [Hashable α] : DecidableEq (ExtHashSet α) := + fun _ _ => decidable_of_iff _ beq_iff_eq + /-- Computes the intersection of the given hash sets. diff --git a/src/Std/Data/HashMap.lean b/src/Std/Data/HashMap.lean index 02b56e2ec617..04e3a2086bec 100644 --- a/src/Std/Data/HashMap.lean +++ b/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 diff --git a/src/Std/Data/HashMap/DecidableEquiv.lean b/src/Std/Data/HashMap/DecidableEquiv.lean new file mode 100644 index 000000000000..a3149244d3c7 --- /dev/null +++ b/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} [DecidableEq α] [Hashable α] [DecidableEq β] (m₁ m₂ : HashMap α β) : Decidable (m₁ ~m m₂) := + decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩ + +end Std.HashMap diff --git a/src/Std/Data/HashMap/RawDecidableEquiv.lean b/src/Std/Data/HashMap/RawDecidableEquiv.lean new file mode 100644 index 000000000000..cf8a667e87d3 --- /dev/null +++ b/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} [DecidableEq α] [Hashable α] [DecidableEq β] {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 diff --git a/src/Std/Data/HashSet.lean b/src/Std/Data/HashSet.lean index c81d347feef5..adc683d5d71b 100644 --- a/src/Std/Data/HashSet.lean +++ b/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 diff --git a/src/Std/Data/HashSet/DecidableEquiv.lean b/src/Std/Data/HashSet/DecidableEquiv.lean new file mode 100644 index 000000000000..8baa49a051f2 --- /dev/null +++ b/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} [DecidableEq α] [Hashable α] (m₁ m₂ : HashSet α) : Decidable (m₁ ~m m₂) := + decidable_of_iff _ ⟨fun h => ⟨h⟩, fun h => h.1⟩ + +end Std.HashSet diff --git a/src/Std/Data/HashSet/RawDecidableEquiv.lean b/src/Std/Data/HashSet/RawDecidableEquiv.lean new file mode 100644 index 000000000000..fa8d1f9827c1 --- /dev/null +++ b/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} [DecidableEq α] [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