Convert subsingleton lemmas to instances #6025
Comments
This was referenced Feb 3, 2021
Closed
This was referenced Jun 27, 2021
bors bot
pushed a commit
that referenced
this issue
Jun 30, 2021
…duplicate instance (#8140) We already had a `subsingleton` instance on `alg_hom`s added in #5672, but we didn't find it #8110 because * gh-6025 means we can't ask `apply_instance` to find it * it had an incorrect name in the wrong namespace Code opting into this instance will need to change from ```lean local attribute [instance] alg_hom.subsingleton ``` to ```lean local attribute [instance] alg_hom.subsingleton subalgebra.subsingleton_of_subsingleton ```
b-mehta
pushed a commit
that referenced
this issue
Jul 6, 2021
…duplicate instance (#8140) We already had a `subsingleton` instance on `alg_hom`s added in #5672, but we didn't find it #8110 because * gh-6025 means we can't ask `apply_instance` to find it * it had an incorrect name in the wrong namespace Code opting into this instance will need to change from ```lean local attribute [instance] alg_hom.subsingleton ``` to ```lean local attribute [instance] alg_hom.subsingleton subalgebra.subsingleton_of_subsingleton ```
This was referenced Aug 11, 2022
alreadydone
added a commit
that referenced
this issue
Aug 13, 2022
bors bot
pushed a commit
that referenced
this issue
Aug 15, 2022
) + Add `unique` instances when the codomain types are subsingletons and rename the original `unique` instances (which apply when the domain is empty) to `unique_of_is_empty`. These are in analogy to [pi.unique](https://leanprover-community.github.io/mathlib_docs/logic/unique.html#pi.unique) and [pi.unique_of_is_empty](https://leanprover-community.github.io/mathlib_docs/logic/unique.html#pi.unique_of_is_empty). + Golf the `unique` instances for (d)finsupp using `fun_like.coe_injective.unique`. The names `unique_of_left` and `unique_of_right` remain unchanged in the finsupp case, because finsupp is special in that it consists of non-dependent functions, unlike dfinsupp or direct_sum. (There was a concern that adding `unique` instances would slow down `simp` (see #6025), but it has been fixed in [lean#665](leanprover-community/lean#665).)
bors bot
pushed a commit
that referenced
this issue
Aug 15, 2022
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
bors bot
pushed a commit
that referenced
this issue
Aug 15, 2022
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
bors bot
pushed a commit
that referenced
this issue
Aug 15, 2022
#### Background The `simp` tactic used to [look for subsingleton instances excessively](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/223034551), so every subsingleton/unique instances added to mathlib could slow down `simp` performance; in fact, removing some subsingleton instances locally led to such speedup that three hacks #5779, #5878 and #6639 along this line have been merged into mathlib. Since the problem was discovered, new subsingleton instances were mostly turned into lemma/defs, with a reference to gh-6025 that @eric-wieser created to track them and a notice to restore them as instances once safe to do so. This bad behavior of `simp` was finally fixed in [lean#665](leanprover-community/lean#665) by @gebner in January 2022, so it is now safe to remove the hacks and restore the instances. In fact, the hack #5878 was already removed in [#13127](c7626b7#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I [measured the difference in performance](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.235672.20breaks.20timeout/near/293228091) from removing one of the remaining hacks and it was negligible. Therefore, in this PR, we: + Remove both hacks remaining; + Turn all would-be instances that mention gh-6025 into actual global instances; + Golf proofs that explicitly invoked these instances previously; + Remove `local attribute [instance]` lines that were added when these instances were needed. Closes #6025.
2 tasks
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
This zulip discussion noticed that due to leanprover-community/lean#521,
simpis significantly slowed down by the presence of subsingleton instances.As a result of this, various PRs have received feedback to replace
instance : subsingleton Twithlemma T_subsingleton : subsingleton T. If this happens to your PR, please add the following comment next to the incriminated instance.This issue is to track swapping these back to
instanceonce the performance issues are resolved.The text was updated successfully, but these errors were encountered: