## Stream: maths

### Topic: IMO problems

#### Kevin Buzzard (Aug 07 2019 at 12:03):

(following on from the IMO2019 thread ): IMO 1988 Q6 has just gone viral at some school maths camp which is taking place at Imperial. It's a famous problem -- the one about if $a$ and $b$ are positive integers such that $ab+1$ divides $a^2+b^2$ then the ratio $\frac{a^2+b^2}{ab+1}$ must be a perfect square. The proof is not too hard if you know the trick, see e.g. Wikipedia but very tough otherwise (as is sometimes the case for IMO problems).

#### Kevin Buzzard (Aug 07 2019 at 12:06):

The guy running the camp is going to make a little video about it, and I've been asked to supply a Lean proof ASAP. I have a busy day :-/ but might get to it later if nobody else takes the bait. The proof is that if the ratio is k, a given fixed non-square, then considering the set of bad pairs (a,b) for which the ratio is k one can choose an element of the set with b<=a and a+b minimised, and then check check that a'=kb-a is a smaller counterexample.

#### Kevin Buzzard (Aug 07 2019 at 12:08):

It would be good to ultimately get a solution in Patrick's formatter

#### Johan Commelin (Aug 07 2019 at 14:35):

Here is a little start:

import data.rat.basic

@[simp] lemma int.square_zero {n : ℤ} : n^2 = 0 ↔ n = 0 :=
begin
rw pow_two,
split,
{ contrapose!, intro h,
rcases lt_trichotomy n 0 with H|rfl|H,
{ apply ne_of_gt, exact mul_pos_of_neg_of_neg H H },
{ apply ne_of_gt, exact mul_pos H H } },
{ rintro rfl, simp },
end

lemma int.square_pos {n : ℤ} : n^2 > 0 ↔ n ≠ 0 :=
begin
rw ←not_iff_not, push_neg,
split,
{ rw ←int.square_zero, intro h, apply le_antisymm h, exact pow_two_nonneg n },
{ rintro rfl, simp [pow_two] }
end

variables {a b : ℤ} (h : a*b + 1 ∣ a^2 + b^2)
include h

lemma nz : a*b + 1 ≠ 0 :=
begin
cases h with c h,
contrapose! h,
simp [h],
rw [add_eq_zero_iff' (pow_two_nonneg _) (pow_two_nonneg _)],
rw [int.square_zero, int.square_zero],
rintro ⟨rfl, rfl⟩,
simpa using h,
end

lemma q6_aux (a b : ℤ) (h : a*b + 1 ∣ a^2 + b^2) :
∃ k : ℤ, a^2 + b^2 = k^2 * (a*b + 1) :=
sorry

lemma q6 (a b : ℤ) (h : a*b + 1 ∣ a^2 + b^2) :
∃ q : ℚ, q^2 = (a^2 + b^2)/(a*b + 1) :=
begin
cases q6_aux a b h with k hk,
use k,
rw_mod_cast hk, rw rat.mk_eq_div,
simp,
rw mul_div_cancel,
norm_cast,
simpa using nz h,
end


#### Alex J. Best (Aug 07 2019 at 14:46):

I also started, but may not finish :rolling_on_the_floor_laughing:

import data.nat.basic
import data.int.basic
import order.basic
import algebra.ring
import tactic.wlog
import tactic.omega
import tactic.tidy
import tactic.library_search

local attribute [instance, priority 0] classical.prop_decidable

theorem q6 (a b : ℕ) (h : ((a*b + 1) ∣ (a^2 + b^2))) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a*b + 1)  :=
begin
suffices : ∀ a b : ℕ, ∀ (h : ((a*b + 1) ∣ (a^2 + b^2))), ∃ k : ℕ , k^2 = (a^2 + b^2) / (a*b + 1), by exact this a b h,
clear h a b, -- forget about a b now
-- the set of possible counterexamples
let A : set (ℕ × ℕ) := { ab | (ab.1*ab.2 + 1) ∣ (ab.1^2 + ab.2^2) ∧ ¬ (∃ k : ℕ , k^2 = (ab.1^2 + ab.2^2) / (ab.1*ab.2 + 1)) },
suffices : A = ∅, begin
intros a b h,
have ab_in_A : (⟨ a, b ⟩ : ℕ × ℕ) ∈ A := begin dsimp, split, exact h, exact not_exists, end,
rw set.eq_empty_iff_forall_not_mem at this,
have := this ⟨a, b⟩,
end,
let r : (ℕ × ℕ) → ℕ := λ ⟨a, b⟩, a + b,
let min_elem := well_founded.min (measure_wf r) A h,
let a := max min_elem.1 min_elem.2,
let b := min min_elem.1 min_elem.2,
have min_is_elem : min_elem ∈ A := well_founded.min_mem (measure_wf r) A h,
dsimp at min_is_elem,
have ab_mem : (a, b) ∈ A := begin
dsimp,
by_cases min_elem.1 ≤ min_elem.2,
{
have : a = min_elem.2 := if_pos h,
rw this,
have : b = min_elem.1 := if_pos h,
rw this,
simp at min_is_elem,
simp [mul_comm,min_is_elem],
},
{
have : a = min_elem.1 := if_neg h,
rw this,
have : b = min_elem.2 := if_neg h,
rw this,
exact min_is_elem,
}
end,
let x := (a^2 + b^2) / (a*b + 1),
let newa := x*b - a,
have new_mem : (newa, b) ∈ A := begin
simp [newa, x],
split,
end,
have new_smaller : measure r (newa, b) (a, b) := begin sorry end,
have := well_founded.not_lt_min (measure_wf r) A h new_mem,

end


#### Johan Commelin (Aug 07 2019 at 15:14):

Ok, I missed the positivity condition.

#### Johan Commelin (Aug 07 2019 at 15:15):

@Kevin Buzzard What does "positive" mean on IMO problems?

≥ 0 or > 0?

0

#### Kevin Buzzard (Aug 07 2019 at 15:15):

rofl > 0

Great.

#### Johan Commelin (Aug 07 2019 at 15:15):

The strategy would be to use prod.lex_wf

#### Johan Commelin (Aug 07 2019 at 15:16):

And well_found.min

#### Johan Commelin (Aug 07 2019 at 15:16):

I don't have working Lean nearby, but I think this should be very straightforward.

#### Johan Commelin (Aug 07 2019 at 15:24):

It would be nice to formalise a theorem standard_vieta_jumping and standard_vieta_jumping_2

#### Johan Commelin (Aug 07 2019 at 15:24):

(The latter would take two arguments, instead of pairs.)

#### Johan Commelin (Aug 07 2019 at 15:41):

Hmmm, maybe I should shut up and code before doing any more talking.

#### Alex J. Best (Aug 07 2019 at 15:54):

Its still true if you just assume nonneg right? At least that's how I justified using nat to myself so id have less hypotheses floating around

#### Floris van Doorn (Aug 07 2019 at 17:43):

Did we have this part already?

import data.int.basic

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
(h : x * x - b * x + c = 0) : ∃ y : α,
y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end


That's nice!

#### Alex J. Best (Aug 07 2019 at 18:04):

Oh cool, here's where I'm up to, going to stop for a while so feel free to combine them and finish (if you want to) I think that missing piece is almost everything (except some sillyness?)

import data.nat.basic
import data.int.basic
import order.basic
import algebra.ring
import tactic.wlog
import tactic.interactive
import tactic.omega
import tactic.abel
import tactic.linarith
import tactic.tidy
import tactic.library_search

local attribute [instance, priority 0] classical.prop_decidable

lemma max_add_min (a b : ℤ) : max a b + min a b = a + b :=
begin
by_cases a ≤ b,
{
have : min a b = a := if_pos h,
rw this,
have : max a b = b := if_pos h,
},
{
have : min a b = b := if_neg h,
rw this,
have : max a b = a := if_neg h,
rw this,
}
end

lemma dumb_measure_fact {α : Type*} (r : α → ℕ) (a b c : α) (h : r a = r b) : measure r c a ↔ measure r c b :=
begin
change r c < r a ↔ r c < r b,
rwa ← h,
end

theorem q6 (a b : ℤ) (ha : a > 0) (hb : b > 0) (h : ((a*b + 1) ∣ (a^2 + b^2))) : ∃ k : ℤ, k^2 = (a^2 + b^2) / (a*b + 1)  :=
begin
suffices : ∀ a b : ℤ, ∀ ha : a > 0, ∀ hb : b > 0, ∀ h : ((a*b + 1) ∣ (a^2 + b^2)), ∃ k : ℤ, k^2 = (a^2 + b^2) / (a*b + 1), by exact this a b ha hb h,
clear h ha hb a b, -- forget about a b now
-- the set of possible counterexamples
let A : set (ℤ × ℤ) := { ab | (ab.1 > 0) ∧ (ab.2 > 0) ∧ ((ab.1*ab.2 + 1) ∣ (ab.1^2 + ab.2^2)) ∧ ¬ (∃ k : ℤ, k^2 = (ab.1^2 + ab.2^2) / (ab.1*ab.2 + 1)) },
suffices : A = ∅, begin
intros a b ha hb h,
have ab_in_A : (⟨ a, b ⟩ : ℤ × ℤ) ∈ A := begin rw set.mem_set_of_eq, split, exact ha, split, exact hb, split, exact h, exact not_exists, end,
rw set.eq_empty_iff_forall_not_mem at this,
have := this ⟨a, b⟩,
end,
let r : (ℤ × ℤ) → ℕ := λ ⟨a, b⟩, int.nat_abs (a + b),
let min_elem := well_founded.min (measure_wf r) A h,
let a := max min_elem.1 min_elem.2,
let b := min min_elem.1 min_elem.2,
have min_is_elem : min_elem ∈ A := well_founded.min_mem (measure_wf r) A h,
dsimp at min_is_elem,
have ab_mem : (a, b) ∈ A := begin
dsimp,
by_cases min_elem.1 ≤ min_elem.2,
{
have : a = min_elem.2 := if_pos h,
rw this,
have : b = min_elem.1 := if_pos h,
rw this,
simp at min_is_elem,
simp [mul_comm,min_is_elem],
},
{
have : a = min_elem.1 := if_neg h,
rw this,
have : b = min_elem.2 := if_neg h,
rw this,
exact min_is_elem,
}
end,
rcases ab_mem with ⟨ha, hb, h1, h2⟩,
dsimp at *,

let x := (a^2 + b^2) / (a*b + 1),
have a2b2_pos : 0 < a^2 + b^2 := add_pos (pow_pos ha 2) (pow_pos hb 2),
have abadd1_pos : 0 < a*b + 1 := add_pos (mul_pos ha hb) int.one_pos,
have x_pos : 0 < x := sorry,
let newa := x*b - a,
have newa_pos : 0 < newa := by sorry,
have new_mem : (newa, b) ∈ A := begin
squeeze_simp [newa],
have : x = (newa^2 + b^2) / (newa*b + 1) := begin
simp [newa],
ring,
apply eq.symm,
rw int.div_eq_iff_eq_mul_right _ _,
ring,
sorry,
sorry,
sorry,
end,
split,
{
ring,
sorry,
},
{sorry,
},
end,
have new_smaller : measure r (newa, b) (a, b) := begin
suffices : ((int.nat_abs (newa + b)) : ℤ) < (int.nat_abs (a + b)),
exact int.coe_nat_lt.mp this,
rw (int.nat_abs_of_nonneg $le_of_lt$ add_pos newa_pos hb),
rw (int.nat_abs_of_nonneg $le_of_lt$ add_pos ha hb),
suffices : (newa < a),
{linarith},
sorry
end,
have := well_founded.not_lt_min (measure_wf r) A h new_mem,
have measure_eq : r min_elem = r (a, b) := begin squeeze_simp [r, a, b], rw max_add_min,
sorry, end,
simp only [min_elem] at measure_eq,
rw dumb_measure_fact at this,
exact measure_eq,
end


#### Kevin Buzzard (Aug 07 2019 at 18:06):

Thanks to everyone for this. I am bogged down in a grant application and would never have got round to doing this over the next few days.

#### Johan Commelin (Aug 07 2019 at 18:37):

@Alex J. Best That's an impressively long proof!

#### Alex J. Best (Aug 07 2019 at 18:38):

Yeah thats my bad lol, I always forget to split things off into lemmas.

#### Alex J. Best (Aug 07 2019 at 18:40):

Also I still write things in an inefficient way I'm sure!

#### Floris van Doorn (Aug 07 2019 at 19:59):

I'm also working on this, and almost done. I'm struggling a bit with the argument (on the Wikipedia page) that x_2 is nonnegative: you have to show that x_2 * B + 1 != 0. If it were equal to 0, then you can easily derive a contradiction, using the fact that a ^ 2 + b ^ 2 = 0 -> a = b = 0. Is this fact already in mathlib?

import data.int.basic

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
(h : x * x - b * x + c = 0) : ∃ y : α,
y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, mul_comm, this],
end

lemma fn_min_add_fn_max {α β} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β)
(n m : α) : f (min n m) + f (max n m) = f n + f m :=
begin
by_cases n ≤ m, { simp [h] },
have : m ≤ n := le_of_lt (lt_of_not_ge h),
simp [this]
end

lemma min_add_max {α} [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
min n m + max n m = n + m :=

lemma fn_min_mul_fn_max {α β} [decidable_linear_order α] [comm_semigroup β] (f : α → β)
(n m : α) : f (min n m) * f (max n m) = f n * f m :=
begin
by_cases n ≤ m, { simp [h] },
have : m ≤ n := le_of_lt (lt_of_not_ge h),
simp [this, mul_comm]
end

lemma min_mul_max {α} [decidable_linear_order α] [comm_semigroup α] (n m : α) :
min n m * max n m = n * m :=
fn_min_mul_fn_max id n m

lemma min_le_max {α} [decidable_linear_order α] (n m : α) : min n m ≤ max n m :=
le_trans (min_le_left n m) (le_max_left n m)

lemma eq_iff_eq_of_eq {α} {x y z : α} (h : x = y) : x = z ↔ y = z :=
by rw [h]

theorem q6' (k : ℕ) (h : ∃ a b : ℕ, a * a + b * b = (a * b + 1) * k) : ∃ l : ℕ , l * l = k :=
begin
have lemma1 : ∀{a b : ℤ}, a * a + b * b = (a * b + 1) * k ↔ b * b - (k * a) * b + (a * a - k) = 0,
{ intros a b, rw [right_distrib, ← sub_eq_iff_eq_add, ← sub_eq_zero],
apply eq_iff_eq_of_eq, simp [mul_comm, mul_assoc] },
cases nat.eq_zero_or_pos k with hk hk, { use 0, rw [hk], refl },
let s : set (ℕ × ℕ) := { ab | ab.1 * ab.1 + ab.2 * ab.2 = (ab.1 * ab.2 + 1) * k },
have hs : s ≠ ∅,
{ rw [set.ne_empty_iff_exists_mem], rcases h with ⟨a, b, hab⟩,
use ⟨a, b⟩, simp [hab] },
let r : ℕ × ℕ → ℕ := λ ab, ab.1 + ab.2,
let s_min := well_founded.min (measure_wf r) s hs,
let a' : ℕ := min s_min.1 s_min.2,
let b' : ℕ := max s_min.1 s_min.2,
let a : ℤ := a',
let b : ℤ := b',
have ha : 0 ≤ a := int.coe_zero_le a',
have hb : 0 ≤ b := int.coe_zero_le b',
have a_le_b : a ≤ b, { apply_mod_cast min_le_max },
have hab : a * a + b * b = (a * b + 1) * k,
{ norm_cast,
rw [fn_min_add_fn_max (λ x, x * x) s_min.1 s_min.2, min_mul_max s_min.1 s_min.2],
exact well_founded.min_mem (measure_wf r) s hs },
have h2ab : b * b - (k * a) * b + (a * a - k) = 0, { rwa [← lemma1] },
rcases Vieta_formula_quadratic h2ab with ⟨c, h1c, h2c, h3c⟩,
have h4c : c ≥ 0,
{ have : c * c + a * a = k * (c * a + 1),
{ sorry },
have : (0 : ℤ) ≤ k * (c * a + 1),
{ rw [← this], apply add_nonneg; apply mul_self_nonneg },
-- apply nonneg_of_mul_nonneg_right,
sorry
},
have h5c : c < b,
{ apply lt_of_mul_lt_mul_left _ hb, rw [h3c],
apply lt_of_lt_of_le (sub_lt_self _ _) (mul_le_mul a_le_b a_le_b ha hb),
apply_mod_cast hk },
obtain ⟨c', rfl⟩ : ∃ c' : ℕ, c = c',
{ use c.nat_abs, rw [int.nat_abs_of_nonneg h4c] },
suffices : c' = 0,
{ subst this, use a', rw [int.coe_nat_zero, mul_zero, eq_comm, sub_eq_zero] at h3c,
exact_mod_cast h3c },
have hc' : (a', c') ∈ s,
{ rw [← lemma1] at h1c, exact_mod_cast h1c },
have : a' + b' ≤ a' + c',
{ rw [← not_lt, min_add_max s_min.1 s_min.2],
exact well_founded.not_lt_min (measure_wf r) s hs hc' },
sorry
end

theorem q6 (a b : ℕ) (h : a*b + 1 ∣ a^2 + b^2) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a * b + 1)  :=
begin
cases h with k hk,
cases q6' k ⟨a, b, _⟩ with l hl,
swap, rw [← nat.pow_two, ← nat.pow_two, hk],
use l, rw [hk, nat.mul_div_cancel_left], rw [nat.pow_two, hl], apply nat.zero_lt_succ
end


#### Chris Hughes (Aug 07 2019 at 20:03):

I think nat.add_eq_zero and nat.mul_self_eq_zero are there.

#### Kevin Buzzard (Aug 07 2019 at 20:07):

In the proof that the complexes are a field it uses a lemma of the form x*x+y*y=0 -> x=0 but I can't remember the hypotheses, it might be totally ordered fields

#### Floris van Doorn (Aug 07 2019 at 20:26):

done!

import data.int.basic tactic.ring

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α} (h : x * x - b * x + c = 0) :
∃ y : α, y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, mul_comm, this],
end

lemma fn_min_add_fn_max {α β} [decidable_linear_order α] [add_comm_semigroup β] (f : α → β)
(n m : α) : f (min n m) + f (max n m) = f n + f m :=
begin
by_cases n ≤ m, { simp [h] },
have : m ≤ n := le_of_lt (lt_of_not_ge h),
simp [this]
end

lemma min_add_max {α} [decidable_linear_order α] [add_comm_semigroup α] (n m : α) :
min n m + max n m = n + m :=

lemma fn_min_mul_fn_max {α β} [decidable_linear_order α] [comm_semigroup β] (f : α → β)
(n m : α) : f (min n m) * f (max n m) = f n * f m :=
begin
by_cases n ≤ m, { simp [h] },
have : m ≤ n := le_of_lt (lt_of_not_ge h),
simp [this, mul_comm]
end

lemma min_mul_max {α} [decidable_linear_order α] [comm_semigroup α] (n m : α) :
min n m * max n m = n * m :=
fn_min_mul_fn_max id n m

lemma min_le_max {α} [decidable_linear_order α] (n m : α) : min n m ≤ max n m :=
le_trans (min_le_left n m) (le_max_left n m)

lemma eq_iff_eq_of_eq {α} {x y z : α} (h : x = y) : x = z ↔ y = z :=
by rw [h]

lemma mul_self_eq_zero {α} [domain α] {x : α} : x * x = 0 ↔ x = 0 :=
by simp

lemma mul_self_add_mul_self_eq_zero {α} [linear_ordered_ring α] {x y : α} :
x * x + y * y = 0 ↔ x = 0 ∧ y = 0 :=
begin
split; intro h, swap, { rcases h with ⟨rfl, rfl⟩, norm_num },
have : y * y ≤ 0, { rw [← h], apply le_add_of_nonneg_left (mul_self_nonneg x) },
have : y * y = 0 := le_antisymm this (mul_self_nonneg y),
rw mul_self_eq_zero at this,
have : x = 0, { rwa [this, mul_zero, add_zero, mul_self_eq_zero] at h },
split; assumption
end

theorem q6' (k : ℕ) (h : ∃ a b : ℕ, a * a + b * b = (a * b + 1) * k) : ∃ l : ℕ , l * l = k :=
begin
have lemma1 : ∀{a b : ℤ}, a * a + b * b = (a * b + 1) * k ↔ b * b - (k * a) * b + (a * a - k) = 0,
{ intros a b, rw [right_distrib, ← sub_eq_iff_eq_add, ← sub_eq_zero],
apply eq_iff_eq_of_eq, simp [mul_comm, mul_assoc] },
cases nat.eq_zero_or_pos k with hk hk, { use 0, rw [hk], refl },
let s : set (ℕ × ℕ) := { ab | ab.1 * ab.1 + ab.2 * ab.2 = (ab.1 * ab.2 + 1) * k },
have hs : s ≠ ∅,
{ rw [set.ne_empty_iff_exists_mem], rcases h with ⟨a, b, hab⟩,
use ⟨a, b⟩, simp [hab] },
let r : ℕ × ℕ → ℕ := λ ab, ab.1 + ab.2,
let s_min := well_founded.min (measure_wf r) s hs,
let a' : ℕ := min s_min.1 s_min.2,
let b' : ℕ := max s_min.1 s_min.2,
let a : ℤ := a',
let b : ℤ := b',
have ha : 0 ≤ a := int.coe_zero_le a',
have hb : 0 ≤ b := int.coe_zero_le b',
have a_le_b : a ≤ b, { apply_mod_cast min_le_max },
have hab : a * a + b * b = (a * b + 1) * k,
{ norm_cast,
rw [fn_min_add_fn_max (λ x, x * x) s_min.1 s_min.2, min_mul_max s_min.1 s_min.2],
exact well_founded.min_mem (measure_wf r) s hs },
have h2ab : b * b - (k * a) * b + (a * a - k) = 0, { rwa [← lemma1] },
cases eq_or_lt_of_le ha with h2a h2a, -- if a = 0 it is easy
{ use b', rw [← h2a] at hab, have : b * b = k, { simpa using hab }, exact_mod_cast this },
rcases Vieta_formula_quadratic h2ab with ⟨c, h1c, h2c, h3c⟩,
have h4c : c ≥ 0,
{ have h1 : c * c + a * a = k * (c * a + 1),
have : 0 ≤ ↑k * (c * a + 1),
{ rw [← h1], apply add_nonneg; apply mul_self_nonneg },
have : 0 ≤ c * a + 1,
{ apply nonneg_of_mul_nonneg_left this, apply_mod_cast hk },
have : 0 ≤ c * a,
{ apply int.le_of_lt_add_one, apply lt_of_le_of_ne this,
intro h2, rw [← h2, mul_zero, mul_self_add_mul_self_eq_zero] at h1,
exact ne_of_gt h2a h1.2 },
apply nonneg_of_mul_nonneg_right this,
exact h2a },
have h5c : c < b,
{ apply lt_of_mul_lt_mul_left _ hb, rw [h3c],
apply lt_of_lt_of_le (sub_lt_self _ _) (mul_le_mul a_le_b a_le_b ha hb),
apply_mod_cast hk },
obtain ⟨c', rfl⟩ : ∃ c' : ℕ, c = c',
{ use c.nat_abs, rw [int.nat_abs_of_nonneg h4c] },
have hc' : (a', c') ∈ s,
{ rw [← lemma1] at h1c, exact_mod_cast h1c },
have : a' + b' ≤ a' + c',
{ rw [← not_lt, min_add_max s_min.1 s_min.2],
exact well_founded.not_lt_min (measure_wf r) s hs hc' },
exfalso, apply not_le_of_lt h5c,
end

theorem q6 (a b : ℕ) (h : a*b + 1 ∣ a^2 + b^2) : ∃ k : ℕ , k^2 = (a^2 + b^2) / (a * b + 1)  :=
begin
cases h with k hk,
cases q6' k ⟨a, b, _⟩ with l hl,
swap, rw [← nat.pow_two, ← nat.pow_two, hk],
use l, rw [hk, nat.mul_div_cancel_left], rw [nat.pow_two, hl], apply nat.zero_lt_succ
end


#### Floris van Doorn (Aug 07 2019 at 20:31):

I used some of @Alex J. Best proof steps (involving finding the minimal pair).

#### Alex J. Best (Aug 07 2019 at 20:35):

I used some of Alex J. Best proof steps (involving finding the minimal pair).

Nice job! I'm glad some of what I did was helpful in the end :upside_down:

#### Alex J. Best (Aug 07 2019 at 20:39):

I wonder how much of the overall strategy can be made into a general infinite_descent or vieta_jumping theorem? For instance to prove the other example on the wikipedia page also:

Let a and b be positive integers such that ab divides a^2 + b^2 + 1. Prove that 3ab= a^2 + b^2 + 1

#### Johan Commelin (Aug 07 2019 at 20:54):

This is what I have so far:

import data.rat.basic
import tactic.linarith
import tactic.wlog

-- local attribute [instance] classical.prop_decidable
local attribute [simp] nat.pow_two

lemma nat.le_one_cases : ∀ n ≤ 1, n = 0 ∨ n = 1
| 0     h := by left;  refl
| 1     h := by right; refl
| (n+2) h := by linarith

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
(h : x * x - b * x + c = 0) : ∃ y : α,
y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end

lemma infinite_descent (P : ℕ → Prop) (n : ℕ) (hn : P n)
(ih : ∀ n, n > 0 → P n → ∃ m < n, P m) : P 0 :=
begin
-- let k := well_founded.min
sorry
end

variables (k a b : ℕ)

@[reducible]
def P := a^2 + b^2 = k * a * b + k

variables {k a b}

lemma P_comm : P k a b ↔ P k b a :=
begin
unfold P,
end

lemma P.symm (h : P k a b) : P k b a := P_comm.mp h

lemma P_of_eq (h : P k a a) : k ≤ 1 :=
begin
replace h : 2 * a ^ 2 = k * (a ^ 2 + 1),
{ simpa [P, two_mul, mul_add, mul_assoc] using h, },
contrapose! h,
apply ne_of_lt,
calc 2 * a^2 ≤ k * a^2       : nat.mul_le_mul_right _ h
... < k * (a^2 + 1) :
begin
apply mul_lt_mul',
all_goals {linarith},
end
end

lemma P.level_zero (h : P 0 a b) : a = 0 ∧ b = 0 :=
begin
simpa [P] using h,
end

lemma P_zero (h : P k a 0) : k = a^2 :=
begin
symmetry,
simpa [P] using h
end

P k a b ↔ (b:ℤ) * b - (k * a) * b + (a^2 - k) = 0 :=
begin
unfold P,
rw [← int.coe_nat_inj', ← sub_eq_zero],
simp [pow_two],
end

lemma P.level_pos (h : P k a b) (H : a < b) : k > 0 :=
begin
contrapose! H,
rw nat.le_zero_iff at H,
subst k,
rcases h.level_zero with ⟨rfl, rfl⟩,
refl
end

lemma P_root_ineq (h : P k a b) (H : a < b) : b ≤ k*a :=
begin
rcases nat.exists_eq_add_of_le (le_of_lt H) with ⟨c, rfl⟩,
rcases nat.exists_eq_add_of_lt (h.level_pos H) with ⟨l, rfl⟩,
clear H,
simp only [P, zero_add] at h ⊢,
simp at h,
ring at h,
-- contrapose! h,
end

lemma P_vieta_jump (h : P k a b) (H : a < b) : P k a (k*a - b) :=
begin
have hb : b ≤ k*a := P_root_ineq h H,
rcases Vieta_formula_quadratic h with ⟨c, h_root, hV₁, hV₂⟩,
simpa only [eq_sub_of_add_eq' hV₁, int.coe_nat_sub hb] using h_root,
end

lemma level_square (h : P k a b) (H : k > 1) : ∃ d, k = d^2 :=
begin
suffices h₀ : ∃ d, P k d 0,
{ rcases h₀ with ⟨d, hd⟩,
use d,
exact P_zero hd },
apply infinite_descent (λ y, ∃ x, P k x y) b ⟨a, h⟩,
clear h a b,
rintros b bpos ⟨a, h⟩,
have aneb : a ≠ b,
{ contrapose! H,
subst H,
exact P_of_eq h },
rcases lt_trichotomy a b with h'|rfl|h',
{ use [a, H', k*a - b],
rw P_comm,
apply P_vieta_jump h H', },
{ specialize this (lt_trans bpos H') h.symm aneb.symm, }
end


#### Johan Commelin (Aug 07 2019 at 20:54):

This follows the ideas at the bottom of the Wiki page.

#### Johan Commelin (Aug 07 2019 at 20:57):

I've tried to write it in a style that is easy to document for use with Patrick's formatter.

#### Johan Commelin (Aug 07 2019 at 20:57):

I'm struggling with two the "wlog" part of the proof :expressionless:

#### Johan Commelin (Aug 08 2019 at 00:02):

Ok, here is my working solution

import data.rat.basic
import tactic.linarith
import tactic.wlog

local attribute [simp] nat.pow_two

lemma nat.le_one_cases : ∀ n ≤ 1, n = 0 ∨ n = 1
| 0     h := by left;  refl
| 1     h := by right; refl
| (n+2) h := by linarith

/- Vieta's formula for a quadratic equation -/
lemma Vieta_formula_quadratic {α} [comm_ring α] {b c x : α}
(h : x * x - b * x + c = 0) : ∃ y : α,
y * y - b * y + c = 0 ∧ x + y = b ∧ x * y = c :=
begin
have : c = b * x - x * x, { apply eq_of_sub_eq_zero, simpa using h },
use b - x, simp [left_distrib, right_distrib, mul_comm, this],
end

variables (k a b : ℕ)

@[reducible]
def P := a^2 + b^2 = k * a * b + k

variables {k a b}

lemma P_comm : P k a b ↔ P k b a :=
begin
unfold P,
end

lemma P.symm (h : P k a b) : P k b a := P_comm.mp h

lemma level_le_one_of_eq (h : P k a a) : k ≤ 1 :=
begin
replace h : 2 * a ^ 2 = k * (a ^ 2 + 1),
{ simpa [P, two_mul, mul_add, mul_assoc] using h, },
contrapose! h,
apply ne_of_lt,
calc 2 * a^2 ≤ k * a^2       : nat.mul_le_mul_right _ h
... < k * (a^2 + 1) :
begin
apply mul_lt_mul',
all_goals {linarith},
end
end

lemma P.level_zero (h : P 0 a b) : a = 0 ∧ b = 0 :=
begin
simpa [P] using h,
end

lemma P_zero (h : P k a 0) : k = a^2 :=
begin
symmetry,
simpa [P] using h
end

P k a b ↔ (b:ℤ) * b - (k * a) * b + (a^2 - k) = 0 :=
begin
unfold P,
rw [← int.coe_nat_inj', ← sub_eq_zero],
simp [pow_two],
end

lemma P.level_pos (h : P k a b) (H : a < b) : k > 0 :=
begin
contrapose! H,
rw nat.le_zero_iff at H,
subst k,
rcases h.level_zero with ⟨rfl, rfl⟩,
refl
end

lemma P_vieta_jump (h : P k a b) (ha : a > 0) (H : a < b) :
P k a (k*a - b) ∧ (k*a - b < a) :=
begin
have hk := h.level_pos H,
rcases Vieta_formula_quadratic h with ⟨c, h_root, hV₁, hV₂⟩,
have hnat : c ≥ 0,
{ have Pkac : (a:ℤ)^2 + c^2 = (a * c + 1) * k,
{ rw [← sub_eq_zero, ← h_root],
ring },
have hpos : (a:ℤ)^2 + c^2 > 0,
{ rw pow_two,
apply mul_pos;
exact_mod_cast ha },
{ apply pow_two_nonneg } },
rw Pkac at hpos,
replace hpos : (a:ℤ) * c + 1 > 0 := pos_of_mul_pos_right hpos
(by exact_mod_cast (le_of_lt hk)),
replace hpos : (a:ℤ) * c ≥ 0 := int.le_of_lt_add_one hpos,
apply nonneg_of_mul_nonneg_left hpos (by exact_mod_cast ha), },
have b_le_ka : b ≤ k * a,
{ rw [← int.coe_nat_le, ← sub_nonneg],
rw hc at hnat,
exact_mod_cast hnat },
have c_lt_a : c < a,
{ contrapose! hV₂,
apply ne_of_gt,
calc (b:ℤ) * c > a^2 :
begin
rw pow_two,
apply mul_lt_mul,
all_goals { linarith },
end
... > a^2 - k : sub_lt_self _ (by exact_mod_cast hk) },
subst c,
split,
{ simpa only [int.coe_nat_sub b_le_ka] using h_root },
{ assumption_mod_cast },
end

lemma infinite_descent (P : ℕ → Prop) (n : ℕ) (hn : P n)
(ih : ∀ n > 0, P n → (P 0 ∨ ∃ m < n, P m)) : P 0 :=
begin
have h : P ≠ (∅ : set ℕ),
{ rintro rfl,
assumption, },
let k := well_founded.min nat.lt_wf P h,
have hPk : P k := well_founded.min_mem nat.lt_wf P h,
by_cases hk : k = 0,
{ rwa hk at hPk },
replace hk : k > 0 := nat.pos_iff_ne_zero.mpr hk,
rcases ih k hk hPk with H|⟨m,hm,hPm⟩,
{ assumption },
{ exfalso,
exact well_founded.not_lt_min nat.lt_wf P h hPm hm, },
end

lemma level_square (h : P k a b) : ∃ d, k = d^2 :=
begin
wlog : a ≤ b,
swap,
{ exact this h.symm },
by_cases H : a = b,
{ subst H,
replace h := level_le_one_of_eq h,
rcases nat.le_one_cases k h with rfl|rfl,
{ use 0,
simp, },
{ use 1,
simp, } },
suffices h₀ : ∃ d, P k d 0,
{ rcases h₀ with ⟨d, hd⟩,
use d,
exact P_zero hd },
replace H : a < b := lt_of_le_of_ne case H,
{ have := infinite_descent (λ y, ∃ x, P k x y ∧ (y > 0 → x < y)) b _ _,
{ simpa using this },
{ use [a, h],
intro,
assumption },
{ clear h H case a b,
rintros b bpos ⟨a, h, h'⟩,
specialize h' bpos,
by_cases ha : a = 0,
{ left,
subst a,
simp,
use [b, h.symm], },
{ right,
use [a, h', k*a - b],
replace ha : a > 0 := nat.pos_iff_ne_zero.mpr ha,
cases P_vieta_jump h ha h',
split,
{ rwa P_comm, },
{ intro,
assumption } } } },
end


#### Johan Commelin (Aug 08 2019 at 00:02):

Maybe, strictly speaking, I should include a little wrapper at the end...

#### Johan Commelin (Aug 08 2019 at 00:03):

But Kevin didn't provide a formalisation. So I will say that I completed the problem (-;

#### Johan Commelin (Aug 09 2019 at 11:10):

@Kevin Buzzard Voila:

example {a b : ℕ} (h : a*b ∣ a^2 + b^2 + 1) :
3*a*b = a^2 + b^2 + 1 :=
begin
rcases h with ⟨k, hk⟩,
suffices : k = 3, { simp * at *, ring, },
simp only [nat.pow_two] at hk,
apply constant_descent_vieta_jumping a b hk (λ x, k * x) (λ x, x*x + 1) (λ x y, x ≤ 1),
{ intros x y, simp, apply eq_iff_eq_cancel_left, ring },
{ intros x y, dsimp,
rw [← int.coe_nat_inj', ← sub_eq_zero],
apply eq_iff_eq_cancel_right,
simp, ring, },
{ simp },
{ clear hk a b, intros x hx,
have x_sq_dvd : x*x ∣ x*x*k := dvd_mul_right (x*x) k,
rw ← hx at x_sq_dvd,
rcases x_sq_dvd with ⟨y, hy⟩,
rw eq_comm at hy,
simp [nat.mul_eq_one_iff] at hy,
rcases hy with ⟨rfl,rfl⟩,
simpa using hx.symm, },
{ clear hk a b,
intros x y x_lt_y hx h_base h z h_root hV₁ hV₀,
split,
{ have zy_pos : z * y ≥ 0,
{ rw hV₀, exact_mod_cast (nat.zero_le _) },
apply nonneg_of_mul_nonneg_right zy_pos,
linarith },
{ contrapose! hV₀,
apply ne_of_gt,
push_neg at h_base,
calc z * y > x * y       : by apply mul_lt_mul_of_pos_right; linarith
... ≥ x * (x + 1) : by apply mul_le_mul; linarith
... > x * x + 1   :
begin
assumption_mod_cast
end, } },
{ intros x y h h_base,
rcases nat.le_one_cases x h_base with rfl|rfl,
{ simp at h, contradiction },
{ simp at h,
have y_dvd : y ∣ y * k := dvd_mul_right y k,
have y_eq : y = 1 ∨ y = 2 := nat.prime_two.2 y y_dvd,
rcases y_eq with rfl|rfl,
{ simpa using h.symm, },
{ replace h : 2 * k = 2 * 3 := h.symm,
apply nat.eq_of_mul_eq_mul_left _ h,
exact (nat.succ_pos _), } } }
end


#### Johan Commelin (Aug 09 2019 at 11:11):

I'm quite satisfied with how this turned out

#### Johan Commelin (Aug 09 2019 at 11:11):

All the magic happens in apply constant_descent_vieta_jumping

#### Johan Commelin (Aug 09 2019 at 11:12):

Here's a gist with the full code: https://gist.github.com/jcommelin/619d66ccb3dcf534017051b0a1263f6f

#### Johan Commelin (Aug 09 2019 at 11:13):

I didn't try to golf, on purpose. I want to run this through Patrick's formatter now.

#### Johan Commelin (Aug 09 2019 at 11:14):

I hoped that omega would discharge some of the easier goals... but it didn't want to, see the other thread.

Last updated: May 14 2021 at 19:21 UTC