Zulip Chat Archive

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.

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 (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.

Anne Baanen (Apr 04 2022 at 16:06):

#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