Proposal to move project regexp-Brzozowski to coq-community

[anton-trunov]

Project name: A Decision Procedure for Regular Expression Equivalence in Type Theory (regexp-Brzozowski)

Initial author(s): Thierry Coquand and Vincent Siles (@vsiles)

Current URL: https://github.com/vsiles/regexp-Brzozowski

Kind: pure Coq library

License: MIT (GPL v3 at the time of publication)

Description: A complete formalization of Brzozowski decision procedure based on derivatives of regular expressions, using the MathComp library and the SSReflect proof language. Artifact for a research paper.

Status: not maintained since 2014 (was developed with Coq v8.3 / SSReflect v1.3).

New maintainer: I volunteer to maintain the library. Looking for co-maintainers.

Here is the link to the corresponding issue I opened in the original repo: coq-community/regexp-Brzozowski#2.

[palmskog]

I think we need @chdoc also to comment if/how this should be maintained, since some parts of RegLang are already using definitions from regexp-Brzozowski. We want to avoid a scenario where the same code is double-maintained.

[anton-trunov]

Definitely! Any feedback and suggestions are very welcome.

[chdoc]

IMHO, the overlap between RegLang and this development is so minor (less than 30 lines), that it does not merit any special treatment, in particular not the introduction of a dependency of RegLang on this develoment. This is the relevant comment

(** The definitions of [conc] and [star] as well as the proofs of [starP] and [concP] are taken from from regexp.v in:
Thierry Coquand, Vincent Siles, A Decision Procedure for Regular Expression Equivalence in Type Theory (DOI: 10.1007/978-3-642-25379-9_11). See also: https://github.com/vsiles/regexp-Brzozowski *)

Moreover, I faintly recall someone mentioning that both "atbr" and the tactics from RelationAlgebra (by @damien-pous ) perform better in practice. @anton-trunov , may I inquire as to what is your motivation for reviving this?

[anton-trunov]

My primary interest in reviving the project stems from the fact it is a paper artifact, it's not because I want to use it as a library. It's a pretty big formalization (around 6 kLoC, iirc) and it uses SSReflect, which I'm fond of. So it would be nice to have it around if someone in the future wants to read the paper and play with the source code. We can certainly add a note mentioning the practical merits of this approach compared to others.

[chdoc]

My primary interest in reviving the project stems from the fact it is a paper artifact, it's not because I want to use it as a library.

I agree with your motives. I mainly wanted to ensure that we're all on the same page and that there are no unreasonable expectations. On the other hand, if someone goes through the trouble of reviving this development, then it might be interesting to actually do a performance comparison between the aforementioned three tactics for deciding (in)equalities of regular languages.

[anton-trunov]

it might be interesting to actually do a performance comparison between the aforementioned three tactics for deciding (in)equalities of regular languages.

Indeed, sounds like an interesting project! We should turn your comment into an issue.

[vsiles]

Hi ! Thanks for taking care of that. I don't have a lot of time to manage this project, so I'm grateful 👍
Please ping me if need to do anything at some point in the transfer process.

[anton-trunov]

@vsiles Thank you very much! I've invited you to the coq-community organization, so after you accept the invitation you should be able to transfer the regexp-Brzozowski repository from your account to coq-community. (Just in case: if you click the settings icon in your repo and scroll all the way down you should be able to see the "Transfer" button. Hope this helps.).

[anton-trunov]

I'm closing this issue since the transfer is done. Many thanks to @vsiles for his awesome contribution!

[Zimmi48]

@anton-trunov The description of the repo should probably be edited now that it has been transferred. Currently it says:

Coq files for the formalization of "A Decision Procedure for Regular Expression Equivalence in Type Theory" by Thierry Coquand and myself

[anton-trunov]

@Zimmi48 Good catch, thanks. Fixed.