Merge pull request #21 from JasonGross/base-log-cap-notations

Make [base] and [log_cap] notations

7 files changed, 96 insertions, 85 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 9ed7d065e..2a06d9c41 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -9,6 +9,7 @@ Local Open Scope Z_scope.
 
 Section ExtendedBaseVector.
   Context `{prm : PseudoMersenneBaseParams}.
+  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
 
   (* This section defines a new BaseVector that has double the length of the BaseVector
   * used to construct [params]. The coefficients of the new vector are as follows:
@@ -159,4 +160,3 @@ Section ExtendedBaseVector.
     unfold ext_base; rewrite app_length; rewrite map_length; auto.
   Qed.
 End ExtendedBaseVector.
-
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 856cb1e81..8ce395289 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -4,7 +4,6 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import Crypto.BaseSystem.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
 Require Import Crypto.Tactics.VerdiTactics.
 Require Import Crypto.Util.Notations.
@@ -13,6 +12,7 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
   Context `{prm :PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
 
@@ -39,22 +39,20 @@ End PseudoMersenneBase.
 
 Section CarryBasePow2.
   Context `{prm :PseudoMersenneBaseParams}.
-
-  Definition log_cap i := nth_default 0 limb_widths i.
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
 
   Definition add_to_nth n (x:Z) xs :=
     set_nth n (x + nth_default 0 xs n) xs.
 
-  Definition pow2_mod n i := Z.land n (Z.ones i).
-
   Definition carry_simple i := fun us =>
     let di := nth_default 0 us      i in
-    let us' := set_nth i (pow2_mod di (log_cap i)) us in
+    let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in
     add_to_nth (S i) (   (Z.shiftr di (log_cap i))) us'.
 
   Definition carry_and_reduce i := fun us =>
     let di := nth_default 0 us      i in
-    let us' := set_nth i (pow2_mod di (log_cap i)) us in
+    let us' := set_nth i (Z.pow2_mod di (log_cap i)) us in
     add_to_nth   0  (c * (Z.shiftr di (log_cap i))) us'.
 
   Definition carry i : digits -> digits :=
@@ -80,6 +78,8 @@ End CarryBasePow2.
 
 Section Canonicalization.
   Context `{prm :PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
 
   (* compute at compile time *)
   Definition max_ones := Z.ones (fold_right Z.max 0 limb_widths).
diff --git a/src/ModularArithmetic/ModularBaseSystemInterface.v b/src/ModularArithmetic/ModularBaseSystemInterface.v
index e4192428e..4a3859077 100644
--- a/src/ModularArithmetic/ModularBaseSystemInterface.v
+++ b/src/ModularArithmetic/ModularBaseSystemInterface.v
@@ -13,8 +13,9 @@ Generalizable All Variables.
 Section s.
   Context `{prm:PseudoMersenneBaseParams m} {sc : SubtractionCoefficient m prm}.
   Context {k_ c_} (pfk : k = k_) (pfc:c = c_).
+  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
 
-  Definition fe := tuple Z (length PseudoMersenneBaseParamProofs.base).
+  Definition fe := tuple Z (length base).
 
   Definition mul  (x y:fe) : fe :=
     carry_mul_opt_cps k_ c_ (from_list_default 0%Z (length base))
@@ -86,4 +87,4 @@ Section s.
     apply carry_mul_rep; auto using decode_rep, length_to_list.
   Qed.
 
-End s.
\ No newline at end of file
+End s.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 332c0cdb2..f7d33a97b 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -14,8 +14,8 @@ Local Open Scope Z.
 
 Class SubtractionCoefficient (m : Z) (prm : PseudoMersenneBaseParams m) := {
   coeff : BaseSystem.digits;
-  coeff_length : (length coeff = length PseudoMersenneBaseParamProofs.base)%nat;
-  coeff_mod: (BaseSystem.decode PseudoMersenneBaseParamProofs.base coeff) mod m = 0
+  coeff_length : (length coeff = length (Pow2Base.base_from_limb_widths limb_widths))%nat;
+  coeff_mod: (BaseSystem.decode (Pow2Base.base_from_limb_widths limb_widths) coeff) mod m = 0
 }.
 
 (* Computed versions of some functions. *)
@@ -31,10 +31,11 @@ Definition Z_shiftl_by_opt := Eval compute in Z.shiftl_by.
 
 Definition nth_default_opt {A} := Eval compute in @nth_default A.
 Definition set_nth_opt {A} := Eval compute in @set_nth A.
+Definition update_nth_opt {A} := Eval compute in @update_nth A.
 Definition map_opt {A B} := Eval compute in @map A B.
 Definition full_carry_chain_opt := Eval compute in @full_carry_chain.
 Definition length_opt := Eval compute in length.
-Definition base_opt := Eval compute in @base.
+Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths.
 Definition max_ones_opt := Eval compute in @max_ones.
 Definition max_bound_opt := Eval compute in @max_bound.
 Definition minus_opt := Eval compute in minus.
@@ -107,6 +108,7 @@ Section Carries.
   Context `{prm : PseudoMersenneBaseParams}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_).
+  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
 
   Definition carry_opt_sig
              (i : nat) (b : digits)
@@ -116,10 +118,10 @@ Section Carries.
     cbv [carry].
     rewrite <- pull_app_if_sumbool.
     cbv beta delta
-      [carry carry_and_reduce carry_simple add_to_nth log_cap
-       pow2_mod Z.ones Z.pred
+      [carry carry_and_reduce carry_simple add_to_nth
+       Z.pow2_mod Z.ones Z.pred
        PseudoMersenneBaseParams.limb_widths].
-    change @base with @base_opt.
+    change @Pow2Base.base_from_limb_widths with @base_from_limb_widths_opt.
     change @nth_default with @nth_default_opt in *.
     change @set_nth with @set_nth_opt in *.
     lazymatch goal with
@@ -372,7 +374,7 @@ Section Multiplication.
     cbv [mul_bi'_step].
     opt_step.
     { reflexivity. }
-    { cbv [crosscoef ext_base base].
+    { cbv [crosscoef ext_base].
       change Z.div with Z_div_opt.
       change Z.mul with Z_mul_opt at 2.
       change @nth_default with @nth_default_opt.
@@ -401,7 +403,7 @@ Section Multiplication.
       rewrite <- IHvsr; clear IHvsr.
       unfold mul_bi'_opt, mul_bi'_opt_step.
       apply f_equal2; [ | reflexivity ].
-      cbv [crosscoef ext_base base].
+      cbv [crosscoef ext_base].
       change Z.div with Z_div_opt.
       change Z.mul with Z_mul_opt at 2.
       change @nth_default with @nth_default_opt.
@@ -419,7 +421,9 @@ Section Multiplication.
 
   Lemma map_zeros : forall a n l,
     map (Z.mul a) (zeros n ++ l) = zeros n ++ map (Z.mul a) l.
-  Admitted.
+  Proof.
+    induction n; simpl; [ reflexivity | intros; apply f_equal2; [ omega | congruence ] ].
+  Qed.
 
   Definition mul'_opt_step_sig
              (mul' : digits -> digits -> list Z -> digits)
@@ -473,7 +477,7 @@ Section Multiplication.
     eexists.
     cbv [BaseSystem.mul mul mul_each mul_bi mul_bi' zeros ext_base reduce].
     rewrite <- mul'_opt_correct.
-    change @base with base_opt.
+    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.
@@ -507,16 +511,22 @@ Section Multiplication.
     := proj2_sig (carry_mul_opt_sig f us vs).
 End Multiplication.
 
-Record freezePreconditions {modulus} (prm : PseudoMersenneBaseParams modulus) int_width :=
-mkFreezePreconditions {
-    lt_1_length_base : (1 < length base)%nat;
-    int_width_pos : 0 < int_width;
-    int_width_compat : forall w, In w limb_widths -> w <= int_width;
-    c_pos : 0 < c;
-    c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1;
-    c_reduce2 : c <= max_bound 0 - c;
-    two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus
-}.
+Section with_base.
+  Context {modulus} (prm : PseudoMersenneBaseParams modulus).
+  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
+
+  Record freezePreconditions int_width :=
+    mkFreezePreconditions {
+        lt_1_length_base : (1 < length base)%nat;
+        int_width_pos : 0 < int_width;
+        int_width_compat : forall w, In w limb_widths -> w <= int_width;
+        c_pos : 0 < c;
+        c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < max_bound 0 + 1;
+        c_reduce2 : c <= max_bound 0 - c;
+        two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus
+      }.
+End with_base.
 Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos
     c_reduce1 c_reduce2 two_pow_k_le_2modulus.
 
@@ -537,7 +547,7 @@ Section Canonicalization.
     change minus with minus_opt.
     change Z.add with Z_add_opt.
     change Z.sub with Z_sub_opt.
-    change @base with base_opt.
+    change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
     reflexivity.
   Defined.
 
@@ -589,7 +599,7 @@ Section Canonicalization.
     change @max_bound with max_bound_opt.
     rewrite c_subst.
     change @max_ones with max_ones_opt.
-    change @base with base_opt.
+    change @Pow2Base.base_from_limb_widths with base_from_limb_widths_opt.
     change minus with minus_opt.
     change @map with @map_opt.
     change Z.sub with Z_sub_opt at 1.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 43af6dee0..ba06d4e6c 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -23,6 +23,8 @@ Section PseudoMersenneProofs.
   Local Notation "u .* x" := (ModularBaseSystem.mul u x).
   Local Hint Unfold rep.
   Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg.
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
 
   Lemma rep_decode : forall us x, us ~= x -> decode us = x.
   Proof.
@@ -61,8 +63,8 @@ Section PseudoMersenneProofs.
       rewrite Z.land_ones, Z.shiftr_div_pow2 by eauto.
       match goal with H : (S _ <= length base)%nat |- _ =>
         apply le_lt_or_eq in H; destruct H end.
-      - repeat f_equal; unfold base in *; rewrite nth_default_base  by (eauto || omega); reflexivity.
-      - repeat f_equal; try solve [unfold base in *; rewrite nth_default_base  by (eauto || omega); reflexivity].
+      - repeat f_equal; rewrite nth_default_base  by (eauto || omega); reflexivity.
+      - repeat f_equal; try solve [rewrite nth_default_base  by (eauto || omega); reflexivity].
         rewrite nth_default_out_of_bounds by omega.
         unfold k.
         rewrite <-base_length; congruence.
@@ -99,9 +101,9 @@ Section PseudoMersenneProofs.
             rewrite <-!nth_default_eq.
             apply base_succ; eauto; omega.
         - rewrite nth_default_out_of_bounds with (n := S i) by omega.
-          unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+          rewrite nth_default_base by (omega || eauto).
           unfold k.
-          match goal with H : S _ = length base |- _ => 
+          match goal with H : S _ = length base |- _ =>
             rewrite base_length in H; rewrite <-H end.
           erewrite sum_firstn_succ by (apply nth_error_Some_nth_default with (x0 := 0); omega).
           rewrite Z.pow_add_r by (eauto using sum_firstn_limb_widths_nonneg;
@@ -333,7 +335,7 @@ Section PseudoMersenneProofs.
 
   Lemma log_cap_nonneg : forall i, 0 <= log_cap i.
   Proof.
-    unfold log_cap, nth_default; intros.
+    unfold nth_default; intros.
     case_eq (nth_error limb_widths i); intros; try omega.
     apply limb_widths_nonneg.
     eapply nth_error_value_In; eauto.
@@ -368,8 +370,9 @@ End PseudoMersenneProofs.
 
 Section CarryProofs.
   Context `{prm : PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
   Local Notation "u ~= x" := (rep u x).
-  Hint Unfold log_cap.
   Local Hint Resolve limb_widths_nonneg sum_firstn_limb_widths_nonneg.
 
   Lemma base_length_lt_pred : (pred (length base) < length base)%nat.
@@ -382,14 +385,13 @@ Section CarryProofs.
     nth_default 0 base (S i) = 2 ^ log_cap i * nth_default 0 base i.
   Proof.
     intros.
-    unfold base; repeat rewrite nth_default_base by (unfold base in *; omega || eauto).
+    repeat rewrite nth_default_base by (omega || eauto).
     rewrite <- Z.pow_add_r by eauto using log_cap_nonneg.
     destruct (NPeano.Nat.eq_dec i 0).
     + subst; f_equal.
-      unfold sum_firstn, log_cap.
+      unfold sum_firstn.
       destruct limb_widths; auto.
     + erewrite sum_firstn_succ; eauto.
-      unfold log_cap.
       apply nth_error_Some_nth_default.
       rewrite <- base_length; omega.
   Qed.
@@ -402,7 +404,7 @@ Section CarryProofs.
     unfold carry_simple. intros.
     rewrite add_to_nth_sum by (rewrite length_set_nth; omega).
     rewrite set_nth_sum by omega.
-    unfold pow2_mod.
+    unfold Z.pow2_mod.
     rewrite Z.land_ones by apply log_cap_nonneg.
     rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
     rewrite nth_default_base_succ by omega.
@@ -434,12 +436,11 @@ Section CarryProofs.
       apply length0_nil in length_eq.
       symmetry in limbs_length.
       apply length0_nil in limbs_length.
-      unfold log_cap.
       subst; rewrite length_zero, limbs_length, nth_default_nil.
       reflexivity.
-    + unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+    + rewrite nth_default_base by (omega || eauto).
       rewrite <- Z.add_opp_l, <- Z.opp_sub_distr.
-      unfold pow2_mod.
+      unfold Z.pow2_mod.
       rewrite Z.land_ones by apply log_cap_nonneg.
       rewrite <- Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.pow_pos_nonneg; omega || apply log_cap_nonneg).
       rewrite Z.shiftr_div_pow2 by apply log_cap_nonneg.
@@ -451,11 +452,10 @@ Section CarryProofs.
       replace (length limb_widths) with (S (pred (length base))) by
         (subst; rewrite <- base_length; apply NPeano.Nat.succ_pred; omega).
       rewrite sum_firstn_succ with (x:= log_cap (pred (length base))) by
-        (unfold log_cap; apply nth_error_Some_nth_default; rewrite <- base_length; omega).
+        (apply nth_error_Some_nth_default; rewrite <- base_length; omega).
       rewrite <- Zopp_mult_distr_r.
       rewrite Z.mul_comm.
       rewrite (Z.add_comm (log_cap (pred (length base)))).
-      unfold base.
       ring.
   Qed.
 
@@ -538,7 +538,10 @@ Section CarryProofs.
 End CarryProofs.
 
 Section CanonicalizationProofs.
-  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat)
+  Context `{prm : PseudoMersenneBaseParams}.
+  Local Notation base := (base_from_limb_widths limb_widths).
+  Local Notation log_cap i := (nth_default 0 limb_widths i).
+  Context (lt_1_length_base : (1 < length base)%nat)
    {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B)
    (* on the first reduce step, we add at most one bit of width to the first digit *)
    (c_reduce1 : c * (Z.ones (B - log_cap (pred (length base)))) < max_bound 0 + 1)
@@ -565,10 +568,10 @@ Section CanonicalizationProofs.
   Qed.
 
   Local Hint Resolve log_cap_nonneg.
-  Lemma pow2_mod_log_cap_range : forall a i, 0 <= pow2_mod a (log_cap i) <= max_bound i.
+  Lemma pow2_mod_log_cap_range : forall a i, 0 <= Z.pow2_mod a (log_cap i) <= max_bound i.
   Proof.
     intros.
-    unfold pow2_mod.
+    unfold Z.pow2_mod.
     rewrite Z.land_ones by apply log_cap_nonneg.
     unfold max_bound, Z.ones.
     rewrite Z.shiftl_1_l, <-Z.lt_le_pred.
@@ -577,23 +580,23 @@ Section CanonicalizationProofs.
     omega.
   Qed.
 
-  Lemma pow2_mod_log_cap_bounds_lower : forall a i, 0 <= pow2_mod a (log_cap i).
+  Lemma pow2_mod_log_cap_bounds_lower : forall a i, 0 <= Z.pow2_mod a (log_cap i).
   Proof.
     intros.
     pose proof (pow2_mod_log_cap_range a  i); omega.
   Qed.
 
-  Lemma pow2_mod_log_cap_bounds_upper : forall a i, pow2_mod a (log_cap i) <= max_bound i.
+  Lemma pow2_mod_log_cap_bounds_upper : forall a i, Z.pow2_mod a (log_cap i) <= max_bound i.
   Proof.
     intros.
     pose proof (pow2_mod_log_cap_range a  i); omega.
   Qed.
 
   Lemma pow2_mod_log_cap_small : forall a i, 0 <= a <= max_bound i ->
-    pow2_mod a (log_cap i) = a.
+    Z.pow2_mod a (log_cap i) = a.
   Proof.
     intros.
-    unfold pow2_mod.
+    unfold Z.pow2_mod.
     rewrite Z.land_ones by apply log_cap_nonneg.
     apply Z.mod_small.
     split; try omega.
@@ -603,7 +606,7 @@ Section CanonicalizationProofs.
 
   Lemma max_bound_pos : forall i, (i < length base)%nat -> 0 < max_bound i.
   Proof.
-    unfold max_bound, log_cap; intros; apply Z.ones_pos_pos.
+    unfold max_bound; intros; apply Z.ones_pos_pos.
     apply limb_widths_pos.
     rewrite nth_default_eq.
     apply nth_In.
@@ -617,10 +620,10 @@ Section CanonicalizationProofs.
   Qed.
   Local Hint Resolve max_bound_nonneg.
 
-  Lemma pow2_mod_spec : forall a b, (0 <= b) -> pow2_mod a b = a mod (2 ^ b).
+  Lemma pow2_mod_spec : forall a b, (0 <= b) -> Z.pow2_mod a b = a mod (2 ^ b).
   Proof.
     intros.
-    unfold pow2_mod.
+    unfold Z.pow2_mod.
     rewrite Z.land_ones; auto.
   Qed.
 
@@ -639,7 +642,7 @@ Section CanonicalizationProofs.
 
   Lemma B_compat_log_cap : forall i, 0 <= B - log_cap i.
   Proof.
-    unfold log_cap; intros.
+    intros.
     destruct (lt_dec i (length limb_widths)).
     + apply Z.le_0_sub.
       apply B_compat.
@@ -670,7 +673,7 @@ Section CanonicalizationProofs.
   Qed.
 
   (* END groundwork proofs *)
-  Opaque pow2_mod log_cap max_bound.
+  Opaque Z.pow2_mod max_bound.
 
   (* automation *)
   Ltac carry_length_conditions' := unfold carry_full, add_to_nth;
@@ -1296,12 +1299,13 @@ Section CanonicalizationProofs.
     unfold max_ones.
     apply Z.ones_nonneg.
     pose proof limb_widths_nonneg.
-    induction limb_widths.
+    clear c_reduce1 lt_1_length_base.
+    induction limb_widths as [|?? IHl].
     cbv; congruence.
     simpl.
     apply Z.max_le_iff.
     right.
-    apply IHl; auto using in_cons.
+    apply IHl; eauto using in_cons.
   Qed.
 
   Lemma land_max_ones_noop : forall x i, 0 <= x < 2 ^ log_cap i -> Z.land max_ones x = x.
@@ -1314,7 +1318,6 @@ Section CanonicalizationProofs.
     split; try omega.
     eapply Z.lt_le_trans; try eapply x_range.
     apply Z.pow_le_mono_r; try omega.
-    rewrite log_cap_eq.
     destruct (lt_dec i (length limb_widths)).
     + apply Z.le_fold_right_max.
       - apply limb_widths_nonneg.
@@ -1430,9 +1433,8 @@ Section CanonicalizationProofs.
       destruct (nth_error_length_exists_value _ _ n_lt_length).
       erewrite sum_firstn_succ; eauto.
       rewrite Z.pow_add_r; eauto.
-      unfold base.
       rewrite nth_default_base by
-        (unfold base in *; try rewrite base_from_limb_widths_length; omega || eauto).
+        (try rewrite base_from_limb_widths_length; omega || eauto).
       rewrite Z.lt_add_lt_sub_r.
       eapply Z.lt_le_trans; eauto.
       rewrite Z.mul_comm at 1.
@@ -1443,7 +1445,6 @@ Section CanonicalizationProofs.
       rewrite Z.le_succ_l, Z.lt_0_sub.
       match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end.
       replace x with (log_cap n); try intuition.
-      rewrite log_cap_eq.
       apply nth_error_value_eq_nth_default; auto.
     + repeat erewrite firstn_all_strong by omega.
       rewrite sum_firstn_all_succ by (rewrite <-base_length; omega).
@@ -1469,7 +1470,7 @@ Section CanonicalizationProofs.
     destruct (lt_dec n (length base)) as [ n_lt_length | ? ].
     + rewrite decode_firstn_succ by auto.
       zero_bounds.
-      - unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+      - rewrite nth_default_base by (omega || eauto).
         apply Z.pow_nonneg; omega.
       - match goal with H : carry_done us |- _ => rewrite carry_done_bounds in H by auto; specialize (H n) end.
         intuition.
@@ -1561,15 +1562,16 @@ Section CanonicalizationProofs.
     BaseSystem.decode' base (modulus_digits' i) = 2 ^ (sum_firstn limb_widths (S i)) - c.
   Proof.
     induction i; intros; unfold modulus_digits'; fold modulus_digits'.
-    + case_eq base;
+    + let base := constr:(base) in
+      case_eq base;
         [ intro base_eq; rewrite base_eq, (@nil_length0 Z) in lt_1_length_base; omega | ].
       intros z ? base_eq.
       rewrite decode'_cons, decode_nil, Z.add_0_r.
       replace z with (nth_default 0 base 0) by (rewrite base_eq; auto).
-      unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+      rewrite nth_default_base by (omega || eauto).
       replace (max_bound 0 - c + 1) with (Z.succ (max_bound 0) - c) by ring.
       rewrite max_bound_log_cap.
-      rewrite sum_firstn_succ with (x := log_cap 0) by (rewrite log_cap_eq;
+      rewrite sum_firstn_succ with (x := log_cap 0) by (
         apply nth_error_Some_nth_default; rewrite <-base_length; omega).
       rewrite Z.pow_add_r by eauto.
       cbv [sum_firstn fold_right firstn].
@@ -1577,11 +1579,11 @@ Section CanonicalizationProofs.
     + assert (S i < length base \/ S i = length base)%nat as cases by omega.
       destruct cases.
       - rewrite sum_firstn_succ with (x := log_cap (S i)) by
-          (rewrite log_cap_eq; apply nth_error_Some_nth_default;
+          (apply nth_error_Some_nth_default;
           rewrite <-base_length; omega).
         rewrite Z.pow_add_r, <-max_bound_log_cap, set_higher by eauto.
         rewrite IHi, modulus_digits'_length by omega.
-        unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+        rewrite nth_default_base by (omega || eauto).
         ring.
       - rewrite sum_firstn_all_succ by (rewrite <-base_length; omega).
         rewrite decode'_splice, modulus_digits'_length, firstn_all by auto.
@@ -1759,7 +1761,7 @@ Section CanonicalizationProofs.
     + eapply Z.le_lt_trans.
       - eapply Z.add_le_mono with (q := nth_default 0 base n * -1); [ apply Z.le_refl | ].
         apply Z.mul_le_mono_nonneg_l; try omega.
-        unfold base; rewrite nth_default_base by (unfold base in *; omega || eauto).
+        rewrite nth_default_base by (omega || eauto).
         zero_bounds.
       - ring_simplify.
         apply Z.lt_sub_0.
@@ -2100,4 +2102,4 @@ Section CanonicalizationProofs.
     eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
 
-End CanonicalizationProofs.
\ No newline at end of file
+End CanonicalizationProofs.
diff --git a/src/ModularArithmetic/Pow2Base.v b/src/ModularArithmetic/Pow2Base.v
index 847967f52..7d0495ef3 100644
--- a/src/ModularArithmetic/Pow2Base.v
+++ b/src/ModularArithmetic/Pow2Base.v
@@ -14,14 +14,13 @@ Section Pow2Base.
     | w :: lw => 1 :: map (Z.mul (two_p w)) (base_from_limb_widths lw)
     end.
 
-  Local Notation "{base}" := (base_from_limb_widths limb_widths).
-
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Definition bounded us := forall i, 0 <= nth_default 0 us i < 2 ^ w[i].
 
   Definition upper_bound := 2 ^ (sum_firstn limb_widths (length limb_widths)).
 
-  Fixpoint decode_bitwise' us i acc := 
+  Fixpoint decode_bitwise' us i acc :=
     match i with
     | O => acc
     | S i' => decode_bitwise' us i' (Z.lor (nth_default 0 us i') (Z.shiftl acc w[i']))
@@ -40,4 +39,4 @@ Section Pow2Base.
   (* max must be greater than input; this is used to truncate last digit *)
   Definition encodeZ x:= encode' x (length limb_widths).
 
-End Pow2Base.
\ No newline at end of file
+End Pow2Base.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index c07da850f..b1e88d605 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -23,11 +23,11 @@ Section PseudoMersenneBaseParamProofs.
     apply sum_firstn_limb_widths_nonneg; auto.
   Qed. Hint Resolve k_nonneg.
 
-  Definition base := base_from_limb_widths limb_widths.
+  Local Notation base := (base_from_limb_widths limb_widths).
 
   Lemma base_length : length base = length limb_widths.
   Proof.
-    unfold base; auto using base_from_limb_widths_length.
+    auto using base_from_limb_widths_length.
   Qed.
 
   Lemma base_matches_modulus: forall i j,
@@ -43,18 +43,18 @@ Section PseudoMersenneBaseParamProofs.
     subst r.
     assert (i + j - length base < length base)%nat by omega.
     rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos;
-      [ | subst b; unfold base; rewrite nth_default_base; try assumption ];
+      [ | subst b; rewrite nth_default_base; try assumption ];
       zero_bounds; 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.
-    unfold base; repeat rewrite nth_default_base by auto.
+    repeat rewrite nth_default_base by 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_length, base_from_limb_widths_length in * by auto.
+    + rewrite base_length in * by auto.
       apply limb_widths_match_modulus; auto.
   Qed.
 
@@ -71,7 +71,7 @@ Section PseudoMersenneBaseParamProofs.
 
    Lemma b0_1 : forall x : Z, nth_default x base 0 = 1.
    Proof.
-     unfold base; case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity].
+     case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity].
    Qed.
 
    Lemma base_good : forall i j : nat,
@@ -81,7 +81,6 @@ Section PseudoMersenneBaseParamProofs.
                 b i * b j = r * b (i + j)%nat.
    Proof.
      intros; subst b r.
-     unfold base in *.
      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;
@@ -99,4 +98,4 @@ Section PseudoMersenneBaseParamProofs.
     base_good := base_good
   }.
 
-End PseudoMersenneBaseParamProofs.
\ No newline at end of file
+End PseudoMersenneBaseParamProofs.