View the project on GitHub
Welcome to the AAC Tactics project website! This project is part of coq-community.
This Coq plugin provides tactics for rewriting and proving universally quantified equations modulo associativity and commutativity of some operator, with idempotent commutative operators enabling additional simplifications. The tactics can be applied for custom operators by registering the operators and their properties as type class instances. Instances for many commonly used operators, such as for binary integer arithmetic and booleans, are provided with the plugin.
This is an open source project, licensed under the GNU Lesser General Public License v3.0 or later.
The current stable release of AAC Tactics can be downloaded from GitHub.