Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

You must be signed in to change notification settings

# coq-community/regexp-Brzozowski

## Folders and files

NameName
Last commit message
Last commit date

# Regexp Brzozowski

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.

## Meta

• Author(s):
• Thierry Coquand (initial)
• Vincent Siles (initial)
• Coq-community maintainer(s):
• Compatible Coq versions: 8.16 or later
• MathComp 2.0.0 or later (`ssreflect` suffices)
• RegLang 1.2.0 or later
• Coq namespace: `RegexpBrzozowski`
• Related publication(s):

## Building and installation instructions

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

## Documentation

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:

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.

Coq formalization of decision procedures for regular expression equivalence [maintainer=@anton-trunov]

## Releases 3

Regexp Brzozowski 1.2 Latest
Oct 14, 2023

•
•
•