\import Algebra.Domain
\import Algebra.Domain.IntegrallyClosed
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Monoid.GCD
\import Algebra.Monoid.Sub
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Localization \hiding (FieldOfQuotients)
\import Algebra.Ring.Poly
\import Algebra.Semiring
\import Arith.Nat
\import Data.Or
\import Function.Meta ($)
\import Logic
\import Logic.Meta
\import Meta
\import Order.LinearOrder
\import Paths
\import Paths.Meta
\import Relation.Equivalence
\import Set
\open Monoid

\class GCDDomain \extends IntegralDomain {
  | isGCDDomain (x y : E) : x `#0 -> y `#0 -> TruncP (GCD x y)

  \func nonZeroGCDMonoid : CancelGCDMonoid \cowith
    | CancelCMonoid => nonZeroCMonoid
    | isGCD x y =>
      \have | (inP (g : GCD x. y.)) => isGCDDomain x. y. x. y.
            | g*x#0 => transport #0 (inv g.res|val1.inv-right) x.
            | g#0 => #0-*-left g*x#0
      \in inP (\new GCD {
                 | res => (g, g#0)
                 | res|val1 => \new LDiv {
                   | inv => (g.res|val1.inv, #0-*-right g*x#0)
                   | inv-right => ext g.res|val1.inv-right
                 }
                 | res|val2 => \new LDiv {
                   | inv => (g.res|val2.inv, #0-*-right (transport #0 (inv g.res|val2.inv-right) y.))
                   | inv-right => ext g.res|val2.inv-right
                 }
                 | res-univ h (h|x : LDiv h x) (h|y : LDiv h y) =>
                   \have h|g : LDiv h. g => g.res-univ h. (\new LDiv h. x. h|x.inv. (pmap __. h|x.inv-right))
                                                            (\new LDiv h. y. h|y.inv. (pmap __. h|y.inv-right))
                   \in \new LDiv {
                     | inv => (h|g.inv, #0-*-right (transport #0 (inv h|g.inv-right) g#0))
                     | inv-right => ext h|g.inv-right
                   }
               })

  \protected \func gcd_0 (x : E) : GCD x  x \cowith
    | res|val1 => \new LDiv {
      | inv => 
      | inv-right => ide-right
    }
    | res|val2 => \new LDiv {
      | inv => 
      | inv-right => zro_*-right
    }
    | res-univ g g|a _ => g|a

  \func gcd_sum (d : E) (g : GCD {\this}) : GCD (g.val1 + g.val2 * d) g.val2 g \cowith
    | res|val1 => \new LDiv {
      | inv => g.res|val1.inv + g.res|val2.inv * d
      | inv-right => ldistr *> pmap2 (+) g.res|val1.inv-right (inv *-assoc *> pmap (`* d) g.res|val2.inv-right)
    }
    | res|val2 => g.res|val2
    | res-univ g' (g'|a+bd : LDiv) (g'|b : LDiv) => g.res-univ g' (\new LDiv {
      | inv => g'|a+bd.inv - g'|b.inv * d
      | inv-right => ldistr *> pmap2 (+) g'|a+bd.inv-right (Ring.negative_*-right *> pmap negative (inv *-assoc *> pmap (`* d) g'|b.inv-right)) *> simplify
    }) g'|b
} \where {
  \class Dec \extends GCDDomain, GCDMonoid, IntegralDomain.Dec, IntegrallyClosedDomain {
    | isGCD => gcd nonZeroApart
    | gcd-ldistr c {x} {y} g => \case decideEq c  \with {
      | yes c=0 => rewrite c=0 $ simplify $ inP \new GCD {
        | res|val1 => LDiv.id-div
        | res|val2 => LDiv.id-div
        | res-univ g g|0 _ => g|0
      }
      | no c/=0 => TruncP.map (gcd nonZeroApart (c * x) (c * y)) $ GCDMonoid.gcd-ldistr_cancel (\lam {a} {b} => nonZero-cancel-left c/=0) g
    }
    | isIntegrallyClosedDomain x xi => \case Dec.coprime-repr-aux x, \elim xi \with {
      | inP c, inP d => \case loc_poly (\lam s p => nonZero-cancel-right (apartNonZero s) p) d. d. (rewrite c. in d.) \with {
        | inP e => rewrite c. \case decide#0 c. \with {
          | inl q => inP (, LocRing.equals1 $ simplify $ inv q)
          | inr c1#0 => inP (_, inv $ div_loc $ nonZero_ldiv $ CancelGCDMonoid.gcd_pow_div {nonZeroGCDMonoid} {c.,c.} {c.,c1#0} {e.}
                          (transport (LDiv _) (ext $ inv subMonoid.embedMonoid.func-pow) $ ldiv_nonZero {_} {_} {_, pow_#0 c1#0} e.) $ IsCoprime.<=gcd $ later \new GCD {
                            | res|val1 => LDiv.ide-div
                            | res|val2 => LDiv.ide-div
                            | res-univ g g|c2 g|c1 => ldiv_nonZero $ GCD.res-univ {c.} g. (nonZero_ldiv g|c1) (nonZero_ldiv g|c2)
                          })
        }
      }
    }

    \lemma coprime-repr (x : LocRing subMonoid) => coprime-repr-aux x

    \lemma oneDimensional_Bezout (d : Dim<= ) : IsStrictBezout
      => \lam a b => \case isGCD a b \with {
        | inP (g : GCD) => \case decideEq a  \with {
          | yes a=0 => inP (, , , , simplify a=0, simplify)
          | no a/=0 =>
            \let | u => g.res|val2.inv
                 | v => g.res|val1.inv
                 | g' : GCD v u  => g.reduce $ LDiv_IsRegular g.res|val1 (IsRegular_/=0. a/=0)
                 | (inP (c,n,p)) => oneDimensional-char. d v u $ ldiv/=0 a/=0 (LDiv.swap g.res|val1)
                 | (inP (d,q)) => coprime_*_div p (IsCoprime_pow-right $ IsCoprime.<=gcd g')
            \in inP (c, d, u, v, rewriteI (g.res|val1.inv-right,g.res|val2.inv-right) equation.cMonoid, equation.cRing {q})
        }
      }

    \lemma split_* {a b c : E} (a|bc : LDiv a (b * c)) : ∃ (a1 a2 : E) (a = a1 * a2) (LDiv a1 b) (LDiv a2 c)
      => \case decideEq a  \with {
        | yes a=0 => inP (b, c, later (rewrite a=0 $ inv zro_*-left) *> a|bc.inv-right, LDiv.id-div, LDiv.id-div)
        | no a/=0 => split-regular (\lam p => nonZero-cancel-left a/=0 p) a|bc
      }

    \lemma div_unit : (\Pi (a b : E) -> Set.Dec (TruncP (LDiv a b))) <-> (\Pi (a : E) -> Set.Dec (Monoid.Inv a))
      => (\lam f a => \case f a  \with {
            | yes (inP r) => yes (Monoid.Inv.ldiv r)
            | no r => no \lam p => r (inP p)
          }, \lam f a b => \case decide#0 a, decide#0 b \with {
            | _, inl b=0 => yes $ inP $ LDiv.make  $ zro_*-right *> inv b=0
            | inl a=0, inr b#0 => no \lam (inP a|b) => #0-zro $ transport #0 (ldiv=0 a|b a=0) b#0
            | inr a#0, inr b#0 => \case nonZeroGCDMonoid.div_unit. (\lam x => \case f x. \with {
              | yes e => yes (inv_nonZero e)
              | no q => no \lam e => q (nonZero_inv e)
            }) (a,a#0) (b,b#0) \with {
              | yes e => yes $ inP (nonZero_ldiv e)
              | no q => no \lam (inP a|b) => q (ldiv_nonZero a|b)
            }
      })
  } \where {
    \private \lemma gcd {M : GCDDomain} {D : DecSet M} (d : \Pi {x : M} -> x /=  -> x M.`#0) (a b : M) : TruncP (GCD a b)
      => \case decideEq a , decideEq b  \with {
        | yes a=0, _ => inP (GCD.swap {transportInv (GCD b __) a=0 (M.gcd_0 b)})
        | _, yes b=0 => inP (transportInv (GCD a __) b=0 (M.gcd_0 a))
        | no a/=0, no b/=0 => isGCDDomain a b (d a/=0) (d b/=0)
      }

    \lemma coprime-repr-aux {D : GCDDomain} {dec : IntegralDomain.Dec { | IntegralDomain => D }} (x : LocRing D.subMonoid)
      : ∃ (a b : D) (b#0 : D.#0 b) (GCD a b ) (x = inl~ (a, b, b#0)) \elim x
      | in~ (x,y,y#0) => \case decideEq x  \with {
        | yes x=0 => inP (, , zro#ide, GCD.swap {div_gcd LDiv.ide-div}, LocRing.equals1 $ simplify x=0)
        | no x/=0 => TruncP.map (isGCDDomain x y (dec.nonZeroApart x/=0) y#0) \lam (gcd : GCD x y) =>
            (gcd.res|val1.inv, gcd.res|val2.inv, D.#0-*-right $ transportInv D.#0 gcd.res|val2.inv-right y#0,
             gcd.reduce \lam {x} {y} => D.nonZero-cancel-left \lam gcd=0 => x/=0 $ inv gcd.res|val1.inv-right *> equation.cSemiring {gcd=0},
             LocRing.equals1 $ equation.cMonoid {inv gcd.res|val1.inv-right, gcd.res|val2.inv-right})
      }

    \lemma loc_poly {R : CRing} {S : SubMonoid R} (nt : \Pi {a : R} -> S a -> \Pi {x y : R} -> x * a = y * a -> x = y)
                    (p : Poly R) (m : isMonic p) {a b : R} {Sb : S b} (e : polyEval (polyMap locMap p) (inl~ (a,b,Sb)) = )
      : ∃ (n : Nat) (LDiv b (pow a n)) \elim m
      | inP (n, d, m) => inP (n, \new LDiv {
        | inv => negative $ R.BigSum \new Array R n \lam j => polyCoef p j * pow a j * pow b (n -' suc j)
        | inv-right => \have | s i q : locMap (polyCoef p i * pow a i * pow b (n -' i)) = polyCoef (polyMap locMap p) i * pow (inl~ (a,b,Sb)) i * pow (locMap b) n
                                 => locMap.func-* *> pmap (locMap _ *) locMap.func-pow *> pmap (`* _) (locMap.func-* *> pmap2 (*) (inv (polyCoef_polyMap {locMap})) locMap.func-pow) *> *-assoc *> pmap (_ *) (later $ rewriteI {} (<=_exists q) $ rewrite pow_+ $ pmap (`* _) (pmap (pow __ i) (LocRing.equals1 simplify) *> CMonoid.pow_*-comm) *> *-assoc) *> inv *-assoc
                             | t => inv (R.BigSum_suc {n} {\lam j => polyCoef p j * pow a j * pow b (n -' j)}) *> locMap-inj nt (locMap.func-BigSum {\new Array R (suc n) \lam j => polyCoef p j * pow a j * pow b (n -' j)} *> path (\lam i => AddMonoid.BigSum (\new Array (LocRing S) (suc n) \lam j => s j (<_suc_<= $ fin_< j) i)) *> inv (Semiring.BigSum-rdistr {_} {\new Array (LocRing S) (suc n) \lam j => polyCoef (polyMap locMap p) j * pow (inl~ (a,b,Sb)) j}) *> pmap (`* pow (locMap b) n) (inv (polyEval_polyCoef $ degree<=_degree< $ degree<=_polyMap d) *> e) *> zro_*-left)
                             | q (j : Fin n) => *-comm *> pmap (pow b) {suc (n -' suc j)} (NatSemiring.cancel-left j $ <=_exists (suc_<_<= $ fin_< j) *> inv (<=_exists $ LinearOrder.<_<= $ fin_< j))
                       \in R.negative-unique _ (pmap (`+ _) (R.negative_*-right *> pmap negative (R.BigSum-ldistr *> pmap R.BigSum (exts \lam j => equation.cRing {q j}))) *> negative-left) (pmap (_ +) (later (rewrite (m,-'id) simplify) *> inv (pmap (\lam x => polyCoef p x * pow a x * pow b (n -' x)) (mod_< id<suc))) *> t)
      })
  }
}