diff options
author | 2009-11-03 08:24:06 +0000 | |
---|---|---|
committer | 2009-11-03 08:24:06 +0000 | |
commit | 4f0ad99adb04e7f2888e75f2a10e8c916dde179b (patch) | |
tree | 4b52d7436fe06f4b2babfd5bfed84762440e7de7 /theories/Structures/DecidableType2Ex.v | |
parent | 4e68924f48d3f6d5ffdf1cd394b590b5a6e15ea1 (diff) |
OrderedType implementation for various numerical datatypes + min/max structures
- A richer OrderedTypeFull interface : OrderedType + predicate "le"
- Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
- By the way: as suggested by S. Lescuyer, specification of compare is
now inductive
- GenericMinMax: axiomatisation + properties of min and max out of
OrderedTypeFull structures.
- MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
with also some domain-specific results, and compatibility layer
with already existing results.
- Some ML code of plugins had to be adapted, otherwise wrong "eq",
"lt" or simimlar constants were found by functions like coq_constant.
- Beware of the aliasing problems: for instance eq:=@eq t instead of
eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
instead of Z in statement of Zmax_spec).
- Some Morphism declaration are now ambiguous: switch to new syntax
anyway.
- Misc adaptations of FSets/MSets
- Classes/RelationPairs.v: from two relations over A and B, we
inspect relations over A*B and their properties in terms of classes.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12461 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Structures/DecidableType2Ex.v')
-rw-r--r-- | theories/Structures/DecidableType2Ex.v | 44 |
1 files changed, 6 insertions, 38 deletions
diff --git a/theories/Structures/DecidableType2Ex.v b/theories/Structures/DecidableType2Ex.v index 7b9c052ec..2ce2b5662 100644 --- a/theories/Structures/DecidableType2Ex.v +++ b/theories/Structures/DecidableType2Ex.v @@ -8,61 +8,29 @@ (* $Id$ *) -Require Import DecidableType2. +Require Import DecidableType2 Morphisms RelationPairs. 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 Inline t : Type. - Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. - 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 shortcut for easily building a UsualDecidableType *) - -Module Type MiniDecidableType. - Parameter Inline t : Type. - Parameter eq_dec : forall x y:t, { x=y }+{ x<>y }. -End MiniDecidableType. - -Module Make_UDT (M:MiniDecidableType) <: UsualDecidableType. - Definition t:=M.t. - Definition eq := @eq t. - Program Instance eq_equiv : Equivalence eq. - Definition eq_dec := M.eq_dec. -End Make_UDT. (** From two decidable types, we can build a new DecidableType over their cartesian product. *) Module PairDecidableType(D1 D2:DecidableType) <: DecidableType. - Definition t := prod D1.t D2.t. + Definition t := (D1.t * D2.t)%type. - Definition eq x y := D1.eq (fst x) (fst y) /\ D2.eq (snd x) (snd y). + Definition eq := (D1.eq * D2.eq)%signature. Instance eq_equiv : Equivalence eq. - Proof. - constructor. - intros (x1,x2); red; simpl; auto. - intros (x1,x2) (y1,y2); unfold eq; simpl; intuition. - intros (x1,x2) (y1,y2) (z1,z2); unfold eq; simpl; intuition eauto. - Qed. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. Proof. intros (x1,x2) (y1,y2); unfold eq; simpl. - destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); intuition. + destruct (D1.eq_dec x1 y1); destruct (D2.eq_dec x2 y2); + compute; intuition. Defined. End PairDecidableType. @@ -70,7 +38,7 @@ End PairDecidableType. (** Similarly for pairs of UsualDecidableType *) Module PairUsualDecidableType(D1 D2:UsualDecidableType) <: UsualDecidableType. - Definition t := prod D1.t D2.t. + Definition t := (D1.t * D2.t)%type. Definition eq := @eq t. Program Instance eq_equiv : Equivalence eq. Definition eq_dec : forall x y, { eq x y }+{ ~eq x y }. |