Why is my code so slow?

Stream: general

[Chiyu Zhou]

I'm trying to define regular representation and proving properties. However, my code is super slow and make it hard to debug:
Here's a mwe:

import representation_theory.basic
import representation_theory.Rep
import representation_theory.Action
import representation_theory.fdRep
import field_theory.is_alg_closed.basic
import representation_theory.invariants
noncomputable theory

universes u

open_locale classical big_operators polynomial
open representation
open fdRep


variables {k : Type u} [field k] [is_alg_closed k]
variables {G : Type u} [group G]

variables [fintype G] [invertible (fintype.card G : k)]

@[class] instance (k G : Type u) [fintype G] [field k] [group G] : module.finite k (monoid_algebra k G) := sorry,

def regular_fdrep (k G : Type u) [field k] [group G] : representation k G (monoid_algebra k G):=
{ to_fun := λg : G, linear_map.mul_left k (finsupp.single g 1),
  map_one' := by sorry{tidy},
  map_mul' := by sorry{intros x y, ext, simp, rw group.mul_assoc, refl,}
}

def regular_basis (k G : Type u) [field k] [group G]: (basis G k (monoid_algebra k G)) := finsupp.basis_single_one

@[simp] lemma regular_fdrep_act : ∀g h : G, ((regular_fdrep k G) g) (finsupp.single h 1) = (finsupp.single (g * h) 1) :=
begin
  intros g h, rw regular_fdrep, simp only [linear_map.mul_left_apply,mul_one,eq_self_iff_true,monoid_hom.coe_mk,monoid_algebra.single_mul_single],
end

def regular_phi_linmap  (W : fdRep k G)  (v : W)  : (monoid_algebra k G) →ₗ[k] W :=
((regular_basis k G).constr k (λx, (W.ρ x) v))

@[simp] lemma regular_fdrep_of_hom_eq :
(fdRep.of (regular_fdrep k G)).ρ = regular_fdrep k G :=
begin
  refl, -- why is this refl taking so long time?
end

lemma fdRep_assoc_apply (W : fdRep k G) (g h : G) (v : W): (W.ρ g) ((W.ρ h) v) = (W.ρ (g * h)) v :=
begin
  simp
end

def regular_phi (W : fdRep k G)  (v : W) (b : basis G k (monoid_algebra k G)) : fdRep.of (regular_fdrep k G) ⟶ W :=
{ hom := regular_phi_linmap W v,
  comm' :=
  begin
  intro s,
  simp only [fdRep.of_ρ],
  simp_rw category_theory.category_struct.comp,
  ext,
  -- `simp` here will run timeout
  simp_rw linear_map.comp_apply,
  simp only [finsupp.lsingle_apply],
  rw regular_phi_linmap, simp_rw basis.constr_apply,
  simp only [linear_map.map_finsupp_sum],
  rw regular_fdrep_act,
  rw finsupp.sum_fintype, rw finsupp.sum_fintype, -- `simp_rw` or `simp only [finsupp.sum_fintype]` doesn't work here
  simp_rw map_smul,
  -- `simp_rw fdRep_assoc_apply` here doesn't work, but after changing goal with `suffices` it works
  suffices : ∑ (i : G), (((regular_basis k G).repr) (finsupp.single (s * a) 1)) i • ((W.ρ) i) v =
    ∑ (x : G), (((regular_basis k G).repr) (finsupp.single a 1)) x • ((W.ρ) s) (((W.ρ) x) v),
  { exact this },
  simp_rw fdRep_assoc_apply,
  end,
}

On line 42, the refl is taking 10+ seconds to compute. Also in the proof of regular_phi.comm' , simp often run timeout, and simp_rw often fail to work (or does nothing). I think my approach of doing some categorical stuff might be wrong (or inefficient), is it the issue?

[Kevin Buzzard]

Even changing refl to sorry it takes a long time! I feel like people have seen this kind of thing before, but I don't know why it's so slow.

[Floris van Doorn]

Lean has trouble elaborating the type of the lemma.
The computed type of the LHS is G →* ↥(of (regular_fdrep k G)) →ₗ[k] ↥(of (regular_fdrep k G)), and for some reason Lean has a hard time understanding that regular_fdrep k G has this type.
If you replace the statement with (fdRep.of (regular_fdrep k G)).ρ = by apply regular_fdrep k G, then it will be instant.

[Floris van Doorn]

For the simp issue, it's unfortunately the case that in Lean 3, simp is very slow if you import a lot of files.
One thing you can do is to run simp? or squeeze_simp (more expensive, but more reliable) with extra memory and a higher timeout, and then continue with the resulting simp only.
You can set the timeout in VSCode by going to Settings with ctrl+, and searching for Lean: Time Limit (I have 500000).
Then, in your position, squeeze_simp still times out, but simp? gives
simp only [function.comp_app, linear_map.coe_comp, regular_fdrep_act, finsupp.lsingle_apply],
It's not ideal. I hope (and think) this will be better in Lean 4.

[Floris van Doorn]

(unrelated: remove the @[class])

[Chiyu Zhou]

Floris van Doorn said:

For the simp issue, it's unfortunately the case that in Lean 3, simp is very slow if you import a lot of files.
One thing you can do is to run simp? or squeeze_simp (more expensive, but more reliable) with extra memory and a higher timeout, and then continue with the resulting simp only.
You can set the timeout in VSCode by going to Settings with ctrl+, and searching for Lean: Time Limit (I have 500000).
Then, in your position, squeeze_simp still times out, but simp? gives
simp only [function.comp_app, linear_map.coe_comp, regular_fdrep_act, finsupp.lsingle_apply],
It's not ideal. I hope (and think) this will be better in Lean 4.

Thank you! I removed some of unnecessary imports and the simp issue went better.