Zulip Chat Archive

Stream: general

Topic: Extremely slow simp


view this post on Zulip Gabriel Ebner (Feb 27 2020 at 23:02):

The following example takes more than one minute on my machine:

import all
set_option trace.simplify true
set_option profiler true

open_locale nnreal
example (a : ) (ha) : ((a, ha : 0) : ) = a :=
by simp

The simplifier rewrites once. However it seems to spend a huge time trying to match add_con.coe_add (20s), con.coe_mul (19s), filter.filter_product.of_one (9s), filter.filter_product.of_neg (4s), and filter.filter_product.of_zero (15s). Does anybody have any idea what's going on here?

view this post on Zulip Rob Lewis (Feb 27 2020 at 23:04):

What are the imports?

view this post on Zulip Gabriel Ebner (Feb 27 2020 at 23:05):

import all

view this post on Zulip Kevin Buzzard (Feb 27 2020 at 23:14):

You should have used squeeze_simp, then you would only have to do it once

view this post on Zulip Rob Lewis (Feb 27 2020 at 23:42):

Past my bedtime now, but the (or a) culprit seems to be an instance search for example : has_mul {r : ℝ // 0 ≤ r} := by apply_instance. nnreal gets unfolded somewhere it shouldn't.

view this post on Zulip Rob Lewis (Feb 27 2020 at 23:48):

Ah, (⟨a, ha⟩ : ℝ≥0) doesn't actually have type nnreal, it has type {r : real // 0 <= r}. Nothing's getting unfolded, it isn't even folded to start with.


Last updated: May 11 2021 at 23:11 UTC