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] - refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for linear_ordered_comm_group_with_zero #7645

Closed
wants to merge 339 commits into from
Closed

[Merged by Bors] - refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for linear_ordered_comm_group_with_zero #7645

wants to merge 339 commits into from

Conversation

adomani
Copy link
Collaborator

@adomani adomani commented May 18, 2021 •
edited by github-actions bot

This PR continues the refactor of the ordered hierarchy, begun in #7371.

In this iteration, I weakened the assumptions of the lemmas in ordered_group. The bulk of the changes are in the two files

  • algebra/ordered_monoid_lemmas
  • algebra/ordered_group

while the remaining files have been edited mostly to accommodate for name/assumption changes.

I have tried to be careful to maintain the exact assumptions of each one of the norm_num and linarith lemmas. For this reason, some lemmas have a proof that is simply an application of a lemma with weaker assumptions. The end result is that no lemma whose proof involved a call to norm_num or linarith broke.

Open in Gitpod

@adomani adomani added the awaiting-review The author would like community review of the PR label May 18, 2021
@sgouezel
Copy link
Collaborator

Not directly related to this PR, but I just noticed that covariant_class and contravariant_class are registered as Type, not Prop. It should instead be

class covariant_class : Prop :=
(covc : covariant M N μ r)

@adomani
Copy link
Collaborator Author

adomani commented May 21, 2021

Sébastien, I changed the classes from Type to Prop, but honestly, I do not know what this change does. I remember that you already mentioned that this was a subtle but important point, but I could not figure out the difference between the two, in practical term.

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 25, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label May 25, 2021
@fpvandoorn
Copy link
Member

fpvandoorn commented Jul 10, 2021 •
edited

Oh great! I misread the fact that you changed labels. I thought you put it back to awaiting-review, but I see you did it the other way around. I tend to forget to change labels after I review :)

No need to ping me once you're done. I generally look though all Github notifications on PRs I've interacted with (but feel free to ping me once it's waiting for a few days).

@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 23, 2021
@github-actions
Copy link

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 15, 2022
@adomani adomani added awaiting-CI The author would like to see what CI has to say before doing more work. and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 26, 2022
@adomani
Copy link
Collaborator Author

adomani commented Jan 26, 2022

After a really long time, this PR is finally ready again for review!

@adomani adomani added awaiting-review The author would like community review of the PR and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Jan 26, 2022
jcommelin
jcommelin reviewed Jan 28, 2022
View reviewed changes
src/algebra/order/with_zero.lean Outdated
... ≤ x * x ^ n : mul_le_mul_left' (left.one_le_pow_of_le H) x
... = x ^ n.succ : (pow_succ x n).symm

--alias left.one_le_pow_of_le ← one_le_pow_of_one_le'
Copy link
Member

Choose a reason for hiding this comment

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

Is this intentionally commented out?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

The lemma name one_le_pow_of_one_le' is already used, so I simply removed the comment. Now that the refactor is getting to lemmas that already exist, there might be a little bit of cleaning up to remove duplicates.

I would leave this for subsequent PRs, though!

@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Jan 28, 2022

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

@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 Jan 28, 2022
@adomani
Copy link
Collaborator Author

adomani commented Jan 28, 2022

bors r+

@adomani
Copy link
Collaborator Author

adomani commented Jan 28, 2022

Thank you, Johan for the approval! I am really happy to get this moving again!

bors bot pushed a commit that referenced this pull request Jan 28, 2022
@adomani
refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take…
7e8cb75 
… advantage of the new classes for `linear_ordered_comm_group_with_zero` (#7645)

This PR continues the refactor of the `ordered` hierarchy, begun in #7371.

In this iteration, I weakened the assumptions of the lemmas in `ordered_group`.  The bulk of the changes are in the two files

* `algebra/ordered_monoid_lemmas`
* `algebra/ordered_group`

while the remaining files have been edited mostly to accommodate for name/assumption changes.

I have tried to be careful to maintain the **exact** assumptions of each one of the `norm_num` and `linarith` lemmas.  For this reason, some lemmas have a proof that is simply an application of a lemma with weaker assumptions.  The end result is that no lemma whose proof involved a call to `norm_num` or `linarith` broke.
@bors
Copy link

bors bot commented Jan 28, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for linear_ordered_comm_group_with_zero [Merged by Bors] - refactor(algebra/linear_ordered_comm_group_with_zero, *): mostly take advantage of the new classes for linear_ordered_comm_group_with_zero Jan 28, 2022
@bors bors bot closed this Jan 28, 2022
@bors bors bot deleted the adomani_ordered_stuff branch January 28, 2022 18:46
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@jcommelin jcommelin jcommelin left review comments

@fpvandoorn fpvandoorn fpvandoorn 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
6 participants
@adomani @sgouezel @fpvandoorn @jcommelin @eric-wieser @leanprover-community-bot-assistant