diff options
| author | letouzey | 2010-11-02 15:10:43 +0000 |
|---|---|---|
| committer | letouzey | 2010-11-02 15:10:43 +0000 |
| commit | d6ebd62341fd6bbe2b7d4e5309d8e13f786a9462 (patch) | |
| tree | 575ec66b8028a599f94d293ae32260b09e7874ef /theories/Numbers/Natural/BigN | |
| 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/BigN')
| -rw-r--r-- | theories/Numbers/Natural/BigN/BigN.v | 3 | ||||
| -rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 13 |
2 files changed, 14 insertions, 2 deletions
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v index 0f04869c09..209bee8c16 100644 --- a/theories/Numbers/Natural/BigN/BigN.v +++ b/theories/Numbers/Natural/BigN/BigN.v @@ -61,10 +61,13 @@ Arguments Scope BigN.eq_bool [bigN_scope bigN_scope]. Arguments Scope BigN.pow_pos [bigN_scope positive_scope]. Arguments Scope BigN.pow_N [bigN_scope N_scope]. Arguments Scope BigN.pow [bigN_scope bigN_scope]. +Arguments Scope BigN.log2 [bigN_scope]. Arguments Scope BigN.sqrt [bigN_scope]. Arguments Scope BigN.div_eucl [bigN_scope bigN_scope]. Arguments Scope BigN.modulo [bigN_scope bigN_scope]. Arguments Scope BigN.gcd [bigN_scope bigN_scope]. +Arguments Scope BigN.even [bigN_scope]. +Arguments Scope BigN.odd [bigN_scope]. Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *) Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 60a836d416..306efc19ca 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1151,7 +1151,7 @@ Module Make (W0:CyclicType) <: NType. rewrite Zmult_comm in H0. auto with zarith. Qed. - Lemma spec_log2 : forall x, [x]<>0 -> + Lemma spec_log2_pos : forall x, [x]<>0 -> 2^[log2 x] <= [x] < 2^([log2 x]+1). Proof. intros x H. rewrite log2_fold. @@ -1178,6 +1178,15 @@ Module Make (W0:CyclicType) <: NType. apply ZnZ.spec_head0; auto with zarith. Qed. + Lemma spec_log2 : forall x, [log2 x] = Zlog2 [x]. + Proof. + intros. destruct (Z_lt_ge_dec 0 [x]). + symmetry. apply Z.log2_unique. apply spec_pos. + apply spec_log2_pos. intro EQ; rewrite EQ in *; auto with zarith. + rewrite spec_log2_0. rewrite Z.log2_nonpos; auto with zarith. + generalize (spec_pos x); auto with zarith. + Qed. + Lemma log2_digits_head0 : forall x, 0 < [x] -> [log2 x] = Zpos (digits x) - [head0 x] - 1. Proof. @@ -1311,7 +1320,7 @@ Module Make (W0:CyclicType) <: NType. (* [x] <> 0 *) apply spec_unsafe_shiftl_aux with ([log2 x] + 1); auto with zarith. generalize (spec_pos (log2 x)); auto with zarith. - destruct (spec_log2 x); auto with zarith. + destruct (spec_log2_pos x); auto with zarith. rewrite log2_digits_head0; auto with zarith. generalize (spec_pos x); auto with zarith. Qed. |