From 4f0ad99adb04e7f2888e75f2a10e8c916dde179b Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 3 Nov 2009 08:24:06 +0000 Subject: 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 --- theories/FSets/FSetCompat.v | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) (limited to 'theories/FSets/FSetCompat.v') diff --git a/theories/FSets/FSetCompat.v b/theories/FSets/FSetCompat.v index 487b4fc32..f6d5ae1ac 100644 --- a/theories/FSets/FSetCompat.v +++ b/theories/FSets/FSetCompat.v @@ -209,11 +209,10 @@ Module Backport_Sets Qed. Definition compare : forall s s', Compare lt eq s s'. Proof. - intros s s'. generalize (M.compare_spec s s'). - destruct (M.compare s s'); simpl; intros. - constructor 2; auto. - constructor 1; auto. - constructor 3; auto. + intros s s'. + assert (H := M.compare_spec s s'). + destruct (M.compare s s'); [ apply EQ | apply LT | apply GT ]; + inversion H; auto. Defined. End Backport_Sets. @@ -407,7 +406,7 @@ Module Update_Sets | GT _ => Gt end. - Lemma compare_spec : forall s s', Cmp eq lt (compare s s') s s'. + Lemma compare_spec : forall s s', Cmp eq lt s s' (compare s s'). Proof. intros; unfold compare; destruct M.compare; auto. Qed. End Update_Sets. -- cgit v1.2.3