More efficient test for powers of two

The previous implementation used to build the full powers-of-two decomposition
of the number.  The present implementation recognizes powers of two directly,
then takes the log2.

2 files changed, 105 insertions, 26 deletions

diff --git a/lib/Integers.v b/lib/Integers.v
index 8f528079..f4213332 100644
--- a/lib/Integers.v
+++ b/lib/Integers.v
@@ -268,9 +268,9 @@ Definition one_bits (x: int) : list int :=
 (** Recognition of powers of two. *)
 
 Definition is_power2 (x: int) : option int :=
-  match Z_one_bits wordsize (unsigned x) 0 with
-  | i :: nil => Some (repr i)
-  | _ => None
+  match Z_is_power2 (unsigned x) with
+  | Some i => Some (repr i)
+  | None => None
   end.
 
 (** Comparisons. *)
@@ -2146,21 +2146,27 @@ Qed.
 
 (** ** Properties of [is_power2]. *)
 
+Remark is_power2_inv:
+  forall n logn,
+  is_power2 n = Some logn ->
+  Z_is_power2 (unsigned n) = Some (unsigned logn) /\ 0 <= unsigned logn < zwordsize.
+Proof.
+  unfold is_power2; intros.
+  destruct (Z_is_power2 (unsigned n)) as [i|] eqn:E; inv H.
+  assert (0 <= i < zwordsize).
+  { apply Z_is_power2_range with (unsigned n). 
+    generalize wordsize_pos; omega.
+    rewrite <- modulus_power. apply unsigned_range.
+    auto. }
+  rewrite unsigned_repr; auto. generalize wordsize_max_unsigned; omega.
+Qed.
+
 Lemma is_power2_rng:
   forall n logn,
   is_power2 n = Some logn ->
   0 <= unsigned logn < zwordsize.
 Proof.
-  intros n logn. unfold is_power2.
-  generalize (Z_one_bits_range wordsize (unsigned n)).
-  destruct (Z_one_bits wordsize (unsigned n) 0).
-  intros; discriminate.
-  destruct l.
-  intros. injection H0; intro; subst logn; clear H0.
-  assert (0 <= z < zwordsize).
-  apply H. auto with coqlib.
-  rewrite unsigned_repr. auto. generalize wordsize_max_unsigned; omega.
-  intros; discriminate.
+  intros. apply (is_power2_inv n logn); auto.
 Qed.
 
 Theorem is_power2_range:
@@ -2176,18 +2182,8 @@ Lemma is_power2_correct:
   is_power2 n = Some logn ->
   unsigned n = two_p (unsigned logn).
 Proof.
-  intros n logn. unfold is_power2.
-  generalize (Z_one_bits_powerserie wordsize (unsigned n) (unsigned_range n)).
-  generalize (Z_one_bits_range wordsize (unsigned n)).
-  destruct (Z_one_bits wordsize (unsigned n) 0).
-  intros; discriminate.
-  destruct l.
-  intros. simpl in H0. injection H1; intros; subst logn; clear H1.
-  rewrite unsigned_repr. replace (two_p z) with (two_p z + 0).
-  auto. omega. elim (H z); change (Z.of_nat wordsize) with zwordsize; intros.
-  generalize wordsize_max_unsigned; omega.
-  auto with coqlib.
-  intros; discriminate.
+  intros. apply is_power2_inv in H. destruct H as [P Q].
+  apply Z_is_power2_sound in P. tauto.
 Qed.
 
 Remark two_p_range:
@@ -2207,7 +2203,7 @@ Lemma is_power2_two_p:
   is_power2 (repr (two_p n)) = Some (repr n).
 Proof.
   intros. unfold is_power2. rewrite unsigned_repr.
-  rewrite Z_one_bits_two_p. auto. auto.
+  rewrite Z_is_power2_complete by omega; auto.
   apply two_p_range. auto.
 Qed.
 
diff --git a/lib/Zbits.v b/lib/Zbits.v
index 74f66b6e..dca2a5a2 100644
--- a/lib/Zbits.v
+++ b/lib/Zbits.v
@@ -796,6 +796,89 @@ Proof.
   rewrite IHn. f_equal; omega. omega.
 Qed.
 
+(** ** Recognition of powers of two *)
+
+Fixpoint P_is_power2 (p: positive) : bool :=
+  match p with
+  | xH => true
+  | xO q => P_is_power2 q
+  | xI q => false
+  end.
+
+Definition Z_is_power2 (x: Z) : option Z :=
+  match x with
+  | Z0 => None
+  | Zpos p => if P_is_power2 p then Some (Z.log2 x) else None
+  | Zneg _ => None
+  end.
+
+Remark P_is_power2_sound:
+  forall p, P_is_power2 p = true -> Z.pos p = two_p (Z.log2 (Z.pos p)).
+Proof.
+  induction p; simpl P_is_power2; intros.
+- discriminate.
+- change (Z.pos p~0) with (2 * Z.pos p).  apply IHp in H.
+  rewrite Z.log2_double by xomega. rewrite two_p_S.  congruence.
+  apply Z.log2_nonneg.
+- reflexivity.
+Qed.
+ 
+Lemma Z_is_power2_sound:
+  forall x i, Z_is_power2 x = Some i -> x = two_p i /\ i = Z.log2 x.
+Proof.
+  unfold Z_is_power2; intros. destruct x; try discriminate.
+  destruct (P_is_power2 p) eqn:P; try discriminate.
+  apply P_is_power2_sound in P. rewrite P; split; congruence.
+Qed.
+
+Corollary Z_is_power2_range:
+  forall n x i,
+  0 <= n -> 0 <= x < two_p n -> Z_is_power2 x = Some i -> 0 <= i < n.
+Proof.
+  intros.
+  assert (x <> 0) by (red; intros; subst x; discriminate).
+  apply Z_is_power2_sound in H1. destruct H1 as [P Q]. subst i.
+  split. apply Z.log2_nonneg. apply Z.log2_lt_pow2. omega. rewrite <- two_p_equiv; tauto.
+Qed.
+
+Lemma Z_is_power2_complete:
+  forall i, 0 <= i -> Z_is_power2 (two_p i) = Some i.
+Proof.
+Opaque Z.log2.
+  assert (A: forall x i, Z_is_power2 x = Some i -> Z_is_power2 (2 * x) = Some (Z.succ i)).
+  { destruct x; simpl; intros; try discriminate.
+    change (2 * Z.pos p) with (Z.pos (xO p)); simpl.
+    destruct (P_is_power2 p); inv H. rewrite <- Z.log2_double by xomega. auto.
+  }
+  induction i using Znatlike_ind; intros.
+- replace i with 0 by omega. reflexivity.
+- rewrite two_p_S by omega. apply A. apply IHi; omega.
+Qed.
+
+Definition Z_is_power2m1 (x: Z) : option Z := Z_is_power2 (Z.succ x).
+
+Lemma Z_is_power2m1_sound:
+  forall x i, Z_is_power2m1 x = Some i -> x = two_p i - 1.
+Proof.
+  unfold Z_is_power2m1; intros. apply Z_is_power2_sound in H. omega.
+Qed.
+
+Lemma Z_is_power2m1_complete:
+  forall i, 0 <= i -> Z_is_power2m1 (two_p i - 1) = Some i.
+Proof.
+  intros. unfold Z_is_power2m1. replace (Z.succ (two_p i - 1)) with (two_p i) by omega.
+  apply Z_is_power2_complete; auto.
+Qed.
+
+Lemma Z_is_power2m1_range:
+  forall n x i,
+  0 <= n -> 0 <= x < two_p n -> Z_is_power2m1 x = Some i -> 0 <= i <= n.
+Proof.
+  intros. destruct (zeq x (two_p n - 1)).
+- subst x. rewrite Z_is_power2m1_complete in H1 by auto. inv H1; omega.
+- unfold Z_is_power2m1 in H1. apply (Z_is_power2_range n (Z.succ x) i) in H1; omega.
+Qed.
+
 (** ** Relation between bitwise operations and multiplications / divisions by powers of 2 *)
 
 (** Left shifts and multiplications by powers of 2. *)