The Coq mailing list

[Freek Wiedijk <freek AT cs.ru.nl>]

Andrej:

>That is exactly what most implementations of real number do. For
>example Robbert Krebbers and Bas Spitter's, the first link I provided,
>works with dyadic rationals (which are rationals of the form m * 2^e,
>just like you'd like them to be). Their implementation is written in
>Coq.

Note that this is the culmination of quite a bit of work
on the CoRN (Coq Repository Nijmegen) library.  Earlier
PhD's that worked on this library were Milad Niqui, Luís
Cruz-Filipe and Russell O'Connor.  In fact, Milad Niqui
already fully developed the theory of constructive reals,
he just didn't have a computationally efficient version yet.
Only Robbert went to the obvious  choice of dyadic rationals
for the Cauchy sequences, I think, please correct me if I'm
wrong (I think Russell also still used ordinary rationals.)

I understand that CoRN might currently be in a bit of disarray,
because Robbert and Bas started changing to a different
form for the algebraic hierarchy, using type classes (see
<http://robbertkrebbers.nl/research/articles/typeclasses_reals.pdf>),
but large parts of the library still are about the old
representation.  I don't know what exactly the state of
this is, maybe Robbert can tell us?

Note also that the library <http://lipforge.ens-lyon.fr/www/pff/>
originally by Laurent Théry and Laurence Rideau and
currently maintained by Sylvie Boldo is also about rationals
of the form m * 2^e.  I don't know whether they built exact
real numbers out of _their_ floating point numbers, though.
Laurent, can you tell us?

Freek