# Library CoLoR.Util.Nat.Log2

CoLoR, a Coq library on rewriting and termination. See the COPYRIGHTS and LICENSE files.
• Leo Ducas, 2007-08-06
Definition of log2 (floor) and exp2, and some equalities

Lemma div2_le_n : forall n, div2 n <= n.

Inductive log2_prop : nat -> nat -> Prop :=
| log2_prop_O : log2_prop 0 0
| log2_prop_1 : log2_prop 1 0
| log2_prop_p : forall p q,
p <> 0 -> p <> 1 -> log2_prop (div2 p) q -> log2_prop p (S q).

Hint Constructors log2_prop.

Fixpoint log2_aux n count : nat :=
match count with
| 0 => 0
| S count' =>
match n with
| 0 => 0
| 1 => 0
| _ => S (log2_aux (div2 n) count')
end
end.

Lemma log2_aux_matches : forall count n, n <= count ->
log2_prop n (log2_aux n count).

Definition log2 n := log2_aux n n.

Lemma log2_matches : forall n, log2_prop n (log2 n).

Lemma log2_prop_func : forall p q,
log2_prop p q -> forall q', log2_prop p q' -> q = q'.

Lemma log2_matches_log2_prop : forall n p, log2_prop n p -> p = log2 n.

Fixpoint exp2 n :=
match n with
| O => 1
| S i => 2 * exp2 i
end.

Lemma double_div2 : forall n, S (2 * div2 n) >= n.

Lemma exp2_pos : forall n, exp2 n >0.

Lemma exp2_log2_prop : forall n p, log2_prop n p -> exp2 (S p) > n.

Lemma exp2_log2 : forall n, exp2(S (log2 n)) > n.