diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:32 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-01-07 15:32:32 +0000 |
commit | 50411a16e71008f9d4f951e82637d1f38b02a58d (patch) | |
tree | b9da02a276a6fcbf4ccaa4992f59d3304b2365ad /theories/MSets | |
parent | 345c0ee557465d7d2f22ac34898388dfbb57cd0f (diff) |
MSetInterface: more modularity
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12637 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/MSets')
-rw-r--r-- | theories/MSets/MSetInterface.v | 44 |
1 files changed, 20 insertions, 24 deletions
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index b21c00fe2..effd5e35a 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -34,11 +34,11 @@ Require Export Bool SetoidList RelationClasses Morphisms Set Implicit Arguments. Unset Strict Implicit. -Module Type WOps (E : DecidableType). - - Definition elt := E.t. +Module Type TypElt. + Parameters t elt : Type. +End TypElt. - Parameter t : Type. (** the abstract type of sets *) +Module Type HasWOps (Import T:TypElt). Parameter empty : t. (** The empty set. *) @@ -112,9 +112,13 @@ Module Type WOps (E : DecidableType). the set is empty. Which element is chosen is unspecified. Equal sets could return different elements. *) -End WOps. - +End HasWOps. +Module Type WOps (E : DecidableType). + Definition elt := E.t. + Parameter t : Type. (** the abstract type of sets *) + Include Type HasWOps. +End WOps. (** ** Functorial signature for weak sets @@ -140,8 +144,8 @@ Module Type WSetsOn (E : DecidableType). Notation "s [<=] t" := (Subset s t) (at level 70, no associativity). Definition eq : t -> t -> Prop := Equal. - Declare Instance eq_equiv : Equivalence eq. (* obvious, for subtyping only *) - Parameter eq_dec : forall s s', { eq s s' } + { ~ eq s s' }. + Include Type IsEq. (** [eq] is obviously an equivalence, for subtyping only *) + Include Type HasEqDec. (** Specifications of set operators *) @@ -201,8 +205,7 @@ End WSets. Based on [WSetsOn], plus ordering on sets and [min_elt] and [max_elt] and some stronger specifications for other functions. *) -Module Type SetsOn (E : OrderedType). - Include Type WSetsOn E. +Module Type HasOrdOps (Import T:TypElt). Parameter compare : t -> t -> comparison. (** Total ordering between sets. Can be used as the ordering function @@ -217,11 +220,13 @@ Module Type SetsOn (E : OrderedType). (** Same as [min_elt], but returns the largest element of the given set. *) - Parameter lt : t -> t -> Prop. +End HasOrdOps. + +Module Type Ops (E : OrderedType) := WOps E <+ HasOrdOps. - (** Specification of [lt] *) - Declare Instance lt_strorder : StrictOrder lt. - Declare Instance lt_compat : Proper (eq==>eq==>iff) lt. + +Module Type SetsOn (E : OrderedType). + Include Type WSetsOn E <+ HasOrdOps <+ HasLt <+ IsStrOrder. Section Spec. Variable s s': t. @@ -554,16 +559,7 @@ End WRaw2Sets. (** Same approach for ordered sets *) Module Type RawSets (E : OrderedType). - Include Type WRawSets E. - - Parameter compare : t -> t -> comparison. - Parameter min_elt : t -> option elt. - Parameter max_elt : t -> option elt. - Parameter lt : t -> t -> Prop. - - (** Specification of [lt] *) - Declare Instance lt_strorder : StrictOrder lt. - Declare Instance lt_compat : Proper (eq==>eq==>iff) lt. + Include Type WRawSets E <+ HasOrdOps <+ HasLt <+ IsStrOrder. Section Spec. Variable s s': t. |