Zulip Chat Archive

Stream: general

Topic: norm_num and exponentiation


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Chris Hughes (Aug 01 2019 at 19:12):

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

view this post on Zulip 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