Proof review

Stream: new members

[Bhavik Mehta]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

[spoiler alert]

[Kevin Buzzard]

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

[Kevin Buzzard]

https://github.com/b-mehta/lean-experiments/blob/669f0d464167db055836768d94af88f30da88ed9/number_theory_q5.lean#L10 is your proof of

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
  rw [nat.pow_succ, mul_add, ←mul_assoc, ←hq],
  -- ⊢ 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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

existsi q * a + 1 is way faster

[Kevin Buzzard]

?!

[Kevin Buzzard]

  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]

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]

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]

@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,
  rw [mul_add, mul_one, nat.add_sub_assoc (pow_pos ha _)], simpa
end

[Mario Carneiro]

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

[Kevin Buzzard]

and only one non-terminal simp ;-)

[Mario Carneiro]

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

[Mario Carneiro]

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

[Bryan Gin-ge Chen]

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

[Mario Carneiro]

That should go in braces though, as a style matter

[Kenny Lau]

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 _),
  conv_lhs { rw [nat.pow_succ, ← nat.sub_add_cancel (pow_pos ha n), add_mul, one_mul, nat.add_sub_assoc ha] }
end

[Kenny Lau]

no simp

[Kevin Buzzard]

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

[Bhavik Mehta]

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]

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]

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]

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]

finset.sum

[Kevin Buzzard]

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]

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]

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

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]

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]

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]

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]

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.