# Library Coq.Numbers.Integer.BigZ.ZMake

Require Import ZArith.
Require Import BigNumPrelude.
Require Import NSig.
Require Import ZSig.

Open Scope Z_scope.

# ZMake

A generic transformation from a structure of natural numbers NSig.NType to a structure of integers ZSig.ZType.

Module Make (NN:NType) <: ZType.

Inductive t_ :=
| Pos : NN.t -> t_
| Neg : NN.t -> t_.

Definition t := t_.

Definition zero := Pos NN.zero.
Definition one := Pos NN.one.
Definition two := Pos NN.two.
Definition minus_one := Neg NN.one.

Definition of_Z x :=
match x with
| Zpos x => Pos (NN.of_N (Npos x))
| Z0 => zero
| Zneg x => Neg (NN.of_N (Npos x))
end.

Definition to_Z x :=
match x with
| Pos nx => NN.to_Z nx
| Neg nx => Z.opp (NN.to_Z nx)
end.

Theorem spec_of_Z: forall x, to_Z (of_Z x) = x.

Definition eq x y := (to_Z x = to_Z y).

Theorem spec_0: to_Z zero = 0.

Theorem spec_1: to_Z one = 1.

Theorem spec_2: to_Z two = 2.

Theorem spec_m1: to_Z minus_one = -1.

Definition compare x y :=
match x, y with
| Pos nx, Pos ny => NN.compare nx ny
| Pos nx, Neg ny =>
match NN.compare nx NN.zero with
| Gt => Gt
| _ => NN.compare ny NN.zero
end
| Neg nx, Pos ny =>
match NN.compare NN.zero nx with
| Lt => Lt
| _ => NN.compare NN.zero ny
end
| Neg nx, Neg ny => NN.compare ny nx
end.

Theorem spec_compare :
forall x y, compare x y = Z.compare (to_Z x) (to_Z y).

Definition eqb x y :=
match compare x y with
| Eq => true
| _ => false
end.

Theorem spec_eqb x y : eqb x y = Z.eqb (to_Z x) (to_Z y).

Definition lt n m := to_Z n < to_Z m.
Definition le n m := to_Z n <= to_Z m.

Definition ltb (x y : t) : bool :=
match compare x y with
| Lt => true
| _ => false
end.

Theorem spec_ltb x y : ltb x y = Z.ltb (to_Z x) (to_Z y).

Definition leb (x y : t) : bool :=
match compare x y with
| Gt => false
| _ => true
end.

Theorem spec_leb x y : leb x y = Z.leb (to_Z x) (to_Z y).

Definition min n m := match compare n m with Gt => m | _ => n end.
Definition max n m := match compare n m with Lt => m | _ => n end.

Theorem spec_min : forall n m, to_Z (min n m) = Z.min (to_Z n) (to_Z m).

Theorem spec_max : forall n m, to_Z (max n m) = Z.max (to_Z n) (to_Z m).

Definition to_N x :=
match x with
| Pos nx => nx
| Neg nx => nx
end.

Definition abs x := Pos (to_N x).

Theorem spec_abs: forall x, to_Z (abs x) = Z.abs (to_Z x).

Definition opp x :=
match x with
| Pos nx => Neg nx
| Neg nx => Pos nx
end.

Theorem spec_opp: forall x, to_Z (opp x) = - to_Z x.

Definition succ x :=
match x with
| Pos n => Pos (NN.succ n)
| Neg n =>
match NN.compare NN.zero n with
| Lt => Neg (NN.pred n)
| _ => one
end
end.

Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.

match x, y with
| Pos nx, Pos ny => Pos (NN.add nx ny)
| Pos nx, Neg ny =>
match NN.compare nx ny with
| Gt => Pos (NN.sub nx ny)
| Eq => zero
| Lt => Neg (NN.sub ny nx)
end
| Neg nx, Pos ny =>
match NN.compare nx ny with
| Gt => Neg (NN.sub nx ny)
| Eq => zero
| Lt => Pos (NN.sub ny nx)
end
| Neg nx, Neg ny => Neg (NN.add nx ny)
end.

Theorem spec_add: forall x y, to_Z (add x y) = to_Z x + to_Z y.

Definition pred x :=
match x with
| Pos nx =>
match NN.compare NN.zero nx with
| Lt => Pos (NN.pred nx)
| _ => minus_one
end
| Neg nx => Neg (NN.succ nx)
end.

Theorem spec_pred: forall x, to_Z (pred x) = to_Z x - 1.

Definition sub x y :=
match x, y with
| Pos nx, Pos ny =>
match NN.compare nx ny with
| Gt => Pos (NN.sub nx ny)
| Eq => zero
| Lt => Neg (NN.sub ny nx)
end
| Pos nx, Neg ny => Pos (NN.add nx ny)
| Neg nx, Pos ny => Neg (NN.add nx ny)
| Neg nx, Neg ny =>
match NN.compare nx ny with
| Gt => Neg (NN.sub nx ny)
| Eq => zero
| Lt => Pos (NN.sub ny nx)
end
end.

Theorem spec_sub: forall x y, to_Z (sub x y) = to_Z x - to_Z y.

Definition mul x y :=
match x, y with
| Pos nx, Pos ny => Pos (NN.mul nx ny)
| Pos nx, Neg ny => Neg (NN.mul nx ny)
| Neg nx, Pos ny => Neg (NN.mul nx ny)
| Neg nx, Neg ny => Pos (NN.mul nx ny)
end.

Theorem spec_mul: forall x y, to_Z (mul x y) = to_Z x * to_Z y.

Definition square x :=
match x with
| Pos nx => Pos (NN.square nx)
| Neg nx => Pos (NN.square nx)
end.

Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x.

Definition pow_pos x p :=
match x with
| Pos nx => Pos (NN.pow_pos nx p)
| Neg nx =>
match p with
| xH => x
| xO _ => Pos (NN.pow_pos nx p)
| xI _ => Neg (NN.pow_pos nx p)
end
end.

Theorem spec_pow_pos: forall x n, to_Z (pow_pos x n) = to_Z x ^ Zpos n.

Definition pow_N x n :=
match n with
| N0 => one
| Npos p => pow_pos x p
end.

Theorem spec_pow_N: forall x n, to_Z (pow_N x n) = to_Z x ^ Z.of_N n.

Definition pow x y :=
match to_Z y with
| Z0 => one
| Zpos p => pow_pos x p
| Zneg p => zero
end.

Theorem spec_pow: forall x y, to_Z (pow x y) = to_Z x ^ to_Z y.

Definition log2 x :=
match x with
| Pos nx => Pos (NN.log2 nx)
| Neg nx => zero
end.

Theorem spec_log2: forall x, to_Z (log2 x) = Z.log2 (to_Z x).

Definition sqrt x :=
match x with
| Pos nx => Pos (NN.sqrt nx)
| Neg nx => Neg NN.zero
end.

Theorem spec_sqrt: forall x, to_Z (sqrt x) = Z.sqrt (to_Z x).

Definition div_eucl x y :=
match x, y with
| Pos nx, Pos ny =>
let (q, r) := NN.div_eucl nx ny in
(Pos q, Pos r)
| Pos nx, Neg ny =>
let (q, r) := NN.div_eucl nx ny in
if NN.eqb NN.zero r
then (Neg q, zero)
else (Neg (NN.succ q), Neg (NN.sub ny r))
| Neg nx, Pos ny =>
let (q, r) := NN.div_eucl nx ny in
if NN.eqb NN.zero r
then (Neg q, zero)
else (Neg (NN.succ q), Pos (NN.sub ny r))
| Neg nx, Neg ny =>
let (q, r) := NN.div_eucl nx ny in
(Pos q, Neg r)
end.

Ltac break_nonneg x px EQx :=
let H := fresh "H" in
assert (H:=NN.spec_pos x);
destruct (NN.to_Z x) as [|px|px] eqn:EQx;
[clear H|clear H|elim H; reflexivity].

Theorem spec_div_eucl: forall x y,
let (q,r) := div_eucl x y in
(to_Z q, to_Z r) = Z.div_eucl (to_Z x) (to_Z y).

Definition div x y := fst (div_eucl x y).

Definition spec_div: forall x y,
to_Z (div x y) = to_Z x / to_Z y.

Definition modulo x y := snd (div_eucl x y).

Theorem spec_modulo:
forall x y, to_Z (modulo x y) = to_Z x mod to_Z y.

Definition quot x y :=
match x, y with
| Pos nx, Pos ny => Pos (NN.div nx ny)
| Pos nx, Neg ny => Neg (NN.div nx ny)
| Neg nx, Pos ny => Neg (NN.div nx ny)
| Neg nx, Neg ny => Pos (NN.div nx ny)
end.

Definition rem x y :=
if eqb y zero then x
else
match x, y with
| Pos nx, Pos ny => Pos (NN.modulo nx ny)
| Pos nx, Neg ny => Pos (NN.modulo nx ny)
| Neg nx, Pos ny => Neg (NN.modulo nx ny)
| Neg nx, Neg ny => Neg (NN.modulo nx ny)
end.

Lemma spec_quot : forall x y, to_Z (quot x y) = (to_Z x) ÷ (to_Z y).

Lemma spec_rem : forall x y,
to_Z (rem x y) = Z.rem (to_Z x) (to_Z y).

Definition gcd x y :=
match x, y with
| Pos nx, Pos ny => Pos (NN.gcd nx ny)
| Pos nx, Neg ny => Pos (NN.gcd nx ny)
| Neg nx, Pos ny => Pos (NN.gcd nx ny)
| Neg nx, Neg ny => Pos (NN.gcd nx ny)
end.

Theorem spec_gcd: forall a b, to_Z (gcd a b) = Z.gcd (to_Z a) (to_Z b).

Definition sgn x :=
match compare zero x with
| Lt => one
| Eq => zero
| Gt => minus_one
end.

Lemma spec_sgn : forall x, to_Z (sgn x) = Z.sgn (to_Z x).

Definition even z :=
match z with
| Pos n => NN.even n
| Neg n => NN.even n
end.

Definition odd z :=
match z with
| Pos n => NN.odd n
| Neg n => NN.odd n
end.

Lemma spec_even : forall z, even z = Z.even (to_Z z).

Lemma spec_odd : forall z, odd z = Z.odd (to_Z z).

Definition norm_pos z :=
match z with
| Pos _ => z
| Neg n => if NN.eqb n NN.zero then Pos n else z
end.

Definition testbit a n :=
match norm_pos n, norm_pos a with
| Pos p, Pos a => NN.testbit a p
| Pos p, Neg a => negb (NN.testbit (NN.pred a) p)
| Neg p, _ => false
end.

Definition shiftl a n :=
match norm_pos a, n with
| Pos a, Pos n => Pos (NN.shiftl a n)
| Pos a, Neg n => Pos (NN.shiftr a n)
| Neg a, Pos n => Neg (NN.shiftl a n)
| Neg a, Neg n => Neg (NN.succ (NN.shiftr (NN.pred a) n))
end.

Definition shiftr a n := shiftl a (opp n).

Definition lor a b :=
match norm_pos a, norm_pos b with
| Pos a, Pos b => Pos (NN.lor a b)
| Neg a, Pos b => Neg (NN.succ (NN.ldiff (NN.pred a) b))
| Pos a, Neg b => Neg (NN.succ (NN.ldiff (NN.pred b) a))
| Neg a, Neg b => Neg (NN.succ (NN.land (NN.pred a) (NN.pred b)))
end.

Definition land a b :=
match norm_pos a, norm_pos b with
| Pos a, Pos b => Pos (NN.land a b)
| Neg a, Pos b => Pos (NN.ldiff b (NN.pred a))
| Pos a, Neg b => Pos (NN.ldiff a (NN.pred b))
| Neg a, Neg b => Neg (NN.succ (NN.lor (NN.pred a) (NN.pred b)))
end.

Definition ldiff a b :=
match norm_pos a, norm_pos b with
| Pos a, Pos b => Pos (NN.ldiff a b)
| Neg a, Pos b => Neg (NN.succ (NN.lor (NN.pred a) b))
| Pos a, Neg b => Pos (NN.land a (NN.pred b))
| Neg a, Neg b => Pos (NN.ldiff (NN.pred b) (NN.pred a))
end.

Definition lxor a b :=
match norm_pos a, norm_pos b with
| Pos a, Pos b => Pos (NN.lxor a b)
| Neg a, Pos b => Neg (NN.succ (NN.lxor (NN.pred a) b))
| Pos a, Neg b => Neg (NN.succ (NN.lxor a (NN.pred b)))
| Neg a, Neg b => Pos (NN.lxor (NN.pred a) (NN.pred b))
end.

Definition div2 x := shiftr x one.

Lemma Zlnot_alt1 : forall x, -(x+1) = Z.lnot x.

Lemma Zlnot_alt2 : forall x, Z.lnot (x-1) = -x.

Lemma Zlnot_alt3 : forall x, Z.lnot (-x) = x-1.

Lemma spec_norm_pos : forall x, to_Z (norm_pos x) = to_Z x.

Lemma spec_norm_pos_pos : forall x y, norm_pos x = Neg y ->
0 < NN.to_Z y.

Ltac destr_norm_pos x :=
rewrite <- (spec_norm_pos x);
let H := fresh in
let x' := fresh x in
assert (H := spec_norm_pos_pos x);
destruct (norm_pos x) as [x'|x'];
specialize (H x' (eq_refl _)) || clear H.

Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p).

Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p).

Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p).

Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y).

Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y).

Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y).

Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y).

Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x).

End Make.