diff options
Diffstat (limited to 'theories')
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 2 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 6 | ||||
-rw-r--r-- | theories/ZArith/ZArith.v | 3 | ||||
-rw-r--r-- | theories/ZArith/Zlog_def.v | 13 | ||||
-rw-r--r-- | theories/ZArith/Zlogarithm.v | 31 | ||||
-rw-r--r-- | theories/ZArith/vo.itarget | 1 |
8 files changed, 26 insertions, 38 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 0bcf22e32..cb16e1291 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -368,12 +368,12 @@ Module Make (N:NType) <: ZType. | Neg nx => zero end. - Theorem spec_log2: forall x, to_Z (log2 x) = Zlog2 (to_Z x). + Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x). Proof. intros. destruct x as [p|p]; simpl. apply N.spec_log2. rewrite N.spec_0. destruct (Z_le_lt_eq_dec _ _ (N.spec_pos p)) as [LT|EQ]. - rewrite Zlog2_nonpos; auto with zarith. + rewrite Z.log2_nonpos; auto with zarith. now rewrite <- EQ. Qed. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index dd83b65da..f40928566 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -324,12 +324,12 @@ Qed. Lemma log2_spec : forall n, 0<n -> 2^(log2 n) <= n /\ n < 2^(succ (log2 n)). Proof. - intros n. zify. apply Zlog2_spec. + intros n. zify. apply Z.log2_spec. Qed. Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. Proof. - intros n. zify. apply Zlog2_nonpos. + intros n. zify. apply Z.log2_nonpos. Qed. (** Even / Odd *) diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 66b39aca9..64b8ec844 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1244,7 +1244,7 @@ Module Make (W0:CyclicType) <: NType. apply ZnZ.spec_head0; auto with zarith. Qed. - Lemma spec_log2 : forall x, [log2 x] = Zlog2 [x]. + Lemma spec_log2 : forall x, [log2 x] = Z.log2 [x]. Proof. intros. destruct (Z_lt_ge_dec 0 [x]). symmetry. apply Z.log2_unique. apply spec_pos. diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 9bed794f2..225c0853e 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -277,13 +277,13 @@ Qed. 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. + intros n. zify. change (Z.log2 [n]+1)%Z with (Z.succ (Z.log2 [n])). + apply Z.log2_spec. Qed. Lemma log2_nonpos : forall n, n<=0 -> log2 n == 0. Proof. - intros n. zify. apply Zlog2_nonpos. + intros n. zify. apply Z.log2_nonpos. Qed. (** Even / Odd *) diff --git a/theories/ZArith/ZArith.v b/theories/ZArith/ZArith.v index 5a927fe6b..abd735de5 100644 --- a/theories/ZArith/ZArith.v +++ b/theories/ZArith/ZArith.v @@ -12,8 +12,7 @@ Require Export ZArith_base. (** Extra definitions *) -Require Export - Zpow_def Zlog_def Zdigits_def. +Require Export Zpow_def Zdigits_def. (** Extra modules using [Omega] or [Ring]. *) diff --git a/theories/ZArith/Zlog_def.v b/theories/ZArith/Zlog_def.v deleted file mode 100644 index 8326cb13c..000000000 --- a/theories/ZArith/Zlog_def.v +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import BinInt Zorder Zpow_def. - -Notation Zlog2 := Z.log2 (only parsing). -Notation Zlog2_spec := Z.log2_spec (only parsing). -Notation Zlog2_nonpos := Z.log2_nonpos (only parsing). diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v index b80e96c2a..30948ca7a 100644 --- a/theories/ZArith/Zlogarithm.v +++ b/theories/ZArith/Zlogarithm.v @@ -8,11 +8,14 @@ (**********************************************************************) -(** The integer logarithms with base 2. +(** The integer logarithms with base 2. *) - NOTA: This file is deprecated, please use Zlog2 defined in Zlog_def. +(** THIS FILE IS DEPRECATED. + Please rather use [Z.log2] (or [Z.log2_up]), which + are defined in [BinIntDef], and whose properties can + be found in [BinInt.Z]. *) - There are three logarithms defined here, +(* There are three logarithms defined here, depending on the rounding of the real 2-based logarithm: - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)] i.e. [Log_inf x] is the biggest integer that is smaller than [Log x] @@ -21,7 +24,7 @@ - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)] i.e. [Log_nearest x] is the integer nearest from [Log x] *) -Require Import ZArith_base Omega Zcomplements Zlog_def Zpower. +Require Import ZArith_base Omega Zcomplements Zpower. Local Open Scope Z_scope. Section Log_pos. (* Log of positive integers *) @@ -44,25 +47,25 @@ Section Log_pos. (* Log of positive integers *) Hint Unfold log_inf log_sup. - Lemma Psize_log_inf : forall p, Zpos (Psize_pos p) = Zsucc (log_inf p). + Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p). Proof. - induction p; simpl; now rewrite ?Zpos_succ_morphism, ?IHp. + induction p; simpl; now rewrite <- ?Z.succ_Zpos, ?IHp. Qed. - Lemma Zlog2_log_inf : forall p, Zlog2 (Zpos p) = log_inf p. + Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p. Proof. - unfold Zlog2. destruct p; simpl; trivial; apply Psize_log_inf. + unfold Z.log2. destruct p; simpl; trivial; apply Psize_log_inf. Qed. Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p. Proof. induction p; simpl. - change (Zpos p~1) with (2*(Zpos p)+1). - rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. - unfold Zsucc. now rewrite !(Zplus_comm _ 1), Zplus_assoc. - change (Zpos p~0) with (2*Zpos p). - now rewrite Z.log2_up_double, IHp. - reflexivity. + - change (Zpos p~1) with (2*(Zpos p)+1). + rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy. + unfold Z.succ. now rewrite !(Z.add_comm _ 1), Z.add_assoc. + - change (Zpos p~0) with (2*Zpos p). + now rewrite Z.log2_up_double, IHp. + - reflexivity. Qed. (** Then we give the specifications of [log_inf] and [log_sup] diff --git a/theories/ZArith/vo.itarget b/theories/ZArith/vo.itarget index 9605735dc..767ba4f1b 100644 --- a/theories/ZArith/vo.itarget +++ b/theories/ZArith/vo.itarget @@ -29,6 +29,5 @@ Zpower.vo Zpow_facts.vo Zsqrt_compat.vo Zwf.vo -Zlog_def.vo Zeuclid.vo Zdigits_def.vo
\ No newline at end of file |