← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to theories/Reals/Rcomplete.v

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
theories/Reals/Rcomplete.v
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
4
(*   \VV/  **************************************************************)
 
5
(*    //   *      This file is distributed under the terms of the       *)
 
6
(*         *       GNU Lesser General Public License Version 2.1        *)
 
7
(************************************************************************)
 
8
 
 
9
(*i $Id: Rcomplete.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
Require Import Rbase.
 
12
Require Import Rfunctions.
 
13
Require Import Rseries.
 
14
Require Import SeqProp.
 
15
Require Import Max.
 
16
Open Local Scope R_scope.
 
17
 
 
18
(****************************************************)
 
19
(*              R is complete :                     *)
 
20
(*        Each sequence which satisfies             *)
 
21
(*       the Cauchy's criterion converges           *)
 
22
(*                                                  *)
 
23
(*    Proof with adjacent sequences (Vn and Wn)     *)
 
24
(****************************************************)
 
25
 
 
26
Theorem R_complete :
 
27
  forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
 
28
Proof.
 
29
  intros.
 
30
  set (Vn := sequence_minorant Un (cauchy_min Un H)).
 
31
  set (Wn := sequence_majorant Un (cauchy_maj Un H)).
 
32
  assert (H0 := maj_cv Un H).
 
33
  fold Wn in H0.
 
34
  assert (H1 := min_cv Un H).
 
35
  fold Vn in H1.
 
36
  elim H0; intros.
 
37
  elim H1; intros.
 
38
  cut (x = x0).
 
39
  intros.
 
40
  exists x.
 
41
  rewrite <- H2 in p0.
 
42
  unfold Un_cv in |- *.
 
43
  intros.
 
44
  unfold Un_cv in p; unfold Un_cv in p0.
 
45
  cut (0 < eps / 3).
 
46
  intro.
 
47
  elim (p (eps / 3) H4); intros.
 
48
  elim (p0 (eps / 3) H4); intros.
 
49
  exists (max x1 x2).
 
50
  intros.
 
51
  unfold R_dist in |- *.
 
52
  apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)).
 
53
  replace (Un n - x) with (Un n - Vn n + (Vn n - x));
 
54
  [ apply Rabs_triang | ring ].
 
55
  apply Rle_lt_trans with (Rabs (Wn n - Vn n) + Rabs (Vn n - x)).
 
56
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
 
57
  apply Rplus_le_compat_l.
 
58
  repeat rewrite Rabs_right.
 
59
  unfold Rminus in |- *; do 2 rewrite <- (Rplus_comm (- Vn n));
 
60
    apply Rplus_le_compat_l.
 
61
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
 
62
  fold Vn Wn in H8.
 
63
  elim (H8 n); intros.
 
64
  assumption.
 
65
  apply Rle_ge.
 
66
  unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n).
 
67
  rewrite Rplus_0_r.
 
68
  replace (Vn n + (Wn n + - Vn n)) with (Wn n); [ idtac | ring ].
 
69
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
 
70
  fold Vn Wn in H8.
 
71
  elim (H8 n); intros.
 
72
  apply Rle_trans with (Un n); assumption.
 
73
  apply Rle_ge.
 
74
  unfold Rminus in |- *; apply Rplus_le_reg_l with (Vn n).
 
75
  rewrite Rplus_0_r.
 
76
  replace (Vn n + (Un n + - Vn n)) with (Un n); [ idtac | ring ].
 
77
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
 
78
  fold Vn Wn in H8.
 
79
  elim (H8 n); intros.
 
80
  assumption.
 
81
  apply Rle_lt_trans with (Rabs (Wn n - x) + Rabs (x - Vn n) + Rabs (Vn n - x)).
 
82
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
 
83
  apply Rplus_le_compat_l.
 
84
  replace (Wn n - Vn n) with (Wn n - x + (x - Vn n));
 
85
  [ apply Rabs_triang | ring ].
 
86
  apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3).
 
87
  repeat apply Rplus_lt_compat.
 
88
  unfold R_dist in H5.
 
89
  apply H5.
 
90
  unfold ge in |- *; apply le_trans with (max x1 x2).
 
91
  apply le_max_l.
 
92
  assumption.
 
93
  rewrite <- Rabs_Ropp.
 
94
  replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ].
 
95
  unfold R_dist in H6.
 
96
  apply H6.
 
97
  unfold ge in |- *; apply le_trans with (max x1 x2).
 
98
  apply le_max_r.
 
99
  assumption.
 
100
  unfold R_dist in H6.
 
101
  apply H6.
 
102
  unfold ge in |- *; apply le_trans with (max x1 x2).
 
103
  apply le_max_r.
 
104
  assumption.
 
105
  right.
 
106
  pattern eps at 4 in |- *; replace eps with (3 * (eps / 3)).
 
107
  ring.
 
108
  unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR.
 
109
  unfold Rdiv in |- *; apply Rmult_lt_0_compat;
 
110
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
 
111
  apply cond_eq.
 
112
  intros.
 
113
  cut (0 < eps / 5).
 
114
  intro.
 
115
  unfold Un_cv in p; unfold Un_cv in p0.
 
116
  unfold R_dist in p; unfold R_dist in p0.
 
117
  elim (p (eps / 5) H3); intros N1 H4.
 
118
  elim (p0 (eps / 5) H3); intros N2 H5.
 
119
  unfold Cauchy_crit in H.
 
120
  unfold R_dist in H.
 
121
  elim (H (eps / 5) H3); intros N3 H6.
 
122
  set (N := max (max N1 N2) N3).
 
123
  apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
 
124
  replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
 
125
  apply Rle_lt_trans with
 
126
    (Rabs (x - Wn N) + Rabs (Wn N - Vn N) + Rabs (Vn N - x0)).
 
127
  rewrite Rplus_assoc.
 
128
  apply Rplus_le_compat_l.
 
129
  replace (Wn N - x0) with (Wn N - Vn N + (Vn N - x0));
 
130
  [ apply Rabs_triang | ring ].
 
131
  replace eps with (eps / 5 + 3 * (eps / 5) + eps / 5).
 
132
  repeat apply Rplus_lt_compat.
 
133
  rewrite <- Rabs_Ropp.
 
134
  replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ].
 
135
  unfold ge, N in |- *.
 
136
  apply le_trans with (max N1 N2); apply le_max_l.
 
137
  unfold Wn, Vn in |- *.
 
138
  unfold sequence_majorant, sequence_minorant in |- *.
 
139
  assert
 
140
    (H7 :=
 
141
      approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
 
142
  assert
 
143
    (H8 :=
 
144
      approx_min (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
 
145
  cut
 
146
    (Wn N =
 
147
      majorant (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
 
148
  cut
 
149
    (Vn N =
 
150
      minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
 
151
  intros.
 
152
  rewrite <- H9; rewrite <- H10.
 
153
  rewrite <- H9 in H8.
 
154
  rewrite <- H10 in H7.
 
155
  elim (H7 (eps / 5) H3); intros k2 H11.
 
156
  elim (H8 (eps / 5) H3); intros k1 H12.
 
157
  apply Rle_lt_trans with
 
158
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)).
 
159
  replace (Wn N - Vn N) with
 
160
  (Wn N - Un (N + k2)%nat + (Un (N + k2)%nat - Vn N));
 
161
  [ apply Rabs_triang | ring ].
 
162
  apply Rle_lt_trans with
 
163
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Un (N + k1)%nat) +
 
164
      Rabs (Un (N + k1)%nat - Vn N)).
 
165
  rewrite Rplus_assoc.
 
166
  apply Rplus_le_compat_l.
 
167
  replace (Un (N + k2)%nat - Vn N) with
 
168
  (Un (N + k2)%nat - Un (N + k1)%nat + (Un (N + k1)%nat - Vn N));
 
169
  [ apply Rabs_triang | ring ].
 
170
  replace (3 * (eps / 5)) with (eps / 5 + eps / 5 + eps / 5);
 
171
  [ repeat apply Rplus_lt_compat | ring ].
 
172
  assumption.
 
173
  apply H6.
 
174
  unfold ge in |- *.
 
175
  apply le_trans with N.
 
176
  unfold N in |- *; apply le_max_r.
 
177
  apply le_plus_l.
 
178
  unfold ge in |- *.
 
179
  apply le_trans with N.
 
180
  unfold N in |- *; apply le_max_r.
 
181
  apply le_plus_l.
 
182
  rewrite <- Rabs_Ropp.
 
183
  replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat);
 
184
  [ assumption | ring ].
 
185
  reflexivity.
 
186
  reflexivity.
 
187
  apply H5.
 
188
  unfold ge in |- *; apply le_trans with (max N1 N2).
 
189
  apply le_max_r.
 
190
  unfold N in |- *; apply le_max_l.
 
191
  pattern eps at 4 in |- *; replace eps with (5 * (eps / 5)).
 
192
  ring.
 
193
  unfold Rdiv in |- *; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
 
194
  discrR.
 
195
  unfold Rdiv in |- *; apply Rmult_lt_0_compat.
 
196
  assumption.
 
197
  apply Rinv_0_lt_compat.
 
198
  prove_sup0; try apply lt_O_Sn.
 
199
Qed.