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

6 files changed, 13 insertions, 13 deletions

diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v
index fdec8ceb7..ee03e5f94 100644
--- a/theories/Numbers/NatInt/NZAddOrder.v
+++ b/theories/Numbers/NatInt/NZAddOrder.v
@@ -157,7 +157,7 @@ Proof.
  intros n m H. apply le_ind with (4:=H). solve_proper.
  exists 0; nzsimpl; split; order.
  clear m H. intros m H (p & EQ & LE). exists (S p).
-  split. nzsimpl. now apply succ_wd. now apply le_le_succ_r.
+  split. nzsimpl. now f_equiv. now apply le_le_succ_r.
 Qed.
 
 (** For the moment, it doesn't seem possible to relate
diff --git a/theories/Numbers/NatInt/NZBase.v b/theories/Numbers/NatInt/NZBase.v
index 7c7f43de0..56fad9347 100644
--- a/theories/Numbers/NatInt/NZBase.v
+++ b/theories/Numbers/NatInt/NZBase.v
@@ -48,7 +48,7 @@ Theorem succ_inj_wd : forall n1 n2, S n1 == S n2 <-> n1 == n2.
 Proof.
 intros; split.
 apply succ_inj.
-intros. now apply succ_wd.
+intros. now f_equiv.
 Qed.
 
 Theorem succ_inj_wd_neg : forall n m, S n ~= S m <-> n ~= m.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index 9c01ba8cd..176e557b8 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -85,7 +85,7 @@ intros n n' Hn. rewrite Hn; auto with *.
 reflexivity.
 split; intros (p & q & H).
 exists p; exists (Datatypes.S q). rewrite <- iter_alt; simpl.
- apply succ_wd; auto.
+ now f_equiv.
 exists (Datatypes.S p); exists q. rewrite iter_alt; auto.
 Qed.
 
@@ -373,14 +373,14 @@ Lemma ofnat_add_l : forall n m, [n]+m == (S^n) m.
 Proof.
  induction n; intros.
  apply add_0_l.
- rewrite ofnat_succ, add_succ_l. simpl; apply succ_wd; auto.
+ rewrite ofnat_succ, add_succ_l. simpl. now f_equiv.
 Qed.
 
 Lemma ofnat_add : forall n m, [n+m] == [n]+[m].
 Proof.
  intros. rewrite ofnat_add_l.
  induction n; simpl. reflexivity.
- rewrite ofnat_succ. now apply succ_wd.
+ rewrite ofnat_succ. now f_equiv.
 Qed.
 
 Lemma ofnat_mul : forall n m, [n*m] == [n]*[m].
@@ -389,14 +389,14 @@ Proof.
  symmetry. apply mul_0_l.
  rewrite plus_comm.
  rewrite ofnat_succ, ofnat_add, mul_succ_l.
- now apply add_wd.
+ now f_equiv.
 Qed.
 
 Lemma ofnat_sub_r : forall n m, n-[m] == (P^m) n.
 Proof.
  induction m; simpl; intros.
  rewrite ofnat_zero. apply sub_0_r.
- rewrite ofnat_succ, sub_succ_r. now apply pred_wd.
+ rewrite ofnat_succ, sub_succ_r. now f_equiv.
 Qed.
 
 Lemma ofnat_sub : forall n m, m<=n -> [n-m] == [n]-[m].
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v
index 3cd78351d..7061dddcd 100644
--- a/theories/Numbers/NatInt/NZMulOrder.v
+++ b/theories/Numbers/NatInt/NZMulOrder.v
@@ -96,7 +96,7 @@ Qed.
 
 Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m).
 Proof.
-intros n m p Hp; split; intro H; [|now apply mul_wd].
+intros n m p Hp; split; intro H; [|now f_equiv].
 apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp];
  destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial.
 apply (mul_lt_mono_neg_l p) in LT; order.
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 4287319e4..29109ccb6 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -33,12 +33,12 @@ Proof. unfold Odd. solve_proper. Qed.
 
 Instance even_wd : Proper (eq==>Logic.eq) even.
 Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now apply Even_wd.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 even_spec. now f_equiv.
 Qed.
 
 Instance odd_wd : Proper (eq==>Logic.eq) odd.
 Proof.
- intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now apply Odd_wd.
+ intros x x' EQ. rewrite eq_iff_eq_true, 2 odd_spec. now f_equiv.
 Qed.
 
 (** Evenness and oddity are dual notions *)
@@ -141,7 +141,7 @@ Lemma Odd_succ : forall n, Odd (S n) <-> Even n.
 Proof.
  split; intros (m,H).
  exists m. apply succ_inj. now rewrite add_1_r in H.
- exists m. rewrite add_1_r. now apply succ_wd.
+ exists m. rewrite add_1_r. now f_equiv.
 Qed.
 
 Lemma odd_succ : forall n, odd (S n) = even n.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 8b6dcc3d6..6e85c6893 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -323,7 +323,7 @@ Proof.
  intros (b & Hb & H).
  rewrite H. rewrite sqrt_square; try order.
  symmetry.
- rewrite <- (lt_succ_pred 0 b Hb). apply succ_wd.
+ rewrite <- (lt_succ_pred 0 b Hb). f_equiv.
  rewrite <- (lt_succ_pred 0 b²) in H. apply succ_inj in H.
  now rewrite H, sqrt_pred_square.
  now apply mul_pos_pos.
@@ -450,7 +450,7 @@ Proof.
   by (apply le_lt_trans with (P b)²; trivial using square_nonneg).
  rewrite sqrt_up_eqn; trivial.
  assert (Hb' := lt_succ_pred 0 b Hb).
- rewrite <- Hb'. apply succ_wd. apply sqrt_unique.
+ rewrite <- Hb'. f_equiv. apply sqrt_unique.
  rewrite <- le_succ_l, <- lt_succ_r, Hb'.
  rewrite (lt_succ_pred 0 a Ha). now split.
 Qed.