diff options
Diffstat (limited to 'theories/Reals/RIneq.v')
| -rw-r--r-- | theories/Reals/RIneq.v | 145 |
1 files changed, 108 insertions, 37 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index b881250f..8dca0197 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -1,7 +1,7 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -43,7 +43,7 @@ Hint Immediate Rge_refl: rorders. Lemma Rlt_irrefl : forall r, ~ r < r. Proof. - generalize Rlt_asym. intuition eauto. + intros r H; eapply Rlt_asym; eauto. Qed. Hint Resolve Rlt_irrefl: real. @@ -64,7 +64,9 @@ Qed. (**********) Lemma Rlt_dichotomy_converse : forall r1 r2, r1 < r2 \/ r1 > r2 -> r1 <> r2. Proof. - generalize Rlt_not_eq Rgt_not_eq. intuition eauto. + intuition. + - apply Rlt_not_eq in H1. eauto. + - apply Rgt_not_eq in H1. eauto. Qed. Hint Resolve Rlt_dichotomy_converse: real. @@ -74,7 +76,7 @@ Hint Resolve Rlt_dichotomy_converse: real. Lemma Req_dec : forall r1 r2, r1 = r2 \/ r1 <> r2. Proof. intros; generalize (total_order_T r1 r2) Rlt_dichotomy_converse; - intuition eauto 3. + unfold not; intuition eauto 3. Qed. Hint Resolve Req_dec: real. @@ -175,7 +177,7 @@ Proof. eauto using Rnot_gt_ge with rorders. Qed. Lemma Rlt_not_le : forall r1 r2, r2 < r1 -> ~ r1 <= r2. Proof. generalize Rlt_asym Rlt_dichotomy_converse; unfold Rle. - intuition eauto 3. + unfold not; intuition eauto 3. Qed. Hint Immediate Rlt_not_le: real. @@ -407,11 +409,20 @@ Proof. rewrite Rplus_assoc; rewrite H; ring. Qed. -Hint Resolve (f_equal (A:=R)): real. +Definition f_equal_R := (f_equal (A:=R)). + +Hint Resolve f_equal_R : real. Lemma Rplus_eq_compat_l : forall r r1 r2, r1 = r2 -> r + r1 = r + r2. Proof. - auto with real. + intros r r1 r2. + apply f_equal. +Qed. + +Lemma Rplus_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 + r = r2 + r. +Proof. + intros r r1 r2. + apply (f_equal (fun v => v + r)). Qed. (*i Old i*)Hint Resolve Rplus_eq_compat_l: v62. @@ -427,6 +438,13 @@ Proof. Qed. Hint Resolve Rplus_eq_reg_l: real. +Lemma Rplus_eq_reg_r : forall r r1 r2, r1 + r = r2 + r -> r1 = r2. +Proof. + intros r r1 r2 H. + apply Rplus_eq_reg_l with r. + now rewrite 2!(Rplus_comm r). +Qed. + (**********) Lemma Rplus_0_r_uniq : forall r r1, r + r1 = r -> r1 = 0. Proof. @@ -664,6 +682,11 @@ Hint Resolve Ropp_plus_distr: real. (** ** Opposite and multiplication *) (*********************************************************) +Lemma Ropp_mult_distr_l : forall r1 r2, - (r1 * r2) = - r1 * r2. +Proof. + intros; ring. +Qed. + Lemma Ropp_mult_distr_l_reverse : forall r1 r2, - r1 * r2 = - (r1 * r2). Proof. intros; ring. @@ -677,13 +700,18 @@ Proof. Qed. Hint Resolve Rmult_opp_opp: real. +Lemma Ropp_mult_distr_r : forall r1 r2, - (r1 * r2) = r1 * - r2. +Proof. + intros; ring. +Qed. + Lemma Ropp_mult_distr_r_reverse : forall r1 r2, r1 * - r2 = - (r1 * r2). Proof. intros; ring. Qed. (*********************************************************) -(** ** Substraction *) +(** ** Subtraction *) (*********************************************************) Lemma Rminus_0_r : forall r, r - 0 = r. @@ -794,7 +822,7 @@ Hint Resolve Rinv_involutive: real. Lemma Rinv_mult_distr : forall r1 r2, r1 <> 0 -> r2 <> 0 -> / (r1 * r2) = / r1 * / r2. Proof. - intros; field; auto. + intros; field; auto. Qed. (*********) @@ -969,7 +997,7 @@ Qed. (** *** Cancellation *) -Lemma Rplus_lt_reg_r : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. +Lemma Rplus_lt_reg_l : forall r r1 r2, r + r1 < r + r2 -> r1 < r2. Proof. intros; cut (- r + r + r1 < - r + r + r2). rewrite Rplus_opp_l. @@ -979,10 +1007,17 @@ Proof. apply (Rplus_lt_compat_l (- r) (r + r1) (r + r2) H). Qed. +Lemma Rplus_lt_reg_r : forall r r1 r2, r1 + r < r2 + r -> r1 < r2. +Proof. + intros. + apply (Rplus_lt_reg_l r). + now rewrite 2!(Rplus_comm r). +Qed. + Lemma Rplus_le_reg_l : forall r r1 r2, r + r1 <= r + r2 -> r1 <= r2. Proof. unfold Rle; intros; elim H; intro. - left; apply (Rplus_lt_reg_r r r1 r2 H0). + left; apply (Rplus_lt_reg_l r r1 r2 H0). right; apply (Rplus_eq_reg_l r r1 r2 H0). Qed. @@ -995,7 +1030,7 @@ Qed. Lemma Rplus_gt_reg_l : forall r r1 r2, r + r1 > r + r2 -> r1 > r2. Proof. - unfold Rgt; intros; apply (Rplus_lt_reg_r r r2 r1 H). + unfold Rgt; intros; apply (Rplus_lt_reg_l r r2 r1 H). Qed. Lemma Rplus_ge_reg_l : forall r r1 r2, r + r1 >= r + r2 -> r1 >= r2. @@ -1047,12 +1082,10 @@ Qed. Lemma Ropp_gt_lt_contravar : forall r1 r2, r1 > r2 -> - r1 < - r2. Proof. unfold Rgt; intros. - apply (Rplus_lt_reg_r (r2 + r1)). - replace (r2 + r1 + - r1) with r2. - replace (r2 + r1 + - r2) with r1. - trivial. - ring. - ring. + apply (Rplus_lt_reg_l (r2 + r1)). + replace (r2 + r1 + - r1) with r2 by ring. + replace (r2 + r1 + - r2) with r1 by ring. + exact H. Qed. Hint Resolve Ropp_gt_lt_contravar. @@ -1324,19 +1357,22 @@ Qed. Lemma Rlt_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. + intros; apply (Rplus_lt_reg_l r2). + replace (r2 + (r1 - r2)) with r1 by ring. + now rewrite Rplus_0_r. 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. + intros; apply (Rplus_lt_reg_l r2). + replace (r2 + (r1 - r2)) with r1 by ring. + now rewrite Rplus_0_r. +Qed. + +Lemma Rlt_Rminus : forall a b:R, a < b -> 0 < b - a. +Proof. + intros a b; apply Rgt_minus. Qed. (**********) @@ -1368,6 +1404,9 @@ Proof. ring. Qed. +Lemma Rminus_gt_0_lt : forall a b, 0 < b - a -> a < b. +Proof. intro; intro; apply Rminus_gt. Qed. + (**********) Lemma Rminus_le : forall r1 r2, r1 - r2 <= 0 -> r1 <= r2. Proof. @@ -1625,7 +1664,7 @@ Proof. apply (Rlt_irrefl 0); auto. do 2 rewrite S_INR in H1; cut (INR n1 < INR n0). intro H2; generalize (H0 n0 H2); intro; auto with arith. - apply (Rplus_lt_reg_r 1 (INR n1) (INR n0)). + apply (Rplus_lt_reg_l 1 (INR n1) (INR n0)). rewrite Rplus_comm; rewrite (Rplus_comm 1 (INR n0)); trivial. Qed. Hint Resolve INR_lt: real. @@ -1931,18 +1970,26 @@ Proof. apply (Rmult_le_compat_l x 0 y H H0). Qed. +Lemma Rinv_le_contravar : + forall x y, 0 < x -> x <= y -> / y <= / x. +Proof. + intros x y H1 [H2|H2]. + apply Rlt_le. + apply Rinv_lt_contravar with (2 := H2). + apply Rmult_lt_0_compat with (1 := H1). + now apply Rlt_trans with x. + rewrite H2. + apply Rle_refl. +Qed. + Lemma Rle_Rinv : forall x y:R, 0 < x -> 0 < y -> x <= y -> / y <= / x. Proof. - intros; apply Rmult_le_reg_l with x. - apply H. - rewrite <- Rinv_r_sym. - apply Rmult_le_reg_l with y. - apply H0. - rewrite Rmult_1_r; rewrite Rmult_comm; rewrite Rmult_assoc; - rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; apply H1. - red; intro; rewrite H2 in H0; elim (Rlt_irrefl _ H0). - red; intro; rewrite H2 in H; elim (Rlt_irrefl _ H). + intros x y H _. + apply Rinv_le_contravar with (1 := H). +Qed. + +Lemma Ropp_div : forall x y, -x/y = - (x / y). +intros x y; unfold Rdiv; ring. Qed. Lemma double : forall r1, 2 * r1 = r1 + r1. @@ -2018,6 +2065,29 @@ Proof. intros; elim (completeness E H H0); intros; split with x; assumption. Qed. +Lemma Rdiv_lt_0_compat : forall a b, 0 < a -> 0 < b -> 0 < a/b. +Proof. +intros; apply Rmult_lt_0_compat;[|apply Rinv_0_lt_compat]; assumption. +Qed. + +Lemma Rdiv_plus_distr : forall a b c, (a + b)/c = a/c + b/c. +intros a b c; apply Rmult_plus_distr_r. +Qed. + +Lemma Rdiv_minus_distr : forall a b c, (a - b)/c = a/c - b/c. +intros a b c; unfold Rminus, Rdiv; rewrite Rmult_plus_distr_r; ring. +Qed. + +(* A test for equality function. *) +Lemma Req_EM_T : forall r1 r2:R, {r1 = r2} + {r1 <> r2}. +Proof. + intros; destruct (total_order_T r1 r2) as [[H|]|H]. + - right; red; intros ->; elim (Rlt_irrefl r2 H). + - left; assumption. + - right; red; intros ->; elim (Rlt_irrefl r2 H). +Qed. + + (*********************************************************) (** * Definitions of new types *) (*********************************************************) @@ -2035,6 +2105,7 @@ 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). |