The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Dear coq users and developpers,

We're currently working on a class project based on Coq for our master's
first year at the ENS of Lyon. Our goals include extending stdlib with
lemmas which ought to be there, and commenting/cleaning stdlib in order
to conform to the naming convention.

Across our work on real analysis and properties of real numbers, we
realized (and proved) that Coq's classical axiomatization of reals
implied Markov's principle and countable principle of omniscience. After
some research, we found out that it had been already proved by Kaliszyk
and O'Connor, and that is was to be put in stdlib (although I did not
find it in the SVN yet).

So I came up with two questions :

- From a purely logical point of view, does classical axiomatization of
reals implies stronger than those two principles? (I guess not, as the
main classical facts comes from the decidability of equality on reals,
which is isomorphic to decidable equality on sequences nat -> bool).

- Is there any interest to create a "per se" library of real numbers
that would not use classical facts in their full power?

I mean, most of the classical theorems of real analysis rely only upon
countable principle of omniscience (as most of the properties are
defined in terms of sequences). We could that way prove those theorems
using only the very nature of classical reals, and nothing more.

One of the most salient examples would be Bolzano-Weierstrass theorem
which is, I think, provable using only properties entailed by the
classical axiomatisation.

That way, we would have a three-level distinction on real analysis theorem :

1. Purely constructive theorems (that don't use dedidable equality)
2. Partly classical theorems (that only use Markov or omniscience)
3. Fully classical theorems (that use excluded middle over uncoutable sets)

As we have got time to spare to demonstrate such theorems, do you Coq
users and developpers think that it could have any interest? Or could we
rewrite semi-classical theorems of stdlib using the aforementioned
principles?

Cordially,
Pierre-Marie Pédrot