Remove the workarounds introduced in #1125 by pi8027 · Pull Request #1365 · math-comp/math-comp

pi8027 · 2025-03-19T13:23:36Z

Motivation for this change

#1125 introduced some workarounds for performance issues with linear lemmas. This PR removes them, relying on the performance improvements introduced in Rocq 9.0.

Minimal TODO list

added changelog entries with doc/changelog/make-entry.sh

added corresponding documentation in the headers
tried to abide by the contribution guide
this PR contains an optimum number of meaningful commits

See this Checklist for details.

Automatic note to reviewers

Read this Checklist.

pi8027

I did a performance comparison of the (* slow *) lines before/after this PR (c34342c) in Rocq 9.0.0.

EDIT 2025-11-06: I rebenched it in Rocq 9.1.0. The commit hash is bf7bc67.

pi8027 · 2025-04-04T16:30:50Z


 Let vs2mx0 : @vs2mx K vT 0 = 0.
-Proof. by rewrite /= linear0 genmx0. Qed.
+Proof. by rewrite /= linear0 genmx0. Qed. (* slow *)


0.002s -> 0.044s

0.003s -> 0.002s

pi8027 · 2025-04-04T16:31:55Z

 Lemma vlineP v1 v2 : reflect (exists k, v1 = k *: v2) (v1 \in <[v2]>)%VS.
 Proof.
-apply: (iffP idP) => [|[k ->]]; rewrite memvK genmxE ?linearZ ?scalemx_sub //.
+apply: (iffP idP) => [|[k ->]]; rewrite memvK genmxE ?linearZ ?scalemx_sub //. (* slow *)


0.011s -> 0.158s

0.017s -> 0.014s

pi8027 · 2025-04-04T16:32:29Z

 Proof.
-split=> [|a u v]; rewrite !memvK 1?linear0 1?sub0mx // => Uu Uv.
-by rewrite linearP addmx_sub ?scalemx_sub.
+split=> [|a u v]; rewrite !memvK 1?linear0 1?sub0mx // => Uu Uv. (* slow *)


0.005s -> 0.175s

0.006s -> 0.008s

pi8027 · 2025-04-04T16:32:54Z

-split=> [|a u v]; rewrite !memvK 1?linear0 1?sub0mx // => Uu Uv.
-by rewrite linearP addmx_sub ?scalemx_sub.
+split=> [|a u v]; rewrite !memvK 1?linear0 1?sub0mx // => Uu Uv. (* slow *)
+by rewrite linearP addmx_sub ?scalemx_sub. (* slow *)


0.006s -> 0.044s

0.007s -> 0.007s

pi8027 · 2025-04-04T16:33:42Z


 Lemma memv_add u v U V : u \in U -> v \in V -> u + v \in (U + V)%VS.
-Proof. by rewrite !memvK genmxE linearD; apply: addmx_sub_adds. Qed.
+Proof. by rewrite !memvK genmxE linearD; apply: addmx_sub_adds. Qed. (* slow *)


0.005s -> 0.133s

0.004s -> 0.005s

pi8027 · 2025-04-04T16:38:50Z


 Lemma xcfun_is_additive phi : additive (xcfun phi).
-Proof. by move=> A B; rewrite /xcfun [gring_row _]linearB mulmxBl !mxE. Qed.
+Proof. by move=> A B; rewrite /xcfun [gring_row _]linearB mulmxBl !mxE. Qed. (* slow *)


0.033s -> 0.036s

0.07s -> 0.071s

pi8027 · 2025-04-04T16:41:27Z

-    move=> Gx; apply/eqP; rewrite 2!mulmxA mul_rV_lin1 -subr_eq0 -mulmxBr /=.
-    rewrite uv0 // linearB /= mulmxBr vec_mxK; split. (* FIXME: slow *)
+    move=> Gx; apply/eqP; rewrite 2!mulmxA mul_rV_lin1 -subr_eq0 -mulmxBr.
+    rewrite uv0 // 2!linearB /= vec_mxK; split. (* slow *)


0.032s -> 0.291s

It might be worth keeping the workaround here.

0.071s -> 0.998s

This one sounds bad (with which version of Rocq?)

Damn, then we should indeed keep the workaround here.

For me, it's unclear if the slowdown comes from 1) the changes in instance declarations, 2) the changes in proofs, or 3) both. We should keep the whole workaround in place until we better understand the situation.

pi8027 · 2025-04-04T16:42:09Z

 move=> A B RnA RnB /= eqAB; apply/eqP; rewrite -subr_eq0 -mxvec_eq0 -submx0.
 rewrite -ker_irr_comp_op sub_capmx (sameP sub_kermxP eqP) mul_vec_lin.
-by rewrite 2!raddfB /= eqAB subrr linear0 addmx_sub ?eqmx_opp /=.
+by rewrite 2!linearB /= eqAB subrr linear0 addmx_sub ?eqmx_opp /=. (* slow *)


0.064s -> 0.057s

0.012s -> 0.138s

pi8027 · 2025-04-04T16:42:23Z

  rewrite (mx_Schur irrG) ?subr_eq0 //; last first.
    by apply: contraNneq nscal_rGx => ->; apply: scalar_mx_is_scalar.
-  rewrite -memmx_cent_envelop raddfB.
+  rewrite -memmx_cent_envelop linearB. (* slow *)


0.029s -> 0.025s

0.003s -> 0.061s

pi8027 · 2025-04-04T16:43:33Z

 Proof. by apply: (canLR in_genK); rewrite in_gen0. Qed.

+Lemma in_genN : {morph in_gen : W / - W}.
+Proof. by move=> W; apply/matrixP=> i j; rewrite !mxE 4!(mulNmx, linearN). Qed. (* slow *)


0.003s -> 0.246s

It might be worth keeping the workaround here.

0.003s -> 0.701s

pi8027 · 2025-04-04T16:51:43Z

For vector.v, I hope its generalization to semi-vector spaces will further mitigate the issue. Most GRing.semilinear_linear should disappear anyway thanks to #1269.

Tragicus · 2025-06-09T11:17:53Z

rocq-prover/rocq#20730 is 0.3% slower on master and 5% faster on this branch (than rocq/master). With the Rocq PR, this branch becomes 1% slower than master.

pi8027 · 2025-09-15T12:25:49Z

I discarded the changes to poly.v and matrix.v: they were just removal of GRing.semilinear_linear which has been done in #1395 and #1398 (in the right way). I hope this will also be the case in mxpoly.v (#1269), vector.v, and qpoly.v, but the last two are non-trivial (#1269 (comment)).

pi8027 · 2025-10-21T12:29:29Z

This PR can probably be merged safely now. It would be nice to compare the performance of the (* slow *) lines before/after this PR using a recent version of Rocq (9.1 or master) before doing so.

pi8027 · 2025-11-06T15:39:34Z

 Proof.
 rewrite unlock /pinvmx rank_rV; case: negP => [[] | _].
-  by apply/eqP/rowP=> j; rewrite !mxE (tnth_nth 0) /= linear0 mxE.
+  by apply/eqP/rowP=> j; rewrite !mxE (tnth_nth 0) /= linear0 mxE. (* slow *)


0.005s -> 0.005s

pi8027 · 2025-11-06T15:52:58Z

I rebenched this PR with Rocq 9.1.0. To sum up, I don't see any slowdown in vector.v anymore. However, mxrepresentation.v has become slower for unclear reasons. (It's a bit concerning to see that the master branch is already slower than before. Perhaps it's because of new structures?)

We should probably wait for rocq-prover/rocq#20730 at least.

pi8027 added kind: clean-up This issure/PR is about cleaning up obsolete code, removing hacks, etc drops: coq 8.20 labels Mar 19, 2025

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch 2 times, most recently from 40508a7 to bd7c788 Compare March 19, 2025 16:54

pi8027 mentioned this pull request Mar 20, 2025

Add semi-modules, semi-algebras, and semilinear functions #1125

Merged

3 tasks

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch 2 times, most recently from df61543 to c34342c Compare April 4, 2025 13:14

pi8027 commented Apr 4, 2025

View reviewed changes

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from c34342c to 40e81b7 Compare May 15, 2025 15:48

Tragicus mentioned this pull request Jun 9, 2025

Reduce projections during unification rocq-prover/rocq#20730

Closed

6 tasks

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 40e81b7 to 8950dd5 Compare September 15, 2025 12:21

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 8950dd5 to 4dcae16 Compare September 17, 2025 08:26

proux01 added this to the 2.6.0 milestone Sep 22, 2025

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 4dcae16 to 672a31d Compare September 23, 2025 10:44

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 672a31d to 6534948 Compare October 21, 2025 12:09

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 6534948 to d7f79ae Compare October 21, 2025 12:58

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from d7f79ae to 5623704 Compare November 3, 2025 12:14

Remove the workarounds for the performance issues with linear lemmas

bf7bc67

pi8027 force-pushed the semi-modules-rm-perf-workarounds branch from 5623704 to bf7bc67 Compare November 6, 2025 15:28

pi8027 commented Nov 6, 2025

View reviewed changes

pi8027 modified the milestones: 2.6.0, 2.7.0 Feb 24, 2026

Uh oh!

Conversation

pi8027 commented Mar 19, 2025

Motivation for this change

Minimal TODO list

Automatic note to reviewers

Uh oh!

pi8027 left a comment • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pi8027 commented Apr 4, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Tragicus commented Jun 9, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

pi8027 commented Sep 15, 2025

Uh oh!

pi8027 commented Oct 21, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

pi8027 commented Nov 6, 2025

Uh oh!

Reviewers

Assignees

Labels

pi8027 left a comment •

edited

Loading

pi8027 commented Apr 4, 2025 •

edited

Loading

Tragicus commented Jun 9, 2025 •

edited

Loading