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.