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

1 files changed, 4 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 8a1a4def6..321508f58 100644
--- a/theories/Numbers/Natural/Abstract/NLcm.v
+++ b/theories/Numbers/Natural/Abstract/NLcm.v
@@ -59,7 +59,7 @@ Proof.
  apply mod_divide, div_exact in H; try order.
  rewrite <- H.
  rewrite <- gcd_mul_mono_l; try order.
- apply gcd_wd; symmetry; apply div_exact; try order;
+ f_equiv; symmetry; apply div_exact; try order;
   apply mod_divide; trivial; try order.
 Qed.
 
@@ -95,9 +95,7 @@ Qed.
 Definition lcm a b := a*(b/gcd a b).
 
 Instance lcm_wd : Proper (eq==>eq==>eq) lcm.
-Proof.
- unfold lcm. intros x x' Hx y y' Hy. now rewrite Hx, Hy.
-Qed.
+Proof. unfold lcm. solve_proper. Qed.
 
 Lemma lcm_equiv1 : forall a b, gcd a b ~= 0 ->
   a * (b / gcd a b) == (a*b)/gcd a b.
@@ -154,7 +152,7 @@ Proof.
  exists b'.
  rewrite <- mul_assoc, Hb'.
  rewrite (proj2 (div_exact c g NEQ)).
- rewrite <- Ha', mul_assoc. apply mul_wd; try easy.
+ rewrite <- Ha', mul_assoc. f_equiv.
  apply div_exact; trivial.
  apply mod_divide; trivial.
  apply mod_divide; trivial. transitivity a; trivial.
@@ -264,7 +262,7 @@ Proof.
   nzsimpl. rewrite lcm_0_l. now nzsimpl.
  unfold lcm.
  rewrite gcd_mul_mono_l.
- rewrite mul_assoc. apply mul_wd; try easy.
+ rewrite mul_assoc. f_equiv.
  now rewrite div_mul_cancel_l.
 Qed.