diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 10:26:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-01 11:33:55 +0200 |
| commit | 76adb57c72fccb4f3e416bd7f3927f4fff72178b (patch) | |
| tree | f8d72073a2ea62d3e5c274c201ef06532ac57b61 /theories/Reals | |
| parent | be01deca2b8ff22505adaa66f55f005673bf2d85 (diff) | |
Making those proofs which depend on names generated for the arguments
in Prop of constructors of inductive types independent of these names.
Incidentally upgraded/simplified a couple of proofs, mainly in Reals.
This prepares to the next commit about using names based on H for such
hypotheses in Prop.
Diffstat (limited to 'theories/Reals')
33 files changed, 1016 insertions, 1354 deletions
diff --git a/theories/Reals/Alembert.v b/theories/Reals/Alembert.v index 38e9bf7f4..a92b3584b 100644 --- a/theories/Reals/Alembert.v +++ b/theories/Reals/Alembert.v @@ -400,15 +400,14 @@ Theorem Alembert_C3 : Un_cv (fun n:nat => Rabs (An (S n) / An n)) 0 -> { l:R | Pser An x l }. Proof. - intros; case (total_order_T x 0); intro. - elim s; intro. + intros; destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red; intro; rewrite H1 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H1 in Hlt; elim (Rlt_irrefl _ Hlt). apply AlembertC3_step2; assumption. cut (x <> 0). intro; apply AlembertC3_step1; assumption. - red; intro; rewrite H1 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H1 in Hgt; elim (Rlt_irrefl _ Hgt). Defined. Lemma Alembert_C4 : @@ -586,14 +585,13 @@ Lemma Alembert_C6 : elim X; intros. exists x0. apply tech12; assumption. - case (total_order_T x 0); intro. - elim s; intro. + destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. eapply Alembert_C5 with (k * Rabs x). split. unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H3 in Hlt; elim (Rlt_irrefl _ Hlt). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. @@ -604,7 +602,7 @@ Lemma Alembert_C6 : intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red; intro; rewrite H3 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H3 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). @@ -621,7 +619,7 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. @@ -629,7 +627,7 @@ Lemma Alembert_C6 : unfold R_dist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. simpl. @@ -641,14 +639,14 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). apply H0. apply pow_nonzero. - red; intro; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro H7; rewrite H7 in a; elim (Rlt_irrefl _ a). + red; intro H7; rewrite H7 in Hlt; elim (Rlt_irrefl _ Hlt). exists (An 0%nat). unfold Un_cv. intros. @@ -661,14 +659,14 @@ Lemma Alembert_C6 : simpl; ring. rewrite tech5. rewrite <- Hrecn. - rewrite b; simpl; ring. + rewrite Heq; simpl; ring. unfold ge; apply le_O_n. eapply Alembert_C5 with (k * Rabs x). split. unfold Rdiv; apply Rmult_le_pos. left; assumption. left; apply Rabs_pos_lt. - red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H3 in Hgt; elim (Rlt_irrefl _ Hgt). apply Rmult_lt_reg_l with (/ k). apply Rinv_0_lt_compat; assumption. rewrite <- Rmult_assoc. @@ -679,7 +677,7 @@ Lemma Alembert_C6 : intro; apply prod_neq_R0. apply H0. apply pow_nonzero. - red; intro; rewrite H3 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H3 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Un_cv; unfold Un_cv in H1. intros. cut (0 < eps / Rabs x). @@ -696,7 +694,7 @@ Lemma Alembert_C6 : rewrite Rabs_Rabsolu. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). rewrite <- Rmult_assoc. rewrite <- Rinv_l_sym. rewrite Rmult_1_l. @@ -704,7 +702,7 @@ Lemma Alembert_C6 : unfold R_dist in H5. unfold Rdiv; unfold Rdiv in H5; apply H5; assumption. apply Rabs_no_R0. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Rdiv; replace (S n) with (n + 1)%nat; [ idtac | ring ]. rewrite pow_add. simpl. @@ -716,12 +714,12 @@ Lemma Alembert_C6 : rewrite <- Rinv_r_sym. rewrite Rmult_1_r; reflexivity. apply pow_nonzero. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). apply H0. apply pow_nonzero. - red; intro; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt. - red; intro H7; rewrite H7 in r; elim (Rlt_irrefl _ r). + red; intro H7; rewrite H7 in Hgt; elim (Rlt_irrefl _ Hgt). Qed. diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index a9beba23c..781b32ee1 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -105,14 +105,14 @@ Proof. exists (x - IZR k0 * y). split. ring. - unfold k0; case (Rcase_abs y); intro. + unfold k0; case (Rcase_abs y) as [Hlt|Hge]. assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. split. apply Rmult_le_reg_l with (/ - y). - apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r. + apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt. rewrite Rmult_0_r; rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r; rewrite <- Ropp_inv_permute; [ idtac | assumption ]. rewrite Rmult_assoc; repeat rewrite Ropp_mult_distr_r_reverse; @@ -125,8 +125,8 @@ Proof. (- (x * / y) + - (IZR (up (x * / - y)) - 1))) with 1; [ idtac | ring ]. elim H0; intros _ H1; unfold Rdiv in H1; exact H1. - rewrite (Rabs_left _ r); apply Rmult_lt_reg_l with (/ - y). - apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact r. + rewrite (Rabs_left _ Hlt); apply Rmult_lt_reg_l with (/ - y). + apply Rinv_0_lt_compat; apply Ropp_0_gt_lt_contravar; exact Hlt. rewrite <- Rinv_l_sym. rewrite (Rmult_comm (/ - y)); rewrite Rmult_plus_distr_r; rewrite <- Ropp_inv_permute; [ idtac | assumption ]. @@ -157,7 +157,7 @@ Proof. (IZR (up (x * / y)) - x * / y + (x * / y + (1 - IZR (up (x * / y))))) with 1; [ idtac | ring ]; elim H0; intros _ H2; unfold Rdiv in H2; exact H2. - rewrite (Rabs_right _ r); apply Rmult_lt_reg_l with (/ y). + rewrite (Rabs_right _ Hge); apply Rmult_lt_reg_l with (/ y). apply Rinv_0_lt_compat; assumption. rewrite <- (Rinv_l_sym _ H); rewrite (Rmult_comm (/ y)); rewrite Rmult_plus_distr_r; rewrite Rmult_assoc; rewrite <- Rinv_r_sym; @@ -168,11 +168,10 @@ Proof. replace (IZR (up (x / y)) - 1 + (x * / y + (1 - IZR (up (x / y))))) with (x * / y); [ idtac | ring ]; elim H0; unfold Rdiv; intros H2 _; exact H2. - case (total_order_T 0 y); intro. - elim s; intro. + destruct (total_order_T 0 y) as [[Hlt|Heq]|Hgt]. assumption. - elim H; symmetry ; exact b. - assert (H1 := Rge_le _ _ r); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r0)). + elim H; symmetry ; exact Heq. + apply Rge_le in Hge; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hge Hgt)). Qed. Lemma tech8 : forall n i:nat, (n <= S n + i)%nat. diff --git a/theories/Reals/Cos_rel.v b/theories/Reals/Cos_rel.v index 335d5b16a..6fd3d9e66 100644 --- a/theories/Reals/Cos_rel.v +++ b/theories/Reals/Cos_rel.v @@ -258,49 +258,30 @@ Qed. Lemma A1_cvg : forall x:R, Un_cv (A1 x) (cos x). intro. -assert (H := exist_cos (x * x)). -elim H; intros. -assert (p_i := p). -unfold cos_in in p. -unfold cos_n, infinite_sum in p. -unfold R_dist in p. -cut (cos x = x0). -intro. -rewrite H0. -unfold Un_cv; unfold R_dist; intros. -elim (p eps H1); intros. +unfold cos; destruct (exist_cos (Rsqr x)) as (x0,p). +unfold cos_in, cos_n, infinite_sum, R_dist in p. +unfold Un_cv, R_dist; intros. +destruct (p eps H) as (x1,H0). exists x1; intros. unfold A1. replace (sum_f_R0 (fun k:nat => (-1) ^ k / INR (fact (2 * k)) * x ^ (2 * k)) n) with (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * (x * x) ^ i) n). -apply H2; assumption. +apply H0; assumption. apply sum_eq. intros. replace ((x * x) ^ i) with (x ^ (2 * i)). reflexivity. apply pow_sqr. -unfold cos. -case (exist_cos (Rsqr x)). -unfold Rsqr; intros. -unfold cos_in in p_i. -unfold cos_in in c. -apply uniqueness_sum with (fun i:nat => cos_n i * (x * x) ^ i); assumption. Qed. Lemma C1_cvg : forall x y:R, Un_cv (C1 x y) (cos (x + y)). intros. -assert (H := exist_cos ((x + y) * (x + y))). -elim H; intros. -assert (p_i := p). -unfold cos_in in p. -unfold cos_n, infinite_sum in p. -unfold R_dist in p. -cut (cos (x + y) = x0). -intro. -rewrite H0. -unfold Un_cv; unfold R_dist; intros. -elim (p eps H1); intros. +unfold cos. +destruct (exist_cos (Rsqr (x + y))) as (x0,p). +unfold cos_in, cos_n, infinite_sum, R_dist in p. +unfold Un_cv, R_dist; intros. +destruct (p eps H) as (x1,H0). exists x1; intros. unfold C1. replace @@ -308,19 +289,12 @@ replace with (sum_f_R0 (fun i:nat => (-1) ^ i / INR (fact (2 * i)) * ((x + y) * (x + y)) ^ i) n). -apply H2; assumption. +apply H0; assumption. apply sum_eq. intros. replace (((x + y) * (x + y)) ^ i) with ((x + y) ^ (2 * i)). reflexivity. apply pow_sqr. -unfold cos. -case (exist_cos (Rsqr (x + y))). -unfold Rsqr; intros. -unfold cos_in in p_i. -unfold cos_in in c. -apply uniqueness_sum with (fun i:nat => cos_n i * ((x + y) * (x + y)) ^ i); - assumption. Qed. Lemma B1_cvg : forall x:R, Un_cv (B1 x) (sin x). @@ -339,21 +313,14 @@ simpl; ring. rewrite tech5; rewrite <- Hrecn. simpl; ring. unfold ge; apply le_O_n. -assert (H0 := exist_sin (x * x)). -elim H0; intros. -assert (p_i := p). -unfold sin_in in p. -unfold sin_n, infinite_sum in p. -unfold R_dist in p. -cut (sin x = x * x0). -intro. -rewrite H1. -unfold Un_cv; unfold R_dist; intros. +unfold sin. destruct (exist_sin (Rsqr x)) as (x0,p). +unfold sin_in, sin_n, infinite_sum, R_dist in p. +unfold Un_cv, R_dist; intros. cut (0 < eps / Rabs x); [ intro | unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption ] ]. -elim (p (eps / Rabs x) H3); intros. +destruct (p (eps / Rabs x) H1) as (x1,H2). exists x1; intros. unfold B1. replace @@ -371,9 +338,7 @@ replace rewrite Rabs_mult. apply Rmult_lt_reg_l with (/ Rabs x). apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. -rewrite <- Rmult_assoc. -rewrite <- Rinv_l_sym. -rewrite Rmult_1_l; rewrite <- (Rmult_comm eps); unfold Rdiv in H4; apply H4; +rewrite <- Rmult_assoc, <- Rinv_l_sym, Rmult_1_l, <- (Rmult_comm eps). apply H2; assumption. apply Rabs_no_R0; assumption. rewrite scal_sum. @@ -383,12 +348,4 @@ rewrite pow_add. rewrite pow_sqr. simpl. ring. -unfold sin. -case (exist_sin (Rsqr x)). -unfold Rsqr; intros. -unfold sin_in in p_i. -unfold sin_in in s. -assert - (H1 := uniqueness_sum (fun i:nat => sin_n i * (x * x) ^ i) x0 x1 p_i s). -rewrite H1; reflexivity. Qed. diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v index dbf48e61a..160f3d480 100644 --- a/theories/Reals/Exp_prop.v +++ b/theories/Reals/Exp_prop.v @@ -723,15 +723,14 @@ Qed. (**********) Lemma exp_pos : forall x:R, 0 < exp x. Proof. - intro; case (total_order_T 0 x); intro. - elim s; intro. - apply (exp_pos_pos _ a). - rewrite <- b; rewrite exp_0; apply Rlt_0_1. + intro; destruct (total_order_T 0 x) as [[Hlt|<-]|Hgt]. + apply (exp_pos_pos _ Hlt). + rewrite exp_0; apply Rlt_0_1. replace (exp x) with (1 / exp (- x)). unfold Rdiv; apply Rmult_lt_0_compat. apply Rlt_0_1. apply Rinv_0_lt_compat; apply exp_pos_pos. - apply (Ropp_0_gt_lt_contravar _ r). + apply (Ropp_0_gt_lt_contravar _ Hgt). cut (exp (- x) <> 0). intro; unfold Rdiv; apply Rmult_eq_reg_l with (exp (- x)). rewrite Rmult_1_l; rewrite <- Rinv_r_sym. @@ -772,10 +771,10 @@ Proof. apply (not_eq_sym H6). rewrite Rminus_0_r; apply H7. unfold SFL. - case (cv 0); intros. + case (cv 0) as (x,Hu). eapply UL_sequence. - apply u. - unfold Un_cv, SP. + apply Hu. + unfold Un_cv, SP in |- *. intros; exists 1%nat; intros. unfold R_dist; rewrite decomp_sum. rewrite (Rplus_comm (fn 0%nat 0)). @@ -792,14 +791,13 @@ Proof. unfold Rdiv; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. apply lt_le_trans with 1%nat; [ apply lt_n_Sn | apply H9 ]. unfold SFL, exp. - case (cv h); case (exist_exp h); simpl; intros. + case (cv h) as (x0,Hu); case (exist_exp h) as (x,Hexp); simpl. eapply UL_sequence. - apply u. + apply Hu. unfold Un_cv; intros. - unfold exp_in in e. - unfold infinite_sum in e. + unfold exp_in, infinite_sum in Hexp. cut (0 < eps0 * Rabs h). - intro; elim (e _ H9); intros N0 H10. + intro; elim (Hexp _ H9); intros N0 H10. exists N0; intros. unfold R_dist. apply Rmult_lt_reg_l with (Rabs h). diff --git a/theories/Reals/MVT.v b/theories/Reals/MVT.v index 5cada6c5f..4b8d9af48 100644 --- a/theories/Reals/MVT.v +++ b/theories/Reals/MVT.v @@ -233,21 +233,18 @@ Proof. intros. unfold increasing. intros. - case (total_order_T x y); intro. - elim s; intro. + destruct (total_order_T x y) as [[H1| ->]|H1]. apply Rplus_le_reg_l with (- f x). rewrite Rplus_opp_l; rewrite Rplus_comm. - assert (H1 := MVT_cor1 f _ _ pr a). - elim H1; intros. - elim H2; intros. + pose proof (MVT_cor1 f _ _ pr H1) as (c & H3 & H4). unfold Rminus in H3. rewrite H3. apply Rmult_le_pos. apply H. apply Rplus_le_reg_l with x. rewrite Rplus_0_r; replace (x + (y + - x)) with y; [ assumption | ring ]. - rewrite b; right; reflexivity. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)). + right; reflexivity. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 H1)). Qed. (**********) @@ -269,7 +266,7 @@ Proof. cut ((f (x + delta / 2) - f x) / (delta / 2) <= 0). intro; cut (0 < - ((f (x + delta / 2) - f x) / (delta / 2) - l)). intro; unfold Rabs; - case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)). + case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)) as [Hlt|Hge]. intros; generalize (Rplus_lt_compat_r (- l) (- ((f (x + delta / 2) - f x) / (delta / 2) - l)) @@ -294,7 +291,7 @@ Proof. ring. intros. generalize - (Ropp_ge_le_contravar ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 r). + (Ropp_ge_le_contravar ((f (x + delta / 2) - f x) / (delta / 2) - l) _ Hge). rewrite Ropp_0. intro. elim @@ -587,12 +584,8 @@ Theorem IAF : f b - f a <= k * (b - a). Proof. intros. - case (total_order_T a b); intro. - elim s; intro. - assert (H1 := MVT_cor1 f _ _ pr a0). - elim H1; intros. - elim H2; intros. - rewrite H3. + destruct (total_order_T a b) as [[H1| -> ]|H1]. + pose proof (MVT_cor1 f _ _ pr H1) as (c & -> & H4). do 2 rewrite <- (Rmult_comm (b - a)). apply Rmult_le_compat_l. apply Rplus_le_reg_l with a; rewrite Rplus_0_r. @@ -600,10 +593,9 @@ Proof. apply H0. elim H4; intros. split; left; assumption. - rewrite b0. unfold Rminus; do 2 rewrite Rplus_opp_r. rewrite Rmult_0_r; right; reflexivity. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H H1)). Qed. Lemma IAF_var : @@ -648,8 +640,7 @@ Lemma null_derivative_loc : (forall (x:R) (P:a < x < b), derive_pt f x (pr x P) = 0) -> constant_D_eq f (fun x:R => a <= x <= b) (f a). Proof. - intros; unfold constant_D_eq; intros; case (total_order_T a b); intro. - elim s; intro. + intros; unfold constant_D_eq; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. assert (H2 : forall y:R, a < y < x -> derivable_pt id y). intros; apply derivable_pt_id. assert (H3 : forall y:R, a <= y <= x -> continuity_pt id y). @@ -678,10 +669,10 @@ Proof. assumption. rewrite H1; reflexivity. assert (H2 : x = a). - rewrite <- b0 in H1; elim H1; intros; apply Rle_antisym; assumption. + rewrite <- Heq in H1; elim H1; intros; apply Rle_antisym; assumption. rewrite H2; reflexivity. elim H1; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H2 H3) r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H2 H3) Hgt)). Qed. (* Unicity of the antiderivative *) diff --git a/theories/Reals/NewtonInt.v b/theories/Reals/NewtonInt.v index f67659b5b..928422ed8 100644 --- a/theories/Reals/NewtonInt.v +++ b/theories/Reals/NewtonInt.v @@ -87,42 +87,7 @@ Lemma NewtonInt_P4 : forall (f:R -> R) (a b:R) (pr:Newton_integrable f a b), NewtonInt f a b pr = - NewtonInt f b a (NewtonInt_P3 f a b pr). Proof. - intros; unfold Newton_integrable in pr; elim pr; intros; elim p; intro. - unfold NewtonInt; - case - (NewtonInt_P3 f a b - (exist - (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x - p)). - intros; elim o; intro. - unfold antiderivative in H0; elim H0; intros; elim H2; intro. - unfold antiderivative in H; elim H; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)). - rewrite H3; ring. - assert (H1 := antiderivative_Ucte f x x0 a b H H0); elim H1; intros; - unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - assert (H3 : a <= a <= b). - split; [ right; reflexivity | assumption ]. - assert (H4 : a <= b <= b). - split; [ assumption | right; reflexivity ]. - assert (H5 := H2 _ H3); assert (H6 := H2 _ H4); rewrite H5; rewrite H6; ring. - unfold NewtonInt; - case - (NewtonInt_P3 f a b - (exist - (fun g:R -> R => antiderivative f g a b \/ antiderivative f g b a) x - p)); intros; elim o; intro. - assert (H1 := antiderivative_Ucte f x x0 b a H H0); elim H1; intros; - unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - assert (H3 : b <= a <= a). - split; [ assumption | right; reflexivity ]. - assert (H4 : b <= b <= a). - split; [ right; reflexivity | assumption ]. - assert (H5 := H2 _ H3); assert (H6 := H2 _ H4); rewrite H5; rewrite H6; ring. - unfold antiderivative in H0; elim H0; intros; elim H2; intro. - unfold antiderivative in H; elim H; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H5 H3)). - rewrite H3; ring. + intros f a b (x,H). unfold NewtonInt, NewtonInt_P3; simpl; ring. Qed. (* The set of Newton integrable functions is a vectorial space *) @@ -227,10 +192,8 @@ Lemma NewtonInt_P6 : l * NewtonInt f a b pr1 + NewtonInt g a b pr2. Proof. intros f g l a b pr1 pr2; unfold NewtonInt; - case (NewtonInt_P5 f g l a b pr1 pr2); intros; case pr1; - intros; case pr2; intros; case (total_order_T a b); - intro. - elim s; intro. + destruct (NewtonInt_P5 f g l a b pr1 pr2) as (x,o); destruct pr1 as (x0,o0); + destruct pr2 as (x1,o1); destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. elim o; intro. elim o0; intro. elim o1; intro. @@ -242,21 +205,21 @@ Proof. split; [ left; assumption | right; reflexivity ]. assert (H7 := H4 _ H5); assert (H8 := H4 _ H6); rewrite H7; rewrite H8; ring. unfold antiderivative in H1; elim H1; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 Hlt)). unfold antiderivative in H0; elim H0; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). unfold antiderivative in H; elim H; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 a0)). - rewrite b0; ring. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 Hlt)). + rewrite Heq; ring. elim o; intro. unfold antiderivative in H; elim H; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 Hgt)). elim o0; intro. unfold antiderivative in H0; elim H0; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hgt)). elim o1; intro. unfold antiderivative in H1; elim H1; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H3 Hgt)). assert (H2 := antiderivative_P1 f g x0 x1 l b a H0 H1); assert (H3 := antiderivative_Ucte _ _ _ _ _ H H2); elim H3; intros; assert (H5 : b <= a <= a). @@ -277,14 +240,12 @@ Lemma antiderivative_P2 : | right _ => F1 x + (F0 b - F1 b) end) a c. Proof. - unfold antiderivative; intros; elim H; clear H; intros; elim H0; - clear H0; intros; split. + intros; destruct H as (H,H1), H0 as (H0,H2); split. 2: apply Rle_trans with b; assumption. - intros; elim H3; clear H3; intros; case (total_order_T x b); intro. - elim s; intro. + intros x (H3,H4); destruct (total_order_T x b) as [[Hlt|Heq]|Hgt]. assert (H5 : a <= x <= b). split; [ assumption | left; assumption ]. - assert (H6 := H _ H5); elim H6; clear H6; intros; + destruct (H _ H5) as (x0,H6). assert (H7 : derivable_pt_lim @@ -293,27 +254,26 @@ Proof. | left _ => F0 x | right _ => F1 x + (F0 b - F1 b) end) x (f x)). - unfold derivable_pt_lim; assert (H7 : derive_pt F0 x x0 = f x). - symmetry ; assumption. - assert (H8 := derive_pt_eq_1 F0 x (f x) x0 H7); unfold derivable_pt_lim in H8; - intros; elim (H8 _ H9); intros; set (D := Rmin x1 (b - x)). + unfold derivable_pt_lim. intros eps H9. + assert (H7 : derive_pt F0 x x0 = f x) by (symmetry; assumption). + destruct (derive_pt_eq_1 F0 x (f x) x0 H7 _ H9) as (x1,H10); set (D := Rmin x1 (b - x)). assert (H11 : 0 < D). - unfold D; unfold Rmin; case (Rle_dec x1 (b - x)); intro. + unfold D, Rmin; case (Rle_dec x1 (b - x)); intro. apply (cond_pos x1). apply Rlt_Rminus; assumption. - exists (mkposreal _ H11); intros; case (Rle_dec x b); intro. - case (Rle_dec (x + h) b); intro. + exists (mkposreal _ H11); intros h H12 H13. case (Rle_dec x b) as [|[]]. + case (Rle_dec (x + h) b) as [|[]]. apply H10. assumption. apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. - elim n; left; apply Rlt_le_trans with (x + D). + left; apply Rlt_le_trans with (x + D). apply Rplus_lt_compat_l; apply Rle_lt_trans with (Rabs h). apply RRle_abs. apply H13. apply Rplus_le_reg_l with (- x); rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; rewrite Rplus_comm; unfold D; apply Rmin_r. - elim n; left; assumption. + left; assumption. assert (H8 : derivable_pt @@ -348,7 +308,7 @@ Proof. unfold D; unfold Rmin; case (Rle_dec x2 x3); intro. apply (cond_pos x2). apply (cond_pos x3). - exists (mkposreal _ H16); intros; case (Rle_dec x b); intro. + exists (mkposreal _ H16); intros; case (Rle_dec x b) as [|[]]. case (Rle_dec (x + h) b); intro. apply H15. assumption. @@ -357,8 +317,8 @@ Proof. apply H14. assumption. apply Rlt_le_trans with D; [ assumption | unfold D; apply Rmin_l ]. - rewrite b0; ring. - elim n; right; assumption. + rewrite Heq; ring. + right; assumption. assert (H14 : derivable_pt @@ -388,11 +348,11 @@ Proof. unfold D; unfold Rmin; case (Rle_dec x1 (x - b)); intro. apply (cond_pos x1). apply Rlt_Rminus; assumption. - exists (mkposreal _ H11); intros; case (Rle_dec x b); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 r)). - case (Rle_dec (x + h) b); intro. + exists (mkposreal _ H11); intros; destruct (Rle_dec x b) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt)). + destruct (Rle_dec (x + h) b) as [Hle'|Hnle']. cut (b < x + h). - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H14)). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H14)). apply Rplus_lt_reg_l with (- h - b); replace (- h - b + b) with (- h); [ idtac | ring ]; replace (- h - b + (x + h)) with (x - b); [ idtac | ring ]; apply Rle_lt_trans with (Rabs h). @@ -425,8 +385,7 @@ Lemma antiderivative_P3 : antiderivative f F1 c a \/ antiderivative f F0 a c. Proof. intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0; - intros; case (total_order_T a c); intro. - elim s; intro. + intros; destruct (total_order_T a c) as [[Hle|Heq]|Hgt]. right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ assumption | apply Rle_trans with c; assumption ]. @@ -448,8 +407,7 @@ Lemma antiderivative_P4 : antiderivative f F1 b c \/ antiderivative f F0 c b. Proof. intros; unfold antiderivative in H, H0; elim H; clear H; elim H0; clear H0; - intros; case (total_order_T c b); intro. - elim s; intro. + intros; destruct (total_order_T c b) as [[Hlt|Heq]|Hgt]. right; unfold antiderivative; split. intros; apply H1; elim H3; intros; split; [ apply Rle_trans with c; assumption | assumption ]. @@ -499,10 +457,8 @@ Proof. intros. elim X; intros F0 H0. elim X0; intros F1 H1. - case (total_order_T a b); intro. - elim s; intro. - case (total_order_T b c); intro. - elim s0; intro. + destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. + destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. (* a<b & b<c *) unfold Newton_integrable; exists @@ -515,78 +471,75 @@ Proof. elim H1; intro. left; apply antiderivative_P2; assumption. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a1)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt')). unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). (* a<b & b=c *) - rewrite b0 in X; apply X. + rewrite Heq' in X; apply X. (* a<b & b>c *) - case (total_order_T a c); intro. - elim s0; intro. + destruct (total_order_T a c) as [[Hlt''|Heq'']|Hgt'']. unfold Newton_integrable; exists F0. left. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). elim H0; intro. assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H). elim H3; intro. unfold antiderivative in H4; elim H4; clear H4; intros _ H4. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 a1)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hlt'')). assumption. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). - rewrite b0; apply NewtonInt_P1. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). + rewrite Heq''; apply NewtonInt_P1. unfold Newton_integrable; exists F1. right. elim H1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). elim H0; intro. assert (H3 := antiderivative_P3 f F0 F1 a b c H2 H). elim H3; intro. assumption. unfold antiderivative in H4; elim H4; clear H4; intros _ H4. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 r0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hgt'')). unfold antiderivative in H2; elim H2; clear H2; intros _ H2. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt)). (* a=b *) - rewrite b0; apply X0. - case (total_order_T b c); intro. - elim s; intro. + rewrite Heq; apply X0. + destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. (* a>b & b<c *) - case (total_order_T a c); intro. - elim s0; intro. + destruct (total_order_T a c) as [[Hlt''|Heq'']|Hgt'']. unfold Newton_integrable; exists F1. left. elim H1; intro. (*****************) elim H0; intro. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hgt)). assert (H3 := antiderivative_P4 f F0 F1 b a c H2 H). elim H3; intro. assumption. unfold antiderivative in H4; elim H4; clear H4; intros _ H4. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 a1)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hlt'')). unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). - rewrite b0; apply NewtonInt_P1. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt')). + rewrite Heq''; apply NewtonInt_P1. unfold Newton_integrable; exists F0. right. elim H0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). elim H1; intro. assert (H3 := antiderivative_P4 f F0 F1 b a c H H2). elim H3; intro. unfold antiderivative in H4; elim H4; clear H4; intros _ H4. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 r0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 Hgt'')). assumption. unfold antiderivative in H2; elim H2; clear H2; intros _ H2. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H2 Hlt')). (* a>b & b=c *) - rewrite b0 in X; apply X. + rewrite Heq' in X; apply X. (* a>b & b>c *) assert (X1 := NewtonInt_P3 f a b X). assert (X2 := NewtonInt_P3 f b c X0). @@ -602,17 +555,15 @@ Lemma NewtonInt_P9 : NewtonInt f a b pr1 + NewtonInt f b c pr2. Proof. intros; unfold NewtonInt. - case (NewtonInt_P8 f a b c pr1 pr2); intros. - case pr1; intros. - case pr2; intros. - case (total_order_T a b); intro. - elim s; intro. - case (total_order_T b c); intro. - elim s0; intro. + case (NewtonInt_P8 f a b c pr1 pr2) as (x,Hor). + case pr1 as (x0,Hor0). + case pr2 as (x1,Hor1). + destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. + destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. (* a<b & b<c *) - elim o0; intro. - elim o1; intro. - elim o; intro. + case Hor0; intro. + case Hor1; intro. + case Hor; intro. assert (H2 := antiderivative_P2 f x0 x1 a b c H H0). assert (H3 := @@ -628,23 +579,23 @@ Proof. assert (H6 : a <= c <= c). split; [ left; apply Rlt_trans with b; assumption | right; reflexivity ]. rewrite (H4 _ H5); rewrite (H4 _ H6). - case (Rle_dec a b); intro. - case (Rle_dec c b); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 a1)). + destruct (Rle_dec a b) as [Hlea|Hnlea]. + destruct (Rle_dec c b) as [Hlec|Hnlec]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlec Hlt')). ring. - elim n; left; assumption. + elim Hnlea; left; assumption. unfold antiderivative in H1; elim H1; clear H1; intros _ H1. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ a0 a1))). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ Hlt Hlt'))). unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a1)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt')). unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). (* a<b & b=c *) - rewrite <- b0. + rewrite <- Heq'. unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. - rewrite <- b0 in o. - elim o0; intro. - elim o; intro. + rewrite <- Heq' in Hor. + elim Hor0; intro. + elim Hor; intro. assert (H1 := antiderivative_Ucte f x x0 a b H0 H). elim H1; intros. rewrite (H2 b). @@ -653,25 +604,25 @@ Proof. split; [ right; reflexivity | left; assumption ]. split; [ left; assumption | right; reflexivity ]. unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt)). unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hlt)). (* a<b & b>c *) - elim o1; intro. + elim Hor1; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). - elim o0; intro. - elim o; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt')). + elim Hor0; intro. + elim Hor; intro. assert (H2 := antiderivative_P2 f x x1 a c b H1 H). assert (H3 := antiderivative_Ucte _ _ _ a b H0 H2). elim H3; intros. rewrite (H4 a). rewrite (H4 b). - case (Rle_dec b c); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 r)). - case (Rle_dec a c); intro. + destruct (Rle_dec b c) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt')). + destruct (Rle_dec a c) as [Hle'|Hnle']. ring. - elim n0; unfold antiderivative in H1; elim H1; intros; assumption. + elim Hnle'; unfold antiderivative in H1; elim H1; intros; assumption. split; [ left; assumption | right; reflexivity ]. split; [ right; reflexivity | left; assumption ]. assert (H2 := antiderivative_P2 _ _ _ _ _ _ H1 H0). @@ -679,19 +630,19 @@ Proof. elim H3; intros. rewrite (H4 c). rewrite (H4 b). - case (Rle_dec b a); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 a0)). - case (Rle_dec c a); intro. + destruct (Rle_dec b a) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hlt)). + destruct (Rle_dec c a) as [Hle'|[]]. ring. - elim n0; unfold antiderivative in H1; elim H1; intros; assumption. + unfold antiderivative in H1; elim H1; intros; assumption. split; [ left; assumption | right; reflexivity ]. split; [ right; reflexivity | left; assumption ]. unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt)). (* a=b *) - rewrite b0 in o; rewrite b0. - elim o; intro. - elim o1; intro. + rewrite Heq in Hor |- *. + elim Hor; intro. + elim Hor1; intro. assert (H1 := antiderivative_Ucte _ _ _ b c H H0). elim H1; intros. assert (H3 : b <= c). @@ -705,7 +656,7 @@ Proof. unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym; assumption. rewrite H1; ring. - elim o1; intro. + elim Hor1; intro. assert (H1 : b = c). unfold antiderivative in H, H0; elim H; elim H0; intros; apply Rle_antisym; assumption. @@ -720,25 +671,24 @@ Proof. split; [ assumption | right; reflexivity ]. split; [ right; reflexivity | assumption ]. (* a>b & b<c *) - case (total_order_T b c); intro. - elim s; intro. - elim o0; intro. + destruct (total_order_T b c) as [[Hlt'|Heq']|Hgt']. + elim Hor0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). - elim o1; intro. - elim o; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). + elim Hor1; intro. + elim Hor; intro. assert (H2 := antiderivative_P2 _ _ _ _ _ _ H H1). assert (H3 := antiderivative_Ucte _ _ _ b c H0 H2). elim H3; intros. rewrite (H4 b). rewrite (H4 c). - case (Rle_dec b a); intro. - case (Rle_dec c a); intro. + case (Rle_dec b a) as [|[]]. + case (Rle_dec c a) as [|]. assert (H5 : a = c). unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption. rewrite H5; ring. ring. - elim n; left; assumption. + left; assumption. split; [ left; assumption | right; reflexivity ]. split; [ right; reflexivity | left; assumption ]. assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H1). @@ -746,27 +696,27 @@ Proof. elim H3; intros. rewrite (H4 a). rewrite (H4 b). - case (Rle_dec b c); intro. - case (Rle_dec a c); intro. + case (Rle_dec b c) as [|[]]. + case (Rle_dec a c) as [|]. assert (H5 : a = c). unfold antiderivative in H1; elim H1; intros; apply Rle_antisym; assumption. rewrite H5; ring. ring. - elim n; left; assumption. + left; assumption. split; [ right; reflexivity | left; assumption ]. split; [ left; assumption | right; reflexivity ]. unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 a0)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hlt')). (* a>b & b=c *) - rewrite <- b0. + rewrite <- Heq'. unfold Rminus; rewrite Rplus_opp_r; rewrite Rplus_0_r. - rewrite <- b0 in o. - elim o0; intro. + rewrite <- Heq' in Hor. + elim Hor0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). - elim o; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). + elim Hor; intro. unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgt)). assert (H1 := antiderivative_Ucte f x x0 b a H0 H). elim H1; intros. rewrite (H2 b). @@ -775,15 +725,15 @@ Proof. split; [ left; assumption | right; reflexivity ]. split; [ right; reflexivity | left; assumption ]. (* a>b & b>c *) - elim o0; intro. + elim Hor0; intro. unfold antiderivative in H; elim H; clear H; intros _ H. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). - elim o1; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). + elim Hor1; intro. unfold antiderivative in H0; elim H0; clear H0; intros _ H0. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 r0)). - elim o; intro. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H0 Hgt')). + elim Hor; intro. unfold antiderivative in H1; elim H1; clear H1; intros _ H1. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ r0 r))). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 (Rlt_trans _ _ _ Hgt' Hgt))). assert (H2 := antiderivative_P2 _ _ _ _ _ _ H0 H). assert (H3 := antiderivative_Ucte _ _ _ c a H1 H2). elim H3; intros. @@ -791,11 +741,11 @@ Proof. unfold antiderivative in H1; elim H1; intros; assumption. rewrite (H4 c). rewrite (H4 a). - case (Rle_dec a b); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r1 r)). - case (Rle_dec c b); intro. + destruct (Rle_dec a b) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle Hgt)). + destruct (Rle_dec c b) as [|[]]. ring. - elim n0; left; assumption. + left; assumption. split; [ assumption | right; reflexivity ]. split; [ right; reflexivity | assumption ]. Qed. diff --git a/theories/Reals/PartSum.v b/theories/Reals/PartSum.v index 59e52fe3a..10c3327f2 100644 --- a/theories/Reals/PartSum.v +++ b/theories/Reals/PartSum.v @@ -508,12 +508,11 @@ Lemma sum_incr : Un_cv (fun n:nat => sum_f_R0 An n) l -> (forall n:nat, 0 <= An n) -> sum_f_R0 An N <= l. Proof. - intros; case (total_order_T (sum_f_R0 An N) l); intro. - elim s; intro. - left; apply a. - right; apply b. + intros; destruct (total_order_T (sum_f_R0 An N) l) as [[Hlt|Heq]|Hgt]. + left; apply Hlt. + right; apply Heq. cut (Un_growing (fun n:nat => sum_f_R0 An n)). - intro; set (l1 := sum_f_R0 An N) in r. + intro; set (l1 := sum_f_R0 An N) in Hgt. unfold Un_cv in H; cut (0 < l1 - l). intro; elim (H _ H2); intros. set (N0 := max x N); cut (N0 >= x)%nat. @@ -528,7 +527,7 @@ Proof. apply Rle_ge; apply Rplus_le_reg_l with l. rewrite Rplus_0_r; replace (l + (sum_f_R0 An N0 - l)) with (sum_f_R0 An N0); [ idtac | ring ]; apply Rle_trans with l1. - left; apply r. + left; apply Hgt. apply H6. unfold l1; apply Rge_le; apply (growing_prop (fun k:nat => sum_f_R0 An k)). @@ -536,7 +535,7 @@ Proof. unfold ge, N0; apply le_max_r. unfold ge, N0; apply le_max_l. apply Rplus_lt_reg_l with l; rewrite Rplus_0_r; - replace (l + (l1 - l)) with l1; [ apply r | ring ]. + replace (l + (l1 - l)) with l1; [ apply Hgt | ring ]. unfold Un_growing; intro; simpl; pattern (sum_f_R0 An n) at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; apply H0. @@ -549,10 +548,9 @@ Lemma sum_cv_maj : Un_cv (fun n:nat => sum_f_R0 An n) l2 -> (forall n:nat, Rabs (fn n x) <= An n) -> Rabs l1 <= l2. Proof. - intros; case (total_order_T (Rabs l1) l2); intro. - elim s; intro. - left; apply a. - right; apply b. + intros; destruct (total_order_T (Rabs l1) l2) as [[Hlt|Heq]|Hgt]. + left; apply Hlt. + right; apply Heq. cut (forall n0:nat, Rabs (SP fn n0 x) <= sum_f_R0 An n0). intro; cut (0 < (Rabs l1 - l2) / 2). intro; unfold Un_cv in H, H0. @@ -568,16 +566,16 @@ Proof. intro; assert (H11 := H2 N). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H10)). apply Rlt_trans with ((Rabs l1 + l2) / 2); assumption. - case (Rcase_abs (Rabs l1 - Rabs (SP fn N x))); intro. + destruct (Rcase_abs (Rabs l1 - Rabs (SP fn N x))) as [Hlt|Hge]. apply Rlt_trans with (Rabs l1). apply Rmult_lt_reg_l with 2. prove_sup0. unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym. - rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply r. + rewrite Rmult_1_r; rewrite double; apply Rplus_lt_compat_l; apply Hgt. discrR. - apply (Rminus_lt _ _ r0). - rewrite (Rabs_right _ r0) in H7. + apply (Rminus_lt _ _ Hlt). + rewrite (Rabs_right _ Hge) in H7. apply Rplus_lt_reg_l with ((Rabs l1 - l2) / 2 - Rabs (SP fn N x)). replace ((Rabs l1 - l2) / 2 - Rabs (SP fn N x) + (Rabs l1 + l2) / 2) with (Rabs l1 - Rabs (SP fn N x)). @@ -586,18 +584,18 @@ Proof. unfold Rdiv; rewrite Rmult_plus_distr_r; rewrite <- (Rmult_comm (/ 2)); rewrite Rmult_minus_distr_l; repeat rewrite (Rmult_comm (/ 2)); pattern (Rabs l1) at 1; - rewrite double_var; unfold Rdiv; ring. - case (Rcase_abs (sum_f_R0 An N - l2)); intro. + rewrite double_var; unfold Rdiv in |- *; ring. + destruct (Rcase_abs (sum_f_R0 An N - l2)) as [Hlt|Hge]. apply Rlt_trans with l2. - apply (Rminus_lt _ _ r0). + apply (Rminus_lt _ _ Hlt). apply Rmult_lt_reg_l with 2. prove_sup0. rewrite (double l2); unfold Rdiv; rewrite (Rmult_comm 2); rewrite Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_r; rewrite (Rplus_comm (Rabs l1)); apply Rplus_lt_compat_l; - apply r. + apply Hgt. discrR. - rewrite (Rabs_right _ r0) in H6; apply Rplus_lt_reg_l with (- l2). + rewrite (Rabs_right _ Hge) in H6; apply Rplus_lt_reg_l with (- l2). replace (- l2 + (Rabs l1 + l2) / 2) with ((Rabs l1 - l2) / 2). rewrite Rplus_comm; apply H6. unfold Rdiv; rewrite <- (Rmult_comm (/ 2)); @@ -612,7 +610,7 @@ Proof. unfold Rdiv; apply Rmult_lt_0_compat. apply Rplus_lt_reg_l with l2. rewrite Rplus_0_r; replace (l2 + (Rabs l1 - l2)) with (Rabs l1); - [ apply r | ring ]. + [ apply Hgt | ring ]. apply Rinv_0_lt_compat; prove_sup0. intros; induction n0 as [| n0 Hrecn0]. unfold SP; simpl; apply H1. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index acc9fd5d6..cb75500d0 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -682,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. @@ -695,6 +700,11 @@ 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. diff --git a/theories/Reals/R_sqr.v b/theories/Reals/R_sqr.v index d6e18d9d8..24fe26613 100644 --- a/theories/Reals/R_sqr.v +++ b/theories/Reals/R_sqr.v @@ -97,7 +97,7 @@ Qed. Lemma Rsqr_incr_0 : forall x y:R, Rsqr x <= Rsqr y -> 0 <= x -> 0 <= y -> x <= y. Proof. - intros; case (Rle_dec x y); intro; + intros; destruct (Rle_dec x y) as [Hle|Hnle]; [ assumption | cut (y < x); [ intro; unfold Rsqr in H; @@ -109,7 +109,7 @@ Qed. Lemma Rsqr_incr_0_var : forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> x <= y. Proof. - intros; case (Rle_dec x y); intro; + intros; destruct (Rle_dec x y) as [Hle|Hnle]; [ assumption | cut (y < x); [ intro; unfold Rsqr in H; @@ -146,8 +146,8 @@ Qed. Lemma Rsqr_neg_pos_le_0 : forall x y:R, Rsqr x <= Rsqr y -> 0 <= y -> - y <= x. Proof. - intros; case (Rcase_abs x); intro. - generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; + intros; destruct (Rcase_abs x) as [Hlt|Hle]. + generalize (Ropp_lt_gt_contravar x 0 Hlt); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H1); intro; rewrite (Rsqr_neg x) in H; generalize (Rsqr_incr_0 (- x) y H H2 H0); intro; rewrite <- (Ropp_involutive x); apply Ropp_ge_le_contravar; @@ -160,25 +160,23 @@ Qed. Lemma Rsqr_neg_pos_le_1 : forall x y:R, - y <= x -> x <= y -> 0 <= y -> Rsqr x <= Rsqr y. Proof. - intros; case (Rcase_abs x); intro. - generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Rlt_le 0 (- x) H2); intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; - intro; generalize (Rge_le y (- x) H4); intro; rewrite (Rsqr_neg x); - apply Rsqr_incr_1; assumption. - generalize (Rge_le x 0 r); intro; apply Rsqr_incr_1; assumption. + intros x y H H0 H1; destruct (Rcase_abs x) as [Hlt|Hle]. + apply Ropp_lt_gt_contravar, Rlt_le in Hlt; rewrite Ropp_0 in Hlt; + apply Ropp_le_ge_contravar, Rge_le in H; rewrite Ropp_involutive in H; + rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. + apply Rge_le in Hle; apply Rsqr_incr_1; assumption. Qed. Lemma neg_pos_Rsqr_le : forall x y:R, - y <= x -> x <= y -> Rsqr x <= Rsqr y. Proof. - intros; case (Rcase_abs x); intro. - generalize (Ropp_lt_gt_contravar x 0 r); rewrite Ropp_0; intro; - generalize (Ropp_le_ge_contravar (- y) x H); rewrite Ropp_involutive; - intro; generalize (Rge_le y (- x) H2); intro; generalize (Rlt_le 0 (- x) H1); - intro; generalize (Rle_trans 0 (- x) y H4 H3); intro; - rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. - generalize (Rge_le x 0 r); intro; generalize (Rle_trans 0 x y H1 H0); intro; - apply Rsqr_incr_1; assumption. + intros x y H H0; destruct (Rcase_abs x) as [Hlt|Hle]. + apply Ropp_lt_gt_contravar, Rlt_le in Hlt; rewrite Ropp_0 in Hlt; + apply Ropp_le_ge_contravar, Rge_le in H; rewrite Ropp_involutive in H. + assert (0 <= y) by (apply Rle_trans with (-x); assumption). + rewrite (Rsqr_neg x); apply Rsqr_incr_1; assumption. + apply Rge_le in Hle; + assert (0 <= y) by (apply Rle_trans with x; assumption). + apply Rsqr_incr_1; assumption. Qed. Lemma Rsqr_abs : forall x:R, Rsqr x = Rsqr (Rabs x). @@ -220,22 +218,22 @@ Qed. Lemma Rsqr_eq_abs_0 : forall x y:R, Rsqr x = Rsqr y -> Rabs x = Rabs y. Proof. - intros; unfold Rabs; case (Rcase_abs x); case (Rcase_abs y); intros. - rewrite (Rsqr_neg x) in H; rewrite (Rsqr_neg y) in H; - generalize (Ropp_lt_gt_contravar y 0 r); - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + intros; unfold Rabs; case (Rcase_abs x) as [Hltx|Hgex]; + case (Rcase_abs y) as [Hlty|Hgey]. + rewrite (Rsqr_neg x), (Rsqr_neg y) in H; + generalize (Ropp_lt_gt_contravar y 0 Hlty); + generalize (Ropp_lt_gt_contravar x 0 Hltx); rewrite Ropp_0; intros; generalize (Rlt_le 0 (- x) H0); generalize (Rlt_le 0 (- y) H1); intros; apply Rsqr_inj; assumption. - rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 r); intro; - generalize (Ropp_lt_gt_contravar x 0 r0); rewrite Ropp_0; + rewrite (Rsqr_neg x) in H; generalize (Rge_le y 0 Hgey); intro; + generalize (Ropp_lt_gt_contravar x 0 Hltx); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- x) H1); intro; apply Rsqr_inj; assumption. - rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 r0); intro; - generalize (Ropp_lt_gt_contravar y 0 r); rewrite Ropp_0; + rewrite (Rsqr_neg y) in H; generalize (Rge_le x 0 Hgex); intro; + generalize (Ropp_lt_gt_contravar y 0 Hlty); rewrite Ropp_0; intro; generalize (Rlt_le 0 (- y) H1); intro; apply Rsqr_inj; assumption. - generalize (Rge_le x 0 r0); generalize (Rge_le y 0 r); intros; apply Rsqr_inj; - assumption. + apply Rsqr_inj; auto using Rge_le. Qed. Lemma Rsqr_eq_asb_1 : forall x y:R, Rabs x = Rabs y -> Rsqr x = Rsqr y. diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v index 2d9419bdf..19e111f23 100644 --- a/theories/Reals/R_sqrt.v +++ b/theories/Reals/R_sqrt.v @@ -37,8 +37,8 @@ Lemma sqrt_sqrt : forall x:R, 0 <= x -> sqrt x * sqrt x = x. Proof. intros. unfold sqrt. - case (Rcase_abs x); intro. - elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ r H)). + case (Rcase_abs x) as [Hlt|Hge]. + elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ Hlt H)). rewrite Rsqrt_Rsqrt; reflexivity. Qed. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 5cdb39dd6..0409c99e4 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -1123,7 +1123,7 @@ Proof. case (Rcase_abs ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / - Rmin (delta / 2) ((b + - c) / 2) + - l)); intro. + Rmin (delta / 2) ((b + - c) / 2) + - l)) as [Hlt|Hge]. replace (- ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / @@ -1165,7 +1165,7 @@ Proof. (H20 := Rge_le ((f (c + Rmin (delta / 2) ((b + - c) / 2)) + - f c) / - Rmin (delta / 2) ((b + - c) / 2) + - l) 0 r). + Rmin (delta / 2) ((b + - c) / 2) + - l) 0 Hge). elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H20 H18)). assumption. rewrite <- Ropp_0; @@ -1242,17 +1242,16 @@ Proof. (mkposreal ((b - c) / 2) H8)). unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. - unfold Rabs; case (Rcase_abs (Rmin (delta / 2) ((b - c) / 2))). - intro. + unfold Rabs; case (Rcase_abs (Rmin (delta / 2) ((b - c) / 2))) as [Hlt|Hge]. cut (0 < delta / 2). intro. generalize (Rmin_stable_in_posreal (mkposreal (delta / 2) H10) (mkposreal ((b - c) / 2) H8)); simpl; intro; - elim (Rlt_irrefl 0 (Rlt_trans 0 (Rmin (delta / 2) ((b - c) / 2)) 0 H11 r)). + elim (Rlt_irrefl 0 (Rlt_trans 0 (Rmin (delta / 2) ((b - c) / 2)) 0 H11 Hlt)). unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos delta) | apply Rinv_0_lt_compat; prove_sup0 ]. - intro; apply Rle_lt_trans with (delta / 2). + apply Rle_lt_trans with (delta / 2). apply Rmin_l. unfold Rdiv; apply Rmult_lt_reg_l with 2. prove_sup0. @@ -1311,13 +1310,12 @@ Proof. case (Rcase_abs ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / - Rmax (- (delta / 2)) ((a + - c) / 2) + - l)). - intro; - elim + Rmax (- (delta / 2)) ((a + - c) / 2) + - l)) as [Hlt|Hge]. + elim (Rlt_irrefl 0 (Rlt_trans 0 ((f (c + Rmax (- (delta / 2)) ((a + - c) / 2)) + - f c) / - Rmax (- (delta / 2)) ((a + - c) / 2) + - l) 0 H19 r)). + Rmax (- (delta / 2)) ((a + - c) / 2) + - l) 0 H19 Hlt)). intros; generalize (Rplus_lt_compat_r l @@ -1380,8 +1378,8 @@ Proof. apply Rplus_lt_compat_l; assumption. field; discrR. assumption. - unfold Rabs; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))). - intro; generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro; + unfold Rabs; case (Rcase_abs (Rmax (- (delta / 2)) ((a - c) / 2))) as [Hlt|Hge]. + generalize (RmaxLess1 (- (delta / 2)) ((a - c) / 2)); intro; generalize (Ropp_le_ge_contravar (- (delta / 2)) (Rmax (- (delta / 2)) ((a - c) / 2)) H12); rewrite Ropp_involutive; intro; @@ -1402,7 +1400,7 @@ Proof. generalize (Rmax_stable_in_negreal (mknegreal (- (delta / 2)) H13) (mknegreal ((a - c) / 2) H12)); simpl; - intro; generalize (Rge_le (Rmax (- (delta / 2)) ((a - c) / 2)) 0 r); + intro; generalize (Rge_le (Rmax (- (delta / 2)) ((a - c) / 2)) 0 Hge); intro; elim (Rlt_irrefl 0 @@ -1494,11 +1492,10 @@ Proof. cut (0 <= (f (x + delta / 2) - f x) / (delta / 2)). intro; cut (0 <= (f (x + delta / 2) - f x) / (delta / 2) - l). intro; unfold Rabs; - case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)). - intro; - elim + case (Rcase_abs ((f (x + delta / 2) - f x) / (delta / 2) - l)) as [Hlt|Hge]. + elim (Rlt_irrefl 0 - (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 H12 r)). + (Rle_lt_trans 0 ((f (x + delta / 2) - f x) / (delta / 2) - l) 0 H12 Hlt)). intros; generalize (Rplus_lt_compat_r l ((f (x + delta / 2) - f x) / (delta / 2) - l) diff --git a/theories/Reals/Ranalysis2.v b/theories/Reals/Ranalysis2.v index c66c7b412..052e80006 100644 --- a/theories/Reals/Ranalysis2.v +++ b/theories/Reals/Ranalysis2.v @@ -433,10 +433,10 @@ Proof. unfold IZR; unfold INR, Pos.to_nat; simpl; intro; elim (Rlt_irrefl 1 (Rlt_trans _ _ _ H13 H12)). apply IZR_lt; omega. - unfold Rabs; case (Rcase_abs (/ 2)); intro. + unfold Rabs; case (Rcase_abs (/ 2)) as [Hlt|Hge]. assert (Hyp : 0 < 2). prove_sup0. - assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp r); rewrite Rmult_0_r in H11; + assert (H11 := Rmult_lt_compat_l 2 _ _ Hyp Hlt); rewrite Rmult_0_r in H11; rewrite <- Rinv_r_sym in H11; [ idtac | discrR ]. elim (Rlt_irrefl 0 (Rlt_trans _ _ _ Rlt_0_1 H11)). reflexivity. diff --git a/theories/Reals/Ranalysis4.v b/theories/Reals/Ranalysis4.v index 45c79af48..663f62f7a 100644 --- a/theories/Reals/Ranalysis4.v +++ b/theories/Reals/Ranalysis4.v @@ -117,14 +117,14 @@ Proof. rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. apply H1. apply Rle_ge. - case (Rcase_abs h); intro. - rewrite (Rabs_left h r) in H2. + destruct (Rcase_abs h) as [Hlt|Hgt]. + rewrite (Rabs_left h Hlt) in H2. left; rewrite Rplus_comm; apply Rplus_lt_reg_l with (- h); rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H2. apply Rplus_le_le_0_compat. left; apply H. - apply Rge_le; apply r. + apply Rge_le; apply Hgt. left; apply H. Qed. @@ -145,12 +145,12 @@ Proof. rewrite <- Rinv_r_sym. rewrite Ropp_involutive; rewrite Rplus_opp_l; rewrite Rabs_R0; apply H0. apply H2. - case (Rcase_abs h); intro. + destruct (Rcase_abs h) as [Hlt|Hgt]. apply Ropp_lt_cancel. rewrite Ropp_0; rewrite Ropp_plus_distr; apply Rplus_lt_0_compat. apply H1. - apply Ropp_0_gt_lt_contravar; apply r. - rewrite (Rabs_right h r) in H3. + apply Ropp_0_gt_lt_contravar; apply Hlt. + rewrite (Rabs_right h Hgt) in H3. apply Rplus_lt_reg_l with (- x); rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; rewrite Rplus_0_l; apply H3. apply H. @@ -161,13 +161,12 @@ Qed. Lemma Rderivable_pt_abs : forall x:R, x <> 0 -> derivable_pt Rabs x. Proof. intros. - case (total_order_T x 0); intro. - elim s; intro. + destruct (total_order_T x 0) as [[Hlt|Heq]|Hgt]. unfold derivable_pt; exists (-1). - apply (Rabs_derive_2 x a). - elim H; exact b. + apply (Rabs_derive_2 x Hlt). + elim H; exact Heq. unfold derivable_pt; exists 1. - apply (Rabs_derive_1 x r). + apply (Rabs_derive_1 x Hgt). Qed. (** Rabsolu is continuous for all x *) diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v index 3a5f932dd..6f8dcdc71 100644 --- a/theories/Reals/Ranalysis5.v +++ b/theories/Reals/Ranalysis5.v @@ -338,14 +338,14 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) left; assumption. intro. unfold cond_positivity in |- *. - case (Rle_dec 0 z); intro. + destruct (Rle_dec 0 z) as [|Hnotle]. split. intro; assumption. intro; reflexivity. split. intro feqt;discriminate feqt. intro. - elim n0; assumption. + elim Hnotle; assumption. unfold Vn in |- *. cut (forall z:R, cond_positivity z = false <-> z < 0). intros. @@ -359,10 +359,10 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) assumption. intro. unfold cond_positivity in |- *. - case (Rle_dec 0 z); intro. + destruct (Rle_dec 0 z) as [Hle|]. split. intro feqt; discriminate feqt. - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H7)). split. intro; auto with real. intro; reflexivity. @@ -371,10 +371,9 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) assert (Temp : x <= x0 <= y). apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption. assert (H7 := continuity_seq f Wn x0 (H x0 Temp) H5). - case (total_order_T 0 (f x0)); intro. - elim s; intro. + destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. left; assumption. - rewrite <- b; right; reflexivity. + right; reflexivity. unfold Un_cv in H7; unfold R_dist in H7. cut (0 < - f x0). intro. @@ -397,11 +396,10 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) assert (Temp : x <= x0 <= y). apply IVT_interv_prelim1 with (D:=(fun z : R => cond_positivity (f z))) ; assumption. assert (H7 := continuity_seq f Vn x0 (H x0 Temp) H5). - case (total_order_T 0 (f x0)); intro. - elim s; intro. + destruct (total_order_T 0 (f x0)) as [[Hlt|Heq]|]. unfold Un_cv in H7; unfold R_dist in H7. - elim (H7 (f x0) a); intros. - cut (x2 >= x2)%nat; [ intro | unfold ge in |- *; apply le_n ]. + elim (H7 (f x0) Hlt); intros. + cut (x2 >= x2)%nat; [ intro | unfold ge; apply le_n ]. assert (H10 := H8 x2 H9). rewrite Rabs_left in H10. pattern (f x0) at 2 in H10; rewrite <- Rplus_0_r in H10. @@ -419,7 +417,7 @@ intros. (* f x y f_cont_interv x_lt_y fx_neg fy_pos.*) [ unfold Rminus in |- *; apply Rplus_lt_le_0_compat | ring ]. assumption. apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6. - right; rewrite <- b; reflexivity. + right; rewrite <- Heq; reflexivity. left; assumption. unfold Vn in |- *; assumption. Qed. diff --git a/theories/Reals/Ratan.v b/theories/Reals/Ratan.v index dcf2f9709..6146b979f 100644 --- a/theories/Reals/Ratan.v +++ b/theories/Reals/Ratan.v @@ -450,9 +450,9 @@ fourier. Qed. Definition frame_tan y : {x | 0 < x < PI/2 /\ Rabs y < tan x}. -destruct (total_order_T (Rabs y) 1). - assert (yle1 : Rabs y <= 1) by (destruct s; fourier). - clear s; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. +destruct (total_order_T (Rabs y) 1) as [Hs|Hgt]. + assert (yle1 : Rabs y <= 1) by (destruct Hs; fourier). + clear Hs; exists 1; split;[split; [exact Rlt_0_1 | exact PI2_1] | ]. apply Rle_lt_trans with (1 := yle1); exact tan_1_gt_1. assert (0 < / (Rabs y + 1)). apply Rinv_0_lt_compat; fourier. @@ -530,7 +530,7 @@ split. assumption. replace (/(Rabs y + 1)) with (2 * u). fourier. - unfold u; field; apply Rgt_not_eq; clear -r; fourier. + unfold u; field; apply Rgt_not_eq; clear -Hgt; fourier. solve[discrR]. apply Rgt_not_eq; assumption. unfold tan. diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index 560f389b8..daf895fd2 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -45,12 +45,12 @@ Qed. (*********) Lemma Rmin_Rgt_l : forall r1 r2 r, Rmin r1 r2 > r -> r1 > r /\ r2 > r. Proof. - intros r1 r2 r; unfold Rmin; case (Rle_dec r1 r2); intros. + intros r1 r2 r; unfold Rmin; case (Rle_dec r1 r2) as [Hle|Hnle]; intros. split. assumption. - unfold Rgt; unfold Rgt in H; exact (Rlt_le_trans r r1 r2 H r0). + unfold Rgt; exact (Rlt_le_trans r r1 r2 H Hle). split. - generalize (Rnot_le_lt r1 r2 n); intro; exact (Rgt_trans r1 r2 r H0 H). + generalize (Rnot_le_lt r1 r2 Hnle); intro; exact (Rgt_trans r1 r2 r H0 H). assumption. Qed. @@ -168,10 +168,10 @@ Lemma Rmax_Rle : forall r1 r2 r, r <= Rmax r1 r2 <-> r <= r1 \/ r <= r2. Proof. intros; split. unfold Rmax; case (Rle_dec r1 r2); intros; auto. - intro; unfold Rmax; case (Rle_dec r1 r2); elim H; clear H; intros; + intro; unfold Rmax; case (Rle_dec r1 r2) as [|Hnle]; 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; + generalize (Rnot_le_lt r1 r2 Hnle); clear Hnle; intro; unfold Rgt in H0; apply (Rlt_le r r1 (Rle_lt_trans r r2 r1 H H0)). Qed. @@ -320,9 +320,9 @@ Qed. (*********) Lemma Rabs_right : forall r, r >= 0 -> Rabs r = r. Proof. - intros; unfold Rabs; case (Rcase_abs r); intro. + intros; unfold Rabs; case (Rcase_abs r) as [Hlt|Hge]. absurd (r >= 0). - exact (Rlt_not_ge r 0 r0). + exact (Rlt_not_ge r 0 Hlt). assumption. trivial. Qed. @@ -337,9 +337,9 @@ Qed. (*********) Lemma Rabs_pos : forall x:R, 0 <= Rabs x. Proof. - 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; left; assumption. + intros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]. + generalize (Ropp_lt_gt_contravar x 0 Hlt); intro; unfold Rgt in H; + rewrite Ropp_0 in H; left; assumption. apply Rge_le; assumption. Qed. @@ -353,8 +353,8 @@ Definition RRle_abs := Rle_abs. (*********) Lemma Rabs_pos_eq : forall x:R, 0 <= x -> Rabs x = x. Proof. - intros; unfold Rabs; case (Rcase_abs x); intro; - [ generalize (Rgt_not_le 0 x r); intro; exfalso; auto | trivial ]. + intros; unfold Rabs; case (Rcase_abs x) as [Hlt|Hge]; + [ generalize (Rgt_not_le 0 x Hlt); intro; exfalso; auto | trivial ]. Qed. (*********) @@ -366,100 +366,70 @@ Qed. (*********) 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; - 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); - trivial. + intros; destruct (Rabs_pos x) as [|Heq]; auto. + apply Rabs_no_R0 in H; symmetry in Heq; contradiction. Qed. (*********) Lemma Rabs_minus_sym : forall x y:R, Rabs (x - y) = Rabs (y - x). Proof. - 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; - auto. + intros; unfold Rabs; case (Rcase_abs (x - y)) as [Hlt|Hge]; + case (Rcase_abs (y - x)) as [Hlt'|Hge']. + apply Rminus_lt, Rlt_asym in Hlt; apply Rminus_lt in Hlt'; contradiction. rewrite (Ropp_minus_distr x y); trivial. rewrite (Ropp_minus_distr y x); trivial. - unfold Rge in r, r0; elim r; elim r0; intros; clear r r0. - generalize (Ropp_lt_gt_0_contravar (x - y) H); rewrite (Ropp_minus_distr x y); - intro; unfold Rgt in H0; generalize (Rlt_asym 0 (y - x) H0); - intro; exfalso; auto. - rewrite (Rminus_diag_uniq x y H); trivial. - rewrite (Rminus_diag_uniq y x H0); trivial. - rewrite (Rminus_diag_uniq y x H0); trivial. + destruct Hge; destruct Hge'. + apply Ropp_lt_gt_0_contravar in H; rewrite (Ropp_minus_distr x y) in H; + apply Rlt_asym in H0; contradiction. + apply Rminus_diag_uniq in H0 as ->; trivial. + apply Rminus_diag_uniq in H as ->; trivial. + apply Rminus_diag_uniq in H0 as ->; trivial. Qed. (*********) Lemma Rabs_mult : forall x y:R, Rabs (x * y) = Rabs x * Rabs y. Proof. - 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); - intro; unfold Rgt in H; exfalso; rewrite (Rmult_comm y x) in H; - auto. + intros; unfold Rabs; case (Rcase_abs (x * y)) as [Hlt|Hge]; + case (Rcase_abs x) as [Hltx|Hgex]; + case (Rcase_abs y) as [Hlty|Hgey]; auto. + apply Rmult_lt_gt_compat_neg_l with (r:=x), Rlt_asym in Hlty; trivial. + rewrite Rmult_0_r in Hlty; contradiction. rewrite (Ropp_mult_distr_l_reverse x y); trivial. rewrite (Rmult_comm x (- y)); rewrite (Ropp_mult_distr_l_reverse y x); rewrite (Rmult_comm x y); trivial. - unfold Rge in r, r0; elim r; elim r0; clear r r0; intros; unfold Rgt in H, H0. - generalize (Rmult_lt_compat_l x 0 y H H0); intro; rewrite (Rmult_0_r x) in H1; - generalize (Rlt_asym (x * y) 0 r1); intro; exfalso; - auto. - rewrite H in r1; rewrite (Rmult_0_l y) in r1; generalize (Rlt_irrefl 0); - intro; exfalso; auto. - rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0); - intro; exfalso; auto. - rewrite H0 in r1; rewrite (Rmult_0_r x) in r1; generalize (Rlt_irrefl 0); - intro; exfalso; auto. + destruct Hgex as [| ->], Hgey as [| ->]. + apply Rmult_lt_compat_l with (r:=x), Rlt_asym in H0; trivial. + rewrite Rmult_0_r in H0; contradiction. + rewrite Rmult_0_r in Hlt; contradiction (Rlt_irrefl 0). + rewrite Rmult_0_l in Hlt; contradiction (Rlt_irrefl 0). + rewrite Rmult_0_l in Hlt; contradiction (Rlt_irrefl 0). rewrite (Rmult_opp_opp x y); trivial. - unfold Rge in r, r1; elim r; elim r1; clear r r1; intros; unfold Rgt in H0, H. - generalize (Rmult_lt_compat_l y x 0 H0 r0); intro; - rewrite (Rmult_0_r y) in H1; rewrite (Rmult_comm y x) in H1; - generalize (Rlt_asym (x * y) 0 H1); intro; exfalso; - auto. - generalize (Rlt_dichotomy_converse x 0 (or_introl (x > 0) r0)); - generalize (Rlt_dichotomy_converse y 0 (or_intror (y < 0) H0)); - intros; generalize (Rmult_integral x y H); intro; - elim H3; intro; exfalso; auto. - rewrite H0 in H; rewrite (Rmult_0_r x) in H; unfold Rgt in H; - generalize (Rlt_irrefl 0); intro; exfalso; - auto. - rewrite H0; rewrite (Rmult_0_r x); rewrite (Rmult_0_r (- x)); trivial. - unfold Rge in r0, r1; elim r0; elim r1; clear r0 r1; intros; - unfold Rgt in H0, H. - generalize (Rmult_lt_compat_l x y 0 H0 r); intro; rewrite (Rmult_0_r x) in H1; - generalize (Rlt_asym (x * y) 0 H1); intro; exfalso; - auto. - generalize (Rlt_dichotomy_converse y 0 (or_introl (y > 0) r)); - generalize (Rlt_dichotomy_converse 0 x (or_introl (0 > x) H0)); - intros; generalize (Rmult_integral x y H); intro; - elim H3; intro; exfalso; auto. - rewrite H0 in H; rewrite (Rmult_0_l y) in H; unfold Rgt in H; - generalize (Rlt_irrefl 0); intro; exfalso; - auto. - rewrite H0; rewrite (Rmult_0_l y); rewrite (Rmult_0_l (- y)); trivial. + destruct Hge. destruct Hgey. + apply Rmult_lt_compat_r with (r:=y), Rlt_asym in Hltx; trivial. + rewrite Rmult_0_l in Hltx; contradiction. + rewrite H0, Rmult_0_r in H; contradiction (Rlt_irrefl 0). + rewrite <- Ropp_mult_distr_l, H, Ropp_0; trivial. + destruct Hge. destruct Hgex. + apply Rmult_lt_compat_l with (r:=x), Rlt_asym in Hlty; trivial. + rewrite Rmult_0_r in Hlty; contradiction. + rewrite H0, 2!Rmult_0_l; trivial. + rewrite <- Ropp_mult_distr_r, H, Ropp_0; trivial. Qed. (*********) Lemma Rabs_Rinv : forall r, r <> 0 -> Rabs (/ r) = / Rabs r. Proof. - intro; unfold Rabs; case (Rcase_abs r); case (Rcase_abs (/ r)); auto; + intro; unfold Rabs; case (Rcase_abs r) as [Hlt|Hge]; + case (Rcase_abs (/ r)) as [Hlt'|Hge']; auto; intros. apply Ropp_inv_permute; auto. - generalize (Rinv_lt_0_compat r r1); intro; unfold Rge in r0; elim r0; intros. - unfold Rgt in H1; generalize (Rlt_asym 0 (/ r) H1); intro; exfalso; - auto. - generalize (Rlt_dichotomy_converse (/ r) 0 (or_introl (/ r > 0) H0)); intro; - exfalso; auto. - unfold Rge in r1; elim r1; clear r1; intro. - unfold Rgt in H0; generalize (Rlt_asym 0 (/ r) (Rinv_0_lt_compat r H0)); - intro; exfalso; auto. - exfalso; auto. + rewrite <- Ropp_inv_permute; trivial. + destruct Hge' as [| ->]. + apply Rinv_lt_0_compat, Rlt_asym in Hlt; contradiction. + rewrite Ropp_0; trivial. + destruct Hge as [| ->]. + apply Rinv_0_lt_compat, Rlt_asym in H0; contradiction. + contradiction (refl_equal 0). Qed. Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x. @@ -483,13 +453,14 @@ Qed. (*********) Lemma Rabs_triang : forall a b:R, Rabs (a + b) <= Rabs a + Rabs b. Proof. - intros a b; unfold Rabs; case (Rcase_abs (a + b)); case (Rcase_abs a); - case (Rcase_abs b); intros. + intros a b; unfold Rabs; case (Rcase_abs (a + b)) as [Hlt|Hge]; + case (Rcase_abs a) as [Hlta|Hgea]; + case (Rcase_abs b) as [Hltb|Hgeb]. 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; unfold Rge in r; elim r; intro. + unfold Rle; elim Hgeb; 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). @@ -497,24 +468,24 @@ 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; unfold Rge in r0; elim r0; intro. + unfold Rle; elim Hgea; 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). right; rewrite H; apply Ropp_0. (**) - exfalso; generalize (Rplus_ge_compat_l a b 0 r); intro; + exfalso; generalize (Rplus_ge_compat_l a b 0 Hgeb); intro; elim (Rplus_ne a); intros v w; rewrite v in H; clear v w; - generalize (Rge_trans (a + b) a 0 H r0); intro; clear H; + generalize (Rge_trans (a + b) a 0 H Hgea); intro; clear H; unfold Rge in H0; elim H0; intro; clear H0. - unfold Rgt in H; generalize (Rlt_asym (a + b) 0 r1); intro; auto. + unfold Rgt in H; generalize (Rlt_asym (a + b) 0 Hlt); intro; auto. absurd (a + b = 0); auto. apply (Rlt_dichotomy_converse (a + b) 0); left; assumption. (**) - exfalso; generalize (Rplus_lt_compat_l a b 0 r); intro; + exfalso; generalize (Rplus_lt_compat_l a b 0 Hltb); intro; elim (Rplus_ne a); intros v w; rewrite v in H; clear v w; - generalize (Rlt_trans (a + b) a 0 H r0); intro; clear H; - unfold Rge in r1; elim r1; clear r1; intro. + generalize (Rlt_trans (a + b) a 0 H Hlta); intro; clear H; + destruct Hge. unfold Rgt in H; generalize (Rlt_trans (a + b) 0 (a + b) H0 H); intro; apply (Rlt_irrefl (a + b)); assumption. rewrite H in H0; apply (Rlt_irrefl 0); assumption. @@ -522,16 +493,16 @@ 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; rewrite (Ropp_involutive a); - generalize (Rplus_lt_compat_l a a 0 r0); clear r r1; + generalize (Rplus_lt_compat_l a a 0 Hlta); clear Hge Hgeb; intro; elim (Rplus_ne a); intros v w; rewrite v in H; - clear v w; generalize (Rlt_trans (a + a) a 0 H r0); + clear v w; generalize (Rlt_trans (a + a) a 0 H Hlta); intro; apply (Rlt_le (a + a) 0 H0). (**) apply (Rplus_le_compat_l a b (- b)); apply (Rminus_le b (- b)); unfold Rminus; rewrite (Ropp_involutive b); - generalize (Rplus_lt_compat_l b b 0 r); clear r0 r1; + generalize (Rplus_lt_compat_l b b 0 Hltb); clear Hge Hgea; intro; elim (Rplus_ne b); intros v w; rewrite v in H; - clear v w; generalize (Rlt_trans (b + b) b 0 H r); + clear v w; generalize (Rlt_trans (b + b) b 0 H Hltb); intro; apply (Rlt_le (b + b) 0 H0). (**) unfold Rle; right; reflexivity. @@ -585,15 +556,15 @@ Qed. (*********) Lemma Rabs_def2 : forall x a:R, Rabs x < a -> x < a /\ - a < x. Proof. - unfold Rabs; intro x; case (Rcase_abs x); intros. - generalize (Ropp_gt_lt_0_contravar x r); unfold Rgt; intro; + unfold Rabs; intro x; case (Rcase_abs x) as [Hlt|Hge]; intros. + generalize (Ropp_gt_lt_0_contravar x Hlt); unfold Rgt; intro; generalize (Rlt_trans 0 (- x) a H0 H); intro; split. - apply (Rlt_trans x 0 a r H1). + apply (Rlt_trans x 0 a Hlt H1). generalize (Ropp_lt_gt_contravar (- x) a H); rewrite (Ropp_involutive x); unfold Rgt; trivial. - fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H r); intro; + fold (a > x) in H; generalize (Rgt_ge_trans a x 0 H Hge); intro; generalize (Ropp_lt_gt_0_contravar a H0); intro; fold (0 > - a); - generalize (Rge_gt_trans x 0 (- a) r H1); unfold Rgt; + generalize (Rge_gt_trans x 0 (- a) Hge H1); unfold Rgt; intro; split; assumption. Qed. diff --git a/theories/Reals/Rderiv.v b/theories/Reals/Rderiv.v index e714f5f8c..69ef143e7 100644 --- a/theories/Reals/Rderiv.v +++ b/theories/Reals/Rderiv.v @@ -162,9 +162,9 @@ Proof. (Rplus_lt_compat (Rabs (d x0 * (x1 - x0))) (eps * / 2) (Rabs (x1 - x0) * eps) (eps * / 2) H5 H3); intro; rewrite eps2 in H10; assumption. - unfold Rabs; case (Rcase_abs 2); auto. - intro; cut (0 < 2). - intro ; elim (Rlt_asym 0 2 H7 r). + unfold Rabs; destruct (Rcase_abs 2) as [Hlt|Hge]; auto. + cut (0 < 2). + intro H7; elim (Rlt_asym 0 2 H7 Hlt). fourier. apply Rabs_no_R0. discrR. @@ -193,11 +193,11 @@ Proof. unfold limit_in; intros; simpl; split with eps; split; auto. intros; elim H0; clear H0; intros; unfold D_x in H0; elim H0; intros; - rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (not_eq_sym H3))); - unfold R_dist; rewrite (Rminus_diag_eq 1 1 (eq_refl 1)); - unfold Rabs; case (Rcase_abs 0); intro. + rewrite (Rinv_r (x - x0) (Rminus_eq_contra x x0 (sym_not_eq H3))); + unfold R_dist; rewrite (Rminus_diag_eq 1 1 (refl_equal 1)); + unfold Rabs; case (Rcase_abs 0) as [Hlt|Hge]. absurd (0 < 0); auto. - red; intro; apply (Rlt_irrefl 0 r). + red in |- *; intro; apply (Rlt_irrefl 0 Hlt). unfold Rgt in H; assumption. Qed. diff --git a/theories/Reals/Rfunctions.v b/theories/Reals/Rfunctions.v index 5eb34324e..604160834 100644 --- a/theories/Reals/Rfunctions.v +++ b/theories/Reals/Rfunctions.v @@ -489,16 +489,16 @@ Lemma pow_Rabs : forall (x:R) (n:nat), x ^ n <= Rabs x ^ n. Proof. intros; induction n as [| n Hrecn]. right; reflexivity. - simpl; case (Rcase_abs x); intro. + simpl; destruct (Rcase_abs x) as [Hlt|Hle]. apply Rle_trans with (Rabs (x * x ^ n)). apply RRle_abs. rewrite Rabs_mult. apply Rmult_le_compat_l. apply Rabs_pos. - right; symmetry ; apply RPow_abs. - pattern (Rabs x) at 1; rewrite (Rabs_right x r); + right; symmetry; apply RPow_abs. + pattern (Rabs x) at 1; rewrite (Rabs_right x Hle); apply Rmult_le_compat_l. - apply Rge_le; exact r. + apply Rge_le; exact Hle. apply Hrecn. Qed. @@ -741,10 +741,11 @@ Qed. Lemma R_dist_sym : forall x y:R, R_dist x y = R_dist y x. Proof. unfold R_dist; intros; split_Rabs; try ring. - generalize (Ropp_gt_lt_0_contravar (y - x) r); intro; - rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 r0); +Show. + generalize (Ropp_gt_lt_0_contravar (y - x) Hlt0); intro; + rewrite (Ropp_minus_distr y x) in H; generalize (Rlt_asym (x - y) 0 Hlt); intro; unfold Rgt in H; exfalso; auto. - generalize (minus_Rge y x r); intro; generalize (minus_Rge x y r0); intro; + generalize (minus_Rge y x Hge0); intro; generalize (minus_Rge x y Hge); intro; generalize (Rge_antisym x y H0 H); intro; rewrite H1; ring. Qed. diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index cdd3b96c0..1445e7dbe 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -108,12 +108,10 @@ Proof. replace (vn n x + -1 * vn m x) with (vn n x - f x + (f x - vn m x)); [ apply Rabs_triang | ring ]. assert (H12 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. assert (H13 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. - rewrite <- H12 in H11; pattern b at 2 in H11; rewrite <- H13 in H11; + unfold Rmax; decide (Rle_dec a b) with H0; reflexivity. + rewrite <- H12 in H11; rewrite <- H13 in H11 at 2; rewrite Rmult_1_l; apply Rplus_le_compat. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9. elim H11; intros; split; left; assumption. @@ -140,7 +138,7 @@ Lemma RiemannInt_P3 : Rabs (RiemannInt_SF (wn n)) < un n) -> { l:R | Un_cv (fun N:nat => RiemannInt_SF (vn N)) l }. Proof. - intros; case (Rle_dec a b); intro. + intros; destruct (Rle_dec a b) as [Hle|Hnle]. apply RiemannInt_P2 with f un wn; assumption. assert (H1 : b <= a); auto with real. set (vn' := fun n:nat => mkStepFun (StepFun_P6 (pre (vn n)))); @@ -151,26 +149,24 @@ Proof. (forall t:R, Rmin b a <= t <= Rmax b a -> Rabs (f t - vn' n t) <= wn' n t) /\ Rabs (RiemannInt_SF (wn' n)) < un n). - intro; elim (H0 n0); intros; split. - intros; apply (H2 t); elim H4; clear H4; intros; split; + intro; elim (H0 n); intros; split. + intros t (H4,H5); apply (H2 t); split; [ apply Rle_trans with (Rmin b a); try assumption; right; unfold Rmin | apply Rle_trans with (Rmax b a); try assumption; right; unfold Rmax ]; - (case (Rle_dec a b); case (Rle_dec b a); intros; - try reflexivity || apply Rle_antisym; - [ assumption | assumption | auto with real | auto with real ]). - generalize H3; unfold RiemannInt_SF; case (Rle_dec a b); - case (Rle_dec b a); unfold wn'; intros; + decide (Rle_dec a b) with Hnle; decide (Rle_dec b a) with H1; reflexivity. + generalize H3; unfold RiemannInt_SF; destruct (Rle_dec a b) as [Hleab|Hnleab]; + destruct (Rle_dec b a) as [Hle'|Hnle']; unfold wn'; intros; (replace - (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (wn n0))))) - (subdivision (mkStepFun (StepFun_P6 (pre (wn n0)))))) with - (Int_SF (subdivision_val (wn n0)) (subdivision (wn n0))); + (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (wn n))))) + (subdivision (mkStepFun (StepFun_P6 (pre (wn n)))))) with + (Int_SF (subdivision_val (wn n)) (subdivision (wn n))); [ idtac - | apply StepFun_P17 with (fe (wn n0)) a b; + | apply StepFun_P17 with (fe (wn n)) a b; [ apply StepFun_P1 | apply StepFun_P2; - apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (wn n0))))) ] ]). + apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (wn n))))) ] ]). apply H4. rewrite Rabs_Ropp; apply H4. rewrite Rabs_Ropp in H4; apply H4. @@ -179,21 +175,22 @@ Proof. exists (- x); unfold Un_cv; unfold Un_cv in p; intros; elim (p _ H4); intros; exists x0; intros; generalize (H5 _ H6); unfold R_dist, RiemannInt_SF; - case (Rle_dec b a); case (Rle_dec a b); intros. - elim n; assumption. + destruct (Rle_dec b a) as [Hle'|Hnle']; destruct (Rle_dec a b) as [Hle''|Hnle'']; + intros. + elim Hnle; assumption. unfold vn' in H7; - replace (Int_SF (subdivision_val (vn n0)) (subdivision (vn n0))) with - (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (vn n0))))) - (subdivision (mkStepFun (StepFun_P6 (pre (vn n0)))))); + replace (Int_SF (subdivision_val (vn n)) (subdivision (vn n))) with + (Int_SF (subdivision_val (mkStepFun (StepFun_P6 (pre (vn n))))) + (subdivision (mkStepFun (StepFun_P6 (pre (vn n)))))); [ unfold Rminus; rewrite Ropp_involutive; rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive; apply H7 - | symmetry ; apply StepFun_P17 with (fe (vn n0)) a b; + | symmetry ; apply StepFun_P17 with (fe (vn n)) a b; [ apply StepFun_P1 | apply StepFun_P2; - apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (vn n0))))) ] ]. - elim n1; assumption. - elim n2; assumption. + apply (StepFun_P1 (mkStepFun (StepFun_P6 (pre (vn n))))) ] ]. + elim Hnle'; assumption. + elim Hnle'; assumption. Qed. Lemma RiemannInt_exists : @@ -242,7 +239,7 @@ Proof. (RiemannInt_SF (phi_sequence vn pr2 n) + -1 * RiemannInt_SF (phi_sequence un pr1 n)); [ idtac | ring ]; rewrite <- StepFun_P30. - case (Rle_dec a b); intro. + destruct (Rle_dec a b) as [Hle|Hnle]. apply Rle_lt_trans with (RiemannInt_SF (mkStepFun @@ -261,13 +258,11 @@ Proof. (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x)); [ apply Rabs_triang | ring ]. assert (H10 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hle; reflexivity. assert (H11 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hle; reflexivity. rewrite (Rplus_comm (psi_un x)); apply Rplus_le_compat. - rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim H5; intros; apply H8. + rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; destruct H5 as (H8,H9); apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. elim H6; intros; apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. @@ -317,11 +312,9 @@ Proof. (phi_sequence vn pr2 n x - f x + (f x - phi_sequence un pr1 n x)); [ apply Rabs_triang | ring ]. assert (H10 : Rmin a b = b). - unfold Rmin; case (Rle_dec a b); intro; - [ elim n0; assumption | reflexivity ]. + unfold Rmin; decide (Rle_dec a b) with Hnle; reflexivity. assert (H11 : Rmax a b = a). - unfold Rmax; case (Rle_dec a b); intro; - [ elim n0; assumption | reflexivity ]. + unfold Rmax; decide (Rle_dec a b) with Hnle; reflexivity. apply Rplus_le_compat. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim H5; intros; apply H8. rewrite H10; rewrite H11; elim H7; intros; split; left; assumption. @@ -410,10 +403,10 @@ Lemma RiemannInt_P5 : RiemannInt pr1 = RiemannInt pr2. Proof. intros; unfold RiemannInt; - case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x,HUn); + case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x0,HUn0); eapply UL_sequence; - [ apply u0 + [ apply HUn | apply RiemannInt_P4 with pr2 RinvN; apply RinvN_cv || assumption ]. Qed. @@ -433,11 +426,10 @@ Proof. intro; assert (H2 := Nzorn H0 H1); elim H2; intros; exists x; elim p; intros; split. apply H3. - case (total_order_T (a + INR (S x) * del) b); intro. - elim s; intro. - assert (H5 := H4 (S x) a0); elim (le_Sn_n _ H5). + destruct (total_order_T (a + INR (S x) * del) b) as [[Hlt|Heq]|Hgt]. + assert (H5 := H4 (S x) Hlt); elim (le_Sn_n _ H5). right; symmetry ; assumption. - left; apply r. + left; apply Hgt. assert (H1 : 0 <= (b - a) / del). unfold Rdiv; apply Rmult_le_pos; [ apply Rge_le; apply Rge_minus; apply Rle_ge; left; apply H @@ -542,17 +534,16 @@ Lemma Heine_cor2 : a <= x <= b -> a <= y <= b -> Rabs (x - y) < delta -> Rabs (f x - f y) < eps }. Proof. - intro f; intros; case (total_order_T a b); intro. - elim s; intro. - assert (H0 := Heine_cor1 a0 H eps); elim H0; intros; exists x; + intro f; intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. + assert (H0 := Heine_cor1 Hlt H eps); elim H0; intros; exists x; elim p; intros; apply H2; assumption. exists (mkposreal _ Rlt_0_1); intros; assert (H3 : x = y); - [ elim H0; elim H1; intros; rewrite b0 in H3; rewrite b0 in H5; + [ elim H0; elim H1; intros; rewrite Heq in H3, H5; apply Rle_antisym; apply Rle_trans with b; assumption | rewrite H3; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply (cond_pos eps) ]. exists (mkposreal _ Rlt_0_1); intros; elim H0; intros; - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H3 H4) Hgt)). Qed. Lemma SubEqui_P1 : @@ -565,7 +556,7 @@ Lemma SubEqui_P2 : forall (a b:R) (del:posreal) (h:a < b), pos_Rl (SubEqui del h) (pred (Rlength (SubEqui del h))) = b. Proof. - intros; unfold SubEqui; case (maxN del h); intros; clear a0; + intros; unfold SubEqui; destruct (maxN del h)as (x,_). cut (forall (x:nat) (a:R) (del:posreal), pos_Rl (SubEquiN (S x) a b del) @@ -621,8 +612,8 @@ Proof. simpl in H; inversion H. rewrite (SubEqui_P6 del h (i:=(max_N del h))). replace (S (max_N del h)) with (pred (Rlength (SubEqui del h))). - rewrite SubEqui_P2; unfold max_N; case (maxN del h); intros; left; - elim a0; intros; assumption. + rewrite SubEqui_P2; unfold max_N; case (maxN del h) as (?&?&?); left; + assumption. rewrite SubEqui_P5; reflexivity. apply lt_n_Sn. repeat rewrite SubEqui_P6. @@ -676,11 +667,11 @@ Proof. | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rlt_Rminus; assumption ] ]. assert (H2 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; left; assumption ]. + apply Rlt_le in H. + unfold Rmin; decide (Rle_dec a b) with H; reflexivity. assert (H3 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; left; assumption ]. + apply Rlt_le in H. + unfold Rmax; decide (Rle_dec a b) with H; reflexivity. elim (Heine_cor2 H0 (mkposreal _ H1)); intros del H4; elim (SubEqui_P9 del f H); intros phi [H5 H6]; split with phi; split with (mkStepFun (StepFun_P4 a b (eps / (2 * (b - a))))); @@ -736,8 +727,8 @@ Proof. rewrite H13 in H12; rewrite SubEqui_P2 in H12; apply H12. rewrite SubEqui_P6. 2: apply lt_n_Sn. - unfold max_N; case (maxN del H); intros; elim a0; clear a0; - intros _ H13; replace (a + INR x * del + del) with (a + INR (S x) * del); + unfold max_N; destruct (maxN del H) as (?&?&H13); + replace (a + INR x * del + del) with (a + INR (S x) * del); [ assumption | rewrite S_INR; ring ]. apply Rplus_lt_reg_l with (pos_Rl (SubEqui del H) I); replace (pos_Rl (SubEqui del H) I + (t - pos_Rl (SubEqui del H) I)) with t; @@ -757,7 +748,7 @@ Proof. intros; assumption. assert (H4 : Nbound I). unfold Nbound; exists (S (max_N del H)); intros; unfold max_N; - case (maxN del H); intros; elim a0; clear a0; intros _ H5; + destruct (maxN del H) as (?&_&H5); apply INR_le; apply Rmult_le_reg_l with (pos del). apply (cond_pos del). apply Rplus_le_reg_l with a; do 2 rewrite (Rmult_comm del); @@ -765,12 +756,12 @@ Proof. apply Rle_trans with b; try assumption; elim H8; intros; assumption. elim (Nzorn H1 H4); intros N [H5 H6]; assert (H7 : (N < S (max_N del H))%nat). - unfold max_N; case (maxN del H); intros; apply INR_lt; + unfold max_N; case (maxN del H) as (?&?&?); apply INR_lt; apply Rmult_lt_reg_l with (pos del). apply (cond_pos del). apply Rplus_lt_reg_l with a; do 2 rewrite (Rmult_comm del); apply Rle_lt_trans with t0; unfold I in H5; try assumption; - elim a0; intros; apply Rlt_le_trans with b; try assumption; + apply Rlt_le_trans with b; try assumption; elim H8; intros. elim H11; intro. assumption. @@ -789,8 +780,8 @@ Proof. elim H0; assumption. rewrite SubEqui_P5; reflexivity. rewrite SubEqui_P6. - case (Rle_dec (a + INR (S N) * del) t0); intro. - assert (H11 := H6 (S N) r); elim (le_Sn_n _ H11). + destruct (Rle_dec (a + INR (S N) * del) t0) as [Hle|Hnle]. + assert (H11 := H6 (S N) Hle); elim (le_Sn_n _ H11). auto with real. apply le_lt_n_Sm; assumption. Qed. @@ -803,8 +794,8 @@ Proof. intros; simpl; unfold fct_cte; replace t with a. unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; right; reflexivity. - generalize H; unfold Rmin, Rmax; case (Rle_dec a a); intros; elim H0; - intros; apply Rle_antisym; assumption. + generalize H; unfold Rmin, Rmax; decide (Rle_dec a a) with (Rle_refl a). + intros (?,?); apply Rle_antisym; assumption. rewrite StepFun_P18; rewrite Rmult_0_l; rewrite Rabs_R0; apply (cond_pos eps). Qed. @@ -813,10 +804,9 @@ Lemma continuity_implies_RiemannInt : a <= b -> (forall x:R, a <= x <= b -> continuity_pt f x) -> Riemann_integrable f a b. Proof. - intros; case (total_order_T a b); intro; - [ elim s; intro; - [ apply RiemannInt_P6; assumption | rewrite b0; apply RiemannInt_P7 ] - | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)) ]. + intros; destruct (total_order_T a b) as [[Hlt| -> ]|Hgt]; + [ apply RiemannInt_P6; assumption | apply RiemannInt_P7 + | elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)) ]. Qed. Lemma RiemannInt_P8 : @@ -824,9 +814,9 @@ Lemma RiemannInt_P8 : (pr2:Riemann_integrable f b a), RiemannInt pr1 = - RiemannInt pr2. Proof. intro f; intros; eapply UL_sequence. - unfold RiemannInt; case (RiemannInt_exists pr1 RinvN RinvN_cv); - intros; apply u. - unfold RiemannInt; case (RiemannInt_exists pr2 RinvN RinvN_cv); + unfold RiemannInt; destruct (RiemannInt_exists pr1 RinvN RinvN_cv) as (?,HUn); + apply HUn. + unfold RiemannInt; destruct (RiemannInt_exists pr2 RinvN RinvN_cv) as (?,HUn); intros; cut (exists psi1 : nat -> StepFun a b, @@ -855,7 +845,7 @@ Proof. [ assumption | unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply Rabs_right; left; apply (cond_pos (RinvN n)) ]. - clear H1; unfold Un_cv in u; elim (u _ H3); clear u; intros N1 H1; + clear H1; destruct (HUn _ H3) as (N1,H1); exists (max N0 N1); intros; unfold R_dist; apply Rle_lt_trans with (Rabs @@ -879,7 +869,7 @@ Proof. -1 * RiemannInt_SF (mkStepFun (StepFun_P6 (pre (phi_sequence RinvN pr2 n))))); [ idtac | ring ]; rewrite <- StepFun_P30. - case (Rle_dec a b); intro. + destruct (Rle_dec a b) as [Hle|Hnle]. apply Rle_lt_trans with (RiemannInt_SF (mkStepFun @@ -901,11 +891,9 @@ Proof. (phi_sequence RinvN pr1 n x0 - f x0 + (f x0 - phi_sequence RinvN pr2 n x0)); [ apply Rabs_triang | ring ]. assert (H7 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hle; reflexivity. assert (H8 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hle; reflexivity. apply Rplus_le_compat. elim (H0 n); intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9; rewrite H7; rewrite H8. @@ -954,11 +942,9 @@ Proof. (phi_sequence RinvN pr1 n x0 - f x0 + (f x0 - phi_sequence RinvN pr2 n x0)); [ apply Rabs_triang | ring ]. assert (H7 : Rmin a b = b). - unfold Rmin; case (Rle_dec a b); intro; - [ elim n0; assumption | reflexivity ]. + unfold Rmin; decide (Rle_dec a b) with Hnle; reflexivity. assert (H8 : Rmax a b = a). - unfold Rmax; case (Rle_dec a b); intro; - [ elim n0; assumption | reflexivity ]. + unfold Rmax; decide (Rle_dec a b) with Hnle; reflexivity. apply Rplus_le_compat. elim (H0 n); intros; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply H9; rewrite H7; rewrite H8. @@ -1021,10 +1007,9 @@ Lemma RiemannInt_P10 : Riemann_integrable g a b -> Riemann_integrable (fun x:R => f x + l * g x) a b. Proof. - unfold Riemann_integrable; intros f g; intros; case (Req_EM_T l 0); - intro. + unfold Riemann_integrable; intros f g; intros; destruct (Req_EM_T l 0) as [Heq|Hneq]. elim (X eps); intros; split with x; elim p; intros; split with x0; elim p0; - intros; split; try assumption; rewrite e; intros; + intros; split; try assumption; rewrite Heq; intros; rewrite Rmult_0_l; rewrite Rplus_0_r; apply H; assumption. assert (H : 0 < eps / 2). unfold Rdiv; apply Rmult_lt_0_compat; @@ -1111,18 +1096,14 @@ Proof. rewrite (Rplus_comm (psi1 n x)); apply Rplus_le_compat. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; elim (H1 n); intros; apply H7. assert (H10 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (H11 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. elim (H0 n); intros; apply H7; assert (H10 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (H11 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. rewrite H10; rewrite H11; elim H6; intros; split; left; assumption. rewrite StepFun_P30; rewrite Rmult_1_l; rewrite double; apply Rplus_lt_compat. apply Rlt_trans with (pos (un n)). @@ -1254,10 +1235,10 @@ Lemma RiemannInt_P12 : Proof. intro f; intros; case (Req_dec l 0); intro. pattern l at 2; rewrite H0; rewrite Rmult_0_l; rewrite Rplus_0_r; - unfold RiemannInt; case (RiemannInt_exists pr3 RinvN RinvN_cv); - case (RiemannInt_exists pr1 RinvN RinvN_cv); intros; + unfold RiemannInt; destruct (RiemannInt_exists pr3 RinvN RinvN_cv) as (?,HUn_cv); + destruct (RiemannInt_exists pr1 RinvN RinvN_cv) as (?,HUn_cv0); intros. eapply UL_sequence; - [ apply u0 + [ apply HUn_cv | set (psi1 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr1 n)); set (psi2 := fun n:nat => proj1_sig (phi_sequence_prop RinvN pr3 n)); apply RiemannInt_P11 with f RinvN (phi_sequence RinvN pr1) psi1 psi2; @@ -1276,22 +1257,22 @@ Proof. [ apply H2; assumption | rewrite H0; ring ] ] | assumption ] ]. eapply UL_sequence. - unfold RiemannInt; case (RiemannInt_exists pr3 RinvN RinvN_cv); - intros; apply u. + unfold RiemannInt; destruct (RiemannInt_exists pr3 RinvN RinvN_cv) as (?,HUn_cv); + intros; apply HUn_cv. unfold Un_cv; intros; unfold RiemannInt; - case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); unfold Un_cv; + case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x0,HUn_cv0); + case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x,HUn_cv); unfold Un_cv; intros; assert (H2 : 0 < eps / 5). unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - elim (u0 _ H2); clear u0; intros N0 H3; assert (H4 := RinvN_cv); + elim (HUn_cv0 _ H2); clear HUn_cv0; intros N0 H3; assert (H4 := RinvN_cv); unfold Un_cv in H4; elim (H4 _ H2); clear H4 H2; intros N1 H4; assert (H5 : 0 < eps / (5 * Rabs l)). unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; apply Rmult_lt_0_compat; [ prove_sup0 | apply Rabs_pos_lt; assumption ] ]. - elim (u _ H5); clear u; intros N2 H6; assert (H7 := RinvN_cv); + elim (HUn_cv _ H5); clear HUn_cv; intros N2 H6; assert (H7 := RinvN_cv); unfold Un_cv in H7; elim (H7 _ H5); clear H7 H5; intros N3 H5; unfold R_dist in H3, H4, H5, H6; set (N := max (max N0 N1) (max N2 N3)). assert (H7 : forall n:nat, (n >= N1)%nat -> RinvN n < eps / 5). @@ -1379,11 +1360,9 @@ Proof. (RiemannInt_SF (phi_sequence RinvN pr1 n) + l * RiemannInt_SF (phi_sequence RinvN pr2 n))); [ idtac | ring ]; do 2 rewrite <- StepFun_P30; assert (H10 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H; reflexivity. assert (H11 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H; reflexivity. rewrite H10 in H7; rewrite H10 in H8; rewrite H10 in H9; rewrite H11 in H7; rewrite H11 in H8; rewrite H11 in H9; apply Rle_lt_trans with @@ -1493,7 +1472,7 @@ Lemma RiemannInt_P13 : (pr3:Riemann_integrable (fun x:R => f x + l * g x) a b), RiemannInt pr3 = RiemannInt pr1 + l * RiemannInt pr2. Proof. - intros; case (Rle_dec a b); intro; + intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply RiemannInt_P12; assumption | assert (H : b <= a); [ auto with real @@ -1524,9 +1503,9 @@ Lemma RiemannInt_P15 : forall (a b c:R) (pr:Riemann_integrable (fct_cte c) a b), RiemannInt pr = c * (b - a). Proof. - intros; unfold RiemannInt; case (RiemannInt_exists pr RinvN RinvN_cv); + intros; unfold RiemannInt; destruct (RiemannInt_exists pr RinvN RinvN_cv) as (?,HUn_cv); intros; eapply UL_sequence. - apply u. + apply HUn_cv. set (phi1 := fun N:nat => phi_sequence RinvN pr N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) (c * (b - a))); set (f := fct_cte c); @@ -1572,11 +1551,11 @@ Lemma Rle_cv_lim : forall (Un Vn:nat -> R) (l1 l2:R), (forall n:nat, Un n <= Vn n) -> Un_cv Un l1 -> Un_cv Vn l2 -> l1 <= l2. Proof. - intros; case (Rle_dec l1 l2); intro. + intros; destruct (Rle_dec l1 l2) as [Hle|Hnle]. assumption. assert (H2 : l2 < l1). auto with real. - clear n; assert (H3 : 0 < (l1 - l2) / 2). + assert (H3 : 0 < (l1 - l2) / 2). unfold Rdiv; apply Rmult_lt_0_compat; [ apply Rlt_Rminus; assumption | apply Rinv_0_lt_compat; prove_sup0 ]. elim (H1 _ H3); elim (H0 _ H3); clear H0 H1; unfold R_dist; intros; @@ -1613,9 +1592,9 @@ Lemma RiemannInt_P17 : a <= b -> Rabs (RiemannInt pr1) <= RiemannInt pr2. Proof. intro f; intros; unfold RiemannInt; - case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; - set (phi1 := phi_sequence RinvN pr1) in u0; + case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x0,HUn_cv0); + case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x,HUn_cv); + set (phi1 := phi_sequence RinvN pr1) in HUn_cv0; set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); apply Rle_cv_lim with (fun N:nat => Rabs (RiemannInt_SF (phi1 N))) @@ -1670,10 +1649,10 @@ Lemma RiemannInt_P18 : (forall x:R, a < x < b -> f x = g x) -> RiemannInt pr1 = RiemannInt pr2. Proof. intro f; intros; unfold RiemannInt; - case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x0,HUn_cv0); + case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x,HUn_cv); eapply UL_sequence. - apply u0. + apply HUn_cv0. set (phi1 := fun N:nat => phi_sequence RinvN pr1 N); change (Un_cv (fun N:nat => RiemannInt_SF (phi1 N)) x); assert @@ -1716,48 +1695,48 @@ Proof. apply RinvN_cv. intro; elim (H2 n); intros; split; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; - case (Req_EM_T t a); case (Req_EM_T t b); intros. - rewrite e0; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; + destruct (Req_EM_T t a) as [Heqa|Hneqa]; destruct (Req_EM_T t b) as [Heqb|Hneqb]. + rewrite Heqa; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). apply Rabs_pos. - pattern a at 3; rewrite <- e0; apply H3; assumption. - rewrite e; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; + pattern a at 3; rewrite <- Heqa; apply H3; assumption. + rewrite Heqa; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). apply Rabs_pos. - pattern a at 3; rewrite <- e; apply H3; assumption. - rewrite e; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; + pattern a at 3; rewrite <- Heqa; apply H3; assumption. + rewrite Heqb; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply Rle_trans with (Rabs (g t - phi2 n t)). apply Rabs_pos. - pattern b at 3; rewrite <- e; apply H3; assumption. + pattern b at 3; rewrite <- Heqb; apply H3; assumption. replace (f t) with (g t). apply H3; assumption. symmetry ; apply H0; elim H5; clear H5; intros. assert (H7 : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n2; assumption ]. + unfold Rmin; destruct (Rle_dec a b) as [Heqab|Hneqab]; + [ reflexivity | elim Hneqab; assumption ]. assert (H8 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n2; assumption ]. + unfold Rmax; destruct (Rle_dec a b) as [Heqab|Hneqab]; + [ reflexivity | elim Hneqab; assumption ]. rewrite H7 in H5; rewrite H8 in H6; split. - elim H5; intro; [ assumption | elim n1; symmetry ; assumption ]. - elim H6; intro; [ assumption | elim n0; assumption ]. + elim H5; intro; [ assumption | elim Hneqa; symmetry ; assumption ]. + elim H6; intro; [ assumption | elim Hneqb; assumption ]. cut (forall N:nat, RiemannInt_SF (phi2_m N) = RiemannInt_SF (phi2 N)). - intro; unfold Un_cv; intros; elim (u _ H4); intros; exists x1; intros; + intro; unfold Un_cv; intros; elim (HUn_cv _ H4); intros; exists x1; intros; rewrite (H3 n); apply H5; assumption. intro; apply Rle_antisym. apply StepFun_P37; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; - case (Req_EM_T x1 a); case (Req_EM_T x1 b); intros. - elim H3; intros; rewrite e0 in H4; elim (Rlt_irrefl _ H4). - elim H3; intros; rewrite e in H4; elim (Rlt_irrefl _ H4). - elim H3; intros; rewrite e in H5; elim (Rlt_irrefl _ H5). + destruct (Req_EM_T x1 a) as [Heqa|Hneqa]; destruct (Req_EM_T x1 b) as [Heqb|Hneqb]. + elim H3; intros; rewrite Heqa in H4; elim (Rlt_irrefl _ H4). + elim H3; intros; rewrite Heqa in H4; elim (Rlt_irrefl _ H4). + elim H3; intros; rewrite Heqb in H5; elim (Rlt_irrefl _ H5). right; reflexivity. apply StepFun_P37; try assumption. intros; unfold phi2_m; simpl; unfold phi2_aux; - case (Req_EM_T x1 a); case (Req_EM_T x1 b); intros. - elim H3; intros; rewrite e0 in H4; elim (Rlt_irrefl _ H4). - elim H3; intros; rewrite e in H4; elim (Rlt_irrefl _ H4). - elim H3; intros; rewrite e in H5; elim (Rlt_irrefl _ H5). + destruct (Req_EM_T x1 a) as [ -> |Hneqa]. + elim H3; intros; elim (Rlt_irrefl _ H4). + destruct (Req_EM_T x1 b) as [ -> |Hneqb]. + elim H3; intros; elim (Rlt_irrefl _ H5). right; reflexivity. intro; assert (H2 := pre (phi2 N)); unfold IsStepFun in H2; unfold is_subdivision in H2; elim H2; clear H2; intros l [lf H2]; @@ -1773,21 +1752,19 @@ Proof. apply le_O_n. apply lt_trans with (pred (Rlength l)); [ assumption | apply lt_pred_n_n ]. apply neq_O_lt; intro; rewrite <- H12 in H6; discriminate. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H; reflexivity. assert (H11 : pos_Rl l (S i) <= b). replace b with (Rmax a b). rewrite <- H4; elim (RList_P6 l); intros; apply H11. assumption. apply lt_le_S; assumption. apply lt_pred_n_n; apply neq_O_lt; intro; rewrite <- H13 in H6; discriminate. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - elim H7; clear H7; intros; unfold phi2_aux; case (Req_EM_T x1 a); - case (Req_EM_T x1 b); intros. - rewrite e in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). - rewrite e in H7; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H10 H7)). - rewrite e in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). + unfold Rmax; decide (Rle_dec a b) with H; reflexivity. + elim H7; clear H7; intros; unfold phi2_aux; destruct (Req_EM_T x1 a) as [Heq|Hneq]; + destruct (Req_EM_T x1 b) as [Heq'|Hneq']. + rewrite Heq' in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). + rewrite Heq in H7; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H10 H7)). + rewrite Heq' in H12; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H11 H12)). reflexivity. Qed. @@ -1850,17 +1827,17 @@ Proof. intros; replace (primitive h pr a) with 0. replace (RiemannInt pr0) with (primitive h pr b). ring. - unfold primitive; case (Rle_dec a b); case (Rle_dec b b); intros; + unfold primitive; destruct (Rle_dec a b) as [Hle|[]]; destruct (Rle_dec b b) as [Hle'|Hnle']; [ apply RiemannInt_P5 - | elim n; right; reflexivity - | elim n; assumption - | elim n0; assumption ]. - symmetry ; unfold primitive; case (Rle_dec a a); - case (Rle_dec a b); intros; + | destruct Hnle'; right; reflexivity + | assumption + | assumption]. + symmetry ; unfold primitive; destruct (Rle_dec a a) as [Hle|[]]; + destruct (Rle_dec a b) as [Hle'|Hnle']; [ apply RiemannInt_P9 - | elim n; assumption - | elim n; right; reflexivity - | elim n0; right; reflexivity ]. + | elim Hnle'; assumption + | right; reflexivity + | right; reflexivity ]. Qed. Lemma RiemannInt_P21 : @@ -1904,34 +1881,29 @@ Proof. intro; cut (IsStepFun psi3 a c). intro; split with (mkStepFun X); split with (mkStepFun X2); simpl; split. - intros; unfold phi3, psi3; case (Rle_dec t b); case (Rle_dec a t); - intros. + intros; unfold phi3, psi3; case (Rle_dec t b) as [|Hnle]; case (Rle_dec a t) as [|Hnle']. elim H1; intros; apply H3. replace (Rmin a b) with a. replace (Rmax a b) with b. split; assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - elim n; replace a with (Rmin a c). + unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. + unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. + elim Hnle'; replace a with (Rmin a c). elim H0; intros; assumption. - unfold Rmin; case (Rle_dec a c); intro; - [ reflexivity | elim n0; apply Rle_trans with b; assumption ]. + unfold Rmin; case (Rle_dec a c) as [|[]]; + [ reflexivity | apply Rle_trans with b; assumption ]. elim H2; intros; apply H3. replace (Rmax b c) with (Rmax a c). elim H0; intros; split; try assumption. replace (Rmin b c) with b. auto with real. - unfold Rmin; case (Rle_dec b c); intro; - [ reflexivity | elim n0; assumption ]. - unfold Rmax; case (Rle_dec a c); case (Rle_dec b c); intros; - try (elim n0; assumption || elim n0; apply Rle_trans with b; assumption). - reflexivity. - elim n; replace a with (Rmin a c). + unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. + unfold Rmax; decide (Rle_dec b c) with Hyp2; case (Rle_dec a c) as [|[]]; + [ reflexivity | apply Rle_trans with b; assumption ]. + elim Hnle'; replace a with (Rmin a c). elim H0; intros; assumption. - unfold Rmin; case (Rle_dec a c); intro; - [ reflexivity | elim n1; apply Rle_trans with b; assumption ]. + unfold Rmin; case (Rle_dec a c) as [|[]]; + [ reflexivity | apply Rle_trans with b; assumption ]. rewrite <- (StepFun_P43 X0 X1 X2). apply Rle_lt_trans with (Rabs (RiemannInt_SF (mkStepFun X0)) + Rabs (RiemannInt_SF (mkStepFun X1))). @@ -1945,33 +1917,33 @@ Proof. apply Rle_antisym. apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; - case (Rle_dec a x); case (Rle_dec x b); intros; - [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H0)) + destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; + [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H0)) | right; reflexivity - | elim n; apply Rle_trans with b; [ assumption | left; assumption ] - | elim n0; apply Rle_trans with b; [ assumption | left; assumption ] ]. + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; - case (Rle_dec a x); case (Rle_dec x b); intros; - [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H0)) + destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; + [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H0)) | right; reflexivity - | elim n; apply Rle_trans with b; [ assumption | left; assumption ] - | elim n0; apply Rle_trans with b; [ assumption | left; assumption ] ]. + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. apply Rle_antisym. apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; - case (Rle_dec a x); case (Rle_dec x b); intros; + destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ right; reflexivity - | elim n; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | elim Hnle'; left; assumption + | elim Hnle; left; assumption + | elim Hnle; left; assumption ]. apply StepFun_P37; try assumption. simpl; intros; unfold psi3; elim H0; clear H0; intros; - case (Rle_dec a x); case (Rle_dec x b); intros; + destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; [ right; reflexivity - | elim n; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | elim Hnle'; left; assumption + | elim Hnle; left; assumption + | elim Hnle; left; assumption ]. apply StepFun_P46 with b; assumption. assert (H3 := pre psi2); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; @@ -1988,14 +1960,14 @@ Proof. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. - unfold Rmin; case (Rle_dec b c); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec b c) with Hyp2; + reflexivity. elim H7; intros; assumption. - case (Rle_dec a x); case (Rle_dec x b); intros; - [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)) + destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; + [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H10)) | reflexivity - | elim n; apply Rle_trans with b; [ assumption | left; assumption ] - | elim n0; apply Rle_trans with b; [ assumption | left; assumption ] ]. + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. assert (H3 := pre psi1); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; split with lf1; unfold adapted_couple in H3; decompose [and] H3; @@ -2010,8 +1982,7 @@ Proof. rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. assert (H11 : a <= x). apply Rle_trans with (pos_Rl l1 i). replace a with (Rmin a b). @@ -2020,11 +1991,9 @@ Proof. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. left; elim H7; intros; assumption. - case (Rle_dec a x); case (Rle_dec x b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec a x) with H11; decide (Rle_dec x b) with H10; reflexivity. apply StepFun_P46 with b. assert (H3 := pre phi1); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; @@ -2040,8 +2009,7 @@ Proof. rewrite <- H4; elim (RList_P6 l1); intros; apply H10; try assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp1; reflexivity. assert (H11 : a <= x). apply Rle_trans with (pos_Rl l1 i). replace a with (Rmin a b). @@ -2050,10 +2018,9 @@ Proof. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H13 in H6; discriminate. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp1; reflexivity. left; elim H7; intros; assumption. - unfold phi3; case (Rle_dec a x); case (Rle_dec x b); intros; + unfold phi3; decide (Rle_dec a x) with H11; decide (Rle_dec x b) with H10; reflexivity || elim n; assumption. assert (H3 := pre phi2); unfold IsStepFun in H3; unfold is_subdivision in H3; elim H3; clear H3; intros l1 [lf1 H3]; split with l1; @@ -2070,14 +2037,13 @@ Proof. apply lt_trans with (pred (Rlength l1)); try assumption; apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H12 in H6; discriminate. - unfold Rmin; case (Rle_dec b c); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec b c) with Hyp2; reflexivity. elim H7; intros; assumption. - unfold phi3; case (Rle_dec a x); case (Rle_dec x b); intros; - [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)) + unfold phi3; destruct (Rle_dec a x) as [Hle|Hnle]; destruct (Rle_dec x b) as [Hle'|Hnle']; intros; + [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H10)) | reflexivity - | elim n; apply Rle_trans with b; [ assumption | left; assumption ] - | elim n0; apply Rle_trans with b; [ assumption | left; assumption ] ]. + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] + | elim Hnle; apply Rle_trans with b; [ assumption | left; assumption ] ]. Qed. Lemma RiemannInt_P22 : @@ -2096,21 +2062,10 @@ Proof. split; assumption. split with (mkStepFun H3); split with (mkStepFun H4); split. simpl; intros; apply H. - replace (Rmin a b) with (Rmin a c). - elim H5; intros; split; try assumption. + replace (Rmin a b) with (Rmin a c) by (rewrite 2!Rmin_left; eauto using Rle_trans). + destruct H5; split; try assumption. apply Rle_trans with (Rmax a c); try assumption. - replace (Rmax a b) with b. - replace (Rmax a c) with c. - assumption. - unfold Rmax; case (Rle_dec a c); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmin; case (Rle_dec a c); case (Rle_dec a b); intros; - [ reflexivity - | elim n; apply Rle_trans with c; assumption - | elim n; assumption - | elim n0; assumption ]. + apply Rle_max_compat_l; assumption. rewrite Rabs_right. assert (H5 : IsStepFun psi c b). apply StepFun_P46 with a. @@ -2128,15 +2083,11 @@ Proof. apply Rle_trans with (Rabs (f x - phi x)). apply Rabs_pos. apply H. - replace (Rmin a b) with a. - replace (Rmax a b) with b. - elim H6; intros; split; left. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. + destruct H6; split; left. apply Rle_lt_trans with c; assumption. assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. rewrite StepFun_P18; ring. apply Rle_lt_trans with (Rabs (RiemannInt_SF psi)). apply RRle_abs. @@ -2158,15 +2109,11 @@ Proof. apply Rle_trans with (Rabs (f x - phi x)). apply Rabs_pos. apply H. - replace (Rmin a b) with a. - replace (Rmax a b) with b. - elim H5; intros; split; left. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. + destruct H5; split; left. assumption. apply Rlt_le_trans with c; assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. rewrite StepFun_P18; ring. Qed. @@ -2189,18 +2136,10 @@ Proof. replace (Rmax a b) with (Rmax c b). elim H5; intros; split; try assumption. apply Rle_trans with (Rmin c b); try assumption. - replace (Rmin a b) with a. - replace (Rmin c b) with c. - assumption. - unfold Rmin; case (Rle_dec c b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmax; case (Rle_dec c b); case (Rle_dec a b); intros; - [ reflexivity - | elim n; apply Rle_trans with c; assumption - | elim n; assumption - | elim n0; assumption ]. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. rewrite Rabs_right. assert (H5 : IsStepFun psi a c). apply StepFun_P46 with b. @@ -2218,15 +2157,11 @@ Proof. apply Rle_trans with (Rabs (f x - phi x)). apply Rabs_pos. apply H. - replace (Rmin a b) with a. - replace (Rmax a b) with b. - elim H6; intros; split; left. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. + destruct H6; split; left. assumption. apply Rlt_le_trans with c; assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. rewrite StepFun_P18; ring. apply Rle_lt_trans with (Rabs (RiemannInt_SF psi)). apply RRle_abs. @@ -2248,15 +2183,11 @@ Proof. apply Rle_trans with (Rabs (f x - phi x)). apply Rabs_pos. apply H. - replace (Rmin a b) with a. - replace (Rmax a b) with b. - elim H5; intros; split; left. + rewrite Rmin_left; eauto using Rle_trans. + rewrite Rmax_right; eauto using Rle_trans. + destruct H5; split; left. apply Rle_lt_trans with c; assumption. assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; apply Rle_trans with c; assumption ]. rewrite StepFun_P18; ring. Qed. @@ -2289,16 +2220,15 @@ Lemma RiemannInt_P25 : a <= b -> b <= c -> RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3. Proof. intros f a b c pr1 pr2 pr3 Hyp1 Hyp2; unfold RiemannInt; - case (RiemannInt_exists pr1 RinvN RinvN_cv); - case (RiemannInt_exists pr2 RinvN RinvN_cv); - case (RiemannInt_exists pr3 RinvN RinvN_cv); intros; + case (RiemannInt_exists pr1 RinvN RinvN_cv) as (x1,HUn_cv1); + case (RiemannInt_exists pr2 RinvN RinvN_cv) as (x0,HUn_cv0); + case (RiemannInt_exists pr3 RinvN RinvN_cv) as (x,HUn_cv); symmetry ; eapply UL_sequence. - apply u. + apply HUn_cv. unfold Un_cv; intros; assert (H0 : 0 < eps / 3). unfold Rdiv; apply Rmult_lt_0_compat; [ assumption | apply Rinv_0_lt_compat; prove_sup0 ]. - elim (u1 _ H0); clear u1; intros N1 H1; elim (u0 _ H0); clear u0; - intros N2 H2; + destruct (HUn_cv1 _ H0) as (N1,H1); clear HUn_cv1; destruct (HUn_cv0 _ H0) as (N2,H2); clear HUn_cv0; cut (Un_cv (fun n:nat => @@ -2355,7 +2285,7 @@ Proof. do 2 rewrite (Rmult_comm 3); repeat rewrite Rmult_assoc; rewrite <- Rinv_l_sym; [ ring | discrR ] | discrR ]. - clear x u x0 x1 eps H H0 N1 H1 N2 H2; + clear x HUn_cv x0 x1 eps H H0 N1 H1 N2 H2; assert (H1 : exists psi1 : nat -> StepFun a b, @@ -2475,25 +2405,17 @@ Proof. apply Rplus_le_compat. apply H1. elim H14; intros; split. - replace (Rmin a c) with a. + rewrite Rmin_left; eauto using Rle_trans. apply Rle_trans with b; try assumption. left; assumption. - unfold Rmin; case (Rle_dec a c); intro; - [ reflexivity | elim n0; apply Rle_trans with b; assumption ]. - replace (Rmax a c) with c. + rewrite Rmax_right; eauto using Rle_trans. left; assumption. - unfold Rmax; case (Rle_dec a c); intro; - [ reflexivity | elim n0; apply Rle_trans with b; assumption ]. apply H3. elim H14; intros; split. - replace (Rmin b c) with b. + rewrite Rmin_left; eauto using Rle_trans. left; assumption. - unfold Rmin; case (Rle_dec b c); intro; - [ reflexivity | elim n0; assumption ]. - replace (Rmax b c) with c. + rewrite Rmax_right; eauto using Rle_trans. left; assumption. - unfold Rmax; case (Rle_dec b c); intro; - [ reflexivity | elim n0; assumption ]. do 2 rewrite <- (Rplus_comm @@ -2507,26 +2429,18 @@ Proof. apply Rplus_le_compat. apply H1. elim H14; intros; split. - replace (Rmin a c) with a. + rewrite Rmin_left; eauto using Rle_trans. left; assumption. - unfold Rmin; case (Rle_dec a c); intro; - [ reflexivity | elim n0; apply Rle_trans with b; assumption ]. - replace (Rmax a c) with c. + rewrite Rmax_right; eauto using Rle_trans. apply Rle_trans with b. left; assumption. assumption. - unfold Rmax; case (Rle_dec a c); intro; - [ reflexivity | elim n0; apply Rle_trans with b; assumption ]. apply H8. elim H14; intros; split. - replace (Rmin a b) with a. + rewrite Rmin_left; trivial. left; assumption. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. - replace (Rmax a b) with b. + rewrite Rmax_right; trivial. left; assumption. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n0; assumption ]. do 2 rewrite StepFun_P30. do 2 rewrite Rmult_1_l; replace @@ -2569,27 +2483,27 @@ Lemma RiemannInt_P26 : (pr2:Riemann_integrable f b c) (pr3:Riemann_integrable f a c), RiemannInt pr1 + RiemannInt pr2 = RiemannInt pr3. Proof. - intros; case (Rle_dec a b); case (Rle_dec b c); intros. + intros; destruct (Rle_dec a b) as [Hle|Hnle]; destruct (Rle_dec b c) as [Hle'|Hnle']. apply RiemannInt_P25; assumption. - case (Rle_dec a c); intro. + destruct (Rle_dec a c) as [Hle''|Hnle'']. assert (H : c <= b). auto with real. - rewrite <- (RiemannInt_P25 pr3 (RiemannInt_P1 pr2) pr1 r0 H); + rewrite <- (RiemannInt_P25 pr3 (RiemannInt_P1 pr2) pr1 Hle'' H); rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); ring. assert (H : c <= a). auto with real. rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); - rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr3) pr1 (RiemannInt_P1 pr2) H r); + rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr3) pr1 (RiemannInt_P1 pr2) H Hle); rewrite (RiemannInt_P8 pr3 (RiemannInt_P1 pr3)); ring. assert (H : b <= a). auto with real. - case (Rle_dec a c); intro. - rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr1) pr3 pr2 H r0); + destruct (Rle_dec a c) as [Hle''|Hnle'']. + rewrite <- (RiemannInt_P25 (RiemannInt_P1 pr1) pr3 pr2 H Hle''); rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); ring. assert (H0 : c <= a). auto with real. rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); - rewrite <- (RiemannInt_P25 pr2 (RiemannInt_P1 pr3) (RiemannInt_P1 pr1) r H0); + rewrite <- (RiemannInt_P25 pr2 (RiemannInt_P1 pr3) (RiemannInt_P1 pr1) Hle' H0); rewrite (RiemannInt_P8 pr3 (RiemannInt_P1 pr3)); ring. rewrite (RiemannInt_P8 pr1 (RiemannInt_P1 pr1)); rewrite (RiemannInt_P8 pr2 (RiemannInt_P1 pr2)); @@ -2614,13 +2528,13 @@ Proof. assert (H4 : 0 < del). unfold del; unfold Rmin; case (Rle_dec (b - x) (x - a)); intro. - case (Rle_dec x0 (b - x)); intro; + destruct (Rle_dec x0 (b - x)) as [Hle|Hnle]; [ elim H3; intros; assumption | apply Rlt_Rminus; assumption ]. - case (Rle_dec x0 (x - a)); intro; + destruct (Rle_dec x0 (x - a)) as [Hle'|Hnle']; [ elim H3; intros; assumption | apply Rlt_Rminus; assumption ]. split with (mkposreal _ H4); intros; assert (H7 : Riemann_integrable f x (x + h0)). - case (Rle_dec x (x + h0)); intro. + destruct (Rle_dec x (x + h0)) as [Hle''|Hnle'']. apply continuity_implies_RiemannInt; try assumption. intros; apply C0; elim H7; intros; split. apply Rle_trans with x; [ left; assumption | assumption ]. @@ -2657,7 +2571,7 @@ Proof. with ((RiemannInt H7 - RiemannInt (RiemannInt_P14 x (x + h0) (f x))) / h0). replace (RiemannInt H7 - RiemannInt (RiemannInt_P14 x (x + h0) (f x))) with (RiemannInt (RiemannInt_P10 (-1) H7 (RiemannInt_P14 x (x + h0) (f x)))). - unfold Rdiv; rewrite Rabs_mult; case (Rle_dec x (x + h0)); intro. + unfold Rdiv; rewrite Rabs_mult; destruct (Rle_dec x (x + h0)) as [Hle|Hnle]. apply Rle_lt_trans with (RiemannInt (RiemannInt_P16 @@ -2676,10 +2590,10 @@ Proof. apply Rabs_pos. apply RiemannInt_P19; try assumption. intros; replace (f x1 + -1 * fct_cte (f x) x1) with (f x1 - f x). - unfold fct_cte; case (Req_dec x x1); intro. + unfold fct_cte; destruct (Req_dec x x1) as [H9|H9]. rewrite H9; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; left; assumption. - elim H3; intros; left; apply H11. + elim H3; intros; left; apply H11. repeat split. assumption. rewrite Rabs_right. @@ -2705,7 +2619,7 @@ Proof. apply Rinv_r_sym. assumption. apply Rle_ge; left; apply Rinv_0_lt_compat. - elim r; intro. + elim Hle; intro. apply Rplus_lt_reg_l with x; rewrite Rplus_0_r; assumption. elim H5; symmetry ; apply Rplus_eq_reg_l with x; rewrite Rplus_0_r; assumption. @@ -2790,9 +2704,11 @@ Proof. cut (a <= x + h0). cut (x + h0 <= b). intros; unfold primitive. - case (Rle_dec a (x + h0)); case (Rle_dec (x + h0) b); case (Rle_dec a x); - case (Rle_dec x b); intros; try (elim n; assumption || left; assumption). - rewrite <- (RiemannInt_P26 (FTC_P1 h C0 r0 r) H7 (FTC_P1 h C0 r2 r1)); ring. + assert (H10: a <= x) by (left; assumption). + assert (H11: x <= b) by (left; assumption). + decide (Rle_dec a (x + h0)) with H9; decide (Rle_dec (x + h0) b) with H8; + decide (Rle_dec a x) with H10; decide (Rle_dec x b) with H11. + rewrite <- (RiemannInt_P26 (FTC_P1 h C0 H10 H11) H7 (FTC_P1 h C0 H9 H8)); ring. apply Rplus_le_reg_l with (- x); replace (- x + (x + h0)) with h0; [ idtac | ring ]. rewrite Rplus_comm; apply Rle_trans with (Rabs h0). @@ -2852,11 +2768,11 @@ Proof. unfold R_dist; intros; set (del := Rmin x0 (Rmin x1 (b - a))); assert (H10 : 0 < del). unfold del; unfold Rmin; case (Rle_dec x1 (b - a)); intros. - case (Rle_dec x0 x1); intro; + destruct (Rle_dec x0 x1) as [Hle|Hnle]; [ apply (cond_pos x0) | elim H9; intros; assumption ]. - case (Rle_dec x0 (b - a)); intro; + destruct (Rle_dec x0 (b - a)) as [Hle'|Hnle']; [ apply (cond_pos x0) | apply Rlt_Rminus; assumption ]. - split with (mkposreal _ H10); intros; case (Rcase_abs h0); intro. + split with (mkposreal _ H10); intros; destruct (Rcase_abs h0) as [Hle|Hnle]. assert (H14 : b + h0 < b). pattern b at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. @@ -2955,11 +2871,11 @@ Proof. | assumption ]. cut (a <= b + h0). cut (b + h0 <= b). - intros; unfold primitive; case (Rle_dec a (b + h0)); - case (Rle_dec (b + h0) b); case (Rle_dec a b); case (Rle_dec b b); - intros; try (elim n; right; reflexivity) || (elim n; left; assumption). - rewrite <- (RiemannInt_P26 (FTC_P1 h C0 r3 r2) H13 (FTC_P1 h C0 r1 r0)); ring. - elim n; assumption. + intros; unfold primitive; destruct (Rle_dec a (b + h0)) as [Hle'|Hnle']; + destruct (Rle_dec (b + h0) b) as [Hle''|[]]; destruct (Rle_dec a b) as [Hleab|[]]; destruct (Rle_dec b b) as [Hlebb|[]]; + assumption || (right; reflexivity) || (try (left; assumption)). + rewrite <- (RiemannInt_P26 (FTC_P1 h C0 Hle' Hle'') H13 (FTC_P1 h C0 Hleab Hlebb)); ring. + elim Hnle'; assumption. left; assumption. apply Rplus_le_reg_l with (- a - h0). replace (- a - h0 + a) with (- h0); [ idtac | ring ]. @@ -2977,22 +2893,22 @@ Proof. [ assumption | unfold del; apply Rmin_l ]. assert (H14 : b < b + h0). pattern b at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. - assert (H14 := Rge_le _ _ r); elim H14; intro. + assert (H14 := Rge_le _ _ Hnle); elim H14; intro. assumption. elim H11; symmetry ; assumption. - unfold primitive; case (Rle_dec a (b + h0)); - case (Rle_dec (b + h0) b); intros; - [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H14)) + unfold primitive; destruct (Rle_dec a (b + h0)) as [Hle|[]]; + destruct (Rle_dec (b + h0) b) as [Hle'|Hnle']; + [ elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H14)) | unfold f_b; reflexivity - | elim n; left; apply Rlt_trans with b; assumption - | elim n0; left; apply Rlt_trans with b; assumption ]. + | left; apply Rlt_trans with b; assumption + | left; apply Rlt_trans with b; assumption ]. unfold f_b; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; unfold primitive; - case (Rle_dec a b); case (Rle_dec b b); intros; + destruct (Rle_dec a b) as [Hle'|Hnle']; destruct (Rle_dec b b) as [Hle''|[]]; [ apply RiemannInt_P5 - | elim n; right; reflexivity - | elim n; left; assumption - | elim n; right; reflexivity ]. + | right; reflexivity + | elim Hnle'; left; assumption + | right; reflexivity ]. (*****) set (f_a := fun x:R => f a * (x - a)); rewrite <- H2; assert (H3 : derivable_pt_lim f_a a (f a)). @@ -3026,16 +2942,18 @@ Proof. apply (cond_pos x0). apply Rlt_Rminus; assumption. split with (mkposreal _ H9). - intros; case (Rcase_abs h0); intro. + intros; destruct (Rcase_abs h0) as [Hle|Hnle]. assert (H12 : a + h0 < a). pattern a at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. unfold primitive. - case (Rle_dec a (a + h0)); case (Rle_dec (a + h0) b); case (Rle_dec a a); - case (Rle_dec a b); intros; - try (elim n; left; assumption) || (elim n; right; reflexivity). - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H12)). - elim n; left; apply Rlt_trans with a; assumption. + destruct (Rle_dec a (a + h0)) as [Hle'|Hnle']; + destruct (Rle_dec (a + h0) b) as [Hle''|Hnle'']; + destruct (Rle_dec a a) as [Hleaa|[]]; + destruct (Rle_dec a b) as [Hleab|[]]; + try (left; assumption) || (right; reflexivity). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle' H12)). + elim Hnle''; left; apply Rlt_trans with a; assumption. rewrite RiemannInt_P9; replace 0 with (f_a a). replace (f a * (a + h0 - a)) with (f_a (a + h0)). apply H5; try assumption. @@ -3043,10 +2961,10 @@ Proof. [ assumption | unfold del; apply Rmin_l ]. unfold f_a; ring. unfold f_a; ring. - elim n; left; apply Rlt_trans with a; assumption. + elim Hnle''; left; apply Rlt_trans with a; assumption. assert (H12 : a < a + h0). pattern a at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. - assert (H12 := Rge_le _ _ r); elim H12; intro. + assert (H12 := Rge_le _ _ Hnle); elim H12; intro. assumption. elim H10; symmetry ; assumption. assert (H13 : Riemann_integrable f a (a + h0)). @@ -3119,7 +3037,7 @@ Proof. rewrite Rplus_comm; unfold Rminus; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; rewrite <- Rinv_r_sym; [ reflexivity | assumption ]. - apply Rle_ge; left; apply Rinv_0_lt_compat; assert (H14 := Rge_le _ _ r); + apply Rle_ge; left; apply Rinv_0_lt_compat; assert (H14 := Rge_le _ _ Hnle); elim H14; intro. assumption. elim H10; symmetry ; assumption. @@ -3134,13 +3052,13 @@ Proof. rewrite Rmult_assoc; rewrite <- Rinv_r_sym; [ ring | assumption ]. cut (a <= a + h0). cut (a + h0 <= b). - intros; unfold primitive; case (Rle_dec a (a + h0)); - case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); - intros; try (elim n; right; reflexivity) || (elim n; left; assumption). + intros; unfold primitive. + decide (Rle_dec (a+h0) b) with H14. + decide (Rle_dec a a) with (Rle_refl a). + decide (Rle_dec a (a+h0)) with H15. + decide (Rle_dec a b) with h. rewrite RiemannInt_P9; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; apply RiemannInt_P5. - elim n; assumption. - elim n; assumption. 2: left; assumption. apply Rplus_le_reg_l with (- a); replace (- a + (a + h0)) with h0; [ idtac | ring ]. @@ -3187,18 +3105,18 @@ Proof. unfold derivable_pt_lim; intros; elim (H2 _ H4); intros; elim (H3 _ H4); intros; set (del := Rmin x0 x1). assert (H7 : 0 < del). - unfold del; unfold Rmin; case (Rle_dec x0 x1); intro. + unfold del; unfold Rmin; destruct (Rle_dec x0 x1) as [Hle|Hnle]. apply (cond_pos x0). apply (cond_pos x1). - split with (mkposreal _ H7); intros; case (Rcase_abs h0); intro. + split with (mkposreal _ H7); intros; destruct (Rcase_abs h0) as [Hle|Hnle]. assert (H10 : a + h0 < a). pattern a at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. - rewrite H1; unfold primitive; case (Rle_dec a (a + h0)); - case (Rle_dec (a + h0) b); case (Rle_dec a a); case (Rle_dec a b); - intros; try (elim n; right; assumption || reflexivity). - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H10)). - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r2 H10)). + rewrite H1; unfold primitive. + apply (decide_left (Rle_dec a b) h); intro h'. + assert (H11:~ a<=a+h0) by auto using Rlt_not_le. + decide (Rle_dec a (a+h0)) with H11. + decide (Rle_dec a a) with (Rle_refl a). rewrite RiemannInt_P9; replace 0 with (f_a a). replace (f a * (a + h0 - a)) with (f_a (a + h0)). apply H5; try assumption. @@ -3206,27 +3124,26 @@ Proof. unfold del; apply Rmin_l. unfold f_a; ring. unfold f_a; ring. - elim n; rewrite <- H0; left; assumption. assert (H10 : a < a + h0). pattern a at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l. - assert (H10 := Rge_le _ _ r); elim H10; intro. + assert (H10 := Rge_le _ _ Hnle); elim H10; intro. assumption. elim H8; symmetry ; assumption. - rewrite H0 in H1; rewrite H1; unfold primitive; - case (Rle_dec a (b + h0)); case (Rle_dec (b + h0) b); - case (Rle_dec a b); case (Rle_dec b b); intros; - try (elim n; right; assumption || reflexivity). - rewrite H0 in H10; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r2 H10)). - repeat rewrite RiemannInt_P9. - replace (RiemannInt (FTC_P1 h C0 r1 r0)) with (f_b b). + rewrite H0 in H1; rewrite H1; unfold primitive. + decide (Rle_dec a b) with h. + decide (Rle_dec b b) with (Rle_refl b). + assert (H12 : a<=b+h0) by (eauto using Rlt_le_trans with real). + decide (Rle_dec a (b+h0)) with H12. + rewrite H0 in H10. + assert (H13 : ~b+h0<=b) by (auto using Rlt_not_le). + decide (Rle_dec (b+h0) b) with H13. + replace (RiemannInt (FTC_P1 h C0 hbis H11)) with (f_b b). fold (f_b (b + h0)). apply H6; try assumption. apply Rlt_le_trans with del; try assumption. unfold del; apply Rmin_r. unfold f_b; unfold Rminus; rewrite Rplus_opp_r; rewrite Rmult_0_r; rewrite Rplus_0_l; apply RiemannInt_P5. - elim n; rewrite <- H0; left; assumption. - elim n0; rewrite <- H0; left; assumption. Qed. Lemma RiemannInt_P29 : @@ -3264,7 +3181,7 @@ Qed. Lemma RiemannInt_P32 : forall (f:C1_fun) (a b:R), Riemann_integrable (derive f (diff0 f)) a b. Proof. - intro f; intros; case (Rle_dec a b); intro; + intro f; intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply continuity_implies_RiemannInt; try assumption; intros; apply (cont1 f) | assert (H : b <= a); @@ -3294,7 +3211,7 @@ Lemma FTC_Riemann : forall (f:C1_fun) (a b:R) (pr:Riemann_integrable (derive f (diff0 f)) a b), RiemannInt pr = f b - f a. Proof. - intro f; intros; case (Rle_dec a b); intro; + intro f; intros; destruct (Rle_dec a b) as [Hle|Hnle]; [ apply RiemannInt_P33; assumption | assert (H : b <= a); [ auto with real diff --git a/theories/Reals/RiemannInt_SF.v b/theories/Reals/RiemannInt_SF.v index 9de60bb5d..9466ed8e6 100644 --- a/theories/Reals/RiemannInt_SF.v +++ b/theories/Reals/RiemannInt_SF.v @@ -173,8 +173,8 @@ Lemma StepFun_P1 : forall (a b:R) (f:StepFun a b), adapted_couple f a b (subdivision f) (subdivision_val f). Proof. - intros a b f; unfold subdivision_val; case (projT2 (pre f)); intros; - apply a0. + intros a b f; unfold subdivision_val; case (projT2 (pre f)) as (x,H); + apply H. Qed. Lemma StepFun_P2 : @@ -201,19 +201,17 @@ Proof. intros; unfold adapted_couple; repeat split. unfold ordered_Rlist; intros; simpl in H0; inversion H0; [ simpl; assumption | elim (le_Sn_O _ H2) ]. - simpl; unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a b) with H; reflexivity. + simpl; unfold Rmax; decide (Rle_dec a b) with H; reflexivity. unfold constant_D_eq, open_interval; intros; simpl in H0; inversion H0; [ reflexivity | elim (le_Sn_O _ H3) ]. Qed. Lemma StepFun_P4 : forall a b c:R, IsStepFun (fct_cte c) a b. Proof. - intros; unfold IsStepFun; case (Rle_dec a b); intro. + intros; unfold IsStepFun; destruct (Rle_dec a b) as [Hle|Hnle]. apply existT with (cons a (cons b nil)); unfold is_subdivision; - apply existT with (cons c nil); apply (StepFun_P3 c r). + apply existT with (cons c nil); apply (StepFun_P3 c Hle). apply existT with (cons b (cons a nil)); unfold is_subdivision; apply existT with (cons c nil); apply StepFun_P2; apply StepFun_P3; auto with real. @@ -244,17 +242,15 @@ Lemma StepFun_P7 : Proof. unfold adapted_couple; intros; decompose [and] H0; clear H0; assert (H5 : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H; reflexivity. assert (H7 : r2 <= b). rewrite H5 in H2; rewrite <- H2; apply RList_P7; [ assumption | simpl; right; left; reflexivity ]. repeat split. apply RList_P4 with r1; assumption. - rewrite H5 in H2; unfold Rmin; case (Rle_dec r2 b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmax; case (Rle_dec r2 b); intro; - [ rewrite H5 in H2; rewrite <- H2; reflexivity | elim n; assumption ]. + rewrite H5 in H2; unfold Rmin; decide (Rle_dec r2 b) with H7; reflexivity. + unfold Rmax; decide (Rle_dec r2 b) with H7. + rewrite H5 in H2; rewrite <- H2; reflexivity. simpl in H4; simpl; apply INR_eq; apply Rplus_eq_reg_l with 1; do 2 rewrite (Rplus_comm 1); do 2 rewrite <- S_INR; rewrite H4; reflexivity. @@ -340,33 +336,28 @@ Proof. apply H6. rewrite <- Hyp_eq; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; clear H1; simpl in H9; rewrite H9; - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. elim H6; clear H6; intros l' [lf' H6]; case (Req_dec t2 b); intro. exists (cons a (cons b nil)); exists (cons r1 nil); unfold adapted_couple_opt; unfold adapted_couple; repeat split. unfold ordered_Rlist; intros; simpl in H8; inversion H8; [ simpl; assumption | elim (le_Sn_O _ H10) ]. - simpl; unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a b) with H0; reflexivity. + simpl; unfold Rmax; decide (Rle_dec a b) with H0; reflexivity. intros; simpl in H8; inversion H8. unfold constant_D_eq, open_interval; intros; simpl; simpl in H9; rewrite H3 in H1; unfold adapted_couple in H1; decompose [and] H1; apply (H16 0%nat). simpl; apply lt_O_Sn. unfold open_interval; simpl; rewrite H7; simpl in H13; - rewrite H13; unfold Rmin; case (Rle_dec a b); - intro; [ assumption | elim n; assumption ]. + rewrite H13; unfold Rmin; decide (Rle_dec a b) with H0; assumption. elim (le_Sn_O _ H10). intros; simpl in H8; elim (lt_n_O _ H8). intros; simpl in H8; inversion H8; [ simpl; assumption | elim (le_Sn_O _ H10) ]. assert (Hyp_min : Rmin t2 b = t2). - unfold Rmin; case (Rle_dec t2 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec t2 b) with H5; reflexivity. unfold adapted_couple in H6; elim H6; clear H6; intros; elim (RList_P20 _ (StepFun_P9 H6 H7)); intros s1 [s2 [s3 H9]]; induction lf' as [| r2 lf' Hreclf']. @@ -391,18 +382,16 @@ Proof. apply (H16 (S i)); simpl; assumption. simpl; simpl in H14; rewrite H14; reflexivity. simpl; simpl in H18; rewrite H18; unfold Rmax; - case (Rle_dec a b); case (Rle_dec t2 b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec a b) with H0; decide (Rle_dec t2 b) with H5; reflexivity. simpl; simpl in H20; apply H20. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. - simpl; simpl in H6; case (total_order_T x t2); intro. - elim s; intro. + simpl; simpl in H6; destruct (total_order_T x t2) as [[Hlt|Heq]|Hgt]. apply (H17 0%nat); [ simpl; apply lt_O_Sn | unfold open_interval; simpl; elim H6; intros; split; assumption ]. - rewrite b0; assumption. + rewrite Heq; assumption. rewrite H10; apply (H22 0%nat); [ simpl; apply lt_O_Sn | unfold open_interval; simpl; replace s1 with t2; @@ -440,8 +429,7 @@ Proof. assumption. simpl; simpl in H19; apply H19. rewrite H9; simpl; simpl in H13; rewrite H13; unfold Rmax; - case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. rewrite H9; simpl; simpl in H15; rewrite H15; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -483,8 +471,7 @@ Proof. assumption. simpl; simpl in H18; apply H18. rewrite H9; simpl; simpl in H12; rewrite H12; unfold Rmax; - case (Rle_dec t2 b); case (Rle_dec a b); intros; reflexivity || elim n; - assumption. + decide (Rle_dec t2 b) with H5; decide (Rle_dec a b) with H0; reflexivity. rewrite H9; simpl; simpl in H14; rewrite H14; reflexivity. intros; simpl in H1; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -511,8 +498,7 @@ Proof. clear H1; clear H H7 H9; cut (Rmax a b = b); [ intro; rewrite H in H5; rewrite <- H5; apply RList_P7; [ assumption | simpl; right; left; reflexivity ] - | unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] ]. + | unfold Rmax; decide (Rle_dec a b) with H0; reflexivity ]. Qed. Lemma StepFun_P11 : @@ -528,7 +514,7 @@ Proof. simpl in H10; simpl in H5; rewrite H10; rewrite H5; reflexivity. assert (H14 := H3 0%nat (lt_O_Sn _)); simpl in H14; elim H14; intro. assert (H15 := H7 0%nat (lt_O_Sn _)); simpl in H15; elim H15; intro. - rewrite <- H12 in H1; case (Rle_dec r1 s2); intro; try assumption. + rewrite <- H12 in H1; destruct (Rle_dec r1 s2) as [Hle|Hnle]; try assumption. assert (H16 : s2 < r1); auto with real. induction s3 as [| r0 s3 Hrecs3]. simpl in H9; rewrite H9 in H16; cut (r1 <= Rmax a b). @@ -662,12 +648,11 @@ Lemma StepFun_P13 : adapted_couple f a b (cons r (cons r1 r2)) (cons r3 lf1) -> adapted_couple_opt f a b (cons s1 (cons s2 s3)) (cons r4 lf2) -> r1 <= s2. Proof. - intros; case (total_order_T a b); intro. - elim s; intro. - eapply StepFun_P11; [ apply a0 | apply H0 | apply H1 ]. + intros; destruct (total_order_T a b) as [[Hlt|Heq]|Hgt]. + eapply StepFun_P11; [ apply Hlt | apply H0 | apply H1 ]. elim H; assumption. eapply StepFun_P11; - [ apply r0 | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. + [ apply Hgt | apply StepFun_P2; apply H0 | apply StepFun_P12; apply H1 ]. Qed. Lemma StepFun_P14 : @@ -689,11 +674,9 @@ Proof. case (Req_dec a b); intro. rewrite (StepFun_P8 H2 H4); rewrite (StepFun_P8 H H4); reflexivity. assert (Hyp_min : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H1; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H1; reflexivity. elim (RList_P20 _ (StepFun_P9 H H4)); intros s1 [s2 [s3 H5]]; rewrite H5 in H; rewrite H5; induction lf1 as [| r3 lf1 Hreclf1]. unfold adapted_couple in H2; decompose [and] H2; @@ -883,8 +866,8 @@ Lemma StepFun_P15 : adapted_couple f a b l1 lf1 -> adapted_couple_opt f a b l2 lf2 -> Int_SF lf1 l1 = Int_SF lf2 l2. Proof. - intros; case (Rle_dec a b); intro; - [ apply (StepFun_P14 r H H0) + intros; destruct (Rle_dec a b) as [Hle|Hnle]; + [ apply (StepFun_P14 Hle H H0) | assert (H1 : b <= a); [ auto with real | eapply StepFun_P14; @@ -897,8 +880,8 @@ Lemma StepFun_P16 : exists l' : Rlist, (exists lf' : Rlist, adapted_couple_opt f a b l' lf'). Proof. - intros; case (Rle_dec a b); intro; - [ apply (StepFun_P10 r H) + intros; destruct (Rle_dec a b) as [Hle|Hnle]; + [ apply (StepFun_P10 Hle H) | assert (H1 : b <= a); [ auto with real | assert (H2 := StepFun_P10 H1 (StepFun_P2 H)); elim H2; @@ -1003,11 +986,9 @@ Lemma StepFun_P22 : Proof. unfold is_subdivision; intros a b f g lf lg Hyp X X0; elim X; elim X0; clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. apply existT with (FF (cons_ORlist lf lg) f); unfold adapted_couple in p, p0; decompose [and] p; decompose [and] p0; clear p p0; rewrite Hyp_min in H6; rewrite Hyp_min in H1; rewrite Hyp_max in H0; @@ -1255,11 +1236,9 @@ Lemma StepFun_P24 : Proof. unfold is_subdivision; intros a b f g lf lg Hyp X X0; elim X; elim X0; clear X X0; intros lg0 p lf0 p0; assert (Hyp_min : Rmin a b = a). - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with Hyp; reflexivity. assert (Hyp_max : Rmax a b = b). - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with Hyp; reflexivity. apply existT with (FF (cons_ORlist lf lg) g); unfold adapted_couple in p, p0; decompose [and] p; decompose [and] p0; clear p p0; rewrite Hyp_min in H1; rewrite Hyp_min in H6; rewrite Hyp_max in H0; @@ -1652,7 +1631,7 @@ Lemma StepFun_P34 : a <= b -> Rabs (RiemannInt_SF f) <= RiemannInt_SF (mkStepFun (StepFun_P32 f)). Proof. - intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; decide (Rle_dec a b) with H. replace (Int_SF (subdivision_val (mkStepFun (StepFun_P32 f))) (subdivision (mkStepFun (StepFun_P32 f)))) with @@ -1663,7 +1642,6 @@ Proof. apply StepFun_P17 with (fun x:R => Rabs (f x)) a b; [ apply StepFun_P31; apply StepFun_P1 | apply (StepFun_P1 (mkStepFun (StepFun_P32 f))) ]. - elim n; assumption. Qed. Lemma StepFun_P35 : @@ -1741,24 +1719,21 @@ Lemma StepFun_P36 : (forall x:R, a < x < b -> f x <= g x) -> RiemannInt_SF f <= RiemannInt_SF g. Proof. - intros; unfold RiemannInt_SF; case (Rle_dec a b); intro. + intros; unfold RiemannInt_SF; decide (Rle_dec a b) with H. replace (Int_SF (subdivision_val f) (subdivision f)) with (Int_SF (FF l f) l). replace (Int_SF (subdivision_val g) (subdivision g)) with (Int_SF (FF l g) l). unfold is_subdivision in X; elim X; clear X; intros; unfold adapted_couple in p; decompose [and] p; clear p; assert (H5 : Rmin a b = a); - [ unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] + [ unfold Rmin; decide (Rle_dec a b) with H; reflexivity | assert (H7 : Rmax a b = b); - [ unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ] + [ unfold Rmax; decide (Rle_dec a b) with H; reflexivity | rewrite H5 in H3; rewrite H7 in H2; eapply StepFun_P35 with a b; assumption ] ]. apply StepFun_P17 with (fe g) a b; [ apply StepFun_P21; assumption | apply StepFun_P1 ]. apply StepFun_P17 with (fe f) a b; [ apply StepFun_P21; assumption | apply StepFun_P1 ]. - elim n; assumption. Qed. Lemma StepFun_P37 : @@ -1819,8 +1794,7 @@ Proof. induction i as [| i Hreci]. simpl; rewrite H12; replace (Rmin r1 b) with r1. simpl in H0; rewrite <- H0; apply (H 0%nat); simpl; apply lt_O_Sn. - unfold Rmin; case (Rle_dec r1 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. apply (H10 i); apply lt_S_n. replace (S (pred (Rlength lg))) with (Rlength lg). apply H9. @@ -1829,8 +1803,7 @@ Proof. simpl; assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec a b) with H14; reflexivity. assert (H14 : a <= b). rewrite <- H1; simpl in H0; rewrite <- H0; apply RList_P7; [ assumption | left; reflexivity ]. @@ -1838,14 +1811,13 @@ Proof. rewrite <- H11; induction lg as [| r0 lg Hreclg]. simpl in H13; discriminate. reflexivity. - unfold Rmax; case (Rle_dec a b); case (Rle_dec r1 b); intros; - reflexivity || elim n; assumption. + unfold Rmax; decide (Rle_dec a b) with H14; decide (Rle_dec r1 b) with H7; + reflexivity. simpl; rewrite H13; reflexivity. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, open_interval; simpl; intros; assert (H16 : Rmin r1 b = r1). - unfold Rmin; case (Rle_dec r1 b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. rewrite H16 in H12; rewrite H12 in H14; elim H14; clear H14; intros _ H14; unfold g'; case (Rle_dec r1 x); intro r3. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r3 H14)). @@ -1862,9 +1834,9 @@ Proof. assert (H18 := H16 H17); unfold constant_D_eq, open_interval in H18; unfold constant_D_eq, open_interval; intros; assert (H19 := H18 _ H14); rewrite <- H19; unfold g'; - case (Rle_dec r1 x); intro. + case (Rle_dec r1 x) as [|[]]. reflexivity. - elim n; replace r1 with (Rmin r1 b). + replace r1 with (Rmin r1 b). rewrite <- H12; elim H14; clear H14; intros H14 _; left; apply Rle_lt_trans with (pos_Rl lg i); try assumption. apply RList_P5. @@ -1874,12 +1846,9 @@ Proof. apply lt_trans with (pred (Rlength lg)); try assumption. apply lt_pred_n_n; apply neq_O_lt; red; intro; rewrite <- H22 in H17; elim (lt_n_O _ H17). - unfold Rmin; case (Rle_dec r1 b); intro; - [ reflexivity | elim n0; assumption ]. + unfold Rmin; decide (Rle_dec r1 b) with H7; reflexivity. exists (mkStepFun H8); split. - simpl; unfold g'; case (Rle_dec r1 b); intro. - assumption. - elim n; assumption. + simpl; unfold g'; decide (Rle_dec r1 b) with H7; assumption. intros; simpl in H9; induction i as [| i Hreci]. unfold constant_D_eq, co_interval; simpl; intros; simpl in H0; rewrite H0; elim H10; clear H10; intros; unfold g'; @@ -1896,9 +1865,9 @@ Proof. assert (H12 := H10 H11); unfold constant_D_eq, co_interval in H12; unfold constant_D_eq, co_interval; intros; rewrite <- (H12 _ H13); simpl; unfold g'; - case (Rle_dec r1 x); intro. + case (Rle_dec r1 x) as [|[]]. reflexivity. - elim n; elim H13; clear H13; intros; + elim H13; clear H13; intros; apply Rle_trans with (pos_Rl (cons r1 l) i); try assumption; change (pos_Rl (cons r1 l) 0 <= pos_Rl (cons r1 l) i); elim (RList_P6 (cons r1 l)); intros; apply H15; @@ -1954,24 +1923,22 @@ Proof. unfold adapted_couple; decompose [and] H1; decompose [and] H2; clear H1 H2; repeat split. apply RList_P25; try assumption. - rewrite H10; rewrite H4; unfold Rmin, Rmax; case (Rle_dec a b); - case (Rle_dec b c); intros; - (right; reflexivity) || (elim n; left; assumption). + rewrite H10; rewrite H4; unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; + case (Rle_dec b c) as [|[]]; + (right; reflexivity) || (left; assumption). rewrite RList_P22. - rewrite H5; unfold Rmin, Rmax; case (Rle_dec a b); case (Rle_dec a c); - intros; + rewrite H5; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; apply Rle_trans with b; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | left; assumption + | apply Rle_trans with b; left; assumption + | left; assumption ]. red; intro; rewrite H1 in H6; discriminate. rewrite RList_P24. - rewrite H9; unfold Rmin, Rmax; case (Rle_dec b c); case (Rle_dec a c); - intros; + rewrite H9; unfold Rmin, Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec b c) as [|[]]; [ reflexivity - | elim n; apply Rle_trans with b; left; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + | left; assumption + | apply Rle_trans with b; left; assumption + | left; assumption ]. red; intro; rewrite H1 in H11; discriminate. apply StepFun_P20. rewrite RList_P23; apply neq_O_lt; red; intro. @@ -2061,7 +2028,7 @@ Proof. assert (H16 : pos_Rl (cons_Rlist l1 l2) (S i) = b). rewrite RList_P29. rewrite H15; rewrite <- minus_n_n; rewrite H10; unfold Rmin; - case (Rle_dec b c); intro; [ reflexivity | elim n; left; assumption ]. + case (Rle_dec b c) as [|[]]; [ reflexivity | left; assumption ]. rewrite H15; apply le_n. induction l1 as [| r l1 Hrecl1]. simpl in H15; discriminate. @@ -2069,8 +2036,8 @@ Proof. assert (H17 : pos_Rl (cons_Rlist l1 l2) i = b). rewrite RList_P26. replace i with (pred (Rlength l1)); - [ rewrite H4; unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; left; assumption ] + [ rewrite H4; unfold Rmax; case (Rle_dec a b) as [|[]]; + [ reflexivity | left; assumption ] | rewrite H15; reflexivity ]. rewrite H15; apply lt_n_Sn. rewrite H16 in H2; rewrite H17 in H2; elim H2; intros; @@ -2095,8 +2062,8 @@ Proof. discriminate. clear Hrecl1; induction l1 as [| r0 l1 Hrecl1]. simpl in H5; simpl in H4; assert (H0 : Rmin a b < Rmax a b). - unfold Rmin, Rmax; case (Rle_dec a b); intro; - [ assumption | elim n; left; assumption ]. + unfold Rmin, Rmax; case (Rle_dec a b) as [|[]]; + [ assumption | left; assumption ]. rewrite <- H5 in H0; rewrite <- H4 in H0; elim (Rlt_irrefl _ H0). clear Hrecl1; simpl; repeat apply le_n_S; apply le_O_n. elim (RList_P20 _ H18); intros r1 [r2 [r3 H19]]; rewrite H19; @@ -2222,9 +2189,9 @@ Proof. | left _ => Int_SF lf3 l3 | right _ => - Int_SF lf3 l3 end. - case (Rle_dec a b); case (Rle_dec b c); case (Rle_dec a c); intros. - elim r1; intro. - elim r0; intro. + case (Rle_dec a b) as [Hle|Hnle]; case (Rle_dec b c) as [Hle'|Hnle']; case (Rle_dec a c) as [Hle''|Hnle'']. + elim Hle; intro. + elim Hle'; intro. replace (Int_SF lf3 l3) with (Int_SF (FF (cons_Rlist l1 l2) f) (cons_Rlist l1 l2)). replace (Int_SF lf1 l1) with (Int_SF (FF l1 f) l1). @@ -2232,8 +2199,7 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H2; decompose [and] H1; decompose [and] H2; clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a b); case (Rle_dec b c); intros; reflexivity || elim n; - assumption. + decide (Rle_dec a b) with Hle; decide (Rle_dec b c) with Hle'; reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2; assumption @@ -2250,13 +2216,13 @@ Proof. rewrite Rplus_0_l; eapply StepFun_P17; [ apply H2 | rewrite H in H3; apply H3 ]. symmetry ; eapply StepFun_P8; [ apply H1 | assumption ]. - elim n; apply Rle_trans with b; assumption. + elim Hnle''; apply Rle_trans with b; assumption. apply Rplus_eq_reg_l with (Int_SF lf2 l2); replace (Int_SF lf2 l2 + (Int_SF lf1 l1 + - Int_SF lf2 l2)) with (Int_SF lf1 l1); [ idtac | ring ]. assert (H : c < b). auto with real. - elim r; intro. + elim Hle''; intro. rewrite Rplus_comm; replace (Int_SF lf1 l1) with (Int_SF (FF (cons_Rlist l3 l2) f) (cons_Rlist l3 l2)). @@ -2264,12 +2230,9 @@ Proof. replace (Int_SF lf2 l2) with (Int_SF (FF l2 f) l2). apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; - clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec b c); intros; - [ elim n; assumption - | reflexivity - | elim n0; assumption - | elim n1; assumption ]. + clear H3 H2; rewrite H10; rewrite H6; unfold Rmax, Rmin. + decide (Rle_dec a c) with Hle''; decide (Rle_dec b c) with Hnle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2284,7 +2247,7 @@ Proof. symmetry ; eapply StepFun_P8; [ apply H3 | assumption ]. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. - elim r; intro. + elim Hle; intro. replace (Int_SF lf2 l2) with (Int_SF (FF (cons_Rlist l3 l1) f) (cons_Rlist l3 l1)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2292,11 +2255,7 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H9; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec a b); intros; - [ elim n; assumption - | elim n1; assumption - | reflexivity - | elim n1; assumption ]. + decide (Rle_dec a c) with Hnle''; decide (Rle_dec a b) with Hle; reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. @@ -2316,7 +2275,7 @@ Proof. auto with real. replace (Int_SF lf2 l2) with (Int_SF lf3 l3 + Int_SF lf1 l1). ring. - rewrite Rplus_comm; elim r; intro. + rewrite Rplus_comm; elim Hle''; intro. replace (Int_SF lf2 l2) with (Int_SF (FF (cons_Rlist l1 l3) f) (cons_Rlist l1 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2324,11 +2283,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H1, H3; decompose [and] H1; decompose [and] H3; clear H3 H1; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec a b); intros; - [ elim n; assumption - | reflexivity - | elim n0; assumption - | elim n1; assumption ]. + decide (Rle_dec a c) with Hle''; decide (Rle_dec a b) with Hnle; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf1; apply H1 | assumption ]. @@ -2346,7 +2302,7 @@ Proof. auto with real. replace (Int_SF lf1 l1) with (Int_SF lf2 l2 + Int_SF lf3 l3). ring. - elim r; intro. + elim Hle'; intro. replace (Int_SF lf1 l1) with (Int_SF (FF (cons_Rlist l2 l3) f) (cons_Rlist l2 l3)). replace (Int_SF lf3 l3) with (Int_SF (FF l3 f) l3). @@ -2354,11 +2310,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H3; decompose [and] H2; decompose [and] H3; clear H3 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a c); case (Rle_dec b c); intros; - [ elim n; assumption - | elim n1; assumption - | reflexivity - | elim n1; assumption ]. + decide (Rle_dec a c) with Hnle''; decide (Rle_dec b c) with Hle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2371,8 +2324,8 @@ Proof. replace (Int_SF lf2 l2) with 0. rewrite Rplus_0_l; eapply StepFun_P17; [ apply H3 | rewrite H0 in H1; apply H1 ]. - symmetry ; eapply StepFun_P8; [ apply H2 | assumption ]. - elim n; apply Rle_trans with a; try assumption. + symmetry; eapply StepFun_P8; [ apply H2 | assumption ]. + elim Hnle'; apply Rle_trans with a; try assumption. auto with real. assert (H : c < b). auto with real. @@ -2387,11 +2340,8 @@ Proof. symmetry ; apply StepFun_P42. unfold adapted_couple in H2, H1; decompose [and] H2; decompose [and] H1; clear H1 H2; rewrite H11; rewrite H5; unfold Rmax, Rmin; - case (Rle_dec a b); case (Rle_dec b c); intros; - [ elim n1; assumption - | elim n1; assumption - | elim n0; assumption - | reflexivity ]. + decide (Rle_dec a b) with Hnle; decide (Rle_dec b c) with Hnle'; + reflexivity. eapply StepFun_P17; [ apply StepFun_P21; unfold is_subdivision; split with lf2; apply H2 | assumption ]. @@ -2463,10 +2413,8 @@ Proof. replace a with (Rmin a b). pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H7; reflexivity. + unfold Rmin; decide (Rle_dec a b) with H7; reflexivity. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. rewrite H2; assumption. @@ -2479,16 +2427,14 @@ Proof. split with (cons r (cons c nil)); split with (cons r3 nil); unfold adapted_couple in H; decompose [and] H; clear H; assert (H6 : r = a). - simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intro; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption ]. elim H0; clear H0; intros; unfold adapted_couple; repeat split. rewrite H6; unfold ordered_Rlist; intros; simpl in H8; inversion H8; [ simpl; assumption | elim (le_Sn_O _ H10) ]. - simpl; unfold Rmin; case (Rle_dec a c); intro; - [ assumption | elim n; assumption ]. - simpl; unfold Rmax; case (Rle_dec a c); intro; - [ reflexivity | elim n; assumption ]. + simpl; unfold Rmin; decide (Rle_dec a c) with H; assumption. + simpl; unfold Rmax; decide (Rle_dec a c) with H; reflexivity. unfold constant_D_eq, open_interval; intros; simpl in H8; inversion H8. simpl; assert (H10 := H7 0%nat); @@ -2508,8 +2454,8 @@ Proof. assert (H14 : a <= b). elim H0; intros; apply Rle_trans with c; assumption. assert (H16 : r = a). - simpl in H7; rewrite H7; unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + simpl in H7; rewrite H7; unfold Rmin; decide (Rle_dec a b) with H14; + reflexivity. induction l1' as [| r4 l1' Hrecl1']. simpl in H13; discriminate. clear Hrecl1'; unfold adapted_couple; repeat split. @@ -2517,18 +2463,18 @@ Proof. simpl; replace r4 with r1. apply (H5 0%nat). simpl; apply lt_O_Sn. - simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; - [ reflexivity | elim n; left; assumption ]. + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; + [ reflexivity | left; assumption ]. apply (H9 i); simpl; apply lt_S_n; assumption. - simpl; unfold Rmin; case (Rle_dec a c); intro; - [ assumption | elim n; elim H0; intros; assumption ]. + simpl; unfold Rmin; case (Rle_dec a c) as [|[]]; + [ assumption | elim H0; intros; assumption ]. replace (Rmax a c) with (Rmax r1 c). rewrite <- H11; reflexivity. - unfold Rmax; case (Rle_dec r1 c); case (Rle_dec a c); intros; - [ reflexivity - | elim n; elim H0; intros; assumption - | elim n; left; assumption - | elim n0; left; assumption ]. + unfold Rmax; case (Rle_dec a c) as [|[]]; case (Rle_dec r1 c) as [|[]]; + [ reflexivity + | left; assumption + | elim H0; intros; assumption + | left; assumption ]. simpl; simpl in H13; rewrite H13; reflexivity. intros; simpl in H; unfold constant_D_eq, open_interval; intros; induction i as [| i Hreci]. @@ -2539,8 +2485,8 @@ Proof. elim H4; clear H4; intros; split; try assumption; replace r1 with r4. assumption. - simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c); intro; - [ reflexivity | elim n; left; assumption ]. + simpl in H12; rewrite H12; unfold Rmin; case (Rle_dec r1 c) as [|[]]; + [ reflexivity | left; assumption ]. clear Hreci; simpl; apply H15. simpl; apply lt_S_n; assumption. unfold open_interval; apply H4. @@ -2578,10 +2524,8 @@ Proof. replace a with (Rmin a b). pattern b at 2; replace b with (Rmax a b). rewrite <- H2; rewrite H3; reflexivity. - unfold Rmax; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. - unfold Rmin; case (Rle_dec a b); intro; - [ reflexivity | elim n; assumption ]. + unfold Rmax; decide (Rle_dec a b) with H7; reflexivity. + unfold Rmin; decide (Rle_dec a b) with H7; reflexivity. split with (cons r nil); split with lf1; assert (H2 : c = b). rewrite H1 in H0; elim H0; intros; apply Rle_antisym; assumption. rewrite <- H2 in H1; rewrite <- H1; assumption. @@ -2597,15 +2541,15 @@ Proof. unfold ordered_Rlist; intros; simpl in H; induction i as [| i Hreci]. simpl; assumption. clear Hreci; apply (H2 (S i)); simpl; assumption. - simpl; unfold Rmin; case (Rle_dec c b); intro; - [ reflexivity | elim n; elim H0; intros; assumption ]. + simpl; unfold Rmin; case (Rle_dec c b) as [|[]]; + [ reflexivity | elim H0; intros; assumption ]. replace (Rmax c b) with (Rmax a b). rewrite <- H3; reflexivity. - unfold Rmax; case (Rle_dec a b); case (Rle_dec c b); intros; + unfold Rmax; case (Rle_dec c b) as [|[]]; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; assumption - | elim n; elim H0; intros; apply Rle_trans with c; assumption - | elim n0; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption + | elim H0; intros; assumption + | elim H0; intros; apply Rle_trans with c; assumption ]. simpl; simpl in H5; apply H5. intros; simpl in H; induction i as [| i Hreci]. unfold constant_D_eq, open_interval; intros; simpl; @@ -2615,9 +2559,9 @@ Proof. intros; split; try assumption; apply Rle_lt_trans with c; try assumption; replace r with a. elim H0; intros; assumption. - simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b); intros; + simpl in H4; rewrite H4; unfold Rmin; case (Rle_dec a b) as [|[]]; [ reflexivity - | elim n; elim H0; intros; apply Rle_trans with c; assumption ]. + | elim H0; intros; apply Rle_trans with c; assumption ]. clear Hreci; apply (H7 (S i)); simpl; assumption. cut (adapted_couple f r1 b (cons r1 r2) lf1). cut (r1 <= c <= b). diff --git a/theories/Reals/Rlimit.v b/theories/Reals/Rlimit.v index 3d52a98cd..375cc2752 100644 --- a/theories/Reals/Rlimit.v +++ b/theories/Reals/Rlimit.v @@ -347,11 +347,11 @@ Proof. unfold limit1_in; unfold limit_in; intros. simpl in *. cut (forall eps:R, eps > 0 -> dist R_met l l' < 2 * eps). - clear H0 H1; simpl @dist; unfold R_met; unfold R_dist, dist; - unfold Rabs; case (Rcase_abs (l - l')); intros. + clear H0 H1; unfold dist in |- *; unfold R_met; unfold R_dist in |- *; + unfold Rabs; case (Rcase_abs (l - l')) as [Hlt|Hge]; intros. cut (forall eps:R, eps > 0 -> - (l - l') < eps). intro; generalize (prop_eps (- (l - l')) H1); intro; - generalize (Ropp_gt_lt_0_contravar (l - l') r); intro; + generalize (Ropp_gt_lt_0_contravar (l - l') Hlt); intro; unfold Rgt in H3; generalize (Rgt_not_le (- (l - l')) 0 H3); intro; exfalso; auto. intros; cut (eps * / 2 > 0). @@ -375,7 +375,7 @@ Proof. intros a b; clear b; apply (Rminus_diag_uniq l l'); apply a; split. assumption. - apply (Rge_le (l - l') 0 r). + apply (Rge_le (l - l') 0 Hge). intros; cut (eps * / 2 > 0). intro; generalize (H0 (eps * / 2) H2); rewrite (Rmult_comm eps (/ 2)); rewrite <- (Rmult_assoc 2 (/ 2) eps); rewrite (Rinv_r 2). diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index 555bdcfab..2eb485188 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -43,7 +43,7 @@ Proof. rewrite Rmult_1_r; rewrite <- (Rmult_comm 3); rewrite <- Rmult_assoc; rewrite <- Rinv_l_sym. rewrite Rmult_1_l; replace (/ exp 1) with (exp (-1)). - unfold exp; case (exist_exp (-1)); intros; simpl; + unfold exp; case (exist_exp (-1)) as (?,e); simpl in |- *; unfold exp_in in e; assert (H := alternated_series_ineq (fun i:nat => / INR (fact i)) x 1). cut @@ -178,13 +178,13 @@ Qed. (**********) Lemma ln_exists : forall y:R, 0 < y -> { z:R | y = exp z }. Proof. - intros; case (Rle_dec 1 y); intro. - apply (ln_exists1 _ r). + intros; destruct (Rle_dec 1 y) as [Hle|Hnle]. + apply (ln_exists1 _ Hle). assert (H0 : 1 <= / y). apply Rmult_le_reg_l with y. apply H. rewrite <- Rinv_r_sym. - rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ n). + rewrite Rmult_1_r; left; apply (Rnot_le_lt _ _ Hnle). red; intro; rewrite H0 in H; elim (Rlt_irrefl _ H). destruct (ln_exists1 _ H0) as (x,p); exists (- x); apply Rmult_eq_reg_l with (exp x / y). @@ -213,12 +213,10 @@ Definition ln (x:R) : R := Lemma exp_ln : forall x:R, 0 < x -> exp (ln x) = x. Proof. - intros; unfold ln; case (Rlt_dec 0 x); intro. + intros; unfold ln; decide (Rlt_dec 0 x) with H. unfold Rln; - case (ln_exists (mkposreal x r) (cond_pos (mkposreal x r))); - intros. - simpl in e; symmetry ; apply e. - elim n; apply H. + case (ln_exists (mkposreal x H) (cond_pos (mkposreal x H))) as (?,Hex). + symmetry; apply Hex. Qed. Theorem exp_inv : forall x y:R, exp x = exp y -> x = y. @@ -610,7 +608,7 @@ Proof. replace h with (x + h - x); [ idtac | ring ]. apply H3; split. unfold D_x; split. - case (Rcase_abs h); intro. + destruct (Rcase_abs h) as [Hlt|Hgt]. assert (H7 : Rabs h < x / 2). apply Rlt_le_trans with alp. apply H6. @@ -623,9 +621,9 @@ Proof. replace (- h - x / 2 + x / 2) with (- h); [ idtac | ring ]. pattern x at 2; rewrite double_var. replace (- h - x / 2 + (x / 2 + x / 2 + h)) with (x / 2); [ apply H7 | ring ]. - apply r. - apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply r ]. - apply (not_eq_sym (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h; + apply Hlt. + apply Rplus_lt_le_0_compat; [ assumption | apply Rge_le; apply Hgt ]. + apply (sym_not_eq (A:=R)); apply Rminus_not_eq; replace (x + h - x) with h; [ apply H5 | ring ]. replace (x + h - x) with h; [ apply Rlt_le_trans with alp; diff --git a/theories/Reals/Rseries.v b/theories/Reals/Rseries.v index 328ba27e6..57b9d3d2f 100644 --- a/theories/Reals/Rseries.v +++ b/theories/Reals/Rseries.v @@ -237,9 +237,9 @@ Section sequence. apply le_n_Sn. rewrite (IHN H6), Rplus_0_l. unfold test. - destruct Rle_lt_dec. + destruct Rle_lt_dec as [Hle|Hlt]. apply eq_refl. - now elim Rlt_not_le with (1 := r). + now elim Rlt_not_le with (1 := Hlt). destruct (le_or_lt N n) as [Hn|Hn]. rewrite le_plus_minus with (1 := Hn). diff --git a/theories/Reals/Rsqrt_def.v b/theories/Reals/Rsqrt_def.v index 48ed16fd4..f9ad64b86 100644 --- a/theories/Reals/Rsqrt_def.v +++ b/theories/Reals/Rsqrt_def.v @@ -276,8 +276,7 @@ Proof. intros. unfold cv_infty. intro. - case (total_order_T 0 M); intro. - elim s; intro. + destruct (total_order_T 0 M) as [[Hlt|<-]|Hgt]. set (N := up M). cut (0 <= N)%Z. intro. @@ -302,7 +301,6 @@ Proof. assert (H0 := archimed M); elim H0; intros. left; apply Rlt_trans with M; assumption. exists 0%nat; intros. - rewrite <- b. unfold pow_2_n; apply pow_lt; prove_sup0. exists 0%nat; intros. apply Rlt_trans with 0. @@ -342,8 +340,7 @@ Proof. unfold Un_cv; unfold R_dist. intros. assert (H4 := cv_infty_cv_R0 pow_2_n pow_2_n_neq_R0 pow_2_n_infty). - case (total_order_T x y); intro. - elim s; intro. + destruct (total_order_T x y) as [[ Hlt | -> ]|Hgt]. unfold Un_cv in H4; unfold R_dist in H4. cut (0 < y - x). intro Hyp. @@ -376,16 +373,15 @@ Proof. apply Rplus_lt_reg_l with x; rewrite Rplus_0_r. replace (x + (y - x)) with y; [ assumption | ring ]. exists 0%nat; intros. - replace (dicho_lb x y P n - dicho_up x y P n - 0) with - (dicho_lb x y P n - dicho_up x y P n); [ idtac | ring ]. + replace (dicho_lb y y P n - dicho_up y y P n - 0) with + (dicho_lb y y P n - dicho_up y y P n); [ idtac | ring ]. rewrite <- Rabs_Ropp. rewrite Ropp_minus_distr'. rewrite dicho_lb_dicho_up. - rewrite b. unfold Rminus, Rdiv; rewrite Rplus_opp_r; rewrite Rmult_0_l; rewrite Rabs_R0; assumption. assumption. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H Hgt)). Qed. Definition cond_positivity (x:R) : bool := @@ -515,14 +511,14 @@ Proof. left; assumption. intro. unfold cond_positivity. - case (Rle_dec 0 z); intro. + case (Rle_dec 0 z) as [Hle|Hnle]. split. intro; assumption. intro; reflexivity. split. intro feqt;discriminate feqt. intro. - elim n0; assumption. + contradiction. unfold Vn. cut (forall z:R, cond_positivity z = false <-> z < 0). intros. @@ -536,20 +532,19 @@ Proof. assumption. intro. unfold cond_positivity. - case (Rle_dec 0 z); intro. + case (Rle_dec 0 z) as [Hle|Hnle]. split. intro feqt; discriminate feqt. - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H7)). + intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H7)). split. intro; auto with real. intro; reflexivity. cut (Un_cv Wn x0). intros. assert (H7 := continuity_seq f Wn x0 (H x0) H5). - case (total_order_T 0 (f x0)); intro. - elim s; intro. + destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. left; assumption. - rewrite <- b; right; reflexivity. + right; reflexivity. unfold Un_cv in H7; unfold R_dist in H7. cut (0 < - f x0). intro. @@ -570,10 +565,9 @@ Proof. cut (Un_cv Vn x0). intros. assert (H7 := continuity_seq f Vn x0 (H x0) H5). - case (total_order_T 0 (f x0)); intro. - elim s; intro. + destruct (total_order_T 0 (f x0)) as [[Hlt|<-]|Hgt]. unfold Un_cv in H7; unfold R_dist in H7. - elim (H7 (f x0) a); intros. + elim (H7 (f x0) Hlt); intros. cut (x2 >= x2)%nat; [ intro | unfold ge; apply le_n ]. assert (H10 := H8 x2 H9). rewrite Rabs_left in H10. @@ -592,7 +586,7 @@ Proof. [ unfold Rminus; apply Rplus_lt_le_0_compat | ring ]. assumption. apply Ropp_0_ge_le_contravar; apply Rle_ge; apply H6. - right; rewrite <- b; reflexivity. + right; reflexivity. left; assumption. unfold Vn; assumption. Qed. @@ -603,22 +597,15 @@ Lemma IVT_cor : x <= y -> f x * f y <= 0 -> { z:R | x <= z <= y /\ f z = 0 }. Proof. intros. - case (total_order_T 0 (f x)); intro. - case (total_order_T 0 (f y)); intro. - elim s; intro. - elim s0; intro. + destruct (total_order_T 0 (f x)) as [[Hltx|Heqx]|Hgtx]. + destruct (total_order_T 0 (f y)) as [[Hlty|Heqy]|Hgty]. cut (0 < f x * f y); [ intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H1 H2)) | apply Rmult_lt_0_compat; assumption ]. exists y. split. split; [ assumption | right; reflexivity ]. - symmetry ; exact b. - exists x. - split. - split; [ right; reflexivity | assumption ]. - symmetry ; exact b. - elim s; intro. + symmetry ; exact Heqy. cut (x < y). intro. assert (H3 := IVT (- f)%F x y (continuity_opp f H) H2). @@ -639,21 +626,20 @@ Proof. assumption. inversion H0. assumption. - rewrite H2 in a. - elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)). + rewrite H2 in Hltx. + elim (Rlt_irrefl _ (Rlt_trans _ _ _ Hgty Hltx)). exists x. split. split; [ right; reflexivity | assumption ]. symmetry ; assumption. - case (total_order_T 0 (f y)); intro. - elim s; intro. + destruct (total_order_T 0 (f y)) as [[Hlty|Heqy]|Hgty]. cut (x < y). intro. apply IVT; assumption. inversion H0. assumption. - rewrite H2 in r. - elim (Rlt_irrefl _ (Rlt_trans _ _ _ r a)). + rewrite H2 in Hgtx. + elim (Rlt_irrefl _ (Rlt_trans _ _ _ Hlty Hgtx)). exists y. split. split; [ assumption | right; reflexivity ]. @@ -676,8 +662,7 @@ Proof. intro. cut (continuity f). intro. - case (total_order_T y 1); intro. - elim s; intro. + destruct (total_order_T y 1) as [[Hlt| -> ]|Hgt]. cut (0 <= f 1). intro. cut (f 0 * f 1 <= 0). @@ -701,7 +686,7 @@ Proof. exists 1. split. left; apply Rlt_0_1. - rewrite b; symmetry ; apply Rsqr_1. + symmetry; apply Rsqr_1. cut (0 <= f y). intro. cut (f 0 * f y <= 0). @@ -723,7 +708,7 @@ Proof. pattern y at 1; rewrite <- Rmult_1_r. unfold Rsqr; apply Rmult_le_compat_l. assumption. - left; exact r. + left; exact Hgt. replace f with (Rsqr - fct_cte y)%F. apply continuity_minus. apply derivable_continuous; apply derivable_Rsqr. @@ -743,39 +728,31 @@ Definition Rsqrt (y:nonnegreal) : R := Lemma Rsqrt_positivity : forall x:nonnegreal, 0 <= Rsqrt x. Proof. intro. - assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)). - elim X; intros. + destruct (Rsqrt_exists (nonneg x) (cond_nonneg x)) as (x0 & H1 & H2). cut (x0 = Rsqrt x). intros. - elim p; intros. - rewrite H in H0; assumption. + rewrite <- H; assumption. unfold Rsqrt. - case (Rsqrt_exists x (cond_nonneg x)). - intros. - elim p; elim a; intros. + case (Rsqrt_exists x (cond_nonneg x)) as (?,[]). apply Rsqr_inj. assumption. assumption. - rewrite <- H0; rewrite <- H2; reflexivity. + rewrite <- H0, <- H2; reflexivity. Qed. (**********) Lemma Rsqrt_Rsqrt : forall x:nonnegreal, Rsqrt x * Rsqrt x = x. Proof. intros. - assert (X := Rsqrt_exists (nonneg x) (cond_nonneg x)). - elim X; intros. + destruct (Rsqrt_exists (nonneg x) (cond_nonneg x)) as (x0 & H1 & H2). cut (x0 = Rsqrt x). intros. rewrite <- H. - elim p; intros. - rewrite H1; reflexivity. + rewrite H2; reflexivity. unfold Rsqrt. - case (Rsqrt_exists x (cond_nonneg x)). - intros. - elim p; elim a; intros. + case (Rsqrt_exists x (cond_nonneg x)) as (x1 & ? & ?). apply Rsqr_inj. assumption. assumption. - rewrite <- H0; rewrite <- H2; reflexivity. + rewrite <- H0, <- H2; reflexivity. Qed. diff --git a/theories/Reals/Rtopology.v b/theories/Reals/Rtopology.v index 7e020dd41..991a52409 100644 --- a/theories/Reals/Rtopology.v +++ b/theories/Reals/Rtopology.v @@ -339,7 +339,7 @@ Proof. unfold neighbourhood in H4; elim H4; intros del H5. exists (pos del); split. apply (cond_pos del). - intros. unfold included in H5; apply H5; elim H6; intros; apply H8. + intros; unfold included in H5; apply H5; elim H6; intros; apply H8. unfold disc; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; apply H0. apply disc_P1. @@ -623,87 +623,79 @@ Qed. (** Borel-Lebesgue's lemma *) Lemma compact_P3 : forall a b:R, compact (fun c:R => a <= c <= b). Proof. - intros; case (Rle_dec a b); intro. - unfold compact; intros; + intros a b; destruct (Rle_dec a b) as [Hle|Hnle]. + unfold compact; intros f0 (H,H5); set (A := fun x:R => a <= x <= b /\ (exists D : R -> Prop, - covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))); - cut (A a). - intro; cut (bound A). - intro; cut (exists a0 : R, A a0). - intro; assert (H3 := completeness A H1 H2); elim H3; clear H3; intros m H3; - unfold is_lub in H3; cut (a <= m <= b). - intro; unfold covering_open_set in H; elim H; clear H; intros; - unfold covering in H; assert (H6 := H m H4); elim H6; - clear H6; intros y0 H6; unfold family_open_set in H5; - assert (H7 := H5 y0); unfold open_set in H7; assert (H8 := H7 m H6); - unfold neighbourhood in H8; elim H8; clear H8; intros eps H8; - cut (exists x : R, A x /\ m - eps < x <= m). - intro; elim H9; clear H9; intros x H9; elim H9; clear H9; intros; - case (Req_dec m b); intro. - rewrite H11 in H10; rewrite H11 in H8; unfold A in H9; elim H9; clear H9; - intros; elim H12; clear H12; intros Dx H12; - set (Db := fun x:R => Dx x \/ x = y0); exists Db; - unfold covering_finite; split. - unfold covering; unfold covering_finite in H12; elim H12; clear H12; - intros; unfold covering in H12; case (Rle_dec x0 x); - intro. - cut (a <= x0 <= x). - intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; - simpl in H16; simpl; unfold Db; elim H16; - clear H16; intros; split; [ apply H16 | left; apply H17 ]. - split. - elim H14; intros; assumption. - assumption. + covering_finite (fun c:R => a <= c <= x) (subfamily f0 D))). + cut (A a); [intro H0|]. + cut (bound A); [intro H1|]. + cut (exists a0 : R, A a0); [intro H2|]. + pose proof (completeness A H1 H2) as (m,H3); unfold is_lub in H3. + cut (a <= m <= b); [intro H4|]. + unfold covering in H; pose proof (H m H4) as (y0,H6). + unfold family_open_set in H5; pose proof (H5 y0 m H6) as (eps,H8). + cut (exists x : R, A x /\ m - eps < x <= m); + [intros (x,((H9 & Dx & H12 & H13),(Hltx,_)))|]. + destruct (Req_dec m b) as [->|H11]. + set (Db := fun x:R => Dx x \/ x = y0); exists Db; + unfold covering_finite; split. + unfold covering; intros x0 (H14,H18); + unfold covering in H12; destruct (Rle_dec x0 x) as [Hle'|Hnle']. + cut (a <= x0 <= x); [intro H15|]. + pose proof (H12 x0 H15) as (x1 & H16 & H17); exists x1; + simpl; unfold Db; split; [ apply H16 | left; apply H17 ]. + split; assumption. exists y0; simpl; split. - apply H8; unfold disc; rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; - rewrite Rabs_right. + apply H8; unfold disc; + rewrite <- Rabs_Ropp, Ropp_minus_distr, Rabs_right. apply Rlt_trans with (b - x). - unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; + unfold Rminus; apply Rplus_lt_compat_l, Ropp_lt_gt_contravar; auto with real. - elim H10; intros H15 _; apply Rplus_lt_reg_l with (x - eps); + apply Rplus_lt_reg_l with (x - eps); replace (x - eps + (b - x)) with (b - eps); - [ replace (x - eps + eps) with x; [ apply H15 | ring ] | ring ]. - apply Rge_minus; apply Rle_ge; elim H14; intros _ H15; apply H15. + [ replace (x - eps + eps) with x; [ apply Hltx | ring ] | ring ]. + apply Rge_minus, Rle_ge, H18. unfold Db; right; reflexivity. - unfold family_finite; unfold domain_finite; - unfold covering_finite in H12; elim H12; clear H12; + unfold family_finite, domain_finite. intros; unfold family_finite in H13; unfold domain_finite in H13; - elim H13; clear H13; intros l H13; exists (cons y0 l); + destruct H13 as (l,H13); exists (cons y0 l); intro; split. - intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); - clear H13; intros; case (Req_dec x0 y0); intro. + intro H14; simpl in H14; unfold intersection_domain in H14; + specialize H13 with x0; destruct H13 as (H13,H15); + destruct (Req_dec x0 y0) as [H16|H16]. simpl; left; apply H16. simpl; right; apply H13. simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. split; assumption. elim H16; assumption. - intro; simpl in H14; elim H14; intro; simpl; + intro H14; simpl in H14; destruct H14 as [H15|H15]; simpl; unfold intersection_domain. split. - apply (cond_fam f0); rewrite H15; exists m; apply H6. + apply (cond_fam f0); rewrite H15; exists b; apply H6. unfold Db; right; assumption. simpl; unfold intersection_domain; elim (H13 x0). intros _ H16; assert (H17 := H16 H15); simpl in H17; unfold intersection_domain in H17; split. elim H17; intros; assumption. unfold Db; left; elim H17; intros; assumption. - set (m' := Rmin (m + eps / 2) b); cut (A m'). - intro; elim H3; intros; unfold is_upper_bound in H13; - assert (H15 := H13 m' H12); cut (m < m'). - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H15 H16)). - unfold m'; unfold Rmin; case (Rle_dec (m + eps / 2) b); intro. - pattern m at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; - unfold Rdiv; apply Rmult_lt_0_compat; - [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. - elim H4; intros. - elim H17; intro. - assumption. - elim H11; assumption. + set (m' := Rmin (m + eps / 2) b). + cut (A m'); [intro H7|]. + destruct H3 as (H14,H15); unfold is_upper_bound in H14. + assert (H16 := H14 m' H7). + cut (m < m'); [intro H17|]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H16 H17))... + unfold m', Rmin; destruct (Rle_dec (m + eps / 2) b) as [Hle'|Hnle']. + pattern m at 1; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; + unfold Rdiv; apply Rmult_lt_0_compat; + [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. + destruct H4 as (_,[]). + assumption. + elim H11; assumption. unfold A; split. split. apply Rle_trans with m. @@ -712,32 +704,26 @@ Proof. pattern m at 1; rewrite <- Rplus_0_r; apply Rplus_le_compat_l; left; unfold Rdiv; apply Rmult_lt_0_compat; [ apply (cond_pos eps) | apply Rinv_0_lt_compat; prove_sup0 ]. - elim H4; intros. - elim H13; intro. + destruct H4. assumption. - elim H11; assumption. unfold m'; apply Rmin_r. - unfold A in H9; elim H9; clear H9; intros; elim H12; clear H12; intros Dx H12; - set (Db := fun x:R => Dx x \/ x = y0); exists Db; - unfold covering_finite; split. - unfold covering; unfold covering_finite in H12; elim H12; clear H12; - intros; unfold covering in H12; case (Rle_dec x0 x); - intro. - cut (a <= x0 <= x). - intro; assert (H16 := H12 x0 H15); elim H16; clear H16; intros; exists x1; - simpl in H16; simpl; unfold Db. - elim H16; clear H16; intros; split; [ apply H16 | left; apply H17 ]. - elim H14; intros; split; assumption. + set (Db := fun x:R => Dx x \/ x = y0); exists Db; + unfold covering_finite; split. + unfold covering; intros x0 (H14,H18); + unfold covering in H12; destruct (Rle_dec x0 x) as [Hle'|Hnle']. + cut (a <= x0 <= x); [intro H15|]. + pose proof (H12 x0 H15) as (x1 & H16 & H17); exists x1; + simpl; unfold Db; split; [ apply H16 | left; apply H17 ]. + split; assumption. exists y0; simpl; split. - apply H8; unfold disc; unfold Rabs; case (Rcase_abs (x0 - m)); - intro. + apply H8; unfold disc, Rabs; destruct (Rcase_abs (x0 - m)) as [Hlt|Hge]. rewrite Ropp_minus_distr; apply Rlt_trans with (m - x). unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_gt_contravar; auto with real. apply Rplus_lt_reg_l with (x - eps); replace (x - eps + (m - x)) with (m - eps). replace (x - eps + eps) with x. - elim H10; intros; assumption. + assumption. ring. ring. apply Rle_lt_trans with (m' - m). @@ -755,22 +741,20 @@ Proof. discrR. ring. unfold Db; right; reflexivity. - unfold family_finite; unfold domain_finite; - unfold covering_finite in H12; elim H12; clear H12; - intros; unfold family_finite in H13; unfold domain_finite in H13; - elim H13; clear H13; intros l H13; exists (cons y0 l); + unfold family_finite, domain_finite; + unfold family_finite, domain_finite in H13; + destruct H13 as (l,H13); exists (cons y0 l); intro; split. - intro; simpl in H14; unfold intersection_domain in H14; elim (H13 x0); - clear H13; intros; case (Req_dec x0 y0); intro. - simpl; left; apply H16. + intro H14; simpl in H14; unfold intersection_domain in H14; + specialize (H13 x0); destruct H13 as (H13,H15); + destruct (Req_dec x0 y0) as [Heq|Hneq]. + simpl; left; apply Heq. simpl; right; apply H13; simpl; unfold intersection_domain; unfold Db in H14; decompose [and or] H14. split; assumption. - elim H16; assumption. - intro; simpl in H14; elim H14; intro; simpl; - unfold intersection_domain. - split. + elim Hneq; assumption. + intros [H15|H15]. split. apply (cond_fam f0); rewrite H15; exists m; apply H6. unfold Db; right; assumption. elim (H13 x0); intros _ H16. @@ -780,22 +764,22 @@ Proof. split. elim H17; intros; assumption. unfold Db; left; elim H17; intros; assumption. - elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro. + elim (classic (exists x : R, A x /\ m - eps < x <= m)); intro H9. assumption. - elim H3; intros; cut (is_upper_bound A (m - eps)). - intro; assert (H13 := H11 _ H12); cut (m - eps < m). - intro; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)). + elim H3; intros H10 H11; cut (is_upper_bound A (m - eps)). + intro H12; assert (H13 := H11 _ H12); cut (m - eps < m). + intro H14; elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H13 H14)). pattern m at 2; rewrite <- Rplus_0_r; unfold Rminus; apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_involutive; rewrite Ropp_0; apply (cond_pos eps). set (P := fun n:R => A n /\ m - eps < n <= m); assert (H12 := not_ex_all_not _ P H9); unfold P in H12; - unfold is_upper_bound; intros; + unfold is_upper_bound; intros x H13; assert (H14 := not_and_or _ _ (H12 x)); elim H14; - intro. + intro H15. elim H15; apply H13. - elim (not_and_or _ _ H15); intro. - case (Rle_dec x (m - eps)); intro. + destruct (not_and_or _ _ H15) as [H16|H16]. + destruct (Rle_dec x (m - eps)) as [H17|H17]. assumption. elim H16; auto with real. unfold is_upper_bound in H10; assert (H17 := H10 x H13); elim H16; apply H17. @@ -803,7 +787,8 @@ Proof. unfold is_upper_bound in H3. split. apply (H3 _ H0). - apply (H4 b); unfold is_upper_bound; intros; unfold A in H5; elim H5; + clear H5. + apply (H4 b); unfold is_upper_bound; intros x H5; unfold A in H5; elim H5; clear H5; intros H5 _; elim H5; clear H5; intros _ H5; apply H5. exists a; apply H0. @@ -811,30 +796,28 @@ Proof. unfold A in H1; elim H1; clear H1; intros H1 _; elim H1; clear H1; intros _ H1; apply H1. unfold A; split. - split; [ right; reflexivity | apply r ]. - unfold covering_open_set in H; elim H; clear H; intros; unfold covering in H; - cut (a <= a <= b). - intro; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D'; + split; [ right; reflexivity | apply Hle ]. + unfold covering in H; cut (a <= a <= b). + intro H1; elim (H _ H1); intros y0 H2; set (D' := fun x:R => x = y0); exists D'; unfold covering_finite; split. - unfold covering; simpl; intros; cut (x = a). - intro; exists y0; split. + unfold covering; simpl; intros x H3; cut (x = a). + intro H4; exists y0; split. rewrite H4; apply H2. unfold D'; reflexivity. elim H3; intros; apply Rle_antisym; assumption. unfold family_finite; unfold domain_finite; exists (cons y0 nil); intro; split. - simpl; unfold intersection_domain; intro; elim H3; clear H3; - intros; unfold D' in H4; left; apply H4. - simpl; unfold intersection_domain; intro; elim H3; intro. + simpl; unfold intersection_domain; intros (H3,H4). + unfold D' in H4; left; apply H4. + simpl; unfold intersection_domain; intros [H4|[]]. split; [ rewrite H4; apply (cond_fam f0); exists a; apply H2 | apply H4 ]. - elim H4. - split; [ right; reflexivity | apply r ]. + split; [ right; reflexivity | apply Hle ]. apply compact_eqDom with (fun c:R => False). apply compact_EMP. unfold eq_Dom; split. unfold included; intros; elim H. unfold included; intros; elim H; clear H; intros; - assert (H1 := Rle_trans _ _ _ H H0); elim n; apply H1. + assert (H1 := Rle_trans _ _ _ H H0); elim Hnle; apply H1. Qed. Lemma compact_P4 : @@ -1017,14 +1000,14 @@ Proof. split. change (0 < a - x); apply Rlt_Rminus; assumption. intros; elim H5; clear H5; intros _ H5; unfold h. - case (Rle_dec x a); intro. - case (Rle_dec x0 a); intro. - unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - elim n; left; apply Rplus_lt_reg_l with (- x); + case (Rle_dec x a) as [|[]]. + case (Rle_dec x0 a) as [|[]]. + unfold Rminus; rewrite Rplus_opp_r, Rabs_R0; assumption. + left; apply Rplus_lt_reg_l with (- x); do 2 rewrite (Rplus_comm (- x)); apply Rle_lt_trans with (Rabs (x0 - x)). apply RRle_abs. assumption. - elim n; left; assumption. + left; assumption. elim H3; intro. assert (H5 : a <= a <= b). split; [ right; reflexivity | left; assumption ]. @@ -1039,19 +1022,19 @@ Proof. elim H8; intros; assumption. change (0 < b - a); apply Rlt_Rminus; assumption. intros; elim H9; clear H9; intros _ H9; cut (x1 < b). - intro; unfold h; case (Rle_dec x a); intro. - case (Rle_dec x1 a); intro. + intro; unfold h; case (Rle_dec x a) as [|[]]. + case (Rle_dec x1 a) as [Hlta|Hnlea]. unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - case (Rle_dec x1 b); intro. + case (Rle_dec x1 b) as [Hleb|[]]. elim H8; intros; apply H12; split. unfold D_x, no_cond; split. trivial. - red; intro; elim n; right; symmetry ; assumption. + red; intro; elim Hnlea; right; symmetry ; assumption. apply Rlt_le_trans with (Rmin x0 (b - a)). rewrite H4 in H9; apply H9. apply Rmin_l. - elim n0; left; assumption. - elim n; right; assumption. + left; assumption. + right; assumption. apply Rplus_lt_reg_l with (- a); do 2 rewrite (Rplus_comm (- a)); rewrite H4 in H9; apply Rle_lt_trans with (Rabs (x1 - a)). apply RRle_abs. @@ -1073,28 +1056,27 @@ Proof. assert (H12 : 0 < b - x). apply Rlt_Rminus; assumption. exists (Rmin x0 (Rmin (x - a) (b - x))); split. - unfold Rmin; case (Rle_dec (x - a) (b - x)); intro. - case (Rle_dec x0 (x - a)); intro. + unfold Rmin; case (Rle_dec (x - a) (b - x)) as [Hle|Hnle]. + case (Rle_dec x0 (x - a)) as [Hlea|Hnlea]. assumption. assumption. - case (Rle_dec x0 (b - x)); intro. + case (Rle_dec x0 (b - x)) as [Hleb|Hnleb]. assumption. assumption. - intros; elim H13; clear H13; intros; cut (a < x1 < b). - intro; elim H15; clear H15; intros; unfold h; case (Rle_dec x a); - intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). - case (Rle_dec x b); intro. - case (Rle_dec x1 a); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r0 H15)). - case (Rle_dec x1 b); intro. + intros x1 (H13,H14); cut (a < x1 < b). + intro; elim H15; clear H15; intros; unfold h; case (Rle_dec x a) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H4)). + case (Rle_dec x b) as [|[]]. + case (Rle_dec x1 a) as [Hle0|]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle0 H15)). + case (Rle_dec x1 b) as [|[]]. apply H10; split. assumption. apply Rlt_le_trans with (Rmin x0 (Rmin (x - a) (b - x))). assumption. apply Rmin_l. - elim n1; left; assumption. - elim n0; left; assumption. + left; assumption. + left; assumption. split. apply Ropp_lt_cancel; apply Rplus_lt_reg_l with x; apply Rle_lt_trans with (Rabs (x1 - x)). @@ -1124,13 +1106,13 @@ Proof. elim H10; intros; assumption. change (0 < b - a); apply Rlt_Rminus; assumption. intros; elim H11; clear H11; intros _ H11; cut (a < x1). - intro; unfold h; case (Rle_dec x a); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). - case (Rle_dec x1 a); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H12)). - case (Rle_dec x b); intro. - case (Rle_dec x1 b); intro. - rewrite H6; elim H10; intros; elim r0; intro. + intro; unfold h; case (Rle_dec x a) as [Hlea|Hnlea]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlea H4)). + case (Rle_dec x1 a) as [Hlea'|Hnlea']. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hlea' H12)). + case (Rle_dec x b) as [Hleb|Hnleb]. + case (Rle_dec x1 b) as [Hleb'|Hnleb']. + rewrite H6; elim H10; intros; destruct Hleb'. apply H14; split. unfold D_x, no_cond; split. trivial. @@ -1142,7 +1124,7 @@ Proof. assumption. rewrite H6; unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - elim n1; right; assumption. + elim Hnleb; right; assumption. rewrite H6 in H11; apply Ropp_lt_cancel; apply Rplus_lt_reg_l with b; apply Rle_lt_trans with (Rabs (x1 - b)). rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. @@ -1160,22 +1142,21 @@ Proof. apply Rle_lt_trans with (Rabs (x0 - x)). rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; apply RRle_abs. assumption. - unfold h; case (Rle_dec x a); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H4)). - case (Rle_dec x b); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H6)). - case (Rle_dec x0 a); intro. - elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 r))). - case (Rle_dec x0 b); intro. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ r H10)). + unfold h; case (Rle_dec x a) as [Hle|Hnle]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hle H4)). + case (Rle_dec x b) as [Hleb|Hnleb]. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hleb H6)). + case (Rle_dec x0 a) as [Hlea'|Hnlea']. + elim (Rlt_irrefl _ (Rlt_trans _ _ _ H1 (Rlt_le_trans _ _ _ H10 Hlea'))). + case (Rle_dec x0 b) as [Hleb'|Hnleb']. + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ Hleb' H10)). unfold Rminus; rewrite Rplus_opp_r; rewrite Rabs_R0; assumption. - intros; elim H3; intros; unfold h; case (Rle_dec c a); intro. - elim r; intro. + intros; elim H3; intros; unfold h; case (Rle_dec c a) as [[|]|]. elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H4 H6)). rewrite H6; reflexivity. - case (Rle_dec c b); intro. + case (Rle_dec c b) as [|[]]. reflexivity. - elim n0; assumption. + assumption. exists (fun _:R => f0 a); split. apply derivable_continuous; apply (derivable_const (f0 a)). intros; elim H2; intros; rewrite H1 in H3; cut (b = c). @@ -1229,8 +1210,8 @@ Proof. apply Rplus_lt_compat_l; apply Ropp_lt_cancel; rewrite Ropp_0; rewrite Ropp_involutive; apply (cond_pos eps). unfold is_upper_bound, image_dir; intros; cut (x <= M). - intro; case (Rle_dec x (M - eps)); intro. - apply r. + intro; destruct (Rle_dec x (M - eps)) as [H13|]. + apply H13. elim (H9 x); unfold intersection_domain, disc, image_dir; split. rewrite <- Rabs_Ropp; rewrite Ropp_minus_distr; rewrite Rabs_right. apply Rplus_lt_reg_l with (x - eps); @@ -1615,13 +1596,12 @@ Proof. apply H3. elim Hyp; intros; elim H4; intros; decompose [and] H5; assert (H10 := H3 _ H6); assert (H11 := H3 _ H8); - elim H10; intros; elim H11; intros; case (total_order_T x x0); - intro. - elim s; intro. + elim H10; intros; elim H11; intros; + destruct (total_order_T x x0) as [[|H15]|H15]. assumption. - rewrite b in H13; rewrite b in H7; elim H9; apply Rle_antisym; + rewrite H15 in H13, H7; elim H9; apply Rle_antisym; apply Rle_trans with x0; assumption. - elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H13 H14) r)). + elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ (Rle_trans _ _ _ H13 H14) H15)). elim X_enc; clear X_enc; intros m X_enc; elim X_enc; clear X_enc; intros M X_enc; elim X_enc; clear X_enc Hyp; intros X_enc Hyp; unfold uniform_continuity; intro; diff --git a/theories/Reals/Rtrigo.v b/theories/Reals/Rtrigo.v index f9cbb6e9d..c9704db3b 100644 --- a/theories/Reals/Rtrigo.v +++ b/theories/Reals/Rtrigo.v @@ -22,4 +22,4 @@ Require Import Rsqrt_def. Require Import PSeries_reg. Require Export Rtrigo1. Require Export Ratan. -Require Export Machin.
\ No newline at end of file +Require Export Machin. diff --git a/theories/Reals/Rtrigo1.v b/theories/Reals/Rtrigo1.v index 0e8beaad3..e42610424 100644 --- a/theories/Reals/Rtrigo1.v +++ b/theories/Reals/Rtrigo1.v @@ -147,11 +147,11 @@ Proof. apply H4. intros; rewrite (H0 x); rewrite (H0 x1); apply H5; apply H6. intro; unfold cos, SFL in |- *. - case (cv x); case (exist_cos (Rsqr x)); intros. - symmetry in |- *; eapply UL_sequence. - apply u. - unfold cos_in in c; unfold infinite_sum in c; unfold Un_cv in |- *; intros. - elim (c _ H0); intros N0 H1. + case (cv x) as (x1,HUn); case (exist_cos (Rsqr x)) as (x0,Hcos); intros. + symmetry; eapply UL_sequence. + apply HUn. + unfold cos_in, infinite_sum in Hcos; unfold Un_cv in |- *; intros. + elim (Hcos _ H0); intros N0 H1. exists N0; intros. unfold R_dist in H1; unfold R_dist, SP in |- *. replace (sum_f_R0 (fun k:nat => fn k x) n) with @@ -585,8 +585,8 @@ Qed. Lemma SIN_bound : forall x:R, -1 <= sin x <= 1. Proof. - intro; case (Rle_dec (-1) (sin x)); intro. - case (Rle_dec (sin x) 1); intro. + intro; destruct (Rle_dec (-1) (sin x)) as [Hle|Hnle]. + destruct (Rle_dec (sin x) 1) as [Hle'|Hnle']. split; assumption. cut (1 < sin x). intro; diff --git a/theories/Reals/Rtrigo_alt.v b/theories/Reals/Rtrigo_alt.v index 23b8e847a..448901f28 100644 --- a/theories/Reals/Rtrigo_alt.v +++ b/theories/Reals/Rtrigo_alt.v @@ -134,13 +134,13 @@ Proof. apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption. apply le_n_Sn. ring. - assert (X := exist_sin (Rsqr a)); elim X; intros. - cut (x = sin a / a). - intro; rewrite H3 in p; unfold sin_in in p; unfold infinite_sum in p; - unfold R_dist in p; unfold Un_cv; unfold R_dist; + unfold sin. + destruct (exist_sin (Rsqr a)) as (x,p). + unfold sin_in, infinite_sum, R_dist in p; + unfold Un_cv, R_dist; intros. cut (0 < eps / Rabs a). - intro; elim (p _ H5); intros N H6. + intro H4; destruct (p _ H4) as (N,H6). exists N; intros. replace (sum_f_R0 (tg_alt Un) n0) with (a * (1 - sum_f_R0 (fun i:nat => sin_n i * Rsqr a ^ i) (S n0))). @@ -151,12 +151,12 @@ Proof. rewrite Rplus_opp_l; rewrite Rplus_0_r; apply Rmult_lt_reg_l with (/ Rabs a). apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. pattern (/ Rabs a) at 1; rewrite <- (Rabs_Rinv a Hyp_a). - rewrite <- Rabs_mult; rewrite Rmult_plus_distr_l; rewrite <- Rmult_assoc; - rewrite <- Rinv_l_sym; [ rewrite Rmult_1_l | assumption ]; - rewrite (Rmult_comm (/ a)); rewrite (Rmult_comm (/ Rabs a)); - rewrite <- Rabs_Ropp; rewrite Ropp_plus_distr; rewrite Ropp_involutive; - unfold Rminus, Rdiv in H6; apply H6; unfold ge; - apply le_trans with n0; [ exact H7 | apply le_n_Sn ]. + rewrite <- Rabs_mult, Rmult_plus_distr_l, <- 2!Rmult_assoc, <- Rinv_l_sym; + [ rewrite Rmult_1_l | assumption ]; + rewrite (Rmult_comm (/ Rabs a)), + <- Rabs_Ropp, Ropp_plus_distr, Ropp_involutive, Rmult_1_l. + unfold Rminus, Rdiv in H6. apply H6; unfold ge; + apply le_trans with n0; [ exact H5 | apply le_n_Sn ]. rewrite (decomp_sum (fun i:nat => sin_n i * Rsqr a ^ i) (S n0)). replace (sin_n 0) with 1. simpl; rewrite Rmult_1_r; unfold Rminus; @@ -176,13 +176,6 @@ Proof. unfold Rdiv; apply Rmult_lt_0_compat. assumption. apply Rinv_0_lt_compat; apply Rabs_pos_lt; assumption. - unfold sin; case (exist_sin (Rsqr a)). - intros; cut (x = x0). - intro; rewrite H3; unfold Rdiv. - symmetry ; apply Rinv_r_simpl_m; assumption. - unfold sin_in in p; unfold sin_in in s; eapply uniqueness_sum. - apply p. - apply s. intros; elim H2; intros. replace (sin a - a) with (- (a - sin a)); [ idtac | ring ]. split; apply Ropp_le_contravar; assumption. @@ -318,12 +311,10 @@ Proof. apply le_n_2n. apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_Sn. apply (fun m n p:nat => mult_le_compat_l p n m); apply le_n_S; assumption. - assert (X := exist_cos (Rsqr a0)); elim X; intros. - cut (x = cos a0). - intro; rewrite H4 in p; unfold cos_in in p; unfold infinite_sum in p; - unfold R_dist in p; unfold Un_cv; unfold R_dist; - intros. - elim (p _ H5); intros N H6. + unfold cos. destruct (exist_cos (Rsqr a0)) as (x,p). + unfold cos_in, infinite_sum, R_dist in p; + unfold Un_cv, R_dist; intros. + destruct (p _ H4) as (N,H6). exists N; intros. replace (sum_f_R0 (tg_alt Un) n1) with (1 - sum_f_R0 (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)). @@ -334,7 +325,7 @@ Proof. rewrite Ropp_plus_distr; rewrite Ropp_involutive; unfold Rminus in H6; apply H6. unfold ge; apply le_trans with n1. - exact H7. + exact H5. apply le_n_Sn. rewrite (decomp_sum (fun i:nat => cos_n i * Rsqr a0 ^ i) (S n1)). replace (cos_n 0) with 1. @@ -354,10 +345,6 @@ Proof. unfold cos_n; unfold Rdiv; simpl; rewrite Rinv_1; rewrite Rmult_1_r; reflexivity. apply lt_O_Sn. - unfold cos; case (exist_cos (Rsqr a0)); intros; unfold cos_in in p; - unfold cos_in in c; eapply uniqueness_sum. - apply p. - apply c. intros; elim H3; intros; replace (cos a0 - 1) with (- (1 - cos a0)); [ idtac | ring ]. split; apply Ropp_le_contravar; assumption. @@ -394,8 +381,7 @@ Proof. replace (2 * n0 + 1)%nat with (S (2 * n0)). apply lt_O_Sn. ring. - intros; case (total_order_T 0 a); intro. - elim s; intro. + intros; destruct (total_order_T 0 a) as [[Hlt|Heq]|Hgt]. apply H; [ left; assumption | assumption ]. apply H; [ right; assumption | assumption ]. cut (0 < - a). diff --git a/theories/Reals/Rtrigo_reg.v b/theories/Reals/Rtrigo_reg.v index fff4fec98..aafa3357e 100644 --- a/theories/Reals/Rtrigo_reg.v +++ b/theories/Reals/Rtrigo_reg.v @@ -176,14 +176,14 @@ Proof. intro; rewrite H9 in H8; rewrite H10 in H8. apply H8. unfold SFL, sin. - case (cv h); intros. - case (exist_sin (Rsqr h)); intros. + case (cv h) as (x,HUn). + case (exist_sin (Rsqr h)) as (x0,Hsin). unfold Rdiv; rewrite (Rinv_r_simpl_m h x0 H6). eapply UL_sequence. - apply u. - unfold sin_in in s; unfold sin_n, infinite_sum in s; + apply HUn. + unfold sin_in in Hsin; unfold sin_n, infinite_sum in Hsin; unfold SP, fn, Un_cv; intros. - elim (s _ H10); intros N0 H11. + elim (Hsin _ H10); intros N0 H11. exists N0; intros. unfold R_dist; unfold R_dist in H11. replace @@ -194,9 +194,9 @@ Proof. apply sum_eq; intros; apply Rmult_eq_compat_l; unfold Rsqr; rewrite pow_sqr; reflexivity. unfold SFL, sin. - case (cv 0); intros. + case (cv 0) as (?,HUn). eapply UL_sequence. - apply u. + apply HUn. unfold SP, fn; unfold Un_cv; intros; exists 1%nat; intros. unfold R_dist; replace diff --git a/theories/Reals/SeqProp.v b/theories/Reals/SeqProp.v index 7f3282a35..d8f1cc6aa 100644 --- a/theories/Reals/SeqProp.v +++ b/theories/Reals/SeqProp.v @@ -461,8 +461,7 @@ Lemma cond_eq : forall x y:R, (forall eps:R, 0 < eps -> Rabs (x - y) < eps) -> x = y. Proof. intros. - case (total_order_T x y); intro. - elim s; intro. + destruct (total_order_T x y) as [[Hlt|Heq]|Hgt]. cut (0 < y - x). intro. assert (H1 := H (y - x) H0). @@ -897,8 +896,7 @@ Lemma growing_ineq : forall (Un:nat -> R) (l:R), Un_growing Un -> Un_cv Un l -> forall n:nat, Un n <= l. Proof. - intros; case (total_order_T (Un n) l); intro. - elim s; intro. + intros; destruct (total_order_T (Un n) l) as [[Hlt|Heq]|Hgt]. left; assumption. right; assumption. cut (0 < Un n - l). @@ -1103,11 +1101,11 @@ Proof. apply (cv_infty_cv_R0 (fun n:nat => INR (S n))). intro; apply not_O_INR; discriminate. assumption. - unfold cv_infty; intro; case (total_order_T M0 0); intro. - elim s; intro. + unfold cv_infty; intro; + destruct (total_order_T M0 0) as [[Hlt|Heq]|Hgt]. exists 0%nat; intros. apply Rlt_trans with 0; [ assumption | apply lt_INR_0; apply lt_O_Sn ]. - exists 0%nat; intros; rewrite b; apply lt_INR_0; apply lt_O_Sn. + exists 0%nat; intros; rewrite Heq; apply lt_INR_0; apply lt_O_Sn. set (M0_z := up M0). assert (H10 := archimed M0). cut (0 <= M0_z)%Z. diff --git a/theories/Reals/SeqSeries.v b/theories/Reals/SeqSeries.v index 6ff3fa8b8..462a94db1 100644 --- a/theories/Reals/SeqSeries.v +++ b/theories/Reals/SeqSeries.v @@ -375,11 +375,11 @@ Proof with trivial. assert (H1 : forall n:nat, 0 < sum_f_R0 An n)... intro; apply tech1... assert (H2 : cv_infty (fun n:nat => sum_f_R0 An n))... - unfold cv_infty; intro; case (Rle_dec M 0); intro... + unfold cv_infty; intro; destruct (Rle_dec M 0) as [Hle|Hnle]... exists 0%nat; intros; apply Rle_lt_trans with 0... assert (H2 : 0 < M)... auto with real... - clear n; set (m := up M); elim (archimed M); intros; + clear Hnle; set (m := up M); elim (archimed M); intros; assert (H5 : (0 <= m)%Z)... apply le_IZR; unfold m; simpl; left; apply Rlt_trans with M... elim (IZN _ H5); intros; exists x; intros; unfold An; rewrite sum_cte; diff --git a/theories/Reals/SplitAbsolu.v b/theories/Reals/SplitAbsolu.v index d0de58b09..c5eec7012 100644 --- a/theories/Reals/SplitAbsolu.v +++ b/theories/Reals/SplitAbsolu.v @@ -11,7 +11,7 @@ Require Import Rbasic_fun. Ltac split_case_Rabs := match goal with | |- context [(Rcase_abs ?X1)] => - case (Rcase_abs X1); try split_case_Rabs + destruct (Rcase_abs X1) as [?Hlt|?Hge]; try split_case_Rabs end. diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v index 985faa21e..87c624182 100644 --- a/theories/Reals/Sqrt_reg.v +++ b/theories/Reals/Sqrt_reg.v @@ -18,8 +18,7 @@ Lemma sqrt_var_maj : Proof. intros; cut (0 <= 1 + h). intro; apply Rle_trans with (Rabs (sqrt (Rsqr (1 + h)) - 1)). - case (total_order_T h 0); intro. - elim s; intro. + destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. repeat rewrite Rabs_left. unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)). do 2 rewrite Ropp_plus_distr; rewrite Ropp_involutive; @@ -51,7 +50,7 @@ Proof. left; apply Rlt_0_1. pattern 1 at 2; rewrite <- Rplus_0_r; apply Rplus_lt_compat_l; assumption. - rewrite b; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right; + rewrite Heq; rewrite Rplus_0_r; rewrite Rsqr_1; rewrite sqrt_1; right; reflexivity. repeat rewrite Rabs_right. unfold Rminus; do 2 rewrite <- (Rplus_comm (-1)); @@ -86,16 +85,15 @@ Proof. rewrite sqrt_Rsqr. replace (1 + h - 1) with h; [ right; reflexivity | ring ]. apply H0. - case (total_order_T h 0); intro. - elim s; intro. - rewrite (Rabs_left h a) in H. + destruct (total_order_T h 0) as [[Hlt|Heq]|Hgt]. + rewrite (Rabs_left h Hlt) in H. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; exact H. - left; rewrite b; rewrite Rplus_0_r; apply Rlt_0_1. + left; rewrite Heq; rewrite Rplus_0_r; apply Rlt_0_1. left; apply Rplus_lt_0_compat. apply Rlt_0_1. - apply r. + apply Hgt. Qed. (** sqrt is continuous in 1 *) @@ -203,8 +201,8 @@ Proof. left; apply Rlt_0_1. left; apply H. elim H6; intros. - case (Rcase_abs (x0 - x)); intro. - rewrite (Rabs_left (x0 - x) r) in H8. + destruct (Rcase_abs (x0 - x)) as [Hlt|Hgt]. + rewrite (Rabs_left (x0 - x) Hlt) in H8. rewrite Rplus_comm. apply Rplus_le_reg_l with (- ((x0 - x) / x)). rewrite Rplus_0_r; rewrite <- Rplus_assoc; rewrite Rplus_opp_l; @@ -220,7 +218,7 @@ Proof. apply Rplus_le_le_0_compat. left; apply Rlt_0_1. unfold Rdiv; apply Rmult_le_pos. - apply Rge_le; exact r. + apply Rge_le; exact Hgt. left; apply Rinv_0_lt_compat; apply H. unfold Rdiv; apply Rmult_lt_0_compat. apply H1. @@ -273,8 +271,8 @@ Proof. apply Rplus_lt_le_0_compat. apply sqrt_lt_R0; apply H. apply sqrt_positivity; apply H10. - case (Rcase_abs h); intro. - rewrite (Rabs_left h r) in H9. + destruct (Rcase_abs h) as [Hlt|Hgt]. + rewrite (Rabs_left h Hlt) in H9. apply Rplus_le_reg_l with (- h). rewrite Rplus_0_r; rewrite Rplus_comm; rewrite Rplus_assoc; rewrite Rplus_opp_r; rewrite Rplus_0_r; left; apply Rlt_le_trans with alpha1. @@ -282,7 +280,7 @@ Proof. unfold alpha1; apply Rmin_r. apply Rplus_le_le_0_compat. left; assumption. - apply Rge_le; apply r. + apply Rge_le; apply Hgt. unfold alpha1; unfold Rmin; case (Rle_dec alpha x); intro. apply H5. apply H. @@ -341,17 +339,16 @@ Proof. rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0; rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5; rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5. - case (Rcase_abs x0); intro. - unfold sqrt; case (Rcase_abs x0); intro. + destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs. + unfold sqrt. rewrite Heqs. rewrite Rabs_R0; apply H2. - assert (H6 := Rge_le _ _ r0); elim (Rlt_irrefl _ (Rle_lt_trans _ _ _ H6 r)). rewrite Rabs_right. apply Rsqr_incrst_0. rewrite Rsqr_sqrt. - rewrite (Rabs_right x0 r) in H5; apply H5. - apply Rge_le; exact r. - apply sqrt_positivity; apply Rge_le; exact r. + rewrite (Rabs_right x0 Hgt) in H5; apply H5. + apply Rge_le; exact Hgt. + apply sqrt_positivity; apply Rge_le; exact Hgt. left; exact H2. - apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact r. + apply Rle_ge; apply sqrt_positivity; apply Rge_le; exact Hgt. elim (Rlt_irrefl _ (Rlt_le_trans _ _ _ H1 H)). Qed. |