Zlogarithm.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(**********************************************************************)

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.

(*  There are three logarithms defined here,
    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 Omega Zcomplements Zpower.
Local Open Scope Z_scope.

Section Log_pos. (* Log of positive integers *)

First we build log_inf and log_sup

  Fixpoint log_inf (p:positive) : Z :=
    match p with
      | xH => 0 (* 1 *)
      | xO q => Z.succ (log_inf q)       (* 2n *)
      | xI q => Z.succ (log_inf q)       (* 2n+1 *)
    end.

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

 Hint Unfold log_inf log_sup : core.

  Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p).forall p : positive,
Z.pos (Pos.size p) = Z.succ (log_inf p)
  Proof.forall p : positive,
Z.pos (Pos.size p) = Z.succ (log_inf p)
   induction p; simpl; now rewrite ?Pos2Z.inj_succ, ?IHp.
  Qed.

  Lemma Zlog2_log_inf : forall p, Z.log2 (Zpos p) = log_inf p.forall p : positive, Z.log2 (Z.pos p) = log_inf p
  Proof.forall p : positive, Z.log2 (Z.pos p) = log_inf p
   unfold Z.log2.forall p : positive,
match p with
| (p0~1)%positive | (p0~0)%positive =>
    Z.pos (Pos.size p0)
| 1%positive => 0
end = log_inf p destruct p; simpl; trivial; apply Psize_log_inf.
  Qed.

  Lemma Zlog2_up_log_sup : forall p, Z.log2_up (Zpos p) = log_sup p.forall p : positive, Z.log2_up (Z.pos p) = log_sup p
  Proof.forall p : positive, Z.log2_up (Z.pos p) = log_sup p
   induction p; simpl log_sup.p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (Z.pos p~1) = Z.succ (Z.succ (log_inf p))
p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (Z.pos p~0) = Z.succ (log_sup p)
Z.log2_up 1 = 0
   -p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (Z.pos p~1) = Z.succ (Z.succ (log_inf p)) change (Zpos p~1) with (2*(Zpos p)+1).p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (2 * Z.pos p + 1) =
Z.succ (Z.succ (log_inf p))
     rewrite Z.log2_up_succ_double, Zlog2_log_inf; try easy.p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
2 + log_inf p = Z.succ (Z.succ (log_inf p))
     unfold Z.succ.p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
2 + log_inf p = log_inf p + 1 + 1 now rewrite !(Z.add_comm _ 1), Z.add_assoc.
   -p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (Z.pos p~0) = Z.succ (log_sup p) change (Zpos p~0) with (2*Zpos p).p:positive
IHp:Z.log2_up (Z.pos p) = log_sup p
Z.log2_up (2 * Z.pos p) = Z.succ (log_sup p)
     now rewrite Z.log2_up_double, IHp.
   -Z.log2_up 1 = 0 reflexivity.
  Qed.

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)).forall x : positive,
0 <= log_inf x /\
two_p (log_inf x) <= Z.pos x <
two_p (Z.succ (log_inf x))
  Proof.forall x : positive,
0 <= log_inf x /\
two_p (log_inf x) <= Z.pos x <
two_p (Z.succ (log_inf x))
    simple induction x; intros; simpl;
      [ elim H; intros Hp HR; clear H; split;
	[ auto with zarith
	  | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial);
	    rewrite two_p_S by trivial;
	    rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xI p);
		omega ]
	| elim H; intros Hp HR; clear H; split;
	  [ auto with zarith
	    | rewrite two_p_S with (x := Z.succ (log_inf p)) by (apply Z.le_le_succ_r; trivial);
	      rewrite two_p_S by trivial;
	      rewrite two_p_S in HR by trivial; rewrite (BinInt.Pos2Z.inj_xO p);
		  omega ]
	| unfold two_power_pos; unfold shift_pos; simpl;
	  omega ].
  Qed.

  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.forall p : positive, 0 <= log_sup p
  Proof.forall p : positive, 0 <= log_sup p
    simple induction p; intros; simpl; auto with zarith.
  Qed.

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).forall p : positive,
IF Z.pos p = two_p (log_inf p)
then Z.pos p = two_p (log_sup p)
else log_sup p = Z.succ (log_inf p)
  Proof.forall p : positive,
IF Z.pos p = two_p (log_inf p)
then Z.pos p = two_p (log_sup p)
else log_sup p = Z.succ (log_inf p)
    simple induction p; intros;
      [ elim H; right; simpl;
	rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
	  rewrite BinInt.Pos2Z.inj_xI; unfold Z.succ; omega
	| elim H; clear H; intro Hif;
	  [ left; simpl;
	    rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
	      rewrite (two_p_S (log_sup p0) (log_sup_correct1 p0));
		rewrite <- (proj1 Hif); rewrite <- (proj2 Hif);
		  auto
	    | right; simpl;
	      rewrite (two_p_S (log_inf p0) (log_inf_correct1 p0));
		rewrite BinInt.Pos2Z.inj_xO; unfold Z.succ;
		  omega ]
	| left; auto ].
  Qed.

  Theorem log_sup_correct2 :
    forall x:positive, two_p (Z.pred (log_sup x)) < Zpos x <= two_p (log_sup x).forall x : positive,
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
  Proof.forall x : positive,
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
    intro.x:positive
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
    elim (log_sup_log_inf x).x:positive
Z.pos x = two_p (log_inf x) /\
Z.pos x = two_p (log_sup x) ->
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
x:positive
Z.pos x <> two_p (log_inf x) /\
log_sup x = Z.succ (log_inf x) ->
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
    (* x is a power of two and [log_sup = log_inf] *)
    intros [E1 E2]; rewrite E2.x:positive
E1:Z.pos x = two_p (log_inf x)
E2:Z.pos x = two_p (log_sup x)
two_p (Z.pred (log_sup x)) < two_p (log_sup x) <=
two_p (log_sup x)
x:positive
Z.pos x <> two_p (log_inf x) /\
log_sup x = Z.succ (log_inf x) ->
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
    split; [ apply two_p_pred; apply log_sup_correct1 | apply Z.le_refl ].x:positive
Z.pos x <> two_p (log_inf x) /\
log_sup x = Z.succ (log_inf x) ->
two_p (Z.pred (log_sup x)) < Z.pos x <=
two_p (log_sup x)
    intros [E1 E2]; rewrite E2.x:positive
E1:Z.pos x <> two_p (log_inf x)
E2:log_sup x = Z.succ (log_inf x)
two_p (Z.pred (Z.succ (log_inf x))) < Z.pos x <=
two_p (Z.succ (log_inf x))
    rewrite (Z.pred_succ (log_inf x)).x:positive
E1:Z.pos x <> two_p (log_inf x)
E2:log_sup x = Z.succ (log_inf x)
two_p (log_inf x) < Z.pos x <=
two_p (Z.succ (log_inf x))
    generalize (log_inf_correct2 x); omega.
  Qed.

  Lemma log_inf_le_log_sup : forall p:positive, log_inf p <= log_sup p.forall p : positive, log_inf p <= log_sup p
  Proof.forall p : positive, log_inf p <= log_sup p
    simple induction p; simpl; intros; omega.
  Qed.

  Lemma log_sup_le_Slog_inf : forall p:positive, log_sup p <= Z.succ (log_inf p).forall p : positive, log_sup p <= Z.succ (log_inf p)
  Proof.forall p : positive, log_sup p <= Z.succ (log_inf p)
    simple induction p; simpl; intros; omega.
  Qed.

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.forall p : positive, 0 <= log_near p
  Proof.forall p : positive, 0 <= log_near p
    simple induction p; simpl; intros;
      [ elim p0; auto with zarith
	| elim p0; auto with zarith
	| trivial with zarith ].p, p0:positive
H:0 <= log_near p0
forall p1 : positive,
0 <=
match p1 with
| 1%positive => 2
| _ => Z.succ (log_near p1)
end -> 0 <= Z.succ (log_near p1~0)
p, p0:positive
H:0 <= log_near p0
forall p1 : positive,
0 <=
match p1 with
| 1%positive => 1
| _ => Z.succ (log_near p1)
end -> 0 <= Z.succ (log_near p1~1)
    intros; apply Z.le_le_succ_r.p, p0:positive
H:0 <= log_near p0
p1:positive
H0:0 <=
match p1 with
| 1%positive => 2
| _ => Z.succ (log_near p1)
end
0 <= log_near p1~0
p, p0:positive
H:0 <= log_near p0
forall p1 : positive,
0 <=
match p1 with
| 1%positive => 1
| _ => Z.succ (log_near p1)
end -> 0 <= Z.succ (log_near p1~1)
    generalize H0; now elim p1.p, p0:positive
H:0 <= log_near p0
forall p1 : positive,
0 <=
match p1 with
| 1%positive => 1
| _ => Z.succ (log_near p1)
end -> 0 <= Z.succ (log_near p1~1)
    intros; apply Z.le_le_succ_r.p, p0:positive
H:0 <= log_near p0
p1:positive
H0:0 <=
match p1 with
| 1%positive => 1
| _ => Z.succ (log_near p1)
end
0 <= log_near p1~1
    generalize H0; now elim p1.
  Qed.

  Theorem log_near_correct2 :
    forall p:positive, log_near p = log_inf p \/ log_near p = log_sup p.forall p : positive,
log_near p = log_inf p \/ log_near p = log_sup p
  Proof.forall p : positive,
log_near p = log_inf p \/ log_near p = log_sup p
    simple induction p.p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    intros p0 [Einf| Esup].p, p0:positive
Einf:log_near p0 = log_inf p0
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    simpl.p, p0:positive
Einf:log_near p0 = log_inf p0
match p0 with
| 1%positive => 2
| _ => Z.succ (log_near p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_near p0)
end = Z.succ (Z.succ (log_inf p0))
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1 rewrite Einf.p, p0:positive
Einf:log_near p0 = log_inf p0
match p0 with
| 1%positive => 2
| _ => Z.succ (log_inf p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_inf p0)
end = Z.succ (Z.succ (log_inf p0))
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    case p0; [ left | left | right ]; reflexivity.p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~1 = log_inf p0~1 \/
log_near p0~1 = log_sup p0~1
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    simpl; rewrite Esup.p, p0:positive
Esup:log_near p0 = log_sup p0
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    elim (log_sup_log_inf p0).p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 = two_p (log_inf p0) /\
Z.pos p0 = two_p (log_sup p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 <> two_p (log_inf p0) /\
log_sup p0 = Z.succ (log_inf p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    generalize (log_inf_le_log_sup p0).p, p0:positive
Esup:log_near p0 = log_sup p0
log_inf p0 <= log_sup p0 ->
Z.pos p0 = two_p (log_inf p0) /\
Z.pos p0 = two_p (log_sup p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 <> two_p (log_inf p0) /\
log_sup p0 = Z.succ (log_inf p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    generalize (log_sup_le_Slog_inf p0).p, p0:positive
Esup:log_near p0 = log_sup p0
log_sup p0 <= Z.succ (log_inf p0) ->
log_inf p0 <= log_sup p0 ->
Z.pos p0 = two_p (log_inf p0) /\
Z.pos p0 = two_p (log_sup p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 <> two_p (log_inf p0) /\
log_sup p0 = Z.succ (log_inf p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    case p0; auto with zarith.p, p0:positive
Esup:log_near p0 = log_sup p0
forall p1 : positive,
log_sup p1~0 <= Z.succ (log_inf p1~0) ->
log_inf p1~0 <= log_sup p1~0 ->
Z.pos p1~0 = two_p (log_inf p1~0) /\
Z.pos p1~0 = two_p (log_sup p1~0) ->
Z.succ (log_sup p1~0) = Z.succ (log_inf p1~0) \/
Z.succ (log_sup p1~0) = Z.succ (Z.succ (log_inf p1~0))
p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 <> two_p (log_inf p0) /\
log_sup p0 = Z.succ (log_inf p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    intros; omega.p, p0:positive
Esup:log_near p0 = log_sup p0
Z.pos p0 <> two_p (log_inf p0) /\
log_sup p0 = Z.succ (log_inf p0) ->
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 2
| _ => Z.succ (log_sup p0)
end = Z.succ (Z.succ (log_inf p0))
p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    case p0; intros; auto with zarith.p:positive
forall p0 : positive,
log_near p0 = log_inf p0 \/ log_near p0 = log_sup p0 ->
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    intros p0 [Einf| Esup].p, p0:positive
Einf:log_near p0 = log_inf p0
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    simpl.p, p0:positive
Einf:log_near p0 = log_inf p0
match p0 with
| 1%positive => 1
| _ => Z.succ (log_near p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 1
| _ => Z.succ (log_near p0)
end = Z.succ (log_sup p0)
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    repeat rewrite Einf.p, p0:positive
Einf:log_near p0 = log_inf p0
match p0 with
| 1%positive => 1
| _ => Z.succ (log_inf p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 1
| _ => Z.succ (log_inf p0)
end = Z.succ (log_sup p0)
p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    case p0; intros; auto with zarith.p, p0:positive
Esup:log_near p0 = log_sup p0
log_near p0~0 = log_inf p0~0 \/
log_near p0~0 = log_sup p0~0
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    simpl.p, p0:positive
Esup:log_near p0 = log_sup p0
match p0 with
| 1%positive => 1
| _ => Z.succ (log_near p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 1
| _ => Z.succ (log_near p0)
end = Z.succ (log_sup p0)
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    repeat rewrite Esup.p, p0:positive
Esup:log_near p0 = log_sup p0
match p0 with
| 1%positive => 1
| _ => Z.succ (log_sup p0)
end = Z.succ (log_inf p0) \/
match p0 with
| 1%positive => 1
| _ => Z.succ (log_sup p0)
end = Z.succ (log_sup p0)
p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    case p0; intros; auto with zarith.p:positive
log_near 1 = log_inf 1 \/ log_near 1 = log_sup 1
    auto.
  Qed.

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.forall x : Z, 0 <= N_digits x
  Proof.forall x : Z, 0 <= N_digits x
    simple induction x; simpl;
      [ apply Z.le_refl | exact log_inf_correct1 | exact log_inf_correct1 ].
  Qed.

  Lemma log_inf_shift_nat : forall n:nat, log_inf (shift_nat n 1) = Z.of_nat n.forall n : nat, log_inf (shift_nat n 1) = Z.of_nat n
  Proof.forall n : nat, log_inf (shift_nat n 1) = Z.of_nat n
    simple induction n; intros;
      [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ].
  Qed.

  Lemma log_sup_shift_nat : forall n:nat, log_sup (shift_nat n 1) = Z.of_nat n.forall n : nat, log_sup (shift_nat n 1) = Z.of_nat n
  Proof.forall n : nat, log_sup (shift_nat n 1) = Z.of_nat n
    simple induction n; intros;
      [ try trivial | rewrite Nat2Z.inj_succ; rewrite <- H; reflexivity ].
  Qed.

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).forall p : positive,
Is_power p <-> (exists y : nat, p = shift_nat y 1)
  Proof.forall p : positive,
Is_power p <-> (exists y : nat, p = shift_nat y 1)
    split;
      [ elim p;
	[ simpl; tauto
	  | simpl; intros; generalize (H H0); intro H1; elim H1;
	    intros y0 Hy0; exists (S y0); rewrite Hy0; reflexivity
	  | intro; exists 0%nat; reflexivity ]
	| intros; elim H; intros; rewrite H0; elim x; intros; simpl; trivial ].
  Qed.

  Lemma Is_power_or : forall p:positive, Is_power p \/ ~ Is_power p.forall p : positive, Is_power p \/ ~ Is_power p
  Proof.forall p : positive, Is_power p \/ ~ Is_power p
    simple induction p;
      [ intros; right; simpl; tauto
	| intros; elim H;
	  [ intros; left; simpl; exact H0
	    | intros; right; simpl; exact H0 ]
	| left; simpl; trivial ].
  Qed.

End divers.