Simplification of OrdersTac thanks to the functor application ! with no inline

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

5 files changed, 46 insertions, 55 deletions

diff --git a/theories/Arith/NatOrderedType.v b/theories/Arith/NatOrderedType.v
index fa4b7172ad..df5b37e019 100644
--- a/theories/Arith/NatOrderedType.v
+++ b/theories/Arith/NatOrderedType.v
@@ -57,3 +57,8 @@ Ltac nat_order := NatOrder.order.
 
 (** Note that [nat_order] is domain-agnostic: it will not prove
     [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
+
+Section Test.
+Let test : forall x y : nat, x<=y -> y<=x -> x=y.
+Proof. nat_order. Qed.
+End Test.
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index aa41a35ea9..734ebe95be 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -120,6 +120,28 @@ le_elim H3. assumption. rewrite <- H3 in H2.
 elim (lt_asymm n m); auto.
 Qed.
 
+Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
+Proof.
+intros n m p. rewrite 3 lt_eq_cases.
+intros [LT|EQ] [LT'|EQ']; try rewrite EQ; try rewrite <- EQ';
+ generalize (lt_trans n m p); auto with relations.
+Qed.
+
+(** Some type classes about order *)
+
+Instance lt_strorder : StrictOrder lt.
+Proof. split. exact lt_irrefl. exact lt_trans. Qed.
+
+Instance le_preorder : PreOrder le.
+Proof. split. exact le_refl. exact le_trans. Qed.
+
+Instance le_partialorder : PartialOrder _ le.
+Proof.
+intros x y. compute. split.
+intro EQ; now rewrite EQ.
+rewrite 2 lt_eq_cases. intuition. elim (lt_irrefl x). now transitivity y.
+Qed.
+
 (** We know enough now to benefit from the generic [order] tactic. *)
 
 Module OrderElts <: TotalOrder.
@@ -128,14 +150,12 @@ Module OrderElts <: TotalOrder.
  Definition lt := lt.
  Definition le := le.
  Definition eq_equiv := eq_equiv.
- Instance lt_strorder : StrictOrder lt.
- Proof. split; [ exact lt_irrefl | exact lt_trans ]. Qed.
- Instance lt_compat : Proper (eq==>eq==>iff) lt.
- Proof. exact lt_wd. Qed. (* BUG(?) pourquoi ne trouve-t'il pas lt_wd *)
+ Definition lt_strorder := lt_strorder.
+ Definition lt_compat := lt_wd.
  Definition lt_total := lt_trichotomy.
  Definition le_lteq := lt_eq_cases.
 End OrderElts.
-Module OrderTac := MakeOrderTac OrderElts.
+Module OrderTac := !MakeOrderTac OrderElts.
 Ltac order := OrderTac.order.
 
 (** Some direct consequences of [order]. *)
@@ -166,9 +186,6 @@ Declare Right Step lt_stepr.
 Declare Left  Step le_stepl.
 Declare Right Step le_stepr.
 
-Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p.
-Proof. order. Qed.
-
 Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p.
 Proof. order. Qed.
 
@@ -187,17 +204,17 @@ Qed.
 
 Theorem lt_succ_l : forall n m, S n < m -> n < m.
 Proof.
-intros n m H; apply -> le_succ_l; now apply lt_le_incl.
+intros n m H; apply -> le_succ_l; order.
 Qed.
 
 Theorem le_le_succ_r : forall n m, n <= m -> n <= S m.
 Proof.
-intros n m LE. rewrite <- lt_succ_r in LE. now apply lt_le_incl.
+intros n m LE. rewrite <- lt_succ_r in LE. order.
 Qed.
 
 Theorem lt_lt_succ_r : forall n m, n < m -> n < S m.
 Proof.
-intros. rewrite lt_succ_r. now apply lt_le_incl.
+intros. rewrite lt_succ_r. order.
 Qed.
 
 Theorem succ_lt_mono : forall n m, n < m <-> S n < S m.
@@ -222,7 +239,7 @@ Qed.
 
 Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
 Proof.
-intros n m H1 H2. apply <- le_succ_l in H1. now apply le_lt_trans with n.
+intros n m H1 H2. apply <- le_succ_l in H1. order.
 Qed.
 
 
@@ -233,12 +250,12 @@ remember whether one has to say le_gt_cases or lt_ge_cases *)
 
 Theorem lt_ge_cases : forall n m, n < m \/ n >= m.
 Proof.
-intros n m; destruct (le_gt_cases m n); [right|left]; order.
+intros n m; destruct (le_gt_cases m n); intuition order.
 Qed.
 
 Theorem le_ge_cases : forall n m, n <= m \/ n >= m.
 Proof.
-intros n m; destruct (le_gt_cases n m); [left|right]; order.
+intros n m; destruct (le_gt_cases n m); intuition order.
 Qed.
 
 Theorem lt_gt_cases : forall n m, n ~= m <-> n < m \/ n > m.
@@ -310,7 +327,7 @@ Qed.
 
 Theorem nlt_succ_r : forall n m, ~ m < S n <-> n < m.
 Proof.
-intros n m; rewrite lt_succ_r; apply nle_gt.
+intros n m; rewrite lt_succ_r. intuition order.
 Qed.
 
 (** The difference between integers and natural numbers is that for
@@ -620,8 +637,7 @@ Module NZOrderPropFunct (NZ : NZOrdSig) :=
 Module NZOrderedTypeFunct (NZ : NZDecOrdSig')
   <: DecidableTypeFull <: OrderedTypeFull.
  Include NZ <+ NZOrderPropFunct.
- Instance lt_compat : Proper (eq==>eq==>iff) lt := lt_wd.
- Instance lt_strorder : StrictOrder lt.
- Include Compare2EqBool <+ HasEqBool2Dec.
+ Definition lt_compat := lt_wd.
  Definition le_lteq := lt_eq_cases.
+ Include Compare2EqBool <+ HasEqBool2Dec.
 End NZOrderedTypeFunct.
diff --git a/theories/Structures/GenericMinMax.v b/theories/Structures/GenericMinMax.v
index 5dec73c623..01c6134b2a 100644
--- a/theories/Structures/GenericMinMax.v
+++ b/theories/Structures/GenericMinMax.v
@@ -79,7 +79,7 @@ End GenericMinMax.
 (** ** Consequences of the minimalist interface: facts about [max]. *)
 
 Module MaxLogicalProperties (Import O:TotalOrder')(Import M:HasMax O).
- Module Import T := MakeOrderTac O.
+ Module Import T := !MakeOrderTac O.
 
 (** An alternative caracterisation of [max], equivalent to
     [max_l /\ max_r] *)
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index 7d56d96665..72fbe79680 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -114,12 +114,11 @@ Module OrderedTypeFacts (Import O: OrderedType).
   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.
+  Definition lt_total := lt_total.
   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.
+  Module OrderTac := !MakeOrderTac OrderElts.
   Ltac order := OrderTac.order.
 
   Lemma le_eq x y z : ~lt x y -> eq y z -> ~lt x z. Proof. order. Qed.
diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v
index 35484ae77a..64c764d9fc 100644
--- a/theories/Structures/OrdersTac.v
+++ b/theories/Structures/OrdersTac.v
@@ -45,38 +45,11 @@ Local Infix "+" := trans_ord.
    [TotalOrder] contains an equivalence [eq],
    a strict order [lt] total and compatible with [eq], and
    a larger order [le] synonym for [lt\/eq].
-
-  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.
 *)
 
-Module Type TotalOrder_NoInline <: TotalOrder.
- Parameter Inline t : Type.
- Parameters eq lt le : t -> t -> Prop.
- Include 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').
+Module OrderFacts(Import O:TotalOrder').
 
 (** Reflexivity rules *)
 
@@ -165,7 +138,7 @@ End OrderFacts.
 
 (** ** [MakeOrderTac] : The functor providing the order tactic. *)
 
-Module MakeOrderTac (Import O:TotalOrder_NoInline').
+Module MakeOrderTac (Import O:TotalOrder').
 
 Include OrderFacts O.
 
@@ -284,16 +257,14 @@ End MakeOrderTac.
 
 Module OTF_to_OrderTac (OTF:OrderedTypeFull).
  Module TO := OTF_to_TotalOrder OTF.
- Module TO' := CloneOrder TO.
- Include MakeOrderTac 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.
+ Include !OTF_to_OrderTac OTF. (* Why a bang here ? *)
 End OT_to_OrderTac.
 
-(** For example of use of this tactic, see for instance [OrderedType] *)
 
 
 Module TotalOrderRev (O:TotalOrder) <: TotalOrder.