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: add BitVec comparison lemmas to bv_normalize #6799

Merged
merged 1 commit into from
Jan 28, 2025
Merged

feat: add BitVec comparison lemmas to bv_normalize #6799

merged 1 commit into from
Jan 28, 2025

Conversation

vlad902
Copy link
Contributor

@vlad902 vlad902 commented Jan 27, 2025

This PR adds a number of simple comparison lemmas to the top/bottom element for BitVec. Then they are applied to teach bv_normalize that (a<1) = (a==0) and to remove an intermediate proof that is no longer necessary along the way.

@vlad902
feat: add BitVec comparison lemmas to bv_normalize
c365a59 
This PR adds a number of simple comparison lemmas to the top/bottom
element for BitVec. Then they are applied to teach bv_normalize that
`(a<1) = (a==0)` and to remove an intermediate proof that is no longer
necessary along the way.
@vlad902
Copy link
Contributor Author

vlad902 commented Jan 27, 2025

changelog-library

@github-actions github-actions bot added changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN labels Jan 27, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 3aea0fd810f404f930aa95f9666cf60940bcf64e --onto 69a73a18fbfa1fc045bfbf1c4cf93b155d4c9387. (2025-01-27 22:22:53)

@hargoniX hargoniX added changelog-library Library and removed changelog-library Library labels Jan 28, 2025
@hargoniX hargoniX added this pull request to the merge queue Jan 28, 2025
Merged via the queue into leanprover:master with commit c7c1e09 Jan 28, 2025
17 of 18 checks passed
luisacicolini pushed a commit to opencompl/lean4 that referenced this pull request Jan 28, 2025
@vlad902 @luisacicolini
feat: add BitVec comparison lemmas to bv_normalize (leanprover#6799)
c0f8403 
This PR adds a number of simple comparison lemmas to the top/bottom
element for BitVec. Then they are applied to teach bv_normalize that
`(a<1) = (a==0)` and to remove an intermediate proof that is no longer
necessary along the way.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees
No one assigned
Labels
changelog-library Library 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
@vlad902 @leanprover-community-bot @hargoniX