From 46e5d165e6277d7502fe4a45e8765526a1117414 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 9 May 2019 14:23:03 +0200 Subject: 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. --- lib/Integers.v | 48 ++++++++++++++++----------------- lib/Zbits.v | 83 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ 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. *) -- cgit