The Coq Proof Assistant

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.