aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/NatInt
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-11-02 15:10:50 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2010-11-02 15:10:50 +0000
commit8e5cae9a9f8edbedc2fb2451d32dc18af89cfa40 (patch)
tree078003a6c219d021755bca4cc477f5d82b1c0540 /theories/Numbers/NatInt
parent0cb098205ba6d85674659bf5d0bfc0ed942464cc (diff)
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
Diffstat (limited to 'theories/Numbers/NatInt')
-rw-r--r--theories/Numbers/NatInt/NZLog.v12
1 files changed, 11 insertions, 1 deletions
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,