Merge pull request #92 from coq-community/v8.13+idemfix

Make 8.13 consistent with 8.14

README.md

@@ -30,12 +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.
+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
 
@@ -77,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.
@@ -90,6 +90,12 @@ Section ZOpp.
     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.
 ```
 

coq-aac-tactics.opam

@@ -1,3 +1,6 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
 opam-version: "2.0"
 maintainer: "[email protected]"
 version: "8.13.dev"
@@ -7,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.13'
 
 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.
   ```
   

theories/Tutorial.v

@@ -48,6 +48,30 @@ Section introduction.
      - here, ring would have done the job.
      *)
 
+  (** several associative/commutative operations can be used at the same time.
+      here, [Zmult] and [Zplus], which are both associative and commutative (AC)
+   *)
+  Goal (b + c) * (c + b) + a + Z.opp ((c + b) * (b + c)) = a.
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
+
+  (** some commutative operations can be declared as idempotent, here [Z.max]
+      which is taken into account by the [aac_normalise] and [aac_reflexivity] tactics.
+      Note however that [aac_rewrite] does not match modulo idempotency.
+   *)
+  Goal Z.max (b + c) (c + b) + a + Z.opp (c + b) = a.
+    aac_normalise.
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
+
+  Goal Z.max c (Z.max b c) + a + Z.opp (Z.max c b) = a.
+    aac_normalise.
+    aac_rewrite H.
+    aac_reflexivity.
+  Qed.
+
 End introduction.