The Coq mailing list

[Robert Rand <rnrand AT gmail.com>]

Thanks for all the helpful responses!

I believe zify is already part of the preprocessing step for lia, so I've never called it separately.

If major revisions to lia are in progress, I'm happy to wait for them and provide some test cases. I was under the impression that this work had stalled (the pull request to remove omega has been open for a while). 

Has anyone compared the performance of solvers like ring/field to lia/lra? If not, the QWIRE and SQIRE libraries make pretty heavy use of both lia and lra, so I could try prepending "try ring/field" and see what happens. (They actually generally call (essentially) "split; lra" since we're usually dealing with complex number equalities, so "field" can skip the splitting step. It doesn't sound like lia/lra are similarly flexible, though.)

Thanks,

Robert

On Wed, Aug 21, 2019 at 10:39 AM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

Dear Robert,

 

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

 

Are you aware of the zify tactic? It converts goals on nats into goals on Z. At least in the past lia could handle this more easily. I didn’t try it in a while though and afaik lia got quite some improvements since then.

 

I fully agree with Laurent and Emilio that the best way forward is to improve lia by providing test cases to the authors.

 

This can be done with timeout, but it is dangerous because it makes your proofs depend on the machine, the current load and other effects. E.g. it could happen that lia can solve a goal within the timeout in one run but not within another run and the alternatives can’t solve it at all, so that the proof would fail in some runs but not in others. Of cause one could do something like trying tactics alternatingly with increasing timeouts (a simple combination of first and timeout should do). But I have my doubts if this is on average faster than trying one tactic after the other.

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, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928