The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

Hi,

On 05/04/2018 01:07, Jason -Zhong Sheng- Hu wrote:
> I am wondering if there is a good support for monoid reasoning and group
> reasoning, namely definitions of structures and corresponding tactics? I
> don't find any from the doc and the source code.
> 
> 
> I kind of find it strange jumping to support semiring, ring and field
> without supporting two more common and basic structures.  Especially
> monoid is observably everywhere, and I dream to have tactics like
> monoid, monoid_simplify to ease my life.
> 
> 
> Or is there anyone has written a library for reasoning of these two
> structures?

There used to be a dedicated library called aac-tactics for rewriting up
to associativity and commutativity :

https://github.com/coq-contribs/aac-tactics

This is precisely what you need for groups and monoids. Unluckily, I
think it is currently unmaintained.

Otherwise, you can probably try to fiddle with the relation-algebra
library, which AFAIU superseded aac-tactics.

https://github.com/damien-pous/relation-algebra

They have a set of tactics for richer settings like Kleene algebras, but
you might manage to use it for monoids and the like.

Cheers,
PMP

Attachment: signature.asc
Description: OpenPGP digital signature