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

5 files changed, 34 insertions, 15 deletions

diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
index 92e90b9c80..4a9cf536be 100644
--- a/theories/Numbers/Natural/Abstract/NSqrt.v
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -22,17 +22,17 @@ Module NSqrtProp (Import A : NAxiomsSig')(Import B : NSubProp A).
 Lemma sqrt_spec' : forall a, √a*√a <= a < S (√a) * S (√a).
 Proof. wrap sqrt_spec. Qed.
 
-Lemma sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b.
-Proof. wrap sqrt_unique. Qed.
+Definition sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b
+ := sqrt_unique.
 
 Lemma sqrt_square : forall a, √(a*a) == a.
 Proof. wrap sqrt_square. Qed.
 
-Lemma sqrt_le_mono : forall a b, a<=b -> √a <= √b.
-Proof. wrap sqrt_le_mono. Qed.
+Definition sqrt_le_mono : forall a b, a<=b -> √a <= √b
+ := sqrt_le_mono.
 
-Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
-Proof. wrap sqrt_lt_cancel. Qed.
+Definition sqrt_lt_cancel : forall a b, √a < √b -> a < b
+ := sqrt_lt_cancel.
 
 Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a.
 Proof. wrap sqrt_le_square. Qed.
@@ -44,19 +44,20 @@ Definition sqrt_0 := sqrt_0.
 Definition sqrt_1 := sqrt_1.
 Definition sqrt_2 := sqrt_2.
 
-Definition sqrt_lt_lin : forall a, 1<a -> √a<a := sqrt_lt_lin.
+Definition sqrt_lt_lin : forall a, 1<a -> √a<a
+ := sqrt_lt_lin.
 
-Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
+Lemma sqrt_le_lin : forall a, √a<=a.
 Proof. wrap sqrt_le_lin. Qed.
 
-Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
-Proof. wrap sqrt_mul_below. Qed.
+Definition sqrt_mul_below : forall a b, √a * √b <= √(a*b)
+ := sqrt_mul_below.
 
 Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b).
 Proof. wrap sqrt_mul_above. Qed.
 
-Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
-Proof. wrap sqrt_add_le. Qed.
+Definition sqrt_add_le : forall a b, √(a+b) <= √a + √b
+ := sqrt_add_le.
 
 Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)).
 Proof. wrap add_sqrt_le. Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index ec0fa89bff..60a836d416 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -746,7 +746,7 @@ Module Make (W0:CyclicType) <: NType.
  Theorem spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
  Proof.
   intros x.
-  symmetry. apply Z.sqrt_unique. apply spec_pos.
+  symmetry. apply Z.sqrt_unique.
   rewrite <- ! Zpower_2. apply spec_sqrt_aux.
  Qed.
 
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 348eee5ed2..8b7b06966f 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -163,14 +163,18 @@ Definition odd_spec := Nodd_spec.
 
 (** Power *)
 
+Program Instance pow_wd : Proper (eq==>eq==>eq) Npow.
 Definition pow_0_r := Npow_0_r.
 Definition pow_succ_r n p (H:0 <= p) := Npow_succ_r n p.
-Program Instance pow_wd : Proper (eq==>eq==>eq) Npow.
+Lemma pow_neg_r : forall a b, b<0 -> a^b = 0.
+Proof. destruct b; discriminate. Qed.
 
 (** Sqrt *)
 
 Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt.
 Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n.
+Lemma sqrt_neg : forall a, a<0 -> Nsqrt a = 0.
+Proof. destruct a; discriminate. Qed.
 
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index b91b43e310..de5ef47872 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -369,10 +369,12 @@ Definition odd_spec := odd_spec.
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 Definition pow_0_r := pow_0_r.
 Definition pow_succ_r := pow_succ_r.
+Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
 Definition pow := pow.
 
-Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
 Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
+Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
+Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed.
 Definition sqrt := sqrt.
 
 Definition div := div.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index f072fc24aa..f242951e54 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -204,6 +204,12 @@ Proof.
  simpl. unfold Zpower_pos; simpl. ring.
 Qed.
 
+Lemma pow_neg_r : forall a b, b<0 -> a^b == 0.
+Proof.
+ intros a b. zify. intro Hb. exfalso.
+ generalize (spec_pos b); omega.
+Qed.
+
 Lemma pow_pow_N : forall a b, a^b == pow_N a (to_N b).
 Proof.
  intros. zify. f_equal.
@@ -230,6 +236,12 @@ Proof.
  intros n. zify. apply Zsqrt_spec.
 Qed.
 
+Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
+Proof.
+ intros n. zify. intro H. exfalso.
+ generalize (spec_pos n); omega.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.