initial import

Makefile

@@ -0,0 +1,18 @@
+.PHONY : all coq html website clean
+
+all: coq
+
+html: coq
+	$(MAKE) -C theories html
+
+coq:
+	$(MAKE) -C theories
+
+website: html
+	test -d website || mkdir website
+	cp theories/html/* website/
+	cp extra/*.css extra/*.js website/
+
+clean:
+	$(MAKE) -C theories clean
+	rm -rf website

README.md

@@ -1,2 +1,37 @@
-# coq-reglang
-Regular Language Representations in the Constructive Type Theory of Coq
+# Regular Language Representations in the Constructive Type Theory of Coq #
+
+This repository contains the coq development accompanying the paper: 
+
+[Christian Doczkal](https://perso.ens-lyon.fr/christian.doczkal/) and [Gert Smolka](https://www.ps.uni-saarland.de/~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 
+
+```
+coq-8.7 + mathcomp-1.6.4 (the ssreflect component) or
+coq-8.6 + mathcomp-1.6.1 (the ssreflect component)
+```
+
+## 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

extra/LICENSE.coqdocjs

@@ -0,0 +1,21 @@
+Copyright (c) 2016, Tobias Tebbi
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+    * Redistributions in binary form must reproduce the above copyright
+      notice, this list of conditions and the following disclaimer in the
+      documentation and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDERS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
+ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

extra/config.js

@@ -0,0 +1,72 @@
+var coqdocjs = coqdocjs || {};
+
+coqdocjs.repl = {
+    "forall": "∀",
+    "exists": "∃",
+    "~": "¬",
+    "/\\": "∧",
+    "\\/": "∨",
+    "->": "→",
+    "<-": "←",
+    "<->": "↔",
+    "=>": "⇒",
+    "<>": "≠",
+    "<=": "≤",
+    ">=": "≥",
+    "el": "∈",
+    "nel": "∉",
+    "<<=": "⊆",
+    "|-": "⊢",
+    ">>": "»",
+    "<<": "⊆",
+    "++": "⧺",
+    "===": "≡",
+    "=/=": "≢",
+    "=~=": "≅",
+    "==>": "⟹",
+    "lhd": "⊲",
+    "rhd": "⊳",
+    "nat": "ℕ",
+    // "alpha": "α",
+    // "beta": "β",
+    // "gamma": "γ",
+    // "delta": "δ",
+    // "epsilon": "ε",
+    // "eta": "η",
+    // "iota": "ι",
+    // "kappa": "κ",
+    // "lambda": "λ",
+    // "mu": "μ",
+    // "nu": "ν",
+    // "omega": "ω",
+    // "phi": "ϕ",
+    // "pi": "π",
+    // "psi": "ψ",
+    // "rho": "ρ",
+    // "sigma": "σ",
+    // "tau": "τ",
+    // "theta": "θ",
+    // "xi": "ξ",
+    // "zeta": "ζ",
+    // "Delta": "Δ",
+    // "Gamma": "Γ",
+    // "Pi": "Π",
+    // "Sigma": "Σ",
+    // "Omega": "Ω",
+    // "Xi": "Ξ"
+};
+
+coqdocjs.subscr = {
+  "0" : "₀",
+  "1" : "₁",
+  "2" : "₂",
+  "3" : "₃",
+  "4" : "₄",
+  "5" : "₅",
+  "6" : "₆",
+  "7" : "₇",
+  "8" : "₈",
+  "9" : "₉",
+};
+
+coqdocjs.replInText = ["==>","<=>", "=>", "->", "<-", ":="];

extra/coqdoc.css

@@ -0,0 +1,198 @@
+@import url(https://fonts.googleapis.com/css?family=Open+Sans:400,700);
+
+body{
+    font-family: 'Open Sans', sans-serif;
+    font-size: 14px;
+    color: #2D2D2D
+}
+
+a {
+    text-decoration: none;
+    border-radius: 3px;
+    padding-left: 3px;
+    padding-right: 3px;
+    margin-left: -3px;
+    margin-right: -3px;
+    color: inherit;
+    font-weight: bold;
+}
+
+#main .code a, #main .inlinecode a, #toc a {
+    font-weight: inherit;
+}
+
+a[href]:hover, [clickable]:hover{
+    background-color: rgba(0,0,0,0.1);
+    cursor: pointer;
+}
+
+h, h1, h2, h3, h4, h5 {
+    line-height: 1;
+    color: black;
+    text-rendering: optimizeLegibility;
+    font-weight: normal;
+    letter-spacing: 0.1em;
+    text-align: left;
+}
+
+div + br {
+  display: none;
+}
+
+div:empty{ display: none;}
+
+#main h1 {
+	font-size: 2em;
+}
+
+#main h2 {
+	font-size: 1.667rem;
+}
+
+#main h3 {
+	font-size: 1.333em;
+}
+
+#main h4, #main h5, #main h6 {
+	font-size: 1em;
+}
+
+#toc h2 {
+    padding-bottom: 0;
+}
+
+#main .doc {
+    margin: 0;
+    text-align: justify;
+}
+
+.inlinecode, .code, #main pre {
+    font-family: monospace;
+}
+
+.code > br:first-child {
+  display: none;
+}
+
+.doc + .code{
+  margin-top:0.5em;
+}
+
+.block{
+    display: block;
+    margin-top: 5px;
+    margin-bottom: 5px;
+    padding: 10px;
+    text-align: center;
+}
+
+.block img{
+    margin: 15px;
+}
+
+table.infrule {
+  border: 0px;
+  margin-left: 50px;
+  margin-top: 10px;
+  margin-bottom: 10px;
+}
+
+td.infrule {
+    font-family: "Droid Sans Mono", "DejaVu Sans Mono", monospace;
+    text-align: center;
+    padding: 0;
+    line-height: 1;
+}
+
+tr.infrulemiddle hr {
+    margin: 1px 0 1px 0;
+}
+
+.infrulenamecol {
+    color: rgb(60%,60%,60%);
+    padding-left: 1em;
+    padding-bottom: 0.1em
+}
+
+.id[type="constructor"], .id[type="projection"], .id[type="method"],
+.id[title="constructor"], .id[title="projection"], .id[title="method"]  {
+    color: #A30E16;
+}
+
+.id[type="var"], .id[type="variable"],
+.id[title="var"], .id[title="variable"] {
+    color: inherit;
+}
+
+.id[type="definition"], .id[type="record"], .id[type="class"], .id[type="instance"], .id[type="inductive"], .id[type="library"],
+.id[title="definition"], .id[title="record"], .id[title="class"], .id[title="instance"], .id[title="inductive"], .id[title="library"] {
+    color: #A6650F;
+}
+
+.id[type="lemma"],
+.id[title="lemma"]{
+    color: #188B0C;
+}
+
+.id[type="keyword"], .id[type="notation"], .id[type="abbreviation"],
+.id[title="keyword"], .id[title="notation"], .id[title="abbreviation"]{
+ color : #2874AE;
+}
+
+.comment {
+  color: #808080;
+}
+
+/* TOC */
+
+#toc h2{
+  letter-spacing: 0;
+  font-size: 1.333em;
+}
+
+/* Index */
+
+#index {
+    margin: 0;
+    padding: 0;
+    width: 100%;
+}
+
+#index #frontispiece {
+    margin: 1em auto;
+    padding: 1em;
+    width: 60%;
+}
+
+.booktitle { font-size : 140%  }
+.authors { font-size : 90%;
+	         line-height: 115%;  }
+.moreauthors { font-size : 60%  }
+
+#index #entrance {
+    text-align: center;
+}
+
+#index #entrance .spacer {
+    margin: 0 30px 0 30px;
+}
+
+ul.doclist {
+    margin-top: 0em;
+    margin-bottom: 0em;
+    white-space:nowrap;
+}
+
+#toc > * {
+    clear: both;
+}
+
+#toc > a {
+    display: block;
+    float: left;
+    margin-top: 1em;
+}
+
+#toc a h2{
+    display: inline;
+}