arithmetic timeout with a^2+b^2+c^2=7

Stream: maths

[Kevin Buzzard]

I'm struggling to prove ¬ (∃ a b c : ℕ, a^2+b^2+c^2=7) via the obvious route (a,b,c<=2 and now check all cases). Maybe this is a lousy way to prove it in Lean 3?

import tactic

example : ¬ (∃ a b c : ℕ, a^2+b^2+c^2=7) :=
begin
  rintro ⟨a, b, c, h⟩,
  have ha : a ≤ 2, by nlinarith, -- quick
  have hb : b ≤ 2, by nlinarith, -- slow
--  have hc : c ≤ 2, by nlinarith, -- timeout
--  interval_cases a;
--  interval_cases b;
--  interval_cases c;
--  norm_num at h,
  sorry
end

I might be better off showing everything which is 7 mod 8 isn't the sum of three squares!

[Stuart Presnell]

Is this something that wlog can help with?

[Stuart Presnell]

NB: I've never used wlog and don't know how it works! But presumably after the rintro you should be able to assume an ordering on the three variables and then show that the greatest must be ≤ 2?

[Patrick Johnson]

import tactic

example : ¬∃ (a b c : ℕ), a ^ 2 + b ^ 2 + c ^ 2 = 7 :=
begin
  have h₁ : ∀ {a b c : ℕ}, a ^ 2 + b ^ 2 + c ^ 2 = 7 → a ≤ 2,
  { rintro a b c h, nlinarith },
  rintro ⟨a, b, c, h₂⟩,
  have ha := h₁ h₂,
  have hb := h₁ (by linarith : b ^ 2 + a ^ 2 + c ^ 2 = 7),
  have hc := h₁ (by linarith : c ^ 2 + b ^ 2 + a ^ 2 = 7),
  interval_cases a; interval_cases b; interval_cases c; cases h₂,
end

[Alex J. Best]

zmod way:

import tactic
import data.zmod.basic

example : ¬ (∃ a b c : ℕ, a^2+b^2+c^2=7) :=
begin
  rintro ⟨a, b, c, h⟩,
  apply_fun (coe : ℕ → zmod 8) at h,
  simp only [nat.cast_add, nat.cast_pow, nat.cast_bit1, nat.cast_one] at h,
  revert h,
  generalize : (a : zmod 8) = A,
  generalize : (b : zmod 8) = B,
  generalize : (c : zmod 8) = C,
  dec_trivial!,
end

[Alex J. Best]

Turns out there is a tactic#generalizes for generalizing multiple exprs at once that makes these proofs a bit nicer, TIL!