Adapt w.r.t. coq/coq#18909.

mit-plv · Apr 17, 2024 · 7ea022b · 7ea022b
1 parent 64d2838
commit 7ea022b
Show file tree

Hide file tree

Showing 11 changed files with 19 additions and 15 deletions.
diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v
@@ -13,7 +13,7 @@ Section Field.
 
   Lemma right_multiplicative_inverse : forall x : T, ~ eq x zero -> eq (mul x (inv x)) one.
   Proof using Type*.
-    intros. rewrite commutative. auto using left_multiplicative_inverse.
+    intros. rewrite commutative. pose left_multiplicative_inverse; eauto.
   Qed.
 
   Lemma left_inv_unique x ix : ix * x = one -> ix = inv x.
@@ -72,7 +72,7 @@ Section Field.
 
   Global Instance integral_domain : @integral_domain T eq zero one opp add sub mul.
   Proof using Type*.
-    split; auto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
+    split; eauto using field_commutative_ring, field_is_zero_neq_one, is_mul_nonzero_nonzero.
   Qed.
 End Field.
 
@@ -90,7 +90,7 @@ Section Homomorphism.
     intros.
     eapply inv_unique.
     rewrite <-Ring.homomorphism_mul.
-    rewrite left_multiplicative_inverse; auto using Ring.homomorphism_one.
+    rewrite left_multiplicative_inverse; pose Ring.homomorphism_one; eauto.
   Qed.
 
   Lemma homomorphism_multiplicative_inverse_complete

diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v
@@ -10,13 +10,13 @@ Section BasicProperties.
   Local Open Scope eq_scope.
 
   Lemma cancel_left : forall z x y, z*x = z*y <-> x = y.
-  Proof using Type*. eauto using Monoid.cancel_left, left_inverse. Qed.
+  Proof using Type*. epose Monoid.cancel_left; epose left_inverse; eauto. Qed.
   Lemma cancel_right : forall z x y, x*z = y*z <-> x = y.
-  Proof using Type*. eauto using Monoid.cancel_right, right_inverse. Qed.
+  Proof using Type*. epose Monoid.cancel_right; epose right_inverse; eauto. Qed.
   Lemma inv_inv x : inv(inv(x)) = x.
-  Proof using Type*. eauto using Monoid.inv_inv, left_inverse. Qed.
+  Proof using Type*. epose Monoid.inv_inv; epose left_inverse; eauto. Qed.
   Lemma inv_op_ext x y : (inv y*inv x)*(x*y) =id.
-  Proof using Type*. eauto using Monoid.inv_op, left_inverse. Qed.
+  Proof using Type*. epose Monoid.inv_op; epose left_inverse; eauto. Qed.
 
   Lemma inv_unique x ix : ix * x = id -> ix = inv x.
   Proof using Type*.

diff --git a/src/Algebra/Hierarchy.v b/src/Algebra/Hierarchy.v
@@ -155,6 +155,6 @@ Section ZeroNeqOne.
 
   Lemma one_neq_zero : not (eq one zero).
   Proof using Type*.
-    intro HH; symmetry in HH. auto using zero_neq_one.
+    intro HH; symmetry in HH. epose zero_neq_one; auto.
   Qed.
 End ZeroNeqOne.
diff --git a/src/Algebra/IntegralDomain.v b/src/Algebra/IntegralDomain.v
@@ -16,7 +16,7 @@ Module IntegralDomain.
     Global Instance Integral_domain :
       @Integral_domain.Integral_domain T zero one add mul sub opp eq Ring.Ncring_Ring_ops
                                        Ring.Ncring_Ring Ring.Cring_Cring_commutative_ring.
-    Proof using Type. split; cbv; eauto using zero_product_zero_factor, one_neq_zero. Qed.
+    Proof using Type. split; cbv; pose zero_product_zero_factor; pose one_neq_zero; eauto. Qed.
   End IntegralDomain.
 
   Module _LargeCharacteristicReflective.

diff --git a/src/Algebra/Ring.v b/src/Algebra/Ring.v
@@ -19,7 +19,9 @@ Section Ring.
   Global Instance Ncring_Ring_ops : @Ncring.Ring_ops T zero one add mul sub opp eq := {}.
   Global Instance Ncring_Ring : @Ncring.Ring T zero one add mul sub opp eq Ncring_Ring_ops.
   Proof using Type*.
-    split; exact _ || cbv; intros; eauto using left_identity, right_identity, commutative, associative, right_inverse, left_distributive, right_distributive, ring_sub_definition with core typeclass_instances.
+    split; exact _ || cbv; intros;
+    pose left_identity; pose right_identity; pose commutative; pose associative; pose right_inverse; pose left_distributive; pose right_distributive; pose ring_sub_definition;
+    eauto with core typeclass_instances.
     - (* TODO: why does [eauto using @left_identity with typeclass_instances] not work? *)
       eapply @left_identity; eauto with typeclass_instances.
     - eapply @right_identity; eauto with typeclass_instances.

diff --git a/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v b/src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v
@@ -168,7 +168,7 @@ Lemma array_dexpr_locals_put
     map.get l x = None → Forall2 (DEXPR m l) exp w → Forall2 (DEXPR m #{ … l; x => v }#) exp w.
 Proof.
   induction 2; constructor;
-    eauto using dexpr_locals_put.
+    solve [eauto|epose dexpr_locals_put; eauto].
 Qed.
 
 (* we leave prior valiues abstract to support compound operations *)

diff --git a/src/Bedrock/Field/Synthesis/New/Signature.v b/src/Bedrock/Field/Synthesis/New/Signature.v
@@ -775,6 +775,8 @@ Section WithParameters.
       autounfold with equivalence pairs;
       rewrite <-?MakeAccessSizes.bytes_per_word_eq;
       sepsimpl; crush_sep; try solve [solve_equivalence_side_conditions].
+        erewrite Util.map_unsigned_of_Z, map_word_wrap_bounded; eauto
+        using byte_unsigned_within_max_bounds; reflexivity.
         change (Z.of_nat (bytes_per access_size.one)) with 1.
          try
           erewrite Util.map_unsigned_of_Z, map_word_wrap_bounded.

diff --git a/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v b/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v
@@ -53,7 +53,7 @@ Section OnlyDiffer.
   Proof.
     cbv [equivalent_base rep.equiv rep.Z WeakestPrecondition.dexpr].
     repeat intro; sepsimpl; subst; eexists; sepsimpl; eauto.
-    eauto using expr_only_differ_undef.
+    pose expr_only_differ_undef; eauto.
   Qed.
 
   Section Local.

diff --git a/src/Bedrock/Field/Translation/Proofs/Func.v b/src/Bedrock/Field/Translation/Proofs/Func.v
@@ -442,7 +442,7 @@ Section Func.
         pose proof H; apply map.only_differ_putmany in H
       end.
 
-      erewrite IHt1; eauto using only_differ_trans; [ |
+      erewrite IHt1; pose only_differ_trans; eauto ; [ |
         apply disjoint_union_l_iff; intuition trivial;
         symmetry; eapply NoDup_disjoint; eauto ].
       erewrite IHt2 by eauto using only_differ_trans.

diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v
@@ -32,7 +32,7 @@ Module E.
       end.
 
     Program Definition zero : point := (0, 1).
-    Next Obligation. eauto using Pre.onCurve_zero. Qed.
+    Next Obligation. pose Pre.onCurve_zero; eauto. Qed.
 
     Program Definition add (P1 P2:point) : point :=
       match coordinates P1, coordinates P2 return (F*F) with

diff --git a/src/Util/Relations.v b/src/Util/Relations.v
@@ -3,7 +3,7 @@ Require Import Crypto.Util.Logic.
 Require Import Coq.Classes.Morphisms Coq.Setoids.Setoid.
 
 Lemma symmetry_iff {T} {R} {Rsym:@Symmetric T R} x y: R x y <-> R y x.
-  intuition eauto using symmetry.
+  epose symmetry; intuition eauto.
 Qed.
 
 Lemma and_rewrite_l {A B} {RA RB} {Equivalence_RA:Equivalence RA} {Equivalence_RB:Equivalence RB}