Timeout when applying a `simps` lemma

Stream: general

[Eric Wieser]

I'm getting very weird behavior in #11468, where rw some_rfl_lemma_generated_by_simps times out. Any suggestions for why this might be happening?

[Eric Wieser]

MWE:

import linear_algebra.exterior_algebra
import linear_algebra.tensor_product
import linear_algebra.prod
import linear_algebra.dual

universes u1 u2 u3

variables {R : Type u1} [comm_ring R]
variables {M : Type u2} [add_comm_group M] [module R M]

namespace exterior_algebra

variables (B : module.dual R M)

/-- The map `g v (x, y) = (ι R v * x, -ι R v * y + B v • x)` -/
@[simps apply_apply]
def g (B : module.dual R M) :
  M →ₗ[R] module.End R (exterior_algebra R M × exterior_algebra R M) :=
begin
  have v_mul := (algebra.lmul R (exterior_algebra R M)).to_linear_map.comp (ι R),
  have l := v_mul.compl₂ (linear_map.fst _ _ (exterior_algebra R M)),
  have r := -v_mul.compl₂ (linear_map.snd _ (exterior_algebra R M) _) +
            B.smul_right (linear_map.fst _ (exterior_algebra R M) (exterior_algebra R M)),
  exact
    { to_fun := λ v, (l v).prod (r v),
      map_add' := λ v₂ v₂, linear_map.ext $ λ x, prod.ext
        (linear_map.congr_fun (l.map_add _ _) x) (linear_map.congr_fun (r.map_add _ _) x),
      map_smul' := λ c v, linear_map.ext $ λ x, prod.ext
        (linear_map.congr_fun (l.map_smul _ _) x) (linear_map.congr_fun (r.map_smul _ _) x), },
end

lemma g_g (v : M) (x : exterior_algebra R M × exterior_algebra R M) : g B v (g B v x) = 0 :=
begin
  rw g_apply_apply, -- timeout!?
end

end exterior_algebra

[Eric Wieser]

Weirdly, if I write the lemma myself it's all fine:

lemma g_apply_apply' (v : M) (p : exterior_algebra R M × exterior_algebra R M) :
  g B v p = (ι R v * p.fst, -(ι R v * p.snd) + B v • p.fst) :=
rfl

[Kevin Buzzard]

Does force_noncomputable fix it? It's the first thing I try nowadays

[Kevin Buzzard]

Several students here have it in their projects

[Eric Wieser]

It looks like the problem is the difference between module.End and linear_map, the generated lemma talks about the former while the hand-written one talks about the latter

[Floris van Doorn]

That doesn't look like it is the problem. I get the same behavior if I unfold the definition of End.
The problem is that g_apply_apply and g_apply_apply' are not syntactically equal, and Lean doesn't find it very easy to make them definitionally equal when working with expressions that are not fully elaborated. The only difference I could see is that there are different paths taken through the algebraic hierarchy (in the instance arguments of the types of the lemmas).
In the following example, you can see some of the difficulties Lean has with unifying, but that (for example) the rewrite is better if you provide B:

import linear_algebra.exterior_algebra
import linear_algebra.tensor_product
import linear_algebra.prod
import linear_algebra.dual

universes u1 u2 u3

variables {R : Type u1} [comm_ring R]
variables {M : Type u2} [add_comm_group M] [module R M]

namespace exterior_algebra

variables (B : module.dual R M)

/-- The map `g v (x, y) = (ι R v * x, -ι R v * y + B v • x)` -/
@[simps? apply_apply]
def g (B : module.dual R M) :
  M →ₗ[R] (exterior_algebra R M × exterior_algebra R M) →ₗ[R] (exterior_algebra R M × exterior_algebra R M) :=
  let v_mul := (algebra.lmul R (exterior_algebra R M)).to_linear_map.comp (ι R) in
  let l := v_mul.compl₂ (linear_map.fst _ _ (exterior_algebra R M)) in
  let r := -v_mul.compl₂ (linear_map.snd _ (exterior_algebra R M) _) +
            B.smul_right (linear_map.fst _ (exterior_algebra R M) (exterior_algebra R M)) in
  -- exact
    { to_fun := λ v, (l v).prod (r v),
      map_add' := λ v₂ v₂, linear_map.ext $ λ x, prod.ext
        (linear_map.congr_fun (l.map_add _ _) x) (linear_map.congr_fun (r.map_add _ _) x),
      map_smul' := λ c v, linear_map.ext $ λ x, prod.ext
        (linear_map.congr_fun (l.map_smul _ _) x) (linear_map.congr_fun (r.map_smul _ _) x), }

lemma g_apply_apply' (v : M) (x : exterior_algebra R M × exterior_algebra R M) :
  g B v x = (ι R v * x.fst, -(ι R v * x.snd) + B v • x.fst) :=
by apply g_apply_apply B v x -- fine
-- by convert g_apply_apply B v x -- fine
-- g_apply_apply B v x -- not fine


lemma g_g (v : M) (x : exterior_algebra R M × exterior_algebra R M) : g B v (g B v x) = 0 :=
begin
  rw g_apply_apply B -- works
end


set_option pp.implicit true
set_option pp.notation false
#print g_apply_apply
#print g_apply_apply'


end exterior_algebra

[Floris van Doorn]

This issue might be solved by making some strategic defs irreducible...

[Kevin Buzzard]

Nice diagnosis! Timeouts are sometimes really hard to pin down.