OrderedType2 : trivial lemmas are turned into tests for order.

In particular we remove them from the hint db, a few autos become
calls to order. Moreover, lt_antirefl --> lt_irrefl for uniformity.

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

2 files changed, 16 insertions, 37 deletions

diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index e38bf171ef..70be28f870 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -859,19 +859,8 @@ Proof. intros; apply add_spec'. Qed.
 
 Instance add_ok s x `(Ok s) : Ok (add x s).
 Proof.
- induct s x; auto; apply bal_ok; auto.
- (* lt_tree -> lt_tree (add ...) *)
- red; red in H3.
- intros.
- rewrite add_spec' in H.
- intuition.
- eauto.
- (* gt_tree -> gt_tree (add ...) *)
- red; red in H3.
- intros.
- rewrite add_spec' in H.
- intuition.
- setoid_replace y with x; auto.
+ induct s x; auto; apply bal_ok; auto;
+  intros y; rewrite add_spec'; intuition; order.
 Qed.
 
 
@@ -1032,7 +1021,7 @@ Proof.
  discriminate.
  intros x y0 U V W.
  inversion V; clear V; subst.
- inv; auto.
+ inv; order.
  intros; inv; auto.
  assert (X.lt x y) by (apply H4; apply min_elt_spec1; auto).
  order.
@@ -1067,7 +1056,7 @@ Proof.
  discriminate.
  intros x y0 U V W.
  inversion V; clear V; subst.
- inv; auto.
+ inv; order.
  intros; inv; auto.
  assert (X.lt y x1) by auto.
  assert (~ X.lt x x1) by auto.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 24e889eeed..ab9c69afb8 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -934,32 +934,24 @@ Module OrdProperties (M:Sets).
 
   Lemma gtb_1 : forall x y, gtb x y = true <-> E.lt y x.
   Proof.
-   intros; unfold gtb; ME.elim_compare x y; intuition; try discriminate; ME.order.
+   intros; rewrite <- ME.compare_gt_iff. unfold gtb.
+   destruct E.compare; intuition; try discriminate.
   Qed.
 
   Lemma leb_1 : forall x y, leb x y = true <-> ~E.lt y x.
   Proof.
-   intros; unfold leb, gtb; ME.elim_compare x y; intuition; try discriminate; ME.order.
+   intros; rewrite <- ME.compare_gt_iff. unfold leb, gtb.
+   destruct E.compare; intuition; try discriminate.
   Qed.
 
-  Lemma gtb_compat : forall x, Proper (E.eq==>Logic.eq) (gtb x).
+  Instance gtb_compat x : Proper (E.eq==>Logic.eq) (gtb x).
   Proof.
-   red; intros x a b H.
-   generalize (gtb_1 x a)(gtb_1 x b); destruct (gtb x a); destruct (gtb x b); auto.
-   intros.
-   symmetry; rewrite H1.
-   apply ME.eq_lt with a; auto.
-   rewrite <- H0; auto.
-   intros.
-   rewrite H0.
-   apply ME.eq_lt with b; auto.
-   rewrite <- H1; auto.
+   intros x a b H. unfold gtb. rewrite H; auto.
   Qed.
 
-  Lemma leb_compat : forall x, Proper (E.eq==>Logic.eq) (leb x).
+  Instance leb_compat x : Proper (E.eq==>Logic.eq) (leb x).
   Proof.
-   red; intros x a b H; unfold leb.
-   f_equal; apply gtb_compat; auto.
+   intros x a b H; unfold leb. rewrite H; auto.
   Qed.
   Hint Resolve gtb_compat leb_compat.
 
@@ -1021,10 +1013,9 @@ Module OrdProperties (M:Sets).
   apply sort_equivlistA_eqlistA; auto with set.
   apply (@SortA_app _ E.eq); auto with *.
   intros.
-  inversion_clear H2.
+  invlist InA.
   rewrite <- elements_iff in H1.
-  apply ME.lt_eq with x; auto.
-  inversion H3.
+  setoid_replace y with x; auto.
   red; intros a.
   rewrite InA_app_iff, InA_cons, InA_nil, <-!elements_iff, (H0 a)
    by (auto with *).
@@ -1040,10 +1031,9 @@ Module OrdProperties (M:Sets).
   change (sort E.lt ((x::nil) ++ elements s)).
   apply (@SortA_app _ E.eq); auto with *.
   intros.
-  inversion_clear H1.
+  invlist InA.
   rewrite <- elements_iff in H2.
-  apply ME.eq_lt with x; auto.
-  inversion H3.
+  setoid_replace x0 with x; auto.
   red; intros a.
   rewrite InA_cons, <- !elements_iff, (H0 a); intuition.
   Qed.