Library Coq.ZArith.Zpower



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

Infix "^" := Zpower : Z_scope.

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)

Definition Zpower_nat (z:Z) (n:nat) := iter_nat n Z (fun x:Z => z * x) 1.

Zpower_nat_is_exp says Zpower_nat is a morphism for plus : nat->nat and Zmult : 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.

This theorem shows that powers of unary and binary integers are the same thing, modulo the function convert : positive -> nat

Lemma Zpower_pos_nat :
  forall (z:Z) (p:positive), Zpower_pos z p = Zpower_nat z (nat_of_P p).

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

Lemma Zpower_pos_is_exp :
  forall (n m:positive) (z:Z),
    Zpower_pos z (n + m) = Zpower_pos z n * Zpower_pos z m.

Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
Hint Unfold Zpower_pos Zpower_nat: zarith.

Theorem Zpower_exp :
  forall x n m:Z, 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. 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

  Definition shift_nat (n:nat) (z:positive) := iter_nat n positive xO z.
  Definition shift_pos (n z:positive) := iter_pos n positive xO z.
  Definition shift (n:Z) (z:positive) :=
    match n with
      | Z0 => z
      | Zpos p => iter_pos p positive xO z
      | 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).

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

  Lemma shift_nat_plus :
    forall (n m:nat) (x:positive),
      shift_nat (n + m) x = shift_nat n (shift_nat m x).

  Theorem shift_nat_correct :
    forall (n:nat) (x:positive), Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.

  Theorem two_power_nat_correct :
    forall n:nat, two_power_nat n = Zpower_nat 2 n.

Second we show that two_power_pos and two_power_nat are the same
  Lemma shift_pos_nat :
    forall p x:positive, shift_pos p x = shift_nat (nat_of_P p) x.

  Lemma two_power_pos_nat :
    forall p:positive, two_power_pos p = two_power_nat (nat_of_P p).

Then we deduce that two_power_pos is also correct

  Theorem shift_pos_correct :
    forall p x:positive, Zpos (shift_pos p x) = Zpower_pos 2 p * Zpos x.

  Theorem two_power_pos_correct :
    forall x:positive, two_power_pos x = Zpower_pos 2 x.

Some consequences

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

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.

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

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

  Lemma two_p_gt_ZERO : forall x:Z, 0 <= x -> two_p x > 0.

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

  Lemma two_p_pred : forall x:Z, 0 <= x -> two_p (Zpred x) < two_p x.

  Lemma Zlt_lt_double : forall x y:Z, 0 <= x < y -> x < 2 * y.

  End Powers_of_2.

Hint Resolve two_p_gt_ZERO: zarith.
Hint Immediate two_p_pred two_p_S: zarith.

Section power_div_with_rest.

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.