# 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