Move mul_rep_extended (do we actually care about this?)

2 files changed, 34 insertions, 8 deletions

diff --git a/src/ModularArithmetic/ExtPow2BaseMulProofs.v b/src/ModularArithmetic/ExtPow2BaseMulProofs.v
new file mode 100644
index 000000000..af2c1a679
--- /dev/null
+++ b/src/ModularArithmetic/ExtPow2BaseMulProofs.v
@@ -0,0 +1,34 @@
+Require Import Coq.ZArith.ZArith Coq.Lists.List.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.BaseSystemProofs.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.Util.ListUtil.
+
+Local Open Scope Z_scope.
+
+Section ext_mul.
+  Context (limb_widths : list Z)
+          (limb_widths_nonnegative : forall x, In x limb_widths -> 0 <= x).
+  Local Notation k := (sum_firstn limb_widths (length limb_widths)).
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Context (bv : BaseVector base)
+          (limb_widths_match_modulus : forall i j,
+              (i < length limb_widths)%nat ->
+              (j < length limb_widths)%nat ->
+              (i + j >= length limb_widths)%nat ->
+              let w_sum := sum_firstn limb_widths in
+              k + w_sum (i + j - length limb_widths)%nat <= w_sum i + w_sum j).
+
+  Local Hint Resolve firstn_us_base_ext_base ExtBaseVector bv.
+
+  Lemma mul_rep_extended : forall (us vs : BaseSystem.digits),
+      (length us <= length base)%nat ->
+      (length vs <= length base)%nat ->
+      (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs).
+  Proof.
+    intros; apply mul_rep_two_base; auto;
+      distr_length.
+  Qed.
+End ext_mul.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index e74051319..b815167e2 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -147,14 +147,6 @@ Section PseudoMersenneProofs.
   Local Hint Resolve firstn_us_base_ext_base bv ExtBaseVector limb_widths_match_modulus.
   Local Hint Extern 1 => apply limb_widths_match_modulus.
 
-  Lemma mul_rep_extended : forall (us vs : BaseSystem.digits),
-      (length us <= length base)%nat ->
-      (length vs <= length base)%nat ->
-      (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode (ext_base limb_widths) (BaseSystem.mul (ext_base limb_widths) us vs).
-  Proof.
-    intros; apply mul_rep_two_base; auto with arith distr_length.
-  Qed.
-
   Lemma modulus_nonzero : modulus <> 0.
     pose proof (Znumtheory.prime_ge_2 _ prime_modulus); omega.
   Qed.