## Stream: general

### Topic: Slow defeqs in algebra/monoid_algebra/grading.lean

#### Anne Baanen (Apr 04 2022 at 14:57):

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.

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

#### Eric Wieser (Apr 04 2022 at 15:03):

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 (Apr 04 2022 at 15:04):

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

#### Anne Baanen (Apr 04 2022 at 15:19):

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 (Apr 04 2022 at 15:27):

Does making grade_by or grade semireducible make any difference?

#### Eric Wieser (Apr 04 2022 at 15:27):

(Rather than making anything irreducible)

#### Eric Wieser (Apr 04 2022 at 15:30):

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 (Apr 04 2022 at 15:38):

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 (Apr 04 2022 at 15:43):

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 (Apr 04 2022 at 15:53):

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 (Apr 04 2022 at 15:55):

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

#### Eric Wieser (Apr 04 2022 at 15:57):

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

#### Anne Baanen (Apr 04 2022 at 16:01):

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

#13169

#### Eric Wieser (Apr 12 2022 at 13:37):

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

Last updated: Dec 20 2023 at 11:08 UTC