[stdlib] Add `Proper` instances for some number theorems to improve rewriting with inequalities #16792

haansn08 · 2022-11-11T08:10:28Z

This should add the required Proper instances to use rewrite like this:

Require Import Arith.

Definition monotonic f := forall x y, x <= y -> f x <= f y.

Goal monotonic (fun n => 5 + 6*n + 7*n^3 + Nat.sqrt(42 + 3*n)).
Proof.
  intros x y H.
  rewrite H.
  reflexivity.
Qed.

ana-borges · 2022-11-15T11:02:59Z

I tried out your example but it doesn't seem to be working...?

haansn08 · 2022-11-15T12:59:06Z

@ana-borges Hm, maybe we should write #[global] instead of #[export].

haansn08 · 2022-11-16T16:08:50Z

@ana-borges It should work now. I also added a Proper (le ==> le) instance for Nat.sqrt and updated the example accordingly.

ana-borges · 2022-11-16T18:19:35Z

@haansn08 Cool! Could you add a changelog entry please?

Also, what about mixing le with lt, eg for add_lt_le_mono? Are there perhaps others missing as well?

ppedrot

Please don't add new global instances. This goes against modularity.

haansn08 · 2022-11-17T10:47:17Z

@ppedrot I would like to make them #[export], but then rewrite does not find the instances anymore.

ppedrot · 2022-11-17T12:47:09Z

Obviously, you have to import the corresponding modules for the instances to be available. Marking them global lets you do that silently through Require, but you lose any control over the fact that the instances are there (or not).

haansn08 · 2022-11-17T18:57:34Z

@ppedrot I have now changed the visibility to export as requested, but I think it will probably take a long time and nerves for a user to figure out one needs to Import Nat for this to work. I feel like things like that should simply work if I Require Import Arith.

ppedrot · 2022-11-17T19:16:23Z

Indeed, we need a serious set of rules for adding instances to the stdlib, so that users know when and what to import. I'm afraid that these guidelines do not exist yet...

JasonGross · 2022-11-17T19:35:33Z

@ppedrot I have now changed the visibility to export as requested, but I think it will probably take a long time and nerves for a user to figure out one needs to Import Nat for this to work. I feel like things like that should simply work if I Require Import Arith.

The way to fix this is to add Export Existing Instances ... inside a module Instances or Hints or w/e in Nat and then Export that module from Arith

haansn08 · 2022-11-18T11:54:47Z

@JasonGross Thanks for the tip!

I tried putting the following at the end of theories/Arith/PeanoNat.v, but I get an Error: The reference _add_lt_mono_l was not found in the current environment. when trying to recompile.
Could somebody tell me what would be an appropriate place to put it?

(** Re-export [Proper] instances for rewriting *)

#[export] Existing Instances
  _add_lt_mono_l
  _add_lt_mono_r
  _add_lt_mono
  _add_le_mono
  _add_le_lt_mono
  _sub_le_mono_l
  _sub_le_mono_r
  _mul_lt_mono
  _mul_le_mono
  _pow_le_mono_l
  _pred_le_mono
  _le_lt_trans
  _lt_le_trans
  _log2_le_mono
  _log2_up_le_mono
  _sqrt_le_mono
  _sqrt_up_le_mono.

Also make theories-arith seems to get stuck in a loop on ZBits.v (it does not compile even after several hours of CPU time) when trying to compile this branch :(

JasonGross · 2022-11-18T14:22:59Z

I tried putting the following at the end of theories/Arith/PeanoNat.v, but I get an Error: The reference _add_lt_mono_l was not found in the current environment. when trying to recompile.
Could somebody tell me what would be an appropriate place to put it?

It occurs to me that there's an even better strategy, though. You can use filtered Export to get the hints exported. That is, you can find all files that Require, e.g., NZAddOrder with git grep NZAddOrder "*.v", and then below Require NZAddOrder you can add Export (hints) NZAddOrder. Then you can find every file that requires one of these files, and repeat the process. Or you can just add Export (hints) NZAddOrder... to all the top-level files you think people are likely to import (PeanoNat and Arith?)

haansn08 · 2022-11-23T16:04:07Z

@ppedrot The initial example works now without any of the instances declared as #[global].

@JasonGross I'm not quite sure how a filtered export could work, but it works using Existing Instance, thanks!

JasonGross · 2022-11-23T20:21:38Z

I'm not quite sure how a filtered export could work

I'm not sure if this is what you're asking, but typeclass instances are just hints in the typeclass_instances database. What do you think wouldn't work?

haansn08 · 2022-11-25T16:15:15Z

@JasonGross It might work, but I'm not sure how to do it. For now, Existing Instance seems to work fine.

mrhaandi · 2022-12-09T10:39:52Z

The combination of all

Proper (eq ==> lt ==> lt) add
Proper (lt ==> eq ==> lt) add
Proper (lt ==> lt ==> lt) add
Proper (le ==> lt ==> lt) add
...
is asking for poor performance in general. Especially, if it is registered on import of PeanoNat (which is common), it will lead to slowdowns in otherwise perfectly working developments.

haansn08 · 2022-12-09T14:58:28Z

@mrhaandi I will gladly remove those instances, but could you explain why this would lead to poor performance?

mrhaandi · 2022-12-09T18:11:03Z

@mrhaandi I will gladly remove those instances, but could you explain why this would lead to poor performance?

Having every possible combination of le, lt, eq as hint introduces non-determinism in proof search, which on larger examples can be detrimental. Arguably, power users of generalized rewriting would be more careful with imports. So usually it would not be problematic.
On my machine, compilation time of your branch is 9% slower than prior to the single commit. So, more performance testing is necessary here already.

JasonGross · 2022-12-09T18:50:00Z

For sure it is a waste to have instances like Proper (lt ==> lt ==> lt) add that can never be used; in order to be useful in generalized rewriting, I believe all but one of the relations on the input variables must be reflexive. (It's possible that I'm wrong, and this will work fine when there are rewriting occurrences on both sides of the addition). I believe there should be a default instance for addition: Proper (eq ==> eq ==> eq) add, and all other instances should be added manually with Hint Extern. The rule of thumb I would use here is that, for the Extern cases, all relations which are either evars or flip of an evar should be instantiated with eq. Then have a bunch of instances that only trigger when none of the relations are evars, one instance for every (valid) combination of eq, lt, le, flip lt, flip le. (If needed, add a pass converting flip eq, ge, gt, flip ge, flip gt to one of these.). The code for this could look like:

Local Ltac instantiate_with_eq T R :=
  tryif is_evar R then unify R (@eq T) else
  lazymatch R with
  | respectful ?R1 ?R2 => instantiate_with_eq T R1; instantiate_with_eq T R2
  | flip ?R => instantiate_with_eq T R
  | _ => idtac
  end.
Local Open Scope signature_scope.
Local Ltac resolve_add R :=
  instantiate_with_eq T R;
  lazymatch R with
  | (eq ==> eq ==> eq) => exact ...
  | (eq ==> lt ==> lt) => exact ...
  | (le ==> eq ==> lt) => exact ...
  | (lt ==> lt ==> lt) => exact ...
  ...
  end.
#[export]
Hint Extern 0 (Proper ?R add) => resolve_add R : typeclass_instances.

JasonGross · 2022-12-09T18:51:02Z

@coqbot bench

coqbot-app · 2022-12-10T06:21:08Z

🏁 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-mathcomp-field │   91.48    92.46  -1.06 │   418578500379    422422328016  -0.91 │   693247373068    693165424684   0.01 │  651160   651144    0.00 │
│       coq-mathcomp-solvable │   80.41    81.12  -0.88 │   367009469752    370072330234  -0.83 │   566351054406    565950058112   0.07 │  665032   662156    0.43 │
│      coq-mathcomp-character │   67.14    67.71  -0.84 │   306755017915    308960767480  -0.71 │   467394061008    468197207637  -0.17 │  738396   740212   -0.25 │
│                   coq-verdi │   48.71    49.08  -0.75 │   221878985690    222203501135  -0.15 │   336140786358    336840701186  -0.21 │  538320   538584   -0.05 │
│      coq-mathcomp-ssreflect │   26.79    26.98  -0.70 │   122062231339    122388597030  -0.27 │   158539551442    157958957479   0.37 │  570476   567664    0.50 │
│            coq-math-classes │   93.06    93.54  -0.51 │   420911097655    423114356829  -0.52 │   599606782979    598881658577   0.12 │  515784   514600    0.23 │
│                    coq-hott │  163.64   164.04  -0.24 │   742054689061    742111470827  -0.01 │  1165360575983   1165294743423   0.01 │  626888   624852    0.33 │
│                coq-rewriter │  360.42   361.16  -0.20 │  1642940832242   1646218952299  -0.20 │  2725665441084   2723456234692   0.08 │ 1234444  1229580    0.40 │
│      coq-mathcomp-odd-order │  420.47   421.31  -0.20 │  1922653796637   1927211842751  -0.24 │  3198566293512   3197473073447   0.03 │  960708   927948    3.53 │
│                 coq-unimath │ 1259.20  1260.57  -0.11 │  5744664576991   5752134825735  -0.13 │ 10632422375242  10634759211222  -0.02 │ 1698500  1697632    0.05 │
│               coq-fourcolor │ 1467.67  1468.77  -0.07 │  6701196222922   6707134587712  -0.09 │ 12213873721316  12212295750749   0.01 │  738296   737320    0.13 │
│               coq-perennial │ 5046.01  5047.77  -0.03 │ 23011139398523  23008712687321   0.01 │ 37571439831414  37493764637250   0.21 │ 2458860  2459452   -0.02 │
│              coq-verdi-raft │  580.44   580.49  -0.01 │  2649415301893   2651503740590  -0.08 │  4171077396088   4166403814949   0.11 │  925156   925268   -0.01 │
│                coq-bedrock2 │  387.23   387.20   0.01 │  1770268331706   1769119085056   0.06 │  3400107141483   3393727020118   0.19 │  975980   968696    0.75 │
│        coq-mathcomp-algebra │   62.90    62.88   0.03 │   287004732452    286706530241   0.10 │   399416558977    398641284748   0.19 │  575360   576400   -0.18 │
│       coq-engine-bench-lite │  162.51   162.40   0.07 │   699057846548    698011062720   0.15 │  1303862659206   1302108777338   0.13 │ 1086112  1183536   -8.23 │
│       coq-mathcomp-fingroup │   22.44    22.42   0.09 │   102350091944    101916749119   0.43 │   151259681327    150713613886   0.36 │  499136   498892    0.05 │
│  coq-performance-tests-lite │  766.70   765.01   0.22 │  3476408123762   3467493287495   0.26 │  6116227627637   6098067906528   0.30 │ 1698804  2427904  -30.03 │
│                    coq-core │  108.73   108.44   0.27 │   451168460989    450418912097   0.17 │   471225805239    471261758064  -0.01 │  287352   286448    0.32 │
│ coq-rewriter-perf-SuperFast │  743.55   740.95   0.35 │  3386015329143   3375061255374   0.32 │  5820695702855   5819538782263   0.02 │ 1408428  1323012    6.46 │
│               coq-fiat-core │   58.61    58.39   0.38 │   253702865470    253246121595   0.18 │   366407176159    365616651351   0.22 │  489568   487404    0.44 │
│            coq-fiat-parsers │  342.65   341.34   0.38 │  1540319704505   1535358488928   0.32 │  2557270356468   2552357219656   0.19 │ 3163696  3157456    0.20 │
│                coq-compcert │  294.26   292.94   0.45 │  1334763416510   1328622209120   0.46 │  2025903882125   2022767259097   0.16 │ 1131200  1128904    0.20 │
│                    coq-corn │  817.22   813.55   0.45 │  3719598615164   3702108035055   0.47 │  5794527563633   5772539644036   0.38 │  862176   837484    2.95 │
│                  coq-geocoq │  689.89   686.51   0.49 │  3141530161076   3126870468170   0.47 │  5021708858168   5017389572329   0.09 │ 1015672  1009860    0.58 │
│           coq-iris-examples │  486.29   483.78   0.52 │  2207707352782   2196045296116   0.53 │  3342668212356   3338020807912   0.14 │ 1221880  1214128    0.64 │
│                 coq-coqutil │   36.20    36.00   0.56 │   162267420798    161555054870   0.44 │   231959210768    230881252227   0.47 │  601088   600264    0.14 │
│                   coq-color │  231.02   229.47   0.68 │  1043518992109   1038912924922   0.44 │  1510719571365   1504740963579   0.40 │ 1188012  1186456    0.13 │
│                coq-coqprime │   45.45    45.06   0.87 │   205456376385    203913982905   0.76 │   311879008618    310715317533   0.37 │  769116   766552    0.33 │
│                 coq-bignums │   28.84    28.58   0.91 │   131267499534    130034690486   0.95 │   186765107752    184490550196   1.23 │  482772   482768    0.00 │
│              coq-coquelicot │   36.66    36.09   1.58 │   164338211512    161634783372   1.67 │   224593340683    219903841276   2.13 │  760240   758112    0.28 │
│                  coq-stdlib │  454.81   430.06   5.76 │  1949674672868   1839930841319   5.96 │  1558340326479   1492163720351   4.43 │  707400   703764    0.52 │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴──────────────────────────┘

INFO: failed to install coq-category-theory
coq-fiat-crypto-with-bedrock
coq-metacoq-erasure
coq-metacoq-pcuic
coq-metacoq-safechecker
coq-metacoq-template
coq-metacoq-translations
coq-vst

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                     TOP 25 SLOW DOWNS                                                      │
│                                                                                                                            │
│   OLD      NEW     DIFF     %DIFF     Ln                  FILE                                                             │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 20.2090  22.3610  2.1520     10.65%   641  coq-perennial/src/program_proof/simplepb/pb_apply_proof.v.html                  │
│ 20.3990  22.4790  2.0800     10.20%   267  coq-perennial/src/program_proof/memkv/memkv_coord_start_proof.v.html            │
│  5.4350   5.9220  0.4870      8.96%   253  coq-perennial/src/program_proof/memkv/memkv_shard_make_proof.v.html             │
│  7.6920   8.1230  0.4310      5.60%   281  coq-perennial/src/program_proof/memkv/memkv_shard_start_proof.v.html            │
│  2.9970   3.4250  0.4280     14.28%   994  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 28.9520  29.3430  0.3910      1.35%    10  coq-fourcolor/theories/job611to617.v.html                                       │
│  0.0140   0.3820  0.3680   2628.57%  1178  coq-perennial/src/program_proof/wal/recovery_proof.v.html                       │
│  0.2030   0.5530  0.3500    172.41%   854  coq-perennial/src/program_proof/wal/installer_proof.v.html                      │
│  0.3250   0.6690  0.3440    105.85%   594  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                 │
│  8.2080   8.5370  0.3290      4.01%  1213  coq-unimath/UniMath/CategoryTheory/DisplayedCats/Examples/Reindexing.v.html     │
│  0.0810   0.3880  0.3070    379.01%  1222  coq-perennial/src/program_proof/aof/proof.v.html                                │
│  0.0030   0.3050  0.3020  10066.67%  1010  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html       │
│  0.0580   0.3540  0.2960    510.34%  1032  coq-perennial/src/program_proof/examples/dir_proof.v.html                       │
│ 11.0010  11.2810  0.2800      2.55%   313  coq-perennial/src/program_proof/mvcc/txn_commit.v.html                          │
│ 23.0840  23.3630  0.2790      1.21%    10  coq-fourcolor/theories/job542to545.v.html                                       │
│ 23.1020  23.3790  0.2770      1.20%    10  coq-fourcolor/theories/job511to516.v.html                                       │
│  2.4550   2.7090  0.2540     10.35%   171  coq-perennial/src/program_proof/mvcc/txnmgr_activate.v.html                     │
│  0.0440   0.2950  0.2510    570.45%   579  coq-color/Term/WithArity/AUnif.v.html                                           │
│  2.7250   2.9740  0.2490      9.14%   466  coq-perennial/src/program_proof/wal/installer_proof.v.html                      │
│ 21.2340  21.4710  0.2370      1.12%    10  coq-fourcolor/theories/job507to510.v.html                                       │
│  2.2220   2.4500  0.2280     10.26%   314  coq-perennial/src/program_proof/mvcc/txn_commit.v.html                          │
│ 27.5750  27.7930  0.2180      0.79%    10  coq-fourcolor/theories/job517to530.v.html                                       │
│  6.7320   6.9500  0.2180      3.24%  1189  coq-perennial/src/goose_lang/logical_reln_fund.v.html                           │
│  2.3540   2.5700  0.2160      9.18%   249  coq-perennial/src/program_proof/memkv/bank_proof.v.html                         │
│ 31.1550  31.3570  0.2020      0.65%    10  coq-fourcolor/theories/job107to164.v.html                                       │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                      TOP 25 SPEED UPS                                                       │
│                                                                                                                             │
│   OLD       NEW      DIFF     %DIFF    Ln                  FILE                                                             │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 132.6220  131.4660  -1.1560   -0.87%   992  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│ 132.3520  131.7560  -0.5960   -0.45%   962  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html │
│   7.1340    6.6300  -0.5040   -7.06%  1582  coq-perennial/src/program_proof/fencing/ctr_proof.v.html                        │
│  22.6220   22.1820  -0.4400   -1.95%    10  coq-fourcolor/theories/job283to286.v.html                                       │
│  18.3520   17.9140  -0.4380   -2.39%    10  coq-fourcolor/theories/job235to238.v.html                                       │
│  23.0380   22.6270  -0.4110   -1.78%    10  coq-fourcolor/theories/job307to310.v.html                                       │
│   3.4140    3.0800  -0.3340   -9.78%  1406  coq-perennial/src/program_proof/wal/installer_proof.v.html                      │
│  23.0460   22.7120  -0.3340   -1.45%    10  coq-fourcolor/theories/job219to222.v.html                                       │
│   4.2230    3.9040  -0.3190   -7.55%   441  coq-perennial/src/program_proof/mvcc/txn_do_txn.v.html                          │
│   0.5770    0.2890  -0.2880  -49.91%  1225  coq-perennial/src/program_proof/aof/proof.v.html                                │
│ 129.9860  129.6990  -0.2870   -0.22%   693  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                     │
│   5.7400    5.4660  -0.2740   -4.77%   926  coq-perennial/src/program_proof/txn/wrapper_proof.v.html                        │
│   9.6810    9.4200  -0.2610   -2.70%    41  coq-perennial/src/program_proof/mvcc/txn_acquire.v.html                         │
│  25.8090   25.5520  -0.2570   -1.00%    10  coq-fourcolor/theories/job295to298.v.html                                       │
│   6.1750    5.9240  -0.2510   -4.06%  5564  coq-fourcolor/theories/present7.v.html                                          │
│ 153.0090  152.7650  -0.2440   -0.16%  1188  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html   │
│   2.7470    2.5140  -0.2330   -8.48%   641  coq-perennial/src/program_proof/examples/async_mem_alloc_dir_proof.v.html       │
│  27.1900   26.9590  -0.2310   -0.85%    10  coq-fourcolor/theories/job227to230.v.html                                       │
│  28.3610   28.1310  -0.2300   -0.81%    10  coq-fourcolor/theories/job466to485.v.html                                       │
│  21.5950   21.3710  -0.2240   -1.04%    10  coq-fourcolor/theories/job239to253.v.html                                       │
│  16.3440   16.1220  -0.2220   -1.36%    10  coq-fourcolor/theories/job215to218.v.html                                       │
│   1.0950    0.8740  -0.2210  -20.18%   237  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                 │
│   7.2790    7.0650  -0.2140   -2.94%   838  coq-perennial/src/program_proof/txn/wrapper_proof.v.html                        │
│   7.9260    7.7250  -0.2010   -2.54%   368  coq-perennial/src/program_proof/simplepb/pb_becomeprimary_proof.v.html          │
│   2.6360    2.4400  -0.1960   -7.44%   610  coq-perennial/src/program_proof/examples/dir_proof.v.html                       │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

haansn08 · 2022-12-11T06:35:43Z

I now removed the Proper instances for the lt altogether. Not sure how useful they were anyways since fun x => n * x is only strictly monotone when 0 < n which is not detected by rewrite. Maybe this can also be solved by using the Hint Extern trick.

theories/Arith/PeanoNat.v

JasonGross · 2022-12-21T13:27:13Z

@coqbot bench

coqbot-app · 2022-12-22T00:36:04Z

🏁 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-verdi │   48.59    49.10  -1.04 │   218716543521    219977762376  -0.57 │   333991637116    336838771473  -0.85 │  534268   534220   0.01 │
│       coq-engine-bench-lite │  162.63   163.98  -0.82 │   692791282611    698674533286  -0.84 │  1302983727976   1308332484737  -0.41 │ 1299900  1186180   9.59 │
│       coq-mathcomp-solvable │   80.55    81.15  -0.74 │   365155983833    366769136017  -0.44 │   565423533001    565809819080  -0.07 │  662948   665112  -0.33 │
│      coq-mathcomp-character │   67.31    67.81  -0.74 │   305087551918    307634535146  -0.83 │   468289239731    468530009640  -0.05 │  736996   738332  -0.18 │
│                coq-compcert │  294.88   296.53  -0.56 │  1320392303370   1326597195513  -0.47 │  2026417402935   2023111749838   0.16 │ 1129276  1129552  -0.02 │
│ coq-rewriter-perf-SuperFast │  749.54   753.65  -0.55 │  3342256856966   3361392262552  -0.57 │  5818880971379   5818825146788   0.00 │ 1322480  1320000   0.19 │
│              coq-verdi-raft │  582.56   585.25  -0.46 │  2643235716802   2654962904124  -0.44 │  4166065105522   4166393110465  -0.01 │  924368   927268  -0.31 │
│                    coq-core │  110.33   110.79  -0.42 │   440727364041    438406366996   0.53 │   471053873915    471048147860   0.00 │  284832   287240  -0.84 │
│      coq-mathcomp-odd-order │  419.84   420.92  -0.26 │  1910147027624   1913731103669  -0.19 │  3198908251222   3198244428495   0.02 │  960080   958700   0.14 │
│                    coq-corn │  818.19   819.71  -0.19 │  3688338103528   3697158038136  -0.24 │  5807060458126   5771779548228   0.61 │  861616   860520   0.13 │
│                 coq-unimath │ 1269.05  1270.99  -0.15 │  5724386704087   5730935166094  -0.11 │ 10631877311346  10636717314508  -0.05 │ 1702372  1698540   0.23 │
│                coq-bedrock2 │  396.57   397.03  -0.12 │  1773186169000   1769947702206   0.18 │  3430993440480   3424322890723   0.19 │  973744   964632   0.94 │
│          coq-mathcomp-field │   92.48    92.57  -0.10 │   419559419710    420505863897  -0.23 │   693578115355    693162291855   0.06 │  651280   653892  -0.40 │
│                    coq-hott │  165.03   165.19  -0.10 │   740127849074    739234782596   0.12 │  1165425209104   1165329178052   0.01 │  626980   626992  -0.00 │
│                coq-coqprime │   45.84    45.84   0.00 │   204627191626    204374478243   0.12 │   312217594785    310154851914   0.67 │  767172   766672   0.07 │
│           coq-iris-examples │  487.33   487.33   0.00 │  2193445706025   2192989569362   0.02 │  3355583741244   3336750120431   0.56 │ 1219332  1215988   0.28 │
│               coq-fourcolor │ 1507.27  1506.78   0.03 │  6664046013167   6663940989976   0.00 │ 12202442799947  12212108344598  -0.08 │  738232   737512   0.10 │
│               coq-perennial │ 5563.51  5561.04   0.04 │ 25104421645186  25092611143365   0.05 │ 41433046906116  41378492165676   0.13 │ 2490856  2485676   0.21 │
│                 coq-coqutil │   36.31    36.29   0.06 │   160477594600    160365037926   0.07 │   232172782637    230906967777   0.55 │  600836   600336   0.08 │
│       coq-mathcomp-fingroup │   22.56    22.50   0.27 │   102047233090    101872245901   0.17 │   150553604567    150828709918  -0.18 │  499692   499240   0.09 │
│  coq-performance-tests-lite │  773.93   771.58   0.30 │  3455829320816   3445198668884   0.31 │  6107752548083   6102470190031   0.09 │ 2427844  2426456   0.06 │
│                coq-rewriter │  364.26   363.12   0.31 │  1643491375164   1639153308663   0.26 │  2724490477564   2723426555888   0.04 │ 1232716  1229496   0.26 │
│               coq-fiat-core │   59.55    59.30   0.42 │   253500884456    252408345321   0.43 │   367389541719    365597633555   0.49 │  491224   488744   0.51 │
│            coq-fiat-parsers │  347.75   345.34   0.70 │  1531911124260   1523062648820   0.58 │  2558122241518   2552483348835   0.22 │ 3160684  3156184   0.14 │
│        coq-mathcomp-algebra │   63.20    62.74   0.73 │   285575878270    284470731246   0.39 │   398310866061    398724773542  -0.10 │  575504   576436  -0.16 │
│                   coq-color │  234.90   232.80   0.90 │  1045572865408   1037894212214   0.74 │  1512869236112   1505397151607   0.50 │ 1184072  1183080   0.08 │
│            coq-math-classes │   94.66    93.81   0.91 │   423289947705    419836793331   0.82 │   600082913680    598943986076   0.19 │  514856   514824   0.01 │
│                  coq-geocoq │  696.71   690.44   0.91 │  3147609543921   3119706515120   0.89 │  5038409653420   5018198684161   0.40 │  916716  1013564  -9.56 │
│      coq-mathcomp-ssreflect │   26.99    26.65   1.28 │   121199068978    120502882002   0.58 │   157754648058    157945866772  -0.12 │  568648   568608   0.01 │
│                  coq-stdlib │  429.86   423.65   1.47 │  1752661762381   1729275497162   1.35 │  1508572906663   1491854150779   1.12 │  683916   700068  -2.31 │
│                 coq-bignums │   29.28    28.75   1.84 │   132271842964    130118218582   1.66 │   187103911205    184371522097   1.48 │  480540   480048   0.10 │
│              coq-coquelicot │   36.95    36.24   1.96 │   163349589077    159937870401   2.13 │   225449715632    220087195103   2.44 │  751732   757528  -0.77 │
└─────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

INFO: failed to install coq-category-theory
coq-fiat-crypto-with-bedrock
coq-metacoq-erasure
coq-metacoq-pcuic
coq-metacoq-safechecker
coq-metacoq-template
coq-metacoq-translations
coq-vst

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                             TOP 25 SLOW DOWNS                                                              │
│                                                                                                                                            │
│   OLD      NEW     DIFF    %DIFF     Ln                     FILE                                                                           │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 18.1690  18.8700  0.7010     3.86%   874  coq-perennial/src/program_proof/simple/setattr.v.html                                            │
│ 16.9770  17.5490  0.5720     3.37%   962  coq-unimath/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v.html │
│ 37.0680  37.5270  0.4590     1.24%    10  coq-fourcolor/theories/job439to465.v.html                                                        │
│ 21.8430  22.2880  0.4450     2.04%    10  coq-fourcolor/theories/job239to253.v.html                                                        │
│  7.7410   8.1190  0.3780     4.88%   281  coq-perennial/src/program_proof/memkv/memkv_shard_start_proof.v.html                             │
│ 40.6320  40.9890  0.3570     0.88%   222  coq-performance-tests-lite/PerformanceExperiments/rewrite_lift_lets_map.v.html                   │
│  0.2040   0.5600  0.3560   174.51%   854  coq-perennial/src/program_proof/wal/installer_proof.v.html                                       │
│  1.6230   1.9790  0.3560    21.93%   981  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                   │
│ 32.1870  32.5350  0.3480     1.08%    10  coq-fourcolor/theories/job107to164.v.html                                                        │
│ 19.4000  19.7460  0.3460     1.78%    10  coq-fourcolor/theories/job550to553.v.html                                                        │
│ 24.7310  25.0610  0.3300     1.33%  2292  coq-perennial/src/goose_lang/logical_reln_fund.v.html                                            │
│  3.6800   3.9900  0.3100     8.42%   817  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                  │
│ 32.0010  32.2950  0.2940     0.92%    10  coq-fourcolor/theories/job563to588.v.html                                                        │
│ 37.1190  37.4030  0.2840     0.77%   521  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                             │
│ 29.1690  29.4320  0.2630     0.90%    10  coq-fourcolor/theories/job466to485.v.html                                                        │
│  2.7390   2.9970  0.2580     9.42%   466  coq-perennial/src/program_proof/wal/installer_proof.v.html                                       │
│  7.8760   8.1130  0.2370     3.01%   290  coq-perennial/src/program_proof/simplepb/pb_applybackup_proof.v.html                             │
│ 30.1140  30.3490  0.2350     0.78%    10  coq-fourcolor/theories/job399to438.v.html                                                        │
│ 30.0280  30.2490  0.2210     0.74%    10  coq-fourcolor/theories/job287to290.v.html                                                        │
│  2.3540   2.5750  0.2210     9.39%   249  coq-perennial/src/program_proof/memkv/bank_proof.v.html                                          │
│  8.2650   8.4800  0.2150     2.60%   672  coq-rewriter/src/Rewriter/Rewriter/Wf.v.html                                                     │
│ 28.3940  28.6070  0.2130     0.75%    10  coq-fourcolor/theories/job517to530.v.html                                                        │
│ 23.0190  23.2270  0.2080     0.90%    10  coq-fourcolor/theories/job283to286.v.html                                                        │
│  0.0950   0.2740  0.1790   188.42%   278  coq-perennial/src/program_proof/txn/twophase_sub_logical_reln_defs.v.html                        │
│  0.0130   0.1920  0.1790  1376.92%    74  coq-perennial/src/program_proof/txn/twophase_refinement_proof.v.html                             │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                               TOP 25 SPEED UPS                                                               │
│                                                                                                                                              │
│   OLD       NEW      DIFF     %DIFF    Ln                     FILE                                                                           │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 133.0530  131.6380  -1.4150   -1.06%   693  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                      │
│  42.1610   41.3970  -0.7640   -1.81%   235  coq-rewriter-perf-SuperFast/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html        │
│   7.1950    6.5130  -0.6820   -9.48%  1582  coq-perennial/src/program_proof/fencing/ctr_proof.v.html                                         │
│   5.8200    5.3510  -0.4690   -8.06%   433  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                  │
│   3.1240    2.6680  -0.4560  -14.60%   982  coq-perennial/src/program_proof/grove_shared/urpc_proof.v.html                                   │
│   4.3580    3.9270  -0.4310   -9.89%  1063  coq-perennial/src/program_proof/simplepb/simplelog/proof.v.html                                  │
│  30.1370   29.7310  -0.4060   -1.35%    10  coq-fourcolor/theories/job611to617.v.html                                                        │
│  28.4180   28.0360  -0.3820   -1.34%    10  coq-fourcolor/theories/job535to541.v.html                                                        │
│  20.1900   19.8120  -0.3780   -1.87%   596  coq-perennial/src/goose_lang/lib/encoding/encoding.v.html                                        │
│   7.8640    7.5040  -0.3600   -4.58%   707  coq-unimath/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v.html │
│  15.6230   15.3100  -0.3130   -2.00%   482  coq-verdi-raft/raft-proofs/EndToEndLinearizability.v.html                                        │
│   3.4510    3.1420  -0.3090   -8.95%  1406  coq-perennial/src/program_proof/wal/installer_proof.v.html                                       │
│  22.2440   21.9410  -0.3030   -1.36%   208  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                             │
│  22.1410   21.8470  -0.2940   -1.33%   318  coq-engine-bench-lite/coq/PerformanceDemos/one_step_reduction.v.html                             │
│   3.1230    2.8370  -0.2860   -9.16%   862  coq-perennial/src/program_proof/wal/logger_proof.v.html                                          │
│  41.9830   41.7130  -0.2700   -0.64%   235  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                       │
│  25.1040   24.8480  -0.2560   -1.02%    10  coq-fourcolor/theories/job303to306.v.html                                                        │
│   2.0100    1.7770  -0.2330  -11.59%   866  coq-unimath/UniMath/CategoryTheory/Monoidal/DisplayedCartesianMonoidalCategoriesWhiskered.v.html │
│  27.9930   27.7760  -0.2170   -0.78%    10  coq-fourcolor/theories/job299to302.v.html                                                        │
│  30.8320   30.6280  -0.2040   -0.66%  1375  coq-fourcolor/theories/cfmap.v.html                                                              │
│  29.6070   29.4080  -0.1990   -0.67%    10  coq-fourcolor/theories/job531to534.v.html                                                        │
│  14.8880   14.6910  -0.1970   -1.32%   417  coq-verdi-raft/raft-proofs/LeaderLogsLogMatchingProof.v.html                                     │
│   0.3710    0.1760  -0.1950  -52.56%   289  coq-perennial/src/program_proof/txn/twophase_sub_logical_reln_defs.v.html                        │
│   8.6490    8.4590  -0.1900   -2.20%    84  coq-engine-bench-lite/coq/PerformanceDemos/quadratic_reduction.v.html                            │
│   2.4720    2.2860  -0.1860   -7.52%   404  coq-perennial/src/program_proof/mvcc/txnmgr_deactivate.v.html                                    │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

JasonGross · 2022-12-22T01:18:48Z

@coqbot run full ci

haansn08 · 2022-12-28T00:19:23Z

@JasonGross I now squashed the commits. Is there anything else I can do to improve this PR?

SkySkimmer · 2024-04-17T13:55:11Z

@coq/stdlib-maintainers please make a decision instead of leaving this open for years

andres-erbsen · 2024-04-17T16:18:02Z

It is indeed a shame that this has been neglected so long. Who would be the most appropriate reviewer wrt considerations of using setoid rewriting at scale? I personally feel compelled to defer to @JasonGross, but I know he doesn't have all that much extra time on his hands these days and perhaps there's somebody who's actually in charge of setoid rewrite and associated infrastructure? @coq/typeclasses-maintainers @coq/tactics-maintainers ?

JasonGross

I think the optimal proper instances have eq in all argument slots but one, but these are good and there's no reason to block this PR. Can someone rebase and let's check full CI and bench again, and if everything looks fine let's merge

andres-erbsen · 2024-04-17T17:48:43Z

The PR rebeases cleanly but I get an error on push. Might it be that I am missing yet another type of permission, or would the PR author have to do it?

…th inequalities

JasonGross · 2024-04-17T17:53:36Z

I tensed through the web interface by temporarily enabling it

@coqbot bench

coqbot-app · 2024-04-18T08:06:55Z

🏁 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-mathcomp-fingroup │   30.48    30.71  -0.75 │   138284943161    139193500166  -0.65 │   208927445586    209026118497  -0.05 │  567920   565508   0.43 │
│                  coq-mathcomp-field │  136.78   137.18  -0.29 │   617007737963    618832550772  -0.29 │  1016918443573   1015483971233   0.14 │ 1408824  1405500   0.24 │
│                         coq-coqutil │   43.28    43.38  -0.23 │   189874470460    189618152706   0.14 │   273197558284    272279626769   0.34 │  566440   564208   0.40 │
│                 coq-category-theory │  701.33   702.95  -0.23 │  3175598447191   3181998405696  -0.20 │  5309773192430   5308430778668   0.03 │  953704   972072  -1.89 │
│               coq-engine-bench-lite │  157.74   158.10  -0.23 │   662136512607    663252498619  -0.17 │  1229063254092   1227806314412   0.10 │ 1233068  1236928  -0.31 │
│                        coq-bedrock2 │  361.59   362.24  -0.18 │  1630746868388   1635060058059  -0.26 │  3104887031958   3101359728522   0.11 │  898788   913976  -1.66 │
│                coq-mathcomp-algebra │  237.64   238.05  -0.17 │  1075002020534   1076407566238  -0.13 │  1772235077779   1771856596385   0.02 │ 1295176  1290768   0.34 │
│                        coq-rewriter │  391.78   392.43  -0.17 │  1764250033500   1768358895744  -0.23 │  2959363425068   2958745521941   0.02 │ 1522176  1523340  -0.08 │
│             coq-metacoq-safechecker │  421.90   422.44  -0.13 │  1921824504160   1924426908433  -0.14 │  3191284884715   3191644423685  -0.01 │ 2061248  2070360  -0.44 │
│ coq-neural-net-interp-computed-lite │  292.01   292.38  -0.13 │  1331437348875   1332128041630  -0.05 │  3427977106755   3427197848403   0.02 │ 1126400  1126376   0.00 │
│                    coq-fiat-parsers │  314.56   314.90  -0.11 │  1392889244485   1393898398707  -0.07 │  2444721212724   2440307330055   0.18 │ 2384072  2397804  -0.57 │
│              coq-mathcomp-ssreflect │   93.71    93.81  -0.11 │   422635657637    423249987551  -0.15 │   664931014354    664765236789   0.02 │ 1362656  1383452  -1.50 │
│                       coq-fourcolor │ 1354.01  1355.44  -0.11 │  6157304257255   6159424643822  -0.03 │ 12153163754956  12152515378202   0.01 │ 2135104  2129604   0.26 │
│                           coq-verdi │   49.07    49.12  -0.10 │   220126212853    219983652455   0.06 │   341969742217    341230905965   0.22 │  530680   530732  -0.01 │
│                         coq-bignums │   29.94    29.94   0.00 │   135570060206    134376862038   0.89 │   194396933879    193397718882   0.52 │  478476   478796  -0.07 │
│                   coq-metacoq-pcuic │  993.64   993.55   0.01 │  4428365992248   4428232648760   0.00 │  6481545791829   6480595457039   0.01 │ 2688040  2684872   0.12 │
│         coq-rewriter-perf-SuperFast │  796.60   796.05   0.07 │  3554924007721   3554360309404   0.02 │  6198337442659   6196936184777   0.02 │ 1625884  1615360   0.65 │
│              coq-mathcomp-character │  103.96   103.88   0.08 │   472681140941    472599354176   0.02 │   746040004559    745201335518   0.11 │ 1035680  1026528   0.89 │
│        coq-fiat-crypto-with-bedrock │ 6230.10  6224.59   0.09 │ 28200675385760  28172548764770   0.10 │ 50372611742171  50334272937755   0.08 │ 3245828  3246096  -0.01 │
│                      coq-verdi-raft │  583.20   582.67   0.09 │  2645827932172   2642388733352   0.13 │  4177805459712   4171856868119   0.14 │  845872   846332  -0.05 │
│               coq-mathcomp-solvable │  118.45   118.30   0.13 │   539036879970    538196388803   0.16 │   857558655643    857179507755   0.04 │  859132   860340  -0.14 │
│                         coq-unimath │ 2436.41  2431.68   0.19 │ 11042131328344  11025762151690   0.15 │ 21926665574931  21927207403538  -0.00 │ 1254488  1255320  -0.07 │
│                 coq-metacoq-erasure │  507.55   506.53   0.20 │  2295295398418   2291252852236   0.18 │  3588806727506   3588851093177  -0.00 │ 2087992  2135532  -2.23 │
│              coq-mathcomp-odd-order │  789.76   788.08   0.21 │  3604602399370   3597317943352   0.20 │  6010914210301   6011135449076  -0.00 │ 1611768  1612876  -0.07 │
│                            coq-hott │  158.72   158.36   0.23 │   701478781105    700198348271   0.18 │  1117926728753   1117869470115   0.01 │  550508   546744   0.69 │
│                    coq-math-classes │   86.50    86.26   0.28 │   386927285996    385372093876   0.40 │   537469430196    536532260234   0.17 │  507644   506412   0.24 │
│          coq-performance-tests-lite │  719.59   717.58   0.28 │  3214986389977   3208422518197   0.20 │  5658121789459   5649372107855   0.15 │ 1591328  1589924   0.09 │
│                       coq-equations │    7.72     7.69   0.39 │    31316075882     31264358453   0.17 │    51061261357     51004245220   0.11 │  387072   386900   0.04 │
│                coq-metacoq-template │  152.62   151.89   0.48 │   671787734931    668436542070   0.50 │  1049353778239   1047685438925   0.16 │ 1489088  1515968  -1.77 │
│                            coq-corn │  736.94   733.41   0.48 │  3332409288438   3314961622635   0.53 │  5208636185976   5175807950999   0.63 │  803908   761152   5.62 │
│                           coq-color │  255.60   254.32   0.50 │  1139372405317   1135101433151   0.38 │  1648209105280   1642533053016   0.35 │ 1198912  1204992  -0.50 │
│                       coq-fiat-core │   60.77    60.44   0.55 │   251158055603    249213112218   0.78 │   371665599378    370100981256   0.42 │  483120   483336  -0.04 │
│                        coq-compcert │  285.16   283.58   0.56 │  1278691692760   1271869024520   0.54 │  1951039449458   1945220422148   0.30 │ 1109104  1166420  -4.91 │
│                             coq-vst │  888.50   883.00   0.62 │  4012011450408   3988680147618   0.58 │  6785996394091   6767708635885   0.27 │ 2375564  2149628  10.51 │
│                   coq-iris-examples │  469.96   466.68   0.70 │  2124971293257   2111856938807   0.62 │  3301203808535   3276929136220   0.74 │ 1128692  1113092   1.40 │
│                                 coq │  732.71   727.52   0.71 │  3072904973416   3057578343298   0.50 │  5467141474680   5454172948603   0.24 │ 2482632  2718024  -8.66 │
│                      coq-coquelicot │   40.20    39.86   0.85 │   177206770915    176512099529   0.39 │   250938604162    250254959372   0.27 │  857032   856696   0.04 │
│                        coq-coqprime │   49.14    48.68   0.94 │   219247189037    217538267507   0.79 │   337004612953    334735613480   0.68 │  788744   789436  -0.09 │
│            coq-metacoq-translations │   17.43    17.26   0.98 │    76231169043     75967131350   0.35 │   125230531695    125018642898   0.17 │  847240   847900  -0.08 │
│                            coq-core │  132.31   130.35   1.50 │   495305477405    490888569669   0.90 │   530326878306    529862740151   0.09 │  457704   457476   0.05 │
│                          coq-stdlib │  379.80   374.06   1.53 │  1577617628937   1553040895118   1.58 │  1355691448365   1340216826747   1.15 │  718632   712924   0.80 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                           TOP 25 SLOW DOWNS                                                            │
│                                                                                                                                        │
│   OLD       NEW      DIFF   %DIFF    Ln                    FILE                                                                        │
├────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│  46.3070   48.4560  2.1490   4.64%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html │
│   9.2280   10.5260  1.2980  14.07%   192  coq-vst/veric/binop_lemmas5.v.html                                                           │
│   3.9250    4.9120  0.9870  25.15%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                       │
│   3.1550    3.9500  0.7950  25.20%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│  95.2040   95.9170  0.7130   0.75%   999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html              │
│ 133.0190  133.7230  0.7040   0.53%    22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                       │
│   2.6550    3.3200  0.6650  25.05%    34  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                       │
│   1.6890    2.2880  0.5990  35.46%   196  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                     │
│   5.5590    6.1200  0.5610  10.09%   308  coq-iris-examples/theories/logrel/F_mu_ref_conc/binary/examples/stack/refinement.v.html      │
│  81.9700   82.5100  0.5400   0.66%    48  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/AffineProofs.v.html                      │
│   2.0430    2.5730  0.5300  25.94%    32  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                  │
│  11.2450   11.7350  0.4900   4.36%   126  coq-vst/veric/binop_lemmas6.v.html                                                           │
│ 154.1910  154.6720  0.4810   0.31%  1190  coq-unimath/UniMath/CategoryTheory/GrothendieckConstruction/IsPullback.v.html                │
│   1.6820    2.1060  0.4240  25.21%    42  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                     │
│  72.5460   72.9690  0.4230   0.58%   905  coq-unimath/UniMath/ModelCategories/Generated/LNWFSCocomplete.v.html                         │
│  87.7090   88.1280  0.4190   0.48%   365  coq-mathcomp-odd-order/theories/PFsection4.v.html                                            │
│   4.6420    5.0530  0.4110   8.85%   111  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                   │
│   1.6300    2.0150  0.3850  23.62%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                  │
│   1.6350    1.9710  0.3360  20.55%   165  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                           │
│  14.6290   14.9640  0.3350   2.29%   490  coq-unimath/UniMath/HomologicalAlgebra/KA.v.html                                             │
│   0.6990    1.0240  0.3250  46.49%   813  coq-stdlib/MSets/MSetRBT.v.html                                                              │
│  95.4300   95.7510  0.3210   0.34%   968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html              │
│  19.3540   19.6730  0.3190   1.65%    12  coq-fourcolor/theories/job546to549.v.html                                                    │
│  39.6380   39.9450  0.3070   0.77%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                       │
│  23.8020   24.1020  0.3000   1.26%    12  coq-fourcolor/theories/job319to322.v.html                                                    │
└────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                   TOP 25 SPEED UPS                                                                   │
│                                                                                                                                                      │
│   OLD       NEW      DIFF     %DIFF     Ln                      FILE                                                                                 │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 217.6290  216.3060  -1.3230    -0.61%   103  coq-fiat-crypto-with-bedrock/src/Arithmetic/BarrettReduction.v.html                                     │
│  63.3410   62.1350  -1.2060    -1.90%   609  coq-bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html                                             │
│  66.6920   66.1310  -0.5610    -0.84%    27  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ToFancyWithCasts.v.html                                │
│ 101.4420  101.0240  -0.4180    -0.41%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                             │
│  25.9170   25.5770  -0.3400    -1.31%   345  coq-fiat-crypto-with-bedrock/src/Curves/Montgomery/XZProofs.v.html                                      │
│ 180.2030  179.8660  -0.3370    -0.19%   233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  18.5320   18.2040  -0.3280    -1.77%   820  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│ 250.2350  249.9260  -0.3090    -0.12%     8  coq-neural-net-interp-computed-lite/theories/MaxOfTwoNumbersSimpler/Computed/AllLogits.v.html           │
│  38.0680   37.7660  -0.3020    -0.79%     3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/with_bedrock2_fiat_crypto.v.html                   │
│  37.0070   36.7070  -0.3000    -0.81%   548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  18.1770   17.8790  -0.2980    -1.64%   708  coq-fiat-crypto-with-bedrock/src/Rewriter/RulesProofs.v.html                                            │
│  39.8510   39.5550  -0.2960    -0.74%   236  coq-rewriter/src/Rewriter/Rewriter/Examples/PerfTesting/LiftLetsMap.v.html                              │
│  24.7550   24.4900  -0.2650    -1.07%    12  coq-fourcolor/theories/job291to294.v.html                                                               │
│  18.3600   18.0980  -0.2620    -1.43%    32  coq-performance-tests-lite/src/pattern.v.html                                                           │
│  16.1230   15.8630  -0.2600    -1.61%   828  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│  27.6420   27.3840  -0.2580    -0.93%    12  coq-fourcolor/theories/job107to164.v.html                                                               │
│  23.2590   23.0110  -0.2480    -1.07%    12  coq-fourcolor/theories/job295to298.v.html                                                               │
│   0.2770    0.0290  -0.2480   -89.53%  1104  coq-fiat-crypto-with-bedrock/src/CLI.v.html                                                             │
│   0.2480    0.0000  -0.2480  -100.00%   476  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/New/Signature.v.html                           │
│   0.2570    0.0130  -0.2440   -94.94%   518  coq-fiat-crypto-with-bedrock/src/CLI.v.html                                                             │
│ 135.0070  134.7650  -0.2420    -0.18%   155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  22.9820   22.7410  -0.2410    -1.05%    12  coq-fourcolor/theories/job554to562.v.html                                                               │
│   0.2370    0.0000  -0.2370  -100.00%    65  coq-fiat-crypto-with-bedrock/src/Bedrock/Standalone/StandaloneOCamlMain.v.html                          │
│   0.2350    0.0000  -0.2350  -100.00%    64  coq-fiat-crypto-with-bedrock/src/Bedrock/Standalone/StandaloneHaskellMain.v.html                        │
│   7.3210    7.0880  -0.2330    -3.18%   604  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Colimits/Examples/StructureEnrichedColimits.v.html      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

andres-erbsen · 2024-04-18T18:59:57Z

@coqbot run full ci

andres-erbsen · 2024-04-19T16:14:04Z

hb failure is unrelated (Error: Unbound type constructor DeclareInd.default_dep_elim)

andres-erbsen · 2024-04-19T16:20:59Z

I intend to merge on Monday or when I next look at this PR.

haansn08 requested a review from a team as a code owner November 11, 2022 08:10

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 11, 2022

haansn08 changed the title ~~[stdlib] add rewrite instances for add_le_mono, mul_le_mono, pow_le_mono_l~~ [stdlib] Add Proper instances for some number theorems to improve rewriting with inequalities Nov 17, 2022

ppedrot requested changes Nov 17, 2022

View reviewed changes

ppedrot self-requested a review November 23, 2022 16:06

haansn08 force-pushed the proper_instances1 branch from 8396f20 to f89c9ce Compare November 26, 2022 14:48

JasonGross added the needs: benchmarking Performance testing is required. label Dec 9, 2022

Blaisorblade reviewed Dec 20, 2022

View reviewed changes

theories/Arith/PeanoNat.v Outdated Show resolved Hide resolved

haansn08 removed the request for review from ppedrot December 21, 2022 09:04

haansn08 requested review from Blaisorblade and ppedrot and removed request for Blaisorblade December 21, 2022 09:04

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 22, 2022

haansn08 force-pushed the proper_instances1 branch from 1e18223 to 827aba6 Compare December 28, 2022 00:16

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Dec 28, 2022

ppedrot added the part: standard library The standard library stdlib. label Oct 30, 2023

JasonGross approved these changes Apr 17, 2024

View reviewed changes

JasonGross added the request: full CI Use this label when you want your next push to trigger a full CI. label Apr 17, 2024

add Proper instances for some number theorems to improve rewriting wi…

569b187

…th inequalities

JasonGross force-pushed the proper_instances1 branch from 827aba6 to 569b187 Compare April 17, 2024 17:53

coqbot-app bot removed request: full CI Use this label when you want your next push to trigger a full CI. needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. labels Apr 17, 2024

andres-erbsen removed the needs: benchmarking Performance testing is required. label Apr 19, 2024

andres-erbsen added this to the 8.20+rc1 milestone Apr 19, 2024

andres-erbsen added the kind: feature New user-facing feature request or implementation. label Apr 19, 2024

[stdlib] Add Proper instances for some number theorems to improve rewriting with inequalities #16792

Are you sure you want to change the base?

[stdlib] Add Proper instances for some number theorems to improve rewriting with inequalities #16792

Conversation

haansn08 commented Nov 11, 2022 • edited

ana-borges commented Nov 15, 2022

haansn08 commented Nov 15, 2022

haansn08 commented Nov 16, 2022

ana-borges commented Nov 16, 2022

ppedrot left a comment

Choose a reason for hiding this comment

haansn08 commented Nov 17, 2022

ppedrot commented Nov 17, 2022

haansn08 commented Nov 17, 2022

ppedrot commented Nov 17, 2022

JasonGross commented Nov 17, 2022

haansn08 commented Nov 18, 2022

JasonGross commented Nov 18, 2022

haansn08 commented Nov 23, 2022 • edited

JasonGross commented Nov 23, 2022

haansn08 commented Nov 25, 2022

mrhaandi commented Dec 9, 2022

haansn08 commented Dec 9, 2022

mrhaandi commented Dec 9, 2022

JasonGross commented Dec 9, 2022

JasonGross commented Dec 9, 2022

coqbot-app bot commented Dec 10, 2022

haansn08 commented Dec 11, 2022

JasonGross commented Dec 21, 2022

coqbot-app bot commented Dec 22, 2022

JasonGross commented Dec 22, 2022

haansn08 commented Dec 28, 2022

SkySkimmer commented Apr 17, 2024

andres-erbsen commented Apr 17, 2024 • edited

JasonGross left a comment

Choose a reason for hiding this comment

andres-erbsen commented Apr 17, 2024

JasonGross commented Apr 17, 2024

coqbot-app bot commented Apr 18, 2024

andres-erbsen commented Apr 18, 2024

andres-erbsen commented Apr 19, 2024

andres-erbsen commented Apr 19, 2024

[stdlib] Add `Proper` instances for some number theorems to improve rewriting with inequalities #16792

[stdlib] Add `Proper` instances for some number theorems to improve rewriting with inequalities #16792

haansn08 commented Nov 11, 2022 •

edited

haansn08 commented Nov 23, 2022 •

edited

andres-erbsen commented Apr 17, 2024 •

edited