Awesome
Regular Language Representations in the Constructive Type Theory of Coq
This repository contains the Coq development accompanying the paper:
Christian Doczkal and Gert Smolka, Regular Language Representations in the Constructive Type Theory of Coq, J. Autom. Reason. - Special Issue on Milestones in Interactive Theorem Proving, Springer, 2018.
Prerequisites
One of the following:
- coq-8.9 + mathcomp-1.7.0 (the ssreflect component)
- coq-8.8 + mathcomp-1.7.0 (the ssreflect component)
- coq-8.7 + mathcomp-1.6.4 (the ssreflect component)
- coq-8.6 + mathcomp-1.6.1 (the ssreflect component)
Building and Installation
The easiest way to install the library is via OPAM:
opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-reglang
To instead build and install the library manually, run make
followed by make install
.
HTML Documentation
To generate the HTML documentation, run make website
and point your browser at website/toc.html
Pregenerated HTML documentation (and a pre-print of the paper) can be found at: https://www.ps.uni-saarland.de/extras/RLR-Coq
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