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 ushiftRight_*_distrib theorems #4667

Merged
merged 3 commits into from
Aug 7, 2024
Merged

feat: add ushiftRight_*_distrib theorems #4667

merged 3 commits into from
Aug 7, 2024

Conversation

tobiasgrosser
Copy link
Contributor

@tobiasgrosser tobiasgrosser commented Jul 6, 2024 •
edited
Loading

No description provided.

@tobiasgrosser tobiasgrosser requested a review from kim-em as a code owner July 6, 2024 08:35
@tobiasgrosser tobiasgrosser marked this pull request as draft July 6, 2024 08:35
@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 6, 2024
@kim-em
Copy link
Collaborator

kim-em commented Jul 8, 2024

This is still set as a draft PR. Is that intentional?

@kim-em
Copy link
Collaborator

kim-em commented Jul 8, 2024

I still don't understand why we don't just have

@[simp] theorem ushiftRight_bitVec (a b : BitVec w) : a >>> b = a >>> b.toNat := rfl

I appreciate that you want to have a >>> operator where the second operand is a BitVec. But why would we want to reason about it separately from the version where the second operand is a Nat?

@leanprover-community-mathlib4-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 14d59b3599d0b4fbfaf147e7ede2d82cbad7a1e7 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-06 07:20:08)

@tobiasgrosser tobiasgrosser marked this pull request as ready for review August 6, 2024 08:39
@tobiasgrosser
Copy link
Contributor Author

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 14d59b3599d0b4fbfaf147e7ede2d82cbad7a1e7 --onto 647a5e94925791f6a16b629b6c16ffad60a7f478. (2024-08-06 07:20:08)

I have now moved these theorems to work on Nat on the RHS. This seems to be the canonical form we are aiming for.

@tobiasgrosser
Copy link
Contributor Author

awaiting-review

@github-actions github-actions bot added the awaiting-review Waiting for someone to review the PR label Aug 6, 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 cc42a17 Aug 7, 2024
12 checks passed
@tobiasgrosser tobiasgrosser mentioned this pull request Aug 8, 2024
Merged
github-merge-queue bot pushed a commit that referenced this pull request Aug 12, 2024
@tobiasgrosser
feat: add BitVec.[sshiftRight/shiftLeft]_*_distrib (#4951)
dfe493d 
After having added already `BitVec.ushiftRight_*_distrib`in
#4667 for ushiftRight, this PR
now completes the `*_distrib` theorems for shift.
Parcly-Taxel pushed a commit to Parcly-Taxel/lean4 that referenced this pull request Aug 12, 2024
@tobiasgrosser @Parcly-Taxel
feat: add BitVec.[sshiftRight/shiftLeft]_*_distrib (leanprover#4951)
c7fdfd6 
After having added already `BitVec.ushiftRight_*_distrib`in
leanprover#4667 for ushiftRight, this PR
now completes the `*_distrib` theorems for shift.
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

Assignees
No one assigned
Labels
awaiting-review Waiting for someone to review the PR 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
@tobiasgrosser @kim-em @leanprover-community-mathlib4-bot