NZLog : since spec is complete, no need for morphism axiom log2_wd

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13608 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 bdaa748e4..d4796d106 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -159,8 +159,6 @@ Definition sqrt := Zsqrt.
 
 (** Log2 *)
 
-Program Instance log2_wd : Proper (eq==>eq) Zlog2.
-
 Definition log2_spec := Zlog2_spec.
 Definition log2_nonpos := Zlog2_nonpos.
 Definition log2 := Zlog2.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 96f243fa6..69feb9315 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -295,8 +295,6 @@ Qed.
 
 (** Log2 *)
 
-Program Instance log2_wd : Proper (eq==>eq) log2.
-
 Lemma log2_spec : forall n, 0<n ->
  2^(log2 n) <= n /\ n < 2^(succ (log2 n)).
 Proof.
diff --git a/theories/Numbers/NatInt/NZLog.v b/theories/Numbers/NatInt/NZLog.v
index 34c57aad9..4c8dcc8f3 100644
--- a/theories/Numbers/NatInt/NZLog.v
+++ b/theories/Numbers/NatInt/NZLog.v
@@ -18,7 +18,6 @@ End Log2.
 
 Module Type NZLog2Spec (A : NZOrdAxiomsSig')(B : Pow' A)(C : Log2 A).
  Import A B C.
- Declare Instance log2_wd : Proper (eq==>eq) log2.
  Axiom log2_spec : forall a, 0<a -> 2^(log2 a) <= a < 2^(S (log2 a)).
  Axiom log2_nonpos : forall a, a<=0 -> log2 a == 0.
 End NZLog2Spec.
@@ -74,6 +73,17 @@ Proof.
  order.
 Qed.
 
+(** Hence log2 is a morphism. *)
+
+Instance log2_wd : Proper (eq==>eq) log2.
+Proof.
+ intros x x' Hx.
+ destruct (le_gt_cases x 0).
+ rewrite 2 log2_nonpos; trivial. reflexivity. now rewrite <- Hx.
+ apply log2_unique. apply log2_nonneg.
+ rewrite Hx in *. now apply log2_spec.
+Qed.
+
 (** An alternate specification *)
 
 Lemma log2_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 97e7b3678..34b44d3c6 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -160,7 +160,6 @@ Proof. destruct b; discriminate. Qed.
 
 (** Log2 *)
 
-Program Instance log2_wd : Proper (eq==>eq) Nlog2.
 Definition log2_spec := Nlog2_spec.
 Definition log2_nonpos := Nlog2_nonpos.
 
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 3255fda68..6502cfa55 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -444,7 +444,6 @@ Definition pow_succ_r := pow_succ_r.
 Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
 Definition pow := pow.
 
-Program Instance log2_wd : Proper (eq==>eq) log2.
 Definition log2_spec := log2_spec.
 Definition log2_nonpos := log2_nonpos.
 Definition log2 := log2.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 64dcd1967..3620045d1 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -245,8 +245,6 @@ Qed.
 
 (** Log2 *)
 
-Program Instance log2_wd : Proper (eq==>eq) log2.
-
 Lemma log2_spec : forall n, 0<n ->
  2^(log2 n) <= n /\ n < 2^(succ (log2 n)).
 Proof.