The Coq mailing list

[Assia Mahboubi <Assia.Mahboubi AT inria.fr>]

Dear Mike,

Le 04/11/2015 17:09, Michael Shulman a écrit :
> I wanted a version of the tactic "ring" which is able to make use of
> equalities in the context.  

[...]

>  Does a tactic like this exist already
> somewhere?
> 

It seems to me that the full generality of what you ask for would solve a
different (and more difficult) problem than the ones the ring tactic is 
designed
to solve.

The ring tactic normalizes terms modulo the axioms of a structure of
(commutative) ring and possibly decides the equality of two such terms, 
deduced
from the equality of their normal forms.

For this purpose, an oracle in the ring tactic extracts a polynomial 
expression
from the term to be normalized, abstracting away all its subterms that are not
in the ring syntax. The evaluation of the normal form of the polynomial at the
tuple of abstracted subterms provides the normal form of the original term.

Now in general, the problem you describe looks more like deducing the nullity 
of
a polynomial (the equation in your goal) from the nullity of some others (the
hypotheses you rewrite), plus the ring axioms of course. This is called the
ideal membership problem and it is solved algorithmically by elimination
methods. If we can reduce the problem to ideal membership in K[X1,...,Xn] 
with K
a field, the common method uses Gröbner bases computation.

Some people have worked on Coq tactics solving this problem, using a certified
implementation of Buchberger's algorithm (see for instance Théry's paper :
http://dx.doi.org/10.1023/A:1026518331905) or certifying the result of
certificates produced by external implementations (see for instance Pottier's
paper : http://arxiv.org/abs/1007.3615).

But I have no idea about the current status of the corresponding code... May 
be
someone better informed than I am can provide more information.

Hope this helps,

assia