Peano natural numbers, definitions of operations
This file is meant to be used as a whole module,
without importing it, leading to qualified definitions
(e.g. Nat.pred)
Euclidean division
This division is linear and tail-recursive.
In
divmod,
y is the predecessor of the actual divisor,
and
u is
y minus the real remainder
Greatest common divisor
We use Euclid algorithm, which is normally not structural,
but Coq is now clever enough to accept this (behind modulo
there is a subtraction, which now preserves being a subterm)
Square root
The following square root function is linear (and tail-recursive).
With Peano representation, we can't do better. For faster algorithm,
see Psqrt/Zsqrt/Nsqrt...
We search the square root of n = k + p^2 + (q - r)
with q = 2p and 0<=r<=q. We start with p=q=r=0, hence
looking for the square root of n = k. Then we progressively
decrease k and r. When k = S k' and r=0, it means we can use (S p)
as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2.
When k reaches 0, we have found the biggest p^2 square contained
in n, hence the square root of n is p.
Log2
This base-2 logarithm is linear and tail-recursive.
In
log2_iter, we maintain the logarithm
p of the counter
q,
while
r is the distance between
q and the next power of 2,
more precisely
q + S r = 2^(S p) and
r<2^p. At each
recursive call,
q goes up while
r goes down. When
r
is 0, we know that
q has almost reached a power of 2,
and we increase
p at the next call, while resetting
r
to
q.
Graphically (numbers are
q, stars are
r) :
10
9
8
7 *
6 *
5 ...
4
3 *
2 *
1 * *
0 * * *
We stop when
k, the global downward counter reaches 0.
At that moment,
q is the number we're considering (since
k+q is invariant), and
p its logarithm.
Bitwise operations
We provide here some bitwise operations for unary numbers.
Some might be really naive, they are just there for fulfilling
the same interface as other for natural representations. As
soon as binary representations such as NArith are available,
it is clearly better to convert to/from them and use their ops.