From 1cfbf3408b8d7d452233b31fbdc2e0b98821c213 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 13 Jul 2005 23:43:54 +0000
Subject: Détection d'un Fold incorrect suite à correction bug #986
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7223 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories7/Reals/PartSum.v    | 3 +--
 theories7/Reals/RiemannInt.v | 8 ++++----
 2 files changed, 5 insertions(+), 6 deletions(-)

(limited to 'theories7')

diff --git a/theories7/Reals/PartSum.v b/theories7/Reals/PartSum.v
index 4dab36368..f9d4f561e 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<l1-l``.
 Intro; Elim (H ? H2); Intros.
 Pose N0 := (max x N); Cut (ge N0 x).
diff --git a/theories7/Reals/RiemannInt.v b/theories7/Reals/RiemannInt.v
index 13d66988e..9b7a66e2c 100644
--- a/theories7/Reals/RiemannInt.v
+++ b/theories7/Reals/RiemannInt.v
@@ -710,9 +710,9 @@ Apply r_Rmult_mult with ``2``; [Unfold Rdiv; Do 2 Rewrite -> (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)<e
 Intros; Replace (pos (RinvN n)) with ``(R_dist (mkposreal (/((INR n)+1)) (RinvN_pos n)) 0)``.
 Apply H; Assumption.
 Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Apply Rabsolu_right; Apply Rle_sym1; 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; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; Pose phi1 := (phi_sequence RinvN pr1 n); Fold phi1 in H8; Pose phi2 := (phi_sequence RinvN pr2 n); Fold phi2 in H3; Pose phi3 := (phi_sequence RinvN pr3 n); Fold phi2 in H1; Assert H10 : (IsStepFun phi3 a b).
+Exists N0; Intros; Elim (H1 n); Elim (H2 n); Elim (H3 n); Clear H1 H2 H3; Intros; Unfold R_dist; Unfold Rminus; Rewrite Ropp_O; Rewrite Rplus_Or; LetTac phi1 := (phi_sequence RinvN pr1 n) in H8 Goal; LetTac phi2 := (phi_sequence RinvN pr2 n) in H3 Goal; LetTac phi3 := (phi_sequence RinvN pr3 n) in H1 Goal; Assert H10 : (IsStepFun phi3 a b).
 Apply StepFun_P44 with c.
 Apply (pre phi3).
 Split; Assumption.
@@ -1171,7 +1171,7 @@ Apply Rle_compatibility; Apply StepFun_P37; Try Assumption.
 Intros; Simpl; Rewrite Rmult_1l; Apply Rle_trans with ``(Rabsolu ((f x)-(phi3 x)))+(Rabsolu ((f x)-(phi2 x)))``.
 Rewrite <- (Rabsolu_Ropp ``(f x)-(phi3 x)``); Rewrite Ropp_distr2; Replace ``(phi3 x)+ -1*(phi2 x)`` with ``((phi3 x)-(f x))+((f x)-(phi2 x))``; [Apply Rabsolu_triang | Ring].
 Apply Rplus_le.
-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.
-- 
cgit v1.2.3