diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 18:16:56 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-08 18:16:56 +0000 |
commit | 009fc6e9d0c92852f3a02ff66876875b9384d41a (patch) | |
tree | ff6a9c10a731f0f5d2fdd5df7b8e3e6cbebb641d | |
parent | 301fcb9e20c1907864034e22dd1fdd2ab7f99c98 (diff) |
misc improvements
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10539 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/FSets/FSetToFiniteSet.v | 22 | ||||
-rw-r--r-- | theories/FSets/OrderedTypeAlt.v | 20 |
2 files changed, 26 insertions, 16 deletions
diff --git a/theories/FSets/FSetToFiniteSet.v b/theories/FSets/FSetToFiniteSet.v index 8c48bc24d..67b20d5d2 100644 --- a/theories/FSets/FSetToFiniteSet.v +++ b/theories/FSets/FSetToFiniteSet.v @@ -16,8 +16,8 @@ Require Import Ensembles Finite_sets. Require Import FSetInterface FSetProperties OrderedTypeEx DecidableTypeEx. -(** * Going from [FSets] with usual equality - to the old [Ensembles] and [Finite_sets] theory. *) +(** * Going from [FSets] with usual Leibniz equality + to the good old [Ensembles] and [Finite_sets] theory. *) Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U). Module MP:= WProperties U M. @@ -136,6 +136,22 @@ Module WS_to_Finite_set (U:UsualDecidableType)(M: WSfun U). apply Add_Add; auto. Qed. + (** we can even build a function from Finite Ensemble to FSet + ... at least in Prop. *) + + Lemma Ens_to_FSet : forall e : Ensemble M.elt, Finite _ e -> + exists s:M.t, !!s === e. + Proof. + induction 1. + exists M.empty. + apply empty_Empty_Set. + destruct IHFinite as (s,Hs). + exists (M.add x s). + apply Extensionality_Ensembles in Hs. + rewrite <- Hs. + apply add_Add. + Qed. + End WS_to_Finite_set. @@ -143,3 +159,5 @@ Module S_to_Finite_set (U:UsualOrderedType)(M: Sfun U). Module D := OT_as_DT U. Include WS_to_Finite_set D M. End S_to_Finite_set. + + diff --git a/theories/FSets/OrderedTypeAlt.v b/theories/FSets/OrderedTypeAlt.v index 4eaaca403..314a95068 100644 --- a/theories/FSets/OrderedTypeAlt.v +++ b/theories/FSets/OrderedTypeAlt.v @@ -17,8 +17,8 @@ Require Import OrderedType. (** * An alternative (but equivalent) presentation for an Ordered Type inferface. *) -(** NB: [comparison], defined in [theories/Init/datatypes.v] is [Eq|Lt|Gt] -whereas [compare], defined in [theories/FSets/OrderedType.v] is [EQ _ | LT _ | GT _ ] +(** NB: [comparison], defined in [Datatypes.v] is [Eq|Lt|Gt] +whereas [compare], defined in [OrderedType.v] is [EQ _ | LT _ | GT _ ] *) Module Type OrderedTypeAlt. @@ -103,24 +103,16 @@ Module OrderedType_to_Alt (O:OrderedType) <: OrderedTypeAlt. Lemma compare_sym : forall x y, (y?=x) = CompOpp (x?=y). Proof. - intros x y. - unfold compare. - destruct (O.compare y x); elim_comp; simpl; auto. + intros x y; unfold compare. + destruct O.compare; elim_comp; simpl; auto. Qed. Lemma compare_trans : forall c x y z, (x?=y) = c -> (y?=z) = c -> (x?=z) = c. Proof. intros c x y z. - destruct c; unfold compare. - destruct (O.compare x y); intros; try discriminate. - destruct (O.compare y z); intros; try discriminate. - elim_comp; auto. - destruct (O.compare x y); intros; try discriminate. - destruct (O.compare y z); intros; try discriminate. - elim_comp; auto. - destruct (O.compare x y); intros; try discriminate. - destruct (O.compare y z); intros; try discriminate. + destruct c; unfold compare; + do 2 (destruct O.compare; intros; try discriminate); elim_comp; auto. Qed. |