The Coq mailing list

[Fr�d�ric Besson <frederic.besson AT inria.fr>]

On 2 août 2011, at 14:03, Laurent Théry wrote:

No, I meant coqtop. Problem is so demanding and proof take so much time

because it's problem within Presburger arithmetic which I try to solve

using omega. It use many hypothesis and axioms. Problem is provable. I

have proved it in theory!

Unfortunately omega is based on fourier elimination so is very sensitive to
the number of equations.
Just to be sure that it is a problem of exponentiel blow-up can you try
with the lia tactic (Require Import Psatz) to see if this crashes too?

Just to complement Laurent's answer:

lia works for Z. If your problem is over nat,  zify ; unfold Zsucc in * ; lia does the trick.

PS: If it still blows up memory with lia, I would be interested in looking at your goal.

--

Frédéric Besson