Theory Symmetric_Polynomials.Vieta

(*
  File:     Vieta.thy
  Author:   Manuel Eberl (TU München)

  Vieta's formulas expressing the coefficients of a factored univariate polynomial in
  terms of its roots.
*)
section ‹Vieta's Formulas›
theory Vieta
imports
  "HOL-Library.FuncSet"
  "HOL-Computational_Algebra.Computational_Algebra"
begin

subsection ‹Auxiliary material›

lemma card_vimage_inter:
  assumes inj: "inj_on f A" and subset: "X  f ` A"
  shows   "card (f -` X  A) = card X"
proof -
  have "card (f -` X  A) = card (f ` (f -` X  A))"
    by (subst card_image) (auto intro!: inj_on_subset[OF inj])
  also have "f ` (f -` X  A) = X"
    using assms by auto
  finally show ?thesis .
qed

lemma bij_betw_image_fixed_card_subset:
  assumes "inj_on f A"
  shows   "bij_betw (λX. f ` X) {X. X  A  card X = k} {X. X  f ` A  card X = k}"
  using assms inj_on_subset[OF assms]
  by (intro bij_betwI[of _ _ _ "λX. f -` X  A"]) (auto simp: card_image card_vimage_inter)

lemma image_image_fixed_card_subset:
  assumes "inj_on f A"
  shows   "(λX. f ` X) ` {X. X  A  card X = k} = {X. X  f ` A  card X = k}"
  using bij_betw_imp_surj_on[OF bij_betw_image_fixed_card_subset[OF assms, of k]] .

lemma prod_uminus: "(xA. -f x :: 'a :: comm_ring_1) = (-1) ^ card A * (xA. f x)"
  by (induction A rule: infinite_finite_induct) (auto simp: algebra_simps)

theorem prod_sum_PiE:
  fixes f :: "'a  'b  'c :: comm_semiring_1"
  assumes finite: "finite A" and finite: "x. x  A  finite (B x)"
  shows   "(xA. yB x. f x y) = (gPiE A B. xA. f x (g x))"
  using assms
proof (induction A rule: finite_induct)
  case empty
  thus ?case by auto
next
  case (insert x A)
  have "(gPiE (insert x A) B. xinsert x A. f x (g x)) =
          (gPiE (insert x A) B. f x (g x) * (x'A. f x' (g x')))"
    using insert by simp
  also have "(λg. x'A. f x' (g x')) = (λg. x'A. f x' (if x' = x then undefined else g x'))"
    using insert by (intro ext prod.cong) auto
  also have "(gPiE (insert x A) B. f x (g x) *  g) =
               ((y,g)B x × PiE A B. f x y * (x'A. f x' (g x')))"
    using insert.prems insert.hyps
    by (intro sum.reindex_bij_witness[of _ "λ(y,g). g(x := y)" "λg. (g x, g(x := undefined))"])
       (auto simp: PiE_def extensional_def)
  also have " = (yB x. gPiE A B. f x y * (x'A. f x' (g x')))"
    by (subst sum.cartesian_product) auto
  also have " = (yB x. f x y) * (gPiE A B. x'A. f x' (g x'))"
    using insert by (subst sum.swap) (simp add: sum_distrib_left sum_distrib_right)
  also have "(gPiE A B. x'A. f x' (g x')) = (xA. yB x. f x y)"
    using insert.prems by (intro insert.IH [symmetric]) auto
  also have "(yB x. f x y) *  = (xinsert x A. yB x. f x y)"
    using insert.hyps by simp
  finally show ?case ..
qed

corollary prod_add:
  fixes f1 f2 :: "'a  'c :: comm_semiring_1"
  assumes finite: "finite A"
  shows   "(xA. f1 x + f2 x) = (XPow A. (xX. f1 x) * (xA-X. f2 x))"
proof -
  have "(xA. f1 x + f2 x) = (gA E UNIV. xA. if g x then f1 x else f2 x)"
    using prod_sum_PiE[of A "λ_. UNIV :: bool set" "λx y. if y then f1 x else f2 x"] assms
    by (simp_all add: UNIV_bool add_ac)
  also have " = (XPow A. xA. if x  X then f1 x else f2 x)"
    by (intro sum.reindex_bij_witness
          [of _ "λX x. if x  A then x  X else undefined" "λP. {xA. P x}"]) auto
  also have " = (XPow A. (xX. f1 x) * (xA-X. f2 x))"
  proof (intro sum.cong refl, goal_cases)
    case (1 X)
    let ?f = "λx. if x  X then f1 x else f2 x"
    have "prod f1 X * prod f2 (A - X) = prod ?f X * prod ?f (A - X)"
      by (intro arg_cong2[of _ _ _ _ "(*)"] prod.cong) auto
    also have " = prod ?f (X  (A - X))"
      using 1 by (subst prod.union_disjoint) (auto intro: finite_subset[OF _ finite])
    also have "X  (A - X) = A" using 1 by auto
    finally show ?case ..
  qed
  finally show ?thesis .
qed

corollary prod_diff1:
  fixes f1 f2 :: "'a  'c :: comm_ring_1"
  assumes finite: "finite A"
  shows   "(xA. f1 x - f2 x) = (XPow A. (-1) ^ card X * (xX. f2 x) * (xA-X. f1 x))"
proof -
  have "(xA. f1 x - f2 x) = (xA. -f2 x + f1 x)"
    by simp
  also have " = (XPow A. (xX. - f2 x) * prod f1 (A - X))"
    by (rule prod_add) fact+
  also have " = (XPow A. (-1) ^ card X * (xX. f2 x) * prod f1 (A - X))"
    by (simp add: prod_uminus)
  finally show ?thesis .
qed

corollary prod_diff2:
  fixes f1 f2 :: "'a  'c :: comm_ring_1"
  assumes finite: "finite A"
  shows   "(xA. f1 x - f2 x) = (XPow A. (-1) ^ (card A - card X) * (xX. f1 x) * (xA-X. f2 x))"
proof -
  have "(xA. f1 x - f2 x) = (xA. f1 x + (-f2 x))"
    by simp
  also have " = (XPow A. (xX. f1 x) * (xA-X. -f2 x))"
    by (rule prod_add) fact+
  also have " = (XPow A. (-1) ^ card (A - X) * (xX. f1 x) * (xA-X. f2 x))"
    by (simp add: prod_uminus mult_ac)
  also have " = (XPow A. (-1) ^ (card A - card X) * (xX. f1 x) * (xA-X. f2 x))"
    using finite_subset[OF _ assms] by (intro sum.cong refl, subst card_Diff_subset) auto
  finally show ?thesis .
qed


subsection ‹Main proofs›

text ‹
  Our goal is to determine the coefficients of some fully factored polynomial
  $p(X) = c (X - x_1) \ldots (X - x_n)$ in terms of the $x_i$. It is clear that it is
  sufficient to consider monic polynomials (i.e. $c = 1$), since the general case follows
  easily from this one.

  We start off by expanding the product over the linear factors:
›
lemma poly_from_roots:
  fixes f :: "'a  'b :: comm_ring_1" assumes fin: "finite A"
  shows "(xA. [:-f x, 1:]) = (XPow A. monom ((-1) ^ card X * (xX. f x)) (card (A - X)))"
proof -
  have "(xA. [:-f x, 1:]) = (xA. [:0, 1:] - [:f x:])"
    by simp
  also have " = (XPow A. (-1) ^ card X * (xX. [:f x:]) * monom 1 (card (A - X)))"
    using fin by (subst prod_diff1) (auto simp: monom_altdef mult_ac)
  also have " = (XPow A. monom ((-1) ^ card X * (xX. f x)) (card (A - X)))"
  proof (intro sum.cong refl, goal_cases)
    case (1 X)
    have "(-1 :: 'b poly) ^ card X = [:(-1) ^ card X:]"
      by (induction X rule: infinite_finite_induct) (auto simp: one_pCons algebra_simps)
    moreover have "(xX. [:f x:]) = [:xX. f x:]"
      by (induction X rule: infinite_finite_induct) auto
    ultimately show ?case by (simp add: smult_monom)
  qed
  finally show ?thesis .
qed

text ‹
  Comparing coefficients yields Vieta's formula:
›
theorem coeff_poly_from_roots:
  fixes f :: "'a  'b :: comm_ring_1"
  assumes fin: "finite A" and k: "k  card A"
  shows   "coeff (xA. [:-f x, 1:]) k =
             (-1) ^ (card A - k) * (X | X  A  card X = card A - k. (xX. f x))"
proof -
  have "(xA. [:-f x, 1:]) = (XPow A. monom ((-1) ^ card X * (xX. f x)) (card (A - X)))"
    by (intro poly_from_roots fin)
  also have "coeff  k = (X | X  A  card X = card A - k. (-1) ^ (card A - k) * (xX. f x))"
    unfolding coeff_sum coeff_monom using finite_subset[OF _ fin] k card_mono[OF fin]
    by (intro sum.mono_neutral_cong_right) (auto simp: card_Diff_subset)
  also have " = (-1) ^ (card A - k) * (X | X  A  card X = card A - k. (xX. f x))"
    by (simp add: sum_distrib_left)
  finally show ?thesis .
qed

text ‹
  If the roots are all distinct, we can get the following alternative representation:
›
corollary coeff_poly_from_roots':
  fixes f :: "'a  'b :: comm_ring_1"
  assumes fin: "finite A" and inj: "inj_on f A" and k: "k  card A"
  shows   "coeff (xA. [:-f x, 1:]) k =
             (-1) ^ (card A - k) * (X | X  f ` A  card X = card A - k. X)"
proof -
  have "coeff (xA. [:-f x, 1:]) k =
          (-1) ^ (card A - k) * (X | X  A  card X = card A - k. (xX. f x))"
    by (intro coeff_poly_from_roots assms)
  also have "(X | X  A  card X = card A - k. (xX. f x)) =
               (X | X  A  card X = card A - k. (f`X))"
    by (intro sum.cong refl, subst prod.reindex) (auto intro: inj_on_subset[OF inj])
  also have " = (X  (λX. f`X) ` {X. X  A  card X = card A - k}. X)"
    by (subst sum.reindex) (auto intro!: inj_on_image inj_on_subset[OF inj])
  also have "(λX. f ` X) ` {X. X  A  card X = card A - k} = {X. X  f ` A  card X = card A - k}"
    by (intro image_image_fixed_card_subset inj)
  finally show ?thesis .
qed

end