From ec008ff55acd740f679969a41a91e177017147ff Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Wed, 10 Dec 2025 16:40:09 +0100 Subject: [PATCH] feat: add `BEq` to `DHashMap`/`HashMap`/`HashSet` and their extensional variants (#11266) This PR adds `BEq` instance for `DHashMap`/`HashMap`/`HashSet` and their extensional variants and proves lemmas relating it to the equivalence of hashmaps/equality of extensional variants. --- src/Init/Data/List/Perm.lean | 6 + src/Std/Data/DHashMap/Basic.lean | 13 ++ src/Std/Data/DHashMap/Internal/Defs.lean | 8 + src/Std/Data/DHashMap/Internal/Raw.lean | 8 + src/Std/Data/DHashMap/Internal/RawLemmas.lean | 47 ++++-- src/Std/Data/DHashMap/Internal/WF.lean | 22 +++ src/Std/Data/DHashMap/Lemmas.lean | 28 ++++ src/Std/Data/DHashMap/Raw.lean | 30 ++-- src/Std/Data/DHashMap/RawDef.lean | 12 ++ src/Std/Data/DHashMap/RawLemmas.lean | 36 ++++- src/Std/Data/ExtDHashMap/Basic.lean | 25 +++ src/Std/Data/ExtHashMap/Basic.lean | 13 ++ src/Std/Data/ExtHashSet/Basic.lean | 13 ++ src/Std/Data/HashMap/Basic.lean | 5 + src/Std/Data/HashMap/Lemmas.lean | 14 ++ src/Std/Data/HashMap/Raw.lean | 5 + src/Std/Data/HashMap/RawLemmas.lean | 14 ++ src/Std/Data/HashSet/Basic.lean | 11 ++ src/Std/Data/HashSet/Lemmas.lean | 14 ++ src/Std/Data/HashSet/Raw.lean | 11 ++ src/Std/Data/HashSet/RawLemmas.lean | 14 ++ src/Std/Data/Internal/List/Associative.lean | 152 ++++++++++++++++++ 22 files changed, 478 insertions(+), 23 deletions(-) diff --git a/src/Init/Data/List/Perm.lean b/src/Init/Data/List/Perm.lean index c29674071c..bc8e3d9db3 100644 --- a/src/Init/Data/List/Perm.lean +++ b/src/Init/Data/List/Perm.lean @@ -601,6 +601,12 @@ theorem sum_nat {l₁ l₂ : List Nat} (h : l₁ ~ l₂) : l₁.sum = l₂.sum : | swap => simpa [List.sum_cons] using Nat.add_left_comm .. | trans _ _ ih₁ ih₂ => simp [ih₁, ih₂] +theorem all_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.all f = l₂.all f := by + rw [Bool.eq_iff_iff]; simp [hp.mem_iff] + +theorem any_eq {l₁ l₂ : List α} {f : α → Bool} (hp : l₁.Perm l₂) : l₁.any f = l₂.any f := by + rw [Bool.eq_iff_iff]; simp [hp.mem_iff] + grind_pattern Perm.sum_nat => l₁ ~ l₂, l₁.sum grind_pattern Perm.sum_nat => l₁ ~ l₂, l₂.sum diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 53453887ef..a96418fada 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -360,6 +360,19 @@ instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩ instance [BEq α] [Hashable α] : Inter (DHashMap α β) := ⟨inter⟩ instance [BEq α] [Hashable α] : SDiff (DHashMap α β) := ⟨diff⟩ +/-- +Compares two hash maps using Boolean equality on keys and values. + +Returns `true` if the maps contain the same key-value pairs, `false` otherwise. +-/ +def beq [LawfulBEq α] [∀ k, BEq (β k)] (a b : DHashMap α β) : Bool := + Raw₀.beq ⟨a.1, a.2.size_buckets_pos⟩ ⟨b.1, b.2.size_buckets_pos⟩ + +instance [LawfulBEq α] [∀ k, BEq (β k)] : BEq (DHashMap α β) := ⟨beq⟩ + +@[inherit_doc DHashMap.beq] def Const.beq {β : Type v} [BEq α] [BEq β] (m₁ m₂ : DHashMap α (fun _ => β)) : Bool := + Raw₀.Const.beq ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 0255c6340a..c31d0fe686 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -490,6 +490,10 @@ def interSmaller [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) def inter [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := if m₁.1.size ≤ m₂.1.size then m₁.filter fun k _ => m₂.contains k else interSmaller m₁ m₂ +/-- Internal implementation detail of the hash map -/ +def beq [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] (m₁ m₂ : Raw₀ α β) : Bool := + if m₁.1.size ≠ m₂.1.size then false else m₁.1.all (fun k v => m₂.get? k == some v) + /-- Internal implementation detail of the hash map -/ @[inline] def diff [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := if m₁.1.size ≤ m₂.1.size then m₁.filter (fun k _ => !m₂.contains k) else (eraseManyEntries m₁ m₂.1).1 @@ -505,6 +509,10 @@ def Const.get? [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) : O let ⟨i, h⟩ := mkIdx buckets.size h (hash a) buckets[i].get? a +/-- Internal implementation detail of the hash map -/ +def Const.beq [BEq α] [Hashable α] [BEq β] (m₁ m₂ : Raw₀ α (fun _ => β)) : Bool := + if m₁.1.size ≠ m₂.1.size then false else m₁.1.all (fun k v => Const.get? m₂ k == some v) + /-- Internal implementation detail of the hash map -/ def Const.get [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) (hma : m.contains a) : β := diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index 89357c414a..254694ed06 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -154,6 +154,14 @@ theorem inter_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) m₁.inter m₂ = Raw₀.inter ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by simp [Raw.inter, h₁.size_buckets_pos, h₂.size_buckets_pos] +theorem beq_eq [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : + m₁.beq m₂ = Raw₀.beq ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by + simp [Raw.beq, h₁.size_buckets_pos, h₂.size_buckets_pos] + +theorem Const.beq_eq {β : Type v} [BEq α] [Hashable α] [BEq β] {m₁ m₂ : Raw α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) : + Raw.Const.beq m₁ m₂ = Raw₀.Const.beq ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by + simp [Raw.Const.beq, h₁.size_buckets_pos, h₂.size_buckets_pos] + theorem diff_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.diff m₂ = Raw₀.diff ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by simp [Raw.diff, h₁.size_buckets_pos, h₂.size_buckets_pos] diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 9fd7f20c7f..db6918675d 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -11,6 +11,7 @@ import all Std.Data.DHashMap.Internal.Defs public import Std.Data.DHashMap.Internal.WF import all Std.Data.DHashMap.Raw import all Std.Data.DHashMap.Basic +import all Std.Data.DHashMap.RawDef meta import Std.Data.DHashMap.Basic public section @@ -162,7 +163,10 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T ⟨`getEntry?, (``getEntry?_eq_getEntry?, #[`(getEntry?_of_perm _)])⟩, ⟨`getEntryD, (``getEntryD_eq_getEntryD, #[`(getEntryD_of_perm _)])⟩, ⟨`getEntry!, (``getEntry!_eq_getEntry!, #[`(getEntry!_of_perm _)])⟩, + ⟨`all, (``Raw.all_eq_all_toListModel, #[])⟩, ⟨`toList, (``Raw.toList_eq_toListModel, #[])⟩, + ⟨`Const.beq, (``Raw₀.Const.beq_eq_beqModel, #[])⟩, + ⟨`beq, (``beq_eq_beqModel, #[])⟩, ⟨`keys, (``Raw.keys_eq_keys_toListModel, #[`(perm_keys_congr_left)])⟩, ⟨`Const.toList, (``Raw.Const.toList_eq_toListModel_map, #[`(perm_map_congr_left)])⟩, ⟨`foldM, (``Raw.foldM_eq_foldlM_toListModel, #[])⟩, @@ -1453,16 +1457,7 @@ theorem any_eq_false [LawfulBEq α] {p : (a : α) → β a → Bool} (h : m.1.WF omit [Hashable α] [BEq α] in theorem all_toList {p : (a : α) → β a → Bool} : m.1.toList.all (fun x => p x.1 x.2) = m.1.all p := by - simp only [Raw.all, ForIn.forIn, Bool.not_eq_true, bind_pure_comp, map_pure, Id.run_bind] - rw [forIn_eq_forIn_toList, forIn_eq_forIn'] - induction m.val.toList with - | nil => simp - | cons hd tl ih => - simp only [forIn'_eq_forIn, List.all_cons] - by_cases h : p hd.fst hd.snd = false - · simp [h] - · simp only [forIn'_eq_forIn] at ih - simp [h, ih] + simp_to_model omit [Hashable α] [BEq α] in theorem all_eq_not_any_not {p : (a : α) → β a → Bool} : @@ -2590,8 +2585,38 @@ end Const end insertMany -section Union +section BEq +variable {m₁ m₂ : Raw₀ α β} [LawfulBEq α] [∀ k, BEq (β k)] +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : m₁.1.Equiv m₂.1 → beq m₁ m₂ := by + simp_to_model using List.beqModel_eq_true_of_perm + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : beq m₁ m₂ = true → m₁.1.Equiv m₂.1 := by + simp_to_model using List.perm_of_beqModel + +theorem Equiv.beq_congr {m₃ m₄ : Raw₀ α β} (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) : + m₁.1.Equiv m₃.1 → m₂.1.Equiv m₄.1 → Raw₀.beq m₁ m₂ = Raw₀.beq m₃ m₄ := by + simp_to_model using List.beqModel_congr + +end BEq + +section + +variable {β : Type v} {m₁ m₂ : Raw₀ α (fun _ => β)} + +theorem Const.Equiv.beq [LawfulHashable α] [EquivBEq α] [BEq β] [ReflBEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : m₁.1.Equiv m₂.1 → Const.beq m₁ m₂ := by + simp_to_model using List.Const.beqModel_eq_true_of_perm + +theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : beq m₁ m₂ = true → m₁.1.Equiv m₂.1 := by + simp_to_model using List.Const.perm_of_beqModel + +theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw₀ α (fun _ => β)} [BEq β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) : + m₁.1.Equiv m₃.1 → m₂.1.Equiv m₄.1 → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by + simp_to_model using List.Const.beqModel_congr + +end + +section Union variable (m₁ m₂ : Raw₀ α β) variable {m₁ m₂} diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index 3cc125dabd..f80d5659f8 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -275,6 +275,19 @@ theorem forIn_eq_forIn_toListModel {δ : Type w} {l : Raw α β} {m : Type w → · simp · simpa using ih' +theorem all_eq_all_toListModel {p : (a: α) → β a → Bool} {m : Raw α β} : + m.all p = (toListModel m.buckets).all (fun x => p x.1 x.2) := by + simp only [Raw.all, ForIn.forIn, Bool.not_eq_true, bind_pure_comp, map_pure, Id.run_bind] + rw [forIn_eq_forIn_toListModel, ← toList_eq_toListModel, forIn_eq_forIn'] + induction m.toList with + | nil => simp only [all_nil, forIn'_nil, Id.run_pure] + | cons hd tl ih => + simp only [forIn'_eq_forIn, List.all_cons] + by_cases h : p hd.fst hd.snd = false + · simp [h] + · simp only [forIn'_eq_forIn] at ih + simp [h, ih] + end Raw namespace Raw₀ @@ -1584,4 +1597,13 @@ theorem Const.wf_insertManyIfNewUnit₀ [BEq α] [Hashable α] [EquivBEq α] [La {l : ρ} (h' : m.WF) : (Const.insertManyIfNewUnit ⟨m, h⟩ l).1.1.WF := (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).2 _ Raw.WF.insertIfNew₀ h' +theorem beq_eq_beqModel [BEq α] [LawfulBEq α] [Hashable α] [∀ k, BEq (β k)] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) : + beq m₁ m₂ = beqModel (toListModel m₁.1.buckets) (toListModel m₂.1.buckets) := by + simp [beq, beqModel, Raw.size_eq_length h₁, Raw.size_eq_length h₂, Raw.all_eq_all_toListModel, + get?_eq_getValueCast? h₂] + +theorem Const.beq_eq_beqModel {β : Type v} [BEq α] [PartialEquivBEq α] [Hashable α] [LawfulHashable α] [BEq β] {m₁ m₂ : Raw₀ α (fun _ => β)} (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) : + beq m₁ m₂ = Const.beqModel (toListModel m₁.1.buckets) (toListModel m₂.1.buckets) := by + simp [beq, Const.beqModel, Raw.size_eq_length h₁, Raw.size_eq_length h₂, Raw.all_eq_all_toListModel, get?_eq_getValue? h₂] + end Raw₀ diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index e5ee617497..a1563b6d26 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -1840,6 +1840,34 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] {l : ρ} : (m.insertMany l).isEmpty → m.isEmpty := Raw₀.isEmpty_of_isEmpty_insertMany ⟨m.1, _⟩ m.2 +section BEq +variable {m₁ m₂ : DHashMap α β} [LawfulBEq α] [∀ k, BEq (β k)] + +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h : m₁ ~m m₂) : m₁ == m₂ := + Raw₀.Equiv.beq m₁.2 m₂.2 h.1 + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨Raw₀.equiv_of_beq m₁.2 m₂.2 h⟩ + +theorem Equiv.beq_congr {m₃ m₄ : DHashMap α β} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + Raw₀.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1 + +end BEq + +section +variable {β : Type v} {m₁ m₂ : DHashMap α (fun _ => β)} [BEq β] + +theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [ReflBEq β] (h : m₁ ~m m₂) : DHashMap.Const.beq m₁ m₂ := + Raw₀.Const.Equiv.beq m₁.2 m₂.2 h.1 + +theorem Const.equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : Const.beq m₁ m₂) : m₁ ~m m₂ := + ⟨Raw₀.Const.equiv_of_beq m₁.2 m₂.2 h⟩ + +theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : DHashMap α (fun _ => β)} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Const.beq m₁ m₂ = Const.beq m₃ m₄ := + Raw₀.Const.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1 + +end + section Union variable (m₁ m₂ : DHashMap α β) diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index fff6248267..d3a5363700 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -476,17 +476,6 @@ only those mappings where the function returns `some` value. @[inline] def keysArray (m : Raw α β) : Array α := m.fold (fun acc k _ => acc.push k) (.emptyWithCapacity m.size) -/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails. -/ -@[inline] def all (m : Raw α β) (p : (a : α) → β a → Bool) : Bool := Id.run do - for a in m do - if ¬ p a.1 a.2 then return false - return true - -/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/ -@[inline] def any (m : Raw α β) (p : (a : α) → β a → Bool) : Bool := Id.run do - for a in m do - if p a.1 a.2 then return true - return false /-- Computes the union of the given hash maps. If a key appears in both maps, the entry contained in the second argument will appear in the result. @@ -522,6 +511,25 @@ This function always merges the smaller map into the larger map, so the expected instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩ +/-- +Compares two hash maps using Boolean equality on keys and values. + +Returns `true` if the maps contain the same key-value pairs, `false` otherwise. +-/ +def beq [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] (m₁ m₂ : Raw α β) : Bool := + if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then + Raw₀.beq ⟨m₁, h.1⟩ ⟨m₂, h.2⟩ + else + false + +instance [BEq α] [Hashable α] [LawfulBEq α] [∀ k, BEq (β k)] : BEq (Raw α β) := ⟨beq⟩ + +@[inherit_doc DHashMap.Raw.beq] def Const.beq {β : Type v} [BEq α] [Hashable α] [BEq β] (m₁ m₂ : Raw α (fun _ => β)) : Bool := + if h : 0 < m₁.buckets.size ∧ 0 < m₂.buckets.size then + Raw₀.Const.beq ⟨m₁, h.1⟩ ⟨m₂, h.2⟩ + else + false + /-- Computes the difference of the given hash maps. diff --git a/src/Std/Data/DHashMap/RawDef.lean b/src/Std/Data/DHashMap/RawDef.lean index da98931f82..4f6d26b7d3 100644 --- a/src/Std/Data/DHashMap/RawDef.lean +++ b/src/Std/Data/DHashMap/RawDef.lean @@ -81,6 +81,18 @@ instance [Monad m] : ForM m (Raw α β) ((a : α) × β a) where instance [Monad m] : ForIn m (Raw α β) ((a : α) × β a) where forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init +/-- Checks if all elements satisfy the predicate, short-circuiting if a predicate fails. -/ +@[inline] def all (m : Raw α β) (p : (a : α) → β a → Bool) : Bool := Id.run do + for a in m do + if ¬ p a.1 a.2 then return false + return true + +/-- Checks if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/ +@[inline] def any (m : Raw α β) (p : (a : α) → β a → Bool) : Bool := Id.run do + for a in m do + if p a.1 a.2 then return true + return false + end Raw end Std.DHashMap diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index c035560fa9..ea96f2f976 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -48,7 +48,7 @@ private meta def baseNames : Array Name := ``getKey?_eq, ``getKey_eq, ``getKey!_eq, ``getKeyD_eq, ``insertMany_eq, ``Const.insertMany_eq, ``Const.insertManyIfNewUnit_eq, ``ofArray_eq, ``Const.ofArray_eq, ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq, ``Const.unitOfArray_eq, - ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq, ``inter_eq, ``diff_eq] + ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq, ``inter_eq, ``diff_eq, ``beq_eq, ``Const.beq_eq] /-- Internal implementation detail of the hash map -/ @@ -3761,6 +3761,40 @@ variable [BEq α] [Hashable α] open Internal.Raw Internal.Raw₀ +section BEq +variable {m₁ m₂ : Raw α β} [LawfulBEq α] [∀ k, BEq (β k)] + +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ := by + simp only [BEq.beq] + simp_to_raw using Raw₀.Equiv.beq + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ := by + revert h + simp only [BEq.beq] + simp_to_raw using Raw₀.equiv_of_beq + +theorem Equiv.beq_congr {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := by + simp only [BEq.beq] + simp_to_raw using Raw₀.Equiv.beq_congr + +end BEq + +section + +variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β)} + +theorem Const.Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := by + simp_to_raw using Raw₀.Const.Equiv.beq + +theorem Const.equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : beq m₁ m₂ = true) : m₁ ~m m₂ := by + revert h + simp_to_raw using Raw₀.Const.equiv_of_beq + +theorem Const.Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ := by + simp_to_raw using Raw₀.Const.Equiv.beq_congr + +end + @[simp, grind =] theorem ofArray_eq_ofList (a : Array ((a : α) × (β a))) : ofArray a = ofList a.toList := by diff --git a/src/Std/Data/ExtDHashMap/Basic.lean b/src/Std/Data/ExtDHashMap/Basic.lean index bf39770e67..a0b3582fdf 100644 --- a/src/Std/Data/ExtDHashMap/Basic.lean +++ b/src/Std/Data/ExtDHashMap/Basic.lean @@ -362,6 +362,31 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : Ex instance [EquivBEq α] [LawfulHashable α] : Union (ExtDHashMap α β) := ⟨union⟩ +instance [LawfulBEq α] [∀ k, BEq (β k)] : BEq (ExtDHashMap α β) where + beq m₁ m₂ := lift₂ (fun x y : DHashMap α β => x.beq y) (fun _ _ _ _ => DHashMap.Equiv.beq_congr) m₁ m₂ + +instance [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] : ReflBEq (ExtDHashMap α β) where + rfl {a} := a.inductionOn fun x => DHashMap.Equiv.beq <| DHashMap.Equiv.refl x + +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 + +namespace Const + +variable {β : Type v} + +@[inline, inherit_doc DHashMap.beq] +def beq [EquivBEq α] [LawfulHashable α] [BEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) : Bool := + lift₂ (fun x y : DHashMap α fun _ => β => DHashMap.Const.beq x y) (fun _ _ _ _ => DHashMap.Const.Equiv.beq_congr) m₁ m₂ + +theorem beq_of_eq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) : m₁ = m₂ → Const.beq m₁ m₂ := + m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.Equiv.beq <| exact h + +theorem eq_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDHashMap α fun _ => β) : Const.beq m₁ m₂ → m₁ = m₂ := + m₁.inductionOn₂ m₂ fun _ _ h => sound <| DHashMap.Const.equiv_of_beq h + +end Const + @[inline, inherit_doc DHashMap.inter] def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : ExtDHashMap α β := lift₂ (fun x y : DHashMap α β => mk (x.inter y)) (fun a b c d equiv₁ equiv₂ => by diff --git a/src/Std/Data/ExtHashMap/Basic.lean b/src/Std/Data/ExtHashMap/Basic.lean index dabe67d7ea..f17a5b712c 100644 --- a/src/Std/Data/ExtHashMap/Basic.lean +++ b/src/Std/Data/ExtHashMap/Basic.lean @@ -249,6 +249,19 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : Ext instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashMap α β) := ⟨union⟩ +instance [EquivBEq α] [LawfulHashable α] [BEq β] : BEq (ExtHashMap α β) where + beq m₁ m₂ := ExtDHashMap.Const.beq m₁.inner m₂.inner + +instance [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] : ReflBEq (ExtHashMap α β) where + rfl := ExtDHashMap.Const.beq_of_eq _ _ rfl + +instance [LawfulBEq α] [BEq β] [LawfulBEq β] : LawfulBEq (ExtHashMap α β) where + eq_of_beq {a} {b} hyp := by + have ⟨_⟩ := a + have ⟨_⟩ := b + simp only [mk.injEq] at |- hyp + exact ExtDHashMap.Const.eq_of_beq _ _ hyp + @[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 7d38884628..6590000bec 100644 --- a/src/Std/Data/ExtHashSet/Basic.lean +++ b/src/Std/Data/ExtHashSet/Basic.lean @@ -204,6 +204,19 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : ExtHas instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashSet α) := ⟨union⟩ +instance [EquivBEq α] [LawfulHashable α] : BEq (ExtHashSet α) where + beq m₁ m₂ := ExtDHashMap.Const.beq m₁.inner.inner m₂.inner.inner + +instance [EquivBEq α] [LawfulHashable α] : ReflBEq (ExtHashSet α) where + rfl := ExtDHashMap.Const.beq_of_eq _ _ rfl + +instance [LawfulBEq α] : LawfulBEq (ExtHashSet α) where + eq_of_beq {a} {b} hyp := by + have ⟨⟨_⟩⟩ := a + have ⟨⟨_⟩⟩ := b + simp only [mk.injEq, ExtHashMap.mk.injEq] at |- hyp + exact ExtDHashMap.Const.eq_of_beq _ _ hyp + /-- Computes the intersection of the given hash sets. diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 769c49f3f6..ab1d167bc3 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -278,6 +278,11 @@ instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩ instance [BEq α] [Hashable α] : Inter (HashMap α β) := ⟨inter⟩ +@[inherit_doc DHashMap.beq] def beq {β : Type v} [BEq α] [BEq β] (m₁ m₂ : HashMap α β) : Bool := + DHashMap.Const.beq m₁.inner m₂.inner + +instance [BEq α] [BEq β] : BEq (HashMap α β) := ⟨beq⟩ + @[inherit_doc DHashMap.inter, inline] def diff [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β := ⟨DHashMap.diff m₁.inner m₂.inner⟩ diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 7446672161..ca9d9df352 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -1346,6 +1346,20 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := DHashMap.Const.isEmpty_of_isEmpty_insertMany +section +variable {β : Type v} {m₁ m₂ : HashMap α β} [BEq β] + +theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [ReflBEq β] (h : m₁ ~m m₂) : m₁ == m₂ := + DHashMap.Const.Equiv.beq h.1 + +theorem equiv_of_beq [LawfulBEq α] [LawfulBEq β] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨DHashMap.Const.equiv_of_beq h⟩ + +theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashMap α β} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + DHashMap.Const.Equiv.beq_congr w₁.1 w₂.1 + +end + section Union variable {β : Type v} diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 3b599e1d99..48b60d460e 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -250,6 +250,11 @@ instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩ instance [BEq α] [Hashable α] : SDiff (Raw α β) := ⟨diff⟩ +@[inherit_doc DHashMap.Raw.beq] def beq {β : Type v} [BEq α] [Hashable α] [BEq β] (m₁ m₂ : Raw α β) : Bool := + DHashMap.Raw.Const.beq m₁.inner m₂.inner + +instance [BEq α] [Hashable α] [BEq β] : BEq (Raw α β) := ⟨beq⟩ + section Unverified @[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ) diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 1a259c4ae5..8e6316db9d 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1308,6 +1308,20 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := DHashMap.Raw.Const.isEmpty_of_isEmpty_insertMany h.out +section +variable {β : Type v} {m₁ m₂ : Raw α β} + +theorem Equiv.beq [EquivBEq α] [LawfulHashable α] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ := + DHashMap.Raw.Const.Equiv.beq h₁.1 h₂.1 h.1 + +theorem equiv_of_beq [LawfulBEq α] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨DHashMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 h⟩ + +theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] [BEq β] {m₃ m₄ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + DHashMap.Raw.Const.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1 + +end + section Union variable {β : Type v} diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 12abbf50c8..5ee9a33425 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -259,6 +259,17 @@ This function always iterates through the smaller set, so the expected runtime i instance [BEq α] [Hashable α] : Inter (HashSet α) := ⟨inter⟩ + +/-- +Compares two hash sets using Boolean equality on keys. + +Returns `true` if the sets contain the same keys, `false` otherwise. +-/ +def beq [BEq α] (m₁ m₂ : HashSet α) : Bool := + HashMap.beq m₁.inner m₂.inner + +instance [BEq α] : BEq (HashSet α) := ⟨beq⟩ + /-- Computes the difference of the given hash sets. diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 026824df69..a41d501561 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -784,6 +784,20 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] end +section +variable {m₁ m₂ : HashSet α} + +theorem Equiv.beq [EquivBEq α] [LawfulHashable α] (h : m₁ ~m m₂) : m₁ == m₂ := + HashMap.Equiv.beq h.1 + +theorem equiv_of_beq [LawfulBEq α] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨HashMap.equiv_of_beq h⟩ + +theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : HashSet α} (h₁ : m₁ ~m m₃) (h₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + HashMap.Equiv.beq_congr h₁.1 h₂.1 + +end + section Union variable (m₁ m₂ : HashSet α) diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index dca7b03a30..ac51893bdb 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -243,6 +243,17 @@ This function always merges the smaller set into the larger set, so the expected instance [BEq α] [Hashable α] : Inter (Raw α) := ⟨inter⟩ + +/-- +Compares two hash sets using Boolean equality on keys. + +Returns `true` if the sets contain the same keys, `false` otherwise. +-/ +def beq [BEq α] [Hashable α] (m₁ m₂ : Raw α) : Bool := + HashMap.Raw.beq m₁.inner m₂.inner + +instance [BEq α] [Hashable α] : BEq (Raw α) := ⟨beq⟩ + /-- Computes the difference of the given hash sets. diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index eeda79bc08..7bb0bf4c62 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -816,6 +816,20 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := HashMap.Raw.isEmpty_of_isEmpty_insertManyIfNewUnit h.out +section +variable {m₁ m₂ : Raw α} + +theorem Equiv.beq [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := + HashMap.Raw.Equiv.beq h₁.1 h₂.1 h.1 + +theorem equiv_of_beq [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨HashMap.Raw.equiv_of_beq h₁.1 h₂.1 h⟩ + +theorem Equiv.beq_congr [EquivBEq α] [LawfulHashable α] {m₃ m₄ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + HashMap.Raw.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1 + +end + section Union variable (m₁ m₂ : Raw α) diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index eb81d1dc2f..a3cc3a8573 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -257,6 +257,10 @@ end | ⟨k, v⟩ :: l => if h : k == a then some (cast (congrArg β (eq_of_beq h)) v) else getValueCast? a l +/-- Internal implementation detail of the hash map -/ +def beqModel [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] (l₁ l₂ : List ((a : α) × β a)) := + if l₁.length ≠ l₂.length then false else (l₁.all fun x => getValueCast? x.fst l₂ == some x.snd) + @[simp] theorem getValueCast?_nil [BEq α] [LawfulBEq α] {a : α} : getValueCast? a ([] : List ((a : α) × β a)) = none := rfl theorem getValueCast?_cons [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k} : @@ -285,6 +289,10 @@ section variable {β : Type v} +/-- Internal implementation detail of the hash map -/ +def Const.beqModel [BEq α] [BEq β] (l₁ l₂ : List ((_ : α) × β)) := + if l₁.length ≠ l₂.length then false else (l₁.all fun x => getValue? x.fst l₂ == some x.snd) + /-- This is a strange dependent version of `Option.map` in which the mapping function is allowed to "know" about the option that is being mapped. This happens to be useful in this file (see `getValueCast_eq_getEntry?`), but we do not want it to leak out of the file. -/ @@ -3569,6 +3577,71 @@ theorem insertList_insertEntry_right_equiv_insertEntry_insertList [BEq α] [Equi . simp only [Option.some_or] . rw [@getEntry?_insertList α β _ _ l toInsert distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) a] +theorem length_le_length_of_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} + (dl₁ : DistinctKeys l₁) + (dl₂ : DistinctKeys l₂) + (h : ∀ a, containsKey a l₁ → containsKey a l₂) : + l₁.length ≤ l₂.length := by + induction l₁ generalizing l₂ with + | nil => simp + | cons hd tl ih => + have hc := h hd.1 (by rw [containsKey_cons_self]) + suffices tl.length ≤ (eraseKey hd.1 l₂).length by + rw [List.length_eraseKey, hc] at this + simp only [↓reduceIte] at this + simp only [List.length_cons, ge_iff_le] + have : l₂.length > 0 := by cases l₂ <;> simp_all + omega + apply ih + · rw [List.distinctKeys_cons_iff] at dl₁ + exact dl₁.1 + · exact DistinctKeys.eraseKey dl₂ + · intro a mem + rw [containsKey_eraseKey] + · simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true] + apply And.intro + · rw [List.distinctKeys_cons_iff] at dl₁ + apply Classical.byContradiction + intro hyp + simp only [Bool.not_eq_false] at hyp + rw [containsKey_congr hyp] at dl₁ + rw [dl₁.2] at mem + contradiction + · specialize h a + rw [containsKey_cons] at h + apply h + simp [mem] + · exact dl₂ + +theorem containsKey_of_length_eq [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) (dl₂ : DistinctKeys l₂) (hl : l₂.length = l₁.length) (hs : ∀ (a : α), containsKey a l₁ → containsKey a l₂) : ∀ (a : α), containsKey a l₂ → containsKey a l₁ := by + intro a ha + apply Classical.byContradiction + intro hb + simp only [Bool.not_eq_true] at hb + suffices l₁.length < l₂.length by omega + suffices l₁.length ≤ (eraseKey a l₂).length ∧ 1 + (eraseKey a l₂).length = l₂.length by omega + apply And.intro + · apply length_le_length_of_containsKey dl₁ (DistinctKeys.eraseKey dl₂) + intro a₂ mem₂ + rw [containsKey_eraseKey dl₂] + simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true] + apply And.intro + · apply Classical.byContradiction + intro hyp + simp only [Bool.not_eq_false] at hyp + rw [containsKey_congr hyp] at hb + rw [hb] at mem₂ + contradiction + · apply hs + exact mem₂ + · simp only [length_eraseKey, ha, ↓reduceIte] + have : l₂.length > 0 := by + cases l₂ with + | nil => simp at ha + | _ => simp + omega + section variable {β : Type v} @@ -7557,6 +7630,85 @@ theorem isEmpty_filter_key_iff [BEq α] [EquivBEq α] {f : α → Bool} simp only [getKey, getKey?_eq_getEntry?, this] at h exact h +theorem beqModel_eq_true_of_perm [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) : l₁.Perm l₂ → beqModel l₁ l₂ := by + intro hyp + rw [beqModel, if_neg (by simpa using hyp.length_eq)] + simp only [List.all_eq_true] + intro ⟨k,v⟩ mem + have hv := getValueCast_of_mem mem + have hc := containsKey_of_mem mem + apply beq_of_eq + simp only at |- hc hv + rw [← hv, ← getValueCast?_eq_some_getValueCast] + · symm + apply getValueCast?_of_perm hl₁ hyp + · exact hl₁ + +theorem Const.beqModel_eq_true_of_perm {β : Type v} [BEq α] [EquivBEq α] [BEq β] [ReflBEq β] {l₁ l₂ : List ((_ : α) × β )} (hl₁ : DistinctKeys l₁) : l₁.Perm l₂ → Const.beqModel l₁ l₂ := by + intro hyp + rw [beqModel, if_neg (by simpa using hyp.length_eq)] + simp only [List.all_eq_true] + intro ⟨k,v⟩ mem + have hv := @getValue_of_mem α β _ _ l₁ ⟨k,v⟩ mem + have hc := containsKey_of_mem mem + apply beq_of_eq + simp only at |- hc hv + rw [← hv, ← getValue?_eq_some_getValue] + · symm + apply getValue?_of_perm hl₁ hyp + · exact hl₁ + · exact hc + +theorem perm_of_beqModel [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) : beqModel l₁ l₂ → l₁.Perm l₂ := by + simp only [beqModel, ne_eq, ite_not, Bool.if_false_right, Bool.and_eq_true, decide_eq_true_eq, + List.all_eq_true, beq_iff_eq, and_imp] + intro he hyp + apply getValueCast?_ext hl₁ hl₂ + intro a + have hyp2 : ∀ (a : α) (h : containsKey a l₁), (getValueCast? a l₂ == getValueCast? a l₁) = true := by + intro a mem + rw [getValueCast?_eq_some_getValueCast mem] + apply beq_of_eq + specialize hyp ⟨a, getValueCast a l₁ mem⟩ (List.getValueCast_mem mem) + simpa using hyp + by_cases hc₁ : containsKey a l₁ + case pos => + exact eq_of_beq <| BEq.symm <| hyp2 _ hc₁ + case neg => + rw [Bool.not_eq_true] at hc₁ + by_cases hc₂ : containsKey a l₂ + case pos => + suffices (∀ (a : α), containsKey a l₁ = true → containsKey a l₂ = true) by + rw [containsKey_of_length_eq hl₁ hl₂ he.symm this a hc₂] at hc₁ + contradiction + intro k' mem + apply List.containsKey_of_getValueCast?_eq_some + simpa [getValueCast?_eq_some_getValueCast mem] using eq_of_beq <| hyp2 k' mem + case neg => + rw [Bool.not_eq_true] at hc₂ + rw [getValueCast?_eq_none hc₁, getValueCast?_eq_none hc₂] + +theorem beqModel_congr [BEq α] [LawfulBEq α] [∀ k, BEq (β k)] {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} + (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by + simp only [beqModel, ne_eq, ite_not, Bool.if_false_right, Perm.length_eq p₁, Perm.length_eq p₂] + suffices h : (l₁.all fun x => getValueCast? x.fst l₂ == some x.snd) = (l₃.all fun x => getValueCast? x.fst l₄ == some x.snd) by simp [h] + simp [getValueCast?_of_perm hl p₂, List.Perm.all_eq p₁] + +theorem Const.beqModel_congr {β : Type v} [BEq α] [EquivBEq α] [BEq β] {l₁ l₂ l₃ l₄ : List ((_ : α) × β)} + (hl : DistinctKeys l₂) (p₁ : l₁.Perm l₃) (p₂ : l₂.Perm l₄) : beqModel l₁ l₂ = beqModel l₃ l₄ := by + simp only [beqModel, ne_eq, ite_not, Bool.if_false_right, Perm.length_eq p₁, Perm.length_eq p₂] + suffices h : (l₁.all fun x => getValue? x.fst l₂ == some x.snd) = (l₃.all fun x => getValue? x.fst l₄ == some x.snd) by simp [h] + simp [getValue?_of_perm hl p₂, List.Perm.all_eq p₁] + +theorem beqModel_eq_constBeqModel {β : Type v} [BEq α] [LawfulBEq α] [BEq β] {l₁ l₂ : List ((_ : α) × β)} : beqModel l₁ l₂ = Const.beqModel l₁ l₂ := by + simp [beqModel, Const.beqModel, getValue?_eq_getValueCast?] + +theorem Const.perm_of_beqModel {β : Type v} [BEq α] [LawfulBEq α] [BEq β] [LawfulBEq β] {l₁ l₂ : List ((_ : α) × β)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) : + beqModel l₁ l₂ → l₁.Perm l₂ := by + rw [← beqModel_eq_constBeqModel] + intro hyp + apply List.perm_of_beqModel hl₁ hl₂ hyp + namespace Const theorem getKey_getValue_mem [BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {k : α} {h} :