non-terminating theorem

Stream: general

[Kevin Buzzard]

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]

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]

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]

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]

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⁻¹ :=
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]

I pushed this to branch#pqr

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Floris van Doorn]

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.