Extremely slow simp

Stream: general

[Gabriel Ebner]

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]

What are the imports?

[Gabriel Ebner]

import all

[Kevin Buzzard]

You should have used squeeze_simp, then you would only have to do it once

[Rob Lewis]

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]

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]

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]

I get an unknown lin_hom. Is this representation.lin_hom?

[Kevin Buzzard]

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

[Antoine Labelle]

Where do you get a type mismatch?

[Kevin Buzzard]

Why not add the simps attribute in the mwe?

[Kevin Buzzard]

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]

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]

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]

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

[Antoine Labelle]

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]

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

[Antoine Labelle]

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]

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]

Or try simp? rather than squeeze_simp - it's a little less reliable, but tends to be faster

[Antoine Labelle]

simp? worked but even after changing to simp_only it takes almost 2 minutes to compile and CI fails with deterministic timeout.

[Stuart Presnell]

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]

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]

It takes a bit more than 11 seconds for me.

[Antoine Labelle]

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]

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]

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]

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]

and just this takes 15 seconds:

#check fdRep.of ρV.dual

[Yaël Dillies]

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

[Kevin Buzzard]

What happens if you put noncomputable! in front of the lemmas?

[Stuart Presnell]

#check fdRep.of ρV takes 3 seconds

[Stuart Presnell]

Adding noncomputable! hasn't changed the timings

[Stuart Presnell]

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]

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]

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]

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]

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]

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]

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]

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

abbreviation is pretty much @[reducible, inline] def (though unlike def it doesn't generate equation lemmas, which impacts how you unfold it.)

[Kyle Miller]

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]

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]

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

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

[Eric Wieser]

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