coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Cao Qinxiang <caoqinxiang AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Tactic for commutative group?
Date: Thu, 8 Aug 2019 09:43:17 +0800
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=caoqinxiang AT gmail.com; spf=Pass smtp.mailfrom=caoqinxiang AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f54.google.com
Ironport-phdr: 9a23:2+Vn1RXHurEnxK7K8EvLj34I+nDV8LGtZVwlr6E/grcLSJyIuqrYYxKBt8tkgFKBZ4jH8fUM07OQ7/m6HzVZvd3b6TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrswndrNQajZZtJ6o+1BfFv2ZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWXFMUdxNWyFbGI6wc5cDAugHMO1Fr4f9vVwOrR6mCASyHuzvzSJDiGT33a083OUhEBvJ3AovH9kTt3nbsM/6NKALUeC0yqnJwjTDYOlQ2Tfy84XIfRUhruuNXbJ0a8be1U4vFwbcg1iWtIfrMTSV1uEXvGia6eptTe2vi287qwFxvzig3d0ghZXOhoIQ0lzE9CN5wJorKt28UkJ0fMCrHZ1NvC+ZL4t7Wt0uT31stSogybALuYS3cDYXxJg73RLSa/OKfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJkt7QtnwQzhDT5MiKR/Rn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn7upOQLY95hw7mPqQrgMO/AOA4MgYUX2ic/OSxzKHs8lf+QLVTj/02lKbYsJHAKsQdqa60GABV0oM55Ba+CzeqysgXnX4CLF5dYhKIk5DpO03SIPD/Ffqwn1OskC5yy//aOr3hH47CI2PYkLbheLZ981RTxBAyzdBZ/ZJUC6sOLOj9Wk/r55TkCUoyNBXxyOL6Av180JkfUCSBGPy3KqTX5HSB4aoWIu+cZYYTt36pIPEi/v/onX4wn1A1cqyg3J9RY3e9SKc1a36FaGbh149SWVwBuRAzGbSz2Q+yFAVLbnP3ZJoSozQyCYaoF4DGH9n/j7mI3SP9FZpTNDkfVgK8VEzwfoDBYM8iLTqIK5Y4wDMBXLmlDYQm0EP27VKo+/9cNuPRvxYgm9fj2dxyvbCBkBgz8XlzE53Y3TzRCW5zmWwMSnk926Ut+UE=

Thank you very much!

- Qinxiang Cao

On Wed, Aug 7, 2019 at 7:02 PM Soegtrop, Michael <michael.soegtrop AT intel.com> wrote:

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