From cd07805915328fd5ee8d41b6cdd4d0340aa156aa Mon Sep 17 00:00:00 2001
From: jadep <jade.philipoom@gmail.com>
Date: Thu, 28 Apr 2016 13:13:08 -0400
Subject: Cleanup: mostly moving lemmas to Util files, some moving lemmas to
 more general contexts.

---
 src/Util/WordUtil.v | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)

(limited to 'src/Util/WordUtil.v')

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 17d04c60a..d655d046d 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1,5 +1,6 @@
 Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.NatUtil.
 Require Import Bedrock.Word.
 
 Local Open Scope nat_scope.
@@ -21,6 +22,30 @@ Proof.
   auto.
 Qed.
 
+Lemma wordToN_NToWord_idempotent : forall sz n, (n < Npow2 sz)%N ->
+  wordToN (NToWord sz n) = n.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat.
+  rewrite wordToNat_natToWord_idempotent; rewrite Nnat.N2Nat.id; auto.
+Qed.
+
+Lemma NToWord_wordToN : forall sz w, NToWord sz (wordToN w) = w.
+Proof.
+  intros.
+  rewrite wordToN_nat, NToWord_nat, Nnat.Nat2N.id.
+  apply natToWord_wordToNat.
+Qed.
+
+Lemma bound_check_nat_N : forall x n, (Z.to_nat x < 2 ^ n)%nat -> (Z.to_N x < Npow2 n)%N.
+Proof.
+  intros x n bound_nat.
+  rewrite <- Nnat.N2Nat.id, Npow2_nat.
+  replace (Z.to_N x) with (N.of_nat (Z.to_nat x)) by apply Z_nat_N.
+  apply (Nat2N_inj_lt _ (pow2 n)).
+  rewrite pow2_id; assumption.
+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
-- 
cgit v1.2.3