diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..3ad4dea --- /dev/null +++ b/LICENSE @@ -0,0 +1,515 @@ + +CeCILL-B FREE SOFTWARE LICENSE AGREEMENT + + + Notice + +This Agreement is a Free Software license agreement that is the result +of discussions between its authors in order to ensure compliance with +the two main principles guiding its drafting: + + * firstly, compliance with the principles governing the distribution + of Free Software: access to source code, broad rights granted to + users, + * secondly, the election of a governing law, French law, with which + it is conformant, both as regards the law of torts and + intellectual property law, and the protection that it offers to + both authors and holders of the economic rights over software. + +The authors of the CeCILL-B (for Ce[a] C[nrs] I[nria] L[ogiciel] L[ibre]) +license are: + +Commissariat l'Energie Atomique - CEA, a public scientific, technical +and industrial research establishment, having its principal place of +business at 25 rue Leblanc, immeuble Le Ponant D, 75015 Paris, France. + +Centre National de la Recherche Scientifique - CNRS, a public scientific +and technological establishment, having its principal place of business +at 3 rue Michel-Ange, 75794 Paris cedex 16, France. + +Institut National de Recherche en Informatique et en Automatique - +INRIA, a public scientific and technological establishment, having its +principal place of business at Domaine de Voluceau, Rocquencourt, BP +105, 78153 Le Chesnay cedex, France. + + + Preamble + +This Agreement is an open source software license intended to give users +significant freedom to modify and redistribute the software licensed +hereunder. + +The exercising of this freedom is conditional upon a strong obligation +of giving credits for everybody that distributes a software +incorporating a software ruled by the current license so as all +contributions to be properly identified and acknowledged. + +In consideration of access to the source code and the rights to copy, +modify and redistribute granted by the license, users are provided only +with a limited warranty and the software's author, the holder of the +economic rights, and the successive licensors only have limited liability. + +In this respect, the risks associated with loading, using, modifying +and/or developing or reproducing the software by the user are brought to +the user's attention, given its Free Software status, which may make it +complicated to use, with the result that its use is reserved for +developers and experienced professionals having in-depth computer +knowledge. Users are therefore encouraged to load and test the +suitability of the software as regards their requirements in conditions +enabling the security of their systems and/or data to be ensured and, +more generally, to use and operate it in the same conditions of +security. This Agreement may be freely reproduced and published, +provided it is not altered, and that no provisions are either added or +removed herefrom. + +This Agreement may apply to any or all software for which the holder of +the economic rights decides to submit the use thereof to its provisions. + + + Article 1 - DEFINITIONS + +For the purpose of this Agreement, when the following expressions +commence with a capital letter, they shall have the following meaning: + +Agreement: means this license agreement, and its possible subsequent +versions and annexes. + +Software: means the software in its Object Code and/or Source Code form +and, where applicable, its documentation, "as is" when the Licensee +accepts the Agreement. + +Initial Software: means the Software in its Source Code and possibly its +Object Code form and, where applicable, its documentation, "as is" when +it is first distributed under the terms and conditions of the Agreement. + +Modified Software: means the Software modified by at least one +Contribution. + +Source Code: means all the Software's instructions and program lines to +which access is required so as to modify the Software. + +Object Code: means the binary files originating from the compilation of +the Source Code. + +Holder: means the holder(s) of the economic rights over the Initial +Software. + +Licensee: means the Software user(s) having accepted the Agreement. + +Contributor: means a Licensee having made at least one Contribution. + +Licensor: means the Holder, or any other individual or legal entity, who +distributes the Software under the Agreement. + +Contribution: means any or all modifications, corrections, translations, +adaptations and/or new functions integrated into the Software by any or +all Contributors, as well as any or all Internal Modules. + +Module: means a set of sources files including their documentation that +enables supplementary functions or services in addition to those offered +by the Software. + +External Module: means any or all Modules, not derived from the +Software, so that this Module and the Software run in separate address +spaces, with one calling the other when they are run. + +Internal Module: means any or all Module, connected to the Software so +that they both execute in the same address space. + +Parties: mean both the Licensee and the Licensor. + +These expressions may be used both in singular and plural form. + + + Article 2 - PURPOSE + +The purpose of the Agreement is the grant by the Licensor to the +Licensee of a non-exclusive, transferable and worldwide license for the +Software as set forth in Article 5 hereinafter for the whole term of the +protection granted by the rights over said Software. + + + Article 3 - ACCEPTANCE + +3.1 The Licensee shall be deemed as having accepted the terms and +conditions of this Agreement upon the occurrence of the first of the +following events: + + * (i) loading the Software by any or all means, notably, by + downloading from a remote server, or by loading from a physical + medium; + * (ii) the first time the Licensee exercises any of the rights + granted hereunder. + +3.2 One copy of the Agreement, containing a notice relating to the +characteristics of the Software, to the limited warranty, and to the +fact that its use is restricted to experienced users has been provided +to the Licensee prior to its acceptance as set forth in Article 3.1 +hereinabove, and the Licensee hereby acknowledges that it has read and +understood it. + + + Article 4 - EFFECTIVE DATE AND TERM + + + 4.1 EFFECTIVE DATE + +The Agreement shall become effective on the date when it is accepted by +the Licensee as set forth in Article 3.1. + + + 4.2 TERM + +The Agreement shall remain in force for the entire legal term of +protection of the economic rights over the Software. + + + Article 5 - SCOPE OF RIGHTS GRANTED + +The Licensor hereby grants to the Licensee, who accepts, the following +rights over the Software for any or all use, and for the term of the +Agreement, on the basis of the terms and conditions set forth hereinafter. + +Besides, if the Licensor owns or comes to own one or more patents +protecting all or part of the functions of the Software or of its +components, the Licensor undertakes not to enforce the rights granted by +these patents against successive Licensees using, exploiting or +modifying the Software. If these patents are transferred, the Licensor +undertakes to have the transferees subscribe to the obligations set +forth in this paragraph. + + + 5.1 RIGHT OF USE + +The Licensee is authorized to use the Software, without any limitation +as to its fields of application, with it being hereinafter specified +that this comprises: + + 1. permanent or temporary reproduction of all or part of the Software + by any or all means and in any or all form. + + 2. loading, displaying, running, or storing the Software on any or + all medium. + + 3. entitlement to observe, study or test its operation so as to + determine the ideas and principles behind any or all constituent + elements of said Software. This shall apply when the Licensee + carries out any or all loading, displaying, running, transmission + or storage operation as regards the Software, that it is entitled + to carry out hereunder. + + + 5.2 ENTITLEMENT TO MAKE CONTRIBUTIONS + +The right to make Contributions includes the right to translate, adapt, +arrange, or make any or all modifications to the Software, and the right +to reproduce the resulting software. + +The Licensee is authorized to make any or all Contributions to the +Software provided that it includes an explicit notice that it is the +author of said Contribution and indicates the date of the creation thereof. + + + 5.3 RIGHT OF DISTRIBUTION + +In particular, the right of distribution includes the right to publish, +transmit and communicate the Software to the general public on any or +all medium, and by any or all means, and the right to market, either in +consideration of a fee, or free of charge, one or more copies of the +Software by any means. + +The Licensee is further authorized to distribute copies of the modified +or unmodified Software to third parties according to the terms and +conditions set forth hereinafter. + + + 5.3.1 DISTRIBUTION OF SOFTWARE WITHOUT MODIFICATION + +The Licensee is authorized to distribute true copies of the Software in +Source Code or Object Code form, provided that said distribution +complies with all the provisions of the Agreement and is accompanied by: + + 1. a copy of the Agreement, + + 2. a notice relating to the limitation of both the Licensor's + warranty and liability as set forth in Articles 8 and 9, + +and that, in the event that only the Object Code of the Software is +redistributed, the Licensee allows effective access to the full Source +Code of the Software at a minimum during the entire period of its +distribution of the Software, it being understood that the additional +cost of acquiring the Source Code shall not exceed the cost of +transferring the data. + + + 5.3.2 DISTRIBUTION OF MODIFIED SOFTWARE + +If the Licensee makes any Contribution to the Software, the resulting +Modified Software may be distributed under a license agreement other +than this Agreement subject to compliance with the provisions of Article +5.3.4. + + + 5.3.3 DISTRIBUTION OF EXTERNAL MODULES + +When the Licensee has developed an External Module, the terms and +conditions of this Agreement do not apply to said External Module, that +may be distributed under a separate license agreement. + + + 5.3.4 CREDITS + +Any Licensee who may distribute a Modified Software hereby expressly +agrees to: + + 1. indicate in the related documentation that it is based on the + Software licensed hereunder, and reproduce the intellectual + property notice for the Software, + + 2. ensure that written indications of the Software intended use, + intellectual property notice and license hereunder are included in + easily accessible format from the Modified Software interface, + + 3. mention, on a freely accessible website describing the Modified + Software, at least throughout the distribution term thereof, that + it is based on the Software licensed hereunder, and reproduce the + Software intellectual property notice, + + 4. where it is distributed to a third party that may distribute a + Modified Software without having to make its source code + available, make its best efforts to ensure that said third party + agrees to comply with the obligations set forth in this Article . + +If the Software, whether or not modified, is distributed with an +External Module designed for use in connection with the Software, the +Licensee shall submit said External Module to the foregoing obligations. + + + 5.3.5 COMPATIBILITY WITH THE CeCILL AND CeCILL-C LICENSES + +Where a Modified Software contains a Contribution subject to the CeCILL +license, the provisions set forth in Article 5.3.4 shall be optional. + +A Modified Software may be distributed under the CeCILL-C license. In +such a case the provisions set forth in Article 5.3.4 shall be optional. + + + Article 6 - INTELLECTUAL PROPERTY + + + 6.1 OVER THE INITIAL SOFTWARE + +The Holder owns the economic rights over the Initial Software. Any or +all use of the Initial Software is subject to compliance with the terms +and conditions under which the Holder has elected to distribute its work +and no one shall be entitled to modify the terms and conditions for the +distribution of said Initial Software. + +The Holder undertakes that the Initial Software will remain ruled at +least by this Agreement, for the duration set forth in Article 4.2. + + + 6.2 OVER THE CONTRIBUTIONS + +The Licensee who develops a Contribution is the owner of the +intellectual property rights over this Contribution as defined by +applicable law. + + + 6.3 OVER THE EXTERNAL MODULES + +The Licensee who develops an External Module is the owner of the +intellectual property rights over this External Module as defined by +applicable law and is free to choose the type of agreement that shall +govern its distribution. + + + 6.4 JOINT PROVISIONS + +The Licensee expressly undertakes: + + 1. not to remove, or modify, in any manner, the intellectual property + notices attached to the Software; + + 2. to reproduce said notices, in an identical manner, in the copies + of the Software modified or not. + +The Licensee undertakes not to directly or indirectly infringe the +intellectual property rights of the Holder and/or Contributors on the +Software and to take, where applicable, vis--vis its staff, any and all +measures required to ensure respect of said intellectual property rights +of the Holder and/or Contributors. + + + Article 7 - RELATED SERVICES + +7.1 Under no circumstances shall the Agreement oblige the Licensor to +provide technical assistance or maintenance services for the Software. + +However, the Licensor is entitled to offer this type of services. The +terms and conditions of such technical assistance, and/or such +maintenance, shall be set forth in a separate instrument. Only the +Licensor offering said maintenance and/or technical assistance services +shall incur liability therefor. + +7.2 Similarly, any Licensor is entitled to offer to its licensees, under +its sole responsibility, a warranty, that shall only be binding upon +itself, for the redistribution of the Software and/or the Modified +Software, under terms and conditions that it is free to decide. Said +warranty, and the financial terms and conditions of its application, +shall be subject of a separate instrument executed between the Licensor +and the Licensee. + + + Article 8 - LIABILITY + +8.1 Subject to the provisions of Article 8.2, the Licensee shall be +entitled to claim compensation for any direct loss it may have suffered +from the Software as a result of a fault on the part of the relevant +Licensor, subject to providing evidence thereof. + +8.2 The Licensor's liability is limited to the commitments made under +this Agreement and shall not be incurred as a result of in particular: +(i) loss due the Licensee's total or partial failure to fulfill its +obligations, (ii) direct or consequential loss that is suffered by the +Licensee due to the use or performance of the Software, and (iii) more +generally, any consequential loss. In particular the Parties expressly +agree that any or all pecuniary or business loss (i.e. loss of data, +loss of profits, operating loss, loss of customers or orders, +opportunity cost, any disturbance to business activities) or any or all +legal proceedings instituted against the Licensee by a third party, +shall constitute consequential loss and shall not provide entitlement to +any or all compensation from the Licensor. + + + Article 9 - WARRANTY + +9.1 The Licensee acknowledges that the scientific and technical +state-of-the-art when the Software was distributed did not enable all +possible uses to be tested and verified, nor for the presence of +possible defects to be detected. In this respect, the Licensee's +attention has been drawn to the risks associated with loading, using, +modifying and/or developing and reproducing the Software which are +reserved for experienced users. + +The Licensee shall be responsible for verifying, by any or all means, +the suitability of the product for its requirements, its good working +order, and for ensuring that it shall not cause damage to either persons +or properties. + +9.2 The Licensor hereby represents, in good faith, that it is entitled +to grant all the rights over the Software (including in particular the +rights set forth in Article 5). + +9.3 The Licensee acknowledges that the Software is supplied "as is" by +the Licensor without any other express or tacit warranty, other than +that provided for in Article 9.2 and, in particular, without any warranty +as to its commercial value, its secured, safe, innovative or relevant +nature. + +Specifically, the Licensor does not warrant that the Software is free +from any error, that it will operate without interruption, that it will +be compatible with the Licensee's own equipment and software +configuration, nor that it will meet the Licensee's requirements. + +9.4 The Licensor does not either expressly or tacitly warrant that the +Software does not infringe any third party intellectual property right +relating to a patent, software or any other property right. Therefore, +the Licensor disclaims any and all liability towards the Licensee +arising out of any or all proceedings for infringement that may be +instituted in respect of the use, modification and redistribution of the +Software. Nevertheless, should such proceedings be instituted against +the Licensee, the Licensor shall provide it with technical and legal +assistance for its defense. Such technical and legal assistance shall be +decided on a case-by-case basis between the relevant Licensor and the +Licensee pursuant to a memorandum of understanding. The Licensor +disclaims any and all liability as regards the Licensee's use of the +name of the Software. No warranty is given as regards the existence of +prior rights over the name of the Software or as regards the existence +of a trademark. + + + Article 10 - TERMINATION + +10.1 In the event of a breach by the Licensee of its obligations +hereunder, the Licensor may automatically terminate this Agreement +thirty (30) days after notice has been sent to the Licensee and has +remained ineffective. + +10.2 A Licensee whose Agreement is terminated shall no longer be +authorized to use, modify or distribute the Software. However, any +licenses that it may have granted prior to termination of the Agreement +shall remain valid subject to their having been granted in compliance +with the terms and conditions hereof. + + + Article 11 - MISCELLANEOUS + + + 11.1 EXCUSABLE EVENTS + +Neither Party shall be liable for any or all delay, or failure to +perform the Agreement, that may be attributable to an event of force +majeure, an act of God or an outside cause, such as defective +functioning or interruptions of the electricity or telecommunications +networks, network paralysis following a virus attack, intervention by +government authorities, natural disasters, water damage, earthquakes, +fire, explosions, strikes and labor unrest, war, etc. + +11.2 Any failure by either Party, on one or more occasions, to invoke +one or more of the provisions hereof, shall under no circumstances be +interpreted as being a waiver by the interested Party of its right to +invoke said provision(s) subsequently. + +11.3 The Agreement cancels and replaces any or all previous agreements, +whether written or oral, between the Parties and having the same +purpose, and constitutes the entirety of the agreement between said +Parties concerning said purpose. No supplement or modification to the +terms and conditions hereof shall be effective as between the Parties +unless it is made in writing and signed by their duly authorized +representatives. + +11.4 In the event that one or more of the provisions hereof were to +conflict with a current or future applicable act or legislative text, +said act or legislative text shall prevail, and the Parties shall make +the necessary amendments so as to comply with said act or legislative +text. All other provisions shall remain effective. Similarly, invalidity +of a provision of the Agreement, for any reason whatsoever, shall not +cause the Agreement as a whole to be invalid. + + + 11.5 LANGUAGE + +The Agreement is drafted in both French and English and both versions +are deemed authentic. + + + Article 12 - NEW VERSIONS OF THE AGREEMENT + +12.1 Any person is authorized to duplicate and distribute copies of this +Agreement. + +12.2 So as to ensure coherence, the wording of this Agreement is +protected and may only be modified by the authors of the License, who +reserve the right to periodically publish updates or new versions of the +Agreement, each with a separate number. These subsequent versions may +address new issues encountered by Free Software. + +12.3 Any Software distributed under a given version of the Agreement may +only be subsequently distributed under the same version of the Agreement +or a subsequent version. + + + Article 13 - GOVERNING LAW AND JURISDICTION + +13.1 The Agreement is governed by French law. The Parties agree to +endeavor to seek an amicable solution to any disagreements or disputes +that may arise during the performance of the Agreement. + +13.2 Failing an amicable solution within two (2) months as from their +occurrence, and unless emergency proceedings are necessary, the +disagreements or disputes shall be referred to the Paris Courts having +jurisdiction, by the more diligent Party. + + +Version 1.0 dated 2006-09-05. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..d24e590 --- /dev/null +++ b/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 diff --git a/README.md b/README.md index 588234d..731ba16 100644 --- a/README.md +++ b/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 diff --git a/extra/LICENSE.coqdocjs b/extra/LICENSE.coqdocjs new file mode 100644 index 0000000..9cc94e5 --- /dev/null +++ b/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. diff --git a/extra/config.js b/extra/config.js new file mode 100644 index 0000000..00cd0fa --- /dev/null +++ b/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 = ["==>","<=>", "=>", "->", "<-", ":="]; diff --git a/extra/coqdoc.css b/extra/coqdoc.css new file mode 100644 index 0000000..2512a5a --- /dev/null +++ b/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; +} diff --git a/extra/coqdocjs.css b/extra/coqdocjs.css new file mode 100644 index 0000000..5303ec2 --- /dev/null +++ b/extra/coqdocjs.css @@ -0,0 +1,245 @@ +/* replace unicode */ + +.id[repl] .hidden { + font-size: 0; +} + +.id[repl]:before{ + content: attr(repl); +} + +/* folding proofs */ + +@keyframes show-proof { + 0% { + max-height: 1.2em; + opacity: 1; + } + 99% { + max-height: 1000em; + } + 100%{ + } +} + +@keyframes hide-proof { + from { + visibility: visible; + max-height: 10em; + opacity: 1; + } + to { + max-height: 1.2em; + } +} + +.proof { + cursor: pointer; +} +.proof * { + cursor: pointer; +} + +.proof { + overflow: hidden; + position: relative; + display: inline-block; +} + +.proof[show="false"] { + max-height: 1.2em; + visibility: hidden; + opacity: 0; +} + +.proof[show="false"][animate] { + animation-name: hide-proof; + animation-duration: 0.25s; +} + +.proof[show=true] { + animation-name: show-proof; + animation-duration: 10s; +} + +.proof[show="false"]:before { + position: absolute; + visibility: visible; + width: 100%; + height: 100%; + display: block; + opacity: 0; + content: "M"; +} +.proof[show="false"]:hover:before { + content: ""; +} + +.proof[show="false"] + br + br { + display: none; +} + +.proof[show="false"]:hover { + visibility: visible; + opacity: 0.5; +} + +#toggle-proofs[proof-status="no-proofs"] { + display: none; +} + +#toggle-proofs[proof-status="some-hidden"]:before { + content: "Show Proofs"; +} + +#toggle-proofs[proof-status="all-shown"]:before { + content: "Hide Proofs"; +} + + +/* page layout */ + +html, body { + height: 100%; + margin:0; + padding:0; +} + +body { + display: flex; + flex-direction: column +} + +#content { + flex: 1; + overflow: auto; + display: flex; + flex-direction: column; +} +#content:focus { + outline: none; /* prevent glow in OS X */ +} + +#main { + display: block; + padding: 16px; + padding-top: 1em; + padding-bottom: 2em; + margin-left: auto; + margin-right: auto; + max-width: 60em; + flex: 1 0 auto; +} + +.libtitle { + display: none; +} + +/* header */ +#header { + width:100%; + padding: 0; + margin: 0; + display: flex; + align-items: center; + background-color: rgb(21,57,105); + color: white; + font-weight: bold; + overflow: hidden; +} + + +.button { + cursor: pointer; +} + +#header * { + text-decoration: none; + vertical-align: middle; + margin-left: 15px; + margin-right: 15px; +} + +#header > .right, #header > .left { + display: flex; + flex: 1; + align-items: center; +} +#header > .left { + text-align: left; +} +#header > .right { + flex-direction: row-reverse; +} + +#header a, #header .button { + color: white; + box-sizing: border-box; +} + +#header a { + border-radius: 0; + padding: 0.2em; +} + +#header .button { + background-color: rgb(63, 103, 156); + border-radius: 1em; + padding-left: 0.5em; + padding-right: 0.5em; + margin: 0.2em; +} + +#header a:hover, #header .button:hover { + background-color: rgb(181, 213, 255); + color: black; +} + +#header h1 { padding: 0; + margin: 0;} + +/* footer */ +#footer { + text-align: center; + opacity: 0.5; + font-size: 75%; +} + +/* hyperlinks */ + +@keyframes highlight { + 50%{ + background-color: black; + } +} + +:target * { + animation-name: highlight; + animation-duration: 1s; +} + +a[name]:empty { + float: right; +} + +/* Proviola */ + +div.code { + width: auto; + float: none; +} + +div.goal { + position: fixed; + left: 75%; + width: 25%; + top: 3em; +} + +div.doc { + clear: both; +} + +span.command:hover { + background-color: inherit; +} diff --git a/extra/coqdocjs.js b/extra/coqdocjs.js new file mode 100644 index 0000000..9d9fec1 --- /dev/null +++ b/extra/coqdocjs.js @@ -0,0 +1,184 @@ +var coqdocjs = coqdocjs || {}; +(function(){ + +function replace(s){ + var m; + if (m = s.match(/^(.+)'/)) { + return replace(m[1])+"'"; + } else if (m = s.match(/^([A-Za-z]+)_?(\d+)$/)) { + return replace(m[1])+m[2].replace(/\d/g, function(d){return coqdocjs.subscr[d]}); + } else if (coqdocjs.repl.hasOwnProperty(s)){ + return coqdocjs.repl[s] + } else { + return s; + } +} + +function toArray(nl){ + return Array.prototype.slice.call(nl); +} + +function replInTextNodes() { + coqdocjs.replInText.forEach(function(toReplace){ + toArray(document.getElementsByClassName("code")).concat(toArray(document.getElementsByClassName("inlinecode"))).forEach(function(elem){ + toArray(elem.childNodes).forEach(function(node){ + if (node.nodeType != Node.TEXT_NODE) return; + var fragments = node.textContent.split(toReplace); + node.textContent = fragments[fragments.length-1]; + for (var k = 0; k < fragments.length - 1; ++k) { + node.parentNode.insertBefore(document.createTextNode(fragments[k]),node); + var replacement = document.createElement("span"); + replacement.appendChild(document.createTextNode(toReplace)); + replacement.setAttribute("class", "id"); + replacement.setAttribute("type", "keyword"); + node.parentNode.insertBefore(replacement, node); + } + }); + }); + }); +} + +function replNodes() { + toArray(document.getElementsByClassName("id")).forEach(function(node){ + if (["var", "variable", "keyword", "notation", "definition", "inductive"].indexOf(node.getAttribute("type"))>=0){ + var text = node.textContent; + var replText = replace(text); + if(text != replText) { + node.setAttribute("repl", replText); + node.setAttribute("title", text); + var hidden = document.createElement("span"); + hidden.setAttribute("class", "hidden"); + while (node.firstChild) { + hidden.appendChild(node.firstChild); + } + node.appendChild(hidden); + } + } + }); +} + +function isVernacStart(l, t){ + t = t.trim(); + for(var s of l){ + if (t == s || t.startsWith(s+" ") || t.startsWith(s+".")){ + return true; + } + } + return false; +} + +function isProofStart(s){ + return isVernacStart(["Proof"], s); +} + +function isProofEnd(s){ + return isVernacStart(["Qed", "Admitted", "Defined"], s); +} + +function proofStatus(){ + var proofs = toArray(document.getElementsByClassName("proof")); + if(proofs.length) { + for(var proof of proofs) { + if (proof.getAttribute("show") === "false") { + return "some-hidden"; + } + } + return "all-shown"; + } + else { + return "no-proofs"; + } +} + +function updateView(){ + document.getElementById("toggle-proofs").setAttribute("proof-status", proofStatus()); +} + +function foldProofs() { + var hasCommands = true; + var nodes = document.getElementsByClassName("command"); + if(nodes.length == 0) { + hasCommands = false; + console.log("no command tags found") + nodes = document.getElementsByClassName("id"); + } + toArray(nodes).forEach(function(node){ + if(isProofStart(node.textContent)) { + var proof = document.createElement("span"); + proof.setAttribute("class", "proof"); + + node.parentNode.insertBefore(proof, node); + if(proof.previousSibling.nodeType === Node.TEXT_NODE) + proof.appendChild(proof.previousSibling); + while(node && !isProofEnd(node.textContent)) { + proof.appendChild(node); + node = proof.nextSibling; + } + if (proof.nextSibling) proof.appendChild(proof.nextSibling); // the Qed + if (!hasCommands && proof.nextSibling) proof.appendChild(proof.nextSibling); // the dot after the Qed + + proof.addEventListener("click", function(proof){return function(e){ + if (e.target.parentNode.tagName.toLowerCase() === "a") + return; + proof.setAttribute("show", proof.getAttribute("show") === "true" ? "false" : "true"); + proof.setAttribute("animate", ""); + updateView(); + };}(proof)); + proof.setAttribute("show", "false"); + } + }); +} + +function toggleProofs(){ + var someProofsHidden = proofStatus() === "some-hidden"; + toArray(document.getElementsByClassName("proof")).forEach(function(proof){ + proof.setAttribute("show", someProofsHidden); + proof.setAttribute("animate", ""); + }); + updateView(); +} + +function repairDom(){ + // pull whitespace out of command + toArray(document.getElementsByClassName("command")).forEach(function(node){ + while(node.firstChild && node.firstChild.textContent.trim() == ""){ + console.log("try move"); + node.parentNode.insertBefore(node.firstChild, node); + } + }); + toArray(document.getElementsByClassName("id")).forEach(function(node){ + node.setAttribute("type", node.getAttribute("title")); + }); + toArray(document.getElementsByClassName("idref")).forEach(function(ref){ + toArray(ref.childNodes).forEach(function(child){ + if (["var", "variable"].indexOf(child.getAttribute("type")) > -1) + ref.removeAttribute("href"); + }); + }); + +} + +function fixTitle(){ + var url = "/" + window.location.pathname; + var modulename = "." + url.substring(url.lastIndexOf('/')+1, url.lastIndexOf('.')); + modulename = modulename.substring(modulename.lastIndexOf('.')+1); + if (modulename === "toc") {modulename = "Table of Contents";} + else if (modulename === "indexpage") {modulename = "Index";} + else {modulename = modulename + ".v";}; + document.title = modulename; +} + +function postprocess(){ + repairDom(); + replInTextNodes() + replNodes(); + foldProofs(); + document.getElementById("toggle-proofs").addEventListener("click", toggleProofs); + updateView(); +} + +fixTitle(); +document.addEventListener('DOMContentLoaded', postprocess); + +coqdocjs.toggleProofs = toggleProofs; +})(); diff --git a/extra/footer.html b/extra/footer.html new file mode 100644 index 0000000..d0f79a8 --- /dev/null +++ b/extra/footer.html @@ -0,0 +1,8 @@ + + + + + + diff --git a/extra/header.html b/extra/header.html new file mode 100644 index 0000000..cc81721 --- /dev/null +++ b/extra/header.html @@ -0,0 +1,27 @@ + + + + + + + + + + + + + +
+
diff --git a/theories/Makefile b/theories/Makefile new file mode 100644 index 0000000..d8fc725 --- /dev/null +++ b/theories/Makefile @@ -0,0 +1,16 @@ +COQVERSION=$(shell coqc -v | grep version | cut -d' ' -f 6 ) + +all: Makefile.coq + +make -f Makefile.coq all + +html: Makefile.coq + +make -f Makefile.coq html + +clean: Makefile.coq + +make -f Makefile.coq clean + rm -f Makefile.coq + +Makefile.coq: _CoqProject + coq_makefile -f _CoqProject -arg -w -arg -notation-overridden -o Makefile.coq + +.PHONY: all html gallinahtml clean diff --git a/theories/_CoqProject b/theories/_CoqProject new file mode 100644 index 0000000..50fe693 --- /dev/null +++ b/theories/_CoqProject @@ -0,0 +1,16 @@ +-R . RegLang +-install none +COQDOCFLAGS = "-R . RegLang -s --external 'http://math-comp.github.io/math-comp/htmldoc/' mathcomp \ +--with-header ../extra/header.html --with-footer ../extra/footer.html --index indexpage --parse-comments" +misc.v +setoid_leq.v +languages.v +dfa.v +nfa.v +regexp.v +minimization.v +myhill_nerode.v +two_way.v +vardi.v +shepherdson.v +wmso.v diff --git a/theories/dfa.v b/theories/dfa.v new file mode 100644 index 0000000..fa27dd7 --- /dev/null +++ b/theories/dfa.v @@ -0,0 +1,525 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages. + +Set Implicit Arguments. +Unset Printing Implicit Defensive. +Unset Strict Implicit. + +Section FA. +Variable char : finType. +Local Notation word := (word char). + +(** * Deterministic Finite Automata *) + +Record dfa : Type := { + dfa_state :> finType; + dfa_s : dfa_state; + dfa_fin : {set dfa_state}; + dfa_trans : dfa_state -> char -> dfa_state }. + +(* Arguments dfa_fin d _ : clear implicits. *) + +(** We define acceptance for every state of a DFA. The language of a +DFA is then just the language of the starting state. *) + +Section DFA_Acceptance. +Variable A : dfa. +Implicit Types (p q : A) (x y : word). + +Fixpoint delta (p : A) x := + if x is a :: x' then delta (dfa_trans p a) x' else p. + +Lemma delta_cons p a x : delta (dfa_trans p a) x = delta p (a :: x). +Proof. by []. Qed. + +Lemma delta_cat p x y : delta p (x ++ y) = delta (delta p x) y. +Proof. elim: x p => // a x /= IH p. by rewrite IH. Qed. + +Definition dfa_accept (p : A) x := delta p x \in dfa_fin A. + +Definition delta_s w := delta (dfa_s A) w. +Definition dfa_lang := [pred x | dfa_accept (dfa_s A) x]. + +Lemma accept_nil p : dfa_accept p [::] = (p \in dfa_fin A). +Proof. by []. Qed. + +Lemma accept_cons (x : A) a w : + dfa_accept x (a :: w) = dfa_accept (dfa_trans x a) w. +Proof. by []. Qed. + +Lemma delta_lang x : (delta_s x \in dfa_fin A) = (x \in dfa_lang). +Proof. by []. Qed. + +Definition accE := (accept_nil,accept_cons). + +End DFA_Acceptance. + +(** ** Regularity + +We formalize the notion of regularity as the type of DFAs accpepting +the language under consideration. This allows closure properties to be +used for the construction of translation functions. Where required, +the propositional variant of regularity is obtained as [inhabited (regular L)]. *) + +Definition regular (L : lang char) := { A : dfa | forall x, L x <-> x \in dfa_lang A }. + +Lemma regular_ext L1 L2 : regular L2 -> L1 =p L2 -> regular L1. +Proof. case => A HA B. exists A => w. by rewrite B. Qed. + +(** ** Operations on DFAs + +To prepare the translation from regular expresstions to DFAs, we show +that finite automata are closed under all regular operations. We build +the primitive automata, complement and boolean combinations using +DFAs. *) + +Definition dfa_void := + {| dfa_s := tt; dfa_fin := set0 ; dfa_trans x a := tt |}. + +Lemma dfa_void_correct (x: dfa_void) w: ~~ dfa_accept x w. +Proof. by rewrite /dfa_accept inE. Qed. + +Section DFAOps. + +Variable op : bool -> bool -> bool. +Variable A1 A2 : dfa. + +(** Complement automaton **) +Definition dfa_compl := + {| dfa_s := dfa_s A1; + dfa_fin := ~: (dfa_fin A1); + dfa_trans := (@dfa_trans A1) |}. + +Lemma dfa_compl_correct w : + w \in dfa_lang dfa_compl = (w \notin dfa_lang A1). +Proof. + rewrite /dfa_lang !inE {2}/dfa_compl /=. + by rewrite /dfa_accept inE. +Qed. + +(** BinOp Automaton *) + +Definition dfa_op := + {| dfa_s := (dfa_s A1, dfa_s A2); + dfa_fin := [set q | op (q.1 \in dfa_fin A1) (q.2 \in dfa_fin A2)]; + dfa_trans x a := (dfa_trans x.1 a, dfa_trans x.2 a) |}. + +Lemma dfa_op_correct w : + w \in dfa_lang dfa_op = op (w \in dfa_lang A1) (w \in dfa_lang A2). +Proof. + rewrite !inE {2}/dfa_op /=. + elim: w (dfa_s A1) (dfa_s A2) => [| a w IHw] x y; by rewrite !accE ?inE /=. +Qed. + +Definition dfa0 := {| dfa_s := tt; dfa_trans q a := tt; dfa_fin := set0 |}. + +Lemma dfa0_correct x : x \in dfa_lang dfa0 = false. +Proof. by rewrite -delta_lang inE. Qed. + +End DFAOps. + +Lemma regular_inter (L1 L2 : lang char) : + regular L1 -> regular L2 -> regular (fun x => L1 x /\ L2 x). +Proof. + move => [A LA] [B LB]. exists (dfa_op andb A B) => x. + by rewrite dfa_op_correct LA LB (rwP andP). +Qed. + +Lemma regular0 : regular (fun _ : word => False). +Proof. exists (dfa0) => x. by rewrite dfa0_correct. Qed. + +Lemma regularU (L1 L2 : lang char) : + regular L1 -> regular L2 -> regular (fun x => L1 x \/ L2 x). +Proof. + move => [A1 acc_L1] [A2 acc_L2]. exists (dfa_op orb A1 A2) => x. + by rewrite dfa_op_correct -(rwP orP) -acc_L1 -acc_L2. +Qed. + +Lemma regular_bigU (T : eqType) (L : T -> lang char) (s : seq T) : + (forall a, a \in s -> regular (L a)) -> regular (fun x => exists2 a, a \in s & L a x). +Proof. + elim: s => //. + - move => _. apply: regular_ext regular0 _. by split => // [[a]]. + - move => a s IH /all1sT [H1 H2]. + pose L' := (fun x => L a x \/ (fun x : word => exists2 a : T, a \in s & L a x) x). + apply: (regular_ext (L2 := L')); first by apply: regularU => //; exact: IH. + move => x. rewrite /L'. exact: ex1s. +Qed. + + + +(** ** Cut-Off Criterion *) + +Section CutOff. + Variables (aT rT : finType) (f : seq aT -> rT). + Hypothesis RC_f : forall x y a, f x = f y -> f (x++[::a]) = f (y++[::a]). + + Lemma RC_seq x y z : f x = f y -> f (x++z) = f (y++z). + Proof. + elim: z x y => [|a z IHz] x y; first by rewrite !cats0. + rewrite -(cat1s a) (catA x [::a]) (catA y [::a]). move/(RC_f a). exact: IHz. + Qed. + + Lemma RC_rep x (i j : 'I_(size x)) : + i < j -> f (take i x) = f (take j x) -> f (take i x ++ drop j x) = f x. + Proof. move => Hij Hfij. rewrite -{5}(cat_take_drop j x). exact: RC_seq. Qed. + + + Definition exseqb (p : pred rT) := + [exists n : 'I_#|rT|.+1, exists x : n.-tuple aT, p (f x)]. + + Lemma exseqP (p : pred rT) : reflect (exists x, p (f x)) (exseqb p). + Proof. + apply: (iffP idP); last case. + - case/existsP => n. case/existsP => x Hx. by exists x. + - apply: (size_induction (measure := size)) => x IHx px. + case H: (size x < #|rT|.+1). + + apply/existsP. exists (Ordinal H). apply/existsP. by exists (in_tuple x). + + have: ~ injective (fun i : 'I_(size x) => f (take i x)). + { move/card_leq_inj. by rewrite -ltnS /= card_ord H. } + move/injectiveP/injectivePn => [i [j]] Hij. + wlog ltn_ij : i j {Hij} / i < j => [W|] E. + { move: Hij. rewrite neq_ltn. case/orP => l; exact: W l _. } + apply: (IHx (take i x ++ drop j x)); last by rewrite RC_rep. + by rewrite size_cat size_take size_drop ltn_ord -ltn_subRL ltn_sub2l. + Qed. + + Lemma exseq_dec (p : pred rT) : decidable (exists x, p (f x)). + Proof. apply: decP. exact: exseqP. Qed. + + Lemma allseq_dec (p : pred rT) : decidable (forall x, p (f x)). + Proof. + case: (exseq_dec (predC p)) => H;[right|left]. + - move => A. case: H => [x /= Hx]. by rewrite A in Hx. + - move => x. apply/negPn/negP => C. apply: H. by exists x. + Qed. + + (** Construction of Image *) + + Definition image_type := { a : rT | exseq_dec (pred1 a) }. + + Lemma image_fun_proof (x : seq aT) : exseq_dec (pred1 (f x)). + Proof. apply/dec_eq. by exists x => /=. Qed. + + Definition image_fun (x : seq aT) : image_type := Sub (f x) (image_fun_proof x). + + Lemma surjective_image_fun : surjective (image_fun). + Proof. move => [y Py]. case/dec_eq : (Py) => /= x ?. by exists x. Qed. + +End CutOff. + +(** ** Decidability of Language Equivalence + +Language emptiness and inhabitation of DFAs is deciadable since the [delta] +function is right congruent *) + +Section Emptyness. + Variable A : dfa. + + Lemma delta_rc x y a : let s := dfa_s A in + delta s x = delta s y -> delta s (x ++ [::a]) = delta s (y ++ [::a]). + Proof. by rewrite /= !delta_cat => <-. Qed. + + Definition dfa_inhab : decidable (exists x, x \in dfa_lang A) := + exseq_dec delta_rc (fun x => x \in dfa_fin A). + + Lemma dfa_inhabP : reflect (exists x, x \in dfa_lang A) (dfa_inhab). + Proof. apply: (iffP idP); by rewrite dec_eq. Qed. + + Definition dfa_empty := allseq_dec delta_rc (fun x => x \notin dfa_fin A). + + Lemma dfa_emptyP : reflect (dfa_lang A =i pred0) (dfa_empty). + Proof. + apply: (iffP idP) => [/dec_eq H x|H]; first by rewrite inE /dfa_accept (negbTE (H _)). + apply/dec_eq => x. by rewrite -[_ \notin _]/(x \notin dfa_lang A) H. + Qed. +End Emptyness. + +(** The problem of deciding language eqivalence reduces to the problem +of deciding emptiness of [A [+] B] *) + +Definition dfa_equiv A1 A2 := dfa_empty (dfa_op addb A1 A2). + +Lemma dfa_equiv_correct A1 A2 : + reflect (dfa_lang A1 =i dfa_lang A2) (dfa_equiv A1 A2). +Proof. + apply: (iffP (dfa_emptyP _)) => H w. + - move/negbT: (H w). rewrite !dfa_op_correct -addNb. + move/addbP. by rewrite negbK. + - apply/negbTE. by rewrite !dfa_op_correct H addbb. +Qed. + +Definition dfa_incl A1 A2 := dfa_empty (dfa_op (fun a b => a && ~~ b) A1 A2). + +Lemma dfa_incl_correct A1 A2 : + reflect {subset dfa_lang A1 <= dfa_lang A2} (dfa_incl A1 A2). +Proof. + apply: (iffP (dfa_emptyP _)) => H w. + - move/negbT: (H w). rewrite dfa_op_correct -negb_imply negbK. + by move/implyP. + - rewrite dfa_op_correct -negb_imply. apply/negbTE. rewrite negbK. + apply/implyP. exact: H. +Qed. + +End FA. + +(** ** DFA for preimages of homomorphisms *) + +Section Preimage. + Variables (char char' : finType). + + Variable (h : word char -> word char'). + Hypothesis h_hom : homomorphism h. + + Definition dfa_preim (A : dfa char') : dfa char := + {| dfa_s := dfa_s A; + dfa_fin := dfa_fin A; + dfa_trans x a := delta x (h [:: a]) |}. + + Lemma dfa_preimP A : dfa_lang (dfa_preim A) =i preim h (dfa_lang A). + Proof. + move => w. rewrite !inE /dfa_accept /dfa_preim /=. + elim: w (dfa_s A) => [|a w IHw] x /= ; first by rewrite h0. + by rewrite -[a :: w]cat1s h_hom !delta_cat -IHw. + Qed. + +End Preimage. + +Lemma preim_regular (char char' : finType) (h : word char -> word char') L : + homomorphism h -> regular L -> regular (preimage h L). +Proof. + move => hom_h [A HA]. exists (dfa_preim h A) => w. + by rewrite dfa_preimP // unfold_in /= -HA. +Qed. + +(** ** Closure under Right Quotients *) + +Section RightQuotient. + Variables (char: finType) (L1 L2 : lang char). + + Definition quotR := fun x => exists2 y, L2 y & L1 (x++y). + + Variable (A : dfa char). + Hypothesis acc_L1 : dfa_lang A =p L1. + Hypothesis dec_L2 : forall (q:A), decidable (exists2 y, L2 y & delta q y \in dfa_fin A). + + (** It would be better to not make the DFA explicit and require + decidabiliy of [(exists2 y, L2 y & L1 (x ++ y))] but that would + require a connected DFA in order to define the final states via + canonical words *) + + Definition dfa_quot := + {| dfa_s := dfa_s A; + dfa_trans := @dfa_trans _ A; + dfa_fin := [set q | dec_L2 q] |}. + + Lemma dfa_quotP x : reflect (quotR x) (x \in dfa_lang dfa_quot). + Proof. + apply: (iffP idP). + - rewrite inE /dfa_accept inE. case/dec_eq => y inL2. + rewrite -delta_cat => H. exists y => //. by rewrite -acc_L1. + - case => y y1 y2. rewrite inE /dfa_accept inE /= dec_eq. + exists y => //. by rewrite -delta_cat acc_L1. + Qed. + +End RightQuotient. + +(** Useful special case of the right-quotient construction. Other +special cases would be where [L2] is context free, the case for +arbitrary [L2] is non-constructive. *) + +Lemma regular_quotR (char : finType) (L1 L2 : lang char) : + regular L1 -> regular L2 -> regular (quotR L1 L2). +Proof. + move => [A LA] reg2. + suff dec_L1 q : decidable (exists2 y, L2 y & delta q y \in dfa_fin A). + { exists (dfa_quot dec_L1) => x. apply: (rwP (dfa_quotP _ _ _)) => {x} x. by rewrite LA. } + case: reg2 => {LA} [B LB]. + pose C := {| dfa_s := q ; dfa_fin := dfa_fin A ; dfa_trans := @dfa_trans _ A |}. + pose dec := dfa_inhab (dfa_op andb B C). + apply: (dec_iff dec); split. + - move => [x X1 X2]. exists x. rewrite dfa_op_correct. apply/andP;split => //. exact/LB. + - move => [x]. rewrite dfa_op_correct. case/andP => *. exists x => //. exact/LB. +Qed. + +(** ** Closure under Left Quotients *) + + +Section LeftQuotient. + Variables (char: finType) (L1 L2 : lang char). + + Definition quotL := fun y => exists2 x, L1 x & L2 (x++y). + + Variable (A : dfa char). + Hypothesis acc_L2 : L2 =p dfa_lang A. + Hypothesis dec_L1 : forall (q:A), decidable (exists2 y, L1 y & delta_s A y = q). + + Let A_start q := {| dfa_s := q; dfa_fin := dfa_fin A; dfa_trans := @dfa_trans _ A |}. + + + Lemma A_start_cat x y : (x ++ y \in dfa_lang A) = (y \in dfa_lang (A_start (delta_s A x))). + Proof. rewrite inE /delta_s. elim: x (dfa_s A)=> //= a x IH q. by rewrite accE IH. Qed. + + Lemma regular_quotL_aux : regular quotL. + Proof. + pose S := [seq q | q <- enum A & dec_L1 q]. + pose L (q:A) := mem (dfa_lang (A_start q)). + pose R x := exists2 a, a \in S & L a x. + suff: quotL =p R. + { apply: regular_ext. apply: regular_bigU => q qS. by exists (A_start q). } + move => y; split. + - case => x H1 /acc_L2 H2. exists (delta_s A x). + + apply/mapP. exists (delta_s A x) => //. rewrite mem_filter mem_enum inE andbT. + apply/dec_eq. by exists x. + + by rewrite /L topredE -A_start_cat. + - case => ? /mapP [q]. rewrite mem_filter mem_enum inE andbT => /dec_eq [x L1_x <- ->]. + rewrite /L topredE -A_start_cat => Hxy. exists x => //. exact/acc_L2. + Qed. +End LeftQuotient. + +Lemma regular_quotL (char: finType) (L1 L2 : lang char) : + regular L1 -> regular L2 -> regular (quotL L1 L2). +Proof. + move => [A acc_L1] [B acc_L2]. apply: regular_quotL_aux acc_L2 _ => q. + pose B_q := {| dfa_s := dfa_s B; dfa_fin := [set q] ; dfa_trans := @dfa_trans _ B |}. + have B_qP y : delta_s B y = q <-> y \in dfa_lang B_q. + { rewrite -delta_lang inE. by split => ?; exact/eqP. } + pose dec := dfa_inhab (dfa_op andb A B_q). + apply: dec_iff dec _. split. + - move => [y] H1 Hq. exists y. rewrite dfa_op_correct. + apply/andP;split; first exact/acc_L1. exact/B_qP. + - move => [y]. rewrite dfa_op_correct => /andP [H1 H2]. exists y; first exact/acc_L1. + exact/B_qP. +Qed. + +(** regular languages are logically determined and since propositions + can be embedded into languages, there are some languages that are regular + iff we assume excluded middle. (take [P] to be any independent proposition) *) + +Lemma regular_det (char : finType) L (w : word char): + inhabited (regular L) -> (L w) \/ (~ L w). +Proof. case. case => A ->. by case: (w \in dfa_lang A); [left|right]. Qed. + +Lemma regular_xm (char : finType) : + (forall P, inhabited (regular (fun _ : word char => P))) <-> (forall P, P \/ ~ P). +Proof. + split => [H|H] P ; first exact: regular_det [::] (H P). + case: (H P) => HP; constructor. + + exists (dfa_compl (dfa_void char)) => x. by rewrite dfa_compl_correct dfa_void_correct. + + exists (dfa_void char) => w. by rewrite /dfa_lang inE (negbTE (dfa_void_correct _ _)). +Qed. + +(** ** Residucal Criterion *) + +Section NonRegular. + Variables (char : finType) . + + Implicit Types (L : lang char). + + Definition residual L x := fun y => L (x ++ y). + + Lemma residualP (f : nat -> word char) (L : lang char) : + (forall n1 n2, residual L (f n1) =p residual L (f n2) -> n1 = n2) -> + ~ inhabited (regular L). + Proof. + move => f_spec [[A E]]. + pose f' (n : 'I_#|A|.+1) := delta_s A (f n). + suff: injective f' by move/card_leq_inj ; rewrite card_ord ltnn. + move => [n1 H1] [n2 H2]. rewrite /f' /delta_s /= => H. + apply/eqP; change (n1 == n2); apply/eqP. apply: f_spec => w. + by rewrite /residual !E !inE /dfa_accept !delta_cat H. + Qed. + + Hypothesis (a b : char) (Hab : a != b). + + Definition Lab w := exists n, w = nseq n a ++ nseq n b. + + Lemma count_nseq (T : eqType) (c d : T) n : + count (pred1 c) (nseq n d) = (c == d) * n. + Proof. elim: n => //= n. rewrite [d == c]eq_sym. by case e: (c == d) => /= ->. Qed. + + Lemma countL n1 n2 : count (pred1 a) (nseq n1 a ++ nseq n2 b) = n1. + Proof. by rewrite count_cat !count_nseq (negbTE Hab) eqxx //= mul1n mul0n addn0. Qed. + + Lemma countR n1 n2 : count (pred1 b) (nseq n1 a ++ nseq n2 b) = n2. + Proof. by rewrite count_cat !count_nseq eq_sym (negbTE Hab) eqxx //= mul1n mul0n. Qed. + + Lemma Lab_eq n1 n2 : Lab (nseq n1 a ++ nseq n2 b) -> n1 = n2. + Proof. + move => [n H]. + by rewrite -[n1](countL _ n2) -{2}[n2](countR n1 n2) H countL countR. + Qed. + + Lemma Lab_not_regular : ~ inhabited (regular Lab). + Proof. + pose f n := nseq n a. + apply: (@residualP f) => n1 n2. move/(_ (nseq n2 b)) => H. + apply: Lab_eq. apply/H. by exists n2. + Qed. + +End NonRegular. + +(** ** Pumping Lemma *) + +Section Pumping. + Definition sub (T:eqType) i j (s : seq T) := take (j-i) (drop i s). + + Definition rep (T : eqType) (s : seq T) n := iter n (cat s) [::]. + + Variable char : finType. + + Lemma delta_rep (A : dfa char) (p : A) x i : delta p x = p -> delta p (rep x i) = p. + Proof. elim: i => //= i IH H. by rewrite delta_cat H IH. Qed. + + Lemma pump_dfa (A : dfa char) x y z : + x ++ y ++ z \in dfa_lang A -> #|A| < size y -> + exists u v w, + [/\ ~~ nilp v, y = u ++ v ++ w & forall i, (x ++ u ++ rep v i ++ w ++ z) \in dfa_lang A]. + Proof. + rewrite -delta_lang => H1 H2. + have/injectivePn : ~~ injectiveb (fun i : 'I_(size y) => delta (delta_s A x) (take i y)). + apply: contraL H2 => /injectiveP/card_leq_inj. by rewrite leqNgt card_ord. + move => [i] [j] ij fij. + wlog {ij} ij : i j fij / i < j. rewrite neq_ltn in ij. case/orP : ij => ij W; exact: W _ ij. + exists (take i y). exists (sub i j y). exists (drop j y). split => [||k]. + - apply: contraL ij. + by rewrite /nilp size_take size_drop ltn_sub2r ?ltn_ord // subn_eq0 leqNgt. + - by rewrite catA -take_addn subnKC 1?ltnW // cat_take_drop. + - rewrite inE /dfa_accept !delta_cat delta_rep. + by rewrite fij -!delta_cat !catA -[(x ++ _) ++ _]catA cat_take_drop -!catA. + rewrite -delta_cat -take_addn subnKC //. exact: ltnW. + Qed. + + Lemma pumping (L : word char -> Prop) : + (forall k, exists x y z, k <= size y /\ L (x ++ y ++ z) /\ + (forall u v w, y = u ++ v ++ w -> ~~ nilp v -> + exists i, L (x ++ u ++ rep v i ++ w ++ z) -> False)) + -> ~ inhabited (regular L). + Proof. + move => H [[A LA]]. + move/(_ #|A|.+1) : H => [x] [y] [z] [size_y [/LA Lxyz]]. + move: (pump_dfa Lxyz size_y) => [u] [v] [w] [Hn Hy Hv] /(_ u v w Hy Hn). + move => [i]. apply. exact/LA. + Qed. + + Lemma cat_nseq_eq n1 n2 (a : char) : + nseq n1 a ++ nseq n2 a = nseq (n1+n2) a. + Proof. elim: n1 => [|n1 IHn1] //=. by rewrite -cat1s IHn1. Qed. + + Example pump_Lab (a b : char) : a != b -> ~ inhabited (regular (Lab a b)). + Proof. + move => neq. apply: pumping => k. + exists [::]. exists (nseq k a). exists (nseq k b). repeat split. + - by rewrite size_nseq. + - by exists k. + - move => u [|c v] w // /eqP e _. exists 0 => /= H. + have Hk: k = size (u ++ (c::v) ++ w) by rewrite -[k](@size_nseq _ _ a) (eqP e). + rewrite Hk !size_cat -!cat_nseq_eq !eqseq_cat ?size_nseq // in e. + case/and3P : e => [/eqP Hu /eqP Hv /eqP Hw]. + rewrite -Hu -Hw catA cat_nseq_eq in H. move/(Lab_eq neq) : H. + move/eqP. by rewrite Hk !size_cat eqn_add2l -{1}[size w]add0n eqn_add2r. + Qed. + +End Pumping. \ No newline at end of file diff --git a/theories/languages.v b/theories/languages.v new file mode 100644 index 0000000..c117546 --- /dev/null +++ b/theories/languages.v @@ -0,0 +1,162 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** * Languages in Type Theory + +In this file mainly defines aliases for (decidable) languages. It also +shows that decidable languages are closed under the primitive regular +operations (e.g. concatenation and interation). This will allow us to +assign decidable languages to regular expressions. We allow for +infinite (but discrete) alphabets *) + +(** The definitions of [conc] and [star] as well as the proofs of +[starP] and [concP] are taken from from regexp.v in: + +Thierry Coquand, Vincent Siles, A Decision Procedure for Regular +Expression Equivalence in Type Theory (DOI: +10.1007/978-3-642-25379-9_11). See also: +https://github.com/vsiles/regexp-Brzozowski *) + +Section Basics. + Variables char : eqType. + Definition word := seq char. + Definition lang := word -> Prop. + Definition dlang := pred word. + + Canonical Structure word_eqType := [eqType of word]. + Identity Coercion pred_of_dlang : dlang >-> pred. +End Basics. + +Section HomDef. + Variables (char char' : finType). + Variable (h : seq char -> seq char'). + + Definition homomorphism := forall w1 w2, h (w1 ++ w2) = h w1 ++ h w2. + Hypothesis h_hom : homomorphism. + + Lemma h0 : h [::] = [::]. + Proof. + apply: size0nil. apply/eqP. + by rewrite -(eqn_add2r (size (h [::]))) -size_cat -h_hom /=. + Qed. + + Lemma h_seq w : h w = flatten [seq h [:: a] | a <- w]. + Proof. elim: w => [|a w IHw] /= ; by rewrite ?h0 // -cat1s h_hom IHw. Qed. + + Lemma h_flatten vv : h (flatten vv) = flatten (map h vv). + Proof. + elim: vv => //= [|v vv IHvv]; first exact: h0. + by rewrite h_hom IHvv. + Qed. + + Definition image (L : word char -> Prop) v := exists w, L w /\ h w = v. + + Lemma image_ext L1 L2 w : + (forall v, L1 v <-> L2 v) -> (image L1 w <-> image L2 w). + Proof. by move => H; split; move => [v] [] /H; exists v. Qed. + + Definition preimage (L : word char' -> Prop) v := L (h v). + + +End HomDef. + +(** ** Closure Properties for Decidable Languages *) + +Section DecidableLanguages. + +Variable char : eqType. +Implicit Types (x y z : char) (u v w : word char) (L : dlang char). + +Definition void : dlang char := pred0. + +Definition eps : dlang char := pred1 [::]. + +Definition atom x : dlang char := pred1 [:: x]. + +Definition compl L : dlang char := predC L. + +Definition prod L1 L2 : dlang char := [pred w in L1 | w \in L2]. + +Definition plus L1 L2 : dlang char := [pred w | (w \in L1) || (w \in L2)]. + +Definition residual x L : dlang char := [pred w | x :: w \in L]. + +(** For the concatenation of two decidable languages, we use finite +types. Note that we need to use [L1] and [L2] applicatively in order +for the termination check for [star] to succeed. *) + +Definition conc (L1 L2: dlang char) : dlang char := + fun v => [exists i : 'I_(size v).+1, L1 (take i v) && L2 (drop i v)]. + +(** The iteration (Kleene star) operator is defined using resisdual +languages. Termination of star relies in the fact that conc applies +its second argument only to [drop i v] which is "structurally less +than or equal" to [v] *) + +Definition star L : dlang char := + fix star v := if v is x :: v' then conc (residual x L) star v' else true. + +Lemma plusP r s w : + reflect (w \in r \/ w \in s) (w \in plus r s). +Proof. rewrite !inE. exact: orP. Qed. + +Lemma concP {L1 L2 : dlang char} {w : word char} : + reflect (exists w1 w2, w = w1 ++ w2 /\ w1 \in L1 /\ w2 \in L2) (w \in conc L1 L2). +Proof. apply: (iffP existsP) => [[n] /andP [H1 H2] | [w1] [w2] [e [H1 H2]]]. + - exists (take n w). exists (drop n w). by rewrite cat_take_drop -topredE. + - have lt_w1: size w1 < (size w).+1 by rewrite e size_cat ltnS leq_addr. + exists (Ordinal lt_w1); subst. + rewrite take_size_cat // drop_size_cat //. exact/andP. +Qed. + +Lemma conc_cat w1 w2 L1 L2 : w1 \in L1 -> w2 \in L2 -> w1 ++ w2 \in conc L1 L2. +Proof. move => H1 H2. apply/concP. exists w1. by exists w2. Qed. + +Lemma conc_eq (l1: dlang char) l2 l3 l4: + l1 =i l2 -> l3 =i l4 -> conc l1 l3 =i conc l2 l4. +Proof. + move => H1 H2 w. apply: eq_existsb => n. + by rewrite (_ : l1 =1 l2) // (_ : l3 =1 l4). +Qed. + +Lemma starP : forall {L v}, + reflect (exists2 vv, all [predD L & eps] vv & v = flatten vv) (v \in star L). +Proof. +move=> L v; + elim: {v}_.+1 {-2}v (ltnSn (size v)) => // n IHn [|x v] /= le_v_n. + by left; exists [::]. +apply: (iffP concP) => [[u] [v'] [def_v [Lxu starLv']] | [[|[|y u] vv] //=]]. + case/IHn: starLv' => [|vv Lvv def_v']. + by rewrite -ltnS (leq_trans _ le_v_n) // def_v size_cat !ltnS leq_addl. + by exists ((x :: u) :: vv); [exact/andP | rewrite def_v def_v']. +case/andP=> Lyu Lvv [def_x def_v]; exists u. exists (flatten vv). +subst. split => //; split => //. apply/IHn; last by exists vv. +by rewrite -ltnS (leq_trans _ le_v_n) // size_cat !ltnS leq_addl. +Qed. + +Lemma star_cat w1 w2 L : w1 \in L -> w2 \in (star L) -> w1 ++ w2 \in star L. +Proof. + case: w1 => [|a w1] // H1 /starP [vv Ha Hf]. apply/starP. + by exists ((a::w1) :: vv); rewrite ?Hf //= H1. +Qed. + +Lemma starI (L : dlang char) vv : + (forall v, v \in vv -> v \in L) -> flatten vv \in star L. +Proof. + elim: vv => /= [//| v vv IHvv /all1s [H1 H2]]. + exact: star_cat _ (IHvv _). +Qed. + +Lemma star_eq (l1 : dlang char) l2: l1 =i l2 -> star l1 =i star l2. +Proof. + move => H1 w. apply/starP/starP; move => [] vv H3 H4; exists vv => //; + erewrite eq_all; try eexact H3; move => x /=; by rewrite ?H1 // -?H1. +Qed. + +End DecidableLanguages. diff --git a/theories/minimization.v b/theories/minimization.v new file mode 100644 index 0000000..d7059e9 --- /dev/null +++ b/theories/minimization.v @@ -0,0 +1,305 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice. +From mathcomp Require Import fintype path fingraph finfun finset generic_quotient. +Require Import misc languages dfa. + +Set Implicit Arguments. +Unset Printing Implicit Defensive. +Unset Strict Implicit. + +Local Open Scope quotient_scope. + +(** * DFA Minimization *) + +Section Minimization. +Variable (char : finType). +Local Notation word := (word char). +Local Notation dfa := (dfa char). + +Definition coll (A : dfa) x y := forall w, (delta x w \in dfa_fin A) = (delta y w \in dfa_fin A). + +Definition connected (A : dfa) := surjective (delta_s A). +Definition collapsed (A : dfa) := forall x y: A, coll x y <-> x = y. +Definition minimal (A : dfa) := forall B, dfa_lang A =i dfa_lang B -> #|A| <= #|B|. + +(** ** Uniqueness of connected and collapsed automata *) + +Definition dfa_iso (A1 A2 : dfa) := + exists i: A1 -> A2, + [/\ bijective i, + forall x a, i (dfa_trans x a) = dfa_trans (i x) a, + forall x, i (x) \in dfa_fin A2 = (x \in dfa_fin A1) & + i (dfa_s A1) = dfa_s A2 ]. + +Section Isomopism. + Variables (A B : dfa). + Hypothesis L_AB : dfa_lang A =i dfa_lang B. + + Hypothesis (A_coll: collapsed A) (B_coll: collapsed B). + Hypothesis (A_conn : connected A) (B_conn : connected B). + + Definition iso := delta_s B \o cr A_conn. + Definition iso_inv := delta_s A \o cr B_conn. + + Lemma delta_iso w x : delta (iso x) w \in dfa_fin B = (delta x w \in dfa_fin A). + Proof. by rewrite -{2}[x](crK (Sf := A_conn)) -!delta_cat !delta_lang L_AB. Qed. + + Lemma delta_iso_inv w x : delta (iso_inv x) w \in dfa_fin A = (delta x w \in dfa_fin B). + Proof. by rewrite -{2}[x](crK (Sf := B_conn)) -!delta_cat !delta_lang L_AB. Qed. + + Lemma can_iso : cancel iso_inv iso. + Proof. move => x. apply/B_coll => w. by rewrite delta_iso delta_iso_inv. Qed. + + Lemma can_iso_inv : cancel iso iso_inv. + Proof. move => x. apply/A_coll => w. by rewrite delta_iso_inv delta_iso. Qed. + + Lemma coll_iso : dfa_iso A B. + Proof. + exists iso. split. + - exact: Bijective can_iso_inv can_iso. + - move => x a. apply/B_coll => w. rewrite -[_ (iso x) a]/(delta (iso x) [::a]). + by rewrite -delta_cat -!delta_iso_inv !can_iso_inv. + - move => x. by rewrite -[iso x]/(delta _ [::]) delta_iso. + - apply/B_coll => w. by rewrite delta_iso !delta_lang. + Qed. + + Lemma dfa_iso_size : dfa_iso A B -> #|A| = #|B|. + Proof. move => [iso [H _ _ _]]. exact (bij_card H). Qed. +End Isomopism. + +Lemma abstract_minimization A f : + (forall B, dfa_lang (f B) =i dfa_lang B /\ #|f B| <= #|B| /\ connected (f B) /\ collapsed (f B)) + -> minimal (f A). +Proof. + move => H B L_AB. apply: (@leq_trans #|f B|); last by firstorder. apply: eq_leq. + apply: dfa_iso_size. (apply: coll_iso; try apply H) => w. rewrite L_AB. by case (H B) => ->. +Qed. + +(** ** Construction of the Connected Sub-Automaton *) + +Section Prune. + Variable A : dfa. + + Definition reachable (q:A) := exseq_dec (@delta_rc _ A) (pred1 q). + Definition connectedb := [forall x: A, reachable x]. + + Lemma connectedP : reflect (connected A) (connectedb). + Proof. + apply: (iffP forallP) => H y; first by move/dec_eq: (H y). + apply/dec_eq. case (H y) => x Hx. by exists x. + Qed. + + Definition reachable_type := { x:A | reachable x }. + + Lemma reachable_trans_proof (x : reachable_type) a : reachable (dfa_trans (val x) a). + Proof. + apply/dec_eq. case/dec_eq : (svalP x) => /= y /eqP <-. + exists (y++[::a]). by rewrite delta_cat. + Qed. + + Definition reachable_trans (x : reachable_type) a : reachable_type := + Sub (dfa_trans (val x) a) (reachable_trans_proof x a). + + Lemma reachabe_s_proof : reachable (dfa_s A). + Proof. apply/dec_eq. exists nil. exact: eqxx. Qed. + + Definition reachable_s : reachable_type := Sub (dfa_s A) reachabe_s_proof. + + Definition dfa_prune := {| + dfa_s := reachable_s; + dfa_fin := [set x | val x \in dfa_fin A]; + dfa_trans := reachable_trans |}. + + Lemma dfa_prune_correct : dfa_lang dfa_prune =i dfa_lang A. + Proof. + rewrite /dfa_lang /= -[dfa_s A]/(val reachable_s) => w. + rewrite !inE. elim: w (reachable_s) => [|a w IHw] [x Hx] //=. + + by rewrite /dfa_accept inE. + + by rewrite accE IHw. + Qed. + + Lemma dfa_prune_connected : connected dfa_prune. + Proof. + move => q. case/dec_eq: (svalP q) => /= x Hx. exists x. + elim/last_ind : x q Hx => //= x a IHx q. + rewrite -!cats1 /delta_s !delta_cat -!/(delta_s _ x) => H. + have X : reachable (delta_s A x). apply/dec_eq; exists x. exact: eqxx. + by rewrite (eqP (IHx (Sub (delta_s A x) X) _)). + Qed. + + Hint Resolve dfa_prune_connected. + + Lemma dfa_prune_size : #|dfa_prune| <= #|A|. + Proof. by rewrite card_sig subset_leq_card // subset_predT. Qed. + + (** If pruning does not remove any states, the automaton is connected *) + + Lemma prune_eq_connected : #|A| = #|dfa_prune| -> connected A. + Proof. + move => H. apply/connectedP. apply/forallP => x. + by move: (cardT_eq (Logic.eq_sym H)) ->. + Qed. + +End Prune. + +(** ** Quoitient modulo collapsing relation + +For the minimization of connected automata we construct the quotient of the +input automaton with respect to the collapsing relation. To form the quotient +constructively, we have to show that the collapsing relation is decidable. *) + +Section Collapse. + Variable A : dfa. + + (** Decidabilty of the collapsing relation *) + + Definition coll_fun (p q : A) x := (delta p x,delta q x). + + Lemma coll_fun_RC p q x y a : + coll_fun p q x = coll_fun p q y -> coll_fun p q (x++[::a]) = coll_fun p q (y++[::a]). + Proof. move => [H1 H2]. by rewrite /coll_fun !delta_cat H1 H2. Qed. + + Definition collb p q : bool := + allseq_dec (@coll_fun_RC p q) [pred p | (p.1 \in dfa_fin A) == (p.2 \in dfa_fin A)]. + + Lemma collP p q : reflect (coll p q) (collb p q). + Proof. + apply: (iffP idP). + - move/dec_eq => H x. by move/eqP: (H x). + - move => H. apply/dec_eq => x. apply/eqP. exact: H. + Qed. + + Lemma collb_refl x : collb x x. + Proof. apply/collP. rewrite /coll. auto. Qed. + + Lemma collb_sym : symmetric collb. + Proof. move => x y. by apply/collP/collP; move => H w; rewrite H. Qed. + + Lemma collb_trans : transitive collb. + Proof. move => x y z /collP H1 /collP H2. apply/collP => w. by rewrite H1 H2. Qed. + + Lemma collb_step a x y : collb x y -> collb (dfa_trans x a) (dfa_trans y a). + Proof. move => /collP H. apply/collP => w. by rewrite !delta_cons H. Qed. + + (** We make collb the canonical equivalence relation on [A] and take + the corresponding quotient type as state space for the minimized automaton *) + + Canonical collb_equiv := EquivRelPack (EquivClass collb_refl collb_sym collb_trans). + + Definition collapse_state := {eq_quot collb_equiv}. + + Canonical min_quotType := [quotType of collapse_state]. + Canonical min_subType := [subType collapse_state of A by %/]. + Canonical min_eqType := EqType _ [eqMixin of collapse_state by <:%/]. + Canonical min_choiceType := ChoiceType _ [choiceMixin of collapse_state by <:%/]. + Canonical min_finType := FinType _ [finMixin of min_eqType by <:%/]. + Canonical min_subFinType := [subFinType of collapse_state]. + + Definition collapse : dfa := {| + dfa_s := \pi_(collapse_state) (dfa_s A); + dfa_trans x a := \pi (dfa_trans (repr x) a); + dfa_fin := [set x : collapse_state | repr x \in dfa_fin A ] |}. + + Lemma collapse_delta (x : A) w : + delta (\pi x : collapse) w = \pi (delta x w). + Proof. + elim: w x => //= a w IHw x. rewrite -IHw. f_equal. + apply/eqmodP. apply: collb_step. exact: epiK. + Qed. + + Lemma collapse_fin (x : A) : + (\pi x \in dfa_fin collapse) = (x \in dfa_fin A). + Proof. + rewrite /collapse /= inE. + by move/collP: (epiK collb_equiv x) => /(_ [::]). + Qed. + +End Collapse. + +(** ** Correctness of Minimization *) + +(** Minimization yields a fully collapsed DFA accpeting the same language *) + +Lemma collapse_collapsed (A : dfa) : collapsed (collapse A). +Proof. + split => [H|->]; last by apply/collP; exact: collb_refl. + rewrite -[x]reprK -[y]reprK. apply/eqmodP/collP => w. + by rewrite -!collapse_fin -!collapse_delta !reprK. +Qed. + +Lemma collapse_correct A : dfa_lang (collapse A) =i dfa_lang A. +Proof. + move => w. rewrite !inE /dfa_accept {1}/dfa_s /= inE collapse_delta. + by rewrite -!collapse_fin reprK. +Qed. + +Lemma collapse_size A : #|collapse A| <= #|A|. +Proof. rewrite card_sub. exact: max_card. Qed. + +Lemma collapse_connected A : connected A -> connected (collapse A). +Proof. + move => H x. case: (H (repr x)) => w /eqP Hw. exists w. + by rewrite /delta_s collapse_delta -/(delta_s A w) Hw reprK. +Qed. + +(** Combine prunine and collapsing into minimization function *) + +Definition minimize := collapse \o dfa_prune. + +Lemma minimize_size (A : dfa) : #|minimize A| <= #|A|. +Proof. exact: leq_trans (collapse_size _) (dfa_prune_size _). Qed. + +Lemma minimize_collapsed (A : dfa) : collapsed (minimize A). +Proof. exact: collapse_collapsed. Qed. + +Lemma minimize_connected (A : dfa) : connected (minimize A). +Proof. apply collapse_connected. exact: dfa_prune_connected. Qed. + +Lemma minimize_correct (A : dfa) : dfa_lang (minimize A) =i dfa_lang A. +Proof. move => x. by rewrite collapse_correct dfa_prune_correct. Qed. + +Hint Resolve minimize_size minimize_collapsed minimize_connected. + +Lemma minimize_minimal A : minimal (minimize A). +Proof. apply: abstract_minimization => B. auto using minimize_correct. (* and hints *) Qed. + +(** ** Uniqueness of minimal automaton *) + +Lemma minimal_connected A : minimal A -> connected A. +Proof. + move => MA. apply: prune_eq_connected. + apply/eqP. rewrite eqn_leq dfa_prune_size andbT. + apply: MA => x. by rewrite dfa_prune_correct. +Qed. + +Lemma minimal_collapsed A : minimal A -> collapsed A. +Proof. + move => MA. + have B : bijective (\pi_(collapse_state A)). + apply: surj_card_bij. + - move => x. exists (repr x). by rewrite reprK. + - apply/eqP. rewrite eqn_leq collapse_size (MA (collapse A)) // => x. + by rewrite collapse_correct. + move => x y. split => [|->]; last exact/collP/collb_refl. + move/collP/eqmodP. exact: bij_inj. +Qed. + +(** In order to generalize the reasoning above to arbitrary quotients +types over finite types we would first have to ensure that [{eq_quot e}] +inherits the finType structure on the carrier of [e]. By default +this is not the case *) + +Lemma minimalP A : minimal A <-> (connected A /\ collapsed A). +Proof. + split. + - move => H. split. exact: minimal_connected. exact: minimal_collapsed. + - move => [H1 H2] B L_AB. apply: leq_trans _ (minimize_size _). apply: eq_leq. + apply: dfa_iso_size. apply: coll_iso => // x. by rewrite minimize_correct. +Qed. + +Lemma minimal_iso A B : + dfa_lang A =i dfa_lang B -> minimal A -> minimal B -> dfa_iso A B. +Proof. move => L_AB /minimalP [? ?] /minimalP [? ?]. exact: coll_iso. Qed. + +End Minimization. diff --git a/theories/misc.v b/theories/misc.v new file mode 100644 index 0000000..c818050 --- /dev/null +++ b/theories/misc.v @@ -0,0 +1,263 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +Require Import mathcomp.ssreflect.ssreflect. +From mathcomp Require Import all_ssreflect. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** * Preliminaries + +This file contains a number of auxiliary lemmas that do not mention +any of the representations of regular languages and may thus also be +useful in other contexts *) + +(** ** Generic Lemmas not in MathComp *) + +(** Logic *) + +Notation "P =p Q" := (forall x, P x <-> Q x) (at level 30). + +Lemma dec_iff P Q : decidable P -> Q <-> P -> decidable Q. +Proof. firstorder. Qed. + +Lemma eqb_iff (b1 b2 : bool) : (b1 <-> b2) <-> (b1 = b2). +Proof. split => [[A B]|->//]. exact/idP/idP. Qed. + +(* equivalence of type inhabitation *) +CoInductive iffT T1 T2 := IffT of (T1 -> T2) & (T2 -> T1). +Notation "T1 <-T-> T2" := (iffT T1 T2) (at level 30). + +Definition iffT_LR T1 T2 : iffT T1 T2 -> T1 -> T2. by case. Qed. +Definition iffT_RL T1 T2 : iffT T1 T2 -> T2 -> T1. by case. Qed. + +Hint View for move/ iffT_LR|2 iffT_RL|2. +Hint View for apply/ iffT_LR|2 iffT_RL|2. + +(** Arithmetic *) + +Lemma size_induction {X : Type} (measure : X -> nat) (p : X ->Prop) : + ( forall x, ( forall y, measure y < measure x -> p y) -> p x) -> forall x, p x. +Proof. + move => A x. apply: (A). elim: (measure x) => // n IHn y Hy. + apply: A => z Hz. apply: IHn. exact: leq_trans Hz Hy. +Qed. + +(** Sequences - seq.v *) + +Lemma nth_cons T (x0:T) x (s : seq T) n : nth x0 (x::s) n.+1 = nth x0 s n. +Proof. done. Qed. + +Lemma take_take T (s : seq T) n m : n < m -> take n (take m s) = take n s. +Proof. elim: m n s => // n IHn [|m] [|a s] //= ?. by rewrite IHn. Qed. + +Lemma take_addn (T : Type) (s : seq T) n m : take (n + m) s = take n s ++ take m (drop n s). +Proof. + elim: n m s => [|n IH] [|m] [|a s] //; first by rewrite take0 addn0 cats0. + by rewrite drop_cons addSn !take_cons /= IH. +Qed. + +Lemma index_take (T : eqType) (a : T) n (s : seq T) : + a \in take n s -> index a (take n s) = index a s. +Proof. move => H. by rewrite -{2}[s](cat_take_drop n) index_cat H. Qed. + +Lemma flatten_rcons T ss (s:seq T) : flatten (rcons ss s) = flatten ss ++ s. +Proof. by rewrite -cats1 flatten_cat /= cats0. Qed. + +Lemma rev_flatten T (ss : seq (seq T)) : + rev (flatten ss) = flatten (rev (map rev ss)). +Proof. +elim: ss => //= s ss IHss. +by rewrite rev_cons flatten_rcons -IHss rev_cat. +Qed. + +Hint Resolve mem_head. + +Lemma all1s {T : eqType} {a : T} {s} {P : T -> Prop} : + (forall b, b \in a :: s -> P b) <-> P a /\ (forall b, b \in s -> P b). +Proof. + split => [A|[A B] b /predU1P [->//|]]; last exact: B. + split => [|b B]; apply: A => //. by rewrite !inE B orbT. +Qed. + +Lemma ex1s {T : eqType} {a : T} {s} {P : T -> Prop} : + (exists2 x : T, x \in a :: s & P x) <-> P a \/ (exists2 x : T, x \in s & P x). +Proof. + split => [[x] /predU1P [->|]|]; firstorder. exists x => //. by rewrite inE H orbT. +Qed. + +Lemma orS (b1 b2 : bool) : b1 || b2 -> {b1} + {b2}. +Proof. by case: b1 => /= [_|H]; [left|right]. Qed. + +Lemma all1sT {T : eqType} {a : T} {s} {P : T -> Type} : + (forall b, b \in a :: s -> P b) <-T-> (P a * (forall b, b \in s -> P b)). +Proof. + split => [A|[A B] b]. + - split; first by apply: A. move => b in_s. apply A. by rewrite inE in_s orbT. + - rewrite inE. case/orS => [/eqP -> //|]. exact: B. +Qed. + +Lemma bigmax_seq_sup (T : eqType) (s:seq T) (P : pred T) F k m : + k \in s -> P k -> m <= F k -> m <= \max_(i <- s | P i) F i. +Proof. move => A B C. by rewrite (big_rem k) //= B leq_max C. Qed. + +Lemma max_mem n0 (s : seq nat) : n0 \in s -> \max_(i <- s) i \in s. +Proof. + case: s => // a s _. rewrite big_cons big_seq. + elim/big_ind : _ => // [n m|n A]. + - rewrite -{5}[a]maxnn maxnACA => ? ?. rewrite {1}/maxn. by case: ifP. + - rewrite /maxn. case: ifP => _ //. by rewrite inE A orbT. +Qed. + +(* reasoning about singletons *) +Lemma seq1P (T : eqType) (x y : T) : reflect (x = y) (x \in [:: y]). +Proof. rewrite inE. exact: eqP. Qed. + +Lemma sub1P (T : eqType) x (p : pred T) : reflect {subset [:: x] <= p} (x \in p). +Proof. apply: (iffP idP) => [A y|]; by [rewrite inE => /eqP->|apply]. Qed. + +(** Finite Types - fintype.v *) + +Lemma sub_forall (T: finType) (p q : pred T) : + subpred p q -> [forall x : T, p x] -> [forall x : T, q x]. +Proof. move => sub /forallP H. apply/forallP => x. exact: sub. Qed. + +Lemma sub_exists (T : finType) (P1 P2 : pred T) : + subpred P1 P2 -> [exists x, P1 x] -> [exists x, P2 x]. +Proof. move => H. case/existsP => x /H ?. apply/existsP. by exists x. Qed. + +Lemma card_leq_inj (T T' : finType) (f : T -> T') : injective f -> #|T| <= #|T'|. +Proof. move => inj_f. by rewrite -(card_imset predT inj_f) max_card. Qed. + +Lemma bij_card {X Y : finType} (f : X->Y): bijective f -> #|X| = #|Y|. +Proof. + case => g /can_inj Hf /can_inj Hg. apply/eqP. + by rewrite eqn_leq (card_leq_inj Hf) (card_leq_inj Hg). +Qed. + +Lemma cardT_eq (T : finType) (p : pred T) : #|{: { x | p x}}| = #|T| -> p =1 predT. +Proof. move/(inj_card_bij val_inj) => [g g1 g2 x]. rewrite -(g2 x). exact: valP. Qed. + +(** Finite Ordinals *) + +Lemma inord_max n : ord_max = inord n :> 'I_n.+1. +Proof. by rewrite -[ord_max]inord_val. Qed. + +Lemma inord0 n : ord0 = inord 0 :> 'I_n.+1. +Proof. by rewrite -[ord0]inord_val. Qed. + +Definition ord1 {n} := (@Ordinal (n.+2) 1 (erefl _)). + +Lemma inord1 n : ord1 = inord 1 :> 'I_n.+2. +Proof. apply: ord_inj => /=. by rewrite inordK. Qed. + +Hint Resolve ltn_ord. + +(** Finite Sets - finset.v *) + +Lemma card_set (T:finType) : #|{set T}| = 2^#|T|. +Proof. rewrite -!cardsT -powersetT. exact: card_powerset. Qed. + +(** Miscellaneous *) + +Lemma Sub_eq (T : Type) (P : pred T) (sT : subType P) (x y : T) (Px : P x) (Py : P y) : + Sub (s := sT) x Px = Sub y Py <-> x = y. +Proof. + split => [|e]. + - by rewrite -{2}[x](SubK sT) -{2}[y](SubK sT) => ->. + - move: Py. rewrite -e => Py. by rewrite (bool_irrelevance Py Px). +Qed. + +Local Open Scope quotient_scope. +Lemma epiK {T:choiceType} (e : equiv_rel T) x : e (repr (\pi_{eq_quot e} x)) x. +Proof. by rewrite -eqmodE reprK. Qed. + +Lemma set_enum (T : finType) : [set x in enum T] = [set: T]. +Proof. apply/setP => x. by rewrite !inE mem_enum. Qed. + +Lemma find_minn_bound (p : pred nat) m : + {n | [/\ n < m, p n & forall i, i < n -> ~~ p i]} + {(forall i, i < m -> ~~ p i)}. +Proof. + case: (boolP [exists n : 'I_m, p n]) => C ; [left|right]. + - have/find_ex_minn: exists n, (n < m) && p n. + case/existsP : C => [[n Hn pn]] /=. exists n. by rewrite Hn. + case => n /andP [lt_m pn] min_n. exists n. split => // i Hi. + apply: contraTN (Hi) => pi. rewrite -leqNgt min_n // pi andbT. + exact: ltn_trans lt_m. + - move => i lt_m. move: C. by rewrite negb_exists => /forallP /(_ (Ordinal lt_m)). +Qed. + +(** Relations *) + +Section Functional. + Variables (T T' : finType) (e : rel T) (e' : rel T') (f : T -> T'). + + Definition terminal x := forall y, e x y = false. + Definition functional := forall x y z, e x y -> e x z -> y = z. + + Lemma term_uniq x y z : functional -> + terminal y -> terminal z -> connect e x y -> connect e x z -> y = z. + Proof. + move => fun_e Ty Tz /connectP [p] p1 p2 /connectP [q]. + elim: p q x p1 p2 => [|a p IH] [|b q] x /=; first congruence. + - move => _ <-. by rewrite Ty. + - case/andP => xa _ _ _ H. by rewrite -H Tz in xa. + - case/andP => xa p1 p2 /andP [xb] q1 q2. + move: (fun_e _ _ _ xa xb) => ?; subst b. exact: IH q2. + Qed. + + Hypothesis f_inj : injective f. + Hypothesis f_eq : forall x y, e x y = e' (f x) (f y). + Hypothesis f_inv: forall x z, e' (f x) z -> exists y, z = f y. + + Lemma connect_transfer x y : connect e x y = connect e' (f x) (f y). + Proof. apply/idP/idP. + - case/connectP => s. + elim: s x => //= [x _ -> |z s IH x]; first exact: connect0. + case/andP => xz pth Hy. rewrite f_eq in xz. + apply: connect_trans (connect1 xz) _. exact: IH. + - case/connectP => s. + elim: s x => //= [x _ /f_inj -> |z s IH x]; first exact: connect0. + case/andP => xz pth Hy. case: (f_inv xz) => z' ?; subst. + rewrite -f_eq in xz. apply: connect_trans (connect1 xz) _. exact: IH. + Qed. +End Functional. + +Lemma functional_sub (T : finType) (e1 e2 : rel T) : + functional e2 -> subrel e1 e2 -> functional e1. +Proof. move => f_e2 sub x y z /sub E1 /sub E2. exact: f_e2 E1 E2. Qed. + +(** ** Inverting surjective functions *) + +Definition surjective aT {rT : eqType} (f : aT -> rT) := forall y, exists x, f x == y. + +Lemma surjectiveE (rT aT : finType) (f : aT -> rT) : surjective f -> #|codom f| = #|rT|. +Proof. + move => H. apply: eq_card => x. rewrite inE. apply/codomP. + move: (H x) => [y /eqP]. eauto. +Qed. + +Lemma surj_card_bij (T T' : finType) (f : T -> T') : + surjective f -> #|T| = #|T'| -> bijective f. +Proof. + move => S E. apply: inj_card_bij (E). apply/injectiveP. change (uniq (codom f)). + apply/card_uniqP. rewrite size_map -cardT E. exact: surjectiveE. +Qed. + +(* We define a general inverse of surjective functions from choiceType -> eqType. + This function gives a canonical representative, thus the name "cr". *) +Definition cr {X : choiceType} {Y : eqType} {f : X -> Y} (Sf : surjective f) y : X := + xchoose (Sf y). + +Lemma crK {X : choiceType} {Y : eqType} {f : X->Y} {Sf : surjective f} x: f (cr Sf x) = x. +Proof. by rewrite (eqP (xchooseP (Sf x))). Qed. + + + +Lemma dec_eq (P : Prop) (decP : decidable P) : decP <-> P. +Proof. by case: decP. Qed. + + + + diff --git a/theories/myhill_nerode.v b/theories/myhill_nerode.v new file mode 100644 index 0000000..2b9a0f4 --- /dev/null +++ b/theories/myhill_nerode.v @@ -0,0 +1,196 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages dfa minimization regexp. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** * Classifiers *) + +(** For us, classifiers (right-congruent functions from words into +some finite type) serve as a constructive approximation of +Myhill-Nerode partition. We show that classifiers for given language +can be turned into DFAs and vice versa. Moroever, we show that there +exist most general classifiers corresponding to minimal automata. *) + +Section Clasifiers. + +Variable char: finType. +Local Notation word := (word char). + +Record classifier := Classifier { + classifier_classes : finType; + classifier_fun :> word -> classifier_classes }. + +(** We register an additional coercion. So we can write + - [x:E] => x is a class of E + - [E w] => the class of w + - [#|E|] => the cardinality of the index type *) + +Coercion classifier_classes : classifier >-> finType. + +Definition right_congruent (X : eqType) (E : word -> X) := + forall u v a, E u = E v -> E (u ++ [::a]) = E (v ++ [::a]). + +Definition refines (X: eqType) (L : dlang char) (E : word -> X) := + forall u v, E u = E v -> (u \in L) = (v \in L). + +Record classifier_for L := { + cf_classifier :> classifier; + cf_congruent : right_congruent cf_classifier; + cf_refines : refines L cf_classifier + }. + +Lemma cf_lang_eq_proof L1 L2 (M1 : classifier_for L1) : L1 =i L2 -> refines L2 M1. +Proof. move => H0 u v /cf_refines. by rewrite -!H0. Qed. + +Definition cf_lang_eq L1 L2 (M1 : classifier_for L1) (H : L1 =i L2) := + {| cf_congruent := @cf_congruent L1 M1; cf_refines := cf_lang_eq_proof H |}. + + +(** ** Conversions between Classifiers and DFAs *) + +Section DFAtoClassifier. + Variable (A : dfa char). + + Lemma delta_s_right_congruent : right_congruent (delta_s A). + Proof. move => u v a H. rewrite /= /delta_s !delta_cat. by f_equal. Qed. + + Lemma delta_s_refines : refines (dfa_lang A) (delta_s A). + Proof. move => u v H. rewrite -!delta_lang. by f_equal. Qed. + + Definition dfa_to_cf : classifier_for (dfa_lang A) := + {| cf_classifier := Classifier (delta_s A); + cf_congruent := delta_s_right_congruent; + cf_refines := delta_s_refines |}. + + Lemma dfa_to_cf_size : #|A| = #|dfa_to_cf|. by []. Qed. +End DFAtoClassifier. + + +Section ClassifierToDFA. + Variables (L : dlang char) (M : classifier_for L). + + Definition imfun_of := image_fun (@cf_congruent _ M). + Definition imfun_of_surj := @surjective_image_fun _ _ _ (@cf_congruent _ M). + + Lemma imfun_of_refines : refines L imfun_of. + Proof. move => x y []. exact: cf_refines. Qed. + + Lemma imfun_of_congruent : right_congruent imfun_of. + Proof. + move => x y a [] /cf_congruent. + move/(_ a) => /eqP H. exact/eqP. + Qed. + + Definition classifier_to_dfa := + {| dfa_s := imfun_of [::]; + dfa_fin := [set x | cr (imfun_of_surj) x \in L]; + dfa_trans x a := imfun_of (cr (imfun_of_surj) x ++ [::a]) |}. + + Lemma classifier_to_dfa_delta : delta_s classifier_to_dfa =1 imfun_of. + Proof. + apply: last_ind => [|w a IHw] //=. + rewrite /delta_s -cats1 delta_cat -!/(delta_s _ _) IHw. + apply: imfun_of_congruent. by rewrite crK. + Qed. + + Lemma classifier_to_dfa_correct : dfa_lang classifier_to_dfa =i L. + Proof. + move => w. rewrite -delta_lang classifier_to_dfa_delta inE. + apply: imfun_of_refines. by rewrite crK. + Qed. +End ClassifierToDFA. + +Lemma classifier_to_dfa_connected L (M : classifier_for L) : + connected (classifier_to_dfa M). +Proof. + move => q. exists (cr (@imfun_of_surj _ M) q). + rewrite -{2}[q](crK (Sf:=(@imfun_of_surj _ M))). + by rewrite -/(delta_s _ _) classifier_to_dfa_delta. +Qed. + +(** ** Most General Classifiers + +Just like there exists a coarsest Myhill-Nerode relation, there also +exist most general classifiers. For these classifiers, the classes +correspond exactly to thos of the coarsest Myhill-Nerode relation. *) + +Definition nerode (X : eqType) (L : dlang char) (E : word -> X) := + forall u v, E u = E v <-> forall w, (u++w \in L) = (v++w \in L). + +Record mgClassifier L := { + mg_classifier :> classifier; + nerodeP : nerode L mg_classifier }. + +Lemma mg_right_congruent L (N : mgClassifier L) : right_congruent N. +Proof. move => u v a /nerodeP H. apply/nerodeP => w. by rewrite -!catA. Qed. + +Lemma mg_refines L (N : mgClassifier L) : refines L N. +Proof. move => u v /nerodeP H. by rewrite -[u]cats0 -[v]cats0. Qed. + +Definition mg_to_classifier L (N : mgClassifier L) := {| + cf_congruent := @mg_right_congruent L N; + cf_refines := @mg_refines L N |}. + +Coercion mg_to_classifier : mgClassifier >-> classifier_for. + +Arguments cf_congruent [L M u v a] H: rename. +Arguments cf_refines [L M u v] H: rename. +Arguments nerodeP [L] N u v: rename. + +(** Most general classifiers coerce to classifiers and can be converted to DFAs *) + +Definition mg_to_dfa L (N : mgClassifier L) := classifier_to_dfa N. + +Lemma mg_to_dfa_correct L (N : mgClassifier L) : dfa_lang (mg_to_dfa N) =i L. +Proof. exact: classifier_to_dfa_correct. Qed. + +Lemma mg_to_connected L (N : mgClassifier L) : connected (mg_to_dfa N). +Proof. exact: classifier_to_dfa_connected. Qed. + +(** Most general classifier yield minimal automata *) + +Lemma mg_minimal (L : dlang char) (M : mgClassifier L) : minimal (mg_to_dfa M). +Proof. + apply/minimalP. split; first exact: mg_to_connected. + move => p q. split => [coll_pq|->//]. + rewrite -[p](crK (Sf := (@imfun_of_surj _ M))). + rewrite -[q](crK (Sf := (@imfun_of_surj _ M))). + apply/Sub_eq. apply/nerodeP => w. + rewrite -!(@classifier_to_dfa_correct _ M) !inE /dfa_accept !delta_cat. + rewrite -!/(delta_s _ _) !classifier_to_dfa_delta !crK. exact: coll_pq. +Qed. + +(** We can cast mgClassifiers to equivalent languages *) + +Lemma mg_eq_proof L1 L2 (N1 : mgClassifier L1) : L1 =i L2 -> nerode L2 N1. +Proof. move => H0 u v. split => [/nerodeP H1 w|H1]. + - by rewrite -!H0. + - apply/nerodeP => w. by rewrite !H0. +Qed. + +Definition mg_eq L1 L2 N1 (H : L1 =i L2) := {| nerodeP := mg_eq_proof N1 H |}. + +(** Minimal DFAs immediately give rise to most general classifiers. *) + +Section mDFAtoMG. + Variable A : dfa char. + Variable MA : minimal A. + + Lemma minimal_nerode : nerode (dfa_lang A) (delta_s A). + Proof. + move => u v. apply: iff_trans (iff_sym (minimal_collapsed MA _ _)) _. + by split => H w; move: (H w); rewrite -!delta_cat !delta_lang. + Qed. + + Definition minimal_classifier := {| classifier_fun := delta_s A |}. + + Definition dfa_to_mg := {| + mg_classifier := minimal_classifier; + nerodeP := minimal_nerode |}. +End mDFAtoMG. + +End Clasifiers. \ No newline at end of file diff --git a/theories/nfa.v b/theories/nfa.v new file mode 100644 index 0000000..daf3f12 --- /dev/null +++ b/theories/nfa.v @@ -0,0 +1,420 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages dfa. + +Set Implicit Arguments. +Unset Printing Implicit Defensive. +Unset Strict Implicit. + +Section NFA. +Variable char : finType. +Local Notation word := (word char). + +(** * Nondeterministic Finite Automata. + +We define both normal NFAs and NFAs with epsilon transitions +(eNFAs). For NFAs acceptance can still be defined by structural +recursion on the word. In particular, the length of an NFA run is +determined by the input word, a property that we exploit repeatedly. *) + +Record nfa : Type := { + nfa_state :> finType; + nfa_s : { set nfa_state }; + nfa_fin : { set nfa_state }; + nfa_trans : nfa_state -> char -> nfa_state -> bool }. + +Fixpoint nfa_accept (A : nfa) (x : A) w := + if w is a :: w' then [exists (y | nfa_trans x a y), nfa_accept y w'] + else x \in nfa_fin A. + +Definition nfa_lang (A : nfa) := [pred w | [exists s, (s \in nfa_s A) && nfa_accept s w]]. + +(** ** Epsilon NFAs *) + +Record enfa : Type := { + enfa_state :> finType; + enfa_s : {set enfa_state}; + enfa_f : {set enfa_state}; + enfa_trans : option char -> enfa_state -> enfa_state -> bool }. + +Section EpsilonNFA. + Variables (N : enfa). + + (** For eNFAs, acceptance is defined relationally since structural + recursion over the word is no longer possible. *) + + Inductive enfa_accept : N -> word -> Prop := + | EnfaFin q : q \in enfa_f N -> enfa_accept q [::] + | EnfaSome p a q x : enfa_trans (Some a) p q -> enfa_accept q x -> enfa_accept p (a::x) + | EnfaNone p q x : enfa_trans None p q -> enfa_accept q x -> enfa_accept p (x). + + Definition enfa_lang x := exists2 s, s \in enfa_s N & enfa_accept s x. + + (** We convert eNFAs to NFAs by extending the set of starting states and all + transitions by epsipon-reachable states - also known as epsilon closure *) + + Definition eps_reach (p : N) := [set q | connect (enfa_trans None) p q]. + + Lemma lift_accept p q x : q \in eps_reach p -> enfa_accept q x -> enfa_accept p x. + Proof. + rewrite inE => /connectP [s]. elim: s p x q => //= [p x q _ -> //| q s IHs p x q']. + case/andP => pq ? ? H. apply: EnfaNone pq _. exact: IHs H. + Qed. + + Definition nfa_of := + {| nfa_s := \bigcup_(p in enfa_s N) (eps_reach p); + nfa_fin := enfa_f N; + nfa_trans p a q := [exists p', enfa_trans (Some a) p p' && (q \in eps_reach p') ] |}. + + Lemma enfaE x p : + (enfa_accept p x) <-> (exists2 q : nfa_of, q \in eps_reach p & nfa_accept q x). + Proof. split. + - elim => {p x} [q H|p a q x H _ [q' Hq1 Hq2]|p p' x]. + + exists q => //. by rewrite inE connect0. + + exists p => /=; first by rewrite inE connect0. + apply/exists_inP. exists q' => //. apply/exists_inP. by exists q. + + move => H1 H2 [q Hq1 Hq2]. exists q => //. rewrite !inE in Hq1 *. + exact: connect_trans (connect1 _) Hq1. + - elim: x p => [|a x IH] p [p'] R /= H. apply: lift_accept R _. exact: EnfaFin. + case/exists_inP : H => q /exists_inP [q' pq' qq'] H. apply: lift_accept R _. + apply: EnfaSome pq' _. apply: IH. by exists q. + Qed. + + Lemma nfa_ofP x : reflect (enfa_lang x) (x \in nfa_lang nfa_of). + Proof. + apply: (iffP exists_inP) => [[p Hp1 Hp2]|[s Hs1 /enfaE [p Hp1 Hp2]]]. + - case/bigcupP : Hp1 => s Hs H. exists s => //. by apply/enfaE; exists p. + - exists p => //. by apply/bigcupP; exists s. + Qed. +End EpsilonNFA. + +(** ** Equivalence of DFAs and NFAs *) +(** We use the powerset construction to obtain + a deterministic automaton from a non-deterministic one. **) +Section PowersetConstruction. + +Variable A : nfa. + +Definition nfa_to_dfa := {| + dfa_s := nfa_s A; + dfa_fin := [set X | X :&: nfa_fin A != set0]; + dfa_trans X a := [set q | [exists (p | p \in X), nfa_trans p a q]] +|}. + +Lemma nfa_to_dfa_correct : nfa_lang A =i dfa_lang nfa_to_dfa. +Proof. + move => w. rewrite !inE {2}/nfa_to_dfa /=. + elim: w (nfa_s _) => [|a x IH] X; rewrite /= accE ?inE. + - apply/existsP/set0Pn => [] [p] H; exists p; by rewrite inE in H *. + - rewrite -IH /dfa_trans /=. apply/exists_inP/exists_inP. + + case => p inX /exists_inP [q ? ?]. exists q => //. rewrite inE. + apply/exists_inP. by exists p. + + case => p. rewrite inE => /exists_inP [q] ? ? ?. + exists q => //. apply/exists_inP. by exists p. +Qed. + +End PowersetConstruction. + +(** We also embed NFAs into DFAs. **) + +Section Embed. + +Variable A : dfa char. + +Definition dfa_to_nfa : nfa := {| + nfa_s := [set dfa_s A]; + nfa_fin := dfa_fin A; + nfa_trans x a y := dfa_trans x a == y |}. + +Lemma dfa_to_nfa_correct : dfa_lang A =i nfa_lang dfa_to_nfa. +Proof. + move => w. rewrite !inE /nfa_s /=. + elim: w (dfa_s A) => [|b w IHw] x; rewrite accE /=. + - apply/idP/existsP => [Fx|[y /andP [/set1P ->]]//]. + exists x. by rewrite !inE eqxx. + - rewrite IHw. apply/exists_inP/exists_inP. + + case => y /set1P -> H. exists x; first exact: set11. + apply/existsP. exists (dfa_trans x b). by rewrite H eqxx. + + case => y /set1P -> {y} /existsP [z] /andP [] /eqP-> H. + exists z; by rewrite ?set11. +Qed. + +End Embed. + +(** ** Operations on NFAs + +To prepare the translation from regular expresstions to DFAs, we show +that finite automata are closed under all regular operations. We build +the primitive automata, complement and boolean combinations using +DFAs. *) + +Definition nfa_char (a:char) := + {| nfa_s := [set false]; + nfa_fin := [set true]; + nfa_trans p b q := if (p,q) is (false,true) then (b == a) else false |}. + +Lemma nfa_char_correct (a : char) : nfa_lang (nfa_char a) =1 pred1 [:: a]. +Proof. + move => w /=. apply/exists_inP/eqP => [[p]|]. + - rewrite inE => /eqP->. case: w => [|b [|c w]] /=; first by rewrite inE. + + by case/exists_inP => [[/eqP->|//]]. + + case/exists_inP => [[_|//]]. by case/exists_inP. + - move->. exists false; first by rewrite inE. apply/exists_inP. + exists true; by rewrite ?inE //=. +Qed. + +Definition nfa_plus (N M : nfa) := + {| nfa_s := [set q | match q with inl q => q \in nfa_s N | inr q => q \in nfa_s M end ]; + nfa_fin := [set q | match q with inl q => q \in nfa_fin N | inr q => q \in nfa_fin M end ]; + nfa_trans p a q := match p,a,q with + | inl p,a,inl q => nfa_trans p a q + | inr p,a,inr q => nfa_trans p a q + | _,_,_ => false + end |}. + +Lemma nfa_plus_correct (N M : nfa) : + nfa_lang (nfa_plus N M) =i plus (nfa_lang N) (nfa_lang M). +Proof. + move => w. apply/idP/idP. + - case/exists_inP => [[s|s]]; rewrite !inE => A B; + apply/orP;[left|right];apply/exists_inP; exists s => //. + + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. + case/exists_inP => [[|]// p A /IH B]. apply/exists_inP. by exists p. + + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. + case/exists_inP => [[|]// p A /IH B]. apply/exists_inP. by exists p. + - rewrite !inE. case/orP => /exists_inP [s A B]; + apply/exists_inP; [exists(inl s)|exists(inr s)]; rewrite ?inE //. + + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. + case/exists_inP => [p A /IH B]. apply/exists_inP. by exists (inl p). + + elim: w s {A} B => /= [|a w IH] s; first by rewrite inE. + case/exists_inP => [p A /IH B]. apply/exists_inP. by exists (inr p). +Qed. + +Definition nfa_eps : nfa := + {| nfa_s := [set tt]; nfa_fin := [set tt]; nfa_trans p a q := false |}. + +Lemma nfa_eps_correct: nfa_lang (nfa_eps) =i pred1 [::]. +Proof. + move => w. apply/exists_inP/idP. + + move => [[]]. case: w => [|a w] //= _. by case/exists_inP. + + move => /=. rewrite inE=>/eqP->. exists tt; by rewrite /= inE. +Qed. + +(** The automata for concatenation and Kleene star are constructed by +taking NFAs as input and first building eNFAs which are then converted +to NFAs. *) + +Section eNFAOps. + +Variables A1 A2 : nfa. + +Definition enfa_conc : enfa := + {| enfa_s := inl @: nfa_s A1; + enfa_f := inr @: nfa_fin A2; + enfa_trans c p q := + match c,p,q with + | Some a,inl p',inl q' => nfa_trans p' a q' + | Some a,inr p',inr q' => nfa_trans p' a q' + | None,inl p', inr q' => (p' \in nfa_fin A1) && (q' \in nfa_s A2) + | _,_,_ => false + end |}. + +Lemma enfa_concE (p : enfa_conc) x : enfa_accept p x -> + match p with + | inr p' => nfa_accept p' x + | inl p' => exists x1 x2, [/\ x = x1 ++ x2, nfa_accept p' x1 & x2 \in nfa_lang A2] + end. +Proof. + elim => {p x} [[?|?] /imsetP [q] // ? [->] //||]. + - move => [p|p] a [q|q] x //. + + move => pq _ [x1] [x2] [X1 X2 X3]. exists (a::x1); exists x2; subst; split => //. + by apply/exists_inP; exists q. + + move => pq _ Hq. by apply/exists_inP; exists q. + - move => [p|p] [q|q] //= x /andP[Hp Hq] _ ?. exists [::]; exists x; split => //. + by apply/exists_inP; exists q. +Qed. + +Lemma enfa_concIr (p : A2) x : nfa_accept p x -> @enfa_accept enfa_conc (inr p) x. +Proof. + elim: x p => [p Hp|a x IH p /= /exists_inP [q q1 q2]]. + - by constructor; rewrite mem_imset. + - apply: (@EnfaSome enfa_conc _ _ (inr q)) => //. exact: IH. +Qed. + +Lemma enfa_concIl (p : A1) x1 x2 : + nfa_accept p x1 -> x2 \in nfa_lang A2 -> @enfa_accept enfa_conc (inl p) (x1++x2). +Proof. + elim: x1 p => /= [p Hp /exists_inP [q q1 q2]|a x1 IH p /exists_inP [q q1 q2] H]. + - apply: (@EnfaNone enfa_conc _ (inr q)). by rewrite /= Hp. exact: enfa_concIr. + - apply: (@EnfaSome enfa_conc _ _ (inl q)). by rewrite /= q1. exact: IH. +Qed. + +Lemma enfa_concP x : reflect (enfa_lang enfa_conc x) (conc (nfa_lang A1) (nfa_lang A2) x). +Proof. + apply: (iffP (@concP _ _ _ _)) => [[x1] [x2] [X1 [X2 X3]] |]. + - case/exists_inP : X2 => s ? ?. exists (inl s); first by rewrite /enfa_conc /= mem_imset. + subst. exact: enfa_concIl. + - move => [[s /imsetP [? ? [?]] /enfa_concE [x1] [x2] [? ? ?] |s]]; last by case/imsetP. + exists x1; exists x2. repeat (split => //). apply/exists_inP. by exists s;subst. +Qed. + +Definition enfa_star : enfa := + {| enfa_s := [set None]; + enfa_f := [set None]; + enfa_trans c p q := + match c,p,q with + Some a,Some p', Some q' => q' \in nfa_trans p' a + | None, Some p', None => p' \in nfa_fin A1 + | None, None, Some s => s \in nfa_s A1 + | _,_,_ => false + end |}. + +Lemma enfa_s_None : None \in enfa_s enfa_star. +Proof. by rewrite inE. Qed. + +Lemma enfa_f_None : None \in enfa_f enfa_star. +Proof. by rewrite inE. Qed. +Hint Resolve enfa_s_None enfa_f_None. + +Lemma enfa_star_cat x1 x2 (p : enfa_star) : + enfa_accept p x1 -> enfa_lang enfa_star x2 -> enfa_accept p (x1 ++ x2). +Proof. + elim => {p x1}. + - move => p. rewrite inE => /eqP->. case => q. by rewrite inE => /eqP->. + - move => p a q x /=. case: p => // p. case: q => // q pq ? IH H. exact: EnfaSome (IH H). + - move => [p|] [q|] x //= p1 p2 IH H; exact: EnfaNone (IH H). +Qed. + +Lemma enfa_starI x (p : A1) : nfa_accept p x -> @enfa_accept enfa_star (Some p) x. +Proof. + elim: x p => /= [p H|a x IH p]. + - apply: (@EnfaNone enfa_star _ None) => //. exact: EnfaFin. + - case/exists_inP => q q1 /IH. exact: EnfaSome. +Qed. + +Lemma enfa_star_langI x : x \in nfa_lang A1 -> @enfa_accept enfa_star None x. +Proof. + case/exists_inP => s s1 s2. + apply: (@EnfaNone enfa_star _ (Some s)) => //. exact: enfa_starI. +Qed. + +Lemma enfa_starE (o : enfa_star) x : enfa_accept o x -> + if o is Some p + then exists x1 x2, [/\ x = x1 ++ x2, nfa_accept p x1 & star (nfa_lang A1) x2] + else star (nfa_lang A1) x. +Proof. + elim => {x o}. + - move => [q|//]. by rewrite inE; move/eqP. + - move => [p|] a [q|] x // H acc [x1] [x2] [H1 H2 H3]. exists (a::x1); exists x2. + rewrite H1. split => //. by apply/exists_inP; exists q. + - move => [p|] [q|] x //=. + + move => *. by exists [::]; exists x. + + move => H acc [x1] [x2] [H1 H2]. rewrite H1. apply: star_cat. + by apply/exists_inP; exists q. +Qed. + +Lemma enfa_starP x : reflect (enfa_lang enfa_star x) (star (nfa_lang A1) x). +Proof. apply: (iffP idP). + - case/starP => vv H ->. elim: vv H => /= [_|v vv]. + + exists None => //. exact: EnfaFin. + + move => IH /andP[/andP [H1 H2] H3]. exists None => //. + apply: enfa_star_cat (IH _) => //. exact: enfa_star_langI. + - case => q. rewrite inE => /eqP-> {q}. exact: enfa_starE. +Qed. + + +Definition nfa_conc := nfa_of (enfa_conc). + +Lemma nfa_conc_correct : nfa_lang nfa_conc =i conc (nfa_lang A1) (nfa_lang A2). +Proof. move => x. apply/nfa_ofP/idP => ?;exact/enfa_concP. Qed. + +Definition nfa_star := nfa_of (enfa_star). +Lemma nfa_star_correct : nfa_lang nfa_star =i star (nfa_lang A1). +Proof. move => x. apply/nfa_ofP/idP => ?;exact/enfa_starP. Qed. + +End eNFAOps. + +(** ** Runs on NFAs *) + +Section NFARun. + Variable (M : nfa). + + Inductive nfa_run : word -> M -> seq M -> Prop := + | run0 p of p \in nfa_fin M : nfa_run [::] p [::] + | runS a p q x r & q \in nfa_trans p a : nfa_run x q r -> nfa_run (a::x) p (q::r). + + Lemma nfa_acceptP x p : reflect (exists r, nfa_run x p r) (nfa_accept p x). + Proof. + apply: (iffP idP) => [|[r]]. + - elim: x p => [|a x IHx] p /=; first by exists [::]; constructor. + case/exists_inP => q p1 p2. case (IHx q p2) => r ?. by exists (q::r); constructor. + - elim: x r p => [|a x IHx] r p; first by inversion 1; subst. + inversion 1; subst. apply/exists_inP. exists q => //. exact: IHx H4. + Qed. + + Lemma run_size x r p : nfa_run x p r -> size x = size r. + Proof. by elim => // {r p x} a p q r x _ _ /= ->. Qed. + + Lemma nfaP x : reflect (exists s r, s \in nfa_s M /\ nfa_run x s r) (x \in nfa_lang M). + Proof. + apply: (iffP exists_inP). + - case => s ? /nfa_acceptP [r] ?. by exists s; exists r. + - case => s [r] [? ?]. exists s => //. apply/nfa_acceptP. by exists r. + Qed. + + Lemma run_last x p r : nfa_run x p r -> last p r \in nfa_fin M. + Proof. by elim. Qed. + + Lemma run_trans x p r i (Hi : i < size x) : nfa_run x p r -> + nth p (p::r) i.+1 \in nfa_trans (nth p (p::r) i) (tnth (in_tuple x) (Ordinal Hi)). + Proof. + move => H. elim: H i Hi => {x p r} // a p q x r tr run IH /= [|i] Hi //. + rewrite !(set_nth_default q); try by rewrite /= -(run_size run) // ltnW. + rewrite {1}[nth]lock (tnth_nth a) /=. rewrite ltnS in Hi. + rewrite -{3}[i]/(nat_of_ord (Ordinal Hi)). + by rewrite -[x]/(tval (in_tuple x)) -tnth_nth -lock IH. + Qed. + + (** The following lemma uses [in_tuple] and [tnth] in order to avoid + having to assume the existence of a default symbol *) + + Lemma runI x s r : + size r = size x -> last s r \in nfa_fin M -> + (forall i : 'I_(size x), + nth s (s::r) i.+1 \in nfa_trans (nth s (s::r) i) (tnth (in_tuple x) i)) -> + nfa_run x s r. + Proof. + elim: x s r => [|a x IHx ] s r /=. + - move/eqP => e inF _. rewrite size_eq0 in e. rewrite (eqP e) in inF *. exact: run0. + - case: r => // p r /eqP /=. rewrite eqSS => /eqP R1 R2 I. + apply: runS (I ord0) _ => /=. apply: IHx => // i. + move: (I (inord i.+1)). rewrite /tnth /= !inordK /= ?ltnS //. + rewrite !(set_nth_default p) /= ?R1 // 1?ltnW ?ltnS //. + by rewrite -[x]/(val (in_tuple x)) -!tnth_nth. + Qed. + +End NFARun. + +(** Decidability of Language Emptiness *) + +Definition nfa_inhab (N : nfa) := dfa_inhab (nfa_to_dfa N). + +Lemma nfa_inhabP N : reflect (exists w, w \in nfa_lang N) (nfa_inhab N). +Proof. + apply: (iffP (dfa_inhabP _)). + - move => [x]. rewrite -nfa_to_dfa_correct. by exists x. + - move => [x ?]. exists x. by rewrite -nfa_to_dfa_correct. +Qed. + +Lemma nfa_regular L : + regular L <-T-> { N : nfa | forall x, L x <-> x \in nfa_lang N }. +Proof. + split => [[A]|[N]] H. + exists (dfa_to_nfa A) => x. by rewrite -dfa_to_nfa_correct. + exists (nfa_to_dfa N) => x. by rewrite -nfa_to_dfa_correct. +Qed. + +End NFA. + +Arguments nfaP [char M x]. \ No newline at end of file diff --git a/theories/regexp.v b/theories/regexp.v new file mode 100644 index 0000000..eedf2fe --- /dev/null +++ b/theories/regexp.v @@ -0,0 +1,485 @@ +(* Authors: Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import setoid_leq misc languages dfa nfa. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** * Regular Expressions + +This file contains the definition of regular expressions and the proof +that regular expressions have the same expressive power as finite +automata. *) + +Section RegExp. +Variable char : eqType. + +Inductive regexp := + | Void + | Eps + | Atom of char + | Star of regexp + | Plus of regexp & regexp + | Conc of regexp & regexp. + +Lemma eq_regexp_dec (e1 e2 : regexp) : {e1 = e2} + {e1 <> e2}. +Proof. decide equality; apply: eq_comparable. Qed. + +Definition regexp_eqMixin := EqMixin (compareP eq_regexp_dec). +Canonical Structure form_eqType := EqType _ regexp_eqMixin. +End RegExp. + +Arguments void : clear implicits. +Arguments eps : clear implicits. +Prenex Implicits Plus. +Arguments plusP [char r s w]. + +Notation "'Void'" := (@Void _). +Notation "'Eps'" := (@Eps _). + +(** We assign a decidable language to every regular expression *) + +Fixpoint re_lang (char: eqType) (e : regexp char) : dlang char := + match e with + | Void => void char + | Eps => eps char + | Atom x => atom x + | Star e1 => star (re_lang e1) + | Plus e1 e2 => plus (re_lang e1) (re_lang e2) + | Conc e1 e2 => conc (re_lang e1) (re_lang e2) + end. + +Canonical Structure regexp_predType (char: eqType) := mkPredType (@re_lang char). + +(** We instantiate Ssreflects Canonical Big Operators *) +Notation "\sigma_( i <- r ) F" := (\big[Plus/Void]_(i <- r) F) (at level 50). +Notation "\sigma_( i | P ) F" := (\big[Plus/Void]_(i | P) F) (at level 50). + +Lemma big_plus_seqP (T char : eqType) (r : seq T) w (F : T -> regexp char) : + reflect (exists2 x, x \in r & w \in F x) (w \in \sigma_(i <- r) F i). +Proof. + elim: r w => [|r rs IHrs] w. rewrite big_nil; by constructor => [[x]]. + rewrite big_cons; apply: (iffP plusP) => [[H|H]|[x]]. + - exists r => //; by rewrite mem_head. + - case/IHrs : H => x Hx ?. exists x => //. by rewrite in_cons Hx orbT. + - rewrite in_cons; case/orP => [/eqP -> |]; auto => ? ?. + right. apply/IHrs. by exists x. +Qed. + +Lemma big_plusP (T char: finType) (P:pred T) w (F : T -> regexp char) : + reflect (exists2 i, P i & w \in F i) (w \in \sigma_(i | P i) F i). +Proof. + rewrite -big_filter filter_index_enum. + apply: (iffP (big_plus_seqP _ _ _)) => [|] [x] H1 H2; exists x => //; + move: H1; by rewrite mem_enum. +Qed. + +Fixpoint re_size (char: eqType) (e : regexp char) := + match e with + | Star s => (re_size s).+1 + | Plus s t => ((re_size s)+(re_size t)).+1 + | Conc s t => ((re_size s)+(re_size t)).+1 + | _ => 1 + end. + +Lemma big_plus_size (T char : eqType) (r : seq T) (F : T -> regexp char) m : + (forall i, i \in r -> re_size (F i) <= m) -> re_size (\sigma_(i <- r) F i) <= (size r * m.+1).+1. +Proof. + elim: r => [|e r IH /all1s [A B]]; first by rewrite big_nil. + rewrite big_cons /= ltnS mulSn addSn -addnS leq_add //. exact: IH. +Qed. + +(** ** Regular Expressions to Finite Automata *) +Section DFAofRE. +Variable (char : finType). + +Fixpoint re_to_nfa (r : regexp char): nfa char := + match r with + | Void => dfa_to_nfa (dfa_void _) + | Eps => nfa_eps _ + | Atom a => nfa_char a + | Star s => nfa_star (re_to_nfa s) + | Plus s t => nfa_plus (re_to_nfa s) (re_to_nfa t) + | Conc s t => nfa_conc (re_to_nfa s) (re_to_nfa t) + end. + +Lemma re_to_nfa_correct (r : regexp char) : nfa_lang (re_to_nfa r) =i r. +Proof. + elim: r => [||a|s IHs |s IHs t IHt |s IHs t IHt] w //=. + - by rewrite -dfa_to_nfa_correct inE /dfa_accept inE. + - exact: nfa_eps_correct. + - exact: nfa_char_correct. + - rewrite nfa_star_correct. exact: star_eq. + - by rewrite nfa_plus_correct /plus inE IHs IHt. + - rewrite nfa_conc_correct. exact: conc_eq. +Qed. + +Lemma re_to_nfa_size e : #|re_to_nfa e| <= 2 * re_size e. +Proof. + elim: e; rewrite /= ?card_unit ?card_bool => //. + - move => e IH. by rewrite card_option (leqRW IH) mulnS add2n. + - move => e1 IH1 e2 IH2. + by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW. + - move => e1 IH1 e2 IH2. + by rewrite card_sum (leqRW IH1) (leqRW IH2) mulnS mulnDr add2n ltnW. +Qed. + +Definition re_to_dfa := @nfa_to_dfa _ \o re_to_nfa. + +Lemma re_to_dfa_correct (r : regexp char) : dfa_lang (re_to_dfa r) =i r. +Proof. move => w. by rewrite -nfa_to_dfa_correct re_to_nfa_correct. Qed. + +Lemma re_to_dfa_size e : #|re_to_dfa e| <= 2^(2 * re_size e). +Proof. by rewrite card_set leq_pexp2l // re_to_nfa_size. Qed. + +(** Decidability of regular expression equivalence *) + +Definition re_equiv r s := dfa_equiv (re_to_dfa r) (re_to_dfa s). + +Lemma re_equiv_correct r s : reflect (r =i s) (re_equiv r s). +Proof. + apply: (iffP (dfa_equiv_correct _ _)) => H w; + move/(_ w) : H; by rewrite !re_to_dfa_correct. +Qed. + +End DFAofRE. + +(** ** Finite Automata to Regular Expressions (Kleene Construction) *) + +Section KleeneAlgorithm. + Variable char : finType. + Variable A : dfa char. + + (** We first define the transition languages between states. The + trasition languages are defined such that [w \in L^X q p] iff for + all nonempty strict prefixes [v] of [w], [delta q v \in X]. *) + + Definition L (X : {set A}) (p q : A) x := + (delta p x == q) && [forall (i : 'I_(size x) | 0 < i), delta p (take i x) \in X]. + Notation "'L^' X" := (L X) (at level 8,format "'L^' X"). + + Lemma dfa_L x y w : w \in L^setT x y = (delta x w == y). + Proof. + rewrite unfold_in. case: (_ == _) => //=. + apply/forall_inP => ? ?. by rewrite inE. + Qed. + + Lemma LP {X : {set A}} {p q : A} {x} : + reflect (delta p x = q /\ forall i, (0 < i) -> (i < size x) -> delta p (take i x) \in X) + (x \in L^X p q). + Proof. + apply: (iffP andP); case => /eqP ? H; split => //. + - move => i I1 I2. exact: (forall_inP H (Ordinal I2)). + - apply/forall_inP => [[i I1 /= I2]]; auto. + Qed. + + Lemma L_monotone (X : {set A}) (x y z : A): {subset L^X x y <= L^(z |: X) x y}. + Proof. + move => w. rewrite !unfold_in. case: (_ == _) => //. apply: sub_forall => i /=. + case: (_ < _) => //= H. by rewrite inE H orbT. + Qed. + + Lemma L_nil X x y : reflect (x = y) ([::] \in L^X x y). + Proof. apply: (iffP LP) => //=. by case. Qed. + + Lemma L_set0 p q w : + L^set0 q p w -> p = q /\ w = [::] \/ exists2 a, w = [::a] & p = dfa_trans q a. + Proof. + case/LP => <-. case: w => [|a [|b w]] H ; [by left|by right;exists a|]. + move: (H 1). do 2 case/(_ _)/Wrap => //. by rewrite inE. + Qed. + + Lemma L_split X p q z w : w \in L (z |: X) p q -> + w \in L^X p q \/ + exists w1 w2, [/\ w = w1 ++ w2, size w2 < size w, w1 \in L^X p z & w2 \in L^(z |: X) z q]. + Proof. + case/LP => H1 H2. + case: (find_minn_bound (fun i => (0 < i) && (delta p (take i w) == z)) (size w)). + - case => i [lt_w /andP [i_gt0 /eqP delta_z] min_i]; right. + exists (take i w); exists (drop i w). + have ? : 0 < size w by exact: ltn_trans lt_w. + rewrite cat_take_drop size_drop -{2}[size w]subn0 ltn_sub2l //; split => //. + + apply/LP. split => // j J1 J2. + have lt_i_j : j < i. apply: leq_trans J2 _. by rewrite size_take lt_w. + have/(H2 _ J1) : j < size w. exact: ltn_trans lt_w. + case/setU1P => [H|]; last by rewrite take_take. + move: (min_i _ lt_i_j). by rewrite negb_and J1 H eqxx. + + apply/LP. rewrite -H1 -{2}[w](cat_take_drop i) delta_cat delta_z. + split => // j J1 J2. rewrite -{1}delta_z -delta_cat -take_addn. + apply: H2; first by rewrite addn_gt0 J1 orbT. + by rewrite -[w](cat_take_drop i) size_cat size_take lt_w ltn_add2l. + - move => H; left. apply/LP. split => // i I1 I2. apply: contraTT (H2 _ I1 I2) => C. + rewrite inE negb_or C inE andbT. apply: contraNN (H _ I2) => ->. by rewrite I1. + Qed. + + Lemma L_cat (X : {set A}) x y z w1 w2 : + z \in X -> w1 \in L^X x z -> w2 \in L^X z y -> w1++w2 \in L^X x y. + Proof. + move => Hz /LP [H11 H12] /LP [H21 H22]. apply/LP. + split; first by rewrite delta_cat H11 H21. + move => i i_gt0 H. rewrite take_cat. case: (boolP (i < _)); first exact: H12. + rewrite delta_cat H11 -leqNgt => le_w1. + case: (posnP (i - size w1)) => [->|Hi]; first by rewrite take0. + apply: H22 => //. by rewrite -(ltn_add2l (size w1)) subnKC // -size_cat. + Qed. + + Lemma L_catL X x y z w1 w2 : + w1 \in L^X x z -> w2 \in L^(z |: X) z y -> w1++w2 \in L^(z |: X) x y. + Proof. move/(L_monotone z). apply: L_cat. exact: setU11. Qed. + + Lemma L_catR X x y z w1 w2 : + w1 \in L^(z |: X) x z -> w2 \in L^X z y -> w1++w2 \in L^(z |: X) x y. + Proof. move => H /(L_monotone z). apply: L_cat H. exact: setU11. Qed. + + Lemma L_star (X : {set A}) z w : w \in star (L^X z z) -> w \in L^(z |: X) z z. + Proof. + move/starP => [vv Hvv ->]. elim: vv Hvv => [_|r vv IHvv]; first exact/L_nil. + move => /= /andP [/andP [_ H1] H2]. exact: L_catL H1 (IHvv H2). + Qed. + + (** Main Lemma - L satisfies a recursive equation that can be used + to construct a regular expression *) + + Lemma L_rec (X : {set A}) x y z : + L^(z |: X) x y =i plus (conc (L^X x z) (conc (star (L^X z z)) (L^X z y))) (L^X x y). + Proof. + move => w. apply/idP/idP. + - move: w x y. apply: (size_induction (measure := size)) => w IHw x y. + move/L_split => [|[w1 [w2 [Hw' H1 Hw1 Hw2]]]]. + + rewrite inE => ->. by rewrite orbT. + + move: (IHw w2 H1 z y Hw2) Hw' => H4 -> {IHw H1}. + rewrite inE (conc_cat Hw1 _) //. + case/plusP : H4 => H; last by rewrite -[w2]cat0s conc_cat //. + move/concP : H => [w21] [w22] [W1 [W2]] /concP [w221] [w222] [W3 [W4 W5]]; subst. + by rewrite catA conc_cat // star_cat. + - case/plusP ; last exact: L_monotone. + move/concP => [w1] [w2] [-> [Hw1]] /concP [w3] [w4] [-> [Hw3 Hw4]]. + by rewrite (L_catL Hw1) // (L_catR _ Hw4) // L_star. + Qed. + + (** Construction of the regular expression *) + + Definition edges (x y : A) := \big[Plus/Void]_(a | dfa_trans x a == y) Atom a. + + Definition edgesP x y w : + reflect (exists2 a, w = [::a] & dfa_trans x a = y) (w \in edges x y). + Proof. apply: (iffP (big_plusP _ _ _)) => [|] [a] /eqP ? /eqP ?; by exists a. Qed. + + Definition R0 x y := Plus (if x == y then Eps else Void) (edges x y). + + Lemma mem_R0 w x y : + reflect (w = [::] /\ x=y \/ exists2 a, w = [::a] & dfa_trans x a = y) + (w \in R0 x y). + Proof. + apply: (iffP plusP). + - case => [| /edgesP]; auto. case e : (x == y) => // /eqP. + by rewrite (eqP e); auto. + - case => [[-> ->]|/edgesP];auto. by rewrite eqxx; auto. + Qed. + + Fixpoint R (X : seq A) (x y : A) := + if X isn't z :: X' then R0 x y else + Plus (Conc (R X' x z) (Conc (Star (R X' z z)) (R X' z y))) (R X' x y). + + Notation "'R^' X" := (R X) (at level 8, format "'R^' X"). + + Lemma L_R (X : seq A) x y : L^[set z in X] x y =i R^X x y. + Proof. + elim: X x y => [|z X' IH] x y w. + - rewrite (_ : [set z in [::]] = set0) //=. + apply/idP/mem_R0. + + move/L_set0 => [[-> ->]|[a -> ->]]; by eauto. + + move => [[-> ->]|[a -> <-]]; apply/LP => /=; split => // [[|i]] //. + - rewrite set_cons /= (L_rec _ _) -2!topredE /= /plus /= IH. + f_equal. + apply: conc_eq; first exact: IH. + apply: conc_eq; last exact: IH. + apply: star_eq. exact: IH. + Qed. + + Definition dfa_to_re : regexp char := \sigma_(x | x \in dfa_fin A) R^(enum A) (dfa_s A) x. + + Lemma dfa_to_re_correct : dfa_lang A =i dfa_to_re. + Proof. + move => w. apply/idP/big_plusP => [H|[x Hx]]. + - exists (delta_s A w) => //. by rewrite -L_R set_enum dfa_L. + - by rewrite -L_R set_enum dfa_L inE /dfa_accept => /eqP ->. + Qed. + + (** ** Size Bound for Kleene Theorem *) + + Let c := (2 * #|char|).+3. + + Lemma R0_size x y : re_size (R0 x y) <= c. + Proof. + rewrite /= [X in X + _](_ : _ = 1); last by case (_ == _). + rewrite add1n !ltnS. rewrite /edges -big_filter. + apply: leq_trans (big_plus_size (m := 1) _) _ => [//|]. + rewrite size_filter ltnS mulnC leq_mul2l /=. + apply: leq_trans (count_size _ _) _. by rewrite /index_enum -enumT cardE. + Qed. + + Fixpoint R_size_rec (n : nat) := if n is n'.+1 then 4 * R_size_rec n' + 4 else c. + + Lemma R_size x : re_size (R^(enum A) (dfa_s A) x) <= R_size_rec #|A| . + Proof. + rewrite cardE. elim: (enum A) (dfa_s A) x => [|r s IH] p q. + - exact: R0_size. + - rewrite /= 6!(addSn,addnS) addn4 !ltnS !(leqRW (IH _ _)). + by rewrite !mulSn mul0n addn0 !addnA. + Qed. + + Lemma R_size_low (n : nat) : 3 <= R_size_rec n. + Proof. elim: n => // n IH. by rewrite (leqRW IH) /= -(leqRW (leq_addr _ _)) leq_pmull. Qed. + + Lemma R_size_high n : R_size_rec n <= c * 4^(2 * n). + Proof. + elim: n => //= [|n IH]. + - by rewrite mulnS muln0 addn0. + - rewrite [in X in _^X]mulnS expnD mulnA [c * _]mulnC -mulnA. + rewrite -(leqRW IH) -[4^2]/((1+3) * 4) -mulnA mulnDl mul1n leq_add //. + by rewrite -(leqRW (R_size_low _)). + Qed. + + Lemma dfa_to_re_size : re_size dfa_to_re <= (#|A| * (c * 4 ^ (2 * #|A|)).+1).+1. + Proof. + rewrite /dfa_to_re -big_filter (leqRW (big_plus_size (m := R_size_rec #|A|)_)). + - rewrite -(leqRW (R_size_high _)) size_filter (leqRW (count_size _ _)). + by rewrite ltnS /index_enum -enumT cardE. + - move => q _. exact: R_size. + Qed. + +End KleeneAlgorithm. + +Lemma regularP (char : finType) (L : lang char) : + regular L <-T-> { e : regexp char | forall x, L x <-> x \in e}. +Proof. + split => [[A HA]|[e He]]. + - exists (dfa_to_re A) => x. by rewrite -dfa_to_re_correct. + - exists (re_to_dfa e) => x. by rewrite re_to_dfa_correct. +Qed. + +(** Closure of Regular Expressions under intersection and complement *) + +Definition Inter (char : finType) (r s : regexp char) := + dfa_to_re (dfa_op andb (re_to_dfa r) (re_to_dfa s)). + +Lemma Inter_correct (char : finType) (r s : regexp char) w : + w \in Inter r s = (w \in r) && (w \in s). +Proof. by rewrite /Inter -dfa_to_re_correct dfa_op_correct !re_to_dfa_correct. Qed. + +Definition Neg (char : finType) (r : regexp char) := + dfa_to_re (dfa_compl (re_to_dfa r)). + +Lemma Neg_correct (char : finType) (r : regexp char) w : + w \in Neg r = (w \notin r). +Proof. by rewrite /Neg -dfa_to_re_correct dfa_compl_correct !re_to_dfa_correct. Qed. + +(** ** Regular expression for images of homomorphimsms *) + +Prenex Implicits Conc. +Definition String (char : finType) (w : word char) := + foldr Conc Eps [seq Atom a | a <- w]. + +Lemma StringE (char : finType) (w : word char) : String w =i pred1 w. +Proof. + elim: w => [|a v IHv] w //=. rewrite inE /String /=. apply/concP/eqP. + - move => [w1] [w2] [e []]. set r := foldr _ _ _. + rewrite -/(re_lang r) inE e => /eqP -> H /=. + rewrite IHv inE in H. by rewrite (eqP H). + - move => e. exists [:: a]; exists v; split => //; split. + by rewrite inE. by rewrite IHv inE eqxx. +Qed. + +Section Image. + Variables (char char' : finType) (h : seq char -> seq char'). + Hypothesis h_hom : homomorphism h. + + Fixpoint re_image (e : regexp char) : regexp char' := + match e with + | Void => Void + | Eps => Eps + | Atom a => String (h [:: a]) + | Star e => Star (re_image e) + | Plus e1 e2 => Plus (re_image e1) (re_image e2) + | Conc e1 e2 => Conc (re_image e1) (re_image e2) + end. + + Lemma re_imageP e v : reflect (image h (re_lang e) v) (v \in re_image e). + Proof. + elim: e v => [||a|e IHe|e1 IHe1 e2 IHe2|e1 IHe1 e2 IHe2] v /=. + - rewrite inE; constructor. move => [u]. by case. + - rewrite inE; apply: (iffP eqP) => [-> |[w] [] /eqP -> <-]; last exact: h0. + exists [::]; by rewrite ?h0. + - rewrite StringE. apply: (iffP eqP) => [->|[w /=]]. + + exists [::a] => //. by rewrite /atom inE. + + by rewrite /atom inE => [[]] /eqP -> <-. + - apply: (iffP idP) => [/starP [vv] /allP Hvv dev_v|]. + have {Hvv IHe} Hvv v' : v' \in vv -> image h (re_lang e) v'. + by move => /Hvv /= /andP [_ /IHe]. + subst v. elim: vv Hvv => [|v vv IHvv] Hvv /=; first by exists [::]; rewrite ?h0. + case: (Hvv v (mem_head _ _)) => w [Hw1 Hw2]. + case/all1s: Hvv => Hv /IHvv [ww [Hww1 Hww2]]. + exists (w++ww); split; by [exact: star_cat | rewrite h_hom Hw2 Hww2]. + + case => w [] /starP [ww] /allP Hww1 -> <-. rewrite h_flatten //. + apply: starI => v' /mapP [w' /Hww1 /= /andP [_ Hw' ->]]. + apply/IHe. by exists w'. + - apply: (iffP orP). + + case => [/IHe1 | /IHe2] [w] [] H <-. + exists w => //. by rewrite /plus inE (_ : w \in re_lang e1). + exists w => //. by rewrite /plus inE (_ : w \in re_lang e2) ?orbT. + + case => w []. case/orP => H <-; [left; apply/IHe1 |right; apply/IHe2]; by exists w. + - apply: (iffP idP). + + case/concP => v1 [v2] [e] [/IHe1 [w [Hw1 Hw2]] /IHe2 [w' [Hw1' Hw2']]]. + exists (w++w'); split; first exact: conc_cat. + by rewrite h_hom e Hw2 Hw2'. + + case => w [] /concP [w1] [w2] [-> [H1 H2 <-]]. rewrite h_hom. + apply: conc_cat; [apply/IHe1|apply/IHe2]. by exists w1. by exists w2. + Qed. + +End Image. + +Lemma im_regular (char char' : finType) (h : word char -> word char') L : + homomorphism h -> regular L -> regular (image h L). +Proof. + move => hom_h /regularP [e He]. apply/regularP. exists (@re_image _ _ h e) => w. + transitivity (image h (re_lang e) w); first exact: image_ext. + exact: rwP (re_imageP _ _ _). +Qed. + + +(** ** Regular Expression for word reversal *) + +Fixpoint Rev (char : finType) (e : regexp char) := + match e with + | Star e => Star (Rev e) + | Plus e1 e2 => Plus (Rev e1) (Rev e2) + | Conc e1 e2 => Conc (Rev e2) (Rev e1) + | _ => e + end. + +Lemma Rev_correct (char : finType) (e : regexp char) w : + w \in Rev e = (rev w \in e). +Proof. + elim: e w => [||a|e IH|e1 IH1 e2 IH2|e1 IH1 e2 IH2] w //. + - rewrite !inE. apply/eqP/idP; first by move->. + elim/last_ind: w => //= s a _. by rewrite rev_rcons. + - rewrite !inE. apply/eqP/eqP; first by move->. + do 2 elim/last_ind: w => //= w ? _. by rewrite !rev_rcons. + - rewrite /=; apply/idP/idP; case/starP => vv /allP /= H. + + move->. rewrite rev_flatten. apply: starI => v'. + rewrite mem_rev => /mapP [v V1 ->]. rewrite -IH. by case/andP: (H _ V1). + + rewrite -{2}[w]revK => ->. rewrite rev_flatten. apply: starI => v'. + rewrite mem_rev => /mapP [v V1 ->]. rewrite IH revK. by case/andP: (H _ V1). + - by rewrite /= !inE -!/(re_lang _) IH1 IH2. + - rewrite /=. apply/concP/concP => [] [w1] [w2]; rewrite -!/(re_lang _). + + move => [-> [A B]]. exists (rev w2); exists (rev w1). by rewrite rev_cat -IH1 -IH2. + + rewrite -{2}[w]revK. move => [-> [A B]]. exists (rev w2); exists (rev w1). + by rewrite rev_cat IH1 IH2 !revK. +Qed. + +Lemma regular_rev (char : finType) (L : lang char) : + regular L -> regular (fun x => L (rev x)). +Proof. case/regularP => e H. apply/regularP. exists (Rev e) => x. by rewrite Rev_correct. Qed. diff --git a/theories/setoid_leq.v b/theories/setoid_leq.v new file mode 100644 index 0000000..f813563 --- /dev/null +++ b/theories/setoid_leq.v @@ -0,0 +1,61 @@ +(* Author: Christian Doczkal *) +(* Distributed under the terms of CeCILL-B. *) + +From Coq Require Import Basics Setoid Morphisms. +From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** ** Setoid Rewriting with Ssreflec's boolean inequalities. *) +(** Solution suggested by Georges Gonthier (ssreflect mailinglist @ 18.12.2016) *) + +(** Preorder and Instances for bool *) + +Inductive leb a b := Leb of (a ==> b). + +Lemma leb_eq a b : leb a b <-> (a -> b). +Proof. move: a b => [|] [|]; firstorder. Qed. + +Instance: PreOrder leb. +Proof. split => [[|]|[|][|][|][?][?]]; try exact: Leb. Qed. + +Instance: Proper (leb ==> leb ==> leb) andb. +Proof. move => [|] [|] [A] c d [B]; exact: Leb. Qed. + +Instance: Proper (leb ==> leb ==> leb) orb. +Proof. move => [|] [|] [A] [|] d [B]; exact: Leb. Qed. + +Instance: Proper (leb ==> impl) is_true. +Proof. move => a b []. exact: implyP. Qed. + +(** Instances for le *) + +Instance: Proper (le --> le ++> leb) leq. +Proof. move => n m /leP ? n' m' /leP ?. apply/leb_eq => ?. eauto using leq_trans. Qed. + +Instance: Proper (le ==> le ==> le) addn. +Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_add. Qed. + +Instance: Proper (le ==> le ==> le) muln. +Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_mul. Qed. + +Instance: Proper (le ++> le --> le) subn. +Proof. move => n m /leP ? n' m' /leP ?. apply/leP. exact: leq_sub. Qed. + +Instance: Proper (le ==> le) S. +Proof. move => n m /leP ?. apply/leP. by rewrite ltnS. Qed. + +Instance: RewriteRelation le. + +(** Wrapper Lemma to trigger setoid rewrite *) +Definition leqRW m n : m <= n -> le m n := leP. + +(** Testing *) + +Lemma T1 : forall x y, x <= y -> x + 1 <= y + 1. +Proof. move => x y h. by rewrite (leqRW h). Qed. + +Lemma T2 : forall x y, x <= y -> (x + 1 <= y + 1) && true. +Proof. move => x y h. by rewrite (leqRW h) andbT. Qed. \ No newline at end of file diff --git a/theories/shepherdson.v b/theories/shepherdson.v new file mode 100644 index 0000000..50b5c5e --- /dev/null +++ b/theories/shepherdson.v @@ -0,0 +1,384 @@ +(* Author: Christian Doczkal *) +(* Distributed under the terms of CeCILL-B. *) +From Coq Require Import Omega. +From mathcomp Require Import all_ssreflect. +Require Import misc setoid_leq languages dfa myhill_nerode two_way. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** ** Shepherdson Construction for 2NFAs *) + +(** Preliminaries *) + +Lemma contraN (b : bool) (P : Prop) : b -> ~~ b -> P. by case b. Qed. + +Lemma inord_inj n m : n <= m -> injective (@inord m \o @nat_of_ord n.+1). +Proof. + move => Hnm k k' /= /(f_equal (@nat_of_ord _)) E. apply/ord_inj. + rewrite !inordK // in E; exact: leq_trans (ltn_ord _) _. +Qed. + +(** Lemmas for character lookups on composite words *) + +Lemma tnthL (T:eqType) (x z : seq T) (i : 'I_(size x)) (j : 'I_(size (x++z))) : + i = j :> nat -> tnth (in_tuple x) i = tnth (in_tuple (x++z)) j. +Proof. + move => e. pose a := tnth (in_tuple x) i. + by rewrite !(tnth_nth a) /= -e nth_cat ltn_ord. +Qed. + +Lemma tnthR (T:eqType) (x z : seq T) (i : 'I_(size z)) (j : 'I_(size (x++z))) : + size x + i = j -> tnth (in_tuple z) i = tnth (in_tuple (x++z)) j. +Proof. + move => e. pose a := tnth (in_tuple z) i. + by rewrite !(tnth_nth a) /= -e nth_cat ltnNge leq_addr /= addKn. +Qed. + +(** Wrapper for omega that uses ssreflects operators on [nat] *) + +Ltac norm := rewrite ?(size_cat,cats0); simpl in *. +Ltac normH := match goal with [ H : is_true (_ <= _) |- _] => move/leP : H end. +Ltac somega := + try (try (apply/andP; split); apply/leP; repeat normH; norm ; rewrite ?addnE /addn_rec ; intros; omega). + +Section NFA2toAFA. + + Variables (char : finType) (M : nfa2 char). + Implicit Types (x y z w v : word char). + + (** We fix some 2NFA [M]. Instead of directly defining a DFA for [M], we + instantiate the construction of DFAs from classifiers. This means that we have + to give a finite type [Q] and define a function [T : word char -> Q] which is + right congruent and refines the language of [M]. We take [Q] to be the type of + tables or black-box results for [M]. *) + + Definition table := ({set M} * {set M * M})%type. + + (** We define the mapping from [word char] to [table] using a restriction of the + step relation. The stop relation [srel k x] behaves like [step x] except that + it does not continue if the head is at position [k]. *) + + Definition srel (k:nat) x (c d : nfa2_config M x) := (step M x c d) && (k != c.2). + Arguments srel : clear implicits. + + Lemma srel_step k w : subrel (srel k w) (step M w). + Proof. by move => c d /= => /andP[->]. Qed. + + Lemma srel_step_max x : srel (size x).+2 x =2 step M x. + Proof. move => c d /=. by rewrite /srel neq_ltn ltn_ord orbT andbT. Qed. + + Definition Tab x : table := + ([set q | connect (srel (size x).+1 x) (nfa2_s M, ord1) (q,ord_max)], + [set pq | connect (srel (size x).+1 x) (pq.1,inord (size x)) (pq.2,ord_max)]). + + (** To show that [Tab] is right-congruent and refines the language of [M], we + need to make use of the fact that [M] moves its head only one step at a + time. In particular, this allows us to split runs starting with head position + [i] and ending at head position [j] at any position [k] in beteen. *) + + Lemma srelLR k x p i q j : srel k x (p,i) (q,j) -> + j.+1 = i :> nat \/ j = i.+1 :> nat. + Proof. move/srel_step. case/orP => /andP [_ /eqP ->]; tauto. Qed. + + Lemma srel1 k x c d : srel k x c d -> d.2 <= c.2.+1. + Proof. move: c d => [p i] [q j] /srelLR [<-|->] //=. by somega. Qed. + + Lemma srelSr k' k x (c d : nfa2_config M x) : c.2 < k -> + srel k x c d = srel (k+k') x c d. + Proof. move => lt_k. by rewrite /srel !neq_ltn ltn_addr lt_k ?orbT. Qed. + + Lemma srelS k x p q (i j : pos x) m : i <= k -> + connect (srel k x) (p,i) (q,j) -> connect (srel (k+m) x) (p,i) (q,j). + Proof. + move => H /connectP [cs]. + elim: cs p i H => [/= p i H _ [-> ->] //|[p' i'] cs IH p i H /= /andP [s pth] l]. + have Hk: i < k. case/andP : s => _ /= s. by rewrite ltn_neqAle H eq_sym s. + apply: (connect_trans (y := (p',i'))) (connect1 _) _; first by rewrite -srelSr. + apply: IH => //. move/srel1 : s Hk => /= s. exact: leq_trans. + Qed. + + Lemma srel_mid_path (k k' : nat) x (i j : pos x) (p q : M) cs : + i <= k <= j -> path (srel k' x) (p,i) cs -> (q,j) = last (p,i) cs -> + exists p' cl cr, [/\ cs = cl ++ cr, (p',inord k) = last (p,i) cl & path (srel k x) (p,i) cl]. + Proof. + move: cs p i. apply: (size_induction (measure := size)) => cs IH p i /andP [H1 H2]. + case: (boolP (i == k :> nat)) => Ei. + - exists p. exists [::]. exists cs. by rewrite -[i]inord_val (eqP Ei). + - destruct cs as [|c cs] => [_ /= [_ E]|/= /andP [s p1] p2]; subst. + + by rewrite eqn_leq H1 H2 in Ei. + + have Hi: i < k by rewrite ltn_neqAle Ei H1. + have mid: c.2 <= k <= j by rewrite (leq_trans (srel1 s)). + case: (IH cs _ c.1 _ mid) ; rewrite -?surjective_pairing //. + move => p' [cl] [cr] [C1 C2 C3]. exists p'. exists (c::cl). exists cr. + rewrite /= -C1 C3 andbT. split => //. rewrite /srel /= eq_sym Ei andbT. + exact: srel_step s. + Qed. + + Lemma srel_mid (k k' : nat) x (i j : pos x) (p q : M) : i <= k <= j -> k <= k' -> + reflect (exists2 p', connect (srel k x) (p,i) (p',inord k) & connect (srel k' x) (p',inord k) (q,j)) + (connect (srel k' x) (p,i) (q,j)). + Proof. + move => H X. apply: (iffP idP). + - case/connectP => cs c1 c2. case: (srel_mid_path H c1 c2) => [p'] [cl] [cr] [Ecs L C]. + subst cs. rewrite cat_path last_cat -L in c1 c2. case/andP : c1 => ? c1. exists p'. + + apply/connectP. by exists cl. + + apply/connectP. by exists cr. + - case/andP: H => H1 H2 [p']. move/(srelS (k'-k) H1). rewrite subnKC //. exact: connect_trans. + Qed. + + Lemma readL x z (p:M) (k : pos x) : k != (size x).+1 :> nat -> + read p (inord k : pos (x++z)) = read p k. + Proof. + move => Hk. rewrite /read. case: (ord2P k) => [/eqP->|E|i Hi]. + - by rewrite /= -inord0 ord2P0. + - apply: contraN Hk. by rewrite (eqP E). + - have oi : i < size (x++z) by rewrite size_cat ltn_addr. + have H_eq: (Ordinal oi).+1 = (inord k : pos (x++z)). by rewrite -Hi inordK // ; somega. + by rewrite (ord2PC H_eq) -(tnthL (i := i)). + Qed. + + Section CompositeWord. + Variables (x z : word char). + + (** We first show that runs on [x] that do not cross the boundary between + [x] and [z] do not depend on [z]. *) + + Lemma srelL (i j : pos x) p q : + srel (size x).+1 x (p,i) (q,j) = srel (size x).+1 (x++z) (p,inord i) (q,inord j). + Proof. + case: (boolP (i == (size x).+1 :> nat)) => Hi. + - rewrite /srel (eqP Hi) /= inordK ?eqxx //= ?andbF //; somega. + - have Hi' : i < (size x).+1. by rewrite ltn_neqAle Hi -ltnS ltn_ord. + rewrite /srel /step readL // !inordK //; somega. + move: (ltn_ord j) => ?. somega. + Qed. + + Lemma runL (i j : pos x) p q : + connect (srel (size x).+1 x) (p,i) (q,j) = + connect (srel (size x).+1 (x++z)) (p,inord i) (q,inord j). + Proof. + pose f (c : nfa2_config M x) : nfa2_config M (x ++ z) := (c.1, inord c.2). + rewrite -[(p,inord i)]/(f (p,i)) -[(q,inord j)]/(f (q,j)). + apply: connect_transfer => //. + - move => {p q i j} [p i] [q j] /= [->] /inord_inj. + case/(_ _)/Wrap => [|->//]. somega. + - move => [? ?] [? ?]. rewrite /f /=. exact: srelL. + - move => {p q i j} [p i] [q j] step. exists (q,inord j). + rewrite /f /= inordK ?inord_val //. move: (srel1 step) => /= Hs. + case/andP : step => /= _ Hi. rewrite (leqRW Hs) ltn_neqAle eq_sym Hi /=. + by rewrite inordK ltnS ?leq_ord // (leqRW (leq_ord i)) ltnS size_cat leq_addr. + Qed. + + (** This entails, that the behaviour of [M] starting from the endpoints of + [x] is also independent of [z]. Note that the direction from right to left + makes use of lemma [term_uniq] *) + + Lemma Tab1P q : q \in (Tab x).1 + <-> connect (srel (size x).+1 (x++z)) (nfa2_s M,ord1) (q,inord (size x).+1). + Proof. by rewrite /Tab inE runL /= -[ord1]inord_val. Qed. + + Lemma Tab2P p q : (p,q) \in (Tab x).2 + <-> connect (srel (size x).+1 (x++z)) (p,inord (size x)) (q,inord (size x).+1). + Proof. by rewrite inE runL /= inordK. Qed. + + (** Dually, steps on the right of [x++z] do not depend on [x], if they do not + cross the boundary between [x] and [z]. *) + + Lemma readR (q:M) k : k != 0 -> k < (size z).+2 -> + read q (inord k : pos z) = read q (inord (size x + k) : pos (x++z)). + Proof. + move => Hk0 Hk. rewrite /read. case: (ord2P _) => [H|H|i Hi]. + - apply: contraN Hk0. + move/eqP/(f_equal (@nat_of_ord _)) : H => /=. by rewrite inordK // => ->. + - by rewrite -[k](@inordK (size z).+1) ?(eqP H) //= addnS -size_cat -inord_max ord2PM. + - have Hi' : size x + i < size (x ++ z) by rewrite size_cat ltn_add2l. + have X: (Ordinal Hi').+1 = (inord (size x + k) : pos (x ++ z)). + by rewrite /= -addnS Hi !inordK //; somega. + by rewrite (ord2PC X) -(tnthR (i := i)). + Qed. + + Lemma srelR (m k k' : nat) p p' : k != 0 -> k < (size z).+2 -> k' < (size z).+2 -> + srel ((size x).+1 + m) (x++z) (p,inord (size x + k)) (p',inord (size x + k')) + = srel m.+1 z (p,inord k) (p',inord k'). + Proof. + move => Hk0 Hk Hk'. rewrite /srel /= !inordK ?addSnnS ?eqn_add2l //; somega. + case: (_ != _); rewrite ?andbT ?andbF // /step -?readR //. + rewrite !inordK //; somega. by rewrite -!addnS !eqn_add2l. + Qed. + + Lemma srelRE m k p c : k < (size z).+2 -> k != 0 -> + srel m (x++z) (p,inord (size x + k)) c -> + exists q k', k' < (size z).+2 /\ c = (q,inord (size x + k')). + Proof. + move: k c => [//|k] [q j] Hk _ /srelLR [/eqP C|/eqP C]; + exists q; rewrite inordK addnS ?eqSS in C; somega. + - exists k. by rewrite ltnW // -[j]inord_val (eqP C). + - exists k.+2. rewrite !addnS -[j]inord_val (eqP C). split => //. + rewrite eqn_leq in C. case/andP : C => _ C. + move: (leq_ltn_trans C (ltn_ord j)). + by rewrite size_cat -!addnS leq_add2l. + Qed. + + End CompositeWord. + + (** The main lemma used both in the proof of right-congruence and language + refinement states that as long as the black-box results for [x] and [y] + agreee, runs starting and ending on the right of composite words [x++z] and + [y++z] behave the same even if they cross the boundaries. *) + + Lemma runR x y z p q (i j: nat) k : + Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 -> + connect (srel ((size x).+1 + k) (x++z)) (p,inord (size x + i)) (q,inord (size x + j)) -> + connect (srel ((size y).+1 + k) (y++z)) (p,inord (size y + i)) (q,inord (size y + j)). + Proof. + move => Tab_eq Hi /andP [Hj0 Hj]. case/connectP => cs. move: cs i Hi p. + apply: (size_induction (measure := size)) => /= cs IH i Hi p. + case: (boolP (i == 0)) => Hi0. + - rewrite (eqP Hi0) !addn0 => p1 p2. + case: (srel_mid_path (k := (size x).+1) _ p1 p2); try solve [rewrite inordI; somega]. + apply/andP; split; rewrite !inordK; somega. move => p' [cl] [cr] [Ecs Lcl Pcl]. + apply/(@srel_mid (size y).+1) ; try solve [rewrite !inordK; somega|rewrite -addn1; somega]. + + exists p'. apply/Tab2P. rewrite -Tab_eq. apply/Tab2P. by apply/connectP; exists cl. + + subst cs. rewrite -[_.+1 as X in inord X]addn1. + apply: (IH cr) => {IH} //; somega. + * destruct cl as [|c cs]; simpl in *. case: Lcl => _. + -- move/(f_equal (@nat_of_ord _)); rewrite ?inordK; intros; somega. + -- by rewrite[size (cs ++ cr)]size_cat -addnS leq_addl. + * rewrite cat_path -Lcl addn1 in p1 *. by case/andP : p1. + * by rewrite p2 last_cat -Lcl addn1. + - destruct cs as [|c cs]; simpl in *. + + move => _ [-> /(f_equal (@nat_of_ord _))/eqP]. + rewrite !inordK ?eqn_add2l ?size_cat -?addnS ?leq_add2l // => /eqP ->. + exact: connect0. + + case/andP => P1 P2 L. case/srelRE: (P1) => // p' [ip] [Hip ?]; subst. + rewrite srelR // -(@srelR y z) // in P1. apply: connect_trans (connect1 P1) _. + exact: (IH cs). + Qed. + + (** Variant of the lemma above, that generales equality subgoals *) + Lemma runR_eq x y z p q (i j: nat) k xk xi xj yk yi yj : + Tab x = Tab y -> i <= (size z).+1 -> 0 < j <= (size z).+1 -> + xk = (size x).+1 + k -> xi = size x + i -> xj = size x + j -> + yk = (size y).+1 + k -> yi = size y + i -> yj = size y + j -> + connect (srel xk (x++z)) (p,inord xi) (q,inord xj) -> + connect (srel yk (y++z)) (p,inord yi) (q,inord yj). + Proof. move => ? ? ? ? ? ? ? ? ?. subst. exact: runR. Qed. + + Lemma Tab_refines : refines (nfa2_lang M) Tab. + Proof. + move => x y E. + wlog suff W: x y E / (x \in nfa2_lang M) -> (y \in nfa2_lang M). + { by apply/idP/idP; exact: W. } + case/exists_inP => f Hq1 Hq2. apply/exists_inP; exists f => //. move: Hq2. + rewrite -[x]cats0 -[y]cats0 -!(eq_connect (@srel_step_max _)). + case/(@srel_mid (size x).+1); somega => q /Tab1P q1 q2. + apply/(@srel_mid (size y).+1); somega. + - exists q. apply/Tab1P. by rewrite -E. + - move: q2 => {q1}. rewrite !inord_max. + apply: (runR_eq (i := 1) (j := 1) (k := 1)); rewrite ?addn1 ?cats0 //=. + Qed. + + Lemma Tab_rc : right_congruent Tab. + Proof. + move => x y a E. + have Tab2 : (Tab (x ++ [:: a])).2 = (Tab (y ++ [:: a])).2. + { apply/setP => [[p q]]. rewrite /Tab !inE /= !inord_max. + apply/idP/idP; apply: (runR_eq (i := 1) (j := 2) (k := 1)); by rewrite ?size_cat ?addn1 ?addn2. } + suff ?: (Tab (x ++ [:: a])).1 = (Tab (y ++ [:: a])).1 by congr pair. + apply/setP => q /=. rewrite !inE. + pose C x := connect (srel (size (x ++ [:: a])).+1 (x ++ [:: a])) (nfa2_s M, ord1) (q, ord_max). + wlog suff W: x y E Tab2 / C x -> C y; [by apply/idP/idP; exact: W|]. + case/(@srel_mid (size x).+1); somega => p /Tab1P p1 p2. + apply/(@srel_mid (size y).+1); somega. + exists p; first by apply/Tab1P; rewrite -E. move: p2. + rewrite -![_.+1 as X in inord X]addn1 -[1]/(size [:: a]) -!size_cat. + rewrite !(@runL _ [::]) !inordK; somega. move/Tab2P => p2. by apply/Tab2P; rewrite -Tab2. + Qed. + + Definition nfa2_to_classifier : classifier_for (nfa2_lang M) := + {| cf_classifier := Classifier Tab; cf_congruent := Tab_rc; cf_refines := Tab_refines |}. + + Theorem nfa2_to_dfa : + { A : dfa char | dfa_lang A =i nfa2_lang M & #|A| <= 2 ^ (#|M| ^ 2 + #|M|) }. + Proof. + exists (classifier_to_dfa (nfa2_to_classifier)); first exact: classifier_to_dfa_correct. + rewrite card_sub (leqRW (max_card _)) [#|_|]/=. + by rewrite card_prod expnD mulnC leq_mul //= card_set // card_prod -mulnn. + Qed. + +End NFA2toAFA. + +(** If M is determinististic, the size bound on the constructed 2DFA improves + to [(#|M|.+1)^(#|M|.+1)] *) + +Arguments srel [char] M k x c d. + +(** ** Imropoved Bound for Translation of 2DFAs to DFAs *) + +Section DFA2toAFA. + Variables (char : finType) (M : dfa2 char). + + Lemma functional_srel k w : functional (srel M k w). + Proof. apply: functional_sub (@srel_step _ _ k w). exact: step_fun. Qed. + + Lemma term_srel k x q (H: k < (size x).+2) : terminal (srel M k x) (q,inord k). + Proof. move => c /=. by rewrite /srel inordK // ?eqxx /= andbF. Qed. + + Lemma Tab1_uniq x p q : p \in (Tab M x).1 -> q \in (Tab M x).1 -> p = q. + Proof. + rewrite !inE => H1 H2. suff: (p,@ord_max (size x).+1) = (q,ord_max) by case. + apply: term_uniq H1 H2; rewrite ?inord_max; auto using term_srel, functional_srel. + Qed. + + Lemma Tab2_functional x p q r : (p,q) \in (Tab M x).2 -> (p,r) \in (Tab M x).2 -> q = r. + Proof. + rewrite !inE => /= H1 H2. suff: (q,@ord_max (size x).+1) = (r,ord_max) by case. + apply: term_uniq H1 H2; rewrite ?inord_max; auto using term_srel, functional_srel. + Qed. + + Definition Tab' := image_fun (@Tab_rc _ M). + + Lemma image_rc : right_congruent Tab'. + Proof. move => x y a /Sub_eq E. apply/Sub_eq. exact: Tab_rc. Qed. + + Lemma image_refines : refines (nfa2_lang M) Tab'. + Proof. move => x y /Sub_eq E. exact: Tab_refines. Qed. + + Definition dfa2_to_myhill := + {| cf_classifier := Classifier Tab'; + cf_congruent := image_rc; + cf_refines := image_refines |}. + + Lemma det_range : #|{:image_type (@Tab_rc _ M)}| <= (#|M|.+1)^(#|M|.+1). + Proof. + pose table' := (option M * {ffun M -> option M})%type. + apply: (@leq_trans #|{: table'}|); last by rewrite card_prod card_ffun !card_option expnS. + pose f (x : image_type (@Tab_rc _ M)) : table' := + let (b,_) := x in ([pick q | q \in b.1],[ffun p => [pick q | (p,q) \in b.2]]). + suff : injective f by apply: card_leq_inj. + move => [[a1 a2] Ha] [[b1 b2] Hb] [E1 /ffunP E2]. apply/Sub_eq. + move: Ha Hb => /dec_eq /= [x Hx] /dec_eq [y Hy]. + rewrite [Tab M x]surjective_pairing [Tab M y]surjective_pairing !xpair_eqE in Hx Hy. + case/andP : Hx => /eqP ? /eqP ?. case/andP : Hy => /eqP ? /eqP ?. subst. f_equal. + - apply/setP => p. case: (pickP _) E1 => q1; case: (pickP _) => q2 //; last by rewrite q1 q2. + move => {E2} H1 H2 [?]; subst. + wlog suff S : p x y H1 H2 / (p \in (Tab M x).1) -> (p \in (Tab M y).1). + { apply/idP/idP; exact: S. } + move => H. by rewrite (@Tab1_uniq x p q2). + - apply/setP => [[p q]]. move: E2 {E1} => /(_ p). rewrite !ffunE. + case: (pickP _) => r1; case: (pickP _) => r2 //; last by rewrite r1 r2. + move => H1 H2 [?]; subst. apply/idP/idP => ?. + + by rewrite (@Tab2_functional x p q r2). + + by rewrite (@Tab2_functional y p q r2). + Qed. + + Theorem dfa2_to_dfa : + { A : dfa char | dfa_lang A =i dfa2_lang M & #|A| <= (#|M|.+1)^(#|M|.+1) }. + Proof. + exists (classifier_to_dfa (dfa2_to_myhill)); first exact: classifier_to_dfa_correct. + rewrite card_sub (leqRW (max_card _)). exact: det_range. + Qed. + +End DFA2toAFA. diff --git a/theories/two_way.v b/theories/two_way.v new file mode 100644 index 0000000..5537d12 --- /dev/null +++ b/theories/two_way.v @@ -0,0 +1,221 @@ +(* Authors Christian Doczkal and Jan-Oliver Kaiser *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages dfa regexp myhill_nerode. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** * Two Way Automata *) + +(** ** Preliminaries + +We want to represent configurations of two-way automata as pairs of states and +positions on the input word extended with left and right markers. That is +positions will be of type ['I_n.+2] with [n] beeing the length of the input +word. We need some facts about finite ordinals of this form. + +We define a three-way case analysis on ['I_n.+2]. If [i:'I_n.+2] is +neither [ord0] nor [ord_max], then we can cast it (with offset 1) to +['I_n]. This is used for looking up charaters of an input word *) + +Inductive ord2_spec n (m : 'I_n.+2) := +| Ord20 of m == ord0 +| Ord2M of m == ord_max +| Ord2C (i : 'I_n) of i.+1 = m. + +Arguments Ord20 [n m] _. +Arguments Ord2M [n m] _. +Arguments Ord2C [n m i] _. + +Lemma ord2P n (m : 'I_n.+2) : ord2_spec m. +Proof. + case: (unliftP ord0 m) => [j Hj|/eqP]; last exact: Ord20. + case: (unliftP ord_max j) => [i Hi|Hj2]; last apply: Ord2M. + * apply: (@Ord2C _ m i). by rewrite Hj Hi lift0 lift_max. + * rewrite Hj Hj2. apply/eqP. apply/ord_inj. by rewrite lift0. +Qed. + +Lemma ord2P0 n : ord2P (@ord0 n.+1) = Ord20 (eqxx _). +Proof. case: (ord2P (@ord0 n.+1)) => //= H. congr Ord20. exact: eq_irrelevance. Qed. + +Lemma ord2PM n : ord2P (@ord_max n.+1) = Ord2M (eqxx _). +Proof. + case: (ord2P (@ord_max n.+1)) => //= [H|i Hi]. + - apply: f_equal. exact: eq_irrelevance. + - move: (ltn_ord i). move: (Hi) => Hi2. move: Hi => [] ->. by rewrite ltnn. +Qed. + +Lemma ord2PC n {i : 'I_n.+2} {i' : 'I_n} (p : i'.+1 = i) : ord2P i = Ord2C p. +Proof. + case: (ord2P i) => [Hi|Hi|j' p']. + - exfalso. move/eqP: Hi => Hi. by rewrite Hi in p. + - exfalso. move:Hi. apply/negP. apply: contra_eqN p => /eqP->. + rewrite eqn_leq negb_and -[~~ (ord_max <= _)]ltnNge [_.+1 < _](_ : _ = true) ?orbT //. + exact: leq_ltn_trans (ltn_ord _) _. + - have ?: i' = j'. apply: ord_inj. apply/eqP. by rewrite -eqSS p p'. subst. + by rewrite (eq_irrelevance p p'). +Qed. + +(** ** Definition of 2NFAs and their languages. + +We need to call 2NFAs [nfa2] since names may not begin with numbers. *) + +Section NFA2. + Variable char : finType. + + Definition dir := bool. + Definition L := true. + Definition R := false. + + Record nfa2 := Nfa2 { + nfa2_state :> finType; + nfa2_s : nfa2_state; + nfa2_f : {set nfa2_state}; + nfa2_trans : nfa2_state -> char -> {set nfa2_state * dir}; + nfa2_transL : nfa2_state -> {set nfa2_state}; + nfa2_transR : nfa2_state -> {set nfa2_state}}. + + Variables (A : nfa2) (x : word char). + + Definition tape := in_tuple x. + Definition pos := ('I_(size x).+2)%type. + Definition nfa2_config := (A * pos)%type. + + Definition read (q:A) (n : pos) : {set (A * dir)} := + match ord2P n with + | Ord20 _ => setX (nfa2_transL q) [set R] + | Ord2M _ => setX (nfa2_transR q) [set L] + | Ord2C m' _ => nfa2_trans q (tnth tape m') + end. + + Definition step (c d : nfa2_config) := + let: ((p,i),(q,j)) := (c,d) in + ((q,R) \in read p i) && (j == i.+1 :> nat) + || ((q,L) \in read p i) && (j.+1 == i :> nat). + + Definition nfa2_lang := [exists (q | q \in nfa2_f A), connect step (nfa2_s A,ord1) (q,ord_max)]. +End NFA2. + +Arguments step [char] A x c d. +Prenex Implicits step. + + +(** ** Definition of 2DFAs as deterministic 2NFAs *) + +Section DFA2. + Variable char : finType. + + Record deterministic (M : nfa2 char) : Prop := + { detC : forall (p:M) a, #|nfa2_trans p a| <= 1; + detL : forall (p:M), #|nfa2_transL p| <= 1; + detR : forall (p:M), #|nfa2_transR p| <= 1}. + + Record dfa2 := DFA2 { nfa2_of :> nfa2 char ; dfa2_det : deterministic nfa2_of }. + Definition dfa2_lang := nfa2_lang. + + Variable M : dfa2. + + Lemma cards_lt1 (T : finType) (A : {set T}) : #|A| <= 1 -> A = set0 \/ exists x, A = [set x]. + Proof. + move => H. case (posnP #|A|) => H'. + - left. exact:cards0_eq. + - right. apply/cards1P. by rewrite eqn_leq H H'. + Qed. + + Lemma read1 x (p:M) (j:pos x) : read p j = set0 \/ exists s : M * dir, read p j = [set s]. + Proof. + rewrite /read. + case: (ord2P _) => [||i] _;apply cards_lt1; rewrite ?cardsX ?cards1 ?muln1; + by auto using detL, detC, detR, dfa2_det. + Qed. + + Lemma step_fun x : functional (step M x). + Proof. + have lr: ((R == L = false)*(L == R = false))%type by done. + move => [p i] [q j] [r k]. rewrite /step. + case: (read1 p i) => [ -> |[[q' [|]] -> ]]; first by rewrite !inE. + - rewrite !inE !xpair_eqE -/L -/R !lr !eqxx !andbT !andbF /=. + move => /andP [/eqP -> /eqP A] /andP [/eqP -> /eqP B]. + f_equal. apply ord_inj. apply/eqP. by rewrite -eqSS A B. + - rewrite !inE !xpair_eqE -/L -/R !lr !eqxx !andbT !andbF !orbF /=. + move => /andP [/eqP -> /eqP A] /andP [/eqP -> /eqP B]. + f_equal. apply ord_inj. apply/eqP. by rewrite -eqSS A B. + Qed. + +End DFA2. + +(** ** Simulation of DFAs *) + + + +Section DFAtoDFA2. + Variables (char : finType) (A : dfa char). + + Definition nfa2_of_dfa : nfa2 char := + {| nfa2_s := dfa_s A; + nfa2_f := [set q in dfa_fin A]; + nfa2_trans q a := [set (dfa_trans q a,R)]; + nfa2_transL q := [set dfa_s A]; (* Never reached *) + nfa2_transR q := set0 + |}. + + Lemma drop_accept (w : word char) (i : 'I_(size w)) (q : A) : + drop i w \in dfa_accept q = (drop i.+1 w \in dfa_accept (dfa_trans q (tnth (tape w) i))). + Proof. + case: w i q => [[//]|a w [m Hm] q]. rewrite [drop]lock (tnth_nth a) /= -lock. + elim: {w} (a :: w) m Hm q => [|b w IHw [|m] Hm q]; first by case. + by rewrite drop0 drop1. exact: IHw. + Qed. + + Variable (w : word char). + Let n := size w. + + Lemma nfa2_of_aux (q:A) i : i < (size w).+1 -> + ((drop i w) \in dfa_accept q) -> + [exists f in nfa2_f nfa2_of_dfa, connect (step nfa2_of_dfa w) (q,inord i.+1) (f,ord_max)]. + Proof. + move eq_m : (n - i) => m. elim: m q i eq_m => [|m IHm] q i /eqP H1 H2. + - have/eqP -> : i == (size w). by rewrite eqn_leq -ltnS H2 -subn_eq0 H1. + rewrite drop_size unfold_in -inord_max /= => F. apply/existsP;exists q. rewrite inE F. exact: connect0. + - move => H. have Hi : i < size w. + { rewrite ltn_neqAle -ltnS H2 andbT. apply: contraTN H1 => /eqP->. by rewrite subnn. } + have Hm : n - i.+1 = m by apply/eqP;rewrite subnS (eqP H1). + move/(_ (dfa_trans q (tnth (tape w) (Ordinal Hi))) _ Hm Hi) : IHm. + rewrite -[i.+1]/(Ordinal Hi).+1 -drop_accept. move => /(_ H). + case/exists_inP => f f1 f2. apply/exists_inP;exists f => //. apply: connect_trans (connect1 _) f2. + rewrite /step /read (ord2PC (i' := (Ordinal Hi))) ?inordK //= => _. + by rewrite inE ?eqxx. + Qed. + + Lemma nfa2_of_aux2 (q f:A) (i : pos w) : i != ord0 -> + f \in nfa2_f nfa2_of_dfa -> connect (step nfa2_of_dfa w) (q,i) (f,ord_max) -> + ((drop i.-1 w) \in dfa_accept q). + Proof. + Proof. + move => H fin_f. case/connectP => p. elim: p i H q => //= [|[q' j] p IHp i Hi q]. + - move => i Hi q _ [<- <-]. rewrite drop_size -topredE /= accept_nil. by rewrite inE in fin_f. + - rewrite {1}/step /read. case: (ord2P i) => /= [|/eqP->|i' Hi']; try by rewrite ?inE ?(negbTE Hi). + rewrite !inE !xpair_eqE (_ : L == R = false) ?eqxx ?andbT ?andbF ?orbF -?andbA //=. + case/and3P => /eqP -> /eqP E. rewrite -Hi' drop_accept. + have -> : i'.+1 = j.-1 by rewrite E. apply IHp. + apply/negP. move/eqP/(f_equal (@nat_of_ord _)). by rewrite E. + Qed. + + Lemma nfa2_of_correct : (w \in dfa_lang A) = (w \in nfa2_lang nfa2_of_dfa). + Proof. + apply/idP/idP; rewrite -![_ \in _ A]topredE /=. + - rewrite -{1}[w]drop0 /nfa2_lang -topredE /= inord1 => H. exact: nfa2_of_aux. + - rewrite -{2}[w]drop0 -[0]/((@ord1 n).-1). case/exists_inP => p. exact: nfa2_of_aux2. + Qed. + + Lemma nfa2_of_dfa_det : deterministic (nfa2_of_dfa). + Proof. split => [p a|p|p]; by rewrite ?cards1 ?cards0. Qed. + + Definition dfa2_of_dfa := DFA2 nfa2_of_dfa_det. + + Lemma dfa2_of_correct : (w \in dfa_lang A) = (w \in dfa2_lang dfa2_of_dfa). + Proof. exact: nfa2_of_correct. Qed. + +End DFAtoDFA2. diff --git a/theories/vardi.v b/theories/vardi.v new file mode 100644 index 0000000..133fc6b --- /dev/null +++ b/theories/vardi.v @@ -0,0 +1,125 @@ +(* Author: Christian Doczkal *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages nfa two_way. + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. + +(** ** Vardi Construction *) + +Definition bsimp := (andbT,andbF,andTb,andFb,orbT,orbF,orTb,orFb). + +(** Translation from 2NFAs to NFAs for the complement language *) + +Section Vardi. + Variables (char : finType) (M : nfa2 char). + Implicit Types (x y z w v : word char) (U V W : {set M}) (X Y : {set M} * {set M}). + + Definition reject_cert x (T : pos x -> {set M}) := + [/\ nfa2_s M \in T ord1, + [disjoint (nfa2_f M) & (T ord_max)] & + forall i p j q, p \in T i -> step M x (p,i) (q,j) -> q \in T j ]. + + Definition run_table x (i : pos x) := [set q | connect (step M x) (nfa2_s M, ord1) (q,i)]. + Arguments run_table x i : clear implicits. + + Lemma sub_run x C (i : pos x) : reject_cert C -> {subset run_table x i <= C i}. + Proof. + case => T1 T2 T3 p. rewrite inE. case/connectP => cs. + elim/last_ind: cs p i => /= [p i _|cs c IH p i]; first by case => -> ->. + rewrite rcons_path last_rcons [last _ _]surjective_pairing => /andP [pth stp] E. subst. + apply: T3 stp. by apply: IH; rewrite -?surjective_pairing. + Qed. + + Lemma dfa2Pn x : reflect (exists T, @reject_cert x T) (x \notin nfa2_lang M). + Proof. apply: introP => [H|]. + - exists (run_table x) ; split; first by rewrite inE ?connect0. + + apply/pred0P => q. rewrite !inE. apply: contraNF H => C. + by apply/existsP; exists q. + + move => i p j q. rewrite !inE => ? S. exact: connect_trans (connect1 S). + - move/negPn => /exists_inP [q Hq1 Hq2] [c C]. + have/(sub_run C) H : q \in run_table x ord_max by rewrite inE. + case: C => _ /disjoint_setI0 C _. move: C. move/setP/(_ q). by rewrite !inE Hq1 H. + Qed. + + Section Completeness. + Variables (a : char) (U V W : {set M}). + + Definition compL := [forall p in U, forall q, (q \in nfa2_transL p) ==> (q \in V)]. + + Definition compR := [forall p in V, forall q, (q \in nfa2_transR p) ==> (q \in U)]. + + Definition comp := [forall p in V, forall q, + (((q,L) \in nfa2_trans p a) ==> (q \in U)) && (((q,R) \in nfa2_trans p a) ==> (q \in W))]. + + End Completeness. + + Definition nfa_of := + {| nfa_s := [set X : {set M} * {set M} | (nfa2_s M \in X.2) & compL X.1 X.2]; + nfa_fin := [set X : {set M} * {set M} | [disjoint (nfa2_f M) & X.2] & compR X.1 X.2]; + nfa_trans X a Y := (X.2 == Y.1) && comp a X.1 X.2 Y.2 |}. + + Lemma nfa_ofP x : reflect (exists T, @reject_cert x T) (x \in nfa_lang nfa_of). + Proof. apply: (iffP nfaP). + - move => [s] [r] [Hp Hr]. + pose T (i : pos x) := if i:nat is i'.+1 then (nth s (s::r) i').2 else (nth s (s::r) 0).1. + have T_comp (j : 'I_(size x)) : + comp (tnth (tape x) j) (T (inord j)) (T (inord j.+1)) (T (inord j.+2)). + case: j => /= m Hm. move: (run_trans Hm Hr) => /andP [_]. + have -> : (nth s (s :: r) m).1 = T (inord m). + case: m Hm => [|m] Hm; first by rewrite -inord0. + rewrite /T inordK ?ltnS // 2?ltnW //. + move/ltnW : Hm => Hm. by case/andP : (run_trans Hm Hr) => /eqP-> ?. + have -> : (nth s (s :: r) m).2 = T (inord m.+1) by rewrite /T inordK // ltnS ltnW. + have -> // : (nth s r m).2 = T (inord m.+2). by rewrite /T inordK // ltnS. + exists T. split => //. + + rewrite /T /=. move: Hp. rewrite inE. by case/andP. + + rewrite /T /= (run_size Hr) -last_nth. + move/run_last : (Hr). rewrite inE. by case/andP. + + move => i p j q H. rewrite /step /read. + case: (ord2P _) => [/eqP ?|/eqP ?|i' Hi']; subst => //=. + * rewrite [_ == 0]eqn_leq ltn0 !bsimp => /andP [q1 q2]. + rewrite /T (eqP q2) /= in H *. + move: Hp. rewrite !inE => /andP [_ /forall_inP /(_ _ H) /forall_inP]. + apply. by rewrite !inE eqxx andbT /= in q1. + * rewrite [_ == _.+2](ltn_eqF) // !bsimp eqSS => /andP [q1 q2]. + rewrite /T /= (run_size Hr) -[size r]/((size (s :: r)).-1) nth_last in H. + move: (run_last Hr). rewrite inE. rewrite !inE eqxx andbT /= in q1. + move => /andP [_ /forall_inP /(_ p H) /forall_inP /(_ q q1)]. + rewrite /T (eqP q2) (run_size Hr). case e : (size r) => [|m] ; first by rewrite (size0nil e). + have Hm : m < size x by rewrite -e (run_size Hr). + rewrite -nth_last e /=. by case/andP: (run_trans Hm Hr) => /eqP ->. + - move: (T_comp i') => /= /forall_inP /(_ p). rewrite Hi' inord_val => /(_ H) /forallP /(_ q). + case/andP => q1 q2. + case/orP; case/andP => Ht e; rewrite ?Ht /= in q1 q2. + -- move: q2. by rewrite /T (eqP e) inordK // -Hi' ?ltnS. + -- move: q1. rewrite -Hi' eqSS in e. by rewrite -(eqP e) -{2}[j]inord_val. + - move => [T] [T1 T2 T3]. + set s := (T ord0, T ord1). exists s. + set r := [tuple (T (inord i.+1), T (inord i.+2)) | i < (size x)]. exists r. + have E m : m <= size x -> nth s (s :: r) m = (T (inord m), T (inord m.+1)). + case: m => m; first by rewrite nth0 /= -inord0 -inord1. + move => H. by rewrite [r]lock /= -lock -[m]/(val (Ordinal H)) -tnth_nth tnth_mktuple. + split. + + rewrite inE /= T1 /=. apply/forall_inP => p /T3 H. apply/forall_inP => q Hq. + apply: H. by rewrite /step /read ord2P0 !inE Hq eqxx. + + apply: runI. + * by rewrite size_map size_enum_ord. + * rewrite -nth_last [nth _ _ _](_ : _ = nth s (s::r) (size r)); last by case: (tval r). + rewrite size_tuple E // -inord_max inE /= T2 /=. + apply/forall_inP => p /T3 H. apply/forall_inP => q Hq. + apply H. by rewrite /step /read ord2PM !inE Hq inordK // eqxx !bsimp. + * move => i. rewrite unfold_in. rewrite !E //= 1?ltnW // eqxx /=. + apply/forall_inP => p /T3 H. apply/forallP => q. + have Hi : i.+1 = (inord i.+1 : pos x). by rewrite inordK // !ltnS 1?ltnW //. + apply/andP ; split; apply/implyP => Ht; apply H; rewrite /step /read /= (ord2PC Hi) Ht. + - by rewrite !inordK ?eqxx ?bsimp // !(ltn_ord,ltnS,ltnW). + - by rewrite !inordK ?eqxx ?bsimp // !(ltn_ord,ltnS,ltnW). + Qed. + + Lemma nfa_of_correct : nfa_lang nfa_of =i [predC (nfa2_lang M) ]. + Proof. move => w. rewrite !inE. apply/idP/dfa2Pn; by move/nfa_ofP. Qed. +End Vardi. + diff --git a/theories/wmso.v b/theories/wmso.v new file mode 100644 index 0000000..bb164d3 --- /dev/null +++ b/theories/wmso.v @@ -0,0 +1,955 @@ +(* Author: Christian Doczkal *) +(* Distributed under the terms of CeCILL-B. *) +From mathcomp Require Import all_ssreflect. +Require Import misc languages dfa nfa regexp. + +Set Implicit Arguments. +Unset Printing Implicit Defensive. +Unset Strict Implicit. + +(** Preliminaries *) + +(* to be used after simplification and rewriting with [tupleE] *) +Lemma behead_cons (T:Type) n (t : n.-tuple T) a : behead_tuple (cons_tuple a t) = t. +Proof. + rewrite /cons_tuple /behead_tuple /=. + case: t => t tP /=. set X := (behead_tupleP _). by rewrite (eq_irrelevance X tP). +Qed. + +(** * Weak Monadic Second-Order Logic *) + +(** We employ a minimal syntax for MSO formulas that permits only second-order +variables. *) + +Inductive form := +| Incl of nat & nat +| Less of nat & nat +| FF +| Imp of form & form +| Ex of form. + +(** All variables are interpreted as finite sets (actually lists) of natural numbers *) +Definition valuation := nat -> seq nat. + +Implicit Types (s t : form) (X Y : nat) (I : valuation) (N : seq nat). + +Definition cons N I : valuation := fun k => if k is k'.+1 then I k' else N. + +Fixpoint satisfies (I : valuation) (s : form) := + match s with + | Incl X Y => {subset I X <= I Y} + | Less X Y => forall x y, x \in I X -> y \in I Y -> x < y + | FF => False + | Imp s t => satisfies I s -> satisfies I t + | Ex s => exists N, satisfies (cons N I) s + end. + +Fixpoint bound (s : form) : nat := + match s with + | Incl X Y => maxn X.+1 Y.+1 + | Less X Y => maxn X.+1 Y.+1 + | FF => 0 + | Imp s t => maxn (bound s) (bound t) + | Ex s => (bound s).-1 + end. + +Definition agree n I I' := forall X, X < n -> I X =i I' X. + +Lemma agree_dc n m I I' : n <= m -> agree m I I' -> agree n I I'. +Proof. move => A B X ltn_m. apply: B. exact: leq_trans A. Qed. + +Lemma coincidence I I' s: + agree (bound s) I I' -> satisfies I s <-> satisfies I' s. +Proof. + elim: s I I' => [X Y|X Y||s IHs t IHt|s IHs] /= I I' C. + - split. + + move => A B. rewrite -!C ?leq_maxl ?leq_maxr //. exact: A. + + move => A B. rewrite !C ?leq_maxl ?leq_maxr //. exact: A. + - split => H x y;[rewrite -!C|rewrite !C]; try solve [exact: H|by rewrite ?leq_maxl ?leq_maxr]. + - tauto. + - by rewrite -(IHs I I') ?(IHt I I') //; apply: agree_dc C; rewrite ?leq_maxl ?leq_maxr. + - have bound_s N : agree (bound s) (cons N I) (cons N I'). + { move => X. case: X C => //= Y A B. apply: A. rewrite -ltnS. by case: (bound s) B. } + split. + + move => [N] sat_s. exists N. rewrite -IHs. eassumption. exact: bound_s. + + move => [N] sat_s. exists N. rewrite IHs. eassumption. exact: bound_s. +Qed. + +Lemma weak_coincidence I I' s : (forall X, I X =i I' X) -> satisfies I s -> satisfies I' s. +Proof. move => H. by rewrite (@coincidence I I' s). Qed. + +(** ** Language-Theoretic Interpretation *) + +Section Language. + Variables (char : finType). + + Definition I_of n (v : seq (n.-tuple bool)) : valuation := + fun X => [seq i <- iota 0 (size v) | nth false (nth [tuple of nseq n false] v i) X]. + + Definition vec_of (w : word char) : seq (#|char|.-tuple bool) := + map (fun a => [tuple X == enum_rank a | X < #|char|]) w. + + Lemma I_of_vev_max k (a:char) w: + k \in I_of (vec_of w) (enum_rank a) -> k < size w. + Proof. by rewrite /vec_of /I_of mem_filter mem_iota add0n size_map => /andP[_]. Qed. + + Lemma I_of_vecP k a w: k < size w -> + (k \in I_of (vec_of w) (enum_rank a) = (nth a w k == a)). + Proof. + move => H. rewrite /vec_of /I_of mem_filter mem_iota add0n size_map /=. + rewrite (nth_map a) // H andbT. + rewrite (nth_map (enum_rank a)) ?size_tuple ?ltn_ord //. + by rewrite nth_ord_enum (inj_eq enum_rank_inj) eq_sym. + Qed. + + Definition vec_lang n s := fun v : seq (n.-tuple bool) => satisfies (I_of v) s. + + Definition mso_lang s := fun w => vec_lang s (vec_of w). + + Lemma vec_of_hom : homomorphism vec_of. + Proof. exact: map_cat. Qed. + + Lemma mso_preim s : mso_lang s =p preimage vec_of (@vec_lang #|char| s). + Proof. done. Qed. + +End Language. + +Notation vec n := [finType of n.-tuple bool]. + +(** ** Translation from MSO Formulas to NFAs *) + +(** propositional connectives *) + +Definition nfa_for_bot n := dfa_to_nfa (dfa_void (vec n)). + +Definition nfa_for_imp n (A B : nfa (vec n)) := + dfa_to_nfa (dfa_op implb (nfa_to_dfa A) (nfa_to_dfa B)). + +(** MSO Primitives *) + +Definition nfa_for_incl n X Y := + {| nfa_state := [finType of unit]; + nfa_s := setT; + nfa_fin := setT; + nfa_trans := fun p (v : vec n) q => nth false v X ==> nth false v Y |}. + +Definition enfa_for_ltn n X Y : enfa (vec n) := + {| enfa_s := [set false]; + enfa_f := setT; + enfa_trans := fun (c : option (vec n)) p q => + match p,c,q with + | false, Some a, false => ~~ nth false a Y + | true, Some a, true => ~~ nth false a X + | false, None, true => true + | _,_,_ => false + end; |}. + +Definition nfa_for_ltn n X Y := nfa_of (enfa_for_ltn n X Y). + +(** Existential Quantification *) + +Definition prj0 n (w : seq (vec n.+1)) : seq (vec n) := + map (fun v : vec (n.+1) => [tuple of behead v]) w. +Prenex Implicits prj0. + +Definition trans_b0 n (A : nfa (vec n.+1)) (p q : A) := + [exists b, nfa_trans p [tuple of b :: nseq n false] q]. +Arguments trans_b0 [n] A p q. + +Definition nfa_for_ex n (A : nfa (vec n.+1)) : nfa (vec n) := + {| nfa_s := nfa_s A; + nfa_fin := [set p | [exists (q | q \in nfa_fin A), connect (trans_b0 A) p q]]; + nfa_trans := fun p (v : vec n) q => [exists b, nfa_trans p [tuple of b::v] q] |}. + +(** Translation to NFAs *) + +Fixpoint nfa_of_form n s {struct s} : nfa (vec n) := + match s with + | Incl X Y => nfa_for_incl n X Y + | Less X Y => nfa_for_ltn n X Y + | FF => nfa_for_bot n + | Imp s t => nfa_for_imp (nfa_of_form n s) (nfa_of_form n t) + | Ex s => nfa_for_ex (nfa_of_form n.+1 s) + end. + +(** ** Correctness of the Translation *) + +(** Correctness of Existential Quantification *) + +Fixpoint glue (bs : seq bool) n (w : seq (vec n)) := + match bs,w with + | b::bs,v::w => [tuple of b :: v] :: glue bs w + | b::bs,[::] => [tuple of b :: nseq n false] :: glue bs [::] + | nil,w => map (fun v : vec n => [tuple of false :: v]) w + end. + +Lemma nfa_for_exI n (A : nfa (vec n.+1)) b w : + glue b w \in nfa_lang A -> w \in nfa_lang (nfa_for_ex A). +Proof. + rewrite /nfa_lang !inE. + case/exists_inP => s s1 s2. apply/exists_inP. exists s => //. + elim: b w s {s1} s2 => [w p /=|b bs IH w p]. + - elim: w p => /= [|v w IHw] p. + + rewrite /= inE => H. by apply/exists_inP; exists p. + + apply: sub_exists => q /andP [q1 q2]. rewrite IHw // andbT. + by apply/existsP;exists false. + - case: w => [|v w] /=. + + case/exists_inP => q q1 /IH /= q2. rewrite !inE in q2 *. + apply: sub_exists q2 => r /andP [r1 r2]. + rewrite r1 (connect_trans (connect1 _) r2) // /trans_b0. by apply/existsP;exists b. + + apply: sub_exists => q /andP [q1 q2]. rewrite IH // andbT. by apply/existsP;exists b. +Qed. + +Lemma nfa_for_exE n (A : nfa (vec n.+1)) w : + w \in nfa_lang (nfa_for_ex A) -> exists b : seq bool, glue b w \in nfa_lang A. +Proof. + rewrite /nfa_lang /= !inE => H. + suff S (q:A) : @nfa_accept _ (nfa_for_ex A) q w -> exists b, nfa_accept q (glue b w). + { case/exists_inP : H => p p1 /S [b b1]. exists b. rewrite inE. by apply/exists_inP; exists p. } + elim: w q {H} => [|v vs IH] q /=. + - rewrite inE => /exists_inP [f f1 /connectP[p]]. + elim: p q => [x _ |p ps IHp q /= /andP [pth1 pth2]] /= E; first by exists nil; subst. + case: (IHp _ pth2 E) => bs Hbs. case/existsP : pth1 => b pth1. exists (b::bs). + by apply/exists_inP; exists p. + - case/exists_inP => p /= /existsP [b p1] p2. case: (IH _ p2) => bs Hbs. exists (b::bs). + by apply/exists_inP; exists p. +Qed. + +Lemma size_glue b n (v : seq (vec n)) : size (glue b v) = maxn (size b) (size v). +Proof. + elim: b v => [|b bs IH] v /=; first by rewrite max0n size_map. + case: v => [|v vs]; by rewrite /= ?maxnSS IH ?maxn0. +Qed. + +Lemma nth_glue0 b n (v : seq (vec n)) k : + nth false (nth [tuple of nseq n.+1 false] (glue b v) k) 0 = + nth false b k. +Proof. + elim: k v b => [|k IH] [|v vs] [|b bs] //; rewrite [glue _ _]/= ?nth_nil ?nth_cons ?IH //. + case: (ltnP k (size vs)) => A. + - by rewrite (nth_map [tuple of nseq n false]) //. + - by rewrite [_ _ _ k]nth_default // size_map. +Qed. + +Lemma I_of_glue0 i b n (v : seq (vec n)) : + i \in I_of (glue b v) 0 = nth false b i. +Proof. + rewrite mem_filter mem_iota add0n leq0n andTb. + rewrite nth_glue0 size_glue leq_max andbC. + case: (ltnP i (size b)) => //= A. by rewrite nth_default ?andbF. +Qed. + +Lemma nth_glueS b n (v : seq (vec n)) i k : + nth false (nth [tuple of nseq n.+1 false] (glue b v) k) i.+1 = + nth false (nth [tuple of nseq n false] v k) i. +Proof. + elim: k v b => [|k IH] [|v vs] [|b bs] //. + - by rewrite [glue _ _]/= IH !nth_nil nth_nseq if_same. + - rewrite [glue _ _]/= !nth_cons. + case: (ltnP k (size vs)) => A. + + by rewrite (nth_map [tuple of nseq n false]). + + by rewrite ![_ _ _ k]nth_default ?size_map. + - by rewrite [glue _ _]/= !nth_cons. +Qed. + +Lemma I_of_glueS i b n (v : seq (vec n)) k : + i \in I_of (glue b v) k.+1 = nth false (nth [tuple of nseq n false] v i) k. +Proof. + rewrite mem_filter mem_iota add0n leq0n andTb. + rewrite nth_glueS size_glue leq_max andbC orbC. + case: (ltnP i (size v)) => //= A. + by rewrite [_ _ v i]nth_default // nth_nseq if_same andbF. +Qed. + +Lemma vec_ex_glue s n (vs : seq (vec n)) : + vec_lang (Ex s) vs -> exists bs, vec_lang s (glue bs vs). +Proof. + rewrite /vec_lang /= => [[N sat_s]]. + exists [seq i \in N | i <- iota 0 (\max_(k <- N) k).+1]. + apply: weak_coincidence sat_s => X i. + case: X => [|X]. + - rewrite I_of_glue0. case: (boolP (i < (\max_(k <- N) k).+1)) => ltn_max. + + by rewrite (nth_map 0) ?size_iota // nth_iota. + + rewrite nth_default ?size_map ?size_iota 1?leqNgt //. + apply: contraNF ltn_max => H. rewrite ltnS. exact: bigmax_seq_sup H _ _. + - rewrite I_of_glueS /= /I_of mem_filter mem_iota /= add0n. + case: (ltnP i (size vs)) => H; first by rewrite andbT. + rewrite andbF [nth _ _ i]nth_default //. + by rewrite nth_nseq if_same. +Qed. + +Lemma vec_lang0 s n (v : seq (vec n)) k : + vec_lang s v <-> vec_lang s (v ++ nseq k [tuple of nseq n false]). +Proof. + apply coincidence => X ? i. rewrite !mem_filter !mem_iota /= !add0n size_cat nth_cat. + case: (boolP (i < size v)) => Hi; first by rewrite ltn_addr. + by rewrite andbF !(nth_nseq,if_same). +Qed. + +Lemma prj_glue bs n (v : seq (vec n)) : + exists k, prj0 (glue bs v) = v ++ nseq k [tuple of nseq n false]. +Proof. + exists (size bs - size v). elim: bs v => [|b bs IH] v /=. + - rewrite /prj0 -map_comp cats0 map_id_in //= => b. by rewrite !tupleE behead_cons. + - case: v => [| v vs] /=; by rewrite IH /= ?subn0 ?subss !tupleE behead_cons. +Qed. + +Lemma vec_Ex_prj0 s n (w : word (vec n.+1)) : vec_lang s w -> vec_lang (Ex s) (prj0 w). +Proof. + rewrite /vec_lang => /= A. + exists [seq i <- iota 0 (size w) | nth false (nth [tuple of nseq n.+1 false] w i) 0]. + apply: weak_coincidence A => X i. rewrite mem_filter mem_iota add0n /= /cons. + case: X => [|X]. + + by rewrite mem_filter mem_iota /= add0n. + + rewrite mem_filter mem_iota add0n size_map /prj0 andTb -nth_behead. + (case: (boolP (i < _)); rewrite ?andbF ?andbT //) => A. congr nth. + by erewrite nth_map. +Qed. + +Lemma nfa_for_ex_correct n s (A : nfa (vec n.+1)) v: + (forall u, reflect (vec_lang s u) (u \in nfa_lang A)) -> + reflect (vec_lang (Ex s) v) (v \in nfa_lang (nfa_for_ex A)). +Proof. + move => IHs. apply: (iffP idP). + + case/nfa_for_exE => b. move/IHs. move/vec_Ex_prj0. + case: (prj_glue b v) => k ->. by rewrite -vec_lang0. + + case/vec_ex_glue => b. move/IHs. exact: nfa_for_exI. +Qed. + +(** Correctness of the NFAs for the primitive operations *) + +Lemma nfa_for_incl_correct X Y n (v : seq (vec n)): + reflect (vec_lang (Incl X Y) v) (v \in nfa_lang (nfa_for_incl n X Y)). +Proof. + rewrite /nfa_lang inE. apply: (equivP existsP). + rewrite (_ : (exists _,_) <-> nfa_accept (tt : nfa_for_incl n X Y) v); last first. + - split => [[x]|];[case: x|exists tt]; by rewrite inE. + - rewrite (_ : vec_lang _ _ <-> (forall u, u \in v -> nth false u X -> nth false u Y)). + + elim: v => //= v vs IH. split. + * case/exists_inP => [[/implyP A] /IH B] u /predU1P []; first by move=>?;subst. + exact: B. + * move => A. apply/exists_inP; exists tt;[apply/implyP|]. + -- apply: A; exact: mem_head. + -- apply/IH => u Hu. apply: A. by rewrite inE Hu orbT. + + rewrite /vec_lang /=. split. + * move => A u in_v u_X. + set i := index u v. + move: (A i). rewrite /I_of !mem_filter !mem_iota !add0n /=. + rewrite index_mem in_v !andbT. rewrite nth_index //. by apply. + * move => A => k. rewrite /I_of !mem_filter !mem_iota !add0n /=. + case: (boolP (_ < _)); rewrite ?andbT ?andbF // => B. + set u := nth [tuple of nseq n false] v k. + apply A. by rewrite mem_nth. +Qed. + +Definition zero_at n X := forall (v : vec n), nth false v X = false. + +Lemma nfa_for_ltnP {X Y n} {v : seq (vec n)} : + reflect (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}]) + (v \in nfa_lang (nfa_for_ltn n X Y)). +Proof. + move: v => v0. apply: (iffP (nfa_ofP _ _)). + - rewrite /enfa_lang => [[[|_]]]; first by rewrite inE. + suff S q v: + enfa_accept (N := enfa_for_ltn n X Y) q v -> + if q + then {in v, zero_at n X} + else (exists v1 v2, [/\ v = v1 ++ v2, {in v1,zero_at n Y} & {in v2,zero_at n X}]). + { by move/S. } + elim => // {v0 v} [||]. + + case => // _. by do 2 exists nil. + + move => [|] a [|] //= v. + * move => A _ B u. case/predU1P => [->|]; by [rewrite (negbTE A)| apply: B]. + * move => A _ [v1] [v2] [C D E]. + exists (a :: v1); exists v2; split => //; first by rewrite C. + apply/all1s. split => //. by rewrite (negbTE A). + + move => [|] [|] // v. by exists nil; exists v. + - move => [v1] [v2] [->] A B. exists false; first by rewrite inE. + elim: v1 A => /= [_|a v1 IH A]. + + (apply: EnfaNone; first instantiate (1 := true)) => //. + elim: v2 B {v0} => [_|a s IH B]. + * constructor. by rewrite inE. + * (apply: EnfaSome; first instantiate (1 := true)) => //=. + -- by rewrite B ?inE ?eqxx. + -- apply: IH => u C. apply B. by rewrite inE C orbT. + + apply: EnfaSome; first instantiate (1 := false). + * by rewrite /= A ?inE ?eqxx. + * apply IH => u C. apply A. by rewrite inE C orbT. +Qed. + +Lemma mem_I_of n (v : seq (vec n)) X k : + (k \in I_of v X) = (k < size v) && nth false (nth [tuple of nseq n false] v k) X. +Proof. by rewrite mem_filter mem_iota add0n /= andbC. Qed. + +Lemma nfa_for_ltn_correct X Y n (v : seq (vec n)): + reflect (vec_lang (Less X Y) v) (v \in nfa_lang (nfa_for_ltn n X Y)). +Proof. + apply: (iffP nfa_for_ltnP). + - move => [v1] [v2] [A B C] i j. + rewrite /I_of !mem_filter !mem_iota !add0n /= ![_ && (_ < _)]andbC. + case: (boolP (_ < _)) => //= D. case: (boolP (_ < _)) => //= E F G. + have Hi : i < size v1. + { move: F. rewrite A nth_cat. case: (ifP _) => // /negbT H. + rewrite C ?mem_nth //. rewrite -leqNgt in H. + by rewrite -subSn // leq_subLR -size_cat -A. } + have : size v1 <= j. + { move: G. rewrite A nth_cat. case: (ltnP j (size v1)) => // H. + by rewrite B ? mem_nth. } + exact: leq_trans. + - rewrite /vec_lang /= => A. + case: (boolP (has predT (I_of v X))). + + case/hasP => x0 /max_mem k_in_X _. + set k := (\max_(i <- I_of v X) i) in k_in_X. + have size_k: k < size v by move: k_in_X; rewrite mem_I_of => /andP[]. + have size_tk: size (take k.+1 v) = k.+1. + { rewrite size_take. + case: (ltnP k.+1 (size v)) size_k => // H1 H2. + apply/eqP. by rewrite eqn_leq H1 H2. } + exists (take k.+1 v); exists (drop k.+1 v); split; first by rewrite cat_take_drop. + * move => u B. apply/negbTE/negP => D. + pose i := index u (take k.+1 v). + have E: i <= k by rewrite -ltnS -size_tk index_mem B. + move: (A k i). case/(_ _ _)/Wrap => //; last by rewrite leqNgt ltnS E. + rewrite mem_I_of (leq_ltn_trans E size_k) /=. + rewrite /i index_take // nth_index //. exact: mem_take B. + * move => u B. apply/negbTE/negP => D. + pose i := k.+1 + index u (drop k.+1 v). + have i_in_X : i \in I_of v X. + { rewrite mem_I_of. + rewrite -[v](cat_take_drop k.+1) size_cat size_tk. + rewrite -addnS leq_add2l index_mem B andTb. + rewrite nth_cat size_tk leqNgt leq_addr /= /i. + by rewrite addnC -addnBA // subnn addn0 nth_index. } + have: i <= k by apply: bigmax_seq_sup i_in_X _ _. + by rewrite /i addSn -ltn_subRL subnn. + + move/hasPn => /= B. exists nil; exists v; split => // u in_v. + apply/negbTE/negP => D. + pose i := index u v. move: (B i). case/(_ _)/Wrap => //. + by rewrite mem_I_of index_mem in_v nth_index. +Qed. + +Theorem nfa_of_form_correct n (v : seq (n.-tuple bool)) s : + reflect (vec_lang s v) (v \in nfa_lang (nfa_of_form n s)). +Proof. + elim: s n v => [X Y|X Y||s IHs t IHt|s IHs] /= n v. + - exact: nfa_for_incl_correct. + - exact: nfa_for_ltn_correct. + - rewrite -dfa_to_nfa_correct in_simpl (negbTE (dfa_void_correct _ _)). + by constructor. + - rewrite -dfa_to_nfa_correct dfa_op_correct -!nfa_to_dfa_correct. + by apply: (iffP implyP) => A /IHs/A/IHt. + - exact: nfa_for_ex_correct. +Qed. + +(** Greatest number used in first n variables *) +Definition lim I n := \max_(X < n) \max_(n <- I X) n. + +Definition vec_of_val I n : seq (n.-tuple bool) := + [seq [tuple i \in I X | X < n] | i <- iota 0 (lim I n).+1]. + +Lemma vec_of_val_agrees : forall I n, agree n I (I_of (vec_of_val I n)). +Proof. + move => I n X lt_n i. + rewrite mem_filter mem_iota /= add0n size_map size_iota. + case: (boolP (i < _)); rewrite ?(andbT,andbF) => A. + + rewrite /vec_of_val. + rewrite (nth_map 0) ?size_iota // nth_iota // add0n. + by rewrite (nth_map (Ordinal lt_n)) ?size_enum_ord ?nth_enum_ord. + + apply: contraNF A => A. rewrite ltnS. rewrite /lim. + apply: bigmax_sup => //. instantiate (1 := Ordinal lt_n) => /=. + exact: bigmax_seq_sup A _ _ . +Qed. + +Lemma vec_of_valP I s : satisfies I s <-> satisfies (I_of (vec_of_val I (bound s))) s. +Proof. apply: coincidence. exact: vec_of_val_agrees. Qed. + +Corollary satisfies_dec I s : decidable (satisfies I s). +Proof. apply: dec_iff (vec_of_valP I s). exact: decP (nfa_of_form_correct _ _). Qed. + +Corollary mso_dec s : decidable (exists I, satisfies I s). +Proof. + pose n := bound s. + case: (nfa_inhabP (nfa_of_form n s)) => A;[left|right]. + - case: A => w /(@nfa_of_form_correct n) Hw. by exists (I_of w). + - move => [I sat_I_s]. apply A. + exists (vec_of_val I n). apply/nfa_of_form_correct. + by rewrite /vec_lang -vec_of_valP. +Qed. + +Corollary vec_lang_regular n s : regular (@vec_lang n s). +Proof. + apply/nfa_regular. exists (nfa_of_form n s) => x. + apply: rwP. exact: nfa_of_form_correct. +Qed. + +(** ** Regularity of the Language of an MSO formula *) + +Corollary mso_regular (char: finType) s : regular (@mso_lang char s). +Proof. + apply: regular_ext (mso_preim s). + exact: preim_regular (@vec_of_hom _) (vec_lang_regular _ _). +Qed. + +(** ** Translation from NFAs to WMSO *) + +(** In order to translate NFAs to formulas, we define a number of defined +operations on top of the minimal syntax employed above. In particular, we make +use of the fact that [satisfies I s] is decidable and, hence, the logic behaves +classically. *) + +Notation "I |= s" := (satisfies I s) (at level 50). + +(** Propositional Connectives *) + +Lemma satNNPP I s : ~ ~ I |= s -> I |= s. +Proof. case: (satisfies_dec I s); tauto. Qed. + +Notation "s --> t" := (Imp s t) (at level 49, right associativity). +Definition Not s := Imp s FF. + +Lemma satDN I s : I |= Not (Not s) <-> I |= s. +Proof. move: (@satNNPP I s) => /= ; tauto. Qed. + +Lemma sat_imp I s t : I |= Imp s t <-> (I |= s -> I |= t). +Proof. done. Qed. + +Lemma sat_not I s : I |= Not s <-> ~ I |= s. +Proof. done. Qed. + +Definition TT := FF --> FF. + +Lemma sat_true I : I |= TT. +Proof. done. Qed. + +Definition And s t := Not (Imp s (Not t)). +Notation "s :/\: t" := (And s t) (at level 45). + +Lemma sat_and I s t : I |= And s t <-> (I |= s /\ I |= t). +Proof. + rewrite /And /Not /=. split => [A|]; last tauto. + split; apply: satNNPP; tauto. +Qed. + +Definition Or s t := Not s --> t. +Notation "s :\/: t" := (Or s t) (at level 47). + +Lemma sat_or I s t : I |= s :\/: t <-> I |= s \/ I |= t. +Proof. rewrite /Or /Not /=. split;[case: (satisfies_dec I s)|];tauto. Qed. + +Opaque And Or. + +Definition Iff s t := (s --> t) :/\: (t --> s). +Notation "s <--> t" := (Iff s t) (at level 50). + +Definition All s := Not (Ex (Not s)). + +Lemma sat_all I s : + I |= All s <-> (forall N, satisfies (cons N I) s). +Proof. + split => [A N|A]. + - apply: satNNPP => B. apply: A. by exists N. + - case: (satisfies_dec I (Ex (Not s))) => //= [[N B]]. + exfalso. exact: B. +Qed. + +Opaque All. + +(** Emptiness and Singletons *) + +Definition empty X := All (Incl (X.+1) 0). + +Lemma sat_empty I X : + I |= empty X <-> I X =i pred0. +Proof. + rewrite sat_all; split => [/= /(_ [::]) A k|A N k]; last by rewrite A. + rewrite inE. apply: negbTE. apply/negP. by move/A. +Qed. + +Lemma sat_emptyN I X : + I |= Not (empty X) <-> (exists n, n \in I X). +Proof. + rewrite satDN; split => [[N]|] /=. + - case: (I X) => [|x IX _]. + + by case/(_ _)/Wrap. + + by exists x; rewrite mem_head. + - case => n A. exists [:: n.+1]. move/(_ _ A). by rewrite inE ltn_eqF. +Qed. + +Definition single X := Not(empty X) :/\: All (Not(empty 0) --> Incl 0 X.+1 --> Incl X.+1 0). + +Lemma sat_singles I X : + I |= single X <-> exists n, I X =i [:: n]. +Proof. + rewrite sat_and sat_emptyN. split. + - move => [[n A] B]. + exists n. move => m. rewrite inE. apply/idP/eqP => [H|-> //]. + move/sat_all/(_ [:: n]): B. rewrite 2!sat_imp. case/(_ _ _)/Wrap. + + rewrite sat_emptyN. exists n. by rewrite inE. + + move => k /=. by rewrite inE => /eqP->. + + move/(_ _ H). by rewrite inE => /eqP->. + - case => n A. split; first by exists n;rewrite A. + apply/sat_all => N. rewrite 2!sat_imp sat_emptyN => /= [[k Hk] D] m E. + move: (D _ Hk). rewrite A inE => /eqP ?; subst. + rewrite A inE in E. by rewrite (eqP E). +Qed. + +(** Big Operatiors *) + +Notation "\or_ ( i <- r ) F" := (\big [Or/FF]_(i <- r) F) + (at level 42, F at level 42, i at level 0, + format "'[' \or_ ( i <- r ) '/ ' F ']'"). + +Notation "\or_ ( i \in A ) F" := (\big [Or/FF]_(i <- enum A) F) + (at level 42, F at level 42, i at level 0, + format "'[' \or_ ( i \in A ) '/ ' F ']'"). + +Notation "\and_ ( i <- r ) F" := (\big [And/TT]_(i <- r) F) + (at level 41, F at level 41, i at level 0, + format "'[' \and_ ( i <- r ) '/ ' F ']'"). + +Notation "\and_ ( i \in A ) F" := (\big [And/TT]_(i <- enum A) F) + (at level 41, F at level 41, i at level 0, + format "'[' \and_ ( i \in A ) '/ ' F ']'"). + +Lemma sat_orI (T:eqType) (s : seq T) x F I : + x \in s -> I |= F x -> I |= \or_(i <- s) F i. +Proof. elim: s => // a s IH /predU1P [<-|/IH A]; rewrite big_cons sat_or; tauto. Qed. + +Lemma sat_orE (T:eqType) (s : seq T) F I : + I |= \or_(i <- s) F i -> exists2 x, x \in s & I |= F x. +Proof. + elim: s => // [|a s IH]; first by rewrite big_nil. + rewrite big_cons sat_or. case => [A|/IH [x A B]]; first by exists a. + exists x => //. by rewrite inE A orbT. +Qed. + +Lemma sat_bigand (T:eqType) (s : seq T) F I : + I |= \and_(i <- s) F i <-> forall x, x \in s -> I |= F x. +Proof. + elim: s => [|a s IH]; first by rewrite big_nil; split => // _; apply. + rewrite big_cons sat_and IH. split => [[A B]x/predU1P[->//|]|A]. exact: B. + split => [|x B]; apply: A => //. by rewrite inE B orbT. +Qed. + +(** First-oder Quantification *) +(** Note that "first-order" variables are interpreted as one-element lists +rather than directly as numbers. Hence we need the lemmas [seq1P] and [sub1P] *) + +Definition All1 s := All (single 0 --> s). + +Lemma sat_all1 I s : + I |= All1 s <-> (forall n, cons [:: n] I |= s). +Proof. + rewrite sat_all; split. + - move => H n. move: (H [:: n]) => {H} /=. apply. rewrite sat_singles. by exists n. + - move => H N. rewrite sat_imp sat_singles => [[n Hn]]. + apply: weak_coincidence (H n). by case. +Qed. + +Definition Ex1 s := Ex (single 0 :/\: s). + +Lemma sat_ex1 I s : + I |= Ex1 s <-> (exists n, cons [:: n] I |= s). +Proof. + rewrite /Ex1; split. + - case => N. rewrite -/satisfies => /sat_and [/sat_singles [n] /= B C]. exists n. + apply: weak_coincidence C. by case. + - case => n A. exists [:: n]. apply/sat_and;split => //. + apply/sat_singles. by exists n. +Qed. + +(* Successor relation and Zero Predicate *) + +Lemma nat_succ x y : y = x.+1 <-> x < y /\ ~ exists k, x < k /\ k < y. +Proof. + split. + - move => ->. rewrite leqnn. split=>//. + move => [k] [A B]. move:(leq_trans A B). by rewrite ltnn. + - move => [A B]. apply/eqP. rewrite eqn_leq leqNgt A andbT. + apply/negP. apply: impliesPn B. constructor. + exists x.+1. by rewrite leqnn H. +Qed. + +Definition succ X Y := + Less X Y :/\: Not (Ex1 (Less X.+1 0 :/\: Less 0 Y.+1)). + +Lemma sat_succ I X x Y y : I X =i [:: x] -> I Y =i [:: y] -> + I |= succ X Y <-> y = x.+1. +Proof. + move => A B. rewrite sat_and sat_not sat_ex1 nat_succ. + split => [[C D]|[C D]]. + - split; first apply C; rewrite ?A ?B //. + apply: impliesPn D; constructor => [[k [k1 k2]]]. exists k. + rewrite sat_and /=; split => ? ?; by rewrite ?A ?B => /seq1P-> /seq1P->. + - split. move => ? ? ; by rewrite ?A ?B => /seq1P-> /seq1P->. + apply: impliesPn D; constructor => [[k] /sat_and [k1 k2]]. exists k. + split; [apply k1|apply k2]; by rewrite /= ?A ?B. +Qed. + +Definition zero X := single X :/\: Not (Ex1 (succ 0 X.+1)). + +Lemma sat_zero I X : I X =i [:: 0] <-> I |= zero X. +Proof. + rewrite sat_and sat_singles sat_not sat_ex1. + split. + - move => A. split; first by exists 0. + move => [n]. move/sat_succ. move/(_ 0 n) => /=. by case/(_ _ _)/Wrap. + - move => [[n A] B] k. rewrite A !inE. + suff S : n == 0. apply/idP/idP => /eqP->; by rewrite // eq_sym. + destruct n as [|n] => //. exfalso. apply B. + exists n. by rewrite (sat_succ (x := n) (y := n.+1)). +Qed. + +Definition Leq X Y := All1 (succ Y.+1 0 --> Less X.+1 0). + +Lemma sat_leq I X x Y y : I X =i [:: x] -> I Y =i [:: y] -> + I |= Leq X Y <-> x <= y. +Proof. + move => A B. rewrite sat_all1. split. + - move/(_ y.+1). rewrite sat_imp. case/(_ _)/Wrap. + + by rewrite (sat_succ (x := y) (y := y.+1)). + + move/(_ x y.+1). rewrite /= A !inE ltnS. by apply. + - move => C n. rewrite sat_imp. rewrite (sat_succ (x := y) (y := n)) // => ->. + move => ? ? /=. rewrite A !inE => /eqP-> /eqP->. by rewrite ltnS. +Qed. + +(** Interated existential quantification *) + +Definition cat (Ns: seq (seq nat)) I := + fun x => if x < size Ns then nth [::] Ns x else I (x - size Ns). + +Lemma cat_prefix I n (Ns : n.-tuple (seq nat)) X : X < n -> cat Ns I X = nth [::] Ns X. +Proof. move => A. by rewrite /cat size_tuple A. Qed. + +Lemma cat_beyond I n (Ns : n.-tuple (seq nat)) X : n <= X -> cat Ns I X = I (X - n). +Proof. move => A. by rewrite /cat size_tuple ltnNge A. Qed. + +Lemma cat_size I n (Ns : n.-tuple (seq nat)) : cat Ns I n = I 0. +Proof. by rewrite cat_beyond ?subnn. Qed. + +Definition exn n s := iter n Ex s. + +Lemma sat_exn n s I : + (I |= exn n s) <-> (exists Ns : n.-tuple (seq nat), cat Ns I |= s). +Proof. + elim: n I => [|n IH] I. + - split. + + exists [tuple]. rewrite /cat /=. apply: weak_coincidence H => X. by rewrite subn0. + + case => Ns. rewrite tuple0 /cat /=. + apply: weak_coincidence => X. by rewrite subn0. + - have agr Ns N X : cat (rcons Ns N) I X =i cat Ns (cons N I) X. + { rewrite /cat /= !size_rcons ltnS. + case: (ltngtP X (size Ns)) => B. + * by rewrite (ltnW B) nth_rcons B. + * rewrite leqNgt B /=. by rewrite -[X - size Ns]prednK ?subn_gt0 //= subnS. + * by rewrite B leqnn subnn nth_rcons ltnn eqxx. } + rewrite /=. split => [[N] /IH [Ns A]|]. + + exists [tuple of rcons Ns N]. apply: weak_coincidence A => X k. by rewrite agr. + + case. case => Ns /=. elim/last_ind : Ns => // Ns N _. + rewrite size_rcons eqSS => A B. + exists N. apply/IH. exists (Tuple A) => /=. + exact: weak_coincidence _ B. +Qed. + +Section NFAtoMSO. + Variables (T : finType) (A : nfa T). + Let n := #|A|. + Notation rank := enum_rank. + Notation val := enum_val. + + Definition max := + All1 (Less 0 1 <--> \or_(a \in T) Incl 0 (rank a).+2). + + Lemma sat_max (w : word T) m : + cons [:: m] (I_of (vec_of w)) |= max <-> m = size w. + Proof. + split. + - move/sat_all1 => B. + apply/eqP. rewrite eqn_leq [_ <= m]leqNgt [m <= _]leqNgt. + apply/andP; split; apply/negP => C. + + case: m C B => // m C /(_ m). case/sat_and => [/sat_imp B _]. move: B. + case/(_ _)/Wrap; first by move => ? ? /seq1P-> /seq1P->. + case/sat_orE => a _ /= /sub1P /I_of_vev_max => D. rewrite ltnS in C. + move: (leq_trans D C). by rewrite ltnn. + + move/(_ m) : B. case/sat_and => _. move/sat_imp. + case/(_ _)/Wrap. + * set a := (tnth (in_tuple w) (Ordinal C)). + apply: (sat_orI (x := a)); first by rewrite mem_enum. + apply/sub1P => /=. by rewrite I_of_vecP // {2}/a (tnth_nth a). + * move/(_ m m) => /=. rewrite !mem_head ltnn. by case/(_ _ _)/Wrap. + - move->. + rewrite sat_all1 => k. + rewrite sat_and; split. + + rewrite /= => H. + move: H => /(_ k (size w)). case/(_ _ _)/Wrap => // H. + pose a0 := tnth (in_tuple w) (Ordinal H). + apply (sat_orI (x := nth a0 w k)); first by rewrite mem_enum. + rewrite /= => ? /seq1P->. by rewrite I_of_vecP ?(set_nth_default a0). + + case/sat_orE => a _ /sub1P /=. + rewrite /vec_of /I_of mem_filter => /andP [_]. + by rewrite mem_iota add0n size_map /= => H ? ? /seq1P-> /seq1P->. + Qed. + + Definition part X := + All1 (Leq 0 X.+1 --> + (\or_(q \in A) (Incl 0 (rank q).+1 :/\: + \and_(q' \in [pred x | q != x]) Not (Incl 0 (rank q').+1)))). + + Lemma sat_part X I k : + I X =i [:: k] -> + I |= part X <-> forall n, n <= k -> exists! q:A, n \in I (rank q). + Proof. + move => H0. split. + - move => H1 m Hm. move/sat_all1 : H1 => /(_ m) /sat_imp. case/(_ _)/Wrap. + + rewrite sat_leq ; first apply Hm; done. + + case/sat_orE => q _ /sat_and [/= /sub1P q1 /sat_bigand q2]. + exists q; split => // q' B. apply/eqP. apply/negPn/negP => C. + apply: (q2 q'); by [rewrite mem_enum inE|apply/sub1P]. + - move => H1. + apply/sat_all1 => m. rewrite sat_imp => /sat_leq H2. + have/H1 {H2} : m <= k by apply: H2. + case => q [q1 q2]. apply: (sat_orI (x := q)); first by rewrite mem_enum. + rewrite sat_and; split; first by move => ? /seq1P ->. + apply/sat_bigand => q'. rewrite mem_enum inE => qq' /sub1P /q2 ?. + subst. by rewrite eqxx in qq'. + Qed. + + (* forall y x -> succ(x,y) -> x < max -> \or_( ... ) ... *) + (* 1 0 *) + Definition run X : form := + All1 (All1(succ 0 1 --> Less 0 X.+2 --> + \or_(paq \in [pred x : A * T * A | nfa_trans x.1.1 x.1.2 x.2]) + let: (p,a,q) := paq in + Incl 0 ((rank a).+1 + X).+2 (* a at pos x *) + :/\: Incl 0 (rank p).+2 (* state p active at time x *) + :/\: Incl 1 (rank q).+2 (* state q is next state of run *) + )). + + Lemma sat_run (Ns : n.-tuple (seq nat)) m I : + cat Ns (cons [:: m] I) |= run n <-> + (forall k, k < m -> exists (p:A) (a:T) (q:A), nfa_trans p a q /\ + k \in I (rank a) /\ + k \in tnth Ns (rank p) /\ + k.+1 \in tnth Ns (rank q)). + Proof. + split. + - move => H k lt_m. move/sat_all1/(_ k.+1) : H. move/sat_all1/(_ k). + rewrite 2!sat_imp. case/(_ _ _)/Wrap. + + by apply/(sat_succ (x := k) (y := k.+1)). + + move => /= ? y /seq1P ->. rewrite cat_beyond // subnn /=. + by move/seq1P->. + + case/sat_orE => [[[p a] q]]. rewrite mem_enum inE /= => B. + rewrite !sat_and. (do 2 case) => /= /sub1P C /sub1P D /sub1P E. + exists p. exists a. exists q. repeat split => //. + * by rewrite cat_beyond ?leq_addl -?addnBA // subnn addn0 in C. + * by rewrite cat_prefix // -tnth_nth in D. + * by rewrite cat_prefix // -tnth_nth in E. + - move => H. apply/sat_all1 => k'. apply/sat_all1 => k. rewrite !sat_imp => B C. + move/sat_succ : B => /(_ k' k). case/(_ _ _)/Wrap => // ?;subst. + case: (H _ (C k m _ _)) => //=; first by rewrite cat_size //=. + move => p [a] [q] [paq [D [E F]]]. + apply: (sat_orI (x := (p,a,q))); first by rewrite mem_enum. + rewrite !sat_and; repeat split. + + apply/sub1P. rewrite /= cat_beyond ?leq_addl //. + rewrite -addnBA // subnn addn0. done. + + apply/sub1P. by rewrite /= cat_prefix // -tnth_nth. + + apply/sub1P. by rewrite /= cat_prefix // -tnth_nth. + Qed. + + Definition init : form := + All1 (zero 0 --> \or_(q \in nfa_s A) Incl 0 (rank q).+1). + + Lemma sat_init (Ns : n.-tuple (seq nat)) I : + cat Ns I |= init <-> exists2 q, q \in nfa_s A & 0 \in tnth Ns (rank q). + Proof. + split. + - move/sat_all1/(_ 0)/sat_imp. case/(_ _)/Wrap; first exact/sat_zero. + case/sat_orE => s. rewrite mem_enum /= => B /sub1P C. exists s => //. + by rewrite cat_prefix // -tnth_nth in C. + - case => q q1 q2. apply/sat_all1 => m. rewrite sat_imp. move/sat_zero => /= B. + have -> : m = 0. move: (B 0). by rewrite !inE eqxx => /eqP. + apply (sat_orI (x := q)); first by rewrite mem_enum. + apply/sub1P. by rewrite /= cat_prefix -?tnth_nth. + Qed. + + Definition accept X := \or_(q \in nfa_fin A) Incl X (rank q). + + Lemma sat_accept (Ns : n.-tuple (seq nat)) m I : + cat Ns (cons [:: m] I) |= accept n <-> + exists2 q, q \in nfa_fin A & m \in tnth Ns (rank q). + Proof. + split. + - case/sat_orE => q. + rewrite mem_enum /= cat_size ?cat_prefix // -tnth_nth. + move => B /sub1P C. by exists q. + - case => q q1 q2. apply: (sat_orI (x := q)); first by rewrite mem_enum. + rewrite /= cat_size ?cat_prefix // -tnth_nth. exact/sub1P. + Qed. + + + (** underneath of [exn], [#|A|] refers to the length of the word (i.e. "max") *) + Definition form_of := + Ex1 (max :/\: exn #|A| ( + part #|A| :/\: init :/\: run #|A| :/\: accept #|A|)). + + + Theorem form_ofP w : reflect (@mso_lang T form_of w) (w \in nfa_lang A). + Proof. + apply: (iffP nfaP). + - move =>[s] [r] [r1 r2]. + rewrite /mso_lang /vec_lang sat_ex1. exists (size w). + set I' := cons _ _. + have Hmax : I' |= max by apply/sat_max. + rewrite sat_and sat_exn. split => //. + pose pos (i : 'I_#|A|) := [seq n <- iota 0 (size r).+1 | nth s (s::r) n == enum_val i]. + pose t := [tuple pos i | i < #|A|]. + exists t. + have tP k N (i : 'I_#|A|) : + k \in nth N t i = (k <= size r) && (nth s (s::r) k == val i). + { by rewrite -tnth_nth tnth_mktuple mem_filter mem_iota /= add0n ltnS andbC. } + rewrite !sat_and; repeat split. + + apply/(sat_part (k := (size w))). by rewrite cat_size. + move => k Hk. exists (nth s (s::r) k) ;split. + * by rewrite cat_prefix // tP -(run_size r2) Hk enum_rankK eqxx. + * move => q'. rewrite cat_prefix //. + rewrite tP -(run_size r2) Hk enum_rankK. by move/eqP. + + apply/sat_init. exists s => //. by rewrite tP /= enum_rankK. + + apply/sat_run => k Hk. have Hk': k < size r by rewrite -(run_size r2). + exists (nth s (s::r) k). + exists (tnth (in_tuple w) (Ordinal Hk)). + exists (nth s (s :: r) k.+1). repeat split. + * exact: run_trans. + * rewrite I_of_vecP //. set X := tnth _ _. by rewrite {2}/X (tnth_nth X). + * by rewrite tP ltnW // enum_rankK eqxx. + * by rewrite tP enum_rankK Hk' eqxx. + + apply/sat_accept. exists (last s r); first exact: run_last r2. + rewrite tP. by rewrite (run_size r2) leqnn enum_rankK nth_last /=. + - rewrite /mso_lang /vec_lang sat_ex1 => [[m] /sat_and [/sat_max B /sat_exn [Ns]]]. + repeat case/sat_and. subst. set I' := cat _ _. + move => /sat_part B /sat_init [s s1 s2] /sat_run D /sat_accept E. + move: {B} (B (size w)). + case/(_ _)/Wrap => [k|B]; first by rewrite /I' cat_size. + have exP (i : 'I_(size w)) : exists q : A, i.+1 \in I' (rank q). + { case: (B i.+1)=> // q [q1 q2]. by exists q. } + exists s. pose r := [tuple xchoose (exP i) | i < size w]. exists r. split => //. + have tP k p : k <= size w -> k \in tnth Ns (rank p) -> nth s (s::r) k = p. + { case: k => [_|k lt_w] H /=. + - case: (B 0 _) => // q' [q1 q2]. + by rewrite -[p]q2 -1?[s]q2 // /I' cat_prefix // -tnth_nth. + - rewrite (nth_map (Ordinal lt_w)) ?size_enum_ord //. + set m := nth _ _ _. move: (exP _) => F. move: (xchooseP F) => G. + case: (B m.+1 _) => // q' [q1 q2]. + rewrite -[xchoose F]q2 -1?[p]q2 //. + rewrite /I' cat_prefix // -tnth_nth. + by rewrite /m nth_enum_ord. + } + apply: runI. + + by rewrite size_tuple. + + case: E => f f1 f2. rewrite (_ : last s r = f) //. + by rewrite (last_nth s) size_tuple (tP _ _ _ f2). + + move => i. move: (D _ (ltn_ord i)) => [p] [a] [q] [pq [Ha [Hp Hq]]]. + rewrite I_of_vecP // in Ha. rewrite (tnth_nth a) (eqP Ha) //. + by rewrite (tP _ _ _ Hp) 1?ltnW // (tP _ _ _ Hq). + Qed. + +End NFAtoMSO.