Split off notation and defs in ZUtil

4 files changed, 19 insertions, 10 deletions

diff --git a/src/Util/WordUtil.v b/src/Util/WordUtil.v
index 4b19d5f8b..c8aa9a4e5 100644
--- a/src/Util/WordUtil.v
+++ b/src/Util/WordUtil.v
@@ -1307,9 +1307,9 @@ Qed.
 
 (* TODO : automate *)
 Lemma WordNZ_split1 : forall {n m} w,
-    Z.of_N (Word.wordToN (Word.split1 n m w)) = ZUtil.Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n).
+    Z.of_N (Word.wordToN (Word.split1 n m w)) = Z.pow2_mod (Z.of_N (Word.wordToN w)) (Z.of_nat n).
 Proof.
-  intros; unfold ZUtil.Z.pow2_mod.
+  intros; unfold Z.pow2_mod.
   rewrite wordToN_split1.
   apply Z.bits_inj_iff'; intros k Hpos.
   rewrite Z.land_spec.
@@ -1338,7 +1338,7 @@ Qed.
 Lemma WordNZ_split2 : forall {n m} w,
     Z.of_N (Word.wordToN (Word.split2 n m w)) = Z.shiftr (Z.of_N (Word.wordToN w)) (Z.of_nat n).
 Proof.
-  intros; unfold ZUtil.Z.pow2_mod.
+  intros; unfold Z.pow2_mod.
   rewrite wordToN_split2.
   apply Z.bits_inj_iff'; intros k Hpos.
   rewrite Z2N.inj_testbit; [|assumption].
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index bb19e6170..8e3d34ce4 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -11,13 +11,11 @@ Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Notations.
 Require Import Coq.Lists.List.
 Require Export Crypto.Util.FixCoqMistakes.
+Require Export Crypto.Util.ZUtil.Notations.
+Require Export Crypto.Util.ZUtil.Definitions.
 Import Nat.
 Local Open Scope Z.
 
-Infix ">>" := Z.shiftr : Z_scope.
-Infix "<<" := Z.shiftl : Z_scope.
-Infix "&'" := Z.land : Z_scope.
-
 Hint Extern 1 => lia : lia.
 Hint Extern 1 => lra : lra.
 Hint Extern 1 => nia : nia.
@@ -332,8 +330,6 @@ Module Z.
     end.
   Ltac peel_le := repeat peel_le_step.
 
-  Definition pow2_mod n i := (n &' (Z.ones i)).
-
   Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b).
   Proof.
     intros.
@@ -387,7 +383,7 @@ Module Z.
                                      else if Z_lt_dec i n then Z.testbit a i else false.
   Proof.
     intros; destruct (Z_lt_dec n 0); [ | apply testbit_pow2_mod; omega ].
-    unfold pow2_mod.
+    unfold Z.pow2_mod.
     autorewrite with Ztestbit_full;
       repeat break_match;
       autorewrite with Ztestbit;
diff --git a/src/Util/ZUtil/Definitions.v b/src/Util/ZUtil/Definitions.v
new file mode 100644
index 000000000..2753f5ff8
--- /dev/null
+++ b/src/Util/ZUtil/Definitions.v
@@ -0,0 +1,7 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.Notations.
+Local Open Scope Z_scope.
+
+Module Z.
+  Definition pow2_mod n i := (n &' (Z.ones i)).
+End Z.
diff --git a/src/Util/ZUtil/Notations.v b/src/Util/ZUtil/Notations.v
new file mode 100644
index 000000000..9a0743524
--- /dev/null
+++ b/src/Util/ZUtil/Notations.v
@@ -0,0 +1,6 @@
+Require Import Coq.ZArith.BinInt.
+Require Import Crypto.Util.Notations.
+
+Infix ">>" := Z.shiftr : Z_scope.
+Infix "<<" := Z.shiftl : Z_scope.
+Infix "&'" := Z.land : Z_scope.