\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.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 r n)
  }
  \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

\lemma div_suc-lem {n m : Nat} (m/=0 : m /= ) : (n + m) div m = suc (n div m)
  => div-unique (mod<right m/=0) (mod<right m/=0) m/=0 $ divModProp (n + m) m *> pmap (`+ m) (inv (divModProp n m) *> pmap (_ +) (inv (pmap (`mod m) +-comm *> n*_+_mod_n=mod.nat {m} {})) *> +-comm) *> +-assoc *> +-comm

\lemma n*_+_div_n=div {m q r : Nat} (m/=0 : m /= ) : (m * q + r) div m = q + r div m \elim q
  |  => idp
  | suc q => pmap (`div m) (+-assoc *> pmap (_ +) +-comm *> inv +-assoc) *> div_suc-lem m/=0 *> pmap suc (n*_+_div_n=div m/=0)

\lemma *_div=id {m q : Nat} (m/=0 : m /= ) : (q * m) div m = q
  => pmap (`div m) *-comm *> n*_+_div_n=div {m} {q} {} m/=0

\lemma div-monotone {n k m : Nat} (p : n <= k) : n div m <= k div m
  => aux n <=-refl p
  \where
    \lemma aux (c : Nat) {n k m : Nat} (q : n <= c) (p : n <= k) : n div m <= k div m \elim c, m
      | _,  => p
      | , _ => rewrite (<=_exists q) zero<=_
      | suc c, suc _ \as m => \case LinearOrder.dec<_<= n m, LinearOrder.dec<_<= k m \with {
        | inl n<m, _ => transportInv (`<= _) (div_< n<m) zero<=_
        | inr m<=n, inl k<m => absurd $ <-irreflexive $ k<m <∘l m<=n <∘l p
        | inr m<=n, inr m<=k => \case m \as m', idp : m' = m \with {
          | , s => rewriteI s p
          | suc xxx, s =>
            \have m/=0 m=0 => suc/=0 (s *> m=0)
            \in rewriteI (<=_exists m<=n, <=_exists m<=k, NatSemiring.+-comm) $ rewrite {} NatSemiring.+-comm $
                  transport2 (<=) (inv $ div_suc-lem m/=0) (inv $ div_suc-lem m/=0) $ suc<=suc $ aux c (cases (n,q) \with {
                    | , _ => zero<=_
                    | suc n, q => -'<=id <=∘ suc<=suc.conv q
                  }) (-'-monotone-left p)
        }
      }

\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 => (x + y : Nat)
  | zro-left {x} => pmap Fin.fromNat zro-left *> fin_mod_id x
  | +-assoc => mod_+-left *> pmap Fin.fromNat +-assoc *> inv mod_+-right
  | +-comm => pmap Fin.fromNat +-comm
  | ide => Fin.fromNat 
  | * x y => (x * y : Nat)
  | ide-left {x} => mod_*-left *> pmap Fin.fromNat ide-left *> fin_mod_id x
  | *-assoc => mod_*-left *> pmap Fin.fromNat *-assoc *> inv mod_*-right
  | ldistr {x} {y} {z} => mod_*-right *> pmap Fin.fromNat ldistr *> inv (mod_+-left *> mod_+-right)
  | negative x => 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 Fin.fromNat *-comm
  | natCoef => Fin.fromNat
  | 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 y n)

    \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 finEq-modeq {x y n : Nat} (p : x = {Fin (suc n)} y) : x Nat.mod suc n = {Nat} y Nat.mod suc n
      => cong

    \lemma ldiv-finEq {x y n : Nat} (p : ∃ (Monoid.LDiv {IntEuclidean} (suc n) (x Nat.- y))) : x = {Fin (suc n)} y
      => 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 \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
      => rewrite (natMod=mod k (suc n), fin_mod_id k) 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))
  }

\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 Fin.fromNat (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)
         }
  }