diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 22:42:23 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-05-15 22:42:23 +0000 |
commit | 49a7bb129b8a7f9d5a9175b7a340112c20e95d96 (patch) | |
tree | 6205fc798ab6b996d1188f7492721d3c0247722f /theories/Numbers/Integer | |
parent | 972a60b36778a5c6971aa3f9a72073fd19f02b84 (diff) |
In practice, the new setoid rewrite (and the "at" syntax) allows to avoid
using the ad-hoc qsetoid_rewrite. Could QRewrite.v be made completely obsolete ?
For the moment rewrite under fun and exists don't work.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10935 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer')
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZPlus.v | 8 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZTimes.v | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 3d21444ad..8ceecdbf2 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -342,7 +342,7 @@ Proof NZgt_wf. Theorem Zlt_pred_l : forall n : Z, P n < n. Proof. -intro n; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n); apply Zlt_succ_diag_r. +intro n; rewrite <- (Zsucc_pred n) at 2; apply Zlt_succ_diag_r. Qed. Theorem Zle_pred_l : forall n : Z, P n <= n. @@ -362,7 +362,7 @@ Qed. Theorem Zlt_pred_le : forall n m : Z, P n < m <-> n <= m. Proof. -intros n m; pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +intros n m; rewrite <- (Zsucc_pred n) at 2. symmetry; apply Zle_succ_l. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZPlus.v b/theories/Numbers/Integer/Abstract/ZPlus.v index cdafa1ca7..2520d62e1 100644 --- a/theories/Numbers/Integer/Abstract/ZPlus.v +++ b/theories/Numbers/Integer/Abstract/ZPlus.v @@ -75,7 +75,7 @@ Proof NZplus_cancel_r. Theorem Zplus_pred_l : forall n m : Z, P n + m == P (n + m). Proof. intros n m. -pattern n at 2. qsetoid_rewrite <- (Zsucc_pred n). +rewrite <- (Zsucc_pred n) at 2. rewrite Zplus_succ_l. now rewrite Zpred_succ. Qed. @@ -104,19 +104,19 @@ Qed. Theorem Zminus_pred_l : forall n m : Z, P n - m == P (n - m). Proof. -intros n m. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +intros n m. rewrite <- (Zsucc_pred n) at 2. rewrite Zminus_succ_l; now rewrite Zpred_succ. Qed. Theorem Zminus_pred_r : forall n m : Z, n - (P m) == S (n - m). Proof. -intros n m. pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m). +intros n m. rewrite <- (Zsucc_pred m) at 2. rewrite Zminus_succ_r; now rewrite Zsucc_pred. Qed. Theorem Zopp_pred : forall n : Z, - (P n) == S (- n). Proof. -intro n. pattern n at 2; qsetoid_rewrite <- (Zsucc_pred n). +intro n. rewrite <- (Zsucc_pred n) at 2. rewrite Zopp_succ. now rewrite Zsucc_pred. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZTimes.v b/theories/Numbers/Integer/Abstract/ZTimes.v index 7819dc085..2d7ff30f7 100644 --- a/theories/Numbers/Integer/Abstract/ZTimes.v +++ b/theories/Numbers/Integer/Abstract/ZTimes.v @@ -73,7 +73,7 @@ Proof NZneq_times_0. Theorem Ztimes_pred_r : forall n m : Z, n * (P m) == n * m - n. Proof. intros n m. -pattern m at 2; qsetoid_rewrite <- (Zsucc_pred m). +rewrite <- (Zsucc_pred m) at 2. now rewrite Ztimes_succ_r, <- Zplus_minus_assoc, Zminus_diag, Zplus_0_r. Qed. |