From 491b18aab9ceb1dab8f4c97aecf4d3ed42376056 Mon Sep 17 00:00:00 2001 From: Karl Palmskog Date: Sun, 10 Oct 2021 11:14:14 +0200 Subject: [PATCH] make documentation and meta.yml consistent --- README.md | 22 +++++++++------------- coq-aac-tactics.opam | 14 +++++++------- meta.yml | 32 +++++++++++++++++++------------- 3 files changed, 35 insertions(+), 33 deletions(-) diff --git a/README.md b/README.md index 66c9f21..a2b1dc9 100644 --- a/README.md +++ b/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. diff --git a/coq-aac-tactics.opam b/coq-aac-tactics.opam index 533e6dc..016fb23 100644 --- a/coq-aac-tactics.opam +++ b/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: [ diff --git a/meta.yml b/meta.yml index 37885bb..92b2fbf 100644 --- a/meta.yml +++ b/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. ```