Jacob Salzberg (Jan 16 2023 at 04:35): Jacob Salzberg (Jan 16 2023 at 04:35):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
Karl Palmskog (Jan 16 2023 at 06:05):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/
Jacob Salzberg (Jan 16 2023 at 07:10):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
Karl Palmskog (Jan 16 2023 at 07:26):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
Karl Palmskog (Jan 16 2023 at 07:29):"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: Apr 19 2024 at 19:02 UTC