  We extend the work of A. Ciaffaglione and P. Di Gianantonio on mechanical
verification of algorithms for exact computation on real numbers, using
infinite streams of digits implemented as co-inductive types. Four aspects are
studied: the first aspect concerns the proof that digit streams can be related
to the axiomatized real numbers that are already axiomatized in the proof
system (axiomatized, but with no fixed representation). The second aspect
re-visits the definition of an addition function, looking at techniques to let
the proof search mechanism perform the effective construction of an algorithm
that is correct by construction. The third aspect concerns the definition of a
function to compute affine formulas with positive rational coefficients. This
should be understood as a testbed to describe a technique to combine
co-recursion and recursion to obtain a model for an algorithm that appears at
first sight to be outside the expressive power allowed by the proof system. The
fourth aspect concerns the definition of a function to compute series, with an
application on the series that is used to compute Euler's number e. All these
experiments should be reproducible in any proof system that supports
co-inductive types, co-recursion and general forms of terminating recursion,
but we performed with the Coq system [12, 3, 14].
