Commit 2022-08-16 10:36 b95b8c7a
View on Github →chore(*): restore subsingleton instances and remove hacks (#16046)
Background
The simp tactic used to look for subsingleton instances excessively, 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](https://github.com/leanprover-community/lean/pull/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](https://github.com/leanprover-community/mathlib/commit/c7626b7dfe2bf35b48cf43178a32d74f5dbf8b3f#diff-02976f8e19552b3c7ea070e30761e4e99f1333085cc5bb94fa170861c6ed27bcL497). I measured the difference in performance 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.