The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

(*

Hi all,

We are pleased to announce the first release of ATBR, a Coq library
whose aim is to provide tools for working with various algebraic
structures, including non-commutative idempotent semirings and Kleene
algebras.

The main tactic we provide in this library is a reflexive tactic for
solving (in)equations in Kleene algebras. The decision procedure goes
through standard finite automata constructions, that we formalized.

For example, this tactic automatically solves goals of the form
a#*(b+a#*(1+c))# == (a+b+c)# or a*b*c*a*b*c*a# <= a#*(b*c+a)#, where a,
b, and c are elements of an arbitrary Kleene algebra (binary
relations, regular languages, min-max expressions...), # is the
(postfix) star operation, * is the infix product or concatenation
operation, + is the sum or union operation, and 1 is the neutral
element for *.

In order to define this tactic, we had to work with matrices, so that
the ATBR library also contains a new formalisation of matrices in Coq
along with a set of tools (notably, "ring"-like tactic for matrices
whose dimensions are not necessarily uniform).

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

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


Comments are welcome!

Thomas Braibant & Damien Pous

*)