From 1cfbf3408b8d7d452233b31fbdc2e0b98821c213 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 13 Jul 2005 23:43:54 +0000 Subject: Détection d'un Fold incorrect suite à correction bug #986 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Reals/RiemannInt.v | 14 +++++++------- theories7/Reals/PartSum.v | 3 +-- theories7/Reals/RiemannInt.v | 8 ++++---- 3 files changed, 12 insertions(+), 13 deletions(-) diff --git a/theories/Reals/RiemannInt.v b/theories/Reals/RiemannInt.v index fe0ed965e9..812f104817 100644 --- a/theories/Reals/RiemannInt.v +++ b/theories/Reals/RiemannInt.v @@ -1593,13 +1593,12 @@ Lemma RiemannInt_P17 : intro f; intros; unfold RiemannInt in |- *; case (RiemannInt_exists pr1 RinvN RinvN_cv); case (RiemannInt_exists pr2 RinvN RinvN_cv); intros; - set (phi1 := phi_sequence RinvN pr1); + set (phi1 := phi_sequence RinvN pr1) in u0; set (phi2 := fun N:nat => mkStepFun (StepFun_P32 (phi1 N))); apply Rle_cv_lim with (fun N:nat => Rabs (RiemannInt_SF (phi1 N))) (fun N:nat => RiemannInt_SF (phi2 N)). intro; unfold phi2 in |- *; apply StepFun_P34; assumption. -fold phi1 in u0; apply (continuity_seq Rabs (fun N:nat => RiemannInt_SF (phi1 N)) x0); try assumption. apply Rcontinuity_abs. @@ -2372,10 +2371,11 @@ unfold R_dist in |- *; unfold Rminus in |- *; rewrite Ropp_0; left; apply (cond_pos (RinvN n)). exists N0; intros; elim (H1 n); elim (H2 n); elim (H3 n); clear H1 H2 H3; intros; unfold R_dist in |- *; unfold Rminus in |- *; - rewrite Ropp_0; rewrite Rplus_0_r; set (phi1 := phi_sequence RinvN pr1 n); - fold phi1 in H8; set (phi2 := phi_sequence RinvN pr2 n); - fold phi2 in H3; set (phi3 := phi_sequence RinvN pr3 n); - fold phi2 in H1; assert (H10 : IsStepFun phi3 a b). + rewrite Ropp_0; rewrite Rplus_0_r; + set (phi1 := phi_sequence RinvN pr1 n) in H8 |- *; + set (phi2 := phi_sequence RinvN pr2 n) in H3 |- *; + set (phi3 := phi_sequence RinvN pr3 n) in H1 |- *; + assert (H10 : IsStepFun phi3 a b). apply StepFun_P44 with c. apply (pre phi3). split; assumption. @@ -2442,7 +2442,7 @@ rewrite <- (Rabs_Ropp (f x - phi3 x)); rewrite Ropp_minus_distr; replace (phi3 x + -1 * phi2 x) with (phi3 x - f x + (f x - phi2 x)); [ apply Rabs_triang | ring ]. apply Rplus_le_compat. -fold phi3 in H1; apply H1. +apply H1. elim H14; intros; split. replace (Rmin a c) with a. apply Rle_trans with b; try assumption. diff --git a/theories7/Reals/PartSum.v b/theories7/Reals/PartSum.v index 4dab36368e..f9d4f561ec 100644 --- a/theories7/Reals/PartSum.v +++ b/theories7/Reals/PartSum.v @@ -385,8 +385,7 @@ Elim s; Intro. Left; Apply a. Right; Apply b. Cut (Un_growing [n:nat](sum_f_R0 An n)). -Intro; Pose l1 := (sum_f_R0 An N). -Fold l1 in r. +Intro; LetTac l1 := (sum_f_R0 An N) in r. Unfold Un_cv in H; Cut ``0 (Rmult_sym ``2``); Qed. Lemma RiemannInt_P17 : (f:R->R;a,b:R;pr1:(Riemann_integrable f a b);pr2:(Riemann_integrable [x:R](Rabsolu (f x)) a b)) ``a<=b`` -> ``(Rabsolu (RiemannInt pr1))<=(RiemannInt pr2)``. -Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; Pose phi1 := (phi_sequence RinvN pr1); Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)). +Intro f; Intros; Unfold RiemannInt; Case (RiemannInt_exists 1!f 2!a 3!b pr1 5!RinvN RinvN_cv); Case (RiemannInt_exists 1!([x0:R](Rabsolu (f x0))) 2!a 3!b pr2 5!RinvN RinvN_cv); Intros; LetTac phi1 := (phi_sequence RinvN pr1) in u0; Pose phi2 := [N:nat](mkStepFun (StepFun_P32 (phi1 N))); Apply Rle_cv_lim with [N:nat](Rabsolu (RiemannInt_SF (phi1 N))) [N:nat](RiemannInt_SF (phi2 N)). Intro; Unfold phi2; Apply StepFun_P34; Assumption. -Fold phi1 in u0; Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption. +Apply (continuity_seq Rabsolu [N:nat](RiemannInt_SF (phi1 N)) x0); Try Assumption. Apply continuity_Rabsolu. Pose phi3 := (phi_sequence RinvN pr2); Assert H0 : (EXT psi3:nat->(StepFun a b) | (n:nat) ((t:R)``(Rmin a b) <= t``/\``t <= (Rmax a b)``->``(Rabsolu ((Rabsolu (f t))-((phi3 n) t)))<= (psi3 n t)``)/\``(Rabsolu (RiemannInt_SF (psi3 n))) < (RinvN n)``). Split with [n:nat](projT1 ? ? (phi_sequence_prop RinvN pr2 n)); Intro; Apply (projT2 ? ? (phi_sequence_prop RinvN pr2 n)). @@ -1139,7 +1139,7 @@ Elim (H ? H4); Clear H; Intros N0 H; Assert H5 : (n:nat)(ge n N0)->``(RinvN n)