[unification] Experiment: add a flag to configure conversion on heads found by FO approximation

[mattam82]

One can then disallow conversion on the heads (not the arguments) for much faster unification.
This is too crude to use directly, hence just a draft at this point.

Fixes / closes #????

• Added / updated test-suite.

• Added changelog.
• Added / updated documentation.
  • Documented any new / changed user messages.
  • Updated documented syntax by running make doc_gram_rsts.

• Opened overlay pull requests.

[SkySkimmer]

@coqbot run full ci

[SkySkimmer]

@coqbot bench

[ppedrot]

The default value of the flag is true, so IIANM this PR is the identity.

[SkySkimmer]

I guess it's been a while since we saw how much noise the bench has in a reflexive test

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│ coq-neural-net-interp-computed-lite │  288.96   298.13  -3.08 │  1319086574693   1361084755543  -3.09 │  3421771882273   3421781515223  -0.00 │ 1130064  1126392   0.33 │
│                            coq-core │  128.10   129.86  -1.36 │   505458189741    499879338524   1.12 │   530678077567    530834540674  -0.03 │  457156   457924  -0.17 │
│                         coq-bignums │   29.60    29.87  -0.90 │   134062709019    135027972845  -0.71 │   193737996402    193572016005   0.09 │  478780   478928  -0.03 │
│                          coq-stdlib │  364.64   365.96  -0.36 │  1551283744125   1554460514369  -0.20 │  1341526752539   1341451293721   0.01 │  716504   719448  -0.41 │
│                    coq-fiat-parsers │  308.97   309.79  -0.26 │  1380241106796   1381877187236  -0.12 │  2431720113451   2431865151510  -0.01 │ 2387916  2389816  -0.08 │
│            coq-metacoq-translations │   16.68    16.72  -0.24 │    75234043127     74858318823   0.50 │   124882954156    124864790667   0.01 │  847340   844428   0.34 │
│                 coq-category-theory │  694.18   695.35  -0.17 │  3160456172048   3163735115778  -0.10 │  5313575923505   5307073712757   0.12 │  969168   974388  -0.54 │
│                      coq-verdi-raft │  578.49   578.59  -0.02 │  2631062977671   2633700242187  -0.10 │  4172998422702   4171006808009   0.05 │  854372   846440   0.94 │
│                    coq-math-classes │   85.12    85.07   0.06 │   383195567874    382840210004   0.09 │   535889553062    535791714352   0.02 │  521408   521132   0.05 │
│                           coq-verdi │   48.49    48.44   0.10 │   218355688703    217881034899   0.22 │   340868430837    340715416693   0.04 │  531936   529484   0.46 │
│                   coq-metacoq-pcuic │  782.53   781.20   0.17 │  3569289669845   3562612713368   0.19 │  5328506850234   5324657413340   0.07 │ 2385980  2385868   0.00 │
│                                 coq │  728.62   726.69   0.27 │  3066938976093   3064089873686   0.09 │  5485713558865   5484000076031   0.03 │ 2716160  2703584   0.47 │
│                        coq-rewriter │  387.48   386.40   0.28 │  1761754175697   1756721235976   0.29 │  2951399878587   2951646102659  -0.01 │ 1481504  1484120  -0.18 │
│               coq-engine-bench-lite │  156.48   156.02   0.29 │   663074437092    661005292360   0.31 │  1225873544515   1226923003960  -0.09 │ 1226648  1226836  -0.02 │
│                             coq-vst │  879.26   876.63   0.30 │  3998747489290   3985801804210   0.32 │  6758678909532   6756905947218   0.03 │ 2338020  2359964  -0.93 │
│                        coq-coqprime │   48.27    48.09   0.37 │   217402730270    215864733260   0.71 │   334602146752    334505677181   0.03 │  789824   789780   0.01 │
│                 coq-metacoq-erasure │  499.63   497.48   0.43 │  2279739066356   2270526479680   0.41 │  3578887015204   3578501869152   0.01 │ 1861196  1856500   0.25 │
│                         coq-coqutil │   42.46    42.24   0.52 │   187336279488    185644556575   0.91 │   271333624761    271271074502   0.02 │  564360   566444  -0.37 │
│                         coq-unimath │ 2432.07  2419.25   0.53 │ 11073380894745  11012898063188   0.55 │ 21924146561648  21927931208779  -0.02 │ 1281672  1254536   2.16 │
│                        coq-bedrock2 │  358.75   356.71   0.57 │  1634105248359   1625774449311   0.51 │  3095958943096   3097824048381  -0.06 │  911976   912548  -0.06 │
│                           coq-color │  251.96   250.52   0.57 │  1132271275941   1125267697123   0.62 │  1636020699281   1635711202756   0.02 │ 1207908  1207508   0.03 │
│             coq-metacoq-safechecker │  419.50   417.10   0.58 │  1921416792078   1909500783715   0.62 │  3178503712156   3177553959624   0.03 │ 1888400  1895684  -0.38 │
│                            coq-hott │  158.18   157.25   0.59 │   706355011084    702534543761   0.54 │  1122171112639   1122282169553  -0.01 │  547872   550052  -0.40 │
│                            coq-corn │  734.32   729.88   0.61 │  3336562304577   3315720943822   0.63 │  5173022653801   5171985271401   0.02 │  802980   804048  -0.13 │
│                       coq-fiat-core │   59.40    58.96   0.75 │   246321538369    245776293206   0.22 │   369326019180    369397007918  -0.02 │  487508   483112   0.91 │
│        coq-fiat-crypto-with-bedrock │ 6198.59  6152.10   0.76 │ 28233261393327  28021863045429   0.75 │ 50354382662814  50325312139264   0.06 │ 3245980  3245952   0.00 │
│                   coq-iris-examples │  469.20   465.63   0.77 │  2131259691859   2116616306425   0.69 │  3272833490992   3272174399081   0.02 │ 1093476  1089496   0.37 │
│                        coq-compcert │  281.47   278.96   0.90 │  1274699146697   1262628952886   0.96 │  1943859822666   1943758985136   0.01 │ 1183336  1184388  -0.09 │
│                coq-metacoq-template │  148.65   147.32   0.90 │   660049599106    655058755333   0.76 │  1034879099733   1034915426813  -0.00 │ 1165952  1167708  -0.15 │
│          coq-performance-tests-lite │  708.35   700.93   1.06 │  3198777346033   3164556627887   1.08 │  5645160039758   5644366259278   0.01 │ 1588848  1589744  -0.06 │
│         coq-rewriter-perf-SuperFast │  787.20   778.77   1.08 │  3577583372923   3539507935022   1.08 │  6186723815829   6186357866848   0.01 │ 1578896  1581068  -0.14 │
│                       coq-equations │    7.68     7.57   1.45 │    31078142813     31007843486   0.23 │    50731222661     50735646901  -0.01 │  387088   387024   0.02 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-mathcomp-ssreflect (dependency install failed in NEW)

coq-mathcomp-fingroup (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-algebra (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-solvable (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-field (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-character (dependency coq-mathcomp-ssreflect failed)
coq-mathcomp-odd-order (dependency coq-mathcomp-ssreflect failed)
coq-coquelicot (dependency coq-mathcomp-ssreflect failed)
coq-fourcolor (dependency coq-mathcomp-ssreflect failed)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                              TOP 25 SLOW DOWNS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF   %DIFF    Ln                     FILE                                                                             │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 152.5250  154.9280  2.4030   1.58%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│  99.1470  100.9060  1.7590   1.77%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                        │
│ 219.6550  221.2410  1.5860   0.72%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                │
│  18.5540   19.6090  1.0550   5.69%   957  coq-unimath/UniMath/CategoryTheory/Monoidal/Examples/DisplayedCartesianMonoidal.v.html             │
│   3.9330    4.9540  1.0210  25.96%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│  95.0340   96.0100  0.9760   1.03%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│  65.5550   66.4840  0.9290   1.42%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                           │
│  46.0770   46.9970  0.9200   2.00%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                         │
│  46.0940   46.9890  0.8950   1.94%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html       │
│  96.4860   97.3630  0.8770   0.91%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                        │
│  46.9650   47.6880  0.7230   1.54%   926  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoor.v.html                          │
│  95.2110   95.9040  0.6930   0.73%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                    │
│   2.6710    3.3260  0.6550  24.52%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│  43.1210   43.7710  0.6500   1.51%   827  coq-vst/veric/binop_lemmas4.v.html                                                                 │
│   7.8460    8.4890  0.6430   8.20%  1225  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html                        │
│  26.8000   27.3960  0.5960   2.22%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html │
│   2.0180    2.5980  0.5800  28.74%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                        │
│  33.3750   33.9520  0.5770   1.73%   839  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│  61.5060   62.0590  0.5530   0.90%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html      │
│  23.7250   24.2410  0.5160   2.17%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                            │
│   1.6390    2.1260  0.4870  29.71%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                           │
│  47.2770   47.7560  0.4790   1.01%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                    │
│  72.8240   73.2820  0.4580   0.63%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                               │
│  26.8380   27.2890  0.4510   1.68%   147  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/GarageDoorTop.v.html                       │
│  41.1310   41.5670  0.4360   1.06%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                                       │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│   OLD       NEW      DIFF     %DIFF     Ln                     FILE                                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 257.7610  248.1680  -9.5930    -3.72%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html      │
│  27.7200   26.8000  -0.9200    -3.32%   373  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│  23.3890   22.7730  -0.6160    -2.63%   595  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                      │
│   9.5210    9.0110  -0.5100    -5.36%   952  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html             │
│   2.7480    2.4120  -0.3360   -12.23%   487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                         │
│   5.4660    5.1400  -0.3260    -5.96%  1099  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/StrictTwoSidedDispCat.v.html             │
│   6.8920    6.6320  -0.2600    -3.77%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html │
│  10.4460   10.1920  -0.2540    -2.43%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                       │
│   0.2430    0.0000  -0.2430  -100.00%   474  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/Signature.v.html                      │
│   0.2410    0.0000  -0.2410  -100.00%    65  coq-fiat-crypto-with-bedrock/src/Bedrock/Standalone/StandaloneOCamlMain.v.html                     │
│ 133.1920  132.9750  -0.2170    -0.16%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                             │
│   0.2080    0.0000  -0.2080  -100.00%   241  coq-metacoq-erasure/erasure/theories/ErasureProperties.v.html                                      │
│   0.2050    0.0040  -0.2010   -98.05%   232  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Translation/Proofs/Cmd.v.html                       │
│   0.1950    0.0010  -0.1940   -99.49%   374  coq-metacoq-erasure/erasure/theories/EGenericGlobalMap.v.html                                      │
│   0.1910    0.0000  -0.1910  -100.00%   106  coq-metacoq-pcuic/pcuic/theories/PCUICSpine.v.html                                                 │
│  12.5640   12.3750  -0.1890    -1.50%   409  coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html                                          │
│   1.9210    1.7380  -0.1830    -9.53%   373  coq-bedrock2/bedrock2/src/bedrock2Examples/memmove.v.html                                          │
│   0.1830    0.0020  -0.1810   -98.91%   150  coq-metacoq-pcuic/pcuic/theories/PCUICContextReduction.v.html                                      │
│  14.8960   14.7170  -0.1790    -1.20%    99  coq-fiat-crypto-with-bedrock/src/Spec/Curve25519.v.html                                            │
│   0.1760    0.0030  -0.1730   -98.30%   122  coq-metacoq-pcuic/pcuic/theories/Typing/PCUICRenameTyp.v.html                                      │
│   0.1730    0.0010  -0.1720   -99.42%   764  coq-metacoq-pcuic/pcuic/theories/PCUICReduction.v.html                                             │
│   4.6330    4.4610  -0.1720    -3.71%     5  coq-fiat-crypto-with-bedrock/src/Assembly/Parse/Examples/fiat_p256_square_optimised_seed103.v.html │
│  15.4720   15.3060  -0.1660    -1.07%   417  coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html                  │
│   0.4890    0.3250  -0.1640   -33.54%   868  coq-stdlib/MSets/MSetRBT.v.html                                                                    │
│   9.9650    9.8010  -0.1640    -1.65%   418  coq-category-theory/Theory/Metacategory/ArrowsOnly.v.html                                          │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job