summaryrefslogtreecommitdiff
path: root/theories/Reals/RIneq.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/RIneq.v')
-rw-r--r--theories/Reals/RIneq.v113
1 files changed, 80 insertions, 33 deletions
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index c07b86a6..2b6af10e 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -6,7 +7,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: RIneq.v 11887 2009-02-06 19:57:33Z herbelin $ i*)
+(*i $Id$ i*)
(*********************************************************)
(** * Basic lemmas for the classical real numbers *)
@@ -19,8 +20,8 @@ Require Export ZArithRing.
Require Import Omega.
Require Export RealField.
-Open Local Scope Z_scope.
-Open Local Scope R_scope.
+Local Open Scope Z_scope.
+Local Open Scope R_scope.
Implicit Type r : R.
@@ -75,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.
+ intuition eauto 3.
Qed.
Hint Resolve Req_dec: real.
@@ -129,7 +130,7 @@ Hint Immediate Rge_le: rorders.
(**********)
Lemma Rlt_gt : forall r1 r2, r1 < r2 -> r2 > r1.
-Proof.
+Proof.
trivial.
Qed.
Hint Resolve Rlt_gt: rorders.
@@ -291,7 +292,7 @@ Proof. eauto using Rlt_trans with rorders. Qed.
(**********)
Lemma Rle_lt_trans : forall r1 r2 r3, r1 <= r2 -> r2 < r3 -> r1 < r3.
Proof.
- generalize Rlt_trans Rlt_eq_compat.
+ generalize Rlt_trans Rlt_eq_compat.
unfold Rle in |- *.
intuition eauto 2.
Qed.
@@ -456,7 +457,7 @@ Proof.
rewrite Rplus_comm; auto with real.
Qed.
-(*********************************************************)
+(*********************************************************)
(** ** Multiplication *)
(*********************************************************)
@@ -515,6 +516,13 @@ Qed.
(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
+Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r.
+Proof.
+ intros.
+ rewrite <- 2!(Rmult_comm r).
+ now apply Rmult_eq_compat_l.
+Qed.
+
(**********)
Lemma Rmult_eq_reg_l : forall r r1 r2, r * r1 = r * r2 -> r <> 0 -> r1 = r2.
Proof.
@@ -525,6 +533,13 @@ Proof.
field; trivial.
Qed.
+Lemma Rmult_eq_reg_r : forall r r1 r2, r1 * r = r2 * r -> r <> 0 -> r1 = r2.
+Proof.
+ intros.
+ apply Rmult_eq_reg_l with (2 := H0).
+ now rewrite 2!(Rmult_comm r).
+Qed.
+
(**********)
Lemma Rmult_integral : forall r1 r2, r1 * r2 = 0 -> r1 = 0 \/ r2 = 0.
Proof.
@@ -554,13 +569,13 @@ Proof.
auto with real.
Qed.
-(**********)
+(**********)
Lemma Rmult_neq_0_reg : forall r1 r2, r1 * r2 <> 0 -> r1 <> 0 /\ r2 <> 0.
Proof.
intros r1 r2 H; split; red in |- *; intro; apply H; auto with real.
Qed.
-(**********)
+(**********)
Lemma Rmult_integral_contrapositive :
forall r1 r2, r1 <> 0 /\ r2 <> 0 -> r1 * r2 <> 0.
Proof.
@@ -569,11 +584,11 @@ Proof.
Qed.
Hint Resolve Rmult_integral_contrapositive: real.
-Lemma Rmult_integral_contrapositive_currified :
+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.
Proof.
@@ -743,7 +758,7 @@ Lemma Rminus_not_eq_right : forall r1 r2, r2 - r1 <> 0 -> r1 <> r2.
Proof.
red in |- *; intros; elim H; rewrite H0; ring.
Qed.
-Hint Resolve Rminus_not_eq_right: real.
+Hint Resolve Rminus_not_eq_right: real.
(**********)
Lemma Rmult_minus_distr_l :
@@ -973,6 +988,13 @@ Proof.
right; apply (Rplus_eq_reg_l r r1 r2 H0).
Qed.
+Lemma Rplus_le_reg_r : forall r r1 r2, r1 + r <= r2 + r -> r1 <= r2.
+Proof.
+ intros.
+ apply (Rplus_le_reg_l r).
+ now rewrite 2!(Rplus_comm r).
+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).
@@ -1261,12 +1283,20 @@ Lemma Rmult_lt_reg_l : forall r r1 r2, 0 < r -> r * r1 < r * r2 -> 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);
+ rewrite Eq0 in H0; exfalso; apply (Rlt_irrefl (z * y)); auto.
+ generalize (Rmult_lt_compat_l z y x H Eq0); intro; exfalso;
+ generalize (Rlt_trans (z * x) (z * y) (z * x) H0 H1);
intro; apply (Rlt_irrefl (z * x)); auto.
Qed.
+Lemma Rmult_lt_reg_r : forall r r1 r2 : R, 0 < r -> r1 * r < r2 * r -> r1 < r2.
+Proof.
+ intros.
+ apply Rmult_lt_reg_l with r.
+ exact H.
+ now rewrite 2!(Rmult_comm r).
+Qed.
+
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 rorders. Qed.
@@ -1282,6 +1312,14 @@ Proof.
rewrite <- Rmult_assoc; rewrite Rinv_l; auto with real.
Qed.
+Lemma Rmult_le_reg_r : forall r r1 r2, 0 < r -> r1 * r <= r2 * r -> r1 <= r2.
+Proof.
+ intros.
+ apply Rmult_le_reg_l with r.
+ exact H.
+ now rewrite 2!(Rmult_comm r).
+Qed.
+
(*********************************************************)
(** ** Order and substraction *)
(*********************************************************)
@@ -1296,7 +1334,7 @@ Qed.
Hint Resolve Rlt_minus: real.
Lemma Rgt_minus : forall r1 r2, r1 > r2 -> r1 - r2 > 0.
-Proof.
+Proof.
intros; apply (Rplus_lt_reg_r r2).
replace (r2 + (r1 - r2)) with r1.
replace (r2 + 0) with r2; auto with real.
@@ -1310,7 +1348,7 @@ Proof.
Qed.
Lemma Rge_minus : forall r1 r2, r1 >= r2 -> r1 - r2 >= 0.
-Proof.
+Proof.
destruct 1.
auto using Rgt_minus, Rgt_ge.
right; auto using Rminus_diag_eq with rorders.
@@ -1463,7 +1501,7 @@ Proof.
Qed.
Hint Resolve Rinv_1_lt_contravar: real.
-(*********************************************************)
+(*********************************************************)
(** ** Miscellaneous *)
(*********************************************************)
@@ -1491,7 +1529,7 @@ Proof.
pattern r1 at 2 in |- *; replace r1 with (r1 + 0); auto with real.
Qed.
-(*********************************************************)
+(*********************************************************)
(** ** Injection from [N] to [R] *)
(*********************************************************)
@@ -1508,7 +1546,7 @@ Proof.
Qed.
(**********)
-Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
+Lemma plus_INR : forall n m:nat, INR (n + m) = INR n + INR m.
Proof.
intros n m; induction n as [| n Hrecn].
simpl in |- *; auto with real.
@@ -1581,11 +1619,11 @@ Hint Resolve pos_INR: real.
Lemma INR_lt : forall n m:nat, INR n < INR m -> (n < m)%nat.
Proof.
double induction n m; intros.
- simpl in |- *; elimtype False; apply (Rlt_irrefl 0); auto.
+ simpl in |- *; exfalso; apply (Rlt_irrefl 0); auto.
auto with arith.
generalize (pos_INR (S n0)); intro; cut (INR 0 = 0);
- [ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
- generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; elimtype False;
+ [ intro H2; rewrite H2 in H0; idtac | simpl in |- *; trivial ].
+ generalize (Rle_lt_trans 0 (INR (S n0)) 0 H1 H0); intro; exfalso;
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.
@@ -1627,7 +1665,7 @@ Proof.
intros n m H; case (le_or_lt n m); intros H1.
case (le_lt_or_eq _ _ H1); intros H2.
apply Rlt_dichotomy_converse; auto with real.
- elimtype False; auto.
+ exfalso; auto.
apply sym_not_eq; apply Rlt_dichotomy_converse; auto with real.
Qed.
Hint Resolve not_INR: real.
@@ -1637,10 +1675,10 @@ Proof.
intros; case (le_or_lt n m); intros H1.
case (le_lt_or_eq _ _ H1); intros H2; auto.
cut (n <> m).
- intro H3; generalize (not_INR n m H3); intro H4; elimtype False; auto.
+ intro H3; generalize (not_INR n m H3); intro H4; exfalso; auto.
omega.
symmetry in |- *; cut (m <> n).
- intro H3; generalize (not_INR m n H3); intro H4; elimtype False; auto.
+ intro H3; generalize (not_INR m n H3); intro H4; exfalso; auto.
omega.
Qed.
Hint Resolve INR_eq: real.
@@ -1659,7 +1697,7 @@ Proof.
Qed.
Hint Resolve not_1_INR: real.
-(*********************************************************)
+(*********************************************************)
(** ** Injection from [Z] to [R] *)
(*********************************************************)
@@ -1741,17 +1779,26 @@ Proof.
Qed.
(**********)
-Lemma Ropp_Ropp_IZR : forall n:Z, IZR (- n) = - IZR n.
+Lemma opp_IZR : forall n:Z, IZR (- n) = - IZR n.
Proof.
intro z; case z; simpl in |- *; auto with real.
Qed.
+Definition Ropp_Ropp_IZR := opp_IZR.
+
+Lemma minus_IZR : forall n m:Z, IZR (n - m) = IZR n - IZR m.
+Proof.
+ intros; unfold Zminus, Rminus.
+ rewrite <- opp_IZR.
+ apply plus_IZR.
+Qed.
+
(**********)
Lemma Z_R_minus : forall n m:Z, IZR n - IZR m = IZR (n - m).
Proof.
intros z1 z2; unfold Rminus in |- *; unfold Zminus in |- *.
rewrite <- (Ropp_Ropp_IZR z2); symmetry in |- *; apply plus_IZR.
-Qed.
+Qed.
(**********)
Lemma lt_0_IZR : forall n:Z, 0 < IZR n -> (0 < n)%Z.
@@ -1766,7 +1813,7 @@ Qed.
(**********)
Lemma lt_IZR : forall n m:Z, IZR n < IZR m -> (n < m)%Z.
Proof.
- intros z1 z2 H; apply Zlt_0_minus_lt.
+ intros z1 z2 H; apply Zlt_0_minus_lt.
apply lt_0_IZR.
rewrite <- Z_R_minus.
exact (Rgt_minus (IZR z2) (IZR z1) H).
@@ -1785,7 +1832,7 @@ Qed.
Lemma eq_IZR : forall n m:Z, IZR n = IZR m -> n = m.
Proof.
intros z1 z2 H; generalize (Rminus_diag_eq (IZR z1) (IZR z2) H);
- rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
+ rewrite (Z_R_minus z1 z2); intro; generalize (eq_IZR_R0 (z1 - z2) H0);
intro; omega.
Qed.
@@ -1837,7 +1884,7 @@ Lemma IZR_lt : forall n m:Z, (n < m)%Z -> IZR n < IZR m.
Proof.
intros m n H; cut (m <= n)%Z.
intro H0; elim (IZR_le m n H0); intro; auto.
- generalize (eq_IZR m n H1); intro; elimtype False; omega.
+ generalize (eq_IZR m n H1); intro; exfalso; omega.
omega.
Qed.
@@ -1935,7 +1982,7 @@ Proof.
rewrite <- Rinv_l_sym.
rewrite Rmult_1_r; replace (2 * x) with (x + x).
rewrite (Rplus_comm y); intro H5; apply Rplus_le_reg_l with x; assumption.
- ring.
+ ring.
replace 2 with (INR 2); [ apply not_0_INR; discriminate | reflexivity ].
pattern y at 2 in |- *; replace y with (y / 2 + y / 2).
unfold Rminus, Rdiv in |- *.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 05:09:07 +0000