diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /theories/Reals/R_Ifp.v | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'theories/Reals/R_Ifp.v')
-rw-r--r-- | theories/Reals/R_Ifp.v | 80 |
1 files changed, 32 insertions, 48 deletions
diff --git a/theories/Reals/R_Ifp.v b/theories/Reals/R_Ifp.v index b6d07283..77e2a1e0 100644 --- a/theories/Reals/R_Ifp.v +++ b/theories/Reals/R_Ifp.v @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (**********************************************************) @@ -42,28 +44,23 @@ Qed. Lemma up_tech : forall (r:R) (z:Z), IZR z <= r -> r < IZR (z + 1) -> (z + 1)%Z = up r. Proof. - intros; generalize (Rplus_le_compat_l 1 (IZR z) r H); intro; clear H; - rewrite (Rplus_comm 1 (IZR z)) in H1; rewrite (Rplus_comm 1 r) in H1; - cut (1 = IZR 1); auto with zarith real. - intro; generalize H1; pattern 1 at 1; rewrite H; intro; clear H H1; - rewrite <- (plus_IZR z 1) in H2; apply (tech_up r (z + 1)); - auto with zarith real. + intros. + apply tech_up with (1 := H0). + rewrite plus_IZR. + now apply Rplus_le_compat_r. Qed. (**********) Lemma fp_R0 : frac_part 0 = 0. Proof. - unfold frac_part; unfold Int_part; elim (archimed 0); intros; - unfold Rminus; elim (Rplus_ne (- IZR (up 0 - 1))); - intros a b; rewrite b; clear a b; rewrite <- Z_R_minus; - cut (up 0 = 1%Z). - intro; rewrite H1; - rewrite (Rminus_diag_eq (IZR 1) (IZR 1) (eq_refl (IZR 1))); - apply Ropp_0. - elim (archimed 0); intros; clear H2; unfold Rgt in H1; - rewrite (Rminus_0_r (IZR (up 0))) in H0; generalize (lt_O_IZR (up 0) H1); - intro; clear H1; generalize (le_IZR_R1 (up 0) H0); - intro; clear H H0; omega. + unfold frac_part, Int_part. + replace (up 0) with 1%Z. + now rewrite <- minus_IZR. + destruct (archimed 0) as [H1 H2]. + apply lt_IZR in H1. + rewrite <- minus_IZR in H2. + apply le_IZR in H2. + omega. Qed. (**********) @@ -112,21 +109,12 @@ Lemma base_Int_part : Proof. intro; unfold Int_part; elim (archimed r); intros. split; rewrite <- (Z_R_minus (up r) 1); simpl. - generalize (Rle_minus (IZR (up r) - r) 1 H0); intro; unfold Rminus in H1; - rewrite (Rplus_assoc (IZR (up r)) (- r) (-1)) in H1; - rewrite (Rplus_comm (- r) (-1)) in H1; - rewrite <- (Rplus_assoc (IZR (up r)) (-1) (- r)) in H1; - fold (IZR (up r) - 1) in H1; fold (IZR (up r) - 1 - r) in H1; - apply Rminus_le; auto with zarith real. - generalize (Rplus_gt_compat_l (-1) (IZR (up r)) r H); intro; - rewrite (Rplus_comm (-1) (IZR (up r))) in H1; - generalize (Rplus_gt_compat_l (- r) (IZR (up r) + -1) (-1 + r) H1); - intro; clear H H0 H1; rewrite (Rplus_comm (- r) (IZR (up r) + -1)) in H2; - fold (IZR (up r) - 1) in H2; fold (IZR (up r) - 1 - r) in H2; - rewrite (Rplus_comm (- r) (-1 + r)) in H2; - rewrite (Rplus_assoc (-1) r (- r)) in H2; rewrite (Rplus_opp_r r) in H2; - elim (Rplus_ne (-1)); intros a b; rewrite a in H2; - clear a b; auto with zarith real. + apply Rminus_le. + replace (IZR (up r) - 1 - r) with (IZR (up r) - r - 1) by ring. + now apply Rle_minus. + apply Rminus_gt. + replace (IZR (up r) - 1 - r - -1) with (IZR (up r) - r) by ring. + now apply Rgt_minus. Qed. (**********) @@ -238,9 +226,7 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H; clear a b; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; - rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H; clear H1; + rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H. rewrite <- (plus_IZR (Int_part r1 - Int_part r2) 1) in H; generalize (up_tech (r1 - r2) (Int_part r1 - Int_part r2) H0 H); intros; clear H H0; unfold Int_part at 1; @@ -324,12 +310,12 @@ Proof. rewrite (Rplus_opp_r (IZR (Int_part r1) - IZR (Int_part r2))) in H0; elim (Rplus_ne (r1 - r2)); intros a b; rewrite b in H0; clear a b; rewrite <- (Rplus_opp_l 1) in H0; - rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-1) 1) + rewrite <- (Rplus_assoc (IZR (Int_part r1) - IZR (Int_part r2)) (-(1)) 1) in H0; fold (IZR (Int_part r1) - IZR (Int_part r2) - 1) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H0; rewrite (Z_R_minus (Int_part r1) (Int_part r2)) in H; - cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H; rewrite H1 in H0; clear H1; + auto with zarith real. + change (_ + -1) with (IZR (Int_part r1 - Int_part r2) - 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H; rewrite (Z_R_minus (Int_part r1 - Int_part r2) 1) in H0; rewrite <- (plus_IZR (Int_part r1 - Int_part r2 - 1) 1) in H0; @@ -442,9 +428,9 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (r1 + r2)); intros a b; rewrite b in H0; clear a b; + change 2 with (1 + 1) in H0; rewrite <- (Rplus_assoc (IZR (Int_part r1) + IZR (Int_part r2)) 1 1) in H0; - cut (1 = IZR 1); auto with zarith real. - intro; rewrite H1 in H0; rewrite H1 in H; clear H1; + auto with zarith real. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H; @@ -507,9 +493,7 @@ Proof. in H0; rewrite (Rplus_opp_r (IZR (Int_part r1) + IZR (Int_part r2))) in H0; elim (Rplus_ne (IZR (Int_part r1) + IZR (Int_part r2))); intros a b; rewrite a in H0; clear a b; elim (Rplus_ne (r1 + r2)); - intros a b; rewrite b in H0; clear a b; cut (1 = IZR 1); - auto with zarith real. - intro; rewrite H in H1; clear H; + intros a b; rewrite b in H0; clear a b. rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H0; rewrite <- (plus_IZR (Int_part r1) (Int_part r2)) in H1; rewrite <- (plus_IZR (Int_part r1 + Int_part r2) 1) in H1; @@ -536,7 +520,7 @@ Proof. rewrite <- (Ropp_plus_distr (IZR (Int_part r1)) (IZR (Int_part r2))); unfold Rminus; rewrite - (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-1)) + (Rplus_assoc (r1 + r2) (- (IZR (Int_part r1) + IZR (Int_part r2))) (-(1))) ; rewrite <- (Ropp_plus_distr (IZR (Int_part r1) + IZR (Int_part r2)) 1); trivial with zarith real. Qed. |