Theory Residues_Properties
section ‹Properties of residues, congruences,
quadratic residues and the Legendre symbol›
theory Residues_Properties
imports "HOL-Number_Theory.Quadratic_Reciprocity"
begin
subsection ‹Properties of residues and congruences›
lemma mod_diff_eq_nat:
fixes a b m :: nat
assumes "a ≥ b"
shows "(a - b) mod m = (m + (a mod m) - (b mod m)) mod m"
proof cases
assume "m = 0"
thus ?thesis by auto
next
assume 0: "m ≠ 0"
have "(a - b) mod m = nat (int (a - b) mod int m)"
unfolding nat_mod_as_int by blast
also have "... = nat ((int a - int b) mod int m)"
using assms by (simp add: of_nat_diff)
also have "... = nat ((int a mod int m - int b mod int m) mod int m)"
using mod_diff_eq by metis
also have "... = nat ((int a mod int m + (int m - int b mod int m)) mod int m)"
by (metis add.left_commute add_uminus_conv_diff mod_add_self1)
also have "... = nat ((int (nat (int a mod int m)) +
(int m - int b mod int m)) mod int m)"
by (metis nat_int of_nat_mod)
also have "... = nat ((int (nat (int a mod int m)) +
int (m - nat (int b mod int m))) mod int m)"
by (metis 0 less_eq_nat.simps(1) mod_less_divisor
nat_int nat_less_le of_nat_diff zmod_int)
also have "... = nat (int (m + nat (int a mod int m) -
nat (int b mod int m)) mod int m)"
by (metis 0 Nat.add_diff_assoc add.commute bot_nat_0.not_eq_extremum
mod_less_divisor nat_less_le nat_mod_as_int of_nat_add)
also have "... = (m + (a mod m) - (b mod m)) mod m"
unfolding nat_mod_as_int by blast
finally show ?thesis .
qed
lemma prime_invertible_int:
fixes a p :: int
assumes "prime p"
assumes "¬ p dvd a"
shows "∃b. [a * b = 1] (mod p)"
using assms coprime_commute coprime_iff_invertible_int prime_imp_coprime by blast
lemma power_cong:
fixes x y a m :: nat
assumes "coprime a m"
assumes "[x = y] (mod totient m)"
shows "[a ^ x = a ^ y] (mod m)"
proof -
obtain k :: int where 0: "x + totient m * k = y"
using assms by (metis cong_iff_lin cong_int_iff)
show ?thesis
proof cases
assume "k ≥ 0"
hence "x + totient m * nat k = y"
using 0 by (metis int_eq_iff nat_int_add of_nat_mult)
hence "[a ^ x * (a ^ totient m) ^ nat k = a ^ y] (mod m)"
unfolding cong_def by (metis power_add power_mult)
hence "[a ^ x * (a ^ totient m mod m) ^ nat k = a ^ y] (mod m)"
unfolding cong_def by (metis mod_mult_right_eq power_mod)
hence "[a ^ x * (1 mod m) ^ nat k = a ^ y] (mod m)"
using euler_theorem[OF assms(1)] unfolding cong_def by argo
hence "[a ^ x * 1 ^ nat k = a ^ y] (mod m)"
unfolding cong_def by (metis mod_mult_right_eq power_mod)
thus "[a ^ x = a ^ y] (mod m)" by auto
next
assume "¬ k ≥ 0"
hence "x = y + totient m * nat (- k)"
using 0
by (smt (verit) int_nat_eq nat_int nat_minus_as_int of_nat_add of_nat_mult
right_diff_distrib')
hence "[a ^ x = a ^ y * (a ^ totient m) ^ nat (- k)] (mod m)"
unfolding cong_def by (metis power_add power_mult)
hence "[a ^ x = a ^ y * (a ^ totient m mod m) ^ nat (- k)] (mod m)"
unfolding cong_def by (metis mod_mult_right_eq power_mod)
hence "[a ^ x = a ^ y * (1 mod m) ^ nat (- k)] (mod m)"
using euler_theorem[OF assms(1)] unfolding cong_def by argo
hence "[a ^ x = a ^ y * 1 ^ nat (- k)] (mod m)"
unfolding cong_def by (metis mod_mult_right_eq power_mod)
thus "[a ^ x = a ^ y] (mod m)" by auto
qed
qed
lemma power_cong_alt:
fixes x a m :: nat
assumes "coprime a m"
shows "a ^ x mod m = a ^ (x mod totient m) mod m"
using power_cong[OF assms] cong_def cong_mod_left by blast
subsection ‹Properties of quadratic residues›
lemma QuadRes_cong:
fixes a b p :: int
assumes "[a = b] (mod p)"
assumes "QuadRes p a"
shows "QuadRes p b"
using assms cong_trans unfolding QuadRes_def by blast
lemma QuadRes_mult:
fixes a b p :: int
assumes "QuadRes p a"
assumes "QuadRes p b"
shows "QuadRes p (a * b)"
using assms
unfolding QuadRes_def
by (metis cong_mult mult.assoc mult.commute power2_eq_square)
lemma QuadRes_inv:
fixes a b p :: int
assumes "prime p"
assumes "[a * b = 1] (mod p)"
assumes "QuadRes p a"
shows "QuadRes p b"
proof -
have 0: "¬ p dvd a"
using assms
by (metis cong_dvd_iff dvd_mult2 not_prime_unit)
obtain x where 1: "[x⇧2 = a] (mod p)" using assms unfolding QuadRes_def by blast
have "¬ p dvd x" using 0 1 assms cong_dvd_iff pos2 prime_dvd_power_iff by blast
then obtain y where "[x * y = 1] (mod p)"
using assms prime_invertible_int by blast
hence 2: "[(x * y)⇧2 = 1] (mod p)" using cong_pow by fastforce
have "[x⇧2 * b = 1] (mod p)" using 1 assms cong_scalar_right cong_trans by blast
hence "[y⇧2 * (x⇧2 * b) = y⇧2 * 1] (mod p)" using cong_scalar_left by blast
hence "[(x * y)⇧2 * b = y⇧2] (mod p)" by (simp add: algebra_simps)
hence "[b = y⇧2] (mod p)"
using 2
by (metis cong_def cong_scalar_left mult.commute mult.right_neutral)
hence "[y⇧2 = b] (mod p)" by (rule cong_sym)
thus ?thesis unfolding QuadRes_def by blast
qed
subsection ‹Properties of the Legendre symbol›
lemma Legendre_cong:
fixes a b p :: int
assumes "[a = b] (mod p)"
shows "Legendre a p = Legendre b p"
using assms QuadRes_cong[of a b p] QuadRes_cong[of b a p]
unfolding Legendre_def cong_def
by auto
lemma Legendre_one:
fixes p :: int
assumes "p > 2"
shows "Legendre 1 p = 1"
using assms
by (smt (verit) Legendre_def QuadRes_def cong_def
cong_less_imp_eq_int one_power2)
lemma Legendre_minus_one:
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre (- 1) p = 1 ⟷ [p = 1] (mod 4)"
proof -
have "Legendre (- 1) p = 1 ⟷ [Legendre (- 1) p = 1] (mod p)"
using assms
by (metis Legendre_def QuadRes_def cong_0_iff cong_def not_prime_unit
one_power2)
also have "... ⟷ [(- 1) ^ ((nat p - 1) div 2) = 1] (mod p)"
using assms euler_criterion[of "nat p" "- 1"]
by (smt (verit) cong_def nat_0_le nat_one_as_int of_nat_add one_add_one
prime_int_nat_transfer zless_nat_eq_int_zless)
also have "... ⟷ ((- 1 :: int) ^ ((nat p - 1) div 2)) = 1"
using assms
by (simp add: cong_iff_dvd_diff minus_one_power_iff zdvd_not_zless)
also have "... ⟷ even ((nat p - 1) div 2)" by (simp add: minus_one_power_iff)
also have "... ⟷ 4 dvd (nat p - 1)"
using assms
by (metis One_nat_def add_Suc_right div_dvd_div even_Suc even_diff_nat
even_numeral even_of_nat group_cancel.rule0 nat_0_le
numeral_Bit0_div_2 prime_int_nat_transfer prime_odd_int)
also have "... ⟷ [p = 1] (mod 4)"
using assms
unfolding cong_iff_dvd_diff int_dvd_int_iff[symmetric]
by (simp add: int_ops)
finally show ?thesis .
qed
lemma Legendre_minus_one_alt:
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre (- 1) p = (if [p = 1] (mod 4) then 1 else - 1)"
using assms Legendre_minus_one[OF assms]
unfolding Legendre_def cong_def
by (auto simp add: zmod_minus1)
lemma Legendre_two:
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre 2 p = 1 ⟷ [p = 1] (mod 8) ∨ [p = 7] (mod 8)"
proof -
let ?n = "(p - 1) div 2 - (p - 1) div 4"
have "odd p" using assms prime_odd_int by blast
hence 0: "(∃k. p = 8 * k + 1) ∨ (∃k. p = 8 * k + 3) ∨
(∃k. p = 8 * k + 5) ∨ (∃k. p = 8 * k + 7)"
by presburger
have 1: "(j + 8 * k) div 4 = j div 4 + 2 * k" for k j :: int by linarith
have 2: "GAUSS (nat p) 2"
using assms unfolding GAUSS_def cong_def by auto
have "Legendre 2 p = (- 1) ^ card (GAUSS.E (nat p) 2)"
using assms GAUSS.gauss_lemma[OF 2] by auto
also have "... = (- 1) ^ card
((λk. k mod p) ` (*) 2 ` {0<..(p - 1) div 2} ∩ {(p - 1) div 2<..})"
unfolding GAUSS.E_def[OF 2] GAUSS.C_def[OF 2]
GAUSS.B_def[OF 2] GAUSS.A_def[OF 2]
by (simp add: algebra_simps)
also have "... = (- 1) ^ card
((*) 2 ` {0<..(p - 1) div 2} ∩ {(p - 1) div 2<..})"
by (rule arg_cong[of _ _ "λA. (- 1) ^ card (A ∩ {(p - 1) div 2<..})"]; force)
also have "... = (- 1) ^ card
{k ∈ (*) 2 ` {0<..(p - 1) div 2}. k > (p - 1) div 2}"
by (rule arg_cong[of _ _ "λA. (- 1) ^ card A"]; blast)
also have "... = (- 1) ^ card {k ∈ {0<..(p - 1) div 2}. 2 * k > (p - 1) div 2}"
apply (rule arg_cong[of _ _ "λn. (- 1) ^ n"])
apply (rule card_bij_eq[where ?f = "λk. k div 2" and ?g = "(*) 2"])
subgoal unfolding inj_on_def by auto
subgoal by auto
subgoal by (simp add: inj_on_mult)
subgoal by auto
subgoal by (rule finite_Collect_conjI; auto)
subgoal by (rule finite_Collect_conjI; auto)
done
also have "... = (- 1) ^ card {k ∈ {0<..(p - 1) div 2}. k > (p - 1) div 4}"
by (rule arg_cong[of _ _ "λf. (- 1) ^ card {k ∈ {0<..(p - 1) div 2}. f k}"];
auto)
also have "... = (- 1) ^ card {(p - 1) div 4<..(p - 1) div 2}"
by (rule arg_cong[of _ _ "λA. (- 1) ^ card A"]; fastforce)
also have "... = (- 1) ^ (nat ?n)" by auto
finally have "Legendre 2 p = 1 ⟷ even ?n"
unfolding minus_one_power_iff
by (simp add: assms even_nat_iff prime_gt_0_int zdiv_mono2)
also have "... ⟷ [p = 1] (mod 8) ∨ [p = 7] (mod 8)" unfolding cong_def
using 0 by (auto simp add: 1)
finally show ?thesis .
qed
lemma Legendre_two_alt:
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre 2 p = (if [p = 1] (mod 8) ∨ [p = 7] (mod 8) then 1 else - 1)"
using assms Legendre_two[OF assms]
unfolding Legendre_def cong_def
by (auto simp add: zmod_minus1)
lemma Legendre_mult:
fixes a b p :: int
assumes "prime p"
shows "Legendre (a * b) p = Legendre a p * Legendre b p"
proof cases
assume 0: "p = 2"
have 1: "QuadRes p = (λx. True)" using 0
by (metis QuadRes_def add_0 cong_iff_dvd_diff even_add odd_one power_one
power_zero_numeral uminus_add_conv_diff)
thus ?thesis using 0 unfolding 1 Legendre_def cong_0_iff by auto
next
assume "p ≠ 2"
hence 2: "p > 2" using assms by (simp add: order_less_le prime_ge_2_int)
have "[Legendre a p = a ^ ((nat p - 1) div 2)] (mod p)"
"[Legendre b p = b ^ ((nat p - 1) div 2)] (mod p)"
"[Legendre (a * b) p = (a * b) ^ ((nat p - 1) div 2)] (mod p)"
using 2 assms euler_criterion[of "nat p" a]
euler_criterion[of "nat p" b]
euler_criterion[of "nat p" "a * b"]
by auto
hence 3: "[Legendre (a * b) p = Legendre a p * Legendre b p] (mod p)"
by (smt (verit, best) cong_mult cong_sym cong_trans power_mult_distrib)
have 4: "{Legendre a p, Legendre b p, Legendre (a * b) p} ⊆ {-1, 0, 1}"
unfolding Legendre_def by auto
show ?thesis using 2 3 4 by (auto simp add: cong_iff_dvd_diff zdvd_not_zless)
qed
lemma Legendre_power:
fixes a :: int
fixes n :: nat
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre (a ^ n) p = (Legendre a p) ^ n"
proof (induct n)
case 0
thus ?case using assms Legendre_one by auto
next
case (Suc n)
thus ?case using assms Legendre_mult by auto
qed
lemma Legendre_prod:
fixes A :: "'a set"
fixes f :: "'a ⇒ int"
fixes p :: int
assumes "prime p"
assumes "p > 2"
shows "Legendre (prod f A) p = (∏x∈A. Legendre (f x) p)"
proof (induct A rule: infinite_finite_induct)
case (infinite A)
thus ?case using assms Legendre_one by auto
next
case empty
thus ?case using assms Legendre_one by auto
next
case (insert x F)
thus ?case using assms Legendre_mult by auto
qed
lemma Legendre_equal:
fixes p q :: int
assumes "prime p" "prime q"
assumes "p > 2" "q > 2"
assumes "p ≠ q"
assumes "[p = 1] (mod 4) ∨ [q = 1] (mod 4)"
shows "Legendre p q = Legendre q p"
proof -
have 0: "even (p - 1)" "even (q - 1)" using assms prime_odd_int by auto
have 1: "((p - 1) div 2) * ((q - 1) div 2) = (p - 1) * (q - 1) div 4"
using 0 by fastforce
have 2: "{Legendre p q, Legendre q p} ⊆ {-1, 0, 1}"
unfolding Legendre_def by auto
have "Legendre p q * Legendre q p =
(- 1) ^ nat (((p - 1) div 2) * ((q - 1) div 2))"
using assms Quadratic_Reciprocity_int[of p q]
by fastforce
also have "... = (- 1) ^ nat ((p - 1) * (q - 1) div 4)" unfolding 1 by rule
also have "... = 1"
using 0 assms even_nat_iff
unfolding minus_one_power_iff cong_iff_dvd_diff
by auto
finally show ?thesis using 2 by auto
qed
lemma Legendre_opposite:
fixes p q :: int
assumes "prime p" "prime q"
assumes "p > 2" "q > 2"
assumes "p ≠ q"
assumes "[p = 3] (mod 4) ∧ [q = 3] (mod 4)"
shows "Legendre p q = - Legendre q p"
proof -
have ‹[p - 1 = 2] (mod 4)› ‹[q - 1 = 2] (mod 4)›
using ‹[p = 3] (mod 4) ∧ [q = 3] (mod 4)›
by (simp_all add: cong_iff_dvd_diff)
from assms have ‹even (p - 1)› ‹even (q - 1)›
using assms by (auto dest: prime_odd_int)
then have *: "(p - 1) * (q - 1) div 4 = ((p - 1) div 2) * ((q - 1) div 2)"
by fastforce
have "odd ((p - 1) * (q - 1) div 4)"
using ‹even (p - 1)› ‹even (q - 1)› ‹[p - 1 = 2] (mod 4)› ‹[q - 1 = 2] (mod 4)›
by (auto elim!: oddE evenE dest: cong_dvd_iff simp add: *)
hence 2: "odd (nat ((p - 1) * (q - 1) div 4))"
using assms even_nat_iff pos_imp_zdiv_nonneg_iff by fastforce
have 3: "{Legendre p q, Legendre q p} ⊆ {-1, 0, 1}"
unfolding Legendre_def by auto
have "Legendre p q * Legendre q p =
(- 1) ^ nat (((p - 1) div 2) * ((q - 1) div 2))"
using assms Quadratic_Reciprocity_int[of p q]
by fastforce
also have "... = (- 1) ^ nat ((p - 1) * (q - 1) div 4)" unfolding * by rule
also have "... = - 1"
using 2 3
unfolding minus_one_power_iff
by auto
finally show ?thesis using 3 by auto
qed
end