perf: linearity in HashMap.(insert|erase)

[TwoFX]

The speedcenter doesn't seem to care much, but in my benchmark for replace-heavy workloads, the fixed code is about 40% faster.

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit f626d65.
There were no significant changes against commit 287d46e.

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• ❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-06-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-06-06 09:36:04)
• ✅ Mathlib branch lean-pr-testing-4372 has successfully built against this PR. (2024-06-07 08:44:36) View Log
• ✅ Mathlib branch lean-pr-testing-4372 has successfully built against this PR. (2024-06-07 11:28:29) View Log

[TwoFX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 37e2bdb.
There were significant changes against commit 287d46e:

  Benchmark   Metric             Change
  ================================================
- stdlib      tactic execution     1.2% (1102.8 σ)

[leodemoura]

@TwoFX Great catch. Have you considered using Array.modify?

[TwoFX]

@leodemoura I have, but I think it makes the code less clear in this case (because we already have bkt, so it's confusing to bind another name to it in the lambda passed to modify) and according to my benchmark there is no statistically significant difference in speed between the two variants. I'm happy to change it if you prefer the modify version (though note that this will make the diff larger because I would have to add a new definition HashMapBucket.modify).

[leodemoura]

@leodemoura I have, but I think it makes the code less clear in this case (because we already have bkt, so it's confusing to bind another name to it in the lambda passed to modify) and according to my benchmark there is no statistically significant difference in speed between the two variants. I'm happy to change it if you prefer the modify version (though note that this will make the diff larger because I would have to add a new definition HashMapBucket.modify).

Great. No need to change. Just wanted to know if you considered. I trust your judgment.