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

4 files changed, 82 insertions, 2 deletions

diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v
index ece3475dc..93121d48f 100644
--- a/theories/ZArith/ZArith.v
+++ b/theories/ZArith/ZArith.v
@@ -13,7 +13,7 @@ Require Export ZArith_base.
 (** Extra modules using [Omega] or [Ring]. *)
 
 Require Export Zcomplements.
-Require Export Zsqrt.
+Require Export Zsqrt_def.
 Require Export Zpower.
 Require Export Zdiv.
 Require Export Zlogarithm.
diff --git a/theories/ZArith/Zsqrt.v b/theories/ZArith/Zsqrt_compat.v
index 20fa6bb5a..ce46aa6d4 100644
--- a/theories/ZArith/Zsqrt.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -11,6 +11,16 @@ Require Import Omega.
 Require Export ZArith_base.
 Open Local Scope Z_scope.
 
+(**    !! This file is deprecated !!
+
+    Please use rather Zsqrt_def.Zsqrt (or Zsqrtrem).
+    Unlike here, proofs there are fully separated from functions.
+    Some equivalence proofs between the old and the new versions
+    can be found below. A Require Import ZArith provides by default
+    the new versions.
+
+*)
+
 (**********************************************************************)
 (** Definition and properties of square root on Z *)
 
@@ -211,3 +221,12 @@ Proof.
 Qed.
 
 
+(** Equivalence between Zsqrt_plain and [Zsqrt_def.Zsqrt] *)
+
+Lemma Zsqrt_equiv : forall n, Zsqrt_plain n = Zsqrt_def.Zsqrt n.
+Proof.
+ intros. destruct (Z_le_gt_dec 0 n).
+ symmetry. apply Z.sqrt_unique; trivial.
+ now apply Zsqrt_interval.
+ now destruct n.
+Qed.
\ No newline at end of file
diff --git a/theories/ZArith/Zsqrt_def.v b/theories/ZArith/Zsqrt_def.v
new file mode 100644
index 000000000..15f4e5275
--- /dev/null
+++ b/theories/ZArith/Zsqrt_def.v
@@ -0,0 +1,60 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Definition of a square root function for Z. *)
+
+Require Import BinPos BinInt Psqrt.
+
+Open Scope Z_scope.
+
+Definition Zsqrtrem n :=
+ match n with
+  | 0 => (0, 0)
+  | Zpos p =>
+    match Psqrtrem p with
+     | (s, IsPos r) => (Zpos s, Zpos r)
+     | (s, _) => (Zpos s, 0)
+    end
+  | Zneg _ => (0,0)
+ end.
+
+Definition Zsqrt n :=
+ match n with
+  | 0 => 0
+  | Zpos p => Zpos (Psqrt p)
+  | Zneg _ => 0
+ end.
+
+Lemma Zsqrtrem_spec : forall n, 0<=n ->
+ let (s,r) := Zsqrtrem n in n = s*s + r /\ 0 <= r <= 2*s.
+Proof.
+ destruct n. now repeat split.
+ generalize (Psqrtrem_spec p). simpl.
+ destruct 1; simpl; subst; now repeat split.
+ now destruct 1.
+Qed.
+
+Lemma Zsqrt_spec : forall n, 0<=n ->
+ let s := Zsqrt n in s*s <= n < (Zsucc s)*(Zsucc s).
+Proof.
+ destruct n. now repeat split. unfold Zsqrt.
+ rewrite <- Zpos_succ_morphism. intros _. apply (Psqrt_spec p).
+ now destruct 1.
+Qed.
+
+Lemma Zsqrt_neg : forall n, n<0 -> Zsqrt n = 0.
+Proof.
+ intros. now destruct n.
+Qed.
+
+Lemma Zsqrtrem_sqrt : forall n, fst (Zsqrtrem n) = Zsqrt n.
+Proof.
+ destruct n; try reflexivity.
+ unfold Zsqrtrem, Zsqrt, Psqrt.
+ destruct (Psqrtrem p) as (s,r). now destruct r.
+Qed.
\ No newline at end of file
diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget
index 59994e32f..28db6848d 100644
--- a/theories/ZArith/vo.itarget
+++ b/theories/ZArith/vo.itarget
@@ -27,5 +27,6 @@ Zorder.vo
 Zpow_def.vo
 Zpower.vo
 Zpow_facts.vo
-Zsqrt.vo
+Zsqrt_compat.vo
 Zwf.vo
+Zsqrt_def.vo