import Mathlib.Data.Finset.Basic
import Goppadecoding.hamming
import Goppadecoding.vanishing

namespace Goppadecoding

open Polynomial

section vanishing_hamming

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

theorem hamming_weight_roots_eq_degree_if_dvd_monic_vanishing_at {α e: U → k} {S: Finset U} {a: k[X]}:
  Set.InjOn α S →
  a ∣ monic_vanishing_at α S →
  (∀ s, s ∈ S → e s = if a.eval (α s) = 0 then 1 else 0) →
  hamming_weight e S = a.degree := by
    intro injective amv ea
    have earoots: hamming_weight e S = (S.filter (fun s ↦ a.eval (α s) = 0)).card := by
      unfold hamming_weight
      apply congr_arg
      ext s
      simp only [ne_eq, Finset.mem_filter, and_congr_right_iff]
      intro sinS
      rw[ea s sinS]
      simp only [ite_eq_right_iff, one_ne_zero, not_forall, exists_prop, and_true]
    have arootsadeg: (S.filter (fun s ↦ a.eval (α s) = 0)).card = a.degree :=
      roots_card_eq_degree_if_dvd_monic_vanishing_at injective amv
    calc
      ((hamming_weight e S): WithBot ℕ)
        = ((S.filter (fun s ↦ a.eval (α s) = 0)).card: WithBot ℕ) := by norm_cast
      _ = a.degree := arootsadeg

end vanishing_hamming