diff options
author | 2012-07-05 16:56:37 +0000 | |
---|---|---|
committer | 2012-07-05 16:56:37 +0000 | |
commit | ffb64d16132dd80f72ecb619ef87e3eee1fa8bda (patch) | |
tree | 5368562b42af1aeef7e19b4bd897c9fc5655769b /theories/Reals/Rsigma.v | |
parent | a46ccd71539257bb55dcddd9ae8510856a5c9a16 (diff) |
Kills the useless tactic annotations "in |- *"
Most of these heavyweight annotations were introduced a long time ago
by the automatic 7.x -> 8.0 translator
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15518 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Reals/Rsigma.v')
-rw-r--r-- | theories/Reals/Rsigma.v | 30 |
1 files changed, 15 insertions, 15 deletions
diff --git a/theories/Reals/Rsigma.v b/theories/Reals/Rsigma.v index d26dcde21..9810c6117 100644 --- a/theories/Reals/Rsigma.v +++ b/theories/Reals/Rsigma.v @@ -28,8 +28,8 @@ Section Sigma. Proof. intros; induction k as [| k Hreck]. cut (low = 0%nat). - intro; rewrite H1; unfold sigma in |- *; rewrite <- minus_n_n; - rewrite <- minus_n_O; simpl in |- *; replace (high - 1)%nat with (pred high). + intro; rewrite H1; unfold sigma; rewrite <- minus_n_n; + rewrite <- minus_n_O; simpl; replace (high - 1)%nat with (pred high). apply (decomp_sum (fun k:nat => f k)). assumption. apply pred_of_minus. @@ -42,8 +42,8 @@ Section Sigma. apply Hreck. assumption. apply lt_trans with (S k); [ apply lt_n_Sn | assumption ]. - unfold sigma in |- *; replace (high - S (S k))%nat with (pred (high - S k)). - pattern (S k) at 3 in |- *; replace (S k) with (S k + 0)%nat; + unfold sigma; replace (high - S (S k))%nat with (pred (high - S k)). + pattern (S k) at 3; replace (S k) with (S k + 0)%nat; [ idtac | ring ]. replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with (sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))). @@ -55,12 +55,12 @@ Section Sigma. replace (high - S (S k))%nat with (high - S k - 1)%nat. apply pred_of_minus. omega. - unfold sigma in |- *; replace (S k - low)%nat with (S (k - low)). - pattern (S k) at 1 in |- *; replace (S k) with (low + S (k - low))%nat. - symmetry in |- *; apply (tech5 (fun i:nat => f (low + i))). + unfold sigma; replace (S k - low)%nat with (S (k - low)). + pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat. + symmetry ; apply (tech5 (fun i:nat => f (low + i))). omega. omega. - rewrite <- H2; unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *; + rewrite <- H2; unfold sigma; rewrite <- minus_n_n; simpl; replace (high - S low)%nat with (pred (high - low)). replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with (sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))). @@ -79,7 +79,7 @@ Section Sigma. (low <= k)%nat -> (k < high)%nat -> sigma low high - sigma low k = sigma (S k) high. Proof. - intros low high k H1 H2; symmetry in |- *; rewrite (sigma_split H1 H2); ring. + intros low high k H1 H2; symmetry ; rewrite (sigma_split H1 H2); ring. Qed. Theorem sigma_diff_neg : @@ -100,8 +100,8 @@ Section Sigma. apply sigma_split. apply le_n. assumption. - unfold sigma in |- *; rewrite <- minus_n_n. - simpl in |- *. + unfold sigma; rewrite <- minus_n_n. + simpl. replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed. @@ -113,20 +113,20 @@ Section Sigma. generalize (lt_le_weak low high H1); intro H3; replace (f high) with (sigma high high). rewrite Rplus_comm; cut (high = S (pred high)). - intro; pattern high at 3 in |- *; rewrite H. + intro; pattern high at 3; rewrite H. apply sigma_split. apply le_S_n; rewrite <- H; apply lt_le_S; assumption. apply lt_pred_n_n; apply le_lt_trans with low; [ apply le_O_n | assumption ]. apply S_pred with 0%nat; apply le_lt_trans with low; [ apply le_O_n | assumption ]. - unfold sigma in |- *; rewrite <- minus_n_n; simpl in |- *; + unfold sigma; rewrite <- minus_n_n; simpl; replace (high + 0)%nat with high; [ reflexivity | ring ]. Qed. Theorem sigma_eq_arg : forall low:nat, sigma low low = f low. Proof. - intro; unfold sigma in |- *; rewrite <- minus_n_n. - simpl in |- *; replace (low + 0)%nat with low; [ reflexivity | ring ]. + intro; unfold sigma; rewrite <- minus_n_n. + simpl; replace (low + 0)%nat with low; [ reflexivity | ring ]. Qed. End Sigma. |