Remove stuff from PseudoMersenneBaseParamProofs.v

4 files changed, 92 insertions, 84 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index e2fcab9a0..1c9555fe6 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -63,7 +63,7 @@ Section ExtendedBaseVector.
       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 sum_firstn_limb_widths_nonneg; auto using limb_widths_nonneg.
   Qed.
 
   Lemma base_length_nonzero : (0 < length base)%nat.
@@ -105,10 +105,10 @@ Section ExtendedBaseVector.
   Proof.
     intros.
     remember (nth_default 0 base) as b.
-    rewrite Zdiv_mult_cancel_l by (exact two_k_nonzero).
+    rewrite Zdiv_mult_cancel_l by apply two_sum_firstn_limb_widths_nonzero, limb_widths_nonneg.
     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).
+    rewrite Z.mul_cancel_l by apply two_sum_firstn_limb_widths_nonzero, limb_widths_nonneg.
     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.
@@ -131,7 +131,9 @@ Section ExtendedBaseVector.
       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.
+      autorewrite with distr_length in * |- .
+      apply base_matches_modulus; auto using limb_widths_nonneg, limb_widths_match_modulus.
+      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'.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 5d1becc00..c3b1b76b4 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -57,6 +57,15 @@ 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 encode'_eq : forall (x : F modulus) i, (i <= length limb_widths)%nat ->
     encode' limb_widths x i = BaseSystem.encode' base x (2 ^ k) i.
   Proof.
@@ -99,7 +108,7 @@ Section PseudoMersenneProofs.
         match goal with H : (_ <= length base)%nat |- _ =>
           apply le_lt_or_eq in H; destruct H end.
         - apply Z.mod_divide.
-          * apply nth_default_base_nonzero; auto using bv, two_k_nonzero.
+          * apply nth_default_base_nonzero, two_sum_firstn_limb_widths_nonzero; auto using bv.
           * rewrite !nth_default_eq.
             do 2 (erewrite nth_indep with (d := 2 ^ k) (d' := 0) by omega).
             rewrite <-!nth_default_eq.
@@ -150,7 +159,7 @@ Section PseudoMersenneProofs.
       (BaseSystem.decode base us) * (BaseSystem.decode base vs) = BaseSystem.decode ext_base (BaseSystem.mul ext_base us vs).
   Proof.
     intros; apply mul_rep_two_base; auto;
-      autorewrite with distr_length; try omega.
+      distr_length.
   Qed.
 
   Lemma modulus_nonzero : modulus <> 0.
@@ -396,7 +405,7 @@ Section CarryProofs.
   Proof.
     pose proof length_carry. pose proof carry_decode_eq_reduce. pose proof (@carry_simple_decode_eq limb_widths).
     specialize_by eauto.
-    intros; split; auto.
+    intros; split; try solve [ distr_length ].
     unfold rep, decode, carry in *.
     intuition; break_if; subst; eauto; apply F_eq; simpl; intuition.
   Qed.
@@ -412,7 +421,7 @@ Section CarryProofs.
   Lemma carry_sequence_length: forall is us,
     (length us = length base)%nat ->
     (length (carry_sequence is us) = length base)%nat.
-  Proof. intros; autorewrite with distr_length; congruence. Qed.
+  Proof. intros; distr_length. Qed.
   Hint Resolve carry_sequence_length.
 
   Lemma carry_sequence_rep : forall is us x,
@@ -432,7 +441,7 @@ Section CarryProofs.
 
   Lemma carry_full_length : forall us, (length us = length base)%nat ->
     length (carry_full us) = length base.
-  Proof. intros; autorewrite with distr_length; congruence. Qed.
+  Proof. intros; distr_length. Qed.
 
   Lemma carry_full_preserves_rep : forall us x,
     rep us x -> rep (carry_full us) x.
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index ca28896dd..d95de5bd1 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,8 +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.
-Hint Rewrite @base_from_limb_widths_length using auto with nocore distr_length : distr_length.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 1cb87910d..14482fe5e 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -14,77 +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 two_k_nonzero : 2^k <> 0.
-  Proof.
-    pose proof (Z.pow_eq_0 2 k k_nonneg).
-    intuition.
-  Qed.
-
-  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.