The Coq mailing list

[Yves Bertot <yves.bertot AT inria.fr>]

Co-inductive digit sequences provide reasonable efficiency, but because 
co-induction privileges laziness, efficiency is not always obtained.  If 
you know beforehand that you want a a result with a high precision, it 
is better to work eagerly to that precision, using divide-and-conquer 
strategies that are not exploited in lazy approaches.

Guillaume Melquiond mentioned Nicolas Julien's thesis.  In this work, 
the real numbers are represented by the pair of an exponent (of the 
base), and an infinite sequence of signed digits.  Most operations are 
provided, but the proofs of correctness rely on the axiomatized real 
numbers of the Coq's standard library.  For this reason, this 
development does not serve as a "constructive" model of the real 
numbers.   It takes a more pragmatical approach: to justify the 
correctness of algorithms (which are inherently constructive), you can 
use classical reasoning (here classical reasoning is ingrained in the 
axioms for real numbers).  This is not work towards building a model of 
real numbers.

If you want to use coinductive sequences of signed digits to build a 
model of constructive real numbers, it is probably sensible to look at 
work by P. di Gianantonio and A. Ciaffaglione at the end of the 90s.

@InProceedings{ciaffaglione.00,
 author =       {Alberto Ciaffaglione and Pietro di Gianantonio},
 title =        {A coinductive approach to real numbers},
 booktitle =    {Types 1999 Workshop, L\"okeberg, Sweden},
 year =         {2000},
 series =       {LNCS},
 number =       {1956},
 editor =       {Th.~Coquand and P.~Dybjer and B.~Nordstr\"om and 
J.~Smith},
 pages =        {114-130},
 publisher =    springer,
}

I hope this helps.

Yves