Theory Dvd_Int_Poly

(*  
    Author:      Sebastiaan Joosten
                 René Thiemann                  
    License:     BSD
*)

section ‹Division of Polynomials over Integers›

text ‹This theory contains an algorithm to efficiently compute
  divisibility of two integer polynomials.›

theory Dvd_Int_Poly
imports
  Polynomial_Interpolation.Ring_Hom_Poly
  Polynomial_Interpolation.Divmod_Int
  Polynomial_Interpolation.Is_Rat_To_Rat
begin

definition div_int_poly_step :: "int poly ⇒ int ⇒ (int poly × int poly) option ⇒ (int poly × int poly) option" where
 "div_int_poly_step q = (λa sro. case sro of Some (s, r) ⇒
      let ar = pCons a r; (b,m) = divmod_int (coeff ar (degree q)) (coeff q (degree q))
      in if m = 0 then Some (pCons b s, ar - smult b q) else None | None ⇒ None)"

declare div_int_poly_step_def[code_unfold]

definition div_mod_int_poly :: "int poly ⇒ int poly ⇒ (int poly × int poly) option" where
 "div_mod_int_poly p q = (if q = 0 then None
    else (let n = degree q; qn = coeff q n
    in fold_coeffs (div_int_poly_step q) p (Some (0, 0))))"

definition div_int_poly :: "int poly ⇒ int poly ⇒ int poly option" where
  "div_int_poly p q = 
    (case div_mod_int_poly p q of None ⇒ None | Some (d,m) ⇒ if m = 0 then Some d else None)"

definition div_rat_poly_step :: "'a::field poly ⇒ 'a ⇒ 'a poly × 'a poly ⇒ 'a poly × 'a poly" where
   "div_rat_poly_step q = (λa (s, r).
      let b = coeff (pCons a r) (degree q) / coeff q (degree q)
      in (pCons b s, pCons a r - smult b q))"

lemma foldr_cong_plus: (* a more elaborate version of foldr_cong. Using f'=id, g'=id and s = set lst would give foldr_cong exactly. *)
  assumes f_is_g : "⋀ a b c. b ∈ s ⟹ f' a = f b (f' c) ⟹ g' a = g b (g' c)" (* main assumption *)
      and f'_inj : "⋀ a b. f' a = f' b ⟹ a = b"
      and f_bit_sur : "⋀ a b c. f' a = f b c ⟹ ∃ c'. c = f' c'" (* should be provable by cases c *)
      and lst_in_s : "set lst ⊆ s" (* formulated like this to make induction easier *)
  shows "f' a = foldr f lst (f' b) ⟹ g' a = foldr g lst (g' b)"
using lst_in_s
proof (induct lst arbitrary: a)
  case (Cons x xs)
  have prems: "f' a = (f x ∘ foldr f xs) (f' b)" using Cons.prems unfolding foldr_Cons by auto
  hence "∃ c'. f' c' = foldr f xs (f' b)" using f_bit_sur by fastforce
  then obtain c' where c'_def: "f' c' = foldr f xs (f' b)" by blast
  hence "f' a = f x (f' c')" using prems by simp
  hence "g' a = g x (g' c')" using f_is_g Cons.prems(2) by simp
  also have "g' c' = foldr g xs (g' b)" using Cons.hyps[of c'] c'_def Cons.prems(2) by auto
  finally have "g' a = (g x ∘ foldr g xs) (g' b)" by simp
  thus ?case using foldr_Cons by simp
qed (insert f'_inj, auto)

abbreviation (input) rp :: "int poly ⇒ rat poly" where 
  "rp ≡ map_poly rat_of_int"

(* fully transitive proof, right to left also holds without the precondition: 
     int_step_then_rat_poly_step
   Left to right holds if q≠0: rat_poly_step_then_int_step *)
lemma rat_int_poly_step_agree :
  assumes "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0"
  shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1,rp c2)
         ⟷ Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))"
proof -
  have coeffs: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0" using assms by auto
  let ?ri = "rat_of_int"
  let ?withDiv1 = "pCons (?ri (coeff (pCons b c2) (degree q) div coeff q (degree q))) (rp c1)"
  let ?withSls1 = "pCons (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp c1)"
  let ?ident1 = "?withDiv1 = ?withSls1"
  let ?withDiv2 = "rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q)"
  let ?withSls2 = "pCons (?ri b) (rp c2) - smult (coeff (pCons (?ri b) (rp c2)) (degree q) / coeff (rp q) (degree q)) (rp q)"
  let ?ident2 = "?withDiv2 = ?withSls2"
  note simps = div_int_poly_step_def option.simps Let_def prod.simps
  have id1:"?ri (coeff (pCons b c2) (degree q) div coeff q (degree q)) = 
            ?ri (coeff (pCons b c2) (degree q)) / ?ri (coeff q (degree q))" using coeffs by auto
  have id2:"?ident1" unfolding id1
    by (simp, fold of_int_hom.coeff_map_poly_hom of_int_hom.map_poly_pCons_hom, simp)
  hence id3:"?ident2" using id2 by (auto simp: hom_distribs)

  have c1:"((rp (pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1)
            ,rp (pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q))
           = div_rat_poly_step (rp q) (?ri b) (rp c1,rp c2)) ⟷ (?ident1 ∧ ?ident2)"
    unfolding div_rat_poly_step_def simps
    by (simp add: hom_distribs)
  have "((rp a1, rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1, rp c2)) ⟷
             (rp a1 = ?withSls1 ∧ rp a2 = ?withSls2)"
    unfolding div_rat_poly_step_def simps by simp
  also have "… ⟷
      ((a1 = pCons (coeff (pCons b c2) (degree q) div coeff q (degree q)) c1) ∧
       (a2 = pCons b c2 - smult (coeff (pCons b c2) (degree q) div coeff q (degree q)) q))"
    by (fold id2 id3 of_int_hom.map_poly_pCons_hom, unfold of_int_poly_hom.eq_iff, auto)
  also have c0:"… ⟷ Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))" 
    unfolding divmod_int_def div_int_poly_step_def option.simps Let_def prod.simps
    using coeffs by (auto split: option.splits prod.splits if_splits)
  finally show ?thesis .
qed

lemma int_step_then_rat_poly_step :
  assumes Some:"Some (a1,a2) = div_int_poly_step q b (Some (c1,c2))"
  shows "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b (rp c1,rp c2)"
proof -
  note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps
  from Some[unfolded simps] have mod0: "coeff (pCons b c2) (degree q) mod coeff q (degree q) = 0" 
    by (auto split: option.splits prod.splits if_splits)
  thus ?thesis using assms rat_int_poly_step_agree by auto
qed

lemma is_int_rat_division : 
  assumes "y ≠ 0"
  shows "is_int_rat (rat_of_int x / rat_of_int y) ⟷ x mod y = 0"
proof
  assume "is_int_rat (rat_of_int x / rat_of_int y)"
  then obtain v where v_def:"rat_of_int v = rat_of_int x / rat_of_int y"
                using int_of_rat(2) is_int_rat by fastforce
  hence "v = ⌊rat_of_int x / rat_of_int y⌋" by linarith
  hence "v * y = x - x mod y" using div_is_floor_divide_rat mod_div_equality_int by simp
  hence "rat_of_int v * rat_of_int y = rat_of_int x - rat_of_int (x mod y)"
    by (fold hom_distribs, unfold of_int_hom.eq_iff)
  hence "(rat_of_int x / rat_of_int y) * rat_of_int y = rat_of_int x - rat_of_int (x mod y)"
    using v_def by simp
  hence "rat_of_int x = rat_of_int x - rat_of_int (x mod y)" by (simp add: assms)
  thus "x mod y = 0" by simp
qed (force)

lemma pCons_of_rp_contains_ints :
  assumes "rp a = pCons b c"
    shows "is_int_rat b"
proof -
  have "⋀ b n. rp a = b ⟹ is_int_rat (coeff b n)" by auto
  hence "rp a = pCons b c ⟹ is_int_rat (coeff (pCons b c) 0)".
  thus ?thesis using assms by auto
qed

lemma rat_step_then_int_poly_step :
  assumes "q ≠ 0"
      and "(rp a1,rp a2) = (div_rat_poly_step (rp q) ∘ rat_of_int) b2 (rp c1,rp c2)"
  shows "Some (a1,a2) = div_int_poly_step q b2 (Some (c1,c2))"
proof -
  let ?mustbeint = "rat_of_int (coeff (pCons b2 c2) (degree q)) / rat_of_int (coeff q (degree q))"
  let ?mustbeint2 = "coeff (pCons (rat_of_int b2) (rp c2)) (degree (rp q)) 
    / coeff (rp q) (degree (rp q))"
  have mustbeint : "?mustbeint = ?mustbeint2" by (fold hom_distribs of_int_hom.coeff_map_poly_hom, simp)
  note simps = div_int_poly_step_def option.simps Let_def divmod_int_def prod.simps
  from assms leading_coeff_neq_0[of q] have q0:"coeff q (degree q) ≠ 0" by simp

  have "rp a1 = pCons ?mustbeint2 (rp c1)"
    using assms(2) unfolding div_rat_poly_step_def by (simp add:div_int_poly_step_def Let_def)
  hence "is_int_rat ?mustbeint2"
    unfolding div_rat_poly_step_def using pCons_of_rp_contains_ints by simp
  hence "is_int_rat ?mustbeint" unfolding mustbeint by simp
  hence "coeff (pCons b2 c2) (degree q) mod coeff q (degree q) = 0"
    using is_int_rat_division q0 by simp
  thus ?thesis using rat_int_poly_step_agree assms by simp
qed

lemma div_int_poly_step_surjective : "Some a = div_int_poly_step q b c ⟹ ∃ c'. c = Some c'"
  unfolding div_int_poly_step_def by(cases c, simp_all)

lemma  div_mod_int_poly_then_pdivmod:
  assumes "div_mod_int_poly p q = Some (r,m)"
  shows   "(rp p div rp q, rp p mod rp q) = (rp r, rp m)"
    and   "q ≠ 0"
proof -
  let ?rpp = "(λ (a,b). (rp a,rp b))"
  let ?p = "rp p"
  let ?q = "rp q"
  let ?r = "rp r"
  let ?m = "rp m"
  let ?div_rat_step = "div_rat_poly_step ?q"
  let ?div_int_step = "div_int_poly_step q"
  from assms show q0 : "q ≠ 0" using div_mod_int_poly_def by auto
  hence "div_mod_int_poly p q = Some (r,m) ⟷ Some (r,m) = foldr (div_int_poly_step q) (coeffs p) (Some (0, 0))"
    unfolding div_mod_int_poly_def fold_coeffs_def by (auto split: option.splits prod.splits if_splits)
  hence innerRes: "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0, 0))" using assms by simp
  { fix oldRes res :: "int poly × int poly"
    fix lst :: "int list"
    have "Some res = foldr ?div_int_step lst (Some oldRes) ⟹
          ?rpp res = foldr (?div_rat_step ∘ rat_of_int) lst (?rpp oldRes)"
      using foldr_cong_plus[of "set lst" Some ?div_int_step ?rpp "?div_rat_step ∘ rat_of_int" 
        lst res oldRes] int_step_then_rat_poly_step div_int_poly_step_surjective by auto
    hence "Some res = foldr ?div_int_step lst (Some oldRes) 
      ⟹ ?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes)" 
      using foldr_map[of ?div_rat_step rat_of_int lst] by simp
  }
  hence equal_foldr : "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0)) 
    ⟹ ?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0))".
  have "(map rat_of_int (coeffs p) = coeffs ?p)" by simp
  hence "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))" using equal_foldr innerRes by simp
  thus "(?p div ?q, ?p mod ?q) = (?r,?m)" 
    using fold_coeffs_def [of "?div_rat_step" ?p] q0 
      div_mod_fold_coeffs [of ?p ?q]
    unfolding div_rat_poly_step_def by auto
qed

lemma div_rat_poly_step_sur:
 assumes "(case a of (a, b) ⇒ (rp a, rp b)) = (div_rat_poly_step (rp q) ∘ rat_of_int) x pair"
   shows "∃c'. pair = (case c' of (a, b) ⇒ (rp a, rp b))"
proof -
  obtain b1 b2 where pair: "pair = (b1, b2)" by (cases pair) simp
  define p12 where "p12 = coeff (pCons (rat_of_int x) b2) (degree (rp q)) / coeff (rp q) (degree (rp q))"
  obtain a1 a2 where "a = (a1, a2)" by (cases a) simp
  with assms pair have "(rp a1, rp a2) = div_rat_poly_step (rp q) (rat_of_int x) (b1, b2)"
    by simp    
  then have a1: "rp a1 = pCons p12 b1"
    and "rp a2 = pCons (rat_of_int x) b2 - smult p12 (rp q)"
    by (auto split: prod.splits simp add: Let_def div_rat_poly_step_def p12_def)
  then obtain p21 p22 where "rp p21 = pCons p22 b2"
    apply (simp add: field_simps)
    apply (metis coeff_pCons_0 of_int_hom.map_poly_hom_add of_int_hom.map_poly_hom_smult of_int_hom.coeff_map_poly_hom)
    done
  moreover obtain p21' p21q where "p21 = pCons p21' p21q"
    by (rule pCons_cases)
  ultimately obtain p2 where "b2 = rp p2 "
    by (auto simp: hom_distribs)
  moreover obtain a1' a1q where "a1 = pCons a1' a1q"
    by (rule pCons_cases)
  with a1 obtain p1 where "b1 = rp p1"
    by (auto simp: hom_distribs)
  ultimately have "pair = (rp p1, rp p2)" using pair by simp
  then show ?thesis by auto
qed

lemma  pdivmod_then_div_mod_int_poly:
  assumes q0: "q ≠ 0" and "(rp p div rp q, rp p mod rp q) = (rp r, rp m)" 
  shows   "div_mod_int_poly p q = Some (r,m)"
proof -
  let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *)
  let ?p = "rp p"
  let ?q = "rp q"
  let ?r = "rp r"
  let ?m = "rp m"
  let ?div_rat_step = "div_rat_poly_step ?q"
  let ?div_int_step = "div_int_poly_step q"
  { fix oldRes res :: "int poly × int poly"
    fix lst :: "int list"
    have inj: "(⋀a b. (case a of (a, b) ⇒ (rp a, rp b)) = (case b of (a, b) ⇒ (rp a, rp b)) ⟹ a = b)"
      by auto
    have "(⋀a b c. b ∈ set lst ⟹
              (case a of (a, b) ⇒ (map_poly rat_of_int a, map_poly rat_of_int b)) =
              (div_rat_poly_step (map_poly rat_of_int q) ∘ rat_of_int) b
               (case c of (a, b) ⇒ (map_poly rat_of_int a, map_poly rat_of_int b)) ⟹
              Some a = div_int_poly_step q b (Some c))"
      using rat_step_then_int_poly_step[OF q0] by auto
    hence "?rpp res = foldr (?div_rat_step ∘ rat_of_int) lst (?rpp oldRes)
          ⟹ Some res = foldr ?div_int_step lst (Some oldRes)"
      using foldr_cong_plus[of "set lst" ?rpp "?div_rat_step ∘ rat_of_int" Some ?div_int_step lst res oldRes]
            div_rat_poly_step_sur inj by simp
    hence "?rpp res = foldr ?div_rat_step (map rat_of_int lst) (?rpp oldRes)
       ⟹ Some res = foldr ?div_int_step lst (Some oldRes)"
       using foldr_map[of ?div_rat_step rat_of_int lst] by auto
  }
  hence equal_foldr : "?rpp (r,m) = foldr (?div_rat_step) (map rat_of_int (coeffs p)) (?rpp (0,0))
                   ⟹ Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))"
    by simp
  have "(?r,?m) = (foldr (?div_rat_step) (coeffs ?p) (0,0))"
    using fold_coeffs_def[of "?div_rat_step" ?p] assms
      div_mod_fold_coeffs [of ?p ?q]
    unfolding div_rat_poly_step_def by auto
  hence "Some (r,m) = foldr (?div_int_step) (coeffs p) (Some (0,0))"
    using equal_foldr by simp
  thus ?thesis using q0 unfolding div_mod_int_poly_def by (simp add: fold_coeffs_def)
qed

lemma div_int_then_rqp:
  assumes "div_int_poly p q = Some r"
  shows "r * q = p"
    and "q ≠ 0"
proof -
  let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *)
  let ?p = "rp p"
  let ?q = "rp q"
  let ?r = "rp r"
  have "Some (r,0) = div_mod_int_poly p q" using assms unfolding div_int_poly_def
      by (auto split:  option.splits prod.splits if_splits)
  with div_mod_int_poly_then_pdivmod[of p q r 0]
  have "?p div ?q = ?r ∧ ?p mod ?q = 0" by simp
  with div_mult_mod_eq[of ?p ?q]
  have "?p = ?r * ?q" by auto
  also have "… = rp (r * q)" by (simp add: hom_distribs)
  finally have "?p = rp (r * q)".
  thus "r * q = p" by simp
  show "q ≠ 0" using assms unfolding div_int_poly_def div_mod_int_poly_def
    by (auto split: option.splits prod.splits if_splits)
qed 

lemma rqp_then_div_int:
  assumes "r * q = p"
      and q0:"q ≠ 0"
  shows "div_int_poly p q = Some r"
proof -
  let ?rpp = "(λ (a,b). (rp a,rp b))" (* rp pair *)
  let ?p = "rp p"
  let ?q = "rp q"
  let ?r = "rp r"
  have "?p = ?r * ?q" using assms(1) by (auto simp: hom_distribs)
  hence "?p div ?q = ?r" and "?p mod ?q = 0"
    using q0 by simp_all
  hence "(rp p div rp q, rp p mod rp q) = (rp r, 0)" by (auto split: prod.splits)
  hence "(rp p div rp q, rp p mod rp q) = (rp r, rp 0)" by simp
  hence "Some (r,0) = div_mod_int_poly p q"
    using pdivmod_then_div_mod_int_poly[OF q0,of p r 0] by simp
  thus ?thesis unfolding div_mod_int_poly_def div_int_poly_def using q0 
    by (metis (mono_tags, lifting) option.simps(5) split_conv)
qed

lemma div_int_poly: "(div_int_poly p q = Some r) ⟷ (q ≠ 0 ∧ p = r * q)"
  using div_int_then_rqp rqp_then_div_int by blast

definition dvd_int_poly :: "int poly ⇒ int poly ⇒ bool" where
  "dvd_int_poly q p = (if q = 0 then p = 0 else div_int_poly p q ≠ None)"

lemma dvd_int_poly[simp]: "dvd_int_poly q p = (q dvd p)"
  unfolding dvd_def dvd_int_poly_def using div_int_poly[of p q]
  by (cases "q = 0", auto)

definition dvd_int_poly_non_0 :: "int poly ⇒ int poly ⇒ bool" where
  "dvd_int_poly_non_0 q p = (div_int_poly p q ≠ None)"

lemma dvd_int_poly_non_0[simp]: "q ≠ 0 ⟹ dvd_int_poly_non_0 q p = (q dvd p)"
  unfolding dvd_def dvd_int_poly_non_0_def using div_int_poly[of p q] by auto

lemma [code_unfold]: "p dvd q ⟷ dvd_int_poly p q" by simp

hide_const rp
end