The Coq mailing list

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

On 04/13/2016 09:54 PM, Abhishek Anand wrote:
> A few months ago, I was happy to find in the manual
> <https://coq.inria.fr/refman/Reference-Manual028.html> that the ring
> tactic can be supplied with
> additional ring equalities using the ring [...] syntax.
> However, it seems that the ring tactic is NOT complete w.r.t the
> supplied equalities. This is illustrated in the example below, which was
> checked with Coq 8.5.

maybe the documentation is not clear about this:

the mechanism provided by the equation is very naive (no knuth-bendix 
like completion), it was meant to be used for cancellation (when a 
monomial can be expressed in terms of "simpler" ones like y^2 = x + y).
Your example would of course work with the "canonical" H : y = 0.

> Is there some other tactic (for unquantified ring equations) that is
> complete w.r.t the supplied (unquantified) ring equalities and the ring
> laws? It need not be complete w.r.t. definitional equalities.

You can use the nullstellensatz tactic nsatz  but of course the 
complexity of the procedure is much higher:

Require Import Nsatz.

Section test.

Context {R:Type}`{Rid:Integral_domain R}.

Lemma nsatz_test1 : forall (y:R),  (1 + 1) * y == y -> y + y == 0.
Proof.
Time nsatz.
Qed.

End test.


> Also, is there a similar tactic for boolean rings (where forall x,
> x*x=x), instead of regular rings?

Not that I remember of, but calling ring with the equations x * x = x
for all the boolean variables of your expression should do the trick.

--
Laurent