Zulip Chat Archive

Stream: new members

Topic: Divisibility Argument


view this post on Zulip Shing Tak Lam (Feb 27 2020 at 11:15):

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,

view this post on Zulip Kenny Lau (Feb 27 2020 at 11:41):

do you mean 3 \| n^2?

view this post on Zulip Kenny Lau (Feb 27 2020 at 11:42):

you can use % (nat.mod)

view this post on Zulip Shing Tak Lam (Feb 27 2020 at 11:58):

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?

view this post on Zulip Shing Tak Lam (Feb 27 2020 at 12:00):

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

view this post on Zulip Shing Tak Lam (Feb 27 2020 at 13:07):

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.

view this post on Zulip Anne Baanen (Feb 27 2020 at 13:09):

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

view this post on Zulip Shing Tak Lam (Feb 27 2020 at 13:14):

Alright. Thank you very much.

view this post on Zulip Kevin Buzzard (Feb 27 2020 at 16:16):

@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.

view this post on Zulip Kenny Lau (Feb 27 2020 at 16:27):

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

view this post on Zulip Kenny Lau (Feb 27 2020 at 16:27):

Cunningham's Law is in full effect

view this post on Zulip Shing Tak Lam (Feb 28 2020 at 01:30):

@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.

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 08:02):

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...)

view this post on Zulip Patrick Massot (Feb 28 2020 at 08:33):

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.

view this post on Zulip Shing Tak Lam (Feb 28 2020 at 08:33):

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)?)

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:02):

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)

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:04):

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)

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 09:09):

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.

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:10):

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

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:11):

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

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:12):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 09:12):

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.

view this post on Zulip Mario Carneiro (Feb 28 2020 at 09:13):

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

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 09:13):

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.

view this post on Zulip Kevin Buzzard (Feb 28 2020 at 09:14):

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.


Last updated: May 12 2021 at 03:23 UTC