# Zulip Chat Archive

## Stream: general

### Topic: Extremely slow simp

#### Gabriel Ebner (Feb 27 2020 at 23:02):

The following example takes more than one minute on my machine:

import all set_option trace.simplify true set_option profiler true open_locale nnreal example (a : ℝ) (ha) : ((⟨a, ha⟩ : ℝ≥0) : ℝ) = a := by simp

The simplifier rewrites once. However it seems to spend a huge time trying to match `add_con.coe_add`

(20s), `con.coe_mul`

(19s), `filter.filter_product.of_one`

(9s), `filter.filter_product.of_neg`

(4s), and `filter.filter_product.of_zero`

(15s). Does anybody have any idea what's going on here?

#### Rob Lewis (Feb 27 2020 at 23:04):

What are the imports?

#### Gabriel Ebner (Feb 27 2020 at 23:05):

`import all`

#### Kevin Buzzard (Feb 27 2020 at 23:14):

You should have used `squeeze_simp`

, then you would only have to do it once

#### Rob Lewis (Feb 27 2020 at 23:42):

Past my bedtime now, but the (or a) culprit seems to be an instance search for `example : has_mul {r : ℝ // 0 ≤ r} := by apply_instance`

. `nnreal`

gets unfolded somewhere it shouldn't.

#### Rob Lewis (Feb 27 2020 at 23:48):

Ah, `(⟨a, ha⟩ : ℝ≥0)`

doesn't actually have type `nnreal`

, it has type `{r : real // 0 <= r}`

. Nothing's getting unfolded, it isn't even folded to start with.

#### Antoine Labelle (May 28 2022 at 17:41):

The following proof takes around 2 min 30 to compile. Any idea why it is so slow and how to speed it up? (it requires adding `@[simps]`

to docs#category_theory.monoidal_category.full_monoidal_subcategory to work).

```
import representation_theory.basic
import representation_theory.fdRep
universes u
open representation
variables {k G V W : Type u} [field k] [group G]
variables [add_comm_group V] [module k V] [add_comm_group W] [module k W]
variables [finite_dimensional k V] [finite_dimensional k W]
variables (ρV : representation k G V) (ρW : representation k G W)
local attribute tensor_product.ext
@[simps] def linear_equiv.to_FinVect_iso
(e : V ≃ₗ[k] W) :
FinVect.of k V ≅ FinVect.of k W :=
{ hom := e.to_linear_map,
inv := e.symm.to_linear_map,
hom_inv_id' := by {ext, exact e.left_inv x},
inv_hom_id' := by {ext, exact e.right_inv x} }
noncomputable
def dual_tensor_iso_lin_hom : (fdRep.of ρV.dual) ⊗ (fdRep.of ρW) ≅ fdRep.of (lin_hom ρV ρW) :=
begin
refine Action.mk_iso (dual_tensor_hom_equiv k V W).to_FinVect_iso _,
intro g, ext f w v, simp [module.dual.transpose_apply],
end
```

#### Kevin Buzzard (May 28 2022 at 17:54):

I get an unknown `lin_hom`

. Is this `representation.lin_hom`

?

#### Kevin Buzzard (May 28 2022 at 17:55):

Then I get a type mismatch. I'm on today's `master`

.

#### Antoine Labelle (May 28 2022 at 17:55):

Where do you get a type mismatch?

#### Kevin Buzzard (May 28 2022 at 17:56):

Why not add the `simps`

attribute in the mwe?

#### Kevin Buzzard (May 28 2022 at 17:56):

If you're on today's master and you cut and paste, you'll be able to see exactly what I'm seeing :-)

#### Kevin Buzzard (May 28 2022 at 17:58):

Am I supposed to be adding `attribute [simps] category_theory.monoidal_category.full_monoidal_subcategory`

to this mwe? I get it on `Action.mk_iso`

, a type mismatch.

#### Antoine Labelle (May 28 2022 at 18:01):

Kevin Buzzard said:

Why not add the

`simps`

attribute in the mwe?

Oh I forgot that you can add the simps attribute locally and not just before the definition. So yes I think the mwe requires `attribute [simps] category_theory.monoidal_category.full_monoidal_subcategory`

.

#### Antoine Labelle (May 28 2022 at 18:05):

Let me try to figure out why there's a type mismatch.

#### Antoine Labelle (May 29 2022 at 18:03):

Ok, I haven't been able to figure out why the MWE didn't work (if someone understands why let me know!) but I PR'd the branch in which the proof works : #14453

#### Antoine Labelle (May 29 2022 at 18:04):

(The proof in question is at the end of `representation_theory/basic`

).

#### Antoine Labelle (May 29 2022 at 19:29):

Hmm, so the proof is so slow that CI gives a deterministic timeout even though it works locally for me. I tried `squeeze_simp`

but my computer start lagging before `squeeze_simp`

succeed... Does `squeeze_simp`

work for anyone else?

#### Alex J. Best (May 29 2022 at 19:33):

`squeeze_simp`

can be quite slow as it basically just tries simp over and over again to do the squeezing, you might be able to adjust the timeout locally (see https://leanprover-community.github.io/tips_and_tricks.html#memory-and-deterministic-timeout) then wait a few minutes for squeeze simp and get a version that works on CI

#### Ruben Van de Velde (May 29 2022 at 19:40):

Or try `simp?`

rather than `squeeze_simp`

- it's a little less reliable, but tends to be faster

#### Antoine Labelle (May 29 2022 at 20:02):

`simp?`

worked but even after changing to `simp_only`

it takes almost 2 minutes to compile and CI fails with deterministic timeout.

#### Stuart Presnell (May 29 2022 at 22:22):

What did `simp?`

suggest? Is there anything you can pull out of the `simp_only`

to use directly in, for example, a `rw`

or `refine`

?

#### Kyle Miller (May 29 2022 at 22:29):

Even this is very slow (with or without `noncomputable!`

):

```
def dual_tensor_iso_lin_hom : (fdRep.of ρV.dual) ⊗ (fdRep.of ρW) ≅ fdRep.of (lin_hom ρV ρW) :=
begin
sorry,
end
```

#### Kyle Miller (May 29 2022 at 22:29):

It takes a bit more than 11 seconds for me.

#### Antoine Labelle (May 29 2022 at 22:35):

Kyle Miller said:

Even this is very slow (with or without

`noncomputable!`

):`def dual_tensor_iso_lin_hom : (fdRep.of ρV.dual) ⊗ (fdRep.of ρW) ≅ fdRep.of (lin_hom ρV ρW) := begin sorry, end`

Indeed that's pretty weird. I wonder what takes so much time.

#### Antoine Labelle (May 30 2022 at 00:22):

And changing the `simp only`

to a bunch of rewrites won't be enough for CI, since just the following gives a deterministic timeout with a time limit of 100 000.

```
def dual_tensor_iso_lin_hom : (fdRep.of ρV.dual) ⊗ (fdRep.of ρW) ≅ fdRep.of (lin_hom ρV ρW) :=
begin
refine Action.mk_iso (dual_tensor_hom_equiv k V W).to_FinVect_iso _,
intro g, ext f w v,
sorry,
end
```

#### Stuart Presnell (May 30 2022 at 09:52):

On my (admittedly rather old) computer this:

```
import representation_theory.basic
import representation_theory.fdRep
universes u
open representation
variables {k G V W : Type u} [field k] [group G]
variables [add_comm_group V] [module k V] [add_comm_group W] [module k W]
variables [finite_dimensional k V] [finite_dimensional k W]
variables (ρV : representation k G V) (ρW : representation k G W)
lemma test1 : fdRep.of ρV.dual = fdRep.of ρV.dual := rfl
```

takes 33 seconds, but then the profiler can't account for that time:

```
parsing took 0.341ms
type checking of test1 took 26.1ms
decl post-processing of test1 took 0.0402ms
elaboration of test1 took 0.587ms
```

#### Stuart Presnell (May 30 2022 at 10:07):

For comparison, this takes 20 seconds:

```
lemma test2 : fdRep.of ρV.dual = fdRep.of ρV := sorry
```

while this is immediate:

```
lemma test3 : ρV.dual = ρV.dual := rfl
```

and this takes 7 seconds:

```
lemma test4 : fdRep.of ρV = fdRep.of ρV := rfl
```

#### Stuart Presnell (May 30 2022 at 10:16):

and just this takes 15 seconds:

```
#check fdRep.of ρV.dual
```

#### Yaël Dillies (May 30 2022 at 10:17):

Something to do with docs#fdRep.of, then?

#### Kevin Buzzard (May 30 2022 at 10:19):

What happens if you put `noncomputable!`

in front of the lemmas?

#### Stuart Presnell (May 30 2022 at 10:19):

`#check fdRep.of ρV`

takes 3 seconds

#### Stuart Presnell (May 30 2022 at 10:24):

Adding `noncomputable!`

hasn't changed the timings

#### Stuart Presnell (May 30 2022 at 10:28):

These are all wall-clock timings, by the way. If I add `set_option profiler true`

then the output of the profiler only adds up to a few milliseconds.

#### Ben Toner (May 30 2022 at 10:39):

You can probably assume that the time missing from the profiler is spent on type checking: see https://github.com/leanprover-community/lean/issues/58

#### Antoine Labelle (Jun 01 2022 at 17:26):

Stuart Presnell said:

On my (admittedly rather old) computer this:

`import representation_theory.basic import representation_theory.fdRep universes u open representation variables {k G V W : Type u} [field k] [group G] variables [add_comm_group V] [module k V] [add_comm_group W] [module k W] variables [finite_dimensional k V] [finite_dimensional k W] variables (ρV : representation k G V) (ρW : representation k G W) lemma test1 : fdRep.of ρV.dual = fdRep.of ρV.dual := rfl`

takes 33 seconds, but then the profiler can't account for that time:

`parsing took 0.341ms type checking of test1 took 26.1ms decl post-processing of test1 took 0.0402ms elaboration of test1 took 0.587ms`

Note that we get equally slow results with docs#Rep.of instead of `fdRep.of`

, so it's not a problem with the finite dimensionality instance. So the thing that takes a lot of time must be the conversion of `ρ : G →* (V →ₗ[k] V)`

to `ρ : G ⟶ Mon.of (category_theory.End (Module.of V))`

in the definition of `Rep.of`

, especially when `ρ`

is defined as `representation.dual`

. Is there a modification of the definition of `Rep.of`

that would make this faster?

#### Stuart Presnell (Jun 01 2022 at 17:55):

Antoine Labelle said:

Note that we get equally slow results with docs#Rep.of instead of

`fdRep.of`

As another data point, this takes 13 seconds:

```
#check Rep.of ρV.dual
```

#### Antoine Labelle (Jun 05 2022 at 15:33):

It took some time, but I think I finally found the culprit here: it seems to be the coercion from `representation k G`

to `G →* (V →ₗ[k] V)`

. Indeed, the following is immediate

```
def representation.to_monoid_hom : G →* (V →ₗ[k] V) := ρV
#check Rep.of ρV.dual.to_monoid_hom
```

whereas without `to_monoid_hom`

it takes 13 seconds as mentioned by Stuart.

#### Antoine Labelle (Jun 05 2022 at 15:38):

This makes me wonder if the definition of `representation`

is ok. It is currently defined as

```
abbreviation representation := G →* (V →ₗ[k] V)
```

I don't know much about how `abbreviation`

works, is it the same as `def`

or does it have a different behavior?

#### Antoine Labelle (Jun 05 2022 at 15:45):

If we keep `representation`

as it is, we have two options. Either we change the argument of `Rep.of`

to be of type `representation k G`

instead of `G →* (V →ₗ[k] V)`

, or we don't touch `Rep.of`

but we put `to_monoid_hom`

everytime we want use `Rep.of`

on something of type `representation k G`

. @Scott Morrison maybe you have an opinion on that since you're the author of `Rep`

?

#### Antoine Labelle (Jun 05 2022 at 15:47):

(One issue with the first option is that it requires `representation_theory.Rep`

to import `representation_theory.basic`

whereas in #14453 I have the opposite import.)

#### Kyle Miller (Jun 05 2022 at 15:52):

`abbreviation`

is pretty much `@[reducible, inline] def`

(though unlike `def`

it doesn't generate equation lemmas, which impacts how you unfold it.)

#### Kyle Miller (Jun 05 2022 at 15:54):

The presence of `V`

twice in that abbreviation is worrisome to me. There's a chance it's causing exponential behavior since `reducible`

means Lean is happy to unfold it when doing typeclass inference.

#### Kyle Miller (Jun 05 2022 at 15:56):

`inline`

only has an effect on VM compilation and the noncomputability checker, but still it doesn't strike me as being a good idea to inline code that refers to variables more than once.

#### Antoine Labelle (Jun 07 2022 at 23:01):

@Kyle Miller Do you think that `representation`

should be a `def`

and not an `abbreviation`

in this case?

Also the problem is really due to presence of `V`

twice, wouldn't docs#module.End have the same problems? Has anyone noticed any issue with `module.End`

?

#### Yaël Dillies (Jun 08 2022 at 06:20):

Surely `V`

appearing twice is not quite the criterion, else we would have had troubles ages ago with docs#equiv.perm.

#### Eric Wieser (Jun 08 2022 at 12:11):

I've had problems with module.End and `@[simps]`

before

Last updated: Aug 03 2023 at 10:10 UTC