\import Algebra.Algebra
\import Algebra.Domain
\import Algebra.Group
\import Algebra.Meta
\import Algebra.Monoid
\import Algebra.Pointed
\import Algebra.Ring
\import Algebra.Ring.Poly
\import Algebra.Ring.RingHom
\import Arith.Nat
\import Data.Or
\import Equiv
\import Function.Meta
\import Logic
\import Logic.Meta
\import Meta
\import Order.Biordered
\import Order.LinearOrder
\import Order.PartialOrder
\import Order.StrictOrder
\import Paths
\import Paths.Meta
\import Set.Fin
\open AddGroup

\type FSeries (R : \Set) => Nat -> R

\lemma fseries-apply {R : \Set} {x y : FSeries R} (p : x = y) {n : Nat} : x n = y n \elim p
  | idp => idp

\instance FSeriesRing (R : Ring) : Ring (FSeries R)
  | zro _ => 
  | + f g n => f n + g n
  | zro-left => ext \lam n => zro-left
  | +-assoc => ext \lam n => +-assoc
  | +-comm => ext \lam n => +-comm
  | negative f n => negative (f n)
  | negative-left => ext \lam n => negative-left
  | ide => coef 
  | * f g n => R.FinSum {PairsFinSet n} \lam s => f s. * g s.
  | *-assoc {x} {y} {z} => ext \lam n => path (\lam i => R.FinSum (\lam (s : PairsFinSet n) => R.FinSum-rdistr {PairsFinSet s.} {z s.} {\lam t => x t. * y t.} i)) *>
      R.FinSum-double-dep (\lam (s : PairsFinSet n) => PairsFinSet s.) *> R.FinSum_Equiv2 (later \new QEquiv {
        | f ((i,j,i+j=n),(k,m,k+m=i)) => ((k, m + j, inv +-assoc *> pmap (`+ j) k+m=i *> i+j=n), (m, j, idp))
        | ret ((i,j,i+j=n),(k,m,k+m=j)) => ((i + k, m, +-assoc *> pmap (i +) k+m=j *> i+j=n), (i, k, idp))
        | ret_f s => PairsFinSet-ext1 s.. idp idp idp
        | f_sec s => PairsFinSet-ext2 idp s.. idp idp
      }) (\lam s => *-assoc) *> inv (path (\lam i => R.FinSum (\lam (s : PairsFinSet n) => R.FinSum-ldistr {PairsFinSet s.} {x s.} {\lam t => y t. * z t.} i)) *> R.FinSum-double-dep (\lam (s : PairsFinSet n) => PairsFinSet s.) {\lam s => x s.. * (y s.. * z s..)})
  | ldistr => ext \lam n => pmap R.FinSum (ext \lam s => R.ldistr) *> R.FinSum_+
  | rdistr => ext \lam n => pmap R.FinSum (ext \lam s => R.rdistr) *> R.FinSum_+
  | ide-left {x} => ext \lam n => R.FinSum-unique (later (, n, idp)) (\lam s s/=0 => pmap (`* _) (coef_/=0 \lam p => s/=0 $ ext (p, pmap (`+ _) (inv p) *> s.)) *> R.zro_*-left) *> ide-left
  | ide-right {x} => ext \lam n => R.FinSum-unique (later (n, , idp)) (\lam s s/=0 => pmap (_ *) (coef_/=0 \lam p => s/=0 $ ext (pmap (_ +) (inv p) *> s., p)) *> R.zro_*-right) *> ide-right
  | natCoef n => coef (R.natCoef n)
  | natCoefZero => ext \case \elim __\with {
    |  => R.natCoefZero
    | suc j => idp
  }
  | natCoefSuc n => ext \case \elim __\with {
    |  => R.natCoefSuc n
    | suc j => inv zro-left
  }
  \where {
    \func coef (a : R) (n : Nat) : R \elim n
      |  => a
      | suc _ => 

    \lemma coef_/=0 {a : R} {n : Nat} (n/=0 : n /= ) : coef a n =  \elim n
      |  => absurd (n/=0 idp)
      | suc n => idp

    \lemma PairsFinSet (n : Nat) : FinSet (\Sigma (i j : Nat) (\property i + j = n)) (suc n) \cowith
      | finEq => inP \new QEquiv {
        | f i => (i, n -' i, <=_exists $ <_suc_<= $ fin_< i)
        | ret s => toFin s. $ <=_<_suc $ NatSemiring.<=_+ <=-refl zero<=_ <=∘ =_<= s.
        | ret_f i => fin_nat-inj toFin=id
        | f_sec s => ext (toFin=id, pmap2 (`-') (inv s. *> +-comm) toFin=id *> -'+)
      }

    \lemma PairsFinSet-ext1 {n : Nat} {x y : \Sigma (s : PairsFinSet n) (PairsFinSet s.)} (p1 : x.. = y..) (p2 : x.. = y..) (p3 : x.. = y..) (p4 : x.. = y..) : x = y \elim x, y, p1, p2, p3, p4
      | ((i1,j1,p1),(k1,m1,q1)), ((i2,j2,p2),(k2,m2,q2)), idp, idp, idp, idp => idp

    \lemma PairsFinSet-ext2 {n : Nat} {x y : \Sigma (s : PairsFinSet n) (PairsFinSet s.)} (p1 : x.. = y..) (p2 : x.. = y..) (p3 : x.. = y..) (p4 : x.. = y..) : x = y \elim x, y, p1, p2, p3, p4
      | ((i1,j1,p1),(k1,m1,q1)), ((i2,j2,p2),(k2,m2,q2)), idp, idp, idp, idp => idp

    \lemma Pairs_zero {f : PairsFinSet  -> R} : R.FinSum f = f (,,idp)
      => R.FinSum-unique (later (,,idp)) \lam s s/=0 => absurd $ s/=0 $ ext
            (<=-antisymmetric (transport (_ <=) s. $ NatSemiring.<=_+ <=-refl zero<=_) zero<=_,
             <=-antisymmetric (transport (_ <=) s. $ NatSemiring.<=_+ zero<=_ <=-refl) zero<=_)

    \lemma Pairs_suc-left {n : Nat} {f : PairsFinSet (suc n) -> R}
      : R.FinSum f = f (, suc n, idp) + R.FinSum \lam (s : PairsFinSet n) => f (suc s., s., pmap suc s.)
      => R.FinSum_Equiv2 (later \new QEquiv {
        | f => \case \elim __ \with {
          | (, _, _) => inl ()
          | (suc i, j, p) => inr (i, j, pmap pred p)
        }
        | ret => \case \elim __ \with {
          | inl _ => (, suc n, idp)
          | inr s => (suc s., s., pmap suc s.)
        }
        | ret_f => \case \elim __ \with {
          | (, j, p) => ext (idp, inv p)
          | (suc i, j, p) => idp
        }
        | f_sec => \case \elim __ \with {
          | inl _ => idp
          | inr s => idp
        }
      }) (later \case \elim __ \with {
        | (, j, p) => pmap f $ ext (idp,p)
        | (suc i, j, p) => idp
      }) *> R.FinSum_Or {UnitFin} {PairsFinSet n} {Or.rec (\lam _ => f (, suc n, idp)) (\lam s => f (suc s., s., pmap suc s.))} *> pmap (`+ _) (R.FinSum-unique () (\lam k c => absurd $ c idp))
  }

\instance FSeriesAlgebra (R : CRing) : CAlgebra R
  | Ring => FSeriesRing R
  | *c c x n => c * x n
  | *c-assoc => ext \lam n => *-assoc
  | *c-ldistr => ext \lam n => R.ldistr
  | *c-rdistr => ext \lam n => R.rdistr
  | ide_*c => ext \lam n => ide-left
  | *c-comm-left => ext \lam n => R.FinSum-ldistr *> pmap R.FinSum (ext \lam s => inv *-assoc)
  | coefMap a => FSeriesRing.coef a
  | coefMap_*c => ext \case \elim __\with {
    |  => inv ide-right
    | suc j => inv R.zro_*-right
  }
  | *-comm => ext \lam n => R.FinSum_Equiv2 (later \new QEquiv {
    | f s => (s., s., +-comm *> s.)
    | ret s => (s., s., +-comm *> s.)
    | ret_f => idpe
    | f_sec => idpe
  }) \lam s => *-comm

\instance FSeriesRingWith# (R : Ring.With#) : Ring.With#
  | Ring => FSeriesRing R
  | #0 x => ∃ (n : Nat) (x n `#0)
  | #0-zro (inP (_,p)) => #0-zro p
  | #0-+ (inP (n,p)) => \case #0-+ p \with {
    | byLeft xn#0 => byLeft $ inP (n, xn#0)
    | byRight yn#0 => byRight $ inP (n, yn#0)
  }
  | #0-tight c => ext \lam n => #0-tight \lam xn#0 => c $ inP (n, xn#0)
  | #0-*-left (inP (n,p)) => \case R.#0-FinSum p \with {
    | inP (s,q) => inP (s., R.#0-*-left q)
  }
  | #0-*-right (inP (n,p)) => \case R.#0-FinSum p \with {
    | inP (s,q) => inP (s., R.#0-*-right q)
  }

\instance FSeriesCRingWith# (R : CRing.With#) : CRing.With#
  | Ring.With# => FSeriesRingWith# R
  | *-comm => (FSeriesAlgebra R).*-comm

\instance FSeriesDomain (R : Domain) : Domain
  | Ring.With# => FSeriesRingWith# R
  | zro#ide => inP (, R.zro#ide)
  | #0-* (inP (n,xn#0)) (inP (m,ym#0)) => aux {R} {_} {n} {m} id<suc xn#0 ym#0
  \where {
    \protected \lemma aux {k n m : Nat} (n+m<k : n + m < k) {x y : FSeries R} (xn#0 : x n `#0) (ym#0 : y m `#0) : ∃ (k : Nat) ((x * y) k `#0) \elim k
      | suc k => \case R.#0-FinSum-conv {FSeriesRing.PairsFinSet (n + m)} {_} {n,m,idp} (R.#0-* xn#0 ym#0) \with {
        | byLeft r => inP (n + m, r)
        | byRight ((i,j,i+j=n+m),ij/=nm,p) => \case LinearOrder.dec<_<= i n \with {
          | inl i<n => aux (NatSemiring.<_+-left m i<n <∘l <_suc_<= n+m<k) (R.#0-*-left p) ym#0
          | inr n<=i => aux (NatSemiring.<_+-right n (\case LinearOrder.dec<_<= j m \with {
            | inl j<m => j<m
            | inr m<=j => absurd $ ij/=nm $ ext
              \have j=m => <=-antisymmetric (NatBSemilattice.<=_cancel-left i $ =_<= i+j=n+m <=∘ NatSemiring.<=_+ n<=i <=-refl) m<=j
              \in (NatSemiring.cancel-right j $ i+j=n+m *> pmap (n +) (inv j=m), j=m)
          }) <∘l <_suc_<= n+m<k) xn#0 (R.#0-*-right p)
        }
      }
  }

\instance FSeriesIntegralDomain (R : IntegralDomain) : IntegralDomain
  | Domain => FSeriesDomain R
  | *-comm => (FSeriesAlgebra R).*-comm

\func poly-FSeries {R : Ring} : RingHom (PolyRing R) (FSeriesRing R) (polyCoef __) \cowith
  | func-+ => ext \lam n => polyCoef_+
  | func-ide => ext \case \elim __\with {
    |  => idp
    | suc n => idp
  }
  | func-* => ext \lam n => *-lem
  \where {
    \lemma *-lem {p q : Poly R} {n : Nat} : polyCoef (p * q) n = (polyCoef p * {FSeriesRing R} polyCoef q) n \elim p, n
      | pzero, n => inv $ fseries-apply $ (FSeriesRing R).zro_*-left {polyCoef q}
      | padd p e,  => polyCoef_+ *> zro-left *> polyCoef_*c *> inv FSeriesRing.Pairs_zero
      | padd p e, suc n => polyCoef_+ *> pmap2 (+) *-lem polyCoef_*c *> +-comm *> inv FSeriesRing.Pairs_suc-left
  }

\lemma geometric-FSeries {R : Ring} : Monoid.Inv {FSeriesRing R} (\lam _ => ) (polyCoef (padd (padd pzero -1) )) \cowith
  | inv-left => ext \case \elim __ \with {
    |  => FSeriesRing.Pairs_zero *> ide-left
    | suc n => R.FinSum-unique2 {FSeriesRing.PairsFinSet (suc n)} {, suc n, idp} {, n, idp} (\lam p => \case pmap __. p) (\case \elim __ \with {
      | (, j, p) => \lam q => absurd $ q $ ext (idp, p)
      | (, j, p) => \lam _ q => absurd $ q $ ext (idp, pmap pred p)
      | (suc (suc i), _, _) => \lam _ _ => R.zro_*-left
    }) *> equation.ring
  }
  | inv-right => ext \case \elim __ \with {
    |  => FSeriesRing.Pairs_zero *> ide-left
    | suc n => R.FinSum-unique2 {FSeriesRing.PairsFinSet (suc n)} {suc n, , idp} {n, , idp} (\lam p => \case pmap __. p) (\case \elim __ \with {
      | (i, , p) => \lam q => absurd $ q $ ext (p, idp)
      | (i, , p) => \lam _ q => absurd $ q $ ext (pmap pred p, idp)
      | (_, suc (suc j), _) => \lam _ _ => R.zro_*-right
    }) *> equation.ring
  }