\import Algebra.Domain.Bezout
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Ring.Ideal
\import Algebra.Semiring
\import Arith.Nat
\import Equiv
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\import Set.Fin

{- | Associative ring -}
\class PseudoRing \extends PseudoSemiring, 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
  )

  \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_* {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 *_sum_diff {x y : E} (p : x * y = y * x) : (x + y) * (x - y) = x * x - y * y
    => rdistr *> pmap2 (+) ldistr_- ldistr_- *> +-assoc *> pmap (_ +) (inv +-assoc *> pmap (`+ _) (pmap (_ +) (inv p) *> negative-left) *> zro-left)

  \lemma *_diff_sum {x y : E} (p : x * y = y * x) : (x - y) * (x + y) = x * x - y * y
    => ldistr *> pmap2 (+) rdistr_- rdistr_- *> +-assoc *> pmap (_ +) (inv +-assoc *> pmap (`+ _) (pmap (_ +) p *> negative-left) *> zro-left)

  \protected \func op : PseudoRing \cowith
    | AbGroup => \this
    | PseudoSemiring => PseudoSemiring.op
}

\class Ring \extends PseudoRing, Semiring {
  \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_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_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} : ( - x) * BigSum (\new Array E n (\lam j => pow x j)) =  - pow x n \elim n
    |  => zro_*-right *> inv negative-right
    | suc n => pmap (_ *) (AddMonoid.BigSum_suc-nat {_} {n} {pow x}) *> ldistr *> pmap2 (+) geometric-partial-sum rdistr *> +-assoc *> pmap (_ +) (inv +-assoc *> pmap (_ +) negative_*-left *> pmap (`+ _) (pmap (_ +) ide-left *> negative-left) *> zro-left *> pmap negative pow-left)

  \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)

  \protected \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)

    \lemma #0-FinSum {J : FinSet} {x : J -> E} (p : FinSum x `#0) : ∃ (j : J) (x j `#0)
      => \case FinSum_char x \with {
        | inP (e,q) => \case #0-BigSum (transport #0 q p) \with {
          | inP (j,xej#0) => inP (e j, xej#0)
        }
      }

    \lemma #0-FinSum-conv {J : FinSet} {x : J -> E} {i : J} (xi#0 : x i `#0) : FinSum x `#0 || (\Sigma (j : J) (j /= i) (x j `#0))
      => \case FinSum_char x \with {
        | inP (e, p) => \case #0-BigSum-conv {_} {\new Array E J.finCard \lam j => x (e j)} $ rewrite e.f_ret xi#0 \with {
          | byLeft r => byLeft $ transportInv #0 p r
          | byRight (j,j/=i,xej#0) => byRight (e j, \lam ej=i => j/=i $ inv (e.ret_f j) *> pmap e.ret ej=i, xej#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 PseudoCRing \extends PseudoRing, PseudoCSemiring

\class CRing \extends Ring, PseudoCRing, 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
    | res|val1 => p
    | res|val2 => q
    | res-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.})
} \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