]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/procedural/CoRN/reals/Q_in_CReals.mma
Stuff moved from old Matita.
[helm.git] / matita / matita / contribs / procedural / CoRN / reals / Q_in_CReals.mma
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 include "CoRN.ma".
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 "model/reals/Cauchy_IR.ma".
30
31 include "model/monoids/Nmonoid.ma".
32
33 include "model/rings/Zring.ma".
34
35 (* UNEXPORTED
36 Section Rational_sequence_prelogue
37 *)
38
39 (*#*
40 %\begin{convention}% Let [R1] be a real number structure.
41 %\end{convention}%
42 *)
43
44 (* UNEXPORTED
45 cic:/CoRN/reals/Q_in_CReals/Rational_sequence_prelogue/R1.var
46 *)
47
48 (* We clone these proofs from CReals1.v just because there IR is an axiom *)
49
50 (* begin hide *)
51
52 inline procedural "cic:/CoRN/reals/Q_in_CReals/CReals_is_CReals.con" as lemma.
53
54 inline procedural "cic:/CoRN/reals/Q_in_CReals/Lim_Cauchy.con" as lemma.
55
56 inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes.con" as lemma.
57
58 inline procedural "cic:/CoRN/reals/Q_in_CReals/Archimedes'.con" as lemma.
59
60 (*#**************************************)
61
62 (* COERCION
63 cic:/Coq/NArith/BinPos/nat_of_P.con
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 procedural "cic:/CoRN/reals/Q_in_CReals/den_is_nonzero.con" as lemma.
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 procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q.con" as definition.
80
81 (*#* Next we need some properties of [nring], on the setoid of natural numbers: *)
82
83 inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_strext.con" as lemma.
84
85 inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_wd.con" as lemma.
86
87 inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_eq.con" as lemma.
88
89 inline procedural "cic:/CoRN/reals/Q_in_CReals/nring_leEq.con" as lemma.
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 procedural "cic:/CoRN/reals/Q_in_CReals/zring_strext.con" as lemma.
102
103 inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_wd.con" as lemma.
104
105 inline procedural "cic:/CoRN/reals/Q_in_CReals/zring_less.con" as lemma.
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 procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_strext.con" as lemma.
110
111 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_wd.con" as lemma.
112
113 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_plus.con" as lemma.
114
115 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_mult.con" as lemma.
116
117 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_less.con" as lemma.
118
119 inline procedural "cic:/CoRN/reals/Q_in_CReals/less_inj_Q.con" as lemma.
120
121 inline procedural "cic:/CoRN/reals/Q_in_CReals/leEq_inj_Q.con" as lemma.
122
123 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_leEq.con" as lemma.
124
125 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_min.con" as lemma.
126
127 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_minus.con" as lemma.
128
129 (*#* Moreover, and as expected, the [AbsSmall] predicate is also
130 preserved under the [inj_Q] *)
131
132 inline procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_AbsSmall.con" as lemma.
133
134 inline procedural "cic:/CoRN/reals/Q_in_CReals/AbsSmall_inj_Q.con" as lemma.
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 procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_Cauchy.con" as theorem.
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 procedural "cic:/CoRN/reals/Q_in_CReals/inj_Q_nring.con" as lemma.
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 procedural "cic:/CoRN/reals/Q_in_CReals/start_of_sequence.con" as theorem.
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 procedural "cic:/CoRN/reals/Q_in_CReals/Q_dense_in_CReals.con" as lemma.
168
169 (* UNEXPORTED
170 End Rational_sequence_prelogue
171 *)
172