## Stream: general

### Topic: non-terminating theorem

#### Kevin Buzzard (Feb 06 2021 at 21:37):

Kenny raised the following question on the discord: if a,b,c are distinct positive integers and 1/a+1/b+1/c=1 then a+b+c is prime. I proved it, but my code didn't terminate even though it seemed to compile. I split my proof into two lemmas and they compile fine. But gluing them together gives me code for which the orange bars never go away. The profiler says that my lemma 1 takes about 7 seconds and lemma 2 about 11 seconds. The profiler says that the combination (the theorem) takes about 19 seconds but if I try to compile it in VS Code or on the command line then it never terminates. This is not a big deal, it's not blocking anything or anything, but it did strike me as odd. Is this sort of thing expected behaviour? I've never seen something like it before.

import data.nat.prime
import tactic

open nat

lemma lemma1 (a b c : ℕ)
(hapos : 0 < a) (hab : a < b) (hbc : b < c)
(h : (a : ℚ)⁻¹ + b⁻¹ + c⁻¹ = 1) :
prime (a + b + c) :=
begin
-- 0 < a so 1 ≤ a
have ha : 1 ≤ a, rwa succ_le_iff, clear hapos,
-- a < b so 2 ≤ b
have hb : 2 ≤ b,
{ cases b, linarith, cases b, linarith, dec_trivial },
-- b < c so 3 ≤ c,
have hc : 3 ≤ c,
{ cases c, linarith, cases c, linarith, cases c, linarith, dec_trivial },
-- clearly b⁻¹ > 0
have hb2 : 0 < (b : ℚ)⁻¹,
-- because b > 0
rw inv_pos, norm_cast, linarith,
-- and clearly c⁻¹ > 0
have hc2 : 0 < (c : ℚ)⁻¹,
-- because c > 0
rw inv_pos, norm_cast, linarith,
-- so a had better not be 1
rw le_iff_eq_or_lt at ha, cases ha,
exfalso, subst ha, simp at h, linarith,
-- So a ≥ 2
rw ← succ_le_iff at ha, change 2 ≤ a at ha,
--Now I claim that in fact a has to be 2
rw le_iff_lt_or_eq at ha, cases ha,
-- because if a > 2 then a >= 3
{ rw ← succ_le_iff at ha, change 3 ≤ a at ha,
-- so b ≥ 4 and c ≥ 5
have hb : 4 ≤ b, linarith,
have hc : 5 ≤ c, linarith,
-- so a⁻¹ + b⁻¹ + c⁻¹ ≤ 1/3+1/4+1/5<1 contradiction
have ha' : (a : ℚ)⁻¹ ≤ 3⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hb' : (b : ℚ)⁻¹ ≤ 4⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hc' : (c : ℚ)⁻¹ ≤ 5⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have : (3 : ℚ)⁻¹ + 4⁻¹ + 5⁻¹ < 1, norm_num,
linarith },
subst ha,
-- We know b ≥ 3
rw ← succ_le_iff at hab, change 3 ≤ b at hab,
-- and now I claim b = 3
rw le_iff_lt_or_eq at hab, cases hab,
-- because if b > 3 then b >= 4
{ rw ← succ_le_iff at hab, change 4 ≤ b at hab,
-- so and c ≥ 5
have hc : 5 ≤ c, linarith,
-- so a⁻¹ + b⁻¹ + c⁻¹ ≤ 1/2+1/4+1/5<1 contradiction
have hb' : (b : ℚ)⁻¹ ≤ 4⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hc' : (c : ℚ)⁻¹ ≤ 5⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have : (2 : ℚ)⁻¹ + 4⁻¹ + 5⁻¹ < 1, norm_num,
norm_cast at h,
linarith },
subst hab,
-- hence c⁻¹ must be 1/6,
have hc' : (c : ℚ)⁻¹ = 6⁻¹,
suffices : (c : ℚ)⁻¹ = 1 - (2⁻¹ + 3⁻¹),
convert this,
norm_cast at h,
-- so c = 6
rw inv_inj' at hc',
norm_cast at hc',
subst hc',
-- and 11 is prime
norm_num,
end

lemma lemma2 (a b c : ℕ)
(hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a)
(hapos : 0 < a) (hbpos : 0 < b) (hcpos : 0 < c)
(h : (a : ℚ)⁻¹ + b⁻¹ + c⁻¹ = 1) :
prime (a + b + c) :=
begin
wlog habc : a < b ∧ b < c using [a b c, a c b, b a c, b c a, c a b, c b a],
{ have := lt_trichotomy a b,
have := lt_trichotomy b c,
have := lt_trichotomy c a,
tauto },
exact lemma1 a b c hapos habc.1 habc.2 h,
end

-- direct glue never terminates though

theorem theorem1 (a b c : ℕ)
(hab : a ≠ b) (hbc : b ≠ c) (hca : c ≠ a)
(hapos : 0 < a) (hbpos : 0 < b) (hcpos : 0 < c)
(h : (a : ℚ)⁻¹ + b⁻¹ + c⁻¹ = 1) :
prime (a + b + c) :=
begin
wlog habc : a < b ∧ b < c using [a b c, a c b, b a c, b c a, c a b, c b a],
{ have := lt_trichotomy a b,
have := lt_trichotomy b c,
have := lt_trichotomy c a,
tauto },
clear hab hbc,
cases habc with hab hbc,
-- 0 < a so 1 ≤ a
have ha : 1 ≤ a, rwa succ_le_iff, clear hapos,
-- a < b so 2 ≤ b
clear hbpos, have hb : 2 ≤ b,
{ cases b, linarith, cases b, linarith, dec_trivial },
-- b < c so 3 ≤ c,
clear hcpos, have hc : 3 ≤ c,
{ cases c, linarith, cases c, linarith, cases c, linarith, dec_trivial },
-- clearly b⁻¹ > 0
have hb2 : 0 < (b : ℚ)⁻¹,
-- because b > 0
rw inv_pos, norm_cast, linarith,
-- and clearly c⁻¹ > 0
have hc2 : 0 < (c : ℚ)⁻¹,
-- because c > 0
rw inv_pos, norm_cast, linarith,
-- so a had better not be 1
rw le_iff_eq_or_lt at ha, cases ha,
exfalso, subst ha, simp at h, linarith,
-- So a ≥ 2
rw ← succ_le_iff at ha, change 2 ≤ a at ha,
--Now I claim that in fact a has to be 2
rw le_iff_lt_or_eq at ha, cases ha,
-- because if a > 2 then a >= 3
{ rw ← succ_le_iff at ha, change 3 ≤ a at ha,
-- so b ≥ 4 and c ≥ 5
have hb : 4 ≤ b, linarith,
have hc : 5 ≤ c, linarith,
-- so a⁻¹ + b⁻¹ + c⁻¹ ≤ 1/3+1/4+1/5<1 contradiction
have ha' : (a : ℚ)⁻¹ ≤ 3⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hb' : (b : ℚ)⁻¹ ≤ 4⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hc' : (c : ℚ)⁻¹ ≤ 5⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have : (3 : ℚ)⁻¹ + 4⁻¹ + 5⁻¹ < 1, norm_num,
linarith },
subst ha,
-- We know b ≥ 3
rw ← succ_le_iff at hab, change 3 ≤ b at hab,
-- and now I claim b = 3
rw le_iff_lt_or_eq at hab, cases hab,
-- because if b > 3 then b >= 4
{ rw ← succ_le_iff at hab, change 4 ≤ b at hab,
-- so and c ≥ 5
have hc : 5 ≤ c, linarith,
-- so a⁻¹ + b⁻¹ + c⁻¹ ≤ 1/2+1/4+1/5<1 contradiction
have hb' : (b : ℚ)⁻¹ ≤ 4⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have hc' : (c : ℚ)⁻¹ ≤ 5⁻¹, rw inv_le_inv, norm_cast, linarith, norm_cast, linarith, linarith,
have : (2 : ℚ)⁻¹ + 4⁻¹ + 5⁻¹ < 1, norm_num,
norm_cast at h,
linarith },
subst hab,
-- hence c⁻¹ must be 1/6,
have hc' : (c : ℚ)⁻¹ = 6⁻¹,
suffices : (c : ℚ)⁻¹ = 1 - (2⁻¹ + 3⁻¹),
convert this,
norm_cast at h,
-- so c = 6
rw inv_inj' at hc',
norm_cast at hc',
subst hc',
-- and 11 is prime
norm_num,
end


#### Johan Commelin (Feb 06 2021 at 21:58):

Now find solutions to 1/p + 1/q + 1/r < 1 (-; We'll need that when we do the classification of root systems.

#### Kevin Buzzard (Feb 06 2021 at 22:11):

And then for each one, prove the number of solutions to a^p+b^q=c^r for positive coprime a,b,c is finite!

#### Johan Commelin (Feb 08 2021 at 10:44):

Why does this not work :sad:

import data.pnat.basic

example : ∀ {p : ℕ+}, p < 3 → p = 1 ∨ p = 2 :=
begin
dec_trivial -- fails
end


#### Johan Commelin (Feb 08 2021 at 11:13):

3 sorrys left, related to the example above :up:

import data.multiset.sort
import data.pnat.basic
import data.rat.order

import tactic.norm_num
import tactic.field_simp
import tactic.fin_cases

namespace pqr

open multiset

def A' (p q : ℕ+) : multiset ℕ+ := {1,p,q}
def A  (n   : ℕ+) : multiset ℕ+ := A' 1 n
def D' (n   : ℕ+) : multiset ℕ+ := {2,2,n}
def E' (n   : ℕ+) : multiset ℕ+ := {2,3,n}
def E6            : multiset ℕ+ := E' 3
def E7            : multiset ℕ+ := E' 4
def E8            : multiset ℕ+ := E' 5

def sum_inv (pqr : multiset ℕ+) : ℚ :=
multiset.sum $pqr.map$ λ x, x⁻¹

lemma sum_inv_pqr (p q r : ℕ+) : sum_inv {p,q,r} = p⁻¹ + q⁻¹ + r⁻¹ :=
singleton_eq_singleton, map_cons, sum_cons, map_zero, sum_zero]

def admissible (pqr : multiset ℕ+) : Prop :=
(∃ p q, A' p q = pqr) ∨ (∃ n, D' n = pqr) ∨ (E' 3 = pqr ∨ E' 4 = pqr ∨ E' 5 = pqr)

lemma admissible.one_lt_sum_inv {pqr : multiset ℕ+} :
admissible pqr → 1 < sum_inv pqr :=
begin
rintro (⟨p', q', H⟩|⟨n, H⟩|H|H|H),
{ rw [← H, A', sum_inv_pqr, add_assoc],
simp only [lt_add_iff_pos_right, pnat.one_coe, inv_one, nat.cast_one, coe_coe],
apply add_pos; simp only [pnat.pos, nat.cast_pos, inv_pos] },
{ rw [← H, D', sum_inv_pqr],
simp only [lt_add_iff_pos_right, pnat.one_coe, inv_one, nat.cast_one,
coe_coe, pnat.coe_bit0, nat.cast_bit0],
norm_num },
all_goals { rw [← H, E', sum_inv_pqr], norm_num }
end

lemma lt_three {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r) (H : 1 < sum_inv {p, q, r}) :
p < 3 :=
begin
have h3 : (0:ℚ) < 3, by norm_num,
contrapose! H, rw sum_inv_pqr,
have h3q := H.trans hpq,
have h3r := h3q.trans hqr,
... = 1 : by norm_num,
all_goals { rw inv_le_inv _ h3; [assumption_mod_cast, norm_num] }
end

lemma lt_four {q r : ℕ+} (h2q : 2 ≤ q) (hqr : q ≤ r) (H : 1 < sum_inv {2, q, r}) :
q < 4 :=
begin
have h4 : (0:ℚ) < 4, by norm_num,
contrapose! H, rw sum_inv_pqr,
have h4r := H.trans hqr,
... = 1 : by norm_num,
all_goals { rw inv_le_inv _ h4; [assumption_mod_cast, norm_num] }
end

lemma lt_six {r : ℕ+} (h3r : 3 ≤ r) (H : 1 < sum_inv {2, 3, r}) :
r < 6 :=
begin
have h6 : (0:ℚ) < 6, by norm_num,
contrapose! H, rw sum_inv_pqr,
... = 1 : by norm_num,
rw inv_le_inv _ h6; [assumption_mod_cast, norm_num]
end

lemma admissible_of_one_lt_sum_inv_aux' {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r)
(H : 1 < sum_inv {p,q,r}) :
begin
have hp3 : p < 3 := lt_three hpq hqr H,
obtain (rfl|rfl) : p = 1 ∨ p = 2, { sorry },
{ /- case A -/ left, exact ⟨q, r, rfl⟩ },
clear hp3,
have hq4 : q < 4 := lt_four hpq hqr H,
obtain (rfl|rfl) : q = 2 ∨ q = 3, { sorry },
{ /- case D -/ right, left, exact ⟨r, rfl⟩ },
have hr6 : r < 6 := lt_six hqr H,
obtain (rfl|rfl|rfl) : r = 3 ∨ r = 4 ∨ r = 5, { sorry },
{ /- case E6 -/ right, right, left, refl },
{ /- case E7 -/ right, right, right, left, refl },
{ /- case E8 -/ right, right, right, right, refl }
end

∀ {pqr : list ℕ+} (hs : pqr.sorted (≤)) (hl : pqr.length = 3) (H : 1 < sum_inv pqr),
| [p,q,r] hs hl H :=
begin
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r,
simpa using hs,
end

lemma admissible_of_one_lt_sum_inv {p q r : ℕ+} (H : 1 < sum_inv {p,q,r}) :
begin
let S := sort ((≤) : ℕ+ → ℕ+ → Prop) {p,q,r},
have hS : S.sorted (≤) := sort_sorted _ _,
have hpqr : ({p,q,r} : multiset ℕ+) = S := (sort_eq has_le.le {p, q, r}).symm,
simp only [hpqr] at *,
simp only [singleton_eq_singleton, length_sort, insert_eq_cons, card_singleton,
card_cons, card_zero],
end

lemma classification (p q r : ℕ+) :
1 < sum_inv {p,q,r} ↔ admissible {p,q,r} :=

end pqr


#### Johan Commelin (Feb 08 2021 at 11:17):

I pushed this to branch#pqr

#### Johan Commelin (Feb 08 2021 at 12:11):

I have no idea what puzzle piece is missing to make dec_trivial work. Do we need something like decidable_lt? That's probably not enough, is it?

#### Johan Commelin (Feb 08 2021 at 12:14):

lemma admissible_of_one_lt_sum_inv_aux' {p q r : ℕ+} (hpq : p ≤ q) (hqr : q ≤ r)
(H : 1 < sum_inv {p,q,r}) :
begin
have hp3 : p < 3 := lt_three hpq hqr H,
interval_cases p,
{ /- case A -/ left, exact ⟨q, r, rfl⟩ },
clear hp3,
have hq4 : q < 4 := lt_four hpq hqr H,
interval_cases q,
{ /- case D -/ right, left, exact ⟨r, rfl⟩ },
have hr6 : r < 6 := lt_six hqr H,
interval_cases r,
{ /- case E6 -/ right, right, left, refl },
{ /- case E7 -/ right, right, right, left, refl },
{ /- case E8 -/ right, right, right, right, refl }
end


#### Johan Commelin (Feb 08 2021 at 12:14):

The right solution is to look for a different tactic :laughing: interval_cases ftw

#### Kevin Buzzard (Feb 08 2021 at 12:26):

But still someone will hopefully come along and explain why it doesn't work. There is just some missing instance, right?

import data.pnat.basic
import tactic

instance : decidable (∀ {p : ℕ+}, p < 3 → p = 1 ∨ p = 2) :=
is_true begin
rintro ⟨p, hp⟩ h3,
change (p < 3) at h3,
interval_cases p;
dec_trivial,
end

example : ∀ {p : ℕ+}, p < 3 → p = 1 ∨ p = 2 :=
begin
dec_trivial -- works
end


FTFY

#### Kevin Buzzard (Feb 08 2021 at 12:27):

Looks like there's missing stuff on pnat but it's there for nat.

#### Johan Commelin (Feb 08 2021 at 12:29):

I pushed updates to branch#pqr. I'm reasonably happy with what this looks like. Except that I don't know how to name things. I've just dumped everything in the pqr namespace. Does this inequality have some name?

#### Johan Commelin (Feb 08 2021 at 12:29):

I think this should go in mathlib, we'll have applications for it in the (near, I hope) future.

#### Floris van Doorn (Feb 08 2021 at 16:22):

For dec_trivial to work, the missing piece is the analogue of docs#nat.decidable_ball_lt for pnat. But interval_cases might be better, as you found.

Last updated: May 17 2021 at 23:14 UTC