diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 1d2f9f21b1..88abac99b4 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -336,7 +336,18 @@ This function always merges the smaller map into the larger map, so the expected inner := Raw₀.union ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ wf := Std.DHashMap.Raw.WF.union₀ m₁.2 m₂.2 +/-- +Computes the intersection of the given hash maps. The result will only contain entries from the first map. + +This function always iterates through the smaller map, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def inter [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β where + inner := Raw₀.inter ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ + wf := Std.DHashMap.Raw.WF.inter₀ m₁.2 m₂.2 + instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩ +instance [BEq α] [Hashable α] : Inter (DHashMap α β) := ⟨inter⟩ section Unverified diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index b776bfc730..effe67fb01 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -461,10 +461,25 @@ def insertMany {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [BEq α] [Hashable r := ⟨r.1.insertIfNew a b, fun _ h hm => h (r.2 _ h hm)⟩ return r +/-- Internal implementation detail of the hash map -/ +@[inline] +def interSmallerFn [BEq α] [Hashable α] (m sofar : Raw₀ α β) (k : α) : Raw₀ α β := + match m.getEntry? k with + | some kv' => sofar.insert kv'.1 kv'.2 + | none => sofar + +/-- Internal implementation detail of the hash map -/ +def interSmaller [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) : Raw₀ α β := + (m₂.fold (fun sofar k _ => interSmallerFn m₁ sofar k) emptyWithCapacity) + /-- Internal implementation detail of the hash map -/ @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := if m₁.1.size ≤ m₂.1.size then (m₂.insertManyIfNew m₁.1).1 else (m₁.insertMany m₂.1).1 +/-- Internal implementation detail of the hash map -/ +def inter [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := + if m₁.1.size ≤ m₂.1.size then m₁.filter fun k _ => m₂.contains k else interSmaller m₁ m₂ + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 5237e19a4d..c70aaf7c3d 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -420,6 +420,12 @@ def unionₘ [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := else insertListₘ m₁ (toListModel m₂.1.buckets) +/-- Internal implementation detail of the hash map -/ +def interSmallerFnₘ [BEq α] [Hashable α] (m sofar : Raw₀ α β) (k : α) : Raw₀ α β := + match m.getEntry?ₘ k with + | some kv' => sofar.insertₘ kv'.1 kv'.2 + | none => sofar + section variable {β : Type v} @@ -664,6 +670,14 @@ theorem insertManyIfNew_eq_insertListIfNewₘ [BEq α] [Hashable α] (m : Raw₀ simp only [List.foldl_cons, insertListIfNewₘ] apply ih +theorem interSmallerFn_eq_interSmallerFnₘ [BEq α] [Hashable α] (m sofar : Raw₀ α β) (k : α) : + interSmallerFn m sofar k = interSmallerFnₘ m sofar k := by + rw [interSmallerFn, interSmallerFnₘ] + rw [getEntry?_eq_getEntry?ₘ] + congr + ext + rw [insert_eq_insertₘ] + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index d7f2ee1a5c..b421e0f6ca 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -145,6 +145,10 @@ theorem union_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) m₁.union m₂ = Raw₀.union ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by simp [Raw.union, h₁.size_buckets_pos, h₂.size_buckets_pos] +theorem inter_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : + m₁.inter m₂ = Raw₀.inter ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩ := by + simp [Raw.inter, h₁.size_buckets_pos, h₂.size_buckets_pos] + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 936b237de4..bf06ebae39 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -107,7 +107,7 @@ macro_rules | apply Raw₀.wf_insertMany₀ | apply Raw₀.Const.wf_insertMany₀ | apply Raw₀.Const.wf_insertManyIfNewUnit₀ | apply Raw₀.wf_union₀ | apply Raw.WF.filter₀ | apply Raw₀.wf_map₀ | apply Raw₀.wf_filterMap₀ - | apply Raw.WF.emptyWithCapacity₀) <;> wf_trivial) + | apply Raw.WF.emptyWithCapacity₀ | apply Raw.WF.inter₀) <;> wf_trivial) /-- Internal implementation detail of the hash map -/ scoped macro "empty" : tactic => `(tactic| { intros; simp_all [List.isEmpty_iff] } ) @@ -121,6 +121,7 @@ private meta def modifyMap : Std.DHashMap Name (fun _ => Name) := ⟨`insertIfNew, ``toListModel_insertIfNew⟩, ⟨`insertMany, ``toListModel_insertMany_list⟩, ⟨`union, ``toListModel_union⟩, + ⟨`inter, ``toListModel_inter⟩, ⟨`Const.insertMany, ``Const.toListModel_insertMany_list⟩, ⟨`Const.insertManyIfNewUnit, ``Const.toListModel_insertManyIfNewUnit_list⟩, ⟨`alter, ``toListModel_alter⟩, @@ -2708,14 +2709,14 @@ theorem get_union_of_contains_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : revert contains_right simp_to_model [union, get, contains] intro contains_right - apply List.getValueCast_insertList_of_contains_right + apply getValueCast_insertList_of_contains_right all_goals wf_trivial theorem get_union_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₁.contains k = false) {h'} : (m₁.union m₂).get k h' = m₂.get k (contains_of_contains_union_of_contains_eq_false_left h₁ h₂ h' contains_eq_false) := by revert contains_eq_false - simp_to_model [union, contains, get] using List.getValueCast_insertList_of_contains_eq_false_left + simp_to_model [union, contains, get] using getValueCast_insertList_of_contains_eq_false_left theorem get_union_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) {h'} : @@ -2739,7 +2740,7 @@ theorem getD_union_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) revert contains_eq_false simp_to_model [union, contains, getD] intro contains_eq_false - apply List.getValueCastD_insertList_of_contains_eq_false_left + apply getValueCastD_insertList_of_contains_eq_false_left all_goals wf_trivial theorem getD_union_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) @@ -2766,7 +2767,7 @@ theorem get!_union_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) revert contains_eq_false simp_to_model [union, contains, get!] intro contains_eq_false - apply List.getValueCastD_insertList_of_contains_eq_false_left + apply getValueCastD_insertList_of_contains_eq_false_left all_goals wf_trivial theorem get!_union_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) @@ -2816,7 +2817,7 @@ theorem getKey_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] {k : α} (contains_eq_false : m₁.contains k = false) {h'} : (m₁.union m₂).getKey k h' = m₂.getKey k (contains_of_contains_union_of_contains_eq_false_left h₁ h₂ h' contains_eq_false) := by revert contains_eq_false - simp_to_model [union, contains, getKey] using List.getKey_insertList_of_contains_eq_false_left + simp_to_model [union, contains, getKey] using getKey_insertList_of_contains_eq_false_left theorem getKey_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) {h'} : @@ -2841,7 +2842,7 @@ theorem getKeyD_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α revert h' simp_to_model [contains, union, getKeyD] intro h' - apply List.getKeyD_insertList_of_contains_eq_false_left + apply getKeyD_insertList_of_contains_eq_false_left . wf_trivial . wf_trivial . exact h' @@ -2852,7 +2853,7 @@ theorem getKeyD_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable revert h' simp_to_model [contains, union, getKeyD] intro h' - apply List.getKeyD_insertList_of_contains_eq_false_right h' + apply getKeyD_insertList_of_contains_eq_false_right h' /- getKey! -/ theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] @@ -2866,14 +2867,14 @@ theorem getKey!_union_of_contains_eq_false_left [Inhabited α] (h' : m₁.contains k = false) : (m₁.union m₂).getKey! k = m₂.getKey! k := by revert h' - simp_to_model [getKey!, contains, union] using List.getKeyD_insertList_of_contains_eq_false_left + simp_to_model [getKey!, contains, union] using getKeyD_insertList_of_contains_eq_false_left theorem getKey!_union_of_contains_eq_false_right [Inhabited α] [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (h' : m₂.contains k = false) : (m₁.union m₂).getKey! k = m₁.getKey! k := by revert h' - simp_to_model [contains, union, getKey!] using List.getKeyD_insertList_of_contains_eq_false_right + simp_to_model [contains, union, getKey!] using getKeyD_insertList_of_contains_eq_false_right /- size -/ theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) @@ -2899,6 +2900,7 @@ theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : (m₁.union m₂).1.isEmpty = (m₁.1.isEmpty && m₂.1.isEmpty) := by simp_to_model [isEmpty, union] using List.isEmpty_insertList + end Union namespace Const @@ -2908,13 +2910,13 @@ variable {β : Type v} {m₁ m₂ : Raw₀ α (fun _ => β)} /- get? -/ theorem get?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : Const.get? (m₁.union m₂) k = (Const.get? m₂ k).or (Const.get? m₁ k) := by - simp_to_model [union, Const.get?] using List.getValue?_insertList + simp_to_model [union, Const.get?] using getValue?_insertList theorem get?_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₁.contains k = false) : Const.get? (m₁.union m₂) k = Const.get? m₂ k := by revert contains_eq_false - simp_to_model [union, contains, Const.get?] using List.getValue?_insertList_of_contains_eq_false_left + simp_to_model [union, contains, Const.get?] using getValue?_insertList_of_contains_eq_false_left theorem get?_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) : @@ -2922,7 +2924,7 @@ theorem get?_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] revert contains_eq_false simp_to_model [union, Const.get?, contains] intro contains_eq_false - apply List.getValue?_insertList_of_contains_eq_false_right contains_eq_false + apply getValue?_insertList_of_contains_eq_false_right contains_eq_false /- get -/ theorem get_union_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) @@ -2931,14 +2933,14 @@ theorem get_union_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m revert h simp_to_model [union, contains, Const.get] intro h - apply List.getValue_insertList_of_contains_right + apply getValue_insertList_of_contains_right all_goals wf_trivial theorem get_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₁.contains k = false) {h'} : Const.get (m₁.union m₂) k h' = Const.get m₂ k (contains_of_contains_union_of_contains_eq_false_left h₁ h₂ h' contains_eq_false) := by revert contains_eq_false - simp_to_model [union, contains, Const.get] using List.getValue_insertList_of_contains_eq_false_left + simp_to_model [union, contains, Const.get] using getValue_insertList_of_contains_eq_false_left theorem get_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) {h'} : @@ -2946,7 +2948,7 @@ theorem get_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] ( revert contains_eq_false simp_to_model [union, Const.get, contains] intro contains_eq_false - apply List.getValue_insertList_of_contains_eq_false_right contains_eq_false + apply getValue_insertList_of_contains_eq_false_right contains_eq_false /- getD -/ theorem getD_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} {fallback : β} : @@ -2957,7 +2959,7 @@ theorem getD_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] ( {k : α} {fallback : β} (contains_eq_false : m₁.contains k = false) : Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k fallback := by revert contains_eq_false - simp_to_model [union, contains, Const.getD] using List.getValueD_insertList_of_contains_eq_false_left + simp_to_model [union, contains, Const.getD] using getValueD_insertList_of_contains_eq_false_left theorem getD_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} {fallback : β} (contains_eq_false : m₂.contains k = false) : @@ -2965,7 +2967,7 @@ theorem getD_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] revert contains_eq_false simp_to_model [union, Const.getD, contains] intro contains_eq_false - apply List.getValueD_insertList_of_contains_eq_false_right contains_eq_false + apply getValueD_insertList_of_contains_eq_false_right contains_eq_false /- get! -/ theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : @@ -2976,7 +2978,7 @@ theorem get!_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] [ {k : α} (contains_eq_false : m₁.contains k = false) : Const.get! (m₁.union m₂) k = Const.get! m₂ k := by revert contains_eq_false - simp_to_model [union, contains, Const.get!] using List.getValueD_insertList_of_contains_eq_false_left + simp_to_model [union, contains, Const.get!] using getValueD_insertList_of_contains_eq_false_left theorem get!_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (contains_eq_false : m₂.contains k = false) : @@ -2984,7 +2986,334 @@ theorem get!_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] revert contains_eq_false simp_to_model [union, Const.get!, contains] intro contains_eq_false - apply List.getValueD_insertList_of_contains_eq_false_right contains_eq_false + apply getValueD_insertList_of_contains_eq_false_right contains_eq_false + +end Const + +section Inter + +variable {m₁ m₂ : Raw₀ α β} + +/- contains -/ +theorem contains_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + (m₁.inter m₂).contains k = (m₁.contains k && m₂.contains k) := by + simp_to_model [contains, inter] using List.containsKey_filter_containsKey + +theorem contains_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + (m₁.inter m₂).contains k ↔ m₁.contains k ∧ m₂.contains k := by + simp_to_model [inter, contains] using containsKey_filter_containsKey_iff + +theorem contains_inter_eq_false_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} + (h : m₁.contains k = false) : + (m₁.inter m₂).contains k = false := by + revert h + simp_to_model [inter, contains] using containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left + +theorem contains_inter_eq_false_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} + (h : m₂.contains k = false) : + (m₁.inter m₂).contains k = false := by + revert h + simp_to_model [inter, contains] using containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + +/- get? -/ +theorem get?_inter [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + (m₁.inter m₂).get? k = + if m₂.contains k then m₁.get? k else none := by + simp_to_model [inter, get?, contains] using getValueCast?_filter_containsKey + +theorem get?_inter_of_contains_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k) : + (m₁.inter m₂).get? k = m₁.get? k := by + revert h + simp_to_model [inter, get?, contains] using getValueCast?_filter_containsKey_of_containsKey_right + +theorem get?_inter_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₁.contains k = false) : + (m₁.inter m₂).get? k = none := by + revert h + simp_to_model [inter, get?, contains] using getValueCast?_filter_containsKey_of_containsKey_eq_false_left + +theorem get?_inter_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k = false) : + (m₁.inter m₂).get? k = none := by + revert h + simp_to_model [inter, get?, contains] using getValueCast?_filter_containsKey_of_containsKey_eq_false_right + +/- get -/ +@[simp] theorem get_inter [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {h_contains : (m₁.inter m₂).contains k} : + (m₁.inter m₂).get k h_contains = + m₁.get k ((contains_inter_iff h₁ h₂).1 h_contains).1 := by + simp_to_model [inter, get, contains] using getValueCast_filter_containsKey + +/- getD -/ +theorem getD_inter [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} : + (m₁.inter m₂).getD k fallback = + if m₂.contains k then m₁.getD k fallback else fallback := by + simp_to_model [inter, getD, contains] using getValueCastD_filter_containsKey + +theorem getD_inter_of_contains_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} (h : m₂.contains k) : + (m₁.inter m₂).getD k fallback = m₁.getD k fallback := by + revert h + simp_to_model [inter, getD, contains] using getValueCastD_filter_containsKey_of_containsKey_right + +theorem getD_inter_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} (h : m₂.contains k = false) : + (m₁.inter m₂).getD k fallback = fallback := by + revert h + simp_to_model [inter, getD, contains] using getValueCastD_filter_containsKey_of_containsKey_eq_false_right + +theorem getD_inter_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} (h : m₁.contains k = false) : + (m₁.inter m₂).getD k fallback = fallback := by + revert h + simp_to_model [inter, getD, contains] using getValueCastD_filter_containsKey_of_containsKey_eq_false_left + +/- get! -/ +theorem get!_inter [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] : + (m₁.inter m₂).get! k = + if m₂.contains k then m₁.get! k else default := by + simp_to_model [inter, get!, contains] using getValueCastD_filter_containsKey + +theorem get!_inter_of_contains_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k) : + (m₁.inter m₂).get! k = m₁.get! k := by + revert h + simp_to_model [inter, get!, contains] using getValueCastD_filter_containsKey_of_containsKey_right + +theorem get!_inter_of_contains_eq_false_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] (h : m₂.contains k = false) : + (m₁.inter m₂).get! k = default := by + revert h + simp_to_model [inter, get!, contains] using getValueCastD_filter_containsKey_of_containsKey_eq_false_right + +theorem get!_inter_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] (h : m₁.contains k = false) : + (m₁.inter m₂).get! k = default := by + revert h + simp_to_model [inter, get!, contains] using getValueCastD_filter_containsKey_of_containsKey_eq_false_left + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + (m₁.inter m₂).getKey? k = + if m₂.contains k then m₁.getKey? k else none := by + simp_to_model [inter, contains, getKey?] using getKey?_filter_containsKey + +theorem getKey?_inter_of_contains_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (h : m₂.contains k) : + (m₁.inter m₂).getKey? k = m₁.getKey? k := by + revert h + simp_to_model [contains, getKey?, inter] using getKey?_filter_containsKey_of_containsKey_right + +theorem getKey?_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (h : m₂.contains k = false) : + (m₁.inter m₂).getKey? k = none := by + revert h + simp_to_model [contains, getKey?, inter] using getKey?_filter_containsKey_of_containsKey_eq_false_right + +theorem getKey?_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} (h : m₁.contains k = false) : + (m₁.inter m₂).getKey? k = none := by + revert h + simp_to_model [contains, getKey?, inter] using getKey?_filter_containsKey_of_containsKey_eq_false_left + +/- getKey -/ +@[simp] theorem getKey_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {h_contains : (m₁.inter m₂).contains k} : + (m₁.inter m₂).getKey k h_contains = + m₁.getKey k (by simp [contains_inter_iff h₁ h₂] at h_contains; exact h_contains.1) := by + simp_to_model [inter, contains, getKey] using getKey_filter_containsKey + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} : + (m₁.inter m₂).getKeyD k fallback = + if m₂.contains k then m₁.getKeyD k fallback else fallback := by + simp_to_model [inter, getKeyD, contains] using getKeyD_filter_containsKey + +theorem getKeyD_inter_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} (h : m₂.contains k) : + (m₁.inter m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + revert h + simp_to_model [inter, getKeyD, contains] using getKeyD_filter_containsKey_of_containsKey_right + +theorem getKeyD_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} (h : m₂.contains k = false) : + (m₁.inter m₂).getKeyD k fallback = fallback := by + revert h + simp_to_model [inter, getKeyD, contains] using getKeyD_filter_containsKey_of_containsKey_eq_false_right + +theorem getKeyD_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} (h : m₁.contains k = false) : + (m₁.inter m₂).getKeyD k fallback = fallback := by + revert h + simp_to_model [inter, getKeyD, contains] using getKeyD_filter_containsKey_of_containsKey_eq_false_left + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} [Inhabited α] : + (m₁.inter m₂).getKey! k = + if m₂.contains k then m₁.getKey! k else default := by + simp_to_model [inter, getKey!, contains] using getKeyD_filter_containsKey + +theorem getKey!_inter_of_contains_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} (h : m₂.contains k) : + (m₁.inter m₂).getKey! k = m₁.getKey! k := by + revert h + simp_to_model [inter, getKey!, contains] using getKeyD_filter_containsKey_of_containsKey_right + +theorem getKey!_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} (h : m₂.contains k = false) : + (m₁.inter m₂).getKey! k = default := by + revert h + simp_to_model [inter, getKey!, contains] using getKeyD_filter_containsKey_of_containsKey_eq_false_right + +theorem getKey!_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} (h : m₁.contains k = false) : + (m₁.inter m₂).getKey! k = default := by + revert h + simp_to_model [inter, getKey!, contains] using getKeyD_filter_containsKey_of_containsKey_eq_false_left + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + (m₁.inter m₂).1.size ≤ m₁.1.size := by + simp_to_model [inter, size] using List.length_filter_le + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + (m₁.inter m₂).1.size ≤ m₂.1.size := by + simp_to_model [inter, size, contains] using List.length_filter_containsKey_le + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + (h : ∀ (a : α), m₁.contains a → m₂.contains a) : + (m₁.inter m₂).1.size = m₁.1.size := by + revert h + simp_to_model [inter, size, contains] using length_filter_containsKey_eq_length_left + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + (h : ∀ (a : α), m₂.contains a → m₁.contains a) : + (m₁.inter m₂).1.size = m₂.1.size := by + revert h + simp_to_model [inter, size, contains] using length_filter_containsKey_of_length_right + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + m₁.1.size + m₂.1.size = (m₁.union m₂).1.size + (m₁.inter m₂).1.size := by + simp_to_model [union, inter, size] using size_add_size_eq_size_insertList_add_size_filter_containsKey + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h : m₁.1.isEmpty) : + (m₁.inter m₂).1.isEmpty = true := by + revert h + simp_to_model [isEmpty, inter, contains] using List.isEmpty_filter_containsKey_left + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) (h : m₂.1.isEmpty) : + (m₁.inter m₂).1.isEmpty = true := by + revert h + simp_to_model [isEmpty, inter, contains] using List.isEmpty_filter_containsKey_right + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + (m₁.inter m₂).1.isEmpty ↔ ∀ k, m₁.contains k → m₂.contains k = false := by + simp_to_model [inter, contains, isEmpty] using List.isEmpty_filter_containsKey_iff + +end Inter +namespace Const + +variable {β : Type v} {m₁ m₂ : Raw₀ α (fun _ => β)} + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + Const.get? (m₁.inter m₂) k = + if m₂.contains k then Const.get? m₁ k else none := by + simp_to_model [inter, Const.get?, contains] using List.getValue?_filter_containsKey + +theorem get?_inter_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k) : + Const.get? (m₁.inter m₂) k = Const.get? m₁ k := by + revert h + simp_to_model [inter, Const.get?, contains] using List.getValue?_filter_containsKey_of_containsKey_right + +theorem get?_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₁.contains k = false) : + Const.get? (m₁.inter m₂) k = none := by + revert h + simp_to_model [inter, Const.get?, contains] using List.getValue?_filter_containsKey_of_containsKey_eq_false_left + +theorem get?_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k = false) : + Const.get? (m₁.inter m₂) k = none := by + revert h + simp_to_model [inter, Const.get?, contains] using getValue?_filter_containsKey_of_containsKey_eq_false_right + +@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {h_contains : (m₁.inter m₂).contains k} : + Const.get (m₁.inter m₂) k h_contains = + Const.get m₁ k ((contains_inter_iff h₁ h₂).1 h_contains).1 := by + simp_to_model [inter, Const.get, contains] using List.getValue_filter_containsKey + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β} : + Const.getD (m₁.inter m₂) k fallback = + if m₂.contains k then Const.getD m₁ k fallback else fallback := by + simp_to_model [inter, Const.getD, contains] using List.getValueD_filter_containsKey + +theorem getD_inter_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β} (h : m₂.contains k) : + Const.getD (m₁.inter m₂) k fallback = Const.getD m₁ k fallback := by + revert h + simp_to_model [inter, Const.getD, contains] using List.getValueD_filter_containsKey_of_containsKey_right + +theorem getD_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β} (h : m₂.contains k = false) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + revert h + simp_to_model [inter, Const.getD, contains] using getValueD_filter_containsKey_of_containsKey_eq_false_right + +theorem getD_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β} (h : m₁.contains k = false) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + revert h + simp_to_model [inter, Const.getD, contains] using getValueD_filter_containsKey_of_containsKey_eq_false_left + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} : + Const.get! (m₁.inter m₂) k = + if m₂.contains k then Const.get! m₁ k else default := by + simp_to_model [inter, Const.get!, contains] using List.getValueD_filter_containsKey + +theorem get!_inter_of_contains_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k) : + Const.get! (m₁.inter m₂) k = Const.get! m₁ k := by + revert h + simp_to_model [inter, Const.get!, contains] using List.getValueD_filter_containsKey_of_containsKey_right + +theorem get!_inter_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k = false) : + Const.get! (m₁.inter m₂) k = default := by + revert h + simp_to_model [inter, Const.get!, contains] using getValueD_filter_containsKey_of_containsKey_eq_false_right + +theorem get!_inter_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₁.contains k = false) : + Const.get! (m₁.inter m₂) k = default := by + revert h + simp_to_model [inter, Const.get!, contains] using getValueD_filter_containsKey_of_containsKey_eq_false_left end Const diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index e602222273..9d7db379b4 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -167,6 +167,23 @@ theorem foldM_eq_foldlM_toListModel {δ : Type w} {m : Type w → Type w'} [Mona funext init' rw [ih] +theorem fold_induction {δ : Type w} + {f : δ → (a : α) → β a → δ} {init : δ} {b : Raw α β} {P : δ → Prop} + (base : P init) (step : ∀ acc a b , P acc → P (f acc a b)) : + P (b.fold f init) := by + simp [Raw.fold, Raw.foldM, ← Array.foldlM_toList] + induction b.buckets.toList generalizing init with + | nil => simp [base] + | cons hd tl ih => + apply ih + induction hd generalizing init with + | nil => simp [AssocList.foldlM, pure, base] + | cons hda hdb tl ih => + simp only [AssocList.foldlM, pure_bind] + apply ih + apply step + exact base + theorem fold_eq_foldl_toListModel {l : Raw α β} {f : γ → (a : α) → β a → γ} {init : γ} : l.fold f init = (toListModel l.buckets).foldl (fun a b => f a b.1 b.2) init := by simp [Raw.fold, foldM_eq_foldlM_toListModel] @@ -1107,7 +1124,6 @@ theorem insertMany_eq_insertListₘ_toListModel [BEq α] [Hashable α] (m m₂ : simp only [List.foldl_cons, insertListₘ] apply ih - theorem insertManyIfNew_eq_insertListIfNewₘ_toListModel [BEq α] [Hashable α] (m m₂ : Raw₀ α β) : insertManyIfNew m m₂.1 = insertListIfNewₘ m (toListModel m₂.1.buckets) := by simp only [insertManyIfNew, bind_pure_comp, map_pure, bind_pure] @@ -1142,6 +1158,20 @@ theorem toListModel_unionₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashabl · exact toListModel_insertListIfNewₘ ‹_› · exact toListModel_insertListₘ ‹_› +theorem wfImp_inter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (wh₁ : Raw.WFImp m₁) : + Raw.WFImp (Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).val := by + rw [inter] + split + · apply wfImp_filter wh₁ + · rw [interSmaller] + apply @Raw.fold_induction _ β _ (fun sofar k x => interSmallerFn ⟨m₁, h₁⟩ sofar k) emptyWithCapacity m₂ (Raw.WFImp ·.val) wfImp_emptyWithCapacity + intro acc a b wf + rw [interSmallerFn] + split + · apply wfImp_insert wf + · apply wf + end Raw₀ namespace Raw @@ -1163,6 +1193,7 @@ theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashabl | constModify₀ _ h => exact Raw₀.Const.wfImp_modify (by apply h) | alter₀ _ h => exact Raw₀.wfImp_alter (by apply h) | constAlter₀ _ h => exact Raw₀.Const.wfImp_alter (by apply h) + | inter₀ _ _ h _ => exact Raw₀.wfImp_inter (by apply h) end Raw @@ -1312,6 +1343,7 @@ theorem wf_union₀ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] · exact wf_insertManyIfNew₀ ‹_› · exact wf_insertMany₀ ‹_› + theorem toListModel_union [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) : Perm (toListModel (m₁.union m₂).1.buckets) @@ -1319,6 +1351,76 @@ theorem toListModel_union [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable rw [union_eq_unionₘ] exact toListModel_unionₘ h₁ h₂ + +/-! # `inter` -/ + +theorem wfImp_interSmallerFnₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m₁ : Raw₀ α β) (m₂ : Raw₀ α β) + (hm₂ : Raw.WFImp m₂.1) (k : α) : Raw.WFImp (m₁.interSmallerFnₘ m₂ k).1 := by + rw [interSmallerFnₘ] + split + · exact wfImp_insertₘ hm₂ + · exact hm₂ + +/-- Internal implementation detail of the hash map -/ +def interSmallerₘ [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) : Raw₀ α β := + m₂.fold (fun sofar k _ => interSmallerFnₘ m₁ sofar k) emptyWithCapacity + +theorem interSmaller_eq_interSmallerₘ [BEq α] [Hashable α] (m₁ : Raw₀ α β) (m₂ : Raw α β) : + m₁.interSmaller m₂ = m₁.interSmallerₘ m₂ := by + rw [interSmaller, interSmallerₘ] + simp only [interSmallerFn_eq_interSmallerFnₘ] + +theorem foldl_perm_cong [BEq α] {init₁ init₂ : List ((a : α) × β a)} {l : List ((a : α) × β a)} + {f : List ((a : α) × β a) → ((a : α) × β a) → List ((a : α) × β a)} (h₁ : Perm init₁ init₂) + (h₂ : ∀ h l₁ l₂, (w : DistinctKeys l₁) → Perm l₁ l₂ → Perm (f l₁ h) (f l₂ h) ∧ DistinctKeys (f l₁ h)) + (h₃ : DistinctKeys init₁) + : Perm (List.foldl f init₁ l) (List.foldl f init₂ l) := by + induction l generalizing init₁ init₂ + case nil => + simp only [foldl_nil, h₁] + case cons h t ih => + simp only [foldl_cons] + apply ih + · exact (h₂ h init₁ init₂ h₃ h₁).1 + · exact (h₂ h init₁ init₂ h₃ h₁).2 + +theorem toListModel_interSmallerFnₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m sofar : Raw₀ α β) + (l : List ((a : α) × β a)) + (hm : Raw.WFImp m.1) (hs : Raw.WFImp sofar.1) (k : α) (hml : toListModel sofar.1.buckets ~ l) : + Perm (toListModel ((interSmallerFnₘ m sofar k).1.buckets)) + (List.interSmallerFn (toListModel m.1.buckets) l k) := by + rw [interSmallerFnₘ, getEntry?ₘ_eq_getEntry? hm, List.interSmallerFn] + split + · simpa [*] using (toListModel_insertₘ hs).trans (List.insertEntry_of_perm hs.distinct hml) + · simp [*] + +theorem toListModel_interSmallerₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + (m₁ : Raw₀ α β) (m₂ : Raw α β) (hm₁ : Raw.WFImp m₁.1) : + toListModel (m₁.interSmallerₘ m₂).1.buckets ~ + List.interSmaller (toListModel m₁.1.buckets) (toListModel m₂.buckets) := by + rw [interSmallerₘ, Raw.fold_eq_foldl_toListModel, List.interSmaller] + generalize toListModel m₂.buckets = l + suffices ∀ m l', Raw.WFImp m.1 → toListModel m.1.buckets ~ l' → toListModel (foldl (fun a b => m₁.interSmallerFnₘ a b.fst) m l).val.buckets ~ + foldl (fun sofar kv => List.interSmallerFn (toListModel m₁.val.buckets) sofar kv.fst) l' l by + simpa using this emptyWithCapacity [] wfImp_emptyWithCapacity (by simp) + intro m l' hm hml' + induction l generalizing m l' with + | nil => simpa + | cons ht tl ih => + rw [List.foldl_cons, List.foldl_cons] + exact ih _ _ (wfImp_interSmallerFnₘ _ _ hm _) (toListModel_interSmallerFnₘ _ _ _ hm₁ hm _ hml') + +theorem toListModel_inter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (m₁ m₂ : Raw₀ α β) (hm₁ : Raw.WFImp m₁.1) (hm₂ : Raw.WFImp m₂.1) : + Perm (toListModel (m₁.inter m₂).1.buckets) ((toListModel m₁.1.buckets).filter fun p => containsKey p.1 (toListModel m₂.1.buckets) ) := by + simp [inter] + split + · rw [filter_eq_filterₘ] + simp only [contains_eq_containsKey hm₂] + exact toListModel_filterₘ + · rw [interSmaller_eq_interSmallerₘ] + exact Perm.trans (toListModel_interSmallerₘ _ _ hm₁) + (interSmaller_perm_filter _ _ hm₁.distinct) + /-! # `Const.insertListₘ` -/ theorem Const.toListModel_insertListₘ {β : Type v} [BEq α] [Hashable α] [EquivBEq α] diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index cd6f020e20..7e63f8a539 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -2146,6 +2146,324 @@ theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited end Const +section Inter + +variable {m₁ m₂ : DHashMap α β} + +@[simp] +theorem inter_eq : 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) := + @Raw₀.contains_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + @Raw₀.contains_inter_iff _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := by + rw [← contains_eq_false_iff_not_mem] at not_mem ⊢ + exact @Raw₀.contains_inter_eq_false_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := by + 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 + +/- get? -/ +theorem get?_inter [LawfulBEq α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + @Raw₀.get?_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k + +theorem get?_inter_of_mem_right [LawfulBEq α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + @Raw₀.get?_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k mem + +theorem get?_inter_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get?_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k not_mem + +theorem get?_inter_of_not_mem_right [LawfulBEq α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get?_inter_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 + +/- 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 + rw [mem_iff_contains] at h_mem + exact @Raw₀.get_inter _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ m₁.2 m₂.2 k h_mem + +/- getD -/ +theorem getD_inter [LawfulBEq α] {k : α} {fallback : β k} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + @Raw₀.getD_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k fallback + +theorem getD_inter_of_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + @Raw₀.getD_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k fallback mem + +theorem getD_inter_of_not_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getD_inter_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k fallback not_mem + +theorem getD_inter_of_not_mem_left [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getD_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k fallback not_mem + +/- get! -/ +theorem get!_inter [LawfulBEq α] {k : α} [Inhabited (β k)] : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + @Raw₀.get!_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k _ + +theorem get!_inter_of_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + @Raw₀.get!_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k _ mem + +theorem get!_inter_of_not_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get!_inter_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 + +theorem get!_inter_of_not_mem_left [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get!_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k _ not_mem + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := + @Raw₀.getKey?_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := + @Raw₀.getKey?_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k mem + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey?_inter_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 + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey?_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k 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) := by + rw [mem_iff_contains] at h_mem + exact @Raw₀.getKey_inter _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k h_mem + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := + @Raw₀.getKeyD_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + @Raw₀.getKeyD_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback mem + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKeyD_inter_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback not_mem + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKeyD_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback not_mem + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := + @Raw₀.getKey!_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k _ + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := + @Raw₀.getKey!_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k mem + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey!_inter_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 + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey!_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + @Raw₀.size_inter_le_size_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + @Raw₀.size_inter_le_size_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := by + have : ∀ (a : α), m₁.contains a → m₂.contains a := by + intro a ha + rw [contains_iff_mem] at ha ⊢ + exact h a ha + exact @Raw₀.size_inter_eq_size_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 this + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := by + have : ∀ (a : α), m₂.contains a → m₁.contains a := by + intro a ha + rw [contains_iff_mem] at ha ⊢ + exact h a ha + exact @Raw₀.size_inter_eq_size_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 this + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + @Raw₀.size_add_size_eq_size_union_add_size_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @Raw₀.isEmpty_inter_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @Raw₀.isEmpty_inter_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := by + simpa only [mem_iff_contains, Bool.not_eq_true] using + @Raw₀.isEmpty_inter_iff _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.wf m₂.wf + +end Inter + +namespace Const + +variable {β : Type v} {m₁ m₂ : DHashMap α (fun _ => β)} + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + Const.get? (m₁.inter m₂) k = + if k ∈ m₂ then Const.get? m₁ k else none := + @Raw₀.Const.get?_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + Const.get? (m₁.inter m₂) k = Const.get? m₁ k := + @Raw₀.Const.get?_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get? (m₁.inter m₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get?_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get? (m₁.inter m₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get?_inter_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 + +/- 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 + rw [mem_iff_contains] at h_mem + exact @Raw₀.Const.get_inter _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k h_mem + +/- 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 := + @Raw₀.Const.getD_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback + +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 := + @Raw₀.Const.getD_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.getD_inter_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + Const.getD (m₁.inter m₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.getD_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : + Const.get! (m₁.inter m₂) k = + if k ∈ m₂ then Const.get! m₁ k else default := + @Raw₀.Const.get!_inter _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (mem : k ∈ m₂) : + Const.get! (m₁.inter m₂) k = Const.get! m₁ k := + @Raw₀.Const.get!_inter_of_contains_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get! (m₁.inter m₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get!_inter_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 + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get! (m₁.inter m₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get!_inter_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k not_mem + +end Const + namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 1ce3942d1b..fbdc6ea5a5 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -384,17 +384,6 @@ This function ensures that the value is used linearly. else ∅ -/-- -Monadically computes a value by folding the given function over the mappings in the hash -map in some order. --/ -@[inline] def foldM (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ := - b.buckets.foldlM (fun acc l => l.foldlM f acc) init - -/-- Folds the given function over the mappings in the hash map in some order. -/ -@[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := - Id.run (b.foldM (pure <| f · · ·) init) - namespace Internal /-- @@ -516,6 +505,23 @@ This function always merges the smaller map into the larger map, so the expected instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ +/-- +Computes the intersection of the given hash maps. The result will only contain entries from the first map. + +This function always merges the smaller map into the larger map, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def inter [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := + if h₁ : 0 < m₁.buckets.size then + if h₂ : 0 < m₂.buckets.size then + Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩ + else + m₁ + else + m₂ + +instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩ + section Unverified @@ -664,6 +670,8 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable /-- Internal implementation detail of the hash map -/ | constAlter₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : Option β → Option β} : WF m → WF (Raw₀.Const.alter ⟨m, h⟩ a f).1 + /-- Internal implementation detail of the hash map -/ + | inter₀ {α β} [BEq α] [Hashable α] {m₁ m₂ : Raw α β} {h₁ h₂} : WF m₁ → WF m₂ → WF (Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).1 -- TODO: this needs to be deprecated, but there is a bootstrapping issue. -- @[deprecated WF.emptyWithCapacity₀ (since := "2025-03-12")] @@ -686,6 +694,7 @@ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 | constModify₀ _ => (Raw₀.Const.modify _ _ _).2 | alter₀ _ => (Raw₀.alter _ _ _).2 | constAlter₀ _ => (Raw₀.Const.alter _ _ _).2 + | inter₀ _ _ => (Raw₀.inter _ _).2 @[simp] theorem WF.emptyWithCapacity [BEq α] [Hashable α] {c : Nat} : (Raw.emptyWithCapacity c : Raw α β).WF := .emptyWithCapacity₀ @@ -761,6 +770,10 @@ theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) 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 + simp [Std.DHashMap.Raw.inter, h₁.size_buckets_pos, h₂.size_buckets_pos] + exact WF.inter₀ h₁ h₂ + end WF end Raw diff --git a/src/Std/Data/DHashMap/RawDef.lean b/src/Std/Data/DHashMap/RawDef.lean index 74ba4c56d6..f17b03f1c7 100644 --- a/src/Std/Data/DHashMap/RawDef.lean +++ b/src/Std/Data/DHashMap/RawDef.lean @@ -56,6 +56,17 @@ namespace Raw variable {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} +/-- +Monadically computes a value by folding the given function over the mappings in the hash +map in some order. +-/ +@[inline] def foldM [Monad m] (f : δ → (a : α) → β a → m δ) (init : δ) (b : Raw α β) : m δ := + b.buckets.foldlM (fun acc l => l.foldlM f acc) init + +/-- Folds the given function over the mappings in the hash map in some order. -/ +@[inline] def fold (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := + Id.run (b.foldM (pure <| f · · ·) init) + /-- Carries out a monadic action on each mapping in the hash map in some order. -/ @[inline] def forM [Monad m] (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit := b.buckets.forM (AssocList.forM f) diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 342318b057..e24813fcd5 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -48,7 +48,7 @@ private meta def baseNames : Array Name := ``getKey?_eq, ``getKey_eq, ``getKey!_eq, ``getKeyD_eq, ``insertMany_eq, ``Const.insertMany_eq, ``Const.insertManyIfNewUnit_eq, ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq, - ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq] + ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq, ``inter_eq] /-- Internal implementation detail of the hash map -/ scoped syntax "simp_to_raw" ("using" term)? : tactic @@ -2433,6 +2433,444 @@ theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited end Const +section Inter + +variable {m₁ m₂ : Raw α β} + +@[simp] +theorem inter_eq : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ + +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] {k : α} (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := by + simp only [Inter.inter] + simp_to_raw using Raw₀.contains_inter + +/- mem -/ + +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := by + simp only [Inter.inter, Membership.mem] + simp_to_raw using Raw₀.contains_inter_iff + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := by + simp only [Inter.inter] + rw [← contains_eq_false_iff_not_mem] at not_mem |- + revert not_mem + simp_to_raw using Raw₀.contains_inter_eq_false_of_contains_eq_false_left + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := by + simp only [Inter.inter] + rw [← contains_eq_false_iff_not_mem] at not_mem |- + revert not_mem + simp_to_raw using Raw₀.contains_inter_eq_false_of_contains_eq_false_right + +/- get? -/ +theorem get?_inter [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := by + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.get?_inter + +theorem get?_inter_of_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := by + simp only [Membership.mem] at mem + simp only [Inter.inter] + revert mem + simp_to_raw using Raw₀.get?_inter_of_contains_right + +theorem get?_inter_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Inter.inter] + simp_to_raw using Raw₀.get?_inter_of_contains_eq_false_left + +theorem get?_inter_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Inter.inter] + simp_to_raw using Raw₀.get?_inter_of_contains_eq_false_right + +/- get -/ +@[simp] theorem get_inter [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem: k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).get k h_mem = + m₁.get k ((mem_inter_iff h₁ h₂).1 h_mem).1 := by + revert h_mem + simp only [Membership.mem, Inter.inter] + simp_to_raw + intro h_mem + apply Raw₀.get_inter + all_goals wf_trivial + +/- getD -/ +theorem getD_inter [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := by + simp only [Inter.inter, Membership.mem] + simp_to_raw using Raw₀.getD_inter + +theorem getD_inter_of_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := by + revert mem + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.getD_inter_of_contains_right + +theorem getD_inter_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getD_inter_of_contains_eq_false_right + +theorem getD_inter_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getD_inter_of_contains_eq_false_left + +/- get! -/ +theorem get!_inter [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := by + simp only [Inter.inter, Membership.mem] + simp_to_raw using Raw₀.get!_inter + +theorem get!_inter_of_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := by + revert mem + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.get!_inter_of_contains_right + +theorem get!_inter_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.get!_inter_of_contains_eq_false_right + +theorem get!_inter_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.get!_inter_of_contains_eq_false_left + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := by + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.getKey?_inter + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := by + simp only [Membership.mem] at mem + simp only [Inter.inter] + revert mem + simp_to_raw using Raw₀.getKey?_inter_of_contains_right + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKey?_inter_of_contains_eq_false_right + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKey?_inter_of_contains_eq_false_left + +/- getKey -/ +@[simp] theorem getKey_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).getKey k h_mem = + m₁.getKey k ((mem_inter_iff h₁ h₂).1 h_mem).1 := by + revert h_mem + simp only [Membership.mem, Inter.inter] + simp_to_raw + intro h_mem + apply Raw₀.getKey_inter + all_goals wf_trivial + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := by + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.getKeyD_inter + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + simp only [Membership.mem] at mem + simp only [Inter.inter] + revert mem + simp_to_raw using Raw₀.getKeyD_inter_of_contains_right + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKeyD_inter_of_contains_eq_false_right + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKeyD_inter_of_contains_eq_false_left + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := by + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.getKey!_inter + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := by + simp only [Membership.mem] at mem + simp only [Inter.inter] + revert mem + simp_to_raw using Raw₀.getKey!_inter_of_contains_right + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKey!_inter_of_contains_eq_false_right + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.getKey!_inter_of_contains_eq_false_left + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₁.size := by + simp only [Inter.inter] + simp_to_raw using Raw₀.size_inter_le_size_left + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₂.size := by + simp only [Inter.inter] + simp_to_raw using Raw₀.size_inter_le_size_right + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := by + have : ∀ (a : α), m₁.contains a → m₂.contains a := by + intro a ha + rw [contains_iff_mem] at ha ⊢ + exact h a ha + revert this + simp only [Inter.inter] + simp_to_raw using Raw₀.size_inter_eq_size_left + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := by + have : ∀ (a : α), m₂.contains a → m₁.contains a := by + intro a ha + rw [contains_iff_mem] at ha ⊢ + exact h a ha + revert this + simp only [Inter.inter] + simp_to_raw using Raw₀.size_inter_eq_size_right + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := by + simp only [Union.union, Inter.inter] + simp_to_raw using @Raw₀.size_add_size_eq_size_union_add_size_inter _ _ _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := by + revert h + simp only [Inter.inter] + simp_to_raw using @Raw₀.isEmpty_inter_left _ _ _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ _ _ + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := by + revert h + simp only [Inter.inter] + simp_to_raw using @Raw₀.isEmpty_inter_right _ _ _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ _ _ + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := by + conv => + rhs + rhs + rhs + rw [← contains_eq_false_iff_not_mem] + simp only [Inter.inter, Membership.mem] + simp_to_raw using @Raw₀.isEmpty_inter_iff _ _ _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ _ _ + +end Inter + +namespace Const + +variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β)} + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get? (m₁ ∩ m₂) k = + if k ∈ m₂ then Const.get? m₁ k else none := by + simp only [Membership.mem, Inter.inter] + simp_to_raw using Raw₀.Const.get?_inter + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + Const.get? (m₁ ∩ m₂) k = Const.get? m₁ k := by + rw [mem_iff_contains] at mem + revert mem + simp only [Inter.inter] + simp_to_raw using Raw₀.Const.get?_inter_of_contains_right + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get? (m₁ ∩ m₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Inter.inter] + simp_to_raw using Raw₀.Const.get?_inter_of_contains_eq_false_left + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get? (m₁ ∩ m₂) k = none := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Inter.inter] + simp_to_raw using Raw₀.Const.get?_inter_of_contains_eq_false_right + +/- get -/ +@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + Const.get (m₁ ∩ m₂) k h_mem = + Const.get m₁ k ((mem_inter_iff h₁ h₂).1 h_mem).1 := by + revert h_mem + simp only [Membership.mem, Inter.inter] + simp_to_raw + intro h_mem + apply Raw₀.Const.get_inter + all_goals wf_trivial + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} : + Const.getD (m₁ ∩ m₂) k fallback = + if k ∈ m₂ then Const.getD m₁ k fallback else fallback := by + simp only [Inter.inter, Membership.mem] + simp_to_raw using Raw₀.Const.getD_inter + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (mem : k ∈ m₂) : + Const.getD (m₁ ∩ m₂) k fallback = Const.getD m₁ k fallback := by + rw [mem_iff_contains] at mem + revert mem + simp only [Inter.inter] + simp_to_raw using Raw₀.Const.getD_inter_of_contains_right + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + Const.getD (m₁ ∩ m₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.Const.getD_inter_of_contains_eq_false_right + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + Const.getD (m₁ ∩ m₂) k fallback = fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.Const.getD_inter_of_contains_eq_false_left + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + Const.get! (m₁ ∩ m₂) k = + if k ∈ m₂ then Const.get! m₁ k else default := by + simp only [Inter.inter, Membership.mem] + simp_to_raw using Raw₀.Const.get!_inter + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + Const.get! (m₁ ∩ m₂) k = Const.get! m₁ k := by + rw [mem_iff_contains] at mem + revert mem + simp only [Inter.inter] + simp_to_raw using Raw₀.Const.get!_inter_of_contains_right + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get! (m₁ ∩ m₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.Const.get!_inter_of_contains_eq_false_right + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get! (m₁ ∩ m₂) k = default := by + rw [← contains_eq_false_iff_not_mem] at not_mem + simp only [Inter.inter] + revert not_mem + simp_to_raw using Raw₀.Const.get!_inter_of_contains_eq_false_left + +end Const + namespace Const variable {β : Type v} {m : Raw α (fun _ => β)} diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index b784f16422..941caf239a 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -269,6 +269,11 @@ This function always merges the smaller map into the larger map, so the expected instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩ +@[inherit_doc DHashMap.inter, inline] def inter [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β := + ⟨DHashMap.inter m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Inter (HashMap α β) := ⟨inter⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index ac02146d60..d81fcff5f7 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -1557,6 +1557,218 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : end Union +section Inter + +variable {β : Type v} + +variable {m₁ m₂ : HashMap α β} + +@[simp] +theorem inter_eq : 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) := + @DHashMap.contains_inter _ _ _ _ m₁.inner m₂.inner _ _ k + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + @DHashMap.mem_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + @DHashMap.not_mem_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + @DHashMap.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + @DHashMap.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + @DHashMap.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := + @DHashMap.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := + @DHashMap.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k 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) := + @DHashMap.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ k h_mem + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + @DHashMap.Const.getD_inter _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + @DHashMap.Const.getD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := + @DHashMap.Const.getD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := + @DHashMap.Const.getD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + @DHashMap.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + @DHashMap.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := + @DHashMap.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := + @DHashMap.Const.get!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := + @DHashMap.getKey?_inter _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := + @DHashMap.getKey?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := + @DHashMap.getKey?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := + @DHashMap.getKey?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k 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) := + @DHashMap.getKey_inter _ _ _ _ m₁.inner m₂.inner _ _ k h_mem + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := + @DHashMap.getKeyD_inter _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + @DHashMap.getKeyD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback mem + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + @DHashMap.getKeyD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + @DHashMap.getKeyD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := + @DHashMap.getKey!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := + @DHashMap.getKey!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := + @DHashMap.getKey!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := + @DHashMap.getKey!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + @DHashMap.size_inter_le_size_left _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + @DHashMap.size_inter_le_size_right _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + @DHashMap.size_inter_eq_size_left _ _ _ _ m₁.inner m₂.inner _ _ h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + @DHashMap.size_inter_eq_size_right _ _ _ _ m₁.inner m₂.inner _ _ h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + @DHashMap.size_add_size_eq_size_union_add_size_inter _ _ _ _ m₁.inner m₂.inner _ _ + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @DHashMap.isEmpty_inter_left α _ _ _ m₁.inner m₂.inner _ _ h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @DHashMap.isEmpty_inter_right α _ _ _ m₁.inner m₂.inner _ _ h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + @DHashMap.isEmpty_inter_iff α _ _ _ m₁.inner m₂.inner _ _ + +end Inter + -- As `insertManyIfNewUnit` is really an implementation detail for `HashSet.insertMany`, -- we do not add `@[grind]` annotations to any of its lemmas. diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 26f49c8446..2c4ca703d6 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -234,8 +234,13 @@ instance {m : Type w → Type w'} : ForIn m (Raw α β) (α × β) where @[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := ⟨DHashMap.Raw.union m₁.inner m₂.inner⟩ +@[inherit_doc DHashMap.Raw.inter, inline] def inter [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := + ⟨DHashMap.Raw.inter m₁.inner m₂.inner⟩ + instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ +instance [BEq α] [Hashable α] : Inter (Raw α β) := ⟨inter⟩ + section Unverified @[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ) diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 0680e00f53..aff224922a 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1534,6 +1534,231 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : end Union +section Inter + +variable {β : Type v} + +variable {m₁ m₂ : Raw α β} + +@[simp] +theorem inter_eq : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := + @DHashMap.Raw.contains_inter _ _ _ _ m₁.inner m₂.inner _ _ k h₁.out h₂.out + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + @DHashMap.Raw.mem_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + @DHashMap.Raw.not_mem_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + @DHashMap.Raw.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + get? (m₁ ∩ m₂) k = + if k ∈ m₂ then get? m₁ k else none := + @DHashMap.Raw.Const.get?_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + get? (m₁ ∩ m₂) k = get? m₁ k := + @DHashMap.Raw.Const.get?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₁) : + get? (m₁ ∩ m₂) k = none := + @DHashMap.Raw.Const.get?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₂) : + get? (m₁ ∩ m₂) k = none := + @DHashMap.Raw.Const.get?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get -/ +@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + get (m₁ ∩ m₂) k h_mem = + get m₁ k ((mem_inter_iff h₁ h₂).1 h_mem).1 := + @DHashMap.Raw.Const.get_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} : + getD (m₁ ∩ m₂) k fallback = + if k ∈ m₂ then getD m₁ k fallback else fallback := + @DHashMap.Raw.Const.getD_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (mem : k ∈ m₂) : + getD (m₁ ∩ m₂) k fallback = getD m₁ k fallback := + @DHashMap.Raw.Const.getD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : k ∉ m₂) : + getD (m₁ ∩ m₂) k fallback = fallback := + @DHashMap.Raw.Const.getD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : k ∉ m₁) : + getD (m₁ ∩ m₂) k fallback = fallback := + @DHashMap.Raw.Const.getD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + get! (m₁ ∩ m₂) k = + if k ∈ m₂ then get! m₁ k else default := + @DHashMap.Raw.Const.get!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + get! (m₁ ∩ m₂) k = get! m₁ k := + @DHashMap.Raw.Const.get!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₂) : + get! (m₁ ∩ m₂) k = default := + @DHashMap.Raw.Const.get!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₁) : + get! (m₁ ∩ m₂) k = default := + @DHashMap.Raw.Const.get!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- getKey? -/ +theorem getKey?_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).getKey? k = + if k ∈ m₂ then m₁.getKey? k else none := + @DHashMap.Raw.getKey?_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem getKey?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey? k = m₁.getKey? k := + @DHashMap.Raw.getKey?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem getKey?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey? k = none := + @DHashMap.Raw.getKey?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem getKey?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey? k = none := + @DHashMap.Raw.getKey?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- getKey -/ +@[simp] theorem getKey_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).getKey k h_mem = + m₁.getKey k ((mem_inter_iff h₁ h₂).1 h_mem).1 := + @DHashMap.Raw.getKey_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem + +/- getKeyD -/ +theorem getKeyD_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∩ m₂).getKeyD k fallback = + if k ∈ m₂ then m₁.getKeyD k fallback else fallback := + @DHashMap.Raw.getKeyD_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getKeyD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + @DHashMap.Raw.getKeyD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback mem + +theorem getKeyD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + @DHashMap.Raw.getKeyD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getKeyD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKeyD k fallback = fallback := + @DHashMap.Raw.getKeyD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- getKey! -/ +theorem getKey!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).getKey! k = + if k ∈ m₂ then m₁.getKey! k else default := + @DHashMap.Raw.getKey!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem getKey!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getKey! k = m₁.getKey! k := + @DHashMap.Raw.getKey!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem + +theorem getKey!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getKey! k = default := + @DHashMap.Raw.getKey!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem getKey!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getKey! k = default := + @DHashMap.Raw.getKey!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₁.size := + @DHashMap.Raw.size_inter_le_size_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₂.size := + @DHashMap.Raw.size_inter_le_size_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + @DHashMap.Raw.size_inter_eq_size_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + @DHashMap.Raw.size_inter_eq_size_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + @DHashMap.Raw.size_add_size_eq_size_union_add_size_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @DHashMap.Raw.isEmpty_inter_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @DHashMap.Raw.isEmpty_inter_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + @DHashMap.Raw.isEmpty_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +end Inter + theorem getElem?_insertMany_list_of_contains_eq_false [EquivBEq α] [LawfulHashable α] (h : m.WF) {l : List (α × β)} {k : α} (contains_eq_false : (l.map Prod.fst).contains k = false) : diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index dcdeebb264..f59584ac4c 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -248,6 +248,17 @@ This function always merges the smaller set into the larger set, so the expected instance [BEq α] [Hashable α] : Union (HashSet α) := ⟨union⟩ +/-- +Computes the intersection of the given hash sets. The result will only contain entries from the first map. + +This function always iterates through the smaller set, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def inter [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α := + ⟨HashMap.inter m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Inter (HashSet α) := ⟨inter⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index 2e0224782b..3477057f09 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -922,6 +922,146 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : end Union +section Inter + +variable {m₁ m₂ : HashSet α} + +@[simp] +theorem inter_eq : 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) := + @HashMap.contains_inter _ _ _ _ m₁.inner m₂.inner _ _ k + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).contains k ↔ m₁.contains k ∧ m₂.contains k := + @HashMap.mem_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + @HashMap.not_mem_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + @HashMap.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + @HashMap.getKey?_inter _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + @HashMap.getKey?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := + @HashMap.getKey?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := + @HashMap.getKey?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k 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) := + @HashMap.getKey_inter _ _ _ _ m₁.inner m₂.inner _ _ k h_mem + +/- getD -/ +theorem getD_inter [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + @HashMap.getKeyD_inter _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + @HashMap.getKeyD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := + @HashMap.getKeyD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := + @HashMap.getKeyD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + @HashMap.getKey!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem get!_inter_of_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + @HashMap.getKey!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem + +theorem get!_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := + @HashMap.getKey!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +theorem get!_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited α] + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := + @HashMap.getKey!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₁.size := + @HashMap.size_inter_le_size_left _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).size ≤ m₂.size := + @HashMap.size_inter_le_size_right _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + @HashMap.size_inter_eq_size_left _ _ _ _ m₁.inner m₂.inner _ _ h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + @HashMap.size_inter_eq_size_right _ _ _ _ m₁.inner m₂.inner _ _ h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + @HashMap.size_add_size_eq_size_union_add_size_inter _ _ _ _ m₁.inner m₂.inner _ _ + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @HashMap.isEmpty_inter_left α _ _ _ m₁.inner m₂.inner _ _ h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @HashMap.isEmpty_inter_right α _ _ _ m₁.inner m₂.inner _ _ h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + @HashMap.isEmpty_inter_iff α _ _ _ m₁.inner m₂.inner _ _ + +end Inter + section @[simp, grind =] diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index dc87ec9488..49824e3e7f 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -232,14 +232,27 @@ This function always merges the smaller set into the larger set, so the expected instance [BEq α] [Hashable α] : Union (Raw α) := ⟨union⟩ +/-- +Computes the intersection of the given hash sets. The result will only contain entries from the first map. + +This function always merges the smaller set into the larger set, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def inter [BEq α] [Hashable α] (m₁ m₂ : Raw α) : Raw α := + ⟨HashMap.Raw.inter m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Inter (Raw α) := ⟨inter⟩ + +section Unverified + +/-! We currently do not provide lemmas for the functions below. -/ + /-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails. -/ @[inline] def all (m : Raw α) (p : α → Bool) : Bool := m.inner.all (fun x _ => p x) /-- Check if any element satisfies the predicate, short-circuiting if a predicate succeeds. -/ @[inline] def any (m : Raw α) (p : α → Bool) : Bool := m.inner.any (fun x _ => p x) -section Unverified - /-! We currently do not provide lemmas for the functions below. -/ /-- diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 649f84cee3..3015d058b9 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -968,6 +968,167 @@ theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : end Union +section Inter + +variable {m₁ m₂ : Raw α} + +@[simp] +theorem inter_eq : m₁.inter m₂ = m₁ ∩ m₂ := by + simp only [Inter.inter] + +/- contains -/ +@[simp] +theorem contains_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k) := + @HashMap.Raw.contains_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +/- mem -/ +@[simp] +theorem mem_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∩ m₂ ↔ k ∈ m₁ ∧ k ∈ m₂ := + @HashMap.Raw.mem_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem not_mem_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₁) : + k ∉ m₁ ∩ m₂ := + @HashMap.Raw.not_mem_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem not_mem_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₂) : + k ∉ m₁ ∩ m₂ := + @HashMap.Raw.not_mem_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get? -/ +theorem get?_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + (m₁ ∩ m₂).get? k = + if k ∈ m₂ then m₁.get? k else none := + @HashMap.Raw.getKey?_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem get?_inter_of_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).get? k = m₁.get? k := + @HashMap.Raw.getKey?_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem get?_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get? k = none := + @HashMap.Raw.getKey?_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem get?_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get? k = none := + @HashMap.Raw.getKey?_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get -/ +@[simp] theorem get_inter [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {h_mem : k ∈ m₁ ∩ m₂} : + (m₁ ∩ m₂).get k h_mem = + m₁.get k ((mem_inter_iff h₁ h₂).1 h_mem).1 := + @HashMap.Raw.getKey_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k h_mem + +/- getD -/ +theorem getD_inter [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∩ m₂).getD k fallback = + if k ∈ m₂ then m₁.getD k fallback else fallback := + @HashMap.Raw.getKeyD_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getD_inter_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (mem : k ∈ m₂) : + (m₁ ∩ m₂).getD k fallback = m₁.getD k fallback := + @HashMap.Raw.getKeyD_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback mem + +theorem getD_inter_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).getD k fallback = fallback := + @HashMap.Raw.getKeyD_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getD_inter_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).getD k fallback = fallback := + @HashMap.Raw.getKeyD_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- get! -/ +theorem get!_inter [EquivBEq α] [LawfulHashable α] [Inhabited α] + (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∩ m₂).get! k = + if k ∈ m₂ then m₁.get! k else default := + @HashMap.Raw.getKey!_inter _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem get!_inter_of_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (mem : k ∈ m₂) : + (m₁ ∩ m₂).get! k = m₁.get! k := + @HashMap.Raw.getKey!_inter_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k mem + +theorem get!_inter_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₂) : + (m₁ ∩ m₂).get! k = default := + @HashMap.Raw.getKey!_inter_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem get!_inter_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : k ∉ m₁) : + (m₁ ∩ m₂).get! k = default := + @HashMap.Raw.getKey!_inter_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- size -/ +theorem size_inter_le_size_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₁.size := + @HashMap.Raw.size_inter_le_size_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_inter_le_size_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : + (m₁ ∩ m₂).size ≤ m₂.size := + @HashMap.Raw.size_inter_le_size_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_inter_eq_size_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₁ → a ∈ m₂) : + (m₁ ∩ m₂).size = m₁.size := + @HashMap.Raw.size_inter_eq_size_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem size_inter_eq_size_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) + (h : ∀ (a : α), a ∈ m₂ → a ∈ m₁) : + (m₁ ∩ m₂).size = m₂.size := + @HashMap.Raw.size_inter_eq_size_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem size_add_size_eq_size_union_add_size_inter [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + m₁.size + m₂.size = (m₁ ∪ m₂).size + (m₁ ∩ m₂).size := + @HashMap.Raw.size_add_size_eq_size_union_add_size_inter _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +/- isEmpty -/ +@[simp] +theorem isEmpty_inter_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₁.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @HashMap.Raw.isEmpty_inter_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +@[simp] +theorem isEmpty_inter_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) (h : m₂.isEmpty) : + (m₁ ∩ m₂).isEmpty = true := + @HashMap.Raw.isEmpty_inter_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out h + +theorem isEmpty_inter_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∩ m₂).isEmpty ↔ ∀ k, k ∈ m₁ → k ∉ m₂ := + @HashMap.Raw.isEmpty_inter_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +end Inter + @[simp, grind =] theorem ofList_nil : ofList ([] : List α) = ∅ := diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index d2de3e3b1d..1de4b9d3f0 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -3334,7 +3334,7 @@ theorem getKeyD_insertList [BEq α] [EquivBEq α] rw [@getKey?_insertList α β _ _ l toInsert k distinct_l distinct_toInsert] simp only [Option.getD_or] -theorem List.getKeyD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] +theorem getKeyD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (not_contains: containsKey k toInsert = false) : List.getKeyD k (insertList l toInsert) fallback = List.getKeyD k l fallback := by @@ -3345,7 +3345,7 @@ theorem List.getKeyD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α apply getEntry?_insertList_of_contains_eq_false . exact not_contains -theorem List.getKeyD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] +theorem getKeyD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k fallback : α} (distinct_l : DistinctKeys l) (distinct_toInsert : DistinctKeys toInsert) @@ -3428,7 +3428,7 @@ theorem getValueCastD_of_insertList [BEq α] [LawfulBEq α] rw [getOr] simp only [Option.getD_or, getValueCastD_eq_getValueCast?] -theorem List.getValueCast_insertList_of_contains_eq_false_left [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} +theorem getValueCast_insertList_of_contains_eq_false_left [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert)) @@ -3439,7 +3439,7 @@ theorem List.getValueCast_insertList_of_contains_eq_false_left [BEq α] [LawfulB rw [← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast] exact getValueCast?_insertList_of_contains_eq_false_left distinct_l distinct_toInsert not_contains -theorem List.getKey_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} +theorem getKey_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert)) @@ -3450,7 +3450,7 @@ theorem List.getKey_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] simp only [← getKey?_eq_some_getKey] exact getKey?_insertList_of_contains_eq_false_left distinct_l distinct_toInsert not_contains -theorem List.getValueCast_insertList_of_contains_right [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} +theorem getValueCast_insertList_of_contains_right [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (contains : containsKey k toInsert) {h} : @@ -3464,7 +3464,7 @@ theorem List.getValueCast_insertList_of_contains_right [BEq α] [LawfulBEq α] { rw [containsKey_eq_isSome_getEntry?] at contains rw [@Option.or_of_isSome _ (getEntry? k toInsert) (getEntry? k l) contains] -theorem List.getValueCastD_insertList_of_contains_eq_false_left [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} +theorem getValueCastD_insertList_of_contains_eq_false_left [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (not_contains: containsKey k l = false) : @@ -3721,14 +3721,14 @@ theorem getValue?_insertListConst_of_contains_eq_false [BEq α] [PartialEquivBEq rw [containsKey_eq_contains_map_fst] simpa using not_contains -theorem List.getValue?_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] +theorem getValue?_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (not_contains : containsKey k toInsert = false) : getValue? k (insertList l toInsert) = getValue? k l := by rw [getValue?_eq_getEntry?, getValue?_eq_getEntry?] simp only [getEntry?_insertList_of_contains_eq_false not_contains] -theorem List.getValueD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] +theorem getValueD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} (not_contains : containsKey k toInsert = false) : getValueD k (insertList l toInsert) fallback = getValueD k l fallback := by @@ -3736,7 +3736,7 @@ theorem List.getValueD_insertList_of_contains_eq_false_right [BEq α] [EquivBEq congr 1 exact getValue?_insertList_of_contains_eq_false_right not_contains -theorem List.getValue_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] +theorem getValue_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (not_contains : containsKey k toInsert = false) {p1 : containsKey k (insertList l toInsert) = true} @@ -3745,9 +3745,9 @@ theorem List.getValue_insertList_of_contains_eq_false_right [BEq α] [EquivBEq suffices some (getValue k (insertList l toInsert) p1) = some (getValue k l p2) from by injection this simp only [← getValue?_eq_some_getValue] - apply List.getValue?_insertList_of_contains_eq_false_right not_contains + apply getValue?_insertList_of_contains_eq_false_right not_contains -theorem List.getValue?_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} +theorem getValue?_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) : (containsKey k l = false) → getValue? k (insertList l toInsert) = getValue? k toInsert := by @@ -3756,7 +3756,7 @@ theorem List.getValue?_insertList_of_contains_eq_false_left [BEq α] [EquivBEq congr 1 exact getEntry?_insertList_of_contains_left_eq_false distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) not_contains -theorem List.getValueD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} +theorem getValueD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) : (containsKey k l = false) → getValueD k (insertList l toInsert) fallback = getValueD k toInsert fallback := by @@ -3765,7 +3765,7 @@ theorem List.getValueD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq congr 1 exact getValue?_insertList_of_contains_eq_false_left distinct_l distinct_toInsert not_contains -theorem List.getValue?_insertList [BEq α] [EquivBEq α] +theorem getValue?_insertList [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) : @@ -3783,9 +3783,9 @@ theorem getValueD_insertList [BEq α] [EquivBEq α] simp only [getValueD_eq_getValue?] simp only [← Option.getD_or] congr 1 - apply List.getValue?_insertList distinct_l distinct_toInsert + apply getValue?_insertList distinct_l distinct_toInsert -theorem List.getValue_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} +theorem getValue_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (contains : containsKey k (insertList l toInsert)) @@ -3798,7 +3798,7 @@ theorem List.getValue_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α congr 1 exact getEntry?_insertList_of_contains_left_eq_false distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) not_contains -theorem List.getValue_insertList_of_contains_right [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} +theorem getValue_insertList_of_contains_right [BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α} (distinct_l : DistinctKeys l) (distinct_toInsert: DistinctKeys toInsert) (contains : containsKey k toInsert) {h} : @@ -5210,6 +5210,194 @@ theorem getEntry?_filter [BEq α] [EquivBEq α] intro p simp only [Option.all_guard, BEq.rfl, Bool.or_true] +theorem getValueCast?_filter_containsKey [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + getValueCast? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + if containsKey k l₂ = true then getValueCast? k l₁ else none := by + simp only [getValueCast?_eq_getEntry?] + split + case isTrue h => + apply Option.dmap_congr + . simp + . rw [getEntry?_filter] + . simp [Option.filter] + split + case h_1 _ val heq => + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm <| @beq_of_getEntry?_eq_some α β _ l₁ k val heq)] at h + simp [h, heq] + case h_2 _ heq => + simp [heq] + . exact dl₁ + case isFalse h => + suffices (getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁)) = none by simp [this] + rw [getEntry?_filter] + simp [Option.filter] + split + case h_1 _ val heq => + have := PartialEquivBEq.symm <| @beq_of_getEntry?_eq_some α β _ l₁ k val heq + simp at h + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm <| @beq_of_getEntry?_eq_some α β _ l₁ k val heq)] at h + simp [h] + case h_2 => rfl + exact dl₁ + +theorem getKey?_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + getKey? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + if containsKey k l₂ = true then getKey? k l₁ else none := by + simp only [getKey?_eq_getEntry?] + split + case isTrue h => + rw [getEntry?_filter] + · congr 1 + simp [Option.filter] + split + case h_1 _ val heq => + rw [heq] + have key_eq := beq_of_getEntry?_eq_some heq + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm key_eq)] at h + simp [h] + case h_2 _ heq => + simp only [heq] + · exact dl₁ + case isFalse h => + suffices (getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁)) = none by + simp [this] + rw [getEntry?_filter] + · simp [Option.filter] + split + case h_1 _ kv heq => + have key_eq := beq_of_getEntry?_eq_some heq + simp at h + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm key_eq)] at h + simp [h] + case h_2 => rfl + · exact dl₁ + +theorem getKey?_filter_containsKey_of_containsKey_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getKey? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + getKey? k l₁ := by + intro h + rw [getKey?_filter_containsKey, h] + · simp only [↓reduceIte] + · exact dl₁ + +theorem getKey?_filter_containsKey_of_containsKey_eq_false_left [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getKey? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getKey?_filter_containsKey] + · split + · rw [getKey?_eq_none h] + · rfl + · exact dl₁ + +theorem getKey?_filter_containsKey_of_containsKey_eq_false_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getKey? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getKey?_filter_containsKey, h] + · simp only [Bool.false_eq_true, ↓reduceIte] + · exact dl₁ + +theorem getValueCast?_filter_containsKey_of_containsKey_right [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getValueCast? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + getValueCast? k l₁ := by + intro h + rw [getValueCast?_filter_containsKey, h] + . simp only [↓reduceIte] + . exact dl₁ + +theorem getValueCast?_filter_containsKey_of_containsKey_eq_false_left [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getValueCast? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getValueCast?_filter_containsKey] + . split + . rw [getValueCast?_eq_none h] + . rfl + . exact dl₁ + +theorem getValueCast?_filter_containsKey_of_containsKey_eq_false_right [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getValueCast? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getValueCast?_filter_containsKey, h] + . simp only [Bool.false_eq_true, ↓reduceIte] + . exact dl₁ + +theorem getEntry?_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + if containsKey k l₂ = true then getEntry? k l₁ else none := by + split + case isTrue h => + rw [getEntry?_filter] + · simp [Option.filter] + split + case h_1 _ val heq => + have key_eq := beq_of_getEntry?_eq_some heq + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm key_eq)] at h + simp [h, heq] + case h_2 _ heq => + simp [heq] + · exact dl₁ + case isFalse h => + suffices (getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁)) = none by + simp [this] + rw [getEntry?_filter] + · simp [Option.filter] + split + case h_1 _ val heq => + have key_eq := beq_of_getEntry?_eq_some heq + simp at h + rw [@containsKey_congr _ _ _ _ l₂ _ _ (PartialEquivBEq.symm key_eq)] at h + simp [h] + case h_2 => rfl + · exact dl₁ + +theorem getEntry?_filter_containsKey_of_containsKey_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + getEntry? k l₁ := by + intro h + rw [getEntry?_filter_containsKey, h] + · simp only [↓reduceIte] + · exact dl₁ + +theorem getEntry?_filter_containsKey_of_containsKey_eq_false_left [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getEntry?_filter_containsKey] + · split + · apply (@getEntry?_eq_none _ _ _ l₁ k).2 + exact h + · rfl + · exact dl₁ + +theorem getEntry?_filter_containsKey_of_containsKey_eq_false_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getEntry? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [getEntry?_filter_containsKey, h] + · simp only [Bool.false_eq_true, ↓reduceIte] + · exact dl₁ + theorem getEntry?_filterMap [BEq α] [EquivBEq α] {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : @@ -5228,6 +5416,285 @@ theorem getEntry?_map [BEq α] [EquivBEq α] intro p exact BEq.rfl +theorem containsKey_filter_containsKey [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} : + (containsKey k (List.filter (fun p => containsKey p.fst (l₂)) l₁)) = + (containsKey k l₁ && containsKey k l₂) := by + rw [containsKey_eq_isSome_getEntry?, containsKey_eq_isSome_getEntry?] + rw [getEntry?_filter] + generalize heq : (getEntry? k l₁) = x + cases x + case none => + simp + case some kv => + simp only [Option.isSome_filter, Option.any_some, Option.isSome_some, Bool.true_and] + rw [containsKey_congr] + apply List.beq_of_getEntry?_eq_some heq + . exact hl₁ + +theorem containsKey_filter_containsKey_iff [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} : + (containsKey k (List.filter (fun p => containsKey p.fst l₂) l₁)) ↔ + (containsKey k l₁ ∧ containsKey k l₂) := by + rw [containsKey_filter_containsKey] + . simp + . exact hl₁ + +theorem getValueCast_filter_containsKey [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) {h₁ h₂} : + getValueCast k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁ = getValueCast k l₁ h₂ := by + suffices some (getValueCast k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁) = some (getValueCast k l₁ h₂) by injections + simp only [← getValueCast?_eq_some_getValueCast] + apply getValueCast?_filter_containsKey_of_containsKey_right dl₁ + . rw [containsKey_filter_containsKey_iff] at h₁ + . exact h₁.2 + . exact dl₁ + +theorem getEntry_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) {h₁ h₂} : + getEntry k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁ = getEntry k l₁ h₂ := by + suffices some (getEntry k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁) = some (getEntry k l₁ h₂) by + injections + simp only [← getEntry?_eq_some_getEntry] + apply getEntry?_filter_containsKey_of_containsKey_right dl₁ + · rw [containsKey_filter_containsKey_iff] at h₁ + · exact h₁.2 + · exact dl₁ + +theorem getKey_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} + (dl₁ : DistinctKeys l₁) {h₁ h₂} : + getKey k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁ = getKey k l₁ h₂ := by + suffices some (getKey k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁) = some (getKey k l₁ h₂) by + injections + simp only [← getKey?_eq_some_getKey] + apply getKey?_filter_containsKey_of_containsKey_right dl₁ + · rw [containsKey_filter_containsKey_iff] at h₁ + · exact h₁.2 + · exact dl₁ + +theorem containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} : + containsKey k l₁ = false → containsKey k (List.filter (fun p => containsKey p.fst l₂) l₁) = false := by + intro h + rw [containsKey_filter_containsKey] + . simp [h] + . exact hl₁ + +theorem containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} {hl₁ : DistinctKeys l₁} {k : α} : + containsKey k l₂ = false → containsKey k (List.filter (fun p => containsKey p.fst l₂) l₁) = false := by + intro h + rw [containsKey_filter_containsKey] + . simp [h] + . exact hl₁ + +theorem List.getValue?_filter_containsKey {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} + (dl₁ : DistinctKeys l₁) : + getValue? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + if containsKey k l₂ = true then getValue? k l₁ else none := by + simp only [getValue?_eq_getEntry?] + split + case isTrue h => + congr 1 + rw [getEntry?_filter] + . simp only [Option.filter] + split + case h_1 _ val heq => + simp [heq] + have := PartialEquivBEq.symm <| @beq_of_getEntry?_eq_some α (fun _ => β) _ l₁ k val heq + rw [← containsKey_congr this] + exact h + case h_2 _ heq => + simp [heq] + . exact dl₁ + case isFalse h => + simp only [Option.map_eq_none_iff, getEntry?_eq_none] + simp only [Bool.not_eq_true] at h + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + . exact dl₁ + . exact h + +theorem List.getValue?_filter_containsKey_of_containsKey_right {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getValue? k (List.filter (fun p => containsKey p.fst l₂) l₁) = + getValue? k l₁ := by + intro h + rw [List.getValue?_filter_containsKey, h] + · simp only [↓reduceIte] + · exact dl₁ + +theorem List.getValue?_filter_containsKey_of_containsKey_eq_false_left {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getValue? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [List.getValue?_filter_containsKey] + · split + · rw [@getValue?_eq_none α β _ l₁ k] + exact h + · rfl + · exact dl₁ + +theorem getValue?_filter_containsKey_of_containsKey_eq_false_right {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getValue? k (List.filter (fun p => containsKey p.fst l₂) l₁) = none := by + intro h + rw [List.getValue?_filter_containsKey, h] + · simp only [Bool.false_eq_true, ↓reduceIte] + · exact dl₁ + +theorem getValueCastD_filter_containsKey [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : β k} + (dl₁ : DistinctKeys l₁) : + getValueCastD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + if containsKey k l₂ = true then getValueCastD k l₁ fallback else fallback := by + split + case isTrue h => + rw [getValueCastD_eq_getValueCast?, getValueCastD_eq_getValueCast?] + congr 1 + apply getValueCast?_filter_containsKey_of_containsKey_right dl₁ h + case isFalse h => + apply getValueCastD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + . exact dl₁ + . simp only [h] + +theorem getValueCastD_filter_containsKey_of_containsKey_right [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback: β k} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getValueCastD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + getValueCastD k l₁ fallback:= by + intro h + rw [getValueCastD_eq_getValueCast?, getValueCastD_eq_getValueCast?] + congr 1 + apply getValueCast?_filter_containsKey_of_containsKey_right dl₁ h + +theorem getValueCastD_filter_containsKey_of_containsKey_eq_false_left [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getValueCastD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getValueCastD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left + . exact dl₁ + . exact h + +theorem getValueCastD_filter_containsKey_of_containsKey_eq_false_right [BEq α] [LawfulBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getValueCastD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getValueCastD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + . exact dl₁ + . exact h + +theorem getKeyD_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : α} + (dl₁ : DistinctKeys l₁) : + getKeyD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + if containsKey k l₂ = true then getKeyD k l₁ fallback else fallback := by + split + case isTrue h => + rw [getKeyD_eq_getKey?, getKeyD_eq_getKey?] + congr 1 + apply getKey?_filter_containsKey_of_containsKey_right dl₁ h + case isFalse h => + apply getKeyD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + · exact dl₁ + · simp only [h] + +theorem getKeyD_filter_containsKey_of_containsKey_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getKeyD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + getKeyD k l₁ fallback := by + intro h + rw [getKeyD_eq_getKey?, getKeyD_eq_getKey?] + congr 1 + apply getKey?_filter_containsKey_of_containsKey_right dl₁ h + +theorem getKeyD_filter_containsKey_of_containsKey_eq_false_left [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getKeyD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getKeyD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left + · exact dl₁ + · exact h + +theorem getKeyD_filter_containsKey_of_containsKey_eq_false_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} {k : α} {fallback : α} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getKeyD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getKeyD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + · exact dl₁ + · exact h + +theorem List.getValue_filter_containsKey {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} + (dl₁ : DistinctKeys l₁) {h₁ h₂} : + getValue k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁ = getValue k l₁ h₂ := by + suffices some (getValue k (List.filter (fun p => containsKey p.fst l₂) l₁) h₁) = some (getValue k l₁ h₂) by + injections + simp only [← getValue?_eq_some_getValue] + apply List.getValue?_filter_containsKey_of_containsKey_right dl₁ + · rw [containsKey_filter_containsKey_iff] at h₁ + · exact h₁.2 + · exact dl₁ + +theorem List.getValueD_filter_containsKey {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} + (dl₁ : DistinctKeys l₁) : + getValueD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + if containsKey k l₂ = true then getValueD k l₁ fallback else fallback := by + split + case isTrue h => + rw [getValueD_eq_getValue?, getValueD_eq_getValue?] + congr 1 + apply List.getValue?_filter_containsKey_of_containsKey_right dl₁ h + case isFalse h => + apply getValueD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + · exact dl₁ + · simp only [h] + +theorem List.getValueD_filter_containsKey_of_containsKey_right {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ → getValueD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = + getValueD k l₁ fallback := by + intro h + rw [getValueD_eq_getValue?, getValueD_eq_getValue?] + congr 1 + apply List.getValue?_filter_containsKey_of_containsKey_right dl₁ h + +theorem getValueD_filter_containsKey_of_containsKey_eq_false_left {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} + (dl₁ : DistinctKeys l₁) : + containsKey k l₁ = false → getValueD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getValueD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_left + · exact dl₁ + · exact h + +theorem getValueD_filter_containsKey_of_containsKey_eq_false_right {β : Type v} [BEq α] [EquivBEq α] + {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β} + (dl₁ : DistinctKeys l₁) : + containsKey k l₂ = false → getValueD k (List.filter (fun p => containsKey p.fst l₂) l₁) fallback = fallback := by + intro h + apply getValueD_eq_fallback + apply containsKey_filter_containsKey_eq_false_of_containsKey_eq_false_right + · exact dl₁ + · exact h + theorem containsKey_of_containsKey_filterMap' [BEq α] [EquivBEq α] {f : ((a : α) × β a) → Option ((a : α) × γ a)} (hf : ∀ p, (f p).all (·.1 == p.1)) @@ -5735,6 +6202,344 @@ theorem length_filter_key_eq_length_iff [BEq α] [EquivBEq α] {f : α → Bool} simp only [getKey, getKey?_eq_getEntry?, this] at h exact h +theorem length_filter_containsKey_eq_length_left [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) + (w : ∀ (a : α), containsKey a l₁ → containsKey a l₂) : + (l₁.filter fun p => containsKey p.fst l₂).length = l₁.length := by + rw [← List.countP_eq_length_filter] + induction l₁ + case nil => simp + case cons h t ih => + simp + rw [List.countP_cons_of_pos] + . rw [List.distinctKeys_cons_iff] at hl₁ + specialize ih hl₁.1 + simp only [Nat.add_right_cancel_iff] + apply ih + intro a hc + apply w + rw [containsKey_cons] + simp [hc] + . apply w + rw [containsKey_cons, BEq.rfl, Bool.true_or] + +theorem length_filter_containsKey_of_length_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) + (w : ∀ (a : α), containsKey a l₂ → containsKey a l₁) : + (l₁.filter fun p => containsKey p.fst l₂).length = l₂.length := by + rw [← List.countP_eq_length_filter] + induction l₁ generalizing l₂ + case nil => + simp only [List.countP_nil] + by_cases heq : l₂ = [] + case pos => + simp only [heq, List.length_nil] + case neg => + have ⟨⟨ek, ev⟩, emem⟩ := @List.exists_mem_of_ne_nil _ l₂ (by simp [heq]) + specialize w ek + rw [List.containsKey_eq_true_iff_exists_mem] at w + specialize w ?_ + . refine ⟨⟨ek,ev⟩, emem, ?_⟩ + simp only [BEq.rfl] + . simp at w + case cons h t ih => + by_cases heq : containsKey h.fst l₂ + case pos => + have len_eq : l₂.length = (eraseKey h.fst l₂).length + 1 := by + induction l₂ + case nil => simp at heq + case cons h' t' ih' => + simp only [List.length_cons, eraseKey, Nat.add_right_cancel_iff] + by_cases heq2 : h'.fst == h.fst + case pos => + simp [heq2] + case neg => + simp only [Bool.not_eq_true] at heq2 + simp only [heq2, cond_false, List.length_cons] + apply ih' + . rw [List.distinctKeys_cons_iff] at hl₂ + exact hl₂.1 + . intro a mem + specialize w a + apply w + rw [containsKey_cons] + simp only [mem, Bool.or_true] + . rw [containsKey_cons] at heq + simp only [heq2, Bool.false_or] at heq + exact heq + rw [len_eq] + rw [List.countP_cons] + simp only [heq, ↓reduceIte, Nat.add_right_cancel_iff] + suffices List.countP (fun p => containsKey p.fst l₂) t = List.countP (fun p => containsKey p.fst (eraseKey h.fst l₂)) t by + rw [this] + apply ih + . rw [List.distinctKeys_cons_iff] at hl₁ + exact hl₁.1 + . apply DistinctKeys.eraseKey hl₂ + . intro a + rw [containsKey_eraseKey] + simp + intro neq contains + specialize w a contains + rw [containsKey_cons] at w + . simp only [neq, Bool.false_or] at w + exact w + . exact hl₂ + clear ih w + induction t + case nil => simp + case cons h' t' ih' => + simp only [List.countP_cons] + split + case isTrue heq2 => + rw [containsKey_eraseKey] + . simp only [heq2, Bool.and_true, Bool.not_eq_eq_eq_not, Bool.not_true] + suffices (h.fst == h'.fst) = false by + simp [this] + apply ih' + . rw [List.distinctKeys_cons_iff, List.distinctKeys_cons_iff, containsKey_cons] at hl₁ + simp only [Bool.or_eq_false_iff] at hl₁ + apply DistinctKeys.cons + all_goals simp only [hl₁] + . rw [List.distinctKeys_cons_iff, containsKey_cons] at hl₁ + apply BEq.symm_false + simp only [Bool.or_eq_false_iff] at hl₁ + exact hl₁.2.1 + . exact hl₂ + case isFalse heq2 => + simp only [Bool.not_eq_true] at heq2 + rw [containsKey_eraseKey] + simp only [Nat.add_zero, heq2, Bool.and_false, Bool.false_eq_true, ↓reduceIte] + apply ih' + . rw [List.distinctKeys_cons_iff, List.distinctKeys_cons_iff, containsKey_cons] at hl₁ + simp only [Bool.or_eq_false_iff] at hl₁ + apply DistinctKeys.cons + all_goals simp only [hl₁] + . exact hl₂ + case neg => + simp only [Bool.not_eq_true] at heq + simp only [heq, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg] + apply ih + . rw [List.distinctKeys_cons_iff] at hl₁ + exact hl₁.1 + . exact hl₂ + . intro a mem + specialize w a mem + rw [containsKey_cons] at w + simp at w + rcases w with inl | inr + case w.inl => + rw [containsKey_congr inl] at heq + rw [mem] at heq + contradiction + case w.inr => + exact inr + +theorem size_add_size_eq_size_insertList_add_size_filter_containsKey [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} (hl₁ : DistinctKeys l₁) (hl₂ : DistinctKeys l₂) : + l₁.length + l₂.length = + (insertList l₁ l₂).length + + (List.filter (fun p => containsKey p.fst l₂) l₁).length := by + rw [← Perm.length_eq (insertListIfNew_perm_insertList hl₂ hl₁)] + induction l₁ generalizing l₂ + case nil => simp [insertListIfNew] + case cons h t ih => + simp [insertListIfNew, List.filter_cons] + split + case isTrue hyp => + simp only [insertEntryIfNew, hyp, cond_true, List.length_cons] + specialize ih (by rw [List.distinctKeys_cons_iff] at hl₁; exact hl₁.1) hl₂ + omega + case isFalse hyp => + rw [Bool.not_eq_true] at hyp + simp [insertEntryIfNew, hyp] + specialize @ih (⟨h.fst, h.snd⟩ :: l₂) (by rw [List.distinctKeys_cons_iff] at hl₁; exact hl₁.1) + rw [List.distinctKeys_cons_iff] at ih + specialize ih ⟨hl₂, hyp⟩ + simp at ih + suffices (List.filter (fun p => h.fst == p.fst || containsKey p.fst l₂) t).length = (List.filter (fun p => containsKey p.fst l₂) t).length by omega + clear ih hl₂ + induction t + case nil => simp + case cons h' t' ih' => + simp [List.filter_cons, Bool.or_eq_true] + by_cases hyp2 : containsKey h'.fst l₂ + case pos => + simp [hyp2] + apply ih' + rw [List.distinctKeys_cons_iff] + rw [List.distinctKeys_cons_iff, List.distinctKeys_cons_iff, List.containsKey_cons] at hl₁ + simp only [Bool.or_eq_false_iff] at hl₁ + exact ⟨hl₁.1.1, hl₁.2.2⟩ + case neg => + simp [hyp2] + simp at hyp2 + rw [List.distinctKeys_cons_iff, containsKey_cons] at hl₁ + simp at hl₁ + simp [BEq.symm_false hl₁.2.1] + apply ih' + rw [List.distinctKeys_cons_iff] at hl₁ |- + exact ⟨hl₁.1.1, hl₁.2.2⟩ + +theorem length_filter_containsKey_le [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} + (dl₁ : DistinctKeys l₂) + (dl₂ : DistinctKeys l₁) : + (l₁.filter fun p => containsKey p.fst l₂).length ≤ l₂.length := by + induction l₁ generalizing l₂ + case nil => simp + case cons h t ih => + by_cases heq : containsKey h.fst l₂ + case pos => + simp [← List.countP_eq_length_filter] + simp only [heq, List.countP_cons_of_pos] + have len_eq : l₂.length = (eraseKey h.fst l₂).length + 1 := by + induction l₂ + case nil => + simp at heq + case cons h' t' ih' => + simp only [List.length_cons, eraseKey, Nat.add_right_cancel_iff] + by_cases heq2 : h'.fst == h.fst + case pos => + simp [heq2] + case neg => + simp only [Bool.not_eq_true] at heq2 + simp only [heq2, cond_false, List.length_cons] + apply ih' + . rw [List.distinctKeys_cons_iff] at dl₁ + exact dl₁.1 + . rw [containsKey_cons] at heq + simp only [heq2, Bool.false_or] at heq + exact heq + rw [len_eq] + simp only [Nat.add_le_add_iff_right, ge_iff_le] + specialize @ih (eraseKey h.fst l₂) ?refine1 ?refine2 + case refine1 => + apply DistinctKeys.eraseKey dl₁ + case refine2 => + rw [List.distinctKeys_cons_iff] at dl₂ + exact dl₂.1 + rw [← List.countP_eq_length_filter] at ih + apply Nat.le_trans ?refine3 ih + case refine3 => + clear ih len_eq + induction t + case nil => simp + case cons h' t' ih' => + by_cases heq2 : h.fst == h'.fst + case pos => + rw [List.distinctKeys_cons_iff] at dl₂ + replace dl₂ := dl₂.2 + rw [containsKey_cons] at dl₂ + simp only [Bool.or_eq_false_iff] at dl₂ + replace dl₂ := dl₂.1 + rw [PartialEquivBEq.symm] at dl₂ + . contradiction + . exact heq2 + case neg => + simp only [Bool.not_eq_true] at heq2 + simp only [List.countP_cons] + split + case isTrue contains => + rw [containsKey_eraseKey] + simp only [heq2, Bool.not_false, contains, Bool.and_self, ↓reduceIte, + Nat.add_le_add_iff_right] + apply ih' + . rw [List.distinctKeys_cons_iff, List.distinctKeys_cons_iff, containsKey_cons] at dl₂ + simp only [Bool.or_eq_false_iff] at dl₂ + apply DistinctKeys.cons + all_goals simp only [dl₂] + . exact dl₁ + case isFalse contains => + rw [containsKey_eraseKey] + simp only [Nat.add_zero, heq2, Bool.not_false, contains, Bool.and_false, + Bool.false_eq_true, ↓reduceIte] + apply ih' + . rw [List.distinctKeys_cons_iff, List.distinctKeys_cons_iff, containsKey_cons] at dl₂ + simp only [Bool.or_eq_false_iff] at dl₂ + apply DistinctKeys.cons + all_goals simp only [dl₂] + . exact dl₁ + case neg => + simp only [List.filter_cons, heq, Bool.false_eq_true, ↓reduceIte] + apply ih dl₁ + rw [List.distinctKeys_cons_iff] at dl₂ + exact dl₂.1 + +theorem isEmpty_filter_containsKey_iff [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} (dl₁ : DistinctKeys l₁) : + (List.filter (fun p => containsKey p.fst l₂) l₁).isEmpty = true ↔ + ∀ (k : α), containsKey k l₁ = true → containsKey k l₂ = false := by + constructor + case mpr => + intro hyp + rw [List.isEmpty_iff] + simp only [List.filter_eq_nil_iff, Bool.not_eq_true] + intro ⟨k,v⟩ mem + apply hyp + apply List.containsKey_of_mem mem + case mp => + intro hyp k mem + rw [List.isEmpty_iff] at hyp + induction l₁ with + | nil => simp at mem + | cons h t ih => + rw [containsKey_cons] at mem + simp only [Bool.or_eq_true] at mem + rw [List.filter_cons] at hyp + split at hyp + case cons.isTrue _ => + simp at hyp + case cons.isFalse heq => + simp only [Bool.not_eq_true] at heq + cases mem + case inl heq2 => + rw [containsKey_congr (PartialEquivBEq.symm heq2)] + exact heq + case inr heq2 => + apply ih + . rw [List.distinctKeys_cons_iff] at dl₁ + exact dl₁.1 + . exact hyp + . exact heq2 + +theorem nil_of_containsKey_eq_false [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} : + (∀ k, containsKey k l = false) ↔ l = [] := by + constructor + case mp => + intro hyp + rw [List.eq_nil_iff_forall_not_mem] + intro a + specialize hyp a.fst + rw [List.containsKey_eq_false_iff_forall_mem_keys] at hyp + specialize hyp a.fst + have : (a.fst == a.fst) → a.fst ∉keys l := by + intro h₁ h₂ + specialize hyp h₂ + rw [hyp] at h₁ + contradiction + specialize this (by simp) + intro h + have := Internal.List.fst_mem_keys_of_mem h + contradiction + case mpr => + intro hyp k + simp [hyp] + +theorem isEmpty_filter_containsKey_left [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} : + l₁.isEmpty → (List.filter (fun p => containsKey p.fst l₂) l₁).isEmpty := by + intro hyp + simp at hyp + simp [hyp] + +theorem isEmpty_filter_containsKey_right [BEq α] [EquivBEq α] + {l₁ l₂ : List ((a : α) × β a)} : + l₂.isEmpty → (List.filter (fun p => containsKey p.fst l₂) l₁).isEmpty := by + intro hyp + simp at hyp + simp [hyp] + theorem perm_filter_self_iff {f : α → Bool} {l : List α} : (l.filter f).Perm l ↔ ∀ a ∈ l, f a = true := by rw (occs := [1]) [← (List.filter_append_perm f _).congr_right, @@ -8250,4 +9055,99 @@ end Const end Max +section InterSmaller + +/-- Internal implementation detail of the hash map -/ +def interSmallerFn [BEq α] (l sofar : List ((a : α) × β a)) (k : α) : List ((a : α) × β a) := + match List.getEntry? k l with + | some kv' => List.insertEntry kv'.1 kv'.2 sofar + | none => sofar + +theorem distinctKeys_interSmallerFn [BEq α] [PartialEquivBEq α] + (l sofar : List ((a : α) × β a)) (k : α) (hs : DistinctKeys sofar) : + DistinctKeys (List.interSmallerFn l sofar k) := by + rw [List.interSmallerFn] + split + · exact hs.insertEntry + · exact hs + +theorem getEntry?_interSmallerFn [BEq α] [PartialEquivBEq α] (l sofar : List ((a : α) × β a)) (k k' : α) : + List.getEntry? k' (List.interSmallerFn l sofar k) = + ((List.getEntry? k' l).filter (fun kv => k == kv.1)).or (List.getEntry? k' sofar) := by + rw [List.interSmallerFn] + split + · rename_i kv hkv + rw [getEntry?_insertEntry] + split <;> rename_i hk + · have hk' : k == k' := (BEq.trans (BEq.symm (List.beq_of_getEntry?_eq_some hkv)) hk) + simp [← List.getEntry?_congr hk', hkv, Option.filter_some, BEq.trans hk' (BEq.symm hk)] + · rw [Option.or_eq_right_of_none] + apply Option.filter_eq_none_iff.2 + intro p hp + have hp' := List.beq_of_getEntry?_eq_some hp + have hkv' := List.beq_of_getEntry?_eq_some hkv + exact fun h => hk (BEq.trans hkv' (BEq.trans h hp')) + · rename_i hk + rw [Option.or_eq_right_of_none] + apply Option.filter_eq_none_iff.2 + intro p hp + have := List.beq_of_getEntry?_eq_some hp + intro hkp + have := BEq.trans hkp this + simp [List.getEntry?_congr this, hp] at hk + +/-- Internal implementation detail of the hash map -/ +def interSmaller [BEq α] (l₁ l₂ : List ((a : α) × β a)) : List ((a : α) × β a) := + l₂.foldl (fun sofar kv => List.interSmallerFn l₁ sofar kv.1) [] + +@[simp] +theorem Option.filter_false {o : Option α} : o.filter (fun _ => false) = none := by + cases o <;> simp + +theorem Option.filter_or {o : Option α} {p q : α → Bool} : o.filter (fun a => p a || q a) = + (o.filter p).or (o.filter q) := by + cases o with + | none => simp + | some a => + simp [Option.filter_some] + cases p a <;> cases q a <;> simp + + +theorem getEntry?_interSmaller [BEq α] [PartialEquivBEq α] (l₁ l₂ : List ((a : α) × β a)) (k : α) : + List.getEntry? k (interSmaller l₁ l₂) = (List.getEntry? k l₁).filter (fun kv => containsKey kv.1 l₂) := by + rw [interSmaller] + suffices ∀ l₃, + List.getEntry? k (List.foldl (fun sofar kv => List.interSmallerFn l₁ sofar kv.fst) l₃ l₂) = + (Option.filter (fun kv => containsKey kv.fst l₂) (List.getEntry? k l₁)).or (List.getEntry? k l₃) by + simpa using this [] + intro l₃ + induction l₂ using assoc_induction generalizing l₃ with + | nil => simp + | cons k v tl ih => + rw [List.foldl_cons, ih] + simp only [List.containsKey_cons, Bool.or_comm (k == _), Option.filter_or, Option.or_assoc, + List.getEntry?_interSmallerFn] + +theorem distinctKeys_interSmaller [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} : + DistinctKeys (interSmaller l₁ l₂) := by + rw [interSmaller] + suffices ∀ l, DistinctKeys l → DistinctKeys (l₂.foldl (fun sofar kv => List.interSmallerFn l₁ sofar kv.1) l) by + simpa using this [] (by simp) + intro l hl + induction l₂ generalizing l with + | nil => simpa + | cons ht tl ih => + rw [List.foldl_cons] + apply ih + exact distinctKeys_interSmallerFn _ _ _ hl + +theorem interSmaller_perm_filter [BEq α] [EquivBEq α] (l₁ l₂ : List ((a : α) × β a)) (h₁ : DistinctKeys l₁) : + List.Perm (List.interSmaller l₁ l₂) (l₁.filter (fun kv => containsKey kv.1 l₂)) := by + apply List.getEntry?_ext + · exact distinctKeys_interSmaller + · exact h₁.filter (f := fun k v => containsKey k l₂) + · intro k' + rw [List.getEntry?_filter h₁, List.getEntry?_interSmaller] + +end InterSmaller end Std.Internal.List