---
fullname: AAC tactics
shortname: aac-tactics

description: |
  This Coq plugin provides tactics for rewriting universally quantified
  equations, modulo associativity and commutativity of some operator.
  The tactics can be applied for custom operators by registering the
  operators and their properties as type class instances. Many common
  operator instances, such as for Z binary arithmetic and booleans, are
  provided with the plugin.

paper:
  doi: 10.1007/978-3-642-25379-9_14
  url: https://arxiv.org/abs/1106.4448
  title: Tactics for Reasoning modulo AC in Coq

authors:
- name: Thomas Braibant
  initial: true
- name: Damien Pous
  initial: true
- name: Fabian Kunze
  initial: false

maintainers:
- name: Fabian Kunze
  nickname: fakusb
- name: Karl Palmskog
  nickname: palmskog

opam-file-maintainer: palmskog@gmail.com

license:
  fullname: GNU Lesser General Public License v3.0 or later
  identifier: LGPL-3.0-or-later

plugin: true

supported_coq_versions:
  text: Coq 8.9 (use the corresponding branch or release for other Coq versions)
  opam: '{>= "8.9" & < "8.10~"}'

tested_coq_versions:
- version_or_url: 8.9

tested_coq_opam_version: 8.9

namespace: AAC_tactics

keywords:
- name: reflexive tactic
- name: rewriting
- name: rewriting modulo associativity and commutativity
- name: rewriting modulo ac
- name: decision procedure

categories:
- name: Miscellaneous/Coq Extensions
- name: Computer Science/Decision Procedures and Certified Algorithms/Decision procedures

documentation: |
  ## Documentation

  The following example shows an application of the tactics for reasoning over Z binary numbers:
  ```coq
  Require Import AAC_tactics.AAC.
  Require AAC_tactics.Instances.
  Require Import ZArith.
  
  Section ZOpp.
    Import Instances.Z.
    Variables a b c : Z.
    Hypothesis H: forall x, x + Z.opp x = 0.
  
    Goal a + b + c + Z.opp (c + a) = b.
      aac_rewrite H.
      aac_reflexivity.
    Qed.
  End ZOpp.
  ```
  
  The file [Tutorial.v](theories/Tutorial.v) provides a succinct introduction
  and more examples of how to use this plugin.
  
  The file [Instances.v](theories/Instances.v) defines several type class instances
  for frequent use-cases of this plugin, that should allow you to use it off-the-shelf.
  Namely, it contains instances for:
  
  - Peano naturals	(`Import Instances.Peano.`)
  - Z binary numbers	(`Import Instances.Z.`)
  - N binary numbers	(`Import Instances.N.`)
  - P binary numbers	(`Import Instances.P.`)
  - Rational numbers	(`Import Instances.Q.`)
  - Prop			(`Import Instances.Prop_ops.`)
  - Booleans		(`Import Instances.Bool.`)
  - Relations		(`Import Instances.Relations.`)
  - all of the above	(`Import Instances.All.`)
  
  To understand the inner workings of the tactics, please refer to
  the `.mli` files as the main source of information on each `.ml` file.
  
  ## Acknowledgements
  
  The initial authors are grateful to Evelyne Contejean, Hugo Herbelin,
  Assia Mahboubi, and Matthieu Sozeau for highly instructive discussions.
  The plugin took inspiration from the plugin tutorial "constructors" by
  Matthieu Sozeau, distributed under the LGPL 2.1.
---