coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Announcing aac_tactics: a plugin for rewriting modulo associativity and commutativity

From: Thomas Braibant <thomas.braibant AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Cc: Damien Pous <Damien.Pous AT inria.fr>
Subject: [Coq-Club] Announcing aac_tactics: a plugin for rewriting modulo associativity and commutativity
Date: Wed, 16 Jun 2010 18:51:35 +0200
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:cc:content-type; b=ArjURrCnLZRxmETHNxdGHvuMEf3ETTZPM4feQa5rZzMJAaf0lErVp6s0yrNSfjBlgg SlHUs6+MlNVTuSEdgDXt82FS4xCSt3xkghIfHfLefLnlRQkQX65g173mkfZR90rNrS9B rMlF9jKLfrJpjSOjRhW0OPFPWpijFY+fjNiDQ=

We are pleased to announce the first release of aac_tactics, a Coq
plugin to support rewriting universally quantified equations, modulo
associativity (and possibly commutativity) of some arbitrary operators.

More details can be found from this web-page:
http://sardes.inrialpes.fr/~braibant/aac_tactics/

In particular, a tutorial Coq file illustrating the kind of tools we provide
can be found there:
http://sardes.inrialpes.fr/~braibant/aac_tactics/html/Tutorial.html

Thanks to all Coq developpers who helped us designing this plugin.

Comments (and bug reports) are welcome!

Thomas Braibant & Damien Pous

-------------------------------
(* Here is a minimal example illustrating the use of these tactics *)

Variables a b c : Z.
Hypothesis H: forall x, x + Zopp x = 0.
Goal a + b + c + Zopp (c + a) = b.
  aac_rewrite H.
  aac_reflexivity.
Qed.
Goal a + c+ Zopp (b + a + Zopp b) = c.
  do 2 aac_rewrite H.
  reflexivity.
Qed.

(* Of course, these particular goals can be solved by ring; for more
   complex examples, see the aforementionned tutorial. *)

[Coq-Club] Announcing aac_tactics: a plugin for rewriting modulo associativity and commutativity, Thomas Braibant