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: sshiftRight bitblasting #4889

Merged
merged 3 commits into from
Aug 7, 2024
Merged

feat: sshiftRight bitblasting #4889

merged 3 commits into from
Aug 7, 2024

Conversation

bollu
Copy link
Contributor

@bollu bollu commented Jul 31, 2024 •
edited
Loading

We follow the same strategy as #4872, #4571, and implement bitblasting theorems for sshiftRight.

@bollu bollu force-pushed the upstream-sshiftRight-recurrence branch 2 times, most recently from 6438ca8 to e77c047 Compare July 31, 2024 21:08
@bollu
feat: sshiftRight bitblasting
8d8183f 
This mimics leanprover#4872
for arithmetic shift right.

This adds theorems sshiftRight_rec_zero, sshiftRight_rec_succ,
sshiftRight_rec_eq, and shiftRight_eq_shiftRight_rec.
@bollu bollu force-pushed the upstream-sshiftRight-recurrence branch from e77c047 to 8d8183f Compare July 31, 2024 21:10
@tobiasgrosser
Copy link
Contributor

This looks good from my side. I am curious what @alexkeizer and @semorrison think.

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

leanprover-community-mathlib4-bot commented Jul 31, 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 dcea47db02a61616060dcc0f6ac19e8e6300b8cc --onto 8acdafd5b3957382c02779ada451c14da44e2aca. (2024-07-31 21:27:15)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e83f78d5af8887d2d384e2405adf85e3ee72fec4 --onto 8acdafd5b3957382c02779ada451c14da44e2aca. (2024-08-01 09:07:20)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e83f78d5af8887d2d384e2405adf85e3ee72fec4 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-05 15:23:45)

@tobiasgrosser
Copy link
Contributor

@bollu, I resolved the merge conflicts. You can undraft this now (also update the PR message to reflect this).

@bollu bollu marked this pull request as ready for review August 1, 2024 13:27
@bollu bollu requested a review from kim-em as a code owner August 1, 2024 13:27
@bollu
Copy link
Contributor Author

bollu commented Aug 1, 2024

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Aug 1, 2024
@leanprover-bot leanprover-bot added the P-high We will work on this issue label Aug 2, 2024
@kim-em kim-em added this pull request to the merge queue Aug 7, 2024
Merged via the queue into leanprover:master with commit e106be1 Aug 7, 2024
12 checks passed
@tobiasgrosser tobiasgrosser mentioned this pull request Aug 8, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

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

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR P-high We will work on this issue 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.
5 participants
@bollu @tobiasgrosser @leanprover-community-mathlib4-bot @kim-em @leanprover-bot