This library provides definitions and verified translations between different representations of regular languages: various forms of automata (deterministic, nondeterministic, one-way, two-way), regular expressions, and the logic WS1S. It also contains various decidability results and closure properties of regular languages.
ssreflect
suffices)RegLang
The easiest way to install the latest released version of Regular Language Representations in Coq is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-reglang
To instead build and install manually, do:
git clone https://github.com/coq-community/reglang.git
cd reglang
make # or make -j <number-of-cores-on-your-machine>
make install
To generate HTML documentation, run make coqdoc
and point your browser at docs/coqdoc/toc.html
.
See also the pregenerated HTML documentation for the latest release.
misc.v
, setoid_leq.v
: basic infrastructure independent of regular languageslanguages.v
: languages and decidable languagesdfa.v
:
nfa.v
: Results on nondeterministic one-way automataregexp.v
: Regular expressions and Kleene Theoremminimization.v
: minimization and uniqueness of minimal DFAsmyhill_nerode.v
: classifiers and the constructive Myhill-Nerode theoremtwo_way.v
: deterministic and nondeterministic two-way automatavardi.v
: translation from 2NFAs to NFAs for the complement languageshepherdson.v
: translation from 2NFAs and 2DFAs to DFAs (via classifiers)wmso.v
: