Drastically speed up ByteCompareSpec

[JasonGross]

Old:

theories/ByteCompareSpec.vo (real: 113.67, user: 111.75, sys: 1.57, mem: 1287536 ko)

New:

COQC theories/ByteCompareSpec.v
theories/ByteCompareSpec.vo (real: 9.46, user: 8.89, sys: 0.26, mem: 442460 ko)

The new file is also compatible with COQNATIVE, taking only seconds rather than dozens of minutes or more.

[ppedrot]

I think that this qualifies as a workaround to an algorithmic issue in Equations, though. Ideally the noconfusion generated there should be the one from your patch.

[JasonGross]

I seen to recall @gares having written some elpi code to do this sort of thing (subquadratic Boolean equality reasoning) automatically, maybe the relevant code can be ported to Equations? Or maybe Equations can have a way of automatically proving that decidable equality implies NoConfusion? I can take a look at the relevant code if someone points me at it, but @mattam82 might know better how easy this approach is.

[gares]

Both the old and the new derive in Elpi prove no confusion by injecting to bool, IIRC, but they don't expose it as a lemma, they give you a view (a reflect), then do a discriminate over bool.

From elpi.apps Require Import derive.std.
From Coq Require Import Strings.Byte.

Time #[verbose] derive byte.

gives

Derivation map on indt «byte»
Derivation map on indt «byte» took 0.009060
Derivation lens on indt «byte»
Derivation lens on indt «byte» failed, continuing
Derivation param1 on indt «byte»
Derivation param1 on indt «byte» took 0.250504
Derivation param2 on indt «byte»
Derivation param2 on indt «byte» took 0.238456
Derivation tag on indt «byte»
Derivation tag on indt «byte» took 0.020242
Derivation eqType_ast on indt «byte»
Derivation eqType_ast on indt «byte» took 0.007213
Derivation lens_laws on indt «byte»
Derivation lens_laws on indt «byte» took 0.000974
Derivation param1_congr on indt «byte»
Derivation param1_congr on indt «byte» took 0.145295
Derivation param1_inhab on indt «byte»
Derivation param1_inhab on indt «byte» took 0.014063
Derivation param1_functor on indt «byte»
Derivation param1_functor on indt «byte» took 0.014611
Derivation fields on indt «byte»
Derivation fields on indt «byte» took 0.285149
Derivation param1_trivial on indt «byte»
Derivation param1_trivial on indt «byte» took 0.180951
Derivation induction on indt «byte»
Derivation induction on indt «byte» took 0.027863
Derivation eqb on indt «byte»
Derivation eqb on indt «byte» took 0.063260
Derivation eqbcorrect on indt «byte»
Derivation eqbcorrect on indt «byte» took 0.770846
Derivation eqbOK on indt «byte»
Derivation eqbOK on indt «byte» took 0.000868
Finished transaction in 2.123 secs (2.089u,0.031s) (successful)

But even if you run the legacy derive (which is quadratic):

From elpi.apps Require Import derive.legacy.

Time #[verbose] derive byte.

you get

Skipping derivation map on indt «byte» 
since it has been already run
Derivation lens on indt «byte»
Derivation lens on indt «byte» failed, continuing
Skipping derivation param1 on indt «byte» 
since it has been already run
Skipping derivation param2 on indt «byte» 
since it has been already run
Skipping derivation tag on indt «byte» 
since it has been already run
Skipping derivation eqType_ast on indt «byte» 
since it has been already run
Derivation projK on indt «byte»
Derivation projK on indt «byte» took 0.001412
Derivation isK on indt «byte»
Derivation isK on indt «byte» took 1.340290
Derivation eq on indt «byte»
Derivation eq on indt «byte» took 1.395229
Skipping derivation lens_laws on indt «byte» 
since it has been already run
Skipping derivation param1_congr on indt «byte» 
since it has been already run
Skipping derivation param1_inhab on indt «byte» 
since it has been already run
Skipping derivation param1_functor on indt «byte» 
since it has been already run
Skipping derivation fields on indt «byte» 
since it has been already run
Derivation bcongr on indt «byte»
Derivation bcongr on indt «byte» took 0.176446
Skipping derivation param1_trivial on indt «byte» 
since it has been already run
Skipping derivation induction on indt «byte» 
since it has been already run
Skipping derivation eqb on indt «byte» 
since it has been already run
Derivation eqK on indt «byte»
Derivation eqK on indt «byte» took 8.059469
Skipping derivation eqbcorrect on indt «byte» 
since it has been already run
Derivation eqcorrect on indt «byte»
Derivation eqcorrect on indt «byte» took 0.022050
Skipping derivation eqbOK on indt «byte» 
since it has been already run
Derivation eqOK on indt «byte»
Derivation eqOK on indt «byte» took 0.000982
Finished transaction in 11.111 secs (11.064u,0.053s) (successful)

So in any case there is something fishy in equations. IMO you should just not use Equations for deriving stuff over large (i.e. more than 50 constructors) datatypes, see also the benchmark section in https://laas.hal.science/INRIA/hal-03800154