From 3243dc595cde44453e7b72ebf2208e2fbe90fb10 Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Tue, 14 Jan 2025 08:47:58 +0100 Subject: [PATCH] feat: faster, linear HashMap.alter and modify (#6573) This PR replaces the existing implementations of `(D)HashMap.alter` and `(D)HashMap.modify` with primitive, more efficient ones and in particular provides proofs that they yield well-formed hash maps (`WF` typeclass). --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> --- src/Std/Data/DHashMap/Basic.lean | 31 +- .../DHashMap/Internal/AssocList/Basic.lean | 57 +++ .../DHashMap/Internal/AssocList/Lemmas.lean | 39 ++ src/Std/Data/DHashMap/Internal/Defs.lean | 66 ++++ .../DHashMap/Internal/List/Associative.lean | 346 +++++++++++++++++- src/Std/Data/DHashMap/Internal/Model.lean | 118 +++++- src/Std/Data/DHashMap/Internal/WF.lean | 239 +++++++++++- src/Std/Data/DHashMap/Raw.lean | 16 + src/Std/Data/HashMap/Basic.lean | 22 +- 9 files changed, 889 insertions(+), 45 deletions(-) diff --git a/src/Std/Data/DHashMap/Basic.lean b/src/Std/Data/DHashMap/Basic.lean index 8ddbfd80216a..2c78504a9007 100644 --- a/src/Std/Data/DHashMap/Basic.lean +++ b/src/Std/Data/DHashMap/Basic.lean @@ -251,34 +251,27 @@ instance [BEq α] [Hashable α] : ForIn m (DHashMap α β) ((a : α) × β a) wh Modifies in place the value associated with a given key. This function ensures that the value is used linearly. -It is currently implemented in terms of `get?`, `erase`, and `insert`, -but will later become a primitive operation. -(It is provided already to help avoid non-linear code.) -/ @[inline] def modify [LawfulBEq α] (m : DHashMap α β) (a : α) (f : β a → β a) : DHashMap α β := - match m.get? a with - | none => m - | some b => m.erase a |>.insert a (f b) + ⟨Raw₀.modify ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.modify₀ m.2⟩ + +@[inline, inherit_doc DHashMap.modify] def Const.modify {β : Type v} (m : DHashMap α (fun _ => β)) + (a : α) (f : β → β) : DHashMap α (fun _ => β) := + ⟨Raw₀.Const.modify ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.constModify₀ m.2⟩ /-- Modifies in place the value associated with a given key, allowing creating new values and deleting values via an `Option` valued replacement function. This function ensures that the value is used linearly. -It is currently implemented in terms of `get?`, `erase`, and `insert`, -but will later become a primitive operation. -(It is provided already to help avoid non-linear code.) -/ -@[inline] def alter [LawfulBEq α] (m : DHashMap α β) (a : α) (f : Option (β a) → Option (β a)) : DHashMap α β := - match m.get? a with - | none => - match f none with - | none => m - | some b => m.insert a b - | some b => - match f (some b) with - | none => m.erase a - | some b => m.erase a |>.insert a b +@[inline] def alter [LawfulBEq α] (m : DHashMap α β) + (a : α) (f : Option (β a) → Option (β a)) : DHashMap α β := + ⟨Raw₀.alter ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.alter₀ m.2⟩ + +@[inline, inherit_doc DHashMap.alter] def Const.alter {β : Type v} + (m : DHashMap α (fun _ => β)) (a : α) (f : Option β → Option β) : DHashMap α (fun _ => β) := + ⟨Raw₀.Const.alter ⟨m.1, m.2.size_buckets_pos⟩ a f, Raw.WF.constAlter₀ m.2⟩ @[inline, inherit_doc Raw.insertMany] def insertMany {ρ : Type w} [ForIn Id ρ ((a : α) × β a)] (m : DHashMap α β) (l : ρ) : DHashMap α β := diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean index 67056dbda3f1..821f923e0542 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Basic.lean @@ -169,6 +169,63 @@ def erase [BEq α] (a : α) : AssocList α β → AssocList α β | nil => nil | cons k v l => bif k == a then l else cons k v (l.erase a) +/-- Internal implementation detail of the hash map -/ +def modify [BEq α] [LawfulBEq α] (a : α) (f : β a → β a) : + AssocList α β → AssocList α β + | nil => nil + | cons k v l => + if h : k == a then + have h' : k = a := eq_of_beq h + let b := f (cast (congrArg β h') v) + cons a b l + else + cons k v (modify a f l) + +/-- Internal implementation detail of the hash map -/ +def alter [BEq α] [LawfulBEq α] (a : α) (f : Option (β a) → Option (β a)) : + AssocList α β → AssocList α β + | nil => match f none with + | none => nil + | some b => cons a b nil + | cons k v l => + if h : k == a then + have h' : k = a := eq_of_beq h + match f (some (cast (congrArg β h') v)) with + | none => l + | some b => cons a b l + else + let tail := alter a f l + cons k v tail + +namespace Const + +/-- Internal implementation detail of the hash map -/ +def modify [BEq α] {β : Type v} (a : α) (f : β → β) : + AssocList α (fun _ => β) → AssocList α (fun _ => β) + | nil => nil + | cons k v l => + if k == a then + cons a (f v) l + else + cons k v (modify a f l) + +/-- Internal implementation detail of the hash map -/ +def alter [BEq α] {β : Type v} (a : α) (f : Option β → Option β) : + AssocList α (fun _ => β) → AssocList α (fun _ => β) + | nil => match f none with + | none => nil + | some b => AssocList.cons a b nil + | cons k v l => + if k == a then + match f v with + | none => l + | some b => cons a b l + else + let tail := alter a f l + cons k v tail + +end Const + /-- Internal implementation detail of the hash map -/ @[inline] def filterMap (f : (a : α) → β a → Option (γ a)) : AssocList α β → AssocList α γ := diff --git a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean index e93eeea4ddad..e4cc4bdfa4fd 100644 --- a/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean +++ b/src/Std/Data/DHashMap/Internal/AssocList/Lemmas.lean @@ -199,6 +199,45 @@ theorem toList_filter {f : (a : α) → β a → Bool} {l : AssocList α β} : · exact (ih _).trans (by simpa using perm_middle.symm) · exact ih _ +theorem toList_alter [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} + {l : AssocList α β} : + Perm (l.alter a f).toList (alterKey a f l.toList) := by + induction l + · simp only [alter, toList_nil, alterKey_nil] + split <;> simp_all + · rw [toList] + refine Perm.trans ?_ alterKey_cons_perm.symm + rw [alter] + split <;> (try split) <;> simp_all + +theorem modify_eq_alter [BEq α] [LawfulBEq α] {a : α} {f : β a → β a} {l : AssocList α β} : + modify a f l = alter a (·.map f) l := by + induction l + · rfl + · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih] + +namespace Const + +variable {β : Type v} + +theorem toList_alter [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} + {l : AssocList α (fun _ => β)} : Perm (alter a f l).toList (Const.alterKey a f l.toList) := by + induction l + · simp only [alter, toList_nil, alterKey_nil] + split <;> simp_all + · rw [toList] + refine Perm.trans ?_ Const.alterKey_cons_perm.symm + rw [alter] + split <;> (try split) <;> simp_all + +theorem modify_eq_alter [BEq α] [EquivBEq α] {a : α} {f : β → β} {l : AssocList α (fun _ => β)} : + modify a f l = alter a (·.map f) l := by + induction l + · rfl + · next ih => simp only [modify, beq_iff_eq, alter, Option.map_some', ih] + +end Const + theorem foldl_apply {l : AssocList α β} {acc : List δ} (f : (a : α) → β a → δ) : l.foldl (fun acc k v => f k v :: acc) acc = (l.toList.map (fun p => f p.1 p.2)).reverse ++ acc := by diff --git a/src/Std/Data/DHashMap/Internal/Defs.lean b/src/Std/Data/DHashMap/Internal/Defs.lean index e4a03ce53ee8..aaafacb82405 100644 --- a/src/Std/Data/DHashMap/Internal/Defs.lean +++ b/src/Std/Data/DHashMap/Internal/Defs.lean @@ -226,6 +226,72 @@ where let buckets' := buckets.uset i (AssocList.cons a b bkt) h expandIfNecessary ⟨⟨size', buckets'⟩, by simpa [buckets']⟩ +/-- Internal implementation detail of the hash map -/ +@[inline] def modify [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) (f : β a → β a) : + Raw₀ α β := + let ⟨⟨size, buckets⟩, hm⟩ := m + let size' := size + let ⟨i, hi⟩ := mkIdx buckets.size hm (hash a) + let bucket := buckets[i] + if bucket.contains a then + let buckets := buckets.uset i .nil hi + let bucket := bucket.modify a f + ⟨⟨size, buckets.uset i bucket (by simpa [buckets])⟩, (by simpa [buckets])⟩ + else + m + +/-- Internal implementation detail of the hash map -/ +@[inline] def Const.modify [BEq α] {β : Type v} [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) + (f : β → β) : Raw₀ α (fun _ => β) := + let ⟨⟨size, buckets⟩, hm⟩ := m + let size' := size + let ⟨i, hi⟩ := mkIdx buckets.size hm (hash a) + let bucket := buckets[i] + if bucket.contains a then + let buckets := buckets.uset i .nil hi + let bucket := AssocList.Const.modify a f bucket + ⟨⟨size, buckets.uset i bucket (by simpa [buckets])⟩, (by simpa [buckets])⟩ + else + m + +/-- Internal implementation detail of the hash map -/ +@[inline] def alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) + (f : Option (β a) → Option (β a)) : Raw₀ α β := + let ⟨⟨size, buckets⟩, hm⟩ := m + let ⟨i, h⟩ := mkIdx buckets.size hm (hash a) + let bkt := buckets[i] + if bkt.contains a then + let buckets' := buckets.uset i .nil h + let bkt' := bkt.alter a f + let size' := if bkt'.contains a then size else size - 1 + ⟨⟨size', buckets'.uset i bkt' (by simpa [buckets'])⟩, by simpa [buckets']⟩ + else + match f none with + | none => m + | some b => + let size' := size + 1 + let buckets' := buckets.uset i (.cons a b bkt) h + expandIfNecessary ⟨⟨size', buckets'⟩, by simpa [buckets']⟩ + +/-- Internal implementation detail of the hash map -/ +@[inline] def Const.alter [BEq α] [Hashable α] {β : Type v} (m : Raw₀ α (fun _ => β)) (a : α) + (f : Option β → Option β) : Raw₀ α (fun _ => β) := + let ⟨⟨size, buckets⟩, hm⟩ := m + let ⟨i, h⟩ := mkIdx buckets.size hm (hash a) + let bkt := buckets[i] + if bkt.contains a then + let buckets' := buckets.uset i .nil h + let bkt' := AssocList.Const.alter a f bkt + let size' := if bkt'.contains a then size else size - 1 + ⟨⟨size', buckets'.uset i bkt' (by simpa [buckets'])⟩, by simpa [buckets']⟩ + else + match f none with + | none => m + | some b => + let size' := size + 1 + let buckets' := buckets.uset i (.cons a b bkt) h + expandIfNecessary ⟨⟨size', buckets'⟩, by simpa [buckets']⟩ + /-- Internal implementation detail of the hash map -/ @[inline] def containsThenInsert [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : Bool × Raw₀ α β := diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index 97bbaf230ace..d262cd88e291 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -775,6 +775,7 @@ def eraseKey [BEq α] (k : α) : List ((a : α) × β a) → List ((a : α) × | ⟨k', v'⟩ :: l => bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l @[simp] theorem eraseKey_nil [BEq α] {k : α} : eraseKey k ([] : List ((a : α) × β a)) = [] := rfl + theorem eraseKey_cons [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v' : β k'} : eraseKey k (⟨k', v'⟩ :: l) = bif k' == k then l else ⟨k', v'⟩ :: eraseKey k l := rfl @@ -849,10 +850,10 @@ theorem isEmpty_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : theorem keys_eq_map (l : List ((a : α) × β a)) : keys l = l.map (·.1) := by induction l using assoc_induction <;> simp_all -theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length := by +theorem length_keys_eq_length (l : List ((a : α) × β a)) : (keys l).length = l.length := by induction l using assoc_induction <;> simp_all -theorem isEmpty_keys_eq_isEmpty (l : List ((a : α) × β a)) : (keys l).isEmpty = l.isEmpty := by +theorem isEmpty_keys_eq_isEmpty (l : List ((a : α) × β a)) : (keys l).isEmpty = l.isEmpty := by induction l using assoc_induction <;> simp_all theorem containsKey_eq_keys_contains [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} @@ -968,8 +969,25 @@ def insertEntry [BEq α] (k : α) (v : β k) (l : List ((a : α) × β a)) : Li @[simp] theorem insertEntry_nil [BEq α] {k : α} {v : β k} : - insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] := by - simp [insertEntry] + insertEntry k v ([] : List ((a : α) × β a)) = [⟨k, v⟩] := + by simp [insertEntry] + +theorem insertEntry_cons_of_false [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} + {v' : β k'} (h : (k' == k) = false) : + Perm (insertEntry k v (⟨k', v'⟩ :: l)) (⟨k', v'⟩ :: insertEntry k v l) := by + simp only [insertEntry, containsKey_cons, h, Bool.false_or, cond_eq_if] + split + · rw [replaceEntry_cons_of_false h] + · apply Perm.swap + +theorem insertEntry_cons_of_beq [BEq α] {l : List ((a : α) × β a)} {k k' : α} {v : β k} {v' : β k'} + (h : k' == k) : insertEntry k v (⟨k', v'⟩ :: l) = ⟨k, v⟩ :: l := by + simp_all only [insertEntry, containsKey_cons, Bool.true_or, cond_true, replaceEntry_cons_of_true] + +@[simp] +theorem insertEntry_cons_self [BEq α] [ReflBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} : + insertEntry k v (⟨k, v⟩ :: l) = ⟨k, v⟩ :: l := + insertEntry_cons_of_beq BEq.refl theorem insertEntry_of_containsKey [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : containsKey k l) : insertEntry k v l = replaceEntry k v l := by @@ -1827,4 +1845,324 @@ theorem eraseKey_append_of_containsKey_right_eq_false [BEq α] {l l' : List ((a · rw [cond_false, cond_false, ih, List.cons_append] · rw [cond_true, cond_true] +/-- Internal implementation detail of the hash map -/ +def alterKey [BEq α] [LawfulBEq α] (k : α) (f : Option (β k) → Option (β k)) + (l : List ((a : α) × β a)) : List ((a : α) × β a) := + match f (getValueCast? k l) with + | none => eraseKey k l + | some v => insertEntry k v l + +theorem length_alterKey [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + {l : List ((a : α) × β a)} : (alterKey k f l).length = + if h : containsKey k l then + if f (getValueCast k l h) |>.isSome then l.length else l.length - 1 + else + if f none |>.isSome then l.length + 1 else l.length := by + rw [alterKey] + cases h : getValueCast? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry, + containsKey_eq_isSome_getValueCast?, ← getValueCast?_eq_some_getValueCast] + +theorem alterKey_cons_perm [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + {k' : α} {v' : β k'} {l : List ((a : α) × β a)} : + Perm (alterKey k f (⟨k', v'⟩ :: l)) (if hk : k' == k then + match f (some (cast (congrArg β (eq_of_beq hk)) v')) with + | none => l + | some v => ⟨k, v⟩ :: l + else + ⟨k', v'⟩ :: alterKey k f l) := by + rw [alterKey] + by_cases hk' : k' == k + · simp only [hk', ↓reduceDIte] + rw [getValueCast?_cons_of_true hk', eraseKey_cons_of_beq hk'] + simp [insertEntry_cons_of_beq hk'] + · simp only [hk', Bool.false_eq_true, ↓reduceDIte] + rw [Bool.not_eq_true] at hk' + rw [getValueCast?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey] + split + · rfl + · simp [insertEntry_cons_of_false hk'] + +theorem alterKey_of_perm [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} + {l l' : List ((a : α) × β a)} (hl : DistinctKeys l) (hp : Perm l l') : + Perm (alterKey a f l) (alterKey a f l') := by + simp only [alterKey, getValueCast?_of_perm hl hp] + split + · exact eraseKey_of_perm hl hp + · exact insertEntry_of_perm hl hp + +theorem alterKey_append_of_containsKey_right_eq_false [BEq α] [LawfulBEq α] {a : α} + {f : Option (β a) → Option (β a)} {l l' : List ((a : α) × β a)} + (hc : containsKey a l' = false) : alterKey a f (l ++ l') = alterKey a f l ++ l' := by + simp only [alterKey, getValueCast?_append_of_containsKey_eq_false hc, + eraseKey_append_of_containsKey_right_eq_false hc, insertEntry_append_of_not_contains_right hc] + split <;> rfl + +@[simp] +theorem alterKey_nil [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} : + alterKey a f [] = match f none with + | none => [] + | some b => [⟨a, b⟩] := rfl + +theorem containsKey_alterKey_self [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) : + containsKey a (alterKey a f l) = (f (getValueCast? a l)).isSome := by + match l with + | [] => + simp only [getValueCast?_nil, Bool.coe_iff_coe, alterKey_nil] + split <;> { rename_i heq; simp [heq] } + | x :: xs => + simp only [alterKey, Bool.coe_iff_coe] + split + · next heq => + simp only [hl, heq, Option.isSome_none, containsKey_eraseKey_self] + · next heq => + simp only [containsKey_insertEntry, heq, beq_self_eq_true, Bool.true_or, Option.isSome_some] + +theorem DistinctKeys.alterKey [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) : DistinctKeys (alterKey a f l) := by + dsimp only [List.alterKey] + split + · exact DistinctKeys.eraseKey hl + · exact DistinctKeys.insertEntry hl + +/-- Internal implementation detail of the hash map -/ +def modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) + (l : List ((a : α) × β a)) : List ((a : α) × β a) := + match getValueCast? k l with + | none => l + | some v => replaceEntry k (f v) l + +theorem modifyKey_eq_alterKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) + (l : List ((a : α) × β a)) : modifyKey k f l = alterKey k (·.map f) l := by + rw [modifyKey, alterKey, Option.map.eq_def] + split <;> next h => + simp [h, insertEntry, containsKey_eq_isSome_getValueCast?, eraseKey_of_containsKey_eq_false] + +theorem mem_replaceEntry_of_key_ne [BEq α] [LawfulBEq α] {a : α} {b : β a} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.1 ≠ a) : + p ∈ replaceEntry a b l ↔ p ∈ l := by + induction l + · simp only [replaceEntry_nil] + · next ih => + simp only [replaceEntry, cond_eq_if] + split + · next h => + simp only [beq_iff_eq] at h + simp only [List.mem_cons, Sigma.ext_iff, h] + apply Iff.intro <;> exact fun + | Or.inr y => Or.inr y + | Or.inl y => hne y.1 |> False.elim + · simp only [List.mem_cons, ih] + +theorem mem_insertEntry_of_key_ne [BEq α] [LawfulBEq α] {a : α} {b : β a} + {l : List ((a : α) × β a)} (p : (a : α) × β a) + (hne : p.1 ≠ a) : p ∈ insertEntry a b l ↔ p ∈ l := by + simp only [insertEntry, cond_eq_if] + split + · exact mem_replaceEntry_of_key_ne p hne + · simp only [List.mem_cons, or_iff_right_iff_imp, Sigma.ext_iff] + exact fun x => hne x.1 |> False.elim + +theorem mem_eraseKey_of_key_ne [BEq α] [LawfulBEq α] {a : α} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.1 ≠ a) : p ∈ eraseKey a l ↔ p ∈ l := by + induction l + · simp only [eraseKey_nil] + · next ih => + simp only [eraseKey, List.mem_cons] + rw [cond_eq_if] + split + · next h => + rw [iff_or_self, Sigma.ext_iff] + exact fun x => (beq_iff_eq.mp h ▸ hne) x.1 |> False.elim + · next h => + simp only [List.mem_cons, ih] + +theorem mem_alterKey_of_key_ne [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.1 ≠ a) : + p ∈ alterKey a f l ↔ p ∈ l := by + rw [alterKey] + split <;> simp only [mem_eraseKey_of_key_ne p hne, mem_insertEntry_of_key_ne p hne] + +theorem length_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) + (l : List ((a : α) × β a)) : (modifyKey k f l).length = l.length := by + induction l + · rfl + · next ih => + simp only [modifyKey] + split <;> next h => simp only [length_replaceEntry, List.length_cons] + +theorem containsKey_modifyKey_self [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) + (l : List ((a : α) × β a)) : containsKey k (modifyKey k f l) = containsKey k l := by + induction l + · simp only [modifyKey, getValueCast?_nil, eraseKey_nil, containsKey_nil, Bool.false_eq_true] + · simp only [modifyKey, Bool.coe_iff_coe] + split + · rfl + · rw [containsKey_replaceEntry] + +namespace Const + +variable {β : Type v} + +/-- Internal implementation detail of the hash map -/ +def alterKey [BEq α] (k : α) (f : Option β → Option β) + (l : List ((_ : α) × β)) : List ((_ : α) × β) := + match f (getValue? k l) with + | none => eraseKey k l + | some v => insertEntry k v l + +theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β} + {l : List ((_ : α) × β)} : (alterKey k f l).length = + if h : containsKey k l then + if f (some (getValue k l h)) |>.isSome then l.length else l.length - 1 + else + if f none |>.isSome then l.length + 1 else l.length := by + rw [alterKey] + cases h : getValue? k l <;> split <;> simp_all [length_eraseKey, length_insertEntry, + containsKey_eq_isSome_getValue?, ← getValue?_eq_some_getValue, -getValue?_eq_none] + +theorem alterKey_cons_perm [BEq α] [EquivBEq α] {k : α} {f : Option β → Option β} + {k' : α} {v' : β} {l : List ((_ : α) × β)} : + Perm (alterKey k f (⟨k', v'⟩ :: l)) (if k' == k then + match f (some v') with + | none => l + | some v => ⟨k, v⟩ :: l + else + ⟨k', v'⟩ :: alterKey k f l) := by + rw [alterKey] + by_cases hk' : k' == k + · simp only [hk', ↓reduceDIte] + rw [getValue?_cons_of_true hk', eraseKey_cons_of_beq hk'] + simp [insertEntry_cons_of_beq hk'] + · simp only [hk', Bool.false_eq_true, ↓reduceDIte] + rw [Bool.not_eq_true] at hk' + rw [getValue?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey] + split + · rfl + · simp [insertEntry_cons_of_false hk'] + +theorem alterKey_of_perm [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} + {l l' : List ((_ : α) × β)} (hl : DistinctKeys l) (hp : Perm l l') : + Perm (alterKey a f l) (alterKey a f l') := by + simp only [alterKey, getValue?_of_perm hl hp] + split + · exact eraseKey_of_perm hl hp + · exact insertEntry_of_perm hl hp + +theorem alterKey_append_of_containsKey_right_eq_false [BEq α] [EquivBEq α] {a : α} + {f : Option β → Option β} {l l' : List ((_ : α) × β)} + (hc : containsKey a l' = false) : alterKey a f (l ++ l') = alterKey a f l ++ l' := by + simp only [alterKey, getValue?_append_of_containsKey_eq_false hc, + eraseKey_append_of_containsKey_right_eq_false hc, insertEntry_append_of_not_contains_right hc] + split <;> rfl + +@[simp] +theorem alterKey_nil [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} : + alterKey a f [] = match f none with + | none => [] + | some b => [⟨a, b⟩] := rfl + +theorem containsKey_alterKey_self [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} + {l : List ((_ : α) × β)} (hl : DistinctKeys l) : + containsKey a (alterKey a f l) ↔ (f (getValue? a l)).isSome := by + match l with + | [] => + simp only [getValue?_nil, Bool.coe_iff_coe, alterKey_nil] + split <;> { rename_i heq; simp [heq] } + | x :: xs => + simp only [alterKey, Bool.coe_iff_coe] + split + · next heq => + simp only [hl, heq, Option.isSome_none, containsKey_eraseKey_self] + · next heq => + simp only [containsKey_insertEntry, BEq.refl, Bool.true_or, heq, Option.isSome_some] + +theorem mem_replaceEntry_of_key_not_beq [BEq α] [EquivBEq α] {a : α} {b : β} + {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) : + p ∈ replaceEntry a b l ↔ p ∈ l := by + induction l + · simp only [replaceEntry_nil] + · next ih => + simp only [replaceEntry, cond_eq_if] + split + · next h => + simp only [List.mem_cons, Sigma.ext_iff] + apply Iff.intro <;> exact fun + | Or.inr y => Or.inr y + | Or.inl y => by simp_all only [BEq.refl, Bool.true_eq_false] + · simp only [List.mem_cons, ih] + +theorem mem_insertEntry_of_key_ne [BEq α] [EquivBEq α] {a : α} {b : β} + {l : List ((_ : α) × β)} (p : (_ : α) × β) + (hne : (p.1 == a) = false) : p ∈ insertEntry a b l ↔ p ∈ l := by + simp only [insertEntry, cond_eq_if] + split + · exact mem_replaceEntry_of_key_not_beq p hne + · simp only [List.mem_cons, or_iff_right_iff_imp, Sigma.ext_iff] + rw [← Bool.not_eq_true] at hne + exact fun x => hne (beq_of_eq x.1) |> False.elim + +theorem mem_eraseKey_of_key_ne [BEq α] [EquivBEq α] {a : α} + {l : List ((_ : α) × β)} (p : (_ : α) × β) (hne : (p.1 == a) = false) : + p ∈ eraseKey a l ↔ p ∈ l := by + induction l + · simp only [eraseKey_nil] + · next ih => + simp only [eraseKey, List.mem_cons] + rw [cond_eq_if] + split + · next h => + rw [iff_or_self, Sigma.ext_iff] + intro ⟨h₁, h₂⟩ + rw [h₁, h] at hne + contradiction + · next h => + simp only [List.mem_cons, ih] + +theorem mem_alterKey_of_key_not_beq {β : Type v} [BEq α] [EquivBEq α] {a : α} + {f : Option β → Option β} {l : List ((_ : α) × β)} (p : (_ : α) × β) + (hne : (p.1 == a) = false) : p ∈ alterKey a f l ↔ p ∈ l := by + rw [alterKey] + split <;> simp only [mem_eraseKey_of_key_ne p hne, mem_insertEntry_of_key_ne p hne] + +/-- Internal implementation detail of the hash map -/ +def modifyKey [BEq α] [EquivBEq α] (k : α) (f : β → β) + (l : List ((_ : α) × β)) : List ((_ : α) × β) := + match getValue? k l with + | none => l + | some v => replaceEntry k (f v) l + +theorem modifyKey_eq_alterKey [BEq α] [EquivBEq α] (k : α) (f : β → β) + (l : List ((_ : α) × β)) : modifyKey k f l = alterKey k (·.map f) l := by + rw [modifyKey, alterKey, Option.map.eq_def] + split <;> next h => + simp [h, insertEntry, containsKey_eq_isSome_getValue?, eraseKey_of_containsKey_eq_false] + +theorem length_modifyKey [BEq α] [EquivBEq α] (k : α) (f : β → β) + (l : List ((_ : α) × β)) : (modifyKey k f l).length = l.length := by + induction l + · rfl + · next ih => + simp only [modifyKey] + split <;> next h => simp only [length_replaceEntry, List.length_cons] + +theorem containsKey_modifyKey_self [BEq α] [EquivBEq α] (k : α) (f : β → β) + (l : List ((_ : α) × β)) : containsKey k (modifyKey k f l) = containsKey k l := by + induction l + · simp only [modifyKey, getValue?_nil, eraseKey_nil, containsKey_nil, Bool.false_eq_true] + · simp only [modifyKey, Bool.coe_iff_coe] + split + · rfl + · rw [containsKey_replaceEntry] + +end Const + +theorem DistinctKeys.constAlterKey {β : Type v} [BEq α] [EquivBEq α] {a : α} + {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : + DistinctKeys (List.Const.alterKey a f l) := by + dsimp only [List.Const.alterKey] + split + · exact DistinctKeys.eraseKey hl + · exact DistinctKeys.insertEntry hl + end List diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 444082ed805d..8384a6976db0 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -41,6 +41,11 @@ def bucket [Hashable α] (self : Array (AssocList α β)) (h : 0 < self.size) (k let ⟨i, h⟩ := mkIdx self.size h (hash k) self[i] +theorem bucket_eq {α : Type u} {β : α → Type v} [Hashable α] (self : Array (AssocList α β)) + (h : 0 < self.size) (k : α) : bucket self h k = + haveI := mkIdx self.size h (hash k) |>.2 + self[mkIdx self.size h (hash k) |>.1] := rfl + /-- Internal implementation detail of the hash map -/ def updateBucket [Hashable α] (self : Array (AssocList α β)) (h : 0 < self.size) (k : α) (f : AssocList α β → AssocList α β) : Array (AssocList α β) := @@ -79,6 +84,13 @@ theorem size_withComputedSize {self : Array (AssocList α β)} : theorem buckets_withComputedSize {self : Array (AssocList α β)} : (withComputedSize self).buckets = self := rfl +@[simp] +theorem bucket_updateBucket [Hashable α] (self : Array (AssocList α β)) (h : 0 < self.size) (k : α) + (f : AssocList α β → AssocList α β) : + bucket (updateBucket self h k f) (by simpa using h) k = f (bucket self h k) := by + unfold bucket updateBucket mkIdx + simp + theorem exists_bucket_of_uset [BEq α] [Hashable α] (self : Array (AssocList α β)) (i : USize) (hi : i.toNat < self.size) (d : AssocList α β) : ∃ l, Perm (toListModel self) (self[i.toNat].toList ++ l) ∧ @@ -165,13 +177,14 @@ theorem apply_bucket_with_proof {γ : α → Type w} [BEq α] [Hashable α] [Par /-- This is the general theorem to show that modification operations are correct. -/ theorem toListModel_updateBucket [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] {m : Raw₀ α β} (hm : Raw.WFImp m.1) {a : α} {f : AssocList α β → AssocList α β} - {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {l}, (f l).toList = g l.toList) + {g : List ((a : α) × β a) → List ((a : α) × β a)} (hfg : ∀ {l}, Perm (f l).toList (g l.toList)) (hg₁ : ∀ {l l'}, DistinctKeys l → Perm l l' → Perm (g l) (g l')) (hg₂ : ∀ {l l'}, containsKey a l' = false → g (l ++ l') = g l ++ l') : Perm (toListModel (updateBucket m.1.buckets m.2 a f)) (g (toListModel m.1.2)) := by obtain ⟨l, h₁, h₂, h₃⟩ := exists_bucket_of_update m.1.buckets m.2 a f refine h₂.trans (Perm.trans ?_ (hg₁ hm.distinct h₁).symm) - rw [hfg, hg₂] + refine Perm.append_right l hfg |>.trans ?_ + rw [hg₂] exact h₃ hm.buckets_hash_self _ rfl /-- This is the general theorem to show that mapping operations (like `map` and `filter`) are @@ -310,6 +323,49 @@ def eraseₘaux [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Raw₀ α def eraseₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) : Raw₀ α β := if m.containsₘ a then m.eraseₘaux a else m +/-- Internal implementation detail of the hash map -/ +def alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) + (f : Option (β a) → Option (β a)) : Raw₀ α β := + if h : m.containsₘ a then + let buckets' := updateBucket m.1.buckets m.2 a (fun l => l.alter a f) + let size' := + if Raw₀.containsₘ ⟨withComputedSize buckets', by simpa [buckets'] using m.2⟩ a + then m.1.size else m.1.size - 1 + ⟨⟨size', buckets'⟩, by simpa [buckets'] using m.2⟩ + else + match f none with + | none => m + | some b => Raw₀.expandIfNecessary (m.consₘ a b) + +/-- Internal implementation detail of the hash map -/ +def modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) (f : β a → β a) : Raw₀ α β := + m.alterₘ a (·.map f) + +namespace Const + +variable {β : Type v} + +/-- Internal implementation detail of the hash map -/ +def alterₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) + (f : Option β → Option β) : Raw₀ α (fun _ => β) := + if h : m.containsₘ a then + let buckets' := updateBucket m.1.buckets m.2 a (fun l => AssocList.Const.alter a f l) + let size' := + if Raw₀.containsₘ ⟨withComputedSize buckets', by simpa [buckets'] using m.2⟩ a + then m.1.size else m.1.size - 1 + ⟨⟨size', buckets'⟩, by simpa [buckets'] using m.2⟩ + else + match f none with + | none => m + | some b => Raw₀.expandIfNecessary (m.consₘ a b) + +/-- Internal implementation detail of the hash map -/ +def modifyₘ [BEq α] [Hashable α] (m : Raw₀ α (fun _ => β)) (a : α) (f : β → β) : + Raw₀ α (fun _ => β) := + alterₘ m a (fun option => option.map f) + +end Const + /-- Internal implementation detail of the hash map -/ def filterMapₘ (m : Raw₀ α β) (f : (a : α) → β a → Option (δ a)) : Raw₀ α δ := ⟨withComputedSize (updateAllBuckets m.1.buckets fun l => l.filterMap f), by simpa using m.2⟩ @@ -391,6 +447,64 @@ theorem insert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) ( simp only [Array.uset, Array.ugetElem_eq_getElem] · rfl +theorem alter_eq_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) + (f : Option (β a) → Option (β a)) : m.alter a f = m.alterₘ a f := by + dsimp only [alter, alterₘ, containsₘ, ← bucket_eq] + split + · congr 2 + · simp only [withComputedSize, bucket_updateBucket] + · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket] + · congr + +theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) + (f : β a → β a) : m.modify a f = m.alter a (·.map f) := by + rw [modify, alter] + split + · dsimp + split + · next h => + simp only [AssocList.contains_eq] at h + simp only [AssocList.modify_eq_alter, Array.set_set, AssocList.contains_eq, + containsKey_of_perm AssocList.toList_alter, ← modifyKey_eq_alterKey, + containsKey_modifyKey_self, h, ↓reduceIte] + · rfl + +theorem modify_eq_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) + (f : β a → β a) : m.modify a f = m.modifyₘ a f := by + rw [modify_eq_alter, alter_eq_alterₘ, modifyₘ] + +namespace Const + +variable {β : Type v} + +theorem alter_eq_alterₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α) + (f : Option β → Option β) : Const.alter m a f = Const.alterₘ m a f := by + dsimp only [alter, alterₘ, containsₘ, ← bucket_eq] + split + · congr 2 + · simp only [withComputedSize, bucket_updateBucket] + · simp only [Array.uset, bucket, Array.ugetElem_eq_getElem, Array.set_set, updateBucket] + · congr + +theorem modify_eq_alter [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α) + (f : β → β) : Const.modify m a f = Const.alter m a (·.map f) := by + rw [modify, alter] + split + · dsimp + split + · next h => + simp only [AssocList.contains_eq] at h + simp only [AssocList.Const.modify_eq_alter, Array.set_set, AssocList.contains_eq, + containsKey_of_perm AssocList.Const.toList_alter, ← Const.modifyKey_eq_alterKey, + Const.containsKey_modifyKey_self, h, ↓reduceIte] + · rfl + +theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α) + (f : β → β) : Const.modify m a f = Const.modifyₘ m a f := by + rw [modify_eq_alter, alter_eq_alterₘ, modifyₘ] + +end Const + theorem containsThenInsert_eq_insertₘ [BEq α] [Hashable α] (m : Raw₀ α β) (a : α) (b : β a) : (m.containsThenInsert a b).2 = m.insertₘ a b := by rw [containsThenInsert, insertₘ, containsₘ, bucket] diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index d0c9b83a0550..87e7e14870db 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -240,6 +240,12 @@ theorem toListModel_expandIfNecessary [BEq α] [Hashable α] [PartialEquivBEq α · dsimp exact toListModel_expand +@[simp] +theorem size_expandIfNecessary [BEq α] [Hashable α] {m : Raw₀ α β} : + (expandIfNecessary m).val.size = m.val.size := by + rw [expandIfNecessary] + split <;> rfl + theorem wfImp_expandIfNecessary [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.1) : Raw.WFImp (expandIfNecessary m).1 := by rw [Raw₀.expandIfNecessary] @@ -402,7 +408,7 @@ end theorem toListModel_replaceₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.1) (a : α) (b : β a) : Perm (toListModel (m.replaceₘ a b).1.buckets) (replaceEntry a b (toListModel m.1.2)) := - toListModel_updateBucket h AssocList.toList_replace List.replaceEntry_of_perm + toListModel_updateBucket h (.of_eq AssocList.toList_replace) List.replaceEntry_of_perm List.replaceEntry_append_of_containsKey_right_eq_false theorem isHashSelf_replaceₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) @@ -422,7 +428,7 @@ theorem wfImp_replaceₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α theorem toListModel_consₘ [BEq α] [Hashable α] [PartialEquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.1) (a : α) (b : β a) : Perm (toListModel (m.consₘ a b).1.buckets) (⟨a, b⟩ :: (toListModel m.1.2)) := - toListModel_updateBucket h rfl (fun _ => Perm.cons _) (fun _ => cons_append _ _ _) + toListModel_updateBucket h .rfl (fun _ => Perm.cons _) (fun _ => cons_append _ _ _) theorem isHashSelf_consₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (h : Raw.WFImp m.1) (a : α) (b : β a) : IsHashSelf (m.consₘ a b).1.buckets := by @@ -479,6 +485,225 @@ theorem wfImp_insert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m rw [insert_eq_insertₘ] exact wfImp_insertₘ h +/-! # `alter` -/ + +theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} + (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} : + Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.alter a f))) + (alterKey a f (toListModel m.1.buckets)) := by + exact toListModel_updateBucket h AssocList.toList_alter List.alterKey_of_perm + List.alterKey_append_of_containsKey_right_eq_false + +theorem isHashSelf_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} + (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} : + IsHashSelf (updateBucket m.1.buckets m.2 a (AssocList.alter a f)) := by + apply h.buckets_hash_self.updateBucket (fun l p hp => ?_) + rw [AssocList.toList_alter.mem_iff] at hp + by_cases h : p.fst = a + · exact .inr <| congrArg hash h + · rw [mem_alterKey_of_key_ne _ h] at hp + exact .inl <| containsKey_of_mem hp + +theorem wfImp_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} + (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} : + Raw.WFImp (withComputedSize <| updateBucket m.1.buckets m.2 a (AssocList.alter a f)) where + buckets_hash_self := isHashSelf_updateBucket_alter h + size_eq := by rw [size_withComputedSize, computeSize_eq, buckets_withComputedSize] + distinct := DistinctKeys.perm (toListModel_updateBucket_alter h) h.distinct.alterKey + +theorem isHashSelf_alterₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (h : Raw.WFImp m.1) + (a : α) (f : Option (β a) → Option (β a)) : IsHashSelf (m.alterₘ a f).1.buckets := by + dsimp only [alterₘ, withComputedSize] + split + · exact isHashSelf_updateBucket_alter h + · next hc => + split + · exact h.buckets_hash_self + · refine (wfImp_expandIfNecessary _ (wfImp_consₘ _ h _ _ ?_)).buckets_hash_self + exact Bool.not_eq_true _ ▸ hc + +theorem toListModel_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) + {a : α} {f : Option (β a) → Option (β a)} : + Perm (toListModel (m.alterₘ a f).1.2) (alterKey a f (toListModel m.1.2)) := by + rw [alterₘ] + split + · exact toListModel_updateBucket_alter h + · next hc => + rw [Bool.not_eq_true, containsₘ_eq_containsKey h] at hc + rw [alterKey, getValueCast?_eq_none hc] + split + · next hn => + simp only [hn] + rw [eraseKey_of_containsKey_eq_false] + exact hc + · next hs => + simp only [hs] + refine Perm.trans (toListModel_expandIfNecessary _) ?_ + refine Perm.trans (toListModel_consₘ m h _ _) ?_ + rw [insertEntry_of_containsKey_eq_false] + exact hc + +theorem toListModel_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) + {a : α} {f : Option (β a) → Option (β a)} : + Perm (toListModel (m.alter a f).1.2) (alterKey a f (toListModel m.1.2)) := by + rw [alter_eq_alterₘ] + exact toListModel_alterₘ h + +theorem wfImp_alterₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} + {f : Option (β a) → Option (β a)} : Raw.WFImp (m.alterₘ a f).1 where + buckets_hash_self := isHashSelf_alterₘ m h a f + distinct := DistinctKeys.perm (toListModel_alterₘ h) h.distinct.alterKey + size_eq := by + rw [← Perm.length_eq (toListModel_alterₘ h).symm, alterₘ] + split + · next h₁ => + rw [containsₘ_eq_containsKey h] at h₁ + simp only [length_alterKey, h.size_eq, dif_pos h₁] + rw [containsₘ_eq_containsKey (by apply wfImp_updateBucket_alter h)] + simp only [buckets_withComputedSize] + simp only [containsKey_of_perm <| toListModel_updateBucket_alter h] + rw [← getValueCast?_eq_some_getValueCast h₁] + conv => lhs; congr; rw [containsKey_alterKey_self h.distinct] + · next h₁ => + rw [containsₘ_eq_containsKey h] at h₁ + rw [alterKey] + rw [getValueCast?_eq_none <| Bool.not_eq_true _ ▸ h₁] + split + · next heq => + rw [heq, h.size_eq, length_eraseKey, if_neg h₁] + · next heq => + rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq] + +theorem wfImp_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} + (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} : Raw.WFImp (m.alter a f).1 := by + rw [alter_eq_alterₘ] + exact wfImp_alterₘ h + +namespace Const + +variable {β : Type v} + +theorem toListModel_updateBucket_alter [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : + Perm (toListModel (updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f))) + (Const.alterKey a f (toListModel m.1.buckets)) := by + exact toListModel_updateBucket h AssocList.Const.toList_alter List.Const.alterKey_of_perm + List.Const.alterKey_append_of_containsKey_right_eq_false + +theorem isHashSelf_updateBucket_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : + IsHashSelf (updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f)) := by + apply h.buckets_hash_self.updateBucket (fun l p hp => ?_) + rw [AssocList.Const.toList_alter.mem_iff] at hp + by_cases h : p.fst == a + · exact .inr <| hash_eq h + · rw [Bool.not_eq_true] at h + rw [Const.mem_alterKey_of_key_not_beq _ h] at hp + exact .inl <| containsKey_of_mem hp + +theorem wfImp_updateBucket_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : + Raw.WFImp (withComputedSize <| updateBucket m.1.buckets m.2 a (AssocList.Const.alter a f)) where + buckets_hash_self := isHashSelf_updateBucket_alter h + size_eq := by rw [size_withComputedSize, computeSize_eq]; rfl + distinct := DistinctKeys.perm (toListModel_updateBucket_alter h) h.distinct.constAlterKey + +theorem isHashSelf_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + (m : Raw₀ α (fun _ => β)) (h : Raw.WFImp m.1) (a : α) (f : Option β → Option β) : + IsHashSelf (Const.alterₘ m a f).1.buckets := by + dsimp only [alterₘ, withComputedSize] + split + · exact isHashSelf_updateBucket_alter h + · next hc => + split + · exact h.buckets_hash_self + · refine (wfImp_expandIfNecessary _ (wfImp_consₘ _ h _ _ ?_)).buckets_hash_self + exact Bool.not_eq_true _ ▸ hc + +theorem toListModel_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] + {m : Raw₀ α (fun _ => β)} (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : + Perm (toListModel (Const.alterₘ m a f).1.2) (Const.alterKey a f (toListModel m.1.2)) := by + rw [Const.alterₘ] + split + · exact toListModel_updateBucket_alter h + · next hc => + rw [Bool.not_eq_true, containsₘ_eq_containsKey h] at hc + rw [Const.alterKey, getValue?_eq_none.mpr hc] + split + · next hn => + simp only [hn] + rw [eraseKey_of_containsKey_eq_false] + exact hc + · next hs => + simp only [hs] + refine Perm.trans (toListModel_expandIfNecessary _) ?_ + refine Perm.trans (toListModel_consₘ m h _ _) ?_ + rw [insertEntry_of_containsKey_eq_false] + exact hc + +theorem wfImp_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} + (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Raw.WFImp (Const.alterₘ m a f).1 where + buckets_hash_self := isHashSelf_alterₘ m h a f + distinct := DistinctKeys.perm (toListModel_alterₘ h) h.distinct.constAlterKey + size_eq := by + rw [← Perm.length_eq (toListModel_alterₘ h).symm, alterₘ] + split + · next h₁ => + rw [containsₘ_eq_containsKey h] at h₁ + simp only [Const.length_alterKey, h.size_eq, dif_pos h₁] + rw [containsₘ_eq_containsKey (by apply wfImp_updateBucket_alter h)] + simp only [buckets_withComputedSize] + simp only [containsKey_of_perm <| toListModel_updateBucket_alter h] + rw [← getValue?_eq_some_getValue h₁] + conv => lhs; congr; rw [Const.containsKey_alterKey_self h.distinct] + · next h₁ => + rw [containsₘ_eq_containsKey h] at h₁ + rw [Const.alterKey] + rw [getValue?_eq_none.mpr <| Bool.not_eq_true _ ▸ h₁] + split + · next heq => + rw [heq, h.size_eq, length_eraseKey, if_neg h₁] + · next heq => + rw [heq, size_expandIfNecessary, consₘ, length_insertEntry, if_neg h₁, h.size_eq] + +theorem wfImp_alter [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} + (h : Raw.WFImp m.1) {a : α} {f : Option β → Option β} : Raw.WFImp (Const.alter m a f).1 := by + rw [Const.alter_eq_alterₘ] + exact wfImp_alterₘ h + +end Const + +/-! # `modify` -/ + +theorem toListModel_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) + {a : α} {f : β a → β a} : + Perm (toListModel (m.modify a f).1.2) (modifyKey a f (toListModel m.1.2)) := by + rw [modify_eq_alter, modifyKey_eq_alterKey] + exact toListModel_alter h + +theorem wfImp_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} + (h : Raw.WFImp m.1) {a : α} {f : β a → β a} : Raw.WFImp (m.modifyₘ a f).1 := wfImp_alterₘ h + +theorem wfImp_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h : Raw.WFImp m.1) {a : α} + {f : β a → β a} : Raw.WFImp (m.modify a f).1 := by + rw [modify_eq_modifyₘ] + exact wfImp_alterₘ h + +namespace Const + +variable {β : Type v} + +theorem wfImp_modifyₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} + (h : Raw.WFImp m.1) {a : α} {f : β → β} : Raw.WFImp (Const.modifyₘ m a f).1 := + Const.wfImp_alterₘ h + +theorem wfImp_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} + (h : Raw.WFImp m.1) {a : α} {f : β → β} : Raw.WFImp (Const.modify m a f).1 := by + rw [Const.modify_eq_modifyₘ] + exact wfImp_alterₘ h + +end Const + /-! # `containsThenInsert` -/ theorem toListModel_containsThenInsert [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] @@ -574,7 +799,7 @@ theorem Const.wfImp_getThenInsertIfNew? {β : Type v} [BEq α] [Hashable α] [Eq theorem toListModel_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) (a : α) (h : Raw.WFImp m.1) : Perm (toListModel (m.eraseₘaux a).1.buckets) (eraseKey a (toListModel m.1.buckets)) := - toListModel_updateBucket h AssocList.toList_erase List.eraseKey_of_perm + toListModel_updateBucket h (.of_eq AssocList.toList_erase) List.eraseKey_of_perm List.eraseKey_append_of_containsKey_right_eq_false theorem isHashSelf_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β) @@ -747,6 +972,10 @@ theorem WF.out [BEq α] [Hashable α] [i₁ : EquivBEq α] [i₂ : LawfulHashabl · next h => exact Raw₀.wfImp_getThenInsertIfNew? (by apply h) · next h => exact Raw₀.wfImp_filter (by apply h) · next h => exact Raw₀.Const.wfImp_getThenInsertIfNew? (by apply h) + · next h => exact Raw₀.wfImp_modify (by apply h) + · next h => exact Raw₀.Const.wfImp_modify (by apply h) + · next h => exact Raw₀.wfImp_alter (by apply h) + · next h => exact Raw₀.Const.wfImp_alter (by apply h) end Raw @@ -762,8 +991,8 @@ theorem Const.wfImp_insertMany {β : Type v} [BEq α] [Hashable α] [EquivBEq α {l : ρ} (h : Raw.WFImp m.1) : Raw.WFImp (Const.insertMany m l).1.1 := Raw.WF.out ((Const.insertMany m l).2 _ Raw.WF.insert₀ (.wf m.2 h)) -theorem Const.wfImp_insertManyIfNewUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {ρ : Type w} - [ForIn Id ρ α] {m : Raw₀ α (fun _ => Unit)} {l : ρ} (h : Raw.WFImp m.1) : +theorem Const.wfImp_insertManyIfNewUnit [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] + {ρ : Type w} [ForIn Id ρ α] {m : Raw₀ α (fun _ => Unit)} {l : ρ} (h : Raw.WFImp m.1) : Raw.WFImp (Const.insertManyIfNewUnit m l).1.1 := Raw.WF.out ((Const.insertManyIfNewUnit m l).2 _ Raw.WF.insertIfNew₀ (.wf m.2 h)) diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index 8074021b8901..5ca1cdc1a588 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -509,6 +509,18 @@ inductive WF : {α : Type u} → {β : α → Type v} → [BEq α] → [Hashable /-- Internal implementation detail of the hash map -/ | constGetThenInsertIfNew?₀ {α β} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a b} : WF m → WF (Raw₀.Const.getThenInsertIfNew? ⟨m, h⟩ a b).2.1 + /-- Internal implementation detail of the hash map -/ + | modify₀ {α β} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} {f : β a → β a} : + WF m → WF (Raw₀.modify ⟨m, h⟩ a f).1 + /-- Internal implementation detail of the hash map -/ + | constModify₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} {f : β → β} : + WF m → WF (Raw₀.Const.modify ⟨m, h⟩ a f).1 + /-- Internal implementation detail of the hash map -/ + | alter₀ {α β} [BEq α] [Hashable α] [LawfulBEq α] {m : Raw α β} {h a} + {f : Option (β a) → Option (β a)} : WF m → WF (Raw₀.alter ⟨m, h⟩ a f).1 + /-- Internal implementation detail of the hash map -/ + | constAlter₀ {α} {β : Type v} [BEq α] [Hashable α] {m : Raw α (fun _ => β)} {h a} + {f : Option β → Option β} : WF m → WF (Raw₀.Const.alter ⟨m, h⟩ a f).1 /-- Internal implementation detail of the hash map -/ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 < m.buckets.size @@ -522,6 +534,10 @@ theorem WF.size_buckets_pos [BEq α] [Hashable α] (m : Raw α β) : WF m → 0 | getThenInsertIfNew?₀ _ => (Raw₀.getThenInsertIfNew? ⟨_, _⟩ _ _).2.2 | filter₀ _ => (Raw₀.filter _ ⟨_, _⟩).2 | constGetThenInsertIfNew?₀ _ => (Raw₀.Const.getThenInsertIfNew? ⟨_, _⟩ _ _).2.2 + | modify₀ _ => (Raw₀.modify _ _ _).2 + | constModify₀ _ => (Raw₀.Const.modify _ _ _).2 + | alter₀ _ => (Raw₀.alter _ _ _).2 + | constAlter₀ _ => (Raw₀.Const.alter _ _ _).2 @[simp] theorem WF.empty [BEq α] [Hashable α] {c : Nat} : (Raw.empty c : Raw α β).WF := .empty₀ diff --git a/src/Std/Data/HashMap/Basic.lean b/src/Std/Data/HashMap/Basic.lean index 0063ae3e4839..70e3d0ee5ec9 100644 --- a/src/Std/Data/HashMap/Basic.lean +++ b/src/Std/Data/HashMap/Basic.lean @@ -245,21 +245,13 @@ instance [BEq α] [Hashable α] {m : Type w → Type w} : ForIn m (HashMap α β Array β := m.inner.valuesArray -@[inline, inherit_doc DHashMap.modify] def modify (m : HashMap α β) (a : α) (f : β → β) : HashMap α β := - match m.get? a with - | none => m - | some b => m.erase a |>.insert a (f b) - -@[inline, inherit_doc DHashMap.alter] def alter (m : HashMap α β) (a : α) (f : Option β → Option β) : HashMap α β := - match m.get? a with - | none => - match f none with - | none => m - | some b => m.insert a b - | some b => - match f (some b) with - | none => m.erase a - | some b => m.erase a |>.insert a b +@[inline, inherit_doc DHashMap.modify] def modify (m : HashMap α β) (a : α) (f : β → β) : + HashMap α β := + ⟨DHashMap.Const.modify m.inner a f⟩ + +@[inline, inherit_doc DHashMap.alter] def alter (m : HashMap α β) (a : α) + (f : Option β → Option β) : HashMap α β := + ⟨DHashMap.Const.alter m.inner a f⟩ @[inline, inherit_doc DHashMap.Const.insertMany] def insertMany {ρ : Type w} [ForIn Id ρ (α × β)] (m : HashMap α β) (l : ρ) : HashMap α β :=