Zulip Chat Archive

Stream: new members

Topic: Tactic to collapse arithmetic on constants

Jason Orendorff (Jun 16 2020 at 18:52):

I'm doing this as an exercise: https://www.codewars.com/kata/5e8a8f8a18f8ed0010f55280

I'm at the point where I need to prove that ⊢ 2 ^ 2 ^ 5 + 1 = 641 * 6700417.

Is there a tactic that can finish this?

Kevin Buzzard (Jun 16 2020 at 18:58):

norm_num

Jason Orendorff (Jun 16 2020 at 19:04):

perfect!

Johan Commelin (Jun 16 2020 at 19:45):

Does hint tell you that norm_num will do it?

Jason Orendorff (Jun 16 2020 at 21:15):

mmm, no, it times out

Jason Orendorff (Jun 16 2020 at 21:15):

(deterministic) timeout

Reid Barton (Jun 16 2020 at 21:16):

maybe it tried rfl first...

Last updated: Dec 20 2023 at 11:08 UTC