Zulip Chat Archive

Stream: new members

Topic: Proof review


view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 01:05):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 01:38):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 01:39):

[spoiler alert]

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 01:40):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 02:05):

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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 02:44):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:04):

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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:04):

existsi q * a + 1 is way faster

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 03:04):

?!

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:11):

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

view this post on Zulip Kevin Buzzard (Nov 02 2019 at 03:12):

and only one non-terminal simp ;-)

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:13):

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

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:13):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 02 2019 at 03:18):

That should go in braces though, as a style matter

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

view this post on Zulip Kenny Lau (Nov 02 2019 at 03:19):

no simp

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Nov 02 2019 at 13:15):

finset.sum

view this post on Zulip 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:

(a1)(i=0n1ai)=i=0n1(ai+1ai)=j=1naji=0n1ai=an+j=1n1aj1i=1n1ai=an1(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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 (8n3n)(8^n-3^n) is a multiple of 5, by induction on nn. 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".

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 i=0n1ai\sum_{i=0}^{n-1}a_i as a0+i=1n1aia_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).

view this post on Zulip 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