simps is very slow

Stream: general

[Eric Wieser]

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]

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]

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

[Eric Wieser]

I added manual versions of the lemmas in #7403

[Eric Wieser]

Thanks for investigating though

[Eric Wieser]

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]

@[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]

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]

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]

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]

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

[Eric Wieser]

(with a unicode arrow to match "initialize_simps_projections")

[Floris van Doorn]

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]

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

[Floris van Doorn]

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