diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-06-08 18:17:13 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-08-07 10:38:34 +0200 |
| commit | f86e6618b62769b1c3e78175f95f882d3960d54b (patch) | |
| tree | a08bf40723ef19d1855fad27dfe575bfaa21bd8d | |
| parent | dd243f5f35200aa9fdcc400300990192ed4bc0b6 (diff) | |
| download | compcert-f86e6618b62769b1c3e78175f95f882d3960d54b.tar.gz compcert-f86e6618b62769b1c3e78175f95f882d3960d54b.zip | |
More lemmas about powers of 2
| -rw-r--r-- | lib/Zbits.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/lib/Zbits.v b/lib/Zbits.v index fb40ccb5..27586aff 100644 --- a/lib/Zbits.v +++ b/lib/Zbits.v @@ -824,6 +824,14 @@ Proof. apply Z.log2_nonneg. - reflexivity. Qed. + +Lemma Z_is_power2_nonneg: + forall x i, Z_is_power2 x = Some i -> 0 <= i. +Proof. + unfold Z_is_power2; intros. destruct x; try discriminate. + destruct (P_is_power2 p) eqn:P; try discriminate. + replace i with (Z.log2 (Z.pos p)) by congruence. apply Z.log2_nonneg. +Qed. Lemma Z_is_power2_sound: forall x i, Z_is_power2 x = Some i -> x = two_p i /\ i = Z.log2 x. @@ -859,6 +867,12 @@ Qed. Definition Z_is_power2m1 (x: Z) : option Z := Z_is_power2 (Z.succ x). +Lemma Z_is_power2m1_nonneg: + forall x i, Z_is_power2m1 x = Some i -> 0 <= i. +Proof. + unfold Z_is_power2m1; intros. eapply Z_is_power2_nonneg; eauto. +Qed. + Lemma Z_is_power2m1_sound: forall x i, Z_is_power2m1 x = Some i -> x = two_p i - 1. Proof. |