coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Monoid and Group?

From: Fabian Kunze <kunze AT ps.uni-saarland.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Monoid and Group?
Date: Thu, 31 May 2018 11:29:56 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=kunze AT ps.uni-saarland.de; spf=Pass smtp.mailfrom=kunze AT ps.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
Ironport-phdr: 9a23:Oj7z0RGj4v28hLMGCRlrBZ1GYnF86YWxBRYc798ds5kLTJ78oMmwAkXT6L1XgUPTWs2DsrQY07eQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDqwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAeobMulDronyvV0Opga7CwmxAuPuyyFHjWLx0K05zuQhFwDH0xI7EtIWq3TYtsj1NKETUeys16nH1y/Mb+lS2Tjn7ojHbwotruySUr9pd8fa1EchFwTAjlqKqIzlOSuY1usMs2iH7+pgSPmgh3Q7pAF2pziiwNonhIrRho8N11zJ+yp0zJwxKNC5UkJ2Y8SoHIVQui2CKYd6XscvT3trtSs60LEKp4O3cScQxJko2RLSbeGMfZKS7RL5TumRJC91hHJ7d7K7gBa/6VSgyvf9Vsmo11ZKqDBJksPNt3wXyhzT7MmHRuJm/ki7wzmPzQTT5ftCIU8pj6bUNoAuzqYxlpoVr0vDAjf7lFj4gaKZbEkp/uml5/7lb7n8uJORN5d4igTkPaQvnsy/D/44Mg8LX2WD+uS8ybvj/EznT7hRlv02ibPVsI3cJcQav6K5GBVa3Zw56xa7FTim1skXkWMaI11bYB6HlZTmO0nSIPDkCveym0ijkDByx/zfIrLhBojNIWPYnbf6fbd97lZcxxApwdBe4ZJUELABL+jpVk//rtyLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDY43ItlrdyOslIuCKLKwIviTwY6wm+vj8gFchghkAe6jsxpIecnSxGPggL0jPMimkucsIDWpf5ll2d+ftklDXCWcCNUb3ZLo143QAMKzjCI7CQo63h7nbhHWjBdtLYGEDEVmFC3PhcYnCV/peMXvOcP8kqSQNUP2ac6FkzQun7leo06EhM+zVvzYRvIjn3d55oeHex0lrqG5ESv+F2mTIdFla22MFQzhsg/Jju01hzVHFy7o+nvpZUMda7ulNWwE2c5LRnbR3

FYI: I ported AAC to coq 8.7 and 8.8.

Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> schrieb am Do., 5. Apr. 2018 um 14:56 Uhr:

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

Re: [Coq-Club] Monoid and Group?, Fabian Kunze, 05/31/2018