[Merged by Bors] - refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'` by vihdzp · Pull Request #15071 · leanprover-community/mathlib3

vihdzp · 2022-06-30T11:54:28Z

The predicate x ≤ y → y = x is no more convenient than ¬ x < y. For this reason, we ditch well_founded.well_founded_iff_has_min' and well_founded.well_founded_iff_has_max' in favor of well_founded.well_founded_iff_has_min (or in some cases, just well_founded.has_min. We also remove the misplaced lemma well_founded.eq_iff_not_lt_of_le, and we golf the theorems that used the removed theorems.

The lemma well_founded.well_founded_iff_has_min has a misleading name when applied on well_founded (>), and mildly screws over dot notation and rewriting by virtue of using >, but a future refactor will fix this.

depends on: [Merged by Bors] - feat(order/order_iso_nat): generalize well_founded.monotone_chain_condition to preorders #15073

If we wanted to, we could golf eq_iff_not_lt_of_le and move it to order/basic.lean, but I'd rather not bother. It's just the negation of lt_iff_le_and_ne.

…_min'

ghost · 2022-07-12T16:46:28Z

This PR/issue depends on:

~~[Merged by Bors] - feat(order/order_iso_nat): generalize well_founded.monotone_chain_condition to preorders #15073~~
By Dependent Issues (🤖). Happy coding!

kbuzzard · 2022-07-20T14:51:46Z

The change seems to make proofs smaller, or at least no bigger.

Vierkantor

The evidence from the refactor seems to show that has_min' and has_max' are typically not the right way to go, so I'm okay with removing them.

Could you merge master before bors mergeing?

bors d+

src/order/well_founded.lean

bors · 2022-09-30T11:11:42Z

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

YaelDillies · 2023-02-12T09:50:40Z

src/ring_theory/artinian.lean


 theorem is_artinian.set_has_minimal [is_artinian R M] (a : set $ submodule R M) (ha : a.nonempty) :
-  ∃ M' ∈ a, ∀ I ∈ a, I ≤ M' → I = M' :=
+  ∃ M' ∈ a, ∀ I ∈ a, ¬ I < M' :=


I'm not sure this is an improvement. ¬ a < b is the correct condition in the generality of preorders, but once you get to a partial_order a ≤ b → a = b is nicer empirically.

To be clear, I'm happy for you to ditch the two well-founded lemmas, but I think you shouldn't change unrelated lemma statements. You can keep the changes internal to the proofs.

"A minimal element is one for which no other element is lesser". I believe my restatement of the lemma much better captures this. Besides, from I ≤ M' and ¬ I < M' one can directly prove I = M' by using eq_of_le_of_not_lt.

Anyways, I won't be petty about this. I thought that the current statement of this lemma reflected the statement of the lemma I deleted, and thus I changed it accordingly. But if you still think this change is unhelpful, I'll revert it.

Yeah I think it's a matter of people not liking to write "a is such that if a ≤ b then a = b" on paper, even though it's better for formalisation.

vihdzp · 2023-03-31T21:09:44Z

bors r+

…well_founded_iff_has_max'` (#15071) The predicate `x ≤ y → y = x` is no more convenient than `¬ x < y`. For this reason, we ditch `well_founded.well_founded_iff_has_min'` and `well_founded.well_founded_iff_has_max'` in favor of `well_founded.well_founded_iff_has_min` (or in some cases, just `well_founded.has_min`. We also remove the misplaced lemma `well_founded.eq_iff_not_lt_of_le`, and we golf the theorems that used the removed theorems. The lemma `well_founded.well_founded_iff_has_min` has a misleading name when applied on `well_founded (>)`, and mildly screws over dot notation and rewriting by virtue of using `>`, but a future refactor will fix this.

bors · 2023-04-01T01:35:32Z

Pull request successfully merged into master.

Build succeeded:

tweak

f5257d3

vihdzp 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. labels Jun 30, 2022

vihdzp mentioned this pull request Jun 30, 2022

refactor(order/well_founded): typeclasses for well-founded < and > #15023

Closed

5 tasks

vihdzp added 2 commits June 30, 2022 07:24

Update order_iso_nat.lean

07f2eae

Update order_iso_nat.lean

eeed488

vihdzp changed the title ~~refactor(order/well_founded): ditch well_founded_iff_has_max' and well_founded_iff_has_min'~~ refactor(order/well_founded): ditch well_founded_iff_has_min' and well_founded_iff_has_max' Jun 30, 2022

vihdzp added 6 commits June 30, 2022 07:37

tweak

4f7136a

This form is useful actually

03aa251

fix

31a13ed

Update compactly_generated.lean

4c1cf78

fix

6f99f4c

generalize well_founded.monotone_chain_condition to preorders

c13e09d

ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jun 30, 2022

vihdzp added 4 commits June 30, 2022 10:46

Update pid.lean

7f30600

Update artinian.lean

a4be77d

Update artinian.lean

0809cb0

Merge branch 'monotone_chain_condition'' into is_well_founded_iff_has…

9da9258

…_min'

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

Update pid.lean

18c5da1

vihdzp added the awaiting-CI The author would like to see what CI has to say before doing more work. label Jul 1, 2022

Update engel.lean

51e1aa9

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

vihdzp added 5 commits June 30, 2022 22:45

golf

d64938e

Update well_founded_set.lean

be33e42

Merge branch 'monotone_chain_condition'' into is_well_founded_iff_has…

916ae41

…_min'

minor spacing tweaks

7415a38

Merge branch 'monotone_chain_condition'' into is_well_founded_iff_has…

0d83b61

…_min'

ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jul 12, 2022

Merge branch 'master' into is_well_founded_iff_has_min'

1dffdfe

vihdzp added 3 commits July 20, 2022 09:55

Merge branch 'master' into is_well_founded_iff_has_min'

aa42128

fix

4a5f01e

fix

06437ba

Vierkantor approved these changes Sep 30, 2022

View reviewed changes

src/order/well_founded.lean Show resolved Hide resolved

YaelDillies reviewed Feb 12, 2023

View reviewed changes

YaelDillies added awaiting-author A reviewer has asked the author a question or requested changes delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Feb 12, 2023

vihdzp added 4 commits February 27, 2023 21:23

move lemma

cb4aa2b

Merge branch 'master' into is_well_founded_iff_has_min'

00c743c

Merge branch 'master' into is_well_founded_iff_has_min'

f2f2f3d

fix

ab49a7e

vihdzp 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 awaiting-review The author would like community review of the PR labels Mar 31, 2023

bors bot changed the title ~~refactor(order/well_founded): ditch well_founded_iff_has_min' and well_founded_iff_has_max'~~ [Merged by Bors] - refactor(order/well_founded): ditch well_founded_iff_has_min' and well_founded_iff_has_max' Apr 1, 2023

bors bot closed this Apr 1, 2023

bors bot deleted the is_well_founded_iff_has_min' branch April 1, 2023 01:35

vihdzp mentioned this pull request Apr 3, 2023

[Merged by Bors] - feat: port #15071 leanprover-community/mathlib4#3248

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'`#15071

[Merged by Bors] - refactor(order/well_founded): ditch `well_founded_iff_has_min'` and `well_founded_iff_has_max'`#15071
vihdzp wants to merge 28 commits intomasterfrom
is_well_founded_iff_has_min'

vihdzp commented Jun 30, 2022 •

edited

Loading

Uh oh!

ghost commented Jul 12, 2022

Uh oh!

kbuzzard commented Jul 20, 2022

Uh oh!

Vierkantor left a comment

Uh oh!

Uh oh!

bors bot commented Sep 30, 2022

Uh oh!

YaelDillies Feb 12, 2023 •

edited

Loading

Uh oh!

vihdzp Feb 28, 2023

Uh oh!

YaelDillies Feb 28, 2023

Uh oh!

vihdzp commented Mar 31, 2023

Uh oh!

bors bot commented Apr 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

Conversation

vihdzp commented Jun 30, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented Jul 12, 2022

Uh oh!

kbuzzard commented Jul 20, 2022

Uh oh!

Vierkantor left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

bors bot commented Sep 30, 2022

Uh oh!

YaelDillies Feb 12, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

vihdzp Feb 28, 2023

Choose a reason for hiding this comment

Uh oh!

YaelDillies Feb 28, 2023

Choose a reason for hiding this comment

Uh oh!

vihdzp commented Mar 31, 2023

Uh oh!

bors bot commented Apr 1, 2023

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

vihdzp commented Jun 30, 2022 •

edited

Loading

YaelDillies Feb 12, 2023 •

edited

Loading