repair FSets/FMap after the change in setoid rewrite

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

6 files changed, 140 insertions, 248 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index a31a0fd84..f3a20eb1c 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -750,11 +750,11 @@ Proof.
  intuition_in.
  destruct s1;try contradiction;clear y.
 (*  rewrite H_eq_2; rewrite H_eq_2 in H_eq_1; clear H_eq_2. *)
- replace s2' with ((remove_min l2 x2 e2 r2)#1); [|rewrite e3; auto].
+ replace s2' with ((remove_min l2 x2 e2 r2)#1) by (rewrite e3; auto).
  rewrite bal_in; auto.
- generalize (remove_min_avl H2); rewrite e3; simpl; auto.
  generalize (remove_min_in y0 H2); rewrite e3; simpl; intro.
  rewrite H3; intuition.
+ generalize (remove_min_avl H2); rewrite e3; simpl; auto.
 Qed.
 
 Lemma merge_mapsto : forall elt (s1 s2:t elt) y e, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -766,10 +766,10 @@ Proof.
  destruct s1;try contradiction;clear y.
  replace s2' with ((remove_min l2 x2 e2 r2)#1); [|rewrite e3; auto].
  rewrite bal_mapsto; auto; unfold create.
- generalize (remove_min_avl H2); rewrite e3; simpl; auto.
  generalize (remove_min_mapsto y0 e H2); rewrite e3; simpl; intro.
  rewrite H3; intuition (try subst; auto).
  inversion_clear H3; intuition.
+ generalize (remove_min_avl H2); rewrite e3; simpl; auto.
 Qed.
 
 Lemma merge_bst : forall elt (s1 s2:t elt), bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -1535,20 +1535,7 @@ simpl; auto.
 intuition.
 inversion H4.
 simpl; destruct a; intros.
-rewrite IHl; clear IHl.
-apply add_bst; auto.
-apply add_avl; auto.
-inversion H1; auto.
-intros.
-inversion_clear H1.
-assert (~X.eq x k).
- contradict H5.
- destruct H3.
- apply InA_eqA with (x,x0); eauto.
-apply (H2 x).
-destruct H3; exists x0; auto.
-revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto.
-eapply add_3; eauto.
+rewrite IHl; clear IHl; auto using add_bst, add_avl.
 intuition.
 assert (find k0 (add k e m) = Some e0).
  apply find_1; auto.
@@ -1565,6 +1552,17 @@ inversion_clear H1.
 destruct (MX.eq_dec k0 k).
 destruct (H2 k); eauto.
 right; apply add_2; auto.
+inversion H1; auto.
+intros.
+inversion_clear H1.
+assert (~X.eq x k).
+ contradict H5.
+ destruct H3.
+ apply InA_eqA with (x,x0); eauto.
+apply (H2 x).
+destruct H3; exists x0; auto.
+revert H4; do 2 rewrite <- In_alt; destruct 1; exists x0; auto.
+eapply add_3; eauto.
 Qed.
 
 Lemma anti_elements_mapsto : forall l k e, NoDupA (PX.eqk (elt:=elt'')) l ->
@@ -1573,9 +1571,9 @@ Proof.
 intros. 
 unfold anti_elements.
 rewrite anti_elements_mapsto_aux; auto; unfold empty; auto.
-inversion 2.
 intuition.
 inversion H1.
+inversion 2.
 Qed.
 
 Lemma map2_avl : forall (m: t elt)(m': t elt'), avl (map2 m m').
@@ -1612,15 +1610,11 @@ intros.
 case_eq (L.find x l); intros.
 apply find_1.
 apply anti_elements_bst; auto.
-rewrite anti_elements_mapsto.
-apply L.PX.Sort_NoDupA; auto.
-apply L.find_2; auto.
+rewrite anti_elements_mapsto; auto using L.PX.Sort_NoDupA, L.find_2.
 case_eq (find x (anti_elements l)); auto; intros.
 rewrite <- H0; symmetry.
 apply L.find_1; auto.
-rewrite <- anti_elements_mapsto.
-apply L.PX.Sort_NoDupA; auto.
-apply find_2; auto.
+rewrite <- anti_elements_mapsto; auto using L.PX.Sort_NoDupA, find_2.
 Qed.
 
 Lemma map2_1 : forall (m: t elt)(m': t elt')(x:key), bst m -> bst m' -> 
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 78962fd1b..993f1ae79 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -1214,7 +1214,6 @@ Module OrdProperties (M:S).
   constructor; auto with map.
   apply (@filter_sort _ eqke); auto with map; clean_eauto.
   rewrite (@InfA_alt _ eqke); auto with map; try (clean_eauto; fail).
-  apply (@filter_sort _ eqke); auto with map; clean_eauto.
   intros.
   rewrite filter_InA in H1; auto with map; destruct H1.
   rewrite leb_1 in H2.
@@ -1224,6 +1223,7 @@ Module OrdProperties (M:S).
    contradict H.
    exists e0; apply MapsTo_1 with t0; auto.
   ME.order.
+  apply (@filter_sort _ eqke); auto with map; clean_eauto.
   intros.
   rewrite filter_InA in H1; auto with map; destruct H1.
   rewrite gtb_1 in H3.
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 26b892885..b75968e9f 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -410,7 +410,7 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   Lemma mapi_2 : forall (elt elt':Type)(m: t elt)(x:key)
         (f:key->elt->elt'), In x (mapi f m) -> In x m.
   Proof.
-  intros elt elt' m; exact (mapi_aux_2 m (fun n => n)).
+  intros elt elt' m. exact (@mapi_aux_2 _ elt' m (fun n => n)).
   Qed.
 
   Lemma map_1 : forall (elt elt':Type)(m: t elt)(x:key)(e:elt)(f:elt->elt'),
@@ -467,38 +467,37 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   intuition.
   inversion H2.
   simpl; destruct a; intros.
-  rewrite IHl; clear IHl.
-  inversion H; auto.
-  intros.
   inversion_clear H.
-  assert (~E.eq x k).
-   contradict H3.
-   destruct H1.
-   apply InA_eqA with (x,x0); eauto.
-   unfold eq_key, E.eq; eauto.
-   unfold eq_key, E.eq; congruence.
-  apply (H0 x).
-  destruct H1; exists x0; auto.
-  revert H2.
-  unfold In.
-  intros (e',He').
-  exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto.
+  rewrite IHl; clear IHl; auto.
   intuition.
-  red in H2.
-  rewrite add_spec in H2; auto.
+  red in H3.
+  rewrite add_spec in H3; auto.
   destruct (ME.eq_dec k0 k).
-  inversion_clear H2; subst; auto.
+  inversion_clear H3; subst; auto.
   right; apply find_2; auto.
-  inversion_clear H2; auto.
-  compute in H1; destruct H1.
+  inversion_clear H3; auto.
+  compute in H; destruct H.
   subst; right; apply add_1; auto.
   red; auto.
-  inversion_clear H.
   destruct (ME.eq_dec k0 k).
   unfold E.eq in *; subst.
   destruct (H0 k); eauto.
   red; eauto.
   right; apply add_2; unfold E.eq in *; auto.
+  (* proof of precondition of IHl *)
+  intros.
+  assert (~E.eq x k).
+   contradict H1.
+   destruct H.
+   apply InA_eqA with (x,x0); eauto.
+   unfold eq_key, E.eq; eauto.
+   unfold eq_key, E.eq; congruence.
+  apply (H0 x).
+  destruct H; exists x0; auto.
+  revert H3.
+  unfold In.
+  intros (e',He').
+  exists e'; apply (@add_3 _ m k x e' a); unfold E.eq; auto.
   Qed.
   
   Lemma anti_elements_mapsto : forall (A:Type) l k e, NoDupA (eq_key (A:=A)) l ->
@@ -507,10 +506,10 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   intros. 
   unfold anti_elements.
   rewrite anti_elements_mapsto_aux; auto; unfold empty; auto.
-  inversion 2.
-  inversion H2.
   intuition.
   inversion H1.
+  inversion 2.
+  inversion H2.
   Qed.
   
   Lemma find_anti_elements : forall (A:Type)(l: list (key*A)) x, sort (@lt_key _) l -> 
@@ -519,15 +518,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   intros.
   case_eq (L.find x l); intros.
   apply find_1.
-  rewrite anti_elements_mapsto.
-  apply L.PX.Sort_NoDupA; auto.
-  apply L.find_2; auto.
+  rewrite anti_elements_mapsto; auto using L.PX.Sort_NoDupA, L.find_2.
   case_eq (find x (anti_elements l)); auto; intros.
   rewrite <- H0; symmetry.
   apply L.find_1; auto.
-  rewrite <- anti_elements_mapsto.
-  apply L.PX.Sort_NoDupA; auto.
-  apply find_2; auto.
+  rewrite <- anti_elements_mapsto; auto using L.PX.Sort_NoDupA, find_2.
   Qed.
 
   Lemma find_elements : forall (A:Type)(m: t A) x,  
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 3a08b0f4f..83dc3f1c4 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -875,9 +875,9 @@ Proof.
  destruct s1;try contradiction;clear y.
  replace s2' with ((remove_min l2 x2 r2)#1); [|rewrite e1; auto].
  rewrite bal_in; auto.
- generalize (remove_min_avl H2); rewrite e1; simpl; auto.
  generalize (remove_min_in y0 H2); rewrite e1; simpl; intro.
  rewrite H3 ; intuition.
+ generalize (remove_min_avl H2); rewrite e1; simpl; auto.
 Qed.
 
 Lemma merge_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -1151,9 +1151,9 @@ Proof.
  inversion_clear H5.
  destruct s1;try contradiction;clear y; intros. 
  rewrite (@join_in _ m s2' y H0).
- generalize (remove_min_avl H2); rewrite e1; simpl; auto.
  generalize (remove_min_in y H2); rewrite e1; simpl.
  intro EQ; rewrite EQ; intuition.
+ generalize (remove_min_avl H2); rewrite e1; simpl; auto.
 Qed.
 
 Hint Resolve concat_avl concat_bst.
@@ -1210,9 +1210,9 @@ Proof.
  (* GT *)
  rewrite e1 in IHp;simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
  rewrite join_in; auto.
- generalize (split_avl x H5); rewrite e1; simpl; intuition.
  rewrite (IHp y0 H1 H5); clear e1.
  intuition; [ eauto | eauto | intuition_in ].
+ generalize (split_avl x H5); rewrite e1; simpl; intuition.
 Qed.
 
 Lemma split_in_2 : forall s x y, bst s -> avl s -> 
@@ -1222,10 +1222,10 @@ Proof.
  intuition; try inversion_clear H1.
  (* LT *)
  rewrite e1 in IHp; simpl in *; inversion_clear 1; inversion_clear 1; clear H7 H6.
-  rewrite join_in; auto.
- generalize (split_avl x H4); rewrite e1; simpl; intuition.
+ rewrite join_in; auto.
  rewrite (IHp y0 H0 H4); clear IHp e0.
  intuition; [ order | order | intuition_in ].
+ generalize (split_avl x H4); rewrite e1; simpl; intuition.
  (* EQ *)
  simpl in *; inversion_clear 1; inversion_clear 1; clear H6 H5 e0.
  intuition; [ order | intuition_in; order ]. 
@@ -1342,13 +1342,13 @@ Proof.
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
  intros; rewrite concat_in; auto.
-  intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  rewrite IHi1; rewrite IHi2.
  rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
  assert (~In x1 r) by (rewrite <- split_in_3; auto; rewrite H13; auto).
  intuition_in.
  elim H12.
  apply In_1 with y; auto.
+ intros y1 y2; rewrite IHi1, IHi2; intuition; order.
 Qed.
 
 Lemma inter_bst : forall s1 s2, bst s1 -> avl s1 -> bst s2 -> avl s2 -> 
@@ -1402,12 +1402,12 @@ Proof.
  apply concat_bst; auto; intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* In concat *)
  intros; rewrite concat_in; auto.
-  intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  rewrite IHi1; rewrite IHi2.
  rewrite <- H11, <- H14, split_in_1; auto; rewrite split_in_2; auto.
  rewrite split_in_3 in H13; intuition_in.
  elim H17.
  apply In_1 with x1; auto.
+ intros y1 y2; rewrite IHi1, IHi2; intuition; order.
  (* bst join *)
  apply join_bst; auto; intro y; [rewrite IHi1|rewrite IHi2]; intuition.
  (* In join *)
@@ -1675,10 +1675,8 @@ Proof.
  induction s; simpl; intros.
  intuition_in.
  inv bst; inv avl.
- rewrite IHs2; auto.
- destruct (f t); auto.
- rewrite IHs1; auto.
- destruct (f t); auto.
+ rewrite IHs2 by (destruct (f t); auto).
+ rewrite IHs1 by (destruct (f t); auto).
  case_eq (f t); intros.
  rewrite (add_in); auto.
  intuition_in.
@@ -1786,11 +1784,9 @@ Proof.
  intuition_in.
  destruct acc as [acct accf]; simpl in *.
  inv bst; inv avl.
- rewrite IHs2; auto.
- destruct (f t); auto.
- apply partition_acc_avl_1; simpl; auto.
- rewrite IHs1; auto.
- destruct (f t); simpl; auto.
+ rewrite IHs2 by 
+  (destruct (f t); auto; apply partition_acc_avl_1; simpl; auto).
+ rewrite IHs1 by (destruct (f t); simpl; auto).
  case_eq (f t); simpl; intros.
  rewrite (add_in); auto.
  intuition_in.
@@ -1799,7 +1795,7 @@ Proof.
  intuition_in.
  rewrite (H1 _ _ H8) in H9.
  rewrite H in H9; discriminate.
-Qed. 
+Qed.
 
 Lemma partition_acc_in_2 : forall s acc, avl s -> avl acc#2 -> 
  compat_bool X.eq f -> forall x : elt, 
@@ -1810,11 +1806,9 @@ Proof.
  intuition_in.
  destruct acc as [acct accf]; simpl in *.
  inv bst; inv avl.
- rewrite IHs2; auto.
- destruct (f t); auto.
- apply partition_acc_avl_2; simpl; auto.
- rewrite IHs1; auto.
- destruct (f t); simpl; auto.
+ rewrite IHs2 by 
+  (destruct (f t); auto; apply partition_acc_avl_2; simpl; auto).
+ rewrite IHs1 by (destruct (f t); simpl; auto).
  case_eq (f t); simpl; intros.
  intuition.
  intuition_in.
@@ -2598,10 +2592,10 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  unfold partition, filter, Equal, In; simpl ;intros H a.
  rewrite Raw.partition_in_2; auto.
  rewrite Raw.filter_in; intuition.
- red; intros.
- f_equal; auto.
- destruct (f a); auto.
+ rewrite H2; auto.
  destruct (f a); auto.
+ red; intros; f_equal.
+ rewrite (H _ _ H0); auto.
  Qed.
 
  End Filter.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index d6a92b673..1c8bac6d9 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -146,57 +146,43 @@ the above form:
         together.
 
         XXX: This tactic and the similar subsequent ones should
-        have been defined using [autorewrite].  However, there
-        is a bug in the order that Coq generates subgoals when
-        rewriting using a setoid.  In order to work around this
-        bug, these tactics had to be written out in an explicit
-        way.  When the bug is fixed these tactics will break!!
-        *)
+        have been defined using [autorewrite]. However, dealing
+        with multiples rewrite sites and side-conditions is 
+        done more cleverly with the following explicit 
+        analysis of goals. *)
+
+    Ltac or_not_l_iff P Q tac := 
+      (rewrite (or_not_l_iff_1 P Q) by tac) || 
+      (rewrite (or_not_l_iff_2 P Q) by tac).
+
+    Ltac or_not_r_iff P Q tac := 
+      (rewrite (or_not_r_iff_1 P Q) by tac) || 
+      (rewrite (or_not_r_iff_2 P Q) by tac).
+
+    Ltac or_not_l_iff_in P Q H tac := 
+      (rewrite (or_not_l_iff_1 P Q) in H by tac) || 
+      (rewrite (or_not_l_iff_2 P Q) in H by tac).
+
+    Ltac or_not_r_iff_in P Q H tac := 
+      (rewrite (or_not_r_iff_1 P Q) in H by tac) || 
+      (rewrite (or_not_r_iff_2 P Q) in H by tac).
 
     Tactic Notation "push" "not" "using" ident(db) :=
+      let dec := solve_decidable using db in 
       unfold not, iff;
       repeat (
         match goal with
-        (** simplification by not_true_iff *)
-        | |- context [True -> False] =>
-          rewrite not_true_iff
-        (** simplification by not_false_iff *)
-        | |- context [False -> False] =>
-          rewrite not_false_iff
-        (** simplification by not_not_iff *)
-        | |- context [(?P -> False) -> False] =>
-          rewrite (not_not_iff P);
-            [ solve_decidable using db | ]
-        (** simplification by contrapositive *)
-        | |- context [(?P -> False) -> (?Q -> False)] =>
-          rewrite (contrapositive P Q);
-            [ solve_decidable using db | ]
-        (** simplification by or_not_l_iff_1/_2 *)
-        | |- context [(?P -> False) \/ ?Q] =>
-          (rewrite (or_not_l_iff_1 P Q);
-            [ solve_decidable using db | ]) ||
-          (rewrite (or_not_l_iff_2 P Q);
-            [ solve_decidable using db | ])
-        (** simplification by or_not_r_iff_1/_2 *)
-        | |- context [?P \/ (?Q -> False)] =>
-          (rewrite (or_not_r_iff_1 P Q);
-            [ solve_decidable using db | ]) ||
-          (rewrite (or_not_r_iff_2 P Q);
-            [ solve_decidable using db | ])
-        (** simplification by imp_not_l *)
-        | |- context [(?P -> False) -> ?Q] =>
-          rewrite (imp_not_l P Q);
-            [ solve_decidable using db | ]
-        (** rewriting by not_or_iff *)
-        | |- context [?P \/ ?Q -> False] =>
-          rewrite (not_or_iff P Q)
-        (** rewriting by not_and_iff *)
-        | |- context [?P /\ ?Q -> False] =>
-          rewrite (not_and_iff P Q)
-        (** rewriting by not_imp_iff *)
-        | |- context [(?P -> ?Q) -> False] =>
-          rewrite (not_imp_iff P Q);
-            [ solve_decidable using db | ]
+        | |- context [True -> False] => rewrite not_true_iff
+        | |- context [False -> False] => rewrite not_false_iff
+        | |- context [(?P -> False) -> False] => rewrite (not_not_iff P) by dec
+        | |- context [(?P -> False) -> (?Q -> False)] => 
+            rewrite (contrapositive P Q) by dec
+        | |- context [(?P -> False) \/ ?Q] => or_not_l_iff P Q dec
+        | |- context [?P \/ (?Q -> False)] => or_not_r_iff P Q dec
+        | |- context [(?P -> False) -> ?Q] => rewrite (imp_not_l P Q) by dec
+        | |- context [?P \/ ?Q -> False] => rewrite (not_or_iff P Q)
+        | |- context [?P /\ ?Q -> False] => rewrite (not_and_iff P Q)
+        | |- context [(?P -> ?Q) -> False] => rewrite (not_imp_iff P Q) by dec
         end);
       fold any not.
 
@@ -205,49 +191,24 @@ the above form:
 
     Tactic Notation
       "push" "not" "in" "*" "|-" "using" ident(db) :=
+      let dec := solve_decidable using db in 
       unfold not, iff in * |-;
       repeat (
         match goal with
-        (** simplification by not_true_iff *)
-        | H: context [True -> False] |- _ =>
-          rewrite not_true_iff in H
-        (** simplification by not_false_iff *)
-        | H: context [False -> False] |- _ =>
-          rewrite not_false_iff in H
-        (** simplification by not_not_iff *)
-        | H: context [(?P -> False) -> False] |- _ =>
-          rewrite (not_not_iff P) in H;
-            [ | solve_decidable using db ]
-        (** simplification by contrapositive *)
+        | H: context [True -> False] |- _ => rewrite not_true_iff in H
+        | H: context [False -> False] |- _ => rewrite not_false_iff in H
+        | H: context [(?P -> False) -> False] |- _ => 
+          rewrite (not_not_iff P) in H by dec
         | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
-          rewrite (contrapositive P Q) in H;
-            [ | solve_decidable using db ]
-        (** simplification by or_not_l_iff_1/_2 *)
-        | H: context [(?P -> False) \/ ?Q] |- _ =>
-          (rewrite (or_not_l_iff_1 P Q) in H;
-            [ | solve_decidable using db ]) ||
-          (rewrite (or_not_l_iff_2 P Q) in H;
-            [ | solve_decidable using db ])
-        (** simplification by or_not_r_iff_1/_2 *)
-        | H: context [?P \/ (?Q -> False)] |- _ =>
-          (rewrite (or_not_r_iff_1 P Q) in H;
-            [ | solve_decidable using db ]) ||
-          (rewrite (or_not_r_iff_2 P Q) in H;
-            [ | solve_decidable using db ])
-        (** simplification by imp_not_l *)
-        | H: context [(?P -> False) -> ?Q] |- _ =>
-          rewrite (imp_not_l P Q) in H;
-            [ | solve_decidable using db ]
-        (** rewriting by not_or_iff *)
-        | H: context [?P \/ ?Q -> False] |- _ =>
-          rewrite (not_or_iff P Q) in H
-        (** rewriting by not_and_iff *)
-        | H: context [?P /\ ?Q -> False] |- _ =>
-          rewrite (not_and_iff P Q) in H
-        (** rewriting by not_imp_iff *)
-        | H: context [(?P -> ?Q) -> False] |- _ =>
-          rewrite (not_imp_iff P Q) in H;
-            [ | solve_decidable using db ]
+          rewrite (contrapositive P Q) in H by dec
+        | H: context [(?P -> False) \/ ?Q] |- _ => or_not_l_iff_in P Q H dec
+        | H: context [?P \/ (?Q -> False)] |- _ => or_not_r_iff_in P Q H dec
+        | H: context [(?P -> False) -> ?Q] |- _ => 
+          rewrite (imp_not_l P Q) in H by dec
+        | H: context [?P \/ ?Q -> False] |- _ => rewrite (not_or_iff P Q) in H
+        | H: context [?P /\ ?Q -> False] |- _ => rewrite (not_and_iff P Q) in H
+        | H: context [(?P -> ?Q) -> False] |- _ => 
+          rewrite (not_imp_iff P Q) in H by dec
         end);
       fold any not.
 
@@ -272,12 +233,14 @@ the above form:
       (R \/ ~ (P /\ Q)) ->
       (~ R \/ (P /\ Q)) ->
       (~ P -> R) ->
-      (~ ((R -> P) \/ (R -> Q))) ->
+      (~ ((R -> P) \/ (Q -> R))) ->
       (~ (P /\ R)) ->
       (~ (P -> R)) ->
       True.
     Proof.
-      intros. push not in *. tauto.
+      intros. push not in *.
+       (* note that ~(R->P) remains (since R isnt decidable) *)
+      tauto.
     Qed.
 
     (** [pull not using db] will pull as many negations as
@@ -289,53 +252,24 @@ the above form:
         the hypotheses and goal together. *)
 
     Tactic Notation "pull" "not" "using" ident(db) :=
+      let dec := solve_decidable using db in 
       unfold not, iff;
       repeat (
         match goal with
-        (** simplification by not_true_iff *)
-        | |- context [True -> False] =>
-          rewrite not_true_iff
-        (** simplification by not_false_iff *)
-        | |- context [False -> False] =>
-          rewrite not_false_iff
-        (** simplification by not_not_iff *)
-        | |- context [(?P -> False) -> False] =>
-          rewrite (not_not_iff P);
-            [ solve_decidable using db | ]
-        (** simplification by contrapositive *)
+        | |- context [True -> False] => rewrite not_true_iff
+        | |- context [False -> False] => rewrite not_false_iff
+        | |- context [(?P -> False) -> False] => rewrite (not_not_iff P) by dec
         | |- context [(?P -> False) -> (?Q -> False)] =>
-          rewrite (contrapositive P Q);
-            [ solve_decidable using db | ]
-        (** simplification by or_not_l_iff_1/_2 *)
-        | |- context [(?P -> False) \/ ?Q] =>
-          (rewrite (or_not_l_iff_1 P Q);
-            [ solve_decidable using db | ]) ||
-          (rewrite (or_not_l_iff_2 P Q);
-            [ solve_decidable using db | ])
-        (** simplification by or_not_r_iff_1/_2 *)
-        | |- context [?P \/ (?Q -> False)] =>
-          (rewrite (or_not_r_iff_1 P Q);
-            [ solve_decidable using db | ]) ||
-          (rewrite (or_not_r_iff_2 P Q);
-            [ solve_decidable using db | ])
-        (** simplification by imp_not_l *)
-        | |- context [(?P -> False) -> ?Q] =>
-          rewrite (imp_not_l P Q);
-            [ solve_decidable using db | ]
-        (** rewriting by not_or_iff *)
+          rewrite (contrapositive P Q) by dec
+        | |- context [(?P -> False) \/ ?Q] => or_not_l_iff P Q dec
+        | |- context [?P \/ (?Q -> False)] => or_not_r_iff P Q dec
+        | |- context [(?P -> False) -> ?Q] => rewrite (imp_not_l P Q) by dec
         | |- context [(?P -> False) /\ (?Q -> False)] =>
           rewrite <- (not_or_iff P Q)
-        (** rewriting by not_and_iff *)
-        | |- context [?P -> ?Q -> False] =>
-          rewrite <- (not_and_iff P Q)
-        (** rewriting by not_imp_iff *)
-        | |- context [?P /\ (?Q -> False)] =>
-          rewrite <- (not_imp_iff P Q);
-            [ solve_decidable using db | ]
-        (** rewriting by not_imp_rev_iff *)
-        | |- context [(?Q -> False) /\ ?P] =>
-          rewrite <- (not_imp_rev_iff P Q);
-            [ solve_decidable using db | ]
+        | |- context [?P -> ?Q -> False] => rewrite <- (not_and_iff P Q)
+        | |- context [?P /\ (?Q -> False)] => rewrite <- (not_imp_iff P Q) by dec
+        | |- context [(?Q -> False) /\ ?P] => 
+          rewrite <- (not_imp_rev_iff P Q) by dec
         end);
       fold any not.
 
@@ -344,53 +278,28 @@ the above form:
 
     Tactic Notation
       "pull" "not" "in" "*" "|-" "using" ident(db) :=
+      let dec := solve_decidable using db in 
       unfold not, iff in * |-;
       repeat (
         match goal with
-        (** simplification by not_true_iff *)
-        | H: context [True -> False] |- _ =>
-          rewrite not_true_iff in H
-        (** simplification by not_false_iff *)
-        | H: context [False -> False] |- _ =>
-          rewrite not_false_iff in H
-        (** simplification by not_not_iff *)
+        | H: context [True -> False] |- _ => rewrite not_true_iff in H
+        | H: context [False -> False] |- _ => rewrite not_false_iff in H
         | H: context [(?P -> False) -> False] |- _ =>
-          rewrite (not_not_iff P) in H;
-            [ | solve_decidable using db ]
-        (** simplification by contrapositive *)
+          rewrite (not_not_iff P) in H by dec
         | H: context [(?P -> False) -> (?Q -> False)] |- _ =>
-          rewrite (contrapositive P Q) in H;
-            [ | solve_decidable using db ]
-        (** simplification by or_not_l_iff_1/_2 *)
-        | H: context [(?P -> False) \/ ?Q] |- _ =>
-          (rewrite (or_not_l_iff_1 P Q) in H;
-            [ | solve_decidable using db ]) ||
-          (rewrite (or_not_l_iff_2 P Q) in H;
-            [ | solve_decidable using db ])
-        (** simplification by or_not_r_iff_1/_2 *)
-        | H: context [?P \/ (?Q -> False)] |- _ =>
-          (rewrite (or_not_r_iff_1 P Q) in H;
-            [ | solve_decidable using db ]) ||
-          (rewrite (or_not_r_iff_2 P Q) in H;
-            [ | solve_decidable using db ])
-        (** simplification by imp_not_l *)
+          rewrite (contrapositive P Q) in H by dec
+        | H: context [(?P -> False) \/ ?Q] |- _ => or_not_l_iff_in P Q H dec
+        | H: context [?P \/ (?Q -> False)] |- _ => or_not_r_iff_in P Q H dec
         | H: context [(?P -> False) -> ?Q] |- _ =>
-          rewrite (imp_not_l P Q) in H;
-            [ | solve_decidable using db ]
-        (** rewriting by not_or_iff *)
+          rewrite (imp_not_l P Q) in H by dec
         | H: context [(?P -> False) /\ (?Q -> False)] |- _ =>
-          rewrite <- (not_or_iff P Q) in H
-        (** rewriting by not_and_iff *)
-        | H: context [?P -> ?Q -> False] |- _ =>
+          rewrite <- (not_or_iff P Q) in H 
+        | H: context [?P -> ?Q -> False] |- _ => 
           rewrite <- (not_and_iff P Q) in H
-        (** rewriting by not_imp_iff *)
         | H: context [?P /\ (?Q -> False)] |- _ =>
-          rewrite <- (not_imp_iff P Q) in H;
-            [ | solve_decidable using db ]
-        (** rewriting by not_imp_rev_iff *)
+          rewrite <- (not_imp_iff P Q) in H by dec
         | H: context [(?Q -> False) /\ ?P] |- _ =>
-          rewrite <- (not_imp_rev_iff P Q) in H;
-            [ | solve_decidable using db ]
+          rewrite <- (not_imp_rev_iff P Q) in H by dec
         end);
       fold any not.
 
@@ -415,7 +324,7 @@ the above form:
       (R \/ ~ (P /\ Q)) ->
       (~ R \/ (P /\ Q)) ->
       (~ P -> R) ->
-      (~ (R -> P) /\ ~ (R -> Q)) ->
+      (~ (R -> P) /\ ~ (Q -> R)) ->
       (~ P \/ ~ R) ->
       (P /\ ~ R) ->
       (~ R /\ P) ->
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index f3da02a83..1ea669eb8 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -859,8 +859,8 @@ Module OrdProperties (M:S).
   apply (@filter_sort _ E.eq); auto with set; eauto with set.
   constructor; auto.
   apply (@filter_sort _ E.eq); auto with set; eauto with set.
-  rewrite ME.Inf_alt; auto; intros.
-  apply (@filter_sort _ E.eq); auto with set; eauto with set.
+  rewrite ME.Inf_alt by (apply (@filter_sort _ E.eq); eauto with set).
+  intros.
   rewrite filter_InA in H1; auto; destruct H1.
   rewrite leb_1 in H2.
   rewrite <- elements_iff in H1.