Refold before evar instantiation

[Tragicus]

Until now, the algorithm unfolded terms blindly and instantiated an evar with whatever term was on the other side. Now, we remember the terms from the initial unification problem, and whenever we reach a problem of the form ?e = t, we replace t with its initial version.
This PR does the minimal change that changes the behavior of the unification algorithm as intended, but this makes the control flow a bit awkward and some computations are done twice, which is a bit inefficient. Should I try to be a bit more aggressive and rewrite some of the code?

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.

Overlays:

• Adapt to rocq#19987 UniMath/UniMath#1995 (comment)
• Adapt to rocq#19987 HoTT/Coq-HoTT#2223
• adapt to rocq#19987 math-comp/odd-order#67
• Lock gedge, gnode and gface rocq-community/fourcolor#73
• Adapt to rocq#19987 math-comp/analysis#1532
• Adapt to Rocq#19987 MetaRocq/metarocq#1152
• https://gitlab.mpi-sws.org/iris/examples/-/merge_requests/70

[gares]

@coqbot bench

[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-equations │   6.91    7.10  -2.68 │   47029485945    47024399829   0.01 │  390336   388596   0.45 │
│                          coq-stdlib │ 187.89  189.58  -0.89 │ 1181739919276  1181696109342   0.00 │  532660   533332  -0.13 │
│                       coq-fiat-core │  56.11   56.45  -0.60 │  341057940535   341175081981  -0.03 │  473588   474472  -0.19 │
│                    coq-fiat-parsers │ 270.61  272.04  -0.53 │ 2106290219301  2105950413535   0.02 │ 2295512  2293532   0.09 │
│                            coq-core │  74.57   74.87  -0.40 │  541584302660   541622084437  -0.01 │  485268   485160   0.02 │
│                 coq-metacoq-erasure │ 515.35  517.12  -0.34 │ 3579815279037  3573514860516   0.18 │ 1821304  1824448  -0.17 │
│         coq-rewriter-perf-SuperFast │ 756.10  758.55  -0.32 │ 5912847787375  5912237388520   0.01 │ 1379000  1377236   0.13 │
│          coq-performance-tests-lite │ 902.37  904.81  -0.27 │ 7294476587492  7284817177578   0.13 │ 2469104  2470336  -0.05 │
│                  coq-metacoq-common │  66.63   66.80  -0.25 │  436060218079   435976582098   0.02 │ 1052520  1050064   0.23 │
│            coq-metacoq-translations │  16.76   16.80  -0.24 │  120426906427   120408204111   0.02 │  774868   772828   0.26 │
│               coq-mathcomp-fingroup │  25.99   26.04  -0.19 │  169328654076   169232083869   0.06 │  591316   589244   0.35 │
│                             coq-vst │ 853.94  855.48  -0.18 │ 6475714073501  6475217517501   0.01 │ 2218036  2214704   0.15 │
│                   coq-metacoq-utils │  22.76   22.80  -0.18 │  149370960530   149329650970   0.03 │  598760   598368   0.07 │
│                      coq-coquelicot │  36.23   36.29  -0.17 │  218177131455   218153317529   0.01 │  817700   817468   0.03 │
│                           coq-verdi │  43.64   43.70  -0.14 │  293299903777   293338999231  -0.01 │  528664   532400  -0.70 │
│                      coq-verdi-raft │ 533.21  533.61  -0.07 │ 3703590081697  3704590964871  -0.03 │  824096   836988  -1.54 │
│                 coq-category-theory │ 592.39  592.67  -0.05 │ 4429349901206  4428761492191   0.01 │  917956   981824  -6.51 │
│ coq-neural-net-interp-computed-lite │ 232.09  232.19  -0.04 │ 2244805485804  2244765908494   0.00 │  863588   865956  -0.27 │
│                coq-metacoq-template │ 146.49  146.51  -0.01 │  985614971489   985539629615   0.01 │ 1053616  1050260   0.32 │
│                        coq-rewriter │ 331.89  331.71   0.05 │ 2496712828296  2497204975808  -0.02 │ 1305200  1308696  -0.27 │
│                        coq-compcert │ 303.33  302.88   0.15 │ 2002039068455  2002152172587  -0.01 │ 1183860  1181964   0.16 │
│             coq-metacoq-safechecker │ 344.22  343.24   0.29 │ 2631523883769  2633899081278  -0.09 │ 1670176  1669784   0.02 │
│               coq-mathcomp-solvable │  90.04   89.77   0.30 │  630380602344   628500746592   0.30 │  946984   946876   0.01 │
│                         coq-coqutil │  42.44   42.29   0.35 │  267634556898   267561895031   0.03 │  560448   557828   0.47 │
│              coq-mathcomp-character │  74.87   74.59   0.38 │  513022774415   512243136548   0.15 │ 1181104  1180956   0.01 │
│                        coq-bedrock2 │ 322.69  320.83   0.58 │ 2710482236396  2711156433429  -0.02 │  895228   893584   0.18 │
│               coq-engine-bench-lite │ 129.73  128.97   0.59 │  968183321277   966225116325   0.20 │ 1076564  1076848  -0.03 │
│              coq-mathcomp-ssreflect │  88.24   87.61   0.72 │  600608498594   599200604406   0.23 │ 1635248  1637960  -0.17 │
│                  coq-mathcomp-field │  91.55   90.29   1.40 │  652151883310   646290054652   0.91 │ 1237468  1255856  -1.46 │
│                           rocq-core │   6.02    5.92   1.69 │   36478760827    36481294303  -0.01 │  436752   439448  -0.61 │
│                coq-mathcomp-algebra │ 164.50  160.62   2.42 │ 1149445502597  1127210229650   1.97 │ 1187236  1188608  -0.12 │
│                   coq-metacoq-pcuic │ 691.49  673.25   2.71 │ 4494550051066  4382440846182   2.56 │ 2259236  2260032  -0.04 │
│                   coq-iris-examples │ 403.41  389.55   3.56 │ 2709351395576  2606732263614   3.94 │ 1102112  1101796   0.03 │
└─────────────────────────────────────┴───────────────────────┴─────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-bignums (in NEW)
coq-hott (in NEW)
coq-mathcomp-odd-order (in NEW)
coq-mathcomp-analysis (dependency install failed in NEW)
coq-unimath (in NEW)
coq-fourcolor (in NEW)

coq-math-classes (dependency coq-bignums failed)
coq-corn (dependency coq-bignums failed)
coq-color (dependency coq-bignums failed)
coq-coqprime (dependency coq-bignums failed)
coq-fiat-crypto-with-bedrock (dependency coq-bignums failed)

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                  TOP 25 SLOW DOWNS                                                   │
│                                                                                                                      │
│   OLD      NEW     DIFF     %DIFF     Ln                FILE                                                         │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  0.1330   4.1990  4.0660   3057.14%  1867  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                           │
│  8.0710  11.0050  2.9340     36.35%   591  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html │
│  8.0830  10.9440  2.8610     35.40%   581  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html │
│  7.9850  10.8230  2.8380     35.54%   580  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/fundamental.v.html │
│  0.2750   1.8080  1.5330    557.45%   177  coq-mathcomp-algebra/mathcomp/algebra/intdiv.v.html                       │
│  0.0220   1.2510  1.2290   5586.36%   302  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0210   1.1660  1.1450   5452.38%   435  coq-metacoq-pcuic/pcuic/theories/PCUICInductiveInversion.v.html           │
│  0.0450   1.0930  1.0480   2328.89%  1902  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                           │
│  0.0140   1.0320  1.0180   7271.43%  1885  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                           │
│ 63.4600  64.4720  1.0120      1.59%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html               │
│  0.0160   1.0210  1.0050   6281.25%  1861  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                           │
│  0.0400   1.0360  0.9960   2490.00%  2065  coq-metacoq-pcuic/pcuic/theories/PCUICSR.v.html                           │
│  0.0300   1.0080  0.9780   3260.00%   531  coq-metacoq-erasure/erasure/theories/ESubstitution.v.html                 │
│  0.0060   0.9330  0.9270  15450.00%  3047  coq-metacoq-pcuic/pcuic/theories/PCUICExpandLetsCorrectness.v.html        │
│  0.0100   0.7910  0.7810   7810.00%   793  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0300   0.8000  0.7700   2566.67%   126  coq-metacoq-pcuic/pcuic/theories/Typing/PCUICRenameTyp.v.html             │
│ 46.3670  46.8170  0.4500      0.97%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                │
│ 10.3170  10.7330  0.4160      4.03%   325  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html      │
│  0.0130   0.4270  0.4140   3184.62%  2483  coq-metacoq-pcuic/pcuic/theories/PCUICInductives.v.html                   │
│ 10.4990  10.9040  0.4050      3.86%   214  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html      │
│  0.0190   0.3980  0.3790   1994.74%   769  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0230   0.4010  0.3780   1643.48%   658  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0170   0.3930  0.3760   2211.76%   792  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0460   0.4090  0.3630    789.13%   676  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                  │
│  0.0790   0.4380  0.3590    454.43%    84  coq-metacoq-pcuic/pcuic/theories/Typing/PCUICRenameTyp.v.html             │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│   OLD       NEW      DIFF     %DIFF     Ln                    FILE                                                                     │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  17.8600   17.0050  -0.8550    -4.79%    32  coq-performance-tests-lite/src/pattern.v.html                                             │
│  42.6870   41.9860  -0.7010    -1.64%   834  coq-vst/veric/binop_lemmas4.v.html                                                        │
│  38.6950   38.1530  -0.5420    -1.40%   224  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html            │
│  36.4320   36.0050  -0.4270    -1.17%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                              │
│ 100.4130  100.0330  -0.3800    -0.38%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│ 100.5450  100.1960  -0.3490    -0.35%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html           │
│  18.3110   18.0040  -0.3070    -1.68%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                         │
│   0.6460    0.3680  -0.2780   -43.03%   333  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                                  │
│   0.5400    0.2810  -0.2590   -47.96%   133  coq-metacoq-pcuic/pcuic/theories/Typing/PCUICRenameTyp.v.html                             │
│   8.5320    8.2950  -0.2370    -2.78%   673  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                              │
│  39.0380   38.8140  -0.2240    -0.57%   236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html │
│  31.2670   31.0520  -0.2150    -0.69%    97  coq-vst/veric/binop_lemmas5.v.html                                                        │
│   0.1910    0.0020  -0.1890   -98.95%   343  coq-metacoq-erasure/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v.html                     │
│  11.4870   11.3010  -0.1860    -1.62%   126  coq-vst/veric/binop_lemmas6.v.html                                                        │
│   4.7930    4.6080  -0.1850    -3.86%  2761  coq-metacoq-safechecker/safechecker/theories/PCUICTypeChecker.v.html                      │
│   0.1710    0.0000  -0.1710  -100.00%   466  coq-metacoq-erasure/erasure/theories/EArities.v.html                                      │
│  11.4820   11.3140  -0.1680    -1.46%   410  coq-verdi-raft/theories/RaftProofs/LeaderLogsLogMatchingProof.v.html                      │
│   0.5660    0.4030  -0.1630   -28.80%     9  coq-mathcomp-character/mathcomp/character/classfun.v.html                                 │
│   0.1670    0.0050  -0.1620   -97.01%   300  coq-metacoq-pcuic/pcuic/theories/PCUICCasesHelper.v.html                                  │
│   5.2680    5.1080  -0.1600    -3.04%   198  coq-compcert/x86/Op.v.html                                                                │
│   0.1630    0.0030  -0.1600   -98.16%   115  coq-mathcomp-field/mathcomp/field/algebraics_fundamentals.v.html                          │
│  38.9850   38.8260  -0.1590    -0.41%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                │
│   0.4330    0.2750  -0.1580   -36.49%    10  coq-mathcomp-character/mathcomp/character/vcharacter.v.html                               │
│   9.9620    9.8060  -0.1560    -1.57%   496  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                              │
│   0.1560    0.0010  -0.1550   -99.36%   236  coq-mathcomp-field/mathcomp/field/separable.v.html                                        │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[gares]

There are some slowdowns to be investigated, especially the metacoq one seems too huge to be acceptable.
It may just be that an intermediate goal is different and the next tactic does silly things.
The iris ones seems also relevant to me.