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

Require Import ZArith_base.
Require Import Omega.
Require Import Zcomplements.
Require Import Zpower.
Open Local Scope Z_scope.

Section Log_pos.
First we build log_inf and log_sup

Fixpoint log_inf (p:positive) : Z :=
match p with
| xH => 0
| xO q => Zsucc (log_inf q)
| xI q => Zsucc (log_inf q)
end.

Fixpoint log_sup (p:positive) : Z :=
match p with
| xH => 0
| xO n => Zsucc (log_sup n)
| xI n => Zsucc (Zsucc (log_inf n))
end.

Hint Unfold log_inf log_sup.

Then we give the specifications of log_inf and log_sup and prove their validity

Hint Resolve Zle_trans: zarith.

Theorem log_inf_correct :
forall x:positive,
0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Zsucc (log_inf x)).

Definition log_inf_correct1 (p:positive) := proj1 (log_inf_correct p).
Definition log_inf_correct2 (p:positive) := proj2 (log_inf_correct p).

Opaque log_inf_correct1 log_inf_correct2.

Hint Resolve log_inf_correct1 log_inf_correct2: zarith.

Lemma log_sup_correct1 : forall p:positive, 0 <= log_sup p.

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

Theorem log_sup_log_inf :
forall p:positive,
IF Zpos p = two_p (log_inf p) then Zpos p = two_p (log_sup p)
else log_sup p = Zsucc (log_inf p).

Theorem log_sup_correct2 :
forall x:positive, two_p (Zpred (log_sup x)) < Zpos x <= two_p (log_sup x).

Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p.

Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Zsucc (log_inf p).

Now it's possible to specify and build the Log rounded to the nearest

Fixpoint log_near (x:positive) : Z :=
match x with
| xH => 0
| xO xH => 1
| xI xH => 2
| xO y => Zsucc (log_near y)
| xI y => Zsucc (log_near y)
end.

Theorem log_near_correct1 : forall p:positive, 0 <= log_near p.

Theorem log_near_correct2 :
forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p.

End Log_pos.

Section divers.

Number of significative digits.

Definition N_digits (x:Z) :=
match x with
| Zpos p => log_inf p
| Zneg p => log_inf p
| Z0 => 0
end.

Lemma ZERO_le_N_digits : forall x:Z, 0 <= N_digits x.

Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z_of_nat n.

Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z_of_nat n.

Is_power p means that p is a power of two
Fixpoint Is_power (p:positive) : Prop :=
match p with
| xH => True
| xO q => Is_power q
| xI q => False
end.

Lemma Is_power_correct :
forall p:positive, Is_power p <-> (exists y : nat, p = shift_nat y 1).

Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p.

End divers.