From 7125be2d478cc213e4317cbf200b25cd5fade783 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Thu, 18 Apr 2024 16:35:45 +0200 Subject: [PATCH] Adapt w.r.t. coq/coq#18909. (#1881) --- src/Algebra/Field.v | 6 +++--- src/Algebra/Group.v | 8 ++++---- src/Algebra/Hierarchy.v | 2 +- src/Algebra/IntegralDomain.v | 2 +- src/Algebra/Ring.v | 4 +++- src/Bedrock/End2End/RupicolaCrypto/ChaCha20.v | 2 +- src/Bedrock/Field/Synthesis/New/Signature.v | 2 +- .../Field/Translation/Proofs/EquivalenceProperties.v | 2 +- src/Bedrock/Field/Translation/Proofs/Func.v | 2 +- src/Spec/CompleteEdwardsCurve.v | 2 +- src/Util/Relations.v | 2 +- 11 files changed, 18 insertions(+), 16 deletions(-) diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index fa2635d93f..8ba0b28b9c 100644 --- 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 index 363099bf90..605ebdd8a9 100644 --- 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 index 8b1fd2eeb9..cb708de768 100644 --- 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 index bb2083bde5..7d334df47e 100644 --- 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 index 0757e2437b..c9f5a3f4b4 100644 --- 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 index c1a5313008..94b1a6edad 100644 --- 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 index 1aaac6b308..def9e8201b 100644 --- a/src/Bedrock/Field/Synthesis/New/Signature.v +++ b/src/Bedrock/Field/Synthesis/New/Signature.v @@ -172,7 +172,7 @@ Section WithParameters. | |- map word.unsigned ?x = map byte.unsigned _ => is_evar x; erewrite Util.map_unsigned_of_Z,MaxBounds.map_word_wrap_bounded - by eauto using byte_unsigned_within_max_bounds; + by (eapply byte_unsigned_within_max_bounds; eauto); reflexivity | _ => equivalence_side_conditions_hook end. diff --git a/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v b/src/Bedrock/Field/Translation/Proofs/EquivalenceProperties.v index 259d4fd799..664c431e4b 100644 --- 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 index 3e259d2ff0..0105402334 100644 --- 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 index 429eae5156..7b9732227b 100644 --- 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 index 179e46a719..d81f09f7f6 100644 --- 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}