Slow defeqs in `algebra/monoid_algebra/grading.lean`

Stream: general

[Anne Baanen]

The lemma docs#add_monoid_algebra.grade.is_internal takes 9 seconds to elaborate on my machine, and even times out on branch#linear_map_class, because it gets blocked on the unification problem id = coe_fn ?m_1, unfolds the entirety of direct_sum.submodule_is_internal, then only when that all fails it starts using the (add_monoid_hom.id ι) argument. So when I replace the proof with by simpa only [grade_by_id] using grade_by.is_internal (add_monoid_hom.id ι), it takes 3 orders of magnitude less time.

There are a few other declarations in this file that have some similarly slow defeq checks: docs#add_monoid_algebra.of_grades_by_of and docs#add_monoid_algebra.grade_by.is_internal.

@Eric Wieser, any ideas for a higher-concept way to deal with this slowness/timeout?

[Eric Wieser]

grade_by was something I wasn't super happy with when it was PR'd, but couldn't come up with a better alternative to either and didn't want to hold up the contributor

[Eric Wieser]

Perhaps it's unfolding so far because grade_by is an abbreviation?

[Anne Baanen]

It's not quite that the problem lies in unfolding grade_by: the problem lies in not unfolding grade to grade_by id. Making grade_by irreducible turns elaboration from 9s to 5s on my machine. If I instead make direct_sum.submodule_is_internal irreducible, it's 8ms.

[Eric Wieser]

Does making grade_by or grade semireducible make any difference?

[Eric Wieser]

(Rather than making anything irreducible)

[Eric Wieser]

Note that my original plan was to not have grade_by at all, and only have grade; then define some operation for reindexing a graded ring via a quotient

[Anne Baanen]

I can't really tell a difference when making either grade, grade_by or direct_sum.submodule_is_internal semireducible: all about 9 seconds +- 1s.

[Anne Baanen]

Another option would be to make direct_sum.submodule_coe irreducible. At least it doesn't need to be unfolded in that file. Nevermind, grade_by.is_internal relies on unfolding that definition.

[Eric Wieser]

I think the simpa solution is quite reasonable here. If unfolding goes in the wrong order, then asking the user to rewrite seems fine

[Eric Wieser]

The other answer here is that that whole file should be overhauled to use docs#graded_algebra anyway

[Eric Wieser]

I'll have a quick investigation of how easy that is

[Anne Baanen]

Alright, I'll make a PR for the simpa solution, so you can compare.

[Anne Baanen]

#13169

[Eric Wieser]

Eric Wieser said:

The other answer here is that that whole file should be overhauled to use docs#graded_algebra anyway

Done in #13360, I was delayed by illness