summaryrefslogtreecommitdiff
path: root/theories/Structures/OrdersFacts.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/Structures/OrdersFacts.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/Structures/OrdersFacts.v')
-rw-r--r--theories/Structures/OrdersFacts.v234
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.
+