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

1 files changed, 57 insertions, 5 deletions

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index e50eac17ad..28a37abf85 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,10 +10,40 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import BinInt Zcompare Zorder ZArith_dec Zbool.
+Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven.
 
 Local Open Scope Z_scope.
 
+(** An alternative Zpow *)
+
+(** The Zpow is extensionnaly equal to Zpower in ZArith, but not
+    convertible with it. This Zpow uses a logarithmic number of
+    multiplications instead of a linear one. We should try someday to
+    replace Zpower with this Zpow.
+*)
+
+Definition Zpow n m :=
+  match m with
+    | Z0 => 1
+    | Zpos p => Piter_op Zmult p n
+    | Zneg p => 0
+  end.
+
+Lemma Zpow_0_r : forall n, Zpow n 0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma Zpow_succ_r : forall a b, 0<=b -> Zpow a (Zsucc b) = a * Zpow a b.
+Proof.
+ intros a [|b|b] Hb; [ | |now elim Hb]; simpl.
+ now rewrite Zmult_1_r.
+ rewrite <- Pplus_one_succ_r. apply Piter_op_succ. apply Zmult_assoc.
+Qed.
+
+Lemma Zpow_neg : forall a b, b<0 -> Zpow a b = 0.
+Proof.
+ now destruct b.
+Qed.
+
 Theorem Z_bi_induction :
   forall A : Z -> Prop, Proper (eq ==> iff) A ->
     A 0 -> (forall n : Z, A n <-> A (Zsucc n)) -> forall n : Z, A n.
@@ -24,11 +54,10 @@ intros; rewrite <- Zsucc_succ'. now apply -> AS.
 intros n H. rewrite <- Zpred_pred'. rewrite Zsucc_pred in H. now apply <- AS.
 Qed.
 
-
-(** * Implementation of [ZAxiomsSig] by [BinInt.Z] *)
+(** * Implementation of [ZAxiomsMiniSig] by [BinInt.Z] *)
 
 Module Z
- <: ZAxiomsExtSig <: UsualOrderedTypeFull <: TotalOrder
+ <: ZAxiomsSig <: UsualOrderedTypeFull <: TotalOrder
  <: UsualDecidableTypeFull.
 
 Definition t := Z.
@@ -110,13 +139,36 @@ Definition sgn_null := Zsgn_0.
 Definition sgn_pos := Zsgn_1.
 Definition sgn_neg := Zsgn_m1.
 
+(** Even and Odd *)
+
+Definition Even n := exists m, n=2*m.
+Definition Odd n := exists m, n=2*m+1.
+
+Lemma even_spec n : Zeven_bool n = true <-> Even n.
+Proof. rewrite Zeven_bool_iff. exact (Zeven_ex_iff n). Qed.
+
+Lemma odd_spec n : Zodd_bool n = true <-> Odd n.
+Proof. rewrite Zodd_bool_iff. exact (Zodd_ex_iff n). Qed.
+
+Definition even := Zeven_bool.
+Definition odd := Zodd_bool.
+
+(** Power *)
+
+Program Instance pow_wd : Proper (eq==>eq==>eq) Zpow.
+
+Definition pow_0_r := Zpow_0_r.
+Definition pow_succ_r := Zpow_succ_r.
+Definition pow_neg := Zpow_neg.
+Definition pow := Zpow.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
 
 (** Now the generic properties. *)
 
-Include ZPropFunct
+Include ZProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
 End Z.