OrderTac: use TotalOrder, no more "change" before calling "order" (stuff with Inline)

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

3 files changed, 137 insertions, 113 deletions

diff --git a/theories/Structures/OrderTac.v b/theories/Structures/OrderTac.v
index f75e1ae91..43df377c0 100644
--- a/theories/Structures/OrderTac.v
+++ b/theories/Structures/OrderTac.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1       *)
 (***********************************************************************)
 
-Require Import Setoid Morphisms.
+Require Import Setoid Morphisms Basics DecidableType2 OrderedType2.
 Set Implicit Arguments.
 
 (** * The order tactic *)
@@ -23,25 +23,6 @@ Set Implicit Arguments.
     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 OrderSig.
-
-Parameter Inline t : Type.
-Parameters eq lt le : t -> t -> Prop.
-Declare Instance eq_equiv : Equivalence eq.
-Declare Instance lt_strorder : StrictOrder lt.
-Declare 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 OrderSig.
-
-(** 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 OLE OLE = OLE] will imply later
@@ -56,19 +37,46 @@ Definition trans_ord o o' :=
  | OLE, OLE => OLE
  | _, _ => OLT
  end.
-Infix "+" := trans_ord : order.
+Local Infix "+" := trans_ord.
 
-(** ** [MakeOrderTac] : The functor providing the order tactic. *)
 
-Module MakeOrderTac(Import O:OrderSig).
+(** ** The requirements of the tactic : [TotalOrder].
 
-Local Open Scope order.
+   [TotalOrder] contains an equivalence [eq],
+   a strict order [lt] total and compatible with [eq], and
+   a larger order [le] synonym for [lt\/eq].
 
-Infix "==" := eq (at level 70, no associativity) : order.
-Infix "<" := lt : order.
-Infix "<=" := le : order.
+  NB: we create here a clone of TotalOrder, but without the [Inline] Pragma.
+  This is important for having later the exact shape in Ltac matching.
+*)
 
-(** ** Properties that will be used by the tactic *)
+Module Type TotalOrder_NoInline <: TotalOrder.
+ Parameter Inline t : Type.
+ Parameters eq lt le : t -> t -> Prop.
+ Include Type IsEq <+ IsStrOrder <+ LeIsLtEq <+ LtIsTotal.
+End TotalOrder_NoInline.
+
+Module Type TotalOrder_NoInline' := TotalOrder_NoInline <+ EqLtLeNotation.
+
+(** We make explicit aliases to help ltac matching *)
+
+Module CloneOrder (O:TotalOrder_NoInline) <: TotalOrder.
+Definition t := O.t.
+Definition eq := O.eq.
+Definition lt := O.lt.
+Definition le := O.le.
+Definition eq_equiv := O.eq_equiv.
+Definition lt_compat := O.lt_compat.
+Definition lt_strorder := O.lt_strorder.
+Definition le_lteq := O.le_lteq.
+Definition lt_total := O.lt_total.
+End CloneOrder.
+
+
+
+(** ** Properties that will be used by the [order] tactic *)
+
+Module OrderFacts(Import O:TotalOrder_NoInline').
 
 (** Reflexivity rules *)
 
@@ -104,8 +112,8 @@ Ltac subst_eqns :=
  end.
 
 Definition interp_ord o :=
- match o with OEQ => eq | OLT => lt | OLE => le end.
-Notation "#" := interp_ord : order.
+ match o with OEQ => O.eq | OLT => O.lt | OLE => O.le end.
+Local Notation "#" := interp_ord.
 
 Lemma trans : forall o o' x y z, #o x y -> #o' y z -> #(o+o') x z.
 Proof.
@@ -113,15 +121,15 @@ 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 OEQ OEQ x y z.
-Definition le_trans x y z : x<=y -> y<=z -> x<=z := trans OLE OLE x y z.
-Definition lt_trans x y z : x<y -> y<z -> x<z := trans OLT OLT x y z.
-Definition le_lt_trans x y z : x<=y -> y<z -> x<z := trans OLE OLT x y z.
-Definition lt_le_trans x y z : x<y -> y<=z -> x<z := trans OLT OLE x y z.
-Definition eq_lt x y z : x==y -> y<z -> x<z := trans OEQ OLT x y z.
-Definition lt_eq x y z : x<y -> y==z -> x<z := trans OLT OEQ x y z.
-Definition eq_le x y z : x==y -> y<=z -> x<=z := trans OEQ OLE x y z.
-Definition le_eq x y z : x<=y -> y==z -> x<=z := trans OLE OEQ x y z.
+Definition eq_trans x y z : x==y -> y==z -> x==z := @trans OEQ OEQ x y z.
+Definition le_trans x y z : x<=y -> y<=z -> x<=z := @trans OLE OLE x y z.
+Definition lt_trans x y z : x<y -> y<z -> x<z := @trans OLT OLT x y z.
+Definition le_lt_trans x y z : x<=y -> y<z -> x<z := @trans OLE OLT x y z.
+Definition lt_le_trans x y z : x<y -> y<=z -> x<z := @trans OLT OLE x y z.
+Definition eq_lt x y z : x==y -> y<z -> x<z := @trans OEQ OLT x y z.
+Definition lt_eq x y z : x<y -> y==z -> x<z := @trans OLT OEQ x y z.
+Definition eq_le x y z : x==y -> y<=z -> x<=z := @trans OEQ OLE x y z.
+Definition le_eq x y z : x<=y -> y==z -> x<=z := @trans OLE OEQ x y z.
 
 Lemma eq_neq : forall x y z, x==y -> ~y==z -> ~x==z.
 Proof. eauto using eq_trans, eq_sym. Qed.
@@ -151,8 +159,15 @@ Qed.
 Lemma le_neq_lt : forall x y, x<=y -> ~x==y -> x<y.
 Proof. auto using not_ge_lt, le_antisym. Qed.
 
+End OrderFacts.
+
 
-(** ** The tactic itself *)
+
+(** ** [MakeOrderTac] : The functor providing the order tactic. *)
+
+Module MakeOrderTac (Import O:TotalOrder_NoInline').
+
+Include OrderFacts O.
 
 (** order_eq : replace x by y in all (in)equations hyps thanks
    to equality EQ (where eq has been hidden in order to avoid
@@ -177,7 +192,7 @@ end.
 Ltac order_eq x y eqn :=
  match x with
  | y => clear eqn
- | _ => change (#OEQ x y) in eqn; order_rewr x eqn
+ | _ => change (interp_ord OEQ x y) in eqn; order_rewr x eqn
  end.
 
 (** Goal preparation : We turn all negative hyps into positive ones
@@ -190,18 +205,31 @@ Ltac order_eq x y eqn :=
 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
+ | H : ~(?R ?x ?y) |- _ =>
+   match R with
+   | eq => fail 1 (* if already using [eq], we leave it this ways *)
+   | _ => (change (~x==y) in H ||
+           apply not_gt_le in H ||
+           apply not_ge_lt in H ||
+           clear H || fail 1); order_prepare
+   end
+ | H : ?R ?x ?y |- _ =>
+   match R with
+   | eq => fail 1
+   | lt => fail 1
+   | le => fail 1
+   | _ => (change (x==y) in H ||
+           change (x<y) in H ||
+           change (x<=y) in H ||
+           clear H || fail 1); order_prepare
+   end
+ | |- ~ _ => intro; order_prepare
+ | |- _ ?x ?x =>
+   exact (eq_refl x) || exact (le_refl x) || exfalso
+ | _ =>
+   (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 *)
@@ -254,4 +282,42 @@ Ltac order :=
 
 End MakeOrderTac.
 
-(** For example of use of this tactic, see for instance [OrderedType] *)
\ No newline at end of file
+Module OTF_to_OrderTac (OTF:OrderedTypeFull).
+ Module TO := OTF_to_TotalOrder OTF.
+ Module TO' := CloneOrder TO.
+ Include MakeOrderTac TO'.
+End OTF_to_OrderTac.
+
+Module OT_to_OrderTac (OT:OrderedType).
+ Module OTF := OT_to_Full OT.
+ Include OTF_to_OrderTac OTF.
+End OT_to_OrderTac.
+
+(** For example of use of this tactic, see for instance [OrderedType] *)
+
+
+Module TotalOrderRev (O:TotalOrder) <: TotalOrder.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+Include Type EqLtLeNotation.
+
+Instance eq_equiv : Equivalence eq.
+
+Instance lt_strorder: StrictOrder lt.
+Proof. unfold lt; auto with *. Qed.
+Instance lt_compat : Proper (eq==>eq==>iff) lt.
+Proof. unfold lt; auto with *. Qed.
+
+Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Lemma lt_total : forall x y, x<y \/ x==y \/ y<x.
+Proof.
+ intros x y; unfold lt, eq, flip.
+ generalize (O.lt_total x y); intuition.
+Qed.
+
+End TotalOrderRev.
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f0d4163c3..ca441fc86 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -103,11 +103,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   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 : OrderSig
-    with Definition t := t
-    with Definition eq := eq
-    with Definition lt := lt.
-  (* Opaque signature is crucial for ltac to work correctly later *)
+  Module OrderElts <: OrderedType2.TotalOrder.
   Definition t := t.
   Definition eq := eq.
   Definition lt := lt.
@@ -121,11 +117,7 @@ Module OrderedTypeFacts (Import O: OrderedType).
   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.
+  Ltac order := 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.
diff --git a/theories/Structures/OrderedType2Facts.v b/theories/Structures/OrderedType2Facts.v
index 9d964d712..b5dc0c92f 100644
--- a/theories/Structures/OrderedType2Facts.v
+++ b/theories/Structures/OrderedType2Facts.v
@@ -9,47 +9,15 @@
 Require Import Basics OrderTac.
 Require Export OrderedType2.
 
-
 Set Implicit Arguments.
 Unset Strict Implicit.
 
+(** * Properties of [OrderedTypeFull] *)
 
-(** * Properties of ordered types *)
-
-(** First, an OrderdType (with [<=]) is enough for building an [order]
-    tactic. *)
-
-Module OTF_to_OrderSig (O : OrderedTypeFull) :
- OrderSig with Definition t := O.t
-          with Definition eq := O.eq
-          with Definition lt := O.lt
-          with Definition le := O.le
-          with Definition eq_equiv := O.eq_equiv
-          with Definition lt_strorder := O.lt_strorder
-          with Definition lt_compat := O.lt_compat.
- Include O.
- Lemma lt_total : forall x y, O.lt x y \/ O.eq x y \/ O.lt y x.
- Proof. intros; destruct (O.compare_spec x y); auto. Qed.
-End OTF_to_OrderSig.
-
-
-Module OTF_to_OrderTac (O:OrderedTypeFull).
- Module OrderElts := OTF_to_OrderSig O.
- Module OrderTac := MakeOrderTac OrderElts.
- Ltac order :=
-   change O.eq with OrderElts.eq in *;
-   change O.lt with OrderElts.lt in *;
-   change O.le with OrderElts.le in *;
-   OrderTac.order.
-End OTF_to_OrderTac.
+Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
 
-
-(** This allows to prove a few properties of [<=] *)
-
-Module OrderedTypeFullFacts (Import O:OrderedTypeFull).
-
- Module Order := OTF_to_OrderTac O.
- Ltac order := Order.order.
+ Module OrderTac := OTF_to_OrderTac O.
+ Ltac order := OrderTac.order.
  Ltac iorder := intuition order.
 
  Instance le_compat : Proper (eq==>eq==>iff) le.
@@ -64,33 +32,31 @@ Module OrderedTypeFullFacts (Import O:OrderedTypeFull).
  Instance le_antisym : Antisymmetric _ eq le.
  Proof. apply partial_order_antisym; auto with *. Qed.
 
- Lemma le_not_gt_iff : forall x y, le x y <-> ~lt y x.
+ Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
  Proof. iorder. Qed.
 
- Lemma lt_not_ge_iff : forall x y, lt x y <-> ~le y x.
+ Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
  Proof. iorder. Qed.
 
- Lemma le_or_gt : forall x y, le x y \/ lt y x.
+ Lemma le_or_gt : forall x y, x<=y \/ y<x.
  Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); auto. Qed.
 
- Lemma lt_or_ge : forall x y, lt x y \/ le y x.
+ Lemma lt_or_ge : forall x y, x<y \/ y<=x.
  Proof. intros. rewrite le_lteq; destruct (O.compare_spec x y); iorder. Qed.
 
- Lemma eq_is_le_ge : forall x y, eq x y <-> le x y /\ le y x.
+ Lemma eq_is_le_ge : forall x y, x==y <-> x<=y /\ y<=x.
  Proof. iorder. Qed.
 
 End OrderedTypeFullFacts.
 
 
-(** * Properties of OrderedType *)
+(** * Properties of [OrderedType] *)
+
+Module OrderedTypeFacts (Import O: OrderedType').
 
-Module OrderedTypeFacts (Import O: OrderedType).
-  Module O' := OT_to_Full O.
-  Module Order := OTF_to_OrderTac O'.
-  Ltac order := Order.order.
+  Module OrderTac := OT_to_OrderTac O.
+  Ltac order := OrderTac.order.
 
-  Infix "==" := eq (at level 70, no associativity) : order.
-  Infix "<" := lt : order.
   Notation "x <= y" := (~lt y x) : order.
   Infix "?=" := compare (at level 70, no associativity) : order.
 
@@ -204,7 +170,7 @@ End OrderedTypeFacts.
 
     Is it at least capable of proving some basic properties ? *)
 
-Module OrderedTypeTest (O:OrderedType).
+Module OrderedTypeTest (Import O:OrderedType').
   Module Import MO := OrderedTypeFacts O.
   Local Open Scope order.
   Lemma lt_not_eq x y : x<y -> ~x==y.  Proof. order. Qed.