## Stream: new members

### Topic: Proof review

#### Bhavik Mehta (Nov 01 2019 at 23:31):

I finally finished my first proper proof in lean (other than the natural numbers game): https://github.com/b-mehta/lean-experiments/blob/master/number_theory_q5.lean. Any reviews/improvements/comments appreciated!

#### Kevin Buzzard (Nov 02 2019 at 01:05):

Hey that is great! If it compiles I'm happy :D

#### Kevin Buzzard (Nov 02 2019 at 01:38):

example : prime 11 := by norm_num
example : ¬ (prime (2^11-1)) := by norm_num


#### Kevin Buzzard (Nov 02 2019 at 01:40):

example : ∃ n : ℕ, prime n ∧ ¬ prime (2^n-1) := by use 11; norm_num


#### Kevin Buzzard (Nov 02 2019 at 02:05):

lemma division_lemma { a n : ℕ } ( ha : a ≥ 1 ) : a - 1 ∣ a ^ n - 1


I want to do this using ring but stupid natural number subtraction gets in the way. Is there a one-line command nowadays which fills in this sorry nowadays?

lemma division_lemma { a n : ℕ } ( ha : a ≥ 1 ) : a - 1 ∣ a ^ n - 1 :=
begin
induction n with d hd,
use 0, refl,
cases hd with q hq,
use q * a + 1,
-- need some extra tidying because need to use IH as we don't have Groebner bases
-- ⊢ a ^ d * a - 1 = (a ^ d - 1) * a + (a - 1) * 1
-- ring doesn't work I think because of natural number subtraction,
suffices : ∀ (b : ℤ) (e : ℕ) (hb : (1 : ℤ) ≤ b),
b ^ e * b - 1 = (b ^ e - 1) * b + (b - 1) * 1,
sorry,
intros, ring,
end


#### Mario Carneiro (Nov 02 2019 at 02:44):

did you try casting the equation to int, using norm_cast, then ring?

#### Mario Carneiro (Nov 02 2019 at 02:48):

example : ∃ n : ℕ, prime n ∧ ¬ prime (2^n-1) := by use 11; norm_num


I just want to say how happy I am that this kind of thing is basically a solved problem today. I have a paper about how much of a struggle this was in 2015: https://arxiv.org/abs/1503.02349

#### Kevin Buzzard (Nov 02 2019 at 02:54):

By the way @Bhavik Mehta don't use a ≥ 1, always use1 ≤ a or you're asking for trouble. Unfold this layer of abstraction yourself.

#### Kevin Buzzard (Nov 02 2019 at 02:59):

did you try casting the equation to int, using norm_cast, then ring?

I can't figure out how to make norm_cast do it because there is stupid natural number subtraction. I realise now that my sorry is perhaps harder than it looks. I am not sure we can get away without proving that b^e*b-1 really is one less if b>=1.

#### Mario Carneiro (Nov 02 2019 at 03:00):

If you apply int.coe_nat_inj and then simp and rw with int.coe_nat_sub, you should get the requisite side conditions

#### Mario Carneiro (Nov 02 2019 at 03:04):

For some reason the use q * a + 1, line takes forever

#### Mario Carneiro (Nov 02 2019 at 03:04):

existsi q * a + 1 is way faster

?!

#### Kevin Buzzard (Nov 02 2019 at 03:06):

  simp only [nat.mul_sub_right_distrib, one_mul],
apply int.coe_nat_inj,
simp,
rw int.coe_nat_sub,
simp,
rw int.coe_nat_sub,
simp,
rw int.coe_nat_sub,
simp,
ring,


Killed it. Is this OK for mathlib by the way?

#### Kevin Buzzard (Nov 02 2019 at 03:07):

3 goals
a : ℕ,
ha : 1 ≤ a,
d q : ℕ,
hq : a ^ d - 1 = (a - 1) * q
⊢ a ≤ a ^ d * a

a : ℕ,
ha : 1 ≤ a,
d q : ℕ,
hq : a ^ d - 1 = (a - 1) * q
⊢ 1 ≤ a

a : ℕ,
ha : 1 ≤ a,
d q : ℕ,
hq : a ^ d - 1 = (a - 1) * q
⊢ 1 ≤ a ^ d * a


sigh

#### Mario Carneiro (Nov 02 2019 at 03:09):

lemma division_lemma { a n : ℕ } ( ha : a ≥ 1 ) : a - 1 ∣ a ^ n - 1 :=
begin
induction n with d hd,
{ use 0, refl },
cases hd with q hq,
existsi q * a + 1,
rw [nat.pow_succ, mul_add, ←mul_assoc, ←hq, ← int.coe_nat_inj'],
have hp : 1 ≤ a ^ d := nat.pow_pos ha _,
have hpa : 1 ≤ a ^ d * a := @mul_pos ℕ _ _ _ hp ha,
simp [int.coe_nat_sub ha, int.coe_nat_sub hp, int.coe_nat_sub hpa],
ring
end


#### Kevin Buzzard (Nov 02 2019 at 03:10):

@Bhavik Mehta 's proof is shorter ;-)

lemma division_lemma { a n : ℕ } ( ha : a ≥ 1 ) : a - 1 ∣ a ^ n - 1 :=
begin
apply dvd_of_mod_eq_zero,
induction n with n, simp,
suffices: (a^n * (a - 1 + 1) - 1) % (a - 1) = 0,
by rwa nat.sub_add_cancel ha at this,
end


#### Mario Carneiro (Nov 02 2019 at 03:11):

I'm not competing, I'm showing how to complete your sorry

#### Kevin Buzzard (Nov 02 2019 at 03:12):

and only one non-terminal simp ;-)

#### Mario Carneiro (Nov 02 2019 at 03:13):

oh, I can get rid of the rw in this version

#### Mario Carneiro (Nov 02 2019 at 03:13):

so no more nonterminal simp (simp, ring doesn't count :P)

#### Bryan Gin-ge Chen (Nov 02 2019 at 03:16):

@Bhavik Mehta 's first simp is terminal too, since it kills off the base case of the induction.

#### Mario Carneiro (Nov 02 2019 at 03:18):

That should go in braces though, as a style matter

#### Kenny Lau (Nov 02 2019 at 03:19):

lemma division_lemma { a n : ℕ } ( ha : a ≥ 1 ) : a - 1 ∣ a ^ n - 1 :=
begin
induction n with n ih, { exact dvd_zero _ },
convert dvd_add (dvd_mul_of_dvd_left ih a) (dvd_refl _),
end


no simp

#### Kevin Buzzard (Nov 02 2019 at 03:27):

There might be more of those French brackets in Bhavik's code than there is in all of mathlib :D

#### Bhavik Mehta (Nov 02 2019 at 13:04):

example : ∃ n : ℕ, prime n ∧ ¬ prime (2^n-1) := by use 11; norm_num


Ah this is nice, but I intentionally didn't use ∃ so that the statement matches that in the question directly. Could you explain the difference between use and existsi?

#### Bhavik Mehta (Nov 02 2019 at 13:06):

My original version had lots of int.coe_nat_... but I thought it was clearer without. What's the significance of a terminal simp?

#### Bhavik Mehta (Nov 02 2019 at 13:09):

There might be more of those French brackets in Bhavik's code than there is in all of mathlib :D

I might have massively overused those, but I thought it looked pretty :D

#### Bhavik Mehta (Nov 02 2019 at 13:15):

Perhaps it wouldn't give the nicest proof overall, but the natural way to prove division_lemma to a mathematician would probably be to just say (a - 1) * (a^{n-1} + a^{n-2} + ... + a + 1) = a^n - 1. How could I express the + ... + in lean?

#### Mario Carneiro (Nov 02 2019 at 13:15):

finset.sum

#### Kevin Buzzard (Nov 02 2019 at 13:41):

If you do it like that you'll have to then prove that the sum telescopes. Tools should be there to do this but I don't know if they're there yet. Here's a roadmap for the natural proof:

$(a-1)(\sum_{i=0}^{n-1}a^i)=\sum_{i=0}^{n-1}(a^{i+1}-a^i)=\sum_{j=1}^{n}a^j-\sum_{i=0}^{n-1}a^i=a^n+\sum_{j=1}^{n-1}a^j-1-\sum_{i=1}^{n-1}a^i=a^n-1$.

Are there any of these equalities which are not yet trivial in Lean? You could try proving this in a calc block, that's the way mathematicians think about it. Which lines do you get stuck on?

#### Kevin Buzzard (Nov 02 2019 at 13:42):

The last time I tried this sort of thing was about 18 months ago and I was very dissatisfied with what I could find at the time. But things move on. @Chris Hughes is each of those equalities one line in Lean yet? Or 2 if you really think I skipped a step

#### Kevin Buzzard (Nov 02 2019 at 13:44):

@Bhavik Mehta you do know, right, that your "natural" proof is just the same proof by induction anyway? You just hide away the induction in the $\ldots$. Even the definition of your (a^{n-1} + a^{n-2} + ... + a + 1) requires recursion so by definition you have to use induction to prove anything about it.

#### Kevin Buzzard (Nov 02 2019 at 13:46):

This reminds me of a question I put on M1F [old Imperial 1st year intro to proof course]. Before Lean it was something like "show $(8^n-3^n)$ is a multiple of 5, by induction on $n$. Then one year I got cocky and added a rider "(b) now show it directly without using induction". And then when I was formalising the solutions in Lean two years ago I added "(c) Now find out where in your non-induction proof you actually used induction anyway".

#### Bhavik Mehta (Nov 02 2019 at 15:18):

Bhavik Mehta you do know, right, that your "natural" proof is just the same proof by induction anyway? You just hide away the induction in the $\ldots$. Even the definition of your (a^{n-1} + a^{n-2} + ... + a + 1) requires recursion so by definition you have to use induction to prove anything about it.

Yeah definitely, but being able to express it in familiar language would be nice

#### Kevin Buzzard (Nov 02 2019 at 15:47):

So you need functions which encapsulate all the ideas, and you need notation which conveys what the functions are doing to the mathematician user. So the challenge is first to formalise the maths proof in the displayed equation above, and then the second challenge is to use notation to make the proof itself look comprehensible to mathematicians. I think this is a very worthwhile project, it's not the sort of thing that people work on here because the CS people just want some obfuscated 3 line term mode proof and the maths people with some Lean background are just relieved to get anything which compiles. Perhaps some kind of document is needed which shows the novice user exactly which functions are available (or which notation is available) and how to use it, with copious examples like this one, and then some exercises. Don't just close the goal, write teaching material as you learn.

#### Kevin Buzzard (Nov 02 2019 at 15:51):

It's all very well me saying "oh I'm sure finset has got a brilliant API, this is exactly what Mario spent 2017 doing and he's extremely good at making API's, you want to write $\sum_{i=0}^{n-1}a_i$ as $a_0+\sum_{i=1}^{n-1}a_i$, that's bound to be in there somewhere" but this is basically telling you to go and read data/finset.lean. We can't tell novice users to do this, we need to tell them how to do these calculations in a calc block in a way that makes it all easy. Calc blocks are often chains of equalities and can be solved using rw. The natural number game shows that mathematicians can get good at rewrites quite quickly if you tell them what they can rewrite. So the procedure should be to do 5 questions like this which involve manipulating sums and then figuring out which functions are being used a lot and making sure that rewriting with them is painless (in the sense that Lean usually guesses what the user means, because we don't want to write rw add_assoc a b in general, we want to rw add_assoc and let Lean do a sensible thing).

#### Kevin Buzzard (Nov 02 2019 at 15:53):

This is all work towards bridging the gap between mathematicians and Lean users. I think it's extremely important. It's clear why we don't have more mathematician users -- the software is impossible to use and the manuals keep going on about type theory. Brian Conrad has said to me on several occasions that he doesn't know what a type is and doesn't care. Type theory puts people off because it's weird. But with nng I hide this weirdness and mathematicians try it.

Last updated: May 08 2021 at 03:17 UTC