The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 01/01/2016 01:39 AM, Abhishek Anand wrote:
> 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.

Did you solve your problem? My guess is that you get stuck because of 
some hidden computation in Rslow.

In your example in Rslow you want to simplify A into B.

What happens if you do directly

Goal A = B.
ring.

Is this immediate?

What about

Goal B = 0.
ring_simplify

does this get stuck too?

regards,

--
Laurent