1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Zlogarithm.v,v 1.14.2.1 2004/07/16 19:31:21 herbelin Exp $ i*)
35 (*#*********************************************************************)
37 (*#* The integer logarithms with base 2.
39 There are three logarithms,
40 depending on the rounding of the real 2-based logarithm:
41 - [Log_inf]: [y = (Log_inf x) iff 2^y <= x < 2^(y+1)]
42 i.e. [Log_inf x] is the biggest integer that is smaller than [Log x]
43 - [Log_sup]: [y = (Log_sup x) iff 2^(y-1) < x <= 2^y]
44 i.e. [Log_inf x] is the smallest integer that is bigger than [Log x]
45 - [Log_nearest]: [y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)]
46 i.e. [Log_nearest x] is the integer nearest from [Log x] *)
48 include "ZArith/ZArith_base.ma".
50 include "ZArith/Zcomplements.ma".
52 include "ZArith/Zpower.ma".
55 Open Local Scope Z_scope.
62 (* Log of positive integers *)
64 (*#* First we build [log_inf] and [log_sup] *)
66 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf.con" as definition.
68 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup.con" as definition.
71 Hint Unfold log_inf log_sup.
74 (*#* Then we give the specifications of [log_inf] and [log_sup]
75 and prove their validity *)
77 (*i Hints Resolve ZERO_le_S : zarith. i*)
80 Hint Resolve Zle_trans: zarith.
83 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct.con" as theorem.
85 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct1.con" as definition.
87 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_correct2.con" as definition.
90 Opaque log_inf_correct1 log_inf_correct2.
94 Hint Resolve log_inf_correct1 log_inf_correct2: zarith.
97 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_correct1.con" as lemma.
99 (*#* For every [p], either [p] is a power of two and [(log_inf p)=(log_sup p)]
100 either [(log_sup p)=(log_inf p)+1] *)
102 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_log_inf.con" as theorem.
104 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_correct2.con" as theorem.
106 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_le_log_sup.con" as lemma.
108 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_le_Slog_inf.con" as lemma.
110 (*#* Now it's possible to specify and build the [Log] rounded to the nearest *)
112 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near.con" as definition.
114 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near_correct1.con" as theorem.
116 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_near_correct2.con" as theorem.
118 (*i******************
119 Theorem log_near_correct: (p:positive)
120 `| (two_p (log_near p)) - (POS p) | <= (POS p)-(two_p (log_inf p))`
121 /\`| (two_p (log_near p)) - (POS p) | <= (two_p (log_sup p))-(POS p)`.
124 Intros p0 [(Einf1,Einf2)|(Esup1,Esup2)].
125 Unfold log_near log_inf log_sup. Fold log_near log_inf log_sup.
127 Repeat Rewrite two_p_S.
128 Case p0; [Left | Left | Right].
132 Rewrite E1; Case p0; Try Reflexivity.
134 Unfold log_near; Fold log_near.
135 Unfold log_inf; Fold log_inf.
138 **********************************i*)
148 (*#* Number of significative digits. *)
150 inline procedural "cic:/Coq/ZArith/Zlogarithm/N_digits.con" as definition.
152 inline procedural "cic:/Coq/ZArith/Zlogarithm/ZERO_le_N_digits.con" as lemma.
154 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_inf_shift_nat.con" as lemma.
156 inline procedural "cic:/Coq/ZArith/Zlogarithm/log_sup_shift_nat.con" as lemma.
158 (*#* [Is_power p] means that p is a power of two *)
160 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power.con" as definition.
162 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power_correct.con" as lemma.
164 inline procedural "cic:/Coq/ZArith/Zlogarithm/Is_power_or.con" as lemma.