NZSqrt : since spec is complete, no need for morphism axiom sqrt_wd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13609 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 11 insertions, 9 deletions

diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index d4796d1067..b92b303f0d 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -151,8 +151,6 @@ Definition pow := Zpower.
 (** 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.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 69feb93151..6689875cb0 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -280,8 +280,6 @@ Qed.
 
 (** Sqrt *)
 
-Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
-
 Lemma sqrt_spec : forall n, 0<=n ->
  (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
 Proof.
diff --git a/theories/Numbers/NatInt/NZSqrt.v b/theories/Numbers/NatInt/NZSqrt.v
index 276c5e9c63..4cdf322fd8 100644
--- a/theories/Numbers/NatInt/NZSqrt.v
+++ b/theories/Numbers/NatInt/NZSqrt.v
@@ -23,7 +23,6 @@ End SqrtNotation.
 Module Type Sqrt' (A : Typ) := Sqrt A <+ SqrtNotation A.
 
 Module Type NZSqrtSpec (Import A : NZOrdAxiomsSig')(Import B : Sqrt' A).
- Declare Instance sqrt_wd : Proper (eq==>eq) sqrt.
  Axiom sqrt_spec : forall a, 0<=a -> √a * √a <= a < S (√a) * S (√a).
  Axiom sqrt_neg : forall a, a<0 -> √a == 0.
 End NZSqrtSpec.
@@ -78,6 +77,17 @@ Proof.
  order.
 Qed.
 
+(** Hence sqrt is a morphism *)
+
+Instance sqrt_wd : Proper (eq==>eq) sqrt.
+Proof.
+ intros x x' Hx.
+ destruct (lt_ge_cases x 0) as [H|H].
+ rewrite 2 sqrt_neg; trivial. reflexivity.
+ now rewrite <- Hx.
+ apply sqrt_unique. rewrite Hx in *. now apply sqrt_spec.
+Qed.
+
 (** An alternate specification *)
 
 Lemma sqrt_spec_alt : forall a, 0<=a -> exists r,
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 34b44d3c60..cc57171b32 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -165,7 +165,6 @@ Definition log2_nonpos := Nlog2_nonpos.
 
 (** Sqrt *)
 
-Program Instance sqrt_wd : Proper (eq==>eq) Nsqrt.
 Definition sqrt_spec n (H:0<=n) := Nsqrt_spec n.
 Lemma sqrt_neg : forall a, a<0 -> Nsqrt a = 0.
 Proof. destruct a; discriminate. Qed.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 6502cfa555..a828ec821c 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -448,7 +448,6 @@ Definition log2_spec := log2_spec.
 Definition log2_nonpos := log2_nonpos.
 Definition log2 := log2.
 
-Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
 Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
 Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed.
 Definition sqrt := sqrt.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 3620045d1e..547f51b3d5 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -229,8 +229,6 @@ Qed.
 
 (** Sqrt *)
 
-Program Instance sqrt_wd : Proper (eq==>eq) sqrt.
-
 Lemma sqrt_spec : forall n, 0<=n ->
  (sqrt n)*(sqrt n) <= n /\ n < (succ (sqrt n))*(succ (sqrt n)).
 Proof.