remove trailing whitespace from src/

5 files changed, 41 insertions, 41 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 2e65df9bd..9ed7d065e 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -22,19 +22,19 @@ Section ExtendedBaseVector.
   *
   * (x \dot base) * (y \dot base) = (z \dot ext_base)
   *
-  * Then we can separate z into its first and second halves: 
+  * Then we can separate z into its first and second halves:
   *
   * (z \dot ext_base) = (z1 \dot base) + (2 ^ k) * (z2 \dot base)
   *
   * Now, if we want to reduce the product modulo 2 ^ k - c:
-  * 
+  *
   * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + (2 ^ k) * (z2 \dot base) mod (2^k-c)
   * (z \dot ext_base) mod (2^k-c)= (z1 \dot base) + c * (z2 \dot base) mod (2^k-c)
   *
   * This sum may be short enough to express using base; if not, we can reduce again.
   *)
   Definition ext_base := base ++ (map (Z.mul (2^k)) base).
-    
+
   Lemma ext_base_positive : forall b, In b ext_base -> b > 0.
   Proof.
     unfold ext_base. intros b In_b_base.
@@ -76,14 +76,14 @@ Section ExtendedBaseVector.
     intuition.
   Qed.
 
-  Lemma map_nth_default_base_high : forall n, (n < (length base))%nat -> 
+  Lemma map_nth_default_base_high : forall n, (n < (length base))%nat ->
     nth_default 0 (map (Z.mul (2 ^ k)) base) n =
     (2 ^ k) * (nth_default 0 base n).
   Proof.
     intros.
     erewrite map_nth_default; auto.
   Qed.
-  
+
   Lemma base_good_over_boundary : forall
     (i : nat)
     (l : (i < length base)%nat)
diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 9c6a58f9a..ca8c19d18 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -11,9 +11,9 @@ Local Open Scope Z_scope.
 
 Section PseudoMersenneBase.
   Context `{prm :PseudoMersenneBaseParams}.
-  
+
   Definition decode (us : digits) : F modulus := ZToField (BaseSystem.decode base us).
-  
+
   Definition rep (us : digits) (x : F modulus) := (length us = length base)%nat /\ decode us = x.
   Local Notation "u '~=' x" := (rep u x) (at level 70).
   Local Hint Unfold rep.
@@ -35,13 +35,13 @@ Section PseudoMersenneBase.
 End PseudoMersenneBase.
 
 Section CarryBasePow2.
-  Context `{prm :PseudoMersenneBaseParams}. 
+  Context `{prm :PseudoMersenneBaseParams}.
 
   Definition 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 =>
@@ -54,7 +54,7 @@ Section CarryBasePow2.
     let us' := set_nth i (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 := 
+  Definition carry i : digits -> digits :=
     if eq_nat_dec i (pred (length base))
     then carry_and_reduce i
     else carry_simple i.
@@ -110,12 +110,12 @@ Section Canonicalization.
     end.
 
   Definition and_term us := if isFull us then max_ones else 0.
-    
+
   Definition freeze us :=
     let us' := carry_full (carry_full (carry_full us)) in
     let and_term := and_term us' in
     (* [and_term] is all ones if us' is full, so the subtractions subtract q overall.
        Otherwise, it's all zeroes, and the subtractions do nothing. *)
      map2 (fun x y => x - y) us' (map (Z.land and_term) modulus_digits).
-   
+
 End Canonicalization.
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index c0e942ece..116fe10e5 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -76,7 +76,7 @@ Ltac construct_params prime_modulus len k :=
   | abstract apply prime_modulus
   | abstract brute_force_indices lw].
 
-Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits :=  
+Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits :=
   match limb_widths with
   | nil => nil
   | x :: tail =>
@@ -91,7 +91,7 @@ Ltac subst_precondition := match goal with
   | [H : ?P, H' : ?P -> _ |- _] => specialize (H' H); clear H
 end.
 
-Ltac kill_precondition H := 
+Ltac kill_precondition H :=
   forward H; [abstract (try exact eq_refl; clear; cbv; intros; repeat break_or_hyp; intuition)|];
   subst_precondition.
 
@@ -207,7 +207,7 @@ Section Carries.
     cbv [carry_sequence].
     transitivity (fold_right carry_opt_cps f (List.rev is) us).
     Focus 2.
-    { 
+    {
       assert (forall i, In i (rev is) -> i < length base)%nat as Hr. {
         subst. intros. rewrite <- in_rev in *. auto. }
       remember (rev is) as ris eqn:Heq.
@@ -239,7 +239,7 @@ Section Carries.
     cbv [carry_sequence].
     transitivity (fold_right carry_opt_cps id (List.rev is) us).
     Focus 2.
-    { 
+    {
       assert (forall i, In i (rev is) -> i < length base)%nat as Hr. {
         subst. intros. rewrite <- in_rev in *. auto. }
       remember (rev is) as ris eqn:Heq.
@@ -273,7 +273,7 @@ Section Carries.
     rewrite carry_sequence_opt_cps_correct by assumption.
     apply carry_sequence_rep; eauto using rep_length.
   Qed.
- 
+
   Lemma full_carry_chain_bounds : forall i, In i full_carry_chain -> (i < length base)%nat.
   Proof.
     unfold full_carry_chain; rewrite <-base_length; intros.
@@ -502,7 +502,7 @@ Section Multiplication.
     rewrite map_shiftl by apply k_nonneg.
     rewrite c_subst.
     rewrite k_subst.
-    change @map with @map_opt. 
+    change @map with @map_opt.
     change @Z_shiftl_by with @Z_shiftl_by_opt.
     reflexivity.
   Defined.
@@ -640,7 +640,7 @@ Section Canonicalization.
     := proj2_sig (freeze_opt_sig us).
 
   Lemma freeze_opt_canonical: forall us vs x,
-    @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x -> 
+    @pre_carry_bounds _ _ int_width us -> PseudoMersenneBaseRep.rep us x ->
     @pre_carry_bounds _ _ int_width vs -> PseudoMersenneBaseRep.rep vs x ->
     freeze_opt us = freeze_opt vs.
   Proof.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 562c7d6d4..0462b0f37 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -418,7 +418,7 @@ Section CarryProofs.
 End CarryProofs.
 
 Section CanonicalizationProofs.
-  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat) 
+  Context `{prm : PseudoMersenneBaseParams} (lt_1_length_base : (1 < length base)%nat)
    {B} (B_pos : 0 < B) (B_compat : forall w, In w limb_widths -> w <= B)
    (c_pos : 0 < c)
    (* on the first reduce step, we add at most one bit of width to the first digit *)
@@ -783,7 +783,7 @@ Section CanonicalizationProofs.
         add_set_nth; [ zero_bounds | ]; apply IHj; auto; omega.
   Qed.
 
-  Ltac carry_seq_lower_bound := 
+  Ltac carry_seq_lower_bound :=
         repeat (intros; eapply carry_sequence_bounds_lower; eauto; carry_length_conditions).
 
   Lemma carry_bounds_lower : forall i us j, (0 < i <= j)%nat -> (length us = length base) ->
@@ -988,7 +988,7 @@ Section CanonicalizationProofs.
     split; (destruct (eq_nat_dec i 0); subst;
       [ cbv [make_chain carry_sequence fold_right carry_simple]; add_set_nth
       | eapply carry_full_2_bounds_succ; eauto; omega]).
-    + zero_bounds. 
+    + zero_bounds.
       - eapply carry_full_2_bounds_0; eauto.
       - eapply carry_full_bounds; eauto; carry_length_conditions.
         carry_seq_lower_bound.
@@ -1097,7 +1097,7 @@ Section CanonicalizationProofs.
           [ apply Z.sub_le_mono_r; subst x; apply carry_full_2_bounds_0; auto;
           ring_simplify | ]; omega.
     + rewrite carry_unaffected_low by carry_length_conditions.
-      assert (0 < S i < length base)%nat by omega. 
+      assert (0 < S i < length base)%nat by omega.
       intuition; right.
       apply carry_carry_done_done; try solve [carry_length_conditions].
       assumption.
@@ -1123,7 +1123,7 @@ Section CanonicalizationProofs.
     unfold carry, carry_and_reduce; break_if; try omega; intros.
     add_set_nth.
     split.
-    + zero_bounds. 
+    + zero_bounds.
       - eapply carry_full_2_bounds_same; eauto; omega.
       - eapply carry_carry_full_2_bounds_0_lower; eauto; omega.
     + pose proof (carry_carry_full_2_bounds_0_upper us (pred (length base))).
@@ -1138,12 +1138,12 @@ Section CanonicalizationProofs.
         ring_simplify.
         apply carry_full_2_bounds_same; auto.
       - match goal with H0 : (pred (length base) < length base)%nat,
-                        H : carry_done _ |- _ => 
+                        H : carry_done _ |- _ =>
           destruct (H (pred (length base)) H0) as [Hcd1 Hcd2]; rewrite Hcd2 by omega end.
         ring_simplify.
         apply shiftr_eq_0_max_bound; auto.
         assert (0 < length base)%nat as zero_lt_length by omega.
-        match goal with H : carry_done _ |- _ => 
+        match goal with H : carry_done _ |- _ =>
           destruct (H 0%nat zero_lt_length) end.
        assumption.
   Qed.
@@ -1277,7 +1277,7 @@ Section CanonicalizationProofs.
   Local Hint Resolve carry_full_3_length.
 
   Lemma nth_default_map2 : forall {A B C} (f : A -> B -> C) ls1 ls2 i d d1 d2,
-    nth_default d (map2 f ls1 ls2) i = 
+    nth_default d (map2 f ls1 ls2) i =
       if lt_dec i (min (length ls1) (length ls2))
       then f (nth_default d1 ls1 i) (nth_default d2 ls2 i)
       else d.
@@ -1487,7 +1487,7 @@ Section CanonicalizationProofs.
     replace (S (length base - 1)) with (length base) by omega.
     reflexivity.
   Qed.
-    
+
   Lemma carry_done_modulus_digits : carry_done modulus_digits.
   Proof.
     apply carry_done_bounds; [apply modulus_digits_length | ].
@@ -1660,7 +1660,7 @@ Section CanonicalizationProofs.
   Proof.
     unfold isFull; intros; auto using isFull'_true_iff.
   Qed.
-  
+
   Definition minimal_rep us := BaseSystem.decode base us = (BaseSystem.decode base us) mod modulus.
 
   Fixpoint compare' us vs i :=
@@ -1813,7 +1813,7 @@ Section CanonicalizationProofs.
     intros.
     destruct (Z_dec (nth_default 0 us n) (nth_default 0 vs n)) as [[?|Hgt]|?]; try congruence.
     + etransitivity; try apply Z_compare_decode_step_lt; auto.
-    + match goal with |- (?a ?= ?b) = (?c ?= ?d) => 
+    + match goal with |- (?a ?= ?b) = (?c ?= ?d) =>
         rewrite (Z.compare_antisym b a); rewrite (Z.compare_antisym d c) end.
       apply CompOpp_inj; rewrite !CompOpp_involutive.
       apply gt_lt_symmetry in Hgt.
@@ -1923,11 +1923,11 @@ Section CanonicalizationProofs.
       - rewrite nth_default_modulus_digits in *.
         repeat (break_if; try omega).
         * subst.
-          match goal with H : isFull' _ _ _ = true |- _ => 
+          match goal with H : isFull' _ _ _ = true |- _ =>
             apply isFull'_lower_bound_0 in H end.
           apply Z.compare_ge_iff.
           omega.
-        * match goal with H : isFull' _ _ _ = true |- _ => 
+        * match goal with H : isFull' _ _ _ = true |- _ =>
             apply isFull'_true_iff in H; try assumption; destruct H as [? eq_max_bound] end.
           specialize (eq_max_bound j).
           omega.
@@ -2065,7 +2065,7 @@ Section CanonicalizationProofs.
     us = vs.
   Proof.
    intros.
-   match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ => 
+   match goal with Hrep1 : rep _ ?x, Hrep2 : rep _ ?x |- _ =>
      pose proof (rep_decode_mod _ _ _ Hrep1 Hrep2) as eqmod end.
    repeat match goal with Hmin : minimal_rep ?us |- _ => unfold minimal_rep in Hmin;
      rewrite <- Hmin in eqmod; clear Hmin end.
@@ -2076,7 +2076,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma freeze_canonical : forall us vs x,
-    pre_carry_bounds us -> rep us x -> 
+    pre_carry_bounds us -> rep us x ->
     pre_carry_bounds vs -> rep vs x ->
     freeze us = freeze vs.
   Proof.
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index 10bbdf33d..49b1875ce 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -32,7 +32,7 @@ Section PseudoMersenneBaseParamProofs.
     unfold value in *.
     congruence.
   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 ->
@@ -45,7 +45,7 @@ Section PseudoMersenneBaseParamProofs.
     case_eq i; intros; subst.
     + subst; apply nth_error_first in nth_err_w.
       apply nth_error_first in nth_err_b; subst.
-      apply map_nth_error. 
+      apply map_nth_error.
       case_eq l; intros; subst; [simpl in *; omega | ].
       unfold base_from_limb_widths; fold base_from_limb_widths.
       reflexivity.
@@ -65,7 +65,7 @@ Section PseudoMersenneBaseParamProofs.
     apply nth_error_first in H.
     subst; eauto.
   Qed.
-  
+
   Lemma sum_firstn_succ : forall l i x,
     nth_error l i = Some x ->
     sum_firstn l (S i) = x + sum_firstn l i.
@@ -117,7 +117,7 @@ Section PseudoMersenneBaseParamProofs.
     induction i; intros.
     + unfold base, sum_firstn, base_from_limb_widths in *; case_eq limb_widths; try reflexivity.
       intro lw_nil; rewrite lw_nil, (@nil_length0 Z) in *; omega.
-    + 
+    +
       assert (i < length base)%nat as lt_i_length by omega.
       specialize (IHi lt_i_length).
       rewrite base_length in lt_i_length.
@@ -138,7 +138,7 @@ Section PseudoMersenneBaseParamProofs.
         apply limb_widths_nonneg.
         eapply nth_error_value_In; eauto.
   Qed.
-  
+
   Lemma nth_default_base : forall d i, (i < length base)%nat ->
     nth_default d base i = 2 ^ (sum_firstn limb_widths i).
   Proof.
@@ -178,7 +178,7 @@ Section PseudoMersenneBaseParamProofs.
     + rewrite base_length in *; apply limb_widths_match_modulus; assumption.
   Qed.
 
-  Lemma base_succ : forall i, ((S i) < length base)%nat -> 
+  Lemma base_succ : forall i, ((S i) < length base)%nat ->
     nth_default 0 base (S i) mod nth_default 0 base i = 0.
   Proof.
     intros.
@@ -226,7 +226,7 @@ Section PseudoMersenneBaseParamProofs.
    Proof.
      unfold base; case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity].
    Qed.
- 
+
    Lemma base_good : forall i j : nat,
                 (i + j < length base)%nat ->
                 let b := nth_default 0 base in