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

4 files changed, 56 insertions, 79 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.
diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 11e3bdf9d0..c2990f2830 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -77,7 +77,7 @@ Proof. reflexivity. Qed.
 Lemma le_refl : forall x, x<=x.
 Proof. intros; rewrite le_lteq; right; reflexivity. Qed.
 
-Lemma lt_antirefl : forall x, ~ x<x.
+Lemma lt_irrefl : forall x, ~ x<x.
 Proof. intros; apply StrictOrder_Irreflexive. Qed.
 
 (** Symmetry rules *)
@@ -133,7 +133,7 @@ Proof. eauto using eq_trans, eq_sym. Qed.
 Lemma not_neq_eq : forall x y, ~~x==y -> x==y.
 Proof.
 intros x y H. destruct (lt_total x y) as [H'|[H'|H']]; auto;
- destruct H; intro H; rewrite H in H'; eapply lt_antirefl; eauto.
+ destruct H; intro H; rewrite H in H'; eapply lt_irrefl; eauto.
 Qed.
 
 Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
@@ -208,7 +208,7 @@ Ltac order_prepare :=
 Ltac order_loop :=
  match goal with
  (* First, successful situations *)
- | H : ?x < ?x |- _ => exact (lt_antirefl H)
+ | H : ?x < ?x |- _ => exact (lt_irrefl H)
  | H : ~ ?x == ?x |- _ => exact (H (eq_refl x))
  (* Second, useless hyps *)
  | H : ?x <= ?x |- _ => clear H; order_loop
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index e223dba43b..7258fe52f2 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -96,8 +96,9 @@ Module OrderedTypeFacts (Import O: OrderedType).
     change lt with OrderElts.lt in *;
     OrderTac.order.
 
-  (** The following lemmas are re-phrasing of eq_equiv and lt_strorder.
-      Interest: compatibility, simple use (e.g. in tactic order), etc. *)
+  (** The following lemmas are either re-phrasing of [eq_equiv] and
+      [lt_strorder] or immediately provable by [order]. Interest:
+      compatibility, test of order, etc *)
 
   Definition eq_refl (x:t) : x==x := Equivalence_Reflexive x.
 
@@ -109,32 +110,9 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
    StrictOrder_Transitive x y z.
 
-  Definition lt_antirefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
+  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
 
-  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
-  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
-  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
-  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
-  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
-  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
-
-  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
-  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
-  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
-  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
-  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
-  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
-  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
-  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
-  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
-  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
-  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
-
-  Hint Resolve eq_trans eq_refl lt_trans.
-  Hint Immediate eq_sym eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
-  Hint Resolve gt_not_eq eq_not_lt.
-  Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
+  (** Some more about [compare] *)
 
   Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
   Proof.
@@ -184,7 +162,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
   Proof.
-   intros; elim_compare x y; [ right | left | right ]; auto.
+   intros; elim_compare x y; [ right | left | right ]; order.
   Defined.
 
   Definition eqb x y : bool := if eq_dec x y then true else false.
@@ -253,6 +231,36 @@ Hint Immediate In_eq Inf_lt.
 
 End OrderedTypeFacts.
 
+
+(** Some tests of [order] : is it at least capable of
+    proving some basic properties ? *)
+
+Module OrderedTypeTest (O:OrderedType).
+  Module Import MO := OrderedTypeFacts O.
+  Local Open Scope order.
+  Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.
+  Lemma lt_eq x y z : x<y -> y==z -> x<z. Proof. order. Qed.
+  Lemma eq_lt x y z : x==y -> y<z -> x<z. Proof. order. Qed.
+  Lemma le_eq x y z : x<=y -> y==z -> x<=z. Proof. order. Qed.
+  Lemma eq_le x y z : x==y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma neq_eq x y z : ~x==y -> y==z -> ~x==z. Proof. order. Qed.
+  Lemma eq_neq x y z : x==y -> ~y==z -> ~x==z. Proof. order. Qed.
+  Lemma le_lt_trans x y z : x<=y -> y<z -> x<z. Proof. order. Qed.
+  Lemma lt_le_trans x y z : x<y -> y<=z -> x<z. Proof. order. Qed.
+  Lemma le_trans x y z : x<=y -> y<=z -> x<=z. Proof. order. Qed.
+  Lemma le_antisym x y : x<=y -> y<=x -> x==y. Proof. order. Qed.
+  Lemma le_neq x y : x<=y -> ~x==y -> x<y. Proof. order. Qed.
+  Lemma neq_sym x y : ~x==y -> ~y==x. Proof. order. Qed.
+  Lemma lt_le x y : x<y -> x<=y. Proof. order. Qed.
+  Lemma gt_not_eq x y : y<x -> ~x==y. Proof. order. Qed.
+  Lemma eq_not_lt x y : x==y -> ~x<y. Proof. order. Qed.
+  Lemma eq_not_gt x y : x==y -> ~ y<x. Proof. order. Qed.
+  Lemma lt_not_gt x y : x<y -> ~ y<x. Proof. order. Qed.
+End OrderedTypeTest.
+
+
+(** * Relations over pairs (TO MIGRATE in some TypeClasses file) *)
+
 Definition ProdRel {A B}(RA:relation A)(RB:relation B) : relation (A*B) :=
  fun p p' => RA (fst p) (fst p') /\ RB (snd p) (snd p').
 
@@ -343,17 +351,6 @@ Module KeyOrderedType(Import O:OrderedType).
   Global Instance eqke_eqk : subrelation eqke eqk.
   Proof. unfold eqke, eqk; auto with *. Qed.
 
-(*
-  (* ltk ignore the second components *)
-
-  Lemma ltk_right_r : forall x k e e', ltk x (k,e) -> ltk x (k,e').
-  Proof. auto. Qed.
-
-  Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
-  Proof. auto. Qed.
-  Hint Immediate ltk_right_r ltk_right_l.
-*)
-
   (* eqk, eqke are equalities, ltk is a strict order *)
 
   Global Instance eqk_equiv : Equivalence eqk.
@@ -531,3 +528,4 @@ Module KeyOrderedType(Import O:OrderedType).
  Hint Resolve In_inv_2 In_inv_3.
 
 End KeyOrderedType.
+