# Algebraic Tools for Binary Relations in Coq

The aim of this project is to provide algebraic tools for reasoning about binary relations in Coq:
• Binary relations have a hierarchy of partial axiomatisations with different properties; the following file illustrates why it may be easier to work with binary relations at this algebraic level.
• Some of these algebraic fragments enjoy decidable equality (semi-lattices, idempotent non-commutative semirings, Kleene algebras), so that we can define tactics to automatically solve the corresponding goals.

## 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

• Fourth release (25th of May, 2011): tar.gz. Compiles with Coq v8.3 (at least pl2 and -r{13766,13769,14149}).
• Third release (25th of October, 2010): tar.gz. Compiles with Coq v8.3 (-r 13566).
• Second release (25th of January, 2010): tar.gz. Compiles with Coq v8.2 "bugfix" (-r 12575 and hopefully the following ones).
• First release (9th of June, 2009): tar.gz. Compiles with Coq v8.2 "bugfix" (-r 12142 and hopefully the following ones).

## Changes

### fourth release:

• Simpler construction for matrices.
• (min,+) model for weighted graphs.
• Alpha-renaming to be consistent with the long version of the article.
• Some benchmarks are included in the archive.

### third release:

• Compiles with Coq v8.3.
• Tactic for "strict Kleene algebras": those without zero element.
• Completely axiom-free: we no longer use the JMeq_eq axiom.
• Use of "positive trees" for sets of positives.
• Reification is now done using OCaml; this produces much smaller proofs.

### second release:

• We switched to positive binary numbers, which required the introduction of a new infrastructure.
• The construction algorithm is no longer Thompson's one; it is no longer implemented using a matricial representation.
• The epsilon removal step is no longer computed algebraically: we prove that our construction returns acyclic epsilon-transitions, so that we can use a linear transitive closure algorithm.
• The determinisation algorithm remained the same, but was re-implemented in a more natural way, thanks to a partial fixpoint operator. (In particular, we no longer need the CoLoR library: termination of the determinisation step no longer requires multiset well-founded orderings.)
• We no longer use minimisation to tests DFAs for equivalence; instead, we implemented Hopcroft and Karp's algorithm, using an efficient disjoint-sets data-structure.
• In case of failure, the tactic now provides a counter-example to the user; the decision procedure was moreover proved complete.

## 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