[Merged by Bors] - chore: use grw, gcongr even more#30632
[Merged by Bors] - chore: use grw, gcongr even more#30632YaelDillies wants to merge 8 commits intoleanprover-community:masterfrom
grw, gcongr even more#30632Conversation
PR summary be9d1e4270Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diff
You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
|
This is controversial because the style guide contains the "hypotheses left of colon" rule, but I claim this rule was written without pattern-matching in mind and should therefore be updated to include an exception. Also delete a redundant instance.
def7b3f to
a726558
Compare
|
I do somewhat agree with @grunweg that your refactor of inductive proofs is controversial. I think it is more readable if all proofs have the hypotheses on the left of the And an advantage of the |
|
So at least we agree that the style guide should be updated to include pattern-matching as a valid reason for having hypotheses right of the colon, and it's just that in those specific cases you believe we should rather use |
|
Sure, you could make an update to the style guide, but that is orthogonal to this PR |
|
I've switched to using |
JovanGerb
left a comment
There was a problem hiding this comment.
Thanks! I agree with these changes now :)
| _ = abv n + 1 := congrArg (abv n + ·) abv.map_one | ||
| _ ≤ n + 1 := add_le_add_right hn 1 | ||
| | succ n ih => | ||
| · grw [Nat.cast_succ, Nat.cast_succ, abv.add_le, abv.map_one, ih] |
There was a problem hiding this comment.
I think you accidentally left a focus dot
| grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ), | ||
| Nat.findGreatest_le] | ||
| rfl |
There was a problem hiding this comment.
| grw [← Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ), | |
| Nat.findGreatest_le] | |
| rfl | |
| grw [Nat.findGreatest_le, | |
| Nat.sub_add_cancel <| Order.one_le_iff_pos.mpr (Finset.card_pos.mpr hJ)] |
|
Thanks! maintainer delegate |
|
🚀 Pull request has been placed on the maintainer queue by JovanGerb. |
|
!bench |
grunweg
left a comment
There was a problem hiding this comment.
Thanks for following up and your patience through the process. Assuming the benchmark is fine, can you update the PR description (this doesn't contain any "hypothesis left of colon"-related changes any more), please?
bors d+
|
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
|
Here are the benchmark results for commit 3c560da. |
3 files, Instructions -2.0⬝10⁹
|
grw, gcongr more, controversial versiongrw, gcongr even more
|
bors merge |
Also delete a redundant instance.
|
Pull request successfully merged into master. Build succeeded: |
grw, gcongr even moregrw, gcongr even more
|
@YaelDillies, I think you forgot to address my comments above |
|
I addressed it, pushed then called bors, but my github token had expired so the push failed... and the PR got merged before I noticed. I have already moved the lost commit to the next PR in the sequence |
Also delete a redundant instance.
Also delete a redundant instance.
Also delete a redundant instance.