Theory QuadRes

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

  Some facts about Quadratic Residues that are missing from the library
*)
section ‹Additional Material on Quadratic Residues›
theory QuadRes
imports 
  Jacobi_Symbol
  Algebraic_Auxiliaries
begin

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

lemma inj_on_QuadRes:
  fixes p :: int
  assumes "prime p"
  shows "inj_on (λx. x^2 mod p) {0..(p-1) div 2}"
proof 
  fix x y :: int
  assume elem: "x ∈ {0..(p-1) div 2}" "y ∈ {0..(p-1) div 2}"

  have * : "abs(a) < p ⟹ p dvd a ⟹ a = 0" for a :: int
    using dvd_imp_le_int by force

  assume "x2 mod p = y2 mod p"

  hence "[x2 = y2] (mod p)" unfolding cong_def .

  hence "p dvd (x2 - y2)" by (simp add: cong_iff_dvd_diff)

  hence "p dvd (x + y) * (x - y)" 
    by (simp add: power2_eq_square square_diff_square_factored) 
  
  hence "p dvd (x + y) ∨ p dvd (x - y)"
    using ‹prime p› by (simp add: prime_dvd_mult_iff) 

  moreover have "p dvd x + y ⟹ x + y = 0" "p dvd x - y ⟹ x - y = 0" 
           and "0 ≤ x" "0 ≤ y"
      using elem  
      by (fastforce intro!: * )+
  
  ultimately show "x = y" by auto
qed

lemma QuadRes_set_prime: 
  assumes "prime p" and "odd p"
  shows "{x . QuadRes p x ∧ x ∈ {0..<p}} = {x^2 mod p | x . x ∈ {0..(p-1) div 2}}"
proof(safe, goal_cases)
  case (1 x)
  then obtain y where "[y2 = x] (mod p)" 
    unfolding QuadRes_def by blast

  then have A: "[(y mod p)2 = x] (mod p)" 
    unfolding cong_def
    by (simp add: power_mod)

  then have "[(-(y mod p))2 = x] (mod p)" 
    by simp

  then have B: "[(p - (y mod p))2 = x] (mod p)" 
    unfolding cong_def 
    using minus_mod_self1
    by (metis power_mod)

  have "p = 1 + ((p - 1) div 2) * 2"
    using prime_gt_0_int[OF ‹prime p›] ‹odd p›
    by simp

  then have C: "(p - (y mod p)) ∈ {0..(p - 1) div 2} ∨ y mod p ∈ {0..(p - 1) div 2}"
    using prime_gt_0_int[OF ‹prime p›] 
    by (clarsimp, auto simp: le_less)

  then show ?case proof
    show ?thesis if "p - y mod p ∈ {0..(p - 1) div 2}"
      using that B
      unfolding cong_def
      using ‹x ∈ {0..<p}› by auto

    show ?thesis if "y mod p ∈ {0..(p - 1) div 2}"
      using that A
      unfolding cong_def
      using ‹x ∈ {0..<p}› by auto
  qed
qed (auto simp: QuadRes_def cong_def)

corollary QuadRes_iff: 
  assumes "prime p" and "odd p"
  shows "(QuadRes p x ∧ x ∈ {0..<p}) ⟷ (∃ a ∈ {0..(p-1) div 2}. a^2 mod p = x)"
proof -
  have "(QuadRes p x ∧ x ∈ {0..<p}) ⟷ x ∈ {x. QuadRes p x ∧ x ∈ {0..<p}}"
    by auto
  also note QuadRes_set_prime[OF assms]
  also have "(x ∈ {x2 mod p |x. x ∈ {0..(p - 1) div 2}}) = (∃a∈{0..(p - 1) div 2}. a2 mod p = x)"
    by blast
  finally show ?thesis .
qed

corollary card_QuadRes_set_prime:
  fixes p :: int
  assumes "prime p" and "odd p"
  shows "card {x. QuadRes p x ∧ x ∈ {0..<p}} = nat (p+1) div 2"
proof -
  have "card {x. QuadRes p x ∧ x ∈ {0..<p}} = card {x2 mod p | x . x ∈ {0..(p-1) div 2}}"
    unfolding QuadRes_set_prime[OF assms] ..

  also have "{x2 mod p | x . x ∈ {0..(p-1) div 2}} = (λx. x2 mod p) ` {0..(p-1) div 2}"
    by auto

  also have "card ... = card {0..(p-1) div 2}"
    using inj_on_QuadRes[OF ‹prime p›] by (rule card_image)

  also have "... = nat (p+1) div 2" by simp

  finally show ?thesis .
qed

corollary card_not_QuadRes_set_prime:
  fixes p :: int
  assumes "prime p" and "odd p"
  shows "card {x. ¬QuadRes p x ∧ x ∈ {0..<p}} = nat (p-1) div 2"
proof -
  have "{0..<p} ∩ {x. QuadRes p x ∧ x ∈ {0..<p}} = {x. QuadRes p x ∧ x ∈ {0..<p}}"
    by blast

  moreover have "nat p - nat (p + 1) div 2 = nat (p - 1) div 2"
    using ‹odd p› prime_gt_0_int[OF ‹prime p›]
    by (auto elim!: oddE simp: nat_add_distrib nat_mult_distrib)

  ultimately have "card {0..<p} - card ({0..<p} ∩ {x. QuadRes p x ∧ x ∈ {0..<p}}) = nat (p - 1) div 2"
    using card_QuadRes_set_prime[OF assms] and card_atLeastZeroLessThan_int by presburger    

  moreover have "{x. ¬QuadRes p x ∧ x ∈ {0..<p}} = {0..<p} - {x. QuadRes p x ∧ x ∈ {0..<p}}"
    by blast

  ultimately show ?thesis by (auto simp add: card_Diff_subset_Int)
qed

lemma not_QuadRes_ex_if_prime:
  assumes "prime p" and "odd p"
  shows "∃ x. ¬QuadRes p x"
proof -
  have "2 < p" using odd_prime_gt_2_int assms by blast

  then have False if "{x . ¬QuadRes p x ∧ x ∈ {0..<p}} = {}"
    using card_not_QuadRes_set_prime[OF assms]
    unfolding that
    by simp

  thus ?thesis by blast
qed

lemma not_QuadRes_ex:
  "1 < p ⟹ odd p ⟹ ∃x. ¬QuadRes p x"
proof (induction p rule: prime_divisors_induct)
  case (factor p x)
  then show ?case 
    by (meson not_QuadRes_ex_if_prime QuadRes_def cong_iff_dvd_diff dvd_mult_left even_mult_iff)
qed simp_all

end