feat(number_theory/lucas_lehmer): prime (2^127 - 1) (#2842)

This PR
1. proves the sufficiency of the Lucas-Lehmer test for Mersenne primes
2. provides a tactic that uses `norm_num` to do each step of the calculation of Lucas-Lehmer residues
3. proves 2^127 - 1 = 170141183460469231731687303715884105727 is prime

It doesn't
1. prove the necessity of the Lucas-Lehmer test (mathlib certainly has the necessary material if someone wants to do this)
2. use the trick `n ≡ (n % 2^p) + (n / 2^p) [MOD 2^p - 1]` that is essential to calculating Lucas-Lehmer residues quickly
3. manage to prove any "computer era" primes are prime! (Although my guess is that 2^521 - 1 would run in <1 day with the current implementation.)

I think using "the trick" is very plausible, and would be a fun project for someone who wanted to experiment with certified/fast arithmetic in Lean. It likely would make much larger Mersenne primes accessible.

This is a tidy-up and completion of work started by a student, Ainsley Pahljina.

archive/examples/mersenne_primes.lean

@@ -0,0 +1,54 @@
+/-
+Copyright (c) 2020 Scott Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Scott Morrison
+-/
+import number_theory.lucas_lehmer
+
+/-!
+# Explicit Mersenne primes
+
+We run some Lucas-Lehmer tests to prove some Mersenne primes are prime.
+
+See the discussion at the end of [src/number_theory/lucas_lehmer.lean]
+for ideas about extending this to larger Mersenne primes.
+-/
+
+example : (mersenne 13).prime :=
+lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+example : (mersenne 17).prime :=
+lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+example : (mersenne 19).prime :=
+lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+
+/-- 2147483647.prime, Euler (1772) -/
+example : (mersenne 31).prime :=
+lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+
+/-!
+The next four primality tests are too slow to run interactively with -T100000,
+but work fine on the command line.
+-/
+
+-- /-- 2305843009213693951.prime, Pervouchine (1883), Seelhoff (1886) -/
+-- example : (mersenne 61).prime :=
+-- lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+-- /-- 618970019642690137449562111.prime, Powers (1911) -/
+-- -- takes ~100s
+-- example : (mersenne 89).prime :=
+-- lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+-- /-- 162259276829213363391578010288127.prime, Power (1914) -/
+-- -- takes ~190s
+-- example : (mersenne 107).prime :=
+-- lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+-- /-- 170141183460469231731687303715884105727.prime, Lucas (1876) -/
+-- -- takes ~370s
+-- example : (mersenne 127).prime :=
+-- lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).
+
+/- This still doesn't get us over the big gap and into the computer era, unfortunately. -/
+
+-- /-- (2^521 - 1).prime, Robinson (1954) -/
+-- -- This has not been run successfully!
+-- example : (mersenne 521).prime :=
+-- lucas_lehmer_sufficiency _ (by norm_num) (by lucas_lehmer.run_test).

src/data/nat/parity.lean

@@ -53,6 +53,15 @@ even_add.2 $ by simp only [*]
 @[simp] theorem not_even_bit1 (n : nat) : ¬ even (bit1 n) :=
 by simp [bit1] with parity_simps
 
+lemma two_not_dvd_two_mul_add_one (a : ℕ) : ¬(2 ∣ 2 * a + 1) :=
+begin
+  convert not_even_bit1 a,
+  exact two_mul a,
+end
+
+lemma two_not_dvd_two_mul_sub_one : Π {a : ℕ} (w : 0 < a), ¬(2 ∣ 2 * a - 1)
+| (a+1) _ := two_not_dvd_two_mul_add_one a
+
 @[parity_simps] theorem even_sub {m n : nat} (h : n ≤ m) : even (m - n) ↔ (even m ↔ even n) :=
 begin
   conv { to_rhs, rw [←nat.sub_add_cancel h, even_add] },