1 files changed, 109 insertions, 0 deletions
diff --git a/meta.yml b/meta.yml
new file mode 100644
index 0000000..bc7f672
--- /dev/null
+++ b/meta.yml
@@ -0,0 +1,109 @@
+---
+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.
+---