\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.Ring
\import Algebra.Ring.Localization
\import Algebra.Ring.Poly
\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(LDiv)

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

  \func nonZeroMonoid : CancelGCDMonoid \cowith
    | CancelCMonoid => IntegralDomain.nonZeroMonoid
    | isGCD x y =>
      \have | (inP (g : GCD x. y.)) => isGCDDomain x. y. x. y.
            | g*x#0 => transport #0 (inv g.gcd|val1.inv-right) x.
            | g#0 => #0-*-left g*x#0
      \in inP (\new GCD {
                 | gcd => (g.gcd, g#0)
                 | gcd|val1 => \new LDiv {
                   | inv => (g.gcd|val1.inv, #0-*-right g*x#0)
                   | inv-right => ext g.gcd|val1.inv-right
                 }
                 | gcd|val2 => \new LDiv {
                   | inv => (g.gcd|val2.inv, #0-*-right (transport #0 (inv g.gcd|val2.inv-right) y.))
                   | inv-right => ext g.gcd|val2.inv-right
                 }
                 | gcd-univ h (h|x : LDiv h x) (h|y : LDiv h y) =>
                   \have h|g : LDiv h. g.gcd => g.gcd-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
                   }
               })

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

  \func gcd_sum (d : E) (g : GCD {\this}) : GCD (g.val1 + g.val2 * d) g.val2 g.gcd \cowith
    | gcd|val1 => \new LDiv {
      | inv => g.gcd|val1.inv + g.gcd|val2.inv * d
      | inv-right => ldistr *> pmap2 (+) g.gcd|val1.inv-right (inv *-assoc *> pmap (`* d) g.gcd|val2.inv-right)
    }
    | gcd|val2 => g.gcd|val2
    | gcd-univ g' (g'|a+bd : LDiv) (g'|b : LDiv) => g.gcd-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 {
        | gcd|val1 => LDiv.id-div
        | gcd|val2 => LDiv.id-div
        | gcd-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 equation)
          | inr c1#0 => inP (_, inv $ div_loc $ nonZero_ldiv $ nonZeroMonoid.gcd_pow_div {c.,c.} {c.,c1#0} {e.}
                          (transport (LDiv _) (ext $ inv subMonoid.embed.func-pow) $ ldiv_nonZero {_} {_} {_, pow_#0 c1#0} e.) $ IsCoprime.<=gcd $ later \new GCD {
                            | gcd|val1 => LDiv.ide-div
                            | gcd|val2 => LDiv.ide-div
                            | gcd-univ g g|c2 g|c1 => ldiv_nonZero $ GCD.gcd-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 (, , , , equation, simplify)
          | no a/=0 =>
            \let | u => g.gcd|val2.inv
                 | v => g.gcd|val1.inv
                 | g' : GCD v u  => g.reduce $ LDiv_IsRegular g.gcd|val1 (IsRegular_/=0. a/=0)
                 | (inP (c,n,p)) => oneDimensional-char. d v u $ ldiv/=0 a/=0 (LDiv.swap g.gcd|val1)
                 | (inP (d,q)) => coprime_*_div p (IsCoprime_pow-right $ IsCoprime.<=gcd g')
            \in inP (c, d, u, v, rewriteI (g.gcd|val1.inv-right,g.gcd|val2.inv-right) equation, equation)
        }
      }

    \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 nonZeroMonoid.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 `#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 (gcd_0 b)})
        | _, yes b=0 => inP (transportInv (GCD a __) b=0 (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 : E) (b#0 : #0 b) (GCD a b ) (x = inl~ (a, b, b#0))
      | in~ (x,y,y#0) => \case decideEq x  \with {
        | yes x=0 => inP (, , zro#ide, GCD.swap {div_gcd LDiv.ide-div}, LocRing.equals1 equation)
        | no x/=0 => TruncP.map (isGCDDomain x y (nonZeroApart x/=0) y#0) \lam (gcd : GCD x y) =>
            (gcd.gcd|val1.inv, gcd.gcd|val2.inv, #0-*-right $ transportInv #0 gcd.gcd|val2.inv-right y#0,
             gcd.reduce \lam {x} {y} => nonZero-cancel-left \lam gcd=0 => x/=0 $ inv gcd.gcd|val1.inv-right *> equation,
             LocRing.equals1 $ equation {usingOnly (gcd.gcd|val1.inv-right, gcd.gcd|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) *> pow_*-comm) *> *-assoc) *> inv *-assoc
                             | t => inv (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 => BigSum (\new Array (LocRing S) (suc n) \lam j => s j (<_suc_<= $ fin_< j) i)) *> inv (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 negative-unique _ (pmap (`+ _) (negative_*-right *> pmap negative (BigSum-ldistr *> pmap BigSum (exts \lam j => equation {usingOnly (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)
      })
  }
}