Coq library that formalizes decision procedures for regular expression equivalence, using the Mathematical Components library. The formalization builds on Brzozowski's derivatives of regular expressions for correctness.

• Author(s):
  • Thierry Coquand (initial)
  • Vincent Siles (initial)
• Coq-community maintainer(s):
  • Anton Trunov (@anton-trunov)
• License: MIT License
• Compatible Coq versions: 8.16 or later
• Additional dependencies:
  • MathComp 2.0.0 or later (ssreflect suffices)
  • RegLang 1.2.0 or later
• Coq namespace: RegexpBrzozowski
• Related publication(s):
  • A Decision Procedure for Regular Expression Equivalence in Type Theory doi:10.1007/978-3-642-25379-9_11

The easiest way to install the latest released version of Regexp Brzozowski is via OPAM:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-regexp-brzozowski

To instead build and install manually, do:

git clone https://github.com/coq-community/regexp-Brzozowski.git
cd regexp-Brzozowski
make   # or make -j <number-of-cores-on-your-machine> 
make install

The paper on the formalization was written at Chalmers, in the ForMath Project. More information about the project and its achievements is available on the Chalmers website:

• http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath
• http://wiki.portal.chalmers.se/cse/pmwiki.php/ForMath/PapersAndSlides

Overview of the Coq files:

• glue.v: Basic definitions and lemmas.
• regexp.v: Description and properties of regular expressions.
• gfinset.v: Alternative definition of finite sets.
• finite_der.v: The main proof that the set of derivatives of a regular expression is finite. The proof uses an abstract notion of similarity with the Brzozowski requirements.
• equiv.v: Description of the equivalence procedure and proof of its correctness. In case of non-equivalence, we also produce a witness which is recognized by the first language but not by the second.
• sim1.v: Naive implementation of similarity checking (by double inclusion), with only Brzozowski simplifications.
• sim2.v: More efficient implementation of similarity checking (with a "compilation" of regular expressions) which implements many more simplifications.
• ex.v: A few test cases which allow comparing the decision procedures in sim1.v and sim2.v inside Coq.