coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Monoid and Group?

From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] Monoid and Group?
Date: Wed, 4 Apr 2018 23:07:40 +0000
Accept-language: en-CA, en-US
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=None smtp.helo=postmaster AT NAM04-SN1-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:ctpZihWwutAsBX/aWDl79fPFFKzV8LGtZVwlr6E/grcLSJyIuqrYYxyDt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRNjzIHZe5uaOOZicq7HYd8WWXdNU8BMXCJBGIO8aI4PAvIFM+lCtIn9oF0OpganCQavBOPvzTlIhnDr1qMn0+QuDwfG3AM5E9kTsnrUscj+OaAcUe+ozKnJzC7DY+1K1Tvg9ITFaRAhofaQXbJ1a8XRyE0vGxnZgVWXrIzoJjWY3fkOvWiD9+dtWv6jh3Qjpg1vuDSj29oghpPNi44LzF3P6D93z5wvJdKiTU52ed6kH4VUtyGdL4Z4Wt8vTWZ0tCs107EIpIa1cDUTxJQg3BHQdeaLc4+V4hL/T+mRJip4hHR4d76lnxay60+gyvHiWcaozFZKry1Fkt/WunAKyhzT9syHSvx6/keiwzqAywfT6uRcLUA1k6rUNYIhz6Y/m5YPq0jOGjH6lF/rgKOLbEkp/vak5/ziYrr8p5+cM4F0ihv5MqQrgsG/D/k3MggPXmiA5+iwyKDv8VHiTbVKif02jqzZv4rbJcQfvKK2HwhV0oM75xalEzimyMgYnWUALF9dZB2HiJHpN0jSL/D8EPewmE+hkCxrxvDDJr3uGI/BLnnFkLf7fLZy8VRQyAQpzYMX25UBQLoGObf4XlL7nN3eFB4wdQKuia6zA9Jkk4gaRGinA6mDMaqUv0Xetcw1JOzZRoYOvzC1bsol4PjhxUQ5lFkSOOGJwNNDZny4DO88exzBSXrrntIIEGNMtQ07Gr+5wGaeWCJeMi7hF5k34Ss2Xdr/XNXzA7u1ibnE5x+VW5hfZ2RIEFeJSCy6d4KYXv4NbGSZJcozy2VYB4jkcJco0FSVjCG/06Bud7GG+ioEsJvi0J5+4OiBzUhvpwwxNNyU1iS2d08xnm4MQGNpjoZWhBQhj2yliO1/ifEeEsFP7fRUVAt8LYTb0+FxF9H1XETGY8uNT1GlBN6hBGNpQw==
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

Hi all,

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?

Sincerely Yours,

Jason (Zhong Sheng) Hu
cell phone: (514) 803-1838

[Coq-Club] Monoid and Group?, Jason -Zhong Sheng- Hu, 04/05/2018
- Re: [Coq-Club] Monoid and Group?, Pierre-Marie Pédrot, 04/05/2018
- <Possible follow-up(s)>
- Re: [Coq-Club] Monoid and Group?, makarius, 04/05/2018