\import Algebra.Domain.Bezout
\import Algebra.Domain.Euclidean
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.Sub
\import Algebra.Group.Symmetric
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.Sub
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Factor
\import Algebra.Ring.Ideal
\import Algebra.Ring.QuotientProperties
\import Algebra.Ring.RingCategory
\import Algebra.Ring.RingHom
\import Algebra.Semiring
\import Arith.Fin
\import Arith.Int
\import Arith.Nat
\import Category
\import Equiv
\import Function (IsSurj)
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Set
\import Set.Fin
\import Set.Fin.Instances
\import Set.Fin.Pigeonhole
\import Set.SetHom
\open IntEuclidean \hiding (isDivMod,mod-unique)
\open FinRing
\open Monoid

\func coPrimes (n : Nat) : FinSet
  => SigmaFin (FinFin (suc n)) \lam k => DecFin $ decideEq (NatEuclidean.gcd k (suc n)) 

\instance InvSubMonoid (M : Monoid) : SubMonoid M
  | contains x => Inv x
  | contains_ide => Inv.ide-isInv
  | contains_* xi yi => Inv.product xi yi

\instance InvGroup (M : Monoid) : Group
  | Monoid => (InvSubMonoid M).IMonoid
  | inverse (x,xi) => (xi.inv, \new Inv {
    | inv => x
    | inv-left => Inv.inv-right
    | inv-right => Inv.inv-left
  })
  | inverse-left {x} => ext x..inv-left

\func coPrimes-eq (n : Nat) (n>0 :  NatOrder.< n) : QEquiv {coPrimes n} {InvGroup (FinRing {n})} \cowith
  | f (k, p) =>
    \let gcd-inv => gcd-inv {n} {k} (rewrite nat_gcd-comm p)
    \in (k, \new Inv {
      | inv => finv-formula k
      | inv-left => rewrite *-comm gcd-inv
      | inv-right => gcd-inv })
  | ret (k, k2) => (k,
    \let | l => k Nat.* k2.inv
         | m => suc n Nat.* (l Nat.div suc n)
         | k_n+1_coprime => run {
           BezoutRing.bezout_coprime {IntRing} {k2.inv} {neg (l Nat.div suc n)} {k},
           unfold,
           rewrite NatSemiring.*-comm,
           IntRing.cancel-right m,
           rewrite (IntRing.*-comm {_} {pos (suc n)}, rewrite IntRing.minus__ in IntRing.minus+pos l m _),
           rewriteI {} (rewrite (finEq-modeq k2.inv-right) in Nat.divModProp l (suc n)),
           rewrite (mod_< (NatOrder.suc<suc n>0)),
           pmap pos idp
         }
    \in rewrite int_gcd_pos in unfold (int_gcd-isUnique (IntEuclidean.gcd-isGCD (pos k) (pos (suc n))) (IsCoprime.=>gcd k_n+1_coprime)))
  | ret_f _ => exts idp
  | f_sec _ => exts idp
  \where {
    \open EuclideanRingData

    \func finv-formula (x : Fin (suc n)) => (IntEuclidean.natDivMod (bezout (pos (suc n)) (pos x)). (suc n)). Nat.mod suc n

    \lemma gcd-inv {x : Fin (suc n)} (x-coprime : NatEuclidean.gcd (suc n) x = {Nat} )
      : x NatSemiring.* finv-formula x = {Fin (suc n)}  Nat.mod suc n
      => \let | (u,v) => bezout (pos (suc n)) (pos x)
              | (q,r) => IntEuclidean.natDivMod v (suc n)
              | int_gcd=1 : EuclideanSemiringData.gcd (pos (suc n)) (pos x) =  => int_gcd_pos *> pmap pos x-coprime
         \in *-comm *> pmap ((__ * x) Nat.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))

  }

\func ker-int-Coef (n : Nat) : RingHom.KernelC (intMap {FinRing {n}}) = {Ideal IntEuclidean} Ideal.closure1 {IntEuclidean} (suc n)
  => exts \lam i => ext
      (\lam (c : intMap i = zro) => \case modEq-ldiv i  n $ rewriteI mod-mod $ finEq-modeq {i IntEuclidean.mod pos (suc n)} {} (rewrite intCoef-char in c) \with {
        | (a, p) => inP ((a, ()) :: nil, simplify (rewrite (IntRing.*-comm, p) linarith))
      }, \lam c => unfold $ rewrite (intCoef-char, (rewrite AddGroup.minus_zro in ldiv-modEq i  n) $ Ideal.closure1_LDiv. c) idp)

\func Z/nZ=FinRing (n : Nat) : Iso {_} {FactorRing (Ideal.closure1 {IntRing} (suc n))} {FinRing {n}}
  => transport (\lam X => Iso {_} {FactorRing X} {FinRing {n}}) (ker-int-Coef n) $
      transport (\lam X => Iso {_} {_} {X}) (CRingCat.Image=Cod (intMap {FinRing {n}}) intCoef-surj) $
        ringKerImageHom-iso (intMap {FinRing {n}})

\func EulerTotient (n : Nat) : Nat => (coPrimes n).finCard

\func chinese-map {n m : Nat} (x : FinRing {suc n * m + n}) : \Sigma (FinRing {n}) (FinRing {m})
  => (Fin.fromNat {n} x, Fin.fromNat {m} x)

\lemma natSemiring-unit {n : Nat} (p : Inv {NatSemiring} n) : n = 
  => natUnit p.inv-left

\lemma chinese-map-surj (n m : Nat) (p : IsCoprime (suc n) (suc m)) : IsSurj (chinese-map {n} {m})
  => \case \elim __ \with {
  | (r1, r2) => \case IntDomain.chinese2 r1 r2 (suc n) (suc m) (\lam z l l1 =>
    \let A0 => natSemiring-unit (p (iabs z) (ldiv_iabs l) (ldiv_iabs l1)) \in \new Inv {
      | inv => signum z
      | inv-left => rewrite (*-comm, inv iabs.signum_*, A0) idp
      | inv-right => rewrite (inv iabs.signum_*, A0) idp
    }) \with {
    | inP (r, (p1, A1), (p2, A2)) => inP (intMap r, ext (
      \let
        | B1 => rewrite (fin_mod_id {n} r1) in unfold Fin.fromNat in ldiv-finEq {r mod (suc n * suc m)} {r1} {n} (inP (\new LDiv {
          | inv => p1 - suc m IntRing.* (r div pos (suc n * suc m))
          | inv-right => rewrite (Ring.ldistr_-, A1, inv (pmap (\lam x => x - r1) (divModProp r (suc n * suc m) (\lam p => \case p)))) equation
        }))
        | B2 => rewrite fin_mod_id in pmap (Fin.fromNat {n}) (mod-inv {suc n} {suc m} (\lam p => \case p) (r mod (suc n * suc m)))
      \in rewrite intCoef-char (B2 *> rewrite fin_mod_id B1),
      \let
        | B1 => rewrite (fin_mod_id {m} r2) in unfold Fin.fromNat in ldiv-finEq {r mod (suc n * suc m)} {r2} {m} (inP (\new LDiv {
          | inv => p2 - suc n IntRing.* (r div pos (suc n * suc m))
          | inv-right => rewrite (Ring.ldistr_-, A2, inv (pmap (\lam x => x - r2) (divModProp r (suc n * suc m) (\lam p => \case p)))) equation
        }))
        | B2 => rewrite (fin_mod_id, *-comm {_} {suc m} {suc n}) in
        pmap (Fin.fromNat {m}) (mod-inv {suc m} {suc n} (\lam p => \case p) (r mod (suc n * suc m)))
      \in rewrite intCoef-char (B2 *> rewrite fin_mod_id B1)))
  }} \where {
  \lemma mod-inv {n m : Nat} (p : n /= ) (x : Nat) : x Nat.mod (n Semigroup.* m) Nat.mod n = x Nat.mod n =>
    \let A0 => rewriteI NatSemiring.ldistr $ rewrite NatSemiring.*-assoc $
        rewriteI (AddMonoid.+-assoc {_} {n Nat.* m Nat.* x Nat.div (n Nat.* m)}) $
            rewriteI (rewrite IntEuclidean.natMod=mod in Nat.divModProp (x IntEuclidean.mod (n Nat.* m)) n) in
            (Nat.divModProp x (n Semigroup.* m) *> inv (Nat.divModProp x n))
    \in mod-unique {n} {m Nat.* x Nat.div (n Nat.* m) Nat.+ x Nat.mod (n Nat.* m) Nat.div n}
        {x Nat.mod (n Nat.* m) Nat.mod n} {x Nat.div n} {x Nat.mod n}
        (mod<right {x Nat.mod (n Nat.* m)} {n} p) (mod<right {x} {n} p) A0
}