coq-club AT inria.fr
Subject: The Coq mailing list
List archive
[Coq-Club] Second release of aac_tactics: a plugin for rewriting modulo associativity and commutativity
chronological Thread
- From: Thomas Braibant <thomas.braibant AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Second release of aac_tactics: a plugin for rewriting modulo associativity and commutativity
- Date: Thu, 2 Dec 2010 17:09:27 +0100
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type :content-transfer-encoding; b=R99b9Z6sadfn+2U3lR365yLqFvgy4EnCpbtQ3EZ6FjXcZmi66aWqSCtDkj2u+7vQ+H 9Mj+UjYDdz8VjkgJDpQ2uTGFVAZdDN+xByi6X+xOFAEvAimUIl9heW15U+nNTlbT2DJV fH4+HWCwPDhepSyqbwzh5azeKT9AfsR4zSdTM=
We are pleased to announce the second 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/
Salient changes with regards to the previous version are:
- Support for binary operators without units (like max on Z)
- Several operators can share a given unit (like max and plus sharing
zero on nat)
- Support for non symmetric relations
- Overhauled inference of morphisms and operators :
- Lift the previous requirement to have at least one AC and one A
operator on each considered type
- Binary operators can be polymorphic (e.g., List.app is recognised
as being associative)
- Should now be able to handle goals with evars (but this is not
unification modulo AC)
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 small example illustrating the use of these tactics to
prove the reverse triangle inequality*)
Lemma Zabs_triangle: forall x y, Zabs (x+y) ≤ Zabs x + Zabs y.
Lemma Zplus_opp_r : forall x, x + - x = 0.
Variables a b : Z.
Goal Zabs a + - Zabs b ≤ Zabs (a - b).
aac_rewrite ← (Zminus_diag b) at 3.
unfold Zminus.
aac_rewrite Zabs_triangle.
aac_rewrite Zplus_opp_r.
aac_reflexivity.
Qed.
- [Coq-Club] Second release of aac_tactics: a plugin for rewriting modulo associativity and commutativity, Thomas Braibant
Archive powered by MhonArc 2.6.16.