merge

7 files changed, 215 insertions, 213 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 0afd6b484..fcd871aae 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -1,18 +1,18 @@
-Require Import Zpower ZArith.
-Require Import List.
+Require Import Coq.ZArith.Zpower Coq.ZArith.ZArith.
+Require Import Coq.Lists.List.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
-Require Import VerdiTactics.
+Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.ModularArithmetic.Pow2Base.
 Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.BaseSystemProofs.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
 Section ExtendedBaseVector.
-  Context `{prm : PseudoMersenneBaseParams}.
+  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).
 
   (* This section defines a new BaseVector that has double the length of the BaseVector
@@ -43,50 +43,21 @@ Section ExtendedBaseVector.
   Lemma ext_base_alt : ext_base = base ++ (map (Z.mul (2^k)) base).
   Proof.
     unfold ext_base, ext_limb_widths.
-    rewrite base_from_limb_widths_app by auto using limb_widths_pos, Z.lt_le_incl.
+    rewrite base_from_limb_widths_app by auto.
     rewrite two_p_equiv.
     reflexivity.
   Qed.
 
   Lemma ext_base_positive : forall b, In b ext_base -> b > 0.
   Proof.
-    rewrite ext_base_alt. intros b In_b_base.
-    rewrite in_app_iff in In_b_base.
-    destruct In_b_base as [In_b_base | In_b_extbase].
-    + eapply BaseSystem.base_positive.
-      eapply In_b_base.
-    + eapply in_map_iff in In_b_extbase.
-      destruct In_b_extbase as [b' [b'_2k_b  In_b'_base]].
-      subst.
-      specialize (BaseSystem.base_positive b' In_b'_base); intro base_pos.
-      replace 0 with (2 ^ k * 0) by ring.
-      apply (Zmult_gt_compat_l b' 0 (2 ^ k)); [| apply base_pos; intuition].
-      rewrite Z.gt_lt_iff.
-      apply Z.pow_pos_nonneg; intuition.
-      pose proof k_nonneg; omega.
+    apply base_positive; unfold ext_limb_widths.
+    intros ? H. apply in_app_or in H; destruct H; auto.
   Qed.
 
-  Lemma base_length_nonzero : (0 < length base)%nat.
+  Lemma b0_1 : forall x, nth_default x base 0 = 1 -> nth_default x ext_base 0 = 1.
   Proof.
-    assert (nth_default 0 base 0 = 1) by (apply BaseSystem.b0_1).
-    unfold nth_default in H.
-    case_eq (nth_error base 0); intros;
-      try (rewrite H0 in H; omega).
-    apply (nth_error_value_length _ 0 base z); auto.
-  Qed.
-
-  Lemma b0_1 : forall x, nth_default x ext_base 0 = 1.
-  Proof.
-    intros. rewrite ext_base_alt.
-    rewrite nth_default_app.
-    assert (0 < length base)%nat by (apply base_length_nonzero).
-    destruct (lt_dec 0 (length base)); try apply BaseSystem.b0_1; try omega.
-  Qed.
-
-  Lemma two_k_nonzero : 2^k <> 0.
-  Proof.
-    pose proof (Z.pow_eq_0 2 k k_nonneg).
-    intuition.
+    intros. rewrite ext_base_alt, nth_default_app.
+    destruct base; assumption.
   Qed.
 
   Lemma map_nth_default_base_high : forall n, (n < (length base))%nat ->
@@ -97,76 +68,85 @@ Section ExtendedBaseVector.
     erewrite map_nth_default; auto.
   Qed.
 
-  Lemma base_good_over_boundary : forall
-    (i : nat)
-    (l : (i < length base)%nat)
-    (j' : nat)
-    (Hj': (i + j' < length base)%nat)
-    ,
-    2 ^ k * (nth_default 0 base i * nth_default 0 base j') =
-    2 ^ k * (nth_default 0 base i * nth_default 0 base j') /
-    (2 ^ k * nth_default 0 base (i + j')) *
-    (2 ^ k * nth_default 0 base (i + j'))
-  .
-  Proof.
-    intros.
-    remember (nth_default 0 base) as b.
-    rewrite Zdiv_mult_cancel_l by (exact two_k_nonzero).
-    replace (b i * b j' / b (i + j')%nat * (2 ^ k * b (i + j')%nat))
-     with  ((2 ^ k * (b (i + j')%nat * (b i * b j' / b (i + j')%nat)))) by ring.
-    rewrite Z.mul_cancel_l by (exact two_k_nonzero).
-    replace (b (i + j')%nat * (b i * b j' / b (i + j')%nat))
-     with ((b i * b j' / b (i + j')%nat) * b (i + j')%nat) by ring.
-    subst b.
-    apply (BaseSystem.base_good i j'); omega.
-  Qed.
+  Section base_good.
+    Context (two_k_nonzero : 2^k <> 0)
+            (base_good : forall i j, (i+j < length base)%nat ->
+                                     let b := nth_default 0 base in
+                                     let r := (b i * b j) / b (i+j)%nat in
+                                     b i * b j = r * b (i+j)%nat)
+            (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).
 
-  Lemma ext_base_good :
-    forall i j, (i+j < length ext_base)%nat ->
-    let b := nth_default 0 ext_base in
-    let r := (b i * b j) / b (i+j)%nat in
-    b i * b j = r * b (i+j)%nat.
-  Proof.
-    intros.
-    subst b. subst r.
-    rewrite ext_base_alt in *.
-    rewrite app_length in H; rewrite map_length in H.
-    repeat rewrite nth_default_app.
-    repeat break_if; try omega.
-    { (* i < length base, j < length base, i + j < length base *)
-      auto using BaseSystem.base_good.
-    } { (* i < length base, j < length base, i + j >= length base *)
-      rewrite (map_nth_default _ _ _ _ 0) by omega.
-      apply (base_matches_modulus i j); rewrite <-base_length by auto using limb_widths_nonneg; omega.
-    } { (* i < length base, j >= length base, i + j >= length base *)
-      do 2 rewrite map_nth_default_base_high by omega.
-      remember (j - length base)%nat as j'.
-      replace (i + j - length base)%nat with (i + j')%nat by omega.
-      replace (nth_default 0 base i * (2 ^ k * nth_default 0 base j'))
-         with (2 ^ k * (nth_default 0 base i * nth_default 0 base j'))
-         by ring.
-      eapply base_good_over_boundary; eauto; omega.
-    } { (* i >= length base, j < length base, i + j >= length base *)
-      do 2 rewrite map_nth_default_base_high by omega.
-      remember (i - length base)%nat as i'.
-      replace (i + j - length base)%nat with (j + i')%nat by omega.
-      replace (2 ^ k * nth_default 0 base i' * nth_default 0 base j)
-         with (2 ^ k * (nth_default 0 base j * nth_default 0 base i'))
-         by ring.
-      eapply base_good_over_boundary; eauto; omega.
-    }
-  Qed.
+    Lemma base_good_over_boundary
+      : forall (i : nat)
+               (l : (i < length base)%nat)
+               (j' : nat)
+               (Hj': (i + j' < length base)%nat),
+        2 ^ k * (nth_default 0 base i * nth_default 0 base j') =
+        (2 ^ k * (nth_default 0 base i * nth_default 0 base j'))
+          / (2 ^ k * nth_default 0 base (i + j')) *
+        (2 ^ k * nth_default 0 base (i + j')).
+    Proof.
+      clear limb_widths_match_modulus.
+      intros.
+      remember (nth_default 0 base) as b.
+      rewrite Zdiv_mult_cancel_l by (exact two_k_nonzero).
+      replace (b i * b j' / b (i + j')%nat * (2 ^ k * b (i + j')%nat))
+      with  ((2 ^ k * (b (i + j')%nat * (b i * b j' / b (i + j')%nat)))) by ring.
+      rewrite Z.mul_cancel_l by (exact two_k_nonzero).
+      replace (b (i + j')%nat * (b i * b j' / b (i + j')%nat))
+      with ((b i * b j' / b (i + j')%nat) * b (i + j')%nat) by ring.
+      subst b.
+      apply (base_good i j'); omega.
+    Qed.
 
-  Instance ExtBaseVector : BaseSystem.BaseVector ext_base := {
-    base_positive := ext_base_positive;
-    b0_1 := b0_1;
-    base_good := ext_base_good
-  }.
+    Lemma ext_base_good :
+      forall i j, (i+j < length ext_base)%nat ->
+                  let b := nth_default 0 ext_base in
+                  let r := (b i * b j) / b (i+j)%nat in
+                  b i * b j = r * b (i+j)%nat.
+    Proof.
+      intros.
+      subst b. subst r.
+      rewrite ext_base_alt in *.
+      rewrite app_length in H; rewrite map_length in H.
+      repeat rewrite nth_default_app.
+      repeat break_if; try omega.
+      { (* i < length base, j < length base, i + j < length base *)
+        auto using BaseSystem.base_good.
+      } { (* i < length base, j < length base, i + j >= length base *)
+        rewrite (map_nth_default _ _ _ _ 0) by omega.
+        apply base_matches_modulus; auto using limb_widths_nonnegative, limb_widths_match_modulus;
+        distr_length.
+      } { (* i < length base, j >= length base, i + j >= length base *)
+        do 2 rewrite map_nth_default_base_high by omega.
+        remember (j - length base)%nat as j'.
+        replace (i + j - length base)%nat with (i + j')%nat by omega.
+        replace (nth_default 0 base i * (2 ^ k * nth_default 0 base j'))
+        with (2 ^ k * (nth_default 0 base i * nth_default 0 base j'))
+          by ring.
+        eapply base_good_over_boundary; eauto; omega.
+      } { (* i >= length base, j < length base, i + j >= length base *)
+        do 2 rewrite map_nth_default_base_high by omega.
+        remember (i - length base)%nat as i'.
+        replace (i + j - length base)%nat with (j + i')%nat by omega.
+        replace (2 ^ k * nth_default 0 base i' * nth_default 0 base j)
+        with (2 ^ k * (nth_default 0 base j * nth_default 0 base i'))
+          by ring.
+        eapply base_good_over_boundary; eauto; omega.
+      }
+    Qed.
+  End base_good.
 
   Lemma extended_base_length:
       length ext_base = (length base + length base)%nat.
   Proof.
-    rewrite ext_base_alt, app_length, map_length; auto.
+    clear limb_widths_nonnegative.
+    unfold ext_base, ext_limb_widths; autorewrite with distr_length; reflexivity.
   Qed.
 
   Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits),
@@ -181,6 +161,21 @@ Section ExtendedBaseVector.
     (length us <= length base)%nat ->
     BaseSystem.decode base us = BaseSystem.decode ext_base us.
   Proof. auto using decode_short_initial, firstn_us_base_ext_base. Qed.
+
+  Section BaseVector.
+    Context {bv : BaseSystem.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).
+
+    Instance ExtBaseVector : BaseSystem.BaseVector ext_base :=
+      { base_positive := ext_base_positive;
+        b0_1 x := b0_1 x (BaseSystem.b0_1 _);
+        base_good := ext_base_good (two_sum_firstn_limb_widths_nonzero limb_widths_nonnegative _) BaseSystem.base_good limb_widths_match_modulus }.
+  End BaseVector.
 End ExtendedBaseVector.
 
 Hint Rewrite @extended_base_length : distr_length.
diff --git a/src/ModularArithmetic/ModularBaseSystemList.v b/src/ModularArithmetic/ModularBaseSystemList.v
index 6a5a30429..07b2c2bac 100644
--- a/src/ModularArithmetic/ModularBaseSystemList.v
+++ b/src/ModularArithmetic/ModularBaseSystemList.v
@@ -26,7 +26,7 @@ Section Defs.
     let wrap := map (Z.mul c) high in
     BaseSystem.add low wrap.
 
-  Definition mul (us vs : digits) := reduce (BaseSystem.mul ext_base us vs).
+  Definition mul (us vs : digits) := reduce (BaseSystem.mul (ext_base limb_widths) us vs).
 
   (* In order to subtract without underflowing, we add a multiple of the modulus first. *)
   Definition sub (us vs : digits) := BaseSystem.sub (add modulus_multiple us) vs.
diff --git a/src/ModularArithmetic/ModularBaseSystemListProofs.v b/src/ModularArithmetic/ModularBaseSystemListProofs.v
index 688d45e1c..35de02cde 100644
--- a/src/ModularArithmetic/ModularBaseSystemListProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemListProofs.v
@@ -24,17 +24,17 @@ Section LengthProofs.
   Proof.
     cbv [encode encodeZ]; intros.
     rewrite encode'_spec;
-      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_length.
+      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length.
   Qed.
 
   Lemma length_reduce : forall us,
-      (length limb_widths <= length us <= length ext_base)%nat ->
+      (length limb_widths <= length us <= length (ext_base limb_widths))%nat ->
       (length (reduce us) = length limb_widths)%nat.
   Proof.
     rewrite extended_base_length.
     unfold reduce; intros.
     rewrite add_length_exact.
-    pose proof base_length.
+    pose proof (@base_from_limb_widths_length limb_widths).
     rewrite map_length, firstn_length, skipn_length, Min.min_l, Max.max_l;
       omega.
   Qed.
@@ -48,7 +48,7 @@ Section LengthProofs.
     apply length_reduce.
     destruct u; try congruence.
     + rewrite @nil_length0 in *; omega.
-    + rewrite mul_length_exact, extended_base_length, base_length; try omega.
+    + rewrite mul_length_exact, extended_base_length, base_from_limb_widths_length; try omega.
       congruence.
   Qed.
 
@@ -80,7 +80,7 @@ Section LengthProofs.
   Proof.
     intros; unfold modulus_digits, encodeZ.
     rewrite encode'_spec, encode'_length;
-      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_length.
+      auto using encode'_length, limb_widths_nonneg, Nat.eq_le_incl, base_from_limb_widths_length.
   Qed.
 
   Lemma length_conditional_subtract_modulus {u cond} :
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index c4d4ccca0..d1a6f6228 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -494,12 +494,12 @@ Section Multiplication.
     rewrite <- from_list_default_eq with (d := 0%Z).
     change (@from_list_default Z) with (@from_list_default_opt Z).
     apply f_equal.
-    rewrite ext_base_alt.
+    rewrite ext_base_alt by auto using limb_widths_pos with zarith.
     rewrite <- mul'_opt_correct.
     change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
     rewrite Z.map_shiftl by apply k_nonneg.
     rewrite c_subst.
-    rewrite k_subst.
+    fold k; rewrite k_subst.
     change @map with @map_opt.
     change @Z.shiftl_by with @Z_shiftl_by_opt.
     reflexivity.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 7d4f0107c..76a7399e3 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -59,6 +59,22 @@ Section PseudoMersenneProofs.
     pose proof (NumTheoryUtil.lt_1_p _ prime_modulus); omega.
   Qed. Hint Resolve modulus_pos.
 
+  (** TODO(jadep, from jgross): The abstraction barrier of
+      [base]/[limb_widths] is repeatedly broken in the following
+      proofs.  This lemma should almost never be needed, but removing
+      it breaks everything.  (And using [distr_length] is too much of
+      a sledgehammer, and demolishes the abstraction barrier that's
+      currently merely in pieces.) *)
+  Lemma base_length : length base = length limb_widths.
+  Proof. distr_length. Qed.
+
+  Lemma base_length_nonzero : length base <> 0%nat.
+  Proof.
+    distr_length.
+    pose proof limb_widths_nonnil.
+    destruct limb_widths; simpl in *; congruence.
+  Qed.
+
   Lemma encode_eq : forall x : F modulus,
     ModularBaseSystemList.encode x = BaseSystem.encode base x (2 ^ k).
   Proof.
@@ -87,29 +103,15 @@ Section PseudoMersenneProofs.
     f_equal; assumption.
   Qed.
 
-  Lemma firstn_us_base_ext_base : forall (us : BaseSystem.digits),
-      (length us <= length base)%nat
-      -> firstn (length us) base = firstn (length us) ext_base.
-  Proof.
-    rewrite ext_base_alt; intros.
-    rewrite firstn_app_inleft; auto; omega.
-  Qed.
-  Local Hint Immediate firstn_us_base_ext_base.
-
-  Lemma decode_short : forall (us : BaseSystem.digits),
-    (length us <= length base)%nat ->
-    BaseSystem.decode base us = BaseSystem.decode ext_base us.
-  Proof. auto using decode_short_initial. Qed.
-
-  Local Hint Immediate ExtBaseVector.
+  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 (BaseSystem.mul ext_base us vs).
+      (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;
-      autorewrite with distr_length; try omega.
+    intros; apply mul_rep_two_base; auto with arith distr_length.
   Qed.
 
   Lemma modulus_nonzero : modulus <> 0.
@@ -135,13 +137,14 @@ Section PseudoMersenneProofs.
   Qed.
 
   Lemma extended_shiftadd: forall (us : BaseSystem.digits),
-    BaseSystem.decode ext_base us =
+    BaseSystem.decode (ext_base limb_widths) us =
       BaseSystem.decode base (firstn (length base) us)
       + (2^k * BaseSystem.decode base (skipn (length base) us)).
   Proof.
     intros.
     unfold BaseSystem.decode; rewrite <- mul_each_rep.
-    rewrite ext_base_alt.
+    rewrite ext_base_alt by auto.
+    fold k.
     replace (map (Z.mul (2 ^ k)) base) with (BaseSystem.mul_each (2 ^ k) base) by auto.
     rewrite base_mul_app.
     rewrite <- mul_each_rep; auto.
@@ -149,7 +152,7 @@ Section PseudoMersenneProofs.
 
   Lemma reduce_rep : forall us,
     BaseSystem.decode base (reduce us) mod modulus =
-    BaseSystem.decode ext_base us mod modulus.
+    BaseSystem.decode (ext_base limb_widths) us mod modulus.
   Proof.
     cbv [reduce]; intros.
     rewrite extended_shiftadd, base_length, pseudomersenne_add, BaseSystemProofs.add_rep.
@@ -159,16 +162,16 @@ Section PseudoMersenneProofs.
 
   Lemma mul_rep : forall u v x y, u ~= x -> v ~= y -> mul u v ~= (x*y)%F.
   Proof.
-    autounfold; cbv [mul]; intros.
-    rewrite to_list_from_list; autounfold.
-    cbv [ModularBaseSystemList.mul].
-    rewrite ZToField_mod, reduce_rep.
-    rewrite mul_rep, <-ZToField_mod, ZToField_mul.
-    rewrite <-!decode_short; rewrite ?base_length;
-      auto using Nat.eq_le_incl, length_to_list.
-    + f_equal; assumption.
-    + apply ExtBaseVector.
-    + rewrite extended_base_length, base_length, !length_to_list. omega.
+    autounfold in *; unfold ModularBaseSystem.mul in *.
+    intuition idtac; subst.
+    rewrite to_list_from_list.
+    cbv [ModularBaseSystemList.mul ModularBaseSystemList.decode].
+    rewrite ZToField_mod, reduce_rep, <-ZToField_mod.
+    pose proof (@base_from_limb_widths_length limb_widths).
+    rewrite mul_rep by (auto using ExtBaseVector || rewrite extended_base_length, !length_to_list; omega).
+    rewrite 2decode_short by (rewrite ?base_from_limb_widths_length;
+      auto using Nat.eq_le_incl, length_to_list with omega).
+    apply ZToField_mul.
   Qed.
 
   Lemma nth_default_base_positive : forall i, (i < length base)%nat ->
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index db910ba93..78c6bba0f 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -15,22 +15,25 @@ Section Pow2BaseProofs.
 
   Lemma base_from_limb_widths_length : length base = length limb_widths.
   Proof.
-    induction limb_widths; try reflexivity.
-    simpl; rewrite map_length.
-    simpl in limb_widths_nonneg.
-    rewrite IHl; auto.
+    clear limb_widths_nonneg.
+    induction limb_widths; [ reflexivity | simpl in * ].
+    autorewrite with distr_length; auto.
   Qed.
+  Hint Rewrite base_from_limb_widths_length : distr_length.
 
   Lemma sum_firstn_limb_widths_nonneg : forall n, 0 <= sum_firstn limb_widths n.
   Proof.
     unfold sum_firstn; intros.
     apply fold_right_invariant; try omega.
-    intros y In_y_lw ? ?.
-    apply Z.add_nonneg_nonneg; try assumption.
-    apply limb_widths_nonneg.
-    eapply In_firstn; eauto.
+    eauto using Z.add_nonneg_nonneg, limb_widths_nonneg, In_firstn.
   Qed. Hint Resolve sum_firstn_limb_widths_nonneg.
 
+  Lemma two_sum_firstn_limb_widths_pos n : 0 < 2^sum_firstn limb_widths n.
+  Proof. auto with zarith. Qed.
+
+  Lemma two_sum_firstn_limb_widths_nonzero n : 2^sum_firstn limb_widths n <> 0.
+  Proof. pose proof (two_sum_firstn_limb_widths_pos n); omega. Qed.
+
   Lemma base_from_limb_widths_step : forall i b w, (S i < length base)%nat ->
     nth_error base i = Some b ->
     nth_error limb_widths i = Some w ->
@@ -162,6 +165,63 @@ Section Pow2BaseProofs.
       do 2 f_equal; apply map_ext; intros; lia. }
   Qed.
 
+  Section make_base_vector.
+    Local Notation k := (sum_firstn limb_widths (length limb_widths)).
+    Context (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)
+            (limb_widths_good : forall i j, (i + j < length limb_widths)%nat ->
+                                            sum_firstn limb_widths (i + j) <=
+                                            sum_firstn limb_widths i + sum_firstn limb_widths j).
+
+    Lemma base_matches_modulus: forall i j,
+      (i   <  length limb_widths)%nat ->
+      (j   <  length limb_widths)%nat ->
+      (i+j >= length limb_widths)%nat->
+      let b := nth_default 0 base in
+      let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
+                b i * b j = r * (2^k * b (i+j-length base)%nat).
+    Proof.
+      intros.
+      rewrite (Z.mul_comm r).
+      subst r.
+      assert (i + j - length limb_widths < length limb_widths)%nat by omega.
+      rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos;
+        subst b; rewrite ?nth_default_base; zero_bounds; rewrite ?base_from_limb_widths_length;
+        auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg).
+      rewrite (Zminus_0_l_reverse (b i * b j)) at 1.
+      f_equal.
+      subst b.
+      repeat rewrite nth_default_base by (rewrite ?base_from_limb_widths_length; auto).
+      do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
+      symmetry.
+      apply Z.mod_same_pow.
+      split.
+      + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg.
+      + rewrite base_from_limb_widths_length; auto using limb_widths_nonneg, limb_widths_match_modulus.
+    Qed.
+
+    Lemma base_good : forall i j : nat,
+                 (i + j < length base)%nat ->
+                 let b := nth_default 0 base in
+                 let r := b i * b j / b (i + j)%nat in
+                 b i * b j = r * b (i + j)%nat.
+    Proof.
+      intros; subst b r.
+      repeat rewrite nth_default_base by (omega || auto).
+      rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))).
+      rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds;
+        auto using sum_firstn_limb_widths_nonneg).
+      rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
+      rewrite Z.mod_same_pow; try ring.
+      split; [ auto using sum_firstn_limb_widths_nonneg | ].
+      apply limb_widths_good.
+      rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg.
+    Qed.
+  End make_base_vector.
 End Pow2BaseProofs.
 
 Section BitwiseDecodeEncode.
@@ -788,7 +848,7 @@ Section carrying.
   Hint Rewrite @nth_default_carry_simple using (omega || distr_length; omega) : push_nth_default.
 End carrying.
 
-Hint Rewrite @length_carry_gen : distr_length.
+Hint Rewrite @length_carry_gen @base_from_limb_widths_length : distr_length.
 Hint Rewrite @length_carry_simple @length_carry_simple_sequence @length_make_chain @length_full_carry_chain @length_carry_simple_full : distr_length.
 Hint Rewrite @nth_default_carry_simple_full @nth_default_carry_gen_full : push_nth_default.
 Hint Rewrite @nth_default_carry_simple @nth_default_carry_gen using (omega || distr_length; omega) : push_nth_default.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 50ef9df00..14482fe5e 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -14,71 +14,15 @@ Section PseudoMersenneBaseParamProofs.
   Local Notation base := (base_from_limb_widths limb_widths).
 
   Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
-  Proof.
-    intros.
-    apply Z.lt_le_incl.
-    auto using limb_widths_pos.
-  Qed. Hint Resolve limb_widths_nonneg.
+  Proof. auto using Z.lt_le_incl, limb_widths_pos. Qed.
 
   Lemma k_nonneg : 0 <= k.
-  Proof.
-    apply sum_firstn_limb_widths_nonneg; auto.
-  Qed. Hint Resolve k_nonneg.
-
-  Lemma base_matches_modulus: forall i j,
-    (i   <  length limb_widths)%nat ->
-    (j   <  length limb_widths)%nat ->
-    (i+j >= length limb_widths)%nat->
-    let b := nth_default 0 base in
-    let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
-              b i * b j = r * (2^k * b (i+j-length base)%nat).
-  Proof.
-    intros.
-    rewrite (Z.mul_comm r).
-    subst r.
-    assert (i + j - length limb_widths < length limb_widths)%nat by omega.
-    rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos;
-      subst b; rewrite ?nth_default_base; zero_bounds; rewrite ?base_from_limb_widths_length;
-      auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg).
-    rewrite (Zminus_0_l_reverse (b i * b j)) at 1.
-    f_equal.
-    subst b.
-    repeat rewrite nth_default_base by (rewrite ?base_from_limb_widths_length; auto).
-    do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
-    symmetry.
-    apply Z.mod_same_pow.
-    split.
-    + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg.
-    + rewrite base_from_limb_widths_length; auto using limb_widths_nonneg, limb_widths_match_modulus.
-  Qed.
-
-   Lemma base_good : forall i j : nat,
-                (i + j < length base)%nat ->
-                let b := nth_default 0 base in
-                let r := b i * b j / b (i + j)%nat in
-                b i * b j = r * b (i + j)%nat.
-   Proof.
-     intros; subst b r.
-     repeat rewrite nth_default_base by (omega || auto).
-     rewrite (Z.mul_comm _ (2 ^ (sum_firstn limb_widths (i+j)))).
-     rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; zero_bounds;
-       auto using sum_firstn_limb_widths_nonneg).
-     rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
-     rewrite Z.mod_same_pow; try ring.
-     split; [ auto using sum_firstn_limb_widths_nonneg | ].
-     apply limb_widths_good.
-     rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg.
-   Qed.
-
-  Lemma base_length : length base = length limb_widths.
-  Proof.
-    auto using base_from_limb_widths_length.
-  Qed.
+  Proof. apply sum_firstn_limb_widths_nonneg, limb_widths_nonneg. Qed.
 
   Global Instance bv : BaseSystem.BaseVector base := {
     base_positive := base_positive limb_widths_nonneg;
     b0_1 := fun x => b0_1 x limb_widths_nonnil;
-    base_good := base_good
+    base_good := base_good limb_widths_nonneg limb_widths_good
   }.
 
-End PseudoMersenneBaseParamProofs.
\ No newline at end of file
+End PseudoMersenneBaseParamProofs.