## Stream: general

### Topic: polynomial elaboration

#### Kenny Lau (Jan 29 2019 at 00:02):

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

#### Kenny Lau (Jan 29 2019 at 00:09):

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 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 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 (Jan 29 2019 at 00:09):

elaboration of ring_equiv_of_equiv took 6.48s


#### Kenny Lau (Jan 29 2019 at 00:13):

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 (Jan 29 2019 at 00:15):

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 (Jan 29 2019 at 01:05):

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 (Jan 29 2019 at 08:28):

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

Last updated: May 10 2021 at 00:31 UTC