Divisibility Argument

Stream: new members

[Shing Tak Lam]

Say I wanted to prove n^2 ∣ 3 -> n ∣ 3,

what I'd do would be to intro h, giving me h : n^2 ∣ 3 and requiring me to prove n ∣ 3. The way I'd do it would be by contradiction, (say n = 3*m + 1 and n = 3*m + 2), then rw at h and reaching a contradiction.

However I'm not sure how I can generate those cases in Lean, ie ¬n ∣ 3 -> ∃ m, n = 3*m + 1 ∨ n = 3*m + 2. I could define that as a lemma but then I don't know how to prove it.

(Should it be ∃ m, n = 3*m + 1 ∨ n = 3*m + 2 or (∃ m, n = 3*m + 1) ∨ (∃ m, n = 3*m + 2)?)

Also how do you enter ∣ in VSCode, since it's not |, and I've just been copy and pasting it.

(Also if there is a more straightforward way to prove the original statement that'd be welcome as well. I'm still in Sixth Form so I haven't properly done any University Mathematics before)

Thank you,

[Kenny Lau]

do you mean 3 \| n^2?

[Kenny Lau]

you can use % (nat.mod)

[Shing Tak Lam]

Yes. Apologies I do mean 3 \| n^2.

I'm not sure what you mean about using % here, do you mean to use n^2 % 3 == 0 instead of 3 \| n^2?

[Shing Tak Lam]

Also, does Ctrl-P # only search in files that have been imported? or is it all of mathlib?

[Shing Tak Lam]

Ok, so I have the proof complete except one thing, which is that I can't seem to find any definitions that can prove 1 < 3.

[Anne Baanen]

If tactics are also ok, then by norm_num is perfect for this

[Shing Tak Lam]

Alright. Thank you very much.

[Kevin Buzzard]

@Shing Tak Lam Here's my attempt at your question (I put in lots of comments so it looks longer than it could be):

import tactic

open nat

example (n : ℕ) (hn2 : 3 ∣ n^2) : 3 ∣ n :=
begin
  -- Let q be floor of n/3 and let r be the remainder when dividing n by 3
  set q := n / 3 with hq,
  set r := n % 3 with hr,
  -- Then n=3q+r
  have hn : r + 3 * q = n,
    rw [hr, hq, mod_add_div],
  -- and r<3
  have hr3 : r < 3,
    rw hr,
    apply mod_lt,
    norm_num,
  -- There are only three cases for r so let's split into those cases.
  set i : fin 3 := ⟨r, hr3⟩ with hi,
  fin_cases i; rw hi at h; replace h := (fin.ext_iff _ _).1 h; dsimp at h; rw h at hn,
  { -- First r = 0
    -- In this case n is a multiple of 3 because it's 3q
    use q,
    rw ←hn,
    simp,
  },
  { -- Next r = 1
    -- I claim this contradicts 3|n^2
    exfalso,
    -- because here 3 | 1+3(2q+3q^2)
    have hbad : 3 ∣ 1 + 3*(2*q+3*q^2),
      convert hn2,
      rw ←hn,
      ring,
    -- and hence 1 mod 3 = 0
    rw [dvd_iff_mod_eq_zero, add_mul_mod_self_left, mod_eq_of_lt] at hbad,
    -- which is nonsense
    cases hbad, norm_num,
  },
  { -- Finally r = 2; the argument is pretty much the same
    exfalso,
    have hbad : 3 ∣ 1 + 3 * (1 + 4 * q + 3 * q ^ 2),
      convert hn2, rw ←hn, ring,
    rw [dvd_iff_mod_eq_zero, add_mul_mod_self_left, mod_eq_of_lt] at hbad,
    cases hbad, norm_num,
  }
end

When I was a beginner I also wrote a proof of this result: you can still see it here. It's nice to see that I've got a bit better since then; that was just over 2 years ago. When I had finished I proved that no rational number squared was 3, and then I looked at the Lean term I had generated using the #print command. I emailed the resulting text file to my son who imported it into blender, coloured it and twisted it around a lot, and we sent the result to the London Mathematical Society who put it on the front page of their newsletter here.

[Kenny Lau]

import data.zmod.basic

example (n : ℕ) (h : 3 ∣ n * n) : 3 ∣ n :=
begin
  have : nat.prime 3, norm_num,
  rw ← zmodp.eq_zero_iff_dvd_nat this at h ⊢,
  rwa [nat.cast_mul, mul_self_eq_zero] at h
end

[Kenny Lau]

Cunningham's Law is in full effect

[Shing Tak Lam]

@Kevin Buzzard

That's great. Mine is much longer than yours (around 100 lines!), but it's nice to see the different approaches and the mistakes (I suppose you can call them that) I made along the way.

• I didn't know set ... := ..., so my goal was full of (n / 3). This sucked for readability, but the result was the same.
• I didn't know about fin and fin_cases, so I wrote my own lemmas that did n % 3 = 0 ∨ n % 3 = 1 ∨ n % 3 = 2.
• In retrospect, using cases made more sense than what I did, which was proof by contradiction from the beginning (although this is what I would do if I was doing this on paper). So I wrote a lemma that gave me n % 3 ≠ 0 -> n % 3 = 1 ∨ n % 3 = 2 and then cases on that by getting 1 = 0 in two separate goals.
• I tried to expand (3*m + 1) and (3*m + 2) to get it in the form 3*k + 1(for some k), which took a lot of rws (12 for 3*m+1, 18 for 3*m + 2), which once again, in retrospect is not the simplest route to take.
• I guess this is more down to my lack of familiarity with University Maths (the little time that I had to explore Maths is now taken up by revision for my A Levels), but I replaced all n ∣ m with m % n = 0, where I was more familiar with % due to the programming that I've done before.

I guess these are all beginner mistakes, and more practice would be better, and hopefully I'd be better at actually doing proofs when I start uni at October, which would hopefully translate into better Lean.

[Kevin Buzzard]

Kenny's approach uses the full force of uniqueness of factorization of integers into primes, that's why it looks so much shorter (it imports so much more -- once you know that p divides ab implies p divides a or p divides b then your problem becomes easy, but the usual proof of this uses Euclid's algorithm etc). The ring tactic will do all the expanding out stuff for you.

Finally, there is not really any correlation between better Lean code and more maths knowledge, you can goof around with Lean in your spare time after A-levels in July and this will teach you far more about Lean than any maths degree will (although hopefully next year I'll be teaching a Lean course as part of Imperial's curriculum...)

[Patrick Massot]

Kevin, I don't think your account of Kenny's proof is accurate. What he uses is Z/p is a domain when p is prime. This has nothing to do with uniqueness of factorization. And he could have done in two lines instead of three by putting the (by norm_num : nat.prime 3) instead of this in the second line.

[Shing Tak Lam]

Thanks a lot. My point about Maths knowledge was referring to me not even knowing the definitions at the moment, so learning the Maths would be useful to know what I should be looking at in the first place. And what to Ctrl-P for. I guess it's like programming, where knowing what to search for is half the struggle (for me at least). It's a bit hard for me right now if I don't know what to search for.

( Part about Imperial sounds great. You're seriously tempting me to firm Imperial :) Do you know if Lean is offered at any other Universities (UK)?)

[Mario Carneiro]

Oh, I hadn't looked closely and thought Kenny gave the Euclid's lemma argument, which is definitely the easiest:

import data.nat.prime

example (n : ℕ) (h : 3 ∣ n * n) : 3 ∣ n :=
have nat.prime 3, from @of_as_true _ (nat.decidable_prime_1 3) ⟨⟩,
(or_self _).1 ((nat.prime.dvd_mul this).1 h)

[Mario Carneiro]

golfed with norm_num:

import tactic.norm_num

example (n : ℕ) (h : 3 ∣ n * n) : 3 ∣ n :=
(or_self _).1 ((nat.prime.dvd_mul (by norm_num : nat.prime 3)).1 h)

[Kevin Buzzard]

What he uses is that Z/p is a domain when p is prime, which is the statement that if p divides ab then p divides a or p divides b. You're right it's not 100% the full force of uniqueness of factorization, but this is the key lemma which makes uniqueness of factorization easy by induction.

[Mario Carneiro]

I don't think the proof of Euclid's lemma in mathlib is at all high powered

[Mario Carneiro]

you need to know that prime.coprime_iff_not_dvd but this is more or less true by the definitions

[Mario Carneiro]

oh but coprime.dvd_of_dvd_mul_left relies on dvd_gcd which is basically the euclidean algorithm proof

[Kevin Buzzard]

Is Euclid's Lemma this p|ab implies p|a or p|b statement? This lemma is exactly the door to uniqueness of factorization. If you ask a new undergrad to prove uniqueness of factorization they usually reduce it easily to this statement, but then they claim this statement is obvious because p is prime and when you press them for details they use uniqueness of factorization. Euclid's Lemma needs an idea.

[Mario Carneiro]

I am willing to grant that dvd_gcd, or the existence of the gcd in general, is nontrivial

[Kevin Buzzard]

I usually explain to them that the assertion that p is prime is an assertion about all the numbers less than p (they don't divide p), so perhaps it isn't obvious that if p divides the product of two numbers much larger than p then it divides one of them. Prime iff irreducible isn't true in an arbitrary integral domain, this is somehow where the tension is.

[Kevin Buzzard]

Interestingly, I do know a direct proof of p|ab implies p|a or p|b by induction, which doesn't use Euclid, but it also relies on an idea.