The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

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