Skip to content

Port to new rewrite goals order #121

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
Mar 24, 2026
Merged

Port to new rewrite goals order #121

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
33 changes: 16 additions & 17 deletions src/freeg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
From mathcomp Require Import fintype bigop order generic_quotient.
From mathcomp Require Import ssralg ssrnum ssrint.
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)

Import Order.Theory GRing.Theory Num.Theory.

Expand All @@ -39,7 +39,7 @@
Unset Printing Implicit Defensive.

(* -------------------------------------------------------------------- *)
Local Notation simpm := Monoid.simpm.

Check warning on line 42 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use

(* -------------------------------------------------------------------- *)
Reserved Notation "{ 'freeg' K / G }" (K at level 2, format "{ 'freeg' K / G }").
Expand Down Expand Up @@ -116,8 +116,8 @@

HB.reexport.

Notation prefreeg := prefreeg.

Check warning on line 119 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use
Notation fgequiv := equiv.

Check warning on line 120 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-dev) 

Use of "Notation" keyword for abbreviations is deprecated, use
Notation mkPrefreeg := mkPrefreeg.

Notation reduced := reduced.
Expand Down Expand Up @@ -331,8 +331,8 @@
Lemma precoeffE x : precoeff x =1 prelift (fun y => (y == x)%:R : R^o).
Proof.
move=> s; rewrite [RHS](bigID [pred kx | kx.2 == x]) /= addrC big1.
by rewrite add0r; apply: eq_bigr => i /eqP ->; rewrite eqxx [_ *: _]mulr1.
by move=> i /negbTE ->; rewrite scaler0.
by move=> i /negbTE ->; rewrite scaler0.
by rewrite add0r; apply: eq_bigr => i /eqP ->; rewrite eqxx [_ *: _]mulr1.
Qed.

Lemma precoeff_nil x : precoeff x [::] = 0.
Expand Down Expand Up @@ -442,7 +442,7 @@
uniq (predom s) -> kz \in s -> precoeff kz.2 s = kz.1.
Proof.
move=> uniq_dom_s kz_in_s; have uniq_s := map_uniq uniq_dom_s.
rewrite precoeff_uniqE // (nth_map kz); last first.
rewrite precoeff_uniqE // (nth_map kz).
by rewrite -(size_map (@snd _ _)) index_mem map_f.
rewrite nth_index_map // => {kz kz_in_s} kz1 kz2 kz1_in_s kz2_in_s eq.
apply/eqP.
Expand All @@ -460,7 +460,7 @@
case/andP: rD => uniqD /allP /= rD; rewrite precoeff_uniqE //.
apply/idP/idP; last apply: contra_neqT; move=> x_in_D; last first.
by rewrite nth_default // memNindex // !size_map.
rewrite (nth_map (0, x)); last first.
rewrite (nth_map (0, x)).
by rewrite -(size_map (@snd _ _)) index_mem x_in_D.
by apply/rD/mem_nth; rewrite -(size_map (@snd _ _)) index_mem.
Qed.
Expand Down Expand Up @@ -570,7 +570,7 @@
Section Lift.
Context (M : lmodType R) (f : K -> M).

Lemma lift_is_additive : additive (fglift f).

Check warning on line 573 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 573 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 573 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 573 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 573 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof.
elim/quotW=> [[D1 /= H1]]; elim/quotW=> [[D2 /= H2]].
unlock fglift; rewrite ?piE [_ + _]piE /lift /=.
Expand All @@ -580,11 +580,11 @@
End Lift.

(* -------------------------------------------------------------------- *)
Lemma coeff_is_additive x : additive (coeff x).

Check warning on line 583 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 583 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 583 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 583 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 583 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof. exact: lift_is_additive R^o _. Qed.

#[export] HB.instance Definition _ x :=
GRing.isAdditive.Build {freeg K / R} R (coeff x)

Check warning on line 587 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 587 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 587 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 587 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.

Check warning on line 587 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Notation GRing.isAdditive.Build is deprecated since mathcomp 2.5.0.
(coeff_is_additive x).

Lemma coeff0 z : coeff z 0 = 0 . Proof. exact: raddf0. Qed.
Expand Down Expand Up @@ -735,8 +735,8 @@
apply/eqP/freeg_eqP=> x /=; rewrite raddf_sum /=.
case x_in_dom: (x \in dom D); last rewrite coeff_outdom ?x_in_dom //.
+ rewrite (bigD1_seq x) ?uniq_dom //= big1 ?addr0.
* by rewrite coeffU eqxx mulr1.
* by move=> z ne_z_x; rewrite coeffU (negbTE ne_z_x) mulr0.
* by rewrite coeffU eqxx mulr1.
+ rewrite big_seq big1 // => z z_notin_dom; rewrite coeffU.
have ->: (z == x)%:R = 0 :> R; last by rewrite mulr0.
by case: (z =P x)=> //= eq_zx; rewrite eq_zx x_in_dom in z_notin_dom.
Expand Down Expand Up @@ -827,7 +827,7 @@

Definition predeg (D : seq (int * K)) := \sum_(kx <- D) kx.1.

Lemma deg_is_additive: additive deg.

Check warning on line 830 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-coq-8.20) 

Reference additive is deprecated since mathcomp 2.5.0.

Check warning on line 830 in src/freeg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.0) 

Reference additive is deprecated since mathcomp 2.5.0.
Proof. exact: (@lift_is_additive _ K int^o). Qed.

#[export] HB.instance Definition _ :=
Expand Down Expand Up @@ -916,7 +916,7 @@
0 <=g D1 -> 0 <=g D2 -> dom (D1 + D2) =i dom D1 ++ dom D2.
Proof.
move=> pos_D1 pos_D2 z; rewrite mem_cat !mem_dom coeffD.
by rewrite paddr_eq0; first 1 [rewrite negb_and] || apply/fgposP.
by rewrite paddr_eq0; last 1 [rewrite negb_and] || apply/fgposP.
Qed.
End FreegCmpDom.

Expand All @@ -931,7 +931,7 @@
z \in dom D -> coeff z (fgmap D) = f (coeff z D) *+ P z.
Proof.
move=> zD; rewrite /fgmap raddf_sum /= -big_filter; case Pz: (P z).
+ rewrite (bigD1_seq z) ?(filter_uniq, uniq_dom) //=; last first.
+ rewrite (bigD1_seq z) ?(filter_uniq, uniq_dom) //=.
by rewrite mem_filter Pz.
rewrite coeffU eqxx mulr1 big1 ?addr0 //.
by move=> z' ne_z'z; rewrite coeffU (negbTE ne_z'z) mulr0.
Expand Down Expand Up @@ -1045,13 +1045,12 @@
Lemma fgpos_eq0P (D : {freeg K}) : 0 <=g D -> deg D = 0 -> D = 0.
Proof.
move=> posD; rewrite -{1}[D]freeg_sumE raddf_sum /=.
rewrite (eq_bigr (fun z => coeff z D)); last first.
rewrite (eq_bigr (fun z => coeff z D)).
by move=> i _; rewrite degU.
move/eqP; rewrite psumr_eq0; last by move=> i _; apply/fgposP.
move/eqP; rewrite psumr_eq0; first by move=> i _; apply/fgposP.
move/allP=> zD; apply/eqP; apply/freeg_eqP=> z; rewrite coeff0.
case z_in_D: (z \in dom D); last first.
by rewrite coeff_outdom // z_in_D.
exact/eqP/zD.
case z_in_D: (z \in dom D); first exact/eqP/zD.
by rewrite coeff_outdom // z_in_D.
Qed.

Lemma fgneg_eq0P (D : {freeg K}) : D <=g 0 -> deg D = 0 -> D = 0.
Expand All @@ -1076,7 +1075,7 @@
case: (p =P q) =>[<-/=|]; last first.
by move=> _; rewrite subr0; apply/fgposP.
by rewrite subr_ge0.
move/fgpos_eq0P=> ->; first by rewrite add0r; exists p.
move/fgpos_eq0P=> ->; last by rewrite add0r; exists p.
by rewrite degB degU degD_eq1 subrr.
Qed.

Expand Down Expand Up @@ -1108,7 +1107,7 @@
move=> p /=; rewrite !inE; apply/negP=> /andP [].
rewrite /DR => /dom_sum_subset /flattenP.
case=> [ps /mapP [q]]; rewrite mem_filter => /andP [].
move=> Rq q_in_D ->; rewrite domU ?mem_seq1; last first.
move=> Rq q_in_D ->; rewrite domU ?mem_seq1.
by rewrite -(mem_dom D q).
by move/eqP=> ->; move: Rq; rewrite /in_mem /= => ->.
move: DR => DR domDR; rewrite addrC -big_filter.
Expand All @@ -1135,15 +1134,15 @@
move/perm_filter=> /(_ [pred q | ~~ (F q)]) /=.
rewrite NRp; rewrite perm_sym; move/perm_trans => /(_ _ DE).
rewrite perm_cons => domD'; rewrite big_seq.
rewrite (eq_bigr (fun q => << coeff q D' *g q >>)); last first.
rewrite (eq_bigr (fun q => << coeff q D' *g q >>)).
move=> q q_in_ps; rewrite /D' coeffB coeffU; case: (p =P q).
- by move=> eq_pq; move: p_notin_ps; rewrite eq_pq q_in_ps.
- by move=> _; rewrite mulr0 subr0.
by rewrite -big_seq; apply: IH.
* apply/negP=> /domD_subset; rewrite mem_cat; case/orP; last first.
by move=> p_in_DR; move/(_ p): domDR; rewrite !inE NRp p_in_DR.
move/dom_sum_subset; rewrite filter_predT => /flattenP [qs].
move/mapP => [q q_in_ps ->]; rewrite domU; last first.
move/mapP => [q q_in_ps ->]; rewrite domU.
move/perm_mem/(_ q): DE; rewrite !inE q_in_ps orbT.
by rewrite mem_filter => /andP [_]; rewrite mem_dom.
rewrite mem_seq1 => /eqP pq_eq; move: p_notin_ps.
Expand Down
16 changes: 8 additions & 8 deletions src/monalg.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,9 +9,9 @@
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat.
From mathcomp Require Import seq path choice finset fintype finfun.
From mathcomp Require Import tuple bigop ssralg ssrint ssrnum.
Set SsrOldRewriteGoalsOrder. (* change Set to Unset when porting the file, then remove the line when requiring MathComp >= 2.6 *)
Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *)

Require Import xfinmap.

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset[ _ ] _ | _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset[ _ ] _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset _ | _ in _ ]" defined at level 0 with arguments

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-coq-8.20) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Check warning on line 14 in src/monalg.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:rocq-prover-9.1) 

Notations "[ fset _ | _ : _ in _ ]" defined at level 0

Set Implicit Arguments.
Unset Strict Implicit.
Expand Down Expand Up @@ -465,7 +465,7 @@
case: (msuppP g) => k1g; last first.
rewrite raddf0; apply: big1_fset => x xg _.
by apply: big1_fset => y _ _; case: eqP xg k1g => //= -> ->.
rewrite (big_fsetD1 _ k1g)/= [s in _ + s]big1_fset; last first.
rewrite (big_fsetD1 _ k1g)/= [s in _ + s]big1_fset.
move=> k1; rewrite !inE => /andP[k1neq _] _.
by apply: big1_fset => k2 _ _; rewrite (negPf k1neq).
rewrite eqxx/= addr0; case: (msuppP g@_k.1) => k2g; last first.
Expand Down Expand Up @@ -688,7 +688,7 @@
msupp g1 `<=` d1 -> msupp g2 `<=` d2 ->
fgmul g1 g2 = \sum_(k1 <- d1) \sum_(k2 <- d2) g1 *M_[k1, k2] g2.
Proof.
move=> le_d1 le_d2; rewrite -(big_fset_incl _ le_d1)/=; last first.
move=> le_d1 le_d2; rewrite -(big_fset_incl _ le_d1)/=.
by move=> k _ /mcoeff_outdom g1k; apply/big1 => ?; rewrite g1k mul0r monalgU0.
apply/eq_bigr=> k1 _; apply/big_fset_incl => // k _ /mcoeff_outdom ->.
by rewrite mulr0 monalgU0.
Expand Down Expand Up @@ -903,9 +903,9 @@
rewrite (big_fsetD1 1%M) //= mulm1 2!mcoeffD mcoeffUU.
rewrite ![\sum_(i <- E `\ 1%M) _]big_seq.
rewrite !raddf_sum !big1 ?addr0 //= => k; rewrite in_fsetD1 => /andP [ne1_k _].
rewrite raddf_sum big1 ?mcoeff0 //= => k'; rewrite mcoeffU.
by case: eqP=> // /eqP /unitmP []; rewrite (negbTE ne1_k).
by rewrite mcoeffU mul1m (negbTE ne1_k).
by rewrite mcoeffU mul1m (negbTE ne1_k).
rewrite raddf_sum big1 ?mcoeff0 //= => k'; rewrite mcoeffU.
by case: eqP=> // /eqP /unitmP []; rewrite (negbTE ne1_k).
Qed.

HB.instance Definition _ :=
Expand All @@ -928,10 +928,10 @@
rewrite (partition_big_imfset _ fst)/= msupp_curryl; apply/eq_bigr => k1l _.
rewrite exchange_big (partition_big_imfset _ fst) raddf_sum msupp_curryl/=.
apply/eq_bigr => k1r _; rewrite exchange_big raddfMn/= mcoeffMl -sumrMnl.
rewrite (* SLOW *)msupp_curryr big_imfset/=; last first.
rewrite (* SLOW *)msupp_curryr big_imfset/=.
by move=> [? ?] [? ?] /andP[/= _ /eqP ->] /andP[/= _ /eqP ->] ->.
rewrite big_filter; apply/eq_bigr => -[_ k2l]/= /eqP ->.
rewrite -sumrMnl msupp_curryr big_imfset/=; last first.
rewrite -sumrMnl msupp_curryr big_imfset/=.
by move=> [? ?] [? ?] /andP[/= _ /eqP ->] /andP[/= _ /eqP ->] ->.
rewrite big_filter; apply/eq_bigr => -[_ k2r]/= /eqP ->.
by rewrite !mcurryE -mulrnA mulnb andbC.
Expand Down
Loading
Loading