## Stream: new members

### Topic: Divisibility Argument

#### 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,

#### Kenny Lau (Feb 27 2020 at 11:41):

do you mean 3 \| n^2?

#### Kenny Lau (Feb 27 2020 at 11:42):

you can use % (nat.mod)

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

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

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

#### Anne Baanen (Feb 27 2020 at 13:09):

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

#### Shing Tak Lam (Feb 27 2020 at 13:14):

Alright. Thank you very much.

#### 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,
-- 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
-- which is nonsense
},
{ -- 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,
}
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 (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


#### Kenny Lau (Feb 27 2020 at 16:27):

Cunningham's Law is in full effect

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

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

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

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

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


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


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

#### 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

#### 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

#### 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

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

#### 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

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

#### 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