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: Zpower.v,v 1.11.2.1 2004/07/16 19:31:22 herbelin Exp $ i*)
35 include "ZArith/ZArith_base.ma".
37 include "ZArith/Zcomplements.ma".
40 Open Local Scope Z_scope.
47 (*#* [Zpower_nat z n] is the n-th power of [z] when [n] is an unary
48 integer (type [nat]) and [z] a signed integer (type [Z]) *)
50 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_nat.con" as definition.
52 (*#* [Zpower_nat_is_exp] says [Zpower_nat] is a morphism for
53 [plus : nat->nat] and [Zmult : Z->Z] *)
55 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_nat_is_exp.con" as lemma.
57 (*#* [Zpower_pos z n] is the n-th power of [z] when [n] is an binary
58 integer (type [positive]) and [z] a signed integer (type [Z]) *)
60 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos.con" as definition.
62 (*#* This theorem shows that powers of unary and binary integers
63 are the same thing, modulo the function convert : [positive -> nat] *)
65 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos_nat.con" as theorem.
67 (*#* Using the theorem [Zpower_pos_nat] and the lemma [Zpower_nat_is_exp] we
68 deduce that the function [[n:positive](Zpower_pos z n)] is a morphism
69 for [add : positive->positive] and [Zmult : Z->Z] *)
71 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_pos_is_exp.con" as theorem.
73 inline procedural "cic:/Coq/ZArith/Zpower/Zpower.con" as definition.
76 Infix "^" := Zpower : Z_scope.
80 Hint Immediate Zpower_nat_is_exp: zarith.
84 Hint Immediate Zpower_pos_is_exp: zarith.
88 Hint Unfold Zpower_pos: zarith.
92 Hint Unfold Zpower_nat: zarith.
95 inline procedural "cic:/Coq/ZArith/Zpower/Zpower_exp.con" as lemma.
101 (* Exporting notation "^" *)
104 Infix "^" := Zpower : Z_scope.
108 Hint Immediate Zpower_nat_is_exp: zarith.
112 Hint Immediate Zpower_pos_is_exp: zarith.
116 Hint Unfold Zpower_pos: zarith.
120 Hint Unfold Zpower_nat: zarith.
127 (*#* For the powers of two, that will be widely used, a more direct
128 calculus is possible. We will also prove some properties such
129 as [(x:positive) x < 2^x] that are true for all integers bigger
130 than 2 but more difficult to prove and useless. *)
132 (*#* [shift n m] computes [2^n * m], or [m] shifted by [n] positions *)
134 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat.con" as definition.
136 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos.con" as definition.
138 inline procedural "cic:/Coq/ZArith/Zpower/shift.con" as definition.
140 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat.con" as definition.
142 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos.con" as definition.
144 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat_S.con" as lemma.
146 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat_plus.con" as lemma.
148 inline procedural "cic:/Coq/ZArith/Zpower/shift_nat_correct.con" as theorem.
150 inline procedural "cic:/Coq/ZArith/Zpower/two_power_nat_correct.con" as theorem.
152 (*#* Second we show that [two_power_pos] and [two_power_nat] are the same *)
154 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos_nat.con" as lemma.
156 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_nat.con" as lemma.
158 (*#* Then we deduce that [two_power_pos] is also correct *)
160 inline procedural "cic:/Coq/ZArith/Zpower/shift_pos_correct.con" as theorem.
162 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_correct.con" as theorem.
164 (*#* Some consequences *)
166 inline procedural "cic:/Coq/ZArith/Zpower/two_power_pos_is_exp.con" as theorem.
168 (*#* The exponentiation [z -> 2^z] for [z] a signed integer.
169 For convenience, we assume that [2^z = 0] for all [z < 0]
170 We could also define a inductive type [Log_result] with
171 3 contructors [ Zero | Pos positive -> | minus_infty]
172 but it's more complexe and not so useful. *)
174 inline procedural "cic:/Coq/ZArith/Zpower/two_p.con" as definition.
176 inline procedural "cic:/Coq/ZArith/Zpower/two_p_is_exp.con" as theorem.
178 inline procedural "cic:/Coq/ZArith/Zpower/two_p_gt_ZERO.con" as lemma.
180 inline procedural "cic:/Coq/ZArith/Zpower/two_p_S.con" as lemma.
182 inline procedural "cic:/Coq/ZArith/Zpower/two_p_pred.con" as lemma.
184 inline procedural "cic:/Coq/ZArith/Zpower/Zlt_lt_double.con" as lemma.
191 Hint Resolve two_p_gt_ZERO: zarith.
195 Hint Immediate two_p_pred two_p_S: zarith.
199 Section power_div_with_rest
202 (*#* Division by a power of two.
203 To [n:Z] and [p:positive], [q],[r] are associated such that
204 [n = 2^p.q + r] and [0 <= r < 2^p] *)
206 (*#* Invariant: [d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'] *)
208 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_aux.con" as definition.
210 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest.con" as definition.
212 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct1.con" as lemma.
214 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct2.con" as lemma.
216 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_proofs.ind".
218 inline procedural "cic:/Coq/ZArith/Zpower/Zdiv_rest_correct.con" as lemma.
221 End power_div_with_rest