{- | Adequate rings were defined in
 -   Olaf Helmer, The elementary divisor theorem for certain rings without chain condition, 1943
 -
 -   The proof that adequate rings satisfy the Kaplansky condition is taken from
 -   Irving Kaplansky, Elementary divisors and modules, 1949
-}

\import Algebra.Domain
\import Algebra.Domain.Bezout
\import Algebra.Domain.GCD
\import Algebra.Group
\import Algebra.Linear.Matrix.Smith
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.MonoidHom
\import Algebra.Monoid.SubMonoid
\import Algebra.Pointed
\import Algebra.Ring.Ideal
\import Algebra.Ring.Noetherian
\import Algebra.Semiring
\import Function.Iterate
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\open DivQuotient \hiding (~)
\open Monoid
\open equation(cRing)

\class PID \extends SmithDomain, WeaklyNoetherianCRing {
  | divChain : CMonoid.DivChain {DivQuotientMonoid nonZeroCMonoid}
  | isWeaklyNoetherian I Ifg => Ideal.fromMonoidChainCondition (IntegralDomain.Dec.fromNonZeroDivChain divChain) I \lam n => bezout_finitelyGenerated_principal. isBezout (Ifg n)
  | isKaplansky => adequate_kaplansky \lam a/=0 => adequate'_adequate (domain_adequate' divChain a/=0)

  \lemma is1Dim : Dim<= 
    => bezout_1Dim<->adequate'. \lam a/=0 => domain_adequate' divChain a/=0
} \where {
  \func IsAdequate {M : CMonoid} (a : M) => \Pi (b : M) -> ∃ (c : M) (LDiv c a) (IsCoprime c b) ∀ d (LDiv d a -> IsCoprime d b -> TruncP (LDiv d c))

  \func IsAdequate' {M : CMonoid} (a : M) => \Pi (b : M) -> ∃ (a1 a2 : M) (n : Nat) (a = a1 * a2) (LDiv a1 (pow b n)) (IsCoprime a2 b)

  \lemma adequate'_adequate {M : GCDMonoid} {a : M} (adeq : IsAdequate' a) : IsAdequate a
    => \lam b => \case adeq b \with {
      | inP s => inP (s., LDiv.make s. (*-comm *> inv s.), s., \lam d d|a d_b => M.coprime_*_div (rewrite s. in d|a) $ IsCoprime.factor-right s. $ M.IsCoprime_pow-right d_b)
    }

  \open UnitlessGCDMonoid \using (gcd)

  \lemma unitless_adequate' {M : UnitlessGCDMonoid} (dc : M.DivChain) (a : M) : IsAdequate' a
    => \lam b =>
        \let | g x => GCD.res|val1 {gcdC x b}
             | f x => LDiv.inv {g x}
             | (inP (n, d : LDiv)) => dc (iterr f __ a) \lam i => inP $ LDiv.swap $ g (iterr f i a)
             | s => iterr-index-ind {_} {\lam n x => \Sigma (d : M) (a = d * x) (LDiv d (pow b n))} (, inv ide-left, LDiv.id-div) (\lam {m} {x} r => (r. * gcd x b, r. *> pmap (r. *) (inv $ LDiv.inv-right {g x}) *> inv *-assoc, LDiv.product r. (GCD.res|val2 {gcdC x b}))) n
             | c => iterr f n a
        \in inP (s., c, n, s., s., IsCoprime.<=gcd $ transport (GCD c b) (uniqueUnit $ Inv.lmake d.inv $ cancel_*-left c $ inv *-assoc *> pmap (* g c) d.inv-right *> *-comm *> LDiv.inv-right {g c} *> inv ide-right) (gcdC c b))

  \lemma monoid_adequate' {M : CancelGCDMonoid} (dc : CMonoid.DivChain {DivQuotientMonoid M}) (a : M) : IsAdequate' a
    => \lam b => \case unitless_adequate' dc (inD a) (inD b) \with {
      | inP (in~ a1, in~ a2, n, a=a1a2, a1|b^n, a2_b) =>
        \have (c : Inv, p) => equivalent-associates a (a1 * a2) (make~ a=a1a2)
        \in inP (c * a1, a2, n, p *> inv *-assoc, LDiv.trans (LDiv.make c.inv $ *-comm *> inv *-assoc *> pmap (* _) c.inv-left *> ide-left) (div-from~ $ transportInv (LDiv _) (inDHom M).func-pow a1|b^n), IsCoprime.<=gcd $ gcd-from~ $ IsCoprime.=>gcd a2_b)
    }

  \lemma domain_adequate' {M : GCDDomain.Dec} (dc : CMonoid.DivChain {DivQuotientMonoid M.nonZeroGCDMonoid}) {a : M} (a/=0 : a /= ) : IsAdequate' a
    => \lam b => \case decideEq b  \with {
      | yes b=0 => inP (a, , , inv ide-right, rewrite b=0 $ simplify M.zero-div, IsCoprime.IsCoprime_ide-left)
      | no b/=0 => TruncP.map (monoid_adequate' dc (a, M.nonZeroApart a/=0) (b, M.nonZeroApart b/=0)) \lam (a1,a2,n,a=a1a2,a1|b^n,a2_b) =>
          (a1., a2., n, pmap __. a=a1a2, transport (LDiv _) IMonoid.embed.func-pow (M.nonZero_ldiv a1|b^n),
           \lam z z|a2 z|b => M.nonZero_inv $ a2_b (z, M.nonZeroApart $ M.ldiv/=0 b/=0 z|b) (M.ldiv_nonZero z|a2) (M.ldiv_nonZero z|b))
    }

  \lemma oneDim_adequate' {R : GCDDomain.Dec} (d : R.Dim<= ) {a : R} (a/=0 : a /= ) : IsAdequate' a
    => \lam b =>
        \have | (inP (v,n,d)) => R.oneDimensional-char. d a b a/=0
              | (inP (a1,a2,a=a1a2,a1|b^n,(c,p))) => R.split_* d
        \in inP (a1, a2, n, a=a1a2, a1|b^n, BezoutRing.bezout_coprime {_} {c} {v} $ cRing {p})

  \lemma bezout_1Dim<->adequate' {R : BezoutDomain.Dec} : R.Dim<=  <-> (\Pi {a : R} -> a /=  -> IsAdequate' a)
    => (oneDim_adequate', \lam f => R.oneDimensional-char. \lam a u a/=0 =>
        \have | (inP (a1,a2,n,a=a1a2,a1|u^n,a2_u)) => f a/=0 u
              | (inP (s,v,p)) => R.gcd_bezout (IsCoprime.=>gcd a2_u)
        \in inP (v, n, rewrite a=a1a2 $ LDiv.product a1|u^n $ LDiv.make s $ cRing {p}))

  \lemma adequate_kaplansky {R : BezoutDomain.Dec} (adeq : \Pi {a : R} -> a /=  -> IsAdequate a) : SmithRing.IsKaplansky R
    => \lam a b c a_b_c => \case R.coprime_bezoutArray a_b_c, decideEq a  \with {
      | inP (s,p), yes a=0 => inP (s , s , BezoutRing.bezout_coprime {_} {} {} $ cRing { p, a=0})
      | _, no a/=0 =>
        \have | (inP r) => adeq a/=0 c
              | (inP (c',c*,cp)) => R.gcd_bezout (IsCoprime.=>gcd r.)
        \in inP (, c* * ( - b), simplify \lam d d1 (y,p) =>
            \have | d_c : IsCoprime d c => \lam z (x1,p1) (x2,p2) => a_b_c z
                            (LDiv.trans (LDiv.make x1 p1) d1, LDiv.make (x1 * y - x2 * c* * ( - b)) (cRing {p1,p2,p}), LDiv.make x2 p2)
                  | d_R : IsCoprime d r. => BezoutRing.bezout_coprime {_} {y} {( - b) * c'} (cRing {p,cp})
            \in d_R d LDiv.id-div $ Domain.Dec.LDiv_TruncP $ r. d d1 d_c)
    }
}