Algebraic Tools for Binary Relations in Coq

The aim of this project is to provide algebraic tools for reasoning about binary relations in Coq:

Deciding Kleene Algebras

Binary relations form a Kleene Algebra, by considering set-theoretic union, relational composition, and reflexive transitive closure. The main tactic we provide in this library allows one to decide (in)equalities in Kleene algebras; using the initiality theorem proved independently by Kozen and Krob in the early 90's. We rely on Kozen's proof: we implement finite automata algorithms (construction, removing of epsilon-transitions, determinisation, DFA equivalence), and the proof goes by replaying these algorithms in an algebraic way, using matrices.

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 (post-fix) star operation, * is the infix product or concatenation operation, + is the sum or union operation, and 1 is the neutral element.

Papers

We presented this library at the first Coq workshop (August 2009); our methodology is described in the following abstract, which we presented and at ITP (July 2010): An Efficient Coq Tactic for Deciding Kleene Algebras, .pdf. We recently wrote and submitted an extended version (May 2011). Here are slides about our usage of Coq typeclasses for (small) algebraic hierarchies and reification.

Documentation

Downloads

This library is distributed under LGPL 3:

Changes

fourth release:

third release:

second release:

Performances

We performed intensive tests on randomly generated regular expressions. On typical use cases, the tactic runs instantaneously. It runs in less than one second for expressions with 200 internal nodes and 30 variables, and less than one minute for even larger expressions (1000 internal nodes, 100 variables), that are very unlikely to appear in "human-written" proofs. These timings correspond to execution inside Coq; extraction to OCaml approximately results in a speed-up by a factor 20.

We compared our implementation with that from Coquand and Siles, and that from Krauss and Nipkow in Isabelle; here are the regular expressions we used (the raw results are available upon request).

We also compared our approach with the works of Struth, Hoefner, and Dang, who work with automatic theorem provers (ATP). Timings can be found here, the whole benchmark is there.

Matrices

Kozen's initiality proof goes by encoding automata at the algebraic level, using matrices. Therefore, the ATBR library contains a set of definitions and tools about matrices (over semirings or Kleene algebras). In particular, it contains "ring"-like tactics for matrices whose dimensions are not necessarily uniform.

Authors

Thomas Braibant and Damien Pous


Last modified: Tue Dec 6 07:15:05 CET 2011