## Stream: general

### Topic: norm_num and exponentiation

#### Reid Barton (Aug 01 2019 at 19:04):

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 (Aug 01 2019 at 19:10):

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 (Aug 01 2019 at 19:12):

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

#### Rob Lewis (Aug 01 2019 at 19:15):

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

Last updated: May 13 2021 at 21:12 UTC