import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.nat
import Goppadecoding.zero
import Goppadecoding.sum

open Polynomial BigOperators Finset

namespace Goppadecoding

section lemmas_poly

theorem degree_add_le_if_degree_ge
  {k: Type _} [Field k] {f g: k[X]}
  (gd: g.degree ≤ f.degree):
  (f+g).degree ≤ f.degree :=
by
  calc
    _ ≤ max f.degree g.degree := degree_add_le f g
    _ ≤ f.degree := max_le (le_refl f.degree) gd

theorem degree_add_eq_if_degree_lt
  {k: Type _} [Field k] {f g: k[X]}
  (gd: g.degree < f.degree):
  (f+g).degree = f.degree :=
by
  apply le_antisymm
  . have gled: g.degree ≤ f.degree := le_of_lt gd
    exact degree_add_le_if_degree_ge gled
  apply not_lt.mp
  intro fd
  have ff: degree f < degree f := by calc
    _ = degree (f+g-g) := by group
    _ ≤ max (f+g).degree g.degree := degree_sub_le (f+g) g
    _ < f.degree := max_lt fd gd
  rw[lt_self_iff_false] at ff
  exact ff

theorem nonzero_if_coeff_nonzero {R: Type _} [Semiring R] {f: R[X]} {n: ℕ}:
  coeff f n ≠ 0 → f ≠ 0 :=
by
  contrapose
  simp only [ne_eq, not_not]
  intro fzero
  rw[fzero]
  apply coeff_zero

theorem coeff_bigsum {U: Type _} [DecidableEq U] {R: Type _} [Semiring R] {f: U → R[X]} {d: ℕ}:
  ∀ S: Finset U,
    coeff (∑ s in S, f s) d = ∑ s in S, coeff (f s) d :=
by 
  apply Finset.induction
  . simp only [Finset.sum_empty, coeff_zero]
  . intro a S notin prevcase 
    repeat rw[Finset.sum_insert notin]
    rw[coeff_add,prevcase]

theorem zero_coeff_of_zero_poly_as_sum {k: Type _} [Field k] {f: ℕ → k} {d: ℕ}:
  ∑ j in range d, C (f j) * X^(d-1-j) = 0 →
  ∀ i, i < d → f i = 0 :=
by
  intro poly0 i id
  apply Eq.symm
  calc
    0 = coeff 0 (d-1-i) := by rw[coeff_zero]
    _ = coeff (∑ j in range d, C (f j) * X^(d-1-j)) (d-1-i) := by rw[poly0]
    _ = ∑ j in range d, coeff (C (f j) * X^(d-1-j)) (d-1-i) := by rw[coeff_bigsum]
    _ = ∑ j in range d, f j * coeff ((X:k[X])^(d-1-j)) (d-1-i) := by
          apply sum_congr; simp only; intro j _
          rw[coeff_C_mul]
    _ = ∑ j in range d, f j * (if d-1-i = d-1-j then 1 else 0) := by
          apply sum_congr; simp only; intro j _
          rw[coeff_X_pow]
    _ = ∑ j in range d, (if i = j then f j else 0) := by
          apply sum_congr; simp only; intro j jd
          rw[mem_range] at jd
          rw[mul_ite,mul_one,mul_zero]
          apply ite_congr
          rw[eq_iff_iff]
          constructor
          . apply eq_if_bounded_bounded_eqflip id jd
          . intro ij; rw[ij]
          repeat simp
    _ = if i ∈ range d then f i else 0 := sum_ite_eq (range d) i f
    _ = if i < d then f i else 0 := by simp only [mem_range]
    _ = f i := by simp[id]

theorem sum_degree_lt {U: Type _} [DecidableEq U] {R: Type _} [Semiring R] {f: U → R[X]} {d: ℕ}:
  ∀ S: Finset U,
    (∀ s, s ∈ S → degree (f s) < d) → degree (∑ s in S, f s) < d :=
by
  apply Finset.induction 
  . simp only [Finset.not_mem_empty, IsEmpty.forall_iff, implies_true, Finset.sum_empty, degree_zero, bot_lt_iff_ne_bot, ne_eq, WithBot.nat_ne_bot, not_false_eq_true, forall_true_left]
  . intro a S notin prevcase 
    rw[Finset.sum_insert]
    intro hyp
    calc
      degree (f a + ∑ x in S, f x)
        ≤ max (degree (f a)) (degree (∑ x in S, f x)) := by apply degree_add_le
      _ < d := by
            apply max_lt
            apply hyp a (Finset.mem_insert_self a S)
            apply prevcase
            intro s sinS
            apply hyp
            exact Finset.mem_insert_of_mem sinS
    simp only [notin, not_false_eq_true]

theorem degree_C_mul_le_degree {k: Type _} [Field k] (f: k[X]) (c: k):
  degree (C c * f) ≤ degree f :=
by
  by_cases csign: c = 0
  . rw[csign,C_0]
    ring_nf
    simp only [degree_zero, bot_le, implies_true]
  . rw[degree_mul,degree_C csign]
    simp only [zero_add, le_refl]

theorem degree_C_mul_lt_if_degree_lt {k: Type _} [Field k] (f: k[X]) (d: ℕ) (c: k)
  (fd: degree f < d): degree (C c * f) < d :=
by calc
  _ ≤ degree f := degree_C_mul_le_degree f c
  _ < d := fd

theorem degree_mul_C_lt_if_degree_lt {k: Type _} [Field k] (f: k[X]) (d: ℕ) (c: k):
  degree f < d → degree (f * C c) < d := by
    rw[mul_comm]
    apply degree_C_mul_lt_if_degree_lt

-- imitating degree_sum_fin_lt in library
theorem degree_sum_range_lt {k: Type _} [Field k] {n: ℕ} (f: ℕ → k):
  degree (∑ i in range n, (monomial i: k →ₗ[k] k[X]) (f i): k[X]) < n := by 
    apply sum_degree_lt
    intro s srange
    by_cases fs: f s = 0 
    . simp only [fs, map_zero, degree_zero]
      apply bot_lt_iff_ne_bot.mpr
      exact WithBot.nat_ne_bot n
    rw[degree_monomial]
    simp only [Nat.cast_lt]
    exact List.mem_range.mp srange
    exact fs

theorem coeff_sum_range_monomial {k: Type _} [Field k] {c: ℕ → k} (n d: ℕ):
  coeff (∑ j in range n, (monomial j: k →ₗ[k] k[X]) (c j)) d
  = if d < n then c d else 0
  := by calc
      coeff (∑ j in range n, (monomial j: k →ₗ[k] k[X]) (c j)) d
        = ∑ j in range n, coeff ((monomial j: k →ₗ[k] k[X]) (c j)) d := finset_sum_coeff (range n) (fun j => (monomial j: k →ₗ[k] k[X]) (c j)) d
      _ = ∑ j in range n, if j = d then c d else 0 := by simp only [coeff_monomial, Finset.sum_ite_eq', Finset.mem_range]
      _ = if d ∈ range n then c d else 0 := by apply Finset.sum_ite_eq'
      _ = if d < n then c d else 0 := by simp only [Finset.mem_range]

theorem degree_lt_if_coeff_zero {k: Type _} [Field k] (f: k[X]) (n: ℕ):
  (∀ d:ℕ, n ≤ d → coeff f d = 0) → degree f < n := by
    intro hyp
    exact (degree_lt_iff_coeff_zero f n).mpr hyp

theorem degree_add_lt_if_coeff_zero {k: Type _} [Field k] (f: k[X]) (m: ℕ) (n: ℕ):
  (∀ d:ℕ, (n-m:ℤ) ≤ (d:ℤ) → coeff f d = 0) → m + degree f < n := by
    intro hyp
    by_cases mn: m ≤ n
    . let nm:ℕ := n-m
      have neq: n = m+nm := Eq.symm (Nat.add_sub_of_le mn)
      have h: ∀ d:ℕ, nm ≤ d → coeff f d = 0 := by
        intro d nmd
        apply hyp d
        rw[neq,Nat.cast_add]
        group
        exact Int.ofNat_le.mpr nmd
      have h2: degree f < nm := degree_lt_if_coeff_zero f nm h
      have h3: m + degree f < m + nm := by
        apply WithBot.add_lt_add_left
        simp only [ne_eq, WithBot.nat_ne_bot, not_false_eq_true]
        apply h2
      rw[neq]
      norm_cast
    . have h: ∀ d:ℕ, 0 ≤ d → coeff f d = 0 := by
        intro d nmd
        apply hyp d
        linarith
      have h2: degree f < 0 := degree_lt_if_coeff_zero f 0 h
      have h3: degree f = ⊥ := (Nat.WithBot.lt_zero_iff (degree f)).mp h2
      have h4: m + degree f = ⊥ := by rw[h3]; rfl
      rw[h4]
      apply WithBot.bot_lt_coe

theorem add_lt_add_right_nonzero_degree {k: Type _} [Field k] {x y: WithBot ℕ} {a: k[X]}:
  a ≠ 0 → x < y → x + degree a < y + degree a := by
    intro anonzero
    have deganat: degree a ≠ ⊥ := by
      simp only [ne_eq, degree_eq_bot, anonzero, not_false_eq_true]
    intro xy
    exact WithBot.add_lt_add_right deganat xy
  
theorem nonzero_if_divides_nonzero {k: Type _} [Field k] {a b: k[X]}:
  a ∣ b → b ≠ 0 → a ≠ 0 := by
    intro adivb
    contrapose
    repeat rw[not_ne_iff]
    intro azero
    cases adivb with | intro q baq =>
      rw[baq,azero]
      exact zero_mul q

theorem no_shared_root_if_coprime {k: Type _} [Field k] {a b: k[X]} {r: k}:
  IsCoprime a b → a.eval r = 0 → b.eval r ≠ 0 := by
    unfold IsCoprime
    intro coprime ar
    cases coprime with | intro x xcond =>
      cases xcond with | intro y ycond =>
        have yb1: y.eval r * b.eval r = 1 := by calc
          _ = (y*b).eval r := by rw[eval_mul]
          _ = 0 + (y*b).eval r := by group
          _ = (x.eval r)*0 + (y*b).eval r := by ring
          _ = (x.eval r)*(a.eval r) + (y*b).eval r := by rw[ar]
          _ = (x*a).eval r + (y*b).eval r := by rw[← eval_mul]
          _ = (x*a+y*b).eval r := by rw[eval_add]
          _ = (1:k[X]).eval r := by rw[ycond]
          _ = (C 1:k[X]).eval r := by rfl
          _ = 1 := by rw[eval_C]
        exact nonzero_if_mul_left_one yb1

theorem eq_C_lead_if_left_inverse {k: Type _} [Field k] {f g: k[X]}:
  f*g = 1 → g = C g.leadingCoeff := by
    rw[mul_comm]
    intro fg1
    have gunit: IsUnit g := isUnit_of_mul_eq_one g f fg1
    have degg: degree g = 0 := degree_eq_zero_of_isUnit gunit
    have natdegg: natDegree g = 0 := natDegree_eq_zero_of_isUnit gunit
    unfold leadingCoeff
    rw[natdegg]
    exact eq_C_of_degree_eq_zero degg

theorem eq_C_lead_if_right_inverse {k: Type _} [Field k] {f g: k[X]}:
  f*g = 1 → f = C f.leadingCoeff := by
    rw[mul_comm]
    exact eq_C_lead_if_left_inverse

theorem eq_lead_mul_if_dvd_dvd {k: Type _} [Field k] {f g: k[X]}:
  f ∣ g → g ∣ f → g.leadingCoeff = 1 → f = C f.leadingCoeff * g := by
    intro fg gf gmonic
    cases fg with | intro q gfq =>
      cases gf with | intro r fgr =>
        have fqr: f*(q*r) = f := by calc
          _ = (f*q)*r := by rw[mul_assoc]
          _ = g*r := by rw[gfq]
          _ = f := by rw[fgr]
        by_cases f0: f = 0
        . simp[f0]
        have qr: q*r = 1 := eq_one_if_mul_eq_self f0 fqr
        have rC: r = C r.leadingCoeff := eq_C_lead_if_left_inverse qr
        have leadqf: r.leadingCoeff = f.leadingCoeff := by calc
          _ = 1 * r.leadingCoeff := by ring
          _ = g.leadingCoeff * r.leadingCoeff := by rw[gmonic]
          _ = (g*r).leadingCoeff := by rw[leadingCoeff_mul g r]
          _ = f.leadingCoeff := by rw[fgr]
        calc
          f = g*r := by rw[fgr]
          _ = r*g := by rw[mul_comm]
          _ = (C r.leadingCoeff)*g := by rw[← rC]
          _ = (C f.leadingCoeff)*g := by rw[leadqf]

theorem coprime_X_minus_nonroot {k: Type _} [Field k] {f: k[X]} {r: k}:
  f.eval r ≠ 0 → IsCoprime f (X - C r) := by
    intro nonroot
    have div: X - C r ∣ f - C (f.eval r) := X_sub_C_dvd_sub_C_eval
    cases div with | intro q qeq =>
      let vinv := (f.eval r)⁻¹
      have vvinv: vinv * (f.eval r) = 1 := inv_mul_cancel nonroot
      unfold IsCoprime
      use C vinv
      use - (C vinv * q)
      calc
        _ = (C vinv) * (f - C (f.eval r) + C (f.eval r) - q * (X - C r)) := by ring
        _ = (C vinv) * ((X - C r) * q + C (f.eval r) - q * (X - C r)) := by rw[qeq]
        _ = (C vinv) * C (f.eval r) := by ring
        _ = C (vinv * f.eval r) := by rw[C_mul]
        _ = C 1 := by rw[vvinv]
        _ = 1 := by rw[map_one]

theorem mul_neg_geom_sum2_X_C {k: Type _} [Field k] (d: ℕ) (r: k):
  X^d - C (r^d) = (X - C r) * ∑ j in range d, C (r^j) * X^(d-1-j) :=
by
  simp only[map_pow]
  rw[Commute.mul_neg_geom_sum₂]
  simp
  unfold Commute
  unfold SemiconjBy
  rw[mul_comm]

theorem as_sum_range_if_degree_lt {k: Type _} [Field k] {f: k[X]} {n: ℕ} (fdeg: f.degree < n):
  f = ∑ i in range n, (monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i) :=
by
  by_cases f0: f = 0
  . simp only [f0, coeff_zero, map_zero, sum_const_zero]
  have fnatdegn: f.natDegree < n := (natDegree_lt_iff_degree_lt f0).mpr fdeg
  exact as_sum_range' f n fnatdegn

theorem coeff_mul_sum_geom {k: Type _} [Field k] {f: k[X]} {n: ℕ} (fdeg: f.degree < n) (r: k):
  coeff (f * (∑ j in range n, C (r^j) * X^(n-1-j))) (n-1)
  = f.eval r :=
by
  by_cases f0: f = 0
  . rw[f0]
    simp only[zero_mul,coeff_zero,eval_zero]
  have degfnat: 0 ≤ f.degree := Iff.mpr zero_le_degree_iff f0
  have npos1: 0 < (n:WithBot ℕ) := by calc
    _ ≤ f.degree := degfnat
    _ < n := fdeg
  have npos: 0 < n := WithBot.coe_pos.mp npos1
  have n1: Nat.succ (n - 1) = n := Nat.succ_pred_eq_of_pos npos
  have n1n: n-1 < n := by calc
    _ < Nat.succ (n-1) := Nat.lt.base (n - 1)
    _ = n := n1
  have fsum: f = ∑ i in range n, (monomial: ℕ → k →ₗ[k] k[X]) i (coeff f i) := as_sum_range_if_degree_lt fdeg
  rw[fsum]
  rw[eval_finset_sum]
  rw[coeff_mul]
  rw[Finset.Nat.sum_antidiagonal_eq_sum_range_succ (fun fst snd ↦ coeff (∑ i in range n, ((monomial: ℕ → k →ₗ[k] k[X]) i) (coeff f i)) fst * coeff (∑ j in range n, C (r^j) * X^(n-1-j)) snd) (n-1)]
  simp only [finset_sum_coeff, coeff_monomial, sum_ite_eq', mem_range, ite_mul, zero_mul, eval_monomial, coeff_C_mul_X_pow]
  rw[n1]
  apply sum_congr; simp only
  intro x xrange
  rw[mem_range] at xrange
  simp only[xrange,ite_true]
  rw[mul_eq_mul_left_iff]; left
  rw[sum_flip_simpler]
  calc
    _ = ∑ x_1 in range n, if n - 1 - x = x_1 then r ^ (n - 1 - x_1) else 0 := by
          apply sum_congr; rfl
          intro x1 x1range
          rw[mem_range] at x1range
          have x1n1: x1 ≤ n-1 := Nat.le_pred_of_lt x1range
          have subsub: n-1-(n-1-x1) = x1 := Nat.sub_sub_self x1n1
          rw[subsub]
    _ = if n - 1 - x ∈ range n then r ^ (n - 1 - (n - 1 - x)) else 0 := sum_ite_eq (range n) (n - 1 - x) fun x => r ^ (n - 1 - x)
    _ = if n - 1 - x ∈ range n then r ^ x else 0 := by
          have xn1: x ≤ n-1 := Nat.le_pred_of_lt xrange
          have subsub: n-1-(n-1-x) = x := Nat.sub_sub_self xn1
          rw[subsub]
    _ = r ^ x := by
          have xr: n-1-x ∈ range n := by
            rw[mem_range]
            calc
              n-1-x ≤ n-1 := Nat.sub_le (n - 1) x
              _ < n := n1n
          simp only[xr,ite_true]

theorem coeff_mul_sum_sum_geom {k: Type _} [Field k] {U: Type _} [DecidableEq U] {S: Finset U} {α c: U → k} {f: k[X]} {n: ℕ} (fdeg: f.degree < n):
  coeff (f * ∑ s in S, (∑ j in range n, C (c s * (α s)^j) * X^(n-1-j))) (n-1)
  = ∑ s in S, c s * f.eval (α s) :=
by
  rw[mul_sum,coeff_bigsum]
  apply sum_congr; rfl
  intro s _
  simp only[C_mul]
  calc
    _ = coeff (f * ∑ j in range n, C (c s) * C (α s ^ j) * X ^ (n - 1 - j)) (n - 1) := by simp only[C_mul]
    _ = coeff (f * ∑ j in range n, C (c s) * (C (α s ^ j) * X ^ (n - 1 - j))) (n - 1) := by simp only[mul_assoc]
    _ = coeff (f * (C (c s) * ∑ j in range n, C (α s ^ j) * X ^ (n - 1 - j))) (n - 1) := by simp only[mul_sum]
    _ = coeff (C (c s) * (f * ∑ j in range n, C (α s ^ j) * X ^ (n - 1 - j))) (n - 1) := by group
    _ = c s * coeff (f * ∑ j in range n, C (α s ^ j) * X ^ (n - 1 - j)) (n - 1) := by rw[coeff_C_mul]
    _ = _ := by rw[coeff_mul_sum_geom fdeg]
 
-- can also do this via zcoeff
theorem coeff_X_pow_add_one_eq_zero {k: Type _} [Field k] (f: k[X]) (d: ℕ)
: coeff (X^(d+1)*f) d = 0 :=
by
  rw[coeff_mul]
  apply sum_eq_zero
  simp only [Nat.mem_antidiagonal, mul_eq_zero, Prod.forall]
  intro a b abd
  left
  rw[coeff_X_pow]
  simp only [ite_eq_right_iff, one_ne_zero]
  intro ad1eq
  have ad: a ≤ d := by rw[← abd]; exact Nat.le_add_right a b
  have ad1: a < d+1 := Nat.lt_succ.mpr ad
  rw[ad1eq,lt_self_iff_false] at ad1
  exact ad1

theorem coeff_X_pow_eq_eval_zero {k: Type _} [Field k] (f: k[X]) (d: ℕ)
: coeff (X^d*f) d = f.eval 0 :=
by calc
  _ = coeff ((1:k[X]) * (X:k[X])^d * f) d := by rw[one_mul]
  _ = coeff (C (1:k) * (X:k[X])^d * f) d := by rw[map_one]
  _ = coeff ((monomial: ℕ → k →ₗ[k] k[X]) d (1:k) * f) d := by rw[C_mul_X_pow_eq_monomial]
  _ = coeff ((monomial: ℕ → k →ₗ[k] k[X]) d (1:k) * f) (0+d) := by rw[zero_add]
  _ = (1:k) * coeff f 0 := by rw[coeff_monomial_mul]
  _ = coeff f 0 := by rw[one_mul]
  _ = f.eval 0 := by rw[coeff_zero_eq_eval_zero]

end lemmas_poly