## A tactic for deciding Kleene algebras

Thomas Braibant and Damien Pous 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 they 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 they 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, they 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 Coq user contribution web-page

In particular, a Coq file illustrating the kind of tools we provide can be found there.