From 76adb57c72fccb4f3e416bd7f3927f4fff72178b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 1 Jun 2014 10:26:26 +0200 Subject: 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. --- theories/Reals/PartSum.v | 40 +++++++++++++++++++--------------------- 1 file changed, 19 insertions(+), 21 deletions(-) (limited to 'theories/Reals/PartSum.v') 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. -- cgit v1.2.3