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 | |
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')
-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 | ||||
-rw-r--r-- | theories/Numbers/NumPrelude.v | 7 |
4 files changed, 8 insertions, 13 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. diff --git a/theories/Numbers/NumPrelude.v b/theories/Numbers/NumPrelude.v index 2c221a88e..f2f6b9082 100644 --- a/theories/Numbers/NumPrelude.v +++ b/theories/Numbers/NumPrelude.v @@ -11,11 +11,6 @@ (*i $Id$ i*) Require Export Setoid. -(*Require Export Bool.*) -(* Standard library. Export, not Import, because if a file -importing the current file wants to use. e.g., -Theorem eq_true_or : forall b1 b2 : bool, b1 || b2 <-> b1 \/ b2, -then it needs to know about bool and have a notation ||. *) Require Export QRewrite. Set Implicit Arguments. @@ -183,7 +178,7 @@ let x2 := fresh "x" in let y2 := fresh "y" in let H2 := fresh "H" in intros x1 y1 H1 x2 y2 H2; - qsetoid_rewrite H1; + rewrite H1; qiff x2 y2 H2. (* The tactic solve_relation_wd is not very efficient because qsetoid_rewrite |