Numbers: specs about sqrt and pow of neg numbers, even in NZ

 These additional specs are useless (but trivially provable) for N.
 They are quite convenient when deriving properties in NZ.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13603 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 9 insertions, 62 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 4f88008be4..6e6cd7f0fc 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -70,26 +70,16 @@ Module Type Parity (Import Z : ZAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** For the power function, we just add to NZPow an addition spec *)
-
-Module Type ZPowSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Pow' Z).
- Axiom pow_neg : forall a b, b<0 -> a^b == 0.
-End ZPowSpecNeg.
-
-(** Same for the sqrt function. *)
-
-Module Type ZSqrtSpecNeg (Import Z : ZAxiomsMiniSig')(Import P : Sqrt' Z).
- Axiom sqrt_neg : forall a, a<0 -> √a == 0.
-End ZSqrtSpecNeg.
+(** For the power and sqrt functions, the NZ axiomatizations are enough. *)
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ ZPowSpecNeg <+ NZSqrt.NZSqrt <+ ZSqrtSpecNeg.
+   <+ NZPow.NZPow <+ NZSqrt.NZSqrt.
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ ZPowSpecNeg <+ NZSqrt.NZSqrt' <+ ZSqrtSpecNeg.
+   <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'.
 
 
 (** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 0241c34762..8ea0122506 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -18,49 +18,6 @@ Module Type ZPowProp
 
  Include NZPowProp A A B.
 
-(** Many results are directly the same as in NZPow, hence
-    the Include above. We extend nonetheless a few of them,
-    and add some results concerning negative first arg.
-*)
-
-Lemma pow_mul_l' : forall a b c, (a*b)^c == a^c * b^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 c). now apply pow_mul_l.
- rewrite !pow_neg by trivial. now nzsimpl.
-Qed.
-
-Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.
-Proof.
- intros a b Ha. destruct (le_gt_cases 0 b).
- now apply pow_nonneg_nonneg.
- rewrite !pow_neg by trivial. order.
-Qed.
-
-Lemma pow_le_mono_l' : forall a b c, 0<=a<=b -> a^c <= b^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 c). now apply pow_le_mono_l.
- rewrite !pow_neg by trivial. order.
-Qed.
-
-(** NB: since 0^0 > 0^1, the following result isn't valid with a=0 *)
-
-Lemma pow_le_mono_r' : forall a b c, 0<a -> b<=c -> a^b <= a^c.
-Proof.
- intros a b c. destruct (le_gt_cases 0 b).
- intros. apply pow_le_mono_r; try split; trivial.
- rewrite !pow_neg by trivial.
- intros. apply pow_nonneg. order.
-Qed.
-
-Lemma pow_le_mono' : forall a b c d, 0<a<=c -> b<=d ->
- a^b <= c^d.
-Proof.
- intros a b c d. destruct (le_gt_cases 0 b).
- intros. apply pow_le_mono. trivial. split; trivial.
- rewrite !pow_neg by trivial.
- intros. apply pow_nonneg. intuition order.
-Qed.
-
 (** Parity of power *)
 
 Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.
@@ -86,7 +43,7 @@ Proof.
  rewrite 2 pow_2_r.
  now rewrite mul_opp_opp.
  assert (2*c < 0) by (apply mul_pos_neg; order').
- now rewrite !pow_neg.
+ now rewrite !pow_neg_r.
 Qed.
 
 Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
@@ -98,7 +55,7 @@ Proof.
  rewrite pow_opp_even by (now exists c).
  apply mul_opp_l.
  apply double_above in GT. rewrite mul_0_r in GT.
- rewrite !pow_neg by trivial. now rewrite opp_0.
+ rewrite !pow_neg_r by trivial. now rewrite opp_0.
 Qed.
 
 Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.
@@ -126,7 +83,7 @@ Proof.
  assert (b~=0) by
   (contradict H; now rewrite H, <-odd_spec, <-negb_even_odd, even_0).
  order.
- now rewrite pow_neg.
+ now rewrite pow_neg_r.
  rewrite abs_neq by order.
  rewrite pow_opp_odd; trivial.
  now rewrite mul_opp_opp, mul_1_l.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index ee75e4aa18..48d166c0ab 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -39,7 +39,7 @@ Proof.
  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.
+Lemma Zpow_neg_r : forall a b, b<0 -> Zpow a b = 0.
 Proof.
  now destruct b.
 Qed.
@@ -171,7 +171,7 @@ 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_neg_r := Zpow_neg_r.
 Definition pow := Zpow.
 
 (** Sqrt *)
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index d632d22607..c2965016ad 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -261,7 +261,7 @@ Proof.
  simpl. unfold Zpower_pos; simpl. ring.
 Qed.
 
-Lemma pow_neg : forall a b, b<0 -> a^b == 0.
+Lemma pow_neg_r : forall a b, b<0 -> a^b == 0.
 Proof.
  intros a b. zify. intros Hb.
  destruct [b]; reflexivity || discriminate.