From 211030a7a870bdf3bc36b0923379e2d1bf6c729a Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 17 Dec 2008 15:31:54 +0000 Subject: FSet/OrderedType now includes an eq_dec, and hence become an extension of DecidableType After lots of hesitations, OrderedType now requires this "eq_dec" field, which is redundant (can be deduced from "compare"), but allows the subtyping relation DecidableType <= OrderedType, and hence WS <= S : ordered sets are now truly extensions of weak sets. Of course this change introduces a last-minute incompatibility, but: - There is a clear gain in term of functionnality / simplicity. - FSets 8.2 already needs some adaptations when compared with 8.1, so it's the right time to push such incompatible changes. - Transition shouldn't be too hard: the old OrderedType still exists under the name MiniOrderedType, and functor MOT_to_OT allows to convert from one to the other. Beware, for a FSetInterface.WS (resp. S) to be coercible to a DecidableType (resp. OrderedType), an eq_dec on sets is now required in these interfaces and in the implementations. In pratice, it is really easy to build from equal and equal_1 and equal_2. Some name changes : in FSetFacts, old WFacts now correspond to WFacts_fun, while WFacts now expects only one argument (WFacts M := WFacts_fun M.E M). Idem with WDecide, WProperties and WEqProperties. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11693 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Logic/DecidableTypeEx.v | 24 ++++++++---------------- 1 file changed, 8 insertions(+), 16 deletions(-) (limited to 'theories/Logic') diff --git a/theories/Logic/DecidableTypeEx.v b/theories/Logic/DecidableTypeEx.v index 30a7bb633..57a2248b3 100644 --- a/theories/Logic/DecidableTypeEx.v +++ b/theories/Logic/DecidableTypeEx.v @@ -46,24 +46,16 @@ Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. Definition eq_dec := M.eq_dec. End Make_UDT. -(** 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. +(** An OrderedType can now directly be seen as a DecidableType *) + +Module OT_as_DT (O:OrderedType) <: DecidableType := O. (** (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). +Module Nat_as_DT <: UsualDecidableType := Nat_as_OT. +Module Positive_as_DT <: UsualDecidableType := Positive_as_OT. +Module N_as_DT <: UsualDecidableType := N_as_OT. +Module Z_as_DT <: UsualDecidableType := Z_as_OT. (** From two decidable types, we can build a new DecidableType over their cartesian product. *) @@ -99,7 +91,7 @@ End PairDecidableType. (** Similarly for pairs of UsualDecidableType *) -Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: DecidableType. +Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. Definition t := prod D1.t D2.t. Definition eq := @eq t. Definition eq_refl := @refl_equal t. -- cgit v1.2.3