From 39bfa90d2bc53d4403962267da4c6ecbe26c3129 Mon Sep 17 00:00:00 2001 From: gmelquio Date: Fri, 11 Sep 2009 13:24:12 +0000 Subject: Added the following lemmas to homogenize Reals a bit: - Rmult_eq_compat_r, Rmult_eq_reg_r, Rplus_le_reg_r, Rmult_lt_reg_r, Rmult_le_reg_r (mirrored variants of the existing _l lemmas); - minus_IZR, opp_IZR (Ropp_Ropp_IZR), abs_IZR (mirrored Rabs_Zabs); - Rle_abs (RRle_abs); - Zpower_pos_powerRZ (signed variant of Zpower_nat_powerRZ). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12321 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 1 + theories/Reals/RIneq.v | 48 ++++++++++++++++++++++++++++++++++++++++++++- theories/Reals/Rbasic_fun.v | 9 ++++++++- theories/Reals/Rfunctions.v | 12 ++++++++++++ 4 files changed, 68 insertions(+), 2 deletions(-) diff --git a/CHANGES b/CHANGES index 70f183d15..6335a6b1d 100644 --- a/CHANGES +++ b/CHANGES @@ -76,6 +76,7 @@ Library - The function Compare_dec.nat_compare is now defined directly, instead of relying on lt_eq_lt_dec. The earlier version is still available under the name nat_compare_alt. +- Lemmas in library Reals have been homogenized a bit. Changes from V8.1 to V8.2 ========================= diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index 55e3896a8..b2e561922 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -515,6 +515,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 +532,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. @@ -973,6 +987,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). @@ -1267,6 +1288,14 @@ Proof. 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 +1311,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 *) (*********************************************************) @@ -1741,11 +1778,20 @@ 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. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 9856b5452..1fcf6f61e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -220,11 +220,13 @@ Proof. apply Rge_le; assumption. Qed. -Lemma RRle_abs : forall x:R, x <= Rabs x. +Lemma Rle_abs : forall x:R, x <= Rabs x. Proof. intro; unfold Rabs in |- *; case (Rcase_abs x); intros; fourier. Qed. +Definition RRle_abs := Rle_abs. + (*********) Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x. Proof. @@ -507,3 +509,8 @@ Proof. apply Rabs_right; auto with real zarith. Qed. +Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z). +Proof. + intros. + now rewrite Rabs_Zabs. +Qed. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index da28184f2..68862f492 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -619,6 +619,18 @@ Proof. unfold Zpower_nat in |- *; auto. Qed. +Lemma Zpower_pos_powerRZ : + forall n m, IZR (Zpower_pos n m) = IZR n ^Z Zpos m. +Proof. + intros. + rewrite Zpower_pos_nat; simpl. + induction (nat_of_P m). + easy. + unfold Zpower_nat; simpl. + rewrite mult_IZR. + now rewrite <- IHn0. +Qed. + Lemma powerRZ_lt : forall (x:R) (z:Z), 0 < x -> 0 < x ^Z z. Proof. intros x z; case z; simpl in |- *; auto with real. -- cgit v1.2.3