From 9e4f9d317bd5b27bd43b76ba811fdf8a9f6d279e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Fri, 12 Dec 2025 09:30:36 +0100 Subject: [PATCH] feat: add BEq to `DTreeMap`/`TreeMap`/`TreeSet` and their extensional variants (#11404) This PR adds BEq instance for `DTreeMap`/`TreeMap`/`TreeSet` and their extensional variants and proves lemmas relating it to the equivalence of hashmaps/equality of extensional variants. Stacked on top of #11266 --- src/Std/Data/DTreeMap/Basic.lean | 23 +++++++----- src/Std/Data/DTreeMap/Internal/Lemmas.lean | 33 +++++++++++++++++ .../Data/DTreeMap/Internal/Operations.lean | 9 +++++ src/Std/Data/DTreeMap/Internal/Queries.lean | 14 ++++++++ src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean | 23 ++++++++++++ src/Std/Data/DTreeMap/Lemmas.lean | 34 ++++++++++++++++-- src/Std/Data/DTreeMap/Raw/Basic.lean | 19 ++++++---- src/Std/Data/DTreeMap/Raw/Lemmas.lean | 36 +++++++++++++++++-- src/Std/Data/ExtDTreeMap/Basic.lean | 24 +++++++++++++ src/Std/Data/ExtTreeMap/Basic.lean | 13 +++++++ src/Std/Data/ExtTreeSet/Basic.lean | 13 +++++++ src/Std/Data/TreeMap/Basic.lean | 5 +++ src/Std/Data/TreeMap/Lemmas.lean | 15 ++++++++ src/Std/Data/TreeMap/Raw/Basic.lean | 5 +++ src/Std/Data/TreeMap/Raw/Lemmas.lean | 14 ++++++++ src/Std/Data/TreeSet/Basic.lean | 10 ++++++ src/Std/Data/TreeSet/Lemmas.lean | 14 ++++++++ src/Std/Data/TreeSet/Raw/Basic.lean | 5 +++ src/Std/Data/TreeSet/Raw/Lemmas.lean | 14 ++++++++ 19 files changed, 304 insertions(+), 19 deletions(-) diff --git a/src/Std/Data/DTreeMap/Basic.lean b/src/Std/Data/DTreeMap/Basic.lean index 701583ddb1..f114914ccf 100644 --- a/src/Std/Data/DTreeMap/Basic.lean +++ b/src/Std/Data/DTreeMap/Basic.lean @@ -870,17 +870,11 @@ end Const /-- Check if any element satisfies the predicate, short-circuiting if a predicate fails. -/ @[inline] -def any (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do - for ⟨a, b⟩ in t do - if p a b then return true - return false +def any (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := t.inner.any p /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/ @[inline] -def all (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do - for ⟨a, b⟩ in t do - if p a b = false then return false - return true +def all (t : DTreeMap α β cmp) (p : (a : α) → β a → Bool) : Bool := t.inner.all p /-- Returns a list of all keys present in the tree map in ascending order. -/ @[inline] @@ -1054,6 +1048,19 @@ def inter (t₁ t₂ : DTreeMap α β cmp) : DTreeMap α β cmp := instance : Inter (DTreeMap α β cmp) := ⟨inter⟩ +/-- +Compares two tree maps using Boolean equality on keys and values. + +Returns `true` if the maps contain the same key-value pairs, `false` otherwise. +-/ +def beq [LawfulEqCmp cmp] [∀ k, BEq (β k)] (t₁ t₂ : DTreeMap α β cmp) : Bool := + letI : Ord α := ⟨cmp⟩; t₁.inner.beq t₂.inner + +instance [LawfulEqCmp cmp] [∀ k, BEq (β k)] : BEq (DTreeMap α β cmp) := ⟨beq⟩ + +@[inherit_doc DTreeMap.beq] def Const.beq {β : Type v} [BEq β] (t₁ t₂ : DTreeMap α (fun _ => β) cmp) : Bool := + letI : Ord α := ⟨cmp⟩; Internal.Impl.Const.beq t₁.inner t₂.inner + /-- Computes the difference of the given tree maps. This function always iterates through the smaller map. diff --git a/src/Std/Data/DTreeMap/Internal/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/Lemmas.lean index ab55c557c0..a076a54497 100644 --- a/src/Std/Data/DTreeMap/Internal/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/Lemmas.lean @@ -101,6 +101,8 @@ private meta def queryMap : Std.DHashMap Name (fun _ => Name × Array (MacroM (T ⟨`getKeyD, (``getKeyD_eq_getKeyD, #[``(getKeyD_of_perm _)])⟩, ⟨`getKey!, (``getKey!_eq_getKey!, #[``(getKey!_of_perm _)])⟩, ⟨`toList, (``toList_eq_toListModel, #[])⟩, + ⟨`beq, (``beq_eq_beqModel, #[])⟩, + ⟨`Const.beq, (``Internal.Impl.Const.beq_eq_beqModel, #[])⟩, ⟨`keys, (``keys_eq_keys, #[])⟩, ⟨`Const.toList, (``Const.toList_eq_toListModel_map, #[])⟩, ⟨`foldlM, (``foldlM_eq_foldlM_toListModel, #[])⟩, @@ -4888,6 +4890,37 @@ theorem get!_inter!_of_contains_eq_false_left [TransOrd α] [Inhabited β] (h₁ end Const +section BEq +variable {m₁ m₂ : Impl α β} [TransOrd α] [LawfulEqOrd α] [∀ k, BEq (β k)] + +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.Equiv m₂ → beq m₁ m₂ := by + simp_to_model using List.beqModel_eq_true_of_perm + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁.Equiv m₂ := by + simp_to_model using List.perm_of_beqModel + +theorem Equiv.beq_congr {m₃ m₄ : Impl α β} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) : + m₁.Equiv m₃ → m₂.Equiv m₄ → (Impl.beq m₁ m₂) = (Impl.beq m₃ m₄) := by + simp_to_model using List.beqModel_congr + +end BEq + +section + +variable {β : Type v} [BEq β] {m₁ m₂ : Impl α (fun _ => β)} + +theorem Const.Equiv.beq [TransOrd α] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁.Equiv m₂ → Const.beq m₁ m₂ := by + simp_to_model using List.Const.beqModel_eq_true_of_perm + +theorem Const.equiv_of_beq [TransOrd α] [LawfulEqOrd α] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : Const.beq m₁ m₂ = true → m₁.Equiv m₂ := by + simp_to_model using List.Const.perm_of_beqModel + +theorem Const.Equiv.beq_congr [TransOrd α] {m₃ m₄ : Impl α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) : + m₁.Equiv m₃ → m₂.Equiv m₄ → Const.beq m₁ m₂ = Const.beq m₃ m₄ := by + simp_to_model using List.Const.beqModel_congr + +end + section Diff variable {m₁ m₂ : Impl α β} diff --git a/src/Std/Data/DTreeMap/Internal/Operations.lean b/src/Std/Data/DTreeMap/Internal/Operations.lean index 20cee886e1..023913a345 100644 --- a/src/Std/Data/DTreeMap/Internal/Operations.lean +++ b/src/Std/Data/DTreeMap/Internal/Operations.lean @@ -822,6 +822,10 @@ information but still assumes the preconditions of `filter`, otherwise might pan def inter! [Ord α] (m₁ m₂ : Impl α β): Impl α β := if m₁.size ≤ m₂.size then m₁.filter! (fun k _ => m₂.contains k) else interSmaller m₁ m₂ +/-- Internal implementation detail of the tree map -/ +def beq [Ord α] [LawfulEqOrd α] [∀ k, BEq (β k)] (t₁ t₂ : Impl α β) : Bool := + if t₁.size ≠ t₂.size then false else t₁.all (fun k v => t₂.get? k == some v) + /-- Computes the difference of the given tree maps. This function always iterates through the smaller map. @@ -950,6 +954,11 @@ def mergeWith! [Ord α] [LawfulEqOrd α] (mergeFn : (a : α) → β a → β a namespace Const variable {β : Type v} + +/-- Internal implementation detail of the hash map -/ +def beq [Ord α] [BEq β] (t₁ t₂ : Impl α fun _ => β) : Bool := + if t₁.size ≠ t₂.size then false else t₁.all (fun k v => Const.get? t₂ k == some v) + local instance : Coe (Type v) (α → Type v) where coe γ := fun _ => γ /-- diff --git a/src/Std/Data/DTreeMap/Internal/Queries.lean b/src/Std/Data/DTreeMap/Internal/Queries.lean index 06c7d8c269..4247b48cc7 100644 --- a/src/Std/Data/DTreeMap/Internal/Queries.lean +++ b/src/Std/Data/DTreeMap/Internal/Queries.lean @@ -293,6 +293,20 @@ def forIn {m} [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (ini instance [Monad m] : ForIn m (Impl α β) ((a : α) × β a) where forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init +/-- Implementation detail. -/ +@[inline] +def any (t : Impl α β) (p : (a : α) → β a → Bool) : Bool := Id.run $ do + for ⟨a, b⟩ in t do + if p a b then return true + return false + +/-- Implementation detail. -/ +@[inline] +def all (t : Impl α β) (p : (a : α) → β a → Bool) : Bool := Id.run $ do + for ⟨a, b⟩ in t do + if p a b = false then return false + return true + /-- Returns a `List` of the keys in order. -/ @[inline] def keys (t : Impl α β) : List α := t.foldr (init := []) fun k _ l => k :: l diff --git a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean index 870daa6921..9a65b149ec 100644 --- a/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Internal/WF/Lemmas.lean @@ -1900,6 +1900,29 @@ theorem WF.union! {_ : Ord α} [TransOrd α] . exact WF.insertManyIfNew! h₂ . exact WF.insertMany! h₁ +theorem all_eq_all_toListModel {p : (a : α) → β a → Bool} {m : Impl α β} : + m.all p = m.toListModel.all (fun x => p x.1 x.2) := by + simp [all, ForIn.forIn, 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 + | 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] + +theorem beq_eq_beqModel {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEq α] [LawfulBEqOrd α] [∀ k, BEq (β k)] {m₁ m₂ : Impl α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : + Impl.beq m₁ m₂ = beqModel m₁.toListModel m₂.toListModel := by + simp [beq, beqModel, size_eq_length _ h₁.balanced, size_eq_length _ h₂.balanced, all_eq_all_toListModel, + get?_eq_getValueCast? h₂.ordered] + +theorem Const.beq_eq_beqModel {β : Type v} {_ : Ord α} [BEq α] [TransOrd α] [LawfulBEqOrd α] [BEq β] {m₁ m₂ : Impl α (fun _ => β)} (h₁ : m₁.WF) (h₂ : m₂.WF) : + beq m₁ m₂ = Const.beqModel m₁.toListModel m₂.toListModel := by + simp [beq, Const.beqModel, size_eq_length _ h₁.balanced, size_eq_length _ h₂.balanced, all_eq_all_toListModel, + get?_eq_getValue? h₂.ordered] + theorem WF.constInsertMany! {β : Type v} {_ : Ord α} [TransOrd α] {ρ} [ForIn Id ρ (α × β)] {l : ρ} {t : Impl α β} (h : t.WF) : (Const.insertMany! t l).1.WF := (Const.insertMany! t l).2 h (fun _ _ _ h' => h'.insert!) diff --git a/src/Std/Data/DTreeMap/Lemmas.lean b/src/Std/Data/DTreeMap/Lemmas.lean index 75ccbb3e43..7777407c10 100644 --- a/src/Std/Data/DTreeMap/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Lemmas.lean @@ -2890,6 +2890,36 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] end Const +section BEq + +variable {m₁ m₂ : DTreeMap α β cmp} [∀ k, BEq (β k)] [LawfulEqCmp cmp] [TransCmp cmp] + +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h : m₁ ~m m₂) : m₁ == m₂ := + Impl.Equiv.beq m₁.2 m₂.2 h.1 + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨Impl.equiv_of_beq m₁.2 m₂.2 h⟩ + +theorem Equiv.beq_congr {m₃ m₄ : DTreeMap α β cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + Impl.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1 + +end BEq + +section + +variable {β : Type v} {m₁ m₂ : DTreeMap α (fun _ => β) cmp} [BEq β] + +theorem Const.Equiv.beq [TransCmp cmp] [ReflBEq β] (h : m₁ ~m m₂) : DTreeMap.Const.beq m₁ m₂ := + Impl.Const.Equiv.beq m₁.2 m₂.2 h.1 + +theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [LawfulBEq β] (h : Const.beq m₁ m₂) : m₁ ~m m₂ := + ⟨Impl.Const.equiv_of_beq m₁.2 m₂.2 h⟩ + +theorem Const.Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : DTreeMap α (fun _ => β) cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : Const.beq m₁ m₂ = Const.beq m₃ m₄ := + Impl.Const.Equiv.beq_congr m₁.2 m₂.2 m₃.2 m₄.2 w₁.1 w₂.1 + +end + section Diff variable {t₁ t₂ : DTreeMap α β cmp} @@ -5372,10 +5402,10 @@ theorem forM_eq [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) × β a h.1.forM_eq t₁.2 t₂.2 theorem any_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h : t₁ ~m t₂) : t₁.any p = t₂.any p := by - simp only [any, h.forIn_eq] + simp only [any, Impl.any, ForIn.forIn, h.1.forIn_eq t₁.2 t₂.2] theorem all_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h : t₁ ~m t₂) : t₁.all p = t₂.all p := by - simp only [all, h.forIn_eq] + simp only [all, Impl.all, ForIn.forIn, h.1.forIn_eq t₁.2 t₂.2] theorem minKey?_eq [TransCmp cmp] (h : t₁ ~m t₂) : t₁.minKey? = t₂.minKey? := h.1.minKey?_eq t₁.2 t₂.2 diff --git a/src/Std/Data/DTreeMap/Raw/Basic.lean b/src/Std/Data/DTreeMap/Raw/Basic.lean index 8d412a603d..3586aa9068 100644 --- a/src/Std/Data/DTreeMap/Raw/Basic.lean +++ b/src/Std/Data/DTreeMap/Raw/Basic.lean @@ -604,16 +604,12 @@ def forInUncurried (f : α × β → δ → m (ForInStep δ)) (init : δ) (t : R end Const @[inline, inherit_doc DTreeMap.any] -def any (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do - for ⟨a, b⟩ in t do - if p a b then return true - return false +def any (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool := + t.inner.any p @[inline, inherit_doc DTreeMap.all] def all (t : Raw α β cmp) (p : (a : α) → β a → Bool) : Bool := Id.run $ do - for ⟨a, b⟩ in t do - if p a b = false then return false - return true + t.inner.all p @[inline, inherit_doc DTreeMap.keys] def keys (t : Raw α β cmp) : List α := @@ -732,6 +728,15 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp := instance : Inter (Raw α β cmp) := ⟨inter⟩ + +@[inherit_doc DTreeMap.beq] def beq [LawfulEqCmp cmp] [∀ k, BEq (β k)] (t₁ t₂ : Raw α β cmp) : Bool := + letI : Ord α := ⟨cmp⟩; t₁.inner.beq t₂.inner + +instance [LawfulEqCmp cmp] [∀ k, BEq (β k)] : BEq (Raw α β cmp) := ⟨beq⟩ + +@[inherit_doc DTreeMap.beq] def Const.beq {β : Type v} [BEq β] (t₁ t₂ : Raw α (fun _ => β) cmp) : Bool := + letI : Ord α := ⟨cmp⟩; Internal.Impl.Const.beq t₁.inner t₂.inner + /-- Computes the difference of the given tree maps. This function always iterates through the smaller map. diff --git a/src/Std/Data/DTreeMap/Raw/Lemmas.lean b/src/Std/Data/DTreeMap/Raw/Lemmas.lean index 1b0c9ce16a..077c0ddf78 100644 --- a/src/Std/Data/DTreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/DTreeMap/Raw/Lemmas.lean @@ -3056,6 +3056,36 @@ theorem get!_inter_of_not_mem_left [TransCmp cmp] [Inhabited β] (h₁ : m₁.WF end Const +section BEq +variable {m₁ m₂ : Raw α β cmp} [∀ k, BEq (β k)] [LawfulEqCmp cmp] [TransCmp cmp] + +theorem Equiv.beq [∀ k, ReflBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := + Impl.Equiv.beq h₁ h₂ h.1 + +theorem equiv_of_beq [∀ k, LawfulBEq (β k)] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := fun hyp => + let : Ord α := ⟨cmp⟩; ⟨Impl.equiv_of_beq h₁.1 h₂.1 hyp⟩ + +theorem Equiv.beq_congr {m₃ m₄ : Raw α β cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) : + m₁ ~m m₃ → m₂ ~m m₄ → Raw.beq m₁ m₂ = Raw.beq m₃ m₄ := + fun w1 w2 => Impl.Equiv.beq_congr h₁ h₂ h₃ h₄ w1.1 w2.1 + +end BEq + +section +variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β) cmp} + +theorem Const.Equiv.beq [TransCmp cmp] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : m₁ ~m m₂ → beq m₁ m₂ := + fun h => Impl.Const.Equiv.beq h₁ h₂ h.1 + +theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) : beq m₁ m₂ = true → m₁ ~m m₂ := + fun hyp => let : Ord α := ⟨cmp⟩; ⟨Impl.Const.equiv_of_beq h₁.1 h₂.1 hyp⟩ + +theorem Const.Equiv.beq_congr [TransCmp cmp] [BEq β] {m₃ m₄ : Raw α (fun _ => β) cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) : + m₁ ~m m₃ → m₂ ~m m₄ → Raw.Const.beq m₁ m₂ = Raw.Const.beq m₃ m₄ := + fun w1 w2 => Impl.Const.Equiv.beq_congr h₁ h₂ h₃ h₄ w1.1 w2.1 + +end + section Diff variable {t₁ t₂ : Raw α β cmp} @@ -5295,11 +5325,13 @@ theorem forM_eq [TransCmp cmp] [Monad m] [LawfulMonad m] {f : (a : α) × β a theorem any_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) : t₁.any p = t₂.any p := by - simp only [any, h.forIn_eq h₁ h₂] + simp only [any, Impl.any, ForIn.forIn, bind_pure_comp, map_pure, h.1.forIn_eq h₁.1 h₂.1, + Id.run_bind] theorem all_eq [TransCmp cmp] {p : (a : α) → β a → Bool} (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) : t₁.all p = t₂.all p := by - simp only [all, h.forIn_eq h₁ h₂] + simp only [all, Impl.all, ForIn.forIn, bind_pure_comp, map_pure, h.1.forIn_eq h₁.1 h₂.1, + Id.run_bind] theorem minKey?_eq [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁ ~m t₂) : t₁.minKey? = t₂.minKey? := diff --git a/src/Std/Data/ExtDTreeMap/Basic.lean b/src/Std/Data/ExtDTreeMap/Basic.lean index 7989265243..567f5eba16 100644 --- a/src/Std/Data/ExtDTreeMap/Basic.lean +++ b/src/Std/Data/ExtDTreeMap/Basic.lean @@ -924,6 +924,30 @@ def inter [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β instance [TransCmp cmp] : Inter (ExtDTreeMap α β cmp) := ⟨inter⟩ +instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] : BEq (ExtDTreeMap α β cmp) where + beq := lift₂ (fun x y : DTreeMap α β cmp => x.beq y) fun _ _ _ _ => DTreeMap.Equiv.beq_congr + +instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] [∀ k, ReflBEq (β k)] : ReflBEq (ExtDTreeMap α β cmp) where + rfl {a} := a.inductionOn fun _ => DTreeMap.Equiv.beq <| DTreeMap.Equiv.rfl + +instance [LawfulEqCmp cmp] [TransCmp cmp] [∀ k, BEq (β k)] [∀ k, LawfulBEq (β k)] : LawfulBEq (ExtDTreeMap α β cmp) where + eq_of_beq {a} {b} := a.inductionOn₂ b fun _ _ h => sound <| DTreeMap.equiv_of_beq h + +namespace Const + +variable {β : Type v} + +@[inline, inherit_doc DTreeMap.beq] +def beq [TransCmp cmp] [BEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : Bool := lift₂ (fun x y : DTreeMap α (fun _ => β) cmp => DTreeMap.Const.beq x y) + (fun _ _ _ _ => DTreeMap.Const.Equiv.beq_congr) m₁ m₂ + +theorem beq_of_eq [TransCmp cmp] [BEq β] [ReflBEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : m₁ = m₂ → Const.beq m₁ m₂ := + m₁.inductionOn₂ m₂ fun _ _ h => DTreeMap.Const.Equiv.beq <| exact h + +theorem eq_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (m₁ m₂ : ExtDTreeMap α (fun _ => β) cmp) : Const.beq m₁ m₂ → m₁ = m₂ := + m₁.inductionOn₂ m₂ fun _ _ h => sound <| DTreeMap.Const.equiv_of_beq h + +end Const @[inline, inherit_doc DTreeMap.diff] def diff [TransCmp cmp] (m₁ m₂ : ExtDTreeMap α β cmp) : ExtDTreeMap α β cmp := lift₂ (fun x y : DTreeMap α β cmp => mk (x.diff y)) (fun a b c d equiv₁ equiv₂ => by diff --git a/src/Std/Data/ExtTreeMap/Basic.lean b/src/Std/Data/ExtTreeMap/Basic.lean index 66f77ed25a..9fb01693b3 100644 --- a/src/Std/Data/ExtTreeMap/Basic.lean +++ b/src/Std/Data/ExtTreeMap/Basic.lean @@ -535,6 +535,19 @@ def inter [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β c instance [TransCmp cmp] : Inter (ExtTreeMap α β cmp) := ⟨inter⟩ +instance [TransCmp cmp] [BEq β] : BEq (ExtTreeMap α β cmp) where + beq m₁ m₂ := ExtDTreeMap.Const.beq m₁.inner m₂.inner + +instance [TransCmp cmp] [BEq β] [ReflBEq β] : ReflBEq (ExtTreeMap α β cmp) where + rfl := ExtDTreeMap.Const.beq_of_eq _ _ rfl + +instance [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] : LawfulBEq (ExtTreeMap α β cmp) where + eq_of_beq {a} {b} hyp := by + have ⟨_⟩ := a + have ⟨_⟩ := b + simp only [mk.injEq] + exact ExtDTreeMap.Const.eq_of_beq _ _ hyp + @[inline, inherit_doc ExtDTreeMap.diff] def diff [TransCmp cmp] (t₁ t₂ : ExtTreeMap α β cmp) : ExtTreeMap α β cmp := ⟨ExtDTreeMap.diff t₁.inner t₂.inner⟩ diff --git a/src/Std/Data/ExtTreeSet/Basic.lean b/src/Std/Data/ExtTreeSet/Basic.lean index eee81d24da..93da549e9b 100644 --- a/src/Std/Data/ExtTreeSet/Basic.lean +++ b/src/Std/Data/ExtTreeSet/Basic.lean @@ -529,6 +529,19 @@ def inter [TransCmp cmp] (t₁ t₂ : ExtTreeSet α cmp) : ExtTreeSet α cmp := instance [TransCmp cmp] : Inter (ExtTreeSet α cmp) := ⟨inter⟩ +instance [TransCmp cmp] : BEq (ExtTreeSet α cmp) where + beq m₁ m₂ := ExtDTreeMap.Const.beq m₁.inner.inner m₂.inner.inner + +instance [TransCmp cmp] : ReflBEq (ExtTreeSet α cmp) where + rfl := ExtDTreeMap.Const.beq_of_eq _ _ rfl + +instance [TransCmp cmp] [LawfulEqCmp cmp] : LawfulBEq (ExtTreeSet α cmp) where + eq_of_beq {a} {b} hyp := by + have ⟨⟨_⟩⟩ := a + have ⟨⟨_⟩⟩ := b + simp only [mk.injEq, ExtTreeMap.mk.injEq] at |- hyp + exact ExtDTreeMap.Const.eq_of_beq _ _ hyp + /-- Computes the difference of the given tree sets. diff --git a/src/Std/Data/TreeMap/Basic.lean b/src/Std/Data/TreeMap/Basic.lean index f3be4df851..dc74a37868 100644 --- a/src/Std/Data/TreeMap/Basic.lean +++ b/src/Std/Data/TreeMap/Basic.lean @@ -501,6 +501,11 @@ def inter (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp := instance : Inter (TreeMap α β cmp) := ⟨inter⟩ +@[inherit_doc DTreeMap.beq] def beq [BEq β] (t₁ t₂ : TreeMap α β cmp) : Bool := + letI : Ord α := ⟨cmp⟩; DTreeMap.Const.beq t₁.inner t₂.inner + +instance [BEq β] : BEq (TreeMap α β cmp) := ⟨beq⟩ + @[inline, inherit_doc DTreeMap.diff] def diff (t₁ t₂ : TreeMap α β cmp) : TreeMap α β cmp := letI : Ord α := ⟨cmp⟩; ⟨DTreeMap.diff t₁.inner t₂.inner⟩ diff --git a/src/Std/Data/TreeMap/Lemmas.lean b/src/Std/Data/TreeMap/Lemmas.lean index 4c5ad92548..83be7f6723 100644 --- a/src/Std/Data/TreeMap/Lemmas.lean +++ b/src/Std/Data/TreeMap/Lemmas.lean @@ -2077,6 +2077,21 @@ theorem isEmpty_inter_iff [TransCmp cmp] : end Inter +section + +variable {β : Type v} {m₁ m₂ : TreeMap α β cmp} [BEq β] + +theorem Equiv.beq [TransCmp cmp] [ReflBEq β] (h : m₁ ~m m₂) : m₁ == m₂ := + DTreeMap.Const.Equiv.beq h.1 + +theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [LawfulBEq β] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨DTreeMap.Const.equiv_of_beq h⟩ + +theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : TreeMap α β cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + DTreeMap.Const.Equiv.beq_congr w₁.1 w₂.1 + +end + section Diff variable {t₁ t₂ : TreeMap α β cmp} diff --git a/src/Std/Data/TreeMap/Raw/Basic.lean b/src/Std/Data/TreeMap/Raw/Basic.lean index 9223222a53..969236743a 100644 --- a/src/Std/Data/TreeMap/Raw/Basic.lean +++ b/src/Std/Data/TreeMap/Raw/Basic.lean @@ -503,6 +503,11 @@ def inter (t₁ t₂ : Raw α β cmp) : Raw α β cmp := instance : Inter (Raw α β cmp) := ⟨inter⟩ +@[inherit_doc DTreeMap.beq] def beq [BEq β] (t₁ t₂ : Raw α β cmp) : Bool := + letI : Ord α := ⟨cmp⟩; DTreeMap.Raw.Const.beq t₁.inner t₂.inner + +instance [BEq β] : BEq (Raw α β cmp) := ⟨beq⟩ + @[inline, inherit_doc DTreeMap.Raw.diff] def diff (t₁ t₂ : Raw α β cmp) : Raw α β cmp := ⟨DTreeMap.Raw.diff t₁.inner t₂.inner⟩ diff --git a/src/Std/Data/TreeMap/Raw/Lemmas.lean b/src/Std/Data/TreeMap/Raw/Lemmas.lean index fb2c68587a..c9626cdcc1 100644 --- a/src/Std/Data/TreeMap/Raw/Lemmas.lean +++ b/src/Std/Data/TreeMap/Raw/Lemmas.lean @@ -2129,6 +2129,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : end Inter +section +variable {β : Type v} {m₁ m₂ : Raw α β cmp} + +theorem Const.Equiv.beq [TransCmp cmp] [BEq β] [ReflBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : m₁ == m₂ := + DTreeMap.Raw.Const.Equiv.beq h₁ h₂ h.1 + +theorem Const.equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] [BEq β] [LawfulBEq β] (h₁ : m₁.WF) (h₂ : m₂.WF) (k : m₁ == m₂) : m₁ ~m m₂ := + ⟨DTreeMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 k⟩ + +theorem Const.Equiv.beq_congr [TransCmp cmp] [BEq β] {m₃ m₄ : Raw α β cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + DTreeMap.Raw.Const.Equiv.beq_congr h₁ h₂ h₃ h₄ w₁.1 w₂.1 + +end + section Diff variable {t₁ t₂ : Raw α β cmp} diff --git a/src/Std/Data/TreeSet/Basic.lean b/src/Std/Data/TreeSet/Basic.lean index 7f6b98e367..c0f720ce50 100644 --- a/src/Std/Data/TreeSet/Basic.lean +++ b/src/Std/Data/TreeSet/Basic.lean @@ -503,6 +503,16 @@ def inter (t₁ t₂ : TreeSet α cmp) : TreeSet α cmp := instance : Inter (TreeSet α cmp) := ⟨inter⟩ +/-- +Compares two tree sets using Boolean equality on keys. + +Returns `true` if the sets contain the same keys, `false` otherwise. +-/ +def beq (t₁ t₂ : TreeSet α cmp) : Bool := + letI : Ord α := ⟨cmp⟩; TreeMap.beq t₁.inner t₂.inner + +instance : BEq (TreeSet α cmp) := ⟨beq⟩ + /-- Computes the difference of the given tree sets. diff --git a/src/Std/Data/TreeSet/Lemmas.lean b/src/Std/Data/TreeSet/Lemmas.lean index 65d7a50dd1..37d06c12ab 100644 --- a/src/Std/Data/TreeSet/Lemmas.lean +++ b/src/Std/Data/TreeSet/Lemmas.lean @@ -778,6 +778,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] : end Inter +section +variable {m₁ m₂ : TreeSet α cmp} + +theorem Equiv.beq [TransCmp cmp] (h : m₁ ~m m₂) : m₁ == m₂ := + TreeMap.Equiv.beq h.1 + +theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] (h : m₁ == m₂) : m₁ ~m m₂ := + ⟨TreeMap.equiv_of_beq h⟩ + +theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : TreeSet α cmp} (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + TreeMap.Equiv.beq_congr w₁.1 w₂.1 + +end + section Diff variable {t₁ t₂ : TreeSet α cmp} diff --git a/src/Std/Data/TreeSet/Raw/Basic.lean b/src/Std/Data/TreeSet/Raw/Basic.lean index 6341c9c639..1086f1fb0c 100644 --- a/src/Std/Data/TreeSet/Raw/Basic.lean +++ b/src/Std/Data/TreeSet/Raw/Basic.lean @@ -353,6 +353,11 @@ def inter (t₁ t₂ : Raw α cmp) : Raw α cmp := instance : Inter (Raw α cmp) := ⟨inter⟩ +@[inherit_doc TreeSet.beq] def beq (t₁ t₂ : Raw α cmp) : Bool := + letI : Ord α := ⟨cmp⟩; TreeMap.Raw.beq t₁.inner t₂.inner + +instance : BEq (Raw α cmp) := ⟨beq⟩ + /-- Computes the difference of the given tree sets. diff --git a/src/Std/Data/TreeSet/Raw/Lemmas.lean b/src/Std/Data/TreeSet/Raw/Lemmas.lean index 985a0ce37c..19ade3ffff 100644 --- a/src/Std/Data/TreeSet/Raw/Lemmas.lean +++ b/src/Std/Data/TreeSet/Raw/Lemmas.lean @@ -818,6 +818,20 @@ theorem isEmpty_inter_iff [TransCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) : end Inter +section +variable {m₁ m₂ : Raw α cmp} + +theorem Equiv.beq [TransCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ ~m m₂) : beq m₁ m₂ := + TreeMap.Raw.Const.Equiv.beq h₁ h₂ h.1 + +theorem equiv_of_beq [TransCmp cmp] [LawfulEqCmp cmp] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁ == m₂): m₁ ~m m₂ := + ⟨TreeMap.Raw.Const.equiv_of_beq h₁.1 h₂.1 h⟩ + +theorem Equiv.beq_congr [TransCmp cmp] {m₃ m₄ : Raw α cmp} (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) (w₁ : m₁ ~m m₃) (w₂ : m₂ ~m m₄) : (m₁ == m₂) = (m₃ == m₄) := + TreeMap.Raw.Const.Equiv.beq_congr h₁.1 h₂.1 h₃.1 h₄.1 w₁.1 w₂.1 + +end + section Diff variable {t₁ t₂ : Raw α cmp}