From 9005d2d1bd80661e777f858e9dfc14cc411b687f Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 21 Oct 2025 15:29:10 +0200 Subject: [PATCH] Revert "Add overlay for #21098" This reverts commit dd3e7306ca1f7f93c06122723c9fcd06463373e9. --- BigN/BigN.v | 2 +- BigQ/QMake.v | 25 ++++++++++++------------- BigZ/BigZ.v | 2 +- CyclicDouble/DoubleSqrt.v | 39 +++++++++++++++++++-------------------- SpecViaQ/QSig.v | 2 +- SpecViaZ/NSigNAxioms.v | 2 +- SpecViaZ/ZSigZAxioms.v | 2 +- 7 files changed, 36 insertions(+), 38 deletions(-) diff --git a/BigN/BigN.v b/BigN/BigN.v index 1c18b5a..fff3d4b 100644 --- a/BigN/BigN.v +++ b/BigN/BigN.v @@ -104,7 +104,7 @@ Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _) (fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b). Proof. constructor. unfold id. intros a b. -BigN.zify. autorewrite with nsimpl. +BigN.zify. case Z.eqb_spec. BigN.zify. auto with zarith. intros NEQ. diff --git a/BigQ/QMake.v b/BigQ/QMake.v index 867f5b6..a6f4787 100644 --- a/BigQ/QMake.v +++ b/BigQ/QMake.v @@ -94,8 +94,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. spec_Z_of_N spec_Zabs_N : nz. - Ltac nzsimpl := try rewrite_strat (repeat (topdown (hints nz))). - Ltac nzsimpl_all := autorewrite with nz in *. + Ltac nzsimpl := autorewrite with nz in *. Ltac qsimpl := try red; unfold to_Q; simpl; intros; destr_eqb; simpl; nzsimpl; intros; @@ -461,7 +460,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. (ZZ.to_Z n' * g = ZZ.to_Z n)%Z /\ (NN.to_Z d' * g = NN.to_Z d)%Z. Proof. intros. - unfold irred. nzsimpl_all. + unfold irred; nzsimpl; simpl. destr_zcompare. exists 1%Z; nzsimpl; auto. exists 0%Z; nzsimpl. @@ -509,7 +508,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. let (n',d') := irred n d in Z.gcd (ZZ.to_Z n') (NN.to_Z d') = 1%Z. Proof. unfold irred; intros. - nzsimpl_all. + nzsimpl. destr_zcompare; simpl; auto. elim H. apply (Z.gcd_eq_0_r (ZZ.to_Z n)). @@ -573,8 +572,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. destruct Z_le_gt_dec. simpl; nzsimpl. - destr_eqb; simpl; nzsimpl_all; auto with zarith. - unfold norm_denum. destr_eqb; simpl; nzsimpl_all. + destr_eqb; simpl; nzsimpl; auto with zarith. + unfold norm_denum. destr_eqb; simpl; nzsimpl. rewrite Hd, Zdiv_0_l; discriminate. intros _. destr_eqb; simpl; nzsimpl; auto. @@ -584,7 +583,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt. destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto. destruct Z_le_gt_dec as [H'|H']. - simpl; nzsimpl_all. + simpl; nzsimpl. destr_eqb; simpl; nzsimpl; auto. intros. rewrite Z2Pos.id; auto. @@ -593,8 +592,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. (Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); lia. destr_eqb; simpl; nzsimpl; auto. unfold norm_denum. - destr_eqb; nzsimpl_all; simpl; destr_eqb; simpl; auto. - intros; nzsimpl_all. + destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto. + intros; nzsimpl. rewrite Z2Pos.id; auto. apply Zgcd_mult_rel_prime. apply Z.gcd_div_gcd. @@ -723,7 +722,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. simpl; nzsimpl; compute; auto. (* 0 < z *) simpl. - destr_eqb; nzsimpl_all; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ]. set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. rewrite Z.abs_eq by lia. @@ -731,7 +730,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. unfold Qinv; simpl; destruct z'; simpl; auto; discriminate. (* 0 > z *) simpl. - destr_eqb; nzsimpl_all; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. + destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; lia | intros _ ]. set (z':=ZZ.to_Z z) in *; clearbody z'. red; simpl. rewrite Z.abs_neq by lia. @@ -746,7 +745,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. destr_eqb; intros; compute; auto. (* 0 < n *) simpl. - destr_eqb; nzsimpl_all; intros. + destr_eqb; nzsimpl; intros. intros; rewrite Z.abs_eq in *; lia. intros; rewrite Z.abs_eq in *; lia. nsubst; compute; auto. @@ -758,7 +757,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType. rewrite Pos2Z.inj_mul, Z2Pos.id; auto. (* 0 > n *) simpl. - destr_eqb; nzsimpl_all; intros. + destr_eqb; nzsimpl; intros. intros; rewrite Z.abs_neq in *; lia. intros; rewrite Z.abs_neq in *; lia. nsubst; compute; auto. diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v index 9fa321a..b8be51a 100644 --- a/BigZ/BigZ.v +++ b/BigZ/BigZ.v @@ -134,7 +134,7 @@ Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _) (fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b). Proof. constructor. unfold id. intros a b. -BigZ.zify. autorewrite with zsimpl. +BigZ.zify. case Z.eqb_spec. BigZ.zify. auto with zarith. intros NEQ. diff --git a/CyclicDouble/DoubleSqrt.v b/CyclicDouble/DoubleSqrt.v index b13c0cb..1d7724b 100644 --- a/CyclicDouble/DoubleSqrt.v +++ b/CyclicDouble/DoubleSqrt.v @@ -18,7 +18,6 @@ Require Import DoubleBase. Local Open Scope Z_scope. Ltac zarith := auto with zarith; fail. -Ltac rm10 := try (rewrite_strat (repeat (topdown (hints rm10)))). Section DoubleSqrt. Variable w : univ_of_cycles. @@ -446,7 +445,7 @@ intros x; case x; simpl ww_is_even. end. apply Z.pow_pos_nonneg; lia. } - unfold ww_digits; rm10. + unfold ww_digits; autorewrite with rm10. assert (tmp: forall p q r, p + (q - r) = p + q - r) by zarith; rewrite tmp; clear tmp. assert (tmp: forall p, p + p = 2 * p) by zarith; @@ -822,9 +821,9 @@ intros x; case x; simpl ww_is_even. assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)). enough (0 < [[WW w4 w5]]) by zarith. apply Z.lt_le_trans with (wB/ 2 * wB + 0). - rm10; apply Z.mul_pos_pos. + autorewrite with rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. - rm10. + autorewrite with rm10. rewrite Z.mul_comm; rewrite wB_div_2. case (spec_to_Z w5);zarith. case (spec_to_Z w5);zarith. @@ -850,9 +849,9 @@ intros x; case x; simpl ww_is_even. rename V1 into VV1. assert (VV2: 0 < [[WW w4 w5]]). apply Z.lt_le_trans with (wB/ 2 * wB + 0). - rm10; apply Z.mul_pos_pos. + autorewrite with rm10; apply Z.mul_pos_pos. apply Z.mul_lt_mono_pos_r with 2. zarith. - rm10. + autorewrite with rm10. rewrite Z.mul_comm, wB_div_2. assert (VV3 := spec_to_Z w5);zarith. assert (VV3 := spec_to_Z w5);zarith. @@ -943,7 +942,7 @@ intros x; case x; simpl ww_is_even. end. assert (V := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V; zarith. - rm10. + autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. @@ -990,7 +989,7 @@ intros x; case x; simpl ww_is_even. end. assert (V1 := Zsquare_pos [|w5|]); rewrite Zsquare_mult in V1; zarith. - rm10. + autorewrite with rm10. match goal with |- _ <= 2 * (?U * ?V + ?W) => apply Z.le_trans with (2 * U * V + 0) end. @@ -1032,9 +1031,9 @@ intros x; case x; simpl ww_is_even. match goal with |- _ <= _ * ?X => apply Z.le_trans with (1 * X); [ | zarith ] end. - rm10. + autorewrite with rm10. rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith. - * rewrite <- V3 in VV; generalize VV; rm10; + * rewrite <- V3 in VV; generalize VV; autorewrite with rm10; clear VV; intros VV. rewrite spec_ww_add_c by zarith. rewrite ww_add_mult_mult_2_plus_1. @@ -1109,7 +1108,7 @@ Qed. generalize (spec_ww_is_even (ww_head0 x)); case_eq (ww_is_even (ww_head0 x)). intros HH H1; rewrite HH; split; auto. intros H2. - generalize (spec_ww_head0 x H2); case (ww_head0 x); rm10. + generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10. intros (H3, H4); split. 2: zarith. apply Z.le_trans with (2 := H3). apply Zdiv_le_compat_l; zarith. @@ -1171,7 +1170,7 @@ Qed. zarith. intros H1. rewrite spec_ww_compare. case Z.compare_spec; - simpl ww_to_Z; rm10. + simpl ww_to_Z; autorewrite with rm10. generalize H1; case x. intros HH; contradict HH; simpl ww_to_Z; zarith. intros w0 w1; simpl ww_to_Z; autorewrite with w_rewrite rm10. @@ -1179,12 +1178,12 @@ Qed. generalize (H4 H2); clear H4; rewrite H5; clear H5; autorewrite with rm10. intros (H4, H5). assert (V: wB/4 <= [|w0|]). { - apply beta_lex with 0 [|w1|] wB. 2-3: zarith. rm10. + apply beta_lex with 0 [|w1|] wB. 2-3: zarith. autorewrite with rm10. rewrite <- wwB_4_wB_4; auto. } generalize (@spec_w_sqrt2 w0 w1 V). case (w_sqrt2 w0 w1); intros w2 c. simpl ww_to_Z; simpl @fst. - case c; unfold interp_carry; rm10. + case c; unfold interp_carry; autorewrite with rm10. intros w3 (H6, H7); rewrite H6. assert (V1 := spec_to_Z w3). split. zarith. @@ -1236,7 +1235,7 @@ Qed. by (rewrite Z.mul_comm; zarith). intros H2. assert (V: wB/4 <= [|w0|]). { - apply beta_lex with 0 [|w1|] wB. 2: zarith. rm10. + apply beta_lex with 0 [|w1|] wB. 2: zarith. autorewrite with rm10. simpl ww_to_Z in H2; rewrite H2. rewrite <- wwB_4_wB_4 by zarith. rewrite Z.mul_comm; zarith. @@ -1261,7 +1260,7 @@ Qed. assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]] = [[ww_head1 x]]/2). rewrite spec_ww_add_mul_div. - simpl ww_to_Z; rm10. + simpl ww_to_Z; autorewrite with rm10. rewrite Hv3. ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)). rewrite Z.pow_1_r. @@ -1278,7 +1277,7 @@ Qed. rewrite spec_w_add_mul_div. rewrite spec_w_sub. rewrite spec_w_0. - simpl ww_to_Z; rm10. + simpl ww_to_Z; autorewrite with rm10. rewrite Hv6; rewrite spec_w_zdigits. rewrite (fun x y => Zmod_small (x - y)). ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)). @@ -1305,7 +1304,7 @@ Qed. enough (0 <= Y) by zarith end. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); zarith. - case c; unfold interp_carry; rm10; + case c; unfold interp_carry; autorewrite with rm10; intros w3; assert (V3 := spec_to_Z w3);zarith. apply Z.mul_lt_mono_pos_r with (2 ^ [[ww_head1 x]]). zarith. rewrite H4. @@ -1327,7 +1326,7 @@ Qed. pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] (2 ^ ([[ww_head1 x]]/2))) by zarith. rewrite <- Z.add_assoc; rewrite Z.mul_add_distr_l. - rm10; apply Z.add_le_mono_l. + autorewrite with rm10; apply Z.add_le_mono_l. case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); zarith. split. zarith. apply Z.le_lt_trans with ([|w2|]). 2: zarith. @@ -1335,7 +1334,7 @@ Qed. pattern [|w2|] at 1; replace [|w2|] with ([|w2|] * 2 ^0). apply Z.mul_le_mono_nonneg_l. zarith. apply Zpower_le_monotone; zarith. - rewrite Z.pow_0_r; rm10; auto. + rewrite Z.pow_0_r; autorewrite with rm10; auto. split. rewrite Hv0 in Hv2; rewrite (Pos2Z.inj_xO w_digits) in Hv2; zarith. apply Z.le_lt_trans with (Zpos w_digits). zarith. diff --git a/SpecViaQ/QSig.v b/SpecViaQ/QSig.v index cdcda82..d994090 100644 --- a/SpecViaQ/QSig.v +++ b/SpecViaQ/QSig.v @@ -102,7 +102,7 @@ Hint Rewrite spec_red spec_compare spec_eq_bool spec_min spec_max spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div spec_power : qsimpl. -Ltac qify := unfold eq, lt, le in *; try (rewrite_strat (repeat (topdown (hints qsimpl)))); +Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl; try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *. (** NB: do not add [spec_0] in the autorewrite database. Otherwise, diff --git a/SpecViaZ/NSigNAxioms.v b/SpecViaZ/NSigNAxioms.v index 035ca08..4d24b0b 100644 --- a/SpecViaZ/NSigNAxioms.v +++ b/SpecViaZ/NSigNAxioms.v @@ -21,7 +21,7 @@ Hint Rewrite spec_pow spec_even spec_odd spec_testbit spec_shiftl spec_shiftr spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N : nsimpl. -Ltac nsimpl := try (rewrite_strat (repeat (topdown (hints nsimpl)))). +Ltac nsimpl := autorewrite with nsimpl. Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence. Ltac zify := unfold eq, lt, le, to_N in *; nsimpl. Ltac omega_pos n := generalize (spec_pos n); lia. diff --git a/SpecViaZ/ZSigZAxioms.v b/SpecViaZ/ZSigZAxioms.v index 4ac48de..97f50bd 100644 --- a/SpecViaZ/ZSigZAxioms.v +++ b/SpecViaZ/ZSigZAxioms.v @@ -23,7 +23,7 @@ Hint Rewrite spec_land spec_lor spec_ldiff spec_lxor spec_div2 : zsimpl. -Ltac zsimpl := try (rewrite_strat (repeat (topdown (hints zsimpl)))). +Ltac zsimpl := autorewrite with zsimpl. Ltac zcongruence := repeat red; intros; zsimpl; congruence. Ltac zify := unfold eq, lt, le in *; zsimpl.