feat: verify all and any for hash maps

[jt0202]

This PR extends the all/any functions from hash sets to hash maps and dependent hash maps and verifies them.

[TwoFX]

Given that we have recently got any and all on iterators (#10686) and hash map iterators are coming up (#10761), the question arises: should we define m.all p on a hash map m to be m.iter.all p (or, even more radical, not provide it at all and expect users to write m.iter.all p themselves)?

And hopefully if the right lemmas about HashMap.iter and Iter.any exist, all any lemmas you might want on hash maps fall right out?

@datokrat, any thoughts?

[jt0202]

Given that we have recently got any and all on iterators (#10686) and hash map iterators are coming up (#10761), the question arises: should we define m.all p on a hash map m to be m.iter.all p (or, even more radical, not provide it at all and expect users to write m.iter.all p themselves)?

This would also work for me and then we can close this one. I feel like it would be more comfortable for the user to still have the custom any/all function as the iterator seems to me like an implementation detail.

[datokrat]

@datokrat, any thoughts?

I think this will work -- however, one should perhaps run a benchmark comparing the iterators' any and the current HashMap.any. Because the compiler is still sometimes struggling to optimize iterator for-in (used to implement any), there might be a slowdown.

If it turns out that there is still a performance benefit to implementing HashMap.any separately, another way to go would be to prove that it coincides with Iter.any and then transport all the lemmas along that equality.

[TwoFX]

@jt202, any and all on iteratos and hash map iterators have landed now. Would you be interested in creating benchmarks to see how the direct implementation fares against the iterator-based one? There are some hash map benchmarks in tests/bench which you could use as a starting point.

[jt0202]

@TwoFX I can give it a try. Should I push then the benchmarks here or share them in another way if they are not meant to be that permanent.

[TwoFX]

Feel free to add them here, more benchmarks are always good to have.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto 3e86729ee0e11548a47f9b294d5292ada92c0b40. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-03 16:52:55)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto d47b474e41e4b134239ef70fa3c15778cc771bcf. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-10 19:05:00)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto 2b85e29cc9828a164f63bcc7ef47581767542460. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-13 19:03:30)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 00e29075f38e5307b404b656805da137e5c52942 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-03 16:52:56)

[jt0202]

I tried a bit with the iterator approach, but to me, it feels like I get more complicated statements than my direct approach in this file. My goal was it to have lemmas looking like those in Init.Data.List.Lemmas and now I get these intermediate steps and would need some sort of induction over the iterator. How do you imagine the resulting lemmas?

[jt0202]

changelog-library

[jt0202]

@TwoFX I tried a bit with the iterator approach, but the lemmas weren't much of use to get something compared to the list API. I talked with @datokrat about that, and we came to the conclusion that the direct approach via toList is the best for now.

How should the benchmark file be adapted for long term use?

[datokrat]

I have nothing to complain except for a few syntactical and stylistical remarks ;)