helm/software/matita/contribs/CoRN-Decl/reals/Q_in_CReals.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 (* This file was automatically generated: do not edit *********************)
  16
  17 set "baseuri" "cic:/matita/CoRN-Decl/reals/Q_in_CReals".
  18
  19 (* $Id: Q_in_CReals.v,v 1.10 2004/04/23 10:01:05 lcf Exp $ *)
  20
  21 (*#* * On density of the image of [Q] in an arbitrary real number structure
  22 In this file we introduce the image of the concrete rational numbers
  23 (as defined earlier) in an arbitrary structure of type
  24 [CReals]. At the end of this file we assign to any real number two
  25 rational numbers for which the real number lies betwen image of them;
  26 in other words we will prove that the image of rational numbers in
  27 dense in any real number structure. *)
  28
  29 (* INCLUDE
  30 Cauchy_IR
  31 *)
  32
  33 (* INCLUDE
  34 Nmonoid
  35 *)
  36
  37 (* INCLUDE
  38 Zring
  39 *)
  40
  41 (* UNEXPORTED
  42 Section Rational_sequence_prelogue.
  43 *)
  44
  45 (*#*
  46 %\begin{convention}% Let [R1] be a real number structure.
  47 %\end{convention}%
  48 *)
  49
  50 inline cic:/CoRN/reals/Q_in_CReals/R1.var.
  51
  52 (* We clone these proofs from CReals1.v just because there IR is an axiom *)
  53
  54 (* begin hide *)
  55
  56 inline cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con.
  57
  58 inline cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con.
  59
  60 inline cic:/CoRN/reals/Q_in_CReals/Archimedes.con.
  61
  62 inline cic:/CoRN/reals/Q_in_CReals/Archimedes'.con.
  63
  64 (*#**************************************)
  65
  66 (* end hide *)
  67
  68 (*#*
  69 ** Injection from [Q] to an arbitrary real number structure
  70  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].
  71
  72  To define the injection we need one elemntary lemma about the denominator:
  73 *)
  74
  75 inline cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con.
  76
  77 (*#* 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]. *)
  78
  79 inline cic:/CoRN/reals/Q_in_CReals/inj_Q.con.
  80
  81 (*#* Next we need some properties of [nring], on the setoid of natural numbers: *)
  82
  83 inline cic:/CoRN/reals/Q_in_CReals/nring_strext.con.
  84
  85 inline cic:/CoRN/reals/Q_in_CReals/nring_wd.con.
  86
  87 inline cic:/CoRN/reals/Q_in_CReals/nring_eq.con.
  88
  89 inline cic:/CoRN/reals/Q_in_CReals/nring_leEq.con.
  90
  91 (* begin hide *)
  92
  93 (* UNEXPORTED
  94 Unset Printing Coercions.
  95 *)
  96
  97 (* end hide *)
  98
  99 (*#* Similarly we prove some properties of [zring] on the ring of integers: *)
 100
 101 inline cic:/CoRN/reals/Q_in_CReals/zring_strext.con.
 102
 103 inline cic:/CoRN/reals/Q_in_CReals/zring_wd.con.
 104
 105 inline cic:/CoRN/reals/Q_in_CReals/zring_less.con.
 106
 107 (*#* 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. *)
 108
 109 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con.
 110
 111 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con.
 112
 113 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con.
 114
 115 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con.
 116
 117 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con.
 118
 119 inline cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con.
 120
 121 inline cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con.
 122
 123 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con.
 124
 125 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con.
 126
 127 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con.
 128
 129 (*#* Moreover, and as expected, the [AbsSmall] predicate is also
 130 preserved under the [inj_Q] *)
 131
 132 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con.
 133
 134 inline cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con.
 135
 136 (*#* ** Injection preserves Cauchy property
 137 We apply the above lemmata to obtain following theorem, which says
 138 that a Cauchy sequence of elemnts of [Q] will be Cauchy in [R1].
 139 *)
 140
 141 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con.
 142
 143 (*#* Furthermore we prove that applying [nring] (which is adding the
 144 ring unit [n] times) is the same whether we do it in [Q] or in [R1]:
 145 *)
 146
 147 inline cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con.
 148
 149 (*#* ** Injection of [Q] is dense
 150 Finally we are able to prove the density of image of [Q] in [R1]. We
 151 state this fact in two different ways. Both of them have their
 152 specific use.
 153
 154 The first theorem states the fact that any real number can be bound by
 155 the image of two rational numbers. This is called [start_of_sequence]
 156 because it can be used as an starting point for the typical "interval
 157 trisection" argument, which is ubiquitous in constructive analysis.
 158 *)
 159
 160 inline cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con.
 161
 162 (*#* The second version of the density of [Q] in [R1] states that given
 163 any positive real number, there is a rational number between it and
 164 zero. This lemma can be used to prove the more general fact that there
 165 is a rational number between any two real numbers. *)
 166
 167 inline cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con.
 168
 169 (* UNEXPORTED
 170 End Rational_sequence_prelogue.
 171 *)
 172