norm_num and exponentiation

Stream: general

[Reid Barton]

This is very slow without the change, and fast (~1s) with it. I don't really understand norm_num so I'm at a loss as to why.
The slow version finishes the tactic quickly, but then it seems that the resulting proof is expensive to check.

example : 2^36 = 68719476736 := begin
  -- change 1*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2*2 = _,
  norm_num,
end

[Rob Lewis]

It's doing kernel computation when it shouldn't -- it's instant if you do it in an arbitrary ring instead of nat. Not sure why.

[Chris Hughes]

No support for nat.pow I guess. The powinstance for nat is not monoid.pow

[Rob Lewis]

I don't think that's it. norm_num finds the same proof for both nat and the arbitrary ring.