1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_in_CReals".
21 (* $Id: Q_in_CReals.v,v 1.10 2004/04/23 10:01:05 lcf Exp $ *)
23 (*#* * On density of the image of [Q] in an arbitrary real number structure
24 In this file we introduce the image of the concrete rational numbers
25 (as defined earlier) in an arbitrary structure of type
26 [CReals]. At the end of this file we assign to any real number two
27 rational numbers for which the real number lies betwen image of them;
28 in other words we will prove that the image of rational numbers in
29 dense in any real number structure. *)
31 include "model/reals/Cauchy_IR.ma".
33 include "model/monoids/Nmonoid.ma".
35 include "model/rings/Zring.ma".
38 Section Rational_sequence_prelogue
42 %\begin{convention}% Let [R1] be a real number structure.
46 inline "cic:/CoRN/reals/Q_in_CReals/Rational_sequence_prelogue/R1.var" "Rational_sequence_prelogue__".
48 (* We clone these proofs from CReals1.v just because there IR is an axiom *)
52 inline "cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con".
54 inline "cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con".
56 inline "cic:/CoRN/reals/Q_in_CReals/Archimedes.con".
58 inline "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con".
60 (*#**************************************)
62 coercion cic:/Coq/NArith/BinPos/nat_of_P.con 0 (* compounds *).
67 ** Injection from [Q] to an arbitrary real number structure
68 First we need to define the injection from [Q] to [R1]. Note that in [Cauchy_CReals] we defined [inject_Q] from an arbitray field [F] to [(R_COrdField F)] which was the set of Cauchy sequences of that field. But since [R1] is an %\emph{arbitrary}%#<i>arbitrary</i># real number structure we can not use [inject_Q].
70 To define the injection we need one elemntary lemma about the denominator:
73 inline "cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con".
75 (*#* And we define the injection in the natural way, using [zring] and [nring]. We call this [inj_Q], in contrast with [inject_Q] defined in [Cauchy_CReals]. *)
77 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q.con".
79 (*#* Next we need some properties of [nring], on the setoid of natural numbers: *)
81 inline "cic:/CoRN/reals/Q_in_CReals/nring_strext.con".
83 inline "cic:/CoRN/reals/Q_in_CReals/nring_wd.con".
85 inline "cic:/CoRN/reals/Q_in_CReals/nring_eq.con".
87 inline "cic:/CoRN/reals/Q_in_CReals/nring_leEq.con".
92 Unset Printing Coercions.
97 (*#* Similarly we prove some properties of [zring] on the ring of integers: *)
99 inline "cic:/CoRN/reals/Q_in_CReals/zring_strext.con".
101 inline "cic:/CoRN/reals/Q_in_CReals/zring_wd.con".
103 inline "cic:/CoRN/reals/Q_in_CReals/zring_less.con".
105 (*#* Using the above lemmata we prove the basic properties of [inj_Q], i.e.%\% it is a setoid function and preserves the ring operations and oreder operation. *)
107 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con".
109 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con".
111 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con".
113 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con".
115 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con".
117 inline "cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con".
119 inline "cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con".
121 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con".
123 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con".
125 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con".
127 (*#* Moreover, and as expected, the [AbsSmall] predicate is also
128 preserved under the [inj_Q] *)
130 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con".
132 inline "cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con".
134 (*#* ** Injection preserves Cauchy property
135 We apply the above lemmata to obtain following theorem, which says
136 that a Cauchy sequence of elemnts of [Q] will be Cauchy in [R1].
139 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con".
141 (*#* Furthermore we prove that applying [nring] (which is adding the
142 ring unit [n] times) is the same whether we do it in [Q] or in [R1]:
145 inline "cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con".
147 (*#* ** Injection of [Q] is dense
148 Finally we are able to prove the density of image of [Q] in [R1]. We
149 state this fact in two different ways. Both of them have their
152 The first theorem states the fact that any real number can be bound by
153 the image of two rational numbers. This is called [start_of_sequence]
154 because it can be used as an starting point for the typical "interval
155 trisection" argument, which is ubiquitous in constructive analysis.
158 inline "cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con".
160 (*#* The second version of the density of [Q] in [R1] states that given
161 any positive real number, there is a rational number between it and
162 zero. This lemma can be used to prove the more general fact that there
163 is a rational number between any two real numbers. *)
165 inline "cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con".
168 End Rational_sequence_prelogue