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

5 files changed, 60 insertions, 138 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index 70f6f79451..f5b9005328 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -39,8 +39,7 @@ Proof.
  intros a b c Hb H.
  apply div_unique with 0.
  generalize (pow_nonzero b c Hb) (le_0_l (b^c)); order'.
- nzsimpl. rewrite <- pow_mul_l. apply pow_wd. now apply div_exact.
- reflexivity.
+ nzsimpl. rewrite <- pow_mul_l. f_equiv. now apply div_exact.
 Qed.
 
 (** An injection from bits [true] and [false] to numbers 1 and 0.
@@ -309,8 +308,8 @@ Proof.
  rewrite EQ in H |- *. symmetry. apply bits_inj_0.
  intros n. now rewrite <- H, bits_0.
  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; trivial using le_0_l.
  apply div_lt; order'.
  intro n. rewrite 2 div2_bits. apply H.
@@ -697,14 +696,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, (2^n).[n] = true.
 Proof.
@@ -853,10 +848,10 @@ Definition ones n := P (1 << n).
 Definition lnot a n := lxor a (ones 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.
 
 Instance lnot_wd : Proper (eq==>eq==>eq) lnot.
-Proof. intros a a' Ha n n' Hn; unfold lnot; now rewrite Ha, Hn. Qed.
+Proof. unfold lnot. solve_proper. Qed.
 
 Lemma ones_equiv : forall n, ones n == P (2^n).
 Proof.
@@ -1225,7 +1220,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. fold (b2n a.[0]).
  rewrite (div2_odd b), <- bit0_odd at 1. fold (b2n b.[0]).
@@ -1273,7 +1268,7 @@ Proof.
  destruct (zero_or_succ m) as [EQ|[m' EQ]]; rewrite EQ; clear EQ.
  now rewrite add_b2n_double_bit0, add3_bit0, b2n_bit0.
  rewrite <- !div2_bits, <- 2 lxor_spec.
- apply testbit_wd; try easy.
+ f_equiv.
  rewrite add_b2n_double_div2, <- IH1. apply add_carry_div2.
  (* - carry *)
  rewrite add_b2n_double_div2.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8df64756ac..8df715af9d 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -28,8 +28,8 @@ Implicit Arguments if_zero [A].
 Instance if_zero_wd (A : Type) :
  Proper (Logic.eq ==> Logic.eq ==> N.eq ==> Logic.eq) (@if_zero A).
 Proof.
-intros; unfold if_zero.
-repeat red; intros. apply recursion_wd; auto. repeat red; auto.
+unfold if_zero. (* TODO : solve_proper : SLOW + BUG *)
+f_equiv'.
 Qed.
 
 Theorem if_zero_0 : forall (A : Type) (a b : A), if_zero a b 0 = a.
@@ -51,17 +51,9 @@ Definition def_add (x y : N.t) := recursion y (fun _ => S) x.
 
 Local Infix "+++" := def_add (at level 50, left associativity).
 
-Instance def_add_prewd : Proper (N.eq==>N.eq==>N.eq) (fun _ => S).
-Proof.
-intros _ _ _ p p' Epp'; now rewrite Epp'.
-Qed.
-
 Instance def_add_wd : Proper (N.eq ==> N.eq ==> N.eq) def_add.
 Proof.
-intros x x' Exx' y y' Eyy'. unfold def_add.
-(* TODO: why rewrite Exx' don't work here (or verrrry slowly) ? *)
-apply recursion_wd with (Aeq := N.eq); auto with *.
-apply def_add_prewd.
+unfold def_add. f_equiv'.
 Qed.
 
 Theorem def_add_0_l : forall y, 0 +++ y == y.
@@ -72,7 +64,7 @@ Qed.
 Theorem def_add_succ_l : forall x y, S x +++ y == S (x +++ y).
 Proof.
 intros x y; unfold def_add.
-rewrite recursion_succ; auto with *.
+rewrite recursion_succ; f_equiv'.
 Qed.
 
 Theorem def_add_add : forall n m, n +++ m == n + m.
@@ -89,18 +81,10 @@ Definition def_mul (x y : N.t) := recursion 0 (fun _ p => p +++ x) y.
 
 Local Infix "**" := def_mul (at level 40, left associativity).
 
-Instance def_mul_prewd :
- Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun x _ p => p +++ x).
-Proof.
-repeat red; intros; now apply def_add_wd.
-Qed.
-
 Instance def_mul_wd : Proper (N.eq ==> N.eq ==> N.eq) def_mul.
 Proof.
-unfold def_mul.
-intros x x' Exx' y y' Eyy'.
-apply recursion_wd; auto with *.
-now apply def_mul_prewd.
+unfold def_mul. (* TODO : solve_proper SLOW + BUG *)
+f_equiv'.
 Qed.
 
 Theorem def_mul_0_r : forall x, x ** 0 == 0.
@@ -112,7 +96,7 @@ Theorem def_mul_succ_r : forall x y, x ** S y == x ** y +++ x.
 Proof.
 intros x y; unfold def_mul.
 rewrite recursion_succ; auto with *.
-now apply def_mul_prewd.
+f_equiv'.
 Qed.
 
 Theorem def_mul_mul : forall n m, n ** m == n * m.
@@ -133,25 +117,9 @@ recursion
 
 Local Infix "<<" := ltb (at level 70, no associativity).
 
-Instance ltb_prewd1 : Proper (N.eq==>Logic.eq) (if_zero false true).
-Proof.
-red; intros; apply if_zero_wd; auto.
-Qed.
-
-Instance ltb_prewd2 : Proper (N.eq==>(N.eq==>Logic.eq)==>N.eq==>Logic.eq)
- (fun _ f n => recursion false (fun n' _ => f n') n).
-Proof.
-repeat red; intros; simpl.
-apply recursion_wd; auto with *.
-repeat red; auto.
-Qed.
-
 Instance ltb_wd : Proper (N.eq ==> N.eq ==> Logic.eq) ltb.
 Proof.
-unfold ltb.
-intros n n' Hn m m' Hm.
-apply f_equiv; auto with *.
-apply recursion_wd; auto; [ apply ltb_prewd1 | apply ltb_prewd2 ].
+unfold ltb. f_equiv'.
 Qed.
 
 Theorem ltb_base : forall n, 0 << n = if_zero false true n.
@@ -163,11 +131,9 @@ Theorem ltb_step :
   forall m n, S m << n = recursion false (fun n' _ => m << n') n.
 Proof.
 intros m n; unfold ltb at 1.
-apply f_equiv; auto with *.
-rewrite recursion_succ by (apply ltb_prewd1||apply ltb_prewd2).
-fold (ltb m).
-repeat red; intros. apply recursion_wd; auto.
-repeat red; intros; now apply ltb_wd.
+f_equiv.
+rewrite recursion_succ; f_equiv'.
+reflexivity.
 Qed.
 
 (* Above, we rewrite applications of function. Is it possible to rewrite
@@ -189,8 +155,7 @@ Qed.
 Theorem succ_ltb_mono : forall n m, (S n << S m) = (n << m).
 Proof.
 intros n m.
-rewrite ltb_step. rewrite recursion_succ; try reflexivity.
-repeat red; intros; now apply ltb_wd.
+rewrite ltb_step. rewrite recursion_succ; f_equiv'.
 Qed.
 
 Theorem ltb_lt : forall n m, n << m = true <-> n < m.
@@ -215,9 +180,7 @@ Definition even (x : N.t) := recursion true (fun _ p => negb p) x.
 
 Instance even_wd : Proper (N.eq==>Logic.eq) even.
 Proof.
-intros n n' Hn. unfold even.
-apply recursion_wd; auto.
-congruence.
+unfold even. f_equiv'.
 Qed.
 
 Theorem even_0 : even 0 = true.
@@ -229,19 +192,12 @@ Qed.
 Theorem even_succ : forall x, even (S x) = negb (even x).
 Proof.
 unfold even.
-intro x; rewrite recursion_succ; try reflexivity.
-congruence.
+intro x; rewrite recursion_succ; f_equiv'.
 Qed.
 
 (*****************************************************)
 (**                Division by 2                     *)
 
-Local Notation "a <= b <= c" := (a<=b /\ b<=c).
-Local Notation "a <= b < c" := (a<=b /\ b<c).
-Local Notation "a < b <= c" := (a<b /\ b<=c).
-Local Notation "a < b < c" := (a<b /\ b<c).
-Local Notation "2" := (S 1).
-
 Definition half_aux (x : N.t) : N.t * N.t :=
   recursion (0, 0) (fun _ p => let (x1, x2) := p in (S x2, x1)) x.
 
@@ -250,14 +206,14 @@ Definition half (x : N.t) := snd (half_aux x).
 Instance half_aux_wd : Proper (N.eq ==> N.eq*N.eq) half_aux.
 Proof.
 intros x x' Hx. unfold half_aux.
-apply recursion_wd; auto with *.
+f_equiv; trivial.
 intros y y' Hy (u,v) (u',v') (Hu,Hv). compute in *.
 rewrite Hu, Hv; auto with *.
 Qed.
 
 Instance half_wd : Proper (N.eq==>N.eq) half.
 Proof.
-intros x x' Hx. unfold half. rewrite Hx; auto with *.
+unfold half. f_equiv'.
 Qed.
 
 Lemma half_aux_0 : half_aux 0 = (0,0).
@@ -272,8 +228,7 @@ intros.
 remember (half_aux x) as h.
 destruct h as (f,s); simpl in *.
 unfold half_aux in *.
-rewrite recursion_succ, <- Heqh; simpl; auto.
-repeat red; intros; subst; auto.
+rewrite recursion_succ, <- Heqh; simpl; f_equiv'.
 Qed.
 
 Theorem half_aux_spec : forall n,
@@ -285,7 +240,7 @@ rewrite half_aux_0; simpl; rewrite add_0_l; auto with *.
 intros.
 rewrite half_aux_succ. simpl.
 rewrite add_succ_l, add_comm; auto.
-apply succ_wd; auto.
+now f_equiv.
 Qed.
 
 Theorem half_aux_spec2 : forall n,
@@ -298,7 +253,7 @@ rewrite half_aux_0; simpl. auto with *.
 intros.
 rewrite half_aux_succ; simpl.
 destruct H; auto with *.
-right; apply succ_wd; auto with *.
+right; now f_equiv.
 Qed.
 
 Theorem half_0 : half 0 == 0.
@@ -315,7 +270,7 @@ Theorem half_double : forall n,
  n == 2 * half n \/ n == 1 + 2 * half n.
 Proof.
 intros. unfold half.
-nzsimpl.
+nzsimpl'.
 destruct (half_aux_spec2 n) as [H|H]; [left|right].
 rewrite <- H at 1. apply half_aux_spec.
 rewrite <- add_succ_l. rewrite <- H at 1. apply half_aux_spec.
@@ -353,16 +308,16 @@ Qed.
 Theorem half_decrease : forall n, 0 < n -> half n < n.
 Proof.
 intros n LT.
-destruct (half_double n) as [E|E]; rewrite E at 2;
- rewrite ?mul_succ_l, ?mul_0_l, ?add_0_l, ?add_assoc.
+destruct (half_double n) as [E|E]; rewrite E at 2; nzsimpl'.
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
 assert (LE : 0 <= half n) by apply le_0_l.
-nzsimpl. le_elim LE; auto.
+le_elim LE; auto.
 rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT).
+rewrite <- add_succ_l.
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
-nzsimpl. apply lt_0_succ.
+apply lt_0_succ.
 Qed.
 
 
@@ -373,17 +328,9 @@ Definition pow (n m : N.t) := recursion 1 (fun _ r => n*r) m.
 
 Local Infix "^^" := pow (at level 30, right associativity).
 
-Instance pow_prewd :
- Proper (N.eq==>N.eq==>N.eq==>N.eq) (fun n _ r => n*r).
-Proof.
-intros n n' Hn x x' Hx y y' Hy. rewrite Hn, Hy; auto with *.
-Qed.
-
 Instance pow_wd : Proper (N.eq==>N.eq==>N.eq) pow.
 Proof.
-intros n n' Hn m m' Hm. unfold pow.
-apply recursion_wd; auto with *.
-now apply pow_prewd.
+unfold pow. f_equiv'.
 Qed.
 
 Lemma pow_0 : forall n, n^^0 == 1.
@@ -393,8 +340,7 @@ Qed.
 
 Lemma pow_succ : forall n m, n^^(S m) == n*(n^^m).
 Proof.
-intros. unfold pow. rewrite recursion_succ; auto with *.
-now apply pow_prewd.
+intros. unfold pow. rewrite recursion_succ; f_equiv'.
 Qed.
 
 
@@ -415,15 +361,13 @@ Proof.
 intros g g' Hg n n' Hn.
 rewrite Hn.
 destruct (n' << 2); auto with *.
-apply succ_wd.
-apply Hg. rewrite Hn; auto with *.
+f_equiv. apply Hg. now f_equiv.
 Qed.
 
 Instance log_wd : Proper (N.eq==>N.eq) log.
 Proof.
 intros x x' Exx'. unfold log.
-apply strong_rec_wd; auto with *.
-apply log_prewd.
+apply strong_rec_wd; f_equiv'.
 Qed.
 
 Lemma log_good_step : forall n h1 h2,
@@ -434,8 +378,8 @@ Proof.
 intros n h1 h2 E.
 destruct (n<<2) as [ ]_eqn:H.
 auto with *.
-apply succ_wd, E, half_decrease.
-rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
+f_equiv. apply E, half_decrease.
+rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
 order'.
 Qed.
 Hint Resolve log_good_step.
@@ -469,12 +413,12 @@ destruct (lt_ge_cases k 2) as [LT|LE].
 rewrite log_init, pow_0 by auto.
 rewrite <- le_succ_l, <- one_succ in Hk2.
 le_elim Hk2.
-rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto.
+rewrite two_succ, <- nle_gt, le_succ_l in LT. destruct LT; auto.
 rewrite <- Hk2.
 rewrite half_1; auto using lt_0_1, le_refl.
 (* step *)
 rewrite log_step, pow_succ by auto.
-rewrite le_succ_l in LE.
+rewrite two_succ, le_succ_l in LE.
 destruct (IH (half k)) as (IH1,IH2).
  rewrite <- lt_succ_r. apply lt_le_trans with k; auto.
   now apply half_decrease.
@@ -484,10 +428,10 @@ split.
 rewrite <- le_succ_l in IH1.
 apply mul_le_mono_l with (p:=2) in IH1.
 eapply lt_le_trans; eauto.
-nzsimpl.
+nzsimpl'.
 rewrite lt_succ_r.
 eapply le_trans; [ eapply half_lower_bound | ].
-nzsimpl; apply le_refl.
+nzsimpl'; apply le_refl.
 eapply le_trans; [ | eapply half_upper_bound ].
 apply mul_le_mono_l; auto.
 Qed.
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 1fe6ed9bf5..bcf746a7d4 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -23,11 +23,8 @@ Definition natural_isomorphism : N1.t -> N2.t :=
 Instance natural_isomorphism_wd : Proper (N1.eq ==> N2.eq) natural_isomorphism.
 Proof.
 unfold natural_isomorphism.
-intros n m Eqxy.
-apply N1.recursion_wd.
-reflexivity.
-intros _ _ _ y' y'' H. now apply N2.succ_wd.
-assumption.
+repeat red; intros. f_equiv; trivial.
+repeat red; intros. now f_equiv.
 Qed.
 
 Theorem natural_isomorphism_0 : natural_isomorphism N1.zero == N2.zero.
@@ -40,7 +37,7 @@ Theorem natural_isomorphism_succ :
 Proof.
 unfold natural_isomorphism.
 intro n. rewrite N1.recursion_succ; auto with *.
-repeat red; intros. apply N2.succ_wd; auto.
+repeat red; intros. now f_equiv.
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v
index 8a1a4def67..321508f584 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.
 
diff --git a/theories/Numbers/Natural/Abstract/NStrongRec.v b/theories/Numbers/Natural/Abstract/NStrongRec.v
index a52a52e766..039eefdf59 100644
--- a/theories/Numbers/Natural/Abstract/NStrongRec.v
+++ b/theories/Numbers/Natural/Abstract/NStrongRec.v
@@ -13,6 +13,8 @@ and proves its properties *)
 
 Require Export NSub.
 
+Ltac f_equiv' := repeat progress (f_equiv; try intros ? ? ?; auto).
+
 Module NStrongRecProp (Import N : NAxiomsRecSig').
 Include NSubProp N.
 
@@ -49,30 +51,18 @@ Proof.
 reflexivity.
 Qed.
 
-(** We need a result similar to [f_equal], but for setoid equalities. *)
-Lemma f_equiv : forall f g x y,
- (N.eq==>Aeq)%signature f g -> N.eq x y -> Aeq (f x) (g y).
-Proof.
-auto.
-Qed.
-
 Instance strong_rec0_wd :
  Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> N.eq ==> Aeq)
   strong_rec0.
 Proof.
-unfold strong_rec0.
-repeat red; intros.
-apply f_equiv; auto.
-apply recursion_wd; try red; auto.
+unfold strong_rec0; f_equiv'.
 Qed.
 
 Instance strong_rec_wd :
  Proper (Aeq ==> ((N.eq ==> Aeq) ==> N.eq ==> Aeq) ==> N.eq ==> Aeq) strong_rec.
 Proof.
 intros a a' Eaa' f f' Eff' n n' Enn'.
-rewrite !strong_rec_alt.
-apply strong_rec0_wd; auto.
-now rewrite Enn'.
+rewrite !strong_rec_alt; f_equiv'.
 Qed.
 
 Section FixPoint.
@@ -90,18 +80,16 @@ Lemma strong_rec0_succ : forall a n m,
  Aeq (strong_rec0 a f (S n) m) (f (strong_rec0 a f n) m).
 Proof.
 intros. unfold strong_rec0.
-apply f_equiv; auto with *.
-rewrite recursion_succ; try (repeat red; auto with *; fail).
-apply f_wd.
-apply recursion_wd; try red; auto with *.
+f_equiv.
+rewrite recursion_succ; f_equiv'.
+reflexivity.
 Qed.
 
 Lemma strong_rec_0 : forall a,
  Aeq (strong_rec a f 0) (f (fun _ => a) 0).
 Proof.
-intros. rewrite strong_rec_alt, strong_rec0_succ.
-apply f_wd; auto with *.
-red; intros; rewrite strong_rec0_0; auto with *.
+intros. rewrite strong_rec_alt, strong_rec0_succ; f_equiv'.
+rewrite strong_rec0_0. reflexivity.
 Qed.
 
 (* We need an assumption saying that for every n, the step function (f h n)
@@ -156,7 +144,7 @@ intros.
 transitivity (f (fun n => strong_rec0 a f (S n) n) n).
 rewrite strong_rec_alt.
 apply strong_rec0_fixpoint.
-apply f_wd; auto with *.
+f_equiv.
 intros x x' Hx; rewrite strong_rec_alt, Hx; auto with *.
 Qed.