Fix bug #1704 (ordering of condition goals for (setoid)rewrite). As part

of the fix I added an optional "by" annotation for rewrite to solve said
conditions in the same tactic call. Most of the theories have been
updated, only FSets is missing, Pierre will take care of it.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10634 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 38 insertions, 35 deletions

diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index adaa340db..f5c550417 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -317,11 +317,12 @@ assert (HH: ~ r5*r6 == 0).
   apply field_is_integral_domain.
     intros H1; case H; rewrite H1; ring.
     intros H1; case H0; rewrite H1; ring.
-rewrite <- rdiv4; auto.
+rewrite <- rdiv4 ; auto.
+  rewrite rdiv_r_r; auto.
+
   apply field_is_integral_domain.
     intros H1; case H; rewrite H1; ring.
     intros H1; case H0; rewrite H1; ring.
-rewrite rdiv_r_r; auto.
 Qed.
 
 
@@ -353,11 +354,11 @@ assert (HH: ~ r5*r6 == 0).
   apply field_is_integral_domain.
     intros H2; case H0; rewrite H2; ring.
     intros H2; case H1; rewrite H2; ring.
-rewrite <- rdiv4; auto.
+rewrite <- rdiv4 ; auto.
+rewrite rdiv_r_r; auto.
   apply field_is_integral_domain.
     intros H2; case H; rewrite H2; ring.
     intros H2; case H0; rewrite H2; ring.
-rewrite rdiv_r_r; auto.
 Qed.
 
 
@@ -379,8 +380,7 @@ transitivity (r1 / r2 * (r4 / r4)).
    rewrite H1 in |- *.
    rewrite (ARmul_comm ARth r2 r4) in |- *.
    rewrite <- rdiv4 in |- *; trivial.
-   rewrite rdiv_r_r in |- *.
-  trivial.
+   rewrite rdiv_r_r in |- * by trivial.
   apply (ARmul_1_r Rsth ARth).
 Qed.
 
@@ -780,7 +780,7 @@ Proof.
   case_eq ((p1 ?= p2)%positive Eq);intros;simpl. 
   repeat rewrite pow_th.(rpow_pow_N);simpl. split. 2:refine (refl_equal _).
   rewrite (Pcompare_Eq_eq _ _ H0).  
-  rewrite H;[trivial | ring [ (morph1 CRmorph)]].
+  rewrite H by trivial. ring [ (morph1 CRmorph)].
   fold (NPEpow e2 (Npos (p2 - p1))).
   rewrite NPEpow_correct;simpl.
   repeat rewrite pow_th.(rpow_pow_N);simpl.
@@ -1048,10 +1048,11 @@ Proof.
  induction p;simpl.
   intro Hp;assert (H1 := @rmul_reg_l _ (pow_pos rmul x p * pow_pos rmul x p) 0 H).
   apply IHp.
-  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp). rewrite H1. rewrite Hp;ring. ring.
-  reflexivity. 
+  rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp). 
+  reflexivity.
+  rewrite H1. ring. rewrite Hp;ring. 
   intro Hp;apply IHp. rewrite (@rmul_reg_l _ (pow_pos rmul x p)  0 IHp).
-  rewrite Hp;ring. reflexivity. trivial.
+  reflexivity. rewrite Hp;ring. trivial.
 Qed.
  
 Theorem Pcond_Fnorm:
@@ -1234,13 +1235,15 @@ generalize (NPEeval l (num (Fnorm e1))) (NPEeval l (denum (Fnorm e1)))
   (Pcond_Fnorm _ _ Hcond).
 intros r r0 Hdiff;induction p;simpl.
 repeat (rewrite <- rdiv4;trivial).
-intro Hp;apply (pow_pos_not_0 Hdiff  p). 
+rewrite IHp. reflexivity.
+apply pow_pos_not_0;trivial.
+apply pow_pos_not_0;trivial.
+intro Hp. apply (pow_pos_not_0 Hdiff  p).
 rewrite  (@rmul_reg_l (pow_pos rmul r0 p) (pow_pos rmul r0 p)  0).
- apply pow_pos_not_0;trivial. ring [Hp]. reflexivity.
-apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
-rewrite IHp;reflexivity.
-rewrite <- rdiv4;trivial. apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
+ reflexivity. apply pow_pos_not_0;trivial. ring [Hp]. 
+rewrite <- rdiv4;trivial. 
 rewrite IHp;reflexivity.
+apply pow_pos_not_0;trivial. apply pow_pos_not_0;trivial.
 reflexivity.
 Qed.
 
@@ -1253,9 +1256,9 @@ Theorem Fnorm_crossproduct:
  PCond l (condition nfe1 ++ condition nfe2) ->
  FEeval l fe1 == FEeval l fe2.
 intros l fe1 fe2 nfe1 nfe2 Hcrossprod Hcond; subst nfe1 nfe2.
-rewrite Fnorm_FEeval_PEeval in |- *.
+rewrite Fnorm_FEeval_PEeval in |- * by
  apply PCond_app_inv_l with (1 := Hcond).
- rewrite Fnorm_FEeval_PEeval in |- *.
+ rewrite Fnorm_FEeval_PEeval in |- * by
   apply PCond_app_inv_r with (1 := Hcond).
   apply cross_product_eq; trivial.
    apply Pcond_Fnorm.
@@ -1473,18 +1476,18 @@ Proof.
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
  ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
  intro Heq; apply AFth.(AF_1_neq_0).
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
  ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
  rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (AFth.(AFdiv_def)).
- repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ repeat rewrite <- Fnorm_FEeval_PEeval ; trivial.
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7).
 Qed.
 
 Theorem Field_simplify_eq_in_correct :
@@ -1523,18 +1526,18 @@ Proof.
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe2))));trivial.
  ring [Heq]. rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  apply (@rmul_reg_l (/NPEeval l (denum (Fnorm fe1)))).
  intro Heq; apply AFth.(AF_1_neq_0).
  rewrite <- (@AFinv_l AFth (NPEeval l (denum (Fnorm fe1))));trivial.
  ring [Heq]. repeat rewrite (ARth.(ARmul_comm)  (/ NPEeval l (denum (Fnorm fe1)))).
  repeat rewrite <- (ARth.(ARmul_assoc)).
- repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r. trivial.
+ repeat rewrite <- (AFth.(AFdiv_def)). rewrite rdiv_r_r by trivial.
  rewrite (AFth.(AFdiv_def)). ring_simplify. unfold SRopp.
  rewrite  (ARth.(ARmul_comm) (/ NPEeval l (denum (Fnorm fe2)))).
  repeat rewrite <- (AFth.(AFdiv_def)).
  repeat rewrite <- Fnorm_FEeval_PEeval;trivial.
- apply (PCond_app_inv_l _ _ _ H7). apply (PCond_app_inv_r _ _ _ H7).
+ apply (PCond_app_inv_r _ _ _ H7). apply (PCond_app_inv_l _ _ _ H7). 
 Qed.
 
 
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index 56b08a8fa..4d96bec4c 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -515,12 +515,12 @@ induction x; intros.
 
   simpl Nwadd in |- *.
   repeat rewrite gen_phiNword_cons in |- *.
-  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- *.
-   destruct Reqe; constructor; trivial.
+  rewrite (fun sreq => gen_phiN_add Rsth sreq (ARth_SRth ARth)) in |- * by
+    (destruct Reqe; constructor; trivial).
 
-   rewrite IHx in |- *.
-   norm.
-   add_push (- gen_phiNword x); reflexivity.
+  rewrite IHx in |- *.
+  norm.
+  add_push (- gen_phiNword x); reflexivity.
 Qed.
 
 Lemma Nwopp_ok : forall x, gen_phiNword (Nwopp x) == - gen_phiNword x.
@@ -537,8 +537,8 @@ induction x; intros.
 
  simpl Nwscal in |- *.
  repeat rewrite gen_phiNword_cons in |- *.
- rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *.
-  destruct Reqe; constructor; trivial.
+ rewrite (fun sreq => gen_phiN_mult Rsth sreq (ARth_SRth ARth)) in |- *
+   by (destruct Reqe; constructor; trivial).
 
   rewrite IHx in |- *.
   norm.
diff --git a/contrib/setoid_ring/Ring_polynom.v b/contrib/setoid_ring/Ring_polynom.v
index 70199676c..45b38e2ed 100644
--- a/contrib/setoid_ring/Ring_polynom.v
+++ b/contrib/setoid_ring/Ring_polynom.v
@@ -1064,7 +1064,7 @@ Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
    rewrite Padd_ok; rewrite PmulC_ok; rsimpl.
  intros i P5 H; rewrite H.
    intros HH H1; injection HH; intros; subst; rsimpl.
-   rewrite Padd_ok; rewrite PmulI_ok. intros;apply Pmul_ok. rewrite H1; rsimpl.
+   rewrite Padd_ok; rewrite PmulI_ok by (intros;apply Pmul_ok). rewrite H1; rsimpl. 
  intros i P5 P6 H1 H2 H3; rewrite H1; rewrite H3.
    assert (P4 = Q1 ++ P3 ** PX i P5 P6).
    injection H2; intros; subst;trivial.
@@ -1258,7 +1258,7 @@ Section POWER.
  
   Lemma Ppow_N_ok : forall l,  (forall P, subst_l P@l == P@l) ->
          forall P n, (Ppow_N P n)@l == (pow_N P1 Pmul P n)@l.
-  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok. trivial. Esimpl.  Qed.
+  Proof.  destruct n;simpl. rrefl. rewrite Ppow_pos_ok by trivial. Esimpl.  Qed.
     
  End POWER.
 
@@ -1334,7 +1334,7 @@ Section POWER.
    rewrite IHpe1;rewrite IHpe2;rrefl.
    rewrite IHpe1;rewrite IHpe2. rewrite Pmul_ok. rrefl.
    rewrite IHpe;rrefl.
-   rewrite Ppow_N_ok. intros;rrefl.
+   rewrite Ppow_N_ok by (intros;rrefl).
    rewrite pow_th.(rpow_pow_N). destruct n0;Esimpl3.
    induction p;simpl;try rewrite IHp;try rewrite IHpe;repeat rewrite Pms_ok; 
       repeat rewrite Pmul_ok;rrefl.
@@ -1425,7 +1425,7 @@ Section POWER.
    assert (HH:=mon_of_pol_ok (norm_subst 0 nil  p));
      destruct  (mon_of_pol (norm_subst 0 nil p)).  
    split.
-   rewrite <- norm_subst_spec. exact I.
+   rewrite <- norm_subst_spec by exact I.
    destruct lpe;try destruct H;rewrite <- H;
    rewrite (norm_subst_spec 0 nil); try exact I;apply HH;trivial.
    apply IHlpe. destruct lpe;simpl;trivial. destruct H. exact H0.