From ca96d3477993d102d6cc42166eab52516630d181 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 20 Jun 2011 17:18:39 +0000 Subject: Arithemtic: more concerning compare, eqb, leb, ltb Start of a uniform treatment of compare, eqb, leb, ltb: - We now ensure that they are provided by N,Z,BigZ,BigN,Nat and Pos - Some generic properties are derived in OrdersFacts.BoolOrderFacts In BinPos, more work about sub_mask with nice implications on compare (e.g. simplier proof of lt_trans). In BinNat/BinPos, for uniformity, compare_antisym is now (y ?= x) = CompOpp (x ?=y) instead of the symmetrical result. In BigN / BigZ, eq_bool is now eqb In BinIntDef, gtb and geb are kept for the moment, but a comment advise to rather use ltb and leb. Z.div now uses Z.ltb and Z.leb. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14227 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Integer/Abstract/ZAxioms.v | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) (limited to 'theories/Numbers/Integer/Abstract') diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v index 237ac93ef5..a5be98aab0 100644 --- a/theories/Numbers/Integer/Abstract/ZAxioms.v +++ b/theories/Numbers/Integer/Abstract/ZAxioms.v @@ -111,14 +111,12 @@ Module Type ZQuot' (Z:ZAxiomsMiniSig) := QuotRem' Z <+ QuotRemSpec Z. (** Let's group everything *) -Module Type ZAxiomsSig := - ZAxiomsMiniSig <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn - <+ NZParity.NZParity +Module Type ZAxiomsSig := ZAxiomsMiniSig <+ OrderFunctions + <+ HasAbs <+ HasSgn <+ NZParity.NZParity <+ NZPow.NZPow <+ NZSqrt.NZSqrt <+ NZLog.NZLog2 <+ NZGcd.NZGcd <+ ZDiv <+ ZQuot <+ NZBits.NZBits. -Module Type ZAxiomsSig' := - ZAxiomsMiniSig' <+ HasCompare <+ HasEqBool <+ HasAbs <+ HasSgn - <+ NZParity.NZParity +Module Type ZAxiomsSig' := ZAxiomsMiniSig' <+ OrderFunctions' + <+ HasAbs <+ HasSgn <+ NZParity.NZParity <+ NZPow.NZPow' <+ NZSqrt.NZSqrt' <+ NZLog.NZLog2 <+ NZGcd.NZGcd' <+ ZDiv' <+ ZQuot' <+ NZBits.NZBits'. -- cgit v1.2.3