Skip to content

[Merged by Bors] - feat: mixin ordered algebraic typeclasses#20593

Closed
astrainfinita wants to merge 93 commits intomasterfrom
FR_ordered_mixin
Closed

[Merged by Bors] - feat: mixin ordered algebraic typeclasses#20593
astrainfinita wants to merge 93 commits intomasterfrom
FR_ordered_mixin

Conversation

@astrainfinita
Copy link
Copy Markdown
Collaborator

@astrainfinita astrainfinita commented Jan 9, 2025 •
edited
Loading

@astrainfinita
Squashed commit of the following:
b1b9b64 
commit 7561e65e55f1dbba1058c43ca1701038ceed98dc
Author: negiizhao <[email protected]>
Date:   Wed Jun 5 04:26:04 2024 +0800

    fix

commit 777db8a7d19ed4d66815f9575206992ca578cb5e
Merge: cc6eede 52b851a
Author: negiizhao <[email protected]>
Date:   Wed Jun 5 04:25:36 2024 +0800

    Merge branch 'master' into FR_canonically

commit cc6eede
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 15:01:00 2023 +0800

    fix

commit ae1dfda
Merge: c1931cf 1a749e0
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 14:10:05 2023 +0800

    Merge branch 'FR_covariance_instance' into FR_canonically

commit c1931cf
Merge: 9e0f667 6cab3d6
Author: negiizhao <[email protected]>
Date:   Thu Dec 28 14:09:53 2023 +0800

    Merge branch 'master' into FR_canonically

commit 1a749e0
Author: negiizhao <[email protected]>
Date:   Tue Dec 26 04:24:52 2023 +0800

    revert some instance changes

commit a6e645f
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 11:01:06 2023 +0800

    fix

commit 6af13a5
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 10:06:19 2023 +0800

    Revert "fix"

    This reverts commit 7ebd135.

commit 63a181b
Author: negiizhao <[email protected]>
Date:   Mon Dec 25 09:49:50 2023 +0800

    hack

commit 7ebd135
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 14:25:47 2023 +0800

    fix

commit 20d2809
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 14:13:08 2023 +0800

    chore: remove redundant instances

commit 9e0f667
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 12:45:15 2023 +0800

    fix

commit bf51f25
Merge: bd9e5b4 e9fb5b3
Author: negiizhao <[email protected]>
Date:   Sun Dec 24 12:00:56 2023 +0800

    Merge branch 'master' into FR_canonically

commit bd9e5b4
Author: negiizhao <[email protected]>
Date:   Tue Oct 24 01:49:05 2023 +0800

    nolint again

commit 6414331
Author: negiizhao <[email protected]>
Date:   Tue Oct 24 00:36:00 2023 +0800

    reduce diffs

commit 6d1f059
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 19:41:50 2023 +0800

    Revert "remove nolint"

    This reverts commit d60fc68.

commit d60fc68
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 10:24:07 2023 +0800

    remove nolint

commit 86f6ec7
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 10:23:24 2023 +0800

    fix

commit a3d8af1
Merge: 58e2ba8 801dc0d
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 09:53:43 2023 +0800

    Merge branch 'master' into FR_canonically

commit 58e2ba8
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 09:52:49 2023 +0800

    reduce diffs

commit be2b4bb
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 08:58:03 2023 +0800

    `[Mul α] [LE α]` -> `[Monoid α] [PartialOrder α]`

commit 0777b07
Author: negiizhao <[email protected]>
Date:   Mon Oct 23 02:46:01 2023 +0800

    rerun bench please

commit 6415bc9
Author: negiizhao <[email protected]>
Date:   Sun Oct 22 18:30:20 2023 +0800

    fix

commit 14cdac7
Author: negiizhao <[email protected]>
Date:   Sun Oct 22 14:11:31 2023 +0800

    nolint

commit 5bc0815
Author: Mario Carneiro <[email protected]>
Date:   Sat Oct 21 17:30:57 2023 -0400

    chore: bump lean toolchain

commit 86c8440
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 23:50:53 2023 +0800

    fix

commit f14bdc9
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 23:07:59 2023 +0800

    fix

commit 5feb528
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 22:41:09 2023 +0800

    fix

commit 958c4a5
Author: negiizhao <[email protected]>
Date:   Sat Oct 21 22:07:26 2023 +0800

    fix

commit fae1c85
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 21:07:44 2023 +0800

    fix

commit e6309d6
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:07:09 2023 +0800

    fix merge

commit a619670
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:06:29 2023 +0800

    oops

commit 9c3d72d
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:04:15 2023 +0800

    fix merge

commit 8a76d2e
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 20:01:16 2023 +0800

    fix merge

commit 7793f03
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 19:59:08 2023 +0800

    fix

commit 659f503
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:59:49 2023 +0800

    fix merge

commit a259cc5
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:54:10 2023 +0800

    fix

commit d6eb31f
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 18:18:02 2023 +0800

    fix

commit 2650679
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 16:31:11 2023 +0800

    fix

commit 5bfb9ec
Merge: c5279c0 08a8af0
Author: negiizhao <[email protected]>
Date:   Fri Oct 20 16:19:14 2023 +0800

    Merge branch 'master' into FR_canonically

commit c5279c0
Author: negiizhao <[email protected]>
Date:   Mon Aug 7 02:47:06 2023 +0800

    lint

commit 19a377f
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 16:57:10 2023 +0800

    lint

commit 048b120
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 15:43:32 2023 +0800

    fix counterexamples

commit 94663ee
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 14:22:22 2023 +0800

    lint style

commit 426dd03
Author: negiizhao <[email protected]>
Date:   Thu Aug 3 14:00:46 2023 +0800

    refactor: make `CanonicallyOrdered...` mixin

    I think this is the proposed refactor.

    However it seems that all things get slower... :(

    Need more love to speed it up.
@astrainfinita
fix
bea3ff0
@astrainfinita
fixfixfix
c24d120
@astrainfinita
remove ancient fixes
f7dfbca
@astrainfinita
shake & lint
ac14b47
@astrainfinita
style
9e571ae
@astrainfinita
remove ancient fixes
ffb2b14
@astrainfinita
Merge branch 'master' into FR_canonically_retry
a200e49
@astrainfinita
Merge branch 'master' into FR_canonically_retry
2028556
@astrainfinita
fix
c7a99cd
@astrainfinita
fix
51def2a
@astrainfinita
Merge branch 'master' into FR_canonically_retry
1542e4e
@astrainfinita
fix
5ee9202
@astrainfinita
fix
33f661d
@astrainfinita
fix
1d3e479
@astrainfinita
fix
283a50c
@astrainfinita
fix
19de397
@astrainfinita
fix
fcba328
@astrainfinita
shake
d729855
@astrainfinita
shake Mathlib.Algebra.Order.Ring.Nat
48e4de6
@astrainfinita
reduce diffs
78a4056
@astrainfinita
fix
6c63912
@astrainfinita
fix
0cdcc93
@astrainfinita
shake
194715e
@astrainfinita
lint
633ee02
@astrainfinita
remove a bad instance
3cbc9a3
@astrainfinita
not shortcuts now
67a9f17
@astrainfinita
fix merge
be85fcb
@astrainfinita
remove ancient fixes (instance priority)
7d6bbf8
@astrainfinita
examples should be removed
c303c30
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 2, 2025
@astrainfinita astrainfinita removed the awaiting-author A reviewer has asked the author a question or requested changes. label Apr 2, 2025
@astrainfinita
Copy link
Copy Markdown
Collaborator Author

astrainfinita commented Apr 2, 2025

Yes, this is part of #20676. I have no idea to make this PR looks better...

@fpvandoorn fpvandoorn added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 2, 2025
fpvandoorn
fpvandoorn reviewed Apr 2, 2025
View reviewed changes
fpvandoorn
fpvandoorn reviewed Apr 2, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

LGTM

I'm happy with this temporary performance hit, as long as the author plans to continue with the future performance improvements we get by removing classes and replacing them by these new ones.

@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Apr 2, 2025
@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Apr 2, 2025

LGTM, but I'd like a second opinion

maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 2, 2025

🚀 Pull request has been placed on the maintainer queue by fpvandoorn.

@github-actions github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Apr 2, 2025
sgouezel
sgouezel reviewed Apr 2, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@sgouezel sgouezel left a comment

Choose a reason for hiding this comment

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

I am fine with the idea of a transitory nonoptimal mathlib, given that having these as mixins is clearly a very good idea on the longer term. Still, having three pairs of eyes is better than two, so:
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 2, 2025

🚀 Pull request has been placed on the maintainer queue by sgouezel.

@kbuzzard kbuzzard mentioned this pull request Apr 2, 2025
Closed
1 task
plp127
plp127 reviewed Apr 2, 2025
View reviewed changes
Mathlib/Algebra/Order/Monoid/Defs.lean
-- TODO: assume weaker typeclasses

/-- An ordered (additive) monoid is a monoid with a partial order such that addition is monotone. -/
class IsOrderedAddMonoid (α : Type*) [AddCommMonoid α] [PartialOrder α] where
Copy link
Copy Markdown
Contributor

@plp127 plp127 Apr 2, 2025

Choose a reason for hiding this comment

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

I'm a bit uncomfortable with [AddCommMonoid α] since that would mean this doesn't apply to ordinals. What's the reason for including it here?

Copy link
Copy Markdown
Collaborator Author

@astrainfinita astrainfinita Apr 3, 2025

Choose a reason for hiding this comment

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

Currently there are no weakening of any typeclass. One reason is to avoid the impact on performance. Also, a TODO has been left on the first line.

@grunweg
Copy link
Copy Markdown
Contributor

grunweg commented Apr 3, 2025

I am not a maintainer, but agree with the above:
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Apr 3, 2025

🚀 Pull request has been placed on the maintainer queue by grunweg.

@fpvandoorn
Copy link
Copy Markdown
Member

fpvandoorn commented Apr 3, 2025

Ok, there seems to be clearly enough support for this.

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Apr 3, 2025
mathlib-bors bot pushed a commit that referenced this pull request Apr 3, 2025
@astrainfinita
feat: mixin ordered algebraic typeclasses (#20593)
b7e7d34
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 3, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: mixin ordered algebraic typeclasses [Merged by Bors] - feat: mixin ordered algebraic typeclasses Apr 3, 2025
@mathlib-bors mathlib-bors bot closed this Apr 3, 2025
@mathlib-bors mathlib-bors bot deleted the FR_ordered_mixin branch April 3, 2025 15:25
tannerduve pushed a commit that referenced this pull request May 13, 2025
@astrainfinita @tannerduve
feat: mixin ordered algebraic typeclasses (#20593)
7f64195
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fpvandoorn fpvandoorn fpvandoorn left review comments

@sgouezel sgouezel sgouezel left review comments

@plp127 plp127 plp127 left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-algebra Algebra (groups, rings, fields, etc) t-order Order theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

9 participants

@astrainfinita @mathlib4-dependent-issues-bot @grunweg @leanprover-bot @kbuzzard @fpvandoorn @sgouezel @plp127 @leanprover-community-bot-assistant