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, 40 insertions, 42 deletions

diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index 11e3bdf9d..c2990f283 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 e223dba43..7258fe52f 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.
+