diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-02 15:10:43 +0000 |
| commit | d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 (patch) | |
| tree | 575ec66b8028a599f94d293ae32260b09e7874ef /theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | |
| parent | 1dccdb6b2c792969c5e09faebc2f761e46192ec4 (diff) | |
Numbers : log2. Abstraction, properties and implementations.
Btw, we finally declare the original Zpower as the power on Z.
We should switch to a more efficient one someday, but in the
meantime BigN is proved with respect to the old one.
TODO: reform Zlogarithm with respect to Zlog_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13606 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v')
| -rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index f242951e5..64dcd1967 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -16,7 +16,8 @@ Module NTypeIsNAxioms (Import N : NType'). Hint Rewrite spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub spec_div spec_modulo spec_gcd spec_compare spec_eq_bool spec_sqrt - spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd + spec_log2 spec_max spec_min spec_pow_pos spec_pow_N spec_pow + spec_even spec_odd : nsimpl. Ltac nsimpl := autorewrite with nsimpl. Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence. @@ -242,6 +243,22 @@ Proof. generalize (spec_pos n); omega. 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. + intros n. zify. change (Zlog2 [n]+1)%Z with (Zsucc (Zlog2 [n])). + apply Zlog2_spec. +Qed. + +Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. +Proof. + intros n. zify. apply Zlog2_nonpos. +Qed. + (** Even / Odd *) Definition Even n := exists m, n == 2*m. |