Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat: verify toList for hash maps #6954

Draft
wants to merge 9 commits into
base: master
Choose a base branch
from
Draft

feat: verify toList for hash maps #6954

wants to merge 9 commits into from
+439 −16

Conversation

jt0202
Copy link
Contributor

@jt0202 jt0202 commented Feb 5, 2025

This PR verifies the toListfunction for hash maps and dependent hash maps.

@jt0202
Copy link
Contributor Author

jt0202 commented Feb 5, 2025

This is currently WIP. If you think further lemmas are useful let me know. One lemma is currently unproven, because there are some problems with casting. As with previous PRs I will first only work in Internal/RawLemmas.lean.

@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 Feb 5, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Feb 5, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto 412389f71f8a24307e3adba69b38b4b685b04f72. (2025-02-05 12:00:25)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto b01ca8ee237a1b3c299384e73ad79d424e216a84. (2025-02-07 11:50:08)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 6d63f6305eee006f1acaddff2f36654c98ce5b5e --onto d61f506da254b919f93e571a84247319de78f526. (2025-02-10 20:03:26)

jt0202
jt0202 commented Feb 7, 2025
View reviewed changes
src/Init/Data/List/Lemmas.lean Outdated Show resolved Hide resolved
TwoFX
TwoFX reviewed Feb 10, 2025
View reviewed changes
src/Std/Data/DHashMap/Internal/RawLemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Internal/RawLemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Internal/RawLemmas.lean Outdated Show resolved Hide resolved
src/Std/Data/DHashMap/Internal/RawLemmas.lean Show resolved Hide resolved
src/Std/Data/DHashMap/Internal/RawLemmas.lean Show resolved Hide resolved
src/Std/Data/DHashMap/Internal/RawLemmas.lean Show resolved Hide resolved
@TwoFX TwoFX self-assigned this Feb 11, 2025
@TwoFX
Copy link
Member

TwoFX commented Feb 11, 2025

RawLemmas statements look good to me. Will take a look at the proofs in a bit.

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

@TwoFX TwoFX TwoFX left review comments

Assignees

@TwoFX TwoFX

Labels
toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@jt0202 @leanprover-community-bot @TwoFX