Ssreflect Users Discussion List

[Florent Hivert <>]

      Hi there,

I'm seriously considering to start to develop a library for formal power
series in math-comp. First of all, even if it is not necessary, I'm planing to
work on top of mathcomp-analysis to deal with decidability of equality
problems. I've given it a very first try, and I think I need to step back to
build a strategy. I'm currently considering two paths, I'd like to gather
opinion to make my choice:

 1 - Define a series as a function nat -> R

    Record fpseries := FPSeries { seriesfun : nat -> R }.

pro:  one can adapt easily what was done for polynomials in poly.v
pro:  might be sufficient for most need
cons: lots of code duplication, only works for univariate power series.

 2 - Start by building a generic inverse limit theory :

    Record invlim :=
      InvLim { types : nat -> Type;
               mor   : forall n, types n.+1 -> types n }.

    showing that if the (types n) are R-algebras and the (mor n) are R-algebra
    morphisms, then invlim is canonically an R-algebra.

    And apply the theory to truncated polynomials :

    Record trunc_polynomial :=
      TruncPolynomial {trpoly : {poly R}; _ : (size trpoly <= n)%N}.

pro:  all the algebraic relations like associativity are nearly free
pro:  one can easily reuse for multivariate or non-commutative series
cons: may be much harder if not overkill

Please feel free to comment and suggest alternative paths.

Best,

Florent