weird performance of norm_num with Nat.digits

Stream: mathlib4

[David Renshaw]

I'm observing norm_num to be surprisingly slow (taking almost a full second) on Nat.digits 10 N when N is between ~500 and ~1500.

On larger values of N, norm_num finishes much more quickly (like 40ms).

Does anyone have any idea about what might explain this behavior?

import Mathlib.Data.Nat.Digits

set_option trace.profiler true

example : [0,0,7] = Nat.digits 10 700 := by norm_num
-- [Elab.command] [0.769513s] example : [0, 0, 7] = Nat.digits 10 700 := by norm_num

example : [0,0,8] = Nat.digits 10 800 := by norm_num
-- [Elab.command] [0.807374s] example : [0, 0, 8] = Nat.digits 10 800 := by norm_num

example : [0,0,9] = Nat.digits 10 900 := by norm_num
-- [Elab.command] [0.765223s] example : [0, 0, 9] = Nat.digits 10 900 := by norm_num

example : [0,0,0,1] = Nat.digits 10 1000 := by norm_num
-- [Elab.command] [0.741816s] example : [0, 0, 0, 1] = Nat.digits 10 1000 := by norm_num

-- The folowing examples are much faster! Why is that?

example : [0,0,8,1] = Nat.digits 10 1800 := by norm_num
-- [Elab.command] [0.033864s] example : [0, 0, 8, 1] = Nat.digits 10 1800 := by norm_num

example : [0,0,8,2] = Nat.digits 10 2800 := by norm_num
-- [Elab.command] [0.032935s] example : [0, 0, 8, 2] = Nat.digits 10 2800 := by norm_num

example : [9,9,9,9,9] = Nat.digits 10 99999 := by norm_num
-- [Elab.command] [0.035004s] example : [9, 9, 9, 9, 9] = Nat.digits 10 99999 := by norm_num

example : [0,0,0,0,0,0,0,1] = Nat.digits 10 10000000 := by norm_num
-- [Elab.command] [0.043711s] example : [0, 0, 0, 0, 0, 0, 0, 1] = Nat.digits 10 10000000 := by norm_num

[Kyle Miller]

norm_num uses simp -- maybe for small enough numbers it leans more on simp? How does norm_num1 do?

[David Renshaw]

norm_num1 is unable to close any of these goals

[David Renshaw]

simp can close all but the bottom three of them

[Kevin Buzzard]

Similar weirdness here, with 317 being some kind of hole where one algorithm stopped being used and another one took over (and as it turned out didn't work).

[Kyle Miller]

I guess norm_num1 doesn't work because there's no norm num extension for Nat.digits. The way it's working is that it repeatedly applies Nat.digits_add_two_add_one using simp and then reduces the numbers involved.

[Kyle Miller]

I think this is what the first one ends up doing, minus some intermediate simplifications using List.cons.injEq:

example : [0,0,7] = Nat.digits 10 700 := by
  rw [Nat.digits_add_two_add_one]
  norm_num1
  rw [Nat.digits_add_two_add_one]
  norm_num1
  rw [Nat.digits_add_two_add_one]
  norm_num1
  rfl

[David Renshaw]

that proof is fast

[David Renshaw]

so I guess maybe simp gets distracted with some other irrelevant stuff

[David Renshaw]

The conclusion that I'm drawing is that we should port the Nat.digits norm_num extension before worrying too much about this

[David Renshaw]

though it would still be nice to understand exactly why norm_num / simp is currently so slow here

[David Renshaw]

hm... but it looks like norm_num extensions in mathlib4 must return an integer or rational, and Nat.digits does not fit into that model?

This plugin is noticeably less powerful than the equivalent version in Mathlib 3: the design of
norm_num means plugins have to return numerals, rather than a generic expression.

https://github.com/leanprover-community/mathlib4/blob/071f47d27115f6b801ba2e4ba42334817abf2446/Mathlib/Tactic/NormNum/BigOperators.lean#L28-L29

[Kyle Miller]

Yeah, I've been wondering about that. I'm not sure what the plan is for normalizing things like lists, vectors, and matrices is.

[David Renshaw]

This works for the above digits examples, and speeds up the small examples (but slows down the large examples):

repeat (simp (config := {decide := false} ) <;> norm_num1)

[Alex J. Best]

Funily enough I started making a PR to change that simp lemma yesterday #7428 I don't think its a particularly good one as it breaks numerals down which you almost never want.

[David Renshaw]

yeah, I saw that. I tried it on the above examples and it did not seem to make much difference.

[Alex J. Best]

Ah thats sad to hear. I still think its a better simp lemma though. I guess it makes sense that there is a deeper root cause though, norm_num probably doesn't have issues adding the numbers back together again when needed.

[David Renshaw]

I built lean configured with RELWITHDEBINFOand ran it on the slow example, yielding this flame graph. (15MB, will take a few moments to load in your browser).

[David Renshaw]

a very substantial proportion of the time is being spent in whnf stuff

[David Renshaw]

29.74% of the time being spent in l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3

[David Renshaw]

looks like approximately 85% of the time is spent in functions with names containing "whnf", "reduceMatcher", "forallBoundedTelescope", or "forallTelescopeReducing".

[David Renshaw]

Here is maybe a more striking illustration:

import Mathlib.Data.Nat.Digits

set_option maxHeartbeats 5000 in
example : [0,0,0,1] = Nat.digits 10 1000 := by norm_num
-- tactic 'simp' failed, nested error:
-- (deterministic) timeout at 'simp', maximum number of heartbeats (5000) has been reached (use 'set_option maxHeartbeats <num>' to set the limit)

set_option maxHeartbeats 1000 in
example : [0,0,8,1] = Nat.digits 10 1800 := by norm_num
-- goals accomplished

[David Renshaw]

I wonder whether https://github.com/leanprover/lean4/commit/9a7565d66c84bdef37f8cd021fe6ca6eebe7b425 fixes this...

[Mauricio Collares]

Works in #7834, so probably norm_num doesn't expect simp to use decide.

[David Renshaw]

interesting!

[David Renshaw]

look to me like lean4#2730 does not fix this problem.

[David Renshaw]

I can test out turning off decide in norm_num like this:

diff --git a/Mathlib/Tactic/NormNum/Core.lean b/Mathlib/Tactic/NormNum/Core.lean
index ddb35ca06..f82790298 100644
--- a/Mathlib/Tactic/NormNum/Core.lean
+++ b/Mathlib/Tactic/NormNum/Core.lean
@@ -233,6 +233,7 @@ def normNumAt (g : MVarId) (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId)
   let mut g := g
   let mut toAssert := #[]
   let mut replaced := #[]
+  let ctx := { ctx with config := {ctx.config with decide := false}}
   for fvarId in fvarIdsToSimp do
     let localDecl ← fvarId.getDecl
     let type ← instantiateMVars localDecl.type

Indeed, that makes the maxHeartbeats 5000 example pass, and it makes the slow examples from further above somewhat faster. But they are still slower than I would expect.