diff options
| author | letouzey | 2011-01-04 16:53:58 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-04 16:53:58 +0000 |
| commit | fdda04b92b7347f252d41aa76693ec221a07fe47 (patch) | |
| tree | 73a4c02ac7dee04734d6ef72b322c33427e09293 /theories/Numbers/Integer/NatPairs | |
| parent | 8e2d90a6a9f4480026afd433fc997d9958f76a38 (diff) | |
f_equiv : a clone of f_equal that handles setoid equivalences
For example, if we know that [f] is a morphism for [E1==>E2==>E],
then the goal [E (f x y) (f x' y')] will be transformed by [f_equiv]
into the subgoals [E1 x x'] and [E2 y y'].
This way, we can remove most of the explicit use of the morphism
instances in Numbers (lemmas foo_wd for each operator foo).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13763 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Integer/NatPairs')
| -rw-r--r-- | theories/Numbers/Integer/NatPairs/ZNatPairs.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 2b568dddcf..dbcc1961e0 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -131,15 +131,14 @@ Qed. Instance sub_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.sub. Proof. -intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp. -apply add_wd, opp_wd; auto. +intros n1 m1 H1 n2 m2 H2. rewrite 2 sub_add_opp. now do 2 f_equiv. Qed. Lemma mul_comm : forall n m, n*m == m*n. Proof. intros (n1,n2) (m1,m2); compute. rewrite (add_comm (m1*n2)%N). -apply N.add_wd; apply N.add_wd; apply mul_comm. +do 2 f_equiv; apply mul_comm. Qed. Instance mul_wd : Proper (Z.eq ==> Z.eq ==> Z.eq) Z.mul. |