Unfold Z.mul_split_at_bitwidth for reification

Also reimplement it with a shift and a mask

1 files changed, 9 insertions, 2 deletions

diff --git a/src/Util/ZUtil/MulSplit.v b/src/Util/ZUtil/MulSplit.v
index 2f6805446..1cc6b7af0 100644
--- a/src/Util/ZUtil/MulSplit.v
+++ b/src/Util/ZUtil/MulSplit.v
@@ -1,4 +1,5 @@
 Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
 Require Import Crypto.Util.ZUtil.Definitions.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.BreakMatch.
@@ -6,9 +7,15 @@ Local Open Scope Z_scope.
 
 Module Z.
   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.
+  Proof.
+    unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
+      apply Z.land_ones; lia.
+  Qed.
   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.
+  Proof.
+    unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
+      apply Z.shiftr_div_pow2; lia.
+  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;