\import Algebra.Domain.Bezout
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.Category
\import Algebra.Monoid.GCD
\import Algebra.Ring.Ideal
\import Algebra.Ring.Local
\import Algebra.Ring.Nakayama
\import Algebra.Ring.Poly
\import Algebra.Ring.Reduced
\import Algebra.Semiring
\import Arith.Nat
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.Lattice
\import Order.PartialOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Fin

\class Ring \extends Semiring, AbGroup {
  | zro_*-left {x} => AddGroup.cancel-left (zro * x) (
    zro * x + zro * x ==< inv rdistr >==
    (zro + zro) * x   ==< pmap (`* x) zro-left >==
    zro * x           ==< inv zro-right >==
    zro * x + zro     `qed
  )
  | zro_*-right {x} => AddGroup.cancel-left (x * zro) (
    x * zro + x * zro ==< inv ldistr >==
    x * (zro + zro)   ==< pmap (x *) zro-left >==
    x * zro           ==< inv zro-right >==
    x * zro + zro     `qed
  )

  \func intCoef (x : Int) : E
    | pos n => natCoef n
    | neg (suc _ \as n) => negative (natCoef n)

  \lemma intCoef_neg (n : Nat) : intCoef (neg n) = negative (natCoef n)
    |  => natCoefZero *> inv (pmap negative natCoefZero *> AddGroup.negative_zro)
    | suc n => idp

  \lemma negative_*-left {x y : E} : negative x * y = negative (x * y)
    => negative-unique (x * y) (inv rdistr *> pmap (`* y) negative-left *> zro_*-left) negative-right

  \lemma negative_*-right {x y : E} : x * negative y = negative (x * y)
    => op.negative_*-left

  \lemma negative_ide-left {x : E} : negative ide * x = negative x
    => negative_*-left *> pmap negative ide-left

  \lemma negative_ide-right {x : E} : x * negative ide = negative x
    => negative_*-right *> pmap negative ide-right

  \lemma negative_* {x y : E}  : negative x * negative y = x * y =>
    negative x * negative y     ==< negative_*-left >==
    negative (x * negative y)   ==< pmap negative negative_*-right >==
    negative (negative (x * y)) ==< negative-isInv >==
    x * y                       `qed

  \lemma ldistr_- {x y z : E} : x * (y - z) = x * y - x * z
    => ldistr *> pmap (_ +) negative_*-right

  \lemma rdistr_- {x y z : E} : (x - y) * z = x * z - y * z
    => rdistr *> pmap (_ +) negative_*-left

  \lemma negative_inv (j : Monoid.Inv {\this}) : Monoid.Inv (negative j) (negative j.inv)
    => \new Monoid.Inv {
      | inv-left => negative_* *> j.inv-left
      | inv-right => negative_* *> j.inv-right
    }

  \lemma geometric-partial-sum {n : Nat} {x : E} (xi : Monoid.Inv ( - x)) : xi.inv - BigSum (\new Array E n (\lam j => Monoid.pow x j)) = Monoid.pow x n * xi.inv
    => inv (rdistr_- *> pmap2 (-) ide-left (*-assoc *> pmap (_ *) xi.inv-right *> ide-right)) *> pmap (`* _) (pmap ( -) ldistr_- *> simplify \case \elim n \with {
      |  => simplify
      | suc n => rewrite {} (BigSum_suc,rdistr) $ simplify $ pmap (`+ _) +-comm *> +-assoc *>
          pmap2 (+) (later rewrite (toFin'=id id<suc) idp) (pmap (`+ _) BigSum-rdistr *> negative-right) *> zro-right
    })

  \func IsNilpotent (x : E) => ∃ (n : Nat) (pow x n = )

  \lemma pow_-1_+2 {n : Nat} : pow -1 (n Nat.+ ) = pow -1 n
    => pow_+ {_} { -1} {n} {} *> pmap (_ *) (*-assoc *> ide-left *> negative_* *> ide-left) *> ide-right

  \lemma pow_-1_even {n : Nat} : pow -1 (n Nat.* ) =  \elim n
    |  => idp
    | suc n => negative_ide-right *> pmap negative negative_ide-right *> negative-isInv *> pow_-1_even

  \lemma pow_-1_mod2 {n : Nat} : pow -1 n = pow -1 (n Nat.mod )
    => pmap (pow -1) (inv (Nat.divModProp n )) *> pow_+ *> pmap (`* _) (pow_* *> pmap (pow __ _) (*-assoc *> ide-left *> negative_* *> ide-left) *> pow_ide) *> ide-left

  \lemma idempotent_LDiv {a b : E} (q : b * b = b) (d : Monoid.LDiv b a) : a = b * a
    => inv d.inv-right *> pmap (`* _) (inv q) *> *-assoc *> pmap (b *) d.inv-right

  \type IsConnected => \Pi (a : E) -> a * a = a -> (a = ) || (a = )

  \func IsVonNeumannRegular => \Pi (a : E) -> ∃ (b : E) (a = a * b * a)

  \func op : Ring \cowith
    | AbGroup => \this
    | Semiring => Semiring.op
} \where {
  -- | A ring with a tight apartness relation.
  \class With# \extends Ring, AddGroup.With#
    | #0-*-left {x y : E} : (x * y) `#0 -> x `#0
    | #0-*-right {x y : E} : (x * y) `#0 -> y `#0
    | #0-negative {x} x#0 => #0-*-left (transport #0 (inv (negative_* *> ide-right)) x#0)

  -- | A ring with decidable equality.
  \class Dec \extends AddGroup.Dec, With#
    | #0-*-left {x} {y} x*y#0 => \case decideEq x zro \with {
      | yes x=0 => absurd (#0-zro (transport #0 (pmap (`* y) x=0 *> zro_*-left) x*y#0))
      | no x/=0 => nonZeroApart x/=0
    }
    | #0-*-right {x} {y} x*y#0 => \case decideEq y zro \with {
      | yes y=0 => absurd (#0-zro (transport #0 (pmap (x *) y=0 *> zro_*-right) x*y#0))
      | no y/=0 => nonZeroApart y/=0
    }
}

\class NonZeroRing \extends Ring, NonZeroSemiring

\class CRing \extends Ring, CSemiring {
  \func IsBezout => \Pi (a b : E) -> ∃ (s t : E) (LDiv (s * a + t * b) a) (LDiv (s * a + t * b) b)

  \func IsStrictBezout => \Pi (a b : E) -> ∃ (s t u v : E) (a * u = b * v) (s * u + t * v = )

  \lemma bezout_finitelyGenerated_principal : IsBezout <-> (\Pi {I : Ideal \this} -> I.IsFinitelyGenerated -> I.IsPrincipal)
    => (\lam bez {I : Ideal} Ifg =>
          \have | (inP s) => Ifg
                | (inP t) => BezoutRing.bezoutArray_LDiv {\new BezoutRing { | CRing => \this | isBezout => bez }} s.
          \in inP (BigSum (\lam j => t. j * s. j), (I.bigSum _ \lam j => ideal-left $ later (s.. j), \lam {b} Ib =>
               TruncP.map (s.. Ib) \lam u => transportInv (LDiv _ __) u. (LDiv_BigSum \lam j => later $ LDiv.factor-right $ t. j))),
        \lam p a b =>
          \have | (inP (d,s)) => p {Ideal.closure (a :: b :: nil)} Ideal.closure-finGenerated
                | (inP t) => Ideal.closureN-lem. s.
                | (inP d|a) => s. (Ideal.closure-superset {_} {_} {a :: b :: nil} (later ))
                | (inP d|b) => s. (Ideal.closure-superset {_} {_} {a :: b :: nil} (later ))
                | p => unfold BigSum at t $ rewrite zro-right in t.
          \in inP (t. , t. , rewriteI p d|a, rewriteI p d|b)
    )

  \func bezoutGCD {a b s t : E} (p : LDiv (s * a + t * b) a) (q : LDiv (s * a + t * b) b) : GCD a b (s * a + t * b) \cowith
    | gcd|val1 => p
    | gcd|val2 => q
    | gcd-univ g (g|x : LDiv g a) (g|y : LDiv g b) => \new LDiv {
      | inv => s * g|x.inv + t * g|y.inv
      | inv-right =>
        g * (s * g|x.inv + t * g|y.inv)       ==< ldistr >==
        g * (s * g|x.inv) + g * (t * g|y.inv) ==< inv (pmap2 (+) *-assoc *-assoc) >==
        (g * s) * g|x.inv + (g * t) * g|y.inv ==< pmap2 (__ * g|x.inv + __ * g|y.inv) *-comm *-comm >==
        (s * g) * g|x.inv + (t * g) * g|y.inv ==< pmap2 (+) *-assoc *-assoc >==
        s * (g * g|x.inv) + t * (g * g|y.inv) ==< pmap2 (s * __ + t * __) g|x.inv-right g|y.inv-right >==
        s * a + t * b                         `qed
    }

  \type Dim<= (k : Nat) => \Pi (x : Array E (suc k)) -> ∃ (a : Array E (suc k)) (m : Array Nat (suc k)) (fold x a m = )
    \where
      \func fold {k : Nat} (xs as : Array E k) (ms : Array Nat k) : E \elim k, xs, as, ms
        | , nil, nil, nil => 
        | suc k, x :: xs, a :: as, m :: ms => pow x m * (fold xs as ms - x * a)

  \type IsZeroDimensional => \Pi (a : E) -> ∃ (b : E) (n : Nat) (pow a n = pow a (suc n) * b)

  \lemma finite-zeroDimensional (c : FinSet E) : IsZeroDimensional
    => \lam a => TruncP.map (c.pigeonhole< (pow a)) \lam s => (pow a (s. -' suc s.), s., s. *> pmap (pow a) (inv $ <=_exists $ suc_<_<= s.) *> pow_+ {_} {_} {suc s.})

  \lemma zeroDimensional-char : TFAE (
    IsZeroDimensional,
    Dim<= ,
    \Pi (a : E) -> ∃ (b : E) (k : Nat) (k /= ) (b * b = b) (LDiv (pow a k) b) (LDiv b (pow a k))
  ) => TFAE.cycle (
        \lam zd x => \case zd (x ) \with {
          | inP (b,n,p) => inP (b :: nil, n :: nil, equation)
        },
        \lam zd x => \case zd (x :: nil) \with {
          | inP (a,m,p) => cases (m  arg addPath) \with {
            | , q => inP (, , (\case __), ide-left, LDiv.make (a ) (equation {usingOnly (rewrite q in p)}), LDiv.ide-div)
            | suc n, q => \have t => rewrite pow_*-comm in aux {_} {pow x (m )} {x * a } (m ) equation
                          \in inP (pow x (m ) * pow (a ) (m ), m , rewrite q (\case __), equation, LDiv.factor-left LDiv.id-div, LDiv.make (pow x (m )) equation)
          }
        }, \lam c a => TruncP.map (c a) \lam s =>
            (LDiv.inv {s.} * pow a (pred s.), s., inv (LDiv.idempt s. s.) *> *-comm *>
             pmap (_ *) (inv (LDiv.inv-right {s.}) *> *-comm *> pmap (_ * pow a __) (inv $ suc_pred s.) *> inv *-assoc *> *-comm) *> inv *-assoc))
    \where
      \lemma aux {x c : E} (n : Nat) (p : x = x * c) : x = x * pow c n \elim n
        |  => inv ide-right
        | suc n => aux n p *> pmap (`* _) p *> *-assoc *> pmap (x *) *-comm

  \lemma zeroDimensional_local-char : TFAE (
    \Sigma IsZeroDimensional (\Pi (a : E) -> Inv a || Inv (a + )),
    \Sigma IsZeroDimensional IsConnected,
    \Pi (a : E) -> Inv a || (\Sigma (n : Nat) (pow a n = ))
  ) => TFAE.cycle (
        \lam s => (s., LocalRing.local=>connected s.),
        \lam s a => \case zeroDimensional-char   s. a \with {
          | inP r => \case s. r. r. \with {
            | byLeft r1=0 => byRight (r., inv (LDiv.inv-right {r.}) *> pmap (`* _) r1=0 *> zro_*-left)
            | byRight r1=1 => byLeft $ Inv.cfactor-right $ rewrite (inv $ suc_pred r.) in Inv.lmake (LDiv.inv {r.}) (*-comm *> LDiv.inv-right {r.} *> r1=1)
          }
        }, \lam s => (\lam a => \case s a \with {
              | byLeft (r : Inv) => inP (r.inv, , inv $ simplify r.inv-right)
              | byRight r => inP (, r., rewrite r. simplify)
            }, \lam a => \case s (a + ) \with {
              | byLeft r => byRight r
              | byRight r => byLeft
                \let | p => pow {PolyRing \this} (padd  ) r.
                     | t : polyEval p a =  => MonoidHom.func-pow {polyEvalRingHom a} *> pmap (pow __ r.) equation *> r.
                \in Inv.ldiv $ transport (LDiv a) (lastCoef_pow *> pow_ide) (poly-root-div t)
        }))

  \lemma vonNeumann_idempotent (vn : IsVonNeumannRegular) (a : E) : ∃ (u : E) (u * u = u) (LDiv a u) (a = u * a)
    => TruncP.map (vn a) \lam (b,p) => (a * b, equation, LDiv.factor-left LDiv.id-div, p)

  \lemma vonNeumann-char : TFAE (
    {- 0 -} IsVonNeumannRegular,
    {- 1 -} \Sigma IsZeroDimensional (ReducedRing { | Ring => \this }),
    {- 2 -} \Pi (I : Ideal \this) -> I.IsFinitelyGenerated -> ∃ (u : E) (u * u = u) (I.IsGeneratedBy1 u),
    {- 3 -} \Pi (I : Ideal \this) -> I IdealMonoid.* I = I,
    {- 4 -} \Pi (I J : Ideal \this) -> I ∧ J = I IdealMonoid.* J
  ) => TFAE.proof (
    ((,), \lam c => (\lam a => TruncP.map (c a) \lam s => (s., , equation {usingOnly s.}),
                       \new ReducedRing { | isReduced {a} p => \case c a \with {
                         | inP (b,q) => equation
                       } })),
    ((,), \lam (zd, red : ReducedRing) => \lam a => \case zd a \with {
        | inP (b, , p) => inP (b, equation)
        | inP (b, suc n, p) => inP (b, inv ide-right *> fromZero (inv ldistr_- *>
            red.noNilpotent {_} {suc n} (pow_*-comm {_} {_} {_} {suc n} *> equation)) *> inv *-assoc)
      }
    ),
    ((,), \lam c a => \case c (closure1 a) (principal->finitelyGenerated closure1-principal) \with {
                          | inP (u,uu=u,(a|u',f)) =>
                            \have | (inP (a|u : LDiv a u)) => closure1_LDiv. a|u'
                                  | (inP u|a) => f {a} (closure-superset {_} {_} {\lam _ => a} ())
                            \in inP (a|u.inv, equation {using (a|u.inv-right, idempotent_LDiv uu=u u|a)})
                        }),
    ((,), \lam v I J => <=-antisymmetric (\lam {a} c =>
      \case v a \with {
        | inP (b,p) => rewrite p $ closure-superset {_} {_} {IdealMonoid.func I J} $ later (a * b, a, ideal-right (IdealLattice.meet-left c), IdealLattice.meet-right c)
      }) IdealMonoid.product_meet),
    ((,), \lam f I => inv (f I I) *> IdealLattice.meet-idemp),
    ((,), \lam f I Ifg => nakayama-ideal Ifg (Preorder.=_<= (inv (f I))))
  )
  \where \open Ideal

  \lemma vonNeumann_Bezout (vn : IsVonNeumannRegular) : IsBezout
    => bezout_finitelyGenerated_principal. \lam {I} Ifg => TruncP.map (vonNeumann-char   vn I Ifg) \lam s => (s.,s.)

  \func op : CRing \cowith
    | Ring => Ring.op
    | *-comm => *-comm
} \where {
    \open Monoid(LDiv,Inv)

    -- | A commutative ring with a tight apartness relation.
    \class With# \extends CRing, Ring.With#
      | #0-*-right x*y#0 => #0-*-left (transport #0 *-comm x*y#0)

    -- | A commutative ring with decidable equality.
    \class Dec \extends Ring.Dec, With# {
      \lemma divQuotient_dec0 (a : DivQuotient \this) : Set.Dec (a = in~ )
        | in~ a => \case decideEq a  \with {
          | yes e => yes $ ~-pequiv $ rewrite e (inP LDiv.id-div, inP LDiv.id-div)
          | no q => no \lam p => q \case (DivQuotient.make~ p). \with {
            | inP d => inv (LDiv.inv-right {d}) *> zro_*-left
          }
        }
    }
}

\class NonZeroCRing \extends CRing, NonZeroRing