coq-club AT inria.fr

Subject: The Coq mailing list

List archive

RE: [Coq-Club] Tactic for commutative group?

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Tactic for commutative group?
Date: Wed, 7 Aug 2019 11:01:26 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga18.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.2.0.6
Ironport-phdr: 9a23:OmkDjhJriiACZWjpPNmcpTZWNBhigK39O0sv0rFitYgeIvrxwZ3uMQTl6Ol3ixeRBMOHsqgC0rOM+Pu7EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCejbb9oMRm6sBvdusYYjIZsN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9gqJFrhy8uxxxzY3aYI+XO/p/YqzScsgXSnBdUstVTSFNHp+wYokJAuEcPehYtY79p14WoBewGAesA/3gyjBUhn/s2q06y/wtGhzB0gwhA90OsG7bo8vxNKscTOu4y6zIzTTfYPNWwzjy9ozIfgo6ofGLQ71wftbRyVMoFwPdlViQqIrlPy+L2eQJqWSU8+1gVee2hmMhtgp/rD+vxsI2hYnIgIIY0l/E9SRlwIY1ON23U1R3bsKjEJtVry2aNo12Qt88TGFsoio116MJtJimdyYJ0JQq3wPTZvKIfoSS/x7uWumcLS1liH9reb+znQu+/Vahx+HkS8W50VhHojBLn9TCrHwByRLe58ydRvdg/UqtxC6D2x3S5+xAO0w4i6rWJpE7zrIujJYesUDOEynrk0vslqCWbF8r+u2w5uTnfLrmopicOpdxigHxKKsih8+yDf45MggIQ2iU5+C82Kf/8k3+RbVGlvw2kq/Hv5DGPckXu6C0DgBP3oo+5RuyAC2q3MkWkHQGNl5JZQyLgonxN1HLOv/4DPO/g1q2kDdswvDLJrjhApTRIXjDirjuY7J951RHyAo0099f6I5UCqsGIPLrQULxtdrYDgMnPAyw2eroFNJ91oYGVWKVHqCZKL/SsUOP5u83P+aMY5YVtC/hJPgh+v7hlmQ0mUQdfKmsxZsYcmq0HvVgI0WDYHrjmM0NEWkQvll2cOu/wlaFSHtYY2u4d6M6/DAyToy8R8+XTYe0xbeFwS2TH5tMZ2kABEraQlnycIDREcwLZS2OOMh51nQhVLOhQoIln1n6sQ7xy7NqKqzP/SAXqYjkzPB04fHekVc58jkiXJfV6H2EU2whxjBAfDQxxq0q+RUsmGfG6rBxhrljLfIW4vpIVgkgMpuFlr57Dcz/XkTKedLbEQ/6EOXjOik4S5cK+/FLe1x0Qozwjxbf0i7sCLgQxeTSWc4Et5nE1n20HP5TjnbL0K540AsjTcIWZSungLJy807YAIuby0g=

Dear Qinxiang,

> I am wondering, if I want to prove something for a user-defined commutative group

> (its like we have zero, addition and subtraction but not multiplication), is there any

> proof automation I can use?

I am using the aac-tactics plugin for this:

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

Although it advertises to only support associativity and commutativity, it can work with inverse elements by explicit rewriting for the inverse. But handling inverses is not fully automated as commutativity and associativity are. See e.g. the first example in:

https://github.com/coq-community/aac-tactics/blob/master/theories/Tutorial.v

Best regards,

Michael

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[Coq-Club] Tactic for commutative group?, Cao Qinxiang, 08/07/2019
- RE: [Coq-Club] Tactic for commutative group?, Soegtrop, Michael, 08/07/2019
  - Re: [Coq-Club] Tactic for commutative group?, Cao Qinxiang, 08/08/2019