# Library Coq.ZArith.Zpower

Require Import Wf_nat ZArith_base Zcomplements.
Require Export Zpow_def.
Local Open Scope Z_scope.

# Power functions over Z

Nota : this file is mostly deprecated. The definition of Z.pow and its usual properties are now provided by module BinInt.Z. Powers of 2 are also available there (see Z.shiftl and Z.shiftr). Only remain here:
• Zpower_nat : a power function with a nat exponent
• old-style powers of two, such as two_p
• Zdiv_rest : a division + modulo when the divisor is a power of 2
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)

Definition Zpower_nat (z:Z) := nat_rect _ 1 (fun _ => Z.mul z).

Lemma Zpower_nat_0_r z : Zpower_nat z 0 = 1.

Lemma Zpower_nat_succ_r n z : Zpower_nat z (S n) = z * (Zpower_nat z n).

Zpower_nat_is_exp says Zpower_nat is a morphism for plus : nat->nat->nat and Z.mul : Z->Z->Z

Lemma Zpower_nat_is_exp :
forall (n m:nat) (z:Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m.

Conversions between powers of unary and binary integers
The function (Z.pow_pos z) is a morphism for Pos.add : positive->positive->positive and Z.mul : Z->Z->Z

Lemma Zpower_pos_is_exp (n m : positive)(z:Z) :
Z.pow_pos z (n + m) = Z.pow_pos z n * Z.pow_pos z m.

#[global]
Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
#[global]
Hint Unfold Z.pow_pos Zpower_nat: zarith.

Theorem Zpower_exp x n m :
n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m.

Section Powers_of_2.

# Powers of 2

For the powers of two, that will be widely used, a more direct calculus is possible. shift n m computes 2^n * m, i.e. m shifted by n positions

Definition shift_nat (n:nat) (z:positive) := nat_rect _ z (fun _ => xO) n.
Definition shift_pos (n z:positive) := Pos.iter xO z n.
Definition shift (n:Z) (z:positive) :=
match n with
| Z0 => z
| Zpos p => Pos.iter xO z p
| Zneg p => z
end.

Definition two_power_nat (n:nat) := Zpos (shift_nat n 1).
Definition two_power_pos (x:positive) := Zpos (shift_pos x 1).

Definition two_p (x:Z) :=
match x with
| Z0 => 1
| Zpos y => two_power_pos y
| Zneg y => 0
end.

Equivalence with notions defined in BinInt
Properties of these old versions of powers of two

Lemma two_power_nat_S n : two_power_nat (S n) = 2 * two_power_nat n.

Lemma shift_nat_plus n m x :
shift_nat (n + m) x = shift_nat n (shift_nat m x).

Theorem shift_nat_correct n x :
Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.

Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n.

Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x.

Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p).

Theorem shift_pos_correct p x :
Zpos (shift_pos p x) = Z.pow_pos 2 p * Zpos x.

Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x.

Theorem two_power_pos_is_exp x y :
two_power_pos (x + y) = two_power_pos x * two_power_pos y.

Lemma two_p_correct x : two_p x = 2^x.

Theorem two_p_is_exp x y :
0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.

Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0.

Lemma two_p_S x : 0 <= x -> two_p (Z.succ x) = 2 * two_p x.

Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x.

End Powers_of_2.

#[global]
Hint Resolve two_p_gt_ZERO: zarith.
#[global]
Hint Immediate two_p_pred two_p_S: zarith.

Section power_div_with_rest.

# Division by a power of two.

To x:Z and p:positive, q,r are associated such that x = 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 '(q,r,d) := qrd 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) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in qr.

Lemma Zdiv_rest_correct1 (x:Z) (p:positive) :
let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
d = two_power_pos p.

Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
let '(q,r,d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
x = q * d + r /\ 0 <= r < d.

Old-style rich specification by proof of existence

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 (x:Z) (p:positive) : Zdiv_rest_proofs x p.

Direct correctness of Zdiv_rest

Lemma Zdiv_rest_ok x p :
let (q,r) := Zdiv_rest x p in
x = q * 2^(Zpos p) + r /\ 0 <= r < 2^(Zpos p).

Equivalence with Z.shiftr