import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.prod
import Goppadecoding.char2
import Goppadecoding.vanishing
import Goppadecoding.finite_perfect

open Polynomial BigOperators

namespace Goppadecoding

section goppa_squaring

variable {U: Type _} [DecidableEq U]
variable {k: Type _} [Field k] [CharP k 2] [DecidableEq k]

theorem goppa_squaring
  [PerfectRing k 2] {α c: U → k} {S: Finset U} {A P g: k[X]}
  (Adef: A = monic_vanishing_at α S)
  (gsqfree: Squarefree g)
  (gA: IsCoprime g A)
  (cinF2: (∀ s, s ∈ S → c s = 0 ∨ c s = 1))
  (Pdef: P = (∑ s in S, C (c s) * monic_vanishing_at_except α S s))
: (g ∣ P ↔ g^2 ∣ P) :=
by
  let Y := ∏ s in S.filter (fun s ↦ c s ≠ 0), (X - C (α s))
  let Z := ∏ s in S.filter (fun s ↦ c s = 0), (X - C (α s))
  have YZ: Y*Z = A := by calc
    _ = (∏ s in S.filter (fun s ↦ ¬ c s = 0), (X - C (α s))) * (∏ s in S.filter (fun s ↦ c s = 0), (X - C (α s))) := by rfl
    _ = ∏ s in S, (X - C (α s)) := by apply prod_filter_not_mul_prod_filter
    _ = monic_vanishing_at α S := by rfl
    _ = A := by rw[Adef]
  have gYZ: IsCoprime g (Y*Z) := by rw[YZ]; exact gA
  have gZ: IsCoprime g Z := IsCoprime.of_mul_right_right gYZ
  have Yprime: Y.diff = ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α (S.filter (fun s ↦ c s ≠ 0)) s := by calc
    _ = (monic_vanishing_at α (S.filter (fun s ↦ c s ≠ 0))).diff := by rfl
    _ = ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α (S.filter (fun s ↦ c s ≠ 0)) s := by apply derivative_monic_vanishing_at
  have ZYprime: Z * Y.diff = ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α S s := by calc
    _ = Z * ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α (S.filter (fun t ↦ c t ≠ 0)) s := by rw[Yprime]
    _ = ∑ s in S.filter (fun s ↦ c s ≠ 0), Z * monic_vanishing_at_except α (S.filter (fun t ↦ c t ≠ 0)) s := by rw[Finset.mul_sum]
    _ = ∑ s in S.filter (fun s ↦ c s ≠ 0), (∏ t in S.filter (fun t ↦ c t = 0), (X - C (α t))) * ∏ t in ((S.filter (fun t ↦ c t ≠ 0)).erase s), (X - C (α t)) := by rfl
    _ = ∑ s in S.filter (fun s ↦ c s ≠ 0), ∏ t in S.erase s, (X - C (α t)) := by
          apply Finset.sum_congr
          simp only [ne_eq]
          intro s sY
          have union: S.erase s = (S.filter (fun t ↦ c t = 0)) ∪ ((S.filter (fun t ↦ c t ≠ 0)).erase s) := by
            rw[erase_eq_filter_not_union_filter_erase sY]
            simp only [ne_eq, not_not, Finset.mem_filter, not_and]
          have disjoint: Disjoint (S.filter (fun t ↦ c t = 0)) ((S.filter (fun t ↦ c t ≠ 0)).erase s) := by
            apply disjoint_filter_not_filter_erase
          rw[prod_eq_disjoint_union union disjoint (fun t ↦ X - C (α t))]
    _ = _ := by rfl
  have ZYprime2: Z * Y.diff = ∑ s in S, C (c s) * monic_vanishing_at_except α S s := by calc
    _ = ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α S s := ZYprime
    _ = 0 + ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α S s := by group
    _ = (∑ s in S.filter (fun s ↦ c s = 0), 0) + ∑ s in S.filter (fun s ↦ c s ≠ 0), monic_vanishing_at_except α S s := by rw[Finset.sum_const_zero]
    _ = ∑ s in S, if c s = 0 then 0 else monic_vanishing_at_except α S s := by rw[Finset.sum_ite]
    _ = _ := by
          apply Finset.sum_congr
          simp only
          intro s sinS
          by_cases cs0: c s = 0
          . simp only [cs0, ite_true, map_zero, zero_mul]
          . simp only [cs0, ite_false, ne_eq]
            have cs0or1: c s = 0 ∨ c s = 1 := cinF2 s sinS
            rw[or_iff_not_imp_left] at cs0or1
            have cs1: c s = 1 := cs0or1 cs0
            simp only [cs1, map_one, one_mul]
  have ZYprimeP: Z * Y.diff = P := by rw[ZYprime2,Pdef]
  constructor
  . intro gdivP
    have gYprime: g ∣ Y.diff := by
      have gZYprime: g ∣ Z * Y.diff := by rw[ZYprimeP]; exact gdivP
      exact dvd_if_dvd_mul_left gZ gZYprime
    have ggYprime: g^2 ∣ Y.diff := squarefree_dvd_derivative gsqfree gYprime
    rw[← ZYprimeP]
    exact Dvd.dvd.mul_left ggYprime Z
  . intro g2P
    rw[sq] at g2P
    exact dvd_of_mul_right_dvd g2P

theorem goppa_squaring_finite
  [Fintype k] {α c: U → k} {S: Finset U} {A P g: k[X]}
  (Adef: A = monic_vanishing_at α S)
  (sqfree: Squarefree g)
  (gA: IsCoprime g A)
  (cinF2: (∀ s, s ∈ S → c s = 0 ∨ c s = 1))
  (Pdef: P = (∑ s in S, C (c s) * monic_vanishing_at_except α S s))
: (g ∣ P ↔ g^2 ∣ P) :=
goppa_squaring Adef sqfree gA cinF2 Pdef

end goppa_squaring