Zulip Chat Archive

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 = _,

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: Dec 20 2023 at 11:08 UTC