-rw-r--r-- 15586 leangoppa-20230726/Goppadecoding/goppa_binary.lean raw
import Mathlib.RingTheory.Polynomial.Basic
import Goppadecoding.logic
import Goppadecoding.vanishing
import Goppadecoding.approximant
import Goppadecoding.interpolator
import Goppadecoding.hamming
import Goppadecoding.vanishing_hamming
import Goppadecoding.reedsolomon
import Goppadecoding.diff

open Polynomial BigOperators

namespace Goppadecoding

section goppa_binary

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

theorem goppa_decoding
  {α e: U → k} {S: Finset U} {A B a b G: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Gdeg: G.degree = 2*t)
  (GA: IsCoprime G A)
  (appr: approximant A B t a b)
  (einF2: (∀ s, s ∈ S → e s = 0 ∨ e s = 1))
  (wt: hamming_weight e S ≤ t)
  (codeword: G ∣
     ∑ s in S,
         C (((G * B).eval (α s) / A.diff.eval (α s) - e s))
         * monic_vanishing_at_except α S s)
: ((∀ s, s ∈ S → e s = if a.eval (α s) = 0 then 1 else 0)
   ∧ hamming_weight e S = a.degree
   ∧ a ∣ A
   ∧ a ∣ G*b - a.diff
   ∧ 2*t + (a*B-b*A).degree < S.card + a.degree
  ) :=
by
  have AG: IsCoprime A G := isCoprime_comm.mpr GA
  let c := fun s ↦ (G*B).eval (α s) / A.diff.eval (α s) - e s
  have Gc: G ∣ ∑ s in S, C (c s) * monic_vanishing_at_except α S s := codeword
  cases Gc with
  | intro f Gf =>
    have fdeg: 2*t + f.degree < A.degree := by calc
      _ = G.degree + f.degree := by rw[Gdeg]
      _ = (G*f).degree := by rw[degree_mul]
      _ = (∑ s in S, C (c s) * monic_vanishing_at_except α S s).degree := by rw[←Gf]
      _ < S.card := by
            apply sum_degree_lt S
            intro s sinS
            apply degree_C_mul_lt_if_degree_lt
            apply degree_monic_vanishing_at_except sinS
      _ = A.degree := by rw[Adef,degree_monic_vanishing_at α S]
    have Aprimeevalnonzero: ∀ s, s ∈ S → A.diff.eval (α s) ≠ 0 := by
      intro s sinS
      rw[Adef]
      exact derivative_monic_vanishing_at_eval_nonzero α injective sinS
    have Gfeval: ∀ s, s ∈ S → (G*f).eval (α s) = c s * A.diff.eval (α s) := by
      intro s sinS
      calc
        _ = (∑ s in S, C (c s) * monic_vanishing_at_except α S s).eval (α s) := by rw[←Gf]
        _ = (interpolator α S (fun s ↦ c s * A.diff.eval (α s))).eval (α s) := by rw[sum_C_mul_monic_vanishing_at_except_eq_interpolator _ injective Adef]
        _ = c s * A.diff.eval (α s) := by apply interpolator_eval injective sinS
    have GBfeval: ∀ s, s ∈ S → (G*(B-f)).eval (α s) = e s * A.diff.eval (α s) := by
      intro s sinS
      calc
        _ = (G*B-G*f).eval (α s) := by ring_nf
        _ = (G*B).eval (α s) - (G*f).eval (α s) := by rw[eval_sub]
        _ = (G*B).eval (α s) - (c s * A.diff.eval (α s)) := by rw[Gfeval s sinS]
        _ = (G*B).eval (α s) - (((G*B).eval (α s) / A.diff.eval (α s) - e s) * A.diff.eval (α s)) := rfl
        _ = (G*B).eval (α s) - ((G*B).eval (α s) / A.diff.eval (α s) * A.diff.eval (α s)) + e s * A.diff.eval (α s) := by ring
        _ = (G*B).eval (α s) - (G*B).eval (α s) + e s * A.diff.eval (α s) := by rw[div_mul_cancel _ (Aprimeevalnonzero s sinS)]
        _ = e s * A.diff.eval (α s) := by group
    have Bfevalnonzero: ∀ s, s ∈ S → ((B-f).eval (α s) ≠ 0 ↔ e s ≠ 0) := by
      intro s sinS
      constructor
      . intro Bfnonzero
        have esAnonzero: e s * A.diff.eval (α s) ≠ 0 := by
          have Aeval: A.eval (α s) = 0 := by
            rw[Adef]
            exact monic_vanishing_at_vanishes α S sinS
          have Gnonzero: G.eval (α s) ≠ 0 := by
            exact no_shared_root_if_coprime AG Aeval
          calc
            _ = (G*(B-f)).eval (α s) := by rw[GBfeval s sinS]
            _ = G.eval (α s) * (B-f).eval (α s) := by rw[eval_mul]
            _ ≠ 0 := mul_ne_zero Gnonzero Bfnonzero
        exact nonzero_if_mul_right_nonzero esAnonzero
      . intro esnonzero
        have GBfnonzero: G.eval (α s) * (B-f).eval (α s) ≠ 0 := by calc
          _ = (G*(B-f)).eval (α s) := by rw[eval_mul]
          _ = e s * A.diff.eval (α s) := GBfeval s sinS
          _ ≠ 0 := mul_ne_zero esnonzero (Aprimeevalnonzero s sinS)
        exact nonzero_if_mul_left_nonzero GBfnonzero
    have Bfevalzero: ∀ s, s ∈ S → ((B-f).eval (α s) = 0 ↔ e s = 0) := by
      intro s sinS
      constructor
      . contrapose
        repeat rw[← not_eq_iff]
        rw[Bfevalnonzero s sinS]
        simp only [ne_eq, imp_self]
      . contrapose
        repeat rw[← not_eq_iff]
        rw[Bfevalnonzero s sinS]
        simp only [ne_eq, imp_self]
    let Bf := fun s ↦ B.eval (α s) - f.eval (α s)
    have wtBfwte: hamming_weight Bf S = hamming_weight e S := by calc
      _ = (S.filter (fun s ↦ B.eval (α s) - f.eval (α s) ≠ 0)).card := rfl
      _ = (S.filter (fun s ↦ (B-f).eval (α s) ≠ 0)).card := by simp only [CharTwo.sub_eq_add, ne_eq, eval_add]
      _ = (S.filter (fun s ↦ e s ≠ 0)).card := by
            apply congr_arg
            ext s
            rename_i inst inst_1 inst_2 inst_3
            aesop_subst Adef
            simp_all only [CharTwo.sub_eq_add, eval_add, ne_eq, eval_mul, map_add, Finset.mem_filter, and_congr_right_iff, implies_true]
      _ = hamming_weight e S := rfl
    have wtBf: hamming_weight Bf S ≤ t := by calc
      _ = hamming_weight e S := wtBfwte
      _ ≤ t := wt
    have Bfx: ∀ s, s ∈ S → Bf s = B.eval (α s) - f.eval (α s) := by simp only [CharTwo.sub_eq_add, implies_true]
    have iwe: a ∣ A ∧ a ≠ 0 ∧ f = B-b*(A/a) ∧ 2*t + degree (a*B-b*A) < S.card + degree a ∧ { s ∈ S | Bf s ≠ 0 } = { s ∈ S | a.eval (α s) = 0 } := interpolation_with_errors injective Adef appr fdeg Bfx wtBf
    have aA: a ∣ A := iwe.1
    have anonzero: a ≠ 0 := iwe.2.1
    have fBbAa: f = B-b*(A/a) := iwe.2.2.1
    have degaBbA: 2*t + degree (a*B-b*A) < S.card + degree a := iwe.2.2.2.1
    have Bfa: { u ∈ S | Bf u ≠ 0 } = { u ∈ S | a.eval (α u) = 0 } := iwe.2.2.2.2
    have amv: a ∣ monic_vanishing_at α S := by rw[← Adef]; exact aA
    have ea: ∀ s, s ∈ S → e s = if a.eval (α s) = 0 then 1 else 0 := by
      intro s sinS
      by_cases a0: a.eval (α s) = 0
      . simp only [a0, ite_true]
        have sina: s ∈ { u ∈ S | a.eval (α u) = 0 } := by simp only [Set.mem_setOf_eq, sinS, a0, and_self]
        have sinBf: s ∈ { u ∈ S | Bf u ≠ 0 } := by rw[Bfa]; exact sina
        rw[Set.mem_setOf] at sinBf
        have Bfs: Bf s ≠ 0 := and_imp_right sinBf
        have Bfs2: B.eval (α s) - f.eval (α s) ≠ 0 := Bfs
        have esnonzero: e s ≠ 0 := by
          rw[← Bfevalnonzero s sinS]
          rw[eval_sub]
          exact Bfs2
        have es0or1: e s = 0 ∨ e s = 1 := einF2 s sinS
        rw[or_iff_not_imp_left] at es0or1
        exact es0or1 esnonzero
      . simp only [a0, ite_false]
        have sina: s ∉ { u ∈ S | a.eval (α u) = 0 } := by simp only [Set.mem_setOf_eq, sinS, a0, and_false, not_false_eq_true]
        have sinBf: s ∉ { u ∈ S | Bf u ≠ 0 } := by rw[Bfa]; exact sina
        rw[Set.nmem_setOf_iff] at sinBf
        rw[not_and] at sinBf
        rw[not_ne_iff] at sinBf
        have Bfs: Bf s = 0 := sinBf sinS
        have Bfs2: B.eval (α s) - f.eval (α s) = 0 := Bfs
        rw[← Bfevalzero s sinS]
        rw[eval_sub]
        exact Bfs2
    constructor
    . exact ea
    constructor
    . exact hamming_weight_roots_eq_degree_if_dvd_monic_vanishing_at injective amv ea
    constructor
    . exact aA
    constructor
    . have Gba: ∀ s, s ∈ S → a.eval (α s) = 0 → (G*b - a.diff).eval (α s) = 0 := by
        intro s sinS as0
        have aAa: a*(A/a) = A := EuclideanDomain.mul_div_cancel' anonzero aA
        have derivA: a*(A/a).diff + (a.diff)*(A/a) = A.diff := by calc
          _ = (a*(A/a)).diff := by rw[add_comm,diff]; simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, derivative_mul]
          _ = A.diff := by rw[aAa]
        have derivAeval: a.diff.eval (α s) * (A/a).eval (α s) = A.diff.eval (α s) := by calc
          _ = 0 * (A/a).diff.eval (α s) + a.diff.eval (α s) * (A/a).eval (α s) := by ring
          _ = a.eval (α s) * (A/a).diff.eval (α s) + a.diff.eval (α s) * (A/a).eval (α s) := by rw[as0]
          _ = (a*(A/a).diff).eval (α s) + (a.diff*(A/a)).eval (α s) := by repeat rw[eval_mul]
          _ = (a*(A/a).diff + (a.diff)*(A/a)).eval (α s) := by rw[eval_add]
          _ = A.diff.eval (α s) := by rw[derivA]
        have AprimeGbae: A.diff.eval (α s) * (G*b).eval (α s) = A.diff.eval (α s) * (a.diff.eval (α s) * e s) := by calc
          _ = (a.diff.eval (α s) * (A/a).eval (α s)) * (G*b).eval (α s) := by rw[derivAeval]
          _ = a.diff.eval (α s) * ((A/a).eval (α s) * (G*b).eval (α s)) := by rw[mul_assoc]
          _ = a.diff.eval (α s) * ((A/a)*(G*b)).eval (α s) := by rw[← eval_mul]
          _ = a.diff.eval (α s) * (G*(b*(A/a))).eval (α s) := by group
          _ = a.diff.eval (α s) * (G*(B-f)).eval (α s) := by rw[fBbAa]; group
          _ = a.diff.eval (α s) * (e s * A.diff.eval (α s)) := by rw[GBfeval s sinS]
          _ = _ := by group
        have Gbae: (G*b).eval (α s) = a.diff.eval (α s) * e s := mul_left_cancel₀ (Aprimeevalnonzero s sinS) AprimeGbae
        have es1: e s = 1 := by rw[ea s sinS]; simp only[as0,ite_true]
        rw[es1] at Gbae
        rw[eval_sub,Gbae]
        ring
      rw[Adef] at aA
      apply dvd_if_dvd_monic_vanishing_at_and_root_imp_root injective aA Gba
    exact degaBbA

theorem goppa_checking
  {α e: U → k} {S: Finset U} {A B a b G: k[X]} {t: ℕ}
  (injective: Set.InjOn α S)
  (Adef: A = monic_vanishing_at α S)
  (Gdeg: G.degree = 2*t)
  (aA: a ∣ A)
  (aBbAdeg: 2*t + (a*B-b*A).degree < S.card + a.degree)
  (Gba: a ∣ G*b - a.diff)
  (ea: ∀ s, s ∈ S → e s = if a.eval (α s) = 0 then 1 else 0)
: (hamming_weight e S = a.degree ∧
   G ∣ ∑ s in S, C (((G * B).eval (α s) / A.diff.eval (α s) - e s)) * monic_vanishing_at_except α S s
  ) :=
by
  constructor
  . have amv: a ∣ monic_vanishing_at α S := by rw[← Adef]; exact aA
    exact hamming_weight_roots_eq_degree_if_dvd_monic_vanishing_at injective amv ea
  have Anonzero: A ≠ 0 := by rw[Adef]; exact monic_vanishing_at_nonzero α S
  have anonzero: a ≠ 0 := nonzero_if_divides_nonzero aA Anonzero
  have aAa: a*(A/a) = A := EuclideanDomain.mul_div_cancel' anonzero aA
  let f := B - b*(A/a)
  have af: a*f = a*B-b*A := by calc
    _ = a*(B-b*(A/a)) := rfl
    _ = a*B-b*(a*(A/a)) := by ring
    _ = a*B-b*A := by rw[aAa]
  have afdeg: (2*t + f.degree) + a.degree < S.card + a.degree := by calc
    _ = 2*t + (f.degree + a.degree) := by rw[add_assoc]
    _ = 2*t + (a.degree + f.degree) := by group
    _ = 2*t + (a*f).degree := by rw[degree_mul]
    _ = 2*t + (a*B-b*A).degree := by rw[af]
    _ < S.card + a.degree := aBbAdeg
  have Gfdeg: (G*f).degree < S.card := by calc
    _ = G.degree + f.degree := by rw[degree_mul]
    _ = 2*t + f.degree := by rw[Gdeg]
    _ < S.card := lt_of_add_lt_add_right afdeg
  have derivA: a*(A/a).diff + a.diff*(A/a) = A.diff := by calc
    _ = (a*(A/a)).diff := by rw[add_comm,diff]; simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, derivative_mul]
    _ = A.diff := by rw[aAa]
  have Aprimeevalnonzero: ∀ s, s ∈ S → A.diff.eval (α s) ≠ 0 := by
    intro s sinS
    rw[Adef]
    exact derivative_monic_vanishing_at_eval_nonzero α injective sinS
  have GbAe: ∀ s, s ∈ S → (G*b*(A/a)).eval (α s) = e s * A.diff.eval (α s) := by
    intro s sinS
    by_cases a0: a.eval (α s) = 0
    . have es1: e s = 1 := by rw[ea s sinS]; simp only [a0, ite_true]
      have derivAeval: a.diff.eval (α s) * (A/a).eval (α s) = A.diff.eval (α s) := by calc
        _ = 0 * (A/a).diff.eval (α s) + a.diff.eval (α s) * (A/a).eval (α s) := by ring
        _ = a.eval (α s) * (A/a).diff.eval (α s) + a.diff.eval (α s) * (A/a).eval (α s) := by rw[a0]
        _ = (a*(A/a).diff).eval (α s) + (a.diff*(A/a)).eval (α s) := by repeat rw[eval_mul]
        _ = (a*(A/a).diff + (a.diff)*(A/a)).eval (α s) := by rw[eval_add]
        _ = A.diff.eval (α s) := by rw[derivA]
      have Gba0: (G*b - a.diff).eval (α s) = 0 := eval_eq_zero_of_dvd_of_eval_eq_zero Gba a0
      calc
        _ = (G*b).eval (α s) * (A/a).eval (α s) := by rw[eval_mul]
        _ = ((G*b - a.diff) + a.diff).eval (α s) * (A/a).eval (α s) := by group
        _ = ((G*b - a.diff).eval (α s) + a.diff.eval (α s)) * (A/a).eval (α s) := by rw[eval_add]
        _ = (0 + a.diff.eval (α s)) * (A/a).eval (α s) := by rw[Gba0]
        _ = a.diff.eval (α s) * (A/a).eval (α s) := by group
        _ = A.diff.eval (α s) := by rw[derivAeval]
        _ = 1 * A.diff.eval (α s) := by ring
        _ = e s * A.diff.eval (α s) := by rw[es1]
    . have es0: e s = 0 := by rw[ea s sinS]; simp only [a0, ite_false]
      have aAaeval0: a.eval (α s) * (A/a).eval (α s) = 0 := by calc
        _ = (a*(A/a)).eval (α s) := by rw[eval_mul]
        _ = A.eval (α s) := by rw[aAa]
        _ = (monic_vanishing_at α S).eval (α s) := by rw[Adef]
        _ = 0 := monic_vanishing_at_vanishes α S sinS
      have Aaeval0: (A/a).eval (α s) = 0 := zero_if_mul_left_zero a0 aAaeval0
      calc
        _ = G.eval (α s) * b.eval (α s) * (A/a).eval (α s) := by repeat rw[eval_mul]
        _ = G.eval (α s) * b.eval (α s) * 0 := by rw[Aaeval0]
        _ = 0 * A.diff.eval (α s) := by ring
        _ = e s * A.diff.eval (α s) := by rw[es0]
  have GBfe: ∀ s, s ∈ S → (G*B-G*f).eval (α s) = e s * A.diff.eval (α s) := by
    intro s sinS
    calc
      _ = (G*B-G*(B-b*(A/a))).eval (α s) := rfl
      _ = (G*b*(A/a)).eval (α s) := by ring_nf
      _ = e s * A.diff.eval (α s) := by rw[GbAe s sinS]
  have GBfeover: ∀ s, s ∈ S → (G*B-G*f).eval (α s) / A.diff.eval (α s) = e s := by
    intro s sinS
    rw[GBfe s sinS]
    exact mul_div_cancel (e s) (Aprimeevalnonzero s sinS)
  have GBA: ∀ s, s ∈ S → (G*B).eval (α s) / A.diff.eval (α s) - e s = (G*f).eval (α s) / A.diff.eval (α s) := by
    intro s sinS
    calc
      _ = ((G*B-G*f)+G*f).eval (α s) / A.diff.eval (α s) - e s := by group
      _ = ((G*B-G*f).eval (α s) + (G*f).eval (α s)) / A.diff.eval (α s) - e s := by rw[eval_add]
      _ = (G*B-G*f).eval (α s) / A.diff.eval (α s) + (G*f).eval (α s) / A.diff.eval (α s) - e s := by rw[add_div]
      _ = e s + (G*f).eval (α s) / A.diff.eval (α s) - e s := by rw[GBfeover s sinS]
      _ = (G*f).eval (α s) / A.diff.eval (α s) := by group
  let r := fun s ↦ (G*f).eval (α s)
  have rmatches: ∀ s, s ∈ S → (G*f).eval (α s) = r s := by
    intro s _
    simp only
  have Gf: ∑ s in S, C (((G * B).eval (α s) / A.diff.eval (α s) - e s)) * monic_vanishing_at_except α S s = G*f := by calc
    _ = ∑ s in S, C ((G*f).eval (α s) / A.diff.eval (α s)) * monic_vanishing_at_except α S s := by
          apply Finset.sum_congr
          simp only
          intro s sinS
          rw[GBA s sinS]
    _ = interpolator α S (fun s ↦ ((G*f).eval (α s) / A.diff.eval (α s)) * A.diff.eval (α s)) := by rw[sum_C_mul_monic_vanishing_at_except_eq_interpolator _ injective Adef]
    _ = interpolator α S (fun s ↦ (G*f).eval (α s)) := by
          unfold interpolator
          apply Finset.sum_congr
          simp only
          intro s sinS
          simp only
          rw[div_mul_cancel ((G*f).eval (α s)) (Aprimeevalnonzero s sinS)]
    _ = G*f := by rw[← interpolator_unique injective rmatches Gfdeg]
  apply Dvd.intro f
  rw[Gf]

end goppa_binary