The Coq mailing list

[Marko Malikovi� <marko AT ffri.hr>]

Dear Chantal,

Thank you very much!
However, I still (for my needs) have to stay in the type nat instead
switch to Z. Also, I can't convert my types from Prop to Bool. Therefore,
I must rely on Omega.
In the meantime, I actually understood what seem to be one of the biggest
problem with the Omega (except propositional structure indicated by Mr.
Besson). The problem is subtraction (minus). I do not know how omega's
algorithm handles with a subtraction, but subtraction in Presburger
arithmetic actually can be reduced to disjunction. It seems to me that
omega for each minus generates two new subgoals. If I am wrong then Mr.
Besson (or you) can correct me.
Experimentally I got the following: Suppose that we have 10 subtractions
in the goal and that proof needs, for example, 50 seconds. If we eliminate
one minus (for example, if we convert expression x-y=0 into x<=y) then the
goal will be proven approximately two times faster and will need about 25
seconds. And so on...
I can not affect to the omega, and therefore I am now focused on the
reduction of subtractions in our goals and generated subgoals.

Greetings and thanks again,

Marko Malikoviæ

> Hello Marko,
>
> The main (current) problem with SMTCoq is that it is working in bool and
> not in Prop (we are working on changing it). However, as you said you do
> not care if it is a bit slow, you can first change your goal into a
> boolean problem (using autorewrite) then use SMTCoq. Attached is your
> example; it works fine with coqtop in less than ten seconds.
>
> Chantal.
>
>> In the future, there is hope using SAT, SMT techniques.
>> The most mature prototype is probably SMTCoq:
>> http://www.lix.polytechnique.fr/~keller/Recherche/smtcoq.html
>


-----------------------
Dr. Sc. Marko Malikoviæ
Filozofski fakultet
Sveuèili¹te u Rijeci
---------------------
Ph.D. Marko Malikoviæ
Faculty of Humanities and Social Sciences
University of Rijeka, Croatia
-----------------------------
marko AT ffri.hr
http://www.ffri.hr/~marko
-------------------------