Add Reflexive,Symmetric,Transitive,Antisymmetric,Asymmetric instances for Rle,Rge,Rlt,Rgt

[JasonGross]

This allows using tactics like transitivity on real inequality goals. Priority 10 is chosen arbitrarily amongst positive numbers (importantly, not 0, so that we don't resolve these instances first when we don't know the relation).

• [] Added / updated test-suite.
• Added changelog.
• [] Added / updated documentation.
• [] Opened overlay pull requests.

[JasonGross]

@coqbot bench

[coqbot-app]

Got more than one checkSuite.

[herbelin]

Looks similar to #16873 which was forgotten!

[herbelin]

Not expert enough about instances though to tell if the level 10 is good or not.

[JasonGross]

@herbelin Do you want to assign? Maybe someone in @coq/typeclasses-maintainers or @coq/stdlib-maintainers can weigh in on the instance priorities?

Automatic priorities are assigned to be the number of typeclass assumptions, so 10 will trigger quite late. As far as existing priorities go, we have

$ git grep 'Reflexive\|Symmetric\|Transitive' 'theories/' | grep '|\s*[0-9]
\+'
theories/Classes/CEquivalence.v:  Reflexive (pointwise_relation A eqB) | 9.
theories/Classes/CEquivalence.v:  Symmetric (pointwise_relation A eqB) | 9.
theories/Classes/CEquivalence.v:  Transitive (pointwise_relation A eqB) | 9.
theories/Classes/CMorphisms.v:  `(Transitive A R) {x} : Proper (R --> flip arrow) (R x) | 3.
theories/Classes/CMorphisms.v:    `(Transitive A R) {x} : Proper (R ++> arrow) (R x) | 3.
theories/Classes/CMorphisms.v:  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip arrow) R | 2.
theories/Classes/CRelationClasses.v:    #[global] PreOrder_Reflexive :: Reflexive R | 2 ;
theories/Classes/CRelationClasses.v:    #[global] PreOrder_Transitive :: Transitive R | 2 }.
theories/Classes/CRelationClasses.v:    #[global] PER_Symmetric :: Symmetric R | 3 ;
theories/Classes/CRelationClasses.v:    #[global] PER_Transitive :: Transitive R | 3 }.
theories/Classes/Equivalence.v: Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1.
theories/Classes/Equivalence.v:Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1.
theories/Classes/Equivalence.v:Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
theories/Classes/Equivalence.v:  Reflexive (pointwise_relation A eqB) | 9.
theories/Classes/Equivalence.v:  Symmetric (pointwise_relation A eqB) | 9.
theories/Classes/Equivalence.v:  Transitive (pointwise_relation A eqB) | 9.
theories/Classes/Morphisms.v:  `(Transitive A R) {x} : Proper (R --> flip impl) (R x) | 3.
theories/Classes/Morphisms.v:    `(Transitive A R) {x} : Proper (R ++> impl) (R x) | 3.
theories/Classes/Morphisms.v:  `(Transitive A R) : Proper (R ==> (@eq A) ==> flip impl) R | 2.
theories/Classes/RelationClasses.v:    #[global] PreOrder_Reflexive :: Reflexive R | 2 ;
theories/Classes/RelationClasses.v:    #[global] PreOrder_Transitive :: Transitive R | 2 }.
theories/Classes/RelationClasses.v:    #[global] PER_Symmetric :: Symmetric R | 3 ;
theories/Classes/RelationClasses.v:    #[global] PER_Transitive :: Transitive R | 3 }.
theories/Numbers/NatInt/NZGcd.v:Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
theories/Numbers/NatInt/NZGcd.v:Instance divide_transitive : Transitive divide | 5 := divide_trans.
theories/Numbers/Natural/Abstract/NGcd.v:#[global] Instance divide_reflexive : Reflexive divide | 5 := divide_refl.
theories/Numbers/Natural/Abstract/NGcd.v:#[global] Instance divide_transitive : Transitive divide | 5 := divide_trans.
theories/ssr/ssrsetoid.v:    ssrclasses.Reflexive R | 12.

Really the thing we want here is #14126, to declare that these instances should only trigger when the relation is not an evar, but until we have that, giving a priority of anything above 5 seems reasonable.

[JasonGross]

Is itauto broken everywhere?

[JasonGross]

@coqbot bench

[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-stdlib │  390.63   394.72  -1.04 │  1655618205557   1673681797019  -1.08 │  1406286104636   1405729919851   0.04 │  751928   755808  -0.51 │
│           coq-mathcomp-field │  211.82   213.36  -0.72 │   954071574300    961424855646  -0.76 │  1711609316495   1711681595182  -0.00 │ 1482940  1483488  -0.04 │
│                  coq-coqutil │   41.00    41.21  -0.51 │   182095164490    182014650045   0.04 │   263649593891    263624210678   0.01 │  563496   565052  -0.28 │
│                      coq-vst │  855.40   859.31  -0.46 │  3846291050186   3864555732016  -0.47 │  6356842355466   6355095418450   0.03 │ 2004388  2002660   0.09 │
│ coq-fiat-crypto-with-bedrock │ 6436.28  6459.13  -0.35 │ 28967703832837  29075169587853  -0.37 │ 53408268960860  53410149008784  -0.00 │ 2421340  2421624  -0.01 │
│   coq-performance-tests-lite │  776.15   778.86  -0.35 │  3460270232790   3470116201162  -0.28 │  6146639895651   6145202607202   0.02 │ 1895888  1896836  -0.05 │
│                coq-fiat-core │   60.92    61.07  -0.25 │   258303178303    258668652536  -0.14 │   380792971144    380992754170  -0.05 │  495780   492604   0.64 │
│                    coq-color │  236.58   237.16  -0.24 │  1055523312808   1056805420620  -0.12 │  1544689302639   1545292666061  -0.04 │ 1130528  1128968   0.14 │
│          coq-category-theory │  758.64   760.45  -0.24 │  3442891885263   3450545953753  -0.22 │  5870112833618   5870079875663   0.00 │  879068   881112  -0.23 │
│       coq-mathcomp-odd-order │  874.16   875.35  -0.14 │  3980498651185   3983487638077  -0.08 │  6713708281222   6713794402715  -0.00 │ 1580232  1581172  -0.06 │
│                     coq-hott │  155.88   156.04  -0.10 │   697960084321    697102941984   0.12 │  1102667131257   1102822404449  -0.01 │  518536   520540  -0.38 │
│             coq-math-classes │   88.20    88.24  -0.05 │   394942420208    395642470999  -0.18 │   552760083177    552816510090  -0.01 │  524536   525116  -0.11 │
│         coq-mathcomp-algebra │  473.21   473.34  -0.03 │  2132340795360   2134651013177  -0.11 │  3984803335195   3984772892123   0.00 │ 1376136  1375484   0.05 │
│                 coq-bedrock2 │  358.37   358.44  -0.02 │  1617179965115   1617392635308  -0.01 │  3156835565916   3157394236960  -0.02 │  869520   870840  -0.15 │
│       coq-mathcomp-ssreflect │  183.95   183.97  -0.01 │   830993305005    831777278478  -0.09 │  1478386751773   1478422613727  -0.00 │ 1289020  1288832   0.01 │
│        coq-engine-bench-lite │  161.97   161.93   0.02 │   688843535180    688570981082   0.04 │  1278337479900   1276171099570   0.17 │ 1322700  1277020   3.58 │
│         coq-metacoq-template │  165.24   165.19   0.03 │   729767914798    728852291162   0.13 │  1160016647444   1160214706940  -0.02 │ 1285784  1284456   0.10 │
│        coq-mathcomp-fingroup │   38.69    38.67   0.05 │   175107315812    175179705567  -0.04 │   265056433484    265148030415  -0.03 │  562452   561128   0.24 │
│                coq-fourcolor │ 1548.20  1547.01   0.08 │  6845325410225   6844668035115   0.01 │ 12470193367627  12470565047219  -0.00 │ 2060700  2060624   0.00 │
│                  coq-bignums │   29.05    29.01   0.14 │   130555952845    130730901430  -0.13 │   188311056157    188404447956  -0.05 │  490532   488440   0.43 │
│               coq-verdi-raft │  587.71   586.44   0.22 │  2663757010601   2659204148318   0.17 │  4142082738945   4142477400026  -0.01 │  818140   818084   0.01 │
│                    coq-verdi │   49.75    49.64   0.22 │   223237663316    222690955885   0.25 │   339981056337    340362430034  -0.11 │  528692   526636   0.39 │
│                coq-perennial │ 6453.52  6438.13   0.24 │ 29198398598687  29126992329234   0.25 │ 48767205017371  48766494422836   0.00 │ 2219660  2219580   0.00 │
│                  coq-unimath │ 1642.26  1638.30   0.24 │  7430005839898   7414696758797   0.21 │ 13895382089406  13894031471828   0.01 │ 1299332  1299172   0.01 │
│                 coq-rewriter │  358.58   357.41   0.33 │  1615996072386   1612294227616   0.23 │  2663190427282   2662693494452   0.02 │ 1224888  1224708   0.01 │
│  coq-rewriter-perf-SuperFast │  745.43   742.48   0.40 │  3320628240445   3307670080105   0.39 │  5690719020564   5689175022971   0.03 │ 1329632  1329400   0.02 │
│          coq-metacoq-erasure │  313.19   311.92   0.41 │  1408698381612   1401112995189   0.54 │  2231717213077   2232213715979  -0.02 │ 2033656  2031560   0.10 │
│      coq-metacoq-safechecker │  378.59   376.75   0.49 │  1722790941284   1714150266783   0.50 │  2872086880302   2872186275096  -0.00 │ 1964096  1964588  -0.03 │
│            coq-metacoq-pcuic │  621.65   618.62   0.49 │  2793983217525   2781107775834   0.46 │  4128844537630   4129603656423  -0.02 │ 1991748  1993360  -0.08 │
│                     coq-core │  118.01   117.40   0.52 │   458934393517    455955448323   0.65 │   491117829098    491128812791  -0.00 │  367872   367948  -0.02 │
│     coq-metacoq-translations │   18.45    18.35   0.54 │    80472384229     80765339456  -0.36 │   131688351008    131685199720   0.00 │  905072   906220  -0.13 │
│                coq-equations │   11.24    11.17   0.63 │    48067926936     48081985321  -0.03 │    76343084037     76264338465   0.10 │  417236   416900   0.08 │
│                 coq-compcert │  287.22   285.39   0.64 │  1284682412665   1274486001542   0.80 │  1961046352273   1961852947255  -0.04 │ 1141852  1144404  -0.22 │
│                     coq-corn │  805.18   799.55   0.70 │  3628340111240   3603690468064   0.68 │  5632879234290   5632057830936   0.01 │  778448   777476   0.13 │
│       coq-mathcomp-character │  132.00   130.99   0.77 │   597277851435    593108574467   0.70 │   964810061294    964833592231  -0.00 │ 1261348  1258300   0.24 │
│        coq-mathcomp-solvable │  145.19   144.04   0.80 │   657176553650    653050697223   0.63 │  1057184250559   1057226963862  -0.00 │  912540   915372  -0.31 │
│             coq-fiat-parsers │  335.61   332.83   0.84 │  1481195421052   1469442956704   0.80 │  2458560852567   2458345058498   0.01 │ 2435872  2437608  -0.07 │
│                 coq-coqprime │   48.18    47.74   0.92 │   215136226798    213694232777   0.67 │   328477181577    328497953051  -0.01 │  778640   780676  -0.26 │
│            coq-iris-examples │  491.54   486.24   1.09 │  2216460935457   2192041707723   1.11 │  3373638379419   3373531225423   0.00 │ 1081096  1082248  -0.11 │
│               coq-coquelicot │   39.35    38.61   1.92 │   173474593358    170711952805   1.62 │   242493148183    239572454714   1.22 │  810960   808820   0.26 │
└──────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SLOW DOWNS                                                       │
│                                                                                                                              │
│   OLD       NEW      DIFF    %DIFF    Ln                  FILE                                                               │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  63.3940   64.4470  1.0530    1.66%   139  coq-fiat-parsers/src/Parsers/Refinement/SharpenedJSON.v.html                      │
│ 142.2520  143.0450  0.7930    0.56%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html     │
│  42.4650   43.2120  0.7470    1.76%   995  coq-perennial/src/program_proof/vrsm/replica/apply_proof.v.html                   │
│  17.7580   18.2090  0.4510    2.54%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                         │
│  28.4440   28.8830  0.4390    1.54%    12  coq-fourcolor/theories/job517to530.v.html                                         │
│  31.6230   32.0540  0.4310    1.36%    12  coq-fourcolor/theories/job563to588.v.html                                         │
│  34.8370   35.2560  0.4190    1.20%    12  coq-fourcolor/theories/job254to270.v.html                                         │
│  26.3080   26.7070  0.3990    1.52%  2293  coq-perennial/src/goose_lang/logical_reln_fund.v.html                             │
│   0.0760    0.4600  0.3840  505.26%  1726  coq-perennial/src/program_proof/vrsm/configservice/config_proof.v.html            │
│  39.7470   40.1230  0.3760    0.95%    85  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/AffineProofs.v.html            │
│  27.2850   27.6450  0.3600    1.32%    12  coq-fourcolor/theories/job503to506.v.html                                         │
│  25.1840   25.5120  0.3280    1.30%   373  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html     │
│  29.1250   29.4530  0.3280    1.13%   912  coq-perennial/src/program_proof/vrsm/reconfig/proof.v.html                        │
│   0.5890    0.9160  0.3270   55.52%   200  coq-stdlib/Numbers/HexadecimalNat.v.html                                          │
│  22.4530   22.7630  0.3100    1.38%    12  coq-fourcolor/theories/job546to549.v.html                                         │
│  18.9670   19.2560  0.2890    1.52%   875  coq-perennial/src/program_proof/simple/setattr.v.html                             │
│  27.0290   27.3140  0.2850    1.05%   823  coq-perennial/src/program_proof/aof/proof.v.html                                  │
│  12.9480   13.2300  0.2820    2.18%  1385  coq-perennial/src/program_proof/txn/twophase_sub_logical_reln_defs.v.html         │
│   1.3480    1.6210  0.2730   20.25%   937  coq-vst/veric/binop_lemmas2.v.html                                                │
│  24.0150   24.2880  0.2730    1.14%  1449  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Examples/KleisliEnriched.v.html   │
│   0.7350    1.0030  0.2680   36.46%    32  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/Primitives.v.html            │
│  14.1060   14.3640  0.2580    1.83%   315  coq-fiat-crypto-with-bedrock/src/Bedrock/Group/ScalarMult/MontgomeryLadder.v.html │
│   0.2510    0.5080  0.2570  102.39%  1363  coq-stdlib/FSets/FMapAVL.v.html                                                   │
│  54.8930   55.1330  0.2400    0.44%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                       │
│  18.0480   18.2840  0.2360    1.31%    32  coq-performance-tests-lite/src/pattern.v.html                                     │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                  TOP 25 SPEED UPS                                                                  │
│                                                                                                                                                    │
│   OLD       NEW      DIFF     %DIFF   Ln                      FILE                                                                                 │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 137.5340  136.3630  -1.1710   -0.85%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│ 137.3260  136.1650  -1.1610   -0.85%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│   3.5760    2.7470  -0.8290  -23.18%  487  coq-stdlib/Numbers/HexadecimalFacts.v.html                                                              │
│  55.4420   54.6880  -0.7540   -1.36%  609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│   7.8450    7.1140  -0.7310   -9.32%  288  coq-perennial/src/program_proof/vrsm/paxos/becomeleader_proof.v.html                                    │
│ 113.6950  113.1000  -0.5950   -0.52%   48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                                 │
│  40.3620   39.8970  -0.4650   -1.15%  827  coq-vst/veric/binop_lemmas4.v.html                                                                      │
│   1.5210    1.1270  -0.3940  -25.90%  853  coq-stdlib/FSets/FMapAVL.v.html                                                                         │
│  39.8290   39.4550  -0.3740   -0.94%  835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                  │
│   9.5930    9.2320  -0.3610   -3.76%   87  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                                   │
│ 162.2940  161.9620  -0.3320   -0.20%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  68.3590   68.0360  -0.3230   -0.47%  103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│  22.9860   22.6780  -0.3080   -1.34%  233  coq-fiat-crypto-with-bedrock/src/Curves/EdwardsMontgomery.v.html                                        │
│  61.1510   60.8470  -0.3040   -0.50%   27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│  45.9020   45.6050  -0.2970   -0.65%  558  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html       │
│  23.3860   23.0910  -0.2950   -1.26%  660  coq-perennial/src/program_proof/vrsm/replica/roapply_proof.v.html                                       │
│  53.0960   52.8010  -0.2950   -0.56%   50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                    │
│  10.4640   10.1710  -0.2930   -2.80%  603  coq-unimath/UniMath/Algebra/GroupAction.v.html                                                          │
│   5.3610    5.0680  -0.2930   -5.47%  369  coq-fiat-crypto-with-bedrock/src/Arithmetic/BinaryExtendedGCD.v.html                                    │
│  43.3120   43.0200  -0.2920   -0.67%  236  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html               │
│  15.8780   15.5880  -0.2900   -1.83%  417  coq-verdi-raft/raft-proofs/LeaderLogsLogMatchingProof.v.html                                            │
│  22.9290   22.6400  -0.2890   -1.26%    6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeI.v.html     │
│  19.2870   19.0090  -0.2780   -1.44%   40  coq-fiat-crypto-with-bedrock/src/PushButtonSynthesis/SolinasReductionReificationCache.v.html            │
│  19.9070   19.6430  -0.2640   -1.33%  413  coq-perennial/src/program_proof/vrsm/replica/setstate_proof.v.html                                      │
│  11.2600   11.0030  -0.2570   -2.28%   55  coq-category-theory/Construction/Comma/Natural/Transformation.v.html                                    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

• 🪑 GitLab Bench Job

[herbelin]

@coqbot merge now