[Merged by Bors] - chore: remove "instance was not necessary" porting notes (issue #10670) #17866
Conversation
This file contains 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
These instances are now necessary because instance synthesis now searches with the discrimination tree, so fewer matches are found. This is not likely to be reverted in the future, so the instances remain required. We need a big refactor cleaning up the concrete category bits of the library anyway.
Vierkantor
added
t-category-theory
PR summary 5a80f0e59eImport changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 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 |
Vierkantor
added a commit
that referenced
this pull request
Oct 17, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866.
leanprover-community-mathlib4-bot
added
the
ready-to-merge
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 17, 2024
… (#17866) Discussed with @kim-em. These instances are now necessary because instance synthesis now searches with the full discrimination tree, so mismatches in the arguments to instances are scrutinized much harder. This is not likely to be reverted in the future, so the instances remain required. There were a few further occurrences of #10670 for Grp, see e.g. [Grp.instCoeFunHomForallαGroup](https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/Grp/Basic.html#Grp.instCoeFunHomForall%CE%B1Group). These do look like they are unnecessary but removing them breaks a lot of downstream proofs. (I think it's something to do with `coe_of` unfolding `of` causing a mismatch between the expected types, but it's a bit too subtle to deal with easily.) I'll leave those porting notes for the meantime. We need a big refactor cleaning up the concrete category bits of the library anyway.
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
bot
changed the title
Vierkantor
added a commit
that referenced
this pull request
Oct 18, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the first half of the changes, to see if those work without slowdowns.
Vierkantor
added a commit
that referenced
this pull request
Oct 18, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the first half of the changes, to see if those work without slowdowns.
This was referenced Oct 18, 2024
Vierkantor
added a commit
that referenced
this pull request
Oct 18, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the first half of the changes, to see if those work without slowdowns.
1 task
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 18, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the second half of #17870, and doesn't affect the benchmarks.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 19, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. I am currently bisecting to figure out exactly why the benchmarks are indicating a slowdown with no obvious cause.
Vierkantor
added a commit
that referenced
this pull request
Oct 21, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This is the first half of the changes, to see if those work without slowdowns.
Vierkantor
added a commit
that referenced
this pull request
Oct 21, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 21, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. This contains everything except the interval [1/4, 3/8] of the changes, and doesn't affect the benchmark.
Vierkantor
added a commit
that referenced
this pull request
Oct 21, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.
Vierkantor
added a commit
that referenced
this pull request
Oct 21, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. Compared to previous tests, this only preserves the `Finsupp` and `DFinsupp` instances; my guess is that they are the important shortcut instances preventing slowdowns.
mathlib-bors bot
pushed a commit
that referenced
this pull request
Oct 22, 2024
During the port we found that `FunLike` is robust enough not to need an extra `CoeFun` shortcut. Let's see if that rule can be consistently applied to the whole of the library. There is still duplication between `FunLike` and `CoeFun` for `Grp`, `Mon`, `CommGrp` and `CommMon`, which will need a more thorough fix. See also #17866. There is also a shortcut instance that we need for speed reasons: `SemilinearIsometry.instCoeFun`. I don't know why this is so performance-sensitive but the benchmarks tell us that it is. See also #17871 for removing porting notes and comments where this change happened earlier on.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Discussed with @kim-em.
These instances are now necessary because instance synthesis now searches with the full discrimination tree, so mismatches in the arguments to instances are scrutinized much harder. This is not likely to be reverted in the future, so the instances remain required.
There were a few further occurrences of #10670 for Grp, see e.g. Grp.instCoeFunHomForallαGroup. These do look like they are unnecessary but removing them breaks a lot of downstream proofs. (I think it's something to do with
coe_ofunfoldingofcausing a mismatch between the expected types, but it's a bit too subtle to deal with easily.) I'll leave those porting notes for the meantime.We need a big refactor cleaning up the concrete category bits of the library anyway.