diff options
| -rw-r--r-- | theories/NArith/NArith.v | 2 | ||||
| -rw-r--r-- | theories/Reals/RIneq.v | 996 | ||||
| -rw-r--r-- | theories/Reals/Rdefinitions.v | 24 |
3 files changed, 577 insertions, 445 deletions
diff --git a/theories/NArith/NArith.v b/theories/NArith/NArith.v index 5a2eeda48..53ba50ffe 100644 --- a/theories/NArith/NArith.v +++ b/theories/NArith/NArith.v @@ -12,5 +12,7 @@ Require Export BinPos. Require Export BinNat. +Require Export Nnat. +Require Export Ndigits. Require Export NArithRing. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 8b3847340..0f1b9fdf0 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -8,9 +8,9 @@ (*i $Id$ i*) -(***************************************************************************) -(** Basic lemmas for the classical reals numbers *) -(***************************************************************************) +(*********************************************************) +(** * Basic lemmas for the classical real numbers *) +(*********************************************************) Require Export Raxioms. Require Import Rpow_def. @@ -24,21 +24,32 @@ Open Local Scope R_scope. Implicit Type r : R. -(**************************************************************************) -(** * Relation between orders and equality *) -(**************************************************************************) +(*********************************************************) +(** ** Relation between orders and equality *) +(*********************************************************) + +(** Reflexivity of the large order *) + +Lemma Rle_refl : forall r, r <= r. +Proof. + intro; right; reflexivity. +Qed. +Hint Resolve Rle_refl : real2. + +Lemma Rge_refl : forall r, r <= r. +Proof. exact Rle_refl. Qed. +Hint Resolve Rge_refl : real2. + +(** Irreflexivity of the strict order *) -(**********) Lemma Rlt_irrefl : forall r, ~ r < r. Proof. generalize Rlt_asym. intuition eauto. Qed. Hint Resolve Rlt_irrefl: real. -Lemma Rle_refl : forall r, r <= r. -Proof. - intro; right; reflexivity. -Qed. +Lemma Rgt_irrefl : forall r, ~ r > r. +Proof. exact Rlt_irrefl. Qed. Lemma Rlt_not_eq : forall r1 r2, r1 < r2 -> r1 <> r2. Proof. @@ -58,7 +69,7 @@ Proof. Qed. Hint Resolve Rlt_dichotomy_converse: real. -(** Reasoning by case on equalities and order *) +(** Reasoning by case on equality and order *) (**********) Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2. @@ -80,17 +91,27 @@ Proof. intros; generalize (total_order_T r1 r2); tauto. Qed. +(*********************************************************) +(** ** Relating [<], [>], [<=] and [>=] *) +(*********************************************************) -(*********************************************************************************) -(** * Order Lemma : relating [<], [>], [<=] and [>=] *) -(*********************************************************************************) +(*********************************************************) +(** ** Order *) +(*********************************************************) + +(** *** Relating strict and large orders *) -(**********) Lemma Rlt_le : forall r1 r2, r1 < r2 -> r1 <= r2. Proof. intros; red in |- *; tauto. Qed. -Hint Resolve Rlt_le: real. + +Hint Resolve Rlt_le: real real2. + +Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. +Proof. + intros; red; tauto. +Qed. (**********) Lemma Rle_ge : forall r1 r2, r1 <= r2 -> r2 >= r1. @@ -99,47 +120,77 @@ Proof. Qed. Hint Immediate Rle_ge: real. +Hint Resolve Rle_ge: real2. -(**********) Lemma Rge_le : forall r1 r2, r1 >= r2 -> r2 <= r1. Proof. destruct 1; red in |- *; auto with real. Qed. Hint Resolve Rge_le: real. +Hint Immediate Rge_le: real2. (**********) Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1. -Proof. trivial. Qed. +Proof. + trivial. +Qed. +Hint Resolve Rlt_gt: real2. -(**********) Lemma Rgt_lt : forall r1 r2, r1 > r2 -> r2 < r1. -Proof. trivial. Qed. +Proof. + trivial. +Qed. +Hint Immediate Rgt_lt: real2. (**********) + Lemma Rnot_le_lt : forall r1 r2, ~ r1 <= r2 -> r2 < r1. Proof. intros r1 r2; generalize (Rtotal_order r1 r2); unfold Rle in |- *; tauto. Qed. - Hint Immediate Rnot_le_lt: real. +Lemma Rnot_ge_gt : forall r1 r2, ~ r1 >= r2 -> r2 > r1. +Proof. intros; red; apply Rnot_le_lt. auto with real. Qed. + +Lemma Rnot_le_gt : forall r1 r2, ~ r1 <= r2 -> r1 > r2. +Proof. intros; red; apply Rnot_le_lt. auto with real. Qed. + Lemma Rnot_ge_lt : forall r1 r2, ~ r1 >= r2 -> r1 < r2. +Proof. intros; apply Rnot_le_lt. auto with real. Qed. + +Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1. Proof. - intros; apply Rnot_le_lt; auto with real. + intros r1 r2 H; destruct (Rtotal_order r1 r2) as [ | [ H0 | H0 ] ]. + contradiction. subst; auto with real2. auto with real2. Qed. +Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2. +Proof. auto using Rnot_lt_le with real. Qed. + +Lemma Rnot_gt_ge : forall r1 r2, ~ r1 > r2 -> r2 >= r1. +Proof. intros; eauto using Rnot_lt_le with real2. Qed. + +Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2. +Proof. eauto using Rnot_gt_ge with real2. Qed. + (**********) Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. Proof. generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle in |- *. intuition eauto 3. Qed. +Hint Immediate Rlt_not_le: real. Lemma Rgt_not_le : forall r1 r2, r1 > r2 -> ~ r1 <= r2. -Proof Rlt_not_le. +Proof. exact Rlt_not_le. Qed. -Hint Immediate Rlt_not_le: real. +Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. +Proof. red; intros; eapply Rlt_not_le; eauto with real. Qed. + +Lemma Rgt_not_ge : forall r1 r2, r2 > r1 -> ~ r1 >= r2. +Proof. exact Rlt_not_ge. Qed. Lemma Rle_not_lt : forall r1 r2, r2 <= r1 -> ~ r1 < r2. Proof. @@ -147,13 +198,14 @@ Proof. unfold Rle in |- *; intuition. Qed. -(**********) -Lemma Rlt_not_ge : forall r1 r2, r1 < r2 -> ~ r1 >= r2. -Proof. - generalize Rlt_not_le. unfold Rle, Rge in |- *. intuition eauto 3. -Qed. +Lemma Rge_not_lt : forall r1 r2, r1 >= r2 -> ~ r1 < r2. +Proof. intros; apply Rle_not_lt; auto with real. Qed. -Hint Immediate Rlt_not_ge: real. +Lemma Rle_not_gt : forall r1 r2, r1 <= r2 -> ~ r1 > r2. +Proof. do 2 intro; apply Rle_not_lt. Qed. + +Lemma Rge_not_gt : forall r1 r2, r2 >= r1 -> ~ r1 > r2. +Proof. do 2 intro; apply Rge_not_lt. Qed. (**********) Lemma Req_le : forall r1 r2, r1 = r2 -> r1 <= r2. @@ -180,25 +232,51 @@ Proof. Qed. Hint Immediate Req_ge_sym: real. +(** *** Asymmetry *) + +(** Remark: [Rlt_asym] is an axiom *) + +Lemma Rgt_asym : forall r1 r2:R, r1 > r2 -> ~ r2 > r1. +Proof. do 2 intro; apply Rlt_asym. Qed. + +(** *** Antisymmetry *) + Lemma Rle_antisym : forall r1 r2, r1 <= r2 -> r2 <= r1 -> r1 = r2. Proof. intros r1 r2; generalize (Rlt_asym r1 r2); unfold Rle in |- *; intuition. Qed. Hint Resolve Rle_antisym: real. +Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2. +Proof. auto with real. Qed. + (**********) Lemma Rle_le_eq : forall r1 r2, r1 <= r2 /\ r2 <= r1 <-> r1 = r2. Proof. intuition. Qed. +Lemma Rge_ge_eq : forall r1 r2, r1 >= r2 /\ r2 >= r1 <-> r1 = r2. +Proof. + intuition. +Qed. + +(** *** Compatibility with equality *) + Lemma Rlt_eq_compat : forall r1 r2 r3 r4, r1 = r2 -> r2 < r4 -> r4 = r3 -> r1 < r3. Proof. intros x x' y y'; intros; replace x with x'; replace y with y'; assumption. Qed. -(**********) +Lemma Rgt_eq_compat : + forall r1 r2 r3 r4, r1 = r2 -> r2 > r4 -> r4 = r3 -> r1 > r3. +Proof. intros; red; apply Rlt_eq_compat with (r2:=r4) (r4:=r2); auto. Qed. + +(** *** Transitivity *) + +(** Remark: [Rlt_trans] is an axiom *) + Lemma Rle_trans : forall r1 r2 r3, r1 <= r2 -> r2 <= r3 -> r1 <= r3. Proof. generalize trans_eq Rlt_trans Rlt_eq_compat. @@ -206,6 +284,12 @@ Proof. intuition eauto 2. Qed. +Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. +Proof. eauto using Rle_trans with real2. Qed. + +Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. +Proof. eauto using Rlt_trans with real2. Qed. + (**********) Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3. Proof. @@ -214,14 +298,19 @@ Proof. intuition eauto 2. Qed. -(**********) Lemma Rlt_le_trans : forall r1 r2 r3, r1 < r2 -> r2 <= r3 -> r1 < r3. Proof. generalize Rlt_trans Rlt_eq_compat; unfold Rle in |- *; intuition eauto 2. Qed. +Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. +Proof. eauto using Rlt_le_trans with real2. Qed. + +Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. +Proof. eauto using Rle_lt_trans with real2. Qed. + +(** *** (Classical) decidability *) -(** Decidability of the order *) Lemma Rlt_dec : forall r1 r2, {r1 < r2} + {~ r1 < r2}. Proof. intros; generalize (total_order_T r1 r2) (Rlt_dichotomy_converse r1 r2); @@ -236,35 +325,43 @@ Proof. Qed. Lemma Rgt_dec : forall r1 r2, {r1 > r2} + {~ r1 > r2}. -Proof. - intros; unfold Rgt in |- *; intros; apply Rlt_dec. -Qed. +Proof. do 2 intro; apply Rlt_dec. Qed. Lemma Rge_dec : forall r1 r2, {r1 >= r2} + {~ r1 >= r2}. -Proof. - intros; generalize (Rle_dec r2 r1); intuition. -Qed. +Proof. intros; edestruct Rle_dec; [left|right]; eauto with real2. Qed. Lemma Rlt_le_dec : forall r1 r2, {r1 < r2} + {r2 <= r1}. Proof. intros; generalize (total_order_T r1 r2); intuition. Qed. +Lemma Rgt_ge_dec : forall r1 r2, {r1 > r2} + {r2 >= r1}. +Proof. intros; edestruct Rlt_le_dec; [left|right]; eauto with real2. Qed. + Lemma Rle_lt_dec : forall r1 r2, {r1 <= r2} + {r2 < r1}. Proof. intros; generalize (total_order_T r1 r2); intuition. Qed. +Lemma Rge_gt_dec : forall r1 r2, {r1 >= r2} + {r2 > r1}. +Proof. intros; edestruct Rle_lt_dec; [left|right]; eauto with real2. Qed. + Lemma Rlt_or_le : forall r1 r2, r1 < r2 \/ r2 <= r1. Proof. intros n m; elim (Rle_lt_dec m n); auto with real. Qed. +Lemma Rgt_or_ge : forall r1 r2, r1 > r2 \/ r2 >= r1. +Proof. intros; edestruct Rlt_or_le; [left|right]; eauto with real2. Qed. + Lemma Rle_or_lt : forall r1 r2, r1 <= r2 \/ r2 < r1. Proof. intros n m; elim (Rlt_le_dec m n); auto with real. Qed. +Lemma Rge_or_gt : forall r1 r2, r1 >= r2 \/ r2 > r1. +Proof. intros; edestruct Rle_or_lt; [left|right]; eauto with real2. Qed. + Lemma Rle_lt_or_eq_dec : forall r1 r2, r1 <= r2 -> {r1 < r2} + {r1 = r2}. Proof. intros r1 r2 H; generalize (total_order_T r1 r2); intuition. @@ -277,19 +374,11 @@ Proof. intros n m p q; intros; generalize (Rlt_le_dec m q); intuition. Qed. -(****************************************************************) -(** * Field Lemmas *) -(* This part contains lemma involving the Fields operations *) -(****************************************************************) (*********************************************************) -(** ** Addition *) +(** ** Addition *) (*********************************************************) -Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. -Proof. - split; ring. -Qed. -Hint Resolve Rplus_ne: real v62. +(** Remark: [Rplus_0_l] is an axiom *) Lemma Rplus_0_r : forall r, r + 0 = r. Proof. @@ -297,14 +386,22 @@ Proof. Qed. Hint Resolve Rplus_0_r: real. +Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r. +Proof. + split; ring. +Qed. +Hint Resolve Rplus_ne: real v62. + (**********) + +(** Remark: [Rplus_opp_r] is an axiom *) + Lemma Rplus_opp_l : forall r, - r + r = 0. Proof. intro; ring. Qed. Hint Resolve Rplus_opp_l: real. - (**********) Lemma Rplus_opp_r_uniq : forall r1 r2, r1 + r2 = 0 -> r2 = - r1. Proof. @@ -313,7 +410,6 @@ Proof. rewrite Rplus_assoc; rewrite H; ring. Qed. -(*i New i*) Hint Resolve (f_equal (A:=R)): real. Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2. @@ -340,9 +436,31 @@ Proof. intros r b; pattern r at 2 in |- *; replace r with (r + 0); eauto with real. Qed. -(***********************************************************) -(** ** Multiplication *) -(***********************************************************) +(***********) +Lemma Rplus_eq_0_l : + forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. +Proof. + intros a b H [H0| H0] H1; auto with real. + absurd (0 < a + b). + rewrite H1; auto with real. + apply Rle_lt_trans with (a + 0). + rewrite Rplus_0_r in |- *; assumption. + auto using Rplus_lt_compat_l with real. + rewrite <- H0, Rplus_0_r in H1; assumption. +Qed. + +Lemma Rplus_eq_R0 : + forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0. +Proof. + intros a b; split. + apply Rplus_eq_0_l with b; auto with real. + apply Rplus_eq_0_l with a; auto with real. + rewrite Rplus_comm; auto with real. +Qed. + +(*********************************************************) +(** ** Multiplication *) +(*********************************************************) (**********) Lemma Rinv_r : forall r, r <> 0 -> r * / r = 1. @@ -362,7 +480,6 @@ Proof. Qed. Hint Resolve Rinv_l_sym Rinv_r_sym: real. - (**********) Lemma Rmult_0_r : forall r, r * 0 = 0. Proof. @@ -397,7 +514,7 @@ Proof. auto with real. Qed. -(*i OLD i*)Hint Resolve Rmult_eq_compat_l: v62. +(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62. (**********) Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2. @@ -438,7 +555,6 @@ Proof. auto with real. Qed. - (**********) Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0. Proof. @@ -454,6 +570,10 @@ Proof. Qed. Hint Resolve Rmult_integral_contrapositive: real. +Lemma Rmult_integral_contrapositive_currified : + forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0. +Proof. auto using Rmult_integral_contrapositive. Qed. + (**********) Lemma Rmult_plus_distr_r : forall r1 r2 r3, (r1 + r2) * r3 = r1 * r3 + r2 * r3. @@ -461,7 +581,9 @@ Proof. intros; ring. Qed. -(** ** Square function *) +(*********************************************************) +(** ** Square function *) +(*********************************************************) (***********) Definition Rsqr r : R := r * r. @@ -479,7 +601,7 @@ Lemma Rsqr_0_uniq : forall r, Rsqr r = 0 -> r = 0. Qed. (*********************************************************) -(** ** Opposite *) +(** ** Opposite *) (*********************************************************) (**********) @@ -526,8 +648,9 @@ Proof. Qed. Hint Resolve Ropp_plus_distr: real. - -(** ** Opposite and multiplication *) +(*********************************************************) +(** ** Opposite and multiplication *) +(*********************************************************) Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2). Proof. @@ -547,7 +670,9 @@ Proof. intros; ring. Qed. -(** ** Substraction *) +(*********************************************************) +(** ** Substraction *) +(*********************************************************) Lemma Rminus_0_r : forall r, r - 0 = r. Proof. @@ -622,7 +747,6 @@ Proof. Qed. Hint Resolve Rminus_not_eq_right: real. - (**********) Lemma Rmult_minus_distr_l : forall r1 r2 r3, r1 * (r2 - r3) = r1 * r2 - r1 * r3. @@ -630,7 +754,10 @@ Proof. intros; ring. Qed. -(** ** Inverse *) +(*********************************************************) +(** ** Inverse *) +(*********************************************************) + Lemma Rinv_1 : / 1 = 1. Proof. field. @@ -694,28 +821,28 @@ Proof. ring. Qed. -(** * Field operations and order *) +(*********************************************************) +(** ** Order and addition *) +(*********************************************************) + +(** *** Compatibility *) -(** ** Order and addition *) +(** Remark: [Rplus_lt_compat_l] is an axiom *) +Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. +Proof. eauto using Rplus_lt_compat_l with real2. Qed. +Hint Resolve Rplus_gt_compat_l: real. + +(**********) Lemma Rplus_lt_compat_r : forall r r1 r2, r1 < r2 -> r1 + r < r2 + r. Proof. intros. rewrite (Rplus_comm r1 r); rewrite (Rplus_comm r2 r); auto with real. Qed. - Hint Resolve Rplus_lt_compat_r: real. -(**********) -Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. -Proof. - intros; cut (- r + r + r1 < - r + r + r2). - rewrite Rplus_opp_l. - elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1; - auto with zarith real. - rewrite Rplus_assoc; rewrite Rplus_assoc; - apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H). -Qed. +Lemma Rplus_gt_compat_r : forall r r1 r2, r1 > r2 -> r1 + r > r2 + r. +Proof. do 3 intro; apply Rplus_lt_compat_r. Qed. (**********) Lemma Rplus_le_compat_l : forall r r1 r2, r1 <= r2 -> r + r1 <= r + r2. @@ -725,6 +852,10 @@ Proof. right; rewrite <- H0; auto with zarith real. Qed. +Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. +Proof. auto using Rplus_le_compat_l with real2. Qed. +Hint Resolve Rplus_ge_compat_l: real. + (**********) Lemma Rplus_le_compat_r : forall r r1 r2, r1 <= r2 -> r1 + r <= r2 + r. Proof. @@ -735,23 +866,8 @@ Qed. Hint Resolve Rplus_le_compat_l Rplus_le_compat_r: real. -(**********) -Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. -Proof. - unfold Rle in |- *; intros; elim H; intro. - left; apply (Rplus_lt_reg_r r r1 r2 H0). - right; apply (Rplus_eq_reg_l r r1 r2 H0). -Qed. - -(**********) -Lemma sum_inequa_Rle_lt : - forall a x b c y d:R, - a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. -Proof. - intros; split. - apply Rlt_le_trans with (a + y); auto with real. - apply Rlt_le_trans with (b + y); auto with real. -Qed. +Lemma Rplus_ge_compat_r : forall r r1 r2, r1 >= r2 -> r1 + r >= r2 + r. +Proof. auto using Rplus_le_compat_r with real2. Qed. (*********) Lemma Rplus_lt_compat : @@ -766,6 +882,16 @@ Proof. intros; apply Rle_trans with (r2 + r3); auto with real. Qed. +Hint Immediate Rplus_lt_compat Rplus_le_compat: real. + +Lemma Rplus_gt_compat : + forall r1 r2 r3 r4, r1 > r2 -> r3 > r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_lt_compat with real2. Qed. + +Lemma Rplus_ge_compat : + forall r1 r2 r3 r4, r1 >= r2 -> r3 >= r4 -> r1 + r3 >= r2 + r4. +Proof. auto using Rplus_le_compat with real2. Qed. + (*********) Lemma Rplus_lt_le_compat : forall r1 r2 r3 r4, r1 < r2 -> r3 <= r4 -> r1 + r3 < r2 + r4. @@ -773,19 +899,133 @@ Proof. intros; apply Rlt_le_trans with (r2 + r3); auto with real. Qed. -(*********) Lemma Rplus_le_lt_compat : forall r1 r2 r3 r4, r1 <= r2 -> r3 < r4 -> r1 + r3 < r2 + r4. Proof. intros; apply Rle_lt_trans with (r2 + r3); auto with real. Qed. -Hint Immediate Rplus_lt_compat Rplus_le_compat Rplus_lt_le_compat - Rplus_le_lt_compat: real. +Hint Immediate Rplus_lt_le_compat Rplus_le_lt_compat: real. -(** ** Order and Opposite *) +Lemma Rplus_gt_ge_compat : + forall r1 r2 r3 r4, r1 > r2 -> r3 >= r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_lt_le_compat with real2. Qed. + +Lemma Rplus_ge_gt_compat : + forall r1 r2 r3 r4, r1 >= r2 -> r3 > r4 -> r1 + r3 > r2 + r4. +Proof. auto using Rplus_le_lt_compat with real2. Qed. (**********) +Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; apply Rlt_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; + assumption ]. +Qed. + +Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; apply Rle_lt_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; + assumption ]. +Qed. + +Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. +Proof. + intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; + assumption. +Qed. + +Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. +Proof. + intros x y; intros; apply Rle_trans with x; + [ assumption + | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption ]. +Qed. + +(**********) +Lemma sum_inequa_Rle_lt : + forall a x b c y d:R, + a <= x -> x < b -> c < y -> y <= d -> a + c < x + y < b + d. +Proof. + intros; split. + apply Rlt_le_trans with (a + y); auto with real. + apply Rlt_le_trans with (b + y); auto with real. +Qed. + +(** *** Cancellation *) + +Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. +Proof. + intros; cut (- r + r + r1 < - r + r + r2). + rewrite Rplus_opp_l. + elim (Rplus_ne r1); elim (Rplus_ne r2); intros; rewrite <- H3; rewrite <- H1; + auto with zarith real. + rewrite Rplus_assoc; rewrite Rplus_assoc; + apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H). +Qed. + +Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. +Proof. + unfold Rle in |- *; intros; elim H; intro. + left; apply (Rplus_lt_reg_r r r1 r2 H0). + right; apply (Rplus_eq_reg_l r r1 r2 H0). +Qed. + +Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. +Proof. + unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H). +Qed. + +Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. +Proof. + intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real. +Qed. + +(**********) +Lemma Rplus_le_reg_pos_r : + forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. +Proof. + intros x y z; intros; apply Rle_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_lt_reg_pos_r : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. +Proof. + intros x y z; intros; apply Rle_lt_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_ge_reg_neg_r : + forall r1 r2 r3, 0 >= r2 -> r1 + r2 >= r3 -> r1 >= r3. +Proof. + intros x y z; intros; apply Rge_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l; + assumption + | assumption ]. +Qed. + +Lemma Rplus_gt_reg_neg_r : forall r1 r2 r3, 0 >= r2 -> r1 + r2 > r3 -> r1 > r3. +Proof. + intros x y z; intros; apply Rge_gt_trans with (x + y); + [ pattern x at 1; rewrite <- (Rplus_0_r x); apply Rplus_ge_compat_l; + assumption + | assumption ]. +Qed. + +(*********************************************************) +(** ** Order and opposite *) +(*********************************************************) + +(** *** Contravariant compatibility *) + Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. Proof. unfold Rgt in |- *; intros. @@ -798,27 +1038,22 @@ Proof. Qed. Hint Resolve Ropp_gt_lt_contravar. -(**********) Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2. Proof. unfold Rgt in |- *; auto with real. Qed. Hint Resolve Ropp_lt_gt_contravar: real. -Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. -Proof. - intros x y H'. - rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - auto with real. -Qed. -Hint Immediate Ropp_lt_cancel: real. - +(**********) Lemma Ropp_lt_contravar : forall r1 r2, r2 < r1 -> - r1 < - r2. Proof. auto with real. Qed. Hint Resolve Ropp_lt_contravar: real. +Lemma Ropp_gt_contravar : forall r1 r2, r2 > r1 -> - r1 > - r2. +Proof. auto with real. Qed. + (**********) Lemma Ropp_le_ge_contravar : forall r1 r2, r1 <= r2 -> - r1 >= - r2. Proof. @@ -826,27 +1061,21 @@ Proof. Qed. Hint Resolve Ropp_le_ge_contravar: real. -Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. +Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. Proof. - intros x y H. - elim H; auto with real. - intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); - rewrite H1; auto with real. + unfold Rge in |- *; intros r1 r2 [H| H]; auto with real. Qed. -Hint Immediate Ropp_le_cancel: real. +Hint Resolve Ropp_ge_le_contravar: real. +(**********) Lemma Ropp_le_contravar : forall r1 r2, r2 <= r1 -> - r1 <= - r2. Proof. intros r1 r2 H; elim H; auto with real. Qed. Hint Resolve Ropp_le_contravar: real. -(**********) -Lemma Ropp_ge_le_contravar : forall r1 r2, r1 >= r2 -> - r1 <= - r2. -Proof. - unfold Rge in |- *; intros r1 r2 [H| H]; auto with real. -Qed. -Hint Resolve Ropp_ge_le_contravar: real. +Lemma Ropp_ge_contravar : forall r1 r2, r2 >= r1 -> - r1 >= - r2. +Proof. auto using Ropp_le_contravar with real. Qed. (**********) Lemma Ropp_0_lt_gt_contravar : forall r, 0 < r -> 0 > - r. @@ -855,7 +1084,6 @@ Proof. Qed. Hint Resolve Ropp_0_lt_gt_contravar: real. -(**********) Lemma Ropp_0_gt_lt_contravar : forall r, 0 > r -> 0 < - r. Proof. intros; replace 0 with (-0); auto with real. @@ -868,7 +1096,6 @@ Proof. intros; rewrite <- Ropp_0; auto with real. Qed. -(**********) Lemma Ropp_gt_lt_0_contravar : forall r, r < 0 -> - r > 0. Proof. intros; rewrite <- Ropp_0; auto with real. @@ -882,40 +1109,57 @@ Proof. Qed. Hint Resolve Ropp_0_le_ge_contravar: real. -(**********) Lemma Ropp_0_ge_le_contravar : forall r, 0 >= r -> 0 <= - r. Proof. intros; replace 0 with (-0); auto with real. Qed. Hint Resolve Ropp_0_ge_le_contravar: real. -(** ** Order and multiplication *) +(** *** Cancellation *) -Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. +Lemma Ropp_lt_cancel : forall r1 r2, - r2 < - r1 -> r1 < r2. Proof. - intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. + intros x y H'. + rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); + auto with real. Qed. -Hint Resolve Rmult_lt_compat_r. +Hint Immediate Ropp_lt_cancel: real. -Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. +Lemma Ropp_gt_cancel : forall r1 r2, - r2 > - r1 -> r1 > r2. +Proof. auto using Ropp_lt_cancel with real2. Qed. + +Lemma Ropp_le_cancel : forall r1 r2, - r2 <= - r1 -> r1 <= r2. Proof. - intros z x y H H0. - case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. - rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto. - generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False; - generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); - intro; apply (Rlt_irrefl (z * x)); auto. + intros x y H. + elim H; auto with real. + intro H1; rewrite <- (Ropp_involutive x); rewrite <- (Ropp_involutive y); + rewrite H1; auto with real. Qed. +Hint Immediate Ropp_le_cancel: real. +Lemma Ropp_ge_cancel : forall r1 r2, - r2 >= - r1 -> r1 >= r2. +Proof. auto using Ropp_le_cancel with real2. Qed. -Lemma Rmult_lt_gt_compat_neg_l : - forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. +(*********************************************************) +(** ** Order and multiplication *) +(*********************************************************) + +(** Remark: [Rmult_lt_compat_l] is an axiom *) + +(** *** Covariant compatibility *) + +Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r. Proof. - intros; replace r with (- - r); auto with real. - rewrite (Ropp_mult_distr_l_reverse (- r)); - rewrite (Ropp_mult_distr_l_reverse (- r)). - apply Ropp_lt_gt_contravar; auto with real. + intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real. Qed. +Hint Resolve Rmult_lt_compat_r. + +Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r. +Proof. eauto using Rmult_lt_compat_r with real2. Qed. + +Lemma Rmult_gt_compat_l : forall r r1 r2, r > 0 -> r1 > r2 -> r * r1 > r * r2. +Proof. eauto using Rmult_lt_compat_l with real2. Qed. +Hint Resolve Rplus_gt_compat_l: real. (**********) Lemma Rmult_le_compat_l : @@ -935,17 +1179,58 @@ Proof. Qed. Hint Resolve Rmult_le_compat_r: real. -Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. +Lemma Rmult_ge_compat_l : + forall r r1 r2, r >= 0 -> r1 >= r2 -> r * r1 >= r * r2. +Proof. eauto using Rmult_le_compat_l with real2. Qed. + +Lemma Rmult_ge_compat_r : + forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. +Proof. eauto using Rmult_le_compat_r with real2. Qed. + +(**********) +Lemma Rmult_le_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. Proof. - intros z x y H H0; case H0; auto with real. - intros H1; apply Rlt_le. - apply Rmult_lt_reg_l with (r := z); auto. - intros H1; replace x with (/ z * (z * x)); auto with real. - replace y with (/ z * (z * y)). - rewrite H1; auto with real. - rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. - rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + intros x y z t H' H'0 H'1 H'2. + apply Rle_trans with (r2 := x * t); auto with real. + repeat rewrite (fun x => Rmult_comm x t). + apply Rmult_le_compat_l; auto. + apply Rle_trans with z; auto. Qed. +Hint Resolve Rmult_le_compat: real. + +Lemma Rmult_ge_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. +Proof. auto with real real2. Qed. + +Lemma Rmult_gt_0_lt_compat : + forall r1 r2 r3 r4, + r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Proof. + intros; apply Rlt_trans with (r2 * r3); auto with real. +Qed. + +(*********) +Lemma Rmult_le_0_lt_compat : + forall r1 r2 r3 r4, + 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Proof. + intros; apply Rle_lt_trans with (r2 * r3); + [ apply Rmult_le_compat_r; [ assumption | left; assumption ] + | apply Rmult_lt_compat_l; + [ apply Rle_lt_trans with r1; assumption | assumption ] ]. +Qed. + +(*********) +Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. +Proof. intros; replace 0 with (0 * r2); auto with real. Qed. + +Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. +Proof Rmult_lt_0_compat. + +(** *** Contravariant compatibility *) Lemma Rmult_le_compat_neg_l : forall r r1 r2, r <= 0 -> r1 <= r2 -> r * r2 <= r * r1. @@ -963,35 +1248,45 @@ Proof. Qed. Hint Resolve Rmult_le_ge_compat_neg_l: real. -Lemma Rmult_le_compat : - forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 <= r2 -> r3 <= r4 -> r1 * r3 <= r2 * r4. +Lemma Rmult_lt_gt_compat_neg_l : + forall r r1 r2, r < 0 -> r1 < r2 -> r * r1 > r * r2. Proof. - intros x y z t H' H'0 H'1 H'2. - apply Rle_trans with (r2 := x * t); auto with real. - repeat rewrite (fun x => Rmult_comm x t). - apply Rmult_le_compat_l; auto. - apply Rle_trans with z; auto. + intros; replace r with (- - r); auto with real. + rewrite (Ropp_mult_distr_l_reverse (- r)); + rewrite (Ropp_mult_distr_l_reverse (- r)). + apply Ropp_lt_gt_contravar; auto with real. Qed. -Hint Resolve Rmult_le_compat: real. -Lemma Rmult_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 > 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +(** *** Cancellation *) + +Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. Proof. - intros; apply Rlt_trans with (r2 * r3); auto with real. + intros z x y H H0. + case (Rtotal_order x y); intros Eq0; auto; elim Eq0; clear Eq0; intros Eq0. + rewrite Eq0 in H0; elimtype False; apply (Rlt_irrefl (z * y)); auto. + generalize (Rmult_lt_compat_l z y x H Eq0); intro; elimtype False; + generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1); + intro; apply (Rlt_irrefl (z * x)); auto. Qed. -(*********) -Lemma Rmult_ge_0_gt_0_lt_compat : - forall r1 r2 r3 r4, - r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. +Lemma Rmult_gt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> r1 < r2. +Proof. eauto using Rmult_lt_reg_l with real2. Qed. + +Lemma Rmult_le_reg_l : forall r r1 r2, 0 < r -> r * r1 <= r * r2 -> r1 <= r2. Proof. - intros; apply Rle_lt_trans with (r2 * r3); auto with real. + intros z x y H H0; case H0; auto with real. + intros H1; apply Rlt_le. + apply Rmult_lt_reg_l with (r := z); auto. + intros H1; replace x with (/ z * (z * x)); auto with real. + replace y with (/ z * (z * y)). + rewrite H1; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. + rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real. Qed. - -(** ** Order and Substractions *) +(*********************************************************) +(** ** Order and substraction *) +(*********************************************************) Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. Proof. @@ -1002,12 +1297,27 @@ Proof. Qed. Hint Resolve Rlt_minus: real. +Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. +Proof. + intros; apply (Rplus_lt_reg_r r2). + replace (r2 + (r1 - r2)) with r1. + replace (r2 + 0) with r2; auto with real. + ring. +Qed. + (**********) Lemma Rle_minus : forall r1 r2, r1 <= r2 -> r1 - r2 <= 0. Proof. destruct 1; unfold Rle in |- *; auto with real. Qed. +Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. +Proof. + destruct 1. + auto using Rgt_minus, Rgt_ge. + right; auto using Rminus_diag_eq with real2. +Qed. + (**********) Lemma Rminus_lt : forall r1 r2, r1 - r2 < 0 -> r1 < r2. Proof. @@ -1016,6 +1326,14 @@ Proof. ring. Qed. +Lemma Rminus_gt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. +Proof. + intros; replace r2 with (0 + r2); auto with real. + replace r1 with (r1 - r2 + r2). + apply Rplus_gt_compat_r; assumption. + ring. +Qed. + (**********) Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2. Proof. @@ -1024,6 +1342,14 @@ Proof. ring. Qed. +Lemma Rminus_ge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. +Proof. + intros; replace r2 with (0 + r2); auto with real. + replace r1 with (r1 - r2 + r2). + apply Rplus_ge_compat_r; assumption. + ring. +Qed. + (**********) Lemma tech_Rplus : forall r (s:R), 0 <= r -> 0 < s -> r + s <> 0. Proof. @@ -1032,8 +1358,9 @@ Proof. Qed. Hint Immediate tech_Rplus: real. - -(** ** Order and the square function *) +(*********************************************************) +(** ** Order and square function *) +(*********************************************************) Lemma Rle_0_sqr : forall r, 0 <= Rsqr r. Proof. @@ -1053,7 +1380,26 @@ Proof. Qed. Hint Resolve Rle_0_sqr Rlt_0_sqr: real. -(** ** Zero is less than one *) +(***********) +Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0. +Proof. + intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b); + auto with real. +Qed. + +Lemma Rplus_sqr_eq_0 : + forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0. +Proof. + intros a b; split. + apply Rplus_sqr_eq_0_l with b; auto with real. + apply Rplus_sqr_eq_0_l with a; auto with real. + rewrite Rplus_comm; auto with real. +Qed. + +(*********************************************************) +(** ** Zero is less than one *) +(*********************************************************) + Lemma Rlt_0_1 : 0 < 1. Proof. replace 1 with (Rsqr 1); auto with real. @@ -1067,7 +1413,10 @@ Proof. exact Rlt_0_1. Qed. -(** ** Order and inverse *) +(*********************************************************) +(** ** Order and inverse *) +(*********************************************************) + Lemma Rinv_0_lt_compat : forall r, 0 < r -> 0 < / r. Proof. intros; apply Rnot_le_lt; red in |- *; intros. @@ -1116,68 +1465,9 @@ Proof. Qed. Hint Resolve Rinv_1_lt_contravar: real. -(********************************************************) -(** * Greater *) -(********************************************************) - -(**********) -Lemma Rge_antisym : forall r1 r2, r1 >= r2 -> r2 >= r1 -> r1 = r2. -Proof. - intros; apply Rle_antisym; auto with real. -Qed. - -(**********) -Lemma Rnot_lt_ge : forall r1 r2, ~ r1 < r2 -> r1 >= r2. -Proof. - intros; unfold Rge in |- *; elim (Rtotal_order r1 r2); intro. - absurd (r1 < r2); trivial. - case H0; auto. -Qed. - -(**********) -Lemma Rnot_lt_le : forall r1 r2, ~ r1 < r2 -> r2 <= r1. -Proof. - intros; apply Rge_le; apply Rnot_lt_ge; assumption. -Qed. - -(**********) -Lemma Rnot_gt_le : forall r1 r2, ~ r1 > r2 -> r1 <= r2. -Proof. - intros r1 r2 H; apply Rge_le. - exact (Rnot_lt_ge r2 r1 H). -Qed. - -(**********) -Lemma Rgt_ge : forall r1 r2, r1 > r2 -> r1 >= r2. -Proof. - red in |- *; auto with real. -Qed. - - -(**********) -Lemma Rge_gt_trans : forall r1 r2 r3, r1 >= r2 -> r2 > r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rlt_le_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rgt_ge_trans : forall r1 r2 r3, r1 > r2 -> r2 >= r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rle_lt_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rgt_trans : forall r1 r2 r3, r1 > r2 -> r2 > r3 -> r1 > r3. -Proof. - unfold Rgt in |- *; intros; apply Rlt_trans with r2; auto with real. -Qed. - -(**********) -Lemma Rge_trans : forall r1 r2 r3, r1 >= r2 -> r2 >= r3 -> r1 >= r3. -Proof. - intros; apply Rle_ge. - apply Rle_trans with r2; auto with real. -Qed. +(*********************************************************) +(** ** Miscellaneous *) +(*********************************************************) (**********) Lemma Rle_lt_0_plus_1 : forall r, 0 <= r -> 0 < r + 1. @@ -1203,121 +1493,9 @@ Proof. pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real. Qed. -(***********) -Lemma Rplus_gt_compat_l : forall r r1 r2, r1 > r2 -> r + r1 > r + r2. -Proof. - unfold Rgt in |- *; auto with real. -Qed. -Hint Resolve Rplus_gt_compat_l: real. - -(***********) -Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. -Proof. - unfold Rgt in |- *; intros; apply (Rplus_lt_reg_r r r2 r1 H). -Qed. - -(***********) -Lemma Rplus_ge_compat_l : forall r r1 r2, r1 >= r2 -> r + r1 >= r + r2. -Proof. - intros; apply Rle_ge; auto with real. -Qed. -Hint Resolve Rplus_ge_compat_l: real. - -(***********) -Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. -Proof. - intros; apply Rle_ge; apply Rplus_le_reg_l with r; auto with real. -Qed. - -(***********) -Lemma Rmult_ge_compat_r : - forall r r1 r2, r >= 0 -> r1 >= r2 -> r1 * r >= r2 * r. -Proof. - intros; apply Rle_ge; apply Rmult_le_compat_r; apply Rge_le; assumption. -Qed. - -(***********) -Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0. -Proof. - intros; replace 0 with (r2 - r2); auto with real. - unfold Rgt, Rminus in |- *; auto with real. -Qed. - -(*********) -Lemma minus_Rgt : forall r1 r2, r1 - r2 > 0 -> r1 > r2. -Proof. - intros; replace r2 with (r2 + 0); auto with real. - intros; replace r1 with (r2 + (r1 - r2)); auto with real. -Qed. - -(**********) -Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0. -Proof. - unfold Rge in |- *; intros; elim H; intro. - left; apply (Rgt_minus r1 r2 H0). - right; apply (Rminus_diag_eq r1 r2 H0). -Qed. - -(*********) -Lemma minus_Rge : forall r1 r2, r1 - r2 >= 0 -> r1 >= r2. -Proof. - intros; replace r2 with (r2 + 0); auto with real. - intros; replace r1 with (r2 + (r1 - r2)); auto with real. -Qed. - - -(*********) -Lemma Rmult_gt_0_compat : forall r1 r2, r1 > 0 -> r2 > 0 -> r1 * r2 > 0. -Proof. - unfold Rgt in |- *; intros. - replace 0 with (0 * r2); auto with real. -Qed. - -(*********) -Lemma Rmult_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 * r2. -Proof Rmult_gt_0_compat. - -(***********) -Lemma Rplus_eq_0_l : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0. -Proof. - intros a b [H| H] H0 H1; auto with real. - absurd (0 < a + b). - rewrite H1; auto with real. - replace 0 with (0 + 0); auto with real. -Qed. - - -Lemma Rplus_eq_R0 : - forall r1 r2, 0 <= r1 -> 0 <= r2 -> r1 + r2 = 0 -> r1 = 0 /\ r2 = 0. -Proof. - intros a b; split. - apply Rplus_eq_0_l with b; auto with real. - apply Rplus_eq_0_l with a; auto with real. - rewrite Rplus_comm; auto with real. -Qed. - - -(***********) -Lemma Rplus_sqr_eq_0_l : forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0. -Proof. - intros a b; intros; apply Rsqr_0_uniq; apply Rplus_eq_0_l with (Rsqr b); - auto with real. -Qed. - -Lemma Rplus_sqr_eq_0 : - forall r1 r2, Rsqr r1 + Rsqr r2 = 0 -> r1 = 0 /\ r2 = 0. -Proof. - intros a b; split. - apply Rplus_sqr_eq_0_l with b; auto with real. - apply Rplus_sqr_eq_0_l with a; auto with real. - rewrite Rplus_comm; auto with real. -Qed. - - -(**********************************************************) -(** * Injection from [N] to [R] *) -(**********************************************************) +(*********************************************************) +(** ** Injection from [N] to [R] *) +(*********************************************************) (**********) Lemma S_INR : forall n:nat, INR (S n) = INR n + 1. @@ -1482,9 +1660,9 @@ Proof. Qed. Hint Resolve not_1_INR: real. -(**********************************************************) -(** * Injection from [Z] to [R] *) -(**********************************************************) +(*********************************************************) +(** ** Injection from [Z] to [R] *) +(*********************************************************) (**********) @@ -1708,32 +1886,6 @@ Proof. apply H3; apply single_z_r_R1 with r; trivial. Qed. -(*****************************************************************) -(** * Definitions of new types *) -(*****************************************************************) - -Record nonnegreal : Type := mknonnegreal - {nonneg :> R; cond_nonneg : 0 <= nonneg}. - -Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. - -Record nonposreal : Type := mknonposreal - {nonpos :> R; cond_nonpos : nonpos <= 0}. - -Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. - -Record nonzeroreal : Type := mknonzeroreal - {nonzero :> R; cond_nonzero : nonzero <> 0}. - -(**********) -Lemma prod_neq_R0 : forall r1 r2, r1 <> 0 -> r2 <> 0 -> r1 * r2 <> 0. -Proof. - intros x y; intros; red in |- *; intro; generalize (Rmult_integral x y H1); - intro; elim H2; intro; - [ rewrite H3 in H; elim H | rewrite H3 in H0; elim H0 ]; - reflexivity. -Qed. - (*********) Lemma Rmult_le_pos : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 * r2. Proof. @@ -1754,64 +1906,15 @@ Proof. [ apply not_O_INR; discriminate | unfold INR in |- *; ring ]. Qed. -(**********************************************************) -(** * Other rules about < and <= *) -(**********************************************************) - -Lemma Rplus_lt_0_compat : forall r1 r2, 0 < r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; apply Rlt_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; - assumption ]. -Qed. - -Lemma Rplus_le_lt_0_compat : forall r1 r2, 0 <= r1 -> 0 < r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; apply Rle_lt_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_lt_compat_l; - assumption ]. -Qed. - -Lemma Rplus_lt_le_0_compat : forall r1 r2, 0 < r1 -> 0 <= r2 -> 0 < r1 + r2. -Proof. - intros x y; intros; rewrite <- Rplus_comm; apply Rplus_le_lt_0_compat; - assumption. -Qed. - -Lemma Rplus_le_le_0_compat : forall r1 r2, 0 <= r1 -> 0 <= r2 -> 0 <= r1 + r2. -Proof. - intros x y; intros; apply Rle_trans with x; - [ assumption - | pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption ]. -Qed. - -Lemma plus_le_is_le : forall r1 r2 r3, 0 <= r2 -> r1 + r2 <= r3 -> r1 <= r3. -Proof. - intros x y z; intros; apply Rle_trans with (x + y); - [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption - | assumption ]. -Qed. - -Lemma plus_lt_is_lt : forall r1 r2 r3, 0 <= r2 -> r1 + r2 < r3 -> r1 < r3. -Proof. - intros x y z; intros; apply Rle_lt_trans with (x + y); - [ pattern x at 1 in |- *; rewrite <- (Rplus_0_r x); apply Rplus_le_compat_l; - assumption - | assumption ]. -Qed. +(*********************************************************) +(** ** Other rules about < and <= *) +(*********************************************************) -Lemma Rmult_le_0_lt_compat : +Lemma Rmult_ge_0_gt_0_lt_compat : forall r1 r2 r3 r4, - 0 <= r1 -> 0 <= r3 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. + r3 >= 0 -> r2 > 0 -> r1 < r2 -> r3 < r4 -> r1 * r3 < r2 * r4. Proof. - intros; apply Rle_lt_trans with (r2 * r3); - [ apply Rmult_le_compat_r; [ assumption | left; assumption ] - | apply Rmult_lt_compat_l; - [ apply Rle_lt_trans with r1; assumption | assumption ] ]. + intros; apply Rle_lt_trans with (r2 * r3); auto with real. Qed. Lemma le_epsilon : @@ -1862,3 +1965,28 @@ Lemma completeness_weak : Proof. intros; elim (completeness E H H0); intros; split with x; assumption. Qed. + +(*********************************************************) +(** * Definitions of new types *) +(*********************************************************) + +Record nonnegreal : Type := mknonnegreal + {nonneg :> R; cond_nonneg : 0 <= nonneg}. + +Record posreal : Type := mkposreal {pos :> R; cond_pos : 0 < pos}. + +Record nonposreal : Type := mknonposreal + {nonpos :> R; cond_nonpos : nonpos <= 0}. + +Record negreal : Type := mknegreal {neg :> R; cond_neg : neg < 0}. + +Record nonzeroreal : Type := mknonzeroreal + {nonzero :> R; cond_nonzero : nonzero <> 0}. + +(** Compatibility *) + +Notation prod_neq_R0 := Rmult_integral_contrapositive_currified (only parsing). +Notation minus_Rgt := Rminus_gt (only parsing). +Notation minus_Rge := Rminus_ge (only parsing). +Notation plus_le_is_le := Rplus_le_reg_pos_r (only parsing). +Notation plus_lt_is_lt := Rplus_lt_reg_pos_r (only parsing). diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 3447aa0e4..63b8928fb 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -22,6 +22,8 @@ Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) Bind Scope R_scope with R. +Open Local Scope R_scope. + Parameter R0 : R. Parameter R1 : R. Parameter Rplus : R -> R -> R. @@ -38,33 +40,33 @@ Notation "/ x" := (Rinv x) : R_scope. Infix "<" := Rlt : R_scope. -(*i*******************************************************i*) +(***********************************************************) (**********) -Definition Rgt (r1 r2:R) : Prop := (r2 < r1)%R. +Definition Rgt (r1 r2:R) : Prop := r2 < r1. (**********) -Definition Rle (r1 r2:R) : Prop := (r1 < r2)%R \/ r1 = r2. +Definition Rle (r1 r2:R) : Prop := r1 < r2 \/ r1 = r2. (**********) Definition Rge (r1 r2:R) : Prop := Rgt r1 r2 \/ r1 = r2. (**********) -Definition Rminus (r1 r2:R) : R := (r1 + - r2)%R. +Definition Rminus (r1 r2:R) : R := r1 + - r2. (**********) -Definition Rdiv (r1 r2:R) : R := (r1 * / r2)%R. +Definition Rdiv (r1 r2:R) : R := r1 * / r2. (**********) Infix "-" := Rminus : R_scope. -Infix "/" := Rdiv : R_scope. +Infix "/" := Rdiv : R_scope. Infix "<=" := Rle : R_scope. Infix ">=" := Rge : R_scope. -Infix ">" := Rgt : R_scope. +Infix ">" := Rgt : R_scope. -Notation "x <= y <= z" := ((x <= y)%R /\ (y <= z)%R) : R_scope. -Notation "x <= y < z" := ((x <= y)%R /\ (y < z)%R) : R_scope. -Notation "x < y < z" := ((x < y)%R /\ (y < z)%R) : R_scope. -Notation "x < y <= z" := ((x < y)%R /\ (y <= z)%R) : R_scope. +Notation "x <= y <= z" := (x <= y /\ y <= z) : R_scope. +Notation "x <= y < z" := (x <= y /\ y < z) : R_scope. +Notation "x < y < z" := (x < y /\ y < z) : R_scope. +Notation "x < y <= z" := (x < y /\ y <= z) : R_scope. |