import tactic
import ring_theory.polynomial.basic
import algebra.polynomial.big_operators

universes u v 
open_locale big_operators
open polynomial fin finset

-- in polynomial.
theorem coeff_C_ne_zero {R : Type u} {a : R} {n : ℕ} [semiring R] (h : n ≠ 0) : (C a).coeff n = 0 :=
begin
  rw polynomial.coeff_C,
  simp,
  intro hn,
  exfalso,
  apply h,
  exact hn,
end

namespace finset
variables {α : Type u} (s : finset α)

@[simp] lemma powerset_len_zero (s : finset α) : powerset_len 0 s = {∅} := 
begin
  ext,
  rw mem_singleton,
  rw ← finset.card_eq_zero,
  rw mem_powerset_len,
  simp only [card_eq_zero, and_iff_right_iff_imp],
  intro h,
  rw h,
  simp,
end

end finset

namespace vieta

variables {α : Type u} [integral_domain α]
variables {n : ℕ} {r : ℕ → α} {f : polynomial α}

lemma coeff_prod (n : ℕ) (p q : polynomial α) : coeff (p * q) n = ∑ i in range (n + 1), coeff p i * coeff q (n - i) := 
begin
  sorry
end

example (n : ℕ) : ∏ i in range n, 1 = 1 := prod_const_one
-- use polynomial.leading_coeff_prod

lemma linear_poly_coeff_zero (a : α) : coeff (X + C a) 0 = a :=
begin
  simp [polynomial.coeff_zero_eq_eval_zero],
end

lemma linear_poly_coeff_one (a : α) : coeff (X + C a) 1 = (1 : α) := 
begin
  simp [polynomial.coeff_zero_eq_eval_zero, coeff_C_ne_zero],
end

lemma linear_poly_coeff_ge_two (a : α) (h : 2 ≤ n) : coeff (X + C a) n = (0 : α) :=
begin
  simp only [coeff_add, coeff_C],
  rw polynomial.coeff_X_of_ne_one,
  simp [coeff_C_ne_zero],
  intro hn, exfalso,
  linarith,
  linarith,
end

@[simp] lemma degree_X_add_C (a : α) : degree (X + C a) = 1 :=
have degree (C a) < degree (X : polynomial α),
from calc degree (C a) ≤ 0 : degree_C_le
                   ... < 1 : with_bot.some_lt_some.mpr zero_lt_one
                   ... = degree X : degree_X.symm,
by rw [degree_add_eq_left_of_degree_lt this, degree_X]

lemma coeff_top (n : ℕ) (r : ℕ → α) : coeff (∏ i in range n, (X + C (r i))) n = 1 := 
begin
  have h : nat_degree (∏ i in range n, (X + C (r i))) = n :=
  begin
    rw nat_degree_prod,
    conv { to_rhs, rw ← card_range n, rw finset.card_eq_sum_ones, },
    congr, ext,
    have h := monic_X_add_C (r x),
    rw ← degree_eq_iff_nat_degree_eq,
    simp,
    exact monic.ne_zero h,
    intros,
    have h := monic_X_add_C (r i),
    exact monic.ne_zero h,
  end,
  conv { to_lhs, congr, skip, rw ← h, },
  rw coeff_nat_degree,
  rw leading_coeff_prod,
  rw ← one_mul X,
  rw ← C_1,
  conv { to_rhs, rw ← @prod_const_one _ _ (range n : finset ℕ), },
  congr, ext,
  rw leading_coeff_X_add_C,
  norm_num,
end

lemma step3 (n k: ℕ) (h: k ≤ n) : ∑ l in range (k + 1), 
  (∑ A in powerset_len (n - l) (range n), ∏ j in A, r j) * (X + C (r n)).coeff (k - l) = 
  (∑ A in powerset_len (n - k + 1) (range n), ∏ j in A, r j)
    + (∑ A in powerset_len (n - k) (range n), ∏ j in A, r j) * (r n) :=
begin
  rw [sum_range_succ, nat.sub_self, linear_poly_coeff_zero],
  cases nat.eq_zero_or_pos k,
  { rw h_1, simp,
    have hh : powerset_len (n + 1) (range n) = ∅ := 
    by { apply finset.card_eq_zero.mp, simp },
    rw hh, simp },
  rw [← nat.succ_pred_eq_of_pos h_1, nat.succ_eq_add_one, sum_range_succ, 
      nat.add_sub_cancel_left, linear_poly_coeff_one, mul_one],
  have hsum : ∑ x in range k.pred, 
              (∑ A in powerset_len (n - x) (range n), 
              ∏ j  in A, r j) * (X + C (r n)).coeff (k.pred + 1 - x) = ∑ x in range k.pred, 0 := 
  begin
    apply sum_congr, { refl },
    intros x hx,
    have h_zero : 1 < k.pred + 1 - x := 
    begin
      rw mem_range at hx,
      replace hx := add_lt_add_left hx 1,
      rw add_comm _ k.pred at hx,
      exact nat.lt_sub_right_of_add_lt hx,
    end,
    rwa [linear_poly_coeff_ge_two, mul_zero],
  end,
  rw hsum,
  simp only [hsum, add_zero, sum_const_zero],
  rw add_comm,
  have h_re : n - (k.pred + 1) + 1 = n - k.pred := 
  begin 
    rw [nat.pred_eq_sub_one, nat.sub_add_eq_max, max_eq_left],
    omega nat, exact h_1,
  end,
  rwa h_re,
end

lemma dumb (n k : ℕ) : ∑ A in powerset_len (n - k) (range n), (∏ j in A, r j) * r n = 
                       ∑ A in powerset_len (n - k) (range n), ∏ j in insert n A, r j :=
begin
  have hn : n ∉ range n := finset.not_mem_range_self,
  apply sum_congr, { refl },
  intros x hx,
  rw insert_prod,
  rw finset.mem_powerset_len at hx,
  cases hx,
  intro h,
  apply hn,
  exact mem_of_subset hx_left h,
end

lemma step4 (n k : ℕ) (h : k ≤ n) : 
  ∑ A in powerset_len (n - k + 1) (range n), ∏ j in A, r j +
  ∑ A in powerset_len (n - k) (range n), ∏ j in insert n A, r j = 
  ∑ A in powerset_len (n.succ - k) (range n.succ), ∏ j in A, r j :=
begin
  have hn : n ∉ range n := finset.not_mem_range_self,
  have hh : ∑ a in filter (λ (a : finset ℕ), (insert n a).card = n.succ - k) (range n).powerset, ∏ j in insert n a, r j = 
            ∑ a in filter (λ (a : finset ℕ), a.card = n - k) (range n).powerset, ∏ j in insert n a, r j := 
  begin
    apply sum_congr, 
    { ext,
      rw [mem_filter, mem_filter, and.congr_right_iff],
      intro ha,
      rw card_insert_of_not_mem,
      omega,
      rw finset.mem_powerset at ha,
      intro h,
      apply hn,
      exact mem_of_subset ha h },
    simp,
  end,
  rw [@powerset_len_eq_filter _ _ (range n.succ), range_add_one, sum_filter, sum_powerset_insert,
    ← sum_filter, ← sum_filter, ← powerset_len_eq_filter, hh, ← @powerset_len_eq_filter],
  congr,
  omega,
  exact hn,
end

lemma coeff_poly_from_roots : 
  ∀ (k : ℕ), k ≤ n → coeff (∏ i in range n, (X + C (r i))) k 
  = ∑ A in (powerset_len (n - k) (range n)), (∏ j in A, r j) := 
begin
  induction n with n ih,
  { simp only [nat.nat_zero_eq_zero, le_zero_iff_eq, nat.zero_sub, forall_eq, range_zero],
    rw [prod_empty, coeff_one_zero, finset.powerset_len_zero ∅, sum_singleton, prod_empty] },
  { intros k hk,
    cases nat.of_le_succ hk,
    { clear hk,

calc (∏ i in range n.succ, (X + C (r i))).coeff k
      = ∑ l in range (k + 1), 
        coeff (∏ (i : ℕ) in range n, (X + C (r i))) l * (X + C (r n)).coeff (k - l) : 
  begin
    rw [nat.succ_eq_add_one, prod_range_succ, mul_comm, coeff_prod],
  end
  ... = ∑ l in range (k + 1), 
        (∑ A in powerset_len (n - l) (range n), ∏ j in A, r j) * (X + C (r n)).coeff (k - l) : 
  begin
    apply sum_congr, { refl },
    intros l hl,
    specialize ih l,
    have h_ln : l ≤ n := by { rw finset.mem_range_succ_iff at hl, exact le_trans hl h, },
    rw ih h_ln,
  end
  ... = (∑ A in powerset_len (n - k + 1) (range n), ∏ j in A, r j)
        + (∑ A in powerset_len (n - k) (range n), ∏ j in A, r j) * (r n)  :
  by { exact step3 n k h }
  ... = ∑ A in powerset_len (n.succ - k) (range n.succ), (∏ j in A, r j) : 
  by rwa [sum_mul, dumb, step4] }, 

    { simp only [h, nat.sub_self, finset.powerset_len_zero, sum_singleton, prod_empty],
      convert coeff_top n.succ r } } 
end 

end vieta