Add mul_split_at_bitwidth, define things in terms of that

This will make it easier on the reflective machinery, because it won't
have to carry around such large constants.

1 files changed, 14 insertions, 2 deletions

diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v
index e0448fe69..2f6805446 100644
--- a/src/Util/ZUtil/MulSplit.v
+++ b/src/Util/ZUtil/MulSplit.v
@@ -1,10 +1,22 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Util.ZUtil.Definitions.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.Tactics.BreakMatch.
 Local Open Scope Z_scope.
 
 Module Z.
-  Lemma mul_split_mod s x y : fst (Z.mul_split s x y)  = (x * y) mod s.
+  Lemma mul_split_at_bitwidth_mod bw x y : fst (Z.mul_split_at_bitwidth bw x y)  = (x * y) mod 2^bw.
   Proof. reflexivity. Qed.
-  Lemma mul_split_div s x y : snd (Z.mul_split s x y)  = (x * y) / s.
+  Lemma mul_split_at_bitwidth_div bw x y : snd (Z.mul_split_at_bitwidth bw x y)  = (x * y) / 2^bw.
   Proof. reflexivity. Qed.
+  Lemma mul_split_mod s x y : fst (Z.mul_split s x y)  = (x * y) mod s.
+  Proof.
+    unfold Z.mul_split; break_match; Z.ltb_to_lt;
+      [ rewrite mul_split_at_bitwidth_mod; congruence | reflexivity ].
+  Qed.
+  Lemma mul_split_div s x y : snd (Z.mul_split s x y)  = (x * y) / s.
+  Proof.
+    unfold Z.mul_split; break_match; Z.ltb_to_lt;
+      [ rewrite mul_split_at_bitwidth_div; congruence | reflexivity ].
+  Qed.
 End Z.