Factor out some bedrock dependencies into WordUtil

Also move a definition about words, with a TODO about location, into WordUtil.

3 files changed, 28 insertions, 20 deletions

diff --git a/src/Util/NatUtil.v b/src/Util/NatUtil.v
index 256654df7..4ba6d0808 100644
--- a/src/Util/NatUtil.v
+++ b/src/Util/NatUtil.v
@@ -1,5 +1,4 @@
 Require Import NPeano Omega.
-Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
 
@@ -57,8 +56,3 @@ 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/WordUtil.v b/src/Util/WordUtil.v
new file mode 100644
index 000000000..49de971ef
--- /dev/null
+++ b/src/Util/WordUtil.v
@@ -0,0 +1,27 @@
+Require Import NPeano.
+Require Import ZArith.ZArith.
+Require Import Bedrock.Word.
+
+Local Open Scope nat_scope.
+
+Lemma pow2_id : forall n, pow2 n = 2 ^ n.
+Proof.
+  induction n; intros; simpl; auto.
+Qed.
+
+Lemma Zpow_pow2 : forall n, pow2 n = Z.to_nat (2 ^ (Z.of_nat n)).
+Proof.
+  induction n; intros; auto.
+  simpl pow2.
+  rewrite Nat2Z.inj_succ.
+  rewrite Z.pow_succ_r by apply Zle_0_nat.
+  rewrite untimes2.
+  rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
+  rewrite <- IHn.
+  auto.
+Qed.
+
+Definition wfirstn n {m} (w : Word.word m) {H : n <= m} : Word.word n.
+  refine (Word.split1 n (m - n) (match _ in _ = N return Word.word N with
+                            | eq_refl => w
+                            end)); abstract omega. Defined.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index ac1c47152..2cfab2e90 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -1,7 +1,6 @@
 Require Import Zpower Znumtheory ZArith.ZArith ZArith.Zdiv.
 Require Import Omega NPeano Arith.
 Require Import Crypto.Util.NatUtil.
-Require Import Bedrock.Word.
 Local Open Scope Z.
 
 Lemma gt_lt_symmetry: forall n m, n > m <-> m < n.
@@ -38,7 +37,7 @@ Proof.
   rewrite Zmod_mod; auto.
 Qed.
 
-Lemma pos_pow_nat_pos : forall x n, 
+Lemma pos_pow_nat_pos : forall x n,
   Z.pos x ^ Z.of_nat n > 0.
   do 2 (intros; induction n; subst; simpl in *; auto with zarith).
   rewrite <- Pos.add_1_r, Zpower_pos_is_exp.
@@ -53,18 +52,6 @@ Lemma Zgt0_neq0 : forall x, x > 0 -> x <> 0.
   intuition.
 Qed.
 
-Lemma Zpow_pow2 : forall n, (pow2 n)%nat = Z.to_nat (2 ^ (Z.of_nat n)).
-Proof.
-  induction n; intros; auto.
-  simpl pow2.
-  rewrite Nat2Z.inj_succ.
-  rewrite Z.pow_succ_r by apply Zle_0_nat.
-  rewrite untimes2.
-  rewrite Z2Nat.inj_mul by (try apply Z.pow_nonneg; omega).
-  rewrite <- IHn.
-  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.