1 files changed, 234 insertions, 0 deletions
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
new file mode 100644
index 00000000..a28b7977
--- /dev/null
+++ b/theories/Structures/OrdersFacts.v
@@ -0,0 +1,234 @@
+(***********************************************************************)
+(*  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 Basics OrdersTac.
+Require Export Orders.
+
+Set Implicit Arguments.
+Unset Strict Implicit.
+
+(** * Properties of [OrderedTypeFull] *)
+
+Module OrderedTypeFullFacts (Import O:OrderedTypeFull').
+
+ Module OrderTac := OTF_to_OrderTac O.
+ Ltac order := OrderTac.order.
+ Ltac iorder := intuition order.
+
+ Instance le_compat : Proper (eq==>eq==>iff) le.
+ Proof. repeat red; iorder. Qed.
+
+ Instance le_preorder : PreOrder le.
+ Proof. split; red; order. Qed.
+
+ Instance le_order : PartialOrder eq le.
+ Proof. compute; iorder. Qed.
+
+ Instance le_antisym : Antisymmetric _ eq le.
+ Proof. apply partial_order_antisym; auto with *. Qed.
+
+ Lemma le_not_gt_iff : forall x y, x<=y <-> ~y<x.
+ Proof. iorder. Qed.
+
+ Lemma lt_not_ge_iff : forall x y, x<y <-> ~y<=x.
+ Proof. iorder. Qed.
+
+ 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, 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, x==y <-> x<=y /\ y<=x.
+ Proof. iorder. Qed.
+
+End OrderedTypeFullFacts.
+
+
+(** * Properties of [OrderedType] *)
+
+Module OrderedTypeFacts (Import O: OrderedType').
+
+  Module OrderTac := OT_to_OrderTac O.
+  Ltac order := OrderTac.order.
+
+  Notation "x <= y" := (~lt y x) : order.
+  Infix "?=" := compare (at level 70, no associativity) : order.
+
+  Local Open Scope order.
+
+  Tactic Notation "elim_compare" constr(x) constr(y) :=
+   destruct (compare_spec x y).
+
+  Tactic Notation "elim_compare" constr(x) constr(y) "as" ident(h) :=
+   destruct (compare_spec x y) as [h|h|h].
+
+  (** 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.
+
+  Definition eq_sym (x y:t) : x==y -> y==x := Equivalence_Symmetric x y.
+
+  Definition eq_trans (x y z:t) : x==y -> y==z -> x==z :=
+   Equivalence_Transitive x y z.
+
+  Definition lt_trans (x y z:t) : x<y -> y<z -> x<z :=
+   StrictOrder_Transitive x y z.
+
+  Definition lt_irrefl (x:t) : ~x<x := StrictOrder_Irreflexive x.
+
+  (** Some more about [compare] *)
+
+  Lemma compare_eq_iff : forall x y, (x ?= y) = Eq <-> x==y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_lt_iff : forall x y, (x ?= y) = Lt <-> x<y.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_gt_iff : forall x y, (x ?= y) = Gt <-> y<x.
+  Proof.
+   intros; elim_compare x y; intuition; try discriminate; order.
+  Qed.
+
+  Lemma compare_ge_iff : forall x y, (x ?= y) <> Lt <-> y<=x.
+  Proof.
+   intros; rewrite compare_lt_iff; intuition.
+  Qed.
+
+  Lemma compare_le_iff : forall x y, (x ?= y) <> Gt <-> x<=y.
+  Proof.
+   intros; rewrite compare_gt_iff; intuition.
+  Qed.
+
+  Hint Rewrite compare_eq_iff compare_lt_iff compare_gt_iff : order.
+
+  Instance compare_compat : Proper (eq==>eq==>Logic.eq) compare.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  elim_compare x' y'; autorewrite with order; order.
+  Qed.
+
+  Lemma compare_refl : forall x, (x ?= x) = Eq.
+  Proof.
+   intros; elim_compare x x; auto; order.
+  Qed.
+
+  Lemma compare_antisym : forall x y, (y ?= x) = CompOpp (x ?= y).
+  Proof.
+   intros; elim_compare x y; simpl; autorewrite with order; order.
+  Qed.
+
+  (** For compatibility reasons *)
+  Definition eq_dec := eq_dec.
+
+  Lemma lt_dec : forall x y : t, {lt x y} + {~ lt x y}.
+  Proof.
+   intros x y; destruct (CompSpec2Type (compare_spec x y));
+    [ right | left | right ]; order.
+  Defined.
+
+  Definition eqb x y : bool := if eq_dec x y then true else false.
+
+  Lemma if_eq_dec : forall x y (B:Type)(b b':B),
+    (if eq_dec x y then b else b') =
+    (match compare x y with Eq => b | _ => b' end).
+  Proof.
+  intros; destruct eq_dec; elim_compare x y; auto; order.
+  Qed.
+
+  Lemma eqb_alt :
+    forall x y, eqb x y = match compare x y with Eq => true | _ => false end.
+  Proof.
+  unfold eqb; intros; apply if_eq_dec.
+  Qed.
+
+  Instance eqb_compat : Proper (eq==>eq==>Logic.eq) eqb.
+  Proof.
+  intros x x' Hxx' y y' Hyy'.
+  rewrite 2 eqb_alt, Hxx', Hyy'; auto.
+  Qed.
+
+End OrderedTypeFacts.
+
+
+
+
+
+
+(** * Tests of the order tactic
+
+    Is it at least capable of proving some basic properties ? *)
+
+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.
+  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.
+  Lemma eq_is_nlt_ngt x y : x==y <-> ~x<y /\ ~y<x.
+  Proof. intuition; order. Qed.
+End OrderedTypeTest.
+
+
+
+(** * Reversed OrderedTypeFull.
+
+   we can switch the orientation of the order. This is used for
+   example when deriving properties of [min] out of the ones of [max]
+   (see [GenericMinMax]).
+*)
+
+Module OrderedTypeRev (O:OrderedTypeFull) <: OrderedTypeFull.
+
+Definition t := O.t.
+Definition eq := O.eq.
+Instance eq_equiv : Equivalence eq.
+Definition eq_dec := O.eq_dec.
+
+Definition lt := flip O.lt.
+Definition le := flip O.le.
+
+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, le x y <-> lt x y \/ eq x y.
+Proof. intros; unfold le, lt, flip. rewrite O.le_lteq; intuition. Qed.
+
+Definition compare := flip O.compare.
+
+Lemma compare_spec : forall x y, CompSpec eq lt x y (compare x y).
+Proof.
+intros; unfold compare, eq, lt, flip.
+destruct (O.compare_spec y x); auto with relations.
+Qed.
+
+End OrderedTypeRev.
+