Theory Legendre_Symbol

(*
  File:     Legendre_Symbol.thy
  Authors:  Daniel Stüwe

  Some more facts about the Legendre symbol that are missing from HOL-Number_Theory
*)
section ‹Additional Facts about the Legendre Symbol›
theory Legendre_Symbol
imports 
  "HOL-Number_Theory.Number_Theory"
begin

lemma basic_cong[simp]: 
  fixes p :: int
  assumes "2 < p"
  shows   "[-1   1] (mod p)"
          "[ 1  -1] (mod p)"
          "[ 0   1] (mod p)"
          "[ 1   0] (mod p)"
          "[ 0  -1] (mod p)"
          "[-1   0] (mod p)"
  using assms by (simp_all add: cong_iff_dvd_diff zdvd_not_zless)

lemma [simp]: "0 < n  (a mod 2) ^ n = a mod 2" for n :: nat and a :: int
 by (metis not_mod_2_eq_0_eq_1 power_one zero_power)

lemma Legendre_in_cong_eq: 
  fixes p :: int
  assumes "p > 2" and "b  {-1,0,1}"
  shows   "[Legendre a m = b] (mod p)  Legendre a m = b"
  using assms unfolding Legendre_def by auto

lemma Legendre_p_eq_2[simp]: "Legendre a 2 = a mod 2"  
  by (clarsimp simp: Legendre_def QuadRes_def cong_iff_dvd_diff) presburger

lemma Legendre_p_eq_1[simp]: "Legendre a 1 = 0" by (simp add: Legendre_def)

lemma euler_criterion_int:
  assumes "prime p" and "2 < p" 
  shows "[Legendre a p = a^((nat p-1) div 2)] (mod p)"
  using euler_criterion assms prime_int_nat_transfer
  by (metis int_nat_eq nat_numeral prime_gt_0_int zless_nat_conj) 

lemma QuadRes_neg[simp]: "QuadRes (-p) a = QuadRes p a" unfolding QuadRes_def by auto

lemma Legendre_neg[simp]: "Legendre a (-p) = Legendre a p" unfolding Legendre_def by auto

lemma Legendre_mult[simp]:
  assumes "prime p"
  shows "Legendre (a*b) p = Legendre a p * Legendre b p"
proof -
  consider "p = 2" | "p > 2"
    using assms order_le_less prime_ge_2_int by auto

  thus ?thesis proof (cases)
  case 1
    then show ?thesis
      by (metis Legendre_p_eq_2 mod_mult_eq mod_self mult_cancel_right2
                mult_eq_0_iff not_mod_2_eq_1_eq_0 one_mod_two_eq_one)
  next
  case 2
    hence "[Legendre (a*b) p = (a*b)^((nat p-1) div 2)] (mod p)"
      using euler_criterion_int assms by blast
  
    also have "[(a*b)^((nat p-1) div 2) = a^((nat p-1) div 2) * b^((nat p-1) div 2)] (mod p)"
      by (simp add: field_simps)
      
    also have "[a^((nat p-1) div 2) * b^((nat p-1) div 2) = Legendre a p * Legendre b p] (mod p)"
      using cong_sym[OF euler_criterion_int] assms 2 cong_mult by blast
  
    finally show ?thesis using Legendre_in_cong_eq[OF 2] by (simp add: Legendre_def)
  qed
qed

lemma QuadRes_mod[simp]: "p dvd n  QuadRes p (a mod n) = QuadRes p a"
  by (simp add: mod_mod_cancel QuadRes_def cong_def)

lemma Legendre_mod[simp]: "p dvd n  Legendre (a mod n) p = Legendre a p"
  by (simp add: mod_mod_cancel Legendre_def cong_def)

lemma two_cong_0_iff: "[2 = 0] (mod p)  p = 1  p = 2" for p :: nat
  unfolding cong_altdef_nat[of 0 2 p, simplified]
  using dvd_refl prime_nat_iff two_is_prime_nat by blast

lemma two_cong_0_iff_nat: "[2 = 0] (mod int p)  p = 1  p = 2"
  unfolding cong_iff_dvd_diff
  using two_is_prime_nat prime_nat_iff int_dvd_int_iff[of p 2]
  by auto

lemma two_cong_0_iff_int: "p > 0  [2 = 0] (mod p)  p = 1  p = 2" for p :: int
  by (metis of_nat_numeral pos_int_cases semiring_char_0_class.of_nat_eq_1_iff two_cong_0_iff_nat)

lemma QuadRes_2_2 [simp, intro]: "QuadRes 2 2"
  unfolding QuadRes_def
  unfolding cong_def
  by presburger

lemma Suc_mod_eq[simp]: "[Suc a = Suc b] (mod 2) = [a = b] (mod 2)"
  using Suc_eq_plus1_left cong_add_lcancel_nat by presburger

lemma div_cancel_aux: "c dvd a  (d + a * b) div c = (d div c) + a div c * b" for a b c :: nat
  by (metis div_plus_div_distrib_dvd_right dvd_div_mult dvd_trans dvd_triv_left)

corollary div_cancel_Suc: "c dvd a  1 < c  Suc (a * b) div c = a div c * b"
  using div_cancel_aux[where d = 1] by fastforce

lemma cong_aux_eq_1: "odd p  [(p - 1) div 2 - p div 4 = (p^2 - 1) div 8] (mod 2)" for p :: nat
proof (induction p rule: nat_less_induct)
  case (1 n)

  consider "n = 1" | "n > 1" using odd_pos[OF odd n] by linarith

  then show ?case proof (cases) 
    assume "n > 1"

    then obtain m where m: "m = n - 2" and m': "odd m" "m < n" using odd n by simp
    then obtain b where b: "m = 2 * b + 1" using oddE by blast
  
    have IH: "[(m - 1) div 2 - m div 4 = (m^2 - 1) div 8] (mod 2)" using "1.IH" m' by simp

    have [simp]: "n = 2 * b + 1 + 2" using m n > 1 b by auto

    have *: "(n2 - 1) div 8 = ((n - 2)2 - 1) div 8 + (n - 1) div 2"
      unfolding  power2_sum power2_eq_square by simp

    have "[(n - 1) div 2 - n div 4 = (n - 2 - 1) div 2 - (n - 2) div 4 + (n - 1) div 2] (mod 2)"
      by (rule cong_sym, cases "even b") (auto simp: cong_altdef_nat div_cancel_Suc elim: oddE)
    also have "[(n - 2 - 1) div 2 - (n - 2) div 4 + (n - 1) div 2 = (n2 - 1) div 8] (mod 2)"
        using IH cong_add_rcancel_nat unfolding * m by presburger
    finally show ?thesis . 
     
  qed simp
qed

lemma cong_2_pow[intro]: "(-1 :: int)^a = (-1)^b" if "[a = b] (mod 2)" for a b :: nat
proof -
  have "even a = even b"
    by (simp add: cong_dvd_iff that) 
  then show ?thesis by auto
qed

lemma card_Int: "card (A  B) = card A - card (A - B)" if "finite A"
  by (metis Diff_Diff_Int Diff_subset card_Diff_subset finite_Diff that)

text ‹Proofs are inspired by cite"Quadratic_Reciprocity".›

theorem supplement2_Legendre:
  fixes p :: int
  assumes "p > 2" "prime p"
  shows "Legendre 2 p = (-1) ^ (((nat p)^2 - 1) div 8)"
proof -
  interpret GAUSS "nat p" 2
    using assms
    unfolding GAUSS_def prime_int_nat_transfer
    by (simp add: two_cong_0_iff_int)

  have "card E = card ((λx. x * 2 mod p) `
          {0<..(p - 1) div 2}  {(p - 1) div 2<..})" (is "_ = card ?A")
    unfolding E_def C_def B_def A_def image_image using assms by simp
  also have "(λx. x * 2 mod p) ` {0<..(p - 1) div 2} = ((*) 2) ` {0<..(p - 1) div 2}"
    by (intro image_cong) auto
  also have "card (  {(p - 1) div 2<..}) =
               nat ((p - 1) div 2) - card ((*) 2 ` {0<..(p - 1) div 2} - {(p - 1) div 2<..})"
    using assms by (subst card_Int) (auto simp: card_image inj_onI)
  also have "card (((*) 2) ` {0<..(p - 1) div 2} - {(p - 1) div 2<..}) = card {0 <.. (p div 4)}"
    by (rule sym, intro bij_betw_same_card[of "(*) 2"] bij_betw_imageI inj_onI)
       (insert assms prime_odd_int[of p], auto simp: image_def elim!: oddE)
  also have " = nat p div 4" using assms by simp
  also have "nat ((p - 1) div 2) - nat p div 4 =  nat ((p - 1) div 2 - p div 4)"
    using assms by (simp add: nat_diff_distrib nat_div_distrib)
  finally have "card E = " .

  then have "Legendre 2 p = (-1) ^ nat ((p - 1) div 2 - p div 4)"
    using gauss_lemma assms by simp
  also have "nat ((p - 1) div 2 - p div 4) = (nat p - 1) div 2 - nat p div 4"
    using assms by (simp add: nat_div_distrib nat_diff_distrib)
  also have "(-1) ^  = ((-1) ^ (((nat p)^2 - 1) div 8) :: int)"
    using cong_aux_eq_1[of "nat p"] odd_p by blast 
  finally show ?thesis .
qed

theorem supplement1_Legendre:
  "prime p  2 < p  Legendre (-1) p = (-1)^((p-1) div 2)"
  using euler_criterion[of p "-1"] Legendre_in_cong_eq[symmetric, of p]
  by (simp add: minus_one_power_iff)

lemma QuadRes_1_right [intro, simp]: "QuadRes p 1"
  by (metis QuadRes_def cong_def power_one)

lemma Legendre_1_left [simp]: "prime p  Legendre 1 p = 1"
  by (auto simp add: Legendre_def cong_iff_dvd_diff not_prime_unit)

lemma cong_eq_0_not_coprime: "prime p  [a = 0] (mod p)  ¬coprime a p" for a p :: int
  unfolding cong_iff_dvd_diff prime_int_iff 
  by auto

lemma not_coprime_cong_eq_0: "prime p  ¬coprime a p  [a = 0] (mod p)" for a p :: int
  unfolding cong_iff_dvd_diff
  using prime_imp_coprime[of p a]
  by (auto simp: coprime_commute)

lemma prime_cong_eq_0_iff: "prime p  [a = 0] (mod p)  ¬coprime a p" for a p :: int
  using not_coprime_cong_eq_0[of p a] cong_eq_0_not_coprime[of p a]
  by auto

lemma Legendre_eq_0_iff [simp]: "prime p  Legendre a p = 0  ¬coprime a p"
  unfolding Legendre_def by (auto simp: prime_cong_eq_0_iff)

lemma Legendre_prod_mset [simp]: "prime p  Legendre (prod_mset M) p = (q∈#M. Legendre q p)"
  by (induction M) simp_all

lemma Legendre_0_eq_0[simp]: "Legendre 0 p = 0" unfolding Legendre_def by auto

lemma Legendre_values: "Legendre p q  {1, - 1, 0}"
  unfolding Legendre_def by auto

end