From 37bbfc26a69d3507937e5057fc9fb1c106e1f16a Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 10 Oct 2021 11:42:57 +0200 Subject: [PATCH 1/2] update documentation for idempotence --- README.md | 24 +++++++++++++++--------- coq-aac-tactics.opam | 17 ++++++++++------- meta.yml | 32 +++++++++++++++++++------------- 3 files changed, 44 insertions(+), 29 deletions(-) diff --git a/README.md b/README.md index 2f3481c..25ddd52 100644 --- a/README.md +++ b/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. ``` diff --git a/coq-aac-tactics.opam b/coq-aac-tactics.opam index 22cef86..6800585 100644 --- a/coq-aac-tactics.opam +++ b/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: "palmskog@gmail.com" 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: [ diff --git a/meta.yml b/meta.yml index b4050b2..bdb0ba7 100644 --- a/meta.yml +++ b/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. ``` From 874d2554b7ebba9bd5f3d061a6a3335b52b5ea89 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 10 Oct 2021 11:45:48 +0200 Subject: [PATCH 2/2] update tutorial with new examples by Damien Pous --- theories/Tutorial.v | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/theories/Tutorial.v b/theories/Tutorial.v index 74342f8..c893799 100644 --- a/theories/Tutorial.v +++ b/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.