Algebraic Tools for 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

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

Documentation

• Overall structure of the library, with pointers to the coqdoc generated documentation.
• Simple examples for using the library.
• Other examples: a formalisation of some Church-Rosser theorems.
• The README file from the archive.

Downloads

• 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

Authors