Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Second release of aac_tactics: a plugin for rewriting modulo associativity and commutativity

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.




Archive powered by MhonArc 2.6.16.

Top of Page