Skip to content

Conversation

@wkrozowski
Copy link
Contributor

@wkrozowski wkrozowski commented Nov 19, 2025

This PR adds BEq instance for DHashMap/HashMap/HashSet and their extensional variants and proves lemmas relating it to the equivalence of hashmaps/equality of extensional variants.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 19, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 19, 2025

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 75342961fcc7bbcc911ad0497d18d95b0f008de9 --onto 5a4226f2bdcc6299df76285b1d30f238546c09fe. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-19 20:39:19)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 75342961fcc7bbcc911ad0497d18d95b0f008de9 --onto a106ea053fec080a50204b0ad6dadc69bc3f0937. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-20 20:35:01)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 75342961fcc7bbcc911ad0497d18d95b0f008de9 --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-26 12:51:51)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2025-11-27 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-11-27 12:23:20)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799d5944007085768dcc8b8558c6dae485d4ae22 --onto b0e6db322421ce368999f08870fd747e45242f86. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-27 17:54:43)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 13:53:32)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 0173444d24df9253d7947cfe82519e4a6caffd3a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 13:11:14)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto dd28f005889dd2fcca6fe0638133de561a655ad1. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-04 18:08:38)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 455fd0b4488e2adc85f825a52e2ee7d944a5740a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-05 14:43:36)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 2ca3bc28590c5c33f755d3bd18252f25ea266266. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 09:01:13)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto 62f2f9229356039356c0469a46d8ecd77be88e2a. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-08 12:54:11)

@leanprover-bot
Copy link
Collaborator

leanprover-bot commented Nov 19, 2025

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 75342961fcc7bbcc911ad0497d18d95b0f008de9 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-19 20:39:20)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-11-27 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-11-27 12:23:22)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 799d5944007085768dcc8b8558c6dae485d4ae22 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-27 17:54:44)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 1ae680c5e2f3922ba0c6c257a105426fdab20999 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-01 13:53:34)

@wkrozowski wkrozowski changed the title feat: add BEq to DHashMap/HashMap/HashSet [Work in progress] feat: add BEq to DHashMap/HashMap/HashSet and their extensional variants. Nov 27, 2025
@wkrozowski wkrozowski changed the title feat: add BEq to DHashMap/HashMap/HashSet and their extensional variants. feat: add BEq to DHashMap/HashMap/HashSet and their extensional variants Nov 27, 2025
@wkrozowski wkrozowski marked this pull request as ready for review November 27, 2025 11:09
@wkrozowski wkrozowski requested a review from TwoFX as a code owner November 27, 2025 11:09
@wkrozowski wkrozowski requested a review from kim-em as a code owner December 4, 2025 10:56
suffices tl.length ≤ (eraseKey hd.1 l₂).length by
rw [List.length_eraseKey, hc] at this
simp at this
simp
Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Non-terminal simp

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

5 participants