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/Integer/Binary/ZBinary.v | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) (limited to 'theories/Numbers/Integer/Binary') diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v index 5f87283940..ee75e4aa18 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). -- cgit v1.2.3