import Mathlib.RingTheory.Polynomial.Basic
import Mathlib.FieldTheory.PerfectClosure
import Mathlib.Algebra.CharP.Two
import Goppadecoding.nat
import Goppadecoding.sq
import Goppadecoding.diff

open Polynomial

namespace Goppadecoding

section lemmas_char2

theorem zero_in_char_2_if_even {k: Type _} [Field k] [CharP k 2] (n: ℕ)
  (even: Even n): (n:k) = 0 :=
by
  rw[even_iff_exists_two_mul] at even
  cases even with | intro c nc =>
    simp only [nc, Nat.cast_mul, Nat.cast_ofNat, CharTwo.two_eq_zero, zero_mul]

theorem one_in_char_2_if_not_even {k: Type _} [Field k] [CharP k 2] (n: ℕ)
  (odd: ¬Even n): (n:k) = 1 :=
by
  rw[Nat.even_iff_not_odd] at odd
  simp only[not_not] at odd
  rw[odd_iff_exists_bit1] at odd
  unfold bit1 at odd
  unfold bit0 at odd
  cases odd with | intro c nc =>
    simp only [nc, Nat.cast_add, CharTwo.add_self_eq_zero, Nat.cast_one, zero_add]

theorem derivative_is_square {k: Type _} [Field k] [CharP k 2] [PerfectRing k 2] (h: k[X]):
  ∃ q, h.diff = q^2 :=
by
  rw[diff]
  simp
  rw[derivative_apply]
  use sum h fun n a => if Odd n then C (pthRoot k 2 a) * X^((n-1)/2) else 0
  unfold Polynomial.sum
  rw[CharTwo.sum_sq]
  apply Finset.sum_congr
  simp only
  intro n _
  by_cases nparity: Even n
  . simp only [nparity, zero_in_char_2_if_even, mul_zero, map_zero, ge_iff_le, zero_mul, Nat.odd_iff_not_even, not_true, ite_false, ne_eq, zero_pow']
  have n1: (n:k) = 1 := by apply one_in_char_2_if_not_even n nparity
  simp only [n1, mul_one, ge_iff_le, Nat.odd_iff_not_even, nparity, not_false_eq_true, ite_true]
  rw[mul_sq,←pow_mul,sq,←C_mul,←sq]
  simp only [ge_iff_le, pthRoot_pow_p, mul_eq_mul_left_iff, _root_.map_eq_zero]
  left
  congr
  exact (half_times_2_eq_not_even_1 n nparity).symm

theorem squarefree_dvd_derivative {k: Type _} [Field k] [CharP k 2] [PerfectRing k 2] {g h: k[X]}
  (sqfree: Squarefree g) (gh: g ∣ h.diff): g^2 ∣ h.diff :=
by
  cases derivative_is_square h with | intro q hq2 =>
    rw[hq2] at gh
    rw[hq2]
    exact squarefree_dvd_square_2 g q sqfree gh

end lemmas_char2