polynomial elaboration

Stream: general

[Kenny Lau]

So why is polynomial elaboration slow and what can we do about it?

[Kenny Lau]

import data.equiv.algebra linear_algebra.multivariate_polynomial

universes u v w

variables {σ : Type u} {τ : Type v} {α : Type w} [comm_ring α]
variables [decidable_eq σ] [decidable_eq τ] [decidable_eq α]

namespace mv_polynomial

def equiv_of_equiv (e : σ ≃ τ) : mv_polynomial σ α ≃ mv_polynomial τ α :=
{ to_fun := eval₂ C (X ∘ e),
  inv_fun := eval₂ C (X ∘ e.symm),
  left_inv := λ f, induction_on f
    (λ r, by rw [eval₂_C, eval₂_C])
    (λ p q hp hq, by rw [eval₂_add, eval₂_add, hp, hq])
    (λ p s hp, by simp only [eval₂_mul, eval₂_X, hp, (∘), equiv.inverse_apply_apply]),
  right_inv := λ f, induction_on f
    (λ r, by rw [eval₂_C, eval₂_C])
    (λ p q hp hq, by rw [eval₂_add, eval₂_add, hp, hq])
    (λ p s hp, by simp only [eval₂_mul, eval₂_X, hp, (∘), equiv.apply_inverse_apply]) }

set_option profiler true
def ring_equiv_of_equiv (e : σ ≃ τ) : mv_polynomial σ α ≃r mv_polynomial τ α :=
{ hom := eval₂.is_ring_hom _ _, .. equiv_of_equiv e }
set_option profiler false
end mv_polynomial

[Kenny Lau]

elaboration of ring_equiv_of_equiv took 6.48s

[Kenny Lau]

ha, this is really quick

def ring_equiv_of_equiv (e : σ ≃ τ) : mv_polynomial σ α ≃r mv_polynomial τ α :=
ring_equiv.mk (equiv_of_equiv e) $ by apply eval₂.is_ring_hom

[Kenny Lau]

this is also quick:

def ring_equiv_of_equiv (e : σ ≃ τ) : mv_polynomial σ α ≃r mv_polynomial τ α :=
{ hom := by apply eval₂.is_ring_hom, .. equiv_of_equiv e }

[Kenny Lau]

I would appreciate it if someone could point me as to how I could debug it. the set_option trace. options are not very helpful.

[Kenny Lau]

It would also be quite helpful if the "class instance max depth reached" message could tell us which typeclass they were looking for