The Coq mailing list

[Cedric Auger <sedrikov AT gmail.com>]

2013/10/1 Jason Gross <jasongross9 AT gmail.com>

I assume that by "dense", the desired theorem is that between every two non-equal rational numbers there's a real number.  This is very easy, though: just convert their average to a real number.  Alternatively, you might want the theorem that the irrationals are dense in the rationals (between every two non-equal rationals there is an irrational); I don't know how to prove this).

Hmm, wouldn't it be better to say that "the irrationals are dense in the reals"? As far as I remember, "X is dense IN Y" implies that X is a subset of Y (else, they are not "<some property> IN").
And for that last proof, it should not be hard. Take two rationals x and y such that x<y, x+π⁻¹×(y-x) is irrational (else by stability of the usual operations, that would mean that ((x+π⁻¹×(y-x))×(y-x)⁻¹-x)⁻¹ = π would be rational.
Furthermore, as 0<π⁻¹<1, 0<π⁻¹×(y-x)<y-x, and so x<x+π⁻¹×(y-x)<y.
 

-Jason

On Tuesday, October 1, 2013, Jacques-Henri Jourdan wrote:

Le 01/10/2013 07:51, Lucian M. Patcas a écrit :

Hi,

I have a few questions about real numbers in Coq:

1. Is there a notation for concrete real numbers in Coq, e.g. how can I write 10.55 in Coq?

There is the Q2R function to convert a rational to a real.

2. Is there a theorem or an axiom in the Standard Library that the real numbers are dense? (perhaps I managed to miss it)

What do you mean by dense ? There is the completeness axiom and the R_complete theorem that states that every Cauchy sequence converges.

3. Is anyone aware of a proof in Coq that the real numbers are dense?

Thanks,
Lucian

--
JH

--
.../Sedrikov\...