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 --- plugins/setoid_ring/Field_theory.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'plugins/setoid_ring') diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 205bef6d57..9617d40916 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -439,11 +439,11 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool := | _, _ => false end. -Add Morphism (pow_pos rmul) : pow_morph. +Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph. intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH]. Qed. -Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph. +Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph. intros x y H [|p];simpl;auto. apply pow_morph;trivial. Qed. (* -- cgit v1.2.3