Zulip Chat Archive

Stream: new members

Topic: Tactic to collapse arithmetic on constants


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

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 18:58):

norm_num

view this post on Zulip Jason Orendorff (Jun 16 2020 at 19:04):

perfect!

view this post on Zulip Johan Commelin (Jun 16 2020 at 19:45):

Does hint tell you that norm_num will do it?

view this post on Zulip Jason Orendorff (Jun 16 2020 at 21:15):

mmm, no, it times out

view this post on Zulip Jason Orendorff (Jun 16 2020 at 21:15):

(deterministic) timeout

view this post on Zulip Reid Barton (Jun 16 2020 at 21:16):

maybe it tried rfl first...


Last updated: May 13 2021 at 21:12 UTC