-rw-r--r-- 9274 leangoppa-20230726/Goppadecoding/goppa_parity.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.nat
import Goppadecoding.zero
import Goppadecoding.poly
import Goppadecoding.vanishing
import Goppadecoding.interpolator

open Polynomial BigOperators Finset

namespace Goppadecoding

section goppa_parity

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

theorem goppa_parity_lemma (α f: U → k) (S: Finset U) (d: ℕ)
: X^d * (∑ s in S, C (f s) * monic_vanishing_at_except α S s)
  - (∑ s in S, C (f s * (α s)^d) * monic_vanishing_at_except α S s)
  = monic_vanishing_at α S * ∑ s in S, ∑ j in range d, C (f s * (α s)^j) * X^(d-1-j) :=
by
  have inner1: ∀ s, s ∈ S →
         (X^d * (C (f s) * monic_vanishing_at_except α S s) - C ((f s * (α s)^d)) * monic_vanishing_at_except α S s)
        = (monic_vanishing_at α S) * ((∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s)) :=
  by
    intro s sinS
    calc
      _ = (X^d - C ((α s)^d)) * C (f s) * monic_vanishing_at_except α S s := by rw[sub_mul,C_mul]; ring_nf
      _ = (X - C (α s)) * (∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s) * monic_vanishing_at_except α S s := by rw[mul_neg_geom_sum2_X_C d (α s)]
      _ = (monic_vanishing_at_except α S s * (X - C (α s))) * ((∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s)) := by ring
      _ = (monic_vanishing_at α S) * ((∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s)) := by rw[monic_vanishing_at_except_filter α S s sinS]
  have inner2: ∀ s j,
    (C ((α s)^j) * X^(d-1-j)) * C (f s) = C (f s * (α s)^j) * X^(d-1-j) :=
  by
    intro s j
    rw[C_mul]
    group
  have inner3: ∀ s, 
    (∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s)
    = ∑ j in range d, C (f s * (α s)^j) * X^(d-1-j) :=
  by
    intro s
    rw[sum_mul]
    apply sum_congr
    simp only
    intro j _
    rw[inner2 s j]
  calc
    _ = X^d * (∑ s in S, C (f s) * monic_vanishing_at_except α S s) - (∑ s in S, C ((f s * (α s)^d)) * monic_vanishing_at_except α S s) := rfl
    _ = (∑ s in S, X^d * (C (f s) * monic_vanishing_at_except α S s)) - (∑ s in S, C ((f s * (α s)^d)) * monic_vanishing_at_except α S s) := by rw[mul_sum]
    _ = ∑ s in S, (X^d * (C (f s) * monic_vanishing_at_except α S s) - C ((f s * (α s)^d)) * monic_vanishing_at_except α S s) := by rw[sum_sub_distrib]
    _ = ∑ s in S, (monic_vanishing_at α S) * ((∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s)) := by
        apply sum_congr
        simp only
        intro s sinS
        rw[inner1 s sinS]
    _ = (monic_vanishing_at α S) * ∑ s in S, (∑ j in range d, C ((α s)^j) * X^(d-1-j)) * C (f s) := by rw[mul_sum]
    _ = (monic_vanishing_at α S) * ∑ s in S, ∑ j in range d, C (f s * (α s)^j) * X^(d-1-j) := by
        apply congr_arg
        apply sum_congr
        simp only
        intro s _
        rw[inner3 s]
  
theorem goppa_parity_lemma2 {α f: U → k} {S: Finset U} {d: ℕ}
: X^d * (∑ s in S, C (f s) * monic_vanishing_at_except α S s)
  - (∑ s in S, C (f s * (α s)^d) * monic_vanishing_at_except α S s)
  = monic_vanishing_at α S * ∑ j in range d, C (∑ s in S, f s * (α s)^j) * X^(d-1-j) :=
by calc
  _ = monic_vanishing_at α S * ∑ s in S, ∑ j in range d, C (f s * (α s)^j) * X^(d-1-j) := by
        rw[goppa_parity_lemma]
  _ = monic_vanishing_at α S * ∑ j in range d, ∑ s in S, C (f s * (α s)^j) * X^(d-1-j) := by
        rw[sum_comm]
  _ = monic_vanishing_at α S * ∑ j in range d, C (∑ s in S, f s * (α s)^j) * X^(d-1-j) := by
        apply congr_arg
        apply sum_congr; simp only; intro j _
        rw[map_sum C,sum_mul]

theorem goppa_parity
  {α c: U → k} {S: Finset U} {A G: k[X]} {d: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Gdeg: G.degree = d)
  (GA: IsCoprime G A)
: (G ∣ ∑ s in S, C (c s) * monic_vanishing_at_except α S s
   ↔ ∀ j, j < d → ∑ s in S, (c s / G.eval (α s)) * (α s)^j = 0
  ) :=
by
  have Adeg: A.degree = S.card := by calc
    _ = (monic_vanishing_at α S).degree := by rw[Adef]
    _ = S.card := degree_monic_vanishing_at α S
  have AG: IsCoprime A G := isCoprime_comm.mpr GA
  let Z := ∑ s in S, C (c s) * monic_vanishing_at_except α S s
  let B := ∑ s in S, C (c s / G.eval (α s)) * monic_vanishing_at_except α S s
  let Q := ∑ s in S, C ((c s / G.eval (α s)) * (α s)^d) * monic_vanishing_at_except α S s
  have XdBQA: X^d*B-Q = A * ∑ j in range d, C (∑ s in S, (c s / G.eval (α s)) * (α s)^j) * X^(d-1-j) := by rw[goppa_parity_lemma2,Adef]
  have Zinterp: Z = interpolator α S (fun s ↦ c s * A.diff.eval (α s)) := sum_C_mul_monic_vanishing_at_except_eq_interpolator _ injective Adef
  have Binterp: B = interpolator α S (fun s ↦ (c s / G.eval (α s)) * A.diff.eval (α s)) := sum_C_mul_monic_vanishing_at_except_eq_interpolator _ injective Adef
  have Qinterp: Q = interpolator α S (fun s ↦ ((c s / G.eval (α s)) * (α s)^d) * A.diff.eval (α s)) := sum_C_mul_monic_vanishing_at_except_eq_interpolator _ injective Adef
  have Zdeg: Z.degree < A.degree := by rw[Zinterp,Adeg]; apply degree_interpolator_lt
  have Bdeg: B.degree < A.degree := by rw[Binterp,Adeg]; apply degree_interpolator_lt
  have Qdeg: Q.degree < A.degree := by rw[Qinterp,Adeg]; apply degree_interpolator_lt
  have AZGB: A ∣ Z-G*B := by
    have Zeval: ∀ s, s ∈ S → Z.eval (α s) = c s * A.diff.eval (α s) := by intro s sinS; rw[Zinterp,interpolator_eval injective sinS]
    have Beval: ∀ s, s ∈ S → B.eval (α s) = (c s / G.eval (α s)) * A.diff.eval (α s) := by intro s sinS; rw[Binterp,interpolator_eval injective sinS]
    have ZGBeval: ∀ s, s ∈ S → Z.eval (α s) = G.eval (α s) * B.eval (α s) := by
      intro s sinS
      have Aeval: A.eval (α s) = 0 := by rw[Adef]; exact monic_vanishing_at_vanishes α S sinS
      have Gnonzero: G.eval (α s) ≠ 0 := no_shared_root_if_coprime AG Aeval
      have cGG: G.eval (α s) * (c s / G.eval (α s)) = c s := mul_div_cancel' (c s) Gnonzero
      rw[Zeval s sinS,Beval s sinS,← mul_assoc,cGG]
    have ZGBeval2: ∀ s, s ∈ S → (Z-G*B).eval (α s) = 0 := by
      intro s sinS
      calc
        _ = Z.eval (α s) - G.eval (α s) * B.eval (α s) := by rw[eval_sub,eval_mul]
        _ = 0 := by rw[ZGBeval s sinS]; group
    rw[Adef]
    exact monic_vanishing_at_divides S (Z-G*B) injective ZGBeval2
  constructor
  . intro GdivZ j jd
    have GdivZcopy: G ∣ ∑ s in S, C (c s) * monic_vanishing_at_except α S s := GdivZ
    cases GdivZcopy with | intro ZG GZG =>
    have dZGdeg: d + ZG.degree < A.degree := by calc
      _ = G.degree + ZG.degree := by rw[Gdeg]
      _ = (G*ZG).degree := by rw[degree_mul]
      _ = Z.degree := by rw[← GZG]
      _ < A.degree := Zdeg
    have BZG: B = ZG := by
      have AZGB2: A ∣ ZG-B := by
        have AZZGB: A ∣ G*(ZG-B) := by rw[mul_sub,← GZG]; exact AZGB
        exact dvd_if_dvd_mul_left AG AZZGB
      have ZGBdeg: (ZG-B).degree < A.degree := by
        have ZGdeg: ZG.degree < A.degree := lt_if_nat_add_lt dZGdeg 
        calc
          _ ≤ max ZG.degree B.degree := degree_sub_le ZG B
          _ < A.degree := max_lt ZGdeg Bdeg 
      have ZGB0: ZG-B = 0 := eq_zero_of_dvd_of_degree_lt AZGB2 ZGBdeg
      exact Eq.symm (eq_if_sub_zero ZGB0)
    have XdBQdeg: ((X:k[X])^d*B-Q).degree < A.degree := by
      have dBdeg: d + B.degree < A.degree := by rw[BZG]; exact dZGdeg
      have XdBdeg: ((X:k[X])^d*B).degree < A.degree := by calc
        _ = ((X:k[X])^d).degree + B.degree := degree_mul
        _ = d + B.degree := by rw[degree_pow,degree_X,nsmul_eq_mul,mul_one]
        _ < A.degree := dBdeg
      calc
        _ ≤ max ((X:k[X])^d*B).degree Q.degree := degree_sub_le (X^d*B) Q
        _ < A.degree := max_lt XdBdeg Qdeg
    have sum0: ∑ j in range d, C (∑ s in S, (c s / G.eval (α s)) * (α s)^j) * X^(d-1-j) = 0 := by
      have XdBQA2: A ∣ X^d*B-Q := by
        apply Dvd.intro (∑ j in range d, C (∑ s in S, (c s / G.eval (α s)) * (α s)^j) * X^(d-1-j))
        rw[XdBQA]
      have XdBQ0: X^d*B-Q = 0 := eq_zero_of_dvd_of_degree_lt XdBQA2 XdBQdeg
      have Anonzero: A ≠ 0 := by rw[Adef]; exact monic_vanishing_at_nonzero α S
      rw[XdBQ0] at XdBQA
      apply zero_if_mul_left_zero Anonzero (Eq.symm XdBQA)
    exact zero_coeff_of_zero_poly_as_sum sum0 j jd
  intro zerocoeff
  have XdBQ: X^d*B = Q := by
    have XdBQ0: X^d*B-Q = 0 := by
      rw[XdBQA]
      rw[mul_eq_zero]; right
      apply sum_eq_zero
      intro j jd
      rw[mem_range] at jd
      rw[mul_eq_zero]; left
      rw[zerocoeff,map_zero]
      exact jd
    exact eq_if_sub_zero XdBQ0
  have GBdeg: (G*B).degree < A.degree := by calc
    _ = G.degree + B.degree := by rw[degree_mul]
    _ = d + B.degree := by rw[Gdeg]
    _ = ((X:k[X])^d).degree + B.degree := by rw[degree_pow,degree_X,nsmul_eq_mul,mul_one]
    _ = (X^d*B).degree := by rw[degree_mul]
    _ = Q.degree := by rw[XdBQ]
    _ < A.degree := Qdeg
  have ZGB: Z = G*B := by
    have ZGBdeg: (Z-G*B).degree < A.degree := by calc
      _ ≤ max Z.degree (G*B).degree := degree_sub_le Z (G*B)
      _ < A.degree := max_lt Zdeg GBdeg
    have ZGB0: Z-G*B = 0 := eq_zero_of_dvd_of_degree_lt AZGB ZGBdeg
    exact eq_if_sub_zero ZGB0
  apply Dvd.intro B
  rw[← ZGB]

end goppa_parity