Zulip Chat Archive

Stream: general

Topic: simps is very slow

Eric Wieser (Apr 29 2021 at 08:26):

The @[simps mul] attribute on docs#direct_sum.ghas_mul.of_add_subgroups is making the definition very slow; profiler says:

elaboration of ghas_mul.of_add_subgroups took 184ms
type checking of ghas_mul.of_add_subgroups took 54.6ms
decl post-processing of ghas_mul.of_add_subgroups took 44.3s

Is there an easy way to see what's going on here?

Floris van Doorn (Apr 30 2021 at 18:59):

Investigating this now. Running the profiler on the command

run_cmd tactic.try_for 100000 (simps_tac ``ghas_mul.of_add_subgroups {rhs_md := semireducible} ["mul"] tt)

does not give what I expected. Apparently 99+% of the time is spent in the tactic docs#tactic.mk_mapp.
I expect this has something to do with the fact that the right hand side of the generated lemma is still a (relatively) complicated structure. This is intended, right?

Eric Wieser (Apr 30 2021 at 19:28):

No, I was hoping it would unfold the add_monoid_hom on the RHS

Eric Wieser (Apr 30 2021 at 19:29):

I added manual versions of the lemmas in #7403

Eric Wieser (Apr 30 2021 at 19:30):

Thanks for investigating though

Eric Wieser (Apr 30 2021 at 19:32):

I think it probably loses lots of time unifying the dependent typeclasses; indeed the submodule def was much faster than the subgroup one I drew attention to, presumably because it doesn't need to match indexed families of derived typeclasses

Floris van Doorn (Apr 30 2021 at 20:03):

@[simps mul] tells simps to generate the lemmas by only applying the projection mul, no nested projections (in other words, not applied to a and b).
If you just run @[simps] without arguments, it will generate a lemma applied to a and b, but it will also apply the coercion from subtypes. To get the lemmas you want (modulo name of the lemma), run @[simps mul_apply_apply]. You could consider doing that (if you don't mind that the name is uglier). These other lemmas are also generated very quickly.

Floris van Doorn (Apr 30 2021 at 20:05):

I am still investigating further. The issue is indeed related to the add_comm_monoid structure on (carriers i) and (carriers i).to_add_submonoid.
I can try to improve simps to not use mk_mapp there. I believe I have all the information there in the tactic, so I could just use expr.app manually.

Floris van Doorn (Apr 30 2021 at 20:06):

I minimized the original problem to

import group_theory.subgroup

set_option old_structure_cmd true
structure my_add_monoid_hom (M : Type*) (N : Type*) [add_comm_monoid M] [add_comm_monoid N] :=
(to_fun : M  N)

structure ghas_mul (A : Type*) [add_comm_monoid A] :=
(mul : my_add_monoid_hom A A)

section shorthands

variables {R : Type*}

@[simps mul]
def ghas_mul.of_add_submonoids [add_comm_group R] (carriers : add_submonoid R) : ghas_mul carriers :=
{ mul := { to_fun := λ x, x } }

-- @[simps? mul {rhs_md := semireducible}]
def ghas_mul.of_add_subgroups [add_comm_group R] (carriers : add_subgroup R) : ghas_mul carriers :=
ghas_mul.of_add_submonoids carriers.to_add_submonoid

Floris van Doorn (Apr 30 2021 at 20:55):

The slowdown of the original problem is fixed in #7432.
I didn't completely figure out the bottleneck, but it was easy to remove the offending mk_mapp.

Eric Wieser (Apr 30 2021 at 21:30):

Perhaps we should allow the syntax @[simps mul_apply_apply->mul] to address the ugly name problem?

Eric Wieser (Apr 30 2021 at 21:30):

(with a unicode arrow to match "initialize_simps_projections")

Floris van Doorn (Apr 30 2021 at 21:39):

You can actually already do this unformly:

def ghas_mul.simps.apply [has_add ι] [Π i, add_comm_monoid (A i)] [ghas_mul A] {i j : ι}
  (x : A i) (y : A j) : A (i + j) :=
ghas_mul.mul x y

initialize_simps_projections ghas_mul (mul_to_fun_to_fun  apply, -mul)

Except... that fails. These structures are definitely stress-testing @[simps] :)

Floris van Doorn (Apr 30 2021 at 21:39):

The syntax @[simps mul_apply_apply->mul] is probably also useful, and was already on the wishlist #5489

Floris van Doorn (Apr 30 2021 at 22:46):

After #7433 you should be able to write the following, and then @[simps] (or equivalently @[simps mul]) will generate the simp lemmas you want with the correct name.

def ghas_mul.simps.mul [has_add ι] [Π i, add_comm_monoid (A i)] [ghas_mul A] {i j : ι}
  (x : A i) (y : A j) : A (i + j) :=
ghas_mul.mul x y

initialize_simps_projections ghas_mul (mul  mul', mul_to_fun_to_fun  mul, -mul')
-- Explanation of the last line: the composite projection `mul_to_fun_to_fun` should be called `mul`. Furthermore, we don't generate simp-lemmas that just apply the single projection `mul`. We rename this single projection, because we want to call the composition of 3 projections `mul`.

Last updated: Aug 03 2023 at 10:10 UTC