feat(number_theory/lucas_primality): Add theorem for Lucas primality …

…test (#8820)

This is a PR for adding the [Lucas primality test](https://en.wikipedia.org/wiki/Lucas_primality_test) to mathlib. This tells us that a number `p` is prime when an element `a : zmod p` has order `p-1` .



Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>

src/algebra/divisibility.lean

@@ -107,6 +107,9 @@ alias dvd.intro_left ← dvd_of_mul_left_eq
 theorem exists_eq_mul_left_of_dvd (h : a ∣ b) : ∃ c, b = c * a :=
 dvd.elim h (assume c, assume H1 : b = a * c, exists.intro c (eq.trans H1 (mul_comm a c)))
 
+lemma dvd_iff_exists_eq_mul_left : a ∣ b ↔ ∃ c, b = c * a :=
+⟨exists_eq_mul_left_of_dvd, by { rintro ⟨c, rfl⟩, exact ⟨c, mul_comm _ _⟩, }⟩
+
 theorem dvd.elim_left {P : Prop} (h₁ : a ∣ b) (h₂ : ∀ c, b = c * a → P) : P :=
 exists.elim (exists_eq_mul_left_of_dvd h₁) (assume c, assume h₃ : b = c * a, h₂ c h₃)
 

src/data/nat/totient.lean

@@ -39,14 +39,27 @@ lemma totient_le (n : ℕ) : φ n ≤ n :=
 calc totient n ≤ (range n).card : card_filter_le _ _
            ... = n              : card_range _
 
+lemma totient_lt (n : ℕ) (hn : 1 < n) : φ n < n :=
+calc totient n ≤ ((range n).filter (≠ 0)).card :
+  begin
+    apply card_le_of_subset (monotone_filter_right _ _),
+    intros n1 hn1 hn1',
+    simpa only [hn1', coprime_zero_right, hn.ne'] using hn1,
+  end
+... = n - 1 : by simp only [filter_ne' (range n) 0, card_erase_of_mem, n.pred_eq_sub_one,
+                card_range, pos_of_gt hn, mem_range]
+... < n : nat.sub_lt (pos_of_gt hn) zero_lt_one
+
 lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
 | 0 := dec_trivial
 | 1 := by simp [totient]
 | (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩
 
 open zmod
 
-@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [fact (0 < n)] :
+/-- Note this takes an explicit `fintype (units (zmod n))` argument to avoid trouble with instance
+diamonds. -/
+@[simp] lemma _root_.zmod.card_units_eq_totient (n : ℕ) [fact (0 < n)] [fintype (units (zmod n))] :
   fintype.card (units (zmod n)) = φ n :=
 calc fintype.card (units (zmod n)) = fintype.card {x : zmod n // x.val.coprime n} :
   fintype.card_congr zmod.units_equiv_coprime
@@ -187,6 +200,27 @@ begin
   rwa [succ_le_iff, pos_iff_ne_zero],
 end
 
+lemma card_units_zmod_lt_sub_one {p : ℕ} (hp : 1 < p) [fintype (units (zmod p))] :
+  fintype.card (units (zmod p)) ≤ p - 1 :=
+begin
+  haveI : fact (0 < p) := ⟨zero_lt_one.trans hp⟩,
+  rw zmod.card_units_eq_totient p,
+  exact nat.le_pred_of_lt (nat.totient_lt p hp),
+end
+
+lemma prime_iff_card_units (p : ℕ) [fintype (units (zmod p))] :
+  p.prime ↔ fintype.card (units (zmod p)) = p - 1 :=
+begin
+  by_cases hp : p = 0,
+  { substI hp,
+    simp only [zmod, not_prime_zero, false_iff, zero_tsub],
+    -- the substI created an non-defeq but subsingleton instance diamond; resolve it
+    suffices : fintype.card (units ℤ) ≠ 0, { convert this },
+    simp },
+  haveI : fact (0 < p) := ⟨nat.pos_of_ne_zero hp⟩,
+  rw [zmod.card_units_eq_totient, nat.totient_eq_iff_prime (fact.out (0 < p))],
+end
+
 @[simp] lemma totient_two : φ 2 = 1 :=
 (totient_prime prime_two).trans (by norm_num)
 

src/group_theory/order_of_element.lean

@@ -161,6 +161,33 @@ begin
   exact ⟨m, by rw [←pow_mul, pow_eq_mod_order_of, hm, pow_one]⟩,
 end
 
+/--
+If `x^n = 1`, but `x^(n/p) ≠ 1` for all prime factors `p` of `r`,
+then `x` has order `n` in `G`.
+-/
+@[to_additive add_order_of_eq_of_nsmul_and_div_prime_nsmul]
+theorem order_of_eq_of_pow_and_pow_div_prime (hn : 0 < n) (hx : x^n = 1)
+  (hd : ∀ p : ℕ, p.prime → p ∣ n → x^(n/p) ≠ 1) :
+  order_of x = n :=
+begin
+  -- Let `a` be `n/(order_of x)`, and show `a = 1`
+  cases exists_eq_mul_right_of_dvd (order_of_dvd_of_pow_eq_one hx) with a ha,
+  suffices : a = 1, by simp [this, ha],
+  -- Assume `a` is not one...
+  by_contra,
+  have a_min_fac_dvd_p_sub_one : a.min_fac ∣ n,
+  { obtain ⟨b, hb⟩ : ∃ (b : ℕ), a = b * a.min_fac := exists_eq_mul_left_of_dvd a.min_fac_dvd,
+    rw [hb, ←mul_assoc] at ha,
+    exact dvd.intro_left (order_of x * b) ha.symm, },
+  -- Use the minimum prime factor of `a` as `p`.
+  refine hd a.min_fac (nat.min_fac_prime h) a_min_fac_dvd_p_sub_one _,
+  rw [←order_of_dvd_iff_pow_eq_one, nat.dvd_div_iff (a_min_fac_dvd_p_sub_one),
+      ha, mul_comm, nat.mul_dvd_mul_iff_left (order_of_pos' _)],
+  { exact nat.min_fac_dvd a, },
+  { rw is_of_fin_order_iff_pow_eq_one,
+    exact Exists.intro n (id ⟨hn, hx⟩) },
+end
+
 @[to_additive add_order_of_eq_add_order_of_iff]
 lemma order_of_eq_order_of_iff {H : Type*} [monoid H] {y : H} :
   order_of x = order_of y ↔ ∀ n : ℕ, x ^ n = 1 ↔ y ^ n = 1 :=

src/number_theory/lucas_primality.lean

@@ -0,0 +1,59 @@
+/-
+Copyright (c) 2020 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+import data.zmod.basic
+import data.fintype.basic
+import field_theory.finite.basic
+import group_theory.order_of_element
+import tactic.zify
+
+/-!
+# The Lucas test for primes.
+
+This file implements the Lucas test for primes (not to be confused with the Lucas-Lehmer test for
+Mersenne primes). A number `a` witnesses that `n` is prime if `a` has order `n-1` in the
+multiplicative group of integers mod `n`. This is checked by verifying that `a^(n-1) = 1 (mod n)`
+and `a^d ≠ 1 (mod n)` for any divisor `d | n - 1`. This test is the basis of the Pratt primality
+certificate.
+
+## TODO
+
+- Bonus: Show the reverse implication i.e. if a number is prime then it has a Lucas witness.
+  Use `units.is_cyclic` from `ring_theory/integral_domain` to show the group is cyclic.
+- Write a tactic that uses this theorem to generate Pratt primality certificates
+- Integrate Pratt primality certificates into the norm_num primality verifier
+
+## Implementation notes
+
+Note that the proof for `lucas_primality` relies on analyzing the multiplicative group
+modulo `p`. Despite this, the theorem still holds vacuously for `p = 0` and `p = 1`: In these
+cases, we can take `q` to be any prime and see that `hd` does not hold, since `a^((p-1)/q)` reduces
+to `1`.
+-/
+
+/--
+If `a^(p-1) = 1 mod p`, but `a^((p-1)/q) ≠ 1 mod p` for all prime factors `q` of `p-1`, then `p`
+is prime. This is true because `a` has order `p-1` in the multiplicative group mod `p`, so this
+group must itself have order `p-1`, which only happens when `p` is prime.
+-/
+theorem lucas_primality (p : ℕ) (a : zmod p) (ha : a^(p-1) = 1)
+  (hd : ∀ q : ℕ, q.prime → q ∣ (p-1) → a^((p-1)/q) ≠ 1) : p.prime :=
+begin
+  have h0 : p ≠ 0, { rintro ⟨⟩, exact hd 2 nat.prime_two (dvd_zero _) (pow_zero _) },
+  have h1 : p ≠ 1, { rintro ⟨⟩, exact hd 2 nat.prime_two (dvd_zero _) (pow_zero _) },
+  have hp1 : 1 < p := lt_of_le_of_ne h0.bot_lt h1.symm,
+  have order_of_a : order_of a = p-1,
+  { apply order_of_eq_of_pow_and_pow_div_prime _ ha hd,
+    exact tsub_pos_of_lt hp1, },
+  haveI fhp0 : fact (0 < p) := ⟨h0.bot_lt⟩,
+  rw nat.prime_iff_card_units,
+  -- Prove cardinality of `units` of `zmod p` is both `≤ p-1` and `≥ p-1`
+  refine le_antisymm (nat.card_units_zmod_lt_sub_one hp1) _,
+  have hp' : p - 2 + 1 = p - 1 := tsub_add_eq_add_tsub hp1,
+  let a' : units (zmod p) := units.mk_of_mul_eq_one a (a ^ (p-2)) (by rw [←pow_succ, hp', ha]),
+  calc p - 1 = order_of a : order_of_a.symm
+  ... = order_of a' : order_of_injective (units.coe_hom (zmod p)) units.ext a'
+  ... ≤ fintype.card (units (zmod p)) : order_of_le_card_univ,
+end