diff options
Diffstat (limited to 'theories/Structures/OrderedType2Ex.v')
| -rw-r--r-- | theories/Structures/OrderedType2Ex.v | 205 |
1 files changed, 16 insertions, 189 deletions
diff --git a/theories/Structures/OrderedType2Ex.v b/theories/Structures/OrderedType2Ex.v index 73bd3810f9..801c18723b 100644 --- a/theories/Structures/OrderedType2Ex.v +++ b/theories/Structures/OrderedType2Ex.v @@ -13,174 +13,18 @@ (* $Id$ *) -Require Import OrderedType2 DecidableType2Ex. -Require Import ZArith NArith Ndec Compare_dec. +Require Import OrderedType2 NatOrderedType POrderedType NOrderedType + ZOrderedType DecidableType2Ex RelationPairs. (** * Examples of Ordered Type structures. *) -(** First, a particular case of [OrderedType] where - the equality is the usual one of Coq. *) -Module Type UsualOrderedType. - Include Type UsualDecidableType. - - Parameter Inline lt : t -> t -> Prop. - Instance lt_strorder : StrictOrder lt. - (* The following is useless since eq is Leibniz, but should be there - for subtyping... *) - Instance lt_compat : Proper (eq==>eq==>iff) lt. - - Parameter compare : t -> t -> comparison. - Axiom compare_spec : forall x y, Cmp eq lt (compare x y) x y. - -End UsualOrderedType. - -(** a [UsualOrderedType] is in particular an [OrderedType]. *) - -Module UOT_to_OT (U:UsualOrderedType) <: OrderedType := U. - -(** [nat] is an ordered type with respect to the usual order on natural numbers. *) - -Module Nat_as_OT <: UsualOrderedType. - - Definition t := nat. - Definition eq := @eq nat. - Definition lt := lt. - Definition compare := nat_compare. - Definition eq_dec := eq_nat_dec. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact lt_irrefl|exact lt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply nat_compare_eq; auto. - apply nat_compare_Lt_lt; auto. - apply nat_compare_Gt_gt; auto. - Qed. - -End Nat_as_OT. - - -(** [Z] is an ordered type with respect to the usual order on integers. *) - -Module Z_as_OT <: UsualOrderedType. - - Definition t := Z. - Definition eq := @eq Z. - Definition lt := Zlt. - Definition compare := Zcompare. - Definition eq_dec := Z_eq_dec. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Zlt_irrefl | exact Zlt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Zcompare_Eq_eq; auto. - auto. - apply Zgt_lt; auto. - Qed. - -End Z_as_OT. - -(** [positive] is an ordered type with respect to the usual order - on natural numbers. *) - -Module Positive_as_OT <: UsualOrderedType. - Definition t:=positive. - Definition eq:=@eq positive. - Definition lt:=Plt. - Definition compare x y := Pcompare x y Eq. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Plt_irrefl | exact Plt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Pcompare_Eq_eq; auto. - auto. - apply ZC1; auto. - Qed. - - Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. - Proof. - intros; unfold eq; decide equality. - Defined. - -End Positive_as_OT. - - -(** [N] is an ordered type with respect to the usual order - on natural numbers. *) - -Module N_as_OT <: UsualOrderedType. - Definition t:=N. - Definition eq:=@eq N. - Definition lt:=Nlt. - Definition compare:=Ncompare. - - Program Instance eq_equiv : Equivalence eq. - - Instance lt_strorder : StrictOrder lt. - Proof. - constructor; [exact Nlt_irrefl | exact Nlt_trans]. - Qed. - - Instance lt_compat : Proper (eq==>eq==>iff) lt. - Proof. - unfold eq in *; repeat red; intros; subst; auto. - Qed. - - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. - Proof. - intros. - unfold Cmp, flip, lt, eq. destruct (compare x y) as [ ]_eqn:H. - apply Ncompare_Eq_eq; auto. - auto. - apply Ngt_Nlt; auto. - Qed. - - Definition eq_dec : forall x y, { eq x y } + { ~ eq x y }. - Proof. - intros. unfold eq. decide equality. apply Positive_as_OT.eq_dec. - Defined. - -End N_as_OT. +(** Ordered Type for [nat], [Positive], [N], [Z] with the usual order. *) +Module Nat_as_OT := NatOrderedType.Nat_as_OT. +Module Positive_as_OT := POrderedType.Positive_as_OT. +Module N_as_OT := NOrderedType.N_as_OT. +Module Z_as_OT := ZOrderedType.Z_as_OT. (** An OrderedType can now directly be seen as a DecidableType *) @@ -195,21 +39,14 @@ Module Z_as_DT <: UsualDecidableType := Z_as_OT. - (** From two ordered types, we can build a new OrderedType over their cartesian product, using the lexicographic order. *) Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. + Include PairDecidableType O1 O2. - Definition t := prod O1.t O2.t. - - Definition eq := ProdRel O1.eq O2.eq. - - Definition lt x y := - O1.lt (fst x) (fst y) \/ - (O1.eq (fst x) (fst y) /\ O2.lt (snd x) (snd y)). - - Instance eq_equiv : Equivalence eq. + Definition lt := + (relation_disjunction (O1.lt @@ fst) (O1.eq * O2.lt))%signature. Instance lt_strorder : StrictOrder lt. Proof. @@ -219,7 +56,7 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. apply (StrictOrder_Irreflexive x1); auto. apply (StrictOrder_Irreflexive x2); intuition. (* transitive *) - intros (x1,x2) (y1,y2) (z1,z2); unfold eq, lt; simpl; intuition. + intros (x1,x2) (y1,y2) (z1,z2). compute. intuition. left; etransitivity; eauto. left; rewrite <- H0; auto. left; rewrite H; auto. @@ -228,8 +65,8 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. Instance lt_compat : Proper (eq==>eq==>iff) lt. Proof. + compute. intros (x1,x2) (x1',x2') (X1,X2) (y1,y2) (y1',y2') (Y1,Y2). - unfold lt; simpl in *. rewrite X1,X2,Y1,Y2; intuition. Qed. @@ -240,22 +77,12 @@ Module PairOrderedType(O1 O2:OrderedType) <: OrderedType. | Gt => Gt end. - Lemma compare_spec : forall x y, Cmp eq lt (compare x y) x y. + Lemma compare_spec : forall x y, Cmp eq lt x y (compare x y). Proof. - intros (x1,x2) (y1,y2); unfold Cmp, flip, compare, eq, lt; simpl. - generalize (O1.compare_spec x1 y1); destruct (O1.compare x1 y1); intros; auto. - generalize (O2.compare_spec x2 y2); destruct (O2.compare x2 y2); intros; auto. + intros (x1,x2) (y1,y2); unfold compare; simpl. + destruct (O1.compare_spec x1 y1); try (constructor; compute; auto). + destruct (O2.compare_spec x2 y2); constructor; compute; auto. Qed. - Definition eq_dec : forall x y : t, {eq x y} + {~ eq x y}. - Proof. - intros; generalize (compare_spec x y); destruct (compare x y). - left; auto. - right. intros E; rewrite E in *. - apply (StrictOrder_Irreflexive y); auto. - right. intros E; rewrite E in *. - apply (StrictOrder_Irreflexive y); auto. - Defined. - End PairOrderedType. |