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 *********************)
19 (* $Id: CauchySeq.v,v 1.8 2004/04/23 10:01:04 lcf Exp $ *)
21 (*#* printing IR %\ensuremath{\mathbb R}% *)
23 (*#* printing PartIR %\ensuremath{\mathbb R\!\not\rightarrow\!\mathbb R}% *)
25 (*#* printing ZeroR %\ensuremath{\mathbf0}% #0# *)
27 (*#* printing OneR %\ensuremath{\mathbf1}% #1# *)
29 (*#* printing AbsIR %\ensuremath{|\cdot|_{\mathbb R}}% *)
31 include "reals/CReals.ma".
33 (*#* *Real Number Structures
34 %\begin{convention}% Let [IR] be a structure for real numbers.
39 Require Export R_CReals.
40 Definition IR : CReals := Concrete_R.
44 alias id "IR" = "cic:/CoRN/reals/CauchySeq/IR.var".
47 Notation PartIR := (PartFunct IR).
51 Notation ProjIR1 := (prj1 IR _ _ _).
55 Notation ProjIR2 := (prj2 IR _ _ _).
58 include "tactics/Transparent_algebra.ma".
63 Notation ZeroR := (Zero:IR).
67 Notation OneR := (One:IR).
76 (*#* ** [CReals] axioms *)
78 inline procedural "cic:/CoRN/reals/CauchySeq/CReals_is_CReals.con" as lemma.
80 (*#* First properties which follow trivially from the axioms. *)
82 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_Cauchy.con" as lemma.
84 inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes.con" as lemma.
86 inline procedural "cic:/CoRN/reals/CauchySeq/Archimedes'.con" as lemma.
88 (*#* A stronger version, which often comes in useful. *)
90 inline procedural "cic:/CoRN/reals/CauchySeq/str_Archimedes.con" as lemma.
92 inline procedural "cic:/CoRN/reals/CauchySeq/CauchySeqR.con" as definition.
102 (*#* ** Cauchy sequences
103 *** Alternative definitions
104 This section gives several definitions of Cauchy sequences. There
105 are no lemmas in this section.
107 The current definition of Cauchy ([Cauchy_prop]) is:
109 %\[\forall \epsilon>0. \exists N. \forall m\geq N. |seq_m - seq_N|\leq\varepsilon\]%
110 #for all e>0 there exists N such that for all m≥ N |seqm-seqN|≤ e#
112 Variant 1 of Cauchy ([Cauchy_prop1]) is:
114 %\[\forall k. \exists N. \forall m \geq N. |seq_m - seq_N|\leq1/(k+1)\]%
115 #for all k there exists N such that for all m ≥ N |seqm-seqN| ≤ 1/(k+1)#
117 In all of the following variants the limit occurs in the definition.
118 Therefore it is useful to define an auxiliary predicate
119 [Cauchy_Lim_prop?], in terms of which [Cauchy_prop?] is defined.
121 Variant 2 of Cauchy ([Cauchy_prop2]) is [exists y, (Cauchy_Lim_prop2 seq y)]
124 Cauchy_Lim_prop2 seq y := forall eps [>] Zero, exists N, forall m >= N, (AbsIR seq m - y) [<=] eps
127 Note that [Cauchy_Lim_prop2] equals [seqLimit].
129 Variant 3 of Cauchy ([Cauchy_prop3]) reads [exists y, (Cauchy_Lim_prop3 seq y)]
132 Cauchy_Lim_prop3 seq y := forall k, exists N, forall m >= N, (AbsIR seq m - y) [<=] One[/] (k[+]1)
135 The following variant is more restricted.
137 Variant 4 of Cauchy ([Cauchy_prop4]): [exists y, (Cauchy_Lim_prop4 seq y)]
140 Cauchy_Lim_prop4 seq y := forall k, (AbsIR seq m - y) [<=] One[/] (k[+]1)
145 Cauchy_prop4 -> Cauchy_prop3 Iff Cauchy_prop2 Iff Cauchy_prop1 Iff Cauchy_prop
147 Note: we don't know which formulations are useful.
149 The inequalities are stated with [[<=]] rather than with [<] for the
150 following reason: both formulations are equivalent, as is well known;
151 and [[<=]] being a negative statement, this makes proofs
152 sometimes easier and program extraction much more efficient.
155 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1.con" as definition.
157 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2.con" as definition.
159 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2.con" as definition.
161 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3.con" as definition.
163 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3.con" as definition.
165 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4.con" as definition.
167 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4.con" as definition.
177 (*#* *** Inequalities of Limits
179 The next lemma is equal to lemma [Lim_Cauchy]. *)
181 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_complete.con" as lemma.
183 inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so_less_seq.con" as lemma.
185 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so_seq_less.con" as lemma.
187 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_Lim_so_seq_less_seq.con" as lemma.
189 (*#* The next lemma follows from [less_Lim_so_less_seq] with [y := (y[+] (Lim seq)) [/]TwoNZ]. *)
191 inline procedural "cic:/CoRN/reals/CauchySeq/less_Lim_so.con" as lemma.
193 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_less_so.con" as lemma.
195 inline procedural "cic:/CoRN/reals/CauchySeq/leEq_seq_so_leEq_Lim.con" as lemma.
197 inline procedural "cic:/CoRN/reals/CauchySeq/str_leEq_seq_so_leEq_Lim.con" as lemma.
199 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_leEq_Lim.con" as lemma.
201 inline procedural "cic:/CoRN/reals/CauchySeq/seq_leEq_so_Lim_leEq.con" as lemma.
203 inline procedural "cic:/CoRN/reals/CauchySeq/str_seq_leEq_so_Lim_leEq.con" as lemma.
205 inline procedural "cic:/CoRN/reals/CauchySeq/Limits_unique.con" as lemma.
207 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd.con" as lemma.
209 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_strext.con" as lemma.
211 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap.con" as lemma.
213 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_ap_imp_seq_ap'.con" as lemma.
223 (*#* *** Equivalence of formulations of Cauchy *)
225 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop1_prop.con" as lemma.
227 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop2_prop.con" as lemma.
229 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop3_prop2.con" as lemma.
231 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop2.con" as lemma.
233 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop3_prop.con" as lemma.
235 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq1.con" as definition.
237 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop3.con" as lemma.
239 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop4_prop2.con" as lemma.
241 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop3.con" as lemma.
243 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop4_prop.con" as lemma.
245 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4.con" as definition.
247 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq4_y.con" as definition.
249 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq4.con" as lemma.
251 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2.con" as definition.
253 inline procedural "cic:/CoRN/reals/CauchySeq/Build_CauchySeq2_y.con" as definition.
255 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_CauchySeq2.con" as lemma.
257 (*#* Well definedness. *)
259 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_prop_wd.con" as lemma.
261 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_prop2_wd.con" as lemma.
263 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_wd'.con" as lemma.
265 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_unique.con" as lemma.
275 (*#* *** Properties of Cauchy sequences
277 Some of these lemmas are now obsolete, because they were reproved for arbitrary ordered fields$\ldots$#...#
279 We begin by defining the constant sequence and proving that it is Cauchy with the expected limit.
282 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_const.con" as definition.
284 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_const.con" as lemma.
286 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_plus.con" as lemma.
288 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_plus.con" as lemma.
290 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_plus.con" as lemma.
292 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_inv.con" as lemma.
294 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_inv.con" as lemma.
296 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_inv.con" as lemma.
298 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_minus.con" as lemma.
300 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_minus.con" as lemma.
302 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_minus.con" as lemma.
304 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_Lim_mult.con" as lemma.
306 inline procedural "cic:/CoRN/reals/CauchySeq/Cauchy_mult.con" as lemma.
308 inline procedural "cic:/CoRN/reals/CauchySeq/Lim_mult.con" as lemma.