Add [Proof using] to most proofs

This closes #146 and makes `make quick` faster.

The changes were generated by adding [Global Set Suggest Proof Using.]
to GlobalSettings.v, and then following [the instructions for a script I
wrote](https://github.com/JasonGross/coq-tools#proof-using-helper).

7 files changed, 49 insertions, 49 deletions

diff --git a/src/Util/AdditionChainExponentiation.v b/src/Util/AdditionChainExponentiation.v
index 97c3e02a3..fc082a54a 100644
--- a/src/Util/AdditionChainExponentiation.v
+++ b/src/Util/AdditionChainExponentiation.v
@@ -38,7 +38,7 @@ Section AddChainExp.
       (H:forall i, nth_default id acc i = (nth_default 0 ref i) * x)
       (Hl:Logic.eq (length acc) (length ref)),
       fold_chain id op is acc = (fold_chain 0 N.add is ref) * x.
-  Proof.
+  Proof using Type*.
     induction is; intros; simpl @fold_chain.
     { repeat break_match; specialize (H 0%nat); rewrite ?nth_default_cons, ?nth_default_cons_S in H;
       solve [ simpl length in *; discriminate | apply H | rewrite scalarmult_0_l; reflexivity ]. }
@@ -51,7 +51,7 @@ Section AddChainExp.
   Qed.
 
   Lemma fold_chain_exp x is: fold_chain id op is [x] = (fold_chain 0 N.add is [1]) * x.
-  Proof.
+  Proof using Type*.
     eapply fold_chain_exp'; intros; trivial.
     destruct i; try destruct i; rewrite ?nth_default_cons_S, ?nth_default_cons, ?nth_default_nil;
       rewrite ?scalarmult_1_l, ?scalarmult_0_l; reflexivity.
diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v
index 15b74134d..2fd7f8adc 100644
--- a/src/Util/IterAssocOp.v
+++ b/src/Util/IterAssocOp.v
@@ -16,7 +16,7 @@ Section IterAssocOp.
 
   Lemma nat_iter_op_plus m n a :
     op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a.
-  Proof. symmetry; eapply ScalarMult.scalarmult_add_l. Qed.
+  Proof using Type*. symmetry; eapply ScalarMult.scalarmult_add_l. Qed.
 
   Definition N_iter_op n a :=
     match n with
@@ -25,17 +25,17 @@ Section IterAssocOp.
     end.
 
   Lemma Pos_iter_op_succ : forall p a, Pos.iter_op op (Pos.succ p) a === op a (Pos.iter_op op p a).
-  Proof.
+  Proof using Type*.
    induction p; intros; simpl; rewrite ?associative, ?IHp; reflexivity.
   Qed.
 
   Lemma N_iter_op_succ : forall n a, N_iter_op (N.succ n) a  === op a (N_iter_op n a).
-  Proof.
+  Proof using Type*.
     destruct n; simpl; intros; rewrite ?Pos_iter_op_succ, ?right_identity; reflexivity.
   Qed.
 
   Lemma N_iter_op_is_nat_iter_op : forall n a, N_iter_op n a === nat_iter_op (N.to_nat n) a.
-  Proof.
+  Proof using Type*.
     induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity.
   Qed.
 
@@ -68,7 +68,7 @@ Section IterAssocOp.
   Lemma test_and_op_inv_step : forall a s,
     test_and_op_inv a s ->
     test_and_op_inv a (test_and_op a s).
-  Proof.
+  Proof using Type*.
     destruct s as [i acc].
     unfold test_and_op_inv, test_and_op; simpl; intro Hpre.
     destruct i; [ apply Hpre | ].
@@ -83,13 +83,13 @@ Section IterAssocOp.
   Lemma test_and_op_inv_holds : forall a i s,
     test_and_op_inv a s ->
     test_and_op_inv a (funexp (test_and_op a) s i).
-  Proof.
+  Proof using Type*.
     induction i; intros; auto; simpl; apply test_and_op_inv_step; auto.
   Qed.
 
   Lemma funexp_test_and_op_index : forall a x acc y,
     fst (funexp (test_and_op a) (x, acc) y) = x - y.
-  Proof.
+  Proof using Type.
     induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity.
     match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end.
     simpl in IHy.
@@ -102,7 +102,7 @@ Section IterAssocOp.
     test_and_op_inv a
       (funexp (test_and_op a) (bound, id) bound) ->
     iter_op bound a === nat_iter_op (N.to_nat x) a.
-  Proof.
+  Proof using moinoid.
     unfold test_and_op_inv, iter_op; simpl; intros ? ? ? Hinv.
     rewrite Hinv, funexp_test_and_op_index, Minus.minus_diag.
     reflexivity.
@@ -110,7 +110,7 @@ Section IterAssocOp.
 
   Lemma iter_op_correct : forall a bound, N.size_nat x <= bound ->
     iter_op bound a === nat_iter_op (N.to_nat x) a.
-  Proof.
+  Proof using Type*.
     intros.
     apply iter_op_termination; auto.
     apply test_and_op_inv_holds.
diff --git a/src/Util/ListUtil.v b/src/Util/ListUtil.v
index 3904b1c2e..32c6dbdf7 100644
--- a/src/Util/ListUtil.v
+++ b/src/Util/ListUtil.v
@@ -56,7 +56,7 @@ Module Export List.
     (** Results about [nth_error] *)
 
     Lemma nth_error_In l n (x : A) : nth_error l n = Some x -> In x l.
-    Proof.
+    Proof using Type.
       revert n. induction l as [|a l IH]; intros [|n]; simpl; try easy.
       - injection 1; auto.
       - eauto.
@@ -68,7 +68,7 @@ Module Export List.
     Variable f : A -> B.
 
     Lemma map_cons (x:A)(l:list A) : map f (x::l) = (f x) :: (map f l).
-    Proof.
+    Proof using Type.
       reflexivity.
     Qed.
   End Map.
@@ -90,7 +90,7 @@ Module Export List.
 
     Theorem length_zero_iff_nil (l : list A):
       length l = 0 <-> l=[].
-    Proof.
+    Proof using Type.
       split; [now destruct l | now intros ->].
     Qed.
   End Facts.
@@ -106,13 +106,13 @@ Module Export List.
 
     Theorem repeat_length x n:
       length (repeat x n) = n.
-    Proof.
+    Proof using Type.
       induction n as [| k Hrec]; simpl; rewrite ?Hrec; reflexivity.
     Qed.
 
     Theorem repeat_spec n x y:
       In y (repeat x n) -> y=x.
-    Proof.
+    Proof using Type.
       induction n as [|k Hrec]; simpl; destruct 1; auto.
     Qed.
 
@@ -125,16 +125,16 @@ Module Export List.
     Local Notation firstn := (@firstn A).
 
     Lemma firstn_nil n: firstn n [] = [].
-    Proof. induction n; now simpl. Qed.
+    Proof using Type. induction n; now simpl. Qed.
 
     Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l).
-    Proof. now simpl. Qed.
+    Proof using Type. now simpl. Qed.
 
     Lemma firstn_all l: firstn (length l) l = l.
     Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed.
 
     Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l.
-    Proof. induction n as [|k iHk].
+    Proof using Type. induction n as [|k iHk].
            - intro. inversion 1 as [H1|?].
              rewrite (length_zero_iff_nil l) in H1. subst. now simpl.
            - destruct l as [|x xs]; simpl.
@@ -143,10 +143,10 @@ Module Export List.
     Qed.
 
     Lemma firstn_O l: firstn 0 l = [].
-    Proof. now simpl. Qed.
+    Proof using Type. now simpl. Qed.
 
     Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.
-    Proof.
+    Proof using Type.
       induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl].
       - auto with arith.
       - apply le_n_S, iHk.
@@ -154,7 +154,7 @@ Module Export List.
 
     Lemma firstn_length_le: forall l:list A, forall n:nat,
           n <= length l -> length (firstn n l) = n.
-    Proof. induction l as [|x xs Hrec].
+    Proof using Type. induction l as [|x xs Hrec].
            - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
            - destruct n.
              * now simpl.
@@ -164,7 +164,7 @@ Module Export List.
     Lemma firstn_app n:
       forall l1 l2,
         firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2).
-    Proof. induction n as [|k iHk]; intros l1 l2.
+    Proof using Type. induction n as [|k iHk]; intros l1 l2.
            - now simpl.
            - destruct l1 as [|x xs].
              * unfold List.firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O.
@@ -174,7 +174,7 @@ Module Export List.
     Lemma firstn_app_2 n:
       forall l1 l2,
         firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.
-    Proof. induction n as [| k iHk];intros l1 l2.
+    Proof using Type. induction n as [| k iHk];intros l1 l2.
            - unfold List.firstn at 2. rewrite <- plus_n_O, app_nil_r.
              rewrite firstn_app. rewrite <- minus_diag_reverse.
              unfold List.firstn at 2. rewrite app_nil_r. apply firstn_all.
diff --git a/src/Util/NUtil.v b/src/Util/NUtil.v
index 6f50642c3..1faa1da95 100644
--- a/src/Util/NUtil.v
+++ b/src/Util/NUtil.v
@@ -126,7 +126,7 @@ Module N.
         (0 <= z2 < 2 ^ (Z.of_nat sz2))%Z ->
         Word.combine (ZNWord sz1 z1) (ZNWord sz2 z2) =
         ZNWord (sz1 + sz2) (Z.lor z1 (Z.shiftl z2 (Z.of_nat sz1))).
-    Proof.
+    Proof using Type.
       cbv [ZNWord]; intros.
       rewrite !Word.NToWord_nat.
       match goal with |- ?a = _ => rewrite <- (Word.natToWord_wordToNat a) end.
diff --git a/src/Util/NumTheoryUtil.v b/src/Util/NumTheoryUtil.v
index f89eb6996..05ce4a0de 100644
--- a/src/Util/NumTheoryUtil.v
+++ b/src/Util/NumTheoryUtil.v
@@ -47,12 +47,12 @@ Hypothesis prime_p : prime p.
 Hypothesis neq_p_2 : p <> 2. (* Euler's Criterion is also provable with p = 2, but we do not need it and are lazy.*)
 Hypothesis x_id : x * 2 + 1 = p.
 
-Lemma lt_1_p : 1 < p. Proof. prime_bound. Qed.
-Lemma x_pos: 0 < x. Proof. prime_bound. Qed.
-Lemma x_nonneg: 0 <= x. Proof. prime_bound. Qed.
+Lemma lt_1_p : 1 < p. Proof using prime_p. prime_bound. Qed.
+Lemma x_pos: 0 < x. Proof using prime_p x_id. prime_bound. Qed.
+Lemma x_nonneg: 0 <= x. Proof using prime_p x_id. prime_bound. Qed.
 
 Lemma x_id_inv : x = (p - 1) / 2.
-Proof.
+Proof using x_id.
   intros; apply Zeq_plus_swap in x_id.
   replace (p - 1) with (2 * ((p - 1) / 2)) in x_id by
     (symmetry; apply Z_div_exact_2; [omega | rewrite <- x_id; apply Z_mod_mult]).
@@ -60,19 +60,19 @@ Proof.
 Qed.
 
 Lemma mod_p_order : FGroup.g_order (ZPGroup p lt_1_p) = p - 1.
-Proof.
+Proof using Type.
   intros; rewrite <- phi_is_order.
   apply Euler.prime_phi_n_minus_1; auto.
 Qed.
 
 Lemma p_odd : Z.odd p = true.
-Proof.
+Proof using neq_p_2 prime_p.
   pose proof (Z.prime_odd_or_2 p prime_p).
   destruct H; auto.
 Qed.
 
 Lemma prime_pred_even : Z.even (p - 1) = true.
-Proof.
+Proof using neq_p_2 prime_p.
   intros.
   rewrite <- Z.odd_succ.
   replace (Z.succ (p - 1)) with p by ring.
@@ -81,7 +81,7 @@ Qed.
 
 Lemma fermat_little: forall a (a_nonzero : a mod p <> 0),
   a ^ (p - 1) mod p = 1.
-Proof.
+Proof using prime_p.
   intros.
   assert (rel_prime a p). {
     apply rel_prime_mod_rev; try prime_bound.
@@ -96,7 +96,7 @@ Proof.
 Qed.
 
 Lemma fermat_inv : forall a, a mod p <> 0 -> ((a^(p-2) mod p) * a) mod p = 1.
-Proof.
+Proof using prime_p.
   intros.
   pose proof (prime_ge_2 _ prime_p).
   rewrite Zmult_mod_idemp_l.
@@ -108,7 +108,7 @@ Qed.
 
 Lemma squared_fermat_little: forall a (a_nonzero : a mod p <> 0),
   (a * a) ^ x mod p = 1.
-Proof.
+Proof using prime_p x_id.
   intros.
   rewrite <- Z.pow_2_r.
   rewrite <- Z.pow_mul_r by (apply x_nonneg || omega).
@@ -119,7 +119,7 @@ Qed.
 
 Lemma euler_criterion_square_reverse : forall a (a_nonzero : a mod p <> 0),
   (exists b, b * b mod p = a) -> (a ^ x mod p = 1).
-Proof.
+Proof using Type*.
   intros ? ? a_square.
   destruct a_square as [b a_square].
   assert (b mod p <> 0) as b_nonzero. {
@@ -139,7 +139,7 @@ Lemma exists_primitive_root_power :
   (exists y, List.In y (FGroup.s (ZPGroup p lt_1_p))
   /\ EGroup.e_order Z.eq_dec y (ZPGroup p lt_1_p) = FGroup.g_order (ZPGroup p lt_1_p)
   /\ (forall a (a_range : 1 <= a <= p - 1), exists j, 0 <= j <= p - 1 /\ y ^ j mod p = a)).
-Proof.
+Proof using Type.
   intros.
   destruct (Zp_cyclic p lt_1_p prime_p) as [y [y_in_ZPGroup y_order]].
   exists y; repeat split; auto.
@@ -169,7 +169,7 @@ Ltac ereplace x := match type of x with ?t =>
 
 Lemma euler_criterion_square : forall a (a_range : 1 <= a <= p - 1)
   (pow_a_x : a ^ x mod p = 1), exists b, b * b mod p = a.
-Proof.
+Proof using Type*.
   intros.
   destruct (exists_primitive_root_power) as [y [in_ZPGroup_y [y_order gpow_y]]]; auto.
   destruct (gpow_y a a_range) as [j [j_range pow_y_j]]; clear gpow_y.
@@ -206,7 +206,7 @@ Qed.
 
 Lemma euler_criterion : forall a (a_range : 1 <= a <= p - 1),
   (a ^ x mod p = 1) <-> exists b, b * b mod p = a.
-Proof.
+Proof using Type*.
   intros; split. {
     exact (euler_criterion_square _ a_range).
   } {
@@ -218,7 +218,7 @@ Qed.
 
 Lemma euler_criterion_nonsquare : forall a (a_range : 1 <= a <= p - 1),
   (a ^ x mod p <> 1) <-> ~ (exists b, b * b mod p = a).
-Proof.
+Proof using Type*.
   split; intros A B; apply (euler_criterion a a_range) in B; congruence.
 Qed.
 
diff --git a/src/Util/Tuple.v b/src/Util/Tuple.v
index 03cb4492b..615410f2a 100644
--- a/src/Util/Tuple.v
+++ b/src/Util/Tuple.v
@@ -486,22 +486,22 @@ Local Ltac Equivalence_fieldwise'_t :=
 Section Equivalence.
   Context {A} {R:relation A}.
   Global Instance Reflexive_fieldwise' {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise' n R) | 5.
-  Proof. Equivalence_fieldwise'_t. Qed.
+  Proof using Type. Equivalence_fieldwise'_t. Qed.
   Global Instance Symmetric_fieldwise' {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise' n R) | 5.
-  Proof. Equivalence_fieldwise'_t. Qed.
+  Proof using Type. Equivalence_fieldwise'_t. Qed.
   Global Instance Transitive_fieldwise' {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise' n R) | 5.
-  Proof. Equivalence_fieldwise'_t. Qed.
+  Proof using Type. Equivalence_fieldwise'_t. Qed.
   Global Instance Equivalence_fieldwise' {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise' n R).
-  Proof. constructor; exact _. Qed.
+  Proof using Type. constructor; exact _. Qed.
 
   Global Instance Reflexive_fieldwise {R_Reflexive:Reflexive R} {n:nat} : Reflexive (fieldwise n R) | 5.
-  Proof. destruct n; (repeat constructor || exact _). Qed.
+  Proof using Type. destruct n; (repeat constructor || exact _). Qed.
   Global Instance Symmetric_fieldwise {R_Symmetric:Symmetric R} {n:nat} : Symmetric (fieldwise n R) | 5.
-  Proof. destruct n; (repeat constructor || exact _). Qed.
+  Proof using Type. destruct n; (repeat constructor || exact _). Qed.
   Global Instance Transitive_fieldwise {R_Transitive:Transitive R} {n:nat} : Transitive (fieldwise n R) | 5.
-  Proof. destruct n; (repeat constructor || exact _). Qed.
+  Proof using Type. destruct n; (repeat constructor || exact _). Qed.
   Global Instance Equivalence_fieldwise {R_equiv:Equivalence R} {n:nat} : Equivalence (fieldwise n R).
-  Proof. constructor; exact _. Qed.
+  Proof using Type. constructor; exact _. Qed.
 End Equivalence.
 
 Arguments fieldwise' {A B n} _ _ _.
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v
index b7c22c997..5e59daab9 100644
--- a/src/Util/ZUtil.v
+++ b/src/Util/ZUtil.v
@@ -3210,7 +3210,7 @@ for name in names:
     Proof. split; reflexivity. Qed.
 
     Lemma div_to_inv_modulo a x x' : x > 0 -> x * x' mod N = 1 mod N -> (a / x) == ((a - a mod x) * x').
-    Proof.
+    Proof using Type.
       intros H xinv.
       replace (a / x) with ((a / x) * 1) by lia.
       change (x * x' == 1) in xinv.