Hint Constants Opaque : rewrite

[SkySkimmer]

Fix #8080

Probably not all that compatible but let's see

[coqbot-app]

The job library:ci-fiat_crypto_legacy has failed in allow failure mode
ping @JasonGross

[SkySkimmer]

bench (enough stuff is passing to make me curious) https://gitlab.com/coq/coq/-/jobs/2044617565

[ejgallego]

bench

@SkySkimmer is the bench using 4.07.1 ? IMHO it could use and update if so.

[coqbot-app]

🔴 CI failures at commit 44c51dc without any failure in the test-suite

✔️ Corresponding jobs for the base commit 7d14801 succeeded

❔ Ask me to try to extract minimal test cases that can be added to the test-suite

🏃 @coqbot ci minimize will minimize the following targets: ci-argosy, ci-bedrock2, ci-color, ci-cross_crypto, ci-fiat_crypto_legacy, ci-fiat_parsers, ci-iris, ci-math_classes, ci-metacoq, ci-perennial, ci-quickchick, ci-relation_algebra, ci-rewriter, ci-vst

• You can also pass me a specific list of targets to minimize as arguments.

[SkySkimmer]

┌────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬───────────────────────────────────────┬─────────────────────────┬─────────────────┐
│                            │      user time [s]      │              CPU cycles               │           CPU instructions            │  max resident mem [KB]  │   mem faults    │
│                            │                         │                                       │                                       │                         │                 │
│               package_name │     NEW      OLD  PDIFF │            NEW             OLD  PDIFF │            NEW             OLD  PDIFF │     NEW      OLD  PDIFF │ NEW  OLD  PDIFF │
├────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼───────────────────────────────────────┼─────────────────────────┼─────────────────┤
│             coq-verdi-raft │  553.83   556.17  -0.42 │  2523129190016   2535237556206  -0.48 │  3915441377350   3917197413918  -0.04 │ 1216000  1216584  -0.05 │   0    0    nan │
│                  coq-verdi │   47.23    47.39  -0.34 │   213767542737    213688190592   0.04 │   317580154402    317525469523   0.02 │  820536   822256  -0.21 │   0    0    nan │
│         coq-mathcomp-field │  110.81   111.17  -0.32 │   505688691021    507443662490  -0.35 │   837475015502    837500837318  -0.00 │  649656   653548  -0.60 │   0    0    nan │
│             coq-coquelicot │   33.46    33.56  -0.30 │   149782624030    150110599997  -0.22 │   196962639106    196781298385   0.09 │  745400   745380   0.00 │   4    0    nan │
│              coq-fourcolor │ 1495.59  1498.06  -0.16 │  6601187275822   6611349539167  -0.15 │ 12071636522490  12071351634196   0.00 │  725456   725488  -0.00 │   0    0    nan │
│               coq-compcert │  278.29   278.47  -0.06 │  1251277931131   1252762549345  -0.12 │  1879866278901   1879803116445   0.00 │ 1099092  1097928   0.11 │   0    0    nan │
│ coq-performance-tests-lite │  774.00   774.35  -0.05 │  3474096282786   3477053214638  -0.09 │  5911115144093   5914072304930  -0.05 │ 1824356  1823928   0.02 │   3    0    nan │
│     coq-mathcomp-character │   75.99    76.00  -0.01 │   346485763014    346718747920  -0.07 │   525775942282    525741027872   0.01 │  733664   733648   0.00 │   0    0    nan │
│                coq-bignums │   27.72    27.72   0.00 │   125285484189    125194982726   0.07 │   172227366350    172239032411  -0.01 │  465404   464068   0.29 │   0    0    nan │
│                   coq-core │   96.74    96.72   0.02 │   381659837525    384204843005  -0.66 │   433482348775    433475984028   0.00 │  273168   272756   0.15 │   0    0    nan │
│                coq-unimath │ 3933.84  3930.45   0.09 │ 17887865643136  17875787303078   0.07 │ 35817107784770  35796865812585   0.06 │ 3811284  3826692  -0.40 │   0    0    nan │
│      coq-mathcomp-fingroup │   23.54    23.50   0.17 │   107574775712    107213049281   0.34 │   155956339811    155900630631   0.04 │  483592   483268   0.07 │   0    0    nan │
│                   coq-hott │  152.77   152.40   0.24 │   686733344694    685854957906   0.13 │  1072370775091   1072328938347   0.00 │  569552   569792  -0.04 │   0    0    nan │
│        coq-category-theory │ 1611.59  1607.30   0.27 │  7365238118535   7343819948153   0.29 │ 15247804957147  15247027629184   0.01 │ 1479664  1327472  11.46 │   0    0    nan │
│                 coq-stdlib │  405.98   404.79   0.29 │  1636687613557   1632087981265   0.28 │  1412063423183   1412128496817  -0.00 │  599272   599364  -0.02 │   0    0    nan │
│     coq-mathcomp-odd-order │  549.53   547.84   0.31 │  2513408797868   2505157866794   0.33 │  4256012588924   4255847981124   0.00 │  932860   932476   0.04 │   0    0    nan │
│      coq-mathcomp-solvable │   87.45    87.17   0.32 │   398703436331    397491298296   0.30 │   610992563557    611003160996  -0.00 │  670128   668416   0.26 │   0    0    nan │
│                 coq-flocq3 │   76.33    76.03   0.39 │   346258781985    345461174571   0.23 │   453713384018    453726979237  -0.00 │  989580   988488   0.11 │   9    0    nan │
│               coq-coqprime │  179.29   178.54   0.42 │   817166432818    813513511282   0.45 │  1552871175311   1552780341647   0.01 │  905092   826116   9.56 │   0    0    nan │
│     coq-mathcomp-ssreflect │   26.09    25.98   0.42 │   117852045409    117310247495   0.46 │   148243974321    148251165429  -0.00 │  532308   534084  -0.33 │   0    0    nan │
│                 coq-geocoq │  691.86   688.27   0.52 │  3146596242317   3126491165557   0.64 │  4931750514506   4931163094967   0.01 │ 1075380  1076156  -0.07 │   0    0    nan │
│       coq-mathcomp-algebra │   63.85    63.29   0.88 │   290264910303    288151051060   0.73 │   397669327411    397793760505  -0.03 │  554060   554796  -0.13 │   0    0    nan │
│      coq-engine-bench-lite │  179.11   177.50   0.91 │   768641377682    760668066185   1.05 │  1492244590021   1487270334778   0.33 │ 1175824  1173956   0.16 │   0    0    nan │
└────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┴─────────────────┘

[SkySkimmer]

I had a look at some failures:
mathclasses is having trouble with rewriting through the alias layer needed for its definitional classes, typically

Require Import PeanoNat.
Class SgOp A := sgop : A -> A -> A.

Instance plus_op : SgOp nat := plus.

Goal sgop 1 0 = 2.
  Fail setoid_rewrite Nat.add_comm.
  Hint Transparent sgop plus_op : rewrite.
  setoid_rewrite Nat.add_comm.

metacoq has

• a couple aliases like https://github.com/MetaCoq/metacoq/blob/cd3bc92bc97d974b917b3a6d55a4b9f595e69fa6/template-coq/theories/common/uGraph.v#L27 where the alias and its unfold can both appear due to type inference.
• an issue with https://github.com/MetaCoq/metacoq/blob/cd3bc92bc97d974b917b3a6d55a4b9f595e69fa6/template-coq/theories/Universes.v#L1119-L1121 and the way it gets inlined into

  coq/theories/MSets/MSetFacts.v

  Line 213 in bb5ace7

  Lemma elements_iff : In x s <-> InA E.eq x (elements s).

  producing a lemma elements_iff : In s x <-> @InA (level * constraint_type * level) (@eq UnivConstraint.t) (elements s), the problem is the inconsistent inlining of UnivConstraint.t when rewriting in <- direction.
• a couple times trying to rewrite with a lemma about 1 + _ but the goal has S _ (needs a rewrite <-Nat.add_1_l first, sometimes with explicit argument if there's a literal 1 in the goal)
• a definitional tc https://github.com/MetaCoq/metacoq/blob/cd3bc92bc97d974b917b3a6d55a4b9f595e69fa6/template-coq/theories/Universes.v#L1675

see compat patch at SkySkimmer/metacoq@1d196ca

[SkySkimmer]

In conclusion unfolding constants is needed for these aliases and for when type inference generates syntactically different terms in the lemma vs in the goal. Not sure how we could deal with the later issue.