Skip to content

Commit a66d00f

Browse files
proux01proux01
authored
Merge pull request #120 from proux01/reworder
Port to new rewrite goals order
2 parents 3a5a26c + c095c08 commit a66d00f

52 files changed

Lines changed: 469 additions & 487 deletions

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

‎refinements/bareiss_eff.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,7 +9,7 @@ From CoqEAL Require Import minor hrel param refinements seqmx.
99
Import GRing.Theory Pdiv.Ring Pdiv.CommonRing Pdiv.RingMonic.
1010
Import Refinements.Op.
1111

12-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
12+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1313

1414
Set Implicit Arguments.
1515
Unset Strict Implicit.

‎refinements/binint.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,7 @@ From CoqEAL Require Import hrel param refinements pos.
1717
(* *)
1818
(******************************************************************************)
1919

20-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
20+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
2121

2222
Set Implicit Arguments.
2323
Unset Strict Implicit.
@@ -234,8 +234,8 @@ Proof.
234234
rewrite -[((_<=_)%N)]/(_<=_)%C => ->.
235235
by rewrite /= -subzn.
236236
rewrite [((_<=_)%C)]/(_<=_)%N ifN_eq=> /=.
237-
by rewrite insubdK -?topredE /= ?subn_gt0 // -?subzn 1?ltnW // opprB.
238-
by have := nm; rewrite lt0n_neq0 // subn_gt0.
237+
by have := nm; rewrite lt0n_neq0 // subn_gt0.
238+
by rewrite insubdK -?topredE /= ?subn_gt0 // -?subzn 1?ltnW // opprB.
239239
Qed.
240240

241241
Local Instance Rint_add : refines (Rint ==> Rint ==> Rint) +%R +%C.

‎refinements/binnat.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ From CoqEAL Require Import hrel param refinements pos.
1212
(* *)
1313
(******************************************************************************)
1414

15-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
15+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1616

1717
Set Implicit Arguments.
1818
Unset Strict Implicit.
@@ -437,12 +437,12 @@ simpl.
437437
case: n => [|n]; last case: n => [|n]; last by rewrite IHm.
438438
- rewrite subn0 IHm.
439439
have->: (m.*2.+1 - m = m.+1)%N.
440-
rewrite -addnn subSn; first by rewrite addnK.
440+
rewrite -addnn subSn; last by rewrite addnK.
441441
exact: leq_addr.
442442
by rewrite !(maxn_idPr _) // Nat2Pos_xI.
443443
- rewrite subn1 IHm.
444444
have->: (m.*2.+1 - m = m.+1)%N.
445-
rewrite -addnn subSn; first by rewrite addnK.
445+
rewrite -addnn subSn; last by rewrite addnK.
446446
exact: leq_addr.
447447
by rewrite !(maxn_idPr _) // Nat2Pos_xO.
448448
Qed.

‎refinements/binord.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ From mathcomp Require Import path choice fintype tuple finset ssralg ssrnum bigo
55

66
From CoqEAL Require Import hrel param refinements binnat.
77

8-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
8+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
99
Set Implicit Arguments.
1010
Unset Strict Implicit.
1111
Unset Printing Implicit Defensive.

‎refinements/binrat.v‎

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat order.
66
From mathcomp Require Import ssralg ssrnum ssrint rat div intdiv.
77
From CoqEAL.refinements Require Import hrel refinements param binint.
88
Import Refinements.Op.
9-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
9+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1010

1111
Set Implicit Arguments.
1212
Unset Strict Implicit.
@@ -133,7 +133,7 @@ rewrite /Z2int /GRing.add /= /intZmod.addz /Z.add; case x, y=>//.
133133
by rewrite ltnSn subnn. }
134134
{ move=> p' ->; rewrite -!binnat.to_natE Pos2Nat.inj_add.
135135
case (Pos.to_nat p0); [by rewrite Nat.add_0_l addn0|move=> n].
136-
rewrite ifT; [by rewrite plusE addKn|].
136+
rewrite ifT; [|by rewrite plusE addKn].
137137
by rewrite plusE; apply ltn_addr; rewrite ltnSn. }
138138
move=> p' ->; rewrite -!binnat.to_natE Pos2Nat.inj_add.
139139
case (Pos.to_nat p').
@@ -142,34 +142,34 @@ rewrite /Z2int /GRing.add /= /intZmod.addz /Z.add; case x, y=>//.
142142
move=> n.
143143
case E: (Pos.to_nat p)=>/=; [by rewrite subn0|].
144144
rewrite ifF.
145-
{ by rewrite plusE addnS -addSn addKn. }
146-
by rewrite plusE addnS -addSn -ltn_subRL subnn ltn0. }
145+
by rewrite plusE addnS -addSn -ltn_subRL subnn ltn0.
146+
by rewrite plusE addnS -addSn addKn. }
147147
{ rewrite /GRing.opp /= /intZmod.oppz -binnat.to_natE.
148148
by case (Pos.to_nat p); [rewrite addn0|move=>n; rewrite subn0]. }
149149
{ rewrite -binnat.to_natE /GRing.opp /= /intZmod.oppz.
150150
move: (Z.pos_sub_discr p p0); case E': (Z.pos_sub _ _).
151151
{ move<-; rewrite -binnat.to_natE Z.pos_sub_diag; case (Pos.to_nat _)=>// n.
152152
by rewrite ltnSn subnn. }
153153
{ move=> ->.
154-
rewrite -!binnat.to_natE Pos2Nat.inj_add Z.pos_sub_lt; last first.
154+
rewrite -!binnat.to_natE Pos2Nat.inj_add Z.pos_sub_lt.
155155
{ by apply Pos.lt_add_diag_r. }
156-
rewrite -binnat.to_natE Pos2Nat.inj_sub ?Pos2Nat.inj_add; last first.
156+
rewrite -binnat.to_natE Pos2Nat.inj_sub ?Pos2Nat.inj_add.
157157
{ by apply Pos.lt_add_diag_r. }
158158
rewrite plusE minusE addKn; case (Pos.to_nat _).
159159
{ by rewrite addn0; case (Pos.to_nat p0)=>// n; rewrite ltnSn subnn. }
160160
move=> n.
161161
case E: (Pos.to_nat p0 + n.+1)%N.
162162
{ by exfalso; move: E; rewrite addnS. }
163-
rewrite -E ifF.
163+
rewrite -E ifF; last first.
164164
{ f_equal.
165165
have H: (Pos.to_nat p0 + n.+1 - n.+1 = Pos.to_nat p0 + n.+1 - n.+1)%N.
166166
{ done. }
167167
move: H; rewrite {2}E addnK=>->.
168168
by rewrite subnS subSn /= ?subKn //; move: E;
169169
rewrite addnS=>[] [] <-; rewrite leq_addl. }
170170
by rewrite addnS -ltn_subRL subnn ltn0. }
171-
move=> ->; rewrite Z.pos_sub_gt; [|by apply Pos.lt_add_diag_r].
172-
rewrite -!binnat.to_natE !Pos2Nat.inj_sub; [|by apply Pos.lt_add_diag_r].
171+
move=> ->; rewrite Z.pos_sub_gt; [by apply Pos.lt_add_diag_r|].
172+
rewrite -!binnat.to_natE !Pos2Nat.inj_sub; [by apply Pos.lt_add_diag_r|].
173173
rewrite Pos2Nat.inj_add; case (Pos.to_nat p).
174174
{ by rewrite plusE minusE !add0n subn0. }
175175
by move=> n; rewrite plusE minusE addKn ifT // leq_addr. }
@@ -207,7 +207,7 @@ case: Nat.divmod => q r /(_ (le_n _)) [].
207207
rewrite Nat.mul_0_r Nat.sub_diag !Nat.add_0_r Nat.mul_comm => + Hr /=.
208208
rewrite multE minusE plusE => /(f_equal (fun x => divn x y.+1)) ->.
209209
rewrite divnMDl // divn_small ?addn0 //.
210-
rewrite ltn_subLR; [|exact/ssrnat.leP].
210+
rewrite ltn_subLR; [exact/ssrnat.leP|].
211211
by rewrite -addSnnS addnC addnS ltnS leq_addr.
212212
Qed.
213213

@@ -218,7 +218,7 @@ Proof.
218218
case: x => [|x|//] _; [by rewrite intdiv.div0z|].
219219
case: y => [|y|//] _; [by rewrite intdiv.divz0|].
220220
rewrite -!positive_nat_Z -Nat2Z.inj_div; last first.
221-
rewrite !positive_nat_Z /= /divz gtr0_sgz ?mul1r; last first.
221+
rewrite !positive_nat_Z /= /divz gtr0_sgz ?mul1r.
222222
{ exact: nat_of_pos_gt0. }
223223
rewrite divE !binnat.to_natE absz_nat /Z2int.
224224
move: (Zle_0_nat (nat_of_pos x %/ nat_of_pos y)).
@@ -339,7 +339,7 @@ case: x => [|x|//] _; [by rewrite /= lcm0n|].
339339
case: y => [|y|//] _; [by rewrite /= lcmn0|].
340340
rewrite /Z.lcm Z2int_abs Z2int_mul Z2int_div //.
341341
rewrite ZgcdE' abszM; apply: f_equal; apply/eqP.
342-
rewrite -(@eqn_pmul2r (gcdn `|Z2int (Z.pos x)| `|Z2int (Z.pos y)|)); last first.
342+
rewrite -(@eqn_pmul2r (gcdn `|Z2int (Z.pos x)| `|Z2int (Z.pos y)|)).
343343
{ rewrite gcdn_gt0; apply/orP; left; rewrite absz_gt0 /= eqz_nat.
344344
apply: lt0n_neq0; exact: nat_of_pos_gt0. }
345345
rewrite muln_lcm_gcd.
@@ -423,7 +423,7 @@ case: g => [|g|g].
423423
{ rewrite normr_eq0.
424424
case: d' posd' {coprime_n'_d'} => // d' _.
425425
by rewrite Posz_nat_of_pos_neq0. }
426-
rewrite !Z2int_mul abszM PoszM gez0_abs; [|by rewrite -[0%R]int2ZK Z2int_le].
426+
rewrite !Z2int_mul abszM PoszM gez0_abs; [by rewrite -[0%R]int2ZK Z2int_le|].
427427
rewrite fracqMM ?Posz_nat_of_pos_neq0 // abszE.
428428
move: (@valq_frac (Z2int n', `|Z2int d'|) d'n0).
429429
rewrite scalqE // mul1r => [[neq deq]].
@@ -475,7 +475,7 @@ rewrite Qcanon.Qred_iff ZgcdE -[1%coqZ]/(Z.of_nat 1%nat) => /Nat2Z.inj.
475475
rewrite /Qnum /Qden nat_of_pos_Z_to_pos => /eqP ny_dy_coprime.
476476
move=> /eqP; rewrite rat_eqE !coprimeq_num // !coprimeq_den //=.
477477
rewrite !gtr0_sg ?nat_of_pos_gtr0 // !mul1r => /andP[/eqP <-].
478-
rewrite ifF; [|exact/eqP/eqP/lt0r_neq0/nat_of_pos_gtr0].
478+
rewrite ifF; [exact/eqP/eqP/lt0r_neq0/nat_of_pos_gtr0|].
479479
rewrite -!abszE !absz_nat => /eqP[<-]; split=> [//|].
480480
rewrite -[LHS]/(Z2int (Z.pos (Z.to_pos (BigN.to_Z dy)))) Z2Pos.id //.
481481
exact: BigQ.N_to_Z_pos.
@@ -547,7 +547,7 @@ rewrite /Qeq_bool !Z2int_Qred /=.
547547
do ?[rewrite /Zeq_bool -Z.eqb_compare]. (* remove line when requiring Rocq >= 9.0 *)
548548
rewrite GRing.eqr_div ?intq_eq0 ?Posz_nat_of_pos_neq0 //.
549549
rewrite !nat_of_pos_Z_to_pos.
550-
rewrite !gez0_abs; [|by rewrite -[0%R]int2ZK Z2int_le..].
550+
rewrite !gez0_abs; [by rewrite -[0%R]int2ZK Z2int_le..|].
551551
rewrite -!intrM -!Z2int_mul eqr_int.
552552
by case: Z.eqb_spec => [->|eq]; apply/eqP => // eq'; apply/eq/Z2int_inj.
553553
Qed.
@@ -571,7 +571,7 @@ rewrite !Z2int_Qred /= /Qcompare /= -Z.ltb_compare.
571571
rewrite ltr_pdivrMr ?ltr0z ?nat_of_pos_gtr0 //.
572572
rewrite mulrAC ltr_pdivlMr ?ltr0z ?nat_of_pos_gtr0 //.
573573
rewrite !nat_of_pos_Z_to_pos.
574-
rewrite !gez0_abs; [|by rewrite -[0%R]int2ZK Z2int_le..].
574+
rewrite !gez0_abs; [by rewrite -[0%R]int2ZK Z2int_le..|].
575575
rewrite -!intrM -!Z2int_mul ltr_int.
576576
case: ltP.
577577
{ by move=> /(proj1 (Z2int_lt _ _)) /(proj2 (Z.ltb_lt _ _)) => ->. }
@@ -589,7 +589,7 @@ rewrite !Z2int_Qred /= /Qcompare /=.
589589
rewrite ler_pdivrMr ?ltr0z ?nat_of_pos_gtr0 //.
590590
rewrite mulrAC ler_pdivlMr ?ltr0z ?nat_of_pos_gtr0 //.
591591
rewrite !nat_of_pos_Z_to_pos.
592-
rewrite !gez0_abs; [|by rewrite -[0%R]int2ZK Z2int_le..].
592+
rewrite !gez0_abs; [by rewrite -[0%R]int2ZK Z2int_le..|].
593593
rewrite -!intrM -!Z2int_mul ler_int.
594594
case: leP.
595595
{ move=> /(proj1 (Z2int_le _ _)) /Zle_compare.

‎refinements/boolF2.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ From CoqEAL Require Import hrel param refinements.
77

88
Import Refinements.Op.
99

10-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
10+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1111

1212
Section operations.
1313

‎refinements/examples/irred.v‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ From mathcomp Require Import zmodp ssralg countalg finalg poly polydiv.
77
From CoqEAL Require Import hrel pos param refinements binnat boolF2 seqpoly.
88
From CoqEAL Require Import poly_op trivial_seq poly_div boolF2.
99

10-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
10+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1111

1212
Set Implicit Arguments.
1313
Unset Strict Implicit.
@@ -91,7 +91,7 @@ Definition npoly_enum : seq {poly_n R} :=
9191
Lemma npoly_enum_uniq : uniq npoly_enum.
9292
Proof.
9393
rewrite /npoly_enum; case: n=> [|k] //.
94-
rewrite pmap_sub_uniq // map_inj_uniq => [|f g eqfg]; rewrite ?enum_uniq //.
94+
rewrite pmap_sub_uniq // map_inj_uniq => [f g eqfg|]; rewrite ?enum_uniq //.
9595
apply/ffunP => /= i; have /(congr1 (fun p : {poly _} => p`_i)) := eqfg.
9696
by rewrite !coef_poly ltn_ord inord_val.
9797
Qed.
@@ -114,7 +114,7 @@ HB.instance Definition _ := Finite.on {poly_n R}.
114114
Lemma card_npoly : #|{poly_n R}| = (#|R| ^ n)%N.
115115
Proof.
116116
rewrite cardE enumT unlock /= /npoly_enum; case: n => [|k] //=.
117-
rewrite size_pmap_sub (@eq_in_count _ _ predT) ?count_predT; last first.
117+
rewrite size_pmap_sub (@eq_in_count _ _ predT) ?count_predT.
118118
by move=> _ /mapP /= [f _ ->]; rewrite size_poly.
119119
by rewrite size_map -cardE card_ffun card_ord.
120120
Qed.

‎refinements/hpoly.v‎

Lines changed: 7 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ From CoqEAL Require Import param refinements pos hrel poly_op.
1010
(* *)
1111
(******************************************************************************)
1212

13-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
13+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
1414

1515
Set Implicit Arguments.
1616
Unset Strict Implicit.
@@ -412,7 +412,7 @@ case: eqP => [->|/eqP no].
412412
rewrite mulr1 /= addr0 -mulrA -exprD [_ + (a%:P + _)]addrCA /cast.
413413
by rewrite /cast_pos_nat insubdK ?subnK -?topredE /= ?subn_gt0 // ltnW.
414414
rewrite -mulrA -exprD [_ + (a%:P + _)]addrCA /cast /cast_pos_nat.
415-
rewrite insubdK ?subnK // -?topredE /=; first by rewrite leqNgt hnm.
415+
rewrite insubdK ?subnK // -?topredE /=; last by rewrite leqNgt hnm.
416416
rewrite subn_gt0 ltnNge leq_eqVlt hnm Bool.orb_false_r {hnm}.
417417
move/negbT: hneq; apply: contra; move/eqP=> heq; apply/eqP; exact: val_inj.
418418
rewrite !ih !addXn_constE expr0 mulr1 /= addr0 mulrDl -mulrA -exprD addnC.
@@ -546,7 +546,7 @@ Proof.
546546
have [|/eqP hp0] := eqP.
547547
move/eqP; rewrite lead_coef_eq0; move/eqP=> ->.
548548
by rewrite mul0r add0r lead_coefC.
549-
rewrite lead_coefDl; first by rewrite lead_coef_Mmonic ?monicXn.
549+
rewrite lead_coefDl; last by rewrite lead_coef_Mmonic ?monicXn.
550550
rewrite size_polyC size_Mmonic ?monicXn -?lead_coef_eq0 //.
551551
rewrite size_polyXn !addnS -pred_Sn.
552552
case: (c == 0)=> //=.
@@ -572,7 +572,7 @@ Proof.
572572
rewrite mulrDl -addrA -mulrA -exprD subnK ?rdivp_addl_mul_small //.
573573
by rewrite monicXn.
574574
rewrite size_polyXn (leq_ltn_trans (size_add _ _)) // gtn_max.
575-
rewrite (leq_ltn_trans (size_mul_leq _ _)) /=.
575+
rewrite (leq_ltn_trans (size_mul_leq _ _)) /=; last first.
576576
by rewrite size_polyC; case: (a != 0).
577577
rewrite size_polyXn addnS -pred_Sn addnC -ltn_subRL [X in (_ < X)]subSn //.
578578
by rewrite -[X in (_ < X)](size_polyXn A) ltn_rmodp monic_neq0 ?monicXn.
@@ -592,7 +592,7 @@ Proof.
592592
rewrite mulrDl -addrA -mulrA -exprD subnK ?rmodp_addl_mul_small //.
593593
by rewrite monicXn.
594594
rewrite size_polyXn (leq_ltn_trans (size_add _ _)) // gtn_max.
595-
rewrite (leq_ltn_trans (size_mul_leq _ _)) /=.
595+
rewrite (leq_ltn_trans (size_mul_leq _ _)) /=; last first.
596596
by rewrite size_polyC; case: (a != 0).
597597
rewrite size_polyXn addnS -pred_Sn addnC -ltn_subRL [X in (_ < X)]subSn //.
598598
by rewrite -[X in (_ < X)](size_polyXn A) ltn_rmodp monic_neq0 ?monicXn.
@@ -617,9 +617,9 @@ Proof.
617617
have -> /= := surjective_pairing (split_hpoly (m.+1 - cast n)%C p).
618618
by have [-> ->] := ih (m.+1 - cast n)%C.
619619
rewrite /shift_hpoly [(_ == _)%C]subn_eq0 ifN /=.
620+
by rewrite [(_ <= _)%N]hnSm.
620621
rewrite polyC0 addr0 /cast cast_nat_posK //.
621-
by rewrite subn_gt0 ltnNge [(_ <= _)%N]hnSm.
622-
by rewrite [(_ <= _)%N]hnSm.
622+
by rewrite subn_gt0 ltnNge [(_ <= _)%N]hnSm.
623623
Qed.
624624

625625
Instance Rhpoly_head : refines (Rhpoly ==> Logic.eq) (fun p => p`_0) head_hpoly.

‎refinements/hrel.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
(c) Copyright INRIA and University of Gothenburg, see LICENSE *)
44
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp.
55
From mathcomp Require Import path choice fintype tuple finset bigop.
6-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
6+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
77

88
Set Implicit Arguments.
99
Unset Strict Implicit.

‎refinements/karatsuba.v‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@ From mathcomp Require Import path choice fintype tuple finset bigop poly polydiv
33

44
From CoqEAL Require Import hrel param refinements poly_op.
55

6-
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
6+
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)
77

88
Set Implicit Arguments.
99
Unset Strict Implicit.

0 commit comments

Comments
 (0)