feat: hash map lemmas for filter, map and filterMap by Rob23oba · Pull Request #7400 · leanprover/lean4

Rob23oba · 2025-03-08T20:06:22Z

This PR adds lemmas for the filter, map and filterMap functions of the hash map.

…into hashmap-filter-map

ghost · 2025-03-08T20:51:53Z

Mathlib CI status (docs):

❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase b9f8a859e7f354f026de7c910e17ce29e23678f9 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-08 20:51:52)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase da2d877019c3cc393c24b18919e4c7829bc3b9fe --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-09 07:27:37)
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-10 18:41:15) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-10 19:39:30) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-11 17:12:12) View Log
✅ Mathlib branch lean-pr-testing-7400 has successfully built against this PR. (2025-03-11 19:35:28) View Log
🟡 Mathlib branch lean-pr-testing-7400 build against this PR was cancelled. (2025-03-11 21:01:27) View Log
🟡 Mathlib branch lean-pr-testing-7400 build this PR didn't complete normally. (2025-03-11 21:45:47) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137f5595204c48ec9442711f0e9e43228e40a07c --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 12:33:12)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 137f5595204c48ec9442711f0e9e43228e40a07c --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 17:49:59)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07ee2eea21545fb055f1a8bdb848e2a419502c97 --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-13 20:58:56)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 07ee2eea21545fb055f1a8bdb848e2a419502c97 --onto d5f01f2db1efd18034421ae2f40120d1c608f3c0. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-15 22:06:58)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5a5e83c26c2c74948e32e103e155fb57079e8e6c --onto d32a7b250ad20477d55034488d89a050fbf70af5. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-17 18:22:15)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a5348f4bdc95c5a327817b5c62ee9f99ec8a0bfa --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-19 18:26:39)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c66cb00c0fbdc28636a0ebe7c0ac264e68ecd15b --onto a97813e11f962bc422a03c30b7e29dd2eefb92c8. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-20 20:18:48)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5fb990fcbd8d56e61e4276adcbe6deb19b5d7c64 --onto 060b2fe46fe728934744ee52271b92ab74cbd5b4. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-28 18:00:17)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 107eb845847456ef554a763b16d579284b11ac53 --onto 12a21e79c71880424321d62e60449863c504048a. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-31 10:49:08)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 107eb845847456ef554a763b16d579284b11ac53 --onto 2edfe2e9cffd55e3c79291628ae091b942291ec9. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-01 10:51:40)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 83067d67d65efe4818205ddb3f9b2ab824735b10 --onto 1ee7e1a9d8a67d1d8dcf6a17ac5c92bc2c7e0fac. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-03 15:10:01)
❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-04-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. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-06 13:06:43)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-04-06 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-07 09:18:08)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto da55b2e19b6af219f43f3599f1a72151799eb524. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-07 15:52:51)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto 0f2ede45d50d8fc8cc542517867a9d6a29f805a3. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-08 07:43:03)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase acd6b13d7692c2bf2314c09e406a178407d02743 --onto 388b6f045bd6d79df9b503d55eef6688ceb8f647. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-09 17:50:35)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0669a0470407e46d1ae26be8e201e214d5a91e74 --onto deef1c2739a331899b0e536312e65e9815059014. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-12 09:24:34)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 7cca594a4a567ad801dc0cefc3d1adcd0e141ec7 --onto 020b8834c3e06da1cd1682431b6fa8d52206c8ec. You can force Mathlib CI using the force-mathlib-ci label. (2025-04-16 14:44:30)

…into hashmap-filter-map

TwoFX

Looking very good, so this is mainly blocked on #7855.

src/Std/Data/HashSet/Lemmas.lean

TwoFX · 2025-04-14T08:24:10Z

src/Std/Data/HashMap/Lemmas.lean

      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false (Bool.not_eq_true _ ▸ heq) |>.mp h
-        m[k']'h' :=
+        m[(k')]'h' :=


Why is this suddenly needed?

Without the brackets Lean inteprets this term as containing the string ']' and because of that raises an error.

A space helps alternatively as well.

To be fair: it doesn't raise an error, but the formatting goes all weird because it treats ']' as a character literal and then [... := as an unclosed bracket.

src/Std/Data/HashMap/Lemmas.lean

src/Std/Data/Internal/List/Associative.lean

…into hashmap-filter-map

TwoFX

Great work as always, thanks a lot!

Rob23oba and others added 9 commits March 8, 2025 15:31

getEntry?_filterMap + option lemmas + getValueCast?_filterMap

dbabda4

getEntry?_filter

1646b60

actually getEntry?_filter and getEntry?_map

fb3af25

Length result for filterMap

09c3bb3

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

6c9bb1f

…into hashmap-filter-map

Lengths results for hashmaps and hashsets

cf64f9e

finish getValueCast?

7b3813d

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

0d68565

…into hashmap-filter-map

Rewrote length results without LawfulBEq

a030b42

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 8, 2025

jt0202 and others added 5 commits March 8, 2025 22:30

getKey results for map

96cf77b

take care of todo in simp_to_model

0a9ac13

Merge remote-tracking branch 'upstream/master' into hashmap-filter-map

09d3a00

minor cleanup

615d558

finish getKey_...

49185c1

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 10, 2025

Update lean-toolchain for testing leanprover/lean4#7400

47caae0

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025

Update lean-toolchain for testing leanprover/lean4#7400

891f25d

finish getValueCast_...

34e7803

ghost added the builds-mathlib CI has verified that Mathlib builds against this PR label Mar 10, 2025

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 10, 2025

Trigger CI for leanprover/lean4#7400

e3f88d3

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025

Trigger CI for leanprover/lean4#7400

0b0c2ae

finish getValue_...

71b7315

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 11, 2025

Trigger CI for leanprover/lean4#7400

6ef71b7

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 11, 2025

Trigger CI for leanprover/lean4#7400

aae4ba9

Filter length

97cc513

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 11, 2025

Trigger CI for leanprover/lean4#7400

7035a7a

ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 11, 2025

Trigger CI for leanprover/lean4#7400

a2ed060

Further work on isEmpty & length

c8dac7b

ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 11, 2025

Trigger CI for leanprover/lean4#7400

4ab7f29

jt0202 and others added 7 commits April 13, 2025 12:39

Raw lemmas for HashMap

c244b49

improve proof of getValue?_map, add pfilter

a1678d9

Raw lemmas for hash set

769b654

lemmas for HashMap + small instance adjustments

671ba63

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

a9a2c58

…into hashmap-filter-map

HashSet lemmas

0e42339

more additions for consistency

f8dff37

github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 13, 2025

Rob23oba added 2 commits April 13, 2025 21:32

more cleanup

b204acb

more correctly depict which functions have lemmas about them

be4c0c8

TwoFX reviewed Apr 14, 2025

View reviewed changes

TwoFX added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Apr 14, 2025

jt0202 and others added 5 commits April 14, 2025 19:39

Suggestions from review

fbaf1e9

Merge remote-tracking branch 'upstream/master' into hashmap-filter-map

d161a8e

remove instance

eed74a0

Merge branch 'hashmap-filter-map' of https://github.com/Rob23oba/lean4 …

b1ae350

…into hashmap-filter-map

use beq.rfl

f2509c9

Rob23oba marked this pull request as ready for review April 16, 2025 14:15

Rob23oba requested a review from kim-em as a code owner April 16, 2025 14:15

github-actions bot added the changelog-library Library label Apr 16, 2025

trigger ci

6187f06

github-actions bot added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Apr 16, 2025

Rob23oba mentioned this pull request Apr 16, 2025

Notation x[...]'... gets confused with a character literal leanprover/vscode-lean4#609

Closed

TwoFX approved these changes Apr 17, 2025

View reviewed changes

TwoFX added this pull request to the merge queue Apr 17, 2025

Merged via the queue into leanprover:master with commit acfc9c5 Apr 17, 2025
15 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: hash map lemmas for filter, map and filterMap#7400

feat: hash map lemmas for filter, map and filterMap#7400
TwoFX merged 107 commits intoleanprover:masterfrom
Rob23oba:hashmap-filter-map

Rob23oba commented Mar 8, 2025

Uh oh!

ghost commented Mar 8, 2025 •

edited by ghost

Loading

Uh oh!

TwoFX left a comment

Uh oh!

Uh oh!

TwoFX Apr 14, 2025

Uh oh!

jt0202 Apr 14, 2025

Uh oh!

jt0202 Apr 14, 2025

Uh oh!

Rob23oba Apr 16, 2025 •

edited

Loading

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX left a comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

Rob23oba commented Mar 8, 2025

Uh oh!

ghost commented Mar 8, 2025 • edited by ghost Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

TwoFX Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

jt0202 Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

jt0202 Apr 14, 2025

Choose a reason for hiding this comment

Uh oh!

Rob23oba Apr 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

TwoFX left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

ghost commented Mar 8, 2025 •

edited by ghost

Loading

Rob23oba Apr 16, 2025 •

edited

Loading