Codebase list coq / lintian-fixes/main theories / Reals / Rcomplete.v
lintian-fixes/main

Tree @lintian-fixes/main (Download .tar.gz)

Rcomplete.v @lintian-fixes/main — raw · history · blame 

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import SeqProp.
Local Open Scope R_scope.

(****************************************************)
(*              R is complete :                     *)
(*        Each sequence which satisfies             *)
(*       the Cauchy's criterion converges           *)
(*                                                  *)
(*    Proof with adjacent sequences (Vn and Wn)     *)
(****************************************************)

Theorem R_complete :
  forall Un:nat -> R, Cauchy_crit Un -> { l:R | Un_cv Un l } .
Proof.
  intros.
  set (Vn := sequence_minorant Un (cauchy_min Un H)).
  set (Wn := sequence_majorant Un (cauchy_maj Un H)).
  pose proof (maj_cv Un H) as (x,p).
  fold Wn in p.
  pose proof (min_cv Un H) as (x0,p0).
  fold Vn in p0.
  cut (x = x0).
  intros H2.
  exists x.
  rewrite <- H2 in p0.
  unfold Un_cv.
  intros.
  unfold Un_cv in p; unfold Un_cv in p0.
  cut (0 < eps / 3).
  intro H4.
  elim (p (eps / 3) H4); intros.
  elim (p0 (eps / 3) H4); intros.
  exists (max x1 x2).
  intros.
  unfold R_dist.
  apply Rle_lt_trans with (Rabs (Un n - Vn n) + Rabs (Vn n - x)).
  replace (Un n - x) with (Un n - Vn n + (Vn n - x));
  [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with (Rabs (Wn n - Vn n) + Rabs (Vn n - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
  apply Rplus_le_compat_l.
  repeat rewrite Rabs_right.
  unfold Rminus; do 2 rewrite <- (Rplus_comm (- Vn n));
    apply Rplus_le_compat_l.
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  assumption.
  apply Rle_ge.
  unfold Rminus; apply Rplus_le_reg_l with (Vn n).
  rewrite Rplus_0_r.
  replace (Vn n + (Wn n + - Vn n)) with (Wn n); [ idtac | ring ].
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  apply Rle_trans with (Un n); assumption.
  apply Rle_ge.
  unfold Rminus; apply Rplus_le_reg_l with (Vn n).
  rewrite Rplus_0_r.
  replace (Vn n + (Un n + - Vn n)) with (Un n); [ idtac | ring ].
  assert (H8 := Vn_Un_Wn_order Un (cauchy_maj Un H) (cauchy_min Un H)).
  fold Vn Wn in H8.
  elim (H8 n); intros.
  assumption.
  apply Rle_lt_trans with (Rabs (Wn n - x) + Rabs (x - Vn n) + Rabs (Vn n - x)).
  do 2 rewrite <- (Rplus_comm (Rabs (Vn n - x))).
  apply Rplus_le_compat_l.
  replace (Wn n - Vn n) with (Wn n - x + (x - Vn n));
  [ apply Rabs_triang | ring ].
  apply Rlt_le_trans with (eps / 3 + eps / 3 + eps / 3).
  repeat apply Rplus_lt_compat.
  unfold R_dist in H1.
  apply H1.
  unfold ge; apply Nat.le_trans with (max x1 x2).
  apply Nat.le_max_l.
  assumption.
  rewrite <- Rabs_Ropp.
  replace (- (x - Vn n)) with (Vn n - x); [ idtac | ring ].
  unfold R_dist in H3.
  apply H3.
  unfold ge; apply Nat.le_trans with (max x1 x2).
  apply Nat.le_max_r.
  assumption.
  unfold R_dist in H3.
  apply H3.
  unfold ge; apply Nat.le_trans with (max x1 x2).
  apply Nat.le_max_r.
  assumption.
  right.
  pattern eps at 4; replace eps with (3 * (eps / 3)).
  ring.
  unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m; discrR.
  unfold Rdiv; apply Rmult_lt_0_compat;
    [ assumption | apply Rinv_0_lt_compat; prove_sup0 ].
  apply cond_eq.
  intros.
  cut (0 < eps / 5).
  intro.
  unfold Un_cv in p; unfold Un_cv in p0.
  unfold R_dist in p; unfold R_dist in p0.
  elim (p (eps / 5) H1); intros N1 H4.
  elim (p0 (eps / 5) H1); intros N2 H5.
  unfold Cauchy_crit in H.
  unfold R_dist in H.
  elim (H (eps / 5) H1); intros N3 H6.
  set (N := max (max N1 N2) N3).
  apply Rle_lt_trans with (Rabs (x - Wn N) + Rabs (Wn N - x0)).
  replace (x - x0) with (x - Wn N + (Wn N - x0)); [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with
    (Rabs (x - Wn N) + Rabs (Wn N - Vn N) + Rabs (Vn N - x0)).
  rewrite Rplus_assoc.
  apply Rplus_le_compat_l.
  replace (Wn N - x0) with (Wn N - Vn N + (Vn N - x0));
  [ apply Rabs_triang | ring ].
  replace eps with (eps / 5 + 3 * (eps / 5) + eps / 5).
  repeat apply Rplus_lt_compat.
  rewrite <- Rabs_Ropp.
  replace (- (x - Wn N)) with (Wn N - x); [ apply H4 | ring ].
  unfold ge, N.
  apply Nat.le_trans with (max N1 N2); apply Nat.le_max_l.
  unfold Wn, Vn.
  unfold sequence_majorant, sequence_minorant.
  assert
    (H7 :=
      approx_maj (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
  assert
    (H8 :=
      approx_min (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
  cut
    (Wn N =
      majorant (fun k:nat => Un (N + k)%nat) (maj_ss Un N (cauchy_maj Un H))).
  cut
    (Vn N =
      minorant (fun k:nat => Un (N + k)%nat) (min_ss Un N (cauchy_min Un H))).
  intros H9 H10.
  rewrite <- H9 in H8 |- *.
  rewrite <- H10 in H7 |- *.
  elim (H7 (eps / 5) H1); intros k2 H11.
  elim (H8 (eps / 5) H1); intros k1 H12.
  apply Rle_lt_trans with
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Vn N)).
  replace (Wn N - Vn N) with
  (Wn N - Un (N + k2)%nat + (Un (N + k2)%nat - Vn N));
  [ apply Rabs_triang | ring ].
  apply Rle_lt_trans with
    (Rabs (Wn N - Un (N + k2)%nat) + Rabs (Un (N + k2)%nat - Un (N + k1)%nat) +
      Rabs (Un (N + k1)%nat - Vn N)).
  rewrite Rplus_assoc.
  apply Rplus_le_compat_l.
  replace (Un (N + k2)%nat - Vn N) with
  (Un (N + k2)%nat - Un (N + k1)%nat + (Un (N + k1)%nat - Vn N));
  [ apply Rabs_triang | ring ].
  replace (3 * (eps / 5)) with (eps / 5 + eps / 5 + eps / 5);
  [ repeat apply Rplus_lt_compat | ring ].
  assumption.
  apply H6.
  unfold ge.
  apply Nat.le_trans with N.
  unfold N; apply Nat.le_max_r.
  apply Nat.le_add_r.
  unfold ge.
  apply Nat.le_trans with N.
  unfold N; apply Nat.le_max_r.
  apply Nat.le_add_r.
  rewrite <- Rabs_Ropp.
  replace (- (Un (N + k1)%nat - Vn N)) with (Vn N - Un (N + k1)%nat);
  [ assumption | ring ].
  reflexivity.
  reflexivity.
  apply H5.
  unfold ge; apply Nat.le_trans with (max N1 N2).
  apply Nat.le_max_r.
  unfold N; apply Nat.le_max_l.
  pattern eps at 4; replace eps with (5 * (eps / 5)).
  ring.
  unfold Rdiv; rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
  discrR.
  unfold Rdiv; apply Rmult_lt_0_compat.
  assumption.
  apply Rinv_0_lt_compat.
  prove_sup0.
Qed.

(* TODO #14736 for compatibility only, should be removed after deprecation *)
Require Import Max.