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

7 files changed, 24 insertions, 31 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAdd.v b/theories/Numbers/Integer/Abstract/ZAdd.v
index f95dcc76f..647ab0ac0 100644
--- a/theories/Numbers/Integer/Abstract/ZAdd.v
+++ b/theories/Numbers/Integer/Abstract/ZAdd.v
@@ -34,7 +34,7 @@ Theorem add_opp_r : forall n m, n + (- m) == n - m.
 Proof.
 nzinduct m.
 now nzsimpl.
-intro m. rewrite opp_succ, sub_succ_r, add_pred_r; now rewrite pred_inj_wd.
+intro m. rewrite opp_succ, sub_succ_r, add_pred_r. now rewrite pred_inj_wd.
 Qed.
 
 Theorem sub_0_l : forall n, 0 - n == - n.
@@ -96,7 +96,7 @@ Theorem opp_involutive : forall n, - (- n) == n.
 Proof.
 nzinduct n.
 now nzsimpl.
-intro n. rewrite opp_succ, opp_pred; now rewrite succ_inj_wd.
+intro n. rewrite opp_succ, opp_pred. now rewrite succ_inj_wd.
 Qed.
 
 Theorem opp_add_distr : forall n m, - (n + m) == - n + (- m).
@@ -120,7 +120,7 @@ Qed.
 
 Theorem opp_inj_wd : forall n m, - n == - m <-> n == m.
 Proof.
-intros n m; split; [apply opp_inj | apply opp_wd].
+intros n m; split; [apply opp_inj | intros; now f_equiv].
 Qed.
 
 Theorem eq_opp_l : forall n m, - n == m <-> n == - m.
diff --git a/theories/Numbers/Integer/Abstract/ZBase.v b/theories/Numbers/Integer/Abstract/ZBase.v
index 4afc10201..510548527 100644
--- a/theories/Numbers/Integer/Abstract/ZBase.v
+++ b/theories/Numbers/Integer/Abstract/ZBase.v
@@ -24,7 +24,7 @@ Qed.
 
 Theorem pred_inj_wd : forall n1 n2, P n1 == P n2 <-> n1 == n2.
 Proof.
-intros n1 n2; split; [apply pred_inj | apply pred_wd].
+intros n1 n2; split; [apply pred_inj | intros; now f_equiv].
 Qed.
 
 Lemma succ_m1 : S (-1) == 0.
diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index 641375a5c..de6619598 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -166,14 +166,14 @@ Proof.
  apply lt_succ_r. rewrite sub_1_r, succ_pred. now apply lt_0_sub.
  apply le_succ_l. rewrite sub_1_r, succ_pred. apply le_sub_le_add_r.
  rewrite <- (add_0_r (2^n)) at 1. now apply add_le_mono_l.
- rewrite <- add_sub_swap, sub_1_r. apply pred_wd.
+ rewrite <- add_sub_swap, sub_1_r. f_equiv.
  apply opp_inj. rewrite opp_add_distr, opp_sub_distr.
  rewrite (add_comm _ l), <- add_assoc.
  rewrite EQ at 1. apply add_cancel_l.
  rewrite <- opp_add_distr.
  rewrite <- (mul_1_l (2^n)) at 2. rewrite <- mul_add_distr_r.
  rewrite <- mul_opp_l.
- apply mul_wd; try reflexivity.
+ f_equiv.
  rewrite !opp_add_distr.
  rewrite <- mul_opp_r.
  rewrite opp_sub_distr, opp_involutive.
@@ -471,8 +471,8 @@ Proof.
    intros m. now rewrite <- H, bits_0.
   clear n Hn. intros n Hn IH a b (Ha,Ha') H.
   rewrite (div_mod a 2), (div_mod b 2) by order'.
-  apply add_wd; [ | now rewrite <- 2 bit0_mod, H].
-  apply mul_wd. reflexivity.
+  f_equiv; [ | now rewrite <- 2 bit0_mod, H].
+  f_equiv.
   apply IH.
   split. apply div_pos; order'.
   apply div_lt_upper_bound. order'. now rewrite <- pow_succ_r.
@@ -543,7 +543,7 @@ Proof.
   exists 0. intros m Hm. rewrite bits_0, Hk by order.
   symmetry; rewrite <- H0. apply Hk; order.
   revert f Hf Hk. apply le_ind with (4:=LE).
-  (* compat : solve_predicat_wd fails here *)
+  (* compat : solve_proper fails here *)
   apply proper_sym_impl_iff. exact eq_sym.
   clear k LE. intros k k' Hk IH f Hf H. apply IH; trivial.
   now setoid_rewrite Hk.
@@ -967,14 +967,10 @@ Proof.
 Qed.
 
 Instance setbit_wd : Proper (eq==>eq==>eq) setbit.
-Proof.
- intros a a' Ha n n' Hn. unfold setbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold setbit. solve_proper. Qed.
 
 Instance clearbit_wd : Proper (eq==>eq==>eq) clearbit.
-Proof.
- intros a a' Ha n n' Hn. unfold clearbit. now rewrite Ha, Hn.
-Qed.
+Proof. unfold clearbit. solve_proper. Qed.
 
 Lemma pow2_bits_true : forall n, 0<=n -> (2^n).[n] = true.
 Proof.
@@ -1113,7 +1109,7 @@ Qed.
 Definition lnot a := P (-a).
 
 Instance lnot_wd : Proper (eq==>eq) lnot.
-Proof. intros a a' Ha; unfold lnot; now rewrite Ha. Qed.
+Proof. unfold lnot. solve_proper. Qed.
 
 Lemma lnot_spec : forall a n, 0<=n -> (lnot a).[n] = negb a.[n].
 Proof.
@@ -1251,14 +1247,14 @@ Qed.
 Definition ones n := P (1<<n).
 
 Instance ones_wd : Proper (eq==>eq) ones.
-Proof. intros a a' Ha; unfold ones; now rewrite Ha. Qed.
+Proof. unfold ones. solve_proper. Qed.
 
 Lemma ones_equiv : forall n, ones n == P (2^n).
 Proof.
  intros. unfold ones.
  destruct (le_gt_cases 0 n).
  now rewrite shiftl_mul_pow2, mul_1_l.
- apply pred_wd. rewrite pow_neg_r; trivial.
+ f_equiv. rewrite pow_neg_r; trivial.
  rewrite <- shiftr_opp_r. apply shiftr_eq_0_iff. right; split.
  order'. rewrite log2_1. now apply opp_pos_neg.
 Qed.
@@ -1658,7 +1654,7 @@ Proof.
  rewrite <- add3_bits_div2.
  rewrite (add_comm ((a/2)+_)).
  rewrite <- div_add by order'.
- apply div_wd; try easy.
+ f_equiv.
  rewrite <- !div2_div, mul_comm, mul_add_distr_l.
  rewrite (div2_odd a), <- bit0_odd at 1.
  rewrite (div2_odd b), <- bit0_odd at 1.
@@ -1727,7 +1723,7 @@ Proof.
  le_elim Hm.
  rewrite <- (succ_pred m), lt_succ_r in Hm.
  rewrite <- (succ_pred m), <- !div2_bits, <- 2 lxor_spec by trivial.
- apply testbit_wd; try easy.
+ f_equiv.
  rewrite add_b2z_double_div2, <- IH1. apply add_carry_div2.
  rewrite <- Hm.
  now rewrite add_b2z_double_bit0, add3_bit0, b2z_bit0.
diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v
index f381953fb..052d68ab6 100644
--- a/theories/Numbers/Integer/Abstract/ZLcm.v
+++ b/theories/Numbers/Integer/Abstract/ZLcm.v
@@ -149,7 +149,7 @@ Proof.
  apply mod_divide, div_exact in H; try order.
  rewrite <- H.
  rewrite <- gcd_mul_mono_l_nonneg; 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.
 
@@ -211,9 +211,7 @@ Qed.
 Definition lcm a b := abs (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.
@@ -270,7 +268,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.
@@ -423,7 +421,7 @@ Proof.
   nzsimpl. rewrite lcm_0_l. now nzsimpl.
  unfold lcm.
  rewrite gcd_mul_mono_l.
- rewrite !abs_mul, mul_assoc. apply mul_wd; try easy.
+ rewrite !abs_mul, mul_assoc. f_equiv.
  rewrite <- (abs_sgn p) at 1. rewrite <- mul_assoc.
  rewrite div_mul_cancel_l; trivial.
  rewrite divide_div_mul_exact; trivial. rewrite abs_mul.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 6d2fa41fc..c7795ab90 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -174,7 +174,7 @@ le_elim Hn; split; intros m H.
 destruct (lt_1_mul_l n m) as [|[|]]; order'.
 rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'.
 now left.
-intros; right; symmetry; now apply opp_wd.
+intros; right. now f_equiv.
 Qed.
 
 Theorem lt_mul_diag_l : forall n m, n < 0 -> (1 < m <-> n * m < n).
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 5c7e9eb14..b364ec3f0 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -28,7 +28,7 @@ Qed.
 Lemma even_opp : forall n, even (-n) = even n.
 Proof.
  assert (H : forall n, Even n -> Even (-n)).
-  intros n (m,H). exists (-m). rewrite mul_opp_r. now apply opp_wd.
+  intros n (m,H). exists (-m). rewrite mul_opp_r. now f_equiv.
  intros. rewrite eq_iff_eq_true, !even_spec.
  split. rewrite <- (opp_involutive n) at 2. apply H.
  apply H.
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 2b568dddc..dbcc1961e 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.