diff options
author | 2010-10-14 11:37:33 +0000 | |
---|---|---|
committer | 2010-10-14 11:37:33 +0000 | |
commit | 888c41d2bf95bb84fee28a8737515c9ff66aa94e (patch) | |
tree | 80c67a7a2aa22cabc94335bc14dcd33bed981417 /theories/Numbers/Rational | |
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/Rational')
-rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index d850f927a..6bb9c2ac4 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -937,8 +937,8 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Definition power_pos (x : t) p : t := match x with - | Qz zx => Qz (Z.power_pos zx p) - | Qq nx dx => Qq (Z.power_pos nx p) (N.power_pos dx p) + | Qz zx => Qz (Z.pow_pos zx p) + | Qq nx dx => Qq (Z.pow_pos nx p) (N.pow_pos dx p) end. Theorem spec_power_pos : forall x p, [power_pos x p] == [x] ^ Zpos p. @@ -946,25 +946,25 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. intros [ z | n d ] p; unfold power_pos. (* Qz *) simpl. - rewrite Z.spec_power_pos. + rewrite Z.spec_pow_pos. rewrite Qpower_decomp. red; simpl; f_equal. rewrite Zpower_pos_1_l; auto. (* Qq *) simpl. - rewrite Z.spec_power_pos. + rewrite Z.spec_pow_pos. destr_eqb; nzsimpl; intros. apply Qeq_sym; apply Qpower_positive_0. - rewrite N.spec_power_pos in *. + rewrite N.spec_pow_pos in *. assert (0 < N.to_Z d ^ ' p)%Z by (apply Zpower_gt_0; auto with zarith). romega. - rewrite N.spec_power_pos, H in *. + rewrite N.spec_pow_pos, H in *. rewrite Zpower_0_l in H0; [romega|discriminate]. rewrite Qpower_decomp. red; simpl; do 3 f_equal. rewrite Z2P_correct by (generalize (N.spec_pos d); romega). - rewrite N.spec_power_pos. auto. + rewrite N.spec_pow_pos. auto. Qed. Instance strong_spec_power_pos x p `(Reduced x) : Reduced (power_pos x p). @@ -979,10 +979,10 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. revert H. unfold Reduced; rewrite strong_spec_red, Qred_iff; simpl. destr_eqb; nzsimpl; simpl; intros. - rewrite N.spec_power_pos in H0. + rewrite N.spec_pow_pos in H0. rewrite H, Zpower_0_l in *; [romega|discriminate]. rewrite Z2P_correct in *; auto. - rewrite N.spec_power_pos, Z.spec_power_pos; auto. + rewrite N.spec_pow_pos, Z.spec_pow_pos; auto. rewrite Zgcd_1_rel_prime in *. apply rel_prime_Zpower; auto with zarith. Qed. |