feat: faster, linear HashMap.alter and modify

[datokrat]

This PR replaces the existing implementations of (D)HashMap.alter and (D)HashMap.modify with primitive, more efficient ones and in particular provides proofs that they yield well-formed hash maps (WF typeclass).

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-6573 has successfully built against this PR. (2025-01-09 10:36:44) View Log
• ✅ Mathlib branch lean-pr-testing-6573 has successfully built against this PR. (2025-01-09 13:45:31) View Log
• ✅ Mathlib branch lean-pr-testing-6573 has successfully built against this PR. (2025-01-10 10:00:43) View Log
• 🟡 Mathlib branch lean-pr-testing-6573 build against this PR was cancelled. (2025-01-10 13:30:15) View Log
• ✅ Mathlib branch lean-pr-testing-6573 has successfully built against this PR. (2025-01-10 14:11:16) View Log
• ✅ Mathlib branch lean-pr-testing-6573 has successfully built against this PR. (2025-01-13 14:12:48) View Log
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 05aa256c99ca16ac90536c5ea1322df37b24e958 --onto d2c4471cfa4611977bf4927b5cd849df1a4272b7. (2025-01-14 07:38:34)

[TwoFX]

Might want to remove "linear" from the PR title to avoid the interpretation that there was previously a linearity problem.

@kim-em There was, in fact, a linearity problem. Here is the code for alter:

@[inline] def alter [LawfulBEq α] (m : DHashMap α β) (a : α) (f : Option (β a) → Option (β a)) : DHashMap α β :=
  match m.get? a with
  | none =>
    match f none with
    | none => m
    | some b => m.insert a b
  | some b =>
    match f (some b) with
    | none => m.erase a
    | some b => m.erase a |>.insert a b

In the very bottom branch, we verified using the IR and using benchmarks that the compiler decided to first run f (some b) and then call m.erase a, so when b was passed into f it was in fact shared, leading to quadratic runtimes for example if b is an array and f calls b.push.

[datokrat]

(Update: I didn't see Markus' comment before writing this)

Might want to remove "linear" from the PR title to avoid the interpretation that there was previously a linearity problem.

Indeed, it turned out that alter accidentally wasn't linear before (in the case where the map is List-valued and we modify the contained lists), so this interpretation isn't wrong for alter.

I'm a little surprised at the decision to implement modify at the bottom level, rather than just defining it in terms of alter "further out". Perhaps it is a tiny bit faster, but it seems like a lot of extra work.

In my benchmarks, modify is about 30% faster than doing the same with alter. As far as I can tell, this is because we do not need to recompute the size, since modify never changes the size. Luckily, it wasn't hard to show that modify equals alter, so I was able to avoid most of the work.

[kim-em]

In my benchmarks, modify is about 30% faster than doing the same with alter.

Awesome! Glad I asked.

[TwoFX]

LGTM except for the final few remarks, feel free to merge after fixing.