The Coq mailing list

[Emilio Jesús Gallego Arias <e AT x80.org>]

Hi Robert,

Robert Rand 
<rrand AT seas.upenn.edu>
 writes:

> I'm currently working on a Coq development in which the lia tactic takes up
> a significant percentage of the running time, which is already quite large.
>
> We previously used omega, which was substantially slower. The issue is that
> lia frequently chokes on problems that omega can solve instantaneously, and
> the converse is also true. (This behavior seems to be fairly well
> documented—if desired I can add examples.) Note that lia and omega are
> embedded inside other tactics, so we don't want to manually switch between
> them.
>
> In the absence of an ultimate arithmetic solver, I've been thinking it
> might be worth writing a tactic to interleave lia, [r]omega and possibly
> some other tactics (eg. ring)? Is this doable using Coq's timeout tactical,
> or would it make more sense to try to write a plugin? Which tactics would
> be worth including: Are there any known relationships between them, in
> terms of both what they can solve and how efficiently they can solve them?

As noted by Laurent, the plan is to have Coq provide an ultimate
arithmetic solver, and indeed omega is unsupported and scheduled for
removal: https://github.com/coq/coq/pull/7878

So IMHO the best plan of action would be indeed to coordinate with the `lia`
maintainers so they are aware of any remaining performance regression
[for that you may be requested to try Coq's master tho]

Dispatching goals of a certain shape to specialized solvers is a
different, and quite interesting subject.

Kind regards,
E.