The Coq mailing list

[Robert Rand <rrand AT seas.upenn.edu>]

Hi all,

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?

(Note that we're mainly concerned with equalities between nats.)

Thanks,

Robert