summaryrefslogtreecommitdiff
path: root/theories/Reals/Rbasic_fun.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Reals/Rbasic_fun.v')
-rw-r--r--theories/Reals/Rbasic_fun.v104
1 files changed, 51 insertions, 53 deletions
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index 15b04807..560f389b 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Rbasic_fun.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(*********************************************************)
(** Complements for the real numbers *)
(* *)
@@ -47,10 +45,10 @@ Qed.
(*********)
Lemma Rmin_Rgt_l : forall r1 r2 r, Rmin r1 r2 > r -> r1 > r /\ r2 > r.
Proof.
- intros r1 r2 r; unfold Rmin in |- *; case (Rle_dec r1 r2); intros.
+ intros r1 r2 r; unfold Rmin; case (Rle_dec r1 r2); intros.
split.
assumption.
- unfold Rgt in |- *; unfold Rgt in H; exact (Rlt_le_trans r r1 r2 H r0).
+ unfold Rgt; unfold Rgt in H; exact (Rlt_le_trans r r1 r2 H r0).
split.
generalize (Rnot_le_lt r1 r2 n); intro; exact (Rgt_trans r1 r2 r H0 H).
assumption.
@@ -59,7 +57,7 @@ Qed.
(*********)
Lemma Rmin_Rgt_r : forall r1 r2 r, r1 > r /\ r2 > r -> Rmin r1 r2 > r.
Proof.
- intros; unfold Rmin in |- *; case (Rle_dec r1 r2); elim H; clear H; intros;
+ intros; unfold Rmin; case (Rle_dec r1 r2); elim H; clear H; intros;
assumption.
Qed.
@@ -74,14 +72,14 @@ Qed.
(*********)
Lemma Rmin_l : forall x y:R, Rmin x y <= x.
Proof.
- intros; unfold Rmin in |- *; case (Rle_dec x y); intro H1;
+ intros; unfold Rmin; case (Rle_dec x y); intro H1;
[ right; reflexivity | auto with real ].
Qed.
(*********)
Lemma Rmin_r : forall x y:R, Rmin x y <= y.
Proof.
- intros; unfold Rmin in |- *; case (Rle_dec x y); intro H1;
+ intros; unfold Rmin; case (Rle_dec x y); intro H1;
[ assumption | auto with real ].
Qed.
@@ -125,20 +123,20 @@ Qed.
(*********)
Lemma Rmin_pos : forall x y:R, 0 < x -> 0 < y -> 0 < Rmin x y.
Proof.
- intros; unfold Rmin in |- *.
+ intros; unfold Rmin.
case (Rle_dec x y); intro; assumption.
Qed.
(*********)
Lemma Rmin_glb : forall x y z:R, z <= x -> z <= y -> z <= Rmin x y.
Proof.
- intros; unfold Rmin in |- *; case (Rle_dec x y); intro; assumption.
+ intros; unfold Rmin; case (Rle_dec x y); intro; assumption.
Qed.
(*********)
Lemma Rmin_glb_lt : forall x y z:R, z < x -> z < y -> z < Rmin x y.
Proof.
- intros; unfold Rmin in |- *; case (Rle_dec x y); intro; assumption.
+ intros; unfold Rmin; case (Rle_dec x y); intro; assumption.
Qed.
(*******************************)
@@ -169,8 +167,8 @@ Qed.
Lemma Rmax_Rle : forall r1 r2 r, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2.
Proof.
intros; split.
- unfold Rmax in |- *; case (Rle_dec r1 r2); intros; auto.
- intro; unfold Rmax in |- *; case (Rle_dec r1 r2); elim H; clear H; intros;
+ unfold Rmax; case (Rle_dec r1 r2); intros; auto.
+ intro; unfold Rmax; case (Rle_dec r1 r2); elim H; clear H; intros;
auto.
apply (Rle_trans r r1 r2); auto.
generalize (Rnot_le_lt r1 r2 n); clear n; intro; unfold Rgt in H0;
@@ -179,7 +177,7 @@ Qed.
Lemma Rmax_comm : forall x y:R, Rmax x y = Rmax y x.
Proof.
- intros p q; unfold Rmax in |- *; case (Rle_dec p q); case (Rle_dec q p); auto;
+ intros p q; unfold Rmax; case (Rle_dec p q); case (Rle_dec q p); auto;
intros H1 H2; apply Rle_antisym; auto with real.
Qed.
@@ -190,14 +188,14 @@ Notation RmaxSym := Rmax_comm (only parsing).
(*********)
Lemma Rmax_l : forall x y:R, x <= Rmax x y.
Proof.
- intros; unfold Rmax in |- *; case (Rle_dec x y); intro H1;
+ intros; unfold Rmax; case (Rle_dec x y); intro H1;
[ assumption | auto with real ].
Qed.
(*********)
Lemma Rmax_r : forall x y:R, y <= Rmax x y.
Proof.
- intros; unfold Rmax in |- *; case (Rle_dec x y); intro H1;
+ intros; unfold Rmax; case (Rle_dec x y); intro H1;
[ right; reflexivity | auto with real ].
Qed.
@@ -234,7 +232,7 @@ Qed.
Lemma RmaxRmult :
forall (p q:R) r, 0 <= r -> Rmax (r * p) (r * q) = r * Rmax p q.
Proof.
- intros p q r H; unfold Rmax in |- *.
+ intros p q r H; unfold Rmax.
case (Rle_dec p q); case (Rle_dec (r * p) (r * q)); auto; intros H1 H2; auto.
case H; intros E1.
case H1; auto with real.
@@ -248,7 +246,7 @@ Qed.
(*********)
Lemma Rmax_stable_in_negreal : forall x y:negreal, Rmax x y < 0.
Proof.
- intros; unfold Rmax in |- *; case (Rle_dec x y); intro;
+ intros; unfold Rmax; case (Rle_dec x y); intro;
[ apply (cond_neg y) | apply (cond_neg x) ].
Qed.
@@ -267,7 +265,7 @@ Qed.
(*********)
Lemma Rmax_neg : forall x y:R, x < 0 -> y < 0 -> Rmax x y < 0.
Proof.
- intros; unfold Rmax in |- *.
+ intros; unfold Rmax.
case (Rle_dec x y); intro; assumption.
Qed.
@@ -280,7 +278,7 @@ Lemma Rcase_abs : forall r, {r < 0} + {r >= 0}.
Proof.
intro; generalize (Rle_dec 0 r); intro X; elim X; intro; clear X.
right; apply (Rle_ge 0 r a).
- left; fold (0 > r) in |- *; apply (Rnot_le_lt 0 r b).
+ left; fold (0 > r); apply (Rnot_le_lt 0 r b).
Qed.
(*********)
@@ -293,27 +291,27 @@ Definition Rabs r : R :=
(*********)
Lemma Rabs_R0 : Rabs 0 = 0.
Proof.
- unfold Rabs in |- *; case (Rcase_abs 0); auto; intro.
+ unfold Rabs; case (Rcase_abs 0); auto; intro.
generalize (Rlt_irrefl 0); intro; exfalso; auto.
Qed.
Lemma Rabs_R1 : Rabs 1 = 1.
Proof.
-unfold Rabs in |- *; case (Rcase_abs 1); auto with real.
+unfold Rabs; case (Rcase_abs 1); auto with real.
intros H; absurd (1 < 0); auto with real.
Qed.
(*********)
Lemma Rabs_no_R0 : forall r, r <> 0 -> Rabs r <> 0.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs r); intro; auto.
+ intros; unfold Rabs; case (Rcase_abs r); intro; auto.
apply Ropp_neq_0_compat; auto.
Qed.
(*********)
Lemma Rabs_left : forall r, r < 0 -> Rabs r = - r.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs r); trivial; intro;
+ intros; unfold Rabs; case (Rcase_abs r); trivial; intro;
absurd (r >= 0).
exact (Rlt_not_ge r 0 H).
assumption.
@@ -322,7 +320,7 @@ Qed.
(*********)
Lemma Rabs_right : forall r, r >= 0 -> Rabs r = r.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs r); intro.
+ intros; unfold Rabs; case (Rcase_abs r); intro.
absurd (r >= 0).
exact (Rlt_not_ge r 0 r0).
assumption.
@@ -333,21 +331,21 @@ Lemma Rabs_left1 : forall a:R, a <= 0 -> Rabs a = - a.
Proof.
intros a H; case H; intros H1.
apply Rabs_left; auto.
- rewrite H1; simpl in |- *; rewrite Rabs_right; auto with real.
+ rewrite H1; simpl; rewrite Rabs_right; auto with real.
Qed.
(*********)
Lemma Rabs_pos : forall x:R, 0 <= Rabs x.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs x); intro.
+ intros; unfold Rabs; case (Rcase_abs x); intro.
generalize (Ropp_lt_gt_contravar x 0 r); intro; unfold Rgt in H;
- rewrite Ropp_0 in H; unfold Rle in |- *; left; assumption.
+ rewrite Ropp_0 in H; unfold Rle; left; assumption.
apply Rge_le; assumption.
Qed.
Lemma Rle_abs : forall x:R, x <= Rabs x.
Proof.
- intro; unfold Rabs in |- *; case (Rcase_abs x); intros; fourier.
+ intro; unfold Rabs; case (Rcase_abs x); intros; fourier.
Qed.
Definition RRle_abs := Rle_abs.
@@ -355,7 +353,7 @@ Definition RRle_abs := Rle_abs.
(*********)
Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs x); intro;
+ intros; unfold Rabs; case (Rcase_abs x); intro;
[ generalize (Rgt_not_le 0 x r); intro; exfalso; auto | trivial ].
Qed.
@@ -370,7 +368,7 @@ Lemma Rabs_pos_lt : forall x:R, x <> 0 -> 0 < Rabs x.
Proof.
intros; generalize (Rabs_pos x); intro; unfold Rle in H0; elim H0; intro;
auto.
- exfalso; clear H0; elim H; clear H; generalize H1; unfold Rabs in |- *;
+ exfalso; clear H0; elim H; clear H; generalize H1; unfold Rabs;
case (Rcase_abs x); intros; auto.
clear r H1; generalize (Rplus_eq_compat_l x 0 (- x) H0);
rewrite (let (H1, H2) := Rplus_ne x in H1); rewrite (Rplus_opp_r x);
@@ -380,7 +378,7 @@ Qed.
(*********)
Lemma Rabs_minus_sym : forall x y:R, Rabs (x - y) = Rabs (y - x).
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs (x - y));
+ intros; unfold Rabs; case (Rcase_abs (x - y));
case (Rcase_abs (y - x)); intros.
generalize (Rminus_lt y x r); generalize (Rminus_lt x y r0); intros;
generalize (Rlt_asym x y H); intro; exfalso;
@@ -399,7 +397,7 @@ Qed.
(*********)
Lemma Rabs_mult : forall x y:R, Rabs (x * y) = Rabs x * Rabs y.
Proof.
- intros; unfold Rabs in |- *; case (Rcase_abs (x * y)); case (Rcase_abs x);
+ intros; unfold Rabs; case (Rcase_abs (x * y)); case (Rcase_abs x);
case (Rcase_abs y); intros; auto.
generalize (Rmult_lt_gt_compat_neg_l y x 0 r r0); intro;
rewrite (Rmult_0_r y) in H; generalize (Rlt_asym (x * y) 0 r1);
@@ -450,7 +448,7 @@ Qed.
(*********)
Lemma Rabs_Rinv : forall r, r <> 0 -> Rabs (/ r) = / Rabs r.
Proof.
- intro; unfold Rabs in |- *; case (Rcase_abs r); case (Rcase_abs (/ r)); auto;
+ intro; unfold Rabs; case (Rcase_abs r); case (Rcase_abs (/ r)); auto;
intros.
apply Ropp_inv_permute; auto.
generalize (Rinv_lt_0_compat r r1); intro; unfold Rge in r0; elim r0; intros.
@@ -472,7 +470,7 @@ Proof.
cut (Rabs (-1) = 1).
intros; rewrite H0.
ring.
- unfold Rabs in |- *; case (Rcase_abs (-1)).
+ unfold Rabs; case (Rcase_abs (-1)).
intro; ring.
intro H0; generalize (Rge_le (-1) 0 H0); intros.
generalize (Ropp_le_ge_contravar 0 (-1) H1).
@@ -485,13 +483,13 @@ Qed.
(*********)
Lemma Rabs_triang : forall a b:R, Rabs (a + b) <= Rabs a + Rabs b.
Proof.
- intros a b; unfold Rabs in |- *; case (Rcase_abs (a + b)); case (Rcase_abs a);
+ intros a b; unfold Rabs; case (Rcase_abs (a + b)); case (Rcase_abs a);
case (Rcase_abs b); intros.
apply (Req_le (- (a + b)) (- a + - b)); rewrite (Ropp_plus_distr a b);
reflexivity.
(**)
rewrite (Ropp_plus_distr a b); apply (Rplus_le_compat_l (- a) (- b) b);
- unfold Rle in |- *; unfold Rge in r; elim r; intro.
+ unfold Rle; unfold Rge in r; elim r; intro.
left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- b) 0 b H); intro;
elim (Rplus_ne (- b)); intros v w; rewrite v in H0;
clear v w; rewrite (Rplus_opp_l b) in H0; apply (Rlt_trans (- b) 0 b H0 H).
@@ -499,7 +497,7 @@ Proof.
(**)
rewrite (Ropp_plus_distr a b); rewrite (Rplus_comm (- a) (- b));
rewrite (Rplus_comm a (- b)); apply (Rplus_le_compat_l (- b) (- a) a);
- unfold Rle in |- *; unfold Rge in r0; elim r0; intro.
+ unfold Rle; unfold Rge in r0; elim r0; intro.
left; unfold Rgt in H; generalize (Rplus_lt_compat_l (- a) 0 a H); intro;
elim (Rplus_ne (- a)); intros v w; rewrite v in H0;
clear v w; rewrite (Rplus_opp_l a) in H0; apply (Rlt_trans (- a) 0 a H0 H).
@@ -523,27 +521,27 @@ Proof.
(**)
rewrite (Rplus_comm a b); rewrite (Rplus_comm (- a) b);
apply (Rplus_le_compat_l b a (- a)); apply (Rminus_le a (- a));
- unfold Rminus in |- *; rewrite (Ropp_involutive a);
+ unfold Rminus; rewrite (Ropp_involutive a);
generalize (Rplus_lt_compat_l a a 0 r0); clear r r1;
intro; elim (Rplus_ne a); intros v w; rewrite v in H;
clear v w; generalize (Rlt_trans (a + a) a 0 H r0);
intro; apply (Rlt_le (a + a) 0 H0).
(**)
apply (Rplus_le_compat_l a b (- b)); apply (Rminus_le b (- b));
- unfold Rminus in |- *; rewrite (Ropp_involutive b);
+ unfold Rminus; rewrite (Ropp_involutive b);
generalize (Rplus_lt_compat_l b b 0 r); clear r0 r1;
intro; elim (Rplus_ne b); intros v w; rewrite v in H;
clear v w; generalize (Rlt_trans (b + b) b 0 H r);
intro; apply (Rlt_le (b + b) 0 H0).
(**)
- unfold Rle in |- *; right; reflexivity.
+ unfold Rle; right; reflexivity.
Qed.
(*********)
Lemma Rabs_triang_inv : forall a b:R, Rabs a - Rabs b <= Rabs (a - b).
Proof.
intros; apply (Rplus_le_reg_l (Rabs b) (Rabs a - Rabs b) (Rabs (a - b)));
- unfold Rminus in |- *; rewrite <- (Rplus_assoc (Rabs b) (Rabs a) (- Rabs b));
+ unfold Rminus; rewrite <- (Rplus_assoc (Rabs b) (Rabs a) (- Rabs b));
rewrite (Rplus_comm (Rabs b) (Rabs a));
rewrite (Rplus_assoc (Rabs a) (Rabs b) (- Rabs b));
rewrite (Rplus_opp_r (Rabs b)); rewrite (proj1 (Rplus_ne (Rabs a)));
@@ -563,7 +561,7 @@ Proof.
rewrite <- (Rabs_Ropp (Rabs a - Rabs b)); rewrite <- (Rabs_Ropp (a - b));
do 2 rewrite Ropp_minus_distr.
apply H; left; assumption.
- rewrite Heq; unfold Rminus in |- *; rewrite Rplus_opp_r; rewrite Rabs_R0;
+ rewrite Heq; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0;
apply Rabs_pos.
apply H; left; assumption.
intros; replace (Rabs (Rabs a - Rabs b)) with (Rabs a - Rabs b).
@@ -578,8 +576,8 @@ Qed.
(*********)
Lemma Rabs_def1 : forall x a:R, x < a -> - a < x -> Rabs x < a.
Proof.
- unfold Rabs in |- *; intros; case (Rcase_abs x); intro.
- generalize (Ropp_lt_gt_contravar (- a) x H0); unfold Rgt in |- *;
+ unfold Rabs; intros; case (Rcase_abs x); intro.
+ generalize (Ropp_lt_gt_contravar (- a) x H0); unfold Rgt;
rewrite Ropp_involutive; intro; assumption.
assumption.
Qed.
@@ -587,15 +585,15 @@ Qed.
(*********)
Lemma Rabs_def2 : forall x a:R, Rabs x < a -> x < a /\ - a < x.
Proof.
- unfold Rabs in |- *; intro x; case (Rcase_abs x); intros.
- generalize (Ropp_gt_lt_0_contravar x r); unfold Rgt in |- *; intro;
+ unfold Rabs; intro x; case (Rcase_abs x); intros.
+ generalize (Ropp_gt_lt_0_contravar x r); unfold Rgt; intro;
generalize (Rlt_trans 0 (- x) a H0 H); intro; split.
apply (Rlt_trans x 0 a r H1).
generalize (Ropp_lt_gt_contravar (- x) a H); rewrite (Ropp_involutive x);
- unfold Rgt in |- *; trivial.
+ unfold Rgt; trivial.
fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H r); intro;
- generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a) in |- *;
- generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt in |- *;
+ generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a);
+ generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt;
intro; split; assumption.
Qed.
@@ -625,16 +623,16 @@ Proof.
apply RmaxLess1; auto.
Qed.
-Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Zabs z).
+Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z).
Proof.
- intros z; case z; simpl in |- *; auto with real.
+ intros z; case z; simpl; auto with real.
apply Rabs_right; auto with real.
intros p0; apply Rabs_right; auto with real zarith.
intros p0; rewrite Rabs_Ropp.
apply Rabs_right; auto with real zarith.
Qed.
-Lemma abs_IZR : forall z, IZR (Zabs z) = Rabs (IZR z).
+Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z).
Proof.
intros.
now rewrite Rabs_Zabs.
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-05 14:16:36 +0000