From b03b65fdc44e3c6cfeceaf997cbc1a50a6c19e5c Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 19 Oct 2010 10:16:57 +0000
Subject: 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
---
 theories/Numbers/Natural/Binary/NBinary.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'theories/Numbers/Natural/Binary')

diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index d1217d407e..348eee5ed2 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import BinPos Ndiv_def.
+Require Import BinPos Ndiv_def Nsqrt_def.
 Require Export BinNat.
 Require Import NAxioms NProperties.
 
@@ -167,6 +167,11 @@ 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.
 
+(** Sqrt *)
+
+Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt.
+Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n.
+
 (** The instantiation of operations.
     Placing them at the very end avoids having indirections in above lemmas. *)
 
@@ -192,6 +197,7 @@ Definition modulo := Nmod.
 Definition pow := Npow.
 Definition even := Neven.
 Definition odd := Nodd.
+Definition sqrt := Nsqrt.
 
 Include NProp
  <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
-- 
cgit v1.2.3