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

1 files changed, 10 insertions, 17 deletions

diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 6fcb4cf91..2d9eb395a 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -574,27 +574,19 @@ Section ZModulo.
  generalize (Z_mod_lt [|x|] 2); omega.
  Qed.
 
- Definition sqrt x := Zsqrt_plain [|x|].
+ Definition sqrt x := Zsqrt [|x|].
  Lemma spec_sqrt : forall x,
        [|sqrt x|] ^ 2 <= [|x|] < ([|sqrt x|] + 1) ^ 2.
  Proof.
  intros.
  unfold sqrt.
  repeat rewrite Zpower_2.
- replace [|Zsqrt_plain [|x|]|] with (Zsqrt_plain [|x|]).
- apply Zsqrt_interval; auto with zarith.
+ replace [|Zsqrt [|x|]|] with (Zsqrt [|x|]).
+ apply Zsqrt_spec; auto with zarith.
  symmetry; apply Zmod_small.
- split.
- apply Zsqrt_plain_is_pos; auto with zarith.
-
- cut (Zsqrt_plain [|x|] <= (wB-1)); try omega.
- rewrite <- (Zsqrt_square_id (wB-1)).
- apply Zsqrt_le.
- split; auto.
- apply Zle_trans with (wB-1); auto with zarith.
- generalize (spec_to_Z x); auto with zarith.
- apply Zsquare_le.
- generalize wB_pos; auto with zarith.
+ split. apply Z.sqrt_nonneg; auto.
+ apply Zle_lt_trans with [|x|]; auto.
+ apply Z.sqrt_le_lin; auto.
  Qed.
 
  Definition sqrt2 x y :=
@@ -602,7 +594,7 @@ Section ZModulo.
   match z with
    | Z0 => (0, C0 0)
    | Zpos p =>
-      let (s,r,_,_) := sqrtrempos p in
+      let (s,r) := Zsqrtrem (Zpos p) in
       (s, if Z_lt_le_dec r wB then C0 r else C1 (r-wB))
    | Zneg _ => (0, C0 0)
   end.
@@ -618,11 +610,12 @@ Section ZModulo.
  remember ([|x|]*wB+[|y|]) as z.
  destruct z.
  auto with zarith.
- destruct sqrtrempos; intros.
+ generalize (Zsqrtrem_spec (Zpos p)).
+ destruct Zsqrtrem as (s,r); intros [U V]; auto with zarith.
  assert (s < wB).
   destruct (Z_lt_le_dec s wB); auto.
   assert (wB * wB <= Zpos p).
-   rewrite e.
+   rewrite U.
    apply Zle_trans with (s*s); try omega.
    apply Zmult_le_compat; generalize wB_pos; auto with zarith.
   assert (Zpos p < wB*wB).