# Theory Chinese_Remainder_Poly

```(*
Authors:      Jose Divasón
Sebastiaan Joosten
René Thiemann
*)
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

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

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_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"

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
```