diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index d1777ece5e..20b869b2d6 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -311,6 +311,19 @@ This function ensures that the value is used linearly. Array α := m.1.keysArray +/-- +Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +the second argument will appear in the result. + +This function always merges the smaller map into the larger map, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β where + 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 + +instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ @@ -332,12 +345,6 @@ section Unverified (m : DHashMap α (fun _ => β)) : Array β := m.1.valuesArray -/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : DHashMap α β) : DHashMap α β := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (DHashMap α β) := ⟨union⟩ - @[inline, inherit_doc Raw.Const.unitOfArray] def Const.unitOfArray [BEq α] [Hashable α] (l : Array α) : DHashMap α (fun _ => Unit) := Const.insertManyIfNewUnit ∅ l diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index 721c94ba58..a123996e65 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -426,6 +426,20 @@ def insertMany {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [BEq α] [Hashable r := ⟨r.1.insert a b, fun _ h hm => h (r.2 _ h hm)⟩ return r +/-- Internal implementation detail of the hash map -/ +@[inline] def insertManyIfNew {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] [BEq α] [Hashable α] + (m : Raw₀ α β) (l : ρ) : { m' : Raw₀ α β // ∀ (P : Raw₀ α β → Prop), + (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m' } := Id.run do + let mut r : { m' : Raw₀ α β // ∀ (P : Raw₀ α β → Prop), + (∀ {m'' a b}, P m'' → P (m''.insertIfNew a b)) → P m → P m' } := ⟨m, fun _ _ => id⟩ + for ⟨a, b⟩ in l do + 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 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 + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 3a6e1bd59d..8551d3d6a2 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -396,6 +396,19 @@ def insertListₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l : List ((a : α) | .nil => m | .cons hd tl => insertListₘ (m.insert hd.1 hd.2) tl +/-- Internal implementation detail of the hash map -/ +def insertListIfNewₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l : List ((a : α) × β a)) : Raw₀ α β := + match l with + | .nil => m + | .cons hd tl => insertListIfNewₘ (m.insertIfNew hd.1 hd.2) tl + +/-- Internal implementation detail of the hash map -/ +def unionₘ [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : Raw₀ α β := + if m₁.1.size ≤ m₂.1.size then + insertListIfNewₘ m₂ (toListModel m₁.1.buckets) + else + insertListₘ m₁ (toListModel m₂.1.buckets) + section variable {β : Type v} @@ -614,6 +627,20 @@ theorem insertMany_eq_insertListₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l simp only [List.foldl_cons, insertListₘ] apply ih +theorem insertManyIfNew_eq_insertListIfNewₘ [BEq α] [Hashable α] (m : Raw₀ α β) (l : List ((a : α) × β a)) : + insertManyIfNew m l = insertListIfNewₘ m l := by + simp only [insertManyIfNew, Id.run_pure, pure_bind, List.forIn_pure_yield_eq_foldl] + suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop), + (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insertIfNew a b)) → P m → P m' }), + (List.foldl (fun m' p => ⟨m'.val.insertIfNew p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = + t.val.insertListIfNewₘ l from this _ + intro t + induction l generalizing m with + | nil => simp [insertListIfNewₘ] + | cons hd tl ih => + simp only [List.foldl_cons, insertListIfNewₘ] + apply ih + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index 10ed682a1a..d7f2ee1a5c 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -141,6 +141,10 @@ theorem modify_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.W m.modify k f = Raw₀.modify ⟨m, h.size_buckets_pos⟩ k f := by simp [Raw.modify, h.size_buckets_pos] +theorem union_eq [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (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] + section variable {β : Type v} diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index 7c49340765..3ff4c82c1e 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -105,7 +105,7 @@ macro_rules | apply Raw.WF.alter₀ | apply Raw.WF.modify₀ | apply Raw.WF.constAlter₀ | apply Raw.WF.constModify₀ | apply Raw₀.wf_insertMany₀ | apply Raw₀.Const.wf_insertMany₀ - | apply Raw₀.Const.wf_insertManyIfNewUnit₀ + | 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) @@ -120,6 +120,7 @@ private meta def modifyMap : Std.DHashMap Name (fun _ => Name) := ⟨`erase, ``toListModel_erase⟩, ⟨`insertIfNew, ``toListModel_insertIfNew⟩, ⟨`insertMany, ``toListModel_insertMany_list⟩, + ⟨`union, ``toListModel_union⟩, ⟨`Const.insertMany, ``Const.toListModel_insertMany_list⟩, ⟨`Const.insertManyIfNewUnit, ``Const.toListModel_insertManyIfNewUnit_list⟩, ⟨`alter, ``toListModel_alter⟩, @@ -1951,7 +1952,7 @@ theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_mem [EquivBEq theorem getKey!_insertManyIfNewUnit_list_of_contains [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {l : List α} {k : α} : - m.contains k → getKey! (insertManyIfNewUnit m l).1 k = getKey! m k := by + m.contains k → getKey! (insertManyIfNewUnit m l).1 k = getKey! m k := by simp_to_model [Const.insertManyIfNewUnit, contains, getKey!] using List.getKey!_insertListIfNewUnit_of_contains @@ -2025,12 +2026,12 @@ theorem get?_insertManyIfNewUnit_list [EquivBEq α] [LawfulHashable α] (h : m.1 theorem get_insertManyIfNewUnit_list {l : List α} {k : α} {h} : - get (insertManyIfNewUnit m l).1 k h = () := by + get (insertManyIfNewUnit m l).1 k h = () := by simp theorem get!_insertManyIfNewUnit_list {l : List α} {k : α} : - get! (insertManyIfNewUnit m l).1 k = () := by + get! (insertManyIfNewUnit m l).1 k = () := by simp theorem getD_insertManyIfNewUnit_list @@ -2655,7 +2656,7 @@ abbrev get?_insertManyIfNewUnit_empty_list := @get?_insertManyIfNewUnit_emptyWit theorem get_insertManyIfNewUnit_emptyWithCapacity_list {l : List α} {k : α} {h} : - get (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k h = () := by + get (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k h = () := by simp set_option linter.missingDocs false in @@ -2664,7 +2665,7 @@ abbrev get_insertManyIfNewUnit_empty_list := @get_insertManyIfNewUnit_emptyWithC theorem get!_insertManyIfNewUnit_emptyWithCapacity_list {l : List α} {k : α} : - get! (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k = () := by + get! (insertManyIfNewUnit (emptyWithCapacity : Raw₀ α (fun _ => Unit)) l) k = () := by simp set_option linter.missingDocs false in @@ -2684,6 +2685,382 @@ end Const end insertMany +section Union + +variable (m₁ m₂ : Raw₀ α β) + +variable {m₁ m₂} + +/- contains -/ +theorem contains_union_of_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + m₁.contains k → (m₁.union m₂).contains k := by + simp_to_model [contains, union] using List.contains_insertList_of_left + +theorem contains_union_of_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + m₂.contains k → (m₁.union m₂).contains k := by + simp_to_model [contains, union] using List.contains_insertList_of_right + +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + (m₁.union m₂).contains k = (m₁.contains k || m₂.contains k) := by + simp_to_model [contains, union] using List.containsKey_insertList_disj_of_containsKey + +theorem contains_union_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k : α} : + (m₁.union m₂).contains k ↔ m₁.contains k ∨ m₂.contains k := by + simp_to_model [union, contains] using List.contains_insertList_iff + +theorem contains_of_contains_union_of_contains_eq_false_right [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + (m₁.union m₂).contains k → m₂.contains k = false → m₁.contains k := by + simp_to_model [union, contains] using List.contains_of_contains_insertList_of_contains_eq_false_right + +theorem contains_of_contains_union_of_contains_eq_false_left [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + (m₁.union m₂).contains k → m₁.contains k = false → m₂.contains k := by + simp_to_model [union, contains] using List.contains_of_contains_insertList_of_contains_eq_false_left + +/- Equiv -/ +theorem union_insert_right_equiv_insert_union [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + (m₁.union (m₂.insert p.fst p.snd)).1.Equiv ((m₁.union m₂).insert p.fst p.snd).1 := by + simp_to_model [union, insert] + apply List.Perm.trans + . apply insertList_perm_of_perm_second + simp_to_model [insert] + . apply insertEntry_of_perm + . wf_trivial + . apply List.Perm.refl + . constructor + rw [← Raw.keys_eq_keys_toListModel] + exact m₁.distinct_keys h₁ + . apply List.DistinctKeys.perm + . apply toListModel_insert + . wf_trivial + . apply List.DistinctKeys.insertEntry + . constructor + rw [← Raw.keys_eq_keys_toListModel] + exact m₂.distinct_keys h₂ + . apply List.Perm.trans + . apply insertList_insertEntry_right_equiv_insertEntry_insertList + any_goals wf_trivial + . apply insertEntry_of_perm + . apply List.DistinctKeys.insertList + . wf_trivial + . apply List.Perm.symm + . apply toListModel_union (by wf_trivial) (by wf_trivial) + +/- get? -/ +theorem get?_union [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} : + (m₁.union m₂).get? k = (m₂.get? k).or (m₁.get? k) := by + simp_to_model [union, get?] using List.getValueCast?_of_insertList + +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) : + (m₁.union m₂).get? k = m₂.get? k := by + revert contains_eq_false + 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) : + (m₁.union m₂).get? k = m₁.get? k := by + simp_to_model [union, get?, contains] using List.getValueCast?_insertList_of_contains_eq_false + revert contains_eq_false + simp_to_model [contains] + simp only [containsKey_eq_contains_map_fst, List.contains_eq_mem, List.mem_map, + decide_eq_false_iff_not, not_exists, not_and, imp_self] + +/- get -/ +theorem get_union_of_contains_right [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (contains_right : m₂.contains k) : + (m₁.union m₂).get k (contains_union_of_right h₁ h₂ contains_right) = m₂.get k contains_right := by + revert contains_right + simp_to_model [union, get, contains] + intro contains_right + apply List.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 + +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'} : + (m₁.union m₂).get k h' = m₁.get k (contains_of_contains_union_of_contains_eq_false_right h₁ h₂ h' contains_eq_false) := by + revert contains_eq_false + simp_to_model [union, get, contains] + intro contains_eq_false + apply List.getValueCast_insertList_of_contains_eq_false + . rw [← List.containsKey_eq_contains_map_fst] + exact contains_eq_false + +/- getD -/ +theorem getD_union [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} : + (m₁.union m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := by + simp_to_model [union, getD, contains] using List.getValueCastD_of_insertList + +theorem getD_union_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} {fallback : β k} (contains_eq_false : m₁.contains k = false) : + (m₁.union m₂).getD k fallback = m₂.getD k fallback := by + revert contains_eq_false + simp_to_model [union, contains, getD] + intro contains_eq_false + apply List.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) + {k : α} {fallback : β k} (contains_eq_false : m₂.contains k = false) : + (m₁.union m₂).getD k fallback = m₁.getD k fallback := by + revert contains_eq_false + simp_to_model [union, getD, contains] + intro contains_eq_false + apply List.getValueCastD_insertList_of_contains_eq_false + . rw [← List.containsKey_eq_contains_map_fst] + exact contains_eq_false + +/- get! -/ +theorem get!_union [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] : + (m₁.union m₂).get! k = m₂.getD k (m₁.get! k) := by + simp_to_model [union, get!, getD, contains] + apply List.getValueCastD_of_insertList + all_goals wf_trivial + +theorem get!_union_of_contains_eq_false_left [LawfulBEq α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} [Inhabited (β k)] (contains_eq_false : m₁.contains k = false) : + (m₁.union m₂).get! k = m₂.get! k := by + revert contains_eq_false + simp_to_model [union, contains, get!] + intro contains_eq_false + apply List.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) + {k : α} [Inhabited (β k)] (contains_eq_false : m₂.contains k = false) : + (m₁.union m₂).get! k = m₁.get! k := by + revert contains_eq_false + simp_to_model [union, get!, contains] + intro contains_eq_false + apply List.getValueCastD_insertList_of_contains_eq_false + . rw [← List.containsKey_eq_contains_map_fst] + exact contains_eq_false + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} : + (m₁.union m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := by + simp_to_model [union, contains, getKey?] using List.getKey?_insertList + +theorem getKey?_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (not_mem : m₁.contains k = false) : + (m₁.union m₂).getKey? k = m₂.getKey? k := by + revert not_mem + simp_to_model [contains, getKey?, union] + intro not_mem + apply List.getKey?_insertList_of_contains_eq_false_left + all_goals wf_trivial + +theorem getKey?_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (not_mem : m₂.contains k = false) : + (m₁.union m₂).getKey? k = m₁.getKey? k := by + revert not_mem + simp_to_model [contains, getKey?, union] + intro not_mem + apply List.getKey?_insertList_of_contains_eq_false_right + . exact not_mem + +/- getKey -/ +theorem getKey_union_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (mem : m₂.contains k) : + (m₁.union m₂).getKey k (contains_union_of_right h₁ h₂ mem) = m₂.getKey k mem := by + simp_to_model [union, contains, getKey] using List.getKey_insertList_of_contains_right + +theorem getKey_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'} : + (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 + +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'} : + (m₁.union m₂).getKey k h' = m₁.getKey k (contains_of_contains_union_of_contains_eq_false_right h₁ h₂ h' contains_eq_false) := by + revert contains_eq_false + simp_to_model [union, getKey, contains] + intro contains_eq_false + apply List.getKey_insertList_of_contains_eq_false + . rw [← List.containsKey_eq_contains_map_fst] + exact contains_eq_false + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} : + (m₁.union m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := by + simp_to_model [union, getKeyD] using getKeyD_insertList + +theorem getKeyD_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} (h' : m₁.contains k = false) : + (m₁.union m₂).getKeyD k fallback = m₂.getKeyD k fallback := by + revert h' + simp_to_model [contains, union, getKeyD] + intro h' + apply List.getKeyD_insertList_of_contains_eq_false_left + . wf_trivial + . wf_trivial + . exact h' + +theorem getKeyD_union_of_contains_eq_false_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) {k fallback : α} (h' : m₂.contains k = false) : + (m₁.union m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + revert h' + simp_to_model [contains, union, getKeyD] + intro h' + apply List.getKeyD_insertList_of_contains_eq_false_right h' + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] + (h₁ : m₁.1.WF) + (h₂ : m₂.1.WF) {k : α} : + (m₁.union m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := by + simp_to_model [union, getKey!, getKeyD] using List.getKeyD_insertList + +theorem getKey!_union_of_contains_eq_false_left [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 [getKey!, contains, union] using List.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 + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) : (∀ (a : α), m₁.contains a → m₂.contains a = false) → + (m₁.union m₂).1.size = m₁.1.size + m₂.1.size := by + simp_to_model [union, size, contains] using List.length_insertList_distinct + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) : m₁.1.size ≤ (m₁.union m₂).1.size := by + simp_to_model [union, size] using List.length_le_length_insertList + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) + (h₂ : m₂.val.WF) : m₂.1.size ≤ (m₁.union m₂).1.size := by + simp_to_model [union, size] using List.length_right_le_length_insertList + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) : + (m₁.union m₂).1.size ≤ m₁.1.size + m₂.1.size := by + simp_to_model [union, size] using List.length_insertList_le + +/- isEmpty -/ +@[simp] +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 + +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 + +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 + +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) : + Const.get? (m₁.union m₂) k = Const.get? m₁ k := by + 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 + +/- get -/ +theorem get_union_of_contains_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {k : α} (h : m₂.contains k) : + Const.get (m₁.union m₂) k (contains_union_of_right h₁ h₂ h) = Const.get m₂ k h := by + revert h + simp_to_model [union, contains, Const.get] + intro h + apply List.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 + +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'} : + Const.get (m₁.union m₂) k h' = Const.get m₁ k (contains_of_contains_union_of_contains_eq_false_right h₁ h₂ h' contains_eq_false) := by + 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 + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} {fallback : β} : + Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k (Const.getD m₁ k fallback) := by + simp_to_model [union, Const.getD] using List.getValueD_insertList + +theorem getD_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) + {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 + +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) : + Const.getD (m₁.union m₂) k fallback = Const.getD m₁ k fallback := by + 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 + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.val.WF) (h₂ : m₂.val.WF) {k : α} : + Const.get! (m₁.union m₂) k = Const.getD m₂ k (Const.get! m₁ k) := by + simp_to_model [union, Const.getD, Const.get!] using List.getValueD_insertList + +theorem get!_union_of_contains_eq_false_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (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.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) : + Const.get! (m₁.union m₂) k = Const.get! m₁ k := by + 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 + +end Const + section Alter theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] (h : m.1.WF) {k : α} diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index c80f030c8a..d10022f9ec 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -13,6 +13,7 @@ import all Std.Data.DHashMap.Internal.Defs public import Std.Data.DHashMap.Internal.Model import all Std.Data.DHashMap.Internal.AssocList.Basic public import Std.Data.DHashMap.Internal.AssocList.Lemmas +import all Std.Data.DHashMap.RawDef public section @@ -1026,7 +1027,7 @@ theorem wfImp_filter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m /-! # `insertListₘ` -/ -theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHashable α] +theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : Perm (toListModel (insertListₘ m l).1.buckets) (List.insertList (toListModel m.1.buckets) l) := by @@ -1038,6 +1039,74 @@ theorem toListModel_insertListₘ [BEq α] [Hashable α] [EquivBEq α][LawfulHas apply Perm.trans (ih (wfImp_insert h)) apply List.insertList_perm_of_perm_first (toListModel_insert h) (wfImp_insert h).distinct +/-! # `insertListₘ` -/ + +theorem toListModel_insertListIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {m : Raw₀ α β} {l : List ((a : α) × β a)} (h : Raw.WFImp m.1) : + Perm (toListModel (insertListIfNewₘ m l).1.buckets) + (List.insertListIfNew (toListModel m.1.buckets) l) := by + induction l generalizing m with + | nil => + simp [insertListIfNewₘ, List.insertListIfNew] + | cons hd tl ih => + simp only [insertListIfNewₘ, List.insertListIfNew] + apply Perm.trans (ih (wfImp_insertIfNew h)) + apply List.insertListIfNew_perm_of_perm_first (toListModel_insertIfNew h) (wfImp_insertIfNew h).distinct + +/-! # `unionₘ` -/ + +theorem insertMany_eq_insertListₘ_toListModel [BEq α] [Hashable α] (m m₂ : Raw₀ α β) : + insertMany m m₂.1 = insertListₘ m (toListModel m₂.1.buckets) := by + simp only [insertMany, bind_pure_comp, map_pure, bind_pure] + simp only [ForIn.forIn] + simp only [Raw.forIn_eq_forIn_toListModel, forIn_pure_yield_eq_foldl, Id.run_pure] + generalize toListModel m₂.val.buckets = l + suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop), + (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insert a b)) → P m → P m' }), + (List.foldl (fun m' p => ⟨m'.val.insert p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = + t.val.insertListₘ l from this _ + intro t + induction l generalizing m with + | nil => simp [insertListₘ] + | cons hd tl ih => + 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] + simp only [ForIn.forIn] + simp only [Raw.forIn_eq_forIn_toListModel, forIn_pure_yield_eq_foldl, Id.run_pure] + generalize toListModel m₂.val.buckets = l + suffices ∀ (t : { m' // ∀ (P : Raw₀ α β → Prop), + (∀ {m'' : Raw₀ α β} {a : α} {b : β a}, P m'' → P (m''.insertIfNew a b)) → P m → P m' }), + (List.foldl (fun m' p => ⟨m'.val.insertIfNew p.1 p.2, fun P h₁ h₂ => h₁ (m'.2 _ h₁ h₂)⟩) t l).val = + t.val.insertListIfNewₘ l from this _ + intro t + induction l generalizing m with + | nil => simp [insertListIfNewₘ] + | cons hd tl ih => + simp only [List.foldl_cons] + apply ih + +theorem union_eq_unionₘ [BEq α] [Hashable α] (m₁ m₂ : Raw₀ α β) : + union m₁ m₂ = unionₘ m₁ m₂ := by + rw [union, unionₘ] + split + · rw [insertManyIfNew_eq_insertListIfNewₘ_toListModel] + · rw [insertMany_eq_insertListₘ_toListModel] + +theorem toListModel_unionₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {m₁ m₂ : Raw₀ α β} (h₁ : Raw.WFImp m₁.1) (h₂ : Raw.WFImp m₂.1) : + Perm (toListModel (unionₘ m₁ m₂).1.buckets) + (List.insertList (toListModel m₁.1.buckets) (toListModel m₂.1.buckets)) := by + refine Perm.trans ?_ (Perm.symm (List.insertList_perm_insertSmallerList h₁.distinct h₂.distinct)) + rw [unionₘ, insertSmallerList, h₁.size_eq, h₂.size_eq] + split + · exact toListModel_insertListIfNewₘ ‹_› + · exact toListModel_insertListₘ ‹_› + end Raw₀ namespace Raw @@ -1177,6 +1246,44 @@ theorem toListModel_insertMany_list [BEq α] [Hashable α] [EquivBEq α] [Lawful apply toListModel_insertListₘ exact h +/-! # `insertManyIfNew` -/ + +theorem wfImp_insertManyIfNew [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} + [ForIn Id ρ ((a : α) × β a)] {m : Raw₀ α β} {l : ρ} (h : Raw.WFImp m.1) : + Raw.WFImp (m.insertManyIfNew l).1.1 := + Raw.WF.out ((m.insertManyIfNew l).2 _ Raw.WF.insertIfNew₀ (.wf m.2 h)) + +theorem wf_insertManyIfNew₀ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} + [ForIn Id ρ ((a : α) × β a)] {m : Raw α β} {h : 0 < m.buckets.size} {l : ρ} (h' : m.WF) : + (Raw₀.insertManyIfNew ⟨m, h⟩ l).1.1.WF := + (Raw₀.insertManyIfNew ⟨m, h⟩ l).2 _ Raw.WF.insertIfNew₀ h' + +theorem toListModel_insertManyIfNew_list [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {m : Raw₀ α β} {l : List ((a : α) × (β a))} (h : Raw.WFImp m.1) : + Perm (toListModel (insertManyIfNew m l).1.1.buckets) + (List.insertListIfNew (toListModel m.1.buckets) l) := by + rw [insertManyIfNew_eq_insertListIfNewₘ] + apply toListModel_insertListIfNewₘ + exact h + +/-! # `union` -/ + +theorem wf_union₀ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {m₁ m₂ : Raw α β} {h₁ : 0 < m₁.buckets.size} {h₂ : 0 < m₂.buckets.size} (h'₁ : m₁.WF) + (h'₂ : m₂.WF) : + (Raw₀.union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩).1.WF := by + rw [union] + split + · 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) + (List.insertList (toListModel m₁.1.buckets) (toListModel m₂.1.buckets)) := by + rw [union_eq_unionₘ] + exact toListModel_unionₘ h₁ h₂ + /-! # `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 1e6c941b97..37a809ce75 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -64,6 +64,11 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := Iff.rfl +-- The following lemma becomes a simp lemma at the bottom of the file. +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := by + rw [← Bool.not_eq_true] + simp only [contains_iff_mem] + theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b := Raw₀.contains_congr _ m.2 hab @@ -1766,6 +1771,299 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] {l : ρ} : (m.insertMany l).isEmpty → m.isEmpty := Raw₀.isEmpty_of_isEmpty_insertMany ⟨m.1, _⟩ m.2 +section Union + +variable (m₁ m₂ : DHashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + @Raw₀.contains_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + @Raw₀.contains_union_of_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + @Raw₀.contains_union_of_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + @Raw₀.contains_union_iff _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := by + intro h₁ h₂ + rw [← contains_eq_false_iff_not_mem] at h₂ + exact @Raw₀.contains_of_contains_union_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k h₁ h₂ + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := by + intro h₁ h₂ + rw [← contains_eq_false_iff_not_mem] at h₂ + exact @Raw₀.contains_of_contains_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k h₁ h₂ + +/- Equiv -/ +theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} : + (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) := + ⟨@Raw₀.union_insert_right_equiv_insert_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ p m₁.2 m₂.2⟩ + +/- get? -/ +theorem get?_union [LawfulBEq α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + @Raw₀.get?_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k + +theorem get?_union_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get?_union_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?_union_of_not_mem_right [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get?_union_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_union_of_mem_right [LawfulBEq α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem := + @Raw₀.get_union_of_contains_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ m₁.2 m₂.2 k mem + +theorem get_union_of_not_mem_left [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + rw [mem_iff_contains] at h' + exact @Raw₀.get_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k not_mem h' + +theorem get_union_of_not_mem_right [LawfulBEq α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + rw [mem_iff_contains] at h' + exact @Raw₀.get_union_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k not_mem h' + +/- getD -/ +theorem getD_union [LawfulBEq α] {k : α} {fallback : β k} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + @Raw₀.getD_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k fallback + +theorem getD_union_of_not_mem_left [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getD_union_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 + +theorem getD_union_of_not_mem_right [LawfulBEq α] + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getD_union_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 + +/- get! -/ +theorem get!_union [LawfulBEq α] {k : α} [Inhabited (β k)] : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + @Raw₀.get!_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ m₁.2 m₂.2 k _ + +theorem get!_union_of_not_mem_left [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get!_union_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!_union_of_not_mem_right [LawfulBEq α] + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.get!_union_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 + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := + @Raw₀.getKey?_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey?_union_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 getKey?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey? k = m₁.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey?_union_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 + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right mem) = m₂.getKey k mem := + @Raw₀.getKey_union_of_contains_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k mem + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h' not_mem) :=by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey_union_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 h' + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey_union_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 h' + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := + @Raw₀.getKeyD_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback :=by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKeyD_union_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 + +theorem getKeyD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKeyD_union_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 + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := + @Raw₀.getKey!_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey!_union_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 getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.getKey!_union_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 + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := by + simp only [← contains_eq_false_iff_not_mem] + exact @Raw₀.size_union_of_not_mem _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + @Raw₀.size_left_le_size_union α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + @Raw₀.size_right_le_size_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + @Raw₀.size_union_le_size_add_size _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + @Raw₀.isEmpty_union α β _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 + +end Union + +namespace Const + +variable {β : Type v} {m₁ m₂ : DHashMap α (fun _ => β)} + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + Const.get? (m₁.union m₂) k = (Const.get? m₂ k).or (Const.get? m₁ k) := + @Raw₀.Const.get?_union _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get? (m₁.union m₂) k = Const.get? m₂ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get?_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get? (m₁.union m₂) k = Const.get? m₁ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get?_union_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : m₂.contains k) : + Const.get (m₁.union m₂) k (mem_union_of_right mem) = Const.get m₂ k mem := + @Raw₀.Const.get_union_of_contains_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + Const.get (m₁.union m₂) k h' = Const.get m₂ k (mem_of_mem_union_of_not_mem_left h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get_union_of_contains_eq_false_left _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k not_mem h' + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + Const.get (m₁.union m₂) k h' = Const.get m₁ k (mem_of_mem_union_of_not_mem_right h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get_union_of_contains_eq_false_right _ _ _ _ ⟨m₁.1, _⟩ ⟨m₂.1, _⟩ _ _ m₁.2 m₂.2 k not_mem h' + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k (Const.getD m₁ k fallback) := + @Raw₀.Const.getD_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ m₁.2 m₂.2 k fallback + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + Const.getD (m₁.union m₂) k fallback = Const.getD m₂ k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.getD_union_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 + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + Const.getD (m₁.union m₂) k fallback = Const.getD m₁ k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.getD_union_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 + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] {k : α} : + Const.get! (m₁.union m₂) k = Const.getD m₂ k (Const.get! m₁ k) := + @Raw₀.Const.get!_union _ _ _ _ ⟨m₁.1, m₁.2.size_buckets_pos⟩ ⟨m₂.1, m₂.2.size_buckets_pos⟩ _ _ _ m₁.2 m₂.2 k + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get! (m₁.union m₂) k = Const.get! m₂ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get!_union_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!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get! (m₁.union m₂) k = Const.get! m₁ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + exact @Raw₀.Const.get!_union_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 + +end Const + namespace Const variable {β : Type v} {m : DHashMap α (fun _ => β)} @@ -4273,5 +4571,5 @@ theorem toList_map {m : DHashMap α fun _ => β} end Const end map - +attribute [simp] contains_eq_false_iff_not_mem end Std.DHashMap diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index f123158299..c892bf32ee 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -9,6 +9,7 @@ prelude public import Init.Data.BEq public import Init.Data.LawfulHashable public import Std.Data.DHashMap.Internal.Defs +import all Std.Data.DHashMap.Internal.Defs public section @@ -401,20 +402,6 @@ by `foldM`. -/ def foldRev (f : δ → (a : α) → β a → δ) (init : δ) (b : Raw α β) : δ := Id.run (Internal.foldRevM (pure <| f · · ·) init b) -/-- Carries out a monadic action on each mapping in the hash map in some order. -/ -@[inline] def forM (f : (a : α) → β a → m PUnit) (b : Raw α β) : m PUnit := - b.buckets.forM (AssocList.forM f) - -/-- Support for the `for` loop construct in `do` blocks. -/ -@[inline] def forIn (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : Raw α β) : m δ := - ForIn.forIn b.buckets init (fun bucket acc => bucket.forInStep acc f) - -instance : ForM m (Raw α β) ((a : α) × β a) where - forM m f := m.forM (fun a b => f ⟨a, b⟩) - -instance : ForIn m (Raw α β) ((a : α) × β a) where - forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init - namespace Const variable {β : Type v} @@ -469,6 +456,25 @@ only those mappings where the function returns `some` value. @[inline] def keysArray (m : Raw α β) : Array α := m.fold (fun acc k _ => acc.push k) (.emptyWithCapacity m.size) +/-- +Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +the second argument will appear in the result. + +This function always merges the smaller map into the larger map, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := + if h₁ : 0 < m₁.buckets.size then + if h₂ : 0 < m₂.buckets.size then + Raw₀.union ⟨m₁, h₁⟩ ⟨m₂, h₂⟩ + else + m₁ + else + m₂ + +instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ + + section Unverified /-! We currently do not provide lemmas for the functions below. -/ @@ -515,12 +521,6 @@ This is mainly useful to implement `HashSet.insertMany`, so if you are consideri (Raw₀.Const.insertManyIfNewUnit ⟨m, h⟩ l).1 else m -- will never happen for well-formed inputs -/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ - /-- Creates a hash map from an array of keys, associating the value `()` with each key. This is mainly useful to implement `HashSet.ofArray`, so if you are considering using this, @@ -713,6 +713,16 @@ theorem WF.Const.unitOfList [BEq α] [Hashable α] {l : List α} : (Const.unitOfList l : Raw α (fun _ => Unit)).WF := Const.insertManyIfNewUnit WF.empty +theorem WF.union₀ [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (Raw₀.union ⟨m₁, h₁.size_buckets_pos⟩ ⟨m₂, h₂.size_buckets_pos⟩).val.WF := by + simp only [Raw₀.union] + split + . exact (Raw₀.insertManyIfNew ⟨m₂, h₂.size_buckets_pos⟩ m₁).2 _ WF.insertIfNew₀ h₂ + . exact (Raw₀.insertMany ⟨m₁, h₁.size_buckets_pos⟩ m₂).2 _ WF.insert₀ h₁ + +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂ : Raw α β).WF := by + simp [Std.DHashMap.Raw.union, h₁.size_buckets_pos, h₂.size_buckets_pos] + exact WF.union₀ h₁ h₂ + end WF end Raw diff --git a/src/Std/Data/DHashMap/RawDef.lean b/src/Std/Data/DHashMap/RawDef.lean index 2a28ea7928..74ba4c56d6 100644 --- a/src/Std/Data/DHashMap/RawDef.lean +++ b/src/Std/Data/DHashMap/RawDef.lean @@ -20,10 +20,12 @@ This file defines the type `Std.Data.DHashMap.Raw`. All of its functions are def set_option linter.missingDocs true set_option autoImplicit false -universe u v +universe u v w w' namespace Std.DHashMap +open Internal + /-- Dependent hash maps without a bundled well-formedness invariant, suitable for use in nested inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `DHashMap` @@ -50,4 +52,24 @@ structure Raw (α : Type u) (β : α → Type v) where /-- Internal implementation detail of the hash map -/ buckets : Array (DHashMap.Internal.AssocList α β) +namespace Raw + +variable {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} + +/-- 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) + +/-- Support for the `for` loop construct in `do` blocks. -/ +@[inline] def forIn [Monad m] (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : Raw α β) : m δ := + ForIn.forIn b.buckets init (fun bucket acc => bucket.forInStep acc f) + +instance x : ForM m (Raw α β) ((a : α) × β a) where + forM m f := m.forM (fun a b => f ⟨a, b⟩) + +instance : ForIn m (Raw α β) ((a : α) × β a) where + forIn m init f := m.forIn (fun a b acc => f ⟨a, b⟩ acc) init + +end Raw + end Std.DHashMap diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 60bdf43434..3865c6543c 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -49,7 +49,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] + ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq, ``union_eq] /-- Internal implementation detail of the hash map -/ scoped syntax "simp_to_raw" ("using" term)? : tactic @@ -112,6 +112,11 @@ theorem mem_iff_contains {m : Raw α β} {a : α} : theorem contains_iff_mem {m : Raw α β} {a : α} : m.contains a ↔ a ∈ m := Iff.rfl +-- The following lemma becomes a simp lemma at the bottom of the file. +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := by + rw [← Bool.not_eq_true] + simp only [contains_iff_mem] + theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) : m.contains a = m.contains b := by simp_to_raw using Raw₀.contains_congr @@ -1861,6 +1866,428 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W {l : ρ} : (m.insertMany l).isEmpty → m.isEmpty := by simp_to_raw using Raw₀.isEmpty_of_isEmpty_insertMany +section Union +variable {β : α → Type v} + +variable (m₁ m₂ : Raw α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := by + simp only [Union.union] + simp_to_raw using Raw₀.contains_union + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := by + simp only [Union.union, Membership.mem] + simp_to_raw using Raw₀.contains_union_of_left + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := by + simp only [Union.union, Membership.mem] + simp_to_raw using Raw₀.contains_union_of_right + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := by + simp only [Union.union, Membership.mem] + simp_to_raw using Raw₀.contains_union_iff + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := by + simp only [Union.union] + rw [← contains_eq_false_iff_not_mem] + simp only [mem_iff_contains] + simp_to_raw using Raw₀.contains_of_contains_union_of_contains_eq_false_right + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := by + simp only [Union.union] + rw [← contains_eq_false_iff_not_mem] + simp only [mem_iff_contains] + simp_to_raw using Raw₀.contains_of_contains_union_of_contains_eq_false_left + +/- Equiv -/ +theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : (a : α) × β a} + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) := by + simp only [Union.union] + simp_to_raw using Raw₀.union_insert_right_equiv_insert_union + +/- get? -/ +theorem get?_union [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := by + simp only [Union.union] + simp_to_raw using Raw₀.get?_union + +theorem get?_union_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := by + revert not_mem + simp only [Union.union] + rw [← contains_eq_false_iff_not_mem] + simp_to_raw + apply Raw₀.get?_union_of_contains_eq_false_left + all_goals wf_trivial + +theorem get?_union_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := by + revert not_mem + simp only [Union.union] + rw [← contains_eq_false_iff_not_mem] + simp_to_raw + apply Raw₀.get?_union_of_contains_eq_false_right + all_goals wf_trivial + +/- get -/ +theorem get_union_of_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right h₁ h₂ mem) = m₂.get k mem := by + rw [mem_iff_contains] at mem + revert mem + simp only [Union.union] + simp_to_raw + apply Raw₀.get_union_of_contains_right + all_goals wf_trivial + +theorem get_union_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro contains_eq_false + apply Raw₀.get_union_of_contains_eq_false_left + all_goals wf_trivial + +theorem get_union_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro not_mem + apply Raw₀.get_union_of_contains_eq_false_right + all_goals wf_trivial + +/- getD -/ +theorem getD_union [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := by + simp only [Union.union] + simp_to_raw using Raw₀.getD_union + +theorem getD_union_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.getD_union_of_contains_eq_false_left + +theorem getD_union_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β k} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.getD_union_of_contains_eq_false_right + +/- get! -/ +theorem get!_union [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := by + simp only [Union.union] + simp_to_raw using Raw₀.get!_union + +theorem get!_union_of_not_mem_left [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.get!_union_of_contains_eq_false_left + +theorem get!_union_of_not_mem_right [LawfulBEq α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} [Inhabited (β k)] (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.get!_union_of_contains_eq_false_right + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := by + simp only [Union.union] + simp_to_raw using Raw₀.getKey?_union + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.getKey?_union_of_contains_eq_false_left + +theorem getKey?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey? k = m₁.getKey? k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.getKey?_union_of_contains_eq_false_right + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right h₁ h₂ mem) = m₂.getKey k mem := by + rw [mem_iff_contains] at mem + revert mem + simp only [Union.union] + simp_to_raw using Raw₀.getKey_union_of_contains_right + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro not_mem + apply Raw₀.getKey_union_of_contains_eq_false_left + all_goals wf_trivial + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro contains_eq_false + apply Raw₀.getKey_union_of_contains_eq_false_right + all_goals wf_trivial + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := by + simp only [Union.union] + simp_to_raw using Raw₀.getKeyD_union + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback := by + rw [← contains_eq_false_iff_not_mem] at mem + revert mem + simp only [Union.union] + simp_to_raw + intro mem + apply Raw₀.getKeyD_union_of_contains_eq_false_left + all_goals wf_trivial + +theorem getKeyD_union_of_not_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 + rw [← contains_eq_false_iff_not_mem] at mem + revert mem + simp only [Union.union] + simp_to_raw + intro mem + apply Raw₀.getKeyD_union_of_contains_eq_false_right + all_goals wf_trivial + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] + (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := by + simp only [Union.union] + simp_to_raw using Raw₀.getKey!_union + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using getKey!_union_of_contains_eq_false_left + +theorem getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using getKey!_union_of_contains_eq_false_right + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := by + intro hyp + conv at hyp => + ext + lhs + rw [mem_iff_contains] + simp only [← contains_eq_false_iff_not_mem] at hyp + revert hyp + simp only [Union.union] + simp_to_raw using Raw₀.size_union_of_not_mem + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₁.size ≤ (m₁ ∪ m₂).size := by + simp only [Union.union] + simp_to_raw using @Raw₀.size_left_le_size_union α β _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₂.size ≤ (m₁ ∪ m₂).size := by + simp only [Union.union] + simp_to_raw using @Raw₀.size_right_le_size_union α β _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := by + simp only [Union.union] + simp_to_raw using @Raw₀.size_union_le_size_add_size α β _ _ ⟨m₁, _⟩ ⟨m₂, _⟩ + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := by + simp only [Union.union] + simp_to_raw using Raw₀.isEmpty_union + +end Union + +namespace Const + +variable {β : Type v} {m₁ m₂ : Raw α (fun _ => β)} + +theorem get?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get? (m₁ ∪ m₂) k = (Const.get? m₂ k).or (Const.get? m₁ k) := by + simp only [Union.union] + simp_to_raw using Raw₀.Const.get?_union + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get? (m₁ ∪ m₂) k = Const.get? m₂ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.get?_union_of_contains_eq_false_left + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get? (m₁ ∪ m₂) k = Const.get? m₁ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.get?_union_of_contains_eq_false_right + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + Const.get (m₁ ∪ m₂) k (mem_union_of_right h₁ h₂ mem) = Const.get m₂ k mem := by + rw [mem_iff_contains] at mem + revert mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.get_union_of_contains_right + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + Const.get (m₁ ∪ m₂) k h' = Const.get m₂ k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro not_mem + apply Raw₀.Const.get_union_of_contains_eq_false_left + all_goals wf_trivial + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + Const.get (m₁ ∪ m₂) k h' = Const.get m₁ k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw + intro not_mem + apply Raw₀.Const.get_union_of_contains_eq_false_right + all_goals wf_trivial + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β} : + Const.getD (m₁ ∪ m₂) k fallback = Const.getD m₂ k (Const.getD m₁ k fallback) := by + simp only [Union.union] + simp_to_raw using Raw₀.Const.getD_union + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + Const.getD (m₁ ∪ m₂) k fallback = Const.getD m₂ k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.getD_union_of_contains_eq_false_left + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + Const.getD (m₁ ∪ m₂) k fallback = Const.getD m₁ k fallback := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.getD_union_of_contains_eq_false_right + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + Const.get! (m₁ ∪ m₂) k = Const.getD m₂ k (Const.get! m₁ k) := by + simp only [Union.union] + simp_to_raw using Raw₀.Const.get!_union + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + Const.get! (m₁ ∪ m₂) k = Const.get! m₂ k := by + rw [← contains_eq_false_iff_not_mem] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.get!_union_of_contains_eq_false_left + +theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + Const.get! (m₁ ∪ m₂) k = Const.get! m₁ k := by + rw [← contains_eq_false_iff_not_mem ] at not_mem + revert not_mem + simp only [Union.union] + simp_to_raw using Raw₀.Const.get!_union_of_contains_eq_false_right + +end Const + namespace Const variable {β : Type v} {m : Raw α (fun _ => β)} @@ -4509,6 +4936,6 @@ end Const end map +attribute [simp] contains_eq_false_iff_not_mem end Raw - end Std.DHashMap diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index bc9f478f2a..5ee4c2fa2c 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -255,6 +255,18 @@ instance [BEq α] [Hashable α] {m : Type w → Type w'} : ForIn m (HashMap α Array α := m.inner.keysArray +/-- +Computes the union of the given hash maps. If a key appears in both maps, the entry contains in +the second argument will appear in the result. + +This function always merges the smaller map into the larger map, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β := + ⟨DHashMap.union m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ @@ -271,12 +283,6 @@ section Unverified Array β := m.inner.valuesArray -/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashMap α β) : HashMap α β := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (HashMap α β) := ⟨union⟩ - @[inline, inherit_doc DHashMap.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) : HashMap α Unit := ⟨DHashMap.Const.unitOfArray l⟩ diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 7dff8c621d..cb247163c2 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -61,6 +61,10 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := DHashMap.contains_iff_mem +-- The following lemma becomes a simp lemma at the bottom of the file. +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := + DHashMap.contains_eq_false_iff_not_mem + theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b := DHashMap.contains_congr hab @@ -1305,6 +1309,202 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := DHashMap.Const.isEmpty_of_isEmpty_insertMany +section Union +variable {β : Type v} + +variable (m₁ m₂ : HashMap α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + @DHashMap.contains_union _ _ _ _ m₁.inner m₂.inner _ _ k + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂:= + @DHashMap.mem_union_of_left _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂:= + @DHashMap.mem_union_of_right _ _ _ _ m₁.inner m₂.inner _ _ k + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + @DHashMap.mem_union_iff _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + @DHashMap.mem_of_mem_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + @DHashMap.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k + +/- Equiv -/ +theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : α × β} : + (m₁ ∪ (m₂.insert p.fst p.snd)) ~m ((m₁ ∪ m₂).insert p.fst p.snd) := + ⟨@DHashMap.union_insert_right_equiv_union_insert _ _ _ _ m₁.inner m₂.inner _ _ ⟨p.fst, p.snd⟩⟩ + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + @DHashMap.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := + @DHashMap.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := + @DHashMap.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (contains_right : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right contains_right) = m₂.get k contains_right := + @DHashMap.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k contains_right + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := + @DHashMap.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) := + @DHashMap.Const.get_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + @DHashMap.Const.getD_union _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := + @DHashMap.Const.getD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := + @DHashMap.Const.getD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + @DHashMap.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := + @DHashMap.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} [Inhabited β] (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := + @DHashMap.Const.get!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := + @DHashMap.getKey?_union _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := + @DHashMap.getKey?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem getKey?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey? k = m₁.getKey? k := + @DHashMap.getKey?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right mem) = m₂.getKey k mem := + @DHashMap.getKey_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h' not_mem) := + @DHashMap.getKey_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h' not_mem) := + @DHashMap.getKey_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := + @DHashMap.getKeyD_union _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback := + @DHashMap.getKeyD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback mem + +theorem getKeyD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + @DHashMap.getKeyD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback mem + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := + @DHashMap.getKey!_union _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := + @DHashMap.getKey!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k mem + +theorem getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := + @DHashMap.getKey!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + @DHashMap.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + @DHashMap.size_left_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + @DHashMap.size_right_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + @DHashMap.size_union_le_size_add_size _ _ _ _ m₁.inner m₂.inner _ _ + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + @DHashMap.isEmpty_union α _ _ _ m₁.inner m₂.inner _ _ + +end Union + -- As `insertManyIfNewUnit` is really an implementation detail for `HashSet.insertMany`, -- we do not add `@[grind]` annotations to any of its lemmas. @@ -2782,5 +2982,5 @@ theorem getKeyD_map [EquivBEq α] [LawfulHashable α] DHashMap.getKeyD_map end map - +attribute [simp] contains_eq_false_iff_not_mem end Std.HashMap diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index d653d8ba60..664275559d 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -228,6 +228,12 @@ instance {m : Type w → Type w'} : ForM m (Raw α β) (α × β) where instance {m : Type w → Type w'} : ForIn m (Raw α β) (α × β) where forIn m init f := m.forIn (fun a b acc => f (a, b) acc) init +/-- Computes the union of the given hash maps, inserting smaller hash map into a bigger hash map. In the case of clashes of keys, entries from the left argument, are replaced with entries from the right argument. -/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := + ⟨DHashMap.Raw.union m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ + section Unverified @[inline, inherit_doc DHashMap.Raw.filterMap] def filterMap {γ : Type w} (f : α → β → Option γ) @@ -263,12 +269,6 @@ m.inner.values [Hashable α] {ρ : Type w} [ForIn Id ρ α] (m : Raw α Unit) (l : ρ) : Raw α Unit := ⟨DHashMap.Raw.Const.insertManyIfNewUnit m.inner l⟩ -/-- Computes the union of the given hash maps, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α β) : Raw α β := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (Raw α β) := ⟨union⟩ - @[inline, inherit_doc DHashMap.Raw.Const.unitOfArray] def unitOfArray [BEq α] [Hashable α] (l : Array α) : Raw α Unit := ⟨DHashMap.Raw.Const.unitOfArray l⟩ @@ -342,6 +342,9 @@ theorem WF.ofList [BEq α] [Hashable α] {l : List (α × β)} : (ofList l).WF : theorem WF.unitOfList [BEq α] [Hashable α] {l : List α} : (unitOfList l).WF := ⟨DHashMap.Raw.WF.Const.unitOfList⟩ +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α β} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂).WF := + ⟨DHashMap.Raw.WF.union h₁.out h₂.out⟩ + end Raw end HashMap diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index ac17d4d2f0..f6a55ceff7 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -77,6 +77,9 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := DHashMap.Raw.contains_iff_mem +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := + DHashMap.Raw.contains_eq_false_iff_not_mem + theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) : m.contains a = m.contains b := DHashMap.Raw.contains_congr h.out hab @@ -1272,6 +1275,216 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := DHashMap.Raw.Const.isEmpty_of_isEmpty_insertMany h.out +section Union + +variable {β : Type v} + +variable (m₁ m₂ : Raw α β) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + @DHashMap.Raw.contains_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + @DHashMap.Raw.mem_union_of_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + @DHashMap.Raw.mem_union_of_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + @DHashMap.Raw.mem_union_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + @DHashMap.Raw.mem_of_mem_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + @DHashMap.Raw.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +/- Equiv -/ +theorem union_insert_right_equiv_union_insert [EquivBEq α] [LawfulHashable α] {p : α × β} + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ (m₂.insert p.fst p.snd)).Equiv ((m₁ ∪ m₂).insert p.fst p.snd) := + ⟨@DHashMap.Raw.union_insert_right_equiv_union_insert _ _ _ _ m₁.inner m₂.inner _ _ ⟨p.fst, p.snd⟩ h₁.out h₂.out⟩ + +theorem get?_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + get? (m₁ ∪ m₂) k = (get? m₂ k).or (get? m₁ k) := + @DHashMap.Raw.Const.get?_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + get? (m₁ ∪ m₂) k = get? m₂ k := + @DHashMap.Raw.Const.get?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + get? (m₁ ∪ m₂) k = get? m₁ k := + @DHashMap.Raw.Const.get?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + get (m₁ ∪ m₂) k (mem_union_of_right h₁ h₂ mem) = get m₂ k mem := + @DHashMap.Raw.Const.get_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + get (m₁ ∪ m₂) k h' = get m₂ k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := + @DHashMap.Raw.Const.get_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + get (m₁ ∪ m₂) k h' = get m₁ k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := + @DHashMap.Raw.Const.get_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {fallback : β} : + getD (m₁ ∪ m₂) k fallback = getD m₂ k (getD m₁ k fallback) := + @DHashMap.Raw.Const.getD_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₁) : + getD (m₁ ∪ m₂) k fallback = getD m₂ k fallback := + @DHashMap.Raw.Const.getD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} {fallback : β} (not_mem : ¬k ∈ m₂) : + getD (m₁ ∪ m₂) k fallback = getD m₁ k fallback := + @DHashMap.Raw.Const.getD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + get! (m₁ ∪ m₂) k = getD m₂ k (get! m₁ k) := + @DHashMap.Raw.Const.get!_union _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem get!_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + get! (m₁ ∪ m₂) k = get! m₂ k := + @DHashMap.Raw.Const.get!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem get!_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] [Inhabited β] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + get! (m₁ ∪ m₂) k = get! m₁ k := + @DHashMap.Raw.Const.get!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- getKey? -/ +theorem getKey?_union [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + (m₁ ∪ m₂).getKey? k = (m₂.getKey? k).or (m₁.getKey? k) := + @DHashMap.Raw.getKey?_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem getKey?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey? k = m₂.getKey? k := + @DHashMap.Raw.getKey?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem getKey?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey? k = m₁.getKey? k := + @DHashMap.Raw.getKey?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- getKey -/ +theorem getKey_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).getKey k (mem_union_of_right h₁ h₂ mem) = m₂.getKey k mem := + @DHashMap.Raw.getKey_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem getKey_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).getKey k h' = m₂.getKey k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := + @DHashMap.Raw.getKey_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +theorem getKey_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).getKey k h' = m₁.getKey k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := + @DHashMap.Raw.getKey_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +/- getKeyD -/ +theorem getKeyD_union [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k (m₁.getKeyD k fallback) := + @DHashMap.Raw.getKeyD_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getKeyD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKeyD k fallback = m₂.getKeyD k fallback := + @DHashMap.Raw.getKeyD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getKeyD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKeyD k fallback = m₁.getKeyD k fallback := + @DHashMap.Raw.getKeyD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- getKey! -/ +theorem getKey!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] + (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).getKey! k = m₂.getKeyD k (m₁.getKey! k) := + @DHashMap.Raw.getKey!_union _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem getKey!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getKey! k = m₂.getKey! k := + @DHashMap.Raw.getKey!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem getKey!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getKey! k = m₁.getKey! k := + @DHashMap.Raw.getKey!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + @DHashMap.Raw.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₁.size ≤ (m₁ ∪ m₂).size := + @DHashMap.Raw.size_left_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₂.size ≤ (m₁ ∪ m₂).size := + @DHashMap.Raw.size_right_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + @DHashMap.Raw.size_union_le_size_add_size _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + @DHashMap.Raw.isEmpty_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +end Union + 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) : @@ -2853,7 +3066,7 @@ theorem getD_map_of_getKey?_eq_some [EquivBEq α] [LawfulHashable α] DHashMap.Raw.Const.getD_map_of_getKey?_eq_some h.out h' end map - +attribute [simp] contains_eq_false_iff_not_mem end Raw end Std.HashMap diff --git a/src/Std/Data/HashSet/Basic.lean b/src/Std/Data/HashSet/Basic.lean index 02f6e67353..f7c29e6fee 100644 --- a/src/Std/Data/HashSet/Basic.lean +++ b/src/Std/Data/HashSet/Basic.lean @@ -235,6 +235,17 @@ appearance. @[inline] def toArray (m : HashSet α) : Array α := m.inner.keysArray +/-- +Computes the union of the given hash sets. + +This function always merges the smaller set into the larger set, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α := + ⟨HashMap.union m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Union (HashSet α) := ⟨union⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ @@ -264,12 +275,6 @@ in the collection will be present in the returned hash set. @[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : HashSet α := ⟨HashMap.unitOfArray l⟩ -/-- Computes the union of the given hash sets, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : HashSet α) : HashSet α := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (HashSet α) := ⟨union⟩ - /-- Returns the number of buckets in the internal representation of the hash set. This function may be useful for things like monitoring system health, but it should be considered an internal diff --git a/src/Std/Data/HashSet/Lemmas.lean b/src/Std/Data/HashSet/Lemmas.lean index da4ce3bf82..5f4c9f10f6 100644 --- a/src/Std/Data/HashSet/Lemmas.lean +++ b/src/Std/Data/HashSet/Lemmas.lean @@ -58,6 +58,10 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := HashMap.contains_iff_mem +-- The following lemma becomes a simp lemma at the bottom of the file. +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := + HashMap.contains_eq_false_iff_not_mem + theorem contains_congr [EquivBEq α] [LawfulHashable α] {a b : α} (hab : a == b) : m.contains a = m.contains b := HashMap.contains_congr hab @@ -748,6 +752,135 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] end +section Union + +variable (m₁ m₂ : HashSet α) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] + {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + @HashMap.contains_union _ _ _ _ m₁.inner m₂.inner _ _ k + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂:= + @HashMap.mem_union_of_left _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂:= + @HashMap.mem_union_of_right _ _ _ _ m₁.inner m₂.inner _ _ k + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).contains k ↔ m₁.contains k ∨ m₂.contains k := + @HashMap.mem_union_iff _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + @HashMap.mem_of_mem_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + @HashMap.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k + +/- getKey? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + @HashMap.getKey?_union _ _ _ _ m₁.inner m₂.inner _ _ k + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := + @HashMap.getKey?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := + @HashMap.getKey?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right mem) = m₂.get k mem := + @HashMap.getKey_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h' not_mem) := + @HashMap.getKey_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h' not_mem) := + @HashMap.getKey_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k not_mem h' + +/- getD -/ +theorem getD_union [EquivBEq α] [LawfulHashable α] {k fallback : α} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + @HashMap.getKeyD_union _ _ _ _ m₁.inner m₂.inner _ _ k fallback + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := + @HashMap.getKeyD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := + @HashMap.getKeyD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ k fallback not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + @HashMap.getKey!_union _ _ _ _ m₁.inner m₂.inner _ _ _ k + +theorem get!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := + @HashMap.getKey!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +theorem get!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := + @HashMap.getKey!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ k not_mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] : + (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + @HashMap.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] : m₁.size ≤ (m₁ ∪ m₂).size := + @HashMap.size_left_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] : + m₂.size ≤ (m₁ ∪ m₂).size := + @HashMap.size_right_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + @HashMap.size_union_le_size_add_size _ _ _ _ m₁.inner m₂.inner _ _ + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + @HashMap.isEmpty_union α _ _ _ m₁.inner m₂.inner _ _ + +end Union + section @[simp, grind =] @@ -1045,5 +1178,5 @@ theorem getD_filter [EquivBEq α] [LawfulHashable α] HashMap.getKeyD_filter_key end filter - +attribute [simp] contains_eq_false_iff_not_mem end Std.HashSet diff --git a/src/Std/Data/HashSet/Raw.lean b/src/Std/Data/HashSet/Raw.lean index 490b2b126b..44ac63d9db 100644 --- a/src/Std/Data/HashSet/Raw.lean +++ b/src/Std/Data/HashSet/Raw.lean @@ -224,6 +224,17 @@ instance {m : Type v → Type w} : ForIn m (Raw α) α where @[inline] def toArray (m : Raw α) : Array α := m.inner.keysArray +/-- +Computes the union of the given hash sets. + +This function always merges the smaller set into the larger set, so the expected runtime is +`O(min(m₁.size, m₂.size))`. +-/ +@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α) : Raw α := + ⟨HashMap.Raw.union m₁.inner m₂.inner⟩ + +instance [BEq α] [Hashable α] : Union (Raw α) := ⟨union⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ @@ -260,12 +271,6 @@ in the collection will be present in the returned hash set. @[inline] def ofArray [BEq α] [Hashable α] (l : Array α) : Raw α := ⟨HashMap.Raw.unitOfArray l⟩ -/-- Computes the union of the given hash sets, by traversing `m₂` and inserting its elements into `m₁`. -/ -@[inline] def union [BEq α] [Hashable α] (m₁ m₂ : Raw α) : Raw α := - m₂.fold (init := m₁) fun acc x => acc.insert x - -instance [BEq α] [Hashable α] : Union (Raw α) := ⟨union⟩ - /-- Returns the number of buckets in the internal representation of the hash set. This function may be useful for things like monitoring system health, but it should be considered an internal @@ -320,6 +325,9 @@ theorem WF.ofList [BEq α] [Hashable α] {l : List α} : (ofList l : Raw α).WF := ⟨HashMap.Raw.WF.unitOfList⟩ +theorem WF.union [BEq α] [Hashable α] {m₁ m₂ : Raw α} (h₁ : m₁.WF) (h₂ : m₂.WF) : (m₁.union m₂).WF := + ⟨HashMap.Raw.WF.union h₁.out h₂.out⟩ + end Raw end HashSet diff --git a/src/Std/Data/HashSet/RawLemmas.lean b/src/Std/Data/HashSet/RawLemmas.lean index 5c6f59c3f0..bad45512b3 100644 --- a/src/Std/Data/HashSet/RawLemmas.lean +++ b/src/Std/Data/HashSet/RawLemmas.lean @@ -76,6 +76,10 @@ theorem mem_iff_contains {a : α} : a ∈ m ↔ m.contains a := theorem contains_iff_mem {a : α} : m.contains a ↔ a ∈ m := HashMap.Raw.contains_iff_mem +-- The following lemma becomes a simp lemma at the bottom of the file. +theorem contains_eq_false_iff_not_mem {k : α} : m.contains k = false ↔ ¬k ∈ m := + HashMap.Raw.contains_eq_false_iff_not_mem + theorem contains_congr [EquivBEq α] [LawfulHashable α] (h : m.WF) {a b : α} (hab : a == b) : m.contains a = m.contains b := HashMap.Raw.contains_congr h.out hab @@ -773,6 +777,149 @@ theorem isEmpty_of_isEmpty_insertMany [EquivBEq α] [LawfulHashable α] (h : m.W {l : ρ} : (insertMany m l).isEmpty → m.isEmpty := HashMap.Raw.isEmpty_of_isEmpty_insertManyIfNewUnit h.out +section Union + +variable (m₁ m₂ : Raw α) + +variable {m₁ m₂} + +@[simp] +theorem union_eq : m₁.union m₂ = m₁ ∪ m₂ := by + simp only [Union.union] + +/- contains -/ +@[simp] +theorem contains_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).contains k = (m₁.contains k || m₂.contains k) := + @HashMap.Raw.contains_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +/- mem -/ +theorem mem_union_of_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ → k ∈ m₁ ∪ m₂ := + @HashMap.Raw.mem_union_of_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_union_of_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₂ → k ∈ m₁ ∪ m₂ := + @HashMap.Raw.mem_union_of_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +@[simp] +theorem mem_union_iff [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ ↔ k ∈ m₁ ∨ k ∈ m₂ := + @HashMap.Raw.mem_union_iff _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_of_mem_union_of_not_mem_right [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₂ → k ∈ m₁ := + @HashMap.Raw.mem_of_mem_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem mem_of_mem_union_of_not_mem_left [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} : + k ∈ m₁ ∪ m₂ → ¬k ∈ m₁ → k ∈ m₂ := + @HashMap.Raw.mem_of_mem_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +/- get? -/ +theorem get?_union [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} : + (m₁ ∪ m₂).get? k = (m₂.get? k).or (m₁.get? k) := + @HashMap.Raw.getKey?_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k + +theorem get?_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get? k = m₂.get? k := + @HashMap.Raw.getKey?_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +theorem get?_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get? k = m₁.get? k := + @HashMap.Raw.getKey?_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem + +/- get -/ +theorem get_union_of_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (mem : k ∈ m₂) : + (m₁ ∪ m₂).get k (mem_union_of_right h₁ h₂ mem) = m₂.get k mem := + @HashMap.Raw.getKey_union_of_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k mem + +theorem get_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₁) {h'} : + (m₁ ∪ m₂).get k h' = m₂.get k (mem_of_mem_union_of_not_mem_left h₁ h₂ h' not_mem) := + @HashMap.Raw.getKey_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +theorem get_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) + {k : α} (not_mem : ¬k ∈ m₂) {h'} : + (m₁ ∪ m₂).get k h' = m₁.get k (mem_of_mem_union_of_not_mem_right h₁ h₂ h' not_mem) := + @HashMap.Raw.getKey_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k not_mem h' + +/- getD -/ +theorem getD_union [EquivBEq α] + [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} : + (m₁ ∪ m₂).getD k fallback = m₂.getD k (m₁.getD k fallback) := + @HashMap.Raw.getKeyD_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback + +theorem getD_union_of_not_mem_left [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).getD k fallback = m₂.getD k fallback := + @HashMap.Raw.getKeyD_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +theorem getD_union_of_not_mem_right [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) {k fallback : α} (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).getD k fallback = m₁.getD k fallback := + @HashMap.Raw.getKeyD_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out k fallback not_mem + +/- get! -/ +theorem get!_union [EquivBEq α] [LawfulHashable α] [Inhabited α] + (h₁ : m₁.WF) + (h₂ : m₂.WF) {k : α} : + (m₁ ∪ m₂).get! k = m₂.getD k (m₁.get! k) := + @HashMap.Raw.getKey!_union _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k + +theorem get!_union_of_not_mem_left [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₁) : + (m₁ ∪ m₂).get! k = m₂.get! k := + @HashMap.Raw.getKey!_union_of_not_mem_left _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +theorem get!_union_of_not_mem_right [Inhabited α] + [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} + (not_mem : ¬k ∈ m₂) : + (m₁ ∪ m₂).get! k = m₁.get! k := + @HashMap.Raw.getKey!_union_of_not_mem_right _ _ _ _ m₁.inner m₂.inner _ _ _ h₁.out h₂.out k not_mem + +/- size -/ +theorem size_union_of_not_mem [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : (∀ (a : α), a ∈ m₁ → ¬a ∈ m₂) → + (m₁ ∪ m₂).size = m₁.size + m₂.size := + @HashMap.Raw.size_union_of_not_mem _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_left_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₁.size ≤ (m₁ ∪ m₂).size := + @HashMap.Raw.size_left_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_right_le_size_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) + (h₂ : m₂.WF) : m₂.size ≤ (m₁ ∪ m₂).size := + @HashMap.Raw.size_right_le_size_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +theorem size_union_le_size_add_size [EquivBEq α] [LawfulHashable α] + (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).size ≤ m₁.size + m₂.size := + @HashMap.Raw.size_union_le_size_add_size _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + +/- isEmpty -/ +@[simp] +theorem isEmpty_union [EquivBEq α] [LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) : + (m₁ ∪ m₂).isEmpty = (m₁.isEmpty && m₂.isEmpty) := + @HashMap.Raw.isEmpty_union _ _ _ _ m₁.inner m₂.inner _ _ h₁.out h₂.out + + +end Union + @[simp, grind =] theorem ofList_nil : ofList ([] : List α) = ∅ := @@ -1053,6 +1200,7 @@ theorem get_filter [EquivBEq α] [LawfulHashable α] end filter +attribute [simp] contains_eq_false_iff_not_mem end Raw end Std.HashSet diff --git a/src/Std/Data/Internal/List/Associative.lean b/src/Std/Data/Internal/List/Associative.lean index 8778fc2f22..db3a15e630 100644 --- a/src/Std/Data/Internal/List/Associative.lean +++ b/src/Std/Data/Internal/List/Associative.lean @@ -2486,7 +2486,7 @@ theorem mem_map_toProd_iff_mem {β : Type v} {k : α} {v : β} {l : List ((_ : exists ⟨k, v⟩ · intro h rcases h with ⟨a, a_l, a_k, a_v⟩ - simp [← a_k, ←a_v, a_l] + simp [← a_k, ← a_v, a_l] theorem mem_iff_getValue?_eq_some [BEq α] [LawfulBEq α] {β : Type v} {k : α} {v : β} {l : List ((_ : α) × β)} (h : DistinctKeys l) : @@ -2785,6 +2785,12 @@ theorem containsKey_insertList [BEq α] [PartialEquivBEq α] {l toInsert : List conv => left; left; rw [Bool.or_comm] rw [Bool.or_assoc] +theorem containsKey_insertList_disj_of_containsKey [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} + {k : α} : containsKey k (List.insertList l toInsert) = + (containsKey k l || containsKey k toInsert) := by + rw [@containsKey_eq_contains_map_fst α β _ _ toInsert k] + simp only [containsKey_insertList, List.contains_map] + theorem containsKey_of_containsKey_insertList [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} (h₁ : containsKey k (insertList l toInsert)) (h₂ : (toInsert.map Sigma.fst).contains k = false) : containsKey k l := by @@ -2815,16 +2821,6 @@ theorem getValueCast?_insertList_of_mem [BEq α] [LawfulBEq α] rw [getEntry?_of_mem distinct_toInsert k_beq mem] at this simp only [this, Option.dmap_some] -theorem getValueCast_insertList_of_contains_eq_false [BEq α] [LawfulBEq α] - {l toInsert : List ((a : α) × β a)} {k : α} - (not_contains : (toInsert.map Sigma.fst).contains k = false) - {h} : - getValueCast k (insertList l toInsert) h = - getValueCast k l (containsKey_of_containsKey_insertList h not_contains) := by - rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast, - getValueCast?_insertList_of_contains_eq_false] - exact not_contains - theorem getValueCast_insertList_of_mem [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} (distinct_l : DistinctKeys l) @@ -2999,6 +2995,452 @@ theorem isEmpty_insertList [BEq α] rw [insertList, List.isEmpty_cons, ih, isEmpty_insertEntry] simp +/-- Internal implementation detail of the hash map -/ +def insertListIfNew [BEq α] (l : List ((a : α) × β a)) (toInsert : List ((a : α) × β a)) : + List ((a : α) × β a) := + match toInsert with + | .nil => l + | .cons ⟨k, v⟩ tl => insertListIfNew (insertEntryIfNew k v l) tl + +theorem DistinctKeys.insertListIfNew [BEq α] [PartialEquivBEq α] {l₁ l₂ : List ((a : α) × β a)} + (h : DistinctKeys l₁) : + DistinctKeys (insertListIfNew l₁ l₂) := by + induction l₂ using assoc_induction generalizing l₁ + · simpa [insertListIfNew] + · rename_i k v t ih + rw [insertListIfNew.eq_def] + exact ih h.insertEntryIfNew + +theorem insertListIfNew_perm_of_perm_first [BEq α] [EquivBEq α] {l1 l2 toInsert : List ((a : α) × β a)} + (h : Perm l1 l2) (distinct : DistinctKeys l1) : + Perm (insertListIfNew l1 toInsert) (insertListIfNew l2 toInsert) := by + induction toInsert generalizing l1 l2 with + | nil => simp [insertListIfNew, h] + | cons hd tl ih => + simp only [insertListIfNew] + apply ih (insertEntryIfNew_of_perm distinct h) (DistinctKeys.insertEntryIfNew distinct) + +theorem containsKey_insertListIfNew [BEq α] [PartialEquivBEq α] {l toInsert : List ((a : α) × β a)} + {k : α} : containsKey k (List.insertListIfNew l toInsert) = + (containsKey k l || (toInsert.map Sigma.fst).contains k) := by + induction toInsert generalizing l with + | nil => simp only [insertListIfNew, List.map_nil, List.elem_nil, Bool.or_false] + | cons hd tl ih => + unfold insertListIfNew + rw [ih] + rw [containsKey_insertEntryIfNew] + simp only [List.map_cons, List.contains_cons] + rw [BEq.comm] + conv => left; left; rw [Bool.or_comm] + rw [Bool.or_assoc] + +/-- Internal implementation detail of the hash map -/ +def insertSmallerList [BEq α] (l₁ l₂ : List ((a : α) × β a)) : List ((a : α) × β a) := + if l₁.length ≤ l₂.length then insertListIfNew l₂ l₁ else insertList l₁ l₂ + +theorem contains_insertList_iff [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} : + containsKey k (insertList l toInsert) = true ↔ containsKey k l = true ∨ containsKey k toInsert = true := by + simp only [containsKey_insertList, Bool.or_eq_true] + simp only [containsKey_eq_contains_map_fst, List.contains_map, List.any_eq_true] + +theorem contains_of_contains_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} + (h₁ : containsKey k (insertList l toInsert) = true) + (h₂ : containsKey k toInsert = false) : containsKey k l = true := by + have := contains_insertList_iff.1 h₁ + simp only [h₂, Bool.false_eq_true, or_false] at this + exact this + +theorem contains_of_contains_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} + (h₁ : containsKey k (insertList l toInsert) = true) + (h₂ : containsKey k l = false) : containsKey k toInsert = true := by + have := contains_insertList_iff.1 h₁ + simpa only [h₂, Bool.false_eq_true, false_or] + +theorem contains_insertList_of_left [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} + (contains : containsKey k l = true) : containsKey k (insertList l toInsert) = true := by + rw [containsKey_insertList, ← containsKey_eq_contains_map_fst] + simp only [contains, Bool.true_or] + +theorem contains_insertList_of_right [BEq α] [EquivBEq α] {l toInsert : List ((a : α) × β a)} {k : α} + (contains : containsKey k toInsert = true) : containsKey k (insertList l toInsert) = true := by + rw [containsKey_insertList, ← containsKey_eq_contains_map_fst] + simp only [contains, Bool.or_true] + + +theorem DistinctKeys_impl_Pairwise_distinct [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} (distinct_l : DistinctKeys l) : + List.Pairwise (fun a b => (a.fst == b.fst) = false) l := by + cases distinct_l + case mk distinct_l => + simp only [keys_eq_map] at distinct_l + apply List.Pairwise.of_map + case p => exact distinct_l + simp only [imp_self, implies_true] + +theorem insertList_perm_of_perm_second [BEq α] [EquivBEq α] {l1 l2 l : List ((a : α) × β a)} + (h : Perm l1 l2) (distinct_l : DistinctKeys l) (distinct : DistinctKeys l1) : + Perm (insertList l l1) (insertList l l2) := by + apply getEntry?_ext + . apply DistinctKeys.insertList distinct_l + . apply DistinctKeys.insertList distinct_l + intro k + rw [@getEntry?_insertList α β _ _ l l1 distinct_l (DistinctKeys_impl_Pairwise_distinct distinct) k] + have distinct' := (DistinctKeys.perm (Perm.symm h) distinct) + rw [@getEntry?_insertList α β _ _ l l2 distinct_l (DistinctKeys_impl_Pairwise_distinct distinct') k] + rw [@getEntry?_of_perm α β _ _ l1 l2 k distinct h] + +theorem getEntry?_insertList_of_contains_left_eq_false [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert) + (not_contains : containsKey k l = false) : + getEntry? k (insertList l toInsert) = getEntry? k toInsert := by + have subgoal : getEntry? k l = none := by + rwa [containsKey_eq_isSome_getEntry?, ← Bool.not_eq_true, Option.not_isSome_iff_eq_none] at not_contains + rw [getEntry?_insertList] + simp only [subgoal, Option.or_none] + . exact distinct_l + . exact distinct_toInsert + +theorem getKey?_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + getKey? k (insertList l toInsert) = (getKey? k toInsert).or (getKey? k l) := by + simp only [getKey?_eq_getEntry?] + rw [getEntry?_insertList] + . simp only [Option.map_or] + . exact distinct_l + . exact DistinctKeys_impl_Pairwise_distinct distinct_toInsert + +theorem getKey_insertList_of_contains_right [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) + {m} : (contains : containsKey k toInsert = true) → + getKey k (insertList l toInsert) m = getKey k toInsert contains := by + intro contains + unfold getKey + have get_is_some : (getKey? k (insertList l toInsert)).isSome = true := by + simp only [getKey?_eq_getEntry?, Option.isSome_map] + simp only [←@containsKey_eq_isSome_getEntry? α β _ (insertList l toInsert) k, m] + apply Option.get_congr + . rw [@getKey?_insertList α β _ _ l toInsert k distinct_l distinct_toInsert] + apply Option.or_of_isSome + . simp only [getKey?_eq_getEntry?, Option.isSome_map] + simp only [←@containsKey_eq_isSome_getEntry? α β _ toInsert k, contains] + +theorem getKeyD_insertList_of_contains_right [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k fallback : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + containsKey k toInsert → + getKeyD k (insertList l toInsert) fallback = getKeyD k toInsert fallback := by + intro contains + simp only [getKeyD_eq_getKey?] + rw [@getKey?_insertList _ _ _ _ l toInsert k distinct_l distinct_toInsert] + rw [@getKey?_eq_some_getKey _ _ _ toInsert k contains] + simp only [Option.some_or, Option.getD_some] + +theorem getKey!_insertList_of_contains_right_eq_false [Inhabited α] [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (not_contains: containsKey k toInsert = false) : + getKey! k (insertList l toInsert) = getKey! k l := by + simp only [getKey!_eq_getKey?] + congr 1 + simp only [getKey?_eq_getEntry?] + congr 1 + simp [getEntry?_insertList_of_contains_eq_false not_contains] + +theorem getKey?_insertList_of_contains_eq_false_right [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (not_contains : containsKey k toInsert = false) : + List.getKey? k (insertList l toInsert) = + List.getKey? k l := by + rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?] + congr 1 + apply getEntry?_insertList_of_contains_eq_false not_contains + +theorem getKey?_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) + (not_contains : containsKey k l = false) : + List.getKey? k (insertList l toInsert) = + List.getKey? k toInsert := by + rw [getKey?_eq_getEntry?, getKey?_eq_getEntry?] + congr 1 + apply getEntry?_insertList_of_contains_left_eq_false distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) not_contains + +theorem getKey_insertList_of_contains_left_of_contains_right_eq_false [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} {m} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + (mem : containsKey k l) → + (∃ (mem₂ : containsKey k toInsert), getKey k (insertList l toInsert) m = getKey k toInsert mem₂) + ∨ getKey k (insertList l toInsert) m = getKey k l mem := by + intro mem + apply Or.elim <| Classical.em <| containsKey k toInsert = true + case left => + intro toInsert_contains_k + apply Or.inl + refine ⟨toInsert_contains_k, ?_⟩ + apply getKey_insertList_of_contains_right + . exact distinct_l + . exact distinct_toInsert + case right => + intro toInsert_not_contains_k + apply Or.inr + suffices some (getKey k (insertList l toInsert) m) = some (getKey k l mem) from by + injection this + simp only [← getKey?_eq_some_getKey] + rw [@List.getKey?_insertList_of_contains_eq_false_right α β _ _ l toInsert k (by simp only [toInsert_not_contains_k])] + +theorem getKeyD_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k fallback : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + getKeyD k (insertList l toInsert) fallback = getKeyD k toInsert (getKeyD k l fallback) := by + simp only [getKeyD_eq_getKey?] + 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 α] + {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 + simp only [getKeyD_eq_getKey?] + congr 1 + simp only [getKey?_eq_getEntry?] + congr 1 + apply getEntry?_insertList_of_contains_eq_false + . exact not_contains + +theorem List.getKeyD_insertList_of_contains_eq_false_left [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} {k fallback : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) + (not_contains: containsKey k l = false) : + List.getKeyD k (insertList l toInsert) fallback = List.getKeyD k toInsert fallback := by + simp only [getKeyD_eq_getKey?] + congr 1 + simp only [getKey?_eq_getEntry?] + congr 1 + apply getEntry?_insertList_of_contains_left_eq_false + . exact distinct_l + . exact DistinctKeys_impl_Pairwise_distinct distinct_toInsert + . exact not_contains + +theorem getKey!_insertList_of_contains_left_eq_false [BEq α] [EquivBEq α] [Inhabited α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + (containsKey k l = false) → + getKey! k (insertList l toInsert) = getKey! k toInsert := by + have distinct_toInsert_equiv : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert := by + cases distinct_toInsert + case mk distinct_toInsert => + simp only [keys_eq_map] at distinct_toInsert + apply List.Pairwise.of_map + case p => exact distinct_toInsert + simp only [imp_self, implies_true] + intro not_contains + simp only [getKey!_eq_getKey?] + congr 1 + simp only [getKey?_eq_getEntry?] + congr 1 + apply getEntry?_insertList_of_contains_left_eq_false + . exact distinct_l + . exact distinct_toInsert_equiv + . exact not_contains + +theorem getValueCast?_insertList_of_contains_eq_false_left [BEq α] [LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : (containsKey k l = false) → + getValueCast? k (insertList l toInsert) = getValueCast? k toInsert := by + intro not_contains + rw [getValueCast?_eq_getEntry?, getValueCast?_eq_getEntry?] + have := @getEntry?_insertList_of_contains_left_eq_false α β _ _ l toInsert k distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) not_contains + simp only [this] + +theorem getValueCast?_of_insertList [BEq α] [LawfulBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : + getValueCast? k (insertList l toInsert) = (getValueCast? k toInsert).or (getValueCast? k l) := by + apply Or.elim <| Classical.em <| (containsKey k toInsert) + case left => + intro contains + rw [@getValueCast?_eq_some_getValueCast α β _ _ toInsert k contains] + rw [Option.some_or] + simp [← getValueCast?_eq_some_getValueCast] + simp [getValueCast?_eq_getEntry?] + apply Option.dmap_congr + . simp only [implies_true] + . rw [@getEntry?_insertList α β _ _ l toInsert distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) k] + rw [containsKey_eq_isSome_getEntry?] at contains + rw [Option.eq_some_of_isSome contains] + simp only [Option.some_or] + case right => + intro not_contains + simp only [Bool.not_eq_true] at not_contains + rw [@List.getValueCast?_eq_none α β _ _ toInsert k not_contains, Option.none_or] + apply getValueCast?_insertList_of_contains_eq_false + . rw [← containsKey_eq_contains_map_fst] + exact not_contains + +theorem getValueCastD_of_insertList [BEq α] [LawfulBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} {fallback : β k} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : + getValueCastD k (insertList l toInsert) fallback = getValueCastD k toInsert (getValueCastD k l fallback) := by + rw [getValueCastD_eq_getValueCast?] + have getOr := @getValueCast?_of_insertList α β _ _ l toInsert k distinct_l distinct_toInsert + 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 : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) + (contains : containsKey k (insertList l toInsert)) + (not_contains: containsKey k l = false) : + getValueCast k (insertList l toInsert) contains = getValueCast k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains) := by + suffices h : some (getValueCast k (insertList l toInsert) contains) = some (getValueCast k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains)) from by + injection h + 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 : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) + (contains : containsKey k (insertList l toInsert)) + (not_contains: containsKey k l = false) : + getKey k (insertList l toInsert) contains = getKey k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains) := by + suffices h : some (getKey k (insertList l toInsert) contains) = some (getKey k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains)) from by + injection h + 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 : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) + (contains : containsKey k toInsert) {h} : + getValueCast k (insertList l toInsert) h = getValueCast k toInsert contains := by + suffices h : some (getValueCast k (insertList l toInsert) h) = some (getValueCast k toInsert contains) from by + injection h + simp only [← getValueCast?_eq_some_getValueCast] + simp only [getValueCast?_eq_getEntry?] + suffices getEntry? k (insertList l toInsert) = getEntry? k toInsert from by simp [this] + rw [@getEntry?_insertList α β _ _ l toInsert distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) k] + 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} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) + (not_contains: containsKey k l = false) : + getValueCastD k (insertList l toInsert) fallback = getValueCastD k toInsert fallback := by + simp only [getValueCastD_eq_getValueCast?] + congr 1 + exact getValueCast?_insertList_of_contains_eq_false_left distinct_l distinct_toInsert not_contains + +theorem length_insertList_distinct [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + (∀ (a : α), containsKey a l → containsKey a toInsert = false) → + (insertList l toInsert).length = l.length + toInsert.length := by + replace distinct_toInsert := DistinctKeys_impl_Pairwise_distinct distinct_toInsert + intro distinct_keys + have subgoal2 : ∀ (a : α), containsKey a l = true → (List.map Sigma.fst toInsert).contains a = false := by + intro a h_contains + specialize distinct_keys a h_contains + rwa [containsKey_eq_contains_map_fst] at distinct_keys + apply length_insertList distinct_l distinct_toInsert subgoal2 + +theorem getKey?_insertList_of_mem_of_not_mem [BEq α] [LawfulBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (contains : containsKey k l) + (not_contains : containsKey k toInsert = false) : + List.getKey? k (insertList l toInsert) = some k := by + simp only [List.getKey?_insertList_of_contains_eq_false_right not_contains, getKey?_eq_some contains] + +theorem _root_.Option.or_eq_left_of_isSome {o o' : Option α} : o.isSome = true → o.or o' = o := by + cases o <;> simp + +theorem insertListIfNew_perm_insertList [BEq α] [EquivBEq α] {l₁ l₂ : List ((a : α) × β a)} + (hd₁ : DistinctKeys l₁) (hd₂ : DistinctKeys l₂) : + List.Perm (insertListIfNew l₁ l₂) (insertList l₂ l₁) := by + induction l₂ using assoc_induction generalizing l₁ with + | nil => + simp only [insertListIfNew] + exact Perm.trans (by simp) (perm_insertList hd₂ (pairwise_fst_eq_false hd₁) (by simp)).symm + | cons k v l ih => + simp only [insertListIfNew] + refine Perm.trans (ih hd₁.insertEntryIfNew hd₂.tail) ?_ + refine getEntry?_ext hd₂.tail.insertList hd₂.insertList (fun k' => ?_) + rw [getEntry?_insertList hd₂.tail (pairwise_fst_eq_false hd₁.insertEntryIfNew), + getEntry?_insertList hd₂ (pairwise_fst_eq_false hd₁), getEntry?_insertEntryIfNew] + simp only [Bool.and_eq_true, Bool.not_eq_eq_eq_not, Bool.not_true] + split + · rename_i h + rw [Option.some_or, Option.or_eq_right_of_none, getEntry?_cons_of_true h.1] + rw [← getEntry?_congr h.1, getEntry?_eq_none, h.2] + · rename_i h + rw [getEntry?_cons] + by_cases hk : k == k' + · simp only [hk, true_and, Bool.not_eq_false] at h + suffices (getEntry? k' l₁).isSome by simp [Option.or_eq_left_of_isSome this] + rwa [← containsKey_eq_isSome_getEntry?, ← containsKey_congr hk] + · simp [hk] + +theorem insertList_perm_insertSmallerList [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + (insertList l toInsert).Perm + (insertSmallerList l toInsert) := by + unfold insertSmallerList + split + . apply Perm.symm + . apply insertListIfNew_perm_insertList distinct_toInsert distinct_l + . apply Perm.refl + +theorem length_left_le_length_insertListIfNew [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} : + l.length ≤ (insertListIfNew l toInsert).length := by + induction toInsert generalizing l with + | nil => apply Nat.le_refl + | cons hd tl ih => exact Nat.le_trans length_le_length_insertEntryIfNew ih + +theorem length_right_le_length_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + toInsert.length ≤ (List.insertList l toInsert).length := by + apply Nat.le_trans + case m => exact (insertListIfNew toInsert l).length + . apply length_left_le_length_insertListIfNew + . apply Nat.le_of_eq + . apply Perm.length_eq + . exact @insertListIfNew_perm_insertList α β _ _ toInsert l distinct_toInsert distinct_l + +theorem insertList_insertEntry_right_equiv_insertEntry_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((a : α) × β a)} (p : (a : α) × β a) + (distinct_l : DistinctKeys l) + (distinct_toInsert : DistinctKeys toInsert) : + (insertList l (insertEntry p.fst p.snd toInsert)).Perm + (insertEntry p.fst p.snd (insertList l toInsert)) := by + apply getEntry?_ext (DistinctKeys.insertList distinct_l) + <| DistinctKeys.insertEntry + <| DistinctKeys.insertList distinct_l + intro a + have distinct_toInsert_pairwise := DistinctKeys_impl_Pairwise_distinct <| @DistinctKeys.insertEntry α β _ _ toInsert p.fst p.snd distinct_toInsert + simp only [@getEntry?_insertList α β _ _ l (insertEntry p.fst p.snd toInsert) distinct_l distinct_toInsert_pairwise a, + getEntry?_insertEntry] + split + . simp only [Option.some_or] + . rw [@getEntry?_insertList α β _ _ l toInsert distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) a] + section variable {β : Type v} @@ -3149,6 +3591,98 @@ 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 α] + {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 α] + {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} + (not_contains : containsKey k toInsert = false) : + getValueD k (insertList l toInsert) fallback = getValueD k l fallback := by + simp only [getValueD_eq_getValue?] + congr 1 + exact getValue?_insertList_of_contains_eq_false_right not_contains + +theorem List.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} + {p2 : containsKey k l = true} : + getValue k (insertList l toInsert) p1 = getValue k l p2 := by + 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 + +theorem List.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 + intro not_contains + simp only [getValue?_eq_getEntry?] + 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 : β} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : (containsKey k l = false) → + getValueD k (insertList l toInsert) fallback = getValueD k toInsert fallback := by + intro not_contains + simp only [getValueD_eq_getValue?] + congr 1 + exact getValue?_insertList_of_contains_eq_false_left distinct_l distinct_toInsert not_contains + +theorem List.getValue?_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((_ : α) × β)} {k : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : + getValue? k (insertList l toInsert) = (getValue? k toInsert).or (getValue? k l) := by + simp only [getValue?_eq_getEntry?] + simp only [← Option.map_or] + congr 1 + apply getEntry?_insertList distinct_l (DistinctKeys_impl_Pairwise_distinct distinct_toInsert) + +theorem getValueD_insertList [BEq α] [EquivBEq α] + {l toInsert : List ((_ : α) × β)} {k : α} {fallback : β} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) : + getValueD k (insertList l toInsert) fallback = getValueD k toInsert (getValueD k l fallback) := by + simp only [getValueD_eq_getValue?] + simp only [← Option.getD_or] + congr 1 + apply List.getValue?_insertList distinct_l distinct_toInsert + +theorem List.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)) + (not_contains: containsKey k l = false) : + getValue k (insertList l toInsert) contains = getValue k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains) := by + suffices some (getValue k (insertList l toInsert) contains) = some (getValue k toInsert (contains_of_contains_insertList_of_contains_eq_false_left contains not_contains)) from by + injection this + simp only [← getValue?_eq_some_getValue] + simp only [ getValue?_eq_getEntry? ] + 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 : α} + (distinct_l : DistinctKeys l) + (distinct_toInsert: DistinctKeys toInsert) + (contains : containsKey k toInsert) {h} : + getValue k (insertList l toInsert) h = getValue k toInsert contains := by + suffices some (getValue k (insertList l toInsert) h) = some (getValue k toInsert contains) from by + injection this + simp only [← getValue?_eq_some_getValue] + simp only [ getValue?_eq_getEntry? ] + congr 1 + apply getEntry?_insertList_of_contains_eq_true + . exact distinct_l + . exact DistinctKeys_impl_Pairwise_distinct distinct_toInsert + . exact contains + theorem getValue?_insertListConst_of_mem [BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {toInsert : List (α × β)} (distinct_l : DistinctKeys l) @@ -3399,7 +3933,7 @@ theorem getKey!_insertListIfNewUnit_of_contains [BEq α] [EquivBEq α] [Inhabite {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α} (h : containsKey k l = true) : - getKey! k (insertListIfNewUnit l toInsert) = getKey! k l := by + getKey! k (insertListIfNewUnit l toInsert) = getKey! k l := by rw [getKey!_eq_getKey?, getKey?_insertListIfNewUnit_of_contains h, getKey!_eq_getKey?] theorem getKeyD_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α] @@ -4304,7 +4838,7 @@ theorem containsKey_modifyKey [EquivBEq α] (k k': α) (f : β → β) (l : List theorem getValue?_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) (hl : DistinctKeys l) : - getValue? k' (modifyKey k f l) = + getValue? k' (modifyKey k f l) = if k == k' then (getValue? k l).map f else @@ -4483,7 +5017,7 @@ private theorem Option.get_dmap {α β : Type _} {x : Option α} {f : (a : α) cases x <;> trivial theorem guard_eq_map (p : (a : α) × β a → Prop) [DecidablePred p] : - Option.guard p = fun x => Option.map (fun y => ⟨x.1, y⟩) (if p x then some x.2 else none) := by + Option.guard p = fun x => Option.map (fun y => ⟨x.1, y⟩) (if p x then some x.2 else none) := by funext x simp [Option.guard] @@ -4704,7 +5238,7 @@ theorem getValueCast!_filterMap [BEq α] [LawfulBEq α] theorem getValueCastD_filterMap [BEq α] [LawfulBEq α] {f : (a : α) → β a → Option (γ a)} - {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k}: + {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k} : getValueCastD k (l.filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) fallback = ((getValueCast? k l).bind (f k)).getD fallback := by simp [getValueCastD_eq_getValueCast?, getValueCast?_filterMap hl] @@ -4731,7 +5265,7 @@ theorem getValueCast!_filter [BEq α] [LawfulBEq α] theorem getValueCastD_filter [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} - {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : β k}: + {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : β k} : getValueCastD k (l.filter fun p => f p.1 p.2) fallback = ((getValueCast? k l).filter (f k)).getD fallback := by simp [getValueCastD_eq_getValueCast?, getValueCast?_filter hl] @@ -4756,7 +5290,7 @@ theorem getValueCast!_map [BEq α] [LawfulBEq α] theorem getValueCastD_map [BEq α] [LawfulBEq α] {f : (a : α) → β a → γ a} - {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k}: + {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) {fallback : γ k} : getValueCastD k (l.map fun p => ⟨p.1, f p.1 p.2⟩) fallback = ((getValueCast? k l).map (f k)).getD fallback := by simp [getValueCastD_eq_getValueCast?, getValueCast?_map hl] @@ -4880,6 +5414,16 @@ theorem getValueCast_eq_get_getValueCast? [BEq α] [LawfulBEq α] {a : α} {l : getValueCast a l h = (getValueCast? a l).get (containsKey_eq_isSome_getValueCast? (a := a) ▸ h) := by simp [getValueCast?_eq_some_getValueCast h] +theorem getValueCast_insertList_of_contains_eq_false [BEq α] [LawfulBEq α] + {l toInsert : List ((a : α) × β a)} {k : α} + (not_contains : (toInsert.map Sigma.fst).contains k = false) + {h} : + getValueCast k (insertList l toInsert) h = + getValueCast k l (containsKey_of_containsKey_insertList h not_contains) := by + rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast, ← getValueCast?_eq_some_getValueCast, + getValueCast?_insertList_of_contains_eq_false] + exact not_contains + theorem getKey?_filter [BEq α] [LawfulBEq α] {f : (a : α) → β a → Bool} {l : List ((a : α) × β a)} {k : α} (hl : DistinctKeys l) : @@ -5222,7 +5766,7 @@ theorem getValueD_filterMap {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] { theorem getValueD_filterMap_of_getKey?_eq_some {β : Type v} {γ : Type w} [BEq α] [EquivBEq α] {f : (_ : α) → β → Option γ} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) - {k k' : α} {fallback : γ}: + {k k' : α} {fallback : γ} : getKey? k l = some k' → getValueD k (l.filterMap fun p => (f p.1 p.2).map (fun x => (⟨p.1, x⟩ : (_ : α) × γ))) fallback = ((getValue? k l).bind (fun x => f k' x)).getD fallback := by @@ -5415,7 +5959,7 @@ theorem length_filter_eq_length_iff {β : Type v} [BEq α] [EquivBEq α] theorem length_filter_key_eq_length_iff {β : Type v} [BEq α] [EquivBEq α] {f : (_ : α) → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) : (l.filter fun p => f p.1).length = l.length ↔ - ∀ (a : α) (h : containsKey a l), f (getKey a l h) = true := by + ∀ (a : α) (h : containsKey a l), f (getKey a l h) = true := by simp [← List.filterMap_eq_filter, forall_mem_iff_forall_contains_getKey_getValue (p := fun a b => f a = true) distinct] @@ -5456,7 +6000,7 @@ theorem isEmpty_filter_key_eq_true [BEq α] [EquivBEq α] {β : Type v} theorem isEmpty_filter_key_eq_false [BEq α] [EquivBEq α] {β : Type v} {f : (_ : α) → Bool} {l : List ((_ : α) × β)} (distinct : DistinctKeys l) : (l.filter fun p => (f p.1)).isEmpty = false ↔ - ∃ (k : α) (h : containsKey k l = true), f (getKey k l h) = true := + ∃ (k : α) (h : containsKey k l = true), f (getKey k l h) = true := isEmpty_filter_eq_false (f := fun a _ => f a) distinct theorem toList_map' {β : Type v} {γ : Type w} {f : (_ : α) → β → γ} {l : List ((_ : α) × β)} : @@ -6233,7 +6777,7 @@ theorem minKey_eq_head_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] theorem minKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} : - (modifyKey k f l |> minKey <| he) = minKey l (isEmpty_modifyKey k f l ▸ he):= by + (modifyKey k f l |> minKey <| he) = minKey l (isEmpty_modifyKey k f l ▸ he) := by simp [minKey_eq_get_minKey?, minKey?_modifyKey hd] theorem minKey_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] @@ -7092,7 +7636,7 @@ theorem maxKey_eq_getLast_keys [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] theorem maxKey_modifyKey [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [LawfulEqOrd α] {k f} {l : List ((a : α) × β a)} (hd : DistinctKeys l) {he} : - (modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he):= + (modifyKey k f l |> maxKey <| he) = maxKey l (isEmpty_modifyKey k f l ▸ he) := letI : Ord α := .opposite inferInstance minKey_modifyKey hd @@ -7342,7 +7886,7 @@ theorem maxKey!_modifyKey_beq [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] minKey!_modifyKey_beq hd theorem maxKey!_alterKey_eq_self [Ord α] [TransOrd α] [BEq α] [LawfulBEqOrd α] [Inhabited α] - {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (alterKey k f l).isEmpty = false): + {l : List ((_ : α) × β)} (hd : DistinctKeys l) {k f} (he : (alterKey k f l).isEmpty = false) : (alterKey k f l |> maxKey!) = k ↔ (f (getValue? k l)).isSome ∧ ∀ k', containsKey k' l → (compare k' k).isLE := letI : Ord α := .opposite inferInstance