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

[Merged by Bors] - feat(data/zmod): a lemma on zmod.val_min_abs on negations #17584

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(data/zmod): a lemma on zmod.val_min_abs on negations #17584

wants to merge 19 commits into from

Conversation

javra
Copy link
Collaborator

@javra javra commented Nov 17, 2022

And two necessary lemmas about nat, courtesy of @kmill .

Co-authored-by: Kyle Miller @kmill

Open in Gitpod

@javra javra added the awaiting-review The author would like community review of the PR label Nov 17, 2022
eric-wieser
eric-wieser reviewed Nov 24, 2022
View reviewed changes
src/data/zmod/basic.lean Outdated
{ exfalso, exact h'' (nat.le_half_of_half_lt_sub (not_le.mp h')) }
end

lemma val_min_abs_neg_of_eq_half {n : ℕ} {a : zmod n} (ha : 2 * a.val = n) :
Copy link
Member

Choose a reason for hiding this comment

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

Just to check; eq_half is a deliberate naming of 2 * a.val = n even though it doesn't actually mention / 2; as opposed to being left over from a previous iteration?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, but only due to me not being able to come up with a good alternative. ...of_two_mul_eq maybe?

eric-wieser
eric-wieser approved these changes Nov 24, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Thanks!

javra and others added 2 commits November 24, 2022 10:45
@javra @eric-wieser
apply @eric-wieser's suggestions
c9620fb 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@alreadydone
refactor
41bec7c
@alreadydone
Copy link
Collaborator

I did some refactors at this branch, introducing new lemmas to golf existing proofs and the main result of this PR without using the two lemmas in nat.order.basic. You may adopt whatever you think is good, or I could open another PR.

@javra
Copy link
Collaborator Author

javra commented Nov 27, 2022

@alreadydone Looks good, I'll pull this into this one! By the way, do you have a good idea on how to prove (a + b).val_min_abs.nat_abs ≤ (a.val_min_abs + b.val_min_abs).nat_abs without going through all eight if splits separately? I've proven a.val_min_abs.nat_abs = min a.val (n - a.val) by now, which I should probably just add to this PR

@alreadydone
Copy link
Collaborator

alreadydone commented Nov 27, 2022 •
edited

@javra I worked out a proof in this commit.

jcommelin
jcommelin approved these changes Dec 7, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@jcommelin
Copy link
Member

Hmm, there are merge conflicts.

bors r-
bors d+

@bors
Copy link

bors bot commented Dec 7, 2022

✌️ javra can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@bors
Copy link

bors bot commented Dec 7, 2022

Canceled.

@github-actions github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Dec 7, 2022
@javra
Copy link
Collaborator Author

javra commented Dec 7, 2022

bors r+

bors bot pushed a commit that referenced this pull request Dec 7, 2022
@javra @alreadydone
feat(data/zmod): a lemma on zmod.val_min_abs on negations (#17584)
75bf566 
And two necessary lemmas about `nat`, courtesy of @kmill .

Co-authored-by: Kyle Miller @kmill 



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>
@bors
Copy link

bors bot commented Dec 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(data/zmod): a lemma on zmod.val_min_abs on negations [Merged by Bors] - feat(data/zmod): a lemma on zmod.val_min_abs on negations Dec 7, 2022
@bors bors bot closed this Dec 7, 2022
@bors bors bot deleted the zmod_neg branch December 7, 2022 23:43
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@alreadydone alreadydone alreadydone left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

@jcommelin jcommelin jcommelin approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@javra @alreadydone @jcommelin @eric-wieser