[Merged by Bors] - chore: use grw, gcongr more#30508
[Merged by Bors] - chore: use grw, gcongr more#30508YaelDillies wants to merge 1 commit intoleanprover-community:masterfrom
grw, gcongr more#30508Conversation
PR summary 2528a23415Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
5890999 to
cd8c2c8
Compare
grunweg
left a comment
There was a problem hiding this comment.
Thank you for doing this huge change! I reviewed the first 101 files so far (will continue later, also when you have fixed the build more). I like most of these changes, think we should benchmark this just in case, and have a few comments when I'm not as sure or need to be convinced this is good.
|
This pull request has conflicts, please merge |
cd8c2c8 to
1d846f4
Compare
grunweg
left a comment
There was a problem hiding this comment.
Reviewed the rest (except for 5 files); I'll do one last pass when you have fixed the build and my comments so far. Thanks a lot for doing this!
f05f9a7 to
fbd43e4
Compare
|
Assuming CI is happy, I have no further review comments than the ones above. Let's benchmark this and then merge soon! |
|
I believe I have replied to all your comments, or rather exhibited a section of answers from the equivalence class of comments. Let's bench too: !bench |
|
!bench |
|
IIRC, the bot only picks up comments which contain this exact string, and nothing else. |
|
@JovanGerb Do you mind briefly checking the new |
|
Here are the benchmark results for commit dd3f9dd. |
4 files, Instructions +1.0⬝10⁹
|
JovanGerb
left a comment
There was a problem hiding this comment.
Thanks for making this PR. Most gcongr tags look good, I only suggest a change for the opow one.
| | n + 1 => by rw [sqrtTwoAddSeries, sqrtTwoAddSeries_succ _ _, sqrtTwoAddSeries] | ||
|
|
||
| @[gcongr] | ||
| theorem sqrtTwoAddSeries_monotone_left {x y : ℝ} (h : x ≤ y) : |
There was a problem hiding this comment.
The lemma name should say mono instead of monotone, but I guess that's not for this PR.
There was a problem hiding this comment.
Let's make that a follow-up PR!
There was a problem hiding this comment.
Feel free to open a PR, Jovan :)
| alias isLimit_opow_left := isSuccLimit_opow_left | ||
|
|
||
| @[gcongr] | ||
| theorem opow_le_opow_right {a b c : Ordinal} (h₁ : 0 < a) (h₂ : b ≤ c) : a ^ b ≤ a ^ c := by |
There was a problem hiding this comment.
I suggest tagging opow_le_opow instead of the right version, as it is more general.
There was a problem hiding this comment.
As Heather explained, gcongr needs both (use case being monotonicity of multiplication). I'll tag opow_le_opow too
There was a problem hiding this comment.
I claim that if you tag opow_le_opow, then you can safely drop the tag from the right version
There was a problem hiding this comment.
If Heather explained otherwise, then that explanation is now out of date.
There was a problem hiding this comment.
Sorry, I wasn't aware you had made the change to gcongr. That would have been good to mention the first time around!
|
Thanks for the quick review, Jovan! With the benchmark results being in, I'm happy this PR with all "somewhat controversial parts removed". If you
I'll merge the rest directly. Optionally, waiting on a zulip consensus on the style guide thread is another option. |
69c81af to
e56245d
Compare
|
See #30632 |
|
Thank you for the prompt response and agreeing to split this PR. This subset of changes looks uncontroversial, so I'm happy to merge it directly (once CI has finished). |
|
bors merge |
|
|
|
Sorry for that. Would you like to make a follow-up PR; if it builds, I'll happily merge it! |
Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by #30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.
|
Build failed (retrying...): |
Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by #30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.
|
Pull request successfully merged into master. Build succeeded: |
grw, gcongr moregrw, gcongr more
This tag was accidentally added in #30508, but it is redundant
Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by leanprover-community#30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.
…nity#30651) This tag was accidentally added in leanprover-community#30508, but it is redundant
Golf many proofs using `grw`, `gcongr`, `cutsat`, `linarith`... For this, tag a few more lemmas with `gcongr`, and make some existing ones stronger. The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern. The precise golfs that are performed are motivated by leanprover-community#30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.
…nity#30651) This tag was accidentally added in leanprover-community#30508, but it is redundant
Golf many proofs using
grw,gcongr,cutsat,linarith... For this, tag a few more lemmas withgcongr, and make some existing ones stronger.The goal here is not necessarily to golf (although it usually is the case), but instead to reduce the number of explicit mentions of lemmas, as these are a maintainability concern.
The precise golfs that are performed are motivated by #30242, where four pairs of very basic and widespread lemmas get swapped. The best way to reduce the number of swaps needed is to simply not mention the lemmas explicitly.
Annoyingly,
grwis basically unusable with strict inequalities (it often leaves an unprovable goal since it doesn't know aboutlt_of_le_of_ltnorlt_of_lt_of_le, but onlylt_trans). This means that I must fall back togcongr; exact strict_ineqmany times where I would instead have liked to dogrw [strict_ineq].