The Coq mailing list

[Micaela Mayero <Micaela.Mayero AT inria.fr>]

> Dear All,
>
> I've been hearing word of a development of the real numbers and real 
> analysis in Coq for the last few months, but I can't find any concrete 
> references to the work. Can someone provide a pointer to any published or 
> unpublished research papers on this, or even just the contact name of the 
> developer? We've been developing real analysis in PVS and there've been a 
> number of other provers with real number/analysis developments recently 
> and I'm trying to keep up with them.

Hello,

Currently, there are, at least, two publications about the real numbers 
in Coq: it is an example of use of this developpement to prove the three
gap theorem (Steinhauss conjecture). The research report deals more with Coq 
and the real numbers. The paper is about the theorem itself.
  
ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-3848.ps.gz
ftp://ftp.inria.fr/INRIA/Projects/coq/Micaela.Mayero/PS/three-gap.ps.tar.gz

There is also some people at INRIA Sophia-Antipolis who work with real 
numbers in Coq (you can contact Loic Pottier: 
http://www-sop.inria.fr/lemme/Loic.Pottier/home.html).

A first version of this developpement, with basic lemmas, lemmas about the 
integer and fractional parts, developpements about limits and derivative is 
available with the Coq V6.3.1 distribution:

http://coq.inria.fr/

We can also see the real numbers theory specification on line at:

http://coq.inria.fr/library/REALS/

This work is in progress, and a new corrected version, more concise and
extended will be provided in the next version of Coq (V7).

If you have questions (or remarks), I'll be happy to answer.

Best Regards,

Micaela.

=============================================================================
Micaela Mayero                               <Email>: 
Micaela.Mayero AT inria.fr
<Laboratory>: The Coq Project                         <Domain>: Formal Proofs
<Adress>: INRIA-Rocquencourt Domaine de Voluceau BP105 78153 Le Chesnay Cedex
          FRANCE
<Tel>: (33)-(0)1 39 63 57 51
<Fax>: (33)-(0)1 39 63 56 84
<Url>: http://pauillac.inria.fr/~mayero
=============================================================================