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.
Let's include the macro-generated part. Even if we can't functorize
things (due to Eval red_t below), the rest of the module only uses
elements mentionned in interface NAbstract.
Include NMake_gen.Make W0.
Open Scope Z_scope.
Local Notation "[ x ]" := (
to_Z x).
Definition eq (
x y :
t) :=
[x] = [y].
Ltac red_t :=
match goal with |- ?
u =>
let v := (
eval red_t in u)
in change v end.
Successor
NB: it is crucial here and for the rest of this file to preserve
the let-in's. They allow to pre-compute once and for all the
field access to Z/nZ initial structures (when n=0..6).
Two
Not really pretty, but since W0 might be Z/2Z, we're not sure
there's a proper 2 there.
Division by a smaller number
Definition wn_divn1 n :=
let op :=
dom_op n in
let zd :=
ZnZ.zdigits op in
let zero := @
ZnZ.zero _ op in
let ww := @
ZnZ.WW _ op in
let head0 := @
ZnZ.head0 _ op in
let add_mul_div := @
ZnZ.add_mul_div _ op in
let div21 := @
ZnZ.div21 _ op in
let compare := @
ZnZ.compare _ op in
let sub := @
ZnZ.sub _ op in
let ddivn1 :=
DoubleDivn1.double_divn1 zd zero ww head0 add_mul_div div21 compare sub in
fun m x y =>
let (
u,
v) :=
ddivn1 (
S m)
x y in (mk_t_w' n m u, mk_t n v).
Let div_gtnm n m wx wy :=
let mn :=
Max.max n m in
let d :=
diff n m in
let op :=
make_op mn in
let (
q,
r):=
ZnZ.div_gt
(
castm (
diff_r n m) (
extend_tr wx (
snd d)))
(
castm (
diff_l n m) (
extend_tr wy (
fst d)))
in
(reduce_n mn q, reduce_n mn r).
Local Notation div_gt_folded :=
(
iter _
(
fun n =>
let div_gt :=
ZnZ.div_gt in
fun x y =>
let (
u,
v) :=
div_gt x y in (reduce n u, reduce n v))
(
fun n =>
let div_gt :=
ZnZ.div_gt in
fun m x y =>
let y' :=
DoubleBase.get_low (
zeron n) (
S m)
y in
let (
u,
v) :=
div_gt x y' in (reduce n u, reduce n v))
wn_divn1
div_gtnm).
Definition div_gt :=
Eval lazy beta iota delta
[
iter dom_op dom_t reduce zeron wn_divn1 mk_t_w' mk_t]
in
div_gt_folded.
Lemma div_gt_fold :
div_gt = div_gt_folded.
Lemma spec_get_endn:
forall n m x y,
eval n m x <= [mk_t n y] ->
[mk_t n (
DoubleBase.get_low (
zeron n)
m x)
] = eval n m x.
Let spec_divn1 n :=
DoubleDivn1.spec_double_divn1
(
ZnZ.zdigits (
dom_op n)) (
ZnZ.zero:
dom_t n)
ZnZ.WW ZnZ.head0
ZnZ.add_mul_div ZnZ.div21
ZnZ.compare ZnZ.sub ZnZ.to_Z
ZnZ.spec_to_Z
ZnZ.spec_zdigits
ZnZ.spec_0 ZnZ.spec_WW ZnZ.spec_head0
ZnZ.spec_add_mul_div ZnZ.spec_div21
ZnZ.spec_compare ZnZ.spec_sub.
Lemma spec_div_gt_aux :
forall x y,
[x] > [y] -> 0
< [y] ->
let (
q,
r) :=
div_gt x y in
[x] = [q] * [y] + [r] /\ 0
<= [r] < [y].
Theorem spec_div_gt:
forall x y,
[x] > [y] -> 0
< [y] ->
let (
q,
r) :=
div_gt x y in
[q] = [x] / [y] /\ [r] = [x] mod [y].
Modulo by a smaller number
digits
Number of digits in the representation of a numbers
(including head zero's).
NB: This function isn't a morphism for setoid
eq.
head0 and tail0
Number of zero at the beginning and at the end of
the representation of the number.
NB: these functions are not morphism for setoid
eq.
Ndigits
Same as
digits but encoded using large integers
NB: this function is not a morphism for setoid
eq.
Subtraction without underflow : p <= digits
Subtraction with underflow : digits < p
Left shift
First an unsafe version, working correctly only if
the representation is large enough
Then we define a function doubling the size of the representation
but without changing the value of the number.
Finally we iterate double_size enough before unsafe_shiftl
in order to get a fully correct shiftl.
Other bitwise operations
TODO : provide efficient versions instead of just converting
from/to N (see with Laurent)