Cleanup: mostly moving lemmas to Util files, some moving lemmas to more general contexts.

1 files changed, 3 insertions, 37 deletions

diff --git a/src/Encoding/ModularWordEncodingPre.v b/src/Encoding/ModularWordEncodingPre.v
index cb2f5a045..417344b43 100644
--- a/src/Encoding/ModularWordEncodingPre.v
+++ b/src/Encoding/ModularWordEncodingPre.v
@@ -3,8 +3,7 @@ Require Import Coq.Numbers.Natural.Peano.NPeano.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Bedrock.Word.
 Require Import Crypto.Tactics.VerdiTactics.
-Require Import Crypto.Util.NatUtil.
-Require Import Crypto.Util.WordUtil.
+Require Import Crypto.Util.ZUtil Crypto.Util.WordUtil.
 Require Import Crypto.Spec.Encoding.
 
 Local Open Scope nat_scope.
@@ -21,45 +20,12 @@ Section ModularWordEncodingPre.
       else None
   .
 
-  (* TODO : move to ZUtil *)
-  Lemma bound_check_N : forall x : F m, (Z.to_N x < Npow2 sz)%N.
-  Proof.
-    intro.
-    pose proof (FieldToZ_range x m_pos) as x_range.
-    rewrite <- Nnat.N2Nat.id.
-    rewrite 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 sz)).
-    rewrite Zpow_pow2.
-    destruct x_range as [x_low x_high].
-    apply Z2Nat.inj_lt in x_high; try omega.
-    rewrite <- ZUtil.pow_Z2N_Zpow by omega.
-    replace (Z.to_nat 2) with 2%nat by auto.
-    omega.
-  Qed.
-
-  (* TODO: move to WordUtil *)
-  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.
-
-  (* TODO: move to WordUtil *)
-  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 Fm_encoding_valid : forall x, Fm_dec (Fm_enc x) = Some x.
   Proof.
     unfold Fm_dec, Fm_enc; intros.
     pose proof (FieldToZ_range x m_pos).
-    rewrite wordToN_NToWord_idempotent by apply bound_check_N.
+    rewrite wordToN_NToWord_idempotent by (apply bound_check_nat_N;
+     assert (Z.to_nat x < Z.to_nat m) by (apply Z2Nat.inj_lt; omega); omega).
     rewrite Z2N.id by omega.
     rewrite ZToField_idempotent.
     break_if; auto; omega.