The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

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