## Stream: Is there code for X?

### Topic: nat subtraction hurts

#### 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?

#### 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]


#### 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 }


#### 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)]


#### 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!

#### 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]


#### 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.

#### Kevin Buzzard (May 24 2020 at 13:34):

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

#### 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 }


#### Scott Morrison (May 24 2020 at 13:35):

Now we're cooking with gas!

#### 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.

#### 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.

#### 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.

#### 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]


#### 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.

#### 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.

#### 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 _
-/


#### Alex J. Best (May 24 2020 at 15:42):

example : ¬ 1 < 0.


#### 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.

#### 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