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