[Merged by Bors] - chore: use mixin ordered algebraic typeclasses (part 1)#20594
Closed
astrainfinita wants to merge 142 commits intomasterfrom
Closed
[Merged by Bors] - chore: use mixin ordered algebraic typeclasses (part 1)#20594astrainfinita wants to merge 142 commits intomasterfrom
astrainfinita wants to merge 142 commits intomasterfrom
Conversation
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.
Member
|
!bench |
Collaborator
|
Here are the benchmark results for commit df1585b. Benchmark Metric Change
=========================================================================================
- ~Mathlib.Algebra.Lie.Nilpotent instructions 12.4%
+ ~Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order instructions -8.2%
- ~Mathlib.Topology.Algebra.Field instructions 41.5% |
3 files, Instructions +9.0⬝10⁹
4 files, Instructions +5.0⬝10⁹
3 files, Instructions +4.0⬝10⁹
8 files, Instructions +3.0⬝10⁹
14 files, Instructions +2.0⬝10⁹
39 files, Instructions +1.0⬝10⁹
23 files, Instructions -2.0⬝10⁹
12 files, Instructions -3.0⬝10⁹
4 files, Instructions -4.0⬝10⁹
2 files, Instructions -5.0⬝10⁹
2 files, Instructions -6.0⬝10⁹
|
sgouezel
reviewed
Apr 4, 2025
Contributor
sgouezel
left a comment
sgouezel
left a comment
There was a problem hiding this comment.
Review of the beginning of the file, I have to stop for now. Thanks a lot for doing this!
| let _a ← synthInstanceQ (q(Semifield $α) : Q(Type u)) | ||
| let _a ← synthInstanceQ (q(LinearOrder $α) : Q(Type u)) | ||
| let _a ← synthInstanceQ (q(IsStrictOrderedRing $α) : Q(Prop)) | ||
| assumeInstancesCommute |
Contributor
There was a problem hiding this comment.
Just spotting things which are not "obviously" correct. I don't know anything about metaprogramming, so I don't know why you have inserted an assumeInstancesCommute here.
| theorem antitone_iff_map_nonneg : Antitone (f : α → β) ↔ ∀ a ≤ 0, 0 ≤ f a := | ||
| monotone_comp_ofDual_iff.symm.trans <| monotone_iff_map_nonneg (α := αᵒᵈ) (iamhc := iamhc) _ | ||
|
|
||
| variable [AddLeftStrictMono β] |
Contributor
There was a problem hiding this comment.
Just to point out that there is a strict improvement here: this typeclass was not necessary before, but this wasn't known to typeclass inference at this stage of the library.
kbuzzard
reviewed
Apr 4, 2025
| let _a ← synthInstanceQ (q(Semifield $α) : Q(Type u)) | ||
| let _a ← synthInstanceQ (q(LinearOrder $α) : Q(Type u)) | ||
| let _a ← synthInstanceQ (q(IsStrictOrderedRing $α) : Q(Prop)) | ||
| assumeInstancesCommute |
Member
There was a problem hiding this comment.
I don't feel confident to sign off on this addition of assumeInstancesCommute because I don't understand the code.
| let ra ← core zα pα a | ||
| let ofNonneg (pa : Q(0 ≤ $a)) (_oα : Q(LinearOrderedSemifield $α)) : | ||
| let ofNonneg (pa : Q(0 ≤ $a)) | ||
| (_oα : Q(Semifield $α)) (_oα : Q(LinearOrder $α)) (_oα : Q(IsStrictOrderedRing $α)) : |
Member
There was a problem hiding this comment.
Is it OK here and in other places to use the same variable names?
Contributor
There was a problem hiding this comment.
Do we even need variable names here and elsewhere?
| eval {u α} _ _ e := do | ||
| let ~q(@NonemptyInterval.length _ $ig $ipo $a) := e | | ||
| throwError "not NonemptyInterval.length" | ||
| let _i ← synthInstanceQ q(IsOrderedAddMonoid $α) |
Member
There was a problem hiding this comment.
Again I don't want to sign off on this part of the PR because I don't understand it.
| let _oα ← synthInstanceQ q(LinearOrderedField $α) | ||
| let _oα ← synthInstanceQ q(Field $α) | ||
| let _oα ← synthInstanceQ q(LinearOrder $α) | ||
| let _oα ← synthInstanceQ q(IsStrictOrderedRing $α) |
Member
There was a problem hiding this comment.
(again is it fine that all these instances have the same name? I don't know enough about metaprogramming to know if this is an issue)
| let _oα ← synthInstanceQ q(LinearOrderedField $α) | ||
| let _oα ← synthInstanceQ q(Field $α) | ||
| let _oα ← synthInstanceQ q(LinearOrder $α) | ||
| let _oα ← synthInstanceQ q(IsStrictOrderedRing $α) |
Member
There was a problem hiding this comment.
(again is it fine that all these instances have the same name? I don't know enough about metaprogramming to know if this is an issue)
Contributor
There was a problem hiding this comment.
Note to self let __ ← synthInstanceQ works.
mattrobball
approved these changes
Apr 4, 2025
| ⟨by simp [hbc.trans (le_mabs_self c)], by | ||
| simp [(inv_le_inv_iff.mpr hab).trans (inv_le_mabs a)]⟩ | ||
|
|
||
| omit [IsOrderedMonoid G] in |
Contributor
There was a problem hiding this comment.
These indicate that they are in the wrong module. Something to address on clean up.
Member
There was a problem hiding this comment.
At least one could add a TODO maybe?
Contributor
There was a problem hiding this comment.
I think that grepping for omit is enough since any omit has the same signal.
| section OrderedCommMonoid | ||
|
|
||
| variable {hα : OrderedCommMonoid α} {hβ : OrderedCommMonoid β} | ||
| variable {_ : Preorder α} {_ : Preorder β} {_ : MulOneClass α} {_ : MulOneClass β} |
Contributor
There was a problem hiding this comment.
Not for this PR, but there should be a systematic review of this pattern at some point.
sgouezel
reviewed
Apr 4, 2025
kbuzzard
approved these changes
Apr 4, 2025
Contributor
|
Thanks! \n bors merge |
Contributor
|
bors merge |
ghost
added
the
Contributor
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
tannerduve
pushed a commit
that referenced
this pull request
May 13, 2025
This was referenced Jun 3, 2025
Closed
joelriou
pushed a commit
that referenced
this pull request
Jun 8, 2025
TOMILO87
pushed a commit
that referenced
this pull request
Jun 8, 2025
callesonne
pushed a commit
to callesonne/mathlib4
that referenced
this pull request
Jul 24, 2025
…-community#25412) This restores a change from leanprover-community#22284 that was accidentally reverted in leanprover-community#20594. Also avoid using IsAddUnit when the unit can be constructed directly, which gives better defeqs.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
8 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
diff