chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one` #16525

negiizhao · 2022-09-15T14:14:51Z

The fourth part of #16449

There are still some useless lemmas that were simply ported from algebra/order/monoid_lemmas, this PR removes them. "useless lemmas" are lemmas that just chain an existing lemma with an assumption and lemmas whose assumptions imply 1 ≤ 0. These lemmas were simply ported from algebra/order/monoid_lemmas.

Also, some lemmas have both assumptions like 1 < a 0 < a, this is because the file does not use type classes like zero_le_one_class currently. This PR puts these lemmas in the namespace without_zero_le_one.

mathlib4: leanprover-community/mathlib4#782

…e namespace `without_zero_le_one` The fourth part of #16449 There are still some useless lemmas which were simply ported from `algebra/order/monoid_lemmas`, this PR removes them. Also some lemmas have both assumptions like `1 < a` `0 < a`, this is because the file does not use type classes like `zero_le_one_class` currently. So I put these lemmas in the namespace `without_zero_le_one`.

eric-wieser · 2022-10-25T13:15:16Z

src/algebra/order/ring_lemmas.lean

-lemma mul_le_of_le_one_left [mul_pos_mono α] (hb : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b :=
-by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb
+lemma mul_le_of_le_one_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a :=
+by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0

-lemma le_mul_of_one_le_left [mul_pos_mono α] (hb : 0 ≤ b) (h : 1 ≤ a) : b ≤ a * b :=
-by simpa only [one_mul] using mul_le_mul_of_nonneg_right h hb
+lemma le_mul_of_one_le_right [pos_mul_mono α] (a0 : 0 ≤ a) (h : 1 ≤ b) : a ≤ a * b :=
+by simpa only [mul_one] using mul_le_mul_of_nonneg_left h a0

-lemma mul_le_of_le_one_right [pos_mul_mono α] (ha : 0 ≤ a) (h : b ≤ 1) : a * b ≤ a :=
-by simpa only [mul_one] using mul_le_mul_of_nonneg_left h ha
+lemma mul_le_of_le_one_left [mul_pos_mono α] (b0 : 0 ≤ b) (h : a ≤ 1) : a * b ≤ b :=
+by simpa only [one_mul] using mul_le_mul_of_nonneg_right h b0


Why did you swap the orders of these? It just makes the diff a lot bigger.

(also as a LTR language, I would expect the left lemmas to come before the right lemmas anyway)

This order is consistent with the previous lemmas in the file. Also the order of their typeclass assumptions is consistent with the conventions in this file.

semorrison · 2022-11-11T08:52:56Z

Do we actually need the lemmas in without_zero_le_one? It seems they aren't used anywhere; this might be chance to just dump them?

negiizhao · 2022-11-11T11:14:54Z

These can be dumped currently, but I'm thinking of strengthening these lemmas by using zero_le_one_class and replacing lemmas in algebra/order/ring/defs in the future.

YaelDillies · 2023-01-11T20:59:12Z

Could you explain what your definition of "useless lemma" is in the PR description and either

delete the lemmas in the without_zero_le_one namespace
add a zero_le_one_class assumption to each of them and instead delete the ordered ring lemmas and give an example where the generalised lemmas would be useful

negiizhao · 2023-01-13T00:09:25Z

"useless lemmas" is what you mentioned in doc-string and lemmas whose assumptions imply 1 ≤ 0.

Yaël: What's the point of these lemmas? They just chain an existing lemma with an assumption in
all possible ways, thereby artificially inflating the API and making the truly relevant lemmas hard
to find

These lemmas were simply ported from algebra/order/monoid_lemmas as I mentioned before.

I made PR #18158 to add zero_le_one_class assumption to each of them. #18157 shows ereal would have some covariance typeclasses and zero_le_one_class, but it has no semiring structure.

YaelDillies · 2023-01-15T21:59:48Z

I know what I meant. I'm just asking you to let everyone else know by putting it in the PR description 😄

riccardobrasca · 2023-07-26T12:25:15Z

Can you please fix the conflict?

semorrison · 2023-07-30T22:20:32Z

@YaelDillies, could you comment on this PR? What remains to be done?

eric-wieser · 2024-03-23T23:17:44Z

Closing, since this was ported to leanprover-community/mathlib4#9250

negiizhao added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. t-algebra Algebra (groups, rings, fields etc) t-order Order hierarchy labels Sep 15, 2022

Update bernstein.lean

0ba9c6c

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Sep 16, 2022

riccardobrasca requested a review from YaelDillies September 27, 2022 09:36

YaelDillies added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 8, 2022

Merge renaming file

8ab405c

negiizhao removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 10, 2022

fix

5090a16

eric-wieser reviewed Oct 25, 2022

View reviewed changes

Merge branch 'master' into FR_order_refactor18

19799d9

negiizhao changed the title ~~chore(algebra/order/monoid_lemmas_zero_lt): remove useless lemmas, use namespace without_zero_le_one~~ chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one Nov 8, 2022

Merge branch 'master' into FR_order_refactor18

a776928

negiizhao mentioned this pull request Nov 29, 2022

feat: synchronize with mathlib3 #16525 leanprover-community/mathlib4#784

Closed

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed awaiting-review The author would like community review of the PR labels Jan 7, 2023

Merge branch 'master' into FR_order_refactor18

c138dea

negiizhao 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 merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Jan 7, 2023

Merge branch 'master' into FR_order_refactor18

7774834

negiizhao mentioned this pull request Jan 13, 2023

feat(algebra/order/ring/lemmas): use typeclass zero_le_one_class #18158

Closed

1 task

eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023

semorrison 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 28, 2023

Merge branch 'master' into FR_order_refactor18

9c0bf19

negiizhao added awaiting-review The author would like community review of the PR 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 Jul 28, 2023

github-actions bot added modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. and removed awaiting-CI The author would like to see what CI has to say before doing more work. labels Jul 28, 2023

negiizhao mentioned this pull request Dec 23, 2023

chore(Algebra/Order/Lemmas): remove useless lemmas, use ZeroLEOneClass leanprover-community/mathlib4#9250

Open

eric-wieser closed this Mar 23, 2024

YaelDillies removed awaiting-review The author would like community review of the PR not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 labels Mar 24, 2024

YaelDillies removed their request for review March 24, 2024 08:39

YaelDillies deleted the FR_order_refactor18 branch March 24, 2024 08:40

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one` #16525

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one` #16525

negiizhao commented Sep 15, 2022 •

edited

eric-wieser Oct 25, 2022

eric-wieser Oct 25, 2022

negiizhao Oct 25, 2022

semorrison commented Nov 11, 2022

negiizhao commented Nov 11, 2022 •

edited

YaelDillies commented Jan 11, 2023

negiizhao commented Jan 13, 2023

YaelDillies commented Jan 15, 2023

riccardobrasca commented Jul 26, 2023

semorrison commented Jul 30, 2023

eric-wieser commented Mar 23, 2024

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one #16525

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace without_zero_le_one #16525

Conversation

negiizhao commented Sep 15, 2022 • edited

eric-wieser Oct 25, 2022

Choose a reason for hiding this comment

eric-wieser Oct 25, 2022

Choose a reason for hiding this comment

negiizhao Oct 25, 2022

Choose a reason for hiding this comment

semorrison commented Nov 11, 2022

negiizhao commented Nov 11, 2022 • edited

YaelDillies commented Jan 11, 2023

negiizhao commented Jan 13, 2023

YaelDillies commented Jan 15, 2023

riccardobrasca commented Jul 26, 2023

semorrison commented Jul 30, 2023

eric-wieser commented Mar 23, 2024

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one` #16525

chore(algebra/order/ring/lemmas): remove useless lemmas, use namespace `without_zero_le_one` #16525

negiizhao commented Sep 15, 2022 •

edited

negiizhao commented Nov 11, 2022 •

edited