ssr: skip impargs in pattern FO unif

[gares]

This is an attempt to make changes in the algebraic hierarchy of mathcomp less painful.

When a structure s with op1 and op2 is broken into s1 with op1 and s2 with op2 it may be the case that lemmas involving both operations have a type like forall i:sj, op1 i x (op2 i y) z = .. where an instance of the structure sj (join of s1 and s2) occurs non linearly. A concrete goal may have after the split the shape op1 canon_s1_on_T x (op2 (sj_to_s2 canon_sj_on_T) y) z or something like that, while before both ops would have the same canonical instance on T (the type of x, y, z).
Because of the 2 syntactically different instances the FO pass makes a different choice than before.

This PR tries to avoid breakage by making the FO pass do

• ignore implicit arguments of constants, e.g. structure instances

  • in one case the real arg is implicit because it is followed by a phantom, hence I use the shortest list of impargs
    Not needed/used anymore, but still valid: rewrite takes the shortest list of impargs among the existing ones.

• ignore subterms that are FO-different but the pattern is is a proj

• reduce the goal subterm if it is not equal to the pattern and is a proj (applied to a CS instance)

• fail to match if the pattern contains more evars that the matched goal (i.e. if it contains non-instantiated variables)

• flags Set SsrMatching LegacyFoUnif makes it behave as before, so one can compare old/new using the same version of Rocq and/or give up fixing a proof.

Things tried and abandoned

• completely disable FO pass

  • lemmas with shape _ (if ..) or _ f g rely on the FO pass. I tried adjusting the HO one to behave the same (use the first arg key rigidly) but some lemmas nee more keys...
  • some rewritings become very surprising, even in algebra, eg (_ * _ * _) since some defs compute and can expose *

• do not ignore proj _ = t problems, since in groups we have plenty of set/group lemmas, with gval that would behave surprisingly, eg x \in <[x]> || x \in G where G : group, the second one has an explicit gval, the former none, the lemma has it.

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  I don't think the FO pass was ever documented, and I'm not so sure it should. This PR contains the details for the braves.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• adapt to rocq-prover/rocq#20707 math-comp/math-comp#1438
• adapt to rocq-prover/rocq#20707 math-comp/odd-order#69
• adapt to rocq-prover/rocq#20707 math-comp/analysis#1641
• adapt to rocq-prover/rocq#20707 jasmin-lang/jasmin#1209
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 math-comp/multinomials#103
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 math-comp/real-closed#78
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 rocq-community/coqeal#109
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 math-comp/Abel#101
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 rocq-community/gaia#28
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 rocq-community/apery#35
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 rocq-community/graph-theory#47
• https://gitlab.inria.fr/coquelicot/coquelicot/-/merge_requests/14
• adapt to rocq-prover/rocq#20707 uwplse/verdi#148
• adapt to rocq-prover/rocq#20707 MetaRocq/metarocq#1190
• https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1124
• Adapt to https://github.com/rocq-prover/rocq/pull/20707 mit-pdos/perennial#279

[CohenCyril]

Great!!! There will be legitimate breakage! Maybe we need a flag ?
The second optim would be that the second phase only captures hidden occurrences when it wouldn't typecheck otherwise.

[proux01]

FWIW, a quick look at mathcomp show 85 proofs requiring an update.

[gares]

On the positive side, most of the broken proof were bad ones, i.e. relying in some way on the FO pass to select "the wrong one". The only cases where now things are reversed are because of the behavior above, IIRC 2 occurrences in MC.

[proux01]

Thanks @tchajed here is the (trivial and backward compatible) overlay: mit-pdos/perennial#279

[gares]

@proux01 I plan to test this PR on the wrapping branch with Matteo on Tuesday. Apparently it is not solving all problems as we expected, it may need more fine tuning.

[CalosciMatteo]

Yes, there still seems to be some problems with the unification of the notation "^+" which is present both on the ring and fingroup scope,

This is the error i get (for instance in Lemma lerXn2r in numdomain.v):

Check _ * (y^+n).
  (* The term "y" has type
         "POrderedZmodule.sort
            (join_Num_NumDomain_between_monoid_Magma_and_Num_POrderedZmodule R)"
       while it is expected to have type "BaseFinGroup.arg_sort ?T".
  *)

Despite (y^+n) getting correctly typed as

(*: Magma.sort
         (monoid_BaseUMagma__to__monoid_Magma
            (Num_NumDomain__to__monoid_BaseUMagma R))*)

this is under
'''Variable R : numDomainType.
Implicit Types x y z t : R. '''

The workaround is to annote the context as in 'Check _ * (y^+n)%R.'

[proux01]

Well, this is ready with (almost) all overlays merged, so I'd be inclined to merge it and let any further improvement happen in a new PR. Anyway, this won't land in 9.1 so changes won't be spread across multiple releases.

Let's do the following:

• wait until end of the week, if more fine tuning happens and doesn't need any new overlay, let's keep it here
• otherwise, merge this as it is and let further progress take place in a new PR.

[proux01]

@coqbot bench

[proux01]

This is the error i get (for instance in Lemma lerXn2r in numdomain.v):

Check _ * (y^+n).

Not sure I understand the link between Check and ssrmatching (what this PR is about). I'll let you two sort this out on Tuesday.

The workaround is to annote the context as in 'Check _ * (y^+n)%R.'

Again, this is just changing the notation interpretation, hard to see any clear link with pattern selection.

[gares]

Well, this is ready with (almost) all overlays merged, so I'd be inclined to merge it and let any further improvement happen in a new PR. Anyway, this won't land in 9.1 so changes won't be spread across multiple releases.

Let's do the following:

• wait until end of the week, if more fine tuning happens and doesn't need any new overlay, let's keep it here
• otherwise, merge this as it is and let further progress take place in a new PR.

Totally agree, I just want to look at the rewrite errors. This PR and overlays are sound I believe. If we identify a needed change that requires no overlay update we will propose it, otherwise we make a separate pr.

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│              coq-mathcomp-odd-order │  563.77   581.25  -3.01 │  4074365875853   4172957703564  -2.36 │ 2216436  2225624  -0.41 │
│                            coq-core │    2.84     2.89  -1.73 │    19755383823     19766765107  -0.06 │   92964    93016  -0.06 │
│             rocq-mathcomp-ssreflect │    1.25     1.27  -1.57 │     9177145171      9176825140   0.00 │  556640   556604   0.01 │
│                        rocq-bignums │   27.94    28.25  -1.10 │   181178435137    181182421533  -0.00 │  479788   479984  -0.04 │
│               rocq-metarocq-erasure │  499.60   505.08  -1.08 │  3450861378892   3450420451781   0.01 │ 1838332  1833716   0.25 │
│                        coq-bedrock2 │  345.01   348.14  -0.90 │  2896293387446   2896373316361  -0.00 │  871396   876372  -0.57 │
│                           rocq-core │    6.30     6.35  -0.79 │    39088979987     39058450383   0.08 │  439228   441784  -0.58 │
│                           coq-color │  247.10   248.30  -0.48 │  1566052492213   1565980953309   0.00 │ 1136140  1134772   0.12 │
│                    coq-math-classes │   86.01    86.42  -0.47 │   533306721057    533329710454  -0.00 │  513096   512612   0.09 │
│                             coq-vst │  843.23   847.22  -0.47 │  6440852313459   6441098800405  -0.00 │ 2231848  2235492  -0.16 │
│                 rocq-mathcomp-field │  158.83   159.56  -0.46 │  1211934169381   1215123542285  -0.26 │ 1927740  1741972  10.66 │
│ coq-neural-net-interp-computed-lite │  231.39   232.30  -0.39 │  2249430104625   2249399040492   0.00 │  899308   903364  -0.45 │
│         coq-rewriter-perf-SuperFast │  466.22   467.87  -0.35 │  3741757845166   3743367113656  -0.04 │ 1239740  1216028   1.95 │
│                         coq-coqutil │   44.99    45.13  -0.31 │   285409284953    285347233090   0.02 │  566560   564344   0.39 │
│                        coq-compcert │  307.71   308.40  -0.22 │  2034885381198   2034490332577   0.02 │ 1148392  1150324  -0.17 │
│               rocq-mathcomp-algebra │  282.56   283.06  -0.18 │  2126159166652   2133048885930  -0.32 │ 1425444  1422376   0.22 │
│               coq-engine-bench-lite │  124.58   124.77  -0.15 │   938876566051    940668680249  -0.19 │ 1101752  1099508   0.20 │
│                            coq-corn │  676.95   677.61  -0.10 │  4689696462748   4689396717112   0.01 │  708528   709768  -0.17 │
│                    coq-fiat-parsers │  277.33   277.53  -0.07 │  2148146948966   2147977387171   0.01 │ 2353864  2349636   0.18 │
│                       coq-fourcolor │ 1325.40  1325.26   0.01 │ 12372518628764  12372061575049   0.00 │  894536   896432  -0.21 │
│              rocq-metarocq-template │   81.73    81.72   0.01 │   570085949819    570115963986  -0.01 │  992836   993720  -0.09 │
│          coq-performance-tests-lite │  884.46   884.22   0.03 │  7191391941421   7192693137531  -0.02 │ 1939364  1940428  -0.05 │
│               coq-mathcomp-analysis │  904.72   904.30   0.05 │  6800961266826   6793217914694   0.11 │ 1901168  1895016   0.32 │
│                            coq-hott │  153.58   153.41   0.11 │  1067581877813   1067447288466   0.01 │  489180   486932   0.46 │
│                 coq-category-theory │  610.00   609.32   0.11 │  4516274221269   4516129507231   0.00 │  974084   973968   0.01 │
│                         coq-unimath │ 1755.63  1753.62   0.11 │ 14652140108566  14652610347633  -0.00 │ 1090060  1086608   0.32 │
│                         rocq-stdlib │  446.85   446.31   0.12 │  1592566000555   1592908826257  -0.02 │  616416   614392   0.33 │
│                       coq-fiat-core │   58.27    58.17   0.17 │   357568761465    357580016145  -0.00 │  485460   488176  -0.56 │
│           rocq-metarocq-safechecker │  321.81   321.17   0.20 │  2410432156515   2410275624774   0.01 │ 1796152  1787756   0.47 │
│                rocq-metarocq-common │   41.90    41.80   0.24 │   270245221208    270249821497  -0.00 │  920820   918448   0.26 │
│                   coq-iris-examples │  356.78   355.80   0.28 │  2381143348138   2380925964532   0.01 │ 1058212  1060220  -0.19 │
│             rocq-mathcomp-character │   87.53    87.27   0.30 │   623402347506    614524167252   1.44 │ 1473120  1482020  -0.60 │
│              rocq-mathcomp-fingroup │   23.39    23.32   0.30 │   152335884521    152093828319   0.16 │  529032   532956  -0.74 │
│              rocq-mathcomp-solvable │   93.20    92.90   0.32 │   637986061387    640907847042  -0.46 │ 1040212  1043772  -0.34 │
│                        rocq-runtime │   74.52    74.24   0.38 │   536788848310    536675050944   0.02 │  494968   491288   0.75 │
│                      rocq-equations │    9.12     9.07   0.55 │    63247003847     63230516898   0.03 │  400740   400440   0.07 │
│                 rocq-metarocq-utils │   23.10    22.95   0.65 │   151424893165    151334914047   0.06 │  584216   582300   0.33 │
│                      coq-verdi-raft │  528.34   524.74   0.69 │  3681934837000   3681755082177   0.00 │  847232   848212  -0.12 │
│                        coq-coqprime │   51.48    51.09   0.76 │   352471015661    352470653136   0.00 │  803252   803180   0.01 │
│                        coq-rewriter │  334.63   331.50   0.94 │  2504936582912   2504994948384  -0.00 │ 1311852  1312208  -0.03 │
│                 rocq-metarocq-pcuic │  645.54   639.26   0.98 │  4152514869693   4156225269555  -0.09 │ 2294660  2329660  -1.50 │
│                           coq-verdi │   43.89    43.46   0.99 │   295174514877    295138476948   0.01 │  526088   525556   0.10 │
│                           rocq-elpi │   12.78    12.61   1.35 │    91698694972     91714674634  -0.02 │  485532   485512   0.00 │
│          rocq-metarocq-translations │   16.45    16.22   1.42 │   117493368732    117478712075   0.01 │  762060   762704  -0.08 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-fiat-crypto-with-bedrock (in NEW)
coq-coquelicot (in NEW)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                  TOP 25 SLOW DOWNS                                                   │
│                                                                                                                      │
│   OLD      NEW    DIFF     %DIFF     Ln                 FILE                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    0.205   3.55  3.3458   1633.37%   403  coq-mathcomp-odd-order/theories/BGappendixC.v.html                         │
│   0.0461   1.78  1.7343   3762.00%   394  coq-mathcomp-odd-order/theories/BGappendixC.v.html                         │
│   0.0414   1.75  1.7086   4130.00%   645  coq-mathcomp-analysis/theories/tvs.v.html                                  │
│     38.8   40.1  1.3233      3.41%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│    0.784   1.83  1.0461    133.48%   395  coq-mathcomp-odd-order/theories/BGappendixC.v.html                         │
│     1.07   1.50  0.4300     40.02%    75  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                      │
│     11.7   12.1  0.3425      2.92%   125  coq-mathcomp-odd-order/theories/BGappendixAB.v.html                        │
│     24.0   24.2  0.2745      1.15%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html            │
│     25.9   26.2  0.2700      1.04%    12  coq-fourcolor/theories/proof/job190to206.v.html                            │
│     18.7   19.0  0.2678      1.43%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html          │
│     28.0   28.2  0.2617      0.94%    12  coq-fourcolor/theories/proof/job563to588.v.html                            │
│     1.39   1.65  0.2576     18.53%   313  rocq-stdlib/theories/Strings/Byte.v.html                                   │
│     17.9   18.1  0.2456      1.38%    32  coq-performance-tests-lite/src/pattern.v.html                              │
│    0.307  0.524  0.2168     70.56%   586  rocq-stdlib/theories/Strings/Byte.v.html                                   │
│     25.8   26.1  0.2088      0.81%    12  coq-fourcolor/theories/proof/job399to438.v.html                            │
│ 0.000240  0.204  0.2041  85025.00%   429  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html     │
│   0.0106  0.215  0.2039   1921.02%   766  rocq-metarocq-erasure/erasure/theories/EWcbvEval.v.html                    │
│   0.0391  0.241  0.2017    515.94%  1804  rocq-stdlib/theories/MSets/MSetRBT.v.html                                  │
│    0.349  0.550  0.2011     57.60%    14  rocq-stdlib/theories/extraction/ExtrOcamlZInt.v.html                       │
│   0.0116  0.212  0.2005   1733.96%   143  rocq-mathcomp-field/field/algebraics_fundamentals.v.html                   │
│    0.458  0.657  0.1988     43.38%    10  rocq-mathcomp-character/character/vcharacter.v.html                        │
│     2.27   2.47  0.1953      8.60%   607  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                  │
│   0.0112  0.198  0.1872   1675.40%   359  rocq-metarocq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                 │
│   0.0250  0.212  0.1866    747.57%   432  rocq-metarocq-pcuic/pcuic/theories/PCUICInductiveInversion.v.html          │
│  0.00958  0.195  0.1853   1935.22%   561  rocq-metarocq-pcuic/pcuic/theories/PCUICSR.v.html                          │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD      NEW      DIFF     %DIFF    Ln                    FILE                                                                         │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   8.56    0.0160  -8.5478  -99.81%   925  coq-mathcomp-odd-order/theories/PFsection4.v.html                                             │
│   8.42   0.00606  -8.4182  -99.93%   199  coq-mathcomp-odd-order/theories/PFsection12.v.html                                            │
│   66.0      62.6  -3.4312   -5.20%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│   3.68      2.44  -1.2365  -33.61%  1198  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│   3.58      2.38  -1.1994  -33.47%   986  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│   93.9      93.0  -0.8673   -0.92%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│   93.7      92.9  -0.8168   -0.87%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│    199       198  -0.5727   -0.29%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html │
│  0.450    0.0264  -0.4236  -94.13%  1905  coq-mathcomp-odd-order/theories/PFsection13.v.html                                            │
│   3.96      3.56  -0.4001  -10.11%   492  rocq-stdlib/theories/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                          │
│   1.67      1.27  -0.3989  -23.85%  1207  rocq-metarocq-erasure/erasure/theories/ErasureFunction.v.html                                 │
│   1.11     0.782  -0.3276  -29.52%  1408  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│   1.29     0.988  -0.3008  -23.34%   572  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                     │
│ 31.721    31.425  -0.2960   -0.93%    97  coq-vst/veric/binop_lemmas5.v.html                                                            │
│ 33.314    33.039  -0.2750   -0.83%   194  coq-vst/veric/expr_lemmas4.v.html                                                             │
│ 34.379    34.109  -0.2700   -0.79%   147  coq-vst/veric/expr_lemmas4.v.html                                                             │
│ 40.862    40.616  -0.2460   -0.60%   834  coq-vst/veric/binop_lemmas4.v.html                                                            │
│   1.64      1.42  -0.2246  -13.70%    73  rocq-stdlib/theories/Numbers/HexadecimalString.v.html                                         │
│   9.66      9.44  -0.2210   -2.29%    87  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                         │
│   36.6      36.4  -0.2191   -0.60%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                  │
│   2.57      2.36  -0.2075   -8.07%   447  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html        │
│  0.208   0.00210  -0.2058  -98.99%   428  rocq-metarocq-safechecker/safechecker/theories/PCUICSafeChecker.v.html                        │
│  0.205  0.000356  -0.2047  -99.83%   765  rocq-metarocq-erasure/erasure/theories/EWcbvEval.v.html                                       │
│   5.08      4.88  -0.1935   -3.81%   121  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html         │
│  0.243    0.0539  -0.1888  -77.79%   429  rocq-metarocq-pcuic/pcuic/theories/PCUICInductiveInversion.v.html                             │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[gares]

OK, we confirm the PR fixes all the matching related problems we have in the wrapping branch. Green light.

[proux01]

So, only waiting for the coquelicot overlay to be merged and I merge.

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: You can't merge the PR because it hasn't been approved yet.

[proux01]

@coqbot merge now

[coqbot-app]

@proux01: Please take care of the following overlays:

• 20707-gares-sspart-FO-ignore-imparg.sh