The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hello Basile,

lia does:
1) naive conjunctive normal form + a tiny bit of arithmetic
2) genuine arithmetic reasoning

Given the shape of the goal, 1) is probably exploding.
After subst, the goal seems to simplify a lot.
The tiny bit of arithmetic is then probably sufficient to make the CNF
shrink ... exponentially - you're lucky!

So, this is unfortunate but not completely unexpected.
 
This gives me the opportunity to  unashamedly  advertise a better way
to proceed. I have recently implemented a tactic `itauto tac`[*] which 
uses a SAT solver and runs `tac` on the leaves of a propositional proof
search. For your goal, `itauto lia` succeeds instantly.

Best,
--
Frédéric

[*] https://gitlab.inria.fr/fbesson/itauto


On Tue, 2021-04-20 at 18:36 +0200, Basile Clement wrote:
> Dear Coq-Club,
> 
> It seems like `lia` fails on some goals containing equalities, but
> succeeds after a simple application of the `subst` tactic.  See
> attached .v file for such an example.
> 
> I was surprised by this, because I assumed that exploiting
> substitutions (i.e. equalities where one side is a variable) would be
> generally beneficial due to reducing the number of variables to handle.
> 
> Is this expected from the `lia` tactic?
> 
> Regards,
> - Basile