Skip to content

Commit 05e6ab6

Browse files
proux01proux01
authored
Merge pull request #107 from tabareau/sortpoly-equality
Add overlay for #21098
2 parents 93c065c + dd3e730 commit 05e6ab6

File tree

7 files changed

+38
-36
lines changed

7 files changed

+38
-36
lines changed

‎BigN/BigN.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -104,7 +104,7 @@ Lemma BigNdiv : div_theory BigN.eq BigN.add BigN.mul (@id _)
104104
(fun a b => if b =? 0 then (0,a) else BigN.div_eucl a b).
105105
Proof.
106106
constructor. unfold id. intros a b.
107-
BigN.zify.
107+
BigN.zify. autorewrite with nsimpl.
108108
case Z.eqb_spec.
109109
BigN.zify. auto with zarith.
110110
intros NEQ.

‎BigQ/QMake.v‎

Lines changed: 13 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -94,7 +94,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
9494
spec_Z_of_N spec_Zabs_N
9595
: nz.
9696

97-
Ltac nzsimpl := autorewrite with nz in *.
97+
Ltac nzsimpl := try rewrite_strat (repeat (topdown (hints nz))).
98+
Ltac nzsimpl_all := autorewrite with nz in *.
9899

99100
Ltac qsimpl := try red; unfold to_Q; simpl; intros;
100101
destr_eqb; simpl; nzsimpl; intros;
@@ -460,7 +461,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
460461
(ZZ.to_Z n' * g = ZZ.to_Z n)%Z /\ (NN.to_Z d' * g = NN.to_Z d)%Z.
461462
Proof.
462463
intros.
463-
unfold irred; nzsimpl; simpl.
464+
unfold irred. nzsimpl_all.
464465
destr_zcompare.
465466
exists 1%Z; nzsimpl; auto.
466467
exists 0%Z; nzsimpl.
@@ -508,7 +509,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
508509
let (n',d') := irred n d in Z.gcd (ZZ.to_Z n') (NN.to_Z d') = 1%Z.
509510
Proof.
510511
unfold irred; intros.
511-
nzsimpl.
512+
nzsimpl_all.
512513
destr_zcompare; simpl; auto.
513514
elim H.
514515
apply (Z.gcd_eq_0_r (ZZ.to_Z n)).
@@ -572,8 +573,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
572573
destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
573574
destruct Z_le_gt_dec.
574575
simpl; nzsimpl.
575-
destr_eqb; simpl; nzsimpl; auto with zarith.
576-
unfold norm_denum. destr_eqb; simpl; nzsimpl.
576+
destr_eqb; simpl; nzsimpl_all; auto with zarith.
577+
unfold norm_denum. destr_eqb; simpl; nzsimpl_all.
577578
rewrite Hd, Zdiv_0_l; discriminate.
578579
intros _.
579580
destr_eqb; simpl; nzsimpl; auto.
@@ -583,7 +584,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
583584
unfold mul_norm_Qz_Qq; nzsimpl; rewrite Zcompare_gt.
584585
destr_eqb; intros Hz; simpl; nzsimpl; simpl; auto.
585586
destruct Z_le_gt_dec as [H'|H'].
586-
simpl; nzsimpl.
587+
simpl; nzsimpl_all.
587588
destr_eqb; simpl; nzsimpl; auto.
588589
intros.
589590
rewrite Z2Pos.id; auto.
@@ -592,8 +593,8 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
592593
(Z.gcd_nonneg (ZZ.to_Z z) (NN.to_Z d)); lia.
593594
destr_eqb; simpl; nzsimpl; auto.
594595
unfold norm_denum.
595-
destr_eqb; nzsimpl; simpl; destr_eqb; simpl; auto.
596-
intros; nzsimpl.
596+
destr_eqb; nzsimpl_all; simpl; destr_eqb; simpl; auto.
597+
intros; nzsimpl_all.
597598
rewrite Z2Pos.id; auto.
598599
apply Zgcd_mult_rel_prime.
599600
apply Z.gcd_div_gcd.
@@ -722,15 +723,15 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
722723
simpl; nzsimpl; compute; auto.
723724
(* 0 < z *)
724725
simpl.
725-
destr_eqb; nzsimpl; [ intros; rewrite Z.abs_eq in *; lia | intros _ ].
726+
destr_eqb; nzsimpl_all; [ intros; rewrite Z.abs_eq in *; lia | intros _ ].
726727
set (z':=ZZ.to_Z z) in *; clearbody z'.
727728
red; simpl.
728729
rewrite Z.abs_eq by lia.
729730
rewrite Z2Pos.id by auto.
730731
unfold Qinv; simpl; destruct z'; simpl; auto; discriminate.
731732
(* 0 > z *)
732733
simpl.
733-
destr_eqb; nzsimpl; [ intros; rewrite Z.abs_neq in *; lia | intros _ ].
734+
destr_eqb; nzsimpl_all; [ intros; rewrite Z.abs_neq in *; lia | intros _ ].
734735
set (z':=ZZ.to_Z z) in *; clearbody z'.
735736
red; simpl.
736737
rewrite Z.abs_neq by lia.
@@ -745,7 +746,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
745746
destr_eqb; intros; compute; auto.
746747
(* 0 < n *)
747748
simpl.
748-
destr_eqb; nzsimpl; intros.
749+
destr_eqb; nzsimpl_all; intros.
749750
intros; rewrite Z.abs_eq in *; lia.
750751
intros; rewrite Z.abs_eq in *; lia.
751752
nsubst; compute; auto.
@@ -757,7 +758,7 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
757758
rewrite Pos2Z.inj_mul, Z2Pos.id; auto.
758759
(* 0 > n *)
759760
simpl.
760-
destr_eqb; nzsimpl; intros.
761+
destr_eqb; nzsimpl_all; intros.
761762
intros; rewrite Z.abs_neq in *; lia.
762763
intros; rewrite Z.abs_neq in *; lia.
763764
nsubst; compute; auto.

‎BigZ/BigZ.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -134,7 +134,7 @@ Lemma BigZdiv : div_theory BigZ.eq BigZ.add BigZ.mul (@id _)
134134
(fun a b => if b =? 0 then (0,a) else BigZ.div_eucl a b).
135135
Proof.
136136
constructor. unfold id. intros a b.
137-
BigZ.zify.
137+
BigZ.zify. autorewrite with zsimpl.
138138
case Z.eqb_spec.
139139
BigZ.zify. auto with zarith.
140140
intros NEQ.

‎CyclicDouble/DoubleSqrt.v‎

Lines changed: 20 additions & 19 deletions
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ Require Import DoubleBase.
1818
Local Open Scope Z_scope.
1919

2020
Ltac zarith := auto with zarith; fail.
21+
Ltac rm10 := try (rewrite_strat (repeat (topdown (hints rm10)))).
2122

2223
Section DoubleSqrt.
2324
Variable w : univ_of_cycles.
@@ -445,7 +446,7 @@ intros x; case x; simpl ww_is_even.
445446
end.
446447
apply Z.pow_pos_nonneg; lia.
447448
}
448-
unfold ww_digits; autorewrite with rm10.
449+
unfold ww_digits; rm10.
449450
assert (tmp: forall p q r, p + (q - r) = p + q - r) by zarith;
450451
rewrite tmp; clear tmp.
451452
assert (tmp: forall p, p + p = 2 * p) by zarith;
@@ -821,9 +822,9 @@ intros x; case x; simpl ww_is_even.
821822
assert (V1 := spec_ww_to_Z w_digits w_to_Z spec_to_Z (WW w4 w5)).
822823
enough (0 < [[WW w4 w5]]) by zarith.
823824
apply Z.lt_le_trans with (wB/ 2 * wB + 0).
824-
autorewrite with rm10; apply Z.mul_pos_pos.
825+
rm10; apply Z.mul_pos_pos.
825826
apply Z.mul_lt_mono_pos_r with 2. zarith.
826-
autorewrite with rm10.
827+
rm10.
827828
rewrite Z.mul_comm; rewrite wB_div_2.
828829
case (spec_to_Z w5);zarith.
829830
case (spec_to_Z w5);zarith.
@@ -849,9 +850,9 @@ intros x; case x; simpl ww_is_even.
849850
rename V1 into VV1.
850851
assert (VV2: 0 < [[WW w4 w5]]).
851852
apply Z.lt_le_trans with (wB/ 2 * wB + 0).
852-
autorewrite with rm10; apply Z.mul_pos_pos.
853+
rm10; apply Z.mul_pos_pos.
853854
apply Z.mul_lt_mono_pos_r with 2. zarith.
854-
autorewrite with rm10.
855+
rm10.
855856
rewrite Z.mul_comm, wB_div_2.
856857
assert (VV3 := spec_to_Z w5);zarith.
857858
assert (VV3 := spec_to_Z w5);zarith.
@@ -942,7 +943,7 @@ intros x; case x; simpl ww_is_even.
942943
end.
943944
assert (V := Zsquare_pos [|w5|]);
944945
rewrite Zsquare_mult in V; zarith.
945-
autorewrite with rm10.
946+
rm10.
946947
match goal with |- _ <= 2 * (?U * ?V + ?W) =>
947948
apply Z.le_trans with (2 * U * V + 0)
948949
end.
@@ -989,7 +990,7 @@ intros x; case x; simpl ww_is_even.
989990
end.
990991
assert (V1 := Zsquare_pos [|w5|]);
991992
rewrite Zsquare_mult in V1; zarith.
992-
autorewrite with rm10.
993+
rm10.
993994
match goal with |- _ <= 2 * (?U * ?V + ?W) =>
994995
apply Z.le_trans with (2 * U * V + 0)
995996
end.
@@ -1031,9 +1032,9 @@ intros x; case x; simpl ww_is_even.
10311032
match goal with |- _ <= _ * ?X =>
10321033
apply Z.le_trans with (1 * X); [ | zarith ]
10331034
end.
1034-
autorewrite with rm10.
1035+
rm10.
10351036
rewrite <- wB_div_2; apply Z.mul_le_mono_nonneg_l; zarith.
1036-
* rewrite <- V3 in VV; generalize VV; autorewrite with rm10;
1037+
* rewrite <- V3 in VV; generalize VV; rm10;
10371038
clear VV; intros VV.
10381039
rewrite spec_ww_add_c by zarith.
10391040
rewrite ww_add_mult_mult_2_plus_1.
@@ -1108,7 +1109,7 @@ Qed.
11081109
generalize (spec_ww_is_even (ww_head0 x)); case_eq (ww_is_even (ww_head0 x)).
11091110
intros HH H1; rewrite HH; split; auto.
11101111
intros H2.
1111-
generalize (spec_ww_head0 x H2); case (ww_head0 x); autorewrite with rm10.
1112+
generalize (spec_ww_head0 x H2); case (ww_head0 x); rm10.
11121113
intros (H3, H4); split. 2: zarith.
11131114
apply Z.le_trans with (2 := H3).
11141115
apply Zdiv_le_compat_l; zarith.
@@ -1170,20 +1171,20 @@ Qed.
11701171
zarith.
11711172
intros H1.
11721173
rewrite spec_ww_compare. case Z.compare_spec;
1173-
simpl ww_to_Z; autorewrite with rm10.
1174+
simpl ww_to_Z; rm10.
11741175
generalize H1; case x.
11751176
intros HH; contradict HH; simpl ww_to_Z; zarith.
11761177
intros w0 w1; simpl ww_to_Z; autorewrite with w_rewrite rm10.
11771178
intros H2; case (spec_ww_head1 (WW w0 w1)); intros H3 H4 H5.
11781179
generalize (H4 H2); clear H4; rewrite H5; clear H5; autorewrite with rm10.
11791180
intros (H4, H5).
11801181
assert (V: wB/4 <= [|w0|]). {
1181-
apply beta_lex with 0 [|w1|] wB. 2-3: zarith. autorewrite with rm10.
1182+
apply beta_lex with 0 [|w1|] wB. 2-3: zarith. rm10.
11821183
rewrite <- wwB_4_wB_4; auto. }
11831184
generalize (@spec_w_sqrt2 w0 w1 V).
11841185
case (w_sqrt2 w0 w1); intros w2 c.
11851186
simpl ww_to_Z; simpl @fst.
1186-
case c; unfold interp_carry; autorewrite with rm10.
1187+
case c; unfold interp_carry; rm10.
11871188
intros w3 (H6, H7); rewrite H6.
11881189
assert (V1 := spec_to_Z w3).
11891190
split. zarith.
@@ -1235,7 +1236,7 @@ Qed.
12351236
by (rewrite Z.mul_comm; zarith).
12361237
intros H2.
12371238
assert (V: wB/4 <= [|w0|]). {
1238-
apply beta_lex with 0 [|w1|] wB. 2: zarith. autorewrite with rm10.
1239+
apply beta_lex with 0 [|w1|] wB. 2: zarith. rm10.
12391240
simpl ww_to_Z in H2; rewrite H2.
12401241
rewrite <- wwB_4_wB_4 by zarith.
12411242
rewrite Z.mul_comm; zarith.
@@ -1260,7 +1261,7 @@ Qed.
12601261
assert (Hv5: [[(ww_add_mul_div (ww_pred ww_zdigits) W0 (ww_head1 x))]]
12611262
= [[ww_head1 x]]/2).
12621263
rewrite spec_ww_add_mul_div.
1263-
simpl ww_to_Z; autorewrite with rm10.
1264+
simpl ww_to_Z; rm10.
12641265
rewrite Hv3.
12651266
ring_simplify (Zpos (xO w_digits) - (Zpos (xO w_digits) - 1)).
12661267
rewrite Z.pow_1_r.
@@ -1277,7 +1278,7 @@ Qed.
12771278
rewrite spec_w_add_mul_div.
12781279
rewrite spec_w_sub.
12791280
rewrite spec_w_0.
1280-
simpl ww_to_Z; autorewrite with rm10.
1281+
simpl ww_to_Z; rm10.
12811282
rewrite Hv6; rewrite spec_w_zdigits.
12821283
rewrite (fun x y => Zmod_small (x - y)).
12831284
ring_simplify (Zpos w_digits - (Zpos w_digits - [[ww_head1 x]] / 2)).
@@ -1304,7 +1305,7 @@ Qed.
13041305
enough (0 <= Y) by zarith
13051306
end.
13061307
case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]] / 2))); zarith.
1307-
case c; unfold interp_carry; autorewrite with rm10;
1308+
case c; unfold interp_carry; rm10;
13081309
intros w3; assert (V3 := spec_to_Z w3);zarith.
13091310
apply Z.mul_lt_mono_pos_r with (2 ^ [[ww_head1 x]]). zarith.
13101311
rewrite H4.
@@ -1326,15 +1327,15 @@ Qed.
13261327
pattern [|w2|] at 1; rewrite (Z_div_mod_eq_full [|w2|] (2 ^ ([[ww_head1 x]]/2))) by
13271328
zarith.
13281329
rewrite <- Z.add_assoc; rewrite Z.mul_add_distr_l.
1329-
autorewrite with rm10; apply Z.add_le_mono_l.
1330+
rm10; apply Z.add_le_mono_l.
13301331
case (Z_mod_lt [|w2|] (2 ^ ([[ww_head1 x]]/2))); zarith.
13311332
split. zarith.
13321333
apply Z.le_lt_trans with ([|w2|]). 2: zarith.
13331334
apply Zdiv_le_upper_bound. zarith.
13341335
pattern [|w2|] at 1; replace [|w2|] with ([|w2|] * 2 ^0).
13351336
apply Z.mul_le_mono_nonneg_l. zarith.
13361337
apply Zpower_le_monotone; zarith.
1337-
rewrite Z.pow_0_r; autorewrite with rm10; auto.
1338+
rewrite Z.pow_0_r; rm10; auto.
13381339
split.
13391340
rewrite Hv0 in Hv2; rewrite (Pos2Z.inj_xO w_digits) in Hv2; zarith.
13401341
apply Z.le_lt_trans with (Zpos w_digits). zarith.

‎SpecViaQ/QSig.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -102,7 +102,7 @@ Hint Rewrite
102102
spec_red spec_compare spec_eq_bool spec_min spec_max
103103
spec_add spec_sub spec_opp spec_mul spec_square spec_inv spec_div
104104
spec_power : qsimpl.
105-
Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl;
105+
Ltac qify := unfold eq, lt, le in *; try (rewrite_strat (repeat (topdown (hints qsimpl))));
106106
try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *.
107107

108108
(** NB: do not add [spec_0] in the autorewrite database. Otherwise,

‎SpecViaZ/NSigNAxioms.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@ Hint Rewrite
2121
spec_pow spec_even spec_odd spec_testbit spec_shiftl spec_shiftr
2222
spec_land spec_lor spec_ldiff spec_lxor spec_div2 spec_of_N
2323
: nsimpl.
24-
Ltac nsimpl := autorewrite with nsimpl.
24+
Ltac nsimpl := try (rewrite_strat (repeat (topdown (hints nsimpl)))).
2525
Ltac ncongruence := unfold eq, to_N; repeat red; intros; nsimpl; congruence.
2626
Ltac zify := unfold eq, lt, le, to_N in *; nsimpl.
2727
Ltac omega_pos n := generalize (spec_pos n); lia.

‎SpecViaZ/ZSigZAxioms.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,7 @@ Hint Rewrite
2323
spec_land spec_lor spec_ldiff spec_lxor spec_div2
2424
: zsimpl.
2525

26-
Ltac zsimpl := autorewrite with zsimpl.
26+
Ltac zsimpl := try (rewrite_strat (repeat (topdown (hints zsimpl)))).
2727
Ltac zcongruence := repeat red; intros; zsimpl; congruence.
2828
Ltac zify := unfold eq, lt, le in *; zsimpl.
2929

0 commit comments

Comments
 (0)