Skip to content

Revert "Add overlay for #21098" #108

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Oct 21, 2025
Merged

Revert "Add overlay for #21098" #108

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion BigN/BigN.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
25 changes: 12 additions & 13 deletions BigQ/QMake.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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)).
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -723,15 +722,15 @@ 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.
rewrite Z2Pos.id by auto.
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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion BigZ/BigZ.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
39 changes: 19 additions & 20 deletions CyclicDouble/DoubleSqrt.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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;
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -1171,20 +1170,20 @@ 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.
intros H2; case (spec_ww_head1 (WW w0 w1)); intros H3 H4 H5.
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.
Expand Down Expand Up @@ -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.
Expand All @@ -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.
Expand All @@ -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)).
Expand All @@ -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.
Expand All @@ -1327,15 +1326,15 @@ 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.
apply Zdiv_le_upper_bound. zarith.
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.
Expand Down
2 changes: 1 addition & 1 deletion SpecViaQ/QSig.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
2 changes: 1 addition & 1 deletion SpecViaZ/NSigNAxioms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down
2 changes: 1 addition & 1 deletion SpecViaZ/ZSigZAxioms.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.

Expand Down
Loading