The Coq mailing list

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

> On 22 Sep 2016, at 16:18, Soegtrop, Michael 
> <michael.soegtrop AT intel.com>
>  wrote:
> 
> Dear Frédéric,
> 
> I can confirm that the mylia tactic works in 8.5pl2. But it is far from 
> obvious what your wrapper does and how and why. Would you mind writing a 
> few lines on this or give some pointers?
In 8.5, lia is using ‘abstract’ with the intention of speeding-up 
computations.
However, abstract does not handle existentials. Therefore, lia fails in your 
example because of the abstract.
mylia is a cut and paste of the existing lia tactic without abstract.

I do not think this gives any insight why omega fails...

For Laurent,
This summer, I hope I made lia more robust — thanks to multiple bug reports 
from Jason.
Because it now extract a clean purely arithmetic, quantifier-free goal that 
is solved independently,
I hope it is immune to existential variables. (I very welcome stress tests.)

The changes were committed in the 8.6 branch.

—
Frédéric



> 
> Best regards,
> 
> Michael
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928