map -> List.map (not Tuple.map)

2 files changed, 40 insertions, 40 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 6a3a4f7c2..dba1afd29 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -43,7 +43,7 @@ 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 map_opt {A B} := Eval compute in @List.map A B.
 Definition full_carry_chain_opt := Eval compute in @Pow2Base.full_carry_chain.
 Definition length_opt := Eval compute in length.
 Definition base_from_limb_widths_opt := Eval compute in @Pow2Base.base_from_limb_widths.
@@ -143,7 +143,7 @@ Definition construct_mul2modulus {m} (prm : PseudoMersenneBaseParams m) : digits
   match limb_widths with
   | nil => nil
   | x :: tail =>
-      2 ^ (x + 1) - (2 * c) :: map (fun w => 2 ^ (w + 1) - 2) tail
+      2 ^ (x + 1) - (2 * c) :: List.map (fun w => 2 ^ (w + 1) - 2) tail
   end.
 
 Ltac compute_preconditions :=
@@ -459,7 +459,7 @@ Section Subtraction.
   Definition opp_opt_correct us
     : opp_opt us = opp coeff coeff_mod us
     := proj2_sig (opp_opt_sig us).
-  
+
 End Subtraction.
 
 Section Multiplication.
@@ -532,7 +532,7 @@ Section Multiplication.
        end.
 
   Lemma map_zeros : forall a n l,
-    map (Z.mul a) (zeros n ++ l) = zeros n ++ map (Z.mul a) l.
+    List.map (Z.mul a) (zeros n ++ l) = zeros n ++ List.map (Z.mul a) l.
   Proof.
     induction n; simpl; [ reflexivity | intros; apply f_equal2; [ omega | congruence ] ].
   Qed.
@@ -553,7 +553,7 @@ Section Multiplication.
     { cbv [mul_each mul_bi].
       rewrite <- mul_bi'_opt_correct.
       rewrite map_zeros.
-      change @map with @map_opt.
+      change @List.map with @map_opt.
       cbv [zeros].
       reflexivity. }
   Defined.
@@ -598,7 +598,7 @@ Section Multiplication.
     rewrite Z.map_shiftl by apply k_nonneg.
     rewrite c_subst.
     fold k; rewrite k_subst.
-    change @map with @map_opt.
+    change @List.map with @map_opt.
     change @Z.shiftl_by with @Z_shiftl_by_opt.
     reflexivity.
   Defined.
@@ -670,7 +670,7 @@ Section PowInv.
           {cc : CarryChain limb_widths}.
   Local Notation digits := (tuple Z (length limb_widths)).
   Context (one_ : digits) (one_subst : one = one_).
-  
+
   Fixpoint fold_chain_opt {T} (id : T) op chain acc :=
   match chain with
   | [] => match acc with
@@ -761,7 +761,7 @@ Section Conversion.
   Definition convert'_opt {lwA lwB}
              (nonnegA : forall x, In x lwA -> 0 <= x)
              (nonnegB : forall x, In x lwB -> 0 <= x)
-             bits_fit inp i out := 
+             bits_fit inp i out :=
     Eval cbv [proj1_sig convert'_opt_sig] in
       proj1_sig (convert'_opt_sig nonnegA nonnegB bits_fit inp i out).
 
@@ -769,10 +769,10 @@ Section Conversion.
              (nonnegA : forall x, In x lwA -> 0 <= x)
              (nonnegB : forall x, In x lwB -> 0 <= x)
              bits_fit inp i out :
-    convert'_opt nonnegA nonnegB bits_fit inp i out = convert' nonnegA nonnegB bits_fit inp i out := 
+    convert'_opt nonnegA nonnegB bits_fit inp i out = convert' nonnegA nonnegB bits_fit inp i out :=
     Eval cbv [proj2_sig convert'_opt_sig] in
       proj2_sig (convert'_opt_sig nonnegA nonnegB bits_fit inp i out).
-    
+
   Context {modulus} (prm : PseudoMersenneBaseParams modulus)
           {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x) (bits_eq : sum_firstn limb_widths (length limb_widths) = sum_firstn target_widths (length target_widths)).
   Local Notation digits := (tuple Z (length limb_widths)).
@@ -813,7 +813,7 @@ Section Conversion.
 
   Definition unpack_opt (x : target_digits) : digits :=
     Eval cbv [proj1_sig unpack_opt_sig] in proj1_sig (unpack_opt_sig x).
-  
+
   Definition unpack_correct (x : target_digits) :
     unpack_opt x = unpack target_widths_nonneg bits_eq x
     := Eval cbv [proj2_sig unpack_opt_sig] in proj2_sig (unpack_opt_sig x).
@@ -883,7 +883,7 @@ Section Canonicalization.
     change @max_ones with max_ones_opt.
     reflexivity.
   Defined.
-  
+
   Definition conditional_subtract_modulus_opt f cond : list Z
     := Eval cbv [proj1_sig conditional_subtract_modulus_opt_sig] in proj1_sig (conditional_subtract_modulus_opt_sig f cond).
 
@@ -937,10 +937,10 @@ Section SquareRoots.
   Proof.
     intros; repeat break_if; congruence.
   Qed.
-  
+
   Section SquareRoot3mod4.
   Context {ec : ExponentiationChain (modulus / 4 + 1)}.
-    
+
   Definition sqrt_3mod4_opt_sig (us : digits) :
     { vs : digits | eq vs (sqrt_3mod4 chain chain_correct us)}.
   Proof.
@@ -954,7 +954,7 @@ Section SquareRoots.
   Definition sqrt_3mod4_opt_correct us
     : eq (sqrt_3mod4_opt us) (sqrt_3mod4 chain chain_correct us)
     := Eval cbv [proj2_sig sqrt_3mod4_opt_sig] in proj2_sig (sqrt_3mod4_opt_sig us).
-  
+
   End SquareRoot3mod4.
 
   Import Morphisms.
@@ -963,7 +963,7 @@ Section SquareRoots.
   Section SquareRoot5mod8.
   Context {ec : ExponentiationChain (modulus / 8 + 1)}.
   Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)).
-    
+
   Definition sqrt_5mod8_opt_sig (us : digits) :
     { vs : digits |
       eq vs (sqrt_5mod8 (carry_mul_opt k_ c_) (pow_opt k_ c_ one_) chain chain_correct sqrt_m1 us)}.
@@ -982,7 +982,7 @@ Section SquareRoots.
   Definition sqrt_5mod8_opt_correct us
     : eq (sqrt_5mod8_opt us) (ModularBaseSystem.sqrt_5mod8 _ _ chain chain_correct sqrt_m1 us)
     := Eval cbv [proj2_sig sqrt_5mod8_opt_sig] in proj2_sig (sqrt_5mod8_opt_sig us).
-  
+
   End SquareRoot5mod8.
 
 End SquareRoots.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 5d7a1c24d..c160eca7f 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -138,8 +138,8 @@ Section FieldOperationProofs.
   Lemma modular_base_system_add_monoid : @monoid digits eq add zero.
   Proof.
     repeat match goal with
-           | |- _ => progress intro 
-           | |- _ => cbv [zero]; rewrite encode_rep 
+           | |- _ => progress intro
+           | |- _ => cbv [zero]; rewrite encode_rep
            | |- _ digits eq add => econstructor
            | |- _ digits eq add _ => econstructor
            | |- (_ + _)%F = decode (add ?a ?b) =>  rewrite (add_rep a b) by (try apply add_rep; reflexivity)
@@ -149,7 +149,7 @@ Section FieldOperationProofs.
            | |- add _ _ ~= decode _ => etransitivity
            | x : digits |- ?x ~= _ => reflexivity
            | |- _ => apply associative
-           | |- _ => apply left_identity 
+           | |- _ => apply left_identity
            | |- _ => apply right_identity
            | |- _ => solve [eauto using eq_Equivalence, eq_dec]
            | |- _ => congruence
@@ -165,7 +165,7 @@ Section FieldOperationProofs.
   Proof.
     cbv [reduce]; intros.
     rewrite extended_shiftadd, base_from_limb_widths_length, pseudomersenne_add, BaseSystemProofs.add_rep.
-    change (map (Z.mul c)) with (BaseSystem.mul_each c).
+    change (List.map (Z.mul c)) with (BaseSystem.mul_each c).
     rewrite mul_each_rep; auto.
   Qed.
 
@@ -186,8 +186,8 @@ Section FieldOperationProofs.
   Lemma modular_base_system_mul_monoid : @monoid digits eq mul one.
   Proof.
     repeat match goal with
-           | |- _ => progress intro 
-           | |- _ => cbv [one]; rewrite encode_rep 
+           | |- _ => progress intro
+           | |- _ => cbv [one]; rewrite encode_rep
            | |- _ digits eq mul => econstructor
            | |- _ digits eq mul _ => econstructor
            | |- (_ * _)%F = decode (mul ?a ?b) =>  rewrite (mul_rep a b) by (try apply mul_rep; reflexivity)
@@ -197,7 +197,7 @@ Section FieldOperationProofs.
            | |- mul _ _ ~= decode _ => etransitivity
            | x : digits |- ?x ~= _ => reflexivity
            | |- _ => apply associative
-           | |- _ => apply left_identity 
+           | |- _ => apply left_identity
            | |- _ => apply right_identity
            | |- _ => solve [eauto using eq_Equivalence, eq_dec]
            | |- _ => congruence
@@ -290,7 +290,7 @@ Section FieldOperationProofs.
     cbv beta delta [eq] in *.
     erewrite !add_rep; cbv [rep] in *; try reflexivity; assumption.
   Qed.
-  
+
   Global Instance sub_Proper mm mm_correct
     : Proper (eq ==> eq ==> eq) (sub mm mm_correct).
   Proof.
@@ -298,7 +298,7 @@ Section FieldOperationProofs.
     cbv beta delta [eq] in *.
     erewrite !sub_rep; cbv [rep] in *; try reflexivity; assumption.
   Qed.
-  
+
   Global Instance opp_Proper mm mm_correct
     : Proper (eq ==> eq) (opp mm mm_correct).
   Proof.
@@ -361,7 +361,7 @@ Section FieldOperationProofs.
     + trivial.
   Qed.
   End FieldProofs.
-  
+
 End FieldOperationProofs.
 Opaque encode add mul sub inv pow.
 
@@ -579,7 +579,7 @@ Section CanonicalizationProofs.
                  then
                     if eq_nat_dec n (pred i)
                     then Z.pow2_mod (us {{ pred i }} [n]) (limb_widths [n])
-                    else us{{ pred i }} [n] 
+                    else us{{ pred i }} [n]
                  else us{{ pred i}} [n] +
                     (if eq_nat_dec n i
                       then (us{{ pred i}} [pred i]) >> (limb_widths [pred i])
@@ -631,11 +631,11 @@ Section CanonicalizationProofs.
     reflexivity.
   Qed.
 
-  Ltac bound_during_loop := 
+  Ltac bound_during_loop :=
     repeat match goal with
            | |- _ => progress (intros; subst)
            | |- _ => unique pose proof lt_1_length_limb_widths
-           | |- _ => unique pose proof c_reduce2 
+           | |- _ => unique pose proof c_reduce2
            | |- _ => break_if; try omega
            | |- _ => progress simpl pred in *
            | |- _ => progress rewrite ?Z.add_0_r, ?Z.sub_0_r in *
@@ -770,7 +770,7 @@ Section CanonicalizationProofs.
       if lt_dec i (length limb_widths)
       then
         if Z_lt_dec (us [0]) (2 ^ limb_widths [0])
-        then                      
+        then
           2 ^ limb_widths [n]
         else
           if eq_nat_dec n 0
@@ -798,7 +798,7 @@ Section CanonicalizationProofs.
       auto using length_carry_full, bound_after_second_loop.
   Qed.
 
-  Local Notation initial_bounds u := 
+  Local Notation initial_bounds u :=
       (forall n : nat,
        0 <= to_list (length limb_widths) u [n] <
        2 ^ B -
@@ -807,7 +807,7 @@ Section CanonicalizationProofs.
         else (2 ^ B) >> (limb_widths [pred n]))).
   Local Notation minimal_rep u := ((bounded limb_widths (to_list (length limb_widths) u))
                                    /\ (ge_modulus (to_list _ u) = false)).
-  
+
   Lemma decode_bitwise_eq_iff : forall u v, minimal_rep u -> minimal_rep v ->
     (fieldwise Logic.eq u v <->
      decode_bitwise limb_widths (to_list _ u) = decode_bitwise limb_widths (to_list _ v)).
@@ -851,7 +851,7 @@ Section CanonicalizationProofs.
   Qed.
 
   Lemma bounded_canonical : forall u v x y, rep u x -> rep v y ->
-                                            minimal_rep u -> minimal_rep v -> 
+                                            minimal_rep u -> minimal_rep v ->
                                             (x = y <-> fieldwise Logic.eq u v).
   Proof.
     intros.
@@ -921,7 +921,7 @@ Section CanonicalizationProofs.
     erewrite <-!Fdecode_decode_mod by eauto.
     apply freeze_decode.
   Qed.
-  
+
   Lemma freeze_canonical : forall u v x y, rep u x -> rep v y ->
                                            initial_bounds u ->
                                            initial_bounds v ->
@@ -939,15 +939,15 @@ Section SquareRootProofs.
   Local Notation base := (base_from_limb_widths limb_widths).
   Local Hint Resolve (@limb_widths_nonneg _ prm) sum_firstn_limb_widths_nonneg.
 
-  Definition freeze_input_bounds n := 
+  Definition freeze_input_bounds n :=
      (2 ^ B -
        (if eq_nat_dec n 0
         then 0
         else (2 ^ B) >> (nth_default 0 limb_widths (pred n)))).
-  Definition bounded_by u bounds := 
+  Definition bounded_by u bounds :=
       (forall n : nat,
           0 <= nth_default 0 (to_list (length limb_widths) u) n < bounds n).
-  
+
   Lemma eqb_true_iff : forall u v x y,
     bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds ->
     u ~= x -> v ~= y -> (x = y <-> eqb u v = true).
@@ -1002,7 +1002,7 @@ Section SquareRootProofs.
           {pow_input_bounds : nat -> Z}
           (pow_bounded : forall x is, bounded_by x pow_input_bounds ->
                                       bounded_by (pow_ x is) mul_input_bounds).
-  
+
   Lemma sqrt_5mod8_correct : forall u x, u ~= x ->
     bounded_by u pow_input_bounds -> bounded_by u freeze_input_bounds ->
     (sqrt_5mod8 mul_ pow_ chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x.
@@ -1031,4 +1031,4 @@ Section SquareRootProofs.
   Qed.
   End Sqrt5mod8.
 
-End SquareRootProofs.
\ No newline at end of file
+End SquareRootProofs.