Slow rfl mv_polynomial

Stream: general

[Chris Hughes]

This rfl lemma is extremely slow, but commenting out import data.mv_polynomial.comm_ring or changing R to a comm_semiring really speeds it up. Is there a bad instance somewhere or something? I think mv_polynomial.comm_ring might be a bad instance.

lemma H {R A ι : Type*} [comm_ring R] [comm_ring A] [algebra R A]
  (f : mv_polynomial (option ι) R ≃ₐ[R] polynomial (mv_polynomial ι R))
  (p : mv_polynomial (option ι) R) :
  (option_equiv_left R ι) p = ((option_equiv_left R ι :
    mv_polynomial (option ι) R →ₐ[R] polynomial (mv_polynomial ι R))
    : mv_polynomial (option ι) R →+* polynomial (mv_polynomial ι R)) p :=
rfl

Changing the definition of mv_polynomial.comm_ring to

instance : comm_ring (mv_polynomial σ R) :=
{ ..mv_polynomial.comm_semiring,
  ..add_monoid_algebra.comm_ring }

from

instance : comm_ring (mv_polynomial σ R) := add_monoid_algebra.comm_ring

seems to fix it. Is this a change we should make, and is there anywhere else this sort of change could be made.

[Eric Wieser]

I guess your version speeds up unification of the ring and comm_ring by preventing the unfolding taking the wrong path

[Chris Hughes]

We should probably repeat the changes made by #7421 for mv_polynomial.

[Chris Hughes]

Or for the reals by #6024

[Chris Hughes]

@Sebastien Gouezel @Gabriel Ebner What do you think about making mv_polynomial a wrapper around finsupp with irreducible ring operations? Did it solve these sorts of problems for polynomial or real?

[Eric Wieser]

I think that ship is already sailing and that refactor is probably inevitable (eventually), it's just a lot of work

[Eric Wieser]

From a selfish point of view I'd probably like to get #8913 in before such a refactor happens

[Yury G. Kudryashov]

With this refactor you won't be able to apply lemmas about finsupp/add_monoid_algebra anymore.

[Scott Morrison]

Or rather, you'll have to "copy them across" to mv_polynomial before it gets marked irreducible.

[Yury G. Kudryashov]

AFAIR, "define, prove, make irreducible" is not available in Lean 4, so we try not to use it in mathlib. I may be wrong.

[Chris Hughes]

@Yury G. Kudryashov See this comment https://github.com/leanprover-community/mathlib/pull/6024#discussion_r569734573 You can effectively make it irreducible by wrapping it inside an inductive type. This is how the reals and polynomials are now implmented.