\import Algebra.Domain.Bezout
\import Algebra.Domain.Euclidean
\import Algebra.Group
\import Algebra.Group.GroupHom
\import Algebra.Group.SubGroup
\import Algebra.Group.Symmetric
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Factor
\import Algebra.Ring.Ideal
\import Algebra.Ring.RingCat
\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 Relation.Equivalence
\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 => IMonoid (InvSubMonoid M)
  | 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 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) Nat.mod 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))

  }

\lemma Z/nZ=FinRing {n : Nat}
  : IsEquiv {FactorRing (Ideal.closure1 (pos (suc n)))} {FinRing {n}} (factor-lift FinRing.intHom factor-lem)
  => IsEquiv.fromInjSurj (\lam {x} {y} => \case \elim x, \elim y \with {
    | in~ x, in~ y => \lam p => FactorRing.fequiv $ Ideal.closure1_LDiv. $ inP $ later $ equal-mod_LDiv {_} {_} {suc n} (\case __) (inv FinRing.mod-mod *> p *> FinRing.mod-mod)
  }) \lam y => inP (in~ y, fin_nat-inj $ FinRing.mod-mod *> natMod=mod y _ *> fin_mod_id y)
  \where {
    \func factor-lem {x : Int} (c : Ideal.closure1 (pos (suc n)) x) : FinRing.intHom {n} x = 
      => \case Ideal.closure1-lem. c \with {
        | inP (d,p) => inv (FinRing.intCoef-char n x) *> pmap intMap p *> intMap.func-* *> pmap (* _) (fin_nat-inj $ id_mod {suc n}) *> (FinRing {n}).zro_*-left
      }
  }

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

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

\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 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 (__ Nat.mod suc 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 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 (__ Nat.mod suc 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
}