Could `itauto lia` become a replacement for `lia`?
When lia
is run on goals with many hypotheses containing disjunctions and implications, it can become very slow: https://github.com/coq/coq/issues/10743
However, if we run itauto lia
instead of lia
on these goals, they are solved immediately.
Therefore, it would be nice if lia
could be made an alias for itauto lia
, so I did an initial benchmark on the bedrock2 codebase to see if this is within reach, and the answer might be yes
The benchmark should be reproducible by checking out this commit, running make
, and this script (in order to make the build work, I worked around #2 (closed) and around #3 (closed)).
Here's a graph comparing the running times of plain lia
to itauto lia
:
The dots below the red line are the good ones (itauto lia
is faster than lia
), and the dots above the red line are the ones that we should improve.
As we can see, the cases where lia
takes 1s or more are solved instantaneously by itauto lia
, which is very promising!
On a log scale, it looks as follows:
And some more stats:
- number of cases where
lia
is faster: 84792 - number of cases where
itauto lia
is faster: 139 - number of cases where both have the same running time: 8346
- total number of measurements: 93277
- total time taken by
lia
: 52.4s - total time taken by
itauto lia
: 396.1s - total build time: ~ 1 hour (forgot to measure precisely)