Regular Language Representations in Coq

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.

Meta

• Author(s):
  • Christian Doczkal (initial)
  • Jan-Oliver Kaiser (initial)
  • Gert Smolka (initial)
• Coq-community maintainer(s):
  • Christian Doczkal (@chdoc)
  • Karl Palmskog (@palmskog)
• License: CeCILL-B
• Compatible Coq versions: 8.16 or later (use releases for other Coq versions)
• Additional dependencies:
  • MathComp 2.0 or later (ssreflect suffices)
  • Hierarchy Builder 1.4.0 or later
• Coq namespace: RegLang
• Related publication(s):
  • Regular Language Representations in the Constructive Type Theory of Coq doi:10.1007/s10817-018-9460-x

Building and installation instructions

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

HTML Documentation

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.

File Contents

• misc.v, setoid_leq.v: basic infrastructure independent of regular languages
• languages.v: languages and decidable languages
• dfa.v:
  • results on deterministic one-way automata
  • definition of regularity
  • criteria for nonregularity
• nfa.v: Results on nondeterministic one-way automata
• regexp.v: Regular expressions and Kleene Theorem
• minimization.v: minimization and uniqueness of minimal DFAs
• myhill_nerode.v: classifiers and the constructive Myhill-Nerode theorem
• two_way.v: deterministic and nondeterministic two-way automata
• vardi.v: translation from 2NFAs to NFAs for the complement language
• shepherdson.v: translation from 2NFAs and 2DFAs to DFAs (via classifiers)
• wmso.v:
  • decidability of WS1S
  • WS1S as representation of regular languages