Zulip Chat Archive

Stream: general

Topic: polynomial elaboration


view this post on Zulip Kenny Lau (Jan 29 2019 at 00:02):

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

view this post on Zulip 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 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

view this post on Zulip Kenny Lau (Jan 29 2019 at 00:09):

elaboration of ring_equiv_of_equiv took 6.48s

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip 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.

view this post on Zulip 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