Library Coq.ZArith.Zlogarithm
The integer logarithms with base 2.
There are three logarithms,
depending on the rounding of the real 2-based logarithm:
- Log_inf: y = (Log_inf x) iff 2^y <= x < 2^(y+1)
i.e. Log_inf x is the biggest integer that is smaller than Log x
- Log_sup: y = (Log_sup x) iff 2^(y-1) < x <= 2^y
i.e. Log_inf x is the smallest integer that is bigger than Log x
- Log_nearest: y= (Log_nearest x) iff 2^(y-1/2) < x <= 2^(y+1/2)
i.e. Log_nearest x is the integer nearest from Log x
First we build log_inf and log_sup
Then we give the specifications of log_inf and log_sup
and prove their validity
For every p, either p is a power of two and (log_inf p)=(log_sup p)
either (log_sup p)=(log_inf p)+1
Now it's possible to specify and build the Log rounded to the nearest
Number of significative digits.
Is_power p means that p is a power of two