Skip to content

feat: characterize when T-division equals zero #8204

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
Open
bollu wants to merge 7 commits into
base: master
Choose a base branch
from
Open

feat: characterize when T-division equals zero #8204

bollu wants to merge 7 commits into from

Conversation

@bollu
Copy link
Contributor

@bollu bollu commented May 2, 2025

This PR adds the lemma Int.tdiv_eq_zero_iff_natAbs_lt_or_eq_zero which shows that T-division equals zero iff the absolute value of the numerator is less than the denominator, or the denominator equals zero:

@[simp] theorem tdiv_eq_zero_iff_natAbs_lt_or_eq_zero {a : Int} {b : Int} :
    a.tdiv b = 0 ↔ (a.natAbs < b.natAbs ∨ b = 0):= by

This was used in reasoning about the MSB of BitVec.sdiv. The strategy was
superced, but this lemma was extracted from the earlier proof.

@bollu
Copy link
Contributor Author

bollu commented May 2, 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 May 2, 2025
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8204
a686ad5
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 2, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#8204
c659bcf
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 2, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
eb20d53
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 2, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
da25887
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 2, 2025 •
edited
Loading

Mathlib CI status (docs):

  • 🟡 Mathlib branch lean-pr-testing-8204 build against this PR was cancelled. (2025-05-02 11:08:09) View Log
  • ✅ Mathlib branch lean-pr-testing-8204 has successfully built against this PR. (2025-05-02 11:55:35) View Log
  • ✅ Mathlib branch lean-pr-testing-8204 has successfully built against this PR. (2025-05-12 10:56:50) View Log
  • ✅ Mathlib branch lean-pr-testing-8204 has successfully built against this PR. (2025-06-06 14:49:47) View Log
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase ec9ff12fc65316c902224aa895a32ae943dcc762 --onto faffe863343211d03d07d4ef19d90a2aa9d6fc8c. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-14 14:47:32)

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 2, 2025
luisacicolini
luisacicolini reviewed May 12, 2025
View reviewed changes
luisacicolini
luisacicolini reviewed May 12, 2025
View reviewed changes
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 12, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
9c12fcf
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 12, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
b2f49f3
@bollu bollu marked this pull request as ready for review May 12, 2025 10:24
@bollu bollu requested a review from kim-em as a code owner May 12, 2025 10:24
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label May 13, 2025
tobiasgrosser
tobiasgrosser approved these changes May 27, 2025
View reviewed changes
Copy link
Contributor

@tobiasgrosser tobiasgrosser left a comment

Choose a reason for hiding this comment

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

LGTM.

alexkeizer
alexkeizer reviewed May 28, 2025
View reviewed changes
alexkeizer
alexkeizer reviewed May 28, 2025
View reviewed changes
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
96642d1
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2025
@leanprover-community-mathlib4-bot
Trigger CI for leanprover/lean4#8204
975a12f
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Jun 13, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for leanprover/lean4#8204
d196148
luisacicolini
luisacicolini reviewed Jun 14, 2025
View reviewed changes
bollu and others added 6 commits June 14, 2025 14:55
@bollu
feat: characterize when T-division equals zero
981595d 
This PR adds the lemma `Int.tdiv_eq_zero_iff_natAbs_lt_or_eq_zero`
which shows that T-division equals zero iff the absolute value
of the numerator is less than the denominator, or the denominator equals
zero.

This was used in reasoning about the MSB of `BitVec.sdiv`. The strategy was
superced, but this lemma was extracted from the earlier proof.
@bollu
chore: remove Int, make simp
de68586
@bollu
chore: cleanup, don't unfold tdiv
aebb74e
@bollu @luisacicolini
Apply suggestions from code review
0c79cb3 
Co-authored-by: Luisa Cicolini <[email protected]>
@bollu @alexkeizer
Update src/Init/Data/Int/DivMod/Lemmas.lean
368f235 
Co-authored-by: Alex Keizer <[email protected]>
@bollu @alexkeizer
Update src/Init/Data/Int/DivMod/Lemmas.lean
6b873c6 
Co-authored-by: Alex Keizer <[email protected]>
@bollu bollu force-pushed the tdiv-eq-zero-iff branch from 7549331 to 030aad1 Compare June 14, 2025 14:19
tobiasgrosser
tobiasgrosser approved these changes Jun 14, 2025
View reviewed changes
Copy link
Contributor

@tobiasgrosser tobiasgrosser left a comment

Choose a reason for hiding this comment

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

LGTM. Thank you, @bollu.

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

Reviewers

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

3 more reviewers

@alexkeizer alexkeizer alexkeizer left review comments

@luisacicolini luisacicolini luisacicolini approved these changes

@tobiasgrosser tobiasgrosser tobiasgrosser approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR changelog-library Library P-medium We may work on this issue if we find the time 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.

6 participants

@bollu @leanprover-community-bot @tobiasgrosser @alexkeizer @luisacicolini @leanprover-bot