From c08fcf6c28aa6b8d500b4ee6fe85c76b658bd13a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Mon, 10 Nov 2025 13:48:36 +0000 Subject: [PATCH] feat: add union on ExtDHashMap/ExtHashMap/ExtHashSet (#10946) This PR adds union operation on ExtDHashMap/ExtHashMap/ExtHashSet nd provides lemmas about union operations. --- src/Std/Data/DHashMap/Basic.lean | 2 +- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 18 ++ src/Std/Data/DHashMap/Lemmas.lean | 10 + src/Std/Data/DHashMap/Raw.lean | 2 +- src/Std/Data/DHashMap/RawLemmas.lean | 20 ++ src/Std/Data/ExtDHashMap/Basic.lean | 18 +- src/Std/Data/ExtDHashMap/Lemmas.lean | 282 ++++++++++++++++++ src/Std/Data/ExtHashMap/Basic.lean | 5 + src/Std/Data/ExtHashMap/Lemmas.lean | 184 ++++++++++++ src/Std/Data/ExtHashSet/Basic.lean | 11 + src/Std/Data/ExtHashSet/Lemmas.lean | 123 ++++++++ src/Std/Data/HashMap/Basic.lean | 2 +- src/Std/Data/HashMap/Lemmas.lean | 10 + src/Std/Data/HashMap/RawLemmas.lean | 10 + src/Std/Data/HashSet/Lemmas.lean | 13 +- src/Std/Data/HashSet/RawLemmas.lean | 11 + 16 files changed, 716 insertions(+), 5 deletions(-) diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 1316a4a28e..d2773860ca 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -309,7 +309,7 @@ This function ensures that the value is used linearly. m.1.keysArray /-- -Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +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. This function always merges the smaller map into the larger map, so the expected runtime is diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 7b730bb702..91ff297a9a 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -2420,6 +2420,24 @@ theorem contains_of_contains_union_of_contains_eq_false_left [EquivBEq α] simp_to_model [union, contains] using List.contains_of_contains_insertList_of_contains_eq_false_left /- Equiv -/ +theorem union_equiv_congr_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₁.1.Equiv m₂.1) : + (m₁.union m₃).1.Equiv (m₂.union m₃).1 := by + revert equiv + simp_to_model [union] + intro equiv + apply List.insertList_perm_of_perm_first equiv + wf_trivial + +theorem union_equiv_congr_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₂.1.Equiv m₃.1) : + (m₁.union m₂).1.Equiv (m₁.union m₃).1 := by + revert equiv + simp_to_model [union] + intro equiv + apply @List.insertList_perm_of_perm_second _ _ _ _ (toListModel m₂.val.buckets) (toListModel m₃.val.buckets) (toListModel m₁.val.buckets) equiv + all_goals wf_trivial + theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : (m₁.union (m₂.insert p.fst p.snd)).1.Equiv ((m₁.union m₂).insert p.fst p.snd).1 := by diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index c846ef70ba..6cc74e3070 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -1760,6 +1760,16 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] exact @Raw₀.contains_of_contains_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k h₁ h₂ /- Equiv -/ +theorem union_equiv_congr_left {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := + ⟨@Raw₀.union_equiv_congr_left α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ ⟨m₃.1, m₃.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 m₃.2 equiv.1⟩ + +theorem union_equiv_congr_right {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := + ⟨@Raw₀.union_equiv_congr_right α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ ⟨m₃.1, m₃.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 m₃.2 equiv.1⟩ + theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} : (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) := ⟨@Raw₀.union_insert_right_equiv_insert_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ p m₁.2 m₂.2⟩ diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index b0018b935c..61dbea8ba5 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -453,7 +453,7 @@ only those mappings where the function returns `some` value. m.fold (fun acc k _ => acc.push k) (.emptyWithCapacity m.size) /-- -Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +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. This function always merges the smaller map into the larger map, so the expected runtime is diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index ec60da9345..bf676f2ad3 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -1865,6 +1865,26 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] simp_to_raw using Raw₀.contains_of_contains_union_of_contains_eq_false_left /- Equiv -/ +theorem union_equiv_congr_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := by + revert equiv + simp only [Union.union] + simp_to_raw + intro hyp + apply Raw₀.union_equiv_congr_left + all_goals wf_trivial + +theorem union_equiv_congr_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := by + revert equiv + simp only [Union.union] + simp_to_raw + intro hyp + apply Raw₀.union_equiv_congr_right + all_goals wf_trivial + theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) := by diff --git a/src/Std/Data/ExtDHashMap/Basic.lean b/src/Std/Data/ExtDHashMap/Basic.lean index d2907aadd8..706beda460 100644 --- a/src/Std/Data/ExtDHashMap/Basic.lean +++ b/src/Std/Data/ExtDHashMap/Basic.lean @@ -77,6 +77,10 @@ abbrev mk (m : DHashMap α β) : ExtDHashMap α β := def lift {γ : Sort w} (f : DHashMap α β → γ) (h : ∀ a b, a ~m b → f a = f b) (m : ExtDHashMap α β) : γ := m.1.lift f h +/-- Internal implementation detail of the hash map. -/ +def lift₂ {γ : Sort w} (f : DHashMap α β → DHashMap α β → γ) (h : ∀ a b c d, a ~m c → b ~m d → f a b = f c d) (m₁ m₂ : ExtDHashMap α β) : γ := + Quotient.lift₂ f h m₁.inner m₂.inner + /-- Internal implementation detail of the hash map. -/ def pliftOn {γ : Sort w} (m : ExtDHashMap α β) (f : (a : DHashMap α β) → m = mk a → γ) (h : ∀ a b h₁ h₂, a ~m b → f a h₁ = f b h₂) : γ := @@ -347,7 +351,19 @@ def Const.insertManyIfNewUnit [EquivBEq α] [LawfulHashable α] {ρ : Type w} m := ⟨m.1.insertIfNew a (), fun _ init step => step (m.2 _ init step)⟩ return m.1 --- TODO (after verification): partition, union +theorem union_congr [EquivBEq α] [LawfulHashable α] (a b c d : DHashMap α β) (h₁ : a ~m c) (h₂ : b ~m d) : a ∪ b ~m c ∪ d := + DHashMap.Equiv.trans (DHashMap.union_equiv_congr_left h₁) (DHashMap.union_equiv_congr_right h₂) + +@[inline, inherit_doc DHashMap.union] +def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : ExtDHashMap α β := lift₂ (fun x y : DHashMap α β => mk (x.union y)) + (fun a b c d equiv₁ equiv₂ => by + simp only [DHashMap.union_eq, mk'.injEq] + apply Quotient.sound + apply union_congr + . exact equiv₁ + . exact equiv₂) m₁ m₂ + +instance [EquivBEq α] [LawfulHashable α] : Union (ExtDHashMap α β) := ⟨union⟩ @[inline, inherit_doc DHashMap.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) : diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean index 8e8f4a106e..af6037780d 100644 --- a/src/Std/Data/ExtDHashMap/Lemmas.lean +++ b/src/Std/Data/ExtDHashMap/Lemmas.lean @@ -2136,6 +2136,288 @@ theorem getD_unitOfList [EquivBEq α] [LawfulHashable α] end Const +section Union + +variable (m₁ m₂ : ExtDHashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq [EquivBEq α] [LawfulHashable α] : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +private theorem union_mk [EquivBEq α] [LawfulHashable α] + {m₁ m₂ : DHashMap α β} : + (ExtDHashMap.union (mk m₁) (mk m₂) : ExtDHashMap α β) = mk (m₁ ∪ m₂) := by congr + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.contains_union + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_union_of_left + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_union_of_right + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_union_iff + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_of_mem_union_of_not_mem_right + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_of_mem_union_of_not_mem_left + +theorem union_insert_right_eq_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} : + (m₁ ∪ (m₂.insert p.fst p.snd)) = ((m₁ ∪ m₂).insert p.fst p.snd) := + m₁.inductionOn₂ m₂ fun _ _ => sound DHashMap.union_insert_right_equiv_insert_union + +/- get? -/ +theorem get?_union [LawfulBEq α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.get?_union + +theorem get?_union_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := by + induction m₁ with + | mk a => + induction m₂ with + | mk b => + exact @DHashMap.get?_union_of_not_mem_left α β _ _ a b _ k not_mem + +theorem get?_union_of_not_mem_right [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get?_union_of_not_mem_right h + +/- get -/ +theorem get_union_of_mem_right [LawfulBEq α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get_union_of_mem_right h + +theorem get_union_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := by + revert not_mem h' + exact m₁.inductionOn₂ m₂ fun _ _ not_mem _ => DHashMap.get_union_of_not_mem_left not_mem + +/- getD -/ +theorem getD_union [LawfulBEq α] {k : α} {fallback : β k} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getD_union + +theorem getD_union_of_not_mem_left [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ not_mem => DHashMap.getD_union_of_not_mem_left not_mem + +theorem getD_union_of_not_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ not_mem => DHashMap.getD_union_of_not_mem_right not_mem + +/- get! -/ +theorem get!_union [LawfulBEq α] {k : α} [Inhabited (β k)] : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.get!_union + +theorem get!_union_of_not_mem_left [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get!_union_of_not_mem_left h + +theorem get!_union_of_not_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get!_union_of_not_mem_right h + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKey?_union + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey?_union_of_not_mem_left h + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right mem) = m₂.getKey k mem := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey_union_of_mem_right h + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h' not_mem) := by + revert not_mem h' + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey_union_of_not_mem_left h + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h' not_mem) := by + revert not_mem h' + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey_union_of_not_mem_right h + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKeyD_union + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKeyD_union_of_not_mem_left h + +theorem getKeyD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKeyD_union_of_not_mem_right h + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKey!_union + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey!_union_of_not_mem_left h + +theorem getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKey!_union_of_not_mem_right + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_union_of_not_mem + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_left_le_size_union + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_right_le_size_union + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_union_le_size_add_size + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.isEmpty_union + +end Union + +namespace Const + +variable {β : Type v} {m₁ m₂ : ExtDHashMap α (fun _ => β)} + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + Const.get? (m₁.union m₂) k = (Const.get? m₂ k).or (Const.get? m₁ k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.get?_union + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get? (m₁.union m₂) k = Const.get? m₂ k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get?_union_of_not_mem_left h + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get? (m₁.union m₂) k = Const.get? m₁ k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get?_union_of_not_mem_right h + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : m₂.contains k) : + Const.get (m₁.union m₂) k (mem_union_of_right mem) = Const.get m₂ k mem := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get_union_of_mem_right h + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + Const.get (m₁.union m₂) k h' = Const.get m₂ k (mem_of_mem_union_of_not_mem_left h' not_mem) := by + revert not_mem h' + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get_union_of_not_mem_left h + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + Const.get (m₁.union m₂) k h' = Const.get m₁ k (mem_of_mem_union_of_not_mem_right h' not_mem) := by + revert not_mem h' + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get_union_of_not_mem_right h + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k (Const.getD m₁ k fallback) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.getD_union + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.getD_union_of_not_mem_left h + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + Const.getD (m₁.union m₂) k fallback = Const.getD m₁ k fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.getD_union_of_not_mem_right h + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : + Const.get! (m₁.union m₂) k = Const.getD m₂ k (Const.get! m₁ k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.get!_union + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get! (m₁.union m₂) k = Const.get! m₂ k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get!_union_of_not_mem_left h + +theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get! (m₁.union m₂) k = Const.get! m₁ k := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get!_union_of_not_mem_right h + +end Const + variable {m : ExtDHashMap α β} section Alter diff --git a/src/Std/Data/ExtHashMap/Basic.lean b/src/Std/Data/ExtHashMap/Basic.lean index e681c88c97..838f55494b 100644 --- a/src/Std/Data/ExtHashMap/Basic.lean +++ b/src/Std/Data/ExtHashMap/Basic.lean @@ -244,6 +244,11 @@ def insertManyIfNewUnit [EquivBEq α] [LawfulHashable α] {ρ : Type w} [ForIn Id ρ α] (m : ExtHashMap α Unit) (l : ρ) : ExtHashMap α Unit := ⟨ExtDHashMap.Const.insertManyIfNewUnit m.inner l⟩ +@[inline, inherit_doc ExtDHashMap.union] +def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : ExtHashMap α β := ⟨ExtDHashMap.union m₁.inner m₂.inner⟩ + +instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashMap α β) := ⟨union⟩ + @[inline, inherit_doc ExtDHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) : ExtHashMap α Unit := diff --git a/src/Std/Data/ExtHashMap/Lemmas.lean b/src/Std/Data/ExtHashMap/Lemmas.lean index 99cd23adad..52cf39a62b 100644 --- a/src/Std/Data/ExtHashMap/Lemmas.lean +++ b/src/Std/Data/ExtHashMap/Lemmas.lean @@ -1362,6 +1362,190 @@ theorem unitOfList_eq_empty_iff [EquivBEq α] [LawfulHashable α] {l : List α} end +section Union + +variable (m₁ m₂ : ExtHashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq [EquivBEq α] [LawfulHashable α] : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + ExtDHashMap.contains_union + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + ExtDHashMap.mem_union_of_left + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + ExtDHashMap.mem_union_of_right + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + ExtDHashMap.mem_union_iff + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + ExtDHashMap.mem_of_mem_union_of_not_mem_right + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + ExtDHashMap.mem_of_mem_union_of_not_mem_left + +theorem union_insert_right_eq_insert_union [EquivBEq α] [LawfulHashable α] {p : (_ : α) × β} : + (m₁ ∪ (m₂.insert p.fst p.snd)) = ((m₁ ∪ m₂).insert p.fst p.snd) := by + simp only [Union.union] + simp only [union, insert, ExtDHashMap.union_eq, mk.injEq] + exact ExtDHashMap.union_insert_right_eq_insert_union + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + ExtDHashMap.Const.get?_union + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := + ExtDHashMap.Const.get?_union_of_not_mem_left not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := + ExtDHashMap.Const.get?_union_of_not_mem_right not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem := + ExtDHashMap.Const.get_union_of_mem_right mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := + ExtDHashMap.Const.get_union_of_not_mem_left not_mem + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + ExtDHashMap.Const.getD_union + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := + ExtDHashMap.Const.getD_union_of_not_mem_left not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := + ExtDHashMap.Const.getD_union_of_not_mem_right not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + ExtDHashMap.Const.get!_union + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := + ExtDHashMap.Const.get!_union_of_not_mem_left not_mem + +theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := + ExtDHashMap.Const.get!_union_of_not_mem_right not_mem + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := + ExtDHashMap.getKey?_union + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := + ExtDHashMap.getKey?_union_of_not_mem_left not_mem + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right mem) = m₂.getKey k mem := + ExtDHashMap.getKey_union_of_mem_right mem + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h' not_mem) := + ExtDHashMap.getKey_union_of_not_mem_left not_mem + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h' not_mem) := + ExtDHashMap.getKey_union_of_not_mem_right not_mem + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := + ExtDHashMap.getKeyD_union + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback := + ExtDHashMap.getKeyD_union_of_not_mem_left not_mem + +theorem getKeyD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + ExtDHashMap.getKeyD_union_of_not_mem_right not_mem + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := + ExtDHashMap.getKey!_union + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := + ExtDHashMap.getKey!_union_of_not_mem_left not_mem + +theorem getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := + ExtDHashMap.getKey!_union_of_not_mem_right not_mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + ExtDHashMap.size_union_of_not_mem + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + ExtDHashMap.size_left_le_size_union + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + ExtDHashMap.size_right_le_size_union + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + ExtDHashMap.size_union_le_size_add_size + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + ExtDHashMap.isEmpty_union + +end Union + section Alter variable {m : ExtHashMap α β} diff --git a/src/Std/Data/ExtHashSet/Basic.lean b/src/Std/Data/ExtHashSet/Basic.lean index f83c46cfed..830efa81bb 100644 --- a/src/Std/Data/ExtHashSet/Basic.lean +++ b/src/Std/Data/ExtHashSet/Basic.lean @@ -193,6 +193,17 @@ appearance. (m : ExtHashSet α) (l : ρ) : ExtHashSet α := ⟨m.inner.insertManyIfNewUnit l⟩ +/-- +Computes the union of the given hash sets. + +This function always merges the smaller set into the larger set, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] +def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : ExtHashSet α := ⟨ExtHashMap.union m₁.inner m₂.inner⟩ + +instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashSet α) := ⟨union⟩ + /-- Creates a hash set from an array of elements. Note that unlike repeatedly calling `insert`, if the collection contains multiple elements that are equal (with regard to `==`), then the last element diff --git a/src/Std/Data/ExtHashSet/Lemmas.lean b/src/Std/Data/ExtHashSet/Lemmas.lean index bbe1ea6473..8306c9cb6a 100644 --- a/src/Std/Data/ExtHashSet/Lemmas.lean +++ b/src/Std/Data/ExtHashSet/Lemmas.lean @@ -751,4 +751,127 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α] end filter +section Union + +variable (m₁ m₂ : ExtHashSet α) + +variable {m₁ m₂} + +@[simp] +theorem union_eq [EquivBEq α] [LawfulHashable α] : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + ExtHashMap.contains_union + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + ExtHashMap.mem_union_of_left + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + ExtHashMap.mem_union_of_right + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + ExtHashMap.mem_union_iff + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + ExtHashMap.mem_of_mem_union_of_not_mem_right + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + ExtHashMap.mem_of_mem_union_of_not_mem_left + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + ExtHashMap.getKey?_union + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := + ExtHashMap.getKey?_union_of_not_mem_left not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem := + ExtHashMap.getKey_union_of_mem_right mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := + ExtHashMap.getKey_union_of_not_mem_left not_mem + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) := + ExtHashMap.getKey_union_of_not_mem_right not_mem + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + ExtHashMap.getKeyD_union + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := + ExtHashMap.getKeyD_union_of_not_mem_left not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := + ExtHashMap.getKeyD_union_of_not_mem_right not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + ExtHashMap.getKey!_union + +theorem get!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := + ExtHashMap.getKey!_union_of_not_mem_left not_mem + +theorem get!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := + ExtHashMap.getKey!_union_of_not_mem_right not_mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + ExtHashMap.size_union_of_not_mem + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + ExtHashMap.size_left_le_size_union + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + ExtHashMap.size_right_le_size_union + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + ExtHashMap.size_union_le_size_add_size + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + ExtHashMap.isEmpty_union + +end Union + end Std.ExtHashSet diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index af5950f5e2..748012a4ee 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -253,7 +253,7 @@ instance [BEq α] [Hashable α] {m : Type w → Type w'} : ForIn m (HashMap α m.inner.keysArray /-- -Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +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. This function always merges the smaller map into the larger map, so the expected runtime is diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 70b0aef882..18d7bfb8db 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -1303,6 +1303,16 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] @DHashMap.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k /- Equiv -/ +theorem union_equiv_congr_left {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := + ⟨DHashMap.union_equiv_congr_left equiv.1⟩ + +theorem union_equiv_congr_right {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := + ⟨DHashMap.union_equiv_congr_right equiv.1⟩ + theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : α × β} : (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) := ⟨@DHashMap.union_insert_right_equiv_insert_union _ _ _ _ m₁.inner m₂.inner _ _ ⟨p.fst, p.snd⟩⟩ diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 85126dd4a6..b9e511d327 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1265,6 +1265,16 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] @DHashMap.Raw.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k /- Equiv -/ +theorem union_equiv_congr_left {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := + ⟨@DHashMap.Raw.union_equiv_congr_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem union_equiv_congr_right {m₃ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := + ⟨@DHashMap.Raw.union_equiv_congr_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : α × β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) := diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 3ee84bdaac..d0c99466f6 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -761,7 +761,18 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := @HashMap.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k -/- getKey? -/ +/- Equiv -/ +theorem union_equiv_congr_left {m₃ : HashSet α} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := + ⟨HashMap.union_equiv_congr_left equiv.1⟩ + +theorem union_equiv_congr_right {m₃ : HashSet α} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := + ⟨HashMap.union_equiv_congr_right equiv.1⟩ + +/- get? -/ theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := @HashMap.getKey?_union _ _ _ _ m₁.inner m₂.inner _ _ k diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 7455f3e985..1a6e50ab7d 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -789,6 +789,17 @@ theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := @HashMap.Raw.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k +/- Equiv -/ +theorem union_equiv_congr_left {m₃ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₁ ~m m₂) : + (m₁ ∪ m₃) ~m (m₂ ∪ m₃) := + ⟨@HashMap.Raw.union_equiv_congr_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem union_equiv_congr_right {m₃ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) + (equiv : m₂ ~m m₃) : + (m₁ ∪ m₂) ~m (m₁ ∪ m₃) := + ⟨@HashMap.Raw.union_equiv_congr_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + /- get? -/ theorem get?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF)