The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

On Wed, Nov 4, 2015 at 8:35 AM, Jonathan Leivent 
<jonikelee AT gmail.com>
 wrote:
> 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.

Nice!  Is anything available yet?

> 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.

Yes, that's true.  But omega doesn't cover all my use cases (if I'm
reading the manual correctly, it's because omega can't deal with
equations involving variables multiplied together).  I don't really
understand what lia can do.  Hugo pointed out privately that nsatz
will also work, at least over an integral domain.

Is there a description and comparison of all of the automatic algebra
tactics somewhere that explains in layman's terms what each of them
can and can't do?

Mike