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.