Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

Require Import Wf_nat ZArith_base Omega 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.z:Z
Zpower_nat z 0 = 1
Proof.z:Z
Zpower_nat z 0 = 1 reflexivity. Qed.

Lemma Zpower_nat_succ_r n z : Zpower_nat z (S n) = z * (Zpower_nat z n).n:nat
z:Z
Zpower_nat z (S n) = z * Zpower_nat z n
Proof.n:nat
z:Z
Zpower_nat z (S n) = z * Zpower_nat z n reflexivity. Qed.

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.forall (n m : nat) (z : Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m
Proof.forall (n m : nat) (z : Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m
 induction n.forall (m : nat) (z : Z),
Zpower_nat z (0 + m) = Zpower_nat z 0 * Zpower_nat z m
n:nat
IHn:forall (m : nat) (z : Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m
forall (m : nat) (z : Z),
Zpower_nat z (S n + m) =
Zpower_nat z (S n) * Zpower_nat z m
 -forall (m : nat) (z : Z),
Zpower_nat z (0 + m) = Zpower_nat z 0 * Zpower_nat z m intros.m:nat
z:Z
Zpower_nat z (0 + m) = Zpower_nat z 0 * Zpower_nat z m now rewrite Zpower_nat_0_r, Z.mul_1_l.
 -n:nat
IHn:forall (m : nat) (z : Z),
Zpower_nat z (n + m) = Zpower_nat z n * Zpower_nat z m
forall (m : nat) (z : Z),
Zpower_nat z (S n + m) =
Zpower_nat z (S n) * Zpower_nat z m intros.n:nat
IHn:forall (m0 : nat) (z0 : Z),
Zpower_nat z0 (n + m0) = Zpower_nat z0 n * Zpower_nat z0 m0
m:nat
z:Z
Zpower_nat z (S n + m) =
Zpower_nat z (S n) * Zpower_nat z m simpl.n:nat
IHn:forall (m0 : nat) (z0 : Z),
Zpower_nat z0 (n + m0) = Zpower_nat z0 n * Zpower_nat z0 m0
m:nat
z:Z
z * Zpower_nat z (n + m) =
z * Zpower_nat z n * Zpower_nat z m now rewrite IHn, Z.mul_assoc.
Qed.

Conversions between powers of unary and binary integers

Lemma Zpower_pos_nat (z : Z) (p : positive) :
  Z.pow_pos z p = Zpower_nat z (Pos.to_nat p).z:Z
p:positive
Z.pow_pos z p = Zpower_nat z (Pos.to_nat p)
Proof.z:Z
p:positive
Z.pow_pos z p = Zpower_nat z (Pos.to_nat p)
  apply Pos2Nat.inj_iter.
Qed.

Lemma Zpower_nat_Z (z : Z) (n : nat) :
  Zpower_nat z n = z ^ (Z.of_nat n).z:Z
n:nat
Zpower_nat z n = z ^ Z.of_nat n
Proof.z:Z
n:nat
Zpower_nat z n = z ^ Z.of_nat n
 induction n.z:Z
Zpower_nat z 0 = z ^ Z.of_nat 0
z:Z
n:nat
IHn:Zpower_nat z n = z ^ Z.of_nat n
Zpower_nat z (S n) = z ^ Z.of_nat (S n) trivial.z:Z
n:nat
IHn:Zpower_nat z n = z ^ Z.of_nat n
Zpower_nat z (S n) = z ^ Z.of_nat (S n)
 rewrite Zpower_nat_succ_r, Nat2Z.inj_succ, Z.pow_succ_r.z:Z
n:nat
IHn:Zpower_nat z n = z ^ Z.of_nat n
z * Zpower_nat z n = z * z ^ Z.of_nat n
z:Z
n:nat
IHn:Zpower_nat z n = z ^ Z.of_nat n
0 <= Z.of_nat n
 now f_equal.z:Z
n:nat
IHn:Zpower_nat z n = z ^ Z.of_nat n
0 <= Z.of_nat n
 apply Nat2Z.is_nonneg.
Qed.

Theorem Zpower_nat_Zpower z n : 0 <= n ->
 z^n = Zpower_nat z (Z.abs_nat n).z, n:Z
0 <= n -> z ^ n = Zpower_nat z (Z.abs_nat n)
Proof.z, n:Z
0 <= n -> z ^ n = Zpower_nat z (Z.abs_nat n)
 intros.z, n:Z
H:0 <= n
z ^ n = Zpower_nat z (Z.abs_nat n) now rewrite Zpower_nat_Z, Zabs2Nat.id_abs, Z.abs_eq.
Qed.

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.n, m:positive
z:Z
Z.pow_pos z (n + m) = Z.pow_pos z n * Z.pow_pos z m
Proof.n, m:positive
z:Z
Z.pow_pos z (n + m) = Z.pow_pos z n * Z.pow_pos z m
 now apply (Z.pow_add_r z (Zpos n) (Zpos m)).
Qed.

Hint Immediate Zpower_nat_is_exp Zpower_pos_is_exp : zarith.
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.x, n, m:Z
n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m
Proof.x, n, m:Z
n >= 0 -> m >= 0 -> x ^ (n + m) = x ^ n * x ^ m
 Z.swap_greater.x, n, m:Z
0 <= n -> 0 <= m -> x ^ (n + m) = x ^ n * x ^ m apply Z.pow_add_r.
Qed.

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

  Lemma shift_nat_equiv n p : shift_nat n p = Pos.shiftl_nat p n.n:nat
p:positive
shift_nat n p = Pos.shiftl_nat p n
  Proof.n:nat
p:positive
shift_nat n p = Pos.shiftl_nat p n reflexivity. Qed.

  Lemma shift_pos_equiv n p : shift_pos n p = Pos.shiftl p (Npos n).n, p:positive
shift_pos n p = Pos.shiftl p (N.pos n)
  Proof.n, p:positive
shift_pos n p = Pos.shiftl p (N.pos n) reflexivity. Qed.

  Lemma shift_equiv n p : 0<=n -> Zpos (shift n p) = Z.shiftl (Zpos p) n.n:Z
p:positive
0 <= n -> Z.pos (shift n p) = Z.shiftl (Z.pos p) n
  Proof.n:Z
p:positive
0 <= n -> Z.pos (shift n p) = Z.shiftl (Z.pos p) n
   destruct n.p:positive
0 <= 0 -> Z.pos (shift 0 p) = Z.shiftl (Z.pos p) 0
p0, p:positive
0 <= Z.pos p0 ->
Z.pos (shift (Z.pos p0) p) =
Z.shiftl (Z.pos p) (Z.pos p0)
p0, p:positive
0 <= Z.neg p0 ->
Z.pos (shift (Z.neg p0) p) =
Z.shiftl (Z.pos p) (Z.neg p0)
   -p:positive
0 <= 0 -> Z.pos (shift 0 p) = Z.shiftl (Z.pos p) 0 trivial.
   -p0, p:positive
0 <= Z.pos p0 ->
Z.pos (shift (Z.pos p0) p) =
Z.shiftl (Z.pos p) (Z.pos p0) simpl; intros.p0, p:positive
H:0 <= Z.pos p0
Z.pos (Pos.iter xO p p0) =
Pos.iter (Z.mul 2) (Z.pos p) p0 now apply Pos.iter_swap_gen.
   -p0, p:positive
0 <= Z.neg p0 ->
Z.pos (shift (Z.neg p0) p) =
Z.shiftl (Z.pos p) (Z.neg p0) now destruct 1.
  Qed.

  Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).n:nat
two_power_nat n = 2 ^ Z.of_nat n
  Proof.n:nat
two_power_nat n = 2 ^ Z.of_nat n
   induction n.two_power_nat 0 = 2 ^ Z.of_nat 0
n:nat
IHn:two_power_nat n = 2 ^ Z.of_nat n
two_power_nat (S n) = 2 ^ Z.of_nat (S n)
   -two_power_nat 0 = 2 ^ Z.of_nat 0 trivial.
   -n:nat
IHn:two_power_nat n = 2 ^ Z.of_nat n
two_power_nat (S n) = 2 ^ Z.of_nat (S n) now rewrite Nat2Z.inj_succ, Z.pow_succ_r, <- IHn by apply Nat2Z.is_nonneg.
  Qed.

  Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p.p:positive
two_power_pos p = 2 ^ Z.pos p
  Proof.p:positive
two_power_pos p = 2 ^ Z.pos p
   now apply Pos.iter_swap_gen.
  Qed.

  Lemma two_p_equiv x : two_p x = 2 ^ x.x:Z
two_p x = 2 ^ x
  Proof.x:Z
two_p x = 2 ^ x
   destruct x; trivial.p:positive
two_p (Z.pos p) = 2 ^ Z.pos p apply two_power_pos_equiv.
  Qed.

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.n:nat
two_power_nat (S n) = 2 * two_power_nat n
  Proof.n:nat
two_power_nat (S n) = 2 * two_power_nat n reflexivity. Qed.

  Lemma shift_nat_plus n m x :
    shift_nat (n + m) x = shift_nat n (shift_nat m x).n, m:nat
x:positive
shift_nat (n + m) x = shift_nat n (shift_nat m x)
  Proof.n, m:nat
x:positive
shift_nat (n + m) x = shift_nat n (shift_nat m x)
   induction n; simpl; now f_equal.
  Qed.

  Theorem shift_nat_correct n x :
    Zpos (shift_nat n x) = Zpower_nat 2 n * Zpos x.n:nat
x:positive
Z.pos (shift_nat n x) = Zpower_nat 2 n * Z.pos x
  Proof.n:nat
x:positive
Z.pos (shift_nat n x) = Zpower_nat 2 n * Z.pos x
   induction n.x:positive
Z.pos (shift_nat 0 x) = Zpower_nat 2 0 * Z.pos x
n:nat
x:positive
IHn:Z.pos (shift_nat n x) = Zpower_nat 2 n * Z.pos x
Z.pos (shift_nat (S n) x) =
Zpower_nat 2 (S n) * Z.pos x
   -x:positive
Z.pos (shift_nat 0 x) = Zpower_nat 2 0 * Z.pos x trivial.
   -n:nat
x:positive
IHn:Z.pos (shift_nat n x) = Zpower_nat 2 n * Z.pos x
Z.pos (shift_nat (S n) x) =
Zpower_nat 2 (S n) * Z.pos x now rewrite Zpower_nat_succ_r, <- Z.mul_assoc, <- IHn.
  Qed.

  Theorem two_power_nat_correct n : two_power_nat n = Zpower_nat 2 n.n:nat
two_power_nat n = Zpower_nat 2 n
  Proof.n:nat
two_power_nat n = Zpower_nat 2 n
   now rewrite two_power_nat_equiv, Zpower_nat_Z.
  Qed.

  Lemma shift_pos_nat p x : shift_pos p x = shift_nat (Pos.to_nat p) x.p, x:positive
shift_pos p x = shift_nat (Pos.to_nat p) x
  Proof.p, x:positive
shift_pos p x = shift_nat (Pos.to_nat p) x
   apply Pos2Nat.inj_iter.
  Qed.

  Lemma two_power_pos_nat p : two_power_pos p = two_power_nat (Pos.to_nat p).p:positive
two_power_pos p = two_power_nat (Pos.to_nat p)
  Proof.p:positive
two_power_pos p = two_power_nat (Pos.to_nat p)
   unfold two_power_pos.p:positive
Z.pos (shift_pos p 1) = two_power_nat (Pos.to_nat p) now rewrite shift_pos_nat.
  Qed.

  Theorem shift_pos_correct p x :
    Zpos (shift_pos p x) = Z.pow_pos 2 p * Zpos x.p, x:positive
Z.pos (shift_pos p x) = Z.pow_pos 2 p * Z.pos x
  Proof.p, x:positive
Z.pos (shift_pos p x) = Z.pow_pos 2 p * Z.pos x
   now rewrite shift_pos_nat, Zpower_pos_nat, shift_nat_correct.
  Qed.

  Theorem two_power_pos_correct x : two_power_pos x = Z.pow_pos 2 x.x:positive
two_power_pos x = Z.pow_pos 2 x
  Proof.x:positive
two_power_pos x = Z.pow_pos 2 x
   apply two_power_pos_equiv.
  Qed.

  Theorem two_power_pos_is_exp x y :
   two_power_pos (x + y) = two_power_pos x * two_power_pos y.x, y:positive
two_power_pos (x + y) =
two_power_pos x * two_power_pos y
  Proof.x, y:positive
two_power_pos (x + y) =
two_power_pos x * two_power_pos y
    rewrite 3 two_power_pos_equiv.x, y:positive
2 ^ Z.pos (x + y) = 2 ^ Z.pos x * 2 ^ Z.pos y now apply (Z.pow_add_r 2 (Zpos x) (Zpos y)).
  Qed.

  Lemma two_p_correct x : two_p x = 2^x.x:Z
two_p x = 2 ^ x
  Proof (two_p_equiv x).

  Theorem two_p_is_exp x y :
    0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y.x, y:Z
0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y
  Proof.x, y:Z
0 <= x -> 0 <= y -> two_p (x + y) = two_p x * two_p y
    rewrite !two_p_equiv.x, y:Z
0 <= x -> 0 <= y -> 2 ^ (x + y) = 2 ^ x * 2 ^ y apply Z.pow_add_r.
  Qed.

  Lemma two_p_gt_ZERO x : 0 <= x -> two_p x > 0.x:Z
0 <= x -> two_p x > 0
  Proof.x:Z
0 <= x -> two_p x > 0
   Z.swap_greater.x:Z
0 <= x -> 0 < two_p x rewrite two_p_equiv.x:Z
0 <= x -> 0 < 2 ^ x now apply Z.pow_pos_nonneg.
  Qed.

  Lemma two_p_S x : 0 <= x -> two_p (Z.succ x) = 2 * two_p x.x:Z
0 <= x -> two_p (Z.succ x) = 2 * two_p x
  Proof.x:Z
0 <= x -> two_p (Z.succ x) = 2 * two_p x
   rewrite !two_p_equiv.x:Z
0 <= x -> 2 ^ Z.succ x = 2 * 2 ^ x now apply Z.pow_succ_r.
  Qed.

  Lemma two_p_pred x : 0 <= x -> two_p (Z.pred x) < two_p x.x:Z
0 <= x -> two_p (Z.pred x) < two_p x
  Proof.x:Z
0 <= x -> two_p (Z.pred x) < two_p x
   rewrite !two_p_equiv.x:Z
0 <= x -> 2 ^ Z.pred x < 2 ^ x intros.x:Z
H:0 <= x
2 ^ Z.pred x < 2 ^ x apply Z.pow_lt_mono_r; auto with zarith.
  Qed.

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 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.x:Z
p:positive
let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
d = two_power_pos p
  Proof.x:Z
p:positive
let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
d = two_power_pos p
   rewrite Pos2Nat.inj_iter, two_power_pos_nat.x:Z
p:positive
let (_, d) :=
  nat_rect (fun _ : nat => (Z * Z * Z)%type) (x, 0, 1)
    (fun _ : nat => Zdiv_rest_aux) (Pos.to_nat p) in
d = two_power_nat (Pos.to_nat p)
   induction (Pos.to_nat p); simpl; trivial.x:Z
p:positive
n:nat
IHn:let (_, d) :=
nat_rect (fun _ : nat => (Z * Z * Z)%type) (x, 0, 1)
(fun _ : nat => Zdiv_rest_aux) n in
d = two_power_nat n
let (_, d) :=
  Zdiv_rest_aux
    (nat_rect (fun _ : nat => (Z * Z * Z)%type)
       (x, 0, 1) (fun _ : nat => Zdiv_rest_aux) n) in
d = two_power_nat (S n)
   destruct (nat_rect _ _ _ _) as ((q,r),d).x:Z
p:positive
n:nat
q, r, d:Z
IHn:d = two_power_nat n
let (_, d0) := Zdiv_rest_aux (q, r, d) in
d0 = two_power_nat (S n)
   unfold Zdiv_rest_aux.x:Z
p:positive
n:nat
q, r, d:Z
IHn:d = two_power_nat n
2 * d = two_power_nat (S n) rewrite two_power_nat_S; now f_equal.
  Qed.

  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.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
  Proof.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
   apply Pos.iter_invariant; [|omega].x:Z
p:positive
forall x0 : Z * Z * Z,
(let '(q, r, d) := x0 in x = q * d + r /\ 0 <= r < d) ->
let
'(q, r, d) := Zdiv_rest_aux x0 in
 x = q * d + r /\ 0 <= r < d
   intros ((q,r),d) (H,H').x:Z
p:positive
q, r, d:Z
H:x = q * d + r
H':0 <= r < d
let
'(q0, r0, d0) := Zdiv_rest_aux (q, r, d) in
 x = q0 * d0 + r0 /\ 0 <= r0 < d0 unfold Zdiv_rest_aux.x:Z
p:positive
q, r, d:Z
H:x = q * d + r
H':0 <= r < d
let
'(q0, r0) :=
 match q with
 | 0 => (0, r)
 | Z.pos (n~1)%positive => (Z.pos n, d + r)
 | Z.pos (n~0)%positive => (Z.pos n, r)
 | 1 => (0, d + r)
 | Z.neg (n~1)%positive => (Z.neg n - 1, d + r)
 | Z.neg (n~0)%positive => (Z.neg n, r)
 | -1 => (-1, d + r)
 end in x = q0 * (2 * d) + r0 /\ 0 <= r0 < 2 * d
   destruct q as [ |[q|q| ]|[q|q| ]]; try omega.x:Z
p, q:positive
r, d:Z
H:x = Z.pos q~1 * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + (d + r) /\ 0 <= d + r < 2 * d
x:Z
p, q:positive
r, d:Z
H:x = Z.pos q~0 * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + r /\ 0 <= r < 2 * d
x:Z
p, q:positive
r, d:Z
H:x = Z.neg q~1 * d + r
H':0 <= r < d
x = (Z.neg q - 1) * (2 * d) + (d + r) /\
0 <= d + r < 2 * d
x:Z
p, q:positive
r, d:Z
H:x = Z.neg q~0 * d + r
H':0 <= r < d
x = Z.neg q * (2 * d) + r /\ 0 <= r < 2 * d
   -x:Z
p, q:positive
r, d:Z
H:x = Z.pos q~1 * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + (d + r) /\ 0 <= d + r < 2 * d rewrite Pos2Z.inj_xI, Z.mul_add_distr_r in H.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.pos q * d + 1 * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + (d + r) /\ 0 <= d + r < 2 * d
     rewrite Z.mul_shuffle3, Z.mul_assoc.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.pos q * d + 1 * d + r
H':0 <= r < d
x = 2 * Z.pos q * d + (d + r) /\ 0 <= d + r < 2 * d omega.
   -x:Z
p, q:positive
r, d:Z
H:x = Z.pos q~0 * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + r /\ 0 <= r < 2 * d rewrite Pos2Z.inj_xO in H.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.pos q * d + r
H':0 <= r < d
x = Z.pos q * (2 * d) + r /\ 0 <= r < 2 * d
     rewrite Z.mul_shuffle3, Z.mul_assoc.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.pos q * d + r
H':0 <= r < d
x = 2 * Z.pos q * d + r /\ 0 <= r < 2 * d omega.
   -x:Z
p, q:positive
r, d:Z
H:x = Z.neg q~1 * d + r
H':0 <= r < d
x = (Z.neg q - 1) * (2 * d) + (d + r) /\
0 <= d + r < 2 * d rewrite Pos2Z.neg_xI, Z.mul_sub_distr_r in H.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.neg q * d - 1 * d + r
H':0 <= r < d
x = (Z.neg q - 1) * (2 * d) + (d + r) /\
0 <= d + r < 2 * d
     rewrite Z.mul_sub_distr_r, Z.mul_shuffle3, Z.mul_assoc.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.neg q * d - 1 * d + r
H':0 <= r < d
x = 2 * Z.neg q * d - 1 * (2 * d) + (d + r) /\
0 <= d + r < 2 * d omega.
   -x:Z
p, q:positive
r, d:Z
H:x = Z.neg q~0 * d + r
H':0 <= r < d
x = Z.neg q * (2 * d) + r /\ 0 <= r < 2 * d rewrite Pos2Z.neg_xO in H.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.neg q * d + r
H':0 <= r < d
x = Z.neg q * (2 * d) + r /\ 0 <= r < 2 * d
     rewrite Z.mul_shuffle3, Z.mul_assoc.x:Z
p, q:positive
r, d:Z
H:x = 2 * Z.neg q * d + r
H':0 <= r < d
x = 2 * Z.neg q * d + r /\ 0 <= r < 2 * d omega.
  Qed.

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.x:Z
p:positive
Zdiv_rest_proofs x p
  Proof.x:Z
p:positive
Zdiv_rest_proofs x p
    generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).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) ->
(let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
 d = two_power_pos p) -> Zdiv_rest_proofs x p
    destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).x:Z
p:positive
q, r, d:Z
x = q * d + r /\ 0 <= r < d ->
d = two_power_pos p -> Zdiv_rest_proofs x p
    intros (H1,(H2,H3)) ->.x:Z
p:positive
q, r:Z
H1:x = q * two_power_pos p + r
H2:0 <= r
H3:r < two_power_pos p
Zdiv_rest_proofs x p now exists q r.
  Qed.

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).x:Z
p:positive
let (q, r) := Zdiv_rest x p in
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p
  Proof.x:Z
p:positive
let (q, r) := Zdiv_rest x p in
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p
   unfold Zdiv_rest.x:Z
p:positive
let (q, r) :=
  let (qr, _) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
  qr in
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p
   generalize (Zdiv_rest_correct1 x p); generalize (Zdiv_rest_correct2 x p).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) ->
(let (_, d) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
 d = two_power_pos p) ->
let (q, r) :=
  let (qr, _) := Pos.iter Zdiv_rest_aux (x, 0, 1) p in
  qr in
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p
   destruct (Pos.iter Zdiv_rest_aux (x, 0, 1) p) as ((q,r),d).x:Z
p:positive
q, r, d:Z
x = q * d + r /\ 0 <= r < d ->
d = two_power_pos p ->
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p
   intros H ->.x:Z
p:positive
q, r:Z
H:x = q * two_power_pos p + r /\
0 <= r < two_power_pos p
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p now rewrite two_power_pos_equiv in H.
  Qed.

Equivalence with Z.shiftr

  Lemma Zdiv_rest_shiftr x p :
   fst (Zdiv_rest x p) = Z.shiftr x (Zpos p).x:Z
p:positive
fst (Zdiv_rest x p) = Z.shiftr x (Z.pos p)
  Proof.x:Z
p:positive
fst (Zdiv_rest x p) = Z.shiftr x (Z.pos p)
   generalize (Zdiv_rest_ok x p).x:Z
p:positive
(let (q, r) := Zdiv_rest x p in
 x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p) ->
fst (Zdiv_rest x p) = Z.shiftr x (Z.pos p) destruct (Zdiv_rest x p) as (q,r).x:Z
p:positive
q, r:Z
x = q * 2 ^ Z.pos p + r /\ 0 <= r < 2 ^ Z.pos p ->
fst (q, r) = Z.shiftr x (Z.pos p)
   intros (H,H').x:Z
p:positive
q, r:Z
H:x = q * 2 ^ Z.pos p + r
H':0 <= r < 2 ^ Z.pos p
fst (q, r) = Z.shiftr x (Z.pos p) simpl.x:Z
p:positive
q, r:Z
H:x = q * 2 ^ Z.pos p + r
H':0 <= r < 2 ^ Z.pos p
q = Z.shiftr x (Z.pos p)
   rewrite Z.shiftr_div_pow2 by easy.x:Z
p:positive
q, r:Z
H:x = q * 2 ^ Z.pos p + r
H':0 <= r < 2 ^ Z.pos p
q = x / 2 ^ Z.pos p
   apply Z.div_unique_pos with r; trivial.x:Z
p:positive
q, r:Z
H:x = q * 2 ^ Z.pos p + r
H':0 <= r < 2 ^ Z.pos p
x = 2 ^ Z.pos p * q + r now rewrite Z.mul_comm.
  Qed.

End power_div_with_rest.