Theory Chinese_Remainder_Poly

(*
    Authors:      Jose Divasón
                  Sebastiaan Joosten
                  René Thiemann
                  Akihisa Yamada
*)
subsection ‹Chinese Remainder Theorem for Polynomials›

text ‹We prove the Chinese Remainder Theorem, and strengthen it by showing uniqueness›

theory Chinese_Remainder_Poly
imports
  "HOL-Number_Theory.Residues"  
  Polynomial_Factorization.Polynomial_Divisibility
  Polynomial_Interpolation.Missing_Polynomial
begin

lemma cong_add_poly:
  "[(a::'b::{field_gcd} poly) = b] (mod m) ⟹ [c = d] (mod m) ⟹ [a + c = b + d] (mod m)"
  by (fact cong_add)

lemma cong_mult_poly:
  "[(a::'b::{field_gcd} poly) = b] (mod m) ⟹ [c = d] (mod m) ⟹ [a * c = b * d] (mod m)"
  by (fact cong_mult)

lemma cong_mult_self_poly: "[(a::'b::{field_gcd} poly) * m = 0] (mod m)"
  by (fact cong_mult_self_right)

lemma cong_scalar2_poly: "[(a::'b::{field_gcd} poly)= b] (mod m) ⟹ [k * a = k * b] (mod m)"
  by (fact cong_scalar_left)

lemma cong_sum_poly:
    "(⋀x. x ∈ A ⟹ [((f x)::'b::{field_gcd} poly) = g x] (mod m)) ⟹
      [(∑x∈A. f x) = (∑x∈A. g x)] (mod m)"
  by (rule cong_sum)

lemma cong_iff_lin_poly: "([(a::'b::{field_gcd} poly) = b] (mod m)) = (∃k. b = a + m * k)"
  using cong_diff_iff_cong_0 [of b a m] by (auto simp add: cong_0_iff dvd_def algebra_simps dest: cong_sym)

lemma cong_solve_poly: "(a::'b::{field_gcd} poly) ≠ 0 ⟹ ∃x. [a * x = gcd a n] (mod n)"
proof (cases "n = 0")
  case True
  note n0=True
  show ?thesis
  proof (cases "monic a")
    case True
    have n: "normalize a = a" by (rule normalize_monic[OF True])
    show ?thesis
    by (rule exI[of _ 1], auto simp add: n0 n cong_def)
  next
    case False
    show ?thesis 
      by (auto simp add: True cong_def normalize_poly_old_def map_div_is_smult_inverse)
         (metis mult.right_neutral mult_smult_right) 
  qed
next
 case False
 note n_not_0 = False
 show ?thesis
   using bezout_coefficients_fst_snd [of a n, symmetric]
   by (auto simp add: cong_iff_lin_poly mult.commute [of a] mult.commute [of n])
qed


lemma cong_solve_coprime_poly: 
assumes coprime_an:"coprime (a::'b::{field_gcd} poly) n"
shows "∃x. [a * x = 1] (mod n)"
proof (cases "a = 0")
  case True
  show ?thesis unfolding cong_def
    using True coprime_an by auto
next
  case False  
  show ?thesis
    using coprime_an cong_solve_poly[OF False, of n]
    unfolding cong_def
    by presburger  
qed
  
lemma cong_dvd_modulus_poly:
  "[x = y] (mod m) ⟹ n dvd m ⟹ [x = y] (mod n)" for x y :: "'b::{field_gcd} poly"
  by (auto simp add: cong_iff_lin_poly elim!: dvdE)

lemma chinese_remainder_aux_poly:
  fixes A :: "'a set"
    and m :: "'a ⇒ 'b::{field_gcd} poly"
  assumes fin: "finite A"
    and cop: "∀i ∈ A. (∀j ∈ A. i ≠ j ⟶ coprime (m i) (m j))"
  shows "∃b. (∀i ∈ A. [b i = 1] (mod m i) ∧ [b i = 0] (mod (∏j ∈ A - {i}. m j)))"
proof (rule finite_set_choice, rule fin, rule ballI)
  fix i
  assume "i : A"
  with cop have "coprime (∏j ∈ A - {i}. m j) (m i)"
    by (auto intro: prod_coprime_left)
  then have "∃x. [(∏j ∈ A - {i}. m j) * x = 1] (mod m i)"
    by (elim cong_solve_coprime_poly)
  then obtain x where "[(∏j ∈ A - {i}. m j) * x = 1] (mod m i)"
    by auto
  moreover have "[(∏j ∈ A - {i}. m j) * x = 0]
    (mod (∏j ∈ A - {i}. m j))"
    by (subst mult.commute, rule cong_mult_self_poly)
  ultimately show "∃a. [a = 1] (mod m i) ∧ [a = 0]
      (mod prod m (A - {i}))"
    by blast
qed


(*The Chinese Remainder Theorem for polynomials: *)
lemma chinese_remainder_poly:
  fixes A :: "'a set"
    and m :: "'a ⇒ 'b::{field_gcd} poly"
    and u :: "'a ⇒ 'b poly"
  assumes fin: "finite A"
    and cop: "∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j))"
  shows "∃x. (∀i∈A. [x = u i] (mod m i))"
proof -
  from chinese_remainder_aux_poly [OF fin cop] obtain b where
    bprop: "∀i∈A. [b i = 1] (mod m i) ∧
      [b i = 0] (mod (∏j ∈ A - {i}. m j))"
    by blast
  let ?x = "∑i∈A. (u i) * (b i)"
  show "?thesis"
  proof (rule exI, clarify)
    fix i
    assume a: "i : A"
    show "[?x = u i] (mod m i)"
    proof -
      from fin a have "?x = (∑j ∈ {i}. u j * b j) +
          (∑j ∈ A - {i}. u j * b j)"
        by (subst sum.union_disjoint [symmetric], auto intro: sum.cong)
      then have "[?x = u i * b i + (∑j ∈ A - {i}. u j * b j)] (mod m i)"
        unfolding cong_def
        by auto
      also have "[u i * b i + (∑j ∈ A - {i}. u j * b j) =
                  u i * 1 + (∑j ∈ A - {i}. u j * 0)] (mod m i)"
        apply (rule cong_add_poly)
        apply (rule cong_scalar2_poly)
        using bprop a apply blast
        apply (rule cong_sum)
        apply (rule cong_scalar2_poly)
        using bprop apply auto
        apply (rule cong_dvd_modulus_poly)
        apply (drule (1) bspec)
        apply (erule conjE)
        apply assumption
        apply rule
        using fin a apply auto
        done
       thus ?thesis
       by (metis (no_types, lifting) a add.right_neutral fin mult_cancel_left1 mult_cancel_right1 
         sum.not_neutral_contains_not_neutral sum.remove)
    qed
  qed
qed


(*********************** Now we try to prove the uniqueness **********************)

lemma cong_trans_poly:
    "[(a::'b::{field_gcd} poly) = b] (mod m) ⟹ [b = c] (mod m) ⟹ [a = c] (mod m)"
  by (fact cong_trans)

lemma cong_mod_poly: "(n::'b::{field_gcd} poly) ~= 0 ⟹ [a mod n = a] (mod n)"
  by auto

lemma cong_sym_poly: "[(a::'b::{field_gcd} poly) = b] (mod m) ⟹ [b = a] (mod m)"
  by (fact cong_sym)

lemma cong_1_poly: "[(a::'b::{field_gcd} poly) = b] (mod 1)"
  by (fact cong_1)

lemma coprime_cong_mult_poly:
  assumes "[(a::'b::{field_gcd} poly) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
  shows "[a = b] (mod m * n)"
  using divides_mult assms
  by (metis (no_types, opaque_lifting) cong_dvd_modulus_poly cong_iff_lin_poly dvd_mult2 dvd_refl minus_add_cancel mult.right_neutral) 

lemma coprime_cong_prod_poly:
    "(∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j))) ⟹
      (∀i∈A. [(x::'b::{field_gcd} poly) = y] (mod m i)) ⟹
         [x = y] (mod (∏i∈A. m i))"
  apply (induct A rule: infinite_finite_induct)
    apply auto
  apply (metis coprime_cong_mult_poly prod_coprime_right)
  done

lemma cong_less_modulus_unique_poly:
    "[(x::'b::{field_gcd} poly) = y] (mod m) ⟹ degree x < degree m ⟹ degree y < degree m ⟹ x = y"
    by (simp add: cong_def mod_poly_less)


lemma chinese_remainder_unique_poly:
  fixes A :: "'a set"
    and m :: "'a ⇒ 'b::{field_gcd} poly"
    and u :: "'a ⇒ 'b poly"
  assumes nz: "∀i∈A. (m i) ≠ 0"
    and cop: "∀i∈A. (∀j∈A. i ≠ j ⟶ coprime (m i) (m j))"
    (*The following assumption should not be necessary, but I need it since in Isabelle 
      degree 0 is 0 instead of -∞*)
    and not_constant: "0 < degree (prod m A)" 
  shows "∃!x. degree x < (∑i∈A. degree (m i)) ∧ (∀i∈A. [x = u i] (mod m i))"
proof -
  from not_constant have fin: "finite A"
    by (metis degree_1 gr_implies_not0 prod.infinite)
  from chinese_remainder_poly [OF fin cop]
  obtain y where one: "(∀i∈A. [y = u i] (mod m i))"
    by blast
  let ?x = "y mod (∏i∈A. m i)"
  have degree_prod_sum: "degree (prod m A) = (∑i∈A. degree (m i))" 
    by (rule degree_prod_eq_sum_degree[OF nz])
  from fin nz have prodnz: "(∏i∈A. (m i)) ≠ 0"
     by auto
  (*This would hold without the premise not_constant if degree 0 = -∞*)
  have less: "degree ?x < (∑i∈A. degree (m i))" 
    unfolding degree_prod_sum[symmetric]
    using degree_mod_less[OF prodnz, of y]
    using not_constant
    by auto    
  have cong: "∀i∈A. [?x = u i] (mod m i)"
    apply auto
    apply (rule cong_trans_poly)
    prefer 2
    using one apply auto
    apply (rule cong_dvd_modulus_poly)
    apply (rule cong_mod_poly)
    using prodnz apply auto
    apply rule
    apply (rule fin)
    apply assumption
    done    
  have unique: "∀z. degree z < (∑i∈A. degree (m i)) ∧
      (∀i∈A. [z = u i] (mod m i)) ⟶ z = ?x"
  proof (clarify)
    fix z::"'b poly"
    assume zless: "degree z < (∑i∈A. degree (m i))"
    assume zcong: "(∀i∈A. [z = u i] (mod m i))"   
    have deg1: "degree z < degree (prod m A)"
      using degree_prod_sum zless by simp
    have deg2: "degree ?x < degree (prod m A)"
      by (metis deg1 degree_0 degree_mod_less gr0I gr_implies_not0)
    have "∀i∈A. [?x = z] (mod m i)"
      apply clarify
      apply (rule cong_trans_poly)
      using cong apply (erule bspec)
      apply (rule cong_sym_poly)
      using zcong by auto
    with fin cop have "[?x = z] (mod (∏i∈A. m i))"
      by (intro coprime_cong_prod_poly) auto
    with zless  show "z = ?x"
      apply (intro cong_less_modulus_unique_poly)
      apply (erule cong_sym_poly)
      apply (auto simp add:  deg1 deg2)
      done
  qed
  from less cong unique show ?thesis by blast
qed

end