Theory Lehmer.Lehmer

theory Lehmer
imports
  Main
  "HOL-Number_Theory.Residues"
begin

section ‹Lehmer's Theorem›
text_raw ‹\label{sec:lehmer}›

text ‹
  In this section we prove Lehmer's Theorem~cite"lehmer1927fermat_converse" and its converse.
  These two theorems characterize a necessary and complete criterion for primality. This criterion
  is the basis of the Lucas-Lehmer primality test and the primality certificates of
  Pratt~cite"pratt1975certificate".
›

lemma mod_1_coprime_nat:
  "coprime a b" if "0 < n" "[a ^ n = 1] (mod b)" for a b :: nat
proof -
  from that coprime_1_left have "coprime (a ^ n) b"
    using cong_imp_coprime cong_sym by blast
  with 0 < n show ?thesis
    by simp
qed

text ‹
  This is a weak variant of Lehmer's theorem: All numbers less then @{term "p - 1 :: nat"}
  must be considered.
›

lemma lehmers_weak_theorem:
  assumes "2  p"
  assumes min_cong1: "x. 0 < x  x < p - 1  [a ^ x  1] (mod p)"
  assumes cong1: "[a ^ (p - 1) = 1] (mod p)"
  shows "prime p"
proof (rule totient_imp_prime)
  from 2  p cong1 have "coprime a p"
    by (intro mod_1_coprime_nat[of "p - 1"]) auto
  then have "[a ^ totient p = 1] (mod p)"
    by (intro euler_theorem) auto
  then have "totient p  p - 1  totient p = 0"
    using min_cong1[of "totient p"] by fastforce
  moreover have "totient p > 0"
    using 2  p by simp
  moreover from p  2 have "totient p < p" by (intro totient_less) auto
  ultimately show "totient p = p - 1" by presburger
qed (insert p  2, auto)

lemma prime_factors_elem:
  fixes n :: nat assumes "1 < n" shows "p. p  prime_factors n"
  using assms by (cases "prime n") (auto simp: prime_factors_dvd prime_factor_nat)

lemma cong_pow_1_nat:
  "[a ^ x = 1] (mod b)" if "[a = 1] (mod b)" for a b :: nat
  using cong_pow [of a 1 b x] that by simp

lemma cong_gcd_eq_1_nat:
  fixes a b :: nat
  assumes "0 < m" and cong_props: "[a ^ m = 1] (mod b)" "[a ^ n = 1] (mod b)"
  shows "[a ^ gcd m n = 1] (mod b)"
proof -
  obtain c d where gcd: "m * c = n * d + gcd m n" using bezout_nat[of m n] 0 < m
    by auto
  have cong_m: "[a ^ (m * c) = 1] (mod b)" and cong_n: "[a ^ (n * d) = 1] (mod b)"
    using cong_props by (simp_all only: cong_pow_1_nat power_mult)
  have "[1 * a ^ gcd m n = a ^ (n * d) * a ^ gcd m n] (mod b)"
    by (rule cong_scalar_right, rule cong_sym) (fact cong_n)
  also have "[a ^ (n * d) * a ^ gcd m n = a ^ (m * c)] (mod b)"
    using gcd by (simp add: power_add)
  also have "[a ^ (m * c) = 1] (mod b)" using cong_m by simp
  finally show "[a ^ gcd m n = 1] (mod b)" by simp
qed

lemma One_leq_div:
  "1 < b div a" if "a dvd b" "a < b" for a b :: nat
  using that by (metis dvd_div_mult_self mult.left_neutral mult_less_cancel2)

theorem lehmers_theorem:
  assumes "2  p"
  assumes pf_notcong1: "x. x  prime_factors (p - 1)  [a ^ ((p - 1) div x)  1] (mod p)"
  assumes cong1: "[a ^ (p - 1) = 1] (mod p)"
  shows "prime p"
proof cases
  assume "[a = 1] (mod p)" with 2 p pf_notcong1 show ?thesis
    by (metis cong_pow_1_nat less_diff_conv linorder_neqE_nat linorder_not_less
      one_add_one prime_factors_elem two_is_prime_nat)
next
  assume A_notcong_1: "[a  1] (mod p)"
  { fix x assume "0 < x" "x < p - 1"
    have "[a ^ x  1] (mod p)"
    proof
      assume "[a ^ x = 1] (mod p)"
      then have gcd_cong_1: "[a ^ gcd x (p - 1) = 1] (mod p)"
        by (rule cong_gcd_eq_1_nat[OF 0 < x _ cong1])

      have "gcd x (p - 1) = p - 1"
      proof (rule ccontr)
        assume "¬?thesis"
        then have gcd_p1: "gcd x (p - 1) dvd (p - 1)" "gcd x (p - 1) < p - 1"
          using gcd_le2_nat[of "p - 1" x] 2  p by (simp, linarith)

        define c where "c = (p - 1) div (gcd x (p - 1))"
        then have p_1_eq: "p - 1 = gcd x (p - 1) * c" unfolding c_def using gcd_p1
          by (metis dvd_mult_div_cancel)

        from gcd_p1 have "1 < c" unfolding c_def by (rule One_leq_div)
        then obtain q where q_pf: "q  prime_factors c"
          using prime_factors_elem by auto
        then have "q dvd c" by auto

        have "q  prime_factors (p - 1)" using q_pf 1 < c 2  p
          by (subst p_1_eq) (simp add: prime_factors_product)
        moreover
        have "[a ^ ((p - 1) div q) = 1] (mod p)"
          by (subst p_1_eq,subst dvd_div_mult_self[OF q dvd c,symmetric])
             (simp del: One_nat_def add: power_mult gcd_cong_1 cong_pow_1_nat)
        ultimately
        show False using pf_notcong1 by metis
      qed
      then show False using x < p - 1
        by (metis 0 < x gcd_le1_nat gr_implies_not0 linorder_not_less)
    qed
  }
  with lehmers_weak_theorem[OF 2  p _ cong1] show ?thesis by metis
qed

text ‹
  The converse of Lehmer's theorem is also true.
›

lemma converse_lehmer_weak:
 assumes prime_p: "prime p"
 shows " a. [a^(p - 1) = 1] (mod p)  ( x . 0 < x  x  p - 2  [a^x  1] (mod p))
              a > 0  a < p"
 proof -
   have "p  2" by (rule prime_ge_2_nat[OF prime_p])
   obtain a where a:"a  {1 .. p - 1}  {1 .. p - 1} = {a^i mod p | i . i  UNIV}"
    using residue_prime_mult_group_has_gen[OF prime_p] by blast
  {
   { fix x::nat assume x:"0 < x  x  p - 2  [a^x = 1] (mod p)"
     have "{a^i mod p| i. i  UNIV} = {a^i mod p | i. 0 < i  i  x}"
     proof
      show "{a ^ i mod p | i. 0 < i  i  x}  {a ^ i mod p | i. i  UNIV}" by blast
      { fix y assume y:"y  {a^i mod p| i . i  UNIV}"
        then obtain i where i:"y = a^i mod p" by auto
        define q r where "q = i div x" and "r = i mod x"
        have "i = q*x + r" by (simp add: r_def q_def)
        hence y_q_r:"y = (((a ^ (q*x)) mod p) * ((a ^ r) mod p)) mod p"
          by (simp add: i power_add mod_mult_eq)
        have "a ^ (q*x) mod p = (a ^ x mod p) ^ q mod p"
          by (simp add: power_mod mult.commute power_mult[symmetric])
        then have y_r:"y = a ^ r mod p" using p2 x
          by (simp add: cong_def y_q_r)
        have "y  {a ^ i mod p | i. 0 < i  i  x}"
        proof (cases)
          assume "r = 0"
          then have "y = a^x mod p" using p2 x
            by (simp add: cong_def y_r)
          thus ?thesis using x by blast
        next
          assume "r  0"
          thus ?thesis using x by (auto simp add: y_r r_def)
        qed
      }
      thus " {a ^ i mod p|i. i  UNIV}  {a ^ i mod p | i. 0 < i  i  x}" by auto
    qed
    note X = this

    have "p - 1 = card {1 .. p - 1}" by auto
    also have "{1 .. p - 1} = {a^i mod p | i. 1  i  i  x}" using X a by auto
    also have " = (λ i. a^i mod p) ` {1..x}" by auto
    also have "card   p - 2"
      using Finite_Set.card_image_le[of "{1..x}" "λ i. a^i mod p"] x by auto
    finally have False using 2  p by arith
   }
   hence " x . 0 < x  x  p - 2  [a^x  1] (mod p)" by auto
 } note a_is_gen = this
 {
    assume "a>1"
    have "¬ p dvd a "
    proof (rule ccontr)
      assume "¬ ¬ p dvd a"
      hence "p dvd a" by auto
      have "p  a" using dvd_nat_bounds[OF _ p dvd a] a by simp
      thus False using a>1 a by force
    qed
    hence "coprime a p"
      using prime_imp_coprime_nat [OF prime_p] by (simp add: ac_simps)
    then have "[a ^ totient p = 1] (mod p)"
      by (rule euler_theorem)
    also from prime_p have "totient p = p - 1"
      by (rule totient_prime)
    finally have "[a ^ (p - 1) = 1] (mod p)" .
  }
  hence "[a^(p - 1) = 1] (mod p)" using a by fastforce
  thus ?thesis using a_is_gen a by auto
 qed

theorem converse_lehmer:
 assumes prime_p:"prime(p)"
 shows " a . [a^(p - 1) = 1] (mod p) 
              ( q. q  prime_factors (p - 1)  [a^((p - 1) div q)  1] (mod p))
               a > 0  a < p"
 proof -
  have "p  2" by (rule prime_ge_2_nat[OF prime_p])
  obtain a where a:"[a^(p - 1) = 1] (mod p)  ( x . 0 < x  x  p - 2  [a^x  1] (mod p))
                     a > 0  a < p"
    using converse_lehmer_weak[OF prime_p] by blast
  { fix q assume q:"q  prime_factors (p - 1)"
    hence "0 < q  q  p - 1" using p2
      by (auto simp add: dvd_nat_bounds prime_factors_gt_0_nat)
    hence "(p - 1) div q  1" using div_le_mono[of "q" "p - 1" q] div_self[of q] by simp
    have "q  2" using q by (auto intro: prime_ge_2_nat)
    hence "(p - 1) div q < p - 1" using p  2 by simp
    hence "[a^((p - 1) div q)  1] (mod p)" using a (p - 1) div q  1
      by (auto simp add: Suc_diff_Suc less_eq_Suc_le)
  }
  thus ?thesis using a by auto
 qed

end