From 95b345084e55c24c585607492a17e51c2bc22e94 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. --- 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/LegacyArithmetic/BarretReduction.v | 2 +- src/LegacyArithmetic/MontgomeryReduction.v | 16 ++++++++-------- src/Spec/CompleteEdwardsCurve.v | 2 +- src/Util/Relations.v | 2 +- 9 files changed, 23 insertions(+), 21 deletions(-) diff --git a/src/Algebra/Field.v b/src/Algebra/Field.v index b3dedd145d..7238af5e63 100644 --- a/src/Algebra/Field.v +++ b/src/Algebra/Field.v @@ -20,7 +20,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. @@ -79,7 +79,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. @@ -137,7 +137,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 1f1ed0d950..8384941810 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 9c9e93eeab..d58be9c8ef 100644 --- a/src/Algebra/Hierarchy.v +++ b/src/Algebra/Hierarchy.v @@ -156,7 +156,7 @@ 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 708fdfbeb7..bfdc36bd68 100644 --- a/src/Algebra/IntegralDomain.v +++ b/src/Algebra/IntegralDomain.v @@ -17,7 +17,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 9ca06fd163..3190c42677 100644 --- a/src/Algebra/Ring.v +++ b/src/Algebra/Ring.v @@ -96,7 +96,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/LegacyArithmetic/BarretReduction.v b/src/LegacyArithmetic/BarretReduction.v index 48f4094baa..4c82eb2f42 100644 --- a/src/LegacyArithmetic/BarretReduction.v +++ b/src/LegacyArithmetic/BarretReduction.v @@ -33,7 +33,7 @@ Section barrett. /\ small_valid barrett_reduce }. Proof. intro x. evar (pr : SmallT); exists pr. intros x_valid. - assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid. + assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by eauto using decode_medium_valid. assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; lia). assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith lia. rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by lia. diff --git a/src/LegacyArithmetic/MontgomeryReduction.v b/src/LegacyArithmetic/MontgomeryReduction.v index 3b788a4be7..3cd89c5b7f 100644 --- a/src/LegacyArithmetic/MontgomeryReduction.v +++ b/src/LegacyArithmetic/MontgomeryReduction.v @@ -41,10 +41,10 @@ Section montgomery. /\ small_valid partial_reduce }. Proof. intro T. evar (pr : SmallT); exists pr. intros T_valid. - assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid. - assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid. - assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid. - assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid. + assert (0 <= decode_large T < small_bound * small_bound) by eauto using decode_large_valid. + assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by eauto using decode_small_valid, Mod_SmallBound_valid. + assert (0 <= decode_small modulus' < small_bound) by eauto using decode_small_valid. + assert (0 <= decode_small modulus_digits < small_bound) by eauto using decode_small_valid, modulus_digits_valid. assert (0 <= modulus) by apply (modulus_nonneg _). assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; lia). rewrite <- partial_reduce_alt_eq by lia. @@ -61,10 +61,10 @@ Section montgomery. /\ small_valid reduce }. Proof. intro T. evar (pr : SmallT); exists pr. intros T_valid. - assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid. - assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid. - assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid. - assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid. + assert (0 <= decode_large T < small_bound * small_bound) by eauto using decode_large_valid. + assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by eauto using decode_small_valid, Mod_SmallBound_valid. + assert (0 <= decode_small modulus' < small_bound) by eauto using decode_small_valid. + assert (0 <= decode_small modulus_digits < small_bound) by eauto using decode_small_valid, modulus_digits_valid. assert (0 <= modulus) by apply (modulus_nonneg _). assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; lia). unfold reduce_via_partial. diff --git a/src/Spec/CompleteEdwardsCurve.v b/src/Spec/CompleteEdwardsCurve.v index de3bbb0114..de2cf38234 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 955ecc60f7..156f85475e 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.Classes.Morphisms_Prop 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}