The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/04/2015 11:09 AM, Michael Shulman wrote:
> I wanted a version of the tactic "ring" which is able to make use of
> equalities in the context.  So I wrote my own:
>
> Ltac ring_useeq :=
>    first [ ring
>          | match goal with
>              | [ H : ?a = ?b |- _ ] =>
>                first [ rewrite H; clear H; ring_useeq
>                      | rewrite <- H; clear H; ring_useeq
>                      | clear H; ring_useeq ]
>            end ].
>
> If I did it right, this is doing a tree search through all possible
> combinations of rewriting in either direction or not at all with each
> equality in the context.  However, one could imagine it being even
> smarter and trying more things, e.g. in theory it might matter what
> order the rewrites happen in.  Does a tactic like this exist already
> somewhere?
>
> Mike

Mike,

I have been developing a set of tactics that does something like this - 
it rewrites ring equality hyps so that they have a single variable on 
their lhs, and then rewrites them over the goal, which produces a more 
general rewriting.  However, it only works for equalities that have a 
monomial variable in them - so not something like "x * y = 2 * z", but 
it will work for something like "x * y = 2 + z", as it will rewrite this 
first to "z = x * y - 2", then rewrite z using it.

Also, in many cases, the omega tactic (or the more general variants of 
it, like lia), can solve ring goals by making use of hyps without any 
needed rewriting.

-- Jonathan