\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 Algebra.Semiring
\import Arith.Nat
\import Data.Or
\import Equiv
\import Function
\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
\import Set.Fin.Instances
\open AddGroup
\open Monoid (pow)

\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' _ *> 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' _)
  | 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 : AddPointed} (a : A) (n : Nat) : A \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} {a : R} : Monoid.Inv {FSeriesRing R} (pow a) (polyCoef (padd (padd pzero (negative a)) )) \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
    }) *> rewrite (R.pow-comm1 idp) 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
  }

-- | Coefficients of $\frac{1}{1+x} = \sum_{n \geq 0} (-1)^n x^n$.
\func alt_pm {A : Ring} (n : Nat) : A
  => pow (A.negative ) n

-- | $(-1)^{n+1} = -(-1)^n$.
\lemma alt_pm-suc {A : Ring} {n : Nat} : alt_pm (suc n) = A.negative (alt_pm n)
  => A.negative_*-right *> pmap negative ide-right

-- | The identity series vanishes at every positive index.
\lemma pow-conv-zero-pos {A : Ring} {k : Nat} (k>0 :  NatSemiring.< k) : (FSeriesRing A).ide k =  \elim k
  | suc k => idp

\lemma conv_BigSum {A : Ring} (a b : FSeries A) (n : Nat)
  : (FSeriesRing A).* a b n = AddMonoid.BigSum (\new Array A (suc n) (\lam k => a k * b (n -' k)))
  => A.FinSum_char2 {FSeriesRing.PairsFinSet n} {\lam s => a s. A.* b s.}
    \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 *> -'+)
    }

{- | Finite-support lemma: if $b_0 = 0$, the $n$-fold convolution
     $b^{\star n}$ vanishes at every index $k < n$.

     Combinatorially, $(b^{\star n})_k = \sum b_{i_1} \cdots b_{i_n}$
     summed over compositions $i_1 + \cdots + i_n = k$.  If any $i_j = 0$ the
     factor $b_{i_j} = b_0 = 0$ kills the term, so all $i_j \geq 1$ and hence
     $k \geq n$. -}
\lemma pow-conv-zero-below {A : Ring} {b : FSeries A} (b_0 : b  = )
                           {n k : Nat} (k<n : k NatSemiring.< n)
  : pow b n k =  \elim n
  |  => absurd (\case k<n)
  | suc n => A.FinSum_zro $ later \case \elim __ \with {
    | (i, , p) => pmap (_ *) b_0 *> A.zro_*-right
    | (i, suc j, p) => pmap (* _) (pow-conv-zero-below b_0 linarith) *> A.zro_*-left
  }