a few lemmas in util about powers of 2 in Bedrock's various rewritten forms

2 files changed, 19 insertions, 0 deletions

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index afed2a231..256654df7 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,4 +1,7 @@
 Require Import NPeano Omega.
+Require Import Bedrock.Word.
+
+Local Open Scope nat_scope.
 
 Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
 Proof.
@@ -54,3 +57,8 @@ Proof.
     rewrite <- nat_compare_lt; auto.
   }
 Qed.
+
+Lemma pow2_id : forall n, pow2 n = 2 ^ n.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index 1c3efbdac..ac1c47152 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -65,6 +65,17 @@ Proof.
   auto.
 Qed.
 
+Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
+  ((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
+Proof.
+  intros; induction n; try reflexivity.
+  rewrite Nat2Z.inj_succ.
+  rewrite pow_succ_r by apply le_0_n.
+  rewrite Z.pow_succ_r by apply Zle_0_nat.
+  rewrite IHn.
+  rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
+Qed.
+
 Lemma mod_exp_0 : forall a x m, x > 0 -> m > 1 -> a mod m = 0 ->
   a ^ x mod m = 0.
 Proof.