Home

Awesome

<!--- This file was generated from `meta.yml`, please do not edit manually. Follow the instructions on https://github.com/coq-community/templates to regenerate. --->

AAC Tactics

Docker CI Nix CI Contributing Code of Conduct Zulip coqdoc DOI

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.

Meta

Building and installation instructions

The easiest way to install the latest released version of AAC Tactics is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-aac-tactics

To instead build and install manually, do:

git clone https://github.com/coq-community/aac-tactics.git
cd aac-tactics
make   # or make -j <number-of-cores-on-your-machine> 
make install

Documentation

The following example shows an application of the tactics for reasoning over Z binary numbers:

From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
From Coq 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.

  Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a.
    aac_normalise.
    aac_rewrite H.
    aac_reflexivity.
  Qed.
End ZOpp.

The file Tutorial.v provides a succinct introduction and more examples of how to use this plugin.

The file 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:

To understand the inner workings of the tactics, please refer to the .mli files as the main source of information on each .ml file.

See also the latest coqdoc documentation and the latest ocamldoc documentation.

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.