diff options
Diffstat (limited to 'theories/FSets')
-rw-r--r-- | theories/FSets/DecidableType.v | 7 | ||||
-rw-r--r-- | theories/FSets/DecidableTypeEx.v | 50 | ||||
-rw-r--r-- | theories/FSets/FMapWeak.v | 2 | ||||
-rw-r--r-- | theories/FSets/FSetWeak.v | 1 |
4 files changed, 59 insertions, 1 deletions
diff --git a/theories/FSets/DecidableType.v b/theories/FSets/DecidableType.v index 4e34bbc0d..a4de6ca7f 100644 --- a/theories/FSets/DecidableType.v +++ b/theories/FSets/DecidableType.v @@ -31,6 +31,7 @@ Module Type DecidableType. End DecidableType. +(** * Additional notions about keys and datas used in FMap *) Module KeyDecidableType(D:DecidableType). Import D. @@ -147,5 +148,9 @@ Module KeyDecidableType(D:DecidableType). Hint Unfold MapsTo In. Hint Resolve In_inv_2 In_inv_3. - End KeyDecidableType. + + + + + diff --git a/theories/FSets/DecidableTypeEx.v b/theories/FSets/DecidableTypeEx.v new file mode 100644 index 000000000..dcca37095 --- /dev/null +++ b/theories/FSets/DecidableTypeEx.v @@ -0,0 +1,50 @@ +(***********************************************************************) +(* 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 *) +(***********************************************************************) + +(* $Id$ *) + +Require Import DecidableType OrderedType OrderedTypeEx. +Set Implicit Arguments. +Unset Strict Implicit. + +(** * Examples of Decidable Type structures. *) + +(** A particular case of [DecidableType] where + the equality is the usual one of Coq. *) + +Module Type UsualDecidableType. + Parameter t : Set. + Definition eq := @eq t. + Definition eq_refl := @refl_equal t. + Definition eq_sym := @sym_eq t. + Definition eq_trans := @trans_eq t. + Parameter eq_dec : forall x y, { eq x y }+{~eq x y }. +End UsualDecidableType. + +(** a [UsualDecidableType] is in particular an [DecidableType]. *) + +Module UDT_to_DT (U:UsualDecidableType) <: DecidableType := U. + +(** An OrderedType can be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType. + Module OF := OrderedTypeFacts O. + Definition t := O.t. + Definition eq := O.eq. + Definition eq_refl := O.eq_refl. + Definition eq_sym := O.eq_sym. + Definition eq_trans := O.eq_trans. + Definition eq_dec := OF.eq_dec. +End OT_as_DT. + +(** (Usual) Decidable Type for [nat], [positive], [N], [Z] *) + +Module Nat_as_DT <: UsualDecidableType := OT_as_DT (Nat_as_OT). +Module Positive_as_DT <: UsualDecidableType := OT_as_DT (Positive_as_OT). +Module N_as_DT <: UsualDecidableType := OT_as_DT (N_as_OT). +Module Z_as_DT <: UsualDecidableType := OT_as_DT (Z_as_OT). diff --git a/theories/FSets/FMapWeak.v b/theories/FSets/FMapWeak.v index 7baeb2970..7bdee004e 100644 --- a/theories/FSets/FMapWeak.v +++ b/theories/FSets/FMapWeak.v @@ -8,5 +8,7 @@ (* $Id$ *) +Require Export DecidableType. +Require Export DecidableTypeEx. Require Export FMapWeakInterface. Require Export FMapWeakList. diff --git a/theories/FSets/FSetWeak.v b/theories/FSets/FSetWeak.v index ccf590ca3..8631841fb 100644 --- a/theories/FSets/FSetWeak.v +++ b/theories/FSets/FSetWeak.v @@ -9,6 +9,7 @@ (* $Id$ *) Require Export DecidableType. +Require Export DecidableTypeEx. Require Export FSetWeakInterface. Require Export FSetFacts. Require Export FSetProperties. |