Theory Finite_Fields.Formal_Polynomial_Derivatives

section ‹Formal Derivatives\label{sec:pderiv}›

theory Formal_Polynomial_Derivatives
  imports "HOL-Algebra.Polynomial_Divisibility" "Ring_Characteristic"
begin

definition pderiv (‹pderivı›) where
  "pderiv⇘R⇙ x = ring.normalize R (
    map (λi. int_embed R i ⊗⇘R⇙ ring.coeff R x i) (rev [1..<length x]))"

context domain
begin

lemma coeff_range:
  assumes "subring K R"
  assumes "f ∈ carrier (K[X])"
  shows "coeff f i ∈ K"
proof -
  have "coeff f i ∈ set f ∪ {𝟬}"
    using coeff_img(3) by auto
  also have "... ⊆ K ∪ {𝟬}"
    using assms(2) univ_poly_carrier polynomial_incl by blast
  also have "... ⊆ K"
    using subringE[OF assms(1)] by simp
  finally show ?thesis by simp
qed

lemma pderiv_carr:
  assumes "subring K R"
  assumes "f ∈ carrier (K[X])"
  shows "pderiv f ∈ carrier (K[X])"
proof -
  have "int_embed R i ⊗ coeff f i ∈ K" for i
    using coeff_range[OF assms] int_embed_range[OF assms(1)]
    using subringE[OF assms(1)] by simp
  hence "polynomial K (pderiv f)"
    unfolding pderiv_def by (intro normalize_gives_polynomial, auto)
  thus ?thesis
    using univ_poly_carrier by auto
qed

lemma pderiv_coeff:
  assumes "subring K R"
  assumes "f ∈ carrier (K[X])"
  shows "coeff (pderiv f) k = int_embed R (Suc k) ⊗ coeff f (Suc k)"
    (is "?lhs = ?rhs")
proof (cases "k + 1  < length f")
  case True
  define j where "j = length f - k - 2"
  define d where
    "d = map (λi. int_embed R i ⊗ coeff f i) (rev [1..<length f])"

  have a: "j+1 < length f"
    using True unfolding j_def by simp
  hence b: "j < length [1..<length f]"
    by simp
  have c: "k < length d"
    unfolding d_def using True by simp
  have d: "degree d - k = j"
    unfolding d_def j_def by simp
  have e: "rev [Suc 0..<length f] ! j = length f - 1 - j"
    using b  by (subst rev_nth, auto)
  have f: "length f - j - 1 = k+1"
    unfolding j_def using True by simp

  have "coeff (pderiv f ) k = coeff (normalize d) k"
    unfolding pderiv_def d_def by simp
  also have "... = coeff d k"
    using normalize_coeff by simp
  also have "... = d ! j"
    using c d by (subst coeff_nth, auto)
  also have
    "... = int_embed R (length f - j - 1) ⊗ coeff f (length f - j - 1)"
    using b e unfolding d_def by simp
  also have "... = ?rhs"
    using f by simp
  finally show ?thesis by simp
next
  case False
  hence "Suc k ≥ length f"
    by simp
  hence a:"coeff f (Suc k) = 𝟬"
    using coeff_img by blast
  have b:"coeff (pderiv f) k = 𝟬"
    unfolding pderiv_def normalize_coeff[symmetric] using False
    by (intro coeff_length, simp)
  show ?thesis
    using int_embed_range[OF carrier_is_subring] by (simp add:a b)
qed

lemma pderiv_const:
  assumes "degree x = 0"
  shows "pderiv x = 𝟬⇘K[X]⇙"
proof (cases "length x = 0")
  case True
  then show ?thesis by (simp add:univ_poly_zero pderiv_def)
next
  case False
  hence "length x = 1" using assms by linarith
  then obtain y where "x = [y]" by (cases x, auto)
  then show ?thesis by (simp add:univ_poly_zero pderiv_def)
qed

lemma pderiv_var:
  shows "pderiv X = 𝟭⇘K[X]⇙"
  unfolding var_def pderiv_def
  by (simp add:univ_poly_one int_embed_def)

lemma pderiv_zero:
  shows "pderiv 𝟬⇘K[X]⇙ = 𝟬⇘K[X]⇙"
  unfolding pderiv_def univ_poly_zero by simp

lemma pderiv_add:
  assumes "subring K R"
  assumes [simp]: "f ∈ carrier (K[X])" "g ∈ carrier (K[X])"
  shows "pderiv (f ⊕⇘K[X]⇙ g) = pderiv f ⊕⇘K[X]⇙ pderiv g"
    (is "?lhs = ?rhs")
proof -
  interpret p: ring "(K[X])"
    using univ_poly_is_ring[OF assms(1)] by simp

  let ?n = "(λi. int_embed R i)"

  have a[simp]:"?n k ∈ carrier R" for k
    using int_embed_range[OF carrier_is_subring] by auto
  have b[simp]:"coeff f k ∈ carrier R" if "f ∈ carrier (K[X])" for k f
    using coeff_range[OF assms(1)] that
    using subringE(1)[OF assms(1)] by auto

  have "coeff ?lhs i = coeff ?rhs i" for i
  proof -
    have "coeff ?lhs i = ?n (i+1) ⊗ coeff (f ⊕⇘K [X]⇙ g) (i+1)"
      by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = ?n (i+1) ⊗ (coeff f (i+1) ⊕ coeff g (i+1))"
      by (subst coeff_add[OF assms], simp)
    also have "... = ?n (i+1) ⊗ coeff f (i+1)
      ⊕ int_embed R (i+1) ⊗ coeff g (i+1)"
      by (subst r_distr, simp_all)
    also have "... = coeff (pderiv f) i ⊕ coeff (pderiv g) i"
      by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = coeff (pderiv f ⊕⇘K [X]⇙ pderiv g) i"
      using pderiv_carr[OF assms(1)]
      by (subst coeff_add[OF assms(1)], auto)
    finally show ?thesis by simp
  qed
  hence "coeff ?lhs = coeff ?rhs" by auto
  thus "?lhs = ?rhs"
    using pderiv_carr[OF assms(1)]
    by (subst coeff_iff_polynomial_cond[where K="K"])
      (simp_all add:univ_poly_carrier)+
qed

lemma pderiv_inv:
  assumes "subring K R"
  assumes [simp]: "f ∈ carrier (K[X])"
  shows "pderiv (⊖⇘K[X]⇙ f) = ⊖⇘K[X]⇙ pderiv f" (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(1)] by simp

  have "pderiv (⊖⇘K[X]⇙ f) = pderiv (⊖⇘K[X]⇙ f) ⊕⇘K[X]⇙ 𝟬⇘K[X]⇙"
    using pderiv_carr[OF assms(1)]
    by (subst p.r_zero, simp_all)
  also have "... = pderiv (⊖⇘K[X]⇙ f) ⊕⇘K[X]⇙ (pderiv f ⊖⇘K[X]⇙ pderiv f)"
    using pderiv_carr[OF assms(1)] by simp
  also have "... = pderiv (⊖⇘K[X]⇙ f) ⊕⇘K[X]⇙ pderiv f ⊖⇘K[X]⇙ pderiv f"
    using pderiv_carr[OF assms(1)]
    unfolding a_minus_def by (simp add:p.a_assoc)
  also have "... = pderiv (⊖⇘K[X]⇙ f ⊕⇘K[X]⇙ f) ⊖⇘K[X]⇙ pderiv f"
    by (subst pderiv_add[OF assms(1)], simp_all)
  also have "... = pderiv 𝟬⇘K[X]⇙ ⊖⇘K[X]⇙ pderiv f"
    by (subst p.l_neg, simp_all)
  also have "... = 𝟬⇘K[X]⇙ ⊖⇘K[X]⇙ pderiv f"
    by (subst pderiv_zero, simp)
  also have "... = ⊖⇘K[X]⇙ pderiv f"
    unfolding a_minus_def using pderiv_carr[OF assms(1)]
    by (subst p.l_zero, simp_all)
  finally show "pderiv (⊖⇘K[X]⇙ f) = ⊖⇘K[X]⇙ pderiv f"
    by simp
qed


lemma coeff_mult:
  assumes "subring K R"
  assumes "f ∈ carrier (K[X])" "g ∈ carrier (K[X])"
  shows "coeff (f ⊗⇘K[X]⇙ g) i =
    (⨁ k ∈ {..i}. (coeff f) k ⊗ (coeff g) (i - k))"
proof -
  have a:"set f ⊆ carrier R"
    using assms(1,2) univ_poly_carrier
    using subringE(1)[OF assms(1)] polynomial_incl by blast
  have b:"set g ⊆ carrier R"
    using assms(1,3) univ_poly_carrier
    using subringE(1)[OF assms(1)] polynomial_incl by blast
  show ?thesis
    unfolding univ_poly_mult poly_mult_coeff[OF a b] by simp
qed

lemma pderiv_mult:
  assumes "subring K R"
  assumes [simp]: "f ∈ carrier (K[X])" "g ∈ carrier (K[X])"
  shows "pderiv (f ⊗⇘K[X]⇙ g) =
    pderiv f ⊗⇘K[X]⇙ g ⊕⇘K[X]⇙ f ⊗⇘K[X]⇙ pderiv g"
    (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(1)] by simp

  let ?n = "(λi. int_embed R i)"

  have a[simp]:"?n k ∈ carrier R" for k
    using int_embed_range[OF carrier_is_subring] by auto
  have b[simp]:"coeff f k ∈ carrier R" if "f ∈ carrier (K[X])" for k f
    using coeff_range[OF assms(1)]
    using subringE(1)[OF assms(1)] that by auto

  have "coeff ?lhs i = coeff ?rhs i" for i
  proof -
    have "coeff ?lhs i = ?n (i+1) ⊗ coeff (f ⊗⇘K [X]⇙ g) (i+1)"
      using assms(2,3) by (simp add: pderiv_coeff[OF assms(1)])
    also have "... = ?n (i+1) ⊗
      (⨁k ∈ {..i+1}. coeff f k ⊗ (coeff g (i + 1 - k)))"
      by (subst coeff_mult[OF assms], simp)
    also have "... =
      (⨁k ∈ {..i+1}. ?n (i+1) ⊗ (coeff f k ⊗ coeff g (i + 1 - k)))"
      by (intro finsum_rdistr, simp_all add:Pi_def)
    also have "... =
      (⨁k ∈ {..i+1}. ?n k ⊗ (coeff f k ⊗ coeff g (i + 1 - k)) ⊕
      ?n (i+1-k) ⊗ (coeff f k ⊗ coeff g (i + 1 - k)))"
      using int_embed_add[symmetric] of_nat_diff
      by (intro finsum_cong')
        (simp_all add:l_distr[symmetric] of_nat_diff)
    also have "... =
      (⨁k ∈ {..i+1}. ?n k ⊗ coeff f k ⊗ coeff g (i + 1 - k) ⊕
      coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i + 1 - k)))"
      using Pi_def a b m_assoc m_comm
      by (intro finsum_cong' arg_cong2[where f="(⊕)"], simp_all)
    also have "... =
      (⨁k ∈ {..i+1}. ?n k ⊗ coeff f k ⊗ coeff g (i+1-k)) ⊕
      (⨁k ∈ {..i+1}. coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i+1-k)))"
      by (subst finsum_addf[symmetric], simp_all add:Pi_def)
    also have "... =
      (⨁k∈insert 0 {1..i+1}. ?n k ⊗ coeff f k ⊗ coeff g (i+1-k)) ⊕
      (⨁k∈insert (i+1) {..i}. coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i+1-k)))"
      using subringE(1)[OF assms(1)]
      by (intro arg_cong2[where f="(⊕)"] finsum_cong')
        (auto simp:set_eq_iff)
    also have "... =
      (⨁k ∈ {1..i+1}. ?n k ⊗ coeff f k ⊗ coeff g (i+1-k)) ⊕
      (⨁k ∈ {..i}. coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i+1-k)))"
      by (subst (1 2) finsum_insert, auto simp add:int_embed_zero)
    also have "... =
      (⨁k ∈ Suc ` {..i}. ?n k ⊗ coeff f (k) ⊗ coeff g (i+1-k)) ⊕
      (⨁k ∈ {..i}. coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i+1-k)))"
      by (intro arg_cong2[where f="(⊕)"] finsum_cong')
        (simp_all add:Pi_def atMost_atLeast0)
    also have "... =
      (⨁k ∈ {..i}. ?n (k+1) ⊗ coeff f (k+1) ⊗ coeff g (i-k)) ⊕
      (⨁k ∈ {..i}. coeff f k ⊗ (?n (i+1-k) ⊗ coeff g (i+1-k)))"
      by (subst finsum_reindex, auto)
    also have "... =
      (⨁k ∈ {..i}. coeff (pderiv f) k ⊗ coeff g (i-k)) ⊕
      (⨁k ∈ {..i}. coeff f k ⊗ coeff (pderiv g) (i-k))"
      using Suc_diff_le
      by (subst (1 2) pderiv_coeff[OF assms(1)])
        (auto intro!: finsum_cong')
    also have "... =
      coeff (pderiv f ⊗⇘K[X]⇙ g) i ⊕ coeff (f ⊗⇘K[X]⇙ pderiv g) i"
      using pderiv_carr[OF assms(1)]
      by (subst (1 2) coeff_mult[OF assms(1)], auto)
    also have "... = coeff ?rhs i"
      using pderiv_carr[OF assms(1)]
      by (subst coeff_add[OF assms(1)], auto)
    finally show ?thesis by simp
  qed

  hence "coeff ?lhs = coeff ?rhs" by auto
  thus "?lhs = ?rhs"
    using pderiv_carr[OF assms(1)]
    by (subst coeff_iff_polynomial_cond[where K="K"])
     (simp_all add:univ_poly_carrier)
qed

lemma pderiv_pow:
  assumes "n > (0 :: nat)"
  assumes "subring K R"
  assumes [simp]: "f ∈ carrier (K[X])"
  shows "pderiv (f [^]⇘K[X]⇙ n) =
    int_embed (K[X]) n ⊗⇘K[X]⇙ f [^]⇘K[X]⇙ (n-1) ⊗⇘K[X]⇙ pderiv f"
    (is "?lhs = ?rhs")
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(2)] by simp

  let ?n = "λn. int_embed (K[X]) n"

  have [simp]: "?n i ∈ carrier (K[X])" for i
    using p.int_embed_range[OF p.carrier_is_subring] by simp

  obtain m where n_def: "n = Suc m" using assms(1) lessE by blast
  have "pderiv (f [^]⇘K[X]⇙ (m+1)) =
    ?n (m+1) ⊗⇘K[X]⇙ f [^]⇘K[X]⇙ m ⊗⇘K[X]⇙ pderiv f"
  proof (induction m)
    case 0
    then show ?case
      using pderiv_carr[OF assms(2)] assms(3)
      using p.int_embed_one by simp
  next
    case (Suc m)
    have "pderiv (f [^]⇘K [X]⇙ (Suc m + 1)) =
      pderiv (f [^]⇘K [X]⇙ (m+1) ⊗⇘K[X]⇙ f) "
      by simp
    also have "... =
      pderiv (f [^]⇘K [X]⇙ (m+1)) ⊗⇘K[X]⇙ f ⊕⇘K[X]⇙
      f [^]⇘K [X]⇙ (m+1) ⊗⇘K[X]⇙ pderiv f"
      using assms(3) by (subst pderiv_mult[OF assms(2)], auto)
    also have "... =
      (?n (m+1) ⊗⇘K [X]⇙ f [^]⇘K [X]⇙ m ⊗⇘K [X]⇙ pderiv f) ⊗⇘K[X]⇙ f
      ⊕⇘K[X]⇙ f [^]⇘K [X]⇙ (m+1) ⊗⇘K[X]⇙ pderiv f"
      by (subst Suc(1), simp)
    also have
      "... = ?n (m+1) ⊗⇘K[X]⇙ (f [^]⇘K [X]⇙ (m+1) ⊗⇘K[X]⇙ pderiv f)
      ⊕⇘K[X]⇙ 𝟭⇘K [X]⇙ ⊗⇘K[X]⇙ (f [^]⇘K [X]⇙ (m+1) ⊗⇘K[X]⇙ pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      apply (intro arg_cong2[where f="(⊕⇘K[X]⇙)"])
      apply (simp add:p.m_assoc)
       apply (simp add:p.m_comm)
      by simp
    also have
      "... = (?n (m+1) ⊕⇘K[X]⇙ 𝟭⇘K [X]⇙) ⊗⇘K [X]⇙
      (f [^]⇘K [X]⇙ (m+1) ⊗⇘K [X]⇙ pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      by (subst p.l_distr[symmetric], simp_all)
    also have "... =
      (𝟭⇘K [X]⇙ ⊕⇘K[X]⇙ ?n (m+1)) ⊗⇘K [X]⇙
      (f [^]⇘K [X]⇙ (m+1) ⊗⇘K [X]⇙ pderiv f)"
      using assms(3) pderiv_carr[OF assms(2)]
      by (subst p.a_comm, simp_all)
    also have "... = ?n (1+ Suc m)
      ⊗⇘K [X]⇙ f [^]⇘K [X]⇙ (Suc m) ⊗⇘K [X]⇙ pderiv f"
      using assms(3) pderiv_carr[OF assms(2)] of_nat_add
      apply (subst (2) of_nat_add, subst p.int_embed_add)
      by (simp add:p.m_assoc p.int_embed_one)
    finally show ?case by simp
  qed
  thus "?thesis" using n_def by auto
qed

lemma pderiv_var_pow:
  assumes "n > (0::nat)"
  assumes "subring K R"
  shows "pderiv (X [^]⇘K[X]⇙ n) =
    int_embed (K[X]) n ⊗⇘K[X]⇙ X [^]⇘K[X]⇙ (n-1)"
proof -
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms(2)] by simp

  have [simp]: "int_embed (K[X]) i ∈ carrier (K[X])" for i
    using p.int_embed_range[OF p.carrier_is_subring] by simp

  show ?thesis
    using var_closed[OF assms(2)]
    using pderiv_var[where K="K"] pderiv_carr[OF assms(2)]
    by (subst pderiv_pow[OF assms(1,2)], simp_all)
qed

lemma int_embed_consistent_with_poly_of_const:
  assumes "subring K R"
  shows "int_embed (K[X]) m = poly_of_const (int_embed R m)"
proof -
  define K' where "K' = R ⦇ carrier := K ⦈"
  interpret p: cring "(K[X])"
    using univ_poly_is_cring[OF assms] by simp
  interpret d: domain "K'"
    unfolding K'_def
    using assms(1) subdomainI' subdomain_is_domain by simp
  interpret h: ring_hom_ring  "K'" "K[X]" "poly_of_const"
    unfolding K'_def
    using canonical_embedding_ring_hom[OF assms(1)] by simp

  define n where "n=nat (abs m)"

  have a1: "int_embed (K[X]) (int n) = poly_of_const (int_embed K' n)"
  proof (induction n)
    case 0
    then show ?case by (simp add:d.int_embed_zero p.int_embed_zero)
  next
    case (Suc n)
    then show ?case
      using d.int_embed_closed d.int_embed_add d.int_embed_one
      by (simp add:p.int_embed_add p.int_embed_one)
  qed
  also have "... = poly_of_const (int_embed R n)"
    unfolding K'_def using int_embed_consistent[OF assms] by simp
  finally have a:
    "int_embed (K[X]) (int n) = poly_of_const (int_embed R (int n))"
    by simp

  have "int_embed (K[X]) (-(int n)) =
    poly_of_const (int_embed K' (- (int n)))"
    using d.int_embed_closed a1 by (simp add: p.int_embed_inv d.int_embed_inv)
  also have "... = poly_of_const (int_embed R (- (int n)))"
    unfolding K'_def using int_embed_consistent[OF assms] by simp
  finally have b:
    "int_embed (K[X]) (-int n) = poly_of_const (int_embed R (-int n))"
    by simp

  show ?thesis
    using a b n_def by (cases "m ≥ 0", simp, simp)
qed

end

end