norm_num vs simprocs

Stream: mathlib4

[Eric Wieser]

Joe Hendrix said:

and norm num appears to have its own version of simprocs such as the one for equality solving this.

My understanding is that the key difference between norm_num and simprocs is that norm_num maintains an internal representation across pattern matches that is shared between all norm_num extensions, whereas simprocs have to reparse everything from scratch each time

[Eric Wieser]

(which is presumably important for performance)

[Eric Wieser]

Maybe this is a use-case for Expr.mdata nodes?

[Kyle Miller]

I'm curious how the design of norm_num will evolve now that there are simprocs. The main idea is that norm_num puts numeric literals into a normal form (https://github.com/leanprover-community/mathlib4/blob/a8a6713b92e1dc246a2d2a5255bb2d1846e88fe2/Mathlib/Tactic/NormNum/Result.lean#L240-L251), and it's all Qq-enabled so that you can make sure your proofs are type correct.

Potentially, a simproc version of norm_num would be to have derive be a recognizer that either sees the expression is in normal form or causes the simproc to fail, and then norm_num could be a simp set.

[Kyle Miller]

@Eric Wieser I haven't seen evidence that this is true. The derive function recognizes expressions from scratch and produces a Result

[Eric Wieser]

docs#NormNum.Result is that representation I'm referring to, whereas my impression was that simprocs could only return a substitute expression

[Eric Wieser]

So for instance, if I have mul (add 1 2) (add 3 4), then norm_num calls the mul handler, which gets the rich information about the result of the add handlers it dispatches to via derive. With simproc, the add handler runs, produces expressions, and the mul handler then parses those expressions

[Notification Bot]

7 messages were moved here from #nightly-testing > Mathlib status updates by Eric Wieser.

[Kyle Miller]

Yeah, though norm_num extensions don't take any Results as input. There's some possibility for avoiding re-recognition, but that relies on the fact that extensions run derive on arguments. This comes at the risk though, since derive runs the whole norm_num procedure on each argument, so you could be evaluating it many more times than needed.

[Kyle Miller]

There are pre and post norm_num extensions, and even if it's a post extension, my understanding is that if you do derive on an argument, it will attempt to re-normalize that whole expression, even though it's already been visited.

[Kyle Miller]

(@Joe Hendrix this comment a few up was meant to relate to your comment regarding norm_num vs simprocs in the other thread.)

[Joe Hendrix]

Thanks @Eric Wieser for moving the thread.

With regards to the simproc comment, my suggestion was just limited to ensuring simp simprocs are invoked when norm_num falls back to simp. I didn't mean to suggest that norm num should replace it's own version with the Lean simprocs. I only looked into norm_num enough to understand how changes to Lean simp lemmas impact it.

If one were to look into migrating, I'd recommend seeing if it is feasible to maintain a cache from Lean expressions to NormNum.Result so you can preserve the auxillary information.

[Kyle Miller]

(Oops, I misread "A larger fix would be to support Lean core simprocs so norm_num's use of simp matches the simp elaborator." I think integrating better with simprocs would be interesting though!)

[Joe Hendrix]

I should have been more clear. I looked at the simproc code in simp itself, and adding support is a large enough change that it should probably not be taken in a nightly-testing bump.