Hi all,

I'm trying to do prove some things formally on regexes in research, however I'm running into a bit of a problem...

I was hoping to model them using just inductive types or a fixpoint, but doing either has not allowed me to prove (at least by induction over the matches) that they are deterministic etc etc. Because these are all known facts, I wanted to ask what the state of the art regex libraries are and whether they have eg. closed under negation & intersection, two important ones for me

If anyone here could help me out in this I'd be greatful... Thanks

if you want regex in the sense of regular expressions that express regular languages, the following library might be considered state of the art: https://github.com/coq-community/reglang/

Thank you. It has a lot of nice constructions from the literature etc. I've looked over this one

I'm unfamiliar however with the mathcomp/ssr library. How difficult is it to extend with a proof that regular languages are closed under negation?

Also, I'd want to actually construct the automata matching the input, does this library support that? Thanks

the library provides all the usual automata constructions, but they were designed for easy proof, not to be practically executable. You may want to look at Menhir if you want to actually match input: http://gallium.inria.fr/~fpottier/menhir/manual.html#sec86

"regular language" is defined like this, so all closure properties established for DFAs and regexps apply to regular languages:

```
Definition regular (L : lang char) := { A : dfa | forall x, L x <-> x \in dfa_lang A }.
```

one can also use the specification of regular expressions from the reglang project to prove a Coq matcher function correct (example), or check if regular expressions are equivalent (example)

Last updated: Jun 18 2024 at 22:01 UTC