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.(msb, getMsbD)_(rotateLeft, rotateRight) #6120

Merged
merged 14 commits into from
Nov 19, 2024
Merged

feat: add BitVec.(msb, getMsbD)_(rotateLeft, rotateRight) #6120

merged 14 commits into from
Nov 19, 2024

Conversation

luisacicolini
Copy link
Contributor

@luisacicolini luisacicolini commented Nov 18, 2024 •
edited by kim-em
Loading

This PR adds theorems BitVec.(getMsbD, msb)_(rotateLeft, rotateRight).

We follow the same strategy taken for getLsbD, constructing the necessary auxilliary theorems first (relying on different hypotheses) and then generalizing.

@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 18, 2024
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Nov 18, 2024 •
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 258d3725e73688ef08bc410e4cc8ee91a5641f13 --onto a074bd9a2bd20cc470fbff4f80f2cd7b51ec0d0a. (2024-11-18 17:22:03)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 258d3725e73688ef08bc410e4cc8ee91a5641f13 --onto 5a99cb326c9e9052e135cc63ed02b63371cff6d3. (2024-11-19 09:04:42)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 799b2b662825e646609963921f2c68489b2e664a --onto 4600bb16fcded0356d20ae232e7f8580c56a5955. (2024-11-19 14:10:09)

kim-em
kim-em reviewed Nov 19, 2024
View reviewed changes
src/Init/Data/BitVec/Lemmas.lean Outdated

@[simp]
theorem msb_rotateLeft {m w : Nat} {x : BitVec w} :
(x.rotateLeft m).msb = decide (0 < w && x.getMsbD (m % w)) := by
Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
(x.rotateLeft m).msb = decide (0 < w && x.getMsbD (m % w)) := by
(x.rotateLeft m).msb = (decide (0 < w) && x.getMsbD (m % w)) := by

Copy link
Collaborator

Choose a reason for hiding this comment

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

Is the decide (0 < w) needed here? I think it gives the correct answer without.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

AFAIU it is: if I remove it I get x.getMsbD (m % w) = true → 0 < w, which intro and omega can not solve

Copy link
Contributor

Choose a reason for hiding this comment

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

I managed to drop it with a minor extension of the proof.

Copy link
Contributor Author

Choose a reason for hiding this comment

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

thank you!

Copy link
Collaborator

Choose a reason for hiding this comment

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

A proof not working is not proof that the statement is wrong. :-)

@kim-em kim-em added the awaiting-author Waiting for PR author to address issues label Nov 19, 2024
@kim-em
Copy link
Collaborator

kim-em commented Nov 19, 2024

@luisacicolini, just a quick request re: the PR description. Thanks for adding a paragraph beginning "This PR ..." --- we know automatically extract these to incorporate in the draft release notes. Having PR authors write them saves us lots of time! But it means that things like "cc: @bollu" need to go in a separate paragraph, otherwise they may end up in the release notes!

@kim-em kim-em enabled auto-merge November 19, 2024 21:32
@kim-em kim-em added changelog-library Library and removed awaiting-author Waiting for PR author to address issues labels Nov 19, 2024
@kim-em kim-em added this pull request to the merge queue Nov 19, 2024
@luisacicolini
Copy link
Contributor Author

got it @kim-em! And thanks for reviewing this :)

Merged via the queue into leanprover:master with commit 3c75551 Nov 19, 2024
18 of 20 checks passed
JovanGerb pushed a commit to JovanGerb/lean4 that referenced this pull request Jan 21, 2025
@luisacicolini @bollu
@tobiasgrosser @JovanGerb
feat: add BitVec.(msb, getMsbD)_(rotateLeft, rotateRight) (leanprov…
7447b96 
…er#6120)

This PR adds theorems `BitVec.(getMsbD, msb)_(rotateLeft, rotateRight)`.

We follow the same strategy taken for `getLsbD`, constructing the
necessary auxilliary theorems first (relying on different hypotheses)
and then generalizing.

---------

Co-authored-by: Siddharth <[email protected]>
Co-authored-by: Tobias Grosser <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@tobiasgrosser tobiasgrosser tobiasgrosser left review comments

@kim-em kim-em kim-em left review comments

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.
4 participants
@luisacicolini @leanprover-community-bot @kim-em @tobiasgrosser