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