make documentation and meta.yml consistent

README.md

@@ -30,16 +30,12 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 [doi-shield]: https://zenodo.org/badge/DOI/10.1007/978-3-642-25379-9_14.svg
 [doi-link]: https://doi.org/10.1007/978-3-642-25379-9_14
 
-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.
-
-An additional tactic makes it possible to prove equations between
-expressions involving associative/commutative/idempotent operations
-and their potential units.
+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
 
@@ -81,9 +77,9 @@ make install
 
 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.
+From AAC_tactics Require Import AAC.
+From AAC_tactics Require Instances.
+From Coq Require Import ZArith.
 
 Section ZOpp.
   Import Instances.Z.

coq-aac-tactics.opam

@@ -10,14 +10,14 @@ dev-repo: "git+https://github.com/coq-community/aac-tactics.git"
 bug-reports: "https://github.com/coq-community/aac-tactics/issues"
 license: "LGPL-3.0-or-later"
 
-synopsis: "Coq plugin providing tactics for rewriting universally quantified equations, modulo associative (and possibly commutative) operators"
+synopsis: "Coq tactics for rewriting universally quantified equations, modulo associative (and possibly commutative and idempotent) operators"
 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."""
+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."""
 
 build: ["dune" "build" "-p" name "-j" jobs]
 depends: [

meta.yml

@@ -10,16 +10,16 @@ doi: 10.1007/978-3-642-25379-9_14
 branch: 'v8.14'
 
 synopsis: >-
-  Coq plugin providing tactics for rewriting universally quantified
-  equations, modulo associative (and possibly commutative) operators
+  Coq tactics for rewriting universally quantified equations, modulo
+  associative (and possibly commutative and idempotent) operators
 
 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.
+  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.
 
 publications:
 - pub_doi: 10.1007/978-3-642-25379-9_14
@@ -78,19 +78,25 @@ 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.
-  
+  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.
   ```