The Coq mailing list

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

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?

`ring` always works for me when it is expected to, and it always does so immediately.

Only `ring_simplify` gets stuck sometimes. 

(When dealing with horrendous As, `ring_simplify` is very useful as I usually have no idea what the corresponding Bs looks like.)

 

What about

Goal B = 0.
ring_simplify

does this get stuck too?

Yes, this gets stuck too. 

So does `ring_simplify` on `(0:Rslow) = 0`. 

I tried `compute`  on `(0:Rslow) = 0`.  It got stuck too.

Then I carefully made every constant opaque in `(0:Rslow) = 0`.

After that, `compute` on `(0:Rslow) = 0` returns immediately without changing the goal at all, as expected.

However,  `ring_simplify` still gets stuck on `(0:Rslow) = 0`.

Is there a flag to prevent `ring_simplify` from performing any computations (reductions)?

(I understand that doing computations is useful in many cases, as explained in the manual.)

Thanks,

-- Abhishek

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