Slightly less nonsensical term equality test in progress tactical.

[ppedrot]

For what seems to amount to historical reasons, the progress tactical considered that two unifiable sorts were equal and thus not resulting in a progress. This is very weird and unlike the corresponding treatment of instances. A quick blame indicates that the intended behaviour may have been to check quotient by universe unification through the evarmap, which is weaker than enforcing this quotient. This commit precisely does that and makes the sort code behave like the instance code.

[yannl35133]

You can remove the reference now that the evar_map is only read from.

[ppedrot]

CI green, as expected nobody relies on that.

[ppedrot]

Out of curiosity, let's @coqbot bench

[SkySkimmer]

why do instances use ugraph aware comparison but this only checks the flexible instantiations?

[ppedrot]

Indeed, you're right. For uniformity we should do the same in both cases, but it's not obvious to me which is the more reasonable choice. AFAICT ugraph-aware comparison is slightly more surprising because the printer still treats equivalent universes differently. (Not that I believe it matters a lot in practice, but once again having a spec for this low-level function should be important.)

[coqbot-app]

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│             rocq-mathcomp-ssreflect │    1.10     1.14  -3.51 │     7669491298      7666782484   0.04 │  593600   591544   0.35 │
│          rocq-metarocq-translations │   15.15    15.33  -1.17 │   108787600156    108807759643  -0.02 │  780980   782360  -0.18 │
│                 rocq-metarocq-utils │   24.48    24.65  -0.69 │   159073769470    159100925565  -0.02 │  591000   590960   0.01 │
│ coq-neural-net-interp-computed-lite │  234.77   236.35  -0.67 │  2264503133777   2264539269654  -0.00 │  882352   880400   0.22 │
│                           rocq-core │    6.73     6.76  -0.44 │    41325298660     41330510452  -0.01 │  444444   444512  -0.02 │
│                      coq-verdi-raft │  491.71   493.03  -0.27 │  3392077717836   3392168487634  -0.00 │  816892   814064   0.35 │
│                         coq-unimath │ 1825.20  1828.16  -0.16 │ 15179484924902  15179671443483  -0.00 │ 1086008  1085316   0.06 │
│              rocq-mathcomp-solvable │   98.83    98.99  -0.16 │   666804356446    666797591557   0.00 │ 1098568  1098576  -0.00 │
│                      rocq-equations │    8.52     8.53  -0.12 │    58799580322     58811342070  -0.02 │  400764   399540   0.31 │
│                         rocq-stdlib │  420.58   420.83  -0.06 │  1508047570747   1508281145136  -0.02 │  627824   632428  -0.73 │
│                 coq-category-theory │  639.55   639.67  -0.02 │  4764675256579   4781223692711  -0.35 │ 6747636  6746192   0.02 │
│               coq-mathcomp-analysis │ 1158.18  1158.38  -0.02 │  8441103639076   8440845663988   0.00 │ 1969476  1968884   0.03 │
│                         coq-coqutil │   47.14    47.13   0.02 │   291051153062    291067948854  -0.01 │  568172   566168   0.35 │
│                    coq-math-classes │   82.29    82.27   0.02 │   499833139545    499849531454  -0.00 │  514836   514944  -0.02 │
│              rocq-metarocq-template │   81.76    81.74   0.02 │   560257275360    560092636116   0.03 │ 1082148  1082656  -0.05 │
│                           coq-color │  229.93   229.87   0.03 │  1456307856912   1456431875467  -0.01 │ 1151972  1151256   0.06 │
│                        coq-coqprime │   56.44    56.42   0.04 │   390850709679    390887350644  -0.01 │  821896   821852   0.01 │
│                        rocq-bignums │   24.84    24.83   0.04 │   158038299918    158020199593   0.01 │  461292   458660   0.57 │
│               coq-engine-bench-lite │  128.30   128.15   0.12 │   950930756552    948899118043   0.21 │ 1103428  1103456  -0.00 │
│                   coq-iris-examples │  366.40   365.86   0.15 │  2387890465568   2387864180160   0.00 │ 1068068  1069324  -0.12 │
│                       coq-fiat-core │   55.59    55.50   0.16 │   336192000559    336196169811  -0.00 │  482968   482972  -0.00 │
│                       coq-fourcolor │ 1353.16  1350.82   0.17 │ 12429785319827  12429841141445  -0.00 │ 1017892  1017984  -0.01 │
│                 rocq-mathcomp-field │  193.82   193.48   0.18 │  1451434135703   1451675908205  -0.02 │ 2287780  2285960   0.08 │
│        coq-fiat-crypto-with-bedrock │ 7220.33  7206.47   0.19 │ 59425899387516  59429776146108  -0.01 │ 2849044  2847400   0.06 │
│  rocq-mathcomp-group-representation │  104.23   104.02   0.20 │   729841499904    729720455661   0.02 │ 1703544  1703580  -0.00 │
│                      coq-coquelicot │   38.96    38.88   0.21 │   235022022864    235103209688  -0.03 │  830284   828824   0.18 │
│                 rocq-metarocq-pcuic │  603.61   602.30   0.22 │  3882241117668   3882901253040  -0.02 │ 1692488  1693740  -0.07 │
│               rocq-mathcomp-algebra │  331.97   331.19   0.24 │  2434008479944   2433949729909   0.00 │ 1361188  1360320   0.06 │
│               rocq-metarocq-erasure │  439.89   438.82   0.24 │  2998092981005   2998254754747  -0.01 │ 1804824  1812052  -0.40 │
│                            coq-corn │  639.40   637.71   0.27 │  4326512638551   4326518244032  -0.00 │  617256   619364  -0.34 │
│                    coq-fiat-parsers │  273.28   272.51   0.28 │  2090325908301   2090344880444  -0.00 │ 2032968  2032976  -0.00 │
│         coq-rewriter-perf-SuperFast │  466.77   465.38   0.30 │  3653033343482   3652880363088   0.00 │ 1238524  1272180  -2.65 │
│                        rocq-runtime │   76.48    76.24   0.31 │   551005915462    550937915753   0.01 │  494640   494160   0.10 │
│          rocq-mathcomp-finite-group │   26.66    26.55   0.41 │   172604131523    172624146966  -0.01 │  570548   572240  -0.30 │
│                rocq-metarocq-common │   41.50    41.32   0.44 │   267935242988    267923985539   0.00 │  904844   902132   0.30 │
│          coq-performance-tests-lite │  886.71   882.65   0.46 │  7090098255666   7088593732318   0.02 │ 1307720  1307424   0.02 │
│                  rocq-mathcomp-boot │   39.44    39.25   0.48 │   232436028970    232390970833   0.02 │  655828   655424   0.06 │
│                        coq-rewriter │  332.04   330.26   0.54 │  2454087767863   2454123492205  -0.00 │ 1430072  1432128  -0.14 │
│              coq-mathcomp-odd-order │  602.90   599.61   0.55 │  4275215038430   4274572829751   0.02 │ 2655340  2655364  -0.00 │
│                            coq-hott │  158.06   157.11   0.60 │  1058589559989   1058635562553  -0.00 │  477016   477160  -0.03 │
│           rocq-metarocq-safechecker │  319.77   317.81   0.62 │  2380333208358   2380215488795   0.00 │ 1726660  1727144  -0.03 │
│                        coq-bedrock2 │  359.04   356.00   0.85 │  2967983209133   2968384656472  -0.01 │  814224   811116   0.38 │
│                 rocq-mathcomp-order │   81.97    81.25   0.89 │   600803856008    600788478801   0.00 │ 1606312  1606056   0.02 │
│                           rocq-elpi │   16.42    16.27   0.92 │   116413322809    116406307694   0.01 │  448672   450168  -0.33 │
│                           coq-verdi │   43.61    43.17   1.02 │   288136059945    288091787430   0.02 │  520912   521660  -0.14 │
│                            coq-core │    2.78     2.74   1.46 │    18576590597     18577622482  -0.01 │   90720    90780  -0.07 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install
coq-compcert (dependency install failed in NEW)
coq-vst (dependency install failed in NEW)

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                         TOP 25 SLOW DOWNS                                                          │
│                                                                                                                                    │
│  OLD    NEW    DIFF    %DIFF    Ln                    FILE                                                                         │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  63.9   66.2  2.3070    3.61%   608  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html │
│  63.5   65.4  1.9852    3.13%   608  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                   │
│  43.9   45.1  1.2022    2.74%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html           │
│  34.7   35.7  0.9941    2.87%   194  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  89.7   90.7  0.9580    1.07%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  24.7   25.7  0.9329    3.77%   788  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│  8.97   9.83  0.8613    9.61%   435  coq-mathcomp-odd-order/theories/PFsection12.v.html                                            │
│  44.0   44.8  0.7856    1.79%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html              │
│  42.3   43.1  0.7660    1.81%     2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                       │
│  23.6   24.3  0.6728    2.85%   782  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│  21.4   22.1  0.6521    3.04%    49  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                       │
│  22.1   22.7  0.5529    2.50%   776  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│   107    107  0.5355    0.50%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                        │
│  19.3   19.8  0.5209    2.70%   559  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│  18.1   18.6  0.4915    2.71%    32  coq-performance-tests-lite/src/pattern.v.html                                                 │
│  17.9   18.3  0.4904    2.75%   571  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│ 0.346  0.807  0.4605  132.99%   682  rocq-stdlib/theories/Numbers/DecimalFacts.v.html                                              │
│  16.5   16.9  0.4602    2.80%   762  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                          │
│  89.9   90.3  0.4550    0.51%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html               │
│  10.8   11.2  0.4053    3.77%   159  coq-fiat-crypto-with-bedrock/src/Bedrock/P256.v.html                                          │
│  7.86   8.27  0.4030    5.13%  1331  coq-mathcomp-odd-order/theories/PFsection9.v.html                                             │
│ 0.451  0.848  0.3967   87.91%   393  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                            │
│  20.5   20.9  0.3832    1.87%    24  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/MultiRetSplit.v.html                         │
│  42.9   43.3  0.3750    0.87%   256  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Jacobian.v.html                                 │
│  23.7   24.1  0.3566    1.50%    13  coq-fourcolor/theories/proof/job295to298.v.html                                               │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                            TOP 25 SPEED UPS                                                             │
│                                                                                                                                         │
│  OLD    NEW     DIFF     %DIFF    Ln                     FILE                                                                           │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│   201     199  -1.7399   -0.87%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html    │
│  41.7    40.7  -1.0042   -2.41%   235  coq-category-theory/Construction/DecoratedCospan/Category.v.html                                 │
│  18.6    17.9  -0.7117   -3.82%   481  coq-verdi-raft/theories/RaftProofs/EndToEndLinearizability.v.html                                │
│  28.9    28.3  -0.5852   -2.02%   305  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│  31.4    30.9  -0.5126   -1.63%   180  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│ 0.737   0.239  -0.4972  -67.49%   374  rocq-stdlib/theories/Sorting/SetoidList.v.html                                                   │
│  31.2    30.7  -0.4960   -1.59%   198  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  31.3    30.8  -0.4833   -1.54%   157  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  31.2    30.8  -0.4780   -1.53%   139  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  31.2    30.8  -0.4728   -1.51%   166  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  31.5    31.0  -0.4382   -1.39%   148  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  39.4    39.0  -0.3887   -0.99%  1423  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/FlatToRiscvFunctions.v.html │
│ 0.667   0.279  -0.3883  -58.22%     1  rocq-stdlib/theories/micromega/SatDivMod.v.html                                                  │
│  1.03   0.647  -0.3838  -37.23%   160  rocq-stdlib/theories/Numbers/HexadecimalNat.v.html                                               │
│  21.6    21.2  -0.3812   -1.76%   651  rocq-stdlib/theories/Zmod/ZmodBase.v.html                                                        │
│  32.5    32.1  -0.3794   -1.17%   121  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  31.3    30.9  -0.3400   -1.09%   214  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html             │
│  54.4    54.0  -0.3346   -0.62%   296  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/Addchain.v.html                               │
│  49.1    48.8  -0.3256   -0.66%   376  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                      │
│ 0.615   0.291  -0.3239  -52.67%   110  rocq-stdlib/theories/Numbers/HexadecimalPos.v.html                                               │
│  7.27    6.95  -0.3209   -4.41%    35  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html     │
│ 0.312  0.0148  -0.2974  -95.25%   117  coq-mathcomp-analysis/theories/derive.v.html                                                     │
│  34.3    34.0  -0.2824   -0.82%   898  coq-fiat-crypto-with-bedrock/src/Bedrock/Secp256k1/JoyeLadder.v.html                             │
│  26.7    26.4  -0.2808   -1.05%   375  coq-unimath/UniMath/ModelCategories/Generated/LNWFSMonoidalStructure.v.html                      │
│  42.9    42.6  -0.2808   -0.65%   221  coq-fiat-crypto-with-bedrock/src/Bedrock/P256/Coord32.v.html                                     │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[ppedrot]

I have one more argument in favour of equality rather than unification: the former is actually monotonous w.r.t. evarmap extension, while the latter isn't. Without this property, the fast path on defined evars from tclPROGRESS is actually unsound.

[SkySkimmer]

For that fast path to be sound we would need equality ignoring definition of flexibles right?

[ppedrot]

Formally we need for all terms c1, c2 and evarmaps σ1 ⊆ σ2, c1 ={syntax} c2 implies nf(c1, σ1) ∼ nf(c2, σ2), where ∼ is the equivalence relation considered for progress. AFAIU, adding flexible equalities is fine for this to hold, so taking ∼ to be either equality using level evarmap normalization or level equivalence in ugraph are sound.

[SkySkimmer]

What's ={syntax}?

[ppedrot]

Syntactic equality i.e. without evar expansion.

[SkySkimmer]

Anyway pick equality or equality up to ugraph and use it for both instances and sort, then this should be ready to merge IMO

[yannl35133]

I would argue that the "correct" test is : if the quality variables or universe variables are both flexible, then they should be "indistinguishable", and if not they should be syntactically equal. Since we don't want to know whether flexible things are distinguishable, we have to wonder whether we assume they always are distinguishable (then, we go for syntactic equality) or indistinguishable (then we only test for flexibility and if not for syntactic equality).