diff options
author | 2010-01-05 15:24:29 +0000 | |
---|---|---|
committer | 2010-01-05 15:24:29 +0000 | |
commit | 9332ed8f53f544c0dccac637a88d09a252c3c653 (patch) | |
tree | fe59e48dd8bbce65a19b3e806c70e52db1ed0858 /theories/Numbers/NatInt/NZDiv.v | |
parent | b63cd131e8b4a5600973c860d2ccc6e3e5c8ce91 (diff) |
Division in Numbers: factorisation of signatures
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/NatInt/NZDiv.v')
-rw-r--r-- | theories/Numbers/NatInt/NZDiv.v | 18 |
1 files changed, 13 insertions, 5 deletions
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v index 1be2f8508..bb63b420b 100644 --- a/theories/Numbers/NatInt/NZDiv.v +++ b/theories/Numbers/NatInt/NZDiv.v @@ -12,20 +12,28 @@ Require Import NZAxioms NZMulOrder. Open Scope NumScope. -Module Type NZDiv (Import NZ : NZOrdAxiomsSig). +(** This first signature will be common to all divisions over NZ, N and Z *) +Module Type NZDivCommon (Import NZ : NZAxiomsSig). Parameter Inline div : t -> t -> t. Parameter Inline modulo : t -> t -> t. - Infix "/" := div : NumScope. Infix "mod" := modulo (at level 40, no associativity) : NumScope. - Declare Instance div_wd : Proper (eq==>eq==>eq) div. Declare Instance mod_wd : Proper (eq==>eq==>eq) modulo. - Axiom div_mod : forall a b, b ~= 0 -> a == b*(a/b) + (a mod b). - Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. +End NZDivCommon. +(** The different divisions will only differ in the conditions + they impose on [modulo]. For NZ, we only describe behavior + on positive numbers. + + NB: This axiom would also be true for N and Z, but redundant. +*) + +Module Type NZDiv (Import NZ : NZOrdAxiomsSig). + Include Type NZDivCommon NZ. + Axiom mod_bound : forall a b, 0<=a -> 0<b -> 0 <= a mod b < b. End NZDiv. Module Type NZDivSig := NZOrdAxiomsSig <+ NZDiv. |