Add sqrt in Numbers

 As for power recently, we add a specification in NZ,N,Z,
 derived properties, implementations for nat, N, Z, BigN, BigZ.

  - For nat, this sqrt is brand new :-), cf NPeano.v

  - For Z, we rework what was in Zsqrt: same algorithm,
    no more refine but a pure function, based now on a sqrt
    for positive, from which we derive a Nsqrt and a Zsqrt.
    For the moment, the old Zsqrt.v file is kept as Zsqrt_compat.v.
    It is not loaded by default by Require ZArith.
    New definitions are now in Psqrt.v, Zsqrt_def.v and Nsqrt_def.v

  - For BigN, BigZ, we changed the specifications to refer to Zsqrt
    instead of using characteristic inequations.

 On the way, many extensions, in particular BinPos (lemmas about order),
 NZMulOrder (results about squares)

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

7 files changed, 48 insertions, 27 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAxioms.v b/theories/Numbers/Integer/Abstract/ZAxioms.v
index 38855a85d..4f88008be 100644
--- a/theories/Numbers/Integer/Abstract/ZAxioms.v
+++ b/theories/Numbers/Integer/Abstract/ZAxioms.v
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 Require Export NZAxioms.
-Require Import NZPow.
+Require Import NZPow NZSqrt.
 
 (** We obtain integers by postulating that successor of predecessor
     is identity. *)
@@ -76,15 +76,20 @@ 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.
 
 (** Let's group everything *)
 
 Module Type ZAxiomsSig :=
   ZAxiomsMiniSig <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow <+ ZPowSpecNeg.
+   <+ NZPow.NZPow <+ ZPowSpecNeg <+ NZSqrt.NZSqrt <+ ZSqrtSpecNeg.
 Module Type ZAxiomsSig' :=
   ZAxiomsMiniSig' <+ HasCompare <+ HasAbs <+ HasSgn <+ Parity
-   <+ NZPow.NZPow' <+ ZPowSpecNeg.
+   <+ NZPow.NZPow' <+ ZPowSpecNeg <+ NZSqrt.NZSqrt' <+ ZSqrtSpecNeg.
 
 
 (** Division is left apart, since many different flavours are available *)
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 25989b2d4..1010a0f2f 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -92,14 +92,7 @@ Qed.
 
 Notation mul_nonpos := le_mul_0 (only parsing).
 
-Theorem le_0_square : forall n, 0 <= n * n.
-Proof.
-intro n; destruct (neg_nonneg_cases n).
-apply lt_le_incl; now apply mul_neg_neg.
-now apply mul_nonneg_nonneg.
-Qed.
-
-Notation square_nonneg := le_0_square (only parsing).
+Notation le_0_square := square_nonneg (only parsing).
 
 Theorem nlt_square_0 : forall n, ~ n * n < 0.
 Proof.
diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 7b9c6f452..8b34e5b2d 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -11,6 +11,5 @@ Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow.
 (** This functor summarizes all known facts about Z. *)
 
 Module Type ZProp (Z:ZAxiomsSig) :=
- ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z.
-
-
+ ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
+ <+ NZSqrt.NZSqrtProp Z Z.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index f9490cc9c..099554cd0 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -338,15 +338,14 @@ Module Make (N:NType) <: ZType.
   | Neg nx => Neg N.zero
   end.
 
- Theorem spec_sqrt: forall x, 0 <= to_Z x ->
-   to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
+ Theorem spec_sqrt: forall x, to_Z (sqrt x) = Zsqrt (to_Z x).
  Proof.
- unfold to_Z, sqrt; intros [x | x] H.
-   exact (N.spec_sqrt x).
- replace (N.to_Z x) with 0.
-   rewrite N.spec_0; simpl Zpower; unfold Zpower_pos, iter_pos;
-    auto with zarith.
- generalize (N.spec_pos x); auto with zarith.
+  destruct x as [p|p]; simpl.
+  apply N.spec_sqrt.
+  rewrite N.spec_0.
+  destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ].
+  rewrite Zsqrt_neg; auto with zarith.
+  now rewrite <- EQ.
  Qed.
 
  Definition div_eucl x y :=
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 5f8728394..ee75e4aa1 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -10,7 +10,7 @@
 
 
 Require Import ZAxioms ZProperties.
-Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven.
+Require Import BinInt Zcompare Zorder ZArith_dec Zbool Zeven Zsqrt_def.
 
 Local Open Scope Z_scope.
 
@@ -174,6 +174,17 @@ Definition pow_succ_r := Zpow_succ_r.
 Definition pow_neg := Zpow_neg.
 Definition pow := Zpow.
 
+(** Sqrt *)
+
+(** NB : we use a new Zsqrt defined in Zsqrt_def, the previous
+   module Zsqrt.v is now Zsqrt_compat.v *)
+
+Program Instance sqrt_wd : Proper (eq==>eq) Zsqrt.
+
+Definition sqrt_spec := Zsqrt_spec.
+Definition sqrt_neg := Zsqrt_neg.
+Definition sqrt := Zsqrt.
+
 (** We define [eq] only here to avoid refering to this [eq] above. *)
 
 Definition eq := (@eq Z).
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index be201f2d6..37f5b294e 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -78,13 +78,12 @@ Module Type ZType.
  Parameter spec_pow_pos: forall x n, [pow_pos x n] = [x] ^ Zpos n.
  Parameter spec_pow_N: forall x n, [pow_N x n] = [x] ^ Z_of_N n.
  Parameter spec_pow: forall x n, [pow x n] = [x] ^ [n].
- Parameter spec_sqrt: forall x, 0 <= [x] ->
-   [sqrt x] ^ 2 <= [x] < ([sqrt x] + 1) ^ 2.
+ Parameter spec_sqrt: forall x, [sqrt x] = Zsqrt [x].
  Parameter spec_div_eucl: forall x y,
    let (q,r) := div_eucl x y in ([q], [r]) = Zdiv_eucl [x] [y].
  Parameter spec_div: forall x y, [div x y] = [x] / [y].
  Parameter spec_modulo: forall x y, [modulo x y] = [x] mod [y].
- Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b).
+ Parameter spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].
  Parameter spec_sgn : forall x, [sgn x] = Zsgn [x].
  Parameter spec_abs : forall x, [abs x] = Zabs [x].
  Parameter spec_even : forall x, even x = Zeven_bool [x].
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 3e6375543..d632d2260 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -18,7 +18,7 @@ Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
  spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
- spec_mul spec_opp spec_of_Z spec_div spec_modulo
+ spec_mul spec_opp spec_of_Z spec_div spec_modulo spec_sqrt
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_even spec_odd
  : zsimpl.
@@ -278,6 +278,21 @@ Proof.
  intros a b. red. now rewrite spec_pow_N, spec_pow_pos.
 Qed.
 
+(** Sqrt *)
+
+Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
+
+Lemma sqrt_spec : forall n, 0<=n ->
+ (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
+Proof.
+ intros n. zify. apply Zsqrt_spec.
+Qed.
+
+Lemma sqrt_neg : forall n, n<0 -> sqrt n == 0.
+Proof.
+ intros n. zify. apply Zsqrt_neg.
+Qed.
+
 (** Even / Odd *)
 
 Definition Even n := exists m, n == 2*m.