# Library Coq.Numbers.Natural.BigN.NMake

# NMake

From a cyclic Z/nZ representation to arbitrary precision natural numbers.
NB: This file contain the part which is independent from the underlying representation. The representation-dependent (and macro-generated) part is now in NMake_gen.
Require Import BigNumPrelude ZArith CyclicAxioms.
Require Import Nbasic Wf_nat StreamMemo NSig NMake_gen.
Module Make (Import W0:CyclicType) <: NType.
Macro-generated part
Include NMake_gen.Make W0.

# Predecessor

Lemma spec_pred : forall x, [ pred x ] = Zmax 0 ([ x ] -1).

# Subtraction

Lemma spec_sub : forall x y, [ sub x y ] = Zmax 0 ([ x ] - [ y ]).

# Comparison

Theorem spec_compare : forall x y, compare x y = Zcompare [ x ] [ y ].
Definition eq_bool x y :=
match compare x y with
| Eq => true
| _ => false
end.
Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [ x ] [ y ].
Theorem spec_eq_bool_aux: forall x y,
if eq_bool x y then [ x ] = [ y ] else [ x ] <> [ y ].
Definition lt n m := [ n ] < [ m ].
Definition le n m := [ n ] <= [ m ].
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_max : forall n m, [ max n m ] = Zmax [ n ] [ m ].
Theorem spec_min : forall n m, [ min n m ] = Zmin [ n ] [ m ].

# Power

Fixpoint power_pos (x:t) (p:positive) {struct p} : t :=
match p with
| xH => x
| xO p => square (power_pos x p)
| xI p => mul (square (power_pos x p)) x
end.
Theorem spec_power_pos: forall x n, [ power_pos x n ] = [ x ] ^ Zpos n.
Definition power x (n:N) := match n with
| BinNat.N0 => one
| BinNat.Npos p => power_pos x p
end.
Theorem spec_power: forall x n, [ power x n ] = [ x ] ^ Z_of_N n.

# Div

Definition div_eucl x y :=
if eq_bool y zero then ( zero , zero ) else
match compare x y with
| Eq => ( one , zero )
| Lt => ( zero , x )
| Gt => div_gt x y
end.
Theorem spec_div_eucl: forall x y,
let (q,r) := div_eucl x y in
( [ q ] , [ r ] ) = Zdiv_eucl [ x ] [ y ].
Definition div x y := fst (div_eucl x y).
Theorem spec_div:
forall x y, [ div x y ] = [ x ] / [ y ].

# Modulo

Definition modulo x y :=
if eq_bool y zero then zero else
match compare x y with
| Eq => zero
| Lt => x
| Gt => mod_gt x y
end.
Theorem spec_modulo:
forall x y, [ modulo x y ] = [ x ] mod [ y ].

# Gcd

Definition gcd_gt_body a b cont :=
match compare b zero with
| Gt =>
let r := mod_gt a b in
match compare r zero with
| Gt => cont r (mod_gt b r)
| _ => b
end
| _ => a
end.
Theorem Zspec_gcd_gt_body: forall a b cont p,
[ a ] > [ b ] -> [ a ] < 2 ^ p ->
(forall a1 b1, [ a1 ] < 2 ^ ( p - 1) -> [ a1 ] > [ b1 ] ->
Zis_gcd [ a1 ] [ b1 ] [ cont a1 b1 ]) ->
Zis_gcd [ a ] [ b ] [ gcd_gt_body a b cont ].
Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :=
gcd_gt_body a b
(fun a b =>
match p with
| xH => cont a b
| xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b
| xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b
end).
Theorem Zspec_gcd_gt_aux: forall p n a b cont,
[ a ] > [ b ] -> [ a ] < 2 ^ ( Zpos p + n ) ->
(forall a1 b1, [ a1 ] < 2 ^ n -> [ a1 ] > [ b1 ] ->
Zis_gcd [ a1 ] [ b1 ] [ cont a1 b1 ]) ->
Zis_gcd [ a ] [ b ] [ gcd_gt_aux p cont a b ].
Definition gcd_cont a b :=
match compare one b with
| Eq => one
| _ => a
end.
Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.
Theorem spec_gcd_gt: forall a b,
[ a ] > [ b ] -> [ gcd_gt a b ] = Zgcd [ a ] [ b ].
Definition gcd a b :=
match compare a b with
| Eq => a
| Lt => gcd_gt b a
| Gt => gcd_gt a b
end.
Theorem spec_gcd: forall a b, [ gcd a b ] = Zgcd [ a ] [ b ].

# Conversion

Definition of_N x :=
match x with
| BinNat.N0 => zero
| Npos p => of_pos p
end.
Theorem spec_of_N: forall x,
[ of_N x ] = Z_of_N x.

# Shift

Definition shiftr n x :=
match compare n (Ndigits x) with
| Lt => unsafe_shiftr n x
| _ => N0 w_0
end.
Theorem spec_shiftr: forall n x,
[ shiftr n x ] = [ x ] / 2 ^ [ n ].
Definition shiftl_aux_body cont n x :=
match compare n (head0 x) with
Gt => cont n (double_size x)
| _ => unsafe_shiftl n x
end.
Theorem spec_shiftl_aux_body: forall n p x cont,
2^ Zpos p <= [ head0 x ] ->
(forall x, 2 ^ ( Zpos p + 1) <= [ head0 x ]->
[ cont n x ] = [ x ] * 2 ^ [ n ]) ->
[ shiftl_aux_body cont n x ] = [ x ] * 2 ^ [ n ].
Fixpoint shiftl_aux p cont n x {struct p} :=
shiftl_aux_body
(fun n x => match p with
| xH => cont n x
| xO p => shiftl_aux p (shiftl_aux p cont) n x
| xI p => shiftl_aux p (shiftl_aux p cont) n x
end) n x.
Theorem spec_shiftl_aux: forall p q n x cont,
2 ^ ( Zpos q ) <= [ head0 x ] ->
(forall x, 2 ^ ( Zpos p + Zpos q ) <= [ head0 x ] ->
[ cont n x ] = [ x ] * 2 ^ [ n ]) ->
[ shiftl_aux p cont n x ] = [ x ] * 2 ^ [ n ].
Definition shiftl n x :=
shiftl_aux_body
(shiftl_aux_body
(shiftl_aux (digits n) unsafe_shiftl)) n x.
Theorem spec_shiftl: forall n x,
[ shiftl n x ] = [ x ] * 2 ^ [ n ].

# Zero and One

Theorem spec_0: [ zero ] = 0.
Theorem spec_1: [ one ] = 1.
End Make.