3 files changed, 72 insertions, 6 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAxioms.v b/theories/Numbers/Natural/Abstract/NAxioms.v
index 66ff2ded54..b360c016f3 100644
--- a/theories/Numbers/Natural/Abstract/NAxioms.v
+++ b/theories/Numbers/Natural/Abstract/NAxioms.v
@@ -8,7 +8,7 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Export NZAxioms NZPow NZDiv.
+Require Export NZAxioms NZPow NZSqrt NZDiv.
 
 (** From [NZ], we obtain natural numbers just by stating that [pred 0] == 0 *)
 
@@ -32,7 +32,7 @@ Module Type Parity (Import N : NAxiomsMiniSig').
  Axiom odd_spec : forall n, odd n = true <-> Odd n.
 End Parity.
 
-(** Power function : NZPow is enough *)
+(** For Power and Sqrt functions : NZPow and NZSqrt are enough *)
 
 (** Division Function : we reuse NZDiv.DivMod and NZDiv.NZDivCommon,
     and add to that a N-specific constraint. *)
@@ -45,10 +45,12 @@ End NDivSpecific.
 (** We now group everything together. *)
 
 Module Type NAxiomsSig := NAxiomsMiniSig <+ HasCompare <+ Parity
-  <+ NZPow.NZPow <+ DivMod <+ NZDivCommon <+ NDivSpecific.
+  <+ NZPow.NZPow <+ NZSqrt.NZSqrt
+  <+ DivMod <+ NZDivCommon <+ NDivSpecific.
 
 Module Type NAxiomsSig' := NAxiomsMiniSig' <+ HasCompare <+ Parity
-  <+ NZPow.NZPow' <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
+  <+ NZPow.NZPow' <+ NZSqrt.NZSqrt'
+  <+ DivMod' <+ NZDivCommon <+ NDivSpecific.
 
 
 (** It could also be interesting to have a constructive recursor function. *)
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index c1977f3533..fc8f27ddc9 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -7,9 +7,9 @@
 (************************************************************************)
 
 Require Export NAxioms.
-Require Import NMaxMin NParity NPow NDiv.
+Require Import NMaxMin NParity NPow NSqrt NDiv.
 
 (** This functor summarizes all known facts about N. *)
 
 Module Type NProp (N:NAxiomsSig) :=
- NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NDivProp N.
+ NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N <+ NDivProp N.
diff --git a/theories/Numbers/Natural/Abstract/NSqrt.v b/theories/Numbers/Natural/Abstract/NSqrt.v
new file mode 100644
index 0000000000..d5916bdc2d
--- /dev/null
+++ b/theories/Numbers/Natural/Abstract/NSqrt.v
@@ -0,0 +1,64 @@
+(************************************************************************)
+(*  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        *)
+(************************************************************************)
+
+(** Properties of Square Root Function *)
+
+Require Import NAxioms NSub NZSqrt.
+
+Module NSqrtProp (Import N : NAxiomsSig')(Import NS : NSubProp N).
+
+ Module Import NZSqrtP := NZSqrtProp N N NS.
+
+ Ltac auto' := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
+ Ltac wrap l := intros; apply l; auto'.
+
+ (** We redefine NZSqrt's results, without the non-negative hyps *)
+
+Lemma sqrt_spec' : forall a, √a*√a <= a < S (√a) * S (√a).
+Proof. wrap sqrt_spec. Qed.
+
+Lemma sqrt_unique : forall a b, b*b<=a<(S b)*(S b) -> √a == b.
+Proof. wrap sqrt_unique. Qed.
+
+Lemma sqrt_square : forall a, √(a*a) == a.
+Proof. wrap sqrt_square. Qed.
+
+Lemma sqrt_le_mono : forall a b, a<=b -> √a <= √b.
+Proof. wrap sqrt_le_mono. Qed.
+
+Lemma sqrt_lt_cancel : forall a b, √a < √b -> a < b.
+Proof. wrap sqrt_lt_cancel. Qed.
+
+Lemma sqrt_le_square : forall a b, b*b<=a <-> b <= √a.
+Proof. wrap sqrt_le_square. Qed.
+
+Lemma sqrt_lt_square : forall a b, a<b*b <-> √a < b.
+Proof. wrap sqrt_lt_square. Qed.
+
+Definition sqrt_0 := sqrt_0.
+Definition sqrt_1 := sqrt_1.
+Definition sqrt_2 := sqrt_2.
+
+Definition sqrt_lt_lin : forall a, 1<a -> √a<a := sqrt_lt_lin.
+
+Lemma sqrt_le_lin : forall a, 0<=a -> √a<=a.
+Proof. wrap sqrt_le_lin. Qed.
+
+Lemma sqrt_mul_below : forall a b, √a * √b <= √(a*b).
+Proof. wrap sqrt_mul_below. Qed.
+
+Lemma sqrt_mul_above : forall a b, √(a*b) < S (√a) * S (√b).
+Proof. wrap sqrt_mul_above. Qed.
+
+Lemma sqrt_add_le : forall a b, √(a+b) <= √a + √b.
+Proof. wrap sqrt_add_le. Qed.
+
+Lemma add_sqrt_le : forall a b, √a + √b <= √(2*(a+b)).
+Proof. wrap add_sqrt_le. Qed.
+
+End NSqrtProp.