The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/04/2015 02:47 PM, Michael Shulman wrote:
> 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?

I have a working version embedded into other things - I will dis-embed 
it shortly and pass it along...

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

Probably there aren't enough laymen (like myself) interested in such 
things to motivate the effort.

-- Jonathan