diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:33 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-10-14 11:37:33 +0000 |
commit | 888c41d2bf95bb84fee28a8737515c9ff66aa94e (patch) | |
tree | 80c67a7a2aa22cabc94335bc14dcd33bed981417 /theories/Numbers/Natural/Abstract/NAxioms.v | |
parent | d7a3d9b4fbfdd0df8ab4d0475fc7afa1ed5f5bcb (diff) |
Numbers: new functions pow, even, odd + many reorganisations
- Simplification of functor names, e.g. ZFooProp instead of ZFooPropFunct
- The axiomatisations of the different fonctions are now in {N,Z}Axioms.v
apart for Z division (three separate flavours in there own files).
Content of {N,Z}AxiomsSig is extended, old version is {N,Z}AxiomsMiniSig.
- In NAxioms, the recursion field isn't that useful, since we axiomatize
other functions and not define them (apart in the toy NDefOps.v).
We leave recursion there, but in a separate NAxiomsFullSig.
- On Z, the pow function is specified to behave as Zpower : a^(-1)=0
- In BigN/BigZ, (power:t->N->t) is now pow_N, while pow is t->t->t
These pow could be more clever (we convert 2nd arg to N and use pow_N).
Default "^" is now (pow:t->t->t). BigN/BigZ ring is adapted accordingly
- In BigN, is_even is now even, its spec is changed to use Zeven_bool.
We add an odd. In BigZ, we add even and odd.
- In ZBinary (implem of ZAxioms by ZArith), we create an efficient Zpow
to implement pow. This Zpow should replace the current linear Zpower
someday.
- In NPeano (implem of NAxioms by Arith), we create pow, even, odd functions,
and we modify the div and mod functions for them to be linear, structural,
tail-recursive.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13546 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NAxioms.v')
-rw-r--r-- | theories/Numbers/Natural/Abstract/NAxioms.v | 65 |
1 files changed, 51 insertions, 14 deletions
diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v index fd5a35391..66ff2ded5 100644 --- a/theories/Numbers/Natural/Abstract/NAxioms.v +++ b/theories/Numbers/Natural/Abstract/NAxioms.v @@ -8,30 +8,67 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -Require Export NZAxioms. +Require Export NZAxioms NZPow NZDiv. -Set Implicit Arguments. +(** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *) -Module Type NAxioms (Import NZ : NZDomainSig'). +Module Type NAxiom (Import NZ : NZDomainSig'). + Axiom pred_0 : P 0 == 0. +End NAxiom. -Axiom pred_0 : P 0 == 0. +Module Type NAxiomsMiniSig := NZOrdAxiomsSig <+ NAxiom. +Module Type NAxiomsMiniSig' := NZOrdAxiomsSig' <+ NAxiom. -Parameter Inline recursion : forall A : Type, A -> (t -> A -> A) -> t -> A. -Implicit Arguments recursion [A]. -Declare Instance recursion_wd (A : Type) (Aeq : relation A) : - Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) (@recursion A). +(** Let's now add some more functions and their specification *) + +(** Parity functions *) + +Module Type Parity (Import N : NAxiomsMiniSig'). + Parameter Inline even odd : t -> bool. + Definition Even n := exists m, n == 2*m. + Definition Odd n := exists m, n == 2*m+1. + Axiom even_spec : forall n, even n = true <-> Even n. + Axiom odd_spec : forall n, odd n = true <-> Odd n. +End Parity. + +(** Power function : NZPow is enough *) + +(** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon, + and add to that a N-specific constraint. *) + +Module Type NDivSpecific (Import N : NAxiomsMiniSig')(Import DM : DivMod' N). + Axiom mod_upper_bound : forall a b, b ~= 0 -> a mod b < b. +End NDivSpecific. + + +(** We now group everything together. *) + +Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity + <+ NZPow.NZPow <+ DivMod <+ NZDivCommon <+ NDivSpecific. + +Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity + <+ NZPow.NZPow' <+ DivMod' <+ NZDivCommon <+ NDivSpecific. + + +(** It could also be interesting to have a constructive recursor function. *) + +Module Type NAxiomsRec (Import NZ : NZDomainSig'). + +Parameter Inline recursion : forall {A : Type}, A -> (t -> A -> A) -> t -> A. + +Declare Instance recursion_wd {A : Type} (Aeq : relation A) : + Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion. Axiom recursion_0 : - forall (A : Type) (a : A) (f : t -> A -> A), recursion a f 0 = a. + forall {A} (a : A) (f : t -> A -> A), recursion a f 0 = a. Axiom recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : t -> A -> A), + forall {A} (Aeq : relation A) (a : A) (f : t -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (S n)) (f n (recursion a f n)). -End NAxioms. - -Module Type NAxiomsSig := NZOrdAxiomsSig <+ NAxioms. -Module Type NAxiomsSig' := NZOrdAxiomsSig' <+ NAxioms. +End NAxiomsRec. +Module Type NAxiomsFullSig := NAxiomsSig <+ NAxiomsRec. +Module Type NAxiomsFullSig' := NAxiomsSig' <+ NAxiomsRec. |