nat subtraction hurts

Stream: Is there code for X?

[Scott Morrison]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

Now we're cooking with gas!

[Scott Morrison]

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

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]

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

[Gabriel Ebner]

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]

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]

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]

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]

example : ¬ 1 < 0.

[Kevin Buzzard]

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]

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 _