# Zulip Chat Archive

## 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,
-- because then 1/a+1/b+1/c>1, contradiction
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,
exact eq_sub_of_add_eq' 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,
-- because then 1/a+1/b+1/c>1, contradiction
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,
exact eq_sub_of_add_eq' 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 `sorry`

s 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⁻¹ :=
by simp only [sum_inv, map_congr, coe_coe, add_zero, insert_eq_cons, add_assoc,
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
rw [admissible],
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,
calc (p⁻¹ + q⁻¹ + r⁻¹ : ℚ) ≤ 3⁻¹ + 3⁻¹ + 3⁻¹ : add_le_add (add_le_add _ _) _
... = 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,
calc (2⁻¹ + q⁻¹ + r⁻¹ : ℚ) ≤ 2⁻¹ + 4⁻¹ + 4⁻¹ : add_le_add (add_le_add le_rfl _) _
... = 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,
calc (2⁻¹ + 3⁻¹ + r⁻¹ : ℚ) ≤ 2⁻¹ + 3⁻¹ + 6⁻¹ : add_le_add (add_le_add le_rfl le_rfl) _
... = 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}) :
admissible {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
lemma admissible_of_one_lt_sum_inv_aux :
∀ {pqr : list ℕ+} (hs : pqr.sorted (≤)) (hl : pqr.length = 3) (H : 1 < sum_inv pqr),
admissible pqr
| [p,q,r] hs hl H :=
begin
obtain ⟨⟨hpq, -⟩, hqr⟩ : (p ≤ q ∧ p ≤ r) ∧ q ≤ r,
simpa using hs,
exact admissible_of_one_lt_sum_inv_aux' hpq hqr H,
end
lemma admissible_of_one_lt_sum_inv {p q r : ℕ+} (H : 1 < sum_inv {p,q,r}) :
admissible {p,q,r} :=
begin
simp only [admissible],
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 *,
apply admissible_of_one_lt_sum_inv_aux hS _ H,
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} :=
⟨admissible_of_one_lt_sum_inv, admissible.one_lt_sum_inv⟩
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}) :
admissible {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