Zulip Chat Archive

Stream: Is there code for X?

Topic: nat subtraction hurts


view this post on Zulip Scott Morrison (May 24 2020 at 13:25):

I just wrote a eight line proof of

lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=

Can someone put me out of my misery?

view this post on Zulip Shing Tak Lam (May 24 2020 at 13:28):

import tactic

lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=
by rw [(show (p - 1) = (p - 2) + 1, by omega), nat.pow_succ, mul_two]

view this post on Zulip Reid Barton (May 24 2020 at 13:31):

Or working in the other direction you can golf it a bit more

import tactic

lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=
by { rw [mul_two, nat.pow_succ], congr, omega }

view this post on Zulip Mario Carneiro (May 24 2020 at 13:32):

without omega:

import data.nat.basic
lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=
by rw [ mul_two,  nat.pow_succ, show (p-2).succ = p-1,
  from nat.succ_pred_eq_of_pos (nat.pred_le_pred w)]

view this post on Zulip Scott Morrison (May 24 2020 at 13:33):

Okay, I will agree these are all shorter than my proof. I feel like all of these solutions still take more effort than this problem deserves!

view this post on Zulip Bhavik Mehta (May 24 2020 at 13:33):

Alternate without omega

lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=
by rw [mul_two, nat.pow_succ,  nat.succ_sub w, nat.succ_sub_succ_eq_sub]

view this post on Zulip Scott Morrison (May 24 2020 at 13:33):

Reid's solution was essentially the same as mine, except that I case bashed for another few lines instead of using omega.

view this post on Zulip Kevin Buzzard (May 24 2020 at 13:34):

If you're using nat subtraction you might be doing it wrong

view this post on Zulip Mario Carneiro (May 24 2020 at 13:34):

If you are going for high powered:

import tactic

lemma foo' {p : } (w : 1 < p) : 2^(p-1) = 2^(p-2) + 2^(p-2) :=
by { rw show (p - 1) = (p - 2) + 1, by omega, ring_exp }

view this post on Zulip Scott Morrison (May 24 2020 at 13:35):

Now we're cooking with gas!

view this post on Zulip Scott Morrison (May 24 2020 at 13:36):

@Kevin Buzzard, when the PR is ready, I'd love to have someone have a good look at the nat/int choices we made here.

view this post on Zulip Scott Morrison (May 24 2020 at 13:39):

I guess actually there is a good solution here, and Kevin is right. I could do all my internal working with p' = p - 2, and then avoid most of the nat subtraction.

view this post on Zulip Scott Morrison (May 24 2020 at 13:40):

There would just be one nat subtraction in the translation between the external theorems and the internal stuff.

view this post on Zulip Gabriel Ebner (May 24 2020 at 14:20):

Another easy low-powered solution:

import data.nat.basic

lemma foo' :  {p : } (w : 1 < p), 2^(p-1) = 2^(p-2) + 2^(p-2)
| 1 w := (lt_irrefl 1 w).elim
| (p+2) _ := by simp [nat.pow_succ, nat.mul_succ]

view this post on Zulip Scott Morrison (May 24 2020 at 15:10):

I always forget to use the pattern matcher on inequality arguments. I think part of it is that I'm not confident ahead of time which patterns will be required: e.g. that you can omit p = 0 here, but still have to handle p = 1.

view this post on Zulip Kevin Buzzard (May 24 2020 at 15:40):

example : ¬ 1 < 0 :=
begin
  intro h,
  cases h,
end

example : ¬ 1 < 1 :=
begin
  intro h,
  cases h with h h,
  cases h,
end

Yeah, the equation compiler isn't trying hard enough.

view this post on Zulip Kevin Buzzard (May 24 2020 at 15:41):

On the other hand, it does tell you:

import data.nat.basic

lemma foo' :  {p : } (w : 1 < p), 2^(p-1) = 2^(p-2) + 2^(p-2)
| (p+2) _ := by simp [nat.pow_succ, nat.mul_succ]
/-
non-exhaustive match, the following cases are missing:
foo' 1 _
-/

view this post on Zulip Alex J. Best (May 24 2020 at 15:42):

example : ¬ 1 < 0.

view this post on Zulip Kevin Buzzard (May 24 2020 at 15:50):

import tactic

example : ¬ 1 < 1 :=
by rintros (_ | ⟨_, ⟨⟩⟩)

Does this just mean the equation compiler isn't trying hard enough? There really are no cases.

view this post on Zulip Kenny Lau (May 24 2020 at 19:23):

import data.nat.basic

lemma foo :  {p : } (H : 1 < p), 2^(p-1) = 2^(p-2) + 2^(p-2)
| 1     H := absurd H $ lt_irrefl 1
| (p+2) _ := mul_two _

Last updated: May 07 2021 at 22:14 UTC