# Zulip Chat Archive

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