From 31929c0acd871ff556e73e132fbc23e11198f8b5 Mon Sep 17 00:00:00 2001 From: Paul Reichert Date: Tue, 21 Jan 2025 13:34:19 +0100 Subject: [PATCH] feat: lemmas for HashMap.alter and .modify (#6620) This PR adds lemmas about HashMap.alter and .modify. These lemmas describe the interaction of alter and modify with the read methods of the HashMap. The additions affect the HashMap, the DHashMap and their respective raw versions. Moreover, the raw versions of alter and modify are defined. --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> --- .../DHashMap/Internal/List/Associative.lean | 1011 ++++++++++++++--- src/Std/Data/DHashMap/Internal/Model.lean | 4 +- src/Std/Data/DHashMap/Internal/Raw.lean | 16 + src/Std/Data/DHashMap/Internal/RawLemmas.lean | 565 ++++++++- src/Std/Data/DHashMap/Internal/WF.lean | 18 +- src/Std/Data/DHashMap/Lemmas.lean | 665 +++++++++++ src/Std/Data/DHashMap/Raw.lean | 39 + src/Std/Data/DHashMap/RawLemmas.lean | 727 +++++++++++- src/Std/Data/HashMap/Lemmas.lean | 333 ++++++ src/Std/Data/HashMap/Raw.lean | 8 + src/Std/Data/HashMap/RawLemmas.lean | 332 ++++++ 11 files changed, 3515 insertions(+), 203 deletions(-) diff --git a/src/Std/Data/DHashMap/Internal/List/Associative.lean b/src/Std/Data/DHashMap/Internal/List/Associative.lean index e56d6864e7..4bcee2b7ad 100644 --- a/src/Std/Data/DHashMap/Internal/List/Associative.lean +++ b/src/Std/Data/DHashMap/Internal/List/Associative.lean @@ -676,6 +676,26 @@ theorem isEmpty_replaceEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v · simp only [replaceEntry_cons, cond_eq_if, List.isEmpty_cons] split <;> simp +theorem mem_replaceEntry_of_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β a} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (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_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 := + mem_replaceEntry_of_beq_eq_false p <| beq_false_of_ne hne + theorem getEntry?_replaceEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} {a k : α} {v : β k} (hl : containsKey k l = false) : getEntry? a (replaceEntry k v l) = getEntry? a l := by @@ -810,6 +830,27 @@ theorem eraseKey_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a)} simp only [containsKey_cons, Bool.or_eq_false_iff] at h rw [eraseKey_cons_of_false h.1, ih h.2] +theorem mem_eraseKey_of_key_beq_eq_false [BEq α] {a : α} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (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_eraseKey_of_key_ne [BEq α] [LawfulBEq α] {a : α} + {l : List ((a : α) × β a)} (p : (a : α) × β a) (hne : p.1 ≠ a) : p ∈ eraseKey a l ↔ p ∈ l := + mem_eraseKey_of_key_beq_eq_false p <| beq_false_of_ne hne + theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} : Sublist (eraseKey k l) l := by induction l using assoc_induction @@ -1028,6 +1069,21 @@ theorem insertEntry_of_containsKey_eq_false [BEq α] {l : List ((a : α) × β a (h : containsKey k l = false) : insertEntry k v l = ⟨k, v⟩ :: l := by simp [insertEntry, h] +theorem mem_insertEntry_of_key_beq_eq_false [BEq α] [EquivBEq α] {a : α} {b : β a} + {l : List ((a : α) × β a)} (p : (a : α) × β a) + (hne : (p.1 == a) = false) : p ∈ insertEntry a b l ↔ p ∈ l := by + simp only [insertEntry, cond_eq_if] + split + · exact mem_replaceEntry_of_beq_eq_false 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_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 := + mem_insertEntry_of_key_beq_eq_false p <| beq_false_of_ne hne + theorem DistinctKeys.insertEntry [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} (h : DistinctKeys l) : DistinctKeys (insertEntry k v l) := by cases h' : containsKey k l @@ -2716,26 +2772,52 @@ theorem getValue?_insertListIfNewUnit [BEq α] [PartialEquivBEq α] end +private theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) : + Option.map (cast h) x = cast (congrArg Option h) x := by + cases h; cases x <;> simp + +private theorem cast_eq_id {α : Type u} : cast (rfl : α = α) = id := by rfl + +private theorem function_id_comp {α : Type u} {β : Type v} {f : α → β} : + id ∘ f = f := rfl + +section Alter + +section Dependent + +variable [BEq α] [LawfulBEq α] + /-- Internal implementation detail of the hash map -/ -def alterKey [BEq α] [LawfulBEq α] (k : α) (f : Option (β k) → Option (β k)) +def alterKey (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 +theorem length_alterKey {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 +theorem length_alterKey' {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : + (alterKey k f l).length = + if containsKey k l && (f (getValueCast? k l)).isNone then + l.length - 1 + else if !containsKey k l && (f (getValueCast? k l)).isSome then + l.length + 1 + else + l.length := by + rw [alterKey] + cases h : containsKey k l <;> split <;> split <;> simp_all [length_eraseKey, length_insertEntry] + +theorem alterKey_cons_perm {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 @@ -2751,128 +2833,225 @@ theorem alterKey_cons_perm [BEq α] [LawfulBEq α] {k : α} {f : Option (β k) rw [getValueCast?_cons_of_false hk', eraseKey_cons_of_false hk', alterKey] split · rfl - · simp [insertEntry_cons_of_false hk'] + · exact 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 +theorem isEmpty_alterKey_eq_isEmpty_eraseKey {k : α} {f : Option (β k) → Option (β k)} + {l : List ((a : α) × β a)} : + (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValueCast? k l)).isNone) := by + rw [alterKey, Bool.eq_iff_iff, Bool.and_eq_true_iff] + cases f (getValueCast? k l) + repeat simp [isEmpty_insertEntry] + +theorem isEmpty_alterKey {k : α} {f : Option (β k) → Option (β k)} {l : List ((a : α) × β a)} : + (alterKey k f l).isEmpty = ((l.isEmpty || (l.length == 1 && containsKey k l)) && + (f (getValueCast? k l)).isNone) := by + rw [isEmpty_alterKey_eq_isEmpty_eraseKey, isEmpty_eraseKey] + +theorem alterKey_of_perm {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 +theorem alterKey_append_of_containsKey_right_eq_false {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)} : +theorem alterKey_nil {a : α} {f : Option (β a) → Option (β a)} : alterKey a f [] = match f none with - | none => [] - | some b => [⟨a, b⟩] := rfl +| none => [] +| some b => [⟨a, b⟩] := rfl -theorem containsKey_alterKey_self [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} +theorem containsKey_alterKey_self {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] } + cases f none <;> simp | 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] + cases f (getValueCast? a (x :: xs)) + · simp only [hl, Option.isSome_none, containsKey_eraseKey_self] + · simp only [containsKey_insertEntry, BEq.refl, Bool.true_or, Option.isSome_some] -theorem DistinctKeys.alterKey [BEq α] [LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)} +theorem containsKey_alterKey {k k' : α} {f : Option (β k) → Option (β k)} + {l : List ((a : α) × β a)} (hl : DistinctKeys l) : + containsKey k' (alterKey k f l) = + if k == k' then + f (getValueCast? k l) |>.isSome + else + containsKey k' l := by + split + · next h => + rw [← containsKey_congr h, containsKey_alterKey_self hl] + · next h => + rw [alterKey] + cases f (getValueCast? k l) + · simp [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)] + · simp_all + +theorem DistinctKeys.alterKey {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)} +theorem mem_alterKey_of_key_ne {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] +theorem getValueCast?_alterKey (k k' : α) (f : Option (β k) → Option (β k)) + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast? k' (alterKey k f l) = + if h : k == k' then + cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (getValueCast? k l)) + else + getValueCast? k' l := by + split + · next heq => + cases eq_of_beq heq + simp only [Function.comp_apply, cast_eq] + rw [alterKey] split - · rfl - · rw [containsKey_replaceEntry] + · next hnone => + simp only [getValueCast?_eraseKey_self hl, hnone] + · next hsome => + rw [hsome, getValueCast?_insertEntry_self] + · next heq => + rw [alterKey] + split + · next hnone => + simp only [heq, hnone, hl, beq_iff_eq, getValueCast?_eraseKey, ite_false, Bool.false_eq_true, + reduceIte] + · next hsome => + simp only [beq_iff_eq, getValueCast?_insertEntry, dite_false, heq, Bool.false_eq_true] + +theorem getValueCast_alterKey (k k' : α) (f : Option (β k) → Option (β k)) + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) : + getValueCast k' (alterKey k f l) hc = + if h : k == k' then + haveI hc' : (f (getValueCast? k l)).isSome := by + rwa [containsKey_alterKey hl, if_pos h] at hc + cast (congrArg β (eq_of_beq h)) <| (f (getValueCast? k l)).get hc' + else + haveI hc' : containsKey k' l := by rwa [containsKey_alterKey hl, if_neg h] at hc + getValueCast k' l hc' := by + have := getValueCast?_alterKey k k' f l hl + rw [getValueCast?_eq_some_getValueCast hc] at this + split + · next heq => + cases eq_of_beq heq + apply Option.some_inj.mp + simp_all + · next heq => + apply Option.some_inj.mp + simp_all only [Bool.false_eq_true, Function.comp_apply, dite_false] + rw [getValueCast?_eq_some_getValueCast] + +theorem getValueCast_alterKey_self (k : α) (f : Option (β k) → Option (β k)) + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l)) : + haveI hc' : (f (getValueCast? k l)).isSome := by + rwa [containsKey_alterKey hl, beq_self_eq_true] at hc + getValueCast k (alterKey k f l) hc = (f (getValueCast? k l)).get hc' := by + rw [getValueCast_alterKey _ _ _ _ hl] + simp + +theorem getValueCast!_alterKey {k k' : α} [Inhabited (β k')] {f : Option (β k) → Option (β k)} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCast! k' (alterKey k f l) = + if heq : k == k' then + (f (getValueCast? k l)).map (cast (congrArg β <| eq_of_beq heq)) |>.get! + else + getValueCast! k' l := by + simp only [hl, getValueCast!_eq_getValueCast?, getValueCast?_alterKey, beq_iff_eq, + Function.comp_apply] + split + · next heq => + cases eq_of_beq heq + simp only [cast_eq, Option.map_cast_apply] + · rfl + +theorem getValueCastD_alterKey {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : getValueCastD k' (alterKey k f l) fallback = + if heq : k == k' then + f (getValueCast? k l) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + getValueCastD k' l fallback := by + simp only [getValueCastD_eq_getValueCast?, hl, getValueCast?_alterKey, beq_iff_eq, + Function.comp_apply, apply_dite (Option.getD · fallback), Option.map_cast_apply] + +theorem getKey?_alterKey {k k' : α} {f : Option (β k) → Option (β k)} (l : List ((a : α) × β a)) + (hl : DistinctKeys l) : + getKey? k' (alterKey k f l) = + if k == k' then + if (f (getValueCast? k l)).isSome then some k else none + else + getKey? k' l := by + rw [alterKey] + split <;> next heq => simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry] + +theorem getKey!_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKey! k' (alterKey k f l) = + if k == k' then + if (f (getValueCast? k l)).isSome then k else default + else + getKey! k' l := by + simp only [getKey!_eq_getKey?, hl, getKey?_alterKey, beq_iff_eq] + split + · next heq => + cases eq_of_beq heq + split <;> rfl + · next heq => + rfl + +theorem getKey_alterKey [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) : + getKey k' (alterKey k f l) hc = + if heq : k == k' then + k + else + haveI h' : containsKey k' l := by rwa [containsKey_alterKey hl, if_neg heq] at hc + getKey k' l h' := by + have := getKey?_alterKey (f := f) (k' := k') _ hl + rw [getKey?_eq_some_getKey hc] at this + split + · next heq => + cases eq_of_beq heq + apply Option.some_inj.mp + simp_all + · next heq => + apply Option.some_inj.mp + simp_all only [Bool.false_eq_true, ite_false] + rw [getKey?_eq_some_getKey] + +theorem getKeyD_alterKey {k k' fallback : α} {f : Option (β k) → Option (β k)} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKeyD k' (alterKey k f l) fallback = + if k == k' then + if (f (getValueCast? k l)).isSome then k else fallback + else + getKeyD k' l fallback := by + simp only [hl, getKeyD_eq_getKey?, getKey?_alterKey, beq_iff_eq, Function.comp_apply] + split + · next heq => + cases eq_of_beq heq + split <;> rfl + · rfl + +end Dependent namespace Const +variable [BEq α] + variable {β : Type v} /-- Internal implementation detail of the hash map -/ @@ -2882,8 +3061,8 @@ def alterKey [BEq α] (k : α) (f : Option β → Option β) | 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 = +theorem length_alterKey {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 @@ -2892,9 +3071,41 @@ theorem length_alterKey [BEq α] [EquivBEq α] {k : α} {f : Option β → Optio 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 +theorem length_alterKey' {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : + (alterKey k f l).length = + if containsKey k l && (f (getValue? k l)).isNone then + l.length - 1 + else if !containsKey k l && (f (getValue? k l)).isSome then + l.length + 1 + else + l.length := by + rw [alterKey] + cases h : containsKey k l <;> split <;> split <;> simp_all [length_eraseKey, length_insertEntry] + +theorem length_alterKey_eq_add_one {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} + (h : containsKey k l = false) (h' : (f (getValue? k l)).isSome) : + (alterKey k f l).length = l.length + 1 := by + simp [length_alterKey', h, h'] + +theorem length_alterKey_eq_sub_one {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} + (h : containsKey k l) (h' : (f (getValue? k l)).isNone) : + (alterKey k f l).length = l.length - 1 := by + simp [length_alterKey', h, h'] + +theorem length_alterKey_eq_self {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} + (h : containsKey k l) (h' : (f (getValue? k l)).isSome) : + (alterKey k f l).length = l.length := by + simp [length_alterKey', h, Option.isSome_iff_ne_none.mp h'] + +theorem length_alterKey_eq_self' {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} + (h : containsKey k l = false) (h' : (f (getValue? k l)).isNone) : + (alterKey k f l).length = l.length := by + simp [length_alterKey', h, h'] + +theorem alterKey_cons_perm {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 @@ -2912,30 +3123,41 @@ theorem alterKey_cons_perm [BEq α] [EquivBEq α] {k : α} {f : Option β → Op · 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') : +theorem isEmpty_alterKey_eq_isEmpty_eraseKey {k : α} {f : Option β → Option β} + {l : List ((_ : α) × β)} : + (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValue? k l)).isNone) := by + simp only [alterKey, List.isEmpty_eq_true] + split <;> { next heq => simp [heq] } + +theorem isEmpty_alterKey {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)} : + (alterKey k f l).isEmpty = ((l.isEmpty || (l.length == 1 && containsKey k l)) && + (f (getValue? k l)).isNone) := by + rw [isEmpty_alterKey_eq_isEmpty_eraseKey, isEmpty_eraseKey] + +theorem alterKey_of_perm [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 +theorem alterKey_append_of_containsKey_right_eq_false {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 β} : +theorem alterKey_nil {a : α} {f : Option β → Option β} : alterKey a f [] = match f none with - | none => [] - | some b => [⟨a, b⟩] := rfl +| none => [] +| some b => [⟨a, b⟩] := rfl -theorem containsKey_alterKey_self [BEq α] [EquivBEq α] {a : α} {f : Option β → Option β} +theorem containsKey_alterKey_self [EquivBEq α] {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : - containsKey a (alterKey a f l) ↔ (f (getValue? a l)).isSome := by + 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] @@ -2948,87 +3170,161 @@ theorem containsKey_alterKey_self [BEq α] [EquivBEq α] {a : α} {f : Option β · 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 : β} +theorem mem_alterKey_of_key_not_beq [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {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 + 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] + split <;> simp only + [mem_eraseKey_of_key_beq_eq_false p hne, mem_insertEntry_of_key_beq_eq_false 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] +theorem containsKey_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} + {l : List ((_ : α) × β)} (hl : DistinctKeys l) : + containsKey k' (alterKey k f l) = + if k == k' then + f (getValue? k l) |>.isSome + else + containsKey k' l := by + split + · next h => + rw [← containsKey_congr h] + exact containsKey_alterKey_self hl + · next h => + rw [alterKey] split - · rfl - · rw [containsKey_replaceEntry] + · next heq => + simp only [containsKey_eraseKey_of_false (Bool.not_eq_true _ ▸ h)] + · next heq => + simp_all only [Bool.not_eq_true, containsKey_insertEntry, Bool.false_or] + +theorem getValue?_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β) + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue? k' (alterKey k f l) = + if k == k' then + f (getValue? k l) + else + getValue? k' l := by + split + · next heq => + rw [alterKey] + split + · next hnone => + simp only [getValue?_eraseKey_of_beq hl heq, hnone] + · next hsome => + rw [hsome, getValue?_insertEntry_of_beq heq] + · next heq => + rw [alterKey] + split + · next hnone => + simp only [heq, hnone, hl, beq_iff_eq, getValue?_eraseKey, ite_false, Bool.false_eq_true, + reduceIte] + · next hsome => + simp only [getValue?_insertEntry, heq, Bool.false_eq_true, reduceIte] + +theorem getValue_alterKey [EquivBEq α] (k k' : α) (f : Option β → Option β) (l : List ((_ : α) × β)) + (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) : + getValue k' (alterKey k f l) hc = + if h : k == k' then + haveI hc' : (f (getValue? k l)).isSome := by rwa [containsKey_alterKey hl, if_pos h] at hc + (f (getValue? k l)).get hc' + else + haveI hc' : containsKey k' l := by rwa [containsKey_alterKey hl, if_neg h] at hc + getValue k' l hc' := by + have := getValue?_alterKey k k' f l hl + rw [getValue?_eq_some_getValue hc] at this + split + · next heq => + apply Option.some_inj.mp + simp_all + · next heq => + apply Option.some_inj.mp + simp_all only [Bool.false_eq_true, ite_false] + rw [getValue?_eq_some_getValue] + +theorem getValue_alterKey_self [EquivBEq α] (k : α) (f : Option β → Option β) + (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k (alterKey k f l)) : + haveI hc' : (f (getValue? k l)).isSome := by rwa [containsKey_alterKey hl, BEq.refl] at hc + getValue k (alterKey k f l) hc = (f (getValue? k l)).get hc' := by + rw [getValue_alterKey _ _ _ _ hl] + simp + +theorem getValue!_alterKey [EquivBEq α] {k k' : α} [Inhabited β] {f : Option β → Option β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getValue! k' (alterKey k f l) = + if k == k' then + (f (getValue? k l)).get! + else + getValue! k' l := by + simp only [hl, getValue!_eq_getValue?, getValue?_alterKey, beq_iff_eq, Function.comp_apply, + apply_ite Option.get!] + +theorem getValueD_alterKey [EquivBEq α] {k k' : α} {fallback : β} {f : Option β → Option β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getValueD k' (alterKey k f l) fallback = + if k == k' then + f (getValue? k l) |>.getD fallback + else + getValueD k' l fallback := by + simp only [hl, getValueD_eq_getValue?, getValue?_alterKey, beq_iff_eq, Function.comp_apply, + apply_ite (Option.getD · fallback)] + +theorem getKey?_alterKey [EquivBEq α] {k k' : α} {f : Option β → Option β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : + getKey? k' (alterKey k f l) = + if k == k' then + if (f (getValue? k l)).isSome then some k else none + else + getKey? k' l := by + rw [alterKey] + split <;> next heq => simp [hl, heq, getKey?_eraseKey, getKey?_insertEntry] + +theorem getKey!_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getKey! k' (alterKey k f l) = + if k == k' then + if (f (getValue? k l)).isSome then k else default + else + getKey! k' l := by + simp [hl, getKey!_eq_getKey?, getKey?_alterKey, apply_ite Option.get!] + +theorem getKey_alterKey [EquivBEq α] [Inhabited α] {k k' : α} {f : Option β → Option β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) (hc : containsKey k' (alterKey k f l)) : + getKey k' (alterKey k f l) hc = + if heq : k == k' then + k + else + haveI h' : containsKey k' l := by rwa [containsKey_alterKey hl, if_neg heq] at hc + getKey k' l h' := by + have := getKey?_alterKey (f := f) (k := k) (k' := k') _ hl + rw [getKey?_eq_some_getKey hc] at this + split + · next heq => + apply Option.some_inj.mp + simp_all + · next heq => + apply Option.some_inj.mp + simp_all only [Bool.false_eq_true, ite_false] + rw [getKey?_eq_some_getKey] + +theorem getKeyD_alterKey [EquivBEq α] {k k' fallback : α} {f : Option β → Option β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getKeyD k' (alterKey k f l) fallback = + if k == k' then + if (f (getValue? k l)).isSome then k else fallback + else + getKeyD k' l fallback := by + simp only [hl, getKeyD_eq_getKey?, getKey?_alterKey, beq_iff_eq, Function.comp_apply] + split + · next heq => + split <;> rfl + · rfl end Const -theorem DistinctKeys.constAlterKey {β : Type v} [BEq α] [EquivBEq α] {a : α} +theorem constAlterKey_eq_alterKey [BEq α] [LawfulBEq α] {β : Type v} {k : α} + {f : Option β → Option β} {l : List ((_ : α) × β)} : Const.alterKey k f l = alterKey k f l := by + rw [alterKey, Const.alterKey, getValue?_eq_getValueCast?] + cases f (getValueCast? k l) <;> rfl + +theorem DistinctKeys.constAlterKey [BEq α] [EquivBEq α] {β : Type v} {a : α} {f : Option β → Option β} {l : List ((_ : α) × β)} (hl : DistinctKeys l) : DistinctKeys (List.Const.alterKey a f l) := by dsimp only [List.Const.alterKey] @@ -3036,4 +3332,349 @@ theorem DistinctKeys.constAlterKey {β : Type v} [BEq α] [EquivBEq α] {a : α} · exact DistinctKeys.eraseKey hl · exact DistinctKeys.insertEntry hl +end Alter + +section Modify + +/-- 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 isEmpty_modifyKey [BEq α] [LawfulBEq α] (k : α) (f : β k → β k) (l : List ((a : α) × β a)) : + (modifyKey k f l).isEmpty = l.isEmpty := by + match l with + | [] => simp [modifyKey] + | a :: as => + simp only [modifyKey, replaceEntry, cond_eq_if] + repeat' split <;> simp + +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 [BEq α] [LawfulBEq α] (k 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] + +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 getValueCast?_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l): + getValueCast? k' (modifyKey k f l) = + if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((getValueCast? k l).map f)) + else + getValueCast? k' l := by + simp [modifyKey_eq_alterKey, getValueCast?_alterKey, hl] + +@[simp] +theorem getValueCast?_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getValueCast? k (modifyKey k f l) = (getValueCast? k l).map f := by + simp [getValueCast?_modifyKey, hl] + +theorem getValueCast_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) : + getValueCast k' (modifyKey k f l) h = + if heq : k == k' then + haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← eq_of_beq heq] at h + cast (congrArg β (eq_of_beq heq)) <| f (getValueCast k l h') + else + haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h + getValueCast k' l h' := by + simp only [modifyKey_eq_alterKey, getValueCast_alterKey, hl] + split + · next heq => + cases eq_of_beq heq + haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← eq_of_beq heq] at h + simp [getValueCast?_eq_some_getValueCast, h'] + · rfl + +@[simp] +theorem getValueCast_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l)} : + haveI h' : containsKey k l := by rwa [containsKey_modifyKey] at h + getValueCast k (modifyKey k f l) h = f (getValueCast k l h') := by + simp [getValueCast_modifyKey, hl] + +theorem getValueCast!_modifyKey [BEq α] [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] + {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getValueCast! k' (modifyKey k f l) = + if heq : k == k' then + getValueCast? k l |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + getValueCast! k' l := by + simp only [modifyKey_eq_alterKey, getValueCast!_alterKey, hl] + +@[simp] +theorem getValueCast!_modifyKey_self [BEq α] [LawfulBEq α] {k : α} [Inhabited (β k)] + {f : β k → β k} (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getValueCast! k (modifyKey k f l) = ((getValueCast? k l).map f).get! := by + simp [getValueCast!_modifyKey, hl, List.cast_eq_id, List.function_id_comp] + +theorem getValueCastD_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getValueCastD k' (modifyKey k f l) fallback = + if heq : k == k' then + getValueCast? k l |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + getValueCastD k' l fallback := by + simp [modifyKey_eq_alterKey, getValueCastD_alterKey, hl] + +@[simp] +theorem getValueCastD_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getValueCastD k (modifyKey k f l) fallback = ((getValueCast? k l).map f).getD fallback := by + simp [getValueCastD_modifyKey, hl, List.cast_eq_id, List.function_id_comp] + +theorem getKey?_modifyKey [BEq α] [LawfulBEq α] {k k' : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKey? k' (modifyKey k f l) = + if k == k' then + if containsKey k l then some k else none + else + getKey? k' l := by + simp [modifyKey_eq_alterKey, getKey?_alterKey, containsKey_eq_isSome_getValueCast?, hl] + +theorem getKey?_modifyKey_self [BEq α] [LawfulBEq α] {k : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKey? k (modifyKey k f l) = if containsKey k l then some k else none := by + simp [getKey?_modifyKey, hl] + +theorem getKey!_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKey! k' (modifyKey k f l) = + if k == k' then + if containsKey k l then k else default + else + getKey! k' l := by + simp [modifyKey_eq_alterKey, getKey!_alterKey, containsKey_eq_isSome_getValueCast?, hl] + +theorem getKey!_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKey! k (modifyKey k f l) = if containsKey k l then k else default := by + simp [getKey!_modifyKey, hl] + +theorem getKey_modifyKey [BEq α] [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) : + getKey k' (modifyKey k f l) h = + if k == k' then + k + else + haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h + getKey k' l h' := by + simp [modifyKey_eq_alterKey, getKey_alterKey, hl, ← dite_eq_ite] + +@[simp] +theorem getKey_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) : + getKey k (modifyKey k f l) h = k := by + simp [getKey_modifyKey, hl] + +theorem getKeyD_modifyKey [BEq α] [LawfulBEq α] {k k' fallback : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKeyD k' (modifyKey k f l) fallback = + if k == k' then + if containsKey k l then k else fallback + else + getKeyD k' l fallback := by + simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValueCast?, hl] + +theorem getKeyD_modifyKey_self [BEq α] [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} + (l : List ((a : α) × β a)) (hl : DistinctKeys l) : + getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by + simp [getKeyD_modifyKey, hl] + +namespace Const + +variable {β : Type v} [BEq α] + +/-- Internal implementation detail of the hash map -/ +def modifyKey (k : α) (f : β → β) + (l : List ((_ : α) × β)) : List ((_ : α) × β) := + match getValue? k l with + | none => l + | some v => replaceEntry k (f v) l + +theorem isEmpty_modifyKey (k : α) (f : β → β) (l : List ((_ : α) × β)) : + (modifyKey k f l).isEmpty = l.isEmpty := by + match l with + | [] => simp [modifyKey] + | a :: as => + simp only [modifyKey, replaceEntry, cond_eq_if] + repeat' split <;> simp + +theorem modifyKey_eq_alterKey (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 (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 [EquivBEq α] (k 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] + +theorem getValue?_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : + getValue? k' (modifyKey k f l) = + if k == k' then + (getValue? k l).map f + else + getValue? k' l := by + simp [modifyKey_eq_alterKey, getValue?_alterKey, hl] + +@[simp] +theorem getValue?_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : getValue? k (modifyKey k f l) = (getValue? k l).map f := by + simp [getValue?_modifyKey, hl] + +theorem getValue_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) : + getValue k' (modifyKey k f l) h = + if heq : k == k' then + haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← containsKey_congr heq] at h + f (getValue k l h') + else + haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h + getValue k' l h' := by + simp only [modifyKey_eq_alterKey, getValue_alterKey, hl] + split + · next heq => + haveI h' : containsKey k l := by rwa [containsKey_modifyKey, ← containsKey_congr heq] at h + simp [getValue?_eq_some_getValue, h'] + · rfl + +@[simp] +theorem getValue_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) {h : containsKey k (modifyKey k f l)} : + haveI h' : containsKey k l := by rwa [containsKey_modifyKey] at h + getValue k (modifyKey k f l) h = f (getValue k l h') := by + simp [getValue_modifyKey, hl] + +theorem getValue!_modifyKey [EquivBEq α] {k k' : α} [hi : Inhabited β] {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getValue! k' (modifyKey k f l) = + if k == k' then + getValue? k l |>.map f |>.get! + else + getValue! k' l := by + simp [modifyKey_eq_alterKey, getValue!_alterKey, hl] + +@[simp] +theorem getValue!_modifyKey_self [EquivBEq α] {k : α} [Inhabited (β)] {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getValue! k (modifyKey k f l) = ((getValue? k l).map f).get! := by + simp [getValue!_modifyKey, hl] + +theorem getValueD_modifyKey [EquivBEq α] {k k' : α} {fallback : β} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getValueD k' (modifyKey k f l) fallback = + if k == k' then + getValue? k l |>.map f |>.getD fallback + else + getValueD k' l fallback := by + simp [modifyKey_eq_alterKey, getValueD_alterKey, hl] + +@[simp] +theorem getValueD_modifyKey_self [EquivBEq α] {k : α} {fallback : β} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getValueD k (modifyKey k f l) fallback = ((getValue? k l).map f).getD fallback := by + simp [getValueD_modifyKey, hl] + +theorem getKey?_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : + getKey? k' (modifyKey k f l) = + if k == k' then + if containsKey k l then some k else none + else + getKey? k' l := by + simp [modifyKey_eq_alterKey, getKey?_alterKey, containsKey_eq_isSome_getValue?, hl] + +theorem getKey?_modifyKey_self [EquivBEq α] {k : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : + getKey? k (modifyKey k f l) = if containsKey k l then some k else none := by + simp [getKey?_modifyKey, hl] + +theorem getKey!_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : getKey! k' (modifyKey k f l) = + if k == k' then + if containsKey k l then k else default + else + getKey! k' l := by + simp [modifyKey_eq_alterKey, getKey!_alterKey, containsKey_eq_isSome_getValue?, hl] + +theorem getKey!_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getKey! k (modifyKey k f l) = if containsKey k l then k else default := by + simp [getKey!_modifyKey, hl] + +theorem getKey_modifyKey [EquivBEq α] [Inhabited α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) (h : containsKey k' (modifyKey k f l)) : + getKey k' (modifyKey k f l) h = + if k == k' then + k + else + haveI h' : containsKey k' l := by rwa [containsKey_modifyKey] at h + getKey k' l h' := by + simp [modifyKey_eq_alterKey, getKey_alterKey, hl] + rfl + +@[simp] +theorem getKey_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) : + getKey k (modifyKey k f l) h = k := by + simp [getKey_modifyKey, hl] + +theorem getKeyD_modifyKey [EquivBEq α] {k k' fallback : α} {f : β → β} (l : List ((_ : α) × β)) + (hl : DistinctKeys l) : + getKeyD k' (modifyKey k f l) fallback = + if k == k' then + if containsKey k l then k else fallback + else + getKeyD k' l fallback := by + simp [modifyKey_eq_alterKey, getKeyD_alterKey, containsKey_eq_isSome_getValue?, hl] + +theorem getKeyD_modifyKey_self [EquivBEq α] [Inhabited α] {k fallback : α} {f : β → β} + (l : List ((_ : α) × β)) (hl : DistinctKeys l) : + getKeyD k (modifyKey k f l) fallback = if containsKey k l then k else fallback := by + simp [getKeyD_modifyKey, hl] + +end Const + +theorem constModifyKey_eq_modifyKey {β : Type v} [BEq α] [LawfulBEq α] {k : α} {f : β → β} + {l : List ((_ : α) × β)} : + Const.modifyKey k f l = modifyKey k f l := by + rw [modifyKey, Const.modifyKey, getValue?_eq_getValueCast?] + cases getValueCast? k l <;> rfl + +end Modify + end List diff --git a/src/Std/Data/DHashMap/Internal/Model.lean b/src/Std/Data/DHashMap/Internal/Model.lean index 4020b4a310..b75ca1b1c1 100644 --- a/src/Std/Data/DHashMap/Internal/Model.lean +++ b/src/Std/Data/DHashMap/Internal/Model.lean @@ -486,7 +486,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) 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] + containsKey_modifyKey, h, reduceIte] · rfl theorem modify_eq_modifyₘ [BEq α] [Hashable α] [LawfulBEq α] (m : Raw₀ α β) (a : α) @@ -516,7 +516,7 @@ theorem modify_eq_alter [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun 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] + Const.containsKey_modifyKey, h, reduceIte] · rfl theorem modify_eq_modifyₘ [BEq α] [Hashable α] [EquivBEq α] (m : Raw₀ α (fun _ => β)) (a : α) diff --git a/src/Std/Data/DHashMap/Internal/Raw.lean b/src/Std/Data/DHashMap/Internal/Raw.lean index 4b28a7153e..64845fc3ca 100644 --- a/src/Std/Data/DHashMap/Internal/Raw.lean +++ b/src/Std/Data/DHashMap/Internal/Raw.lean @@ -212,6 +212,14 @@ theorem ofList_eq [BEq α] [Hashable α] {l : List ((a : α) × β a)} : simp only [Raw.ofList, Raw.insertMany, (Raw.WF.empty).size_buckets_pos ∅, ↓reduceDIte] congr +theorem alter_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : Option (β k) → Option (β k)} : + m.alter k f = Raw₀.alter ⟨m, h.size_buckets_pos⟩ k f := by + simp [Raw.alter, h.size_buckets_pos] + +theorem modify_eq [BEq α] [LawfulBEq α] [Hashable α] {m : Raw α β} (h : m.WF) {k : α} {f : β k → β k} : + m.modify k f = Raw₀.modify ⟨m, h.size_buckets_pos⟩ k f := by + simp [Raw.modify, h.size_buckets_pos] + section variable {β : Type v} @@ -299,6 +307,14 @@ theorem Const.getThenInsertIfNew?_fst_val [BEq α] [Hashable α] {m : Raw₀ α (Raw₀.Const.getThenInsertIfNew? m a b).1 := by simp [Raw.Const.getThenInsertIfNew?, m.2] +theorem Const.alter_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : Option β → Option β} : + Raw.Const.alter m k f = Raw₀.Const.alter ⟨m, h.size_buckets_pos⟩ k f := by + simp [Raw.Const.alter, h.size_buckets_pos] + +theorem Const.modify_eq [BEq α] [EquivBEq α] [Hashable α] {m : Raw α (fun _ => β)} (h : m.WF) {k : α} {f : β → β} : + Raw.Const.modify m k f = Raw₀.Const.modify ⟨m, h.size_buckets_pos⟩ k f := by + simp [Raw.Const.modify, h.size_buckets_pos] + end end Raw diff --git a/src/Std/Data/DHashMap/Internal/RawLemmas.lean b/src/Std/Data/DHashMap/Internal/RawLemmas.lean index f04f940323..8e7581b9e6 100644 --- a/src/Std/Data/DHashMap/Internal/RawLemmas.lean +++ b/src/Std/Data/DHashMap/Internal/RawLemmas.lean @@ -71,7 +71,9 @@ variable [BEq α] [Hashable α] scoped macro "wf_trivial" : tactic => `(tactic| repeat (first | apply Raw₀.wfImp_insert | apply Raw₀.wfImp_insertIfNew | apply Raw₀.wfImp_insertMany - | apply Raw₀.Const.wfImp_insertMany| apply Raw₀.Const.wfImp_insertManyIfNewUnit + | apply Raw₀.Const.wfImp_insertMany | apply Raw₀.Const.wfImp_insertManyIfNewUnit + | apply Raw₀.wfImp_alter | apply Raw₀.wfImp_modify + | apply Raw₀.Const.wfImp_alter | apply Raw₀.Const.wfImp_modify | apply Raw₀.wfImp_erase | apply Raw.WF.out | assumption | apply Raw₀.wfImp_empty | apply Raw.WFImp.distinct | apply Raw.WF.empty₀)) @@ -92,8 +94,9 @@ private def queryNames : Array Name := private def modifyNames : Array Name := #[``toListModel_insert, ``toListModel_erase, ``toListModel_insertIfNew, - ``toListModel_insertMany_list, ``Const.toListModel_insertMany_list, - ``Const.toListModel_insertManyIfNewUnit_list] + ``toListModel_insertMany_list, ``Const.toListModel_insertMany_list, + ``Const.toListModel_insertManyIfNewUnit_list, ``toListModel_alter, + ``toListModel_modify, ``Const.toListModel_alter, ``Const.toListModel_modify] private def congrNames : MacroM (Array (TSyntax `term)) := do return #[← `(_root_.List.Perm.isEmpty_eq), ← `(containsKey_of_perm), @@ -310,7 +313,7 @@ theorem get_erase [LawfulBEq α] (h : m.1.WF) {k a : α} {h'} : (m.erase k).get a h' = m.get a (contains_of_contains_erase _ h h') := by simp_to_model using List.getValueCast_eraseKey -theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h} : m.get? a = some (m.get a h) := by +theorem get?_eq_some_get [LawfulBEq α] (h : m.1.WF) {a : α} {h'} : m.get? a = some (m.get a h') := by simp_to_model using List.getValueCast?_eq_some_getValueCast namespace Const @@ -592,8 +595,8 @@ theorem getKey_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} { (m.erase k).getKey a h' = m.getKey a (contains_of_contains_erase _ h h') := by simp_to_model using List.getKey_eraseKey -theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h} : - m.getKey? a = some (m.getKey a h) := by +theorem getKey?_eq_some_getKey [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {h'} : + m.getKey? a = some (m.getKey a h') := by simp_to_model using List.getKey?_eq_some_getKey theorem getKey!_empty {a : α} [Inhabited α] {c} : @@ -1312,12 +1315,6 @@ theorem getD_insertManyIfNewUnit_list end Const -end Raw₀ - -namespace Raw₀ - -variable [BEq α] [Hashable α] - @[simp] theorem insertMany_empty_list_nil : (insertMany empty ([] : List ((a : α) × (β a)))).1 = empty := by @@ -1720,6 +1717,550 @@ theorem getD_insertManyIfNewUnit_empty_list end Const +section Alter + +theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] (h : m.1.WF) {k : α} + {f : Option (β k) → Option (β k)} : + (m.alter k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (m.get? k)).isNone) := by + simp_to_model using List.isEmpty_alterKey_eq_isEmpty_eraseKey + +@[simp] +theorem isEmpty_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).1.isEmpty = (((m.1.isEmpty || (m.1.size == 1 && m.contains k))) && + (f (m.get? k)).isNone) := by + simp_to_model using List.isEmpty_alterKey + +theorem contains_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' := by + simp_to_model using List.containsKey_alterKey + +theorem size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).1.size = + if m.contains k && (f (m.get? k)).isNone then + m.1.size - 1 + else if !m.contains k && (f (m.get? k)).isSome then + m.1.size + 1 + else + m.1.size := by + simp_to_model using List.length_alterKey' + +theorem size_alter_eq_add_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} + (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isSome) : + (m.alter k f).1.size = m.1.size + 1 := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_sub_one [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} + (h₁ : m.contains k) (h₂ : (f (m.get? k)).isNone) : + (m.alter k f).1.size = m.1.size - 1 := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] (h : m.1.WF) {k : α} + {f : Option (β k) → Option (β k)} (h₁ : m.contains k = false) (h₂ : (f (m.get? k)).isNone) : + (m.alter k f).1.size = m.1.size := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_self_of_mem [LawfulBEq α] (h : m.1.WF) {k : α} + {f : Option (β k) → Option (β k)} (h₁ : m.contains k) (h₂ : (f (m.get? k)).isSome) : + (m.alter k f).1.size = m.1.size := by + simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂] + +theorem size_alter_le_size [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).1.size ≤ m.1.size + 1 := by + simp [size_alter, h] + split <;> try split + all_goals omega + +theorem size_le_size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} : + m.1.size - 1 ≤ (m.alter k f).1.size := by + simp [size_alter, h] + split <;> try split + all_goals omega + +theorem get?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).get? k' = + if h : k == k' then + cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k)) + else + m.get? k' := by + simp_to_model using List.getValueCast?_alterKey + +theorem get_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} + (hc : (m.alter k f).contains k') : + (m.alter k f).get k' hc = + if heq : k == k' then + haveI h' : (f (m.get? k)).isSome := by rwa [contains_alter _ h, if_pos heq] at hc + cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h' + else + haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc + m.get k' h' := by + simp_to_model using List.getValueCast_alterKey + +theorem get_alter_self [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option (β k) → Option (β k)} + {hc : (m.alter k f).contains k} : + haveI h' : (f (m.get? k)).isSome := by rwa [contains_alter _ h, beq_self_eq_true] at hc + (m.alter k f).get k hc = (f (m.get? k)).get h' := by + simp_to_model using List.getValueCast_alterKey_self + +theorem get!_alter [LawfulBEq α] {k k' : α} (h : m.1.WF) [Inhabited (β k')] + {f : Option (β k) → Option (β k)} : + (m.alter k f).get! k' = + if heq : k == k' then + (f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := by + simp_to_model using List.getValueCast!_alterKey + +theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} (h : m.1.WF) + {f : Option (β k) → Option (β k)} : + (m.alter k f).getD k' fallback = + if heq : k == k' then + f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := by + simp_to_model using List.getValueCastD_alterKey + +private theorem cast_eq_id {α : Type u} : cast (rfl : α = α) = id := by rfl + +theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} (h : m.1.WF) + {f : Option (β k) → Option (β k)} : + (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback := by + simp only [getD_alter, h, beq_self_eq_true, reduceDIte, cast_eq_id, Option.map_id_fun, id_eq] + +theorem getKey?_alter [LawfulBEq α] (h : m.1.WF) {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKey? k' = + if k == k' then + if (f (m.get? k)).isSome then some k else none + else + m.getKey? k' := by + simp_to_model using List.getKey?_alterKey + +theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF) + {f : Option (β k) → Option (β k)} : (m.alter k f).getKey! k' = + if k == k' then + if (f (m.get? k)).isSome then k else default + else + m.getKey! k' := by + simp_to_model using List.getKey!_alterKey + +theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} (h : m.1.WF) + {f : Option (β k) → Option (β k)} (hc : (m.alter k f).contains k') : + (m.alter k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc + m.getKey k' h' := by + simp_to_model using List.getKey_alterKey + +theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} (h : m.1.WF) + {f : Option (β k) → Option (β k)} : + (m.alter k f).getKeyD k' fallback = + if k == k' then + if (f (m.get? k)).isSome then k else fallback + else + m.getKeyD k' fallback := by + simp_to_model using List.getKeyD_alterKey + +namespace Const + +variable {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α (fun _ => β)) + +theorem isEmpty_alter_eq_isEmpty_erase (h : m.1.WF) {k : α} {f : Option β → Option β} : + (Const.alter m k f).1.isEmpty = ((m.erase k).1.isEmpty && (f (Const.get? m k)).isNone) := by + simp_to_model using List.Const.isEmpty_alterKey_eq_isEmpty_eraseKey + +@[simp] +theorem isEmpty_alter (h : m.1.WF) {k : α} {f : Option β → Option β} : + (Const.alter m k f).1.isEmpty = ((m.1.isEmpty || (m.1.size == 1 && m.contains k)) && + (f (Const.get? m k)).isNone) := by + simp_to_model using List.Const.isEmpty_alterKey + +theorem contains_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} : + (Const.alter m k f).contains k' = + if k == k' then + (f (Const.get? m k)).isSome + else + m.contains k' := by + simp_to_model using List.Const.containsKey_alterKey + +theorem size_alter (h : m.1.WF) {k : α} {f : Option β → Option β} : + (Const.alter m k f).1.size = + if m.contains k && (f (Const.get? m k)).isNone then + m.1.size - 1 + else if !m.contains k && (f (Const.get? m k)).isSome then + m.1.size + 1 + else + m.1.size := by + simp_to_model using List.Const.length_alterKey' + +theorem size_alter_eq_add_one (h : m.1.WF) {k : α} {f : Option β → Option β} + (h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isSome) : + (Const.alter m k f).1.size = m.1.size + 1 := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_sub_one (h : m.1.WF) {k : α} {f : Option β → Option β} + (h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isNone) : + (Const.alter m k f).1.size = m.1.size - 1 := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_self_of_not_mem (h : m.1.WF) {k : α} {f : Option β → Option β} + (h₁ : m.contains k = false) (h₂ : (f (Const.get? m k)).isNone) : + (Const.alter m k f).1.size = m.1.size := by + simp [size_alter, h, h₁, h₂] + +theorem size_alter_eq_self_of_mem (h : m.1.WF) {k : α} {f : Option β → Option β} + (h₁ : m.contains k) (h₂ : (f (Const.get? m k)).isSome) : + (Const.alter m k f).1.size = m.1.size := by + simp [size_alter, h, h₁, Option.isSome_iff_ne_none.mp h₂] + +theorem size_alter_le_size [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option β → Option β} : + (Const.alter m k f).1.size ≤ m.1.size + 1 := by + simp [size_alter, h] + split <;> try split + all_goals omega + +theorem size_le_size_alter [LawfulBEq α] (h : m.1.WF) {k : α} {f : Option β → Option β} : + m.1.size - 1 ≤ (Const.alter m k f).1.size := by + simp [size_alter, h] + split <;> try split + all_goals omega + +theorem get?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} : + Const.get? (Const.alter m k f) k' = + if k == k' then + f (Const.get? m k) + else + Const.get? m k' := by + simp_to_model using List.Const.getValue?_alterKey + +theorem get_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} + (hc : (Const.alter m k f).contains k') : + Const.get (Const.alter m k f) k' hc = + if heq : k == k' then + haveI h' : (f (Const.get? m k)).isSome := by rwa [contains_alter _ h, if_pos heq] at hc + (f (Const.get? m k)).get <| h' + else + haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc + Const.get m k' h' := by + simp_to_model using List.Const.getValue_alterKey + +theorem get_alter_self (h : m.1.WF) {k : α} {f : Option β → Option β} + {hc : (Const.alter m k f).contains k} : + haveI h' : (f (Const.get? m k)).isSome := by rwa [contains_alter _ h, BEq.refl] at hc + Const.get (Const.alter m k f) k hc = (f (Const.get? m k)).get h' := by + simp_to_model using List.Const.getValue_alterKey_self + +theorem get!_alter {k k' : α} (h : m.1.WF) [Inhabited β] {f : Option β → Option β} : + Const.get! (Const.alter m k f) k' = + if k == k' then + (f (Const.get? m k)).get! + else + Const.get! m k' := by + simp_to_model using List.Const.getValue!_alterKey + +theorem getD_alter {k k' : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} : + Const.getD (Const.alter m k f) k' fallback = + if k == k' then + f (Const.get? m k) |>.getD fallback + else + Const.getD m k' fallback := by + simp_to_model using List.Const.getValueD_alterKey + +theorem getD_alter_self {k : α} {fallback : β} (h : m.1.WF) {f : Option β → Option β} : + Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by + simp only [h, getD_alter, BEq.refl, reduceIte] + +theorem getKey?_alter (h : m.1.WF) {k k' : α} {f : Option β → Option β} : + (Const.alter m k f).getKey? k' = + if k == k' then + if (f (Const.get? m k)).isSome then some k else none + else + m.getKey? k' := by + simp_to_model using List.Const.getKey?_alterKey + +theorem getKey!_alter [Inhabited α] {k k' : α} (h : m.1.WF) {f : Option β → Option β} : + (Const.alter m k f).getKey! k' = + if k == k' then + if (f (Const.get? m k)).isSome then k else default + else + m.getKey! k' := by + simp_to_model using List.Const.getKey!_alterKey + +theorem getKey_alter [Inhabited α] {k k' : α} (h : m.1.WF) {f : Option β → Option β} + (hc : (Const.alter m k f).contains k') : + (Const.alter m k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : m.contains k' := by rwa [contains_alter _ h, if_neg heq] at hc + m.getKey k' h' := by + simp_to_model using List.Const.getKey_alterKey + +theorem getKeyD_alter {k k' fallback : α} (h : m.1.WF) {f : Option β → Option β} : + (Const.alter m k f).getKeyD k' fallback = + if k == k' then + if (f (Const.get? m k)).isSome then k else fallback + else + m.getKeyD k' fallback := by + simp_to_model using List.Const.getKeyD_alterKey + +end Const + +end Alter + +section Modify + +variable [LawfulBEq α] + +@[simp] +theorem isEmpty_modify (h : m.1.WF) {k : α} {f : β k → β k} : + (m.modify k f).1.isEmpty = m.1.isEmpty := by + simp_to_model using List.isEmpty_modifyKey + +theorem contains_modify (h : m.1.WF) {k k' : α} {f : β k → β k} : + (m.modify k f).contains k' = m.contains k' := by + simp_to_model using List.containsKey_modifyKey + +theorem size_modify (h : m.1.WF) {k : α} {f : β k → β k} : + (m.modify k f).1.size = m.1.size := by + simp_to_model using List.length_modifyKey + +theorem get?_modify (h : m.1.WF) {k k' : α} {f : β k → β k} : + (m.modify k f).get? k' = + if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f)) + else + m.get? k' := by + simp_to_model using List.getValueCast?_modifyKey + +@[simp] +theorem get?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} : + (m.modify k f).get? k = (m.get? k).map f := by + simp_to_model using List.getValueCast?_modifyKey_self + +theorem get_modify (h : m.1.WF) {k k' : α} {f : β k → β k} + (hc : (m.modify k f).contains k') : + (m.modify k f).get k' hc = + if heq : k == k' then + haveI h' : m.contains k := by rwa [contains_modify _ h, ← eq_of_beq heq] at hc + cast (congrArg β (eq_of_beq heq)) <| f (m.get k h') + else + haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc + m.get k' h' := by + simp_to_model using List.getValueCast_modifyKey + +@[simp] +theorem get_modify_self (h : m.1.WF) {k : α} {f : β k → β k} {hc : (m.modify k f).contains k} : + haveI h' : m.contains k := by rwa [contains_modify _ h] at hc + (m.modify k f).get k hc = f (m.get k h') := by + simp_to_model using List.getValueCast_modifyKey_self + +theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} : + (m.modify k f).get! k' = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := by + simp_to_model using List.getValueCast!_modifyKey + +@[simp] +theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β k)] {f : β k → β k} : + (m.modify k f).get! k = ((m.get? k).map f).get! := by + simp_to_model using List.getValueCast!_modifyKey_self + +theorem getD_modify (h : m.1.WF) {k k' : α} {fallback : β k'} {f : β k → β k} : + (m.modify k f).getD k' fallback = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := by + simp_to_model using List.getValueCastD_modifyKey + +@[simp] +theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β k} {f : β k → β k} : + (m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback := by + simp_to_model using List.getValueCastD_modifyKey_self + +theorem getKey?_modify (h : m.1.WF) {k k' : α} {f : β k → β k} : + (m.modify k f).getKey? k' = + if k == k' then + if m.contains k then some k else none + else + m.getKey? k' := by + simp_to_model using List.getKey?_modifyKey + +theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β k → β k} : + (m.modify k f).getKey? k = if m.contains k then some k else none := by + simp_to_model using List.getKey?_modifyKey_self + +theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k} : + (m.modify k f).getKey! k' = + if k == k' then + if m.contains k then k else default + else + m.getKey! k' := by + simp_to_model using List.getKey!_modifyKey + +theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k} : + (m.modify k f).getKey! k = if m.contains k then k else default := by + simp_to_model using List.getKey!_modifyKey_self + +theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β k → β k} + (hc : (m.modify k f).contains k') : + (m.modify k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc + m.getKey k' h' := by + simp_to_model using List.getKey_modifyKey + +@[simp] +theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β k → β k} + (hc : (m.modify k f).contains k) : (m.modify k f).getKey k hc = k := by + simp_to_model using List.getKey_modifyKey_self + +theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β k → β k} : + (m.modify k f).getKeyD k' fallback = + if k == k' then + if m.contains k then k else fallback + else + m.getKeyD k' fallback := by + simp_to_model using List.getKeyD_modifyKey + +theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β k → β k} : + (m.modify k f).getKeyD k fallback = if m.contains k then k else fallback := by + simp_to_model using List.getKeyD_modifyKey_self + +namespace Const + +variable {β : Type v} [EquivBEq α] [LawfulHashable α] (m : Raw₀ α (fun _ => β)) +omit [LawfulBEq α] + +@[simp] +theorem isEmpty_modify (m : Raw₀ α (fun _ => β)) (h : m.1.WF) {k : α} {f : β → β} : + (Const.modify m k f).1.isEmpty = m.1.isEmpty := by + simp_to_model using List.Const.isEmpty_modifyKey + +theorem contains_modify (h : m.1.WF) {k k' : α} {f : β → β} : + (Const.modify m k f).contains k' = m.contains k' := by + simp_to_model using List.Const.containsKey_modifyKey + +theorem size_modify (h : m.1.WF) {k : α} {f : β → β} : + (Const.modify m k f).1.size = m.1.size := by + simp_to_model using List.Const.length_modifyKey + +theorem get?_modify (h : m.1.WF) {k k' : α} {f : β → β} : + Const.get? (Const.modify m k f) k' = + if k == k' then + (Const.get? m k).map f + else + Const.get? m k' := by + simp_to_model using List.Const.getValue?_modifyKey + +@[simp] +theorem get?_modify_self (h : m.1.WF) {k : α} {f : β → β} : + Const.get? (Const.modify m k f) k = (Const.get? m k).map f := by + simp_to_model using List.Const.getValue?_modifyKey_self + +theorem get_modify (h : m.1.WF) {k k' : α} {f : β → β} + (hc : (Const.modify m k f).contains k') : + Const.get (Const.modify m k f) k' hc = + if heq : k == k' then + haveI h' : m.contains k := by rwa [contains_modify _ h, ← contains_congr _ h heq] at hc + f (Const.get m k h') + else + haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc + Const.get m k' h' := by + simp_to_model using List.Const.getValue_modifyKey + +@[simp] +theorem get_modify_self (h : m.1.WF) {k : α} {f : β → β} {hc : (Const.modify m k f).contains k} : + haveI h' : m.contains k := by rwa [contains_modify _ h] at hc + Const.get (Const.modify m k f) k hc = f (Const.get m k h') := by + simp_to_model using List.Const.getValue_modifyKey_self + +theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited β] {f : β → β} : + Const.get! (Const.modify m k f) k' = + if k == k' then + Const.get? m k |>.map f |>.get! + else + Const.get! m k' := by + simp_to_model using List.Const.getValue!_modifyKey + +@[simp] +theorem get!_modify_self (h : m.1.WF) {k : α} [Inhabited (β)] {f : β → β} : + Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! := by + simp_to_model using List.Const.getValue!_modifyKey_self + +theorem getD_modify (h : m.1.WF) {k k' : α} {fallback : β} {f : β → β} : + Const.getD (Const.modify m k f) k' fallback = + if k == k' then + Const.get? m k |>.map f |>.getD fallback + else + Const.getD m k' fallback := by + simp_to_model using List.Const.getValueD_modifyKey + +@[simp] +theorem getD_modify_self (h : m.1.WF) {k : α} {fallback : β} {f : β → β} : + Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback := by + simp_to_model using List.Const.getValueD_modifyKey_self + +theorem getKey?_modify (h : m.1.WF) {k k' : α} {f : β → β} : + (Const.modify m k f).getKey? k' = + if k == k' then + if m.contains k then some k else none + else + m.getKey? k' := by + simp_to_model using List.Const.getKey?_modifyKey + +theorem getKey?_modify_self (h : m.1.WF) {k : α} {f : β → β} : + (Const.modify m k f).getKey? k = if m.contains k then some k else none := by + simp_to_model using List.Const.getKey?_modifyKey_self + +theorem getKey!_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β} : + (Const.modify m k f).getKey! k' = + if k == k' then + if m.contains k then k else default + else + m.getKey! k' := by + simp_to_model using List.Const.getKey!_modifyKey + +theorem getKey!_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β} : + (Const.modify m k f).getKey! k = if m.contains k then k else default := by + simp_to_model using List.Const.getKey!_modifyKey_self + +theorem getKey_modify (h : m.1.WF) [Inhabited α] {k k' : α} {f : β → β} + (hc : (Const.modify m k f).contains k') : + (Const.modify m k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : m.contains k' := by rwa [contains_modify _ h] at hc + m.getKey k' h' := by + simp_to_model using List.Const.getKey_modifyKey + +@[simp] +theorem getKey_modify_self (h : m.1.WF) [Inhabited α] {k : α} {f : β → β} + (hc : (Const.modify m k f).contains k) : (Const.modify m k f).getKey k hc = k := by + simp_to_model using List.Const.getKey_modifyKey_self + +theorem getKeyD_modify (h : m.1.WF) {k k' fallback : α} {f : β → β} : + (Const.modify m k f).getKeyD k' fallback = + if k == k' then + if m.contains k then k else fallback + else + m.getKeyD k' fallback := by + simp_to_model using List.Const.getKeyD_modifyKey + +theorem getKeyD_modify_self (h : m.1.WF) [Inhabited α] {k fallback : α} {f : β → β} : + (Const.modify m k f).getKeyD k fallback = if m.contains k then k else fallback := by + simp_to_model using List.Const.getKeyD_modifyKey_self + +end Const + +end Modify + end Raw₀ end Std.DHashMap.Internal diff --git a/src/Std/Data/DHashMap/Internal/WF.lean b/src/Std/Data/DHashMap/Internal/WF.lean index d441e5bf36..82448656a5 100644 --- a/src/Std/Data/DHashMap/Internal/WF.lean +++ b/src/Std/Data/DHashMap/Internal/WF.lean @@ -641,6 +641,12 @@ theorem toListModel_alterₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashabl rw [insertEntry_of_containsKey_eq_false] exact 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 [alter_eq_alterₘ] + exact toListModel_alterₘ h + 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 @@ -691,13 +697,19 @@ theorem wfImp_modify [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β} (h namespace Const -variable {β : Type v} +variable {β : Type v} {m : Raw₀ α (fun _ => β)} -theorem wfImp_modifyₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] {m : Raw₀ α (fun _ => β)} +theorem toListModel_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (h : Raw.WFImp m.1) + {a : α} {f : β → β} : + Perm (toListModel (Const.modify m a f).1.2) (Const.modifyKey a f (toListModel m.1.2)) := by + rw [Const.modify_eq_alter, Const.modifyKey_eq_alterKey] + exact Const.toListModel_alter h + +theorem wfImp_modifyₘ [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (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 _ => β)} +theorem wfImp_modify [BEq α] [EquivBEq α] [Hashable α] [LawfulHashable α] (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 diff --git a/src/Std/Data/DHashMap/Lemmas.lean b/src/Std/Data/DHashMap/Lemmas.lean index 7d2eebadce..90edc69978 100644 --- a/src/Std/Data/DHashMap/Lemmas.lean +++ b/src/Std/Data/DHashMap/Lemmas.lean @@ -1866,4 +1866,669 @@ theorem getD_unitOfList end Const +variable {m : DHashMap α β} + +section Alter + +theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone) := + Raw₀.isEmpty_alter_eq_isEmpty_erase _ m.2 + +@[simp] +theorem isEmpty_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) := + Raw₀.isEmpty_alter _ m.2 + +theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} : + (m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' := + Raw₀.contains_alter ⟨_, _⟩ m.2 + +theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} : + k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m := by + simp only [mem_iff_contains, contains_alter, beq_iff_eq, Bool.ite_eq_true_distrib] + +theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : k == k') : + k' ∈ m.alter k f ↔ (f (m.get? k)).isSome := by + rw [mem_alter, if_pos h] + +@[simp] +theorem contains_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).contains k = (f (m.get? k)).isSome := by + simp only [contains_alter, beq_self_eq_true, reduceIte] + +@[simp] +theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + k ∈ m.alter k f ↔ (f (m.get? k)).isSome := by + rw [mem_iff_contains, contains_alter_self] + +theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : (k == k') = false) : (m.alter k f).contains k' = m.contains k' := by + simp only [contains_alter, h, Bool.false_eq_true, reduceIte] + +theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h] + +theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).size = + if m.contains k && (f (m.get? k)).isNone then + m.size - 1 + else if !m.contains k && (f (m.get? k)).isSome then + m.size + 1 + else + m.size := + Raw₀.size_alter ⟨m.1, _⟩ m.2 + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : k ∉ m) (h' : (f (m.get? k)).isSome) : + (m.alter k f).size = m.size + 1 := by + rw [mem_iff_contains, Bool.not_eq_true] at h + exact Raw₀.size_alter_eq_add_one ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : k ∈ m) (h' : (f (m.get? k)).isNone) : + (m.alter k f).size = m.size - 1 := + Raw₀.size_alter_eq_sub_one ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : k ∉ m) (h' : (f (m.get? k)).isNone) : (m.alter k f).size = m.size := by + rw [mem_iff_contains, Bool.not_eq_true] at h + exact Raw₀.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : k ∈ m) (h' : (f (m.get? k)).isSome) : (m.alter k f).size = m.size := + Raw₀.size_alter_eq_self_of_mem ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).size ≤ m.size + 1 := + Raw₀.size_alter_le_size ⟨m.1, _⟩ m.2 + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + m.size - 1 ≤ (m.alter k f).size := + Raw₀.size_le_size_alter ⟨m.1, _⟩ m.2 + +theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).get? k' = + if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))) + else + m.get? k' := + Raw₀.get?_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).get? k = f (m.get? k) := by + simp only [get?_alter, beq_self_eq_true, reduceDIte, Function.comp_apply, cast_eq] + +theorem get_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + {h : k' ∈ m.alter k f} : + (m.alter k f).get k' h = + if heq : k == k' then + haveI h' : (f (m.get? k)).isSome := mem_alter_of_beq heq |>.mp h + cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + m.get k' h' := + Raw₀.get_alter ⟨m.1, _⟩ m.2 h + +@[simp] +theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + {h : k ∈ m.alter k f} : + haveI h' : (f (m.get? k)).isSome := mem_alter_self.mp h + (m.alter k f).get k h = (f (m.get? k)).get h' := + Raw₀.get_alter_self ⟨m.1, _⟩ m.2 + +theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] + {f : Option (β k) → Option (β k)} : (m.alter k f).get! k' = + if heq : k == k' then + (f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := + Raw₀.get!_alter ⟨m.1, _⟩ m.2 + +private theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) : + Option.map (cast h) x = cast (congrArg Option h) x := by + cases h; cases x <;> simp + +@[simp] +theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)} : + (m.alter k f).get! k = (f (m.get? k)).get! := by + simp only [get!_alter, beq_self_eq_true, reduceDIte, cast_eq, Option.map_cast_apply] + +theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} : + (m.alter k f).getD k' fallback = + if heq : k == k' then + f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := + Raw₀.getD_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} : + (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback := + Raw₀.getD_alter_self ⟨m.1, _⟩ m.2 + +theorem getKey?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKey? k' = + if k == k' then + if (f (m.get? k)).isSome then some k else none + else + m.getKey? k' := + Raw₀.getKey?_alter ⟨m.1, _⟩ m.2 + +theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none := by + simp only [getKey?_alter, beq_self_eq_true, ↓reduceIte] + +theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKey! k' = + if k == k' then + if (f (m.get? k)).isSome then k else default + else + m.getKey! k' := by + simp [getKey!_eq_get!_getKey?, getKey?_alter] + split + · next heq => + cases eq_of_beq heq + split <;> rfl + · next heq => + rfl + +theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default := by + simp only [getKey!_alter, beq_self_eq_true, reduceIte] + +theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} + {h : k' ∈ m.alter k f} : + (m.alter k f).getKey k' h = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + m.getKey k' h' := + Raw₀.getKey_alter ⟨m.1, _⟩ m.2 h + +@[simp] +theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} + {h : k ∈ m.alter k f} : (m.alter k f).getKey k h = k := by + simp [getKey_alter] + +theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} : + (m.alter k f).getKeyD k' fallback = + if k == k' then + if (f (m.get? k)).isSome then k else fallback + else + m.getKeyD k' fallback := + Raw₀.getKeyD_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α} + {f : Option (β k) → Option (β k)} : + (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback := by + simp [getKeyD_alter] + +namespace Const + +variable {β : Type v} {m : DHashMap α (fun _ => β)} + +theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} + {f : Option β → Option β} : + (Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Const.get? m k)).isNone) := + Raw₀.Const.isEmpty_alter_eq_isEmpty_erase _ m.2 + +@[simp] +theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (Const.alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) + && (f (Const.get? m k)).isNone) := + Raw₀.Const.isEmpty_alter _ m.2 + +theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} : + (Const.alter m k f).contains k' = + if k == k' then (f (Const.get? m k)).isSome else m.contains k' := + Raw₀.Const.contains_alter ⟨m.1, _⟩ m.2 + +theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} : + k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m := by + simp only [mem_iff_contains, contains_alter, Bool.ite_eq_true_distrib] + +theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by + rw [mem_alter, if_pos h] + +@[simp] +theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (Const.alter m k f).contains k = (f (Const.get? m k)).isSome := by + simp only [contains_alter, BEq.refl, reduceIte] + +@[simp] +theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by + rw [mem_iff_contains, contains_alter_self] + +theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : (k == k') = false) : + (Const.alter m k f).contains k' = m.contains k' := by + simp only [contains_alter, h, Bool.false_eq_true, reduceIte] + +theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : (k == k') = false) : k' ∈ Const.alter m k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_alter_of_beq_eq_false, h] + +theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} : + (Const.alter m k f).size = + if m.contains k && (f (Const.get? m k)).isNone then + m.size - 1 + else if !m.contains k && (f (Const.get? m k)).isSome then + m.size + 1 + else + m.size := + Raw₀.Const.size_alter ⟨m.1, _⟩ m.2 + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∉ m) (h' : (f (Const.get? m k)).isSome) : + (Const.alter m k f).size = m.size + 1 := by + rw [mem_iff_contains, Bool.not_eq_true] at h + exact Raw₀.Const.size_alter_eq_add_one ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∈ m) (h' : (f (Const.get? m k)).isNone) : + (Const.alter m k f).size = m.size - 1 := + Raw₀.Const.size_alter_eq_sub_one ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∉ m) (h' : (f (Const.get? m k)).isNone) : (Const.alter m k f).size = m.size := by + rw [mem_iff_contains, Bool.not_eq_true] at h + exact Raw₀.Const.size_alter_eq_self_of_not_mem ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∈ m) (h' : (f (Const.get? m k)).isSome) : (Const.alter m k f).size = m.size := + Raw₀.Const.size_alter_eq_self_of_mem ⟨m.1, _⟩ m.2 h h' + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} : + (Const.alter m k f).size ≤ m.size + 1 := + Raw₀.Const.size_alter_le_size ⟨m.1, _⟩ m.2 + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} : + m.size - 1 ≤ (Const.alter m k f).size := + Raw₀.Const.size_le_size_alter ⟨m.1, _⟩ m.2 + +theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : + Const.get? (Const.alter m k f) k' = + if k == k' then + f (Const.get? m k) + else + Const.get? m k' := + Raw₀.Const.get?_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + Const.get? (Const.alter m k f) k = f (Const.get? m k) := by + simp [get?_alter] + +theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + {h : k' ∈ Const.alter m k f} : + Const.get (Const.alter m k f) k' h = + if heq : k == k' then + haveI h' : (f (Const.get? m k)).isSome := mem_alter_of_beq heq |>.mp h + f (Const.get? m k) |>.get h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + Const.get m k' h' := + Raw₀.Const.get_alter ⟨m.1, _⟩ m.2 h + +@[simp] +theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + {h : k ∈ Const.alter m k f} : + haveI h' : (f (Const.get? m k)).isSome := mem_alter_self.mp h + Const.get (Const.alter m k f) k h = (f (Const.get? m k)).get h' := by + simp [get_alter] + +theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] + {f : Option β → Option β} : Const.get! (Const.alter m k f) k' = + if k == k' then + f (Const.get? m k) |>.get! + else + Const.get! m k' := + Raw₀.Const.get!_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] + {f : Option β → Option β} : Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get! := by + simp [get!_alter] + +theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} + {f : Option β → Option β} : + Const.getD (Const.alter m k f) k' fallback = + if k == k' then + f (Const.get? m k) |>.getD fallback + else + Const.getD m k' fallback := + Raw₀.Const.getD_alter ⟨m.1, _⟩ m.2 + +@[simp] +theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} + {f : Option β → Option β} : + Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by + simp [getD_alter] + +theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : + (Const.alter m k f).getKey? k' = + if k == k' then + if (f (Const.get? m k)).isSome then some k else none + else + m.getKey? k' := + Raw₀.Const.getKey?_alter ⟨m.1, _⟩ m.2 + +theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none := by + simp [getKey?_alter] + +theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} : (Const.alter m k f).getKey! k' = + if k == k' then + if (f (Const.get? m k)).isSome then k else default + else + m.getKey! k' := + Raw₀.Const.getKey!_alter ⟨m.1, _⟩ m.2 + +theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} : + (Const.alter m k f).getKey! k = if (f (Const.get? m k)).isSome then k else default := by + simp [getKey!_alter] + +theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} {h : k' ∈ Const.alter m k f} : + (Const.alter m k f).getKey k' h = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + m.getKey k' h' := + Raw₀.Const.getKey_alter ⟨m.1, _⟩ m.2 h + +@[simp] +theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} {h : k ∈ Const.alter m k f} : + (Const.alter m k f).getKey k h = k := by + simp [getKey_alter] + +theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} : + (Const.alter m k f).getKeyD k' fallback = + if k == k' then + if (f (Const.get? m k)).isSome then k else fallback + else + m.getKeyD k' fallback := + Raw₀.Const.getKeyD_alter ⟨m.1, _⟩ m.2 + +theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : Option β → Option β} : + (Const.alter m k f).getKeyD k fallback = + if (f (Const.get? m k)).isSome then k else fallback := by + simp [getKeyD_alter] + +end Const + +end Alter + +section Modify + +@[simp] +theorem isEmpty_modify [LawfulBEq α] {k : α} {f : β k → β k} : + (m.modify k f).isEmpty = m.isEmpty := + Raw₀.isEmpty_modify _ m.2 + +@[simp] +theorem contains_modify [LawfulBEq α] {k k': α} {f : β k → β k} : + (m.modify k f).contains k' = m.contains k' := + Raw₀.contains_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} : k' ∈ m.modify k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_modify] + +@[simp] +theorem size_modify [LawfulBEq α] {k : α} {f : β k → β k} : (m.modify k f).size = m.size := + Raw₀.size_modify ⟨m.1, _⟩ m.2 + +theorem get?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} : + (m.modify k f).get? k' = if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f)) + else + m.get? k' := + Raw₀.get?_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem get?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} : + (m.modify k f).get? k = (m.get? k).map f := + Raw₀.get?_modify_self ⟨m.1, _⟩ m.2 + +theorem get_modify [LawfulBEq α] {k k' : α} {f : β k → β k} + (h : k' ∈ m.modify k f) : + (m.modify k f).get k' h = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h + cast (congrArg β (eq_of_beq heq)) <| f (m.get k h') + else + haveI h' : k' ∈ m := mem_modify.mp h + m.get k' h' := + Raw₀.get_modify ⟨m.1, _⟩ m.2 h + +@[simp] +theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} {h : k ∈ m.modify k f} : + haveI h' : k ∈ m := mem_modify.mp h + (m.modify k f).get k h = f (m.get k h') := + Raw₀.get_modify_self ⟨m.1, _⟩ m.2 + +theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} : + (m.modify k f).get! k' = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := + Raw₀.get!_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem get!_modify_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} : + (m.modify k f).get! k = ((m.get? k).map f).get! := + Raw₀.get!_modify_self ⟨m.1, _⟩ m.2 + +theorem getD_modify [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} : + (m.modify k f).getD k' fallback = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := + Raw₀.getD_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem getD_modify_self [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} : + (m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback := + Raw₀.getD_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} : + (m.modify k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := + Raw₀.getKey?_modify ⟨m.1, _⟩ m.2 + +theorem getKey?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} : + (m.modify k f).getKey? k = if k ∈ m then some k else none := + Raw₀.getKey?_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey!_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} : + (m.modify k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := + Raw₀.getKey!_modify ⟨m.1, _⟩ m.2 + +theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} : + (m.modify k f).getKey! k = if k ∈ m then k else default := + Raw₀.getKey!_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} + {h : k' ∈ m.modify k f} : + (m.modify k f).getKey k' h = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify.mp h + m.getKey k' h' := + Raw₀.getKey_modify ⟨m.1, _⟩ m.2 h + +@[simp] +theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} + {h : k ∈ m.modify k f} : (m.modify k f).getKey k h = k := + Raw₀.getKey_modify_self ⟨m.1, _⟩ m.2 h + +theorem getKeyD_modify [LawfulBEq α] {k k' fallback : α} {f : β k → β k} : + (m.modify k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := + Raw₀.getKeyD_modify ⟨m.1, _⟩ m.2 + +theorem getKeyD_modify_self [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} : + (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback := + Raw₀.getKeyD_modify_self ⟨m.1, _⟩ m.2 + +namespace Const + +variable {β : Type v} {m : DHashMap α (fun _ => β)} + +@[simp] +theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (Const.modify m k f).isEmpty = m.isEmpty := + Raw₀.Const.isEmpty_modify _ m.2 + +@[simp] +theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} : + (Const.modify m k f).contains k' = m.contains k' := + Raw₀.Const.contains_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} : + k' ∈ Const.modify m k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_modify] + +@[simp] +theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (Const.modify m k f).size = m.size := + Raw₀.Const.size_modify ⟨m.1, _⟩ m.2 + +theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : + Const.get? (Const.modify m k f) k' = if k == k' then + Const.get? m k |>.map f + else + Const.get? m k' := + Raw₀.Const.get?_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + Const.get? (Const.modify m k f) k = (Const.get? m k).map f := + Raw₀.Const.get?_modify_self ⟨m.1, _⟩ m.2 + +theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} + {h : k' ∈ Const.modify m k f} : + Const.get (Const.modify m k f) k' h = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h + f (Const.get m k h') + else + haveI h' : k' ∈ m := mem_modify.mp h + Const.get m k' h' := + Raw₀.Const.get_modify ⟨m.1, _⟩ m.2 h + +@[simp] +theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} + {h : k ∈ Const.modify m k f} : + haveI h' : k ∈ m := mem_modify.mp h + Const.get (Const.modify m k f) k h = f (Const.get m k h') := + Raw₀.Const.get_modify_self ⟨m.1, _⟩ m.2 + +theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} : + Const.get! (Const.modify m k f) k' = + if k == k' then + Const.get? m k |>.map f |>.get! + else + Const.get! m k' := + Raw₀.Const.get!_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} : + Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! := + Raw₀.Const.get!_modify_self ⟨m.1, _⟩ m.2 + +theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} : + Const.getD (Const.modify m k f) k' fallback = + if k == k' then + Const.get? m k |>.map f |>.getD fallback + else + Const.getD m k' fallback := + Raw₀.Const.getD_modify ⟨m.1, _⟩ m.2 + +@[simp] +theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} : + Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback := + Raw₀.Const.getD_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : + (Const.modify m k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := + Raw₀.Const.getKey?_modify ⟨m.1, _⟩ m.2 + +theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (Const.modify m k f).getKey? k = if k ∈ m then some k else none := + Raw₀.Const.getKey?_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} : + (Const.modify m k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := + Raw₀.Const.getKey!_modify ⟨m.1, _⟩ m.2 + +theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} : + (Const.modify m k f).getKey! k = if k ∈ m then k else default := + Raw₀.Const.getKey!_modify_self ⟨m.1, _⟩ m.2 + +theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + {h : k' ∈ Const.modify m k f} : + (Const.modify m k f).getKey k' h = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify.mp h + m.getKey k' h' := + Raw₀.Const.getKey_modify ⟨m.1, _⟩ m.2 h + +@[simp] +theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + {h : k ∈ Const.modify m k f} : (Const.modify m k f).getKey k h = k := + Raw₀.Const.getKey_modify_self ⟨m.1, _⟩ m.2 h + +theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} : + (Const.modify m k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := + Raw₀.Const.getKeyD_modify ⟨m.1, _⟩ m.2 + +theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β} : + (Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback := + Raw₀.Const.getKeyD_modify_self ⟨m.1, _⟩ m.2 + +end Const + +end Modify + end Std.DHashMap diff --git a/src/Std/Data/DHashMap/Raw.lean b/src/Std/Data/DHashMap/Raw.lean index a5acdd419e..5836b56f11 100644 --- a/src/Std/Data/DHashMap/Raw.lean +++ b/src/Std/Data/DHashMap/Raw.lean @@ -296,6 +296,45 @@ to get anything out of the hash map. @[inline] def isEmpty (m : Raw α β) : Bool := m.size == 0 +/-- +Modifies in place the value associated with a given key. + +This function ensures that the value is used linearly. +-/ +@[inline] def modify [BEq α] [LawfulBEq α] [Hashable α] (m : Raw α β) (a : α) (f : β a → β a) : + Raw α β := + if h : 0 < m.buckets.size then + Raw₀.modify ⟨m, h⟩ a f + else + ∅ + +@[inline, inherit_doc Raw.modify] def Const.modify [BEq α] [EquivBEq α] [Hashable α] {β : Type v} + (m : Raw α (fun _ => β)) (a : α) (f : β → β) : Raw α (fun _ => β) := + if h : 0 < m.buckets.size then + Raw₀.Const.modify ⟨m, h⟩ a f + else + ∅ + +/-- +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. +-/ +@[inline] def alter [BEq α] [LawfulBEq α] [Hashable α] (m : Raw α β) + (a : α) (f : Option (β a) → Option (β a)) : Raw α β := + if h : 0 < m.buckets.size then + Raw₀.alter ⟨m, h⟩ a f + else + ∅ + +@[inline, inherit_doc Raw.alter] def Const.alter [BEq α] [EquivBEq α] [Hashable α] {β : Type v} + (m : Raw α (fun _ => β)) (a : α) (f : Option β → Option β) : Raw α (fun _ => β) := + if h : 0 < m.buckets.size then + Raw₀.Const.alter ⟨m, h⟩ a f + else + ∅ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ diff --git a/src/Std/Data/DHashMap/RawLemmas.lean b/src/Std/Data/DHashMap/RawLemmas.lean index 147a2ce3bd..e11b6a29c9 100644 --- a/src/Std/Data/DHashMap/RawLemmas.lean +++ b/src/Std/Data/DHashMap/RawLemmas.lean @@ -62,7 +62,8 @@ private def baseNames : Array Name := ``insertMany_eq, ``insertMany_val, ``Const.insertMany_eq, ``Const.insertMany_val, ``Const.insertManyIfNewUnit_eq, ``Const.insertManyIfNewUnit_val, - ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq] + ``ofList_eq, ``Const.ofList_eq, ``Const.unitOfList_eq, + ``alter_eq, ``Const.alter_eq, ``modify_eq, ``Const.modify_eq] /-- Internal implementation detail of the hash map -/ scoped syntax "simp_to_raw" ("using" term)? : tactic @@ -1978,4 +1979,728 @@ theorem getD_unitOfList end Const end Raw +namespace Raw + +variable [BEq α] [Hashable α] {m : Raw α β} + +open Internal.Raw Internal.Raw₀ + +section Alter + +theorem isEmpty_alter_eq_isEmpty_erase [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone) := by + simp_to_raw using Raw₀.isEmpty_alter_eq_isEmpty_erase + +@[simp] +theorem isEmpty_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (m.get? k)).isNone) := by + simp_to_raw using Raw₀.isEmpty_alter + +theorem contains_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).contains k' = if k == k' then (f (m.get? k)).isSome else m.contains k' := by + simp_to_raw using Raw₀.contains_alter + +theorem mem_alter [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) : + k' ∈ m.alter k f ↔ if k == k' then (f (m.get? k)).isSome = true else k' ∈ m := by + simp [mem_iff_contains, contains_alter h] + +theorem mem_alter_of_beq [LawfulBEq α] {k k': α} {f : Option (β k) → Option (β k)} (h : m.WF) + (he : k == k') : k' ∈ m.alter k f ↔ (f (m.get? k)).isSome := by + rw [mem_alter h, if_pos he] + +@[simp] +theorem contains_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).contains k = (f (m.get? k)).isSome := by + simp only [contains_alter h, beq_self_eq_true, reduceIte] + +@[simp] +theorem mem_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + k ∈ m.alter k f ↔ (f (m.get? k)).isSome := by + rw [mem_iff_contains, contains_alter_self h] + +theorem contains_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (he : (k == k') = false) : (m.alter k f).contains k' = m.contains k' := by + simp only [contains_alter h, he, Bool.false_eq_true, reduceIte] + +theorem mem_alter_of_beq_eq_false [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (he : (k == k') = false) : k' ∈ m.alter k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he] + +theorem size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).size = + if m.contains k && (f (m.get? k)).isNone then + m.size - 1 + else if !m.contains k && (f (m.get? k)).isSome then + m.size + 1 + else + m.size := by + simp_to_raw using Raw₀.size_alter + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isSome) : + (m.alter k f).size = m.size + 1 := by + revert h₁ h₂ + simp only [mem_iff_contains, Bool.not_eq_true] + simp_to_raw using Raw₀.size_alter_eq_add_one + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isNone) : + (m.alter k f).size = m.size - 1 := by + revert h₁ h₂ + simp only [mem_iff_contains] + simp_to_raw using Raw₀.size_alter_eq_sub_one + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (m.get? k)).isNone) : + (m.alter k f).size = m.size := by + revert h₁ h₂ + simp only [mem_iff_contains, Bool.not_eq_true] + simp_to_raw using Raw₀.size_alter_eq_self_of_not_mem + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (m.get? k)).isSome) : + (m.alter k f).size = m.size := by + revert h₁ h₂ + simp only [mem_iff_contains] + simp_to_raw using Raw₀.size_alter_eq_self_of_mem + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).size ≤ m.size + 1 := by + simp_to_raw using Raw₀.size_alter_le_size + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + m.size - 1 ≤ (m.alter k f).size := by + simp_to_raw using Raw₀.size_le_size_alter ⟨m, h.size_buckets_pos⟩ + +theorem get?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).get? k' = if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) (f (m.get? k))) + else m.get? k' := by + simp_to_raw using Raw₀.get?_alter + +@[simp] +theorem get?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).get? k = f (m.get? k) := by + simp [get?_alter h] + +theorem get_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : m.WF) {hc : k' ∈ m.alter k f} : + (m.alter k f).get k' hc = + if heq : k == k' then + haveI h' : (f (m.get? k)).isSome := mem_alter_of_beq h heq |>.mp hc + cast (congrArg β (eq_of_beq heq)) <| (f (m.get? k)).get <| h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + m.get k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.get_alter + +@[simp] +theorem get_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) {hc : k ∈ m.alter k f} : + haveI h' : (f (m.get? k)).isSome := mem_alter_self h |>.mp hc + (m.alter k f).get k hc = (f (m.get? k)).get h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.get_alter_self + +theorem get!_alter [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] + {f : Option (β k) → Option (β k)} (h : m.WF) : (m.alter k f).get! k' = + if heq : k == k' then + (f (m.get? k)).map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := by + simp_to_raw using Raw₀.get!_alter + +private theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) : + Option.map (cast h) x = cast (congrArg Option h) x := by + cases h; cases x <;> simp + +@[simp] +theorem get!_alter_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).get! k = (f (m.get? k)).get! := by + simp [get!_alter h, Option.map_cast_apply] + +theorem getD_alter [LawfulBEq α] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).getD k' fallback = + if heq : k == k' then + f (m.get? k) |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := by + simp_to_raw using Raw₀.getD_alter + +@[simp] +theorem getD_alter_self [LawfulBEq α] {k : α} {fallback : β k} {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback := by + simp_to_raw using Raw₀.getD_alter_self + +theorem getKey?_alter [LawfulBEq α] {k k' : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).getKey? k' = + if k == k' then + if (f (m.get? k)).isSome then some k else none + else + m.getKey? k' := by + simp_to_raw using Raw₀.getKey?_alter + +theorem getKey?_alter_self [LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).getKey? k = if (f (m.get? k)).isSome then some k else none := by + simp [getKey?_alter h] + +theorem getKey!_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).getKey! k' = + if k == k' then + if (f (m.get? k)).isSome then k else default + else + m.getKey! k' := by + simp_to_raw using Raw₀.getKey!_alter + +theorem getKey!_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) : (m.alter k f).getKey! k = if (f (m.get? k)).isSome then k else default := by + simp [getKey!_alter h] + +theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)} + (h : m.WF) {hc : k' ∈ m.alter k f} : + (m.alter k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + m.getKey k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.getKey_alter + +@[simp] +theorem getKey_alter_self [LawfulBEq α] [Inhabited α] {k : α} {f : Option (β k) → Option (β k)} + (h : m.WF) {hc : k ∈ m.alter k f} : (m.alter k f).getKey k hc = k := by + simp [getKey_alter h] + +theorem getKeyD_alter [LawfulBEq α] {k k' fallback : α} {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).getKeyD k' fallback = + if k == k' then + if (f (m.get? k)).isSome then k else fallback + else + m.getKeyD k' fallback := by + simp_to_raw using Raw₀.getKeyD_alter + +@[simp] +theorem getKeyD_alter_self [LawfulBEq α] [Inhabited α] {k : α} {fallback : α} + {f : Option (β k) → Option (β k)} (h : m.WF) : + (m.alter k f).getKeyD k fallback = if (f (m.get? k)).isSome then k else fallback := by + simp [getKeyD_alter h] + +namespace Const + +variable {β : Type v} {m : Raw α (fun _ => β)} + +theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} + {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).isEmpty = ((m.erase k).isEmpty && (f (Const.get? m k)).isNone) := by + simp_to_raw using Raw₀.Const.isEmpty_alter_eq_isEmpty_erase + +@[simp] +theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && + (f (get? m k)).isNone) := by + simp_to_raw using Raw₀.Const.isEmpty_alter + +theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : m.WF) : (Const.alter m k f).contains k' = + if k == k' then (f (Const.get? m k)).isSome else m.contains k' := by + simp_to_raw using Raw₀.Const.contains_alter + +theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} (h : m.WF) : + k' ∈ Const.alter m k f ↔ if k == k' then (f (Const.get? m k)).isSome = true else k' ∈ m := by + simp only [mem_iff_contains, contains_alter h, Bool.ite_eq_true_distrib] + +theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : m.WF) (he : k == k') : k' ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by + rw [mem_alter h, if_pos he] + +@[simp] +theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : (Const.alter m k f).contains k = (f (Const.get? m k)).isSome := by + simp only [contains_alter h, BEq.refl, reduceIte] + +@[simp] +theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : k ∈ Const.alter m k f ↔ (f (Const.get? m k)).isSome := by + rw [mem_iff_contains, contains_alter_self h] + +theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) : + (Const.alter m k f).contains k' = m.contains k' := by + simp only [contains_alter h, he, Bool.false_eq_true, reduceIte] + +theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) : + k' ∈ Const.alter m k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_alter_of_beq_eq_false h, he] + +theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).size = + if m.contains k && (f (Const.get? m k)).isNone then + m.size - 1 + else if !m.contains k && (f (Const.get? m k)).isSome then + m.size + 1 + else + m.size := by + simp_to_raw using Raw₀.Const.size_alter + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isSome) : + (Const.alter m k f).size = m.size + 1 := by + revert h₁ h₂ + simp only [mem_iff_contains, Bool.not_eq_true] + simp_to_raw using Raw₀.Const.size_alter_eq_add_one + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isNone) : + (Const.alter m k f).size = m.size - 1 := by + revert h₁ h₂ + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.size_alter_eq_sub_one + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : m.WF) (h₁ : k ∉ m) (h₂ : (f (Const.get? m k)).isNone) : + (Const.alter m k f).size = m.size := by + revert h₁ h₂ + simp only [mem_iff_contains, Bool.not_eq_true] + simp_to_raw using Raw₀.Const.size_alter_eq_self_of_not_mem + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : m.WF) (h₁ : k ∈ m) (h₂ : (f (Const.get? m k)).isSome) : + (Const.alter m k f).size = m.size := by + revert h₁ h₂ + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.size_alter_eq_self_of_mem + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).size ≤ m.size + 1 := by + simp_to_raw using Raw₀.Const.size_alter_le_size + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + m.size - 1 ≤ (Const.alter m k f).size := by + simp_to_raw using Raw₀.Const.size_le_size_alter ⟨m, h.size_buckets_pos⟩ + +theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) : + Const.get? (Const.alter m k f) k' = + if k == k' then + f (Const.get? m k) + else + Const.get? m k' := by + simp_to_raw using Raw₀.Const.get?_alter + +@[simp] +theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : Const.get? (Const.alter m k f) k = f (Const.get? m k) := by + simp [get?_alter h] + +theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + (h : m.WF) {hc : k' ∈ Const.alter m k f} : + Const.get (Const.alter m k f) k' hc = + if heq : k == k' then + haveI h' : (f (Const.get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc + f (Const.get? m k) |>.get h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + Const.get m k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.get_alter + +@[simp] +theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) {hc : k ∈ Const.alter m k f} : + haveI h' : (f (Const.get? m k)).isSome := mem_alter_self h |>.mp hc + Const.get (Const.alter m k f) k hc = (f (Const.get? m k)).get h' := by + simp only [mem_iff_contains] at hc + revert hc + simp [get_alter h] + +theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] + {f : Option β → Option β} (h : m.WF) : Const.get! (Const.alter m k f) k' = + if k == k' then + f (Const.get? m k) |>.get! + else + Const.get! m k' := by + simp_to_raw using Raw₀.Const.get!_alter + +@[simp] +theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] + {f : Option β → Option β} (h : m.WF) : + Const.get! (Const.alter m k f) k = (f (Const.get? m k)).get! := by + simp [get!_alter h] + +theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : Option β → Option β} + (h : m.WF) : Const.getD (Const.alter m k f) k' fallback = + if k == k' then + f (Const.get? m k) |>.getD fallback + else + Const.getD m k' fallback := by + simp_to_raw using Raw₀.Const.getD_alter + +@[simp] +theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} + {f : Option β → Option β} (h : m.WF) : + Const.getD (Const.alter m k f) k fallback = (f (Const.get? m k)).getD fallback := by + simp [getD_alter h] + +theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + (h : m.WF) : (Const.alter m k f).getKey? k' = + if k == k' then + if (f (Const.get? m k)).isSome then some k else none + else + m.getKey? k' := by + simp_to_raw using Raw₀.Const.getKey?_alter + +theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : + (Const.alter m k f).getKey? k = if (f (Const.get? m k)).isSome then some k else none := by + simp [getKey?_alter h] + +theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} (h : m.WF) : (Const.alter m k f).getKey! k' = + if k == k' then + if (f (Const.get? m k)).isSome then k else default + else + m.getKey! k' := by + simp_to_raw using Raw₀.Const.getKey!_alter + +theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).getKey! k = if (f (Const.get? m k)).isSome then k else default := by + simp [getKey!_alter h] + +theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} (h : m.WF) {hc : k' ∈ Const.alter m k f} : + (Const.alter m k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + m.getKey k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.getKey_alter + +@[simp] +theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} (h : m.WF) {hc : k ∈ Const.alter m k f} : + (Const.alter m k f).getKey k hc = k := by + simp [getKey_alter h] + +theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} + (h : m.WF) : (Const.alter m k f).getKeyD k' fallback = + if k == k' then + if (f (Const.get? m k)).isSome then k else fallback + else + m.getKeyD k' fallback := by + simp_to_raw using Raw₀.Const.getKeyD_alter + +theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : Option β → Option β} (h : m.WF) : + (Const.alter m k f).getKeyD k fallback = if (f (Const.get? m k)).isSome then k else fallback := by + simp [getKeyD_alter h] + +end Const + +end Alter + +section Modify + +@[simp] +theorem isEmpty_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).isEmpty = m.isEmpty := by + simp_to_raw using Raw₀.isEmpty_modify + +@[simp] +theorem contains_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) : + (m.modify k f).contains k' = m.contains k' := by + simp_to_raw using Raw₀.contains_modify + +@[simp] +theorem mem_modify [LawfulBEq α] {k k': α} {f : β k → β k} (h : m.WF) : + k' ∈ m.modify k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_modify h] + +@[simp] +theorem size_modify [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).size = m.size := by + simp_to_raw using Raw₀.size_modify + +theorem get?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).get? k' = + if h : k == k' then + (cast (congrArg (Option ∘ β) (eq_of_beq h)) ((m.get? k).map f)) + else + m.get? k' := by + simp_to_raw using Raw₀.get?_modify + +@[simp] +theorem get?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).get? k = (m.get? k).map f := by + simp_to_raw using Raw₀.get?_modify_self + +theorem get_modify [LawfulBEq α] {k k' : α} {f : β k → β k} + (h : m.WF) {hc : k' ∈ m.modify k f} : + (m.modify k f).get k' hc = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc + cast (congrArg β (eq_of_beq heq)) <| f (m.get k h') + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + m.get k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.get_modify + +@[simp] +theorem get_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) {hc : k ∈ m.modify k f} : + haveI h' : k ∈ m := mem_modify h |>.mp hc + (m.modify k f).get k hc = f (m.get k h') := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.get_modify_self + +theorem get!_modify [LawfulBEq α] {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} (h : m.WF) : + (m.modify k f).get! k' = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get! + else + m.get! k' := by + simp_to_raw using Raw₀.get!_modify + +@[simp] +theorem get!_modify_self [LawfulBEq α] {k : α} [Inhabited (β k)] {f : β k → β k} (h : m.WF) : + (m.modify k f).get! k = ((m.get? k).map f).get! := by + simp_to_raw using Raw₀.get!_modify_self + +theorem getD_modify [LawfulBEq α] {k k' : α} {fallback : β k'} {f : β k → β k} (h : m.WF) : + (m.modify k f).getD k' fallback = + if heq : k == k' then + m.get? k |>.map f |>.map (cast (congrArg β <| eq_of_beq heq)) |>.getD fallback + else + m.getD k' fallback := by + simp_to_raw using Raw₀.getD_modify + +@[simp] +theorem getD_modify_self [LawfulBEq α] {k : α} {fallback : β k} {f : β k → β k} (h : m.WF) : + (m.modify k f).getD k fallback = ((m.get? k).map f).getD fallback := by + simp_to_raw using Raw₀.getD_modify_self + +theorem getKey?_modify [LawfulBEq α] {k k' : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKey?_modify + +theorem getKey?_modify_self [LawfulBEq α] {k : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKey? k = if k ∈ m then some k else none := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKey?_modify_self + +theorem getKey!_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKey!_modify + +theorem getKey!_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKey! k = if k ∈ m then k else default := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKey!_modify_self + +theorem getKey_modify [LawfulBEq α] [Inhabited α] {k k' : α} {f : β k → β k} + (h : m.WF) {hc : k' ∈ m.modify k f} : + (m.modify k f).getKey k' hc = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + m.getKey k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.getKey_modify + +@[simp] +theorem getKey_modify_self [LawfulBEq α] [Inhabited α] {k : α} {f : β k → β k} + (h : m.WF) {hc : k ∈ m.modify k f} : (m.modify k f).getKey k hc = k := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.getKey_modify_self + +theorem getKeyD_modify [LawfulBEq α] {k k' fallback : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKeyD_modify + +theorem getKeyD_modify_self [LawfulBEq α] [Inhabited α] {k fallback : α} {f : β k → β k} (h : m.WF) : + (m.modify k f).getKeyD k fallback = if k ∈ m then k else fallback := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.getKeyD_modify_self + +namespace Const + +variable {β : Type v} {m : Raw α (fun _ => β)} + +@[simp] +theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (Const.modify m k f).isEmpty = m.isEmpty := by + simp_to_raw using Raw₀.Const.isEmpty_modify + +@[simp] +theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) : + (Const.modify m k f).contains k' = m.contains k' := by + simp_to_raw using Raw₀.Const.contains_modify + +@[simp] +theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) : + k' ∈ Const.modify m k f ↔ k' ∈ m := by + simp only [mem_iff_contains, contains_modify h] + +@[simp] +theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (Const.modify m k f).size = m.size := by + simp_to_raw using Raw₀.Const.size_modify + +theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) : + Const.get? (Const.modify m k f) k' = + if k == k' then + Const.get? m k |>.map f + else + Const.get? m k' := by + simp_to_raw using Raw₀.Const.get?_modify + +@[simp] +theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + Const.get? (Const.modify m k f) k = (Const.get? m k).map f := by + simp_to_raw using Raw₀.Const.get?_modify_self + +theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} + (h : m.WF) {hc : k' ∈ Const.modify m k f} : + Const.get (Const.modify m k f) k' hc = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc + f (Const.get m k h') + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + Const.get m k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.get_modify + +@[simp] +theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} + (h : m.WF) {hc : k ∈ Const.modify m k f} : + haveI h' : k ∈ m := mem_modify h |>.mp hc + Const.get (Const.modify m k f) k hc = f (Const.get m k h') := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.get_modify_self + +theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} + (h : m.WF) : Const.get! (Const.modify m k f) k' = + if k == k' then + Const.get? m k |>.map f |>.get! + else + Const.get! m k' := by + simp_to_raw using Raw₀.Const.get!_modify + +@[simp] +theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} + (h : m.WF) : Const.get! (Const.modify m k f) k = ((Const.get? m k).map f).get! := by + simp_to_raw using Raw₀.Const.get!_modify_self + +theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) : + Const.getD (Const.modify m k f) k' fallback = + if k == k' then + Const.get? m k |>.map f |>.getD fallback + else + Const.getD m k' fallback := by + simp_to_raw using Raw₀.Const.getD_modify + +@[simp] +theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} (h : m.WF) : + Const.getD (Const.modify m k f) k fallback = ((Const.get? m k).map f).getD fallback := by + simp_to_raw using Raw₀.Const.getD_modify_self + +theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) : + (Const.modify m k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKey?_modify + +theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (Const.modify m k f).getKey? k = if k ∈ m then some k else none := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKey?_modify_self + +theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + (h : m.WF) : (Const.modify m k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKey!_modify + +theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + (h : m.WF) : (Const.modify m k f).getKey! k = if k ∈ m then k else default := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKey!_modify_self + +theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + (h : m.WF) {hc : k' ∈ Const.modify m k f} : + (Const.modify m k f).getKey k' hc = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + m.getKey k' h' := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.getKey_modify + +@[simp] +theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + (h : m.WF) {hc : k ∈ Const.modify m k f} : (Const.modify m k f).getKey k hc = k := by + simp only [mem_iff_contains] at hc + revert hc + simp_to_raw using Raw₀.Const.getKey_modify_self + +theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) : + (Const.modify m k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKeyD_modify + +theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} {f : β → β} + (h : m.WF) : (Const.modify m k f).getKeyD k fallback = if k ∈ m then k else fallback := by + simp only [mem_iff_contains] + simp_to_raw using Raw₀.Const.getKeyD_modify_self + +end Const + +end Modify + +end Raw + end Std.DHashMap diff --git a/src/Std/Data/HashMap/Lemmas.lean b/src/Std/Data/HashMap/Lemmas.lean index 688be7b35a..c49f0c3d28 100644 --- a/src/Std/Data/HashMap/Lemmas.lean +++ b/src/Std/Data/HashMap/Lemmas.lean @@ -1269,4 +1269,337 @@ theorem isEmpty_unitOfList [EquivBEq α] [LawfulHashable α] end +section Alter + +variable {m : HashMap α β} + +theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} + {f : Option β → Option β} : + (alter m k f).isEmpty = ((m.erase k).isEmpty && (f (get? m k)).isNone) := + DHashMap.Const.isEmpty_alter_eq_isEmpty_erase + +@[simp] +theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) := + DHashMap.Const.isEmpty_alter + +theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} : + (alter m k f).contains k' = if k == k' then (f (get? m k)).isSome else m.contains k' := + DHashMap.Const.contains_alter + +theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} : + k' ∈ alter m k f ↔ if k == k' then (f (get? m k)).isSome = true else k' ∈ m := + DHashMap.Const.mem_alter + +theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : k == k') : k' ∈ alter m k f ↔ (f (get? m k)).isSome := + DHashMap.Const.mem_alter_of_beq h + +@[simp] +theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (alter m k f).contains k = (f (get? m k)).isSome := + DHashMap.Const.contains_alter_self + +@[simp] +theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + k ∈ alter m k f ↔ (f (get? m k)).isSome := + DHashMap.Const.mem_alter_self + +theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : (k == k') = false) : + (alter m k f).contains k' = m.contains k' := + DHashMap.Const.contains_alter_of_beq_eq_false h + +theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : (k == k') = false) : k' ∈ alter m k f ↔ k' ∈ m := + DHashMap.Const.mem_alter_of_beq_eq_false h + +theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} : + (alter m k f).size = + if m.contains k && (f (get? m k)).isNone then + m.size - 1 + else if !m.contains k && (f (get? m k)).isSome then + m.size + 1 + else + m.size := + DHashMap.Const.size_alter + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∉ m) (h' : (f (get? m k)).isSome) : + (alter m k f).size = m.size + 1 := + DHashMap.Const.size_alter_eq_add_one h h' + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∈ m) (h' : (f (get? m k)).isNone) : + (alter m k f).size = m.size - 1 := + DHashMap.Const.size_alter_eq_sub_one h h' + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∉ m) (h' : (f (get? m k)).isNone) : + (alter m k f).size = m.size := + DHashMap.Const.size_alter_eq_self_of_not_mem h h' + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β} + (h : k ∈ m) (h' : (f (get? m k)).isSome) : + (alter m k f).size = m.size := + DHashMap.Const.size_alter_eq_self_of_mem h h' + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} : + (alter m k f).size ≤ m.size + 1 := + DHashMap.Const.size_alter_le_size + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} : + m.size - 1 ≤ (alter m k f).size := + DHashMap.Const.size_le_size_alter + +theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : + get? (alter m k f) k' = + if k == k' then + f (get? m k) + else + get? m k' := + DHashMap.Const.get?_alter + +@[simp] +theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + get? (alter m k f) k = f (get? m k) := + DHashMap.Const.get?_alter_self + +theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + {h : k' ∈ alter m k f} : + get (alter m k f) k' h = + if heq : k == k' then + haveI h' : (f (get? m k)).isSome := mem_alter_of_beq heq |>.mp h + f (get? m k) |>.get h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + get m k' h' := + DHashMap.Const.get_alter + +@[simp] +theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + {h : k ∈ alter m k f} : + haveI h' : (f (get? m k)).isSome := mem_alter_self.mp h + get (alter m k f) k h = (f (get? m k)).get h' := + DHashMap.Const.get_alter_self + +theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] + {f : Option β → Option β} : get! (alter m k f) k' = + if k == k' then + f (get? m k) |>.get! + else + get! m k' := + DHashMap.Const.get!_alter + +@[simp] +theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] + {f : Option β → Option β} : get! (alter m k f) k = (f (get? m k)).get! := + DHashMap.Const.get!_alter_self + +theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} + {f : Option β → Option β} : + getD (alter m k f) k' fallback = + if k == k' then + f (get? m k) |>.getD fallback + else + getD m k' fallback := + DHashMap.Const.getD_alter + +@[simp] +theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} + {f : Option β → Option β} : + getD (alter m k f) k fallback = (f (get? m k)).getD fallback := + DHashMap.Const.getD_alter_self + +theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} : + (alter m k f).getKey? k' = + if k == k' then + if (f (get? m k)).isSome then some k else none + else + m.getKey? k' := + DHashMap.Const.getKey?_alter + +theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} : + (alter m k f).getKey? k = if (f (get? m k)).isSome then some k else none := + DHashMap.Const.getKey?_alter_self + +theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} : (alter m k f).getKey! k' = + if k == k' then + if (f (get? m k)).isSome then k else default + else + m.getKey! k' := + DHashMap.Const.getKey!_alter + +theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} : + (alter m k f).getKey! k = if (f (get? m k)).isSome then k else default := + DHashMap.Const.getKey!_alter_self + +theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} {h : k' ∈ alter m k f} : + (alter m k f).getKey k' h = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h + m.getKey k' h' := + DHashMap.Const.getKey_alter + +@[simp] +theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} {h : k ∈ alter m k f} : + (alter m k f).getKey k h = k := + DHashMap.Const.getKey_alter_self + +theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} + {f : Option β → Option β} : + (alter m k f).getKeyD k' fallback = + if k == k' then + if (f (get? m k)).isSome then k else fallback + else + m.getKeyD k' fallback := + DHashMap.Const.getKeyD_alter + +theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : Option β → Option β} : + (alter m k f).getKeyD k fallback = if (f (get? m k)).isSome then k else fallback := + DHashMap.Const.getKeyD_alter_self + +end Alter + +section Modify + +variable {m : HashMap α β} + +@[simp] +theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (modify m k f).isEmpty = m.isEmpty := + DHashMap.Const.isEmpty_modify + +@[simp] +theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} : + (modify m k f).contains k' = m.contains k' := + DHashMap.Const.contains_modify + +@[simp] +theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} : + k' ∈ modify m k f ↔ k' ∈ m := + DHashMap.Const.mem_modify + +@[simp] +theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (modify m k f).size = m.size := + DHashMap.Const.size_modify + +theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : + get? (modify m k f) k' = + if k == k' then + get? m k |>.map f + else + get? m k' := + DHashMap.Const.get?_modify + +@[simp] +theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + get? (modify m k f) k = (get? m k).map f := + DHashMap.Const.get?_modify_self + +theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} + {h : k' ∈ modify m k f} : + get (modify m k f) k' h = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr heq |>.mpr <| mem_modify.mp h + f (get m k h') + else + haveI h' : k' ∈ m := mem_modify.mp h + get m k' h' := + DHashMap.Const.get_modify + +@[simp] +theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} + {h : k ∈ modify m k f} : + haveI h' : k ∈ m := mem_modify.mp h + get (modify m k f) k h = f (get m k h') := + DHashMap.Const.get_modify_self + +theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} : + get! (modify m k f) k' = + if k == k' then + get? m k |>.map f |>.get! + else + get! m k' := + DHashMap.Const.get!_modify + +@[simp] +theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} : + get! (modify m k f) k = ((get? m k).map f).get! := + DHashMap.Const.get!_modify_self + +theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} : + getD (modify m k f) k' fallback = + if k == k' then + get? m k |>.map f |>.getD fallback + else + getD m k' fallback := + DHashMap.Const.getD_modify + +@[simp] +theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} : + getD (modify m k f) k fallback = ((get? m k).map f).getD fallback := + DHashMap.Const.getD_modify_self + +theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} : + (modify m k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := + DHashMap.Const.getKey?_modify + +theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} : + (modify m k f).getKey? k = if k ∈ m then some k else none := + DHashMap.Const.getKey?_modify_self + +theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} : + (modify m k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := + DHashMap.Const.getKey!_modify + +theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} : + (modify m k f).getKey! k = if k ∈ m then k else default := + DHashMap.Const.getKey!_modify_self + +theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + {h : k' ∈ modify m k f} : + (modify m k f).getKey k' h = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify.mp h + m.getKey k' h' := + DHashMap.Const.getKey_modify + +@[simp] +theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + {h : k ∈ modify m k f} : (modify m k f).getKey k h = k := + DHashMap.Const.getKey_modify_self + +theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} : + (modify m k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := + DHashMap.Const.getKeyD_modify + +theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : β → β} : (modify m k f).getKeyD k fallback = if k ∈ m then k else fallback := + DHashMap.Const.getKeyD_modify_self + +end Modify + end Std.HashMap diff --git a/src/Std/Data/HashMap/Raw.lean b/src/Std/Data/HashMap/Raw.lean index 5db2a768e6..00186ce380 100644 --- a/src/Std/Data/HashMap/Raw.lean +++ b/src/Std/Data/HashMap/Raw.lean @@ -181,6 +181,14 @@ instance [BEq α] [Hashable α] : GetElem? (Raw α β) α β (fun m a => a ∈ m (l : List α) : Raw α Unit := ⟨DHashMap.Raw.Const.unitOfList l⟩ +@[inline, inherit_doc DHashMap.Raw.Const.alter] def alter [BEq α] [EquivBEq α] [Hashable α] + (m : Raw α β) (a : α) (f : Option β → Option β) : Raw α β := + ⟨DHashMap.Raw.Const.alter m.inner a f⟩ + +@[inline, inherit_doc DHashMap.Raw.Const.modify] def modify [BEq α] [EquivBEq α] [Hashable α] + (m : Raw α β) (a : α) (f : β → β) : Raw α β := + ⟨DHashMap.Raw.Const.modify m.inner a f⟩ + section Unverified /-! We currently do not provide lemmas for the functions below. -/ diff --git a/src/Std/Data/HashMap/RawLemmas.lean b/src/Std/Data/HashMap/RawLemmas.lean index 02d8442c62..11da7fe358 100644 --- a/src/Std/Data/HashMap/RawLemmas.lean +++ b/src/Std/Data/HashMap/RawLemmas.lean @@ -1286,4 +1286,336 @@ theorem getD_unitOfList end Raw +namespace Raw + +variable [BEq α] [Hashable α] {m : Raw α β} + +section Alter + +theorem isEmpty_alter_eq_isEmpty_erase [EquivBEq α] [LawfulHashable α] {k : α} + {f : Option β → Option β} (h : m.WF) : + (alter m k f).isEmpty = ((m.erase k).isEmpty && (f (get? m k)).isNone) := + DHashMap.Raw.Const.isEmpty_alter_eq_isEmpty_erase h.out + +@[simp] +theorem isEmpty_alter [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} (h : m.WF) : + (alter m k f).isEmpty = ((m.isEmpty || (m.size == 1 && m.contains k)) && (f (get? m k)).isNone) := + DHashMap.Raw.Const.isEmpty_alter h.out + +theorem contains_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : m.WF) : (alter m k f).contains k' = + if k == k' then (f (get? m k)).isSome else m.contains k' := + DHashMap.Raw.Const.contains_alter h.out + +theorem mem_alter [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} (h : m.WF) : + k' ∈ alter m k f ↔ if k == k' then (f (get? m k)).isSome = true else k' ∈ m := + DHashMap.Raw.Const.mem_alter h.out + +theorem mem_alter_of_beq [EquivBEq α] [LawfulHashable α] {k k': α} {f : Option β → Option β} + (h : m.WF) (he : k == k') : k' ∈ alter m k f ↔ (f (get? m k)).isSome := + DHashMap.Raw.Const.mem_alter_of_beq h.out he + +@[simp] +theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : (alter m k f).contains k = (f (get? m k)).isSome := + DHashMap.Raw.Const.contains_alter_self h.out + +@[simp] +theorem mem_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : k ∈ alter m k f ↔ (f (get? m k)).isSome := + DHashMap.Raw.Const.mem_alter_self h.out + +theorem contains_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) : + (alter m k f).contains k' = m.contains k' := + DHashMap.Raw.Const.contains_alter_of_beq_eq_false h.out he + +theorem mem_alter_of_beq_eq_false [EquivBEq α] [LawfulHashable α] {k k' : α} + {f : Option β → Option β} (h : m.WF) (he : (k == k') = false) : k' ∈ alter m k f ↔ k' ∈ m := + DHashMap.Raw.Const.mem_alter_of_beq_eq_false h.out he + +theorem size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + (alter m k f).size = + if m.contains k && (f (get? m k)).isNone then + m.size - 1 + else if !m.contains k && (f (get? m k)).isSome then + m.size + 1 + else + m.size := + DHashMap.Raw.Const.size_alter h.out + +theorem size_alter_eq_add_one [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) + (h₁ : k ∉ m) (h₂ : (f (get? m k)).isSome) : + (alter m k f).size = m.size + 1 := + DHashMap.Raw.Const.size_alter_eq_add_one h.out h₁ h₂ + +theorem size_alter_eq_sub_one [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) + (h₁ : k ∈ m) (h₂ : (f (get? m k)).isNone) : + (alter m k f).size = m.size - 1 := + DHashMap.Raw.Const.size_alter_eq_sub_one h.out h₁ h₂ + +theorem size_alter_eq_self_of_not_mem [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) + (h₁ : k ∉ m) (h₂ : (f (get? m k)).isNone) : (alter m k f).size = m.size := + DHashMap.Raw.Const.size_alter_eq_self_of_not_mem h.out h₁ h₂ + +theorem size_alter_eq_self_of_mem [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) + (h₁ : k ∈ m) (h₂ : (f (get? m k)).isSome) : (alter m k f).size = m.size := + DHashMap.Raw.Const.size_alter_eq_self_of_mem h.out h₁ h₂ + +theorem size_alter_le_size [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + (alter m k f).size ≤ m.size + 1 := + DHashMap.Raw.Const.size_alter_le_size h.out + +theorem size_le_size_alter [LawfulBEq α] {k : α} {f : Option β → Option β} (h : m.WF) : + m.size - 1 ≤ (alter m k f).size := + DHashMap.Raw.Const.size_le_size_alter h.out + +theorem get?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} (h : m.WF) : + get? (alter m k f) k' = + if k == k' then + f (get? m k) + else + get? m k' := + DHashMap.Raw.Const.get?_alter h.out + +@[simp] +theorem get?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : get? (alter m k f) k = f (get? m k) := + DHashMap.Raw.Const.get?_alter_self h.out + +theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + (h : m.WF) {hc : k' ∈ alter m k f} : + get (alter m k f) k' hc = + if heq : k == k' then + haveI h' : (f (get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc + f (get? m k) |>.get h' + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + get m k' h' := + DHashMap.Raw.Const.get_alter h.out + +@[simp] +theorem get_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) {hc : k ∈ alter m k f} : + haveI h' : (f (get? m k)).isSome := mem_alter_self h |>.mp hc + get (alter m k f) k hc = (f (get? m k)).get h' := + DHashMap.Raw.Const.get_alter_self h.out + +theorem get!_alter [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] + {f : Option β → Option β} (h : m.WF) : get! (alter m k f) k' = + if k == k' then + f (get? m k) |>.get! + else + get! m k' := + DHashMap.Raw.Const.get!_alter h.out + +@[simp] +theorem get!_alter_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] + {f : Option β → Option β} (h : m.WF) : get! (alter m k f) k = (f (get? m k)).get! := + DHashMap.Raw.Const.get!_alter_self h.out + +theorem getD_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} + {f : Option β → Option β} (h : m.WF) : getD (alter m k f) k' fallback = + if k == k' then + f (get? m k) |>.getD fallback + else + getD m k' fallback := + DHashMap.Raw.Const.getD_alter h.out + +@[simp] +theorem getD_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} + {f : Option β → Option β} (h : m.WF) : + getD (alter m k f) k fallback = (f (get? m k)).getD fallback := + DHashMap.Raw.Const.getD_alter_self h.out + +theorem getKey?_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β} + (h : m.WF) : (alter m k f).getKey? k' = + if k == k' then + if (f (get? m k)).isSome then some k else none + else + m.getKey? k' := + DHashMap.Raw.Const.getKey?_alter h.out + +theorem getKey?_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β} + (h : m.WF) : (alter m k f).getKey? k = if (f (get? m k)).isSome then some k else none := + DHashMap.Raw.Const.getKey?_alter_self h.out + +theorem getKey!_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} (h : m.WF) : (alter m k f).getKey! k' = + if k == k' then + if (f (get? m k)).isSome then k else default + else + m.getKey! k' := + DHashMap.Raw.Const.getKey!_alter h.out + +theorem getKey!_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} (h : m.WF) : + (alter m k f).getKey! k = if (f (get? m k)).isSome then k else default := + DHashMap.Raw.Const.getKey!_alter_self h.out + +theorem getKey_alter [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} + {f : Option β → Option β} (h : m.WF) {hc : k' ∈ alter m k f} : + (alter m k f).getKey k' hc = + if heq : k == k' then + k + else + haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc + m.getKey k' h' := + DHashMap.Raw.Const.getKey_alter h.out + +@[simp] +theorem getKey_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} + {f : Option β → Option β} (h : m.WF) {hc : k ∈ alter m k f} : + (alter m k f).getKey k hc = k := + DHashMap.Raw.Const.getKey_alter_self h.out + +theorem getKeyD_alter [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : Option β → Option β} + (h : m.WF) : (alter m k f).getKeyD k' fallback = + if k == k' then + if (f (get? m k)).isSome then k else fallback + else + m.getKeyD k' fallback := + DHashMap.Raw.Const.getKeyD_alter h.out + +theorem getKeyD_alter_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : Option β → Option β} (h : m.WF) : + (alter m k f).getKeyD k fallback = if (f (get? m k)).isSome then k else fallback := + DHashMap.Raw.Const.getKeyD_alter_self h.out + +end Alter + +section Modify + +@[simp] +theorem isEmpty_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (modify m k f).isEmpty = m.isEmpty := + DHashMap.Raw.Const.isEmpty_modify h.out + +@[simp] +theorem contains_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) : + (modify m k f).contains k' = m.contains k' := + DHashMap.Raw.Const.contains_modify h.out + +@[simp] +theorem mem_modify [EquivBEq α] [LawfulHashable α] {k k': α} {f : β → β} (h : m.WF) : + k' ∈ modify m k f ↔ k' ∈ m := + DHashMap.Raw.Const.mem_modify h.out + +@[simp] +theorem size_modify [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (modify m k f).size = m.size := + DHashMap.Raw.Const.size_modify h.out + +theorem get?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) : + get? (modify m k f) k' = + if k == k' then + get? m k |>.map f + else + get? m k' := + DHashMap.Raw.Const.get?_modify h.out + +@[simp] +theorem get?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + get? (modify m k f) k = (get? m k).map f := + DHashMap.Raw.Const.get?_modify_self h.out + +theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} + (h : m.WF) {hc : k' ∈ modify m k f} : + get (modify m k f) k' hc = + if heq : k == k' then + haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc + f (get m k h') + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + get m k' h' := + DHashMap.Raw.Const.get_modify h.out + +@[simp] +theorem get_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) + {hc : k ∈ modify m k f} : + haveI h' : k ∈ m := mem_modify h |>.mp hc + get (modify m k f) k hc = f (get m k h') := + DHashMap.Raw.Const.get_modify_self h.out + +theorem get!_modify [EquivBEq α] [LawfulHashable α] {k k' : α} [Inhabited β] {f : β → β} + (h : m.WF) : get! (modify m k f) k' = + if k == k' then + get? m k |>.map f |>.get! + else + get! m k' := + DHashMap.Raw.Const.get!_modify h.out + +@[simp] +theorem get!_modify_self [EquivBEq α] [LawfulHashable α] {k : α} [Inhabited β] {f : β → β} + (h : m.WF) : get! (modify m k f) k = ((get? m k).map f).get! := + DHashMap.Raw.Const.get!_modify_self h.out + +theorem getD_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {fallback : β} {f : β → β} (h : m.WF) : + getD (modify m k f) k' fallback = + if k == k' then + get? m k |>.map f |>.getD fallback + else + getD m k' fallback := + DHashMap.Raw.Const.getD_modify h.out + +@[simp] +theorem getD_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {fallback : β} {f : β → β} (h : m.WF) : + getD (modify m k f) k fallback = ((get? m k).map f).getD fallback := + DHashMap.Raw.Const.getD_modify_self h.out + +theorem getKey?_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β} (h : m.WF) : + (modify m k f).getKey? k' = + if k == k' then + if k ∈ m then some k else none + else + m.getKey? k' := + DHashMap.Raw.Const.getKey?_modify h.out + +theorem getKey?_modify_self [EquivBEq α] [LawfulHashable α] {k : α} {f : β → β} (h : m.WF) : + (modify m k f).getKey? k = if k ∈ m then some k else none := + DHashMap.Raw.Const.getKey?_modify_self h.out + +theorem getKey!_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + (h : m.WF) : (modify m k f).getKey! k' = + if k == k' then + if k ∈ m then k else default + else + m.getKey! k' := + DHashMap.Raw.Const.getKey!_modify h.out + +theorem getKey!_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + (h : m.WF) : (modify m k f).getKey! k = if k ∈ m then k else default := + DHashMap.Raw.Const.getKey!_modify_self h.out + +theorem getKey_modify [EquivBEq α] [LawfulHashable α] [Inhabited α] {k k' : α} {f : β → β} + (h : m.WF) {hc : k' ∈ modify m k f} : + (modify m k f).getKey k' hc = + if k == k' then + k + else + haveI h' : k' ∈ m := mem_modify h |>.mp hc + m.getKey k' h' := + DHashMap.Raw.Const.getKey_modify h.out + +@[simp] +theorem getKey_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k : α} {f : β → β} + (h : m.WF) {hc : k ∈ modify m k f} : (modify m k f).getKey k hc = k := + DHashMap.Raw.Const.getKey_modify_self h.out + +theorem getKeyD_modify [EquivBEq α] [LawfulHashable α] {k k' fallback : α} {f : β → β} (h : m.WF) : + (modify m k f).getKeyD k' fallback = + if k == k' then + if k ∈ m then k else fallback + else + m.getKeyD k' fallback := + DHashMap.Raw.Const.getKeyD_modify h.out + +theorem getKeyD_modify_self [EquivBEq α] [LawfulHashable α] [Inhabited α] {k fallback : α} + {f : β → β} (h : m.WF) : (modify m k f).getKeyD k fallback = if k ∈ m then k else fallback := + DHashMap.Raw.Const.getKeyD_modify_self h.out + +end Modify + +end Raw + end Std.HashMap