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 (N:NType) <: ZType.
Inductive t_ :=
| Pos : N.t -> t_
| Neg : N.t -> t_.
Definition t := t_.
Definition zero := Pos N.zero.
Definition one := Pos N.one.
Definition minus_one := Neg N.one.
Definition of_Z x :=
match x with
| Zpos x => Pos (N.of_N (Npos x))
| Z0 => zero
| Zneg x => Neg (N.of_N (Npos x))
end.
Definition to_Z x :=
match x with
| Pos nx => N.to_Z nx
| Neg nx => Zopp (N.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_m1: to_Z minus_one = -1.
Definition compare x y :=
match x, y with
| Pos nx, Pos ny => N.compare nx ny
| Pos nx, Neg ny =>
match N.compare nx N.zero with
| Gt => Gt
| _ => N.compare ny N.zero
end
| Neg nx, Pos ny =>
match N.compare N.zero nx with
| Lt => Lt
| _ => N.compare N.zero ny
end
| Neg nx, Neg ny => N.compare ny nx
end.
Definition lt n m := compare n m = Lt.
Definition le n m := compare n m <> Gt.
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_compare: forall x y,
match compare x y with
Eq => to_Z x = to_Z y
| Lt => to_Z x < to_Z y
| Gt => to_Z x > to_Z y
end.
Definition eq_bool x y :=
match compare x y with
| Eq => true
| _ => false
end.
Theorem spec_eq_bool: forall x y,
if eq_bool x y then to_Z x = to_Z y else to_Z x <> to_Z y.
Definition cmp_sign x y :=
match x, y with
| Pos nx, Neg ny =>
if N.eq_bool ny N.zero then Eq else Gt
| Neg nx, Pos ny =>
if N.eq_bool nx N.zero then Eq else Lt
| _, _ => Eq
end.
Theorem spec_cmp_sign: forall x y,
match cmp_sign x y with
| Gt => 0 <= to_Z x /\ to_Z y < 0
| Lt => to_Z x < 0 /\ 0 <= to_Z y
| Eq => True
end.
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) = Zabs (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 (N.succ n)
| Neg n =>
match N.compare N.zero n with
| Lt => Neg (N.pred n)
| _ => one
end
end.
Theorem spec_succ: forall n, to_Z (succ n) = to_Z n + 1.
Definition add x y :=
match x, y with
| Pos nx, Pos ny => Pos (N.add nx ny)
| Pos nx, Neg ny =>
match N.compare nx ny with
| Gt => Pos (N.sub nx ny)
| Eq => zero
| Lt => Neg (N.sub ny nx)
end
| Neg nx, Pos ny =>
match N.compare nx ny with
| Gt => Neg (N.sub nx ny)
| Eq => zero
| Lt => Pos (N.sub ny nx)
end
| Neg nx, Neg ny => Neg (N.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 N.compare N.zero nx with
| Lt => Pos (N.pred nx)
| _ => minus_one
end
| Neg nx => Neg (N.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 N.compare nx ny with
| Gt => Pos (N.sub nx ny)
| Eq => zero
| Lt => Neg (N.sub ny nx)
end
| Pos nx, Neg ny => Pos (N.add nx ny)
| Neg nx, Pos ny => Neg (N.add nx ny)
| Neg nx, Neg ny =>
match N.compare nx ny with
| Gt => Neg (N.sub nx ny)
| Eq => zero
| Lt => Pos (N.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 (N.mul nx ny)
| Pos nx, Neg ny => Neg (N.mul nx ny)
| Neg nx, Pos ny => Neg (N.mul nx ny)
| Neg nx, Neg ny => Pos (N.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 (N.square nx)
| Neg nx => Pos (N.square nx)
end.
Theorem spec_square: forall x, to_Z (square x) = to_Z x * to_Z x.
Definition power_pos x p :=
match x with
| Pos nx => Pos (N.power_pos nx p)
| Neg nx =>
match p with
| xH => x
| xO _ => Pos (N.power_pos nx p)
| xI _ => Neg (N.power_pos nx p)
end
end.
Theorem spec_power_pos: forall x n, to_Z (power_pos x n) = to_Z x ^ Zpos n.
Definition sqrt x :=
match x with
| Pos nx => Pos (N.sqrt nx)
| Neg nx => Neg N.zero
end.
Theorem spec_sqrt: forall x, 0 <= to_Z x ->
to_Z (sqrt x) ^ 2 <= to_Z x < (to_Z (sqrt x) + 1) ^ 2.
Definition div_eucl x y :=
match x, y with
| Pos nx, Pos ny =>
let (q, r) := N.div_eucl nx ny in
(Pos q, Pos r)
| Pos nx, Neg ny =>
let (q, r) := N.div_eucl nx ny in
match N.compare N.zero r with
| Eq => (Neg q, zero)
| _ => (Neg (N.succ q), Neg (N.sub ny r))
end
| Neg nx, Pos ny =>
let (q, r) := N.div_eucl nx ny in
match N.compare N.zero r with
| Eq => (Neg q, zero)
| _ => (Neg (N.succ q), Pos (N.sub ny r))
end
| Neg nx, Neg ny =>
let (q, r) := N.div_eucl nx ny in
(Pos q, Neg r)
end.
Theorem spec_div_eucl: forall x y,
to_Z y <> 0 ->
let (q,r) := div_eucl x y in
(to_Z q, to_Z r) = Zdiv_eucl (to_Z x) (to_Z y).
Definition div x y := fst (div_eucl x y).
Definition spec_div: forall x y,
to_Z y <> 0 -> to_Z (div x y) = to_Z x / to_Z y.
Qed.
Definition modulo x y := snd (div_eucl x y).
Theorem spec_modulo:
forall x y, to_Z y <> 0 -> to_Z (modulo x y) = to_Z x mod to_Z y.
Definition gcd x y :=
match x, y with
| Pos nx, Pos ny => Pos (N.gcd nx ny)
| Pos nx, Neg ny => Pos (N.gcd nx ny)
| Neg nx, Pos ny => Pos (N.gcd nx ny)
| Neg nx, Neg ny => Pos (N.gcd nx ny)
end.
Theorem spec_gcd: forall a b, to_Z (gcd a b) = Zgcd (to_Z a) (to_Z b).
End Make.