Library Coq.ZArith.Zlogarithm

The integer logarithms with base 2.

THIS FILE IS DEPRECATED. Please rather use Z.log2 (or Z.log2_up), which are defined in BinIntDef, and whose properties can be found in BinInt.Z.

Require Import ZArith_base Omega Zcomplements Zpower.
Local Open 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 => Z.succ (log_inf q)
      | xI q => Z.succ (log_inf q)
    end.

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

  Hint Unfold log_inf log_sup.

  Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p).

  Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p.

  Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p.

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

  Hint Resolve Z.le_trans: zarith.

  Theorem log_inf_correct :
    forall x:positive,
      0 <= log_inf x /\ two_p (log_inf x) <= Zpos x < two_p (Z.succ (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 = Z.succ (log_inf p).

  Theorem log_sup_correct2 :
    forall x:positive, two_p (Z.pred (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 <= Z.succ (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 => Z.succ (log_near y)
      | xI y => Z.succ (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.