diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract/ZProperties.v')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZProperties.v | 25 |
1 files changed, 18 insertions, 7 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v index 8973df358..446fd7eb8 100644 --- a/theories/Numbers/Integer/Abstract/ZProperties.v +++ b/theories/Numbers/Integer/Abstract/ZProperties.v @@ -9,11 +9,22 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor ZGcd ZLcm NZLog NZSqrt ZBits. -(** This functor summarizes all known facts about Z. *) +(** The two following functors summarize all known facts about N. -Module Type ZProp (Z:ZAxiomsSig) := - ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z - <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z - <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z - <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z - <+ ZBitsProp Z. + - [ZBasicProp] provides properties of basic functions: + + - * min max <= < + + - [ZExtraProp] provides properties of advanced functions: + pow, sqrt, log2, div, gcd, and bitwise functions. + + If necessary, the earlier all-in-one functor [ZProp] + could be re-obtained via [ZBasicProp <+ ZExtraProp] *) + +Module Type ZBasicProp (Z:ZAxiomsMiniSig) := ZMaxMinProp Z. + +Module Type ZExtraProp (Z:ZAxiomsSig)(P:ZBasicProp Z) := + ZSgnAbsProp Z P <+ ZParityProp Z P <+ ZPowProp Z P + <+ NZSqrtProp Z Z P <+ NZSqrtUpProp Z Z P + <+ NZLog2Prop Z Z Z P <+ NZLog2UpProp Z Z Z P + <+ ZDivProp Z P <+ ZQuotProp Z P <+ ZGcdProp Z P <+ ZLcmProp Z P + <+ ZBitsProp Z P. |