Structure/OrderTac.v : highlight the "order" tactic by isolating it from FSets, and improve it

 As soon as you have a eq, a lt and a le (that may be lt\/eq, or (complement (flip (lt)))
 and a few basic properties over them, you can instantiate functor MakeOrderTac
 and gain an "order" tactic. See comments in the file for the scope of this tactic.

 NB: order doesn't call auto anymore. It only searches for a contradiction in the
 current set of (in)equalities (after the goal was optionally turned into hyp
 by double negation). Thanks to S. Lescuyer for his suggestions about this tactic.

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

3 files changed, 357 insertions, 365 deletions

diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
new file mode 100644
index 000000000..11e3bdf9d
--- /dev/null
+++ b/theories/Structures/OrderTac.v
@@ -0,0 +1,255 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+Require Import Setoid Morphisms.
+Set Implicit Arguments.
+
+(** * The order tactic *)
+
+(** This tactic is designed to solve systems of (in)equations
+    involving [eq], [lt], [le] and [~eq] on some type. This tactic is
+    domain-agnostic; it will only use equivalence+order axioms, and
+    not analyze elements of the domain. Hypothesis or goal of the form
+    [~lt] or [~le] are initially turned into [le] and [lt], other
+    parts of the goal are ignored. This initial preparation of the
+    goal is the only moment where totality is used. In particular,
+    the core of the tactic only proceeds by saturation of transitivity
+    and similar properties, and does not perform case splitting.
+    The tactic will fail if it doesn't solve the goal. *)
+
+
+(** ** The requirements of the tactic : an equivalence [eq],
+   a strict order [lt] total and compatible with [eq], and
+   a larger order [le] synonym of [lt\/eq]. *)
+
+Module Type OrderTacSig.
+
+Parameter Inline t : Type.
+Parameters eq lt le : t -> t -> Prop.
+Instance eq_equiv : Equivalence eq.
+Instance lt_strorder : StrictOrder lt.
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Parameter lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
+Parameter le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+
+End OrderTacSig.
+
+(** NB : we should _not_ use "Inline" for these predicates,
+   otherwise the ltac matching will not work properly later. *)
+
+(** An abstract vision of the predicates. This allows a one-line
+    statement for interesting transitivity properties: for instance
+    [trans_ord LE LE = LE] will imply later [le x y -> le y z -> le x z].
+ *)
+
+Inductive ord := EQ | LT | LE.
+Definition trans_ord o o' :=
+ match o, o' with
+ | EQ, _ => o'
+ | _, EQ => o
+ | LE, LE => LE
+ | _, _ => LT
+ end.
+Infix "+" := trans_ord : order.
+
+(** ** [MakeOrderTac] : The functor providing the order tactic. *)
+
+Module MakeOrderTac(Import O:OrderTacSig).
+
+Local Open Scope order.
+
+Infix "==" := eq (at level 70, no associativity) : order.
+Infix "<" := lt : order.
+Infix "<=" := le : order.
+
+(** ** Properties that will be used by the tactic *)
+
+(** Reflexivity rules *)
+
+Lemma eq_refl : forall x, x==x.
+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.
+Proof. intros; apply StrictOrder_Irreflexive. Qed.
+
+(** Symmetry rules *)
+
+Lemma eq_sym : forall x y, x==y -> y==x.
+Proof. auto with *. Qed.
+
+Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
+Proof.
+ intros x y; rewrite 2 le_lteq. intuition.
+ elim (StrictOrder_Irreflexive x); transitivity y; auto.
+Qed.
+
+Lemma neq_sym : forall x y, ~x==y -> ~y==x.
+Proof. auto using eq_sym. Qed.
+
+(** Transitivity rules : first, a generic formulation, then instances*)
+
+Ltac subst_eqns :=
+ match goal with
+   | H : _==_ |- _ => (rewrite H || rewrite <- H); clear H; subst_eqns
+   | _ => idtac
+ end.
+
+Definition interp_ord o :=
+ match o with EQ => eq | LT => lt | LE => le end.
+Notation "#" := interp_ord : order.
+
+Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
+Proof.
+destruct o, o'; simpl; intros x y z; rewrite ?le_lteq; intuition;
+ subst_eqns; eauto using (StrictOrder_Transitive x y z) with *.
+Qed.
+
+Definition eq_trans x y z : x==y -> y==z -> x==z := trans EQ EQ x y z.
+Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans LE LE x y z.
+Definition lt_trans x y z : x<y -> y<z -> x<z := trans LT LT x y z.
+Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans LE LT x y z.
+Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans LT LE x y z.
+Definition eq_lt x y z : x==y -> y<z -> x<z := trans EQ LT x y z.
+Definition lt_eq x y z : x<y -> y==z -> x<z := trans LT EQ x y z.
+Definition eq_le x y z : x==y -> y<=z -> x<=z := trans EQ LE x y z.
+Definition le_eq x y z : x<=y -> y==z -> x<=z := trans LE EQ x y z.
+
+Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z.
+Proof. eauto using eq_trans, eq_sym. Qed.
+
+(** (double) negation rules *)
+
+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.
+Qed.
+
+Lemma not_ge_lt : forall x y, ~y<=x -> x<y.
+Proof.
+intros x y H. destruct (lt_total x y); auto.
+destruct H. rewrite le_lteq. intuition.
+Qed.
+
+Lemma not_gt_le : forall x y, ~y<x -> x<=y.
+Proof.
+intros x y H. rewrite le_lteq. generalize (lt_total x y); intuition.
+Qed.
+
+Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
+Proof. auto using not_ge_lt, le_antisym. Qed.
+
+
+(** ** The tactic itself *)
+
+(** order_eq : replace x by y in all (in)equations hyps thanks
+   to equality EQ (where eq has been hidden in order to avoid
+   self-rewriting), then discard EQ. *)
+
+Ltac order_rewr x eqn :=
+ (* NB: we could use the real rewrite here, but proofs would be uglier. *)
+ let rewr H t := generalize t; clear H; intro H
+ in
+ match goal with
+ | H : x == _ |- _ => rewr H (eq_trans (eq_sym eqn) H); order_rewr x eqn
+ | H : _ == x |- _ => rewr H (eq_trans H eqn); order_rewr x eqn
+ | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym eqn) H); order_rewr x eqn
+ | H : ~_ == x |- _ => rewr H (neq_eq H eqn); order_rewr x eqn
+ | H : x < _ |- _ => rewr H (eq_lt (eq_sym eqn) H); order_rewr x eqn
+ | H : _ < x |- _ => rewr H (lt_eq H eqn); order_rewr x eqn
+ | H : x <= _ |- _ => rewr H (eq_le (eq_sym eqn) H); order_rewr x eqn
+ | H : _ <= x |- _ => rewr H (le_eq H eqn); order_rewr x eqn
+ | _ => clear eqn
+end.
+
+Ltac order_eq x y eqn :=
+ match x with
+ | y => clear eqn
+ | _ => change (#EQ x y) in eqn; order_rewr x eqn
+ end.
+
+(** Goal preparation : We turn all negative hyps into positive ones
+  and try to prove False from the inverse of the current goal.
+  These steps require totality of our order. After this preparation,
+  order only deals with the context, and tries to prove False.
+  Hypotheses of the form [A -> False] are also folded in [~A]
+  for convenience (i.e. cope with the mess left by intuition). *)
+
+Ltac order_prepare :=
+ match goal with
+ | H : ?A -> False |- _ => change (~A) in H; order_prepare
+ | H : ~ _ < _ |- _ => apply not_gt_le in H; order_prepare
+ | H : ~ _ <= _ |- _ => apply not_ge_lt in H; order_prepare
+ | |- ~ _ => intro
+ (* Two special cases. This handling is optional but gives nicer proofs. *)
+ | |- ?x == ?x => exact (eq_refl x)
+ | |- ?x <= ?x => exact (le_refl x)
+ | |- ?x < ?x => exfalso
+ (* Any cool stuff left in the goal becomes an hyp via double neg. *)
+ | |- _ == _ => apply not_neq_eq; intro
+ | |- _ < _ => apply not_ge_lt; intro
+ | |- _ <= _ => apply not_gt_le; intro
+ | _ => exfalso
+ end.
+
+(** We now try to prove False from the various [< <= == !=] hypothesis *)
+
+Ltac order_loop :=
+ match goal with
+ (* First, successful situations *)
+ | H : ?x < ?x |- _ => exact (lt_antirefl H)
+ | H : ~ ?x == ?x |- _ => exact (H (eq_refl x))
+ (* Second, useless hyps *)
+ | H : ?x <= ?x |- _ => clear H; order_loop
+ (* Third, we eliminate equalities *)
+ | H : ?x == ?y |- _ => order_eq x y H; order_loop
+ (* Simultaneous le and ge is eq *)
+ | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
+     generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
+ (* Simultaneous le and ~eq is lt *)
+ | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
+     generalize (le_neq_lt H1 H2); clear H1 H2; intro; order_loop
+ | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
+     generalize (le_neq_lt H1 (neq_sym H2)); clear H1 H2; intro; order_loop
+ (* Transitivity of lt and le *)
+ | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x < z |- _ => fail 1
+      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
+    end
+ | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
+    match goal with
+      | H : x <= z |- _ => fail 1
+      | _ => generalize (le_trans H1 H2); intro; order_loop
+    end
+ | _ => idtac
+end.
+
+(** The complete tactic. *)
+
+Ltac order := intros; order_prepare; order_loop; fail.
+
+End MakeOrderTac.
+
+(** For example of use of this tactic, see for instance [OrderedType] *)
\ No newline at end of file
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 2a75f44fd..e582db3ea 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export SetoidList.
+Require Export SetoidList Morphisms OrderTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -67,11 +67,17 @@ End MOT_to_OT.
 
 Module OrderedTypeFacts (Import O: OrderedType).
 
+  Instance eq_equiv : Equivalence eq.
+  Proof. split; [ exact eq_refl | exact eq_sym | exact eq_trans ]. Qed.
+
   Lemma lt_antirefl : forall x, ~ lt x x.
   Proof.
    intros; intro; absurd (eq x x); auto.
   Qed.
 
+  Instance lt_strorder : StrictOrder lt.
+  Proof. split; [ exact lt_antirefl | exact lt_trans]. Qed.
+
   Lemma lt_eq : forall x y z, lt x y -> eq y z -> lt x z.
   Proof.
    intros; destruct (compare x z); auto.
@@ -86,183 +92,59 @@ Module OrderedTypeFacts (Import O: OrderedType).
    elim (lt_not_eq (lt_trans H0 l)); auto.
   Qed.
 
-  Lemma le_eq : forall x y z, ~lt x y -> eq y z -> ~lt x z.
-  Proof.
-   intros; intro; destruct H; apply lt_eq with z; auto.
-  Qed.
-
-  Lemma eq_le : forall x y z, eq x y -> ~lt y z -> ~lt x z.
-  Proof.
-   intros; intro; destruct H0; apply eq_lt with x; auto.
-  Qed.
-
-  Lemma neq_eq : forall x y z, ~eq x y -> eq y z -> ~eq x z.
-  Proof.
-   intros; intro; destruct H; apply eq_trans with z; auto.
-  Qed.
-
-  Lemma eq_neq : forall x y z, eq x y -> ~eq y z -> ~eq x z.
-  Proof.
-   intros; intro; destruct H0; apply eq_trans with x; auto.
-  Qed.
-
-  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
-
-  Lemma le_lt_trans : forall x y z, ~lt y x -> lt y z -> lt x z.
-  Proof.
-   intros; destruct (compare y x); auto.
-   elim (H l).
-   apply eq_lt with y; auto.
-   apply lt_trans with y; auto.
-  Qed.
-
-  Lemma lt_le_trans : forall x y z, lt x y -> ~lt z y -> lt x z.
-  Proof.
-   intros; destruct (compare z y); auto.
-   elim (H0 l).
-   apply lt_eq with y; auto.
-   apply lt_trans with y; auto.
-  Qed.
-
-  Lemma le_neq : forall x y, ~lt x y -> ~eq x y -> lt y x.
-  Proof.
-   intros; destruct (compare x y); intuition.
-  Qed.
-
-  Lemma le_trans : forall x y z, ~lt y x -> ~lt z y -> ~lt z x.
-  Proof.
-   intros x y z Nyx Nzy Lzx. apply Nyx; clear Nyx.
-   destruct (compare z y).
-   intuition.
-   apply eq_lt with z; auto.
-   apply lt_trans with z; auto.
-  Qed.
-
-  Lemma le_antisym : forall x y, ~lt y x -> ~lt x y -> eq x y.
-  Proof.
-   intros. destruct (compare x y); intuition.
-  Qed.
-
-  Lemma neq_sym : forall x y, ~eq x y -> ~eq y x.
-  Proof.
-   intuition.
-  Qed.
-
-  Infix "==" := eq (at level 70, no associativity) : order.
-  Infix "<" := lt : order.
-  Notation "x <= y" := (~lt y x) : order.
-
-  Local Open Scope order.
-
-(** The order tactic *)
-
-(** This tactic is designed to solve systems of (in)equations
-    involving eq and lt and ~eq and ~lt (i.e. ge). All others
-    parts of the goal will be discarded. This tactic is
-    domain-agnostic : it will only use equivalence+order axioms.
-    Moreover it doesn't directly use totality of the order
-    (but uses above lemmas such as le_trans that rely on it).
-    A typical use of this tactic is transitivity problems. *)
-
-Definition hide_eq := eq.
-
-(** order_eq : replace x by y in all (in)equations thanks
-   to equality EQ (where eq has been hidden in order to avoid
-   self-rewriting). *)
-
-Ltac order_eq x y EQ :=
- let rewr H t := generalize t; clear H; intro H
- in
- match goal with
- | H : x == _ |- _ => rewr H (eq_trans (eq_sym EQ) H); order_eq x y EQ
- | H : _ == x |- _ => rewr H (eq_trans H EQ); order_eq x y EQ
- | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym EQ) H); order_eq x y EQ
- | H : ~_ == x |- _ => rewr H (neq_eq H EQ); order_eq x y EQ
- | H : x < ?z |- _ => rewr H (eq_lt (eq_sym EQ) H); order_eq x y EQ
- | H : ?z < x |- _ => rewr H (lt_eq H EQ); order_eq x y EQ
- | H : x <= ?z |- _ => rewr H (eq_le (eq_sym EQ) H); order_eq x y EQ
- | H : ?z <= x |- _ => rewr H (le_eq H EQ); order_eq x y EQ
- (* NB: no negation in the goal, see below *)
- | |- x == ?z => apply eq_trans with y; [apply EQ| ]; order_eq x y EQ
- | |- ?z == x => apply eq_trans with y; [ | apply (eq_sym EQ) ];
-    order_eq x y EQ
- | |- x < ?z => apply eq_lt with y; [apply EQ| ]; order_eq x y EQ
- | |- ?z < x => apply lt_eq with y; [ | apply (eq_sym EQ) ];
-    order_eq x y EQ
- | _ => clear EQ
-end.
-
-Ltac order_loop := intros; trivial;
- match goal with
- | |- ~ _ => intro; order_loop
- | H : ?A -> False |- _ => change (~A) in H; order_loop
- (* First, successful situations *)
- | H : ?x < ?x |- _ => elim (lt_antirefl H)
- | H : ~ ?x == ?x |- _ => elim (H (eq_refl x))
- | |- ?x == ?x => apply (eq_refl x)
- (* Second, useless hyps or goal *)
- | H : ?x == ?x |- _ => clear H; order_loop
- | H : ?x <= ?x |- _ => clear H; order_loop
- | |- ?x < ?x => exfalso; order_loop
- (* We eliminate equalities *)
- | H : ?x == ?y |- _ =>
-   change (hide_eq x y) in H; order_eq x y H; order_loop
- (* Simultaneous le and ge is eq *)
- | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
-   generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
- (* Simultaneous le and ~eq is lt *)
- | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
-     generalize (le_neq H1 (neq_sym H2)); clear H1 H2; intro; order_loop
- | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
-     generalize (le_neq H1 H2); clear H1 H2; intro; order_loop
- (* Transitivity of lt and le *)
- | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x <= z |- _ => fail 1
-      | _ => generalize (le_trans H1 H2); intro; order_loop
-    end
- | _ => auto
-end.
-
-Ltac order := order_loop; fail.
-
-  Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y.
-  Proof.
-    order.
-  Qed.
-
-  Lemma eq_not_lt : forall x y : t, eq x y -> ~ lt x y.
-  Proof.
-    order.
-  Qed.
+  Instance lt_compat : Proper (eq==>eq==>iff) lt.
+  Proof.
+  apply proper_sym_impl_iff_2; auto with *.
+  intros x x' Hx y y' Hy H.
+  apply eq_lt with x; auto.
+  apply lt_eq with y; auto.
+  Qed.
+
+  Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
+  Proof. intros; destruct (compare x y); auto. Qed.
+
+  Module OrderElts : OrderTacSig
+    with Definition t := t
+    with Definition eq := eq
+    with Definition lt := lt.
+  (* Opaque signature is crucial for ltac to work correctly later *)
+  Definition t := t.
+  Definition eq := eq.
+  Definition lt := lt.
+  Definition le x y := lt x y \/ eq x y.
+  Definition eq_equiv := eq_equiv.
+  Definition lt_strorder := lt_strorder.
+  Definition lt_compat := lt_compat.
+  Lemma lt_total : forall x y, lt x y \/ eq x y \/ lt y x.
+  Proof. intros; destruct (compare x y); auto. Qed.
+  Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+  Proof. unfold le; intuition. Qed.
+  End OrderElts.
+  Module OrderTac := MakeOrderTac OrderElts.
+
+  Ltac order :=
+    change eq with OrderElts.eq in *;
+    change lt with OrderElts.lt in *;
+    OrderTac.order.
+
+  Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.
+  Lemma eq_le x y z : eq x y -> ~lt y z -> ~lt x z. Proof. order. Qed.
+  Lemma neq_eq x y z : ~eq x y -> eq y z -> ~eq x z. Proof. order. Qed.
+  Lemma eq_neq x y z : eq x y -> ~eq y z -> ~eq x z. Proof. order. Qed.
+  Lemma le_lt_trans x y z : ~lt y x -> lt y z -> lt x z. Proof. order. Qed.
+  Lemma lt_le_trans x y z : lt x y -> ~lt z y -> lt x z. Proof. order. Qed.
+  Lemma le_neq x y : ~lt x y -> ~eq x y -> lt y x. Proof. order. Qed.
+  Lemma le_trans x y z : ~lt y x -> ~lt z y -> ~lt z x. Proof. order. Qed.
+  Lemma le_antisym x y : ~lt y x -> ~lt x y -> eq x y. Proof. order. Qed.
+  Lemma neq_sym x y : ~eq x y -> ~eq y x. Proof. order. Qed.
+  Lemma lt_le x y : lt x y -> ~lt y x. Proof. order. Qed.
+  Lemma gt_not_eq x y : lt y x -> ~ eq x y. Proof. order. Qed.
+  Lemma eq_not_lt x y : eq x y -> ~ lt x y. Proof. order. Qed.
+  Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
+  Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
 
   Hint Resolve gt_not_eq eq_not_lt.
-
-  Lemma eq_not_gt : forall x y : t, eq x y -> ~ lt y x.
-  Proof.
-   order.
-  Qed.
-
-  Lemma lt_not_gt : forall x y : t, lt x y -> ~ lt y x.
-  Proof.
-   order.
-  Qed.
-
+  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
   Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
 
   Lemma elim_compare_eq :
@@ -294,8 +176,7 @@ Ltac order := order_loop; fail.
       | |- ?e => match e with
            | context ctx [ compare ?a ?b ] =>
                 let H := fresh in
-                (destruct (compare a b) as [H|H|H];
-                 try (intros; exfalso; order))
+                (destruct (compare a b) as [H|H|H]; try order)
          end
     end.
 
diff --git a/theories/Structures/OrderedType2.v b/theories/Structures/OrderedType2.v
index 25cfd3b1a..e223dba43 100644
--- a/theories/Structures/OrderedType2.v
+++ b/theories/Structures/OrderedType2.v
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-Require Export SetoidList2 DecidableType2.
+Require Export SetoidList2 DecidableType2 OrderTac.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
@@ -73,6 +73,29 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Local Open Scope order.
 
+  Ltac elim_compare x y :=
+   generalize (compare_spec x y); destruct (compare x y);
+   unfold Cmp, flip.
+
+  Module OrderElts : OrderTacSig
+    with Definition t := t
+    with Definition eq := eq
+    with Definition lt := lt.
+  (* Opaque signature is crucial for ltac to work correctly later *)
+  Include O.
+  Definition le x y := x<y \/ x==y.
+  Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+  Proof. intros; elim_compare x y; intuition. Qed.
+  Lemma le_lteq : forall x y, le x y <-> lt x y \/ eq x y.
+  Proof. unfold le; intuition. Qed.
+  End OrderElts.
+  Module OrderTac := MakeOrderTac OrderElts.
+
+  Ltac order :=
+    change eq with OrderElts.eq in *;
+    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. *)
 
@@ -88,196 +111,29 @@ Module OrderedTypeFacts (Import O: OrderedType).
 
   Definition lt_antirefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
 
-  Lemma lt_not_eq : forall x y, x<y -> ~x==y.
-  Proof.
-   intros x y H H'. rewrite H' in H.
-   apply lt_antirefl with y; auto.
-  Qed.
-
-  Lemma lt_eq : forall x y z, x<y -> y==z -> x<z.
-  Proof.
-   intros x y z H H'. rewrite <- H'; auto.
-  Qed.
-
-  Lemma eq_lt : forall x y z, x==y -> y<z -> x<z.
-  Proof.
-   intros x y z H H'. rewrite H; auto.
-  Qed.
-
-  Lemma le_eq : forall x y z, x<=y -> y==z -> x<=z.
-  Proof.
-   intros x y z H H' H''. rewrite H' in H; auto.
-  Qed.
-
-  Lemma eq_le : forall x y z, x==y -> y<=z -> x<=z.
-  Proof.
-   intros x y z H H'. rewrite H; auto.
-  Qed.
-
-  Lemma neq_eq : forall x y z, ~x==y -> y==z -> ~x==z.
-  Proof.
-   intros x y z H H'; rewrite <-H'; auto.
-  Qed.
-
-  Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
-  Proof.
-   intros x y z H H'; rewrite H; auto.
-  Qed.
+  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.
-
-  Ltac elim_compare x y :=
-   generalize (compare_spec x y); destruct (compare x y);
-   unfold Cmp, flip.
-
-  Lemma le_lt_trans : forall x y z, x<=y -> y<z -> x<z.
-  Proof.
-   intros. elim_compare x y; intro H'.
-   rewrite H'; auto.
-   transitivity y; auto.
-   intuition.
-  Qed.
-
-  Lemma lt_le_trans : forall x y z, x<y -> y<=z -> x<z.
-  Proof.
-   intros. elim_compare y z; intro H'.
-   rewrite <- H'; auto.
-   transitivity y; auto.
-   intuition.
-  Qed.
-
-  Lemma le_trans : forall x y z, x<=y -> y<=z -> x<=z.
-  Proof.
-   intros x y z Hxy Hyz Hzx.
-   apply Hxy.
-   eapply le_lt_trans; eauto.
-  Qed.
-
-  Lemma le_antisym : forall x y, x<=y -> y<=x -> x==y.
-  Proof.
-   intros. elim_compare x y; intuition.
-  Qed.
-
-  Lemma le_neq : forall x y, x<=y -> ~x==y -> x<y.
-  Proof.
-   intros. elim_compare x y; intuition.
-  Qed.
-
-  Lemma neq_sym : forall x y, ~x==y -> ~y==x.
-  Proof.
-   intuition.
-  Qed.
-
-(** The order tactic *)
-
-(** This tactic is designed to solve systems of (in)equations
-    involving eq and lt and ~eq and ~lt (i.e. ge). All others
-    parts of the goal will be discarded. This tactic is
-    domain-agnostic : it will only use equivalence+order axioms.
-    Moreover it doesn't directly use totality of the order
-    (but uses above lemmas such as le_trans that rely on it).
-    A typical use of this tactic is transitivity problems. *)
-
-Definition hide_eq := eq.
-
-(** order_eq : replace x by y in all (in)equations thanks
-   to equality EQ (where eq has been hidden in order to avoid
-   self-rewriting). *)
-
-Ltac order_eq x y EQ :=
- let rewr H t := generalize t; clear H; intro H
- in
- match goal with
- | H : x == _ |- _ => rewr H (eq_trans (eq_sym EQ) H); order_eq x y EQ
- | H : _ == x |- _ => rewr H (eq_trans H EQ); order_eq x y EQ
- | H : ~x == _ |- _ => rewr H (eq_neq (eq_sym EQ) H); order_eq x y EQ
- | H : ~_ == x |- _ => rewr H (neq_eq H EQ); order_eq x y EQ
- | H : x < ?z |- _ => rewr H (eq_lt (eq_sym EQ) H); order_eq x y EQ
- | H : ?z < x |- _ => rewr H (lt_eq H EQ); order_eq x y EQ
- | H : x <= ?z |- _ => rewr H (eq_le (eq_sym EQ) H); order_eq x y EQ
- | H : ?z <= x |- _ => rewr H (le_eq H EQ); order_eq x y EQ
- (* NB: no negation in the goal, see below *)
- | |- x == ?z => apply eq_trans with y; [apply EQ| ]; order_eq x y EQ
- | |- ?z == x => apply eq_trans with y; [ | apply (eq_sym EQ) ];
-    order_eq x y EQ
- | |- x < ?z => apply eq_lt with y; [apply EQ| ]; order_eq x y EQ
- | |- ?z < x => apply lt_eq with y; [ | apply (eq_sym EQ) ];
-    order_eq x y EQ
- | _ => clear EQ
-end.
-
-Ltac order_loop := intros; trivial;
- match goal with
- | |- ~ _ => intro; order_loop
- | H : ?A -> False |- _ => change (~A) in H; order_loop
- (* First, successful situations *)
- | H : ?x < ?x |- _ => elim (lt_antirefl H)
- | H : ~ ?x == ?x |- _ => elim (H (Equivalence_Reflexive x))
- | |- ?x == ?x => apply (Equivalence_Reflexive x)
- (* Second, useless hyps or goal *)
- | H : ?x == ?x |- _ => clear H; order_loop
- | H : ?x <= ?x |- _ => clear H; order_loop
- | |- ?x < ?x => exfalso; order_loop
- (* We eliminate equalities *)
- | H : ?x == ?y |- _ =>
-   change (hide_eq x y) in H; order_eq x y H; order_loop
- (* Simultaneous le and ge is eq *)
- | H1 : ?x <= ?y, H2 : ?y <= ?x |- _ =>
-   generalize (le_antisym H1 H2); clear H1 H2; intro; order_loop
- (* Simultaneous le and ~eq is lt *)
- | H1: ?x <= ?y, H2: ~ ?x == ?y |- _ =>
-     generalize (le_neq H1 H2); clear H1 H2; intro; order_loop
- | H1: ?x <= ?y, H2: ~ ?y == ?x |- _ =>
-     generalize (le_neq H1 (neq_sym H2)); clear H1 H2; intro; order_loop
- (* Transitivity of lt and le *)
- | H1 : ?x < ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y < ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (le_lt_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x < ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x < z |- _ => fail 1
-      | _ => generalize (lt_le_trans H1 H2); intro; order_loop
-    end
- | H1 : ?x <= ?y, H2 : ?y <= ?z |- _ =>
-    match goal with
-      | H : x <= z |- _ => fail 1
-      | _ => generalize (le_trans H1 H2); intro; order_loop
-    end
- | _ => auto
-end.
-
-Ltac order := order_loop; fail.
-
-  Lemma gt_not_eq : forall x y, lt y x -> ~ eq x y.
-  Proof.
-    order.
-  Qed.
-
-  Lemma eq_not_lt : forall x y : t, eq x y -> ~ lt x y.
-  Proof.
-    order.
-  Qed.
-
   Hint Resolve gt_not_eq eq_not_lt.
-
-  Lemma eq_not_gt : forall x y : t, eq x y -> ~ lt y x.
-  Proof.
-   order.
-  Qed.
-
-  Lemma lt_not_gt : forall x y : t, lt x y -> ~ lt y x.
-  Proof.
-   order.
-  Qed.
-
   Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
 
   Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.