Zulip Chat Archive

Stream: new members

Topic: 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1


view this post on Zulip Julian Berman (Nov 30 2020 at 02:58):

What tactic can prove 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 for me? hint is suggesting ring, but when I use it lean says it didn't make progress.

view this post on Zulip Alex J. Best (Nov 30 2020 at 03:07):

The most tactical proof I can find is

example (d : ) : 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 :=
begin
  zify [nat.one_le_pow'],
  change d.succ with d + 1,
  ring_exp,
end

view this post on Zulip Alex J. Best (Nov 30 2020 at 03:08):

The problem, as always :smile:, is nat subtraction so we need some user input to find the lemma one_le_pow' here I guess.

view this post on Zulip Julian Berman (Nov 30 2020 at 03:09):

hm, thanks, I found both zify and ring_exp but figured there'd be something more sledgehammery

view this post on Zulip Alex J. Best (Nov 30 2020 at 23:33):

I just made #5157 because i noticed ring works as a finisher here without the middle line, but ring_exp doesnt

example (d : ) : 2 * (2 ^ d - 1) + 1 = 2 ^ d.succ - 1 :=
begin
zify [nat.one_le_pow'],
ring,
end

view this post on Zulip Alex J. Best (Nov 30 2020 at 23:35):

Maybe @Anne Baanen has some ideas :smile:?

view this post on Zulip Anne Baanen (Dec 01 2020 at 10:05):

Created #5166 to rewrite nat.succ d to d + 1 automatically, thanks for reporting! :grinning_face_with_smiling_eyes:


Last updated: May 15 2021 at 22:14 UTC