The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Recently, I have often encountered situations where ring_simplify would never return and take up all the memory (~16GB).

In these cases, the involved ring (say Rslow) is a computational one, i.e. the ring operations have concrete implementations in Coq, and are not axiomatic.

When ask ring_simplify to simplify the exact same formula in a different ring, e.g. Z, or a totally abstract one, ring_simplify immediately returns with the  correct answer (normal form).

Once I obtain the normal form, I can go back to the original ring Rslow, and quickly

prove the correctness of the normal form using the ring tactic. 

Is there a way to debug such problems with ring_simplify on Rslow. I tried making all the ring operations of Rslow opaque, but that did not help -- maybe I missed something.

Is there a way to find the cause of the blowup?

Here is one problematic formula :

((X * (c * c) + xy * s * c + Y * (s * s)) * (X1 * X1) +

(Y * (c * c) - xy * s * c + X * (s * s)) * (Y1 * Y1) +

((X0 * c + Y0 * s) * X1 + (Y0 * c + - X0 * s) * Y1 +

 (xy * (1 - 2 * (s * s)) + (Y - X) * (2 * s * c)) * X1 *

 Y1 + cc))

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/