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

Definition Zpower_nat (z:Z) (n:nat) := nat_iter n (Z.mul z) 1.

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).

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

Lemma Zpower_pos_nat (z : Z) (p : positive) :
  Z.pow_pos z p = Zpower_nat z (Pos.to_nat p).

Lemma Zpower_nat_Z (z : Z) (n : nat) :
  Zpower_nat z n = z ^ (Z.of_nat n).

Theorem Zpower_nat_Zpower z n : 0 <= n ->
 z^n = Zpower_nat z (Z.abs_nat n).

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.

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.

Section Powers_of_2.

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

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

  Lemma shift_nat_equiv n p : shift_nat n p = Pos.shiftl_nat p n.

  Lemma shift_pos_equiv n p : shift_pos n p = Pos.shiftl p (Npos n).

  Lemma shift_equiv n p : 0<=n -> Zpos (shift n p) = Z.shiftl (Zpos p) n.

  Lemma two_power_nat_equiv n : two_power_nat n = 2 ^ (Z.of_nat n).

  Lemma two_power_pos_equiv p : two_power_pos p = 2 ^ Zpos p.

  Lemma two_p_equiv x : two_p x = 2 ^ x.

  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.

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

Section power_div_with_rest.

  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 p Zdiv_rest_aux (x, 0, 1) in qr.

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

  Lemma Zdiv_rest_correct2 (x:Z) (p:positive) :
    let ´(q,r,d) := Pos.iter p Zdiv_rest_aux (x, 0, 1) 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 (x:Z) (p:positive) : Zdiv_rest_proofs x p.

  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).

  Lemma Zdiv_rest_shiftr x p :
   fst (Zdiv_rest x p) = Z.shiftr x (Zpos p).

End power_div_with_rest.