Theory SG_Theorem
theory SG_Theorem
imports FLT_Sufficient_Conditions
begin
section ‹Sophie Germain's Theorem: classical Version›
text ‹The proof we give here is from \<^cite>‹Francinou_Gianella_Nicolas_2014›.›
subsection ‹A Crucial Lemma›
lemma Sophie_Germain_lemma_computation :
fixes x y :: int assumes ‹odd p›
defines ‹S ≡ ∑k = 0..p - 1. (- y) ^ (p - 1 - k) * x ^ k›
shows ‹(x + y) * S = x ^ p + y ^ p›
proof -
from ‹odd p› have ‹0 < p› by (simp add: odd_pos)
from int_distrib(1) have ‹(x + y) * S = x * S - (- y) * S› by auto
have ‹x * S = (∑k = 0..p - 1. (- y) ^ (p - 1 - k) * x ^ (k + 1))›
by (unfold S_def, subst sum_distrib_left) (rule sum.cong[OF refl], simp)
also have ‹… = (∑k = 0..p - 1. (- y) ^ (p - (k + 1)) * x ^ (k + 1))› by simp
also have ‹… = x ^ p + (∑k = 1..p - 1. (- y) ^ (p - k) * x ^ k)›
by (subst sum.shift_bounds_cl_nat_ivl[symmetric])
(simp, metis One_nat_def ‹0 < p› not_gr0 power_eq_if)
finally have S1 : ‹x * S = x ^ p + (∑k = 1..p - 1. (- y) ^ (p - k) * x ^ k)› .
have ‹k ∈ {0..p - 1} ⟹ (- y) ^ Suc (p - 1 - k) * x ^ k = (- y) ^ (p - k) * x ^ k› for k
by (rule arg_cong[where f = ‹λn. (- y) ^ n * x ^ _›])
(metis Suc_diff_le Suc_pred' ‹0 < p› atLeastAtMost_iff)
hence ‹(- y) * S = (∑k = 0..p - 1. (- y) ^ (p - k) * x ^ k)›
by (unfold S_def, subst sum_distrib_left, intro sum.cong[OF refl])
(subst mult.assoc[symmetric], subst power_Suc[symmetric], simp)
also have ‹… = (- y) ^ (p - 0) * x ^ 0 + (∑k = 1..p - 1. (- y) ^ (p - k) * x ^ k)›
by (unfold One_nat_def, subst sum.atLeast_Suc_atMost[symmetric]) simp_all
also have ‹(- y) ^ (p - 0) * x ^ 0 = - (y ^ p)›
by (simp add: ‹odd p›)
finally have S2 : ‹- y * S = - (y ^ p) + (∑k = 1..p - 1. (- y) ^ (p - k) * x ^ k)› .
show ‹(x + y) * S = x ^ p + y ^ p›
unfolding ‹(x + y) * S = x * S - (- y) * S› S1 S2 by simp
qed
lemma Sophie_Germain_lemma_computation_cong_simp :
fixes p :: nat and n x y :: int assumes ‹p ≠ 0› ‹[y = - x] (mod n)›
defines ‹S ≡ λx y. ∑k = 0..p - 1. (- y) ^ (p - 1 - k) * x ^ k›
shows ‹[S x y = p * x ^ (p - 1)] (mod n)›
proof -
from ‹[y = - x] (mod n)› have ‹[S x y = S x (- x)] (mod n)›
unfolding S_def
by (meson cong_minus_minus_iff cong_pow cong_scalar_right cong_sum)
also have ‹S x (- x) = (∑k = 0..p - 1. x ^ (p - 1))›
unfolding S_def
by (rule sum.cong[OF refl], simp)
(metis One_nat_def diff_Suc_eq_diff_pred le_add_diff_inverse2 power_add)
also from ‹p ≠ 0› have ‹… = p * x ^ (p - 1)› by simp
finally show ‹[S x y = p * x ^ (p - 1)] (mod n)› .
qed
lemma Sophie_Germain_lemma_only_possible_prime_common_divisor :
fixes x y z :: int and p :: nat
defines S_def: ‹S ≡ λx y. ∑k = 0..p - 1. (- y) ^ (p - 1 - k) * x ^ k›
assumes ‹prime p› ‹prime q› ‹coprime x y› ‹q dvd x + y› ‹q dvd S x y›
shows ‹q = p›
proof (rule ccontr)
from ‹prime p› have ‹p ≠ 0› by auto
assume ‹q ≠ p›
from ‹q dvd x + y› have ‹[y = - x] (mod q)›
by (metis add_minus_cancel cong_iff_dvd_diff uminus_add_conv_diff)
from Sophie_Germain_lemma_computation_cong_simp[OF ‹p ≠ 0› this]
have ‹[S x y = p * x ^ (p - 1)] (mod q)› unfolding S_def .
with ‹q dvd S x y› ‹q ≠ p› ‹prime q› ‹prime p› have ‹q dvd x ^ (p - 1)›
by (metis cong_dvd_iff prime_dvd_mult_iff prime_nat_int_transfer primes_dvd_imp_eq)
with ‹prime q› prime_dvd_power_int prime_nat_int_transfer have ‹q dvd x› by blast
with ‹q dvd x + y› ‹[y = - x] (mod q)› have ‹q dvd y› by (simp add: cong_dvd_iff)
with ‹coprime x y› ‹q dvd x› ‹prime q› show False
by (metis coprime_def not_prime_unit)
qed
lemma Sophie_Germain_lemma :
fixes x y z :: int
assumes ‹odd p› and ‹prime p› and fermat : ‹x ^ p + y ^ p + z ^ p = 0›
and ‹[x ≠ 0] (mod p)› and ‹coprime y z›
defines ‹S ≡ ∑k = 0..p - 1. (- z) ^ (p - 1 - k) * y ^ k›
shows ‹∃a α. y + z = a ^ p ∧ S = α ^ p›
proof -
from Sophie_Germain_lemma_computation[OF ‹odd p›]
have ‹(y + z) * S = y ^ p + z ^ p› unfolding S_def .
also from fermat have ‹… = (- x) ^ p› by (simp add: ‹odd p›)
finally have ‹(y + z) * S = …› .
have ‹coprime (y + z) S›
proof (rule ccontr)
assume ‹¬ coprime (y + z) S›
then consider ‹y + z = 0› | ‹S = 0› | q :: nat where ‹prime q› ‹q dvd y + z› ‹q dvd S›
by (elim not_coprime_nonzeroE)
(use ‹(y + z) * S = (- x) ^ p› ‹[x ≠ 0] (mod p)› in force,
metis nat_0_le prime_int_nat_transfer)
hence ‹p dvd (y + z) * S›
proof cases
fix q :: nat assume ‹prime q› ‹q dvd y + z› ‹q dvd S›
from Sophie_Germain_lemma_only_possible_prime_common_divisor
[OF ‹prime p› _ ‹coprime y z› ‹q dvd y + z› ‹q dvd S›[unfolded S_def]]
show ‹p dvd (y + z) * S› using ‹int q dvd S› ‹prime q› by auto
qed simp_all
with ‹(y + z) * S = (- x) ^ p› ‹[x ≠ 0] (mod p)› show False
by (metis ‹prime p› cong_0_iff dvd_minus_iff prime_dvd_power_int prime_nat_int_transfer)
qed
from prod_is_some_powerE[OF coprime_commute[THEN iffD1, OF ‹coprime (y + z) S›]]
obtain α where ‹normalize S = α ^ p›
by (metis (no_types, lifting) ‹(y + z) * S = (- x) ^ p› mult.commute)
moreover from prod_is_some_powerE[OF ‹coprime (y + z) S› ‹(y + z) * S = (- x) ^ p›]
obtain a where ‹normalize (y + z) = a ^ p› by blast
ultimately have ‹S = (if 0 ≤ S then α ^ p else (- α) ^ p)›
‹y + z = (if 0 ≤ y + z then a ^ p else (- a) ^ p)›
by (metis ‹odd p› abs_of_nonneg abs_of_nonpos
add.inverse_inverse linorder_linear normalize_int_def power_minus_odd)+
thus ‹∃a α. y + z = a ^ p ∧ S = α ^ p› by meson
qed
subsection ‹The Theorem›
theorem Sophie_Germain_theorem :
‹∄x y z :: int. x ^ p + y ^ p = z ^ p ∧ [x ≠ 0] (mod p) ∧
[y ≠ 0] (mod p) ∧ [z ≠ 0] (mod p)› if SG : ‹SG p›
proof (rule ccontr)
from SophGer_primeD(1)[OF ‹SG p›] have odd_p : ‹odd p› .
from SG_simps.pos[OF ‹SG p›] have pos_p : ‹0 < p› .
assume ‹¬ (∄x y z. x ^ p + y ^ p = z ^ p ∧ [x ≠ 0] (mod int p) ∧
[y ≠ 0] (mod int p) ∧ [z ≠ 0] (mod int p))›
then obtain x y z :: int
where fermat : ‹x ^ p + y ^ p = z ^ p›
and not_cong_0 : ‹[x ≠ 0] (mod p)› ‹[y ≠ 0] (mod p)› ‹[z ≠ 0] (mod p)› by blast
let ?gcd = ‹Gcd {x, y, z}›
wlog coprime : ‹?gcd = 1› goal False generalizing x y z keeping fermat not_cong_0
using FLT_setwise_coprime_reduction_mod_version[OF fermat not_cong_0]
hypothesis by blast
have coprime_x_y : ‹coprime x y›
by (fact FLT_setwise_coprime_imp_pairwise_coprime
[OF SG_simps.nonzero[OF ‹SG p›] fermat coprime])
have coprime_y_z : ‹coprime y z›
proof (subst coprime_minus_right_iff[symmetric],
rule FLT_setwise_coprime_imp_pairwise_coprime[OF SG_simps.nonzero[OF ‹SG p›]])
from fermat ‹odd p› show ‹y ^ p + (- z) ^ p = (- x) ^ p› by simp
next
show ‹Gcd {y, - z, - x} = 1›
by (metis Gcd_insert coprime gcd_neg1_int insert_commute)
qed
have coprime_x_z : ‹coprime x z›
proof (subst coprime_minus_right_iff[symmetric],
rule FLT_setwise_coprime_imp_pairwise_coprime[OF SG_simps.nonzero[OF ‹SG p›]])
from fermat ‹odd p› show ‹x ^ p + (- z) ^ p = (- y) ^ p› by simp
next
show ‹Gcd {x, - z, - y} = 1›
by (metis Gcd_insert coprime gcd_neg1_int insert_commute)
qed
let ?q = ‹2 * p + 1›
have q_dvd_xyz : ‹?q dvd x ∨ ?q dvd y ∨ ?q dvd z›
proof (rule ccontr)
have cong_add_here : ‹[x ^ p = n1] (mod ?q) ⟹ [y ^ p = n2] (mod ?q) ⟹ [z ^ p = n3] (mod ?q) ⟹
[x ^ p + y ^ p + (- z) ^ p = n1 + n2 - n3] (mod ?q)› for n1 n2 n3
by (simp add: cong_add cong_diff ‹odd p›)
assume ‹¬ (?q dvd x ∨ ?q dvd y ∨ ?q dvd z)›
hence ‹¬ ?q dvd x› ‹¬ ?q dvd y› ‹¬ ?q dvd z› by simp_all
from this[THEN SG_simps.p_th_power_mod_q[OF ‹SG p›]] cong_add_here ‹odd p›
have ‹ [x ^ p + y ^ p + (- z) ^ p = - 3] (mod ?q) ∨ [x ^ p + y ^ p + (- z) ^ p = - 1] (mod ?q)
∨ [x ^ p + y ^ p + (- z) ^ p = 1] (mod ?q) ∨ [x ^ p + y ^ p + (- z) ^ p = 3] (mod ?q)› (is ?disj_congs)
by (elim disjE) fastforce+
moreover from fermat ‹odd p› have ‹[x ^ p + y ^ p + (- z) ^ p = 0] (mod ?q)› by simp
ultimately show False by (metis cong_def SG_simps.notcong_zero[OF ‹SG p›])
qed
wlog ‹?q dvd x› goal False generalizing x y z
keeping fermat not_cong_0 coprime_x_y coprime_y_z coprime_x_z q_dvd_xyz
proof -
from negation q_dvd_xyz have ‹?q dvd y ∨ ?q dvd z› by simp
thus False
proof (elim disjE)
assume ‹?q dvd y›
thus False
proof (rule hypothesis[OF _ _ not_cong_0(2, 1, 3)])
from fermat show ‹y ^ p + x ^ p = z ^ p› by linarith
next
show ‹coprime y x› ‹coprime x z› ‹coprime y z›
by (simp_all add: coprime_commute coprime_x_y coprime_x_z coprime_y_z)
next
from q_dvd_xyz show ‹?q dvd y ∨ ?q dvd x ∨ ?q dvd z› by linarith
qed
next
assume ‹?q dvd z›
hence ‹?q dvd - z› by simp
thus False
proof (rule hypothesis)
from fermat ‹odd p› show ‹(- z) ^ p + x ^ p = (- y) ^ p› by simp
next
from ‹[x ≠ 0] (mod p)› ‹[y ≠ 0] (mod p)› ‹[z ≠ 0] (mod p)›
show ‹[x ≠ 0] (mod p)› ‹[- y ≠ 0] (mod p)› ‹[- z ≠ 0] (mod p)›
by (simp_all add: cong_0_iff)
next
show ‹coprime (- z) x› ‹coprime x (- y)› ‹coprime (- z) (- y)›
by (simp_all add: coprime_commute coprime_x_y coprime_x_z coprime_y_z)
next
from q_dvd_xyz show ‹?q dvd - z ∨ ?q dvd x ∨ ?q dvd - y› by auto
qed
qed
qed
let ?S = ‹λy z. ∑k = 0..p - 1. (- z) ^ (p - 1 - k) * y ^ k›
from fermat ‹odd p› have ‹y ^ p + x ^ p + (- z) ^ p = 0›
‹x ^ p + y ^ p + (- z) ^ p = 0› ‹(-z ) ^ p + x ^ p + y ^ p = 0› by simp_all
from Sophie_Germain_lemma[OF SophGer_primeD(1-2)[OF ‹SG p›]
‹x ^ p + y ^ p + (- z) ^ p = 0› ‹[x ≠ 0] (mod p)›]
obtain a α where a_prop : ‹y + (- z) = a ^ p›
and α_prop : ‹?S y (-z) = α ^ p›
using coprime_minus_right_iff coprime_y_z by blast
from Sophie_Germain_lemma[OF SophGer_primeD(1-2)[OF ‹SG p›]
‹y ^ p + x ^ p + (- z) ^ p = 0› ‹[y ≠ 0] (mod p)›]
obtain b where b_prop : ‹x + - z = b ^ p›
by (metis coprime_minus_right_iff coprime_x_z)
from Sophie_Germain_lemma[OF SophGer_primeD(1-2)[OF ‹SG p›]
‹(-z ) ^ p + x ^ p + y ^ p = 0›] coprime_x_z ‹[z ≠ 0] (mod p)›
obtain c where c_prop : ‹x + y = c ^ p›
by (meson cong_0_iff coprime_x_y dvd_minus_iff)
from ‹?q dvd x› have ‹¬ ?q dvd y› and ‹¬ ?q dvd z›
using coprime_x_y coprime_x_z not_coprimeI not_prime_unit prime_nat_int_transfer
by (metis SophGer_primeD(3)[OF ‹SG p›] prime_nat_int_transfer)+
from b_prop ‹?q dvd x› have ‹[b ^ p = - z] (mod ?q)›
by (metis add_diff_cancel_right' cong_iff_dvd_diff)
with ‹¬ ?q dvd z› cong_dvd_iff dvd_minus_iff have ‹¬ ?q dvd b ^ p› by blast
with ‹0 < p› have ‹¬ ?q dvd b› by (meson dvd_power dvd_trans)
with SG_simps.p_th_power_mod_q[OF ‹SG p›]
have cong1 : ‹[b ^ p = 1] (mod ?q) ∨ [b ^ p = - 1] (mod ?q)› by blast
from c_prop ‹?q dvd x› have ‹[c ^ p = y] (mod ?q)›
by (metis add_diff_cancel_right' cong_iff_dvd_diff)
with ‹¬ ?q dvd y› cong_dvd_iff have ‹¬ ?q dvd c ^ p› by blast
with ‹0 < p› have ‹¬ ?q dvd c› by (meson dvd_power dvd_trans)
with SG_simps.p_th_power_mod_q[OF ‹SG p›]
have cong2 : ‹[c ^ p = 1] (mod ?q) ∨ [c ^ p = - 1] (mod ?q)› by blast
have ‹?q dvd a›
proof (rule ccontr)
have cong_add_here : ‹[b ^ p = n1] (mod ?q) ⟹ [c ^ p = n2] (mod ?q) ⟹ [a ^ p = n3] (mod ?q) ⟹
[b ^ p + c ^ p - a ^ p = n1 + n2 - n3] (mod ?q)› for n1 n2 n3
by (intro cong_add cong_diff)
assume ‹¬ ?q dvd a›
with SG_simps.p_th_power_mod_q[OF ‹SG p›]
have cong3 : ‹[a ^ p = 1] (mod ?q) ∨ [a ^ p = - 1] (mod ?q)› by blast
from cong1 cong2 cong3 cong_add_here
have ‹ [b ^ p + c ^ p - a ^ p = - 3] (mod ?q) ∨ [b ^ p + c ^ p - a ^ p = - 1] (mod ?q)
∨ [b ^ p + c ^ p - a ^ p = 1] (mod ?q) ∨ [b ^ p + c ^ p - a ^ p = 3] (mod ?q)› (is ?disj_congs)
by (elim disjE) fastforce+
have ‹b ^ p + c ^ p - a ^ p = 2 * x› by (fold a_prop b_prop c_prop) simp
also from ‹?q dvd x› cong_0_iff have ‹[2 * x = 0] (mod ?q)›
by (metis dvd_add_right_iff mult_2)
finally have ‹[b ^ p + c ^ p - a ^ p = 0] (mod ?q)› .
with ‹?disj_congs› show False by (metis cong_def SG_simps.notcong_zero[OF ‹SG p›])
qed
with oddE ‹odd p› have ‹?q dvd a ^ p› by fastforce
with a_prop have ‹[y = z] (mod ?q)› by (simp add: cong_iff_dvd_diff)
with cong_sym have ‹[z = y] (mod ?q)› by blast
have ‹α ^ p = ?S y (-z)› by (fact α_prop[symmetric])
also from SG_simps.nonzero[OF ‹SG p›] ‹[z = y] (mod ?q)› cong_minus_minus_iff
have ‹[?S y (-z) = p * y ^ (p - 1)] (mod ?q)›
by (blast intro: Sophie_Germain_lemma_computation_cong_simp)
finally have ‹[α ^ p = p * y ^ (p - 1)] (mod ?q)› .
from SG_simps.p_th_power_mod_q[OF ‹SG p› ‹¬ ?q dvd c ^ p›] ‹[c ^ p = y] (mod ?q)›
have ‹[y = 1] (mod ?q) ∨ [y = - 1] (mod ?q)› by (metis cong2 cong_def)
hence ‹[y ^ (p - 1) = 1] (mod ?q)›
by (elim disjE) (drule cong_pow[where n = ‹p - 1›], simp add: ‹odd p›)+
from cong_trans[OF ‹[α ^ p = p * y ^ (p - 1)] (mod ?q)› cong_mult[OF cong_refl this]]
have ‹[α ^ p = p] (mod ?q)› by simp
moreover from SG_simps.p_th_power_mod_q[OF ‹SG p›]
have ‹[α ^ p = - 1] (mod ?q) ∨ [α ^ p = 0] (mod ?q) ∨ [α ^ p = 1] (mod ?q)›
by (metis cong_0_iff cong_pow power_0_left)
ultimately show False by (metis SG_simps.notcong_p[OF ‹SG p›] cong_def)
qed
end