Stream: new members

Topic: performance

Jason Gross (Jul 21 2020 at 19:32):

Why is norm_num quadratic when there's only linear work to be done? (I've reported this as an issue at https://github.com/leanprover-community/mathlib/issues/3500 , but let me know if it should be reported elsewhere, or if this is not a real bug)

Reid Barton (Jul 21 2020 at 19:57):

I would guess the answer is that simp does quadratic work to build the expressions like f (f (f ...))

Alex J. Best (Jul 21 2020 at 19:58):

What happens if you use simp only  in place of norm_num?

Alex J. Best (Jul 21 2020 at 20:01):

Also in case you weren't aware, it looks like your comp_pow is the same (but not definitionally) as nat.iterate in core. (P.s. this isn't really a new members question!)

Rob Lewis (Jul 21 2020 at 20:19):

This is entirely simp's doing, not norm_num.

Rob Lewis (Jul 21 2020 at 20:20):

(norm_num calls simp, which is why you see it here.)

Jason Gross (Jul 21 2020 at 20:23):

simp only is also quadratic (I've just reported this as https://github.com/leanprover-community/lean/issues/401), but the coefficient on the quadratic is about 100x smaller than for norm_num. This is perhaps fast enough for now, thanks!

Reid Barton (Jul 21 2020 at 20:23):

Because simp only is not trying to rewrite with 100 other simp lemmas.

Rob Lewis (Jul 21 2020 at 20:24):

FYI, if you want norm_num to not try simp itself, you can use norm_num1. Depending on the order things get solved this may or may not make any difference.

Reid Barton (Jul 21 2020 at 20:25):

Obviously this is an artificial example but there is nothing relevant to norm_num here, right?

Rob Lewis (Jul 21 2020 at 20:26):

No, but given its presence in the artificial example, I assume it's actually doing something in the real life case.

Reid Barton (Jul 21 2020 at 20:27):

Anyways this all seems like expected behavior. I'm not surprised that simp is not smart enough to simplify the term it substitutes recursively in the same pass.

Reid Barton (Jul 21 2020 at 20:29):

In fact if it wasn't a definitional equality then the proof term size would be quadratic right?

Jason Gross (Jul 21 2020 at 20:31):

No, but given its presence in the artificial example, I assume it's actually doing something in the real life case.

No, this is just me being inexperienced with Lean and not knowing the proper way to simplify things (I believe someone suggested norm_num a while back when I was doing something else, and I misremembered why it was suggested over simp)

Jason Gross (Jul 21 2020 at 20:32):

@Reid Barton Is the quadratic part really the "attempt to rewrite with non-matching lemmas" and not the "rewrite successfully"?

Jason Gross (Jul 21 2020 at 20:33):

(I am trying to test this, but I can't seem to get simp only to not solve goals that are solvable by rfl...)

Reid Barton (Jul 21 2020 at 20:34):

for testing purposes, you could delete the Σ' P, P = part

Reid Barton (Jul 21 2020 at 20:36):

Let's say simp has finished the left-hand side, then it has a big expression of 100 fs to search for subexpressions which can be rewritten using simp lemmas

Reid Barton (Jul 21 2020 at 20:37):

as far as I know, it will try to match every simp lemma against every subexpression (and give up as soon as it sees the head symbols do not match), every time it expands one more g on the right

Reid Barton (Jul 21 2020 at 20:37):

so it's quadratic * size of simp set

Jason Gross (Jul 21 2020 at 20:48):

simp is top-down rather than bottom-up? Is there any way to tell it to be bottom-up instead? (Also, it doesn't seem like walking the term should be that expensive...)

Reid Barton (Jul 21 2020 at 20:54):

It doesn't matter whether it's top-down or bottom-up once the LHS is done, that's partly why I used that example.

Reid Barton (Jul 21 2020 at 20:56):

Also I imagine that even if it magically knew where to rewrite next every time, there would still be a considerable (and certainly) quadratic amount of bookkeeping work to figure out how to substitute the definition of comp_pow inside the deeply nested context.

Reid Barton (Jul 21 2020 at 20:57):

I imagine it would help if comp_pow built the nested application in the opposite order

Reid Barton (Jul 21 2020 at 21:00):

We generally don't intentionally introduce large expressions like this when proving, so simp is not really optimized for this use case

Reid Barton (Jul 21 2020 at 21:02):

I think simp is actually bottom up but I'm not sure.

Reid Barton (Jul 21 2020 at 21:02):

You can get a sense of the work simp is doing with set_option trace.simplify true

Last updated: May 08 2021 at 19:11 UTC