← Back to branch summary

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

« back to all changes in this revision

Viewing changes to theories/Reals/Rbasic_fun.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/Rbasic_fun.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: Rbasic_fun.v 10710 2008-03-23 09:24:09Z herbelin $ i*)
 
10
 
 
11
(*********************************************************)
 
12
(**          Complements for the real numbers            *)
 
13
(*                                                       *)
 
14
(*********************************************************)
 
15
 
 
16
Require Import Rbase.
 
17
Require Import R_Ifp.
 
18
Require Import Fourier.
 
19
Open Local Scope R_scope.
 
20
 
 
21
Implicit Type r : R.
 
22
 
 
23
(*******************************)
 
24
(** *        Rmin              *)
 
25
(*******************************)
 
26
 
 
27
(*********)
 
28
Definition Rmin (x y:R) : R :=
 
29
  match Rle_dec x y with
 
30
    | left _ => x
 
31
    | right _ => y
 
32
  end.
 
33
 
 
34
(*********)
 
35
Lemma Rmin_Rgt_l : forall r1 r2 r, Rmin r1 r2 > r -> r1 > r /\ r2 > r.
 
36
Proof.
 
37
  intros r1 r2 r; unfold Rmin in |- *; case (Rle_dec r1 r2); intros.
 
38
  split.
 
39
  assumption.
 
40
  unfold Rgt in |- *; unfold Rgt in H; exact (Rlt_le_trans r r1 r2 H r0).
 
41
  split.
 
42
  generalize (Rnot_le_lt r1 r2 n); intro; exact (Rgt_trans r1 r2 r H0 H).
 
43
  assumption.
 
44
Qed.
 
45
 
 
46
(*********)
 
47
Lemma Rmin_Rgt_r : forall r1 r2 r, r1 > r /\ r2 > r -> Rmin r1 r2 > r.
 
48
Proof.
 
49
  intros; unfold Rmin in |- *; case (Rle_dec r1 r2); elim H; clear H; intros;
 
50
    assumption.
 
51
Qed.
 
52
 
 
53
(*********)
 
54
Lemma Rmin_Rgt : forall r1 r2 r, Rmin r1 r2 > r <-> r1 > r /\ r2 > r.
 
55
Proof.
 
56
  intros; split.
 
57
  exact (Rmin_Rgt_l r1 r2 r).
 
58
  exact (Rmin_Rgt_r r1 r2 r).
 
59
Qed.
 
60
 
 
61
(*********)
 
62
Lemma Rmin_l : forall x y:R, Rmin x y <= x.
 
63
Proof.
 
64
  intros; unfold Rmin in |- *; case (Rle_dec x y); intro H1;
 
65
    [ right; reflexivity | auto with real ].
 
66
Qed.
 
67
 
 
68
(*********)
 
69
Lemma Rmin_r : forall x y:R, Rmin x y <= y.
 
70
Proof.
 
71
  intros; unfold Rmin in |- *; case (Rle_dec x y); intro H1;
 
72
    [ assumption | auto with real ].
 
73
Qed.
 
74
 
 
75
(*********)
 
76
Lemma Rmin_comm : forall a b:R, Rmin a b = Rmin b a.
 
77
Proof.
 
78
  intros; unfold Rmin in |- *; case (Rle_dec a b); case (Rle_dec b a); intros;
 
79
    try reflexivity || (apply Rle_antisym; assumption || auto with real).
 
80
Qed.
 
81
 
 
82
(*********)
 
83
Lemma Rmin_stable_in_posreal : forall x y:posreal, 0 < Rmin x y.
 
84
Proof.
 
85
  intros; apply Rmin_Rgt_r; split; [ apply (cond_pos x) | apply (cond_pos y) ].
 
86
Qed.
 
87
 
 
88
(*******************************)
 
89
(** *        Rmax              *)
 
90
(*******************************)
 
91
 
 
92
(*********)
 
93
Definition Rmax (x y:R) : R :=
 
94
  match Rle_dec x y with
 
95
    | left _ => y
 
96
    | right _ => x
 
97
  end.
 
98
 
 
99
(*********)
 
100
Lemma Rmax_Rle : forall r1 r2 r, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2.
 
101
Proof.
 
102
  intros; split.
 
103
  unfold Rmax in |- *; case (Rle_dec r1 r2); intros; auto.
 
104
  intro; unfold Rmax in |- *; case (Rle_dec r1 r2); elim H; clear H; intros;
 
105
    auto.
 
106
  apply (Rle_trans r r1 r2); auto.
 
107
  generalize (Rnot_le_lt r1 r2 n); clear n; intro; unfold Rgt in H0;
 
108
    apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)).
 
109
Qed.
 
110
 
 
111
Lemma RmaxLess1 : forall r1 r2, r1 <= Rmax r1 r2.
 
112
Proof.
 
113
  intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real.
 
114
Qed.
 
115
 
 
116
Lemma RmaxLess2 : forall r1 r2, r2 <= Rmax r1 r2.
 
117
Proof.
 
118
  intros r1 r2; unfold Rmax in |- *; case (Rle_dec r1 r2); auto with real.
 
119
Qed.
 
120
 
 
121
Lemma Rmax_comm : forall p q:R, Rmax p q = Rmax q p.
 
122
Proof.
 
123
  intros p q; unfold Rmax in |- *; case (Rle_dec p q); case (Rle_dec q p); auto;
 
124
    intros H1 H2; apply Rle_antisym; auto with real.
 
125
Qed.
 
126
 
 
127
Notation RmaxSym := Rmax_comm (only parsing).
 
128
 
 
129
Lemma RmaxRmult :
 
130
  forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q.
 
131
Proof.
 
132
  intros p q r H; unfold Rmax in |- *.
 
133
  case (Rle_dec p q); case (Rle_dec (r * p) (r * q)); auto; intros H1 H2; auto.
 
134
  case H; intros E1.
 
135
  case H1; auto with real.
 
136
  rewrite <- E1; repeat rewrite Rmult_0_l; auto.
 
137
  case H; intros E1.
 
138
  case H2; auto with real.
 
139
  apply Rmult_le_reg_l with (r := r); auto.
 
140
  rewrite <- E1; repeat rewrite Rmult_0_l; auto.
 
141
Qed.
 
142
 
 
143
Lemma Rmax_stable_in_negreal : forall x y:negreal, Rmax x y < 0.
 
144
Proof.
 
145
  intros; unfold Rmax in |- *; case (Rle_dec x y); intro;
 
146
    [ apply (cond_neg y) | apply (cond_neg x) ].
 
147
Qed.
 
148
 
 
149
(*******************************)
 
150
(** *        Rabsolu           *)
 
151
(*******************************)
 
152
 
 
153
(*********)
 
154
Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}. 
 
155
Proof.
 
156
  intro; generalize (Rle_dec 0 r); intro X; elim X; intro; clear X.
 
157
  right; apply (Rle_ge 0 r a).
 
158
  left; fold (0 > r) in |- *; apply (Rnot_le_lt 0 r b).
 
159
Qed.
 
160
 
 
161
(*********)
 
162
Definition Rabs r : R :=
 
163
  match Rcase_abs r with
 
164
    | left _ => - r
 
165
    | right _ => r
 
166
  end.
 
167
 
 
168
(*********)
 
169
Lemma Rabs_R0 : Rabs 0 = 0.
 
170
Proof.
 
171
  unfold Rabs in |- *; case (Rcase_abs 0); auto; intro.
 
172
  generalize (Rlt_irrefl 0); intro; elimtype False; auto.
 
173
Qed.
 
174
 
 
175
Lemma Rabs_R1 : Rabs 1 = 1.
 
176
Proof.
 
177
unfold Rabs in |- *; case (Rcase_abs 1); auto with real.
 
178
intros H; absurd (1 < 0); auto with real.
 
179
Qed.
 
180
 
 
181
(*********)
 
182
Lemma Rabs_no_R0 : forall r, r <> 0 -> Rabs r <> 0.
 
183
Proof.
 
184
  intros; unfold Rabs in |- *; case (Rcase_abs r); intro; auto.
 
185
  apply Ropp_neq_0_compat; auto.
 
186
Qed.
 
187
 
 
188
(*********)
 
189
Lemma Rabs_left : forall r, r < 0 -> Rabs r = - r.
 
190
Proof.
 
191
  intros; unfold Rabs in |- *; case (Rcase_abs r); trivial; intro;
 
192
    absurd (r >= 0).
 
193
  exact (Rlt_not_ge r 0 H).
 
194
  assumption.
 
195
Qed.
 
196
 
 
197
(*********)
 
198
Lemma Rabs_right : forall r, r >= 0 -> Rabs r = r.
 
199
Proof.
 
200
  intros; unfold Rabs in |- *; case (Rcase_abs r); intro.
 
201
  absurd (r >= 0).
 
202
  exact (Rlt_not_ge r 0 r0).
 
203
  assumption.
 
204
  trivial.
 
205
Qed.
 
206
 
 
207
Lemma Rabs_left1 : forall a:R, a <= 0 -> Rabs a = - a.
 
208
Proof.
 
209
  intros a H; case H; intros H1.
 
210
  apply Rabs_left; auto.
 
211
  rewrite H1; simpl in |- *; rewrite Rabs_right; auto with real.
 
212
Qed.
 
213
 
 
214
(*********)
 
215
Lemma Rabs_pos : forall x:R, 0 <= Rabs x.
 
216
Proof.
 
217
  intros; unfold Rabs in |- *; case (Rcase_abs x); intro.
 
218
  generalize (Ropp_lt_gt_contravar x 0 r); intro; unfold Rgt in H;
 
219
    rewrite Ropp_0 in H; unfold Rle in |- *; left; assumption.
 
220
  apply Rge_le; assumption.
 
221
Qed.
 
222
 
 
223
Lemma RRle_abs : forall x:R, x <= Rabs x.
 
224
Proof.
 
225
  intro; unfold Rabs in |- *; case (Rcase_abs x); intros; fourier.
 
226
Qed.
 
227
 
 
228
(*********)
 
229
Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
 
230
Proof.
 
231
  intros; unfold Rabs in |- *; case (Rcase_abs x); intro;
 
232
    [ generalize (Rgt_not_le 0 x r); intro; elimtype False; auto | trivial ].
 
233
Qed.
 
234
 
 
235
(*********)
 
236
Lemma Rabs_Rabsolu : forall x:R, Rabs (Rabs x) = Rabs x.
 
237
Proof.
 
238
  intro; apply (Rabs_pos_eq (Rabs x) (Rabs_pos x)).
 
239
Qed.
 
240
 
 
241
(*********)
 
242
Lemma Rabs_pos_lt : forall x:R, x <> 0 -> 0 < Rabs x.
 
243
Proof.
 
244
  intros; generalize (Rabs_pos x); intro; unfold Rle in H0; elim H0; intro;
 
245
    auto.
 
246
  elimtype False; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
 
247
    case (Rcase_abs x); intros; auto.
 
248
  clear r H1; generalize (Rplus_eq_compat_l x 0 (- x) H0);
 
249
    rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x); 
 
250
      trivial.
 
251
Qed.
 
252
 
 
253
(*********)
 
254
Lemma Rabs_minus_sym : forall x y:R, Rabs (x - y) = Rabs (y - x).
 
255
Proof.
 
256
  intros; unfold Rabs in |- *; case (Rcase_abs (x - y));
 
257
    case (Rcase_abs (y - x)); intros.
 
258
  generalize (Rminus_lt y x r); generalize (Rminus_lt x y r0); intros;
 
259
    generalize (Rlt_asym x y H); intro; elimtype False; 
 
260
      auto.
 
261
  rewrite (Ropp_minus_distr x y); trivial.
 
262
  rewrite (Ropp_minus_distr y x); trivial.
 
263
  unfold Rge in r, r0; elim r; elim r0; intros; clear r r0.
 
264
  generalize (Ropp_lt_gt_0_contravar (x - y) H); rewrite (Ropp_minus_distr x y);
 
265
    intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0); 
 
266
      intro; elimtype False; auto.
 
267
  rewrite (Rminus_diag_uniq x y H); trivial.
 
268
  rewrite (Rminus_diag_uniq y x H0); trivial.
 
269
  rewrite (Rminus_diag_uniq y x H0); trivial.
 
270
Qed.
 
271
 
 
272
(*********)
 
273
Lemma Rabs_mult : forall x y:R, Rabs (x * y) = Rabs x * Rabs y.
 
274
Proof.
 
275
  intros; unfold Rabs in |- *; case (Rcase_abs (x * y)); case (Rcase_abs x);
 
276
    case (Rcase_abs y); intros; auto.
 
277
  generalize (Rmult_lt_gt_compat_neg_l y x 0 r r0); intro;
 
278
    rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1); 
 
279
      intro; unfold Rgt in H; elimtype False; rewrite (Rmult_comm y x) in H; 
 
280
        auto.
 
281
  rewrite (Ropp_mult_distr_l_reverse x y); trivial. 
 
282
  rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x);
 
283
    rewrite (Rmult_comm x y); trivial.
 
284
  unfold Rge in r, r0; elim r; elim r0; clear r r0; intros; unfold Rgt in H, H0.
 
285
  generalize (Rmult_lt_compat_l x 0 y H H0); intro; rewrite (Rmult_0_r x) in H1;
 
286
    generalize (Rlt_asym (x * y) 0 r1); intro; elimtype False; 
 
287
      auto.
 
288
  rewrite H in r1; rewrite (Rmult_0_l y) in r1; generalize (Rlt_irrefl 0);
 
289
    intro; elimtype False; auto.
 
290
  rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
 
291
    intro; elimtype False; auto.
 
292
  rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0);
 
293
    intro; elimtype False; auto.
 
294
  rewrite (Rmult_opp_opp x y); trivial.
 
295
  unfold Rge in r, r1; elim r; elim r1; clear r r1; intros; unfold Rgt in H0, H.
 
296
  generalize (Rmult_lt_compat_l y x 0 H0 r0); intro;
 
297
    rewrite (Rmult_0_r y) in H1; rewrite (Rmult_comm y x) in H1;
 
298
      generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False; 
 
299
        auto.
 
300
  generalize (Rlt_dichotomy_converse x 0 (or_introl (x > 0) r0));
 
301
    generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0)); 
 
302
      intros; generalize (Rmult_integral x y H); intro; 
 
303
        elim H3; intro; elimtype False; auto.  
 
304
  rewrite H0 in H; rewrite (Rmult_0_r x) in H; unfold Rgt in H;
 
305
    generalize (Rlt_irrefl 0); intro; elimtype False; 
 
306
      auto.
 
307
  rewrite H0; rewrite (Rmult_0_r x); rewrite (Rmult_0_r (- x)); trivial.
 
308
  unfold Rge in r0, r1; elim r0; elim r1; clear r0 r1; intros;
 
309
    unfold Rgt in H0, H.
 
310
  generalize (Rmult_lt_compat_l x y 0 H0 r); intro; rewrite (Rmult_0_r x) in H1;
 
311
    generalize (Rlt_asym (x * y) 0 H1); intro; elimtype False; 
 
312
      auto.
 
313
  generalize (Rlt_dichotomy_converse y 0 (or_introl (y > 0) r));
 
314
    generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0)); 
 
315
      intros; generalize (Rmult_integral x y H); intro; 
 
316
        elim H3; intro; elimtype False; auto.  
 
317
  rewrite H0 in H; rewrite (Rmult_0_l y) in H; unfold Rgt in H;
 
318
    generalize (Rlt_irrefl 0); intro; elimtype False; 
 
319
      auto.
 
320
  rewrite H0; rewrite (Rmult_0_l y); rewrite (Rmult_0_l (- y)); trivial.
 
321
Qed.
 
322
 
 
323
(*********)
 
324
Lemma Rabs_Rinv : forall r, r <> 0 -> Rabs (/ r) = / Rabs r.
 
325
Proof.
 
326
  intro; unfold Rabs in |- *; case (Rcase_abs r); case (Rcase_abs (/ r)); auto;
 
327
    intros.
 
328
  apply Ropp_inv_permute; auto.
 
329
  generalize (Rinv_lt_0_compat r r1); intro; unfold Rge in r0; elim r0; intros.
 
330
  unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; elimtype False;
 
331
    auto.
 
332
  generalize (Rlt_dichotomy_converse (/ r) 0 (or_introl (/ r > 0) H0)); intro;
 
333
    elimtype False; auto.
 
334
  unfold Rge in r1; elim r1; clear r1; intro.
 
335
  unfold Rgt in H0; generalize (Rlt_asym 0 (/ r) (Rinv_0_lt_compat r H0));
 
336
    intro; elimtype False; auto.
 
337
  elimtype False; auto.
 
338
Qed. 
 
339
 
 
340
Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
 
341
Proof.
 
342
  intro; cut (- x = -1 * x).
 
343
  intros; rewrite H.
 
344
  rewrite Rabs_mult.
 
345
  cut (Rabs (-1) = 1).
 
346
  intros; rewrite H0.
 
347
  ring.
 
348
  unfold Rabs in |- *; case (Rcase_abs (-1)).
 
349
  intro; ring.
 
350
  intro H0; generalize (Rge_le (-1) 0 H0); intros.
 
351
  generalize (Ropp_le_ge_contravar 0 (-1) H1).
 
352
  rewrite Ropp_involutive; rewrite Ropp_0.
 
353
  intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
 
354
    intro; elimtype False; auto.  
 
355
  ring.
 
356
Qed.
 
357
 
 
358
(*********)
 
359
Lemma Rabs_triang : forall a b:R, Rabs (a + b) <= Rabs a + Rabs b.
 
360
Proof.
 
361
  intros a b; unfold Rabs in |- *; case (Rcase_abs (a + b)); case (Rcase_abs a);
 
362
    case (Rcase_abs b); intros.
 
363
  apply (Req_le (- (a + b)) (- a + - b)); rewrite (Ropp_plus_distr a b);
 
364
    reflexivity.
 
365
(**)
 
366
  rewrite (Ropp_plus_distr a b); apply (Rplus_le_compat_l (- a) (- b) b);
 
367
    unfold Rle in |- *; unfold Rge in r; elim r; intro.
 
368
  left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- b) 0 b H); intro;
 
369
    elim (Rplus_ne (- b)); intros v w; rewrite v in H0; 
 
370
      clear v w; rewrite (Rplus_opp_l b) in H0; apply (Rlt_trans (- b) 0 b H0 H).
 
371
  right; rewrite H; apply Ropp_0.
 
372
(**)
 
373
  rewrite (Ropp_plus_distr a b); rewrite (Rplus_comm (- a) (- b));
 
374
    rewrite (Rplus_comm a (- b)); apply (Rplus_le_compat_l (- b) (- a) a);
 
375
      unfold Rle in |- *; unfold Rge in r0; elim r0; intro.
 
376
  left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- a) 0 a H); intro;
 
377
    elim (Rplus_ne (- a)); intros v w; rewrite v in H0; 
 
378
      clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H).
 
379
  right; rewrite H; apply Ropp_0.
 
380
(**)
 
381
  elimtype False; generalize (Rplus_ge_compat_l a b 0 r); intro;
 
382
    elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
 
383
      generalize (Rge_trans (a + b) a 0 H r0); intro; clear H; 
 
384
        unfold Rge in H0; elim H0; intro; clear H0.
 
385
  unfold Rgt in H; generalize (Rlt_asym (a + b) 0 r1); intro; auto.
 
386
  absurd (a + b = 0); auto.
 
387
  apply (Rlt_dichotomy_converse (a + b) 0); left; assumption.
 
388
(**)
 
389
  elimtype False; generalize (Rplus_lt_compat_l a b 0 r); intro;
 
390
    elim (Rplus_ne a); intros v w; rewrite v in H; clear v w;
 
391
      generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H; 
 
392
        unfold Rge in r1; elim r1; clear r1; intro.
 
393
  unfold Rgt in H; generalize (Rlt_trans (a + b) 0 (a + b) H0 H); intro;
 
394
    apply (Rlt_irrefl (a + b)); assumption.
 
395
  rewrite H in H0; apply (Rlt_irrefl 0); assumption.
 
396
(**)
 
397
  rewrite (Rplus_comm a b); rewrite (Rplus_comm (- a) b);
 
398
    apply (Rplus_le_compat_l b a (- a)); apply (Rminus_le a (- a));
 
399
      unfold Rminus in |- *; rewrite (Ropp_involutive a);
 
400
        generalize (Rplus_lt_compat_l a a 0 r0); clear r r1; 
 
401
          intro; elim (Rplus_ne a); intros v w; rewrite v in H; 
 
402
            clear v w; generalize (Rlt_trans (a + a) a 0 H r0); 
 
403
              intro; apply (Rlt_le (a + a) 0 H0).
 
404
(**)
 
405
  apply (Rplus_le_compat_l a b (- b)); apply (Rminus_le b (- b));
 
406
    unfold Rminus in |- *; rewrite (Ropp_involutive b);
 
407
      generalize (Rplus_lt_compat_l b b 0 r); clear r0 r1; 
 
408
        intro; elim (Rplus_ne b); intros v w; rewrite v in H; 
 
409
          clear v w; generalize (Rlt_trans (b + b) b 0 H r); 
 
410
            intro; apply (Rlt_le (b + b) 0 H0).
 
411
(**)
 
412
  unfold Rle in |- *; right; reflexivity.
 
413
Qed.
 
414
 
 
415
(*********)
 
416
Lemma Rabs_triang_inv : forall a b:R, Rabs a - Rabs b <= Rabs (a - b).
 
417
Proof.
 
418
  intros; apply (Rplus_le_reg_l (Rabs b) (Rabs a - Rabs b) (Rabs (a - b)));
 
419
    unfold Rminus in |- *; rewrite <- (Rplus_assoc (Rabs b) (Rabs a) (- Rabs b));
 
420
      rewrite (Rplus_comm (Rabs b) (Rabs a));
 
421
        rewrite (Rplus_assoc (Rabs a) (Rabs b) (- Rabs b));
 
422
          rewrite (Rplus_opp_r (Rabs b)); rewrite (proj1 (Rplus_ne (Rabs a)));
 
423
            replace (Rabs a) with (Rabs (a + 0)).
 
424
  rewrite <- (Rplus_opp_r b); rewrite <- (Rplus_assoc a b (- b));
 
425
    rewrite (Rplus_comm a b); rewrite (Rplus_assoc b a (- b)).
 
426
  exact (Rabs_triang b (a + - b)).
 
427
  rewrite (proj1 (Rplus_ne a)); trivial.
 
428
Qed.
 
429
 
 
430
(* ||a|-|b||<=|a-b| *)
 
431
Lemma Rabs_triang_inv2 : forall a b:R, Rabs (Rabs a - Rabs b) <= Rabs (a - b). 
 
432
Proof.
 
433
  cut
 
434
    (forall a b:R, Rabs b <= Rabs a -> Rabs (Rabs a - Rabs b) <= Rabs (a - b)). 
 
435
  intros; destruct (Rtotal_order (Rabs a) (Rabs b)) as [Hlt| [Heq| Hgt]].
 
436
  rewrite <- (Rabs_Ropp (Rabs a - Rabs b)); rewrite <- (Rabs_Ropp (a - b));
 
437
    do 2 rewrite Ropp_minus_distr. 
 
438
  apply H; left; assumption. 
 
439
  rewrite Heq; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
 
440
    apply Rabs_pos. 
 
441
  apply H; left; assumption. 
 
442
  intros; replace (Rabs (Rabs a - Rabs b)) with (Rabs a - Rabs b). 
 
443
  apply Rabs_triang_inv. 
 
444
  rewrite (Rabs_right (Rabs a - Rabs b));
 
445
    [ reflexivity
 
446
      | apply Rle_ge; apply Rplus_le_reg_l with (Rabs b); rewrite Rplus_0_r;
 
447
        replace (Rabs b + (Rabs a - Rabs b)) with (Rabs a); 
 
448
        [ assumption | ring ] ]. 
 
449
Qed. 
 
450
 
 
451
(*********)
 
452
Lemma Rabs_def1 : forall x a:R, x < a -> - a < x -> Rabs x < a.
 
453
Proof.
 
454
  unfold Rabs in |- *; intros; case (Rcase_abs x); intro.
 
455
  generalize (Ropp_lt_gt_contravar (- a) x H0); unfold Rgt in |- *;
 
456
    rewrite Ropp_involutive; intro; assumption.
 
457
  assumption.
 
458
Qed.
 
459
 
 
460
(*********)
 
461
Lemma Rabs_def2 : forall x a:R, Rabs x < a -> x < a /\ - a < x.
 
462
Proof.
 
463
  unfold Rabs in |- *; intro x; case (Rcase_abs x); intros.
 
464
  generalize (Ropp_gt_lt_0_contravar x r); unfold Rgt in |- *; intro;
 
465
    generalize (Rlt_trans 0 (- x) a H0 H); intro; split. 
 
466
  apply (Rlt_trans x 0 a r H1).
 
467
  generalize (Ropp_lt_gt_contravar (- x) a H); rewrite (Ropp_involutive x);
 
468
    unfold Rgt in |- *; trivial.
 
469
  fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H r); intro;
 
470
    generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a) in |- *;
 
471
      generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt in |- *; 
 
472
        intro; split; assumption.
 
473
Qed.
 
474
 
 
475
Lemma RmaxAbs :
 
476
  forall (p q:R) r, p <= q -> q <= r -> Rabs q <= Rmax (Rabs p) (Rabs r).
 
477
Proof.
 
478
  intros p q r H' H'0; case (Rle_or_lt 0 p); intros H'1.
 
479
  repeat rewrite Rabs_right; auto with real.
 
480
  apply Rle_trans with r; auto with real.
 
481
  apply RmaxLess2; auto.
 
482
  apply Rge_trans with p; auto with real; apply Rge_trans with q;
 
483
    auto with real.
 
484
  apply Rge_trans with p; auto with real.
 
485
  rewrite (Rabs_left p); auto.
 
486
  case (Rle_or_lt 0 q); intros H'2.
 
487
  repeat rewrite Rabs_right; auto with real.
 
488
  apply Rle_trans with r; auto.
 
489
  apply RmaxLess2; auto.
 
490
  apply Rge_trans with q; auto with real.
 
491
  rewrite (Rabs_left q); auto.
 
492
  case (Rle_or_lt 0 r); intros H'3.
 
493
  repeat rewrite Rabs_right; auto with real.
 
494
  apply Rle_trans with (- p); auto with real.
 
495
  apply RmaxLess1; auto.
 
496
  rewrite (Rabs_left r); auto.
 
497
  apply Rle_trans with (- p); auto with real.
 
498
  apply RmaxLess1; auto.
 
499
Qed.
 
500
 
 
501
Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Zabs z).
 
502
Proof.
 
503
  intros z; case z; simpl in |- *; auto with real.
 
504
  apply Rabs_right; auto with real.
 
505
  intros p0; apply Rabs_right; auto with real zarith.
 
506
  intros p0; rewrite Rabs_Ropp.
 
507
  apply Rabs_right; auto with real zarith.
 
508
Qed.
 
509