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]

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.

[Tragicus]

MetaRocq/metarocq#1152 is only a small performance improvement, so I think we might as well retry the CI now.

[Tragicus]

I expect the errors were due to me not rebasing. Can we try again?

[Tragicus]

It seems the problem is always when we get stuck on a match on an evar, in which case it does not really make sense to refold the other term since we will have to reduce it anyway. So I think we can try again.

[Tragicus]

May I ask for a bench?

[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-core │    2.77     2.90  -4.48 │    19789995251     19789010370   0.00 │   92844    92780   0.07 │
│                        rocq-bignums │   29.88    30.42  -1.78 │   194058587412    194137796412  -0.04 │  484356   484128   0.05 │
│                       coq-fiat-core │   58.58    59.55  -1.63 │   360355000272    360380255704  -0.01 │  485836   484644   0.25 │
│              rocq-metarocq-template │   82.25    83.56  -1.57 │   577193294331    577239652341  -0.01 │  992896   993744  -0.09 │
│             rocq-mathcomp-ssreflect │    1.26     1.28  -1.56 │     9188527398      9187692387   0.01 │  556556   551456   0.92 │
│                           coq-verdi │   44.10    44.74  -1.43 │   297740136373    297768019669  -0.01 │  536004   525376   2.02 │
│ coq-neural-net-interp-computed-lite │  231.95   235.23  -1.39 │  2251102584447   2251079343557   0.00 │  891764   893132  -0.15 │
│               rocq-metarocq-erasure │  515.46   521.78  -1.21 │  3594444123378   3594437334879   0.00 │ 1825600  1821832   0.21 │
│          rocq-metarocq-translations │   16.45    16.64  -1.14 │   117865233329    117894537140  -0.02 │  761360   769712  -1.09 │
│                            coq-hott │  154.44   156.17  -1.11 │  1074656308780   1075060041082  -0.04 │  489096   486408   0.55 │
│                      rocq-equations │    8.97     9.06  -0.99 │    63269370924     63275506700  -0.01 │  401088   400828   0.06 │
│                           rocq-elpi │   12.65    12.77  -0.94 │    91718366006     91751732361  -0.04 │  485032   480568   0.93 │
│                    coq-fiat-parsers │  278.82   281.18  -0.84 │  2159909688485   2159851168494   0.00 │ 2347576  2349516  -0.08 │
│               coq-engine-bench-lite │  124.07   125.09  -0.82 │   940125352447    940330116720  -0.02 │ 1099688  1099656   0.00 │
│                         coq-unimath │ 1760.72  1771.79  -0.62 │ 14696050527525  14692552771446   0.02 │ 1061244  1061128   0.01 │
│                        coq-coqprime │   51.50    51.82  -0.62 │   356303490069    356289950683   0.00 │  805036   805788  -0.09 │
│                        coq-rewriter │  335.43   337.35  -0.57 │  2526219698706   2526124113432   0.00 │ 1312028  1309784   0.17 │
│                        coq-compcert │  308.64   310.17  -0.49 │  2037660123020   2037724707581  -0.00 │ 1153740  1146732   0.61 │
│                    coq-math-classes │   87.11    87.49  -0.43 │   534092674632    534027926502   0.01 │  513828   513764   0.01 │
│                   coq-iris-examples │  360.89   362.42  -0.42 │  2402435286475   2402365079034   0.00 │ 1066168  1057652   0.81 │
│        coq-fiat-crypto-with-bedrock │ 6106.13  6129.51  -0.38 │ 49970775278175  49972814057550  -0.00 │ 3157796  3153972   0.12 │
│              coq-mathcomp-odd-order │  585.95   588.16  -0.38 │  4235748010971   4236082679317  -0.01 │ 2230400  2227372   0.14 │
│                         rocq-stdlib │  438.28   439.93  -0.38 │  1576782212797   1576785995051  -0.00 │  615124   618760  -0.59 │
│                         coq-coqutil │   45.46    45.63  -0.37 │   288690927938    288620130680   0.02 │  562256   562368  -0.02 │
│                            coq-corn │  680.78   683.29  -0.37 │  4705186125571   4704485560979   0.01 │  709844   715232  -0.75 │
│                      coq-verdi-raft │  534.40   536.35  -0.36 │  3730640208354   3730483015271   0.00 │  849792   847572   0.26 │
│                rocq-metarocq-common │   42.22    42.37  -0.35 │   273711085310    273675299916   0.01 │  924456   923120   0.14 │
│                        coq-bedrock2 │  346.08   347.26  -0.34 │  2903841048493   2904194672141  -0.01 │  870992   869608   0.16 │
│                 rocq-metarocq-pcuic │  652.92   655.08  -0.33 │  4240922065570   4241330731224  -0.01 │ 2257652  2260860  -0.14 │
│                           coq-color │  252.66   253.27  -0.24 │  1589050485785   1589213209333  -0.01 │ 1115624  1109892   0.52 │
│                 rocq-metarocq-utils │   23.39    23.44  -0.21 │   152947119785    152977341368  -0.02 │  581696   582144  -0.08 │
│          coq-performance-tests-lite │  894.89   896.19  -0.15 │  7271920433031   7268164680818   0.05 │ 1940296  1939540   0.04 │
│             rocq-mathcomp-character │   87.89    88.01  -0.14 │   625177239783    624660499694   0.08 │ 1482036  1481800   0.02 │
│                 coq-category-theory │  613.96   614.59  -0.10 │  4536878323412   4537036604614  -0.00 │  938916   936892   0.22 │
│               rocq-mathcomp-algebra │  284.27   284.48  -0.07 │  2143773912493   2143774076836  -0.00 │ 1367020  1362888   0.30 │
│         coq-rewriter-perf-SuperFast │  469.59   469.84  -0.05 │  3746294738158   3745075917268   0.03 │ 1233164  1204820   2.35 │
│              rocq-mathcomp-solvable │   93.42    93.46  -0.04 │   641195605852    641208787245  -0.00 │ 1043100  1041496   0.15 │
│                      coq-coquelicot │   38.26    38.27  -0.03 │   231592629634    231607523326  -0.01 │  830184   826592   0.43 │
│                             coq-vst │  868.53   868.51   0.00 │  6596261801918   6596054233412   0.00 │ 2217684  2216796   0.04 │
│           rocq-metarocq-safechecker │  345.33   345.03   0.09 │  2611792904967   2612136267320  -0.01 │ 1791256  1809068  -0.98 │
│              rocq-mathcomp-fingroup │   23.47    23.44   0.13 │   152241787522    152242275582  -0.00 │  528980   529040  -0.01 │
│                       coq-fourcolor │ 1340.61  1338.53   0.16 │ 12373577783208  12372970671852   0.00 │  892416   892452  -0.00 │
│                        rocq-runtime │   74.21    74.08   0.18 │   535383839892    535285633517   0.02 │  487704   487432   0.06 │
│                 rocq-mathcomp-field │  158.15   157.72   0.27 │  1215240980374   1215318363342  -0.01 │ 1752332  1746660   0.32 │
│                           rocq-core │    6.27     6.24   0.48 │    39064492789     39078224385  -0.04 │  438808   441312  -0.57 │
│               coq-mathcomp-analysis │  892.70   885.64   0.80 │  6758848533640   6707421615822   0.77 │ 1915588  1900684   0.78 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                            │
│  OLD   NEW    DIFF   %DIFF    Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  63.2  64.4  1.1800   1.87%   609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│  35.3  36.2  0.8988   2.55%   974  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                    │
│  25.4  26.2  0.8030   3.16%    12  coq-fourcolor/theories/proof/job499to502.v.html                                                         │
│  29.3  30.0  0.6850   2.33%   974  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                    │
│  45.3  46.0  0.6771   1.49%   118  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                              │
│  45.4  46.1  0.6471   1.43%   118  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html            │
│  99.2  99.9  0.6424   0.65%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  99.0  99.6  0.6104   0.62%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  2.33  2.94  0.6068  26.03%  1001  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  91.8  92.4  0.6004   0.65%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  24.5  25.1  0.5726   2.34%    12  coq-fourcolor/theories/proof/job503to506.v.html                                                         │
│  41.3  41.9  0.5610   1.36%   579  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│ 0.649  1.14  0.4955  76.38%   813  rocq-stdlib/theories/MSets/MSetRBT.v.html                                                               │
│  28.9  29.4  0.4929   1.70%   673  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                                    │
│  23.9  24.4  0.4900   2.05%    12  coq-fourcolor/theories/proof/job486to489.v.html                                                         │
│  37.8  38.2  0.4674   1.24%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html        │
│  47.5  47.9  0.4235   0.89%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                             │
│  17.1  17.5  0.4059   2.38%    12  coq-fourcolor/theories/proof/job550to553.v.html                                                         │
│  17.7  18.0  0.3716   2.10%   670  coq-performance-tests-lite/src/Nia.v.html                                                               │
│  1.16  1.50  0.3401  29.23%  1142  rocq-stdlib/theories/FSets/FMapAVL.v.html                                                               │
│ 0.982  1.32  0.3360  34.23%   408  rocq-stdlib/theories/MSets/MSetAVL.v.html                                                               │
│  11.9  12.2  0.2999   2.51%   194  coq-fiat-crypto-with-bedrock/src/Fancy/Barrett256.v.html                                                │
│   174   175  0.2976   0.17%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  23.7  24.0  0.2906   1.23%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                         │
│  20.7  21.0  0.2844   1.37%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                               │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                            │
│                                                                                                                                        │
│  OLD     NEW     DIFF     %DIFF    Ln                     FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│    201     198  -2.7598   -1.37%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html  │
│   65.5    64.0  -1.4792   -2.26%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                    │
│   79.4    78.2  -1.1861   -1.49%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                        │
│   45.4    44.4  -0.9718   -2.14%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html            │
│   9.17    8.41  -0.7666   -8.36%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                              │
│   43.3    42.6  -0.7475   -1.73%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                        │
│   25.5    25.0  -0.5378   -2.11%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                             │
│ 31.926  31.419  -0.5070   -1.59%    97  coq-vst/veric/binop_lemmas5.v.html                                                             │
│   18.1    17.6  -0.4923   -2.72%    32  coq-performance-tests-lite/src/pattern.v.html                                                  │
│   29.1    28.6  -0.4659   -1.60%    32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html           │
│   25.7    25.3  -0.4551   -1.77%    12  coq-fourcolor/theories/proof/job291to294.v.html                                                │
│   12.0    11.6  -0.4544   -3.78%   388  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html       │
│   27.0    26.6  -0.4391   -1.63%    35  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html           │
│   56.0    55.6  -0.4386   -0.78%   731  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JacobianCoZ.v.html                          │
│   12.1    11.7  -0.4284   -3.54%   324  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/Logic/Existential.v.html       │
│   12.4    12.0  -0.4099   -3.31%   930  coq-unimath/UniMath/CategoryTheory/Hyperdoctrines/PartialEqRels/ExponentialEqs.v.html          │
│   58.5    58.1  -0.3983   -0.68%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                       │
│  0.700   0.319  -0.3814  -54.48%    12  rocq-stdlib/theories/MSets/MSets.v.html                                                        │
│   28.0    27.7  -0.3719   -1.33%    12  coq-fourcolor/theories/proof/job107to164.v.html                                                │
│   44.9    44.5  -0.3663   -0.82%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html               │
│   4.14    3.78  -0.3535   -8.55%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                  │
│   3.44    3.11  -0.3290   -9.56%   196  rocq-stdlib/theories/ZArith/ZModOffset.v.html                                                  │
│   16.0    15.7  -0.3263   -2.04%   356  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/EdwardsXYZT.v.html                     │
│   8.92    8.60  -0.3161   -3.55%   199  coq-mathcomp-odd-order/theories/PFsection12.v.html                                             │
│   7.66    7.34  -0.3151   -4.12%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[Tragicus]

Could someone take a look at this?

[gares]

@coqbot run full ci

[gares]

I think the code makes sense but I don't really like "heads" as the name for the original terms.

Since the change broke some user code, I think it needs to have a changelog entry, and the PR description a comment on what/how breaks. I guess there is less unfolding in goals generated by tactics, but you surely know better.

[Tragicus]

Would something like orig be fine for the name of the original terms?

[gares]

yes, I was thinking about type orig = { left : state; right : state }

[gares]

@coqbot run full ci

[gares]

@coqbot merge now