diff options
Diffstat (limited to 'theories/FSets/OrderedTypeEx.v')
| -rw-r--r-- | theories/FSets/OrderedTypeEx.v | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/theories/FSets/OrderedTypeEx.v b/theories/FSets/OrderedTypeEx.v index 28a5705d..03171396 100644 --- a/theories/FSets/OrderedTypeEx.v +++ b/theories/FSets/OrderedTypeEx.v @@ -11,7 +11,7 @@ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud * 91405 Orsay, France *) -(* $Id: OrderedTypeEx.v 9940 2007-07-05 12:32:47Z letouzey $ *) +(* $Id: OrderedTypeEx.v 10739 2008-04-01 14:45:20Z herbelin $ *) Require Import OrderedType. Require Import ZArith. @@ -25,9 +25,9 @@ Require Import Compare_dec. the equality is the usual one of Coq. *) Module Type UsualOrderedType. - Parameter t : Set. + Parameter Inline t : Type. Definition eq := @eq t. - Parameter lt : t -> t -> Prop. + Parameter Inline lt : t -> t -> Prop. Definition eq_refl := @refl_equal t. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. @@ -154,16 +154,16 @@ Module N_as_OT <: UsualOrderedType. Definition eq_sym := @sym_eq t. Definition eq_trans := @trans_eq t. - Definition lt p q:= Nle q p = false. + Definition lt p q:= Nleb q p = false. - Definition lt_trans := Nlt_trans. + Definition lt_trans := Nltb_trans. Lemma lt_not_eq : forall x y : t, lt x y -> ~ eq x y. Proof. intros; intro. rewrite H0 in H. unfold lt in H. - rewrite Nle_refl in H; discriminate. + rewrite Nleb_refl in H; discriminate. Qed. Definition compare : forall x y : t, Compare lt eq x y. @@ -172,16 +172,15 @@ Module N_as_OT <: UsualOrderedType. case_eq ((x ?= y)%N); intros. apply EQ; apply Ncompare_Eq_eq; auto. apply LT; unfold lt; auto. - generalize (Nle_Ncompare y x). - destruct (Nle y x); auto. - rewrite <- Ncompare_antisym. + generalize (Nleb_Nle y x). + unfold Nle; rewrite <- Ncompare_antisym. destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + clear H; intros H. + destruct (Nleb y x); intuition. apply GT; unfold lt. - generalize (Nle_Ncompare x y). - destruct (Nle x y); auto. - destruct (x ?= y)%N; simpl; try discriminate. - intros (H0,_); elim H0; auto. + generalize (Nleb_Nle x y). + unfold Nle; destruct (x ?= y)%N; simpl; try discriminate. + destruct (Nleb x y); intuition. Defined. End N_as_OT. |