performance

Stream: new members

[Jason Gross]

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]

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

[Alex J. Best]

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

[Alex J. Best]

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]

This is entirely simp's doing, not norm_num.

[Rob Lewis]

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

[Jason Gross]

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]

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

[Rob Lewis]

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]

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

[Rob Lewis]

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

[Reid Barton]

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]

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

[Jason Gross]

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]

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

[Jason Gross]

(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]

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

[Reid Barton]

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]

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]

so it's quadratic * size of simp set

[Jason Gross]

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]

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]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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