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

6 files changed, 38 insertions, 37 deletions

diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index fc9115e20..a40832507 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -210,8 +210,9 @@ destruct n as [n m].
 cut (forall p : N, A (p, 0)); [intro H1 |].
 cut (forall p : N, A (0, p)); [intro H2 |].
 destruct (plus_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0, p)); simpl. rewrite plus_0_l; now rewrite plus_comm. apply H2.
-rewrite (A_wd (n, m) (p, 0)); simpl. now rewrite plus_0_r. apply H1.
+rewrite (A_wd (n, m) (0, p)) by (rewrite plus_0_l; now rewrite plus_comm).
+apply H2.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite plus_0_r. apply H1.
 induct p. assumption. intros p IH.
 apply -> (A_wd (0, p) (1, S p)) in IH; [| now rewrite plus_0_l, plus_1_l].
 now apply <- AS.
@@ -302,13 +303,13 @@ Add Morphism NZmin with signature Zeq ==> Zeq ==> Zeq as NZmin_wd.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmin, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_l (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
 stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
 unfold Zeq in H1. rewrite H1. ring.
-rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (min_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (min_r (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
 stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
@@ -318,13 +319,13 @@ Add Morphism NZmax with signature Zeq ==> Zeq ==> Zeq as NZmax_wd.
 Proof.
 intros n1 m1 H1 n2 m2 H2; unfold NZmax, Zeq; simpl.
 destruct (le_ge_cases (fst n1 + snd n2) (fst n2 + snd n1)) as [H | H].
-rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_r (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_r (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n1 m1 H1 n2 m2 H2).
 stepl ((fst n2 + snd m2) + (snd n1 + snd m1)) by ring.
 unfold Zeq in H2. rewrite H2. ring.
-rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)). assumption.
-rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)).
+rewrite (max_l (fst n1 + snd n2) (fst n2 + snd n1)) by assumption.
+rewrite (max_l (fst m1 + snd m2) (fst m2 + snd m1)) by
 now apply -> (NZle_wd n2 m2 H2 n1 m1 H1).
 stepl ((fst n1 + snd m1) + (snd n2 + snd m2)) by ring.
 unfold Zeq in H1. rewrite H1. ring.
@@ -350,25 +351,25 @@ Qed.
 Theorem NZmin_l : forall n m : Z, n <= m -> Zmin n m == n.
 Proof.
 unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_l. assumption. ring.
+rewrite min_l by assumption. ring.
 Qed.
 
 Theorem NZmin_r : forall n m : Z, m <= n -> Zmin n m == m.
 Proof.
 unfold Zmin, Zle, Zeq; simpl; intros n m H.
-rewrite min_r. assumption. ring.
+rewrite min_r by assumption. ring.
 Qed.
 
 Theorem NZmax_l : forall n m : Z, m <= n -> Zmax n m == n.
 Proof.
 unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_l. assumption. ring.
+rewrite max_l by assumption. ring.
 Qed.
 
 Theorem NZmax_r : forall n m : Z, n <= m -> Zmax n m == m.
 Proof.
 unfold Zmax, Zle, Zeq; simpl; intros n m H.
-rewrite max_r. assumption. ring.
+rewrite max_r by assumption. ring.
 Qed.
 
 End NZOrdAxiomsMod.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index bc3600f9c..133bbde4d 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -140,11 +140,12 @@ setoid_replace (n < n) with False using relation iff by
 now setoid_replace (S n <= n) with False using relation iff by
   (apply -> neg_false; apply NZnle_succ_diag_l).
 intro m. rewrite NZlt_succ_r. rewrite NZle_succ_r.
-rewrite NZsucc_inj_wd. rewrite (NZlt_eq_cases n m).
+rewrite NZsucc_inj_wd.
+rewrite (NZlt_eq_cases n m).
 rewrite or_cancel_r.
+reflexivity.
 intros H1 H2; rewrite H2 in H1; false_hyp H1 NZnle_succ_diag_l.
 apply NZlt_neq.
-reflexivity.
 Qed.
 
 Theorem NZlt_succ_l : forall n m : NZ, S n < m -> n < m.
diff --git a/theories/Numbers/NatInt/NZTimesOrder.v b/theories/Numbers/NatInt/NZTimesOrder.v
index 51d2172de..b51e3d22b 100644
--- a/theories/Numbers/NatInt/NZTimesOrder.v
+++ b/theories/Numbers/NatInt/NZTimesOrder.v
@@ -60,7 +60,7 @@ split; [apply LR |]. intro H2. apply -> NZlt_dne; intro H3.
 apply <- NZle_ngt in H3. le_elim H3.
 apply NZlt_asymm in H2. apply H2. now apply LR.
 rewrite H3 in H2; false_hyp H2 NZlt_irrefl.
-rewrite (NZtimes_lt_pred p (S p)); [reflexivity |].
+rewrite (NZtimes_lt_pred p (S p)) by reflexivity.
 rewrite H; do 2 rewrite NZtimes_0_l; now do 2 rewrite NZplus_0_l.
 Qed.
 
@@ -109,9 +109,9 @@ assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_neg_l |].
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 false_hyp H2 H.
 apply -> NZeq_dne; intro H3. apply -> NZlt_gt_cases in H3. destruct H3 as [H3 | H3].
-assert (H4 : p * n < p * m); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * n < p * m) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
-assert (H4 : p * m < p * n); [now apply -> NZtimes_lt_mono_pos_l |].
+assert (H4 : p * m < p * n) by (now apply -> NZtimes_lt_mono_pos_l).
 rewrite H1 in H4; false_hyp H4 NZlt_irrefl.
 now rewrite H1.
 Qed.
@@ -135,9 +135,9 @@ Qed.
 Theorem NZtimes_le_mono_pos_l : forall n m p : NZ, 0 < p -> (n <= m <-> p * n <= p * m).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_pos_l p n m); [assumption |].
-now rewrite -> (NZtimes_cancel_l n m p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_pos_l p n m) by assumption.
+now rewrite -> (NZtimes_cancel_l n m p) by
+(intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 Qed.
 
 Theorem NZtimes_le_mono_pos_r : forall n m p : NZ, 0 < p -> (n <= m <-> n * p <= m * p).
@@ -149,9 +149,8 @@ Qed.
 Theorem NZtimes_le_mono_neg_l : forall n m p : NZ, p < 0 -> (n <= m <-> p * m <= p * n).
 Proof.
 intros n m p H; do 2 rewrite NZlt_eq_cases.
-rewrite (NZtimes_lt_mono_neg_l p n m); [assumption |].
-rewrite -> (NZtimes_cancel_l m n p);
-[intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl |].
+rewrite (NZtimes_lt_mono_neg_l p n m); [| assumption].
+rewrite -> (NZtimes_cancel_l m n p) by (intro H1; rewrite H1 in H; false_hyp H NZlt_irrefl).
 now setoid_replace (n == m) with (m == n) using relation iff by (split; now intro).
 Qed.
 
diff --git a/theories/Numbers/Natural/Abstract/NIso.v b/theories/Numbers/Natural/Abstract/NIso.v
index 10c341cbf..4df46e20e 100644
--- a/theories/Numbers/Natural/Abstract/NIso.v
+++ b/theories/Numbers/Natural/Abstract/NIso.v
@@ -51,8 +51,8 @@ Theorem natural_isomorphism_succ :
   forall n : N1, natural_isomorphism (S1 n) == S2 (natural_isomorphism n).
 Proof.
 unfold natural_isomorphism.
-intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq);
-[| unfold fun2_wd; intros; apply NBasePropMod2.succ_wd |].
+intro n. now rewrite (@NAxiomsMod1.recursion_succ N2 NAxiomsMod2.Neq) ;
+[ | | unfold fun2_wd; intros; apply NBasePropMod2.succ_wd].
 Qed.
 
 Theorem hom_nat_iso : homomorphism natural_isomorphism.
diff --git a/theories/Numbers/Natural/Abstract/NMinus.v b/theories/Numbers/Natural/Abstract/NMinus.v
index faf4759bd..5e1d5d8c3 100644
--- a/theories/Numbers/Natural/Abstract/NMinus.v
+++ b/theories/Numbers/Natural/Abstract/NMinus.v
@@ -63,8 +63,8 @@ Proof.
 intros n m p; induct p.
 intro; now do 2 rewrite minus_0_r.
 intros p IH H. do 2 rewrite minus_succ_r.
-rewrite <- IH; [apply lt_le_incl; now apply -> le_succ_l |].
-rewrite plus_pred_r. apply minus_gt. now apply -> le_succ_l.
+rewrite <- IH by (apply lt_le_incl; now apply -> le_succ_l).
+rewrite plus_pred_r by (apply minus_gt; now apply -> le_succ_l).
 reflexivity.
 Qed.
 
@@ -76,13 +76,13 @@ Qed.
 
 Theorem plus_minus : forall n m : N, (n + m) - m == n.
 Proof.
-intros n m. rewrite <- plus_minus_assoc. apply le_refl.
+intros n m. rewrite <- plus_minus_assoc by (apply le_refl).
 rewrite minus_diag; now rewrite plus_0_r.
 Qed.
 
 Theorem minus_plus : forall n m : N, n <= m -> (m - n) + n == m.
 Proof.
-intros n m H. rewrite plus_comm. rewrite plus_minus_assoc; [assumption |].
+intros n m H. rewrite plus_comm. rewrite plus_minus_assoc by assumption.
 rewrite plus_comm. apply plus_minus.
 Qed.
 
@@ -121,7 +121,7 @@ Theorem plus_minus_swap : forall n m p : N, p <= n -> n + m - p == n - p + m.
 Proof.
 intros n m p H.
 rewrite (plus_comm n m).
-rewrite <- plus_minus_assoc; [assumption |].
+rewrite <- plus_minus_assoc by assumption.
 now rewrite (plus_comm m (n - p)).
 Qed.
 
@@ -151,8 +151,8 @@ Proof.
 intros n m; cases m.
 now rewrite pred_0, times_0_r, minus_0_l.
 intro m; rewrite pred_succ, times_succ_r, <- plus_minus_assoc.
-now apply eq_le_incl.
 now rewrite minus_diag, plus_0_r.
+now apply eq_le_incl.
 Qed.
 
 Theorem times_minus_distr_r : forall n m p : N, (n - m) * p == n * p - m * p.
@@ -160,9 +160,9 @@ Proof.
 intros n m p; induct n.
 now rewrite minus_0_l, times_0_l, minus_0_l.
 intros n IH. destruct (le_gt_cases m n) as [H | H].
-rewrite minus_succ_l; [assumption |]. do 2 rewrite times_succ_l.
+rewrite minus_succ_l by assumption. do 2 rewrite times_succ_l.
 rewrite (plus_comm ((n - m) * p) p), (plus_comm (n * p) p).
-rewrite <- (plus_minus_assoc p (n * p) (m * p)); [now apply times_le_mono_r |].
+rewrite <- (plus_minus_assoc p (n * p) (m * p)) by now apply times_le_mono_r.
 now apply <- plus_cancel_l.
 assert (H1 : S n <= m); [now apply <- le_succ_l |].
 setoid_replace (S n - m) with 0 by now apply <- minus_0_le.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index 7b4645be3..1e53d8063 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -506,7 +506,7 @@ Theorem pred_lt_mono : forall n m : N, n ~= 0 -> (n < m <-> P n < P m).
 Proof.
 intros n m H1; split; intro H2.
 assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n.
-now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2;
+now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ;
 [apply <- succ_lt_mono | | |].
 assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n).
 apply lt_le_trans with (P m). assumption. apply le_pred_l.
@@ -515,7 +515,7 @@ Qed.
 
 Theorem lt_succ_lt_pred : forall n m : N, S n < m <-> n < P m.
 Proof.
-intros n m. rewrite pred_lt_mono. apply neq_succ_0. now rewrite pred_succ.
+intros n m. rewrite pred_lt_mono by apply neq_succ_0. now rewrite pred_succ.
 Qed.
 
 Theorem le_succ_le_pred : forall n m : N, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *)