Library Coq.ZArith.Zpower
Definition of powers over Z
Zpower_nat z n is the n-th power of z when n is an unary
integer (type nat) and z a signed integer (type Z)
Zpower_nat_is_exp says Zpower_nat is a morphism for
plus : nat->nat and Zmult : Z->Z
This theorem shows that powers of unary and binary integers
are the same thing, modulo the function convert : positive -> nat
Using the theorem Zpower_pos_nat and the lemma Zpower_nat_is_exp we
deduce that the function [n:positive](Zpower_pos z n) is a morphism
for add : positive->positive and Zmult : Z->Z
For the powers of two, that will be widely used, a more direct
calculus is possible. We will also prove some properties such
as (x:positive) x < 2^x that are true for all integers bigger
than 2 but more difficult to prove and useless.
shift n m computes 2^n * m, or m shifted by n positions
Second we show that two_power_pos and two_power_nat are the same
Then we deduce that two_power_pos is also correct
Some consequences
The exponentiation z -> 2^z for z a signed integer.
For convenience, we assume that 2^z = 0 for all z < 0
We could also define a inductive type Log_result with
3 contructors Zero | Pos positive -> | minus_infty
but it's more complexe and not so useful.
Division by a power of two.
To n:Z and p:positive, q,r are associated such that
n = 2^p.q + r and 0 <= r < 2^p
Invariant: d*q + r = d'*q + r /\ d' = 2*d /\ 0<= r < d /\ 0 <= r' < d'
Definition Zdiv_rest_aux (
qrd:
Z * Z * Z) :=
let (
qr,
d) :=
qrd in
let (
q,
r) :=
qr in
(match q with
|
Z0 =>
(0
, r)
|
Zpos xH =>
(0
, d + r)
|
Zpos (
xI n) =>
(Zpos n, d + r)
|
Zpos (
xO n) =>
(Zpos n, r)
|
Zneg xH =>
(-1
, d + r)
|
Zneg (
xI n) =>
(Zneg n - 1
, d + r)
|
Zneg (
xO n) =>
(Zneg n, r)
end, 2
* d).
Definition Zdiv_rest (
x:
Z) (
p:
positive) :=
let (
qr,
d) :=
iter_pos p _ Zdiv_rest_aux (x, 0
, 1
) in qr.
Lemma Zdiv_rest_correct1 :
forall (
x:
Z) (
p:
positive),
let (
qr,
d) :=
iter_pos p _ Zdiv_rest_aux (x, 0
, 1
) in d = two_power_pos p.
Lemma Zdiv_rest_correct2 :
forall (
x:
Z) (
p:
positive),
let (
qr,
d) :=
iter_pos p _ Zdiv_rest_aux (x, 0
, 1
) in
let (
q,
r) :=
qr in x = q * d + r /\ 0
<= r < d.
Inductive Zdiv_rest_proofs (
x:
Z) (
p:
positive) :
Set :=
Zdiv_rest_proof :
forall q r:
Z,
x = q * two_power_pos p + r ->
0
<= r ->
r < two_power_pos p ->
Zdiv_rest_proofs x p.
Lemma Zdiv_rest_correct :
forall (
x:
Z) (
p:
positive),
Zdiv_rest_proofs x p.
End power_div_with_rest.