From f86e6618b62769b1c3e78175f95f882d3960d54b Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Sat, 8 Jun 2019 18:17:13 +0200
Subject: More lemmas about powers of 2

---
 lib/Zbits.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

(limited to 'lib/Zbits.v')

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.
-- 
cgit