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
(************************************************************************)
9
(*i $Id: RIneq.v 11887 2009-02-06 19:57:33Z herbelin $ i*)
11
(*********************************************************)
12
(** * Basic lemmas for the classical real numbers *)
13
(*********************************************************)
15
Require Export Raxioms.
16
Require Import Rpow_def.
17
Require Import Zpower.
18
Require Export ZArithRing.
20
Require Export RealField.
22
Open Local Scope Z_scope.
23
Open Local Scope R_scope.
27
(*********************************************************)
28
(** ** Relation between orders and equality *)
29
(*********************************************************)
31
(** Reflexivity of the large order *)
33
Lemma Rle_refl : forall r, r <= r.
35
intro; right; reflexivity.
37
Hint Immediate Rle_refl: rorders.
39
Lemma Rge_refl : forall r, r <= r.
40
Proof. exact Rle_refl. Qed.
41
Hint Immediate Rge_refl: rorders.
43
(** Irreflexivity of the strict order *)
45
Lemma Rlt_irrefl : forall r, ~ r < r.
47
generalize Rlt_asym. intuition eauto.
49
Hint Resolve Rlt_irrefl: real.
51
Lemma Rgt_irrefl : forall r, ~ r > r.
52
Proof. exact Rlt_irrefl. Qed.
54
Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2.
56
red in |- *; intros r1 r2 H H0; apply (Rlt_irrefl r1).
57
pattern r1 at 2 in |- *; rewrite H0; trivial.
60
Lemma Rgt_not_eq : forall r1 r2, r1 > r2 -> r1 <> r2.
62
intros; apply sym_not_eq; apply Rlt_not_eq; auto with real.
66
Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2.
68
generalize Rlt_not_eq Rgt_not_eq. intuition eauto.
70
Hint Resolve Rlt_dichotomy_converse: real.
72
(** Reasoning by case on equality and order *)
75
Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2.
77
intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse;
80
Hint Resolve Req_dec: real.
83
Lemma Rtotal_order : forall r1 r2, r1 < r2 \/ r1 = r2 \/ r1 > r2.
85
intros; generalize (total_order_T r1 r2); tauto.
89
Lemma Rdichotomy : forall r1 r2, r1 <> r2 -> r1 < r2 \/ r1 > r2.
91
intros; generalize (total_order_T r1 r2); tauto.
94
(*********************************************************)
95
(** ** Relating [<], [>], [<=] and [>=] *)
96
(*********************************************************)
98
(*********************************************************)
100
(*********************************************************)
102
(** *** Relating strict and large orders *)
104
Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2.
106
intros; red in |- *; tauto.
108
Hint Resolve Rlt_le: real.
110
Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2.
116
Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1.
118
destruct 1; red in |- *; auto with real.
120
Hint Immediate Rle_ge: real.
121
Hint Resolve Rle_ge: rorders.
123
Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1.
125
destruct 1; red in |- *; auto with real.
127
Hint Resolve Rge_le: real.
128
Hint Immediate Rge_le: rorders.
131
Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
135
Hint Resolve Rlt_gt: rorders.
137
Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1.
141
Hint Immediate Rgt_lt: rorders.
145
Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1.
147
intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto.
149
Hint Immediate Rnot_le_lt: real.
151
Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1.
152
Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
154
Lemma Rnot_le_gt : forall r1 r2, ~ r1 <= r2 -> r1 > r2.
155
Proof. intros; red; apply Rnot_le_lt. auto with real. Qed.
157
Lemma Rnot_ge_lt : forall r1 r2, ~ r1 >= r2 -> r1 < r2.
158
Proof. intros; apply Rnot_le_lt. auto with real. Qed.
160
Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1.
162
intros r1 r2 H; destruct (Rtotal_order r1 r2) as [ | [ H0 | H0 ] ].
163
contradiction. subst; auto with rorders. auto with real.
166
Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2.
167
Proof. auto using Rnot_lt_le with real. Qed.
169
Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1.
170
Proof. intros; eauto using Rnot_lt_le with rorders. Qed.
172
Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2.
173
Proof. eauto using Rnot_gt_ge with rorders. Qed.
176
Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2.
178
generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *.
181
Hint Immediate Rlt_not_le: real.
183
Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2.
184
Proof. exact Rlt_not_le. Qed.
186
Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2.
187
Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed.
188
Hint Immediate Rlt_not_ge: real.
190
Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2.
191
Proof. exact Rlt_not_ge. Qed.
193
Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2.
195
intros r1 r2. generalize (Rlt_asym r1 r2) (Rlt_dichotomy_converse r1 r2).
196
unfold Rle in |- *; intuition.
199
Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2.
200
Proof. intros; apply Rle_not_lt; auto with real. Qed.
202
Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2.
203
Proof. do 2 intro; apply Rle_not_lt. Qed.
205
Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2.
206
Proof. do 2 intro; apply Rge_not_lt. Qed.
209
Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2.
211
unfold Rle in |- *; tauto.
213
Hint Immediate Req_le: real.
215
Lemma Req_ge : forall r1 r2, r1 = r2 -> r1 >= r2.
217
unfold Rge in |- *; tauto.
219
Hint Immediate Req_ge: real.
221
Lemma Req_le_sym : forall r1 r2, r2 = r1 -> r1 <= r2.
223
unfold Rle in |- *; auto.
225
Hint Immediate Req_le_sym: real.
227
Lemma Req_ge_sym : forall r1 r2, r2 = r1 -> r1 >= r2.
229
unfold Rge in |- *; auto.
231
Hint Immediate Req_ge_sym: real.
235
(** Remark: [Rlt_asym] is an axiom *)
237
Lemma Rgt_asym : forall r1 r2:R, r1 > r2 -> ~ r2 > r1.
238
Proof. do 2 intro; apply Rlt_asym. Qed.
240
(** *** Antisymmetry *)
242
Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2.
244
intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition.
246
Hint Resolve Rle_antisym: real.
248
Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2.
249
Proof. auto with real. Qed.
252
Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2.
257
Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2.
262
(** *** Compatibility with equality *)
264
Lemma Rlt_eq_compat :
265
forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3.
267
intros x x' y y'; intros; replace x with x'; replace y with y'; assumption.
270
Lemma Rgt_eq_compat :
271
forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3.
272
Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed.
274
(** *** Transitivity *)
276
(** Remark: [Rlt_trans] is an axiom *)
278
Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3.
280
generalize trans_eq Rlt_trans Rlt_eq_compat.
285
Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3.
286
Proof. eauto using Rle_trans with rorders. Qed.
288
Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3.
289
Proof. eauto using Rlt_trans with rorders. Qed.
292
Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
294
generalize Rlt_trans Rlt_eq_compat.
299
Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3.
301
generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2.
304
Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3.
305
Proof. eauto using Rlt_le_trans with rorders. Qed.
307
Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3.
308
Proof. eauto using Rle_lt_trans with rorders. Qed.
310
(** *** (Classical) decidability *)
312
Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}.
314
intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2);
318
Lemma Rle_dec : forall r1 r2, {r1 <= r2} + {~ r1 <= r2}.
321
generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2).
322
intuition eauto 4 with real.
325
Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}.
326
Proof. do 2 intro; apply Rlt_dec. Qed.
328
Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}.
329
Proof. intros; edestruct Rle_dec; [left|right]; eauto with rorders. Qed.
331
Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}.
333
intros; generalize (total_order_T r1 r2); intuition.
336
Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}.
337
Proof. intros; edestruct Rlt_le_dec; [left|right]; eauto with rorders. Qed.
339
Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}.
341
intros; generalize (total_order_T r1 r2); intuition.
344
Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}.
345
Proof. intros; edestruct Rle_lt_dec; [left|right]; eauto with rorders. Qed.
347
Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1.
349
intros n m; elim (Rle_lt_dec m n); auto with real.
352
Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1.
353
Proof. intros; edestruct Rlt_or_le; [left|right]; eauto with rorders. Qed.
355
Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1.
357
intros n m; elim (Rlt_le_dec m n); auto with real.
360
Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1.
361
Proof. intros; edestruct Rle_or_lt; [left|right]; eauto with rorders. Qed.
363
Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}.
365
intros r1 r2 H; generalize (total_order_T r1 r2); intuition.
369
Lemma inser_trans_R :
370
forall r1 r2 r3 r4, r1 <= r2 < r3 -> {r1 <= r2 < r4} + {r4 <= r2 < r3}.
372
intros n m p q; intros; generalize (Rlt_le_dec m q); intuition.
375
(*********************************************************)
377
(*********************************************************)
379
(** Remark: [Rplus_0_l] is an axiom *)
381
Lemma Rplus_0_r : forall r, r + 0 = r.
385
Hint Resolve Rplus_0_r: real.
387
Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
391
Hint Resolve Rplus_ne: real v62.
395
(** Remark: [Rplus_opp_r] is an axiom *)
397
Lemma Rplus_opp_l : forall r, - r + r = 0.
401
Hint Resolve Rplus_opp_l: real.
404
Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1.
407
replace y with (- x + x + y) by ring.
408
rewrite Rplus_assoc; rewrite H; ring.
411
Hint Resolve (f_equal (A:=R)): real.
413
Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2.
418
(*i Old i*)Hint Resolve Rplus_eq_compat_l: v62.
421
Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 = r + r2 -> r1 = r2.
423
intros; transitivity (- r + r + r1).
425
transitivity (- r + r + r2).
426
repeat rewrite Rplus_assoc; rewrite <- H; reflexivity.
429
Hint Resolve Rplus_eq_reg_l: real.
432
Lemma Rplus_0_r_uniq : forall r r1, r + r1 = r -> r1 = 0.
434
intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real.
439
forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0.
441
intros a b H [H0| H0] H1; auto with real.
443
rewrite H1; auto with real.
444
apply Rle_lt_trans with (a + 0).
445
rewrite Rplus_0_r in |- *; assumption.
446
auto using Rplus_lt_compat_l with real.
447
rewrite <- H0, Rplus_0_r in H1; assumption.
451
forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0.
454
apply Rplus_eq_0_l with b; auto with real.
455
apply Rplus_eq_0_l with a; auto with real.
456
rewrite Rplus_comm; auto with real.
459
(*********************************************************)
460
(** ** Multiplication *)
461
(*********************************************************)
464
Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1.
466
intros; field; trivial.
468
Hint Resolve Rinv_r: real.
470
Lemma Rinv_l_sym : forall r, r <> 0 -> 1 = / r * r.
472
intros; field; trivial.
474
Hint Resolve Rinv_l_sym: real.
476
Lemma Rinv_r_sym : forall r, r <> 0 -> 1 = r * / r.
478
intros; field; trivial.
480
Hint Resolve Rinv_r_sym: real.
483
Lemma Rmult_0_r : forall r, r * 0 = 0.
487
Hint Resolve Rmult_0_r: real v62.
490
Lemma Rmult_0_l : forall r, 0 * r = 0.
494
Hint Resolve Rmult_0_l: real v62.
497
Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r.
501
Hint Resolve Rmult_ne: real v62.
504
Lemma Rmult_1_r : forall r, r * 1 = r.
508
Hint Resolve Rmult_1_r: real.
511
Lemma Rmult_eq_compat_l : forall r r1 r2, r1 = r2 -> r * r1 = r * r2.
516
(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
519
Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
521
intros; transitivity (/ r * r * r1).
523
transitivity (/ r * r * r2).
524
repeat rewrite Rmult_assoc; rewrite H; trivial.
529
Lemma Rmult_integral : forall r1 r2, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0.
531
intros; case (Req_dec r1 0); [ intro Hz | intro Hnotz ].
533
right; apply Rmult_eq_reg_l with r1; trivial.
534
rewrite H; auto with real.
538
Lemma Rmult_eq_0_compat : forall r1 r2, r1 = 0 \/ r2 = 0 -> r1 * r2 = 0.
540
intros r1 r2 [H| H]; rewrite H; auto with real.
543
Hint Resolve Rmult_eq_0_compat: real.
546
Lemma Rmult_eq_0_compat_r : forall r1 r2, r1 = 0 -> r1 * r2 = 0.
552
Lemma Rmult_eq_0_compat_l : forall r1 r2, r2 = 0 -> r1 * r2 = 0.
558
Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
560
intros r1 r2 H; split; red in |- *; intro; apply H; auto with real.
564
Lemma Rmult_integral_contrapositive :
565
forall r1 r2, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0.
567
red in |- *; intros r1 r2 [H1 H2] H.
568
case (Rmult_integral r1 r2); auto with real.
570
Hint Resolve Rmult_integral_contrapositive: real.
572
Lemma Rmult_integral_contrapositive_currified :
573
forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0.
574
Proof. auto using Rmult_integral_contrapositive. Qed.
577
Lemma Rmult_plus_distr_r :
578
forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3.
583
(*********************************************************)
584
(** ** Square function *)
585
(*********************************************************)
588
Definition Rsqr r : R := r * r.
590
Notation "r ²" := (Rsqr r) (at level 1, format "r ²") : R_scope.
593
Lemma Rsqr_0 : Rsqr 0 = 0.
594
unfold Rsqr in |- *; auto with real.
598
Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0.
599
unfold Rsqr in |- *; intros; elim (Rmult_integral r r H); trivial.
602
(*********************************************************)
604
(*********************************************************)
607
Lemma Ropp_eq_compat : forall r1 r2, r1 = r2 -> - r1 = - r2.
611
Hint Resolve Ropp_eq_compat: real.
614
Lemma Ropp_0 : -0 = 0.
618
Hint Resolve Ropp_0: real v62.
621
Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0.
623
intros; rewrite H; auto with real.
625
Hint Resolve Ropp_eq_0_compat: real.
628
Lemma Ropp_involutive : forall r, - - r = r.
632
Hint Resolve Ropp_involutive: real.
635
Lemma Ropp_neq_0_compat : forall r, r <> 0 -> - r <> 0.
637
red in |- *; intros r H H0.
639
transitivity (- - r); auto with real.
641
Hint Resolve Ropp_neq_0_compat: real.
644
Lemma Ropp_plus_distr : forall r1 r2, - (r1 + r2) = - r1 + - r2.
648
Hint Resolve Ropp_plus_distr: real.
650
(*********************************************************)
651
(** ** Opposite and multiplication *)
652
(*********************************************************)
654
Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2).
658
Hint Resolve Ropp_mult_distr_l_reverse: real.
661
Lemma Rmult_opp_opp : forall r1 r2, - r1 * - r2 = r1 * r2.
665
Hint Resolve Rmult_opp_opp: real.
667
Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 = - (r1 * r2).
672
(*********************************************************)
673
(** ** Substraction *)
674
(*********************************************************)
676
Lemma Rminus_0_r : forall r, r - 0 = r.
680
Hint Resolve Rminus_0_r: real.
682
Lemma Rminus_0_l : forall r, 0 - r = - r.
686
Hint Resolve Rminus_0_l: real.
689
Lemma Ropp_minus_distr : forall r1 r2, - (r1 - r2) = r2 - r1.
693
Hint Resolve Ropp_minus_distr: real.
695
Lemma Ropp_minus_distr' : forall r1 r2, - (r2 - r1) = r1 - r2.
701
Lemma Rminus_diag_eq : forall r1 r2, r1 = r2 -> r1 - r2 = 0.
703
intros; rewrite H; ring.
705
Hint Resolve Rminus_diag_eq: real.
708
Lemma Rminus_diag_uniq : forall r1 r2, r1 - r2 = 0 -> r1 = r2.
710
intros r1 r2; unfold Rminus in |- *; rewrite Rplus_comm; intro.
711
rewrite <- (Ropp_involutive r2); apply (Rplus_opp_r_uniq (- r2) r1 H).
713
Hint Immediate Rminus_diag_uniq: real.
715
Lemma Rminus_diag_uniq_sym : forall r1 r2, r2 - r1 = 0 -> r1 = r2.
717
intros; generalize (Rminus_diag_uniq r2 r1 H); clear H; intro H; rewrite H;
720
Hint Immediate Rminus_diag_uniq_sym: real.
722
Lemma Rplus_minus : forall r1 r2, r1 + (r2 - r1) = r2.
726
Hint Resolve Rplus_minus: real.
729
Lemma Rminus_eq_contra : forall r1 r2, r1 <> r2 -> r1 - r2 <> 0.
731
red in |- *; intros r1 r2 H H0.
732
apply H; auto with real.
734
Hint Resolve Rminus_eq_contra: real.
736
Lemma Rminus_not_eq : forall r1 r2, r1 - r2 <> 0 -> r1 <> r2.
738
red in |- *; intros; elim H; apply Rminus_diag_eq; auto.
740
Hint Resolve Rminus_not_eq: real.
742
Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
744
red in |- *; intros; elim H; rewrite H0; ring.
746
Hint Resolve Rminus_not_eq_right: real.
749
Lemma Rmult_minus_distr_l :
750
forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3.
755
(*********************************************************)
757
(*********************************************************)
759
Lemma Rinv_1 : / 1 = 1.
763
Hint Resolve Rinv_1: real.
766
Lemma Rinv_neq_0_compat : forall r, r <> 0 -> / r <> 0.
768
red in |- *; intros; apply R1_neq_R0.
769
replace 1 with (/ r * r); auto with real.
771
Hint Resolve Rinv_neq_0_compat: real.
774
Lemma Rinv_involutive : forall r, r <> 0 -> / / r = r.
776
intros; field; trivial.
778
Hint Resolve Rinv_involutive: real.
781
Lemma Rinv_mult_distr :
782
forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2.
788
Lemma Ropp_inv_permute : forall r, r <> 0 -> - / r = / - r.
790
intros; field; trivial.
793
Lemma Rinv_r_simpl_r : forall r1 r2, r1 <> 0 -> r1 * / r1 * r2 = r2.
795
intros; transitivity (1 * r2); auto with real.
796
rewrite Rinv_r; auto with real.
799
Lemma Rinv_r_simpl_l : forall r1 r2, r1 <> 0 -> r2 * r1 * / r1 = r2.
801
intros; transitivity (r2 * 1); auto with real.
802
transitivity (r2 * (r1 * / r1)); auto with real.
805
Lemma Rinv_r_simpl_m : forall r1 r2, r1 <> 0 -> r1 * r2 * / r1 = r2.
807
intros; transitivity (r2 * 1); auto with real.
808
transitivity (r2 * (r1 * / r1)); auto with real.
811
Hint Resolve Rinv_r_simpl_l Rinv_r_simpl_r Rinv_r_simpl_m: real.
814
Lemma Rinv_mult_simpl :
815
forall r1 r2 r3, r1 <> 0 -> r1 * / r2 * (r3 * / r1) = r3 * / r2.
817
intros a b c; intros.
818
transitivity (a * / a * (c * / b)); auto with real.
822
(*********************************************************)
823
(** ** Order and addition *)
824
(*********************************************************)
826
(** *** Compatibility *)
828
(** Remark: [Rplus_lt_compat_l] is an axiom *)
830
Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2.
831
Proof. eauto using Rplus_lt_compat_l with rorders. Qed.
832
Hint Resolve Rplus_gt_compat_l: real.
835
Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r.
838
rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real.
840
Hint Resolve Rplus_lt_compat_r: real.
842
Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r.
843
Proof. do 3 intro; apply Rplus_lt_compat_r. Qed.
846
Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2.
848
unfold Rle in |- *; intros; elim H; intro.
849
left; apply (Rplus_lt_compat_l r r1 r2 H0).
850
right; rewrite <- H0; auto with zarith real.
853
Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2.
854
Proof. auto using Rplus_le_compat_l with rorders. Qed.
855
Hint Resolve Rplus_ge_compat_l: real.
858
Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r.
860
unfold Rle in |- *; intros; elim H; intro.
861
left; apply (Rplus_lt_compat_r r r1 r2 H0).
862
right; rewrite <- H0; auto with real.
865
Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real.
867
Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r.
868
Proof. auto using Rplus_le_compat_r with rorders. Qed.
871
Lemma Rplus_lt_compat :
872
forall r1 r2 r3 r4, r1 < r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
874
intros; apply Rlt_trans with (r2 + r3); auto with real.
876
Hint Immediate Rplus_lt_compat: real.
878
Lemma Rplus_le_compat :
879
forall r1 r2 r3 r4, r1 <= r2 -> r3 <= r4 -> r1 + r3 <= r2 + r4.
881
intros; apply Rle_trans with (r2 + r3); auto with real.
883
Hint Immediate Rplus_le_compat: real.
885
Lemma Rplus_gt_compat :
886
forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
887
Proof. auto using Rplus_lt_compat with rorders. Qed.
889
Lemma Rplus_ge_compat :
890
forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4.
891
Proof. auto using Rplus_le_compat with rorders. Qed.
894
Lemma Rplus_lt_le_compat :
895
forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4.
897
intros; apply Rlt_le_trans with (r2 + r3); auto with real.
900
Lemma Rplus_le_lt_compat :
901
forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4.
903
intros; apply Rle_lt_trans with (r2 + r3); auto with real.
906
Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real.
908
Lemma Rplus_gt_ge_compat :
909
forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4.
910
Proof. auto using Rplus_lt_le_compat with rorders. Qed.
912
Lemma Rplus_ge_gt_compat :
913
forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4.
914
Proof. auto using Rplus_le_lt_compat with rorders. Qed.
917
Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2.
919
intros x y; intros; apply Rlt_trans with x;
921
| pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
925
Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2.
927
intros x y; intros; apply Rle_lt_trans with x;
929
| pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l;
933
Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2.
935
intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat;
939
Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2.
941
intros x y; intros; apply Rle_trans with x;
943
| pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
948
Lemma sum_inequa_Rle_lt :
949
forall a x b c y d:R,
950
a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d.
953
apply Rlt_le_trans with (a + y); auto with real.
954
apply Rlt_le_trans with (b + y); auto with real.
957
(** *** Cancellation *)
959
Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2.
961
intros; cut (- r + r + r1 < - r + r + r2).
963
elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1;
964
auto with zarith real.
965
rewrite Rplus_assoc; rewrite Rplus_assoc;
966
apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H).
969
Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2.
971
unfold Rle in |- *; intros; elim H; intro.
972
left; apply (Rplus_lt_reg_r r r1 r2 H0).
973
right; apply (Rplus_eq_reg_l r r1 r2 H0).
976
Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2.
978
unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H).
981
Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2.
983
intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real.
987
Lemma Rplus_le_reg_pos_r :
988
forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3.
990
intros x y z; intros; apply Rle_trans with (x + y);
991
[ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
996
Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3.
998
intros x y z; intros; apply Rle_lt_trans with (x + y);
999
[ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l;
1004
Lemma Rplus_ge_reg_neg_r :
1005
forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3.
1007
intros x y z; intros; apply Rge_trans with (x + y);
1008
[ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
1013
Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3.
1015
intros x y z; intros; apply Rge_gt_trans with (x + y);
1016
[ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l;
1021
(*********************************************************)
1022
(** ** Order and opposite *)
1023
(*********************************************************)
1025
(** *** Contravariant compatibility *)
1027
Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2.
1029
unfold Rgt in |- *; intros.
1030
apply (Rplus_lt_reg_r (r2 + r1)).
1031
replace (r2 + r1 + - r1) with r2.
1032
replace (r2 + r1 + - r2) with r1.
1037
Hint Resolve Ropp_gt_lt_contravar.
1039
Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
1041
unfold Rgt in |- *; auto with real.
1043
Hint Resolve Ropp_lt_gt_contravar: real.
1046
Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2.
1050
Hint Resolve Ropp_lt_contravar: real.
1052
Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2.
1053
Proof. auto with real. Qed.
1056
Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2.
1058
unfold Rge; intros r1 r2 [H| H]; auto with real.
1060
Hint Resolve Ropp_le_ge_contravar: real.
1062
Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2.
1064
unfold Rle; intros r1 r2 [H| H]; auto with real.
1066
Hint Resolve Ropp_ge_le_contravar: real.
1069
Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2.
1071
intros r1 r2 H; elim H; auto with real.
1073
Hint Resolve Ropp_le_contravar: real.
1075
Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2.
1076
Proof. auto using Ropp_le_contravar with real. Qed.
1079
Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r.
1081
intros; replace 0 with (-0); auto with real.
1083
Hint Resolve Ropp_0_lt_gt_contravar: real.
1085
Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r.
1087
intros; replace 0 with (-0); auto with real.
1089
Hint Resolve Ropp_0_gt_lt_contravar: real.
1092
Lemma Ropp_lt_gt_0_contravar : forall r, r > 0 -> - r < 0.
1094
intros; rewrite <- Ropp_0; auto with real.
1096
Hint Resolve Ropp_lt_gt_0_contravar: real.
1098
Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0.
1100
intros; rewrite <- Ropp_0; auto with real.
1102
Hint Resolve Ropp_gt_lt_0_contravar: real.
1105
Lemma Ropp_0_le_ge_contravar : forall r, 0 <= r -> 0 >= - r.
1107
intros; replace 0 with (-0); auto with real.
1109
Hint Resolve Ropp_0_le_ge_contravar: real.
1111
Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r.
1113
intros; replace 0 with (-0); auto with real.
1115
Hint Resolve Ropp_0_ge_le_contravar: real.
1117
(** *** Cancellation *)
1119
Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2.
1122
rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
1125
Hint Immediate Ropp_lt_cancel: real.
1127
Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2.
1128
Proof. auto using Ropp_lt_cancel with rorders. Qed.
1130
Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2.
1133
elim H; auto with real.
1134
intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y);
1135
rewrite H1; auto with real.
1137
Hint Immediate Ropp_le_cancel: real.
1139
Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2.
1140
Proof. auto using Ropp_le_cancel with rorders. Qed.
1142
(*********************************************************)
1143
(** ** Order and multiplication *)
1144
(*********************************************************)
1146
(** Remark: [Rmult_lt_compat_l] is an axiom *)
1148
(** *** Covariant compatibility *)
1150
Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
1152
intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
1154
Hint Resolve Rmult_lt_compat_r.
1156
Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
1157
Proof. eauto using Rmult_lt_compat_r with rorders. Qed.
1159
Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2.
1160
Proof. eauto using Rmult_lt_compat_l with rorders. Qed.
1163
Lemma Rmult_le_compat_l :
1164
forall r r1 r2, 0 <= r -> r1 <= r2 -> r * r1 <= r * r2.
1166
intros r r1 r2 H H0; destruct H; destruct H0; unfold Rle in |- *;
1168
right; rewrite <- H; do 2 rewrite Rmult_0_l; reflexivity.
1170
Hint Resolve Rmult_le_compat_l: real.
1172
Lemma Rmult_le_compat_r :
1173
forall r r1 r2, 0 <= r -> r1 <= r2 -> r1 * r <= r2 * r.
1175
intros r r1 r2 H; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r);
1178
Hint Resolve Rmult_le_compat_r: real.
1180
Lemma Rmult_ge_compat_l :
1181
forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2.
1182
Proof. eauto using Rmult_le_compat_l with rorders. Qed.
1184
Lemma Rmult_ge_compat_r :
1185
forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r.
1186
Proof. eauto using Rmult_le_compat_r with rorders. Qed.
1189
Lemma Rmult_le_compat :
1191
0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4.
1193
intros x y z t H' H'0 H'1 H'2.
1194
apply Rle_trans with (r2 := x * t); auto with real.
1195
repeat rewrite (fun x => Rmult_comm x t).
1196
apply Rmult_le_compat_l; auto.
1197
apply Rle_trans with z; auto.
1199
Hint Resolve Rmult_le_compat: real.
1201
Lemma Rmult_ge_compat :
1203
r2 >= 0 -> r4 >= 0 -> r1 >= r2 -> r3 >= r4 -> r1 * r3 >= r2 * r4.
1204
Proof. auto with real rorders. Qed.
1206
Lemma Rmult_gt_0_lt_compat :
1208
r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
1210
intros; apply Rlt_trans with (r2 * r3); auto with real.
1214
Lemma Rmult_le_0_lt_compat :
1216
0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
1218
intros; apply Rle_lt_trans with (r2 * r3);
1219
[ apply Rmult_le_compat_r; [ assumption | left; assumption ]
1220
| apply Rmult_lt_compat_l;
1221
[ apply Rle_lt_trans with r1; assumption | assumption ] ].
1225
Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2.
1226
Proof. intros; replace 0 with (0 * r2); auto with real. Qed.
1228
Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0.
1229
Proof Rmult_lt_0_compat.
1231
(** *** Contravariant compatibility *)
1233
Lemma Rmult_le_compat_neg_l :
1234
forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1.
1236
intros; replace r with (- - r); auto with real.
1237
do 2 rewrite (Ropp_mult_distr_l_reverse (- r)).
1238
apply Ropp_le_contravar; auto with real.
1240
Hint Resolve Rmult_le_compat_neg_l: real.
1242
Lemma Rmult_le_ge_compat_neg_l :
1243
forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r1 >= r * r2.
1245
intros; apply Rle_ge; auto with real.
1247
Hint Resolve Rmult_le_ge_compat_neg_l: real.
1249
Lemma Rmult_lt_gt_compat_neg_l :
1250
forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2.
1252
intros; replace r with (- - r); auto with real.
1253
rewrite (Ropp_mult_distr_l_reverse (- r));
1254
rewrite (Ropp_mult_distr_l_reverse (- r)).
1255
apply Ropp_lt_gt_contravar; auto with real.
1258
(** *** Cancellation *)
1260
Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
1263
case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0.
1264
rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto.
1265
generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False;
1266
generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
1267
intro; apply (Rlt_irrefl (z * x)); auto.
1270
Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2.
1271
Proof. eauto using Rmult_lt_reg_l with rorders. Qed.
1273
Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2.
1275
intros z x y H H0; case H0; auto with real.
1276
intros H1; apply Rlt_le.
1277
apply Rmult_lt_reg_l with (r := z); auto.
1278
intros H1; replace x with (/ z * (z * x)); auto with real.
1279
replace y with (/ z * (z * y)).
1280
rewrite H1; auto with real.
1281
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
1282
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
1285
(*********************************************************)
1286
(** ** Order and substraction *)
1287
(*********************************************************)
1289
Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0.
1291
intros; apply (Rplus_lt_reg_r r2).
1292
replace (r2 + (r1 - r2)) with r1.
1293
replace (r2 + 0) with r2; auto with real.
1296
Hint Resolve Rlt_minus: real.
1298
Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
1300
intros; apply (Rplus_lt_reg_r r2).
1301
replace (r2 + (r1 - r2)) with r1.
1302
replace (r2 + 0) with r2; auto with real.
1307
Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0.
1309
destruct 1; unfold Rle in |- *; auto with real.
1312
Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
1315
auto using Rgt_minus, Rgt_ge.
1316
right; auto using Rminus_diag_eq with rorders.
1320
Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2.
1322
intros; replace r1 with (r1 - r2 + r2).
1323
pattern r2 at 3 in |- *; replace r2 with (0 + r2); auto with real.
1327
Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2.
1329
intros; replace r2 with (0 + r2); auto with real.
1330
replace r1 with (r1 - r2 + r2).
1331
apply Rplus_gt_compat_r; assumption.
1336
Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2.
1338
intros; replace r1 with (r1 - r2 + r2).
1339
pattern r2 at 3 in |- *; replace r2 with (0 + r2); auto with real.
1343
Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2.
1345
intros; replace r2 with (0 + r2); auto with real.
1346
replace r1 with (r1 - r2 + r2).
1347
apply Rplus_ge_compat_r; assumption.
1352
Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0.
1354
intros; apply sym_not_eq; apply Rlt_not_eq.
1355
rewrite Rplus_comm; replace 0 with (0 + 0); auto with real.
1357
Hint Immediate tech_Rplus: real.
1359
(*********************************************************)
1360
(** ** Order and square function *)
1361
(*********************************************************)
1363
Lemma Rle_0_sqr : forall r, 0 <= Rsqr r.
1365
intro; case (Rlt_le_dec r 0); unfold Rsqr in |- *; intro.
1366
replace (r * r) with (- r * - r); auto with real.
1367
replace 0 with (- r * 0); auto with real.
1368
replace 0 with (0 * r); auto with real.
1372
Lemma Rlt_0_sqr : forall r, r <> 0 -> 0 < Rsqr r.
1374
intros; case (Rdichotomy r 0); trivial; unfold Rsqr in |- *; intro.
1375
replace (r * r) with (- r * - r); auto with real.
1376
replace 0 with (- r * 0); auto with real.
1377
replace 0 with (0 * r); auto with real.
1379
Hint Resolve Rle_0_sqr Rlt_0_sqr: real.
1382
Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0.
1384
intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b);
1388
Lemma Rplus_sqr_eq_0 :
1389
forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0.
1392
apply Rplus_sqr_eq_0_l with b; auto with real.
1393
apply Rplus_sqr_eq_0_l with a; auto with real.
1394
rewrite Rplus_comm; auto with real.
1397
(*********************************************************)
1398
(** ** Zero is less than one *)
1399
(*********************************************************)
1401
Lemma Rlt_0_1 : 0 < 1.
1403
replace 1 with (Rsqr 1); auto with real.
1404
unfold Rsqr in |- *; auto with real.
1406
Hint Resolve Rlt_0_1: real.
1408
Lemma Rle_0_1 : 0 <= 1.
1414
(*********************************************************)
1415
(** ** Order and inverse *)
1416
(*********************************************************)
1418
Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r.
1420
intros; apply Rnot_le_lt; red in |- *; intros.
1421
absurd (1 <= 0); auto with real.
1422
replace 1 with (r * / r); auto with real.
1423
replace 0 with (r * 0); auto with real.
1425
Hint Resolve Rinv_0_lt_compat: real.
1428
Lemma Rinv_lt_0_compat : forall r, r < 0 -> / r < 0.
1430
intros; apply Rnot_le_lt; red in |- *; intros.
1431
absurd (1 <= 0); auto with real.
1432
replace 1 with (r * / r); auto with real.
1433
replace 0 with (r * 0); auto with real.
1435
Hint Resolve Rinv_lt_0_compat: real.
1438
Lemma Rinv_lt_contravar : forall r1 r2, 0 < r1 * r2 -> r1 < r2 -> / r2 < / r1.
1440
intros; apply Rmult_lt_reg_l with (r1 * r2); auto with real.
1441
case (Rmult_neq_0_reg r1 r2); intros; auto with real.
1442
replace (r1 * r2 * / r2) with r1.
1443
replace (r1 * r2 * / r1) with r2; trivial.
1444
symmetry in |- *; auto with real.
1445
symmetry in |- *; auto with real.
1448
Lemma Rinv_1_lt_contravar : forall r1 r2, 1 <= r1 -> r1 < r2 -> / r2 < / r1.
1451
cut (0 < x); [ intros Lt0 | apply Rlt_le_trans with (r2 := 1) ];
1453
apply Rmult_lt_reg_l with (r := x); auto with real.
1454
rewrite (Rmult_comm x (/ x)); rewrite Rinv_l; auto with real.
1455
apply Rmult_lt_reg_l with (r := y); auto with real.
1456
apply Rlt_trans with (r2 := x); auto.
1457
cut (y * (x * / y) = x).
1458
intro H1; rewrite H1; rewrite (Rmult_1_r y); auto.
1459
rewrite (Rmult_comm x); rewrite <- Rmult_assoc; rewrite (Rmult_comm y (/ y));
1460
rewrite Rinv_l; auto with real.
1461
apply Rlt_dichotomy_converse; right.
1462
red in |- *; apply Rlt_trans with (r2 := x); auto with real.
1464
Hint Resolve Rinv_1_lt_contravar: real.
1466
(*********************************************************)
1467
(** ** Miscellaneous *)
1468
(*********************************************************)
1471
Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1.
1474
apply Rlt_le_trans with 1; auto with real.
1475
pattern 1 at 1 in |- *; replace 1 with (0 + 1); auto with real.
1477
Hint Resolve Rle_lt_0_plus_1: real.
1480
Lemma Rlt_plus_1 : forall r, r < r + 1.
1483
pattern r at 1 in |- *; replace r with (r + 0); auto with real.
1485
Hint Resolve Rlt_plus_1: real.
1488
Lemma tech_Rgt_minus : forall r1 r2, 0 < r2 -> r1 > r1 - r2.
1490
red in |- *; unfold Rminus in |- *; intros.
1491
pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real.
1494
(*********************************************************)
1495
(** ** Injection from [N] to [R] *)
1496
(*********************************************************)
1499
Lemma S_INR : forall n:nat, INR (S n) = INR n + 1.
1501
intro; case n; auto with real.
1505
Lemma S_O_plus_INR : forall n:nat, INR (1 + n) = INR 1 + INR n.
1507
intro; simpl in |- *; case n; intros; auto with real.
1511
Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
1513
intros n m; induction n as [| n Hrecn].
1514
simpl in |- *; auto with real.
1515
replace (S n + m)%nat with (S (n + m)); auto with arith.
1516
repeat rewrite S_INR.
1517
rewrite Hrecn; ring.
1519
Hint Resolve plus_INR: real.
1522
Lemma minus_INR : forall n m:nat, (m <= n)%nat -> INR (n - m) = INR n - INR m.
1524
intros n m le; pattern m, n in |- *; apply le_elim_rel; auto with real.
1525
intros; rewrite <- minus_n_O; auto with real.
1526
intros; repeat rewrite S_INR; simpl in |- *.
1529
Hint Resolve minus_INR: real.
1532
Lemma mult_INR : forall n m:nat, INR (n * m) = INR n * INR m.
1534
intros n m; induction n as [| n Hrecn].
1535
simpl in |- *; auto with real.
1536
intros; repeat rewrite S_INR; simpl in |- *.
1537
rewrite plus_INR; rewrite Hrecn; ring.
1539
Hint Resolve mult_INR: real.
1542
Lemma lt_0_INR : forall n:nat, (0 < n)%nat -> 0 < INR n.
1544
simple induction 1; intros; auto with real.
1545
rewrite S_INR; auto with real.
1547
Hint Resolve lt_0_INR: real.
1549
Lemma lt_INR : forall n m:nat, (n < m)%nat -> INR n < INR m.
1551
simple induction 1; intros; auto with real.
1552
rewrite S_INR; auto with real.
1553
rewrite S_INR; apply Rlt_trans with (INR m0); auto with real.
1555
Hint Resolve lt_INR: real.
1557
Lemma lt_1_INR : forall n:nat, (1 < n)%nat -> 1 < INR n.
1559
intros; replace 1 with (INR 1); auto with real.
1561
Hint Resolve lt_1_INR: real.
1564
Lemma pos_INR_nat_of_P : forall p:positive, 0 < INR (nat_of_P p).
1566
intro; apply lt_0_INR.
1567
simpl in |- *; auto with real.
1568
apply lt_O_nat_of_P.
1570
Hint Resolve pos_INR_nat_of_P: real.
1573
Lemma pos_INR : forall n:nat, 0 <= INR n.
1576
simpl in |- *; auto with real.
1577
auto with arith real.
1579
Hint Resolve pos_INR: real.
1581
Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
1583
double induction n m; intros.
1584
simpl in |- *; elimtype False; apply (Rlt_irrefl 0); auto.
1586
generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
1587
[ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
1588
generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; elimtype False;
1589
apply (Rlt_irrefl 0); auto.
1590
do 2 rewrite S_INR in H1; cut (INR n1 < INR n0).
1591
intro H2; generalize (H0 n0 H2); intro; auto with arith.
1592
apply (Rplus_lt_reg_r 1 (INR n1) (INR n0)).
1593
rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial.
1595
Hint Resolve INR_lt: real.
1598
Lemma le_INR : forall n m:nat, (n <= m)%nat -> INR n <= INR m.
1600
simple induction 1; intros; auto with real.
1602
apply Rle_trans with (INR m0); auto with real.
1604
Hint Resolve le_INR: real.
1607
Lemma INR_not_0 : forall n:nat, INR n <> 0 -> n <> 0%nat.
1609
red in |- *; intros n H H1.
1611
rewrite H1; trivial.
1613
Hint Immediate INR_not_0: real.
1616
Lemma not_0_INR : forall n:nat, n <> 0%nat -> INR n <> 0.
1619
intro; absurd (0%nat = 0%nat); trivial.
1620
intros; rewrite S_INR.
1621
apply Rgt_not_eq; red in |- *; auto with real.
1623
Hint Resolve not_0_INR: real.
1625
Lemma not_INR : forall n m:nat, n <> m -> INR n <> INR m.
1627
intros n m H; case (le_or_lt n m); intros H1.
1628
case (le_lt_or_eq _ _ H1); intros H2.
1629
apply Rlt_dichotomy_converse; auto with real.
1630
elimtype False; auto.
1631
apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
1633
Hint Resolve not_INR: real.
1635
Lemma INR_eq : forall n m:nat, INR n = INR m -> n = m.
1637
intros; case (le_or_lt n m); intros H1.
1638
case (le_lt_or_eq _ _ H1); intros H2; auto.
1640
intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto.
1642
symmetry in |- *; cut (m <> n).
1643
intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto.
1646
Hint Resolve INR_eq: real.
1648
Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
1650
intros; elim H; intro.
1651
generalize (INR_lt n m H0); intro; auto with arith.
1652
generalize (INR_eq n m H0); intro; rewrite H1; auto.
1654
Hint Resolve INR_le: real.
1656
Lemma not_1_INR : forall n:nat, n <> 1%nat -> INR n <> 1.
1658
replace 1 with (INR 1); auto with real.
1660
Hint Resolve not_1_INR: real.
1662
(*********************************************************)
1663
(** ** Injection from [Z] to [R] *)
1664
(*********************************************************)
1668
Lemma IZN : forall n:Z, (0 <= n)%Z -> exists m : nat, n = Z_of_nat m.
1670
intros z; idtac; apply Z_of_nat_complete; assumption.
1674
Lemma INR_IZR_INZ : forall n:nat, INR n = IZR (Z_of_nat n).
1676
simple induction n; auto with real.
1677
intros; simpl in |- *; rewrite nat_of_P_o_P_of_succ_nat_eq_succ;
1681
Lemma plus_IZR_NEG_POS :
1682
forall p q:positive, IZR (Zpos p + Zneg q) = IZR (Zpos p) + IZR (Zneg q).
1685
case (lt_eq_lt_dec (nat_of_P p) (nat_of_P q)).
1686
intros [H| H]; simpl in |- *.
1687
rewrite nat_of_P_lt_Lt_compare_complement_morphism; simpl in |- *; trivial.
1688
rewrite (nat_of_P_minus_morphism q p).
1689
rewrite minus_INR; auto with arith; ring.
1690
apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
1691
rewrite (nat_of_P_inj p q); trivial.
1692
rewrite Pcompare_refl; simpl in |- *; auto with real.
1693
intro H; simpl in |- *.
1694
rewrite nat_of_P_gt_Gt_compare_complement_morphism; simpl in |- *;
1696
rewrite (nat_of_P_minus_morphism p q).
1697
rewrite minus_INR; auto with arith; ring.
1698
apply ZC2; apply nat_of_P_lt_Lt_compare_complement_morphism; trivial.
1702
Lemma plus_IZR : forall n m:Z, IZR (n + m) = IZR n + IZR m.
1704
intro z; destruct z; intro t; destruct t; intros; auto with real.
1705
simpl in |- *; intros; rewrite nat_of_P_plus_morphism; auto with real.
1706
apply plus_IZR_NEG_POS.
1707
rewrite Zplus_comm; rewrite Rplus_comm; apply plus_IZR_NEG_POS.
1708
simpl in |- *; intros; rewrite nat_of_P_plus_morphism; rewrite plus_INR;
1713
Lemma mult_IZR : forall n m:Z, IZR (n * m) = IZR n * IZR m.
1715
intros z t; case z; case t; simpl in |- *; auto with real.
1716
intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
1717
intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
1719
rewrite Ropp_mult_distr_l_reverse; auto with real.
1720
apply Ropp_eq_compat; rewrite mult_comm; auto with real.
1721
intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
1722
rewrite Ropp_mult_distr_l_reverse; auto with real.
1723
intros t1 z1; rewrite nat_of_P_mult_morphism; auto with real.
1724
rewrite Rmult_opp_opp; auto with real.
1727
Lemma pow_IZR : forall z n, pow (IZR z) n = IZR (Zpower z (Z_of_nat n)).
1729
intros z [|n];simpl;trivial.
1730
rewrite Zpower_pos_nat.
1731
rewrite nat_of_P_o_P_of_succ_nat_eq_succ. unfold Zpower_nat;simpl.
1733
induction n;simpl;trivial.
1734
rewrite mult_IZR;ring[IHn].
1738
Lemma succ_IZR : forall n:Z, IZR (Zsucc n) = IZR n + 1.
1740
intro; change 1 with (IZR 1); unfold Zsucc; apply plus_IZR.
1744
Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
1746
intro z; case z; simpl in |- *; auto with real.
1750
Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
1752
intros z1 z2; unfold Rminus in |- *; unfold Zminus in |- *.
1753
rewrite <- (Ropp_Ropp_IZR z2); symmetry in |- *; apply plus_IZR.
1757
Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
1759
intro z; case z; simpl in |- *; intros.
1760
absurd (0 < 0); auto with real.
1761
unfold Zlt in |- *; simpl in |- *; trivial.
1762
case Rlt_not_le with (1 := H).
1763
replace 0 with (-0); auto with real.
1767
Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
1769
intros z1 z2 H; apply Zlt_0_minus_lt.
1771
rewrite <- Z_R_minus.
1772
exact (Rgt_minus (IZR z2) (IZR z1) H).
1776
Lemma eq_IZR_R0 : forall n:Z, IZR n = 0 -> n = 0%Z.
1778
intro z; destruct z; simpl in |- *; intros; auto with zarith.
1779
case (Rlt_not_eq 0 (INR (nat_of_P p))); auto with real.
1780
case (Rlt_not_eq (- INR (nat_of_P p)) 0); auto with real.
1781
apply Ropp_lt_gt_0_contravar. unfold Rgt in |- *; apply pos_INR_nat_of_P.
1785
Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
1787
intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
1788
rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
1793
Lemma not_0_IZR : forall n:Z, n <> 0%Z -> IZR n <> 0.
1795
intros z H; red in |- *; intros H0; case H.
1800
Lemma le_0_IZR : forall n:Z, 0 <= IZR n -> (0 <= n)%Z.
1802
unfold Rle in |- *; intros z [H| H].
1803
red in |- *; intro; apply (Zlt_le_weak 0 z (lt_0_IZR z H)); assumption.
1804
rewrite (eq_IZR_R0 z); auto with zarith real.
1808
Lemma le_IZR : forall n m:Z, IZR n <= IZR m -> (n <= m)%Z.
1810
unfold Rle in |- *; intros z1 z2 [H| H].
1811
apply (Zlt_le_weak z1 z2); auto with real.
1812
apply lt_IZR; trivial.
1813
rewrite (eq_IZR z1 z2); auto with zarith real.
1817
Lemma le_IZR_R1 : forall n:Z, IZR n <= 1 -> (n <= 1)%Z.
1819
pattern 1 at 1 in |- *; replace 1 with (IZR 1); intros; auto.
1820
apply le_IZR; trivial.
1824
Lemma IZR_ge : forall n m:Z, (n >= m)%Z -> IZR n >= IZR m.
1826
intros m n H; apply Rnot_lt_ge; red in |- *; intro.
1827
generalize (lt_IZR m n H0); intro; omega.
1830
Lemma IZR_le : forall n m:Z, (n <= m)%Z -> IZR n <= IZR m.
1832
intros m n H; apply Rnot_gt_le; red in |- *; intro.
1833
unfold Rgt in H0; generalize (lt_IZR n m H0); intro; omega.
1836
Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
1838
intros m n H; cut (m <= n)%Z.
1839
intro H0; elim (IZR_le m n H0); intro; auto.
1840
generalize (eq_IZR m n H1); intro; elimtype False; omega.
1844
Lemma one_IZR_lt1 : forall n:Z, -1 < IZR n < 1 -> n = 0%Z.
1848
apply Zlt_succ_le; apply lt_IZR; trivial.
1849
replace 0%Z with (Zsucc (-1)); trivial.
1850
apply Zlt_le_succ; apply lt_IZR; trivial.
1853
Lemma one_IZR_r_R1 :
1854
forall r (n m:Z), r < IZR n <= r + 1 -> r < IZR m <= r + 1 -> n = m.
1856
intros r z x [H1 H2] [H3 H4].
1857
cut ((z - x)%Z = 0%Z); auto with zarith.
1859
rewrite <- Z_R_minus; split.
1860
replace (-1) with (r - (r + 1)).
1861
unfold Rminus in |- *; apply Rplus_lt_le_compat; auto with real.
1863
replace 1 with (r + 1 - r).
1864
unfold Rminus in |- *; apply Rplus_le_lt_compat; auto with real.
1870
Lemma single_z_r_R1 :
1872
r < IZR n -> IZR n <= r + 1 -> r < IZR m -> IZR m <= r + 1 -> n = m.
1874
intros; apply one_IZR_r_R1 with r; auto.
1878
Lemma tech_single_z_r_R1 :
1882
(exists s : Z, s <> n /\ r < IZR s /\ IZR s <= r + 1) -> False.
1884
intros r z H1 H2 [s [H3 [H4 H5]]].
1885
apply H3; apply single_z_r_R1 with r; trivial.
1889
Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2.
1891
intros x y H H0; rewrite <- (Rmult_0_l x); rewrite <- (Rmult_comm x);
1892
apply (Rmult_le_compat_l x 0 y H H0).
1895
Lemma double : forall r1, 2 * r1 = r1 + r1.
1900
Lemma double_var : forall r1, r1 = r1 / 2 + r1 / 2.
1902
intro; rewrite <- double; unfold Rdiv in |- *; rewrite <- Rmult_assoc;
1903
symmetry in |- *; apply Rinv_r_simpl_m.
1904
replace 2 with (INR 2);
1905
[ apply not_0_INR; discriminate | unfold INR in |- *; ring ].
1908
(*********************************************************)
1909
(** ** Other rules about < and <= *)
1910
(*********************************************************)
1912
Lemma Rmult_ge_0_gt_0_lt_compat :
1914
r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4.
1916
intros; apply Rle_lt_trans with (r2 * r3); auto with real.
1920
forall r1 r2, (forall eps:R, 0 < eps -> r1 <= r2 + eps) -> r1 <= r2.
1922
intros x y; intros; elim (Rtotal_order x y); intro.
1926
clear H0; generalize (Rgt_minus x y H1); intro H2; change (0 < x - y) in H2.
1929
generalize (Rmult_lt_0_compat (x - y) (/ 2) H2 (Rinv_0_lt_compat 2 H0));
1930
intro H3; generalize (H ((x - y) * / 2) H3);
1931
replace (y + (x - y) * / 2) with ((y + x) * / 2).
1933
generalize (Rmult_le_compat_l 2 x ((y + x) * / 2) (Rlt_le 0 2 H0) H4);
1934
rewrite <- (Rmult_comm ((y + x) * / 2)); rewrite Rmult_assoc;
1935
rewrite <- Rinv_l_sym.
1936
rewrite Rmult_1_r; replace (2 * x) with (x + x).
1937
rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
1939
replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ].
1940
pattern y at 2 in |- *; replace y with (y / 2 + y / 2).
1941
unfold Rminus, Rdiv in |- *.
1942
repeat rewrite Rmult_plus_distr_r.
1944
cut (forall z:R, 2 * z = z + z).
1946
rewrite <- (H4 (y / 2)).
1947
unfold Rdiv in |- *.
1948
rewrite <- Rmult_assoc; apply Rinv_r_simpl_m.
1949
replace 2 with (INR 2).
1952
unfold INR in |- *; reflexivity.
1954
cut (0%nat <> 2%nat);
1955
[ intro H0; generalize (lt_0_INR 2 (neq_O_lt 2 H0)); unfold INR in |- *;
1961
Lemma completeness_weak :
1963
bound E -> (exists x : R, E x) -> exists m : R, is_lub E m.
1965
intros; elim (completeness E H H0); intros; split with x; assumption.
1968
(*********************************************************)
1969
(** * Definitions of new types *)
1970
(*********************************************************)
1972
Record nonnegreal : Type := mknonnegreal
1973
{nonneg :> R; cond_nonneg : 0 <= nonneg}.
1975
Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}.
1977
Record nonposreal : Type := mknonposreal
1978
{nonpos :> R; cond_nonpos : nonpos <= 0}.
1980
Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}.
1982
Record nonzeroreal : Type := mknonzeroreal
1983
{nonzero :> R; cond_nonzero : nonzero <> 0}.
1985
(** Compatibility *)
1987
Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing).
1988
Notation minus_Rgt := Rminus_gt (only parsing).
1989
Notation minus_Rge := Rminus_ge (only parsing).
1990
Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing).
1991
Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing).
1992
Notation INR_lt_1 := lt_1_INR (only parsing).
1993
Notation lt_INR_0 := lt_0_INR (only parsing).
1994
Notation not_nm_INR := not_INR (only parsing).
1995
Notation INR_pos := pos_INR_nat_of_P (only parsing).
1996
Notation not_INR_O := INR_not_0 (only parsing).
1997
Notation not_O_INR := not_0_INR (only parsing).
1998
Notation not_O_IZR := not_0_IZR (only parsing).
1999
Notation le_O_IZR := le_0_IZR (only parsing).
2000
Notation lt_O_IZR := lt_0_IZR (only parsing).
added
removed
theories/Reals/RIneq.v
