From 89d4e9bd4ccd7c751c3628a00eaf3fdc00f9e9d6 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Wojciech=20R=C3=B3=C5=BCowski?= Date: Thu, 20 Nov 2025 15:24:28 +0000 Subject: [PATCH] feat: add intersection for `ExtDHashMap`/`ExtHashMap`/`ExtHashSet` (#11241) This PR provides intersection operation for `ExtDHashMap`/`ExtHashMap`/`ExtHashSet` and proves several lemmas about it. --------- Co-authored-by: Markus Himmel --- src/Std/Data/DHashMap/Internal/RawLemmas.lean | 26 ++ src/Std/Data/DHashMap/Lemmas.lean | 16 + src/Std/Data/DHashMap/Raw.lean | 6 +- src/Std/Data/DHashMap/RawLemmas.lean | 31 ++ src/Std/Data/ExtDHashMap/Basic.lean | 11 + src/Std/Data/ExtDHashMap/Lemmas.lean | 335 ++++++++++++++++++ src/Std/Data/ExtHashMap/Basic.lean | 5 + src/Std/Data/ExtHashMap/Lemmas.lean | 215 +++++++++++ src/Std/Data/ExtHashSet/Basic.lean | 10 + src/Std/Data/ExtHashSet/Lemmas.lean | 143 ++++++++ src/Std/Data/HashMap/Lemmas.lean | 16 + src/Std/Data/HashMap/Raw.lean | 4 +- src/Std/Data/HashMap/RawLemmas.lean | 16 + src/Std/Data/HashSet/Lemmas.lean | 16 + src/Std/Data/HashSet/Raw.lean | 5 +- src/Std/Data/HashSet/RawLemmas.lean | 16 + src/Std/Data/Internal/List/Associative.lean | 26 ++ 17 files changed, 893 insertions(+), 4 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index bf06ebae39..d36e936c83 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -3019,6 +3019,32 @@ theorem contains_inter_eq_false_of_contains_eq_false_right [EquivBEq α] [Lawful revert h simp_to_model [inter, contains] using containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right +/- Equiv -/ + +theorem Equiv.inter_left {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₁.1.Equiv m₂.1) : + (m₁.inter m₃).1.Equiv (m₂.inter m₃).1 := by + revert equiv + simp_to_model [Equiv, inter] using List.Perm.filter + +theorem Equiv.inter_right {m₃ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (equiv : m₂.1.Equiv m₃.1) : + (m₁.inter m₂).1.Equiv (m₁.inter m₃).1 := by + revert equiv + simp_to_model [Equiv, inter] + intro equiv + apply perm_filter_containsKey_of_perm equiv + all_goals wf_trivial + +theorem Equiv.inter_congr {m₃ m₄ : Raw₀ α β} [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h₃ : m₃.val.WF) (h₄ : m₄.val.WF) (equiv₁ : m₁.1.Equiv m₃.1) (equiv₂ : m₂.1.Equiv m₄.1) : + (m₁.inter m₂).1.Equiv (m₃.inter m₄).1 := by + revert equiv₁ equiv₂ + simp_to_model [Equiv, inter] + intro equiv₁ equiv₂ + apply List.congr_filter_containsKey_of_perm + all_goals wf_trivial + /- get? -/ theorem get?_inter [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : (m₁.inter m₂).get? k = diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 7e63f8a539..6c02757d41 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -2178,6 +2178,22 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α rw [← contains_eq_false_iff_not_mem] at not_mem ⊢ exact @Raw₀.contains_inter_eq_false_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k not_mem +/- Equiv -/ +theorem Equiv.inter_left {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∩ m₃) ~m (m₂ ∩ m₃) := + ⟨@Raw₀.Equiv.inter_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 Equiv.inter_right {m₃ : DHashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∩ m₂) ~m (m₁ ∩ m₃) := + ⟨@Raw₀.Equiv.inter_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 Equiv.inter_congr {m₃ m₄ : DHashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := + ⟨@Raw₀.Equiv.inter_congr α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨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 m₄.2 equiv₁.1 equiv₂.1⟩ + /- get? -/ theorem get?_inter [LawfulBEq α] {k : α} : (m₁ ∩ m₂).get? k = diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index fbdc6ea5a5..466558a556 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -766,11 +766,13 @@ theorem WF.union₀ [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁. . exact (Raw₀.insertManyIfNew ⟨m₂, h₂.size_buckets_pos⟩ m₁).2 _ WF.insertIfNew₀ h₂ . exact (Raw₀.insertMany ⟨m₁, h₁.size_buckets_pos⟩ m₂).2 _ WF.insert₀ h₁ -theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂ : Raw α β).WF := by +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ m₂ : Raw α β).WF := by + simp only [Union.union] simp [Std.DHashMap.Raw.union, h₁.size_buckets_pos, h₂.size_buckets_pos] exact WF.union₀ h₁ h₂ -theorem WF.inter [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.inter m₂ : Raw α β).WF := by +theorem WF.inter [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∩ m₂ : Raw α β).WF := by + simp only [Inter.inter] simp [Std.DHashMap.Raw.inter, h₁.size_buckets_pos, h₂.size_buckets_pos] exact WF.inter₀ h₁ h₂ diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index e24813fcd5..3db501b1d3 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -2475,6 +2475,37 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] revert not_mem simp_to_raw using Raw₀.contains_inter_eq_false_of_contains_eq_false_right +/- Equiv -/ +theorem Equiv.inter_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 [Inter.inter] + simp_to_raw + intro hyp + apply Raw₀.Equiv.inter_left + all_goals wf_trivial + +theorem Equiv.inter_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 [Inter.inter] + simp_to_raw + intro hyp + apply Raw₀.Equiv.inter_right + all_goals wf_trivial + +theorem Equiv.inter_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := by + revert equiv₁ equiv₂ + simp only [Inter.inter] + simp_to_raw + intro equiv₁ equiv₂ + apply Raw₀.Equiv.inter_congr + all_goals wf_trivial + /- get? -/ theorem get?_inter [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : (m₁ ∩ m₂).get? k = diff --git a/src/Std/Data/ExtDHashMap/Basic.lean b/src/Std/Data/ExtDHashMap/Basic.lean index 706beda460..e3fc0e146d 100644 --- a/src/Std/Data/ExtDHashMap/Basic.lean +++ b/src/Std/Data/ExtDHashMap/Basic.lean @@ -365,6 +365,17 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtDHashMap α β) : Ex instance [EquivBEq α] [LawfulHashable α] : Union (ExtDHashMap α β) := ⟨union⟩ +@[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 + simp only [DHashMap.inter_eq, mk'.injEq] + apply Quotient.sound + apply DHashMap.Equiv.inter_congr + · exact equiv₁ + · exact equiv₂) m₁ m₂ + +instance [EquivBEq α] [LawfulHashable α] : Inter (ExtDHashMap α β) := ⟨inter⟩ + @[inline, inherit_doc DHashMap.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) : ExtDHashMap α (fun _ => Unit) := diff --git a/src/Std/Data/ExtDHashMap/Lemmas.lean b/src/Std/Data/ExtDHashMap/Lemmas.lean index af6037780d..46b894f590 100644 --- a/src/Std/Data/ExtDHashMap/Lemmas.lean +++ b/src/Std/Data/ExtDHashMap/Lemmas.lean @@ -2418,6 +2418,341 @@ theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited end Const +section Inter + +variable (m₁ m₂ : ExtDHashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem inter_eq [EquivBEq α] [LawfulHashable α] : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.contains_inter + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.mem_inter_iff + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ => DHashMap.not_mem_inter_of_not_mem_left + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ => DHashMap.not_mem_inter_of_not_mem_right + +/- get? -/ +theorem get?_inter [LawfulBEq α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.get?_inter + +theorem get?_inter_of_mem_right [LawfulBEq α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get?_inter_of_mem_right h + +theorem get?_inter_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get?_inter_of_not_mem_left h + +theorem get?_inter_of_not_mem_right [LawfulBEq α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get?_inter_of_not_mem_right h + +/- get -/ +@[simp] +theorem get_inter [LawfulBEq α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).get k h_mem = + m₁.get k (mem_inter_iff.1 h_mem).1 := by + induction m₁ + case mk a => + induction m₂ + case mk b => + apply DHashMap.get_inter + +/- getD -/ +theorem getD_inter [LawfulBEq α] {k : α} {fallback : β k} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getD_inter + +theorem getD_inter_of_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getD_inter_of_mem_right h + +theorem getD_inter_of_not_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getD_inter_of_not_mem_right h + +theorem getD_inter_of_not_mem_left [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getD_inter_of_not_mem_left h + +/- get! -/ +theorem get!_inter [LawfulBEq α] {k : α} [Inhabited (β k)] : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.get!_inter + +theorem get!_inter_of_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get!_inter_of_mem_right h + +theorem get!_inter_of_not_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get!_inter_of_not_mem_right h + +theorem get!_inter_of_not_mem_left [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.get!_inter_of_not_mem_left h + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKey?_inter + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey?_inter_of_mem_right h + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey?_inter_of_not_mem_right h + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey?_inter_of_not_mem_left h + +/- getKey -/ +@[simp] +theorem getKey_inter [EquivBEq α] [LawfulHashable α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).getKey k h_mem = + m₁.getKey k (mem_inter_iff.1 h_mem).1 := by + induction m₁ + case mk a => + induction m₂ + case mk b => + apply DHashMap.getKey_inter + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKeyD_inter + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKeyD_inter_of_mem_right h + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKeyD_inter_of_not_mem_right h + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKeyD_inter_of_not_mem_left h + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.getKey!_inter + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey!_inter_of_mem_right h + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey!_inter_of_not_mem_right h + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.getKey!_inter_of_not_mem_left h + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_inter_le_size_left + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_inter_le_size_right + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + m₁.inductionOn₂ m₂ (fun _ _ => DHashMap.size_inter_eq_size_left) h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + m₁.inductionOn₂ m₂ (fun _ _ => DHashMap.size_inter_eq_size_right) h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.size_add_size_eq_size_union_add_size_inter + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := by + revert h + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.isEmpty_inter_left h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := by + revert h + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.isEmpty_inter_right h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.isEmpty_inter_iff + +end Inter + +namespace Const + +variable {β : Type v} {m₁ m₂ : ExtDHashMap α (fun _ => β)} + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + Const.get? (m₁.inter m₂) k = + if k ∈ m₂ then Const.get? m₁ k else none := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.get?_inter + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + Const.get? (m₁.inter m₂) k = Const.get? m₁ k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get?_inter_of_mem_right h + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + Const.get? (m₁.inter m₂) k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get?_inter_of_not_mem_left h + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + Const.get? (m₁.inter m₂) k = none := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get?_inter_of_not_mem_right h + +/- get -/ +@[simp] +theorem get_inter [EquivBEq α] [LawfulHashable α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + Const.get (m₁.inter m₂) k h_mem = + Const.get m₁ k (mem_inter_iff.1 h_mem).1 := by + induction m₁ + case mk a => + induction m₂ + case mk b => + apply DHashMap.Const.get_inter + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + Const.getD (m₁.inter m₂) k fallback = + if k ∈ m₂ then Const.getD m₁ k fallback else fallback := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.getD_inter + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (mem : k ∈ m₂) : + Const.getD (m₁.inter m₂) k fallback = Const.getD m₁ k fallback := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.getD_inter_of_mem_right h + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₂) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.getD_inter_of_not_mem_right h + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₁) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.getD_inter_of_not_mem_left h + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : + Const.get! (m₁.inter m₂) k = + if k ∈ m₂ then Const.get! m₁ k else default := + m₁.inductionOn₂ m₂ fun _ _ => DHashMap.Const.get!_inter + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (mem : k ∈ m₂) : + Const.get! (m₁.inter m₂) k = Const.get! m₁ k := by + revert mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get!_inter_of_mem_right h + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : k ∉ m₂) : + Const.get! (m₁.inter m₂) k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get!_inter_of_not_mem_right h + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : k ∉ m₁) : + Const.get! (m₁.inter m₂) k = default := by + revert not_mem + exact m₁.inductionOn₂ m₂ fun _ _ h => DHashMap.Const.get!_inter_of_not_mem_left 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 838f55494b..1695280b06 100644 --- a/src/Std/Data/ExtHashMap/Basic.lean +++ b/src/Std/Data/ExtHashMap/Basic.lean @@ -249,6 +249,11 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : Ext instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashMap α β) := ⟨union⟩ +@[inline, inherit_doc ExtDHashMap.inter] +def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashMap α β) : ExtHashMap α β := ⟨ExtDHashMap.inter m₁.inner m₂.inner⟩ + +instance [EquivBEq α] [LawfulHashable α] : Inter (ExtHashMap α β) := ⟨inter⟩ + @[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 52cf39a62b..c1d237aadf 100644 --- a/src/Std/Data/ExtHashMap/Lemmas.lean +++ b/src/Std/Data/ExtHashMap/Lemmas.lean @@ -1546,6 +1546,221 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : end Union +section Inter + +variable (m₁ m₂ : ExtHashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem inter_eq [EquivBEq α] [LawfulHashable α] : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := + ExtDHashMap.contains_inter + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + ExtDHashMap.mem_inter_iff + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + ExtDHashMap.not_mem_inter_of_not_mem_left not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + ExtDHashMap.not_mem_inter_of_not_mem_right not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + ExtDHashMap.Const.get?_inter + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + ExtDHashMap.Const.get?_inter_of_mem_right mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := + ExtDHashMap.Const.get?_inter_of_not_mem_left not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := + ExtDHashMap.Const.get?_inter_of_not_mem_right not_mem + +/- get -/ +@[simp] +theorem get_inter [EquivBEq α] [LawfulHashable α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).get k h_mem = + m₁.get k (mem_inter_iff.1 h_mem).1 := + ExtDHashMap.Const.get_inter + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + ExtDHashMap.Const.getD_inter + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + ExtDHashMap.Const.getD_inter_of_mem_right mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := + ExtDHashMap.Const.getD_inter_of_not_mem_right not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := + ExtDHashMap.Const.getD_inter_of_not_mem_left not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + ExtDHashMap.Const.get!_inter + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + ExtDHashMap.Const.get!_inter_of_mem_right mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := + ExtDHashMap.Const.get!_inter_of_not_mem_right not_mem + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := + ExtDHashMap.Const.get!_inter_of_not_mem_left not_mem + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := + ExtDHashMap.getKey?_inter + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := + ExtDHashMap.getKey?_inter_of_mem_right mem + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := + ExtDHashMap.getKey?_inter_of_not_mem_right not_mem + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := + ExtDHashMap.getKey?_inter_of_not_mem_left not_mem + +/- getKey -/ +@[simp] +theorem getKey_inter [EquivBEq α] [LawfulHashable α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).getKey k h_mem = + m₁.getKey k (mem_inter_iff.1 h_mem).1 := + ExtDHashMap.getKey_inter + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := + ExtDHashMap.getKeyD_inter + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + ExtDHashMap.getKeyD_inter_of_mem_right mem + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + ExtDHashMap.getKeyD_inter_of_not_mem_right not_mem + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + ExtDHashMap.getKeyD_inter_of_not_mem_left not_mem + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := + ExtDHashMap.getKey!_inter + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := + ExtDHashMap.getKey!_inter_of_mem_right mem + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := + ExtDHashMap.getKey!_inter_of_not_mem_right not_mem + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := + ExtDHashMap.getKey!_inter_of_not_mem_left not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + ExtDHashMap.size_inter_le_size_left + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + ExtDHashMap.size_inter_le_size_right + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + ExtDHashMap.size_inter_eq_size_left h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + ExtDHashMap.size_inter_eq_size_right h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + ExtDHashMap.size_add_size_eq_size_union_add_size_inter + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + ExtDHashMap.isEmpty_inter_left h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + ExtDHashMap.isEmpty_inter_right h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + ExtDHashMap.isEmpty_inter_iff + +end Inter + section Alter variable {m : ExtHashMap α β} diff --git a/src/Std/Data/ExtHashSet/Basic.lean b/src/Std/Data/ExtHashSet/Basic.lean index 830efa81bb..43590d6752 100644 --- a/src/Std/Data/ExtHashSet/Basic.lean +++ b/src/Std/Data/ExtHashSet/Basic.lean @@ -204,6 +204,16 @@ def union [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : ExtHas instance [EquivBEq α] [LawfulHashable α] : Union (ExtHashSet α) := ⟨union⟩ +/-- +Computes the intersection of the given hash sets. + +This function always iterates through the smaller set. +-/ +@[inline] +def inter [EquivBEq α] [LawfulHashable α] (m₁ m₂ : ExtHashSet α) : ExtHashSet α := ⟨ExtHashMap.inter m₁.inner m₂.inner⟩ + +instance [EquivBEq α] [LawfulHashable α] : Inter (ExtHashSet α) := ⟨inter⟩ + /-- 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 8306c9cb6a..ddf512a061 100644 --- a/src/Std/Data/ExtHashSet/Lemmas.lean +++ b/src/Std/Data/ExtHashSet/Lemmas.lean @@ -874,4 +874,147 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : end Union +section Inter + +variable (m₁ m₂ : ExtHashSet α) + +variable {m₁ m₂} + +@[simp] +theorem inter_eq [EquivBEq α] [LawfulHashable α] : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := + ExtHashMap.contains_inter + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + ExtHashMap.mem_inter_iff + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + ExtHashMap.not_mem_inter_of_not_mem_left not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + ExtHashMap.not_mem_inter_of_not_mem_right not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + ExtHashMap.getKey?_inter + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + ExtHashMap.getKey?_inter_of_mem_right mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := + ExtHashMap.getKey?_inter_of_not_mem_left not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := + ExtHashMap.getKey?_inter_of_not_mem_right not_mem + +/- get -/ +@[simp] +theorem get_inter [EquivBEq α] [LawfulHashable α] + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).get k h_mem = + m₁.get k (mem_inter_iff.1 h_mem).1 := + ExtHashMap.getKey_inter + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + ExtHashMap.getKeyD_inter + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + ExtHashMap.getKeyD_inter_of_mem_right mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := + ExtHashMap.getKeyD_inter_of_not_mem_right not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := + ExtHashMap.getKeyD_inter_of_not_mem_left not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + ExtHashMap.getKey!_inter + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + ExtHashMap.getKey!_inter_of_mem_right mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := + ExtHashMap.getKey!_inter_of_not_mem_right not_mem + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := + ExtHashMap.getKey!_inter_of_not_mem_left not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + ExtHashMap.size_inter_le_size_left + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + ExtHashMap.size_inter_le_size_right + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + ExtHashMap.size_inter_eq_size_left h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + ExtHashMap.size_inter_eq_size_right h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + ExtHashMap.size_add_size_eq_size_union_add_size_inter + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + ExtHashMap.isEmpty_inter_left h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + ExtHashMap.isEmpty_inter_right h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + ExtHashMap.isEmpty_inter_iff + +end Inter + end Std.ExtHashSet diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index d81fcff5f7..3206f16aa2 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -1589,6 +1589,22 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α k ∉ m₁ ∩ m₂ := @DHashMap.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem +/- Equiv -/ +theorem Equiv.inter_left {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∩ m₃) ~m (m₂ ∩ m₃) := + ⟨DHashMap.Equiv.inter_left equiv.1⟩ + +theorem Equiv.inter_right {m₃ : HashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∩ m₂) ~m (m₁ ∩ m₃) := + ⟨DHashMap.Equiv.inter_right equiv.1⟩ + +theorem Equiv.inter_congr {m₃ m₄ : HashMap α β} [EquivBEq α] [LawfulHashable α] + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := + ⟨DHashMap.Equiv.inter_congr equiv₁.1 equiv₂.1⟩ + /- get? -/ theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∩ m₂).get? k = diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 2c4ca703d6..585cd215c6 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -345,9 +345,11 @@ theorem WF.ofList [BEq α] [Hashable α] {l : List (α × β)} : (ofList l).WF : theorem WF.unitOfList [BEq α] [Hashable α] {l : List α} : (unitOfList l).WF := ⟨DHashMap.Raw.WF.Const.unitOfList⟩ -theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂).WF := +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ m₂).WF := ⟨DHashMap.Raw.WF.union h₁.out h₂.out⟩ +theorem WF.inter [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∩ m₂).WF := + ⟨DHashMap.Raw.WF.inter h₁.out h₂.out⟩ end Raw end HashMap diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 7de00b72f0..5b5be918c8 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1568,6 +1568,22 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] k ∉ m₁ ∩ m₂ := @DHashMap.Raw.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem +/- Equiv -/ +theorem Equiv.inter_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.Equiv.inter_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.inter_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.Equiv.inter_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.inter_congr {m₃ m₄ : Raw α β} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := + ⟨@DHashMap.Raw.Equiv.inter_congr _ _ _ _ m₁.inner m₂.inner m₃.inner m₄.inner _ _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩ + /- get? -/ theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : get? (m₁ ∩ m₂) k = diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 3477057f09..e3a560bfb2 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -952,6 +952,22 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α k ∉ m₁ ∩ m₂ := @HashMap.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem +/- Equiv -/ +theorem Equiv.inter_left {m₃ : HashSet α} [EquivBEq α] [LawfulHashable α] + (equiv : m₁ ~m m₂) : + (m₁ ∩ m₃) ~m (m₂ ∩ m₃) := + ⟨HashMap.Equiv.inter_left equiv.1⟩ + +theorem Equiv.inter_right {m₃ : HashSet α} [EquivBEq α] [LawfulHashable α] + (equiv : m₂ ~m m₃) : + (m₁ ∩ m₂) ~m (m₁ ∩ m₃) := + ⟨HashMap.Equiv.inter_right equiv.1⟩ + +theorem Equiv.inter_congr {m₃ m₄ : HashSet α} [EquivBEq α] [LawfulHashable α] + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := + ⟨HashMap.Equiv.inter_congr equiv₁.1 equiv₂.1⟩ + /- get? -/ theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : (m₁ ∩ m₂).get? k = diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index 49824e3e7f..c314cbd87e 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -325,9 +325,12 @@ theorem WF.ofList [BEq α] [Hashable α] {l : List α} : (ofList l : Raw α).WF := ⟨HashMap.Raw.WF.unitOfList⟩ -theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂).WF := +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∪ m₂).WF := ⟨HashMap.Raw.WF.union h₁.out h₂.out⟩ +theorem WF.inter [BEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁ ∩ m₂).WF := + ⟨HashMap.Raw.WF.inter h₁.out h₂.out⟩ + end Raw end HashSet diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 3015d058b9..b8a9f45956 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -1002,6 +1002,22 @@ theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] k ∉ m₁ ∩ m₂ := @HashMap.Raw.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem +/- Equiv -/ +theorem Equiv.inter_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.Equiv.inter_left _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.inter_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.Equiv.inter_right _ _ _ _ m₁.inner m₂.inner m₃.inner _ _ h₁.out h₂.out h₃.out equiv.1⟩ + +theorem Equiv.inter_congr {m₃ m₄ : Raw α} [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h₃ : m₃.WF) (h₄ : m₄.WF) + (equiv₁ : m₁ ~m m₃) (equiv₂ : m₂ ~m m₄) : + (m₁ ∩ m₂) ~m (m₃ ∩ m₄) := + ⟨@HashMap.Raw.Equiv.inter_congr _ _ _ _ m₁.inner m₂.inner m₃.inner m₄.inner _ _ h₁.out h₂.out h₃.out h₄.out equiv₁.1 equiv₂.1⟩ + /- get? -/ theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 1de4b9d3f0..bb9d81e3f5 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -5487,6 +5487,32 @@ theorem containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right [B . simp [h] . exact hl₁ +theorem perm_filter_containsKey_of_perm {l₁ l₂ l₃ : List ((a : α) × β a)} + [BEq α] [EquivBEq α] + (h : l₂.Perm l₃) + (wf₁ : DistinctKeys l₁) : + (l₁.filter (fun p => containsKey p.fst l₂)).Perm (l₁.filter (fun p => containsKey p.1 l₃)) := by + induction l₁ + case nil => simp + case cons hd tl ih => + rw [List.distinctKeys_cons_iff] at wf₁ + rw [List.filter_cons, List.filter_cons] + rw [List.containsKey_of_perm h] + specialize ih wf₁.1 + split + · simp only [List.perm_cons, ih] + · simp [ih] + +theorem congr_filter_containsKey_of_perm {l₁ l₂ l₃ l₄ : List ((a : α) × β a)} + [BEq α] [EquivBEq α] + (h₁ : l₁.Perm l₃) (h₂ : l₂.Perm l₄) + (hd : DistinctKeys l₃) : + (l₁.filter (fun p => containsKey p.fst l₂)).Perm (l₃.filter (fun p => containsKey p.1 l₄)) := by + apply Perm.trans + · apply List.Perm.filter + · exact h₁ + · apply perm_filter_containsKey_of_perm h₂ hd + theorem List.getValue?_filter_containsKey {β : Type v} [BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} (dl₁ : DistinctKeys l₁) :