\import Algebra.Domain.Euclidean
\import Algebra.Field
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.Prime
\import Algebra.Ring
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Arith.Int
\import Arith.Nat
\import Data.Or
\import Function
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set \hiding (#)
\open Nat(div,mod,divModProp)
\open AddMonoid

\lemma int_n*_+_mod_n {n r : Nat} {q : Int} (r<=n : r < suc n) : (pos (suc n) * q + r) mod suc n = r
  => mod-unique {(pos (suc n) * q + r) div suc n} {q} natMod<right r<=n (natDivModProp (pos (suc n) * q + r) n)
  \where \open IntEuclidean

\lemma int_n*_+_mod_n=mod {n : Nat} {q r : Int} : (pos (suc n) * q + r) mod suc n = r mod suc n
  => run {
    rewriteI {} (natDivModProp r n),
    rewriteI (IntRing.+-assoc {pos (suc n) * q} {pos (suc n) * r div suc n} {pos (r mod suc n)}, IntRing.ldistr {suc n} {q} {r div suc n}),
    int_n*_+_mod_n natMod<right
  }
  \where \open IntEuclidean

\lemma int_mod_*-left {n : Nat} {a b : Int} : (pos (a mod suc n) * b) mod suc n = (a * b) mod suc n
  => run {
    rewriteI {} (natDivModProp a n),
    rewrite (IntRing.rdistr, IntRing.*-assoc),
    inv int_n*_+_mod_n=mod
  }
  \where \open IntEuclidean

\lemma int_mod_*-right {n : Nat} {a b : Int} : (a * b mod suc n) mod suc n = (a * b) mod suc n
  => pmap (mod _) *-comm *> int_mod_*-left *> pmap (mod _) *-comm
  \where \open IntEuclidean

\func base-digit (n b j : Nat) : Nat \elim j
  |  => n mod b
  | suc j => base-digit (n div b) b j

\lemma base-digit-sum {l : Array Nat} {b : Nat} (p : \Pi (j : Fin l.len) -> l j < b) {j : Fin l.len}
  : l j = base-digit (BigSum (\lam j => l j * Monoid.pow b j)) b j \elim l, j
  | a :: l,  => inv $ pmap (mod b) +-comm *> pmap (\lam x => (x + a) mod b) (inv $ *-comm *> Semiring.BigSum-rdistr *> pmap BigSum (exts \lam j => *-assoc)) *> n*_+_mod_n {b} {BigSum (\lam j => l j * Monoid.pow b j)} (p )
  | a :: l, suc j => base-digit-sum (\lam j => p (suc j)) *> pmap (base-digit __ b j) (unfold BigSum $ inv $ pmap (div b) +-comm *> pmap (\lam x => (x + a) div b) (inv $ *-comm *> Semiring.BigSum-rdistr *> pmap BigSum (exts \lam j => *-assoc)) *> n*_+_div_n=div (later \lam b=0 => \case rewrite b=0 in p ) *> pmap (_ +) (div_< (p )) *> zro-right)

\instance FinRing {n : Nat} : CRing.Dec (Fin (suc n))
  | zro => 
  | + x y => finMod (x + y)
  | zro-left {x} => pmap finMod zro-left *> fin_mod_id x
  | +-assoc => mod_+-left *> pmap finMod +-assoc *> inv mod_+-right
  | +-comm => pmap finMod +-comm
  | ide => finMod 
  | * x y => finMod (x * y)
  | ide-left {x} => mod_*-left *> pmap finMod ide-left *> fin_mod_id x
  | *-assoc => mod_*-left *> pmap finMod *-assoc *> inv mod_*-right
  | ldistr {x} {y} {z} => mod_*-right *> pmap finMod ldistr *> inv (mod_+-left *> mod_+-right)
  | negative x => finMod $ iabs (suc n Nat.- x)
  | negative-left {x} =>
    \let t => pmap (+ pos x) (pos_iabs (<=-less (fin_< x))) *> IntRing.+-assoc {pos (suc n)} {neg x} *> pmap (_ +) (IntRing.negative-left {pos x})
    \in mod_+-left *> transport (__ Nat.mod suc n = ) (inv (pmap iabs t)) (fin_nat-inj (n*_+_mod_n {_} {} NatOrder.zero<suc))
  | decideEq x y => \case NatSemiring.decideEq x y \with {
    | yes x=y => yes (fin_nat-inj x=y)
    | no x/=y => no (\lam p => x/=y p)
  }
  | *-comm => pmap finMod *-comm
  | natCoef => finMod
  | natCoefZero => idp
  | natCoefSuc m => inv (mod_+-left *> mod_+-right)
  \where {
    \open IntEuclidean

    \lemma mod-mod {a : Int} {n : Nat} : a mod pos (suc n) Nat.mod suc n = {Nat} a mod pos (suc n)
      => mod_< {a mod pos (suc n)} {suc n} natMod<right

    \lemma ldiv-modEq (x y : Int) (n : Nat) (p : ∃ (Monoid.LDiv {IntEuclidean} (suc n) (x - y))) : x mod suc n = y mod suc n \elim p
      | inP (e, p) => rewrite (rewrite (+-assoc, negative-left, zro-right) in inv (pmap (+ y) p)) $
      rewrite (ldistr, +-assoc, natDivModProp y n) in int_n*_+_mod_n {n} {y mod suc n} {e + y div pos (suc n)} natMod<right

    \sfunc modEq-ldiv (x y : Int) (n : Nat) (p : x mod suc n = y mod suc n) : Monoid.LDiv {IntEuclidean} (suc n) (x - y)
      => \have A x => divModProp x (suc n) \case __
         \in rewriteI (A x, A y, p) \new Monoid.LDiv {
          | inv => x div pos (suc n) - y div pos (suc n)
          | inv-right => rewrite AbGroup.sum-cancel-right Ring.ldistr_-
        }

    \lemma ldiv-finEq {x y n : Nat} (p : ∃ (Monoid.LDiv {IntEuclidean} (suc n) (x Nat.- y))) : x Nat.mod suc n = y Nat.mod suc n
      => fin_nat-inj (repeat {} (rewrite natMod=mod) in ldiv-modEq (pos x) (pos y) n p)

    \lemma intCoef-char (n : Nat) (k : Int) : (FinRing {n}).intCoef k = k mod suc n Nat.mod suc n \elim k {
      | pos zero => idp
      | pos (suc m) => rewrite (natCoefSuc, fin_mod_id {n} (_ Nat.mod suc n)) idp
      | neg (suc m) => ldiv-finEq $ inP \case suc m Nat.mod suc n \as r, idp : suc m Nat.mod suc n = {Nat} r \with {
        | zero, P => \new Monoid.LDiv {
          | inv => 
          | inv-right => unfold (rewrite P idp)
        }
        | suc r, P => \new Monoid.LDiv {
          | inv => 
          | inv-right => unfold (rewrite (P, IntRing.minus__) idp)
        }
      }
    }

    \lemma intCoef_pos-char {n : Nat} (k : Nat) : (FinRing {n}).intCoef (pos k) = k Nat.mod suc n
      => rewrite (natMod=mod k (suc n), fin_mod_id (k Nat.mod suc n)) in intCoef-char n (pos k)

    \lemma intCoef-surj {n : Nat} : IsSurj (FinRing {n}).intCoef => \lam y => inP (y, aux y)
      \where
        \private \lemma aux {n : Nat} (k : Fin (suc n)) : (FinRing {n}).natCoef k = k \elim n, k
          | n,  => natCoefZero
          | n, suc k => rewrite (natCoefSuc k, aux k, mod_+-right) (fin_mod_id (suc k))

    \lemma intHom {n : Nat} : RingHom IntRing (FinRing {n}) (__ mod suc n Nat.mod suc n)
      => transport (RingHom _ _) (ext (FinRing.intCoef-char n)) intMap
  }

\instance FinEuclidean {n : Nat} : EuclideanRingData (Fin (suc n))
  | CRing => FinRing {n}
  | decideEq => decideEq
  | euclideanMap x => x
  | divMod x y =>
    \let! (d,m) => Nat.divMod x y
    \in (d `mod` suc n, m `mod` suc n)
  | isDivMod x y => run {
    unfold_let,
    rewrite mod_*-right,
    mod_+-left *> mod_+-right *> pmap finMod (Nat.divModProp x y) *> fin_mod_id x
  }
  | isEuclideanMap x y y/=0 _ => mod<=left <∘r mod<right (fin_nat-ineq y/=0)

\instance FinField {n : Nat} {p : Prime (suc n)} : DiscreteField (Fin (suc n))
  | CRing => FinRing {n}
  | zro/=ide => \case __ *> {Nat} mod_< (NatOrder.suc<suc (nonZero>0 (\lam n=0 => p.notInv (transportInv (\lam x => Inv (suc x)) n=0 Inv.ide-isInv))))
  | finv x => (IntEuclidean.natDivMod (bezout (pos (suc n)) (pos x)). (suc n)). mod suc n
  | finv_zro => idp
  | finv-right {x} x/=0 =>
    \let | (u,v) => bezout (pos (suc n)) (pos x)
         | (q,r) => IntEuclidean.natDivMod v (suc n)
         | int_gcd=1 : gcd (pos (suc n)) (pos x) =  => int_gcd_pos *> pmap pos (gcd=1 p (fin_nat-ineq x/=0) (fin_< x))
    \in *-comm *> pmap ((__ * x) mod suc n) (inv (int_n*_+_mod_n=mod *> IntEuclidean.natMod=mod r (suc n)) *> pmap (__ IntEuclidean.mod suc n) (IntEuclidean.natDivModProp v n)) *>
                  fin_nat-inj (inv (IntEuclidean.natMod=mod _ _) *> int_mod_*-left *> inv int_n*_+_mod_n=mod *> pmap (__ IntEuclidean.mod suc n) (pmap (__ + v * pos x) *-comm *> bezoutIdentity (pos (suc n)) (pos x) *> int_gcd=1) *> IntEuclidean.natMod=mod  (suc n))
  | decideEq x y => \case NatSemiring.decideEq x y \with {
    | yes x=y => yes (fin_nat-inj x=y)
    | no x/=y => no (\lam x=y => x/=y x=y)
  }
  \where {
    \open EuclideanSemiringData
    \open EuclideanRingData
    \open Monoid(Inv)

    \lemma gcd=1 (p : Prime {NatSemiring}) {x : Nat} (x/=0 : Not (x = )) (x<p : x < p) : gcd p x = 
      => \case nat_irr p (GCD.res|val1 {gcd-isGCD p x}) \with {
           | byLeft gcd=1 => gcd=1
           | byRight gcd=p =>
             \have p<=x => transport (<= x) gcd=p (ldiv_<= x/=0 (GCD.res|val2 {gcd-isGCD p x}))
             \in absurd (p<=x x<p)
         }
  }