Help with an arithmetic lemma

Stream: mathlib4

[ElCondor]

I'm trying to formulate and prove a lemma, as part of a bigger theorem.

My lemma is that if p and q are prime numbers and m < p*q is a natural number not coprime with p*q, then there exists natural integers k > 0 and M such that m = p^k * M (or same with q) and Mis coprime with p * q.

I think I wrote it correctly (although I'm open to suggestions to write it in a more efficient/concise way):

lemma mylemma {p q m k M : ℕ}
    (hp : p.Prime) (hq : q.Prime) (hmgt : 0 < m) (hmlt : m < p * q) (hmpq : ¬Coprime m (p * q)) :
    ∃ k M, k > 0 ∧ Coprime M (p * q) ∧ (m = p^k * M ∨ m = q^k * M) := by sorry

This theorem seems obvious to me but I have no idea how to prove it using the results and tactics available in mathlib.

Would you have some suggestion?

[Junyan Xu]

If m = q then you shouldn't be able to extract factor(s) of p from it? (if p and q are distinct)

[ElCondor]

Junyan Xu said:

If m = q then you shouldn't be able to extract factor(s) of p from it? (if p and q are distinct)

Yes I updated it to add "(or same with q)" (I believe the signature of the lemma below is correct though).

[Yongyi Chen]

This needs another hypothesis m > 0.

[Kevin Buzzard]

ElCondor said:

This theorem seems obvious to me but I have no idea how to prove it using the results and tactics available in mathlib.

Would you have some suggestion?

My first suggestion would be to first write down a careful mathematics proof; "it's obvious" is not mathematics. Once we have a maths proof to work on, we can think about how to translate it into Lean.

[ElCondor]

Yongyi Chen said:

This needs another hypothesis m > 0.

Of course! I forgot to add it in my lemma, but I had it in as an hypothesis
in my theorem... (I updated the signature)

[Yongyi Chen]

Here's something I made to get you started.

import Mathlib

def p_part (p x : ℕ) [Fact (p.Prime)] := p ^ padicValNat p x

lemma not_dvd_of_padicValNat_zero (p x : ℕ) [hp : Fact (p.Prime)] (h : padicValNat p x = 0) (x_ne_zero : x ≠ 0) : ¬p ∣ x := by
  simp_all only [padicValNat.eq_zero_iff, Nat.isUnit_iff, false_or, ne_eq, x_ne_zero]
  rcases h with (h₁ | h₂)
  . simp only [h₁] at hp; exact hp.out.elim
  . trivial

lemma ne_zero_of_div_of_dvd {x y : ℕ} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : y ∣ x) : x / y ≠ 0 := by
  obtain ⟨k, rfl⟩ := hxy
  rw [mul_comm, Nat.mul_div_assoc _ (show y ∣ y by trivial), Nat.div_self (Nat.pos_of_ne_zero hy)]
  simp_all only [ne_eq, mul_eq_zero, false_or, mul_one, not_false_eq_true]

lemma not_dvd_of_div_p_part (p x : ℕ) [hp : Fact (p.Prime)] (x_ne_zero : x ≠ 0) : ¬p ∣ (x / p_part p x) := by
  have p_ne_one : p ≠ 1 := by intro h; simp [h] at hp; exact hp.out.elim
  have p_part_dvd : p_part p x ∣ x := pow_padicValNat_dvd
  have : x / p_part p x ≠ 0 := ne_zero_of_div_of_dvd x_ne_zero (NeZero.ne (p ^ padicValNat p x)) p_part_dvd
  suffices padicValNat p (x / p_part p x) = 0 by
    simp_all only [ne_eq, Nat.isUnit_iff, padicValNat.eq_zero_iff, Nat.dvd_div_iff, IsUnit.mul_iff, and_false, false_or, not_false_eq_true, p_part_dvd]
  calc
    padicValNat p (x / p_part p x) = padicValNat p x - padicValNat p (p_part p x) := padicValNat.div_of_dvd pow_padicValNat_dvd
    _ = padicValNat p x - padicValNat p x := by simp only [p_part, padicValNat.prime_pow, le_refl, tsub_eq_zero_of_le]
    _ = 0 := Nat.sub_self _

lemma mylemma {p q m : ℕ} [pp : Fact p.Prime] [pq : Fact q.Prime] (mpos : m > 0) (hm : m < p * q) (hmpq : ¬m.Coprime (p * q)) : ∃ k M, k > 0 ∧ M.Coprime (p * q) ∧ (m = p^k * M ∨ m = q^k * M) := by
  simp_all only [ne_eq, gt_iff_lt, exists_and_left]
  by_cases hpq : p = q
  . subst hpq
    sorry
  push_neg at hpq
  have pq_coprime : p.Coprime q := Nat.coprime_primes pp.out pq.out |>.mpr hpq
  by_cases hpm : p ∣ m <;> by_cases hqm : q ∣ m
  . have : p * q ∣ m := pq_coprime.mul_dvd_of_dvd_of_dvd hpm hqm
    have : p * q ≤ m := Nat.le_of_dvd mpos this
    rw [← not_le] at hm
    exact (hm this).elim
  . sorry
  . sorry
  . contrapose! hmpq
    rw [Nat.Coprime.gcd_mul m pq_coprime, mul_eq_one]
    exact ⟨pp.out.coprime_iff_not_dvd.mpr hpm |>.symm, pq.out.coprime_iff_not_dvd.mpr hqm |>.symm⟩

[ElCondor]

@Kevin Buzzard

My first suggestion would be to first write down a careful mathematics proof; "it's obvious" is not mathematics. Once we have a maths proof to work on, we can think about how to translate it into Lean.

Mathematically, my proof would be the following:

1. m is not coprime with p * q (by hmpq) so m and p * q share a common prime divisor, invoking the fundamental theorem of arithmetic (FTA)
2. p and q are primes (hp and hq) so this divisor can be taken to be either p or q : let's say it's p (the other case is symmetric)
3. Applying the FTA to m (because of hmgt : 0 < m), consider k > 0 the multiplicity of p and M the product (defaulting to 1) of all the primes different from k with their multiplicities.
4. By the FTA, we have m = p^k * M and by construction p is not a divisor of M
5. By hmlt, if qdiffers from pit cannot be a divisor of Meither because otherwise m >= p * q (contradiction)
6. Using FTA again, we see that M and p * q are coprime, which completes the result.

So I guess I should try and find a way to implement all these steps in Lean. Also, I don't know what would be the best way to formulate the " let's say it's p (the other case is symmetric)" argument in (2) so that I don't duplicate the cases in Lean.

@Yongyi Chen thanks I will also have a look at your proposal.

[Kevin Buzzard]

Yeah, that's the proof I was thinking of and right now that's the kind of thing you have to do step by step in a formalisation system. The only step which I wouldn't be able to immediately start formalising is step 2, because for lean's WLOG tactic to work you might need to isolate a precise symmetric statement which implies the theorem.

[Patrick Massot]

ElCondor, it seems you are well on your way to appreciate formalized math, going from "This theorem seems obvious to me" to: "Actually it misses two assumptions and the proof has six steps" in less than six hours :wink:

[ElCondor]

Patrick Massot said:

ElCondor, it seems you are well on your way to appreciate formalized math, going from "This theorem seems obvious to me" to: "Actually it misses two assumptions and the proof has six steps" in less than six hours :wink:

You know, I feel a bit like if I was writing assembly code before people invented programming languages.
I guess the analogy is that the programming language will be something (better tactics, GPT-things) writing part of the proofs for us?

[Kevin Buzzard]

With my number theory hat on I totally agree that your lemma is mathematically trivial. With my formalisation hat on I can see all the problems. With my optimist's hat on I hope that one day GPT-things or maybe just good-old-fashioned-AI things will be able to turn the obvious sketch into Lean code. With my realists hat on, well, that's why I asked you to spell out the argument, because that's where we are right now.

[Henrik Böving]

What's the difference between GPT things and old fashioned AI? Or do you mean old fashioned AI in the sense of automated reasoning procedures?

[Johan Commelin]

See e.g. https://gowers.wordpress.com/2022/04/28/announcing-an-automatic-theorem-proving-project/

[Kevin Buzzard]

By GOFAI I meant "stuff like aesop": you spell out the statements of the six steps in Lean and then some tactic just finds the proofs for you.

[Yaël Dillies]

Kevin Buzzard said:

for lean's WLOG tactic to work you might need to isolate a precise symmetric statement which implies the theorem.

I think wlog p ∣ m generalizing p q should do exactly what @ElCondor wants.

[ElCondor]

Mathematically, my proof would be the following:

1. m is not coprime with p * q (by hmpq) so m and p * q share a common prime divisor, invoking the fundamental theorem of arithmetic (FTA)

I'm finding it very hard to even write this first step, because the way theorems about Nat are formulated there is not much that I can do with a negated hypothesis ¬Coprime m (p * q).

For instance, shouldn't the theorem coprime_factors_disjoint be formulated as an equivalence in PNat?

[Ruben Van de Velde]

I think I'd do it as follows:

1a. Their GCD is not equal to one or zero
1b. The GCD has a prime factor p
1c. p divides m and p*q

[Ruben Van de Velde]

You might put those substeps in an independent reusable lemma

[Yongyi Chen]

By the way, my code no longer compiles as is due to a simp change in Lean v4.3.0-rc2, but I also finished it shortly after writing up the skeleton. I didn't include the wlog strategy. Here's the finished code for you to play around with:

import Mathlib.NumberTheory.Padics.PadicVal

def pPart (p x : ℕ) [Fact p.Prime] := p ^ padicValNat p x

lemma not_dvd_of_padicValNat_zero (p x : ℕ) [hp : Fact (p.Prime)] (h : padicValNat p x = 0) (x_ne_zero : x ≠ 0) : ¬p ∣ x := by
  simp_all only [padicValNat.eq_zero_iff, Nat.isUnit_iff, false_or, ne_eq, x_ne_zero]
  rcases h with (h₁ | h₂)
  . simp only [h₁, Nat.not_prime_one] at hp; exact hp.out.elim
  . trivial

lemma ne_zero_of_div_of_dvd {x y : ℕ} (hx : x ≠ 0) (hy : y ≠ 0) (hxy : y ∣ x) : x / y ≠ 0 := by
  obtain ⟨k, rfl⟩ := hxy
  rw [mul_comm, Nat.mul_div_assoc _ (show y ∣ y by trivial), Nat.div_self (Nat.pos_of_ne_zero hy)]
  simp_all only [ne_eq, mul_eq_zero, false_or, mul_one, not_false_eq_true]

lemma not_dvd_of_div_pPart (p x : ℕ) [hp : Fact (p.Prime)] (x_ne_zero : x ≠ 0) : ¬p ∣ (x / pPart p x) := by
  have p_ne_one : p ≠ 1 := by intro h; simp only [h, Nat.not_prime_one] at hp; exact hp.out.elim
  have pPart_dvd : pPart p x ∣ x := pow_padicValNat_dvd
  have : x / pPart p x ≠ 0 := ne_zero_of_div_of_dvd x_ne_zero (NeZero.ne (p ^ padicValNat p x)) pPart_dvd
  suffices padicValNat p (x / pPart p x) = 0 by
    simp_all only [ne_eq, Nat.isUnit_iff, padicValNat.eq_zero_iff, Nat.dvd_div_iff, IsUnit.mul_iff, and_false, false_or, not_false_eq_true, pPart_dvd]
  calc
    padicValNat p (x / pPart p x) = padicValNat p x - padicValNat p (pPart p x) := padicValNat.div_of_dvd pow_padicValNat_dvd
    _ = padicValNat p x - padicValNat p x := by simp only [pPart, padicValNat.prime_pow, le_refl, tsub_eq_zero_of_le]
    _ = 0 := Nat.sub_self _

lemma eq_pkm_or_qkm_of_lt_and_coprime_p_times_q {p q m : ℕ} [pp : Fact p.Prime] [pq : Fact q.Prime] (mpos : m > 0) (hm : m < p * q) (hmpq : ¬m.Coprime (p * q)) : ∃ k M, k > 0 ∧ M.Coprime (p * q) ∧ (m = p^k * M ∨ m = q^k * M) := by
  simp_all only [ne_eq, gt_iff_lt, exists_and_left]
  by_cases hpq : p = q
  . subst hpq
    simp only [or_self]
    rw [← Nat.pow_two] at hmpq
    change ¬Nat.Coprime _ _ at hmpq
    simp [Nat.coprime_pow_right_iff (by trivial), Nat.coprime_comm, pp.out.coprime_iff_not_dvd] at hmpq
    use padicValNat p m, one_le_padicValNat_of_dvd mpos hmpq, m / pPart p m, ?_, ?_
    . simp [Nat.coprime_mul_iff_right]
      have := not_dvd_of_div_pPart p m (Nat.pos_iff_ne_zero.mp mpos)
      exact pp.out.coprime_iff_not_dvd.mpr this |>.symm
    . exact Nat.eq_mul_of_div_eq_right pow_padicValNat_dvd rfl
  push_neg at hpq
  have pq_coprime : p.Coprime q := Nat.coprime_primes pp.out pq.out |>.mpr hpq
  by_cases hpm : p ∣ m <;> by_cases hqm : q ∣ m
  . have : p * q ∣ m := pq_coprime.mul_dvd_of_dvd_of_dvd hpm hqm
    have : p * q ≤ m := Nat.le_of_dvd mpos this
    rw [← not_le] at hm
    exact (hm this).elim
  . use padicValNat p m, one_le_padicValNat_of_dvd mpos hpm, m / pPart p m, ?_, .inl ?_
    . rw [Nat.coprime_mul_iff_right]
      constructor
      . exact pp.out.coprime_iff_not_dvd.mpr (not_dvd_of_div_pPart p m (Nat.pos_iff_ne_zero.mp mpos)) |>.symm
      . apply Nat.Coprime.coprime_div_left _ pow_padicValNat_dvd
        exact pq.out.coprime_iff_not_dvd.mpr hqm |>.symm
    . exact Nat.eq_mul_of_div_eq_right pow_padicValNat_dvd rfl
  . use padicValNat q m, one_le_padicValNat_of_dvd mpos hqm, m / pPart q m, ?_, .inr ?_
    . rw [Nat.coprime_mul_iff_right]
      constructor
      . apply Nat.Coprime.coprime_div_left _ pow_padicValNat_dvd
        exact pp.out.coprime_iff_not_dvd.mpr hpm |>.symm
      . exact pq.out.coprime_iff_not_dvd.mpr (not_dvd_of_div_pPart q m (Nat.pos_iff_ne_zero.mp mpos)) |>.symm
    . exact Nat.eq_mul_of_div_eq_right pow_padicValNat_dvd rfl
  . contrapose! hmpq
    rw [Nat.Coprime.gcd_mul m pq_coprime, mul_eq_one]
    exact ⟨pp.out.coprime_iff_not_dvd.mpr hpm |>.symm, pq.out.coprime_iff_not_dvd.mpr hqm |>.symm⟩

[Ruben Van de Velde]

Most likely this is because simp no longer tries decide by default. Possibly just running that afterwards will work

[Yongyi Chen]

@Ruben Van de Velde I added Nat.not_prime_one to the simp list to get it to work. Unfortunately, since my simp was a simp [...] at hp, decide at hp is not a valid syntax so I couldn't use that strategy.