Theory 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 ‹p≥2› 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 ‹p≥2› 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 ‹p≥2›
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