[Merged by Bors] - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups #8060

adomani · 2021-06-23T18:37:31Z

This PR represents another wave of generalization of proofs, following from the order refactor. It is another step towards #7645.

depends on: [Merged by Bors] - feat(algebra/ordered_group): add a few instances, prune unneeded code #8075, containing a few small first steps.

depends on: [Merged by Bors] - refactor(algebra/ordered_monoid): use covariant + contravariant typeclasses in algebra/ordered_monoid #7999, where the waves washes over ordered_monoids.
depends on: [Merged by Bors] - chore(data/real/hyperreal): remove @ in a proof #8063, golf a proof on hyperreals.

…ravariant_file

…t_file

…ariant_file

…nprover-community/mathlib into adomani_covariant_contravariant_file

…t_only

…ntravariant_file

…ty/mathlib into adomani_ordered_group

fpvandoorn

In the first part you have lemmas which each of the four classes below. It would be good if you have the same pattern of lemmas for the four classes, following the same naming scheme (if possible while avoiding naming clashes):
[covariant_class α α (*) (≤)]
[covariant_class α α (*) (<)]
[covariant_class α α (function.swap (*)) (≤)]
[covariant_class α α (function.swap (*)) (<)]
There are currently quite some inconsistencies/omissions.

In some comments I ask about inconsistencies. To what extend is this because of trying to be (somewhat) backwards compatible?

src/algebra/ordered_group.lean

fpvandoorn · 2021-06-30T15:58:53Z

src/algebra/ordered_group.lean

-by { rw [mul_inv_cancel_right, mul_comm a, mul_inv_cancel_right] at this, rw [this] }
+by { rw [← mul_le_mul_iff_left a, ← mul_le_mul_iff_right b], simp }
+
+alias neg_le_neg_iff ↔ le_of_neg_le_neg _


Here and in other places, there are aliases only for additive operations. Is this just because the library doesn't use the multiplicative versions of these lemmas, but it does use the additive version?

Yes, most of the times (probably all, I do not remember), I reformulated the statement from the additive version to multiplicative with to_additive, and then I only introduced the alias for the additive version, since the multiplicative version was not in Lean before anyway.

src/algebra/ordered_group.lean

fpvandoorn · 2021-06-30T16:07:34Z

src/algebra/ordered_group.lean

-lemma le_abs_self (a : α) : a ≤ abs a := le_max_left _ _
-
-lemma neg_le_abs_self (a : α) : -a ≤ abs a := le_max_right _ _
-
 lemma neg_abs_le_self (a : α) : -abs a ≤ a :=


Is there a reason that the shorter proof doesn't work anymore?

Very superficially, neg_le uses both left and right monotonicity. Here we are only assuming one-sided monotonicity and trading the other side for linear_order. This should explain the le_total bit. The calc proof makes it look longer than it really is, but that is another matter! Does this clarify why the old proof does not work?

…a)variant` (#8072) In an attempt to break off small parts of PR #8060, I extracted some of the instances proven there to this PR. This is part of the `order` refactor. ~~I tried to get rid of the `@`, but failed. If you have a trick to avoid them, I would be very happy to learn it!~~ `@`s removed!

fpvandoorn · 2021-07-07T08:31:31Z

Thanks for the changes!

bors d+

bors · 2021-07-07T08:31:32Z

✌️ 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.

fpvandoorn · 2021-07-07T08:47:40Z

bors merge

… -- ordered groups (#8060) This PR represents another wave of generalization of proofs, following from the `order` refactor. It is another step towards #7645.

adomani · 2021-07-07T09:18:32Z

Floris, thank you so much for reviewing and for merging this! I think that the subsequent PRs will be shorter and more easily fractionable!

bors · 2021-07-07T10:24:34Z

Pull request successfully merged into master.

Build succeeded:

adomani added 30 commits June 10, 2021 05:17

is_symm_op.flip_eq

6c915df

data/real/nnreal

3daffc2

extra term mode

466dda7

Merge branch 'adomani_is_symm_op.flip_eq' into adomani_covariant_cont…

7bf24e2

…ravariant_file

introduce new file

b6906a8

ordered_monoid_lemmas

368d359

fix ordered_monoid

d75aba2

small fixes

bae865c

fix linear_ordered_comm_group_with_zero

3062462

change linarith lemmas

291d2df

algebra/big_operators/order

fc76ef6

Merge branch 'adomani_remove_ats' into adomani_covariant_contravarian…

b9e15dd

…t_file

quaternion

b47dfc8

zsqrtd

10054ce

Merge branch 'master' into adomani_covariant_contravariant_file

b6a53d6

remove #check

e324d60

algebra/linear_ordered_comm_group_with_zero.lean

9da1818

ordered_monoid

7fbdadf

ordered_monoid_again

e230d8c

by instead of begin end

6219ee1

Merge branch 'adomani_remove_more_ats' into adomani_covariant_contrav…

f4d2b43

…ariant_file

by apply

6f3197a

Merge branch 'master' into adomani_covariant_contravariant_file

7e4ab3a

Merge branch 'adomani_covariant_contravariant_file' of github.com:lea…

b3c7e15

…nprover-community/mathlib into adomani_covariant_contravariant_file

remove comment

a2215a5

Merge branch 'adomani_is_symm_op.flip_eq' into adomani_covariant_spli…

3623bcc

…t_only

create new file

1fa69d7

remove duplicates

a2e40f3

Merge branch 'adomani_covariant_split_only' into adomani_covariant_co…

3c5037e

…ntravariant_file

move

067dd33

adomani added the awaiting-review The author would like community review of the PR label Jun 29, 2021

adomani added 2 commits June 30, 2021 04:24

Merge branch 'adomani_ordered_group' of github.com:leanprover-communi…

c882b54

…ty/mathlib into adomani_ordered_group

remove duplicate instance

bff8c50

fpvandoorn reviewed Jun 30, 2021

View reviewed changes

fpvandoorn added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Jul 1, 2021

adomani added 3 commits July 2, 2021 10:00

apply Floris' suggestions from code review

170b34a

remove duplicate lemma

07913e9

fx

7d80b0d

adomani added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 2, 2021

github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 6, 2021

Merge branch 'master' into adomani_ordered_group

0a2b594

github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jul 7, 2021

adomani added 3 commits July 7, 2021 08:53

remove unneded file

c587898

remove @

5352985

formatting

02da46d

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 Jul 7, 2021

github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Jul 7, 2021

bors bot changed the title ~~refactor(algebra/ordered_group): another step in the order refactor -- ordered groups~~ [Merged by Bors] - refactor(algebra/ordered_group): another step in the order refactor -- ordered groups Jul 7, 2021

bors bot closed this Jul 7, 2021

bors bot deleted the adomani_ordered_group branch July 7, 2021 10:24

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups #8060

[Merged by Bors] - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups #8060

adomani commented Jun 23, 2021 •

edited by github-actions bot

fpvandoorn left a comment

fpvandoorn Jun 30, 2021

adomani Jul 2, 2021

fpvandoorn Jun 30, 2021

adomani Jul 2, 2021

fpvandoorn commented Jul 7, 2021

bors bot commented Jul 7, 2021

fpvandoorn commented Jul 7, 2021

adomani commented Jul 7, 2021

bors bot commented Jul 7, 2021

[Merged by Bors] - refactor(algebra/ordered_group): another step in the order refactor -- ordered groups #8060

[Merged by Bors] - refactor(algebra/ordered_group): another step in the order refactor -- ordered groups #8060

Conversation

adomani commented Jun 23, 2021 • edited by github-actions bot

fpvandoorn left a comment

Choose a reason for hiding this comment

fpvandoorn Jun 30, 2021

Choose a reason for hiding this comment

adomani Jul 2, 2021

Choose a reason for hiding this comment

fpvandoorn Jun 30, 2021

Choose a reason for hiding this comment

adomani Jul 2, 2021

Choose a reason for hiding this comment

fpvandoorn commented Jul 7, 2021

bors bot commented Jul 7, 2021

fpvandoorn commented Jul 7, 2021

adomani commented Jul 7, 2021

bors bot commented Jul 7, 2021

[Merged by Bors] - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups #8060

[Merged by Bors] - refactor(algebra/ordered_group): another step in the `order` refactor -- ordered groups #8060

adomani commented Jun 23, 2021 •

edited by github-actions bot