diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/LICENSE | 19 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 32 | ||||
| -rw-r--r-- | doc/sphinx/index.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/introduction.rst | 59 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 17 |
6 files changed, 70 insertions, 66 deletions
diff --git a/doc/LICENSE b/doc/LICENSE index dcd8c49537..3789d91040 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -14,15 +14,6 @@ License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub/). Options A and B are *not* elected. -The Coq Tutorial is a work by Gérard Huet, Gilles Kahn and Christine -Paulin-Mohring. All documents (the LaTeX source and the PostScript, -PDF and html outputs) are copyright (c) INRIA 1999-2006. The material -connected to the Coq Tutorial may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 -or later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. - The Coq Standard Library is a collective work from the Coq Development Team whose members are listed in the file CREDITS of the Coq source package. All related documents (the Coq vernacular source files and @@ -31,16 +22,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre -Castéran and Eduardo Gimenez. All related documents (the LaTeX and -BibTeX sources and the PostScript, PDF and html outputs) are copyright -(c) INRIA 1997-2006. The material connected to the Tutorial on -[Co-]Inductive Types in Coq may be distributed only subject to the -terms and conditions set forth in the Open Publication License, v1.0 -or later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are -*not* elected. - ---------------------------------------------------------------------- *Open Publication License* diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 6c7258f9c5..68b5b9d6fe 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -296,6 +296,10 @@ Variants: This variant declares a class a posteriori from a constant or inductive definition. No methods or instances are defined. + .. warn:: @ident is already declared as a typeclass + + This command has no effect when used on a typeclass. + .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } The :cmd:`Instance` command is used to declare a type class instance named diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 3e988709c5..3574bf6750 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -3,6 +3,21 @@ @String{lnai = "Lecture Notes in Artificial Intelligence"} @String{SV = "{Sprin-ger-Verlag}"} +@InCollection{Asp00, + Title = {Proof General: A Generic Tool for Proof Development}, + Author = {Aspinall, David}, + Booktitle = {Tools and Algorithms for the Construction and + Analysis of Systems, {TACAS} 2000}, + Publisher = {Springer Berlin Heidelberg}, + Year = {2000}, + Editor = {Graf, Susanne and Schwartzbach, Michael}, + Pages = {38--43}, + Series = {Lecture Notes in Computer Science}, + Volume = {1785}, + Doi = {10.1007/3-540-46419-0_3}, + ISBN = {978-3-540-67282-1}, +} + @Book{Bar81, author = {H.P. Barendregt}, publisher = {North-Holland}, @@ -290,16 +305,13 @@ the Calculus of Inductive Constructions}}, year = {1995} } -@Misc{Pcoq, - author = {Lemme Team}, - title = {Pcoq a graphical user-interface for {Coq}}, - note = {\url{http://www-sop.inria.fr/lemme/pcoq/}} -} - -@Misc{ProofGeneral, - author = {David Aspinall}, - title = {Proof General}, - note = {\url{https://proofgeneral.github.io/}} +@InProceedings{Pit16, + Title = {Company-Coq: Taking Proof General one step closer to a real IDE}, + Author = {Pit-Claudel, Clément and Courtieu, Pierre}, + Booktitle = {CoqPL'16: The Second International Workshop on Coq for PL}, + Year = {2016}, + Month = jan, + Doi = {10.5281/zenodo.44331}, } @Book{RC95, diff --git a/doc/sphinx/index.rst b/doc/sphinx/index.rst index f3ae493817..baf2e0d981 100644 --- a/doc/sphinx/index.rst +++ b/doc/sphinx/index.rst @@ -84,3 +84,8 @@ This material (the Coq Reference Manual) may be distributed only subject to the terms and conditions set forth in the Open Publication License, v1.0 or later (the latest version is presently available at http://www.opencontent.org/openpub). Options A and B are not elected. + +.. [#PG] Proof-General is available at https://proofgeneral.github.io/. + Optionally, you can enhance it with the minor mode + Company-Coq :cite:`Pit16` + (see https://github.com/cpitclaudel/company-coq). diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 20e4069f45..c7bc69db4e 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -28,37 +28,35 @@ programs called *tactics*. All services of the |Coq| proof assistant are accessible by interpretation of a command language called *the vernacular*. -Coq has an interactive mode in which commands are interpreted as the +Coq has an interactive mode in which commands are interpreted as the user types them in from the keyboard and a compiled mode where commands are processed from a file. -- The interactive mode may be used as a debugging mode in which the - user can develop his theories and proofs step by step, backtracking - if needed and so on. The interactive mode is run with the `coqtop` - command from the operating system (which we shall assume to be some - variety of UNIX in the rest of this document). +- In interactive mode, users can develop their theories and proofs step by + step, and query the system for available theorems and definitions. The + interactive mode is generally run with the help of an IDE, such + as CoqIDE, documented in :ref:`coqintegrateddevelopmentenvironment`, + Emacs with Proof-General :cite:`Asp00` [#PG]_, + or jsCoq to run Coq in your browser (see https://github.com/ejgallego/jscoq). + The `coqtop` read-eval-print-loop can also be used directly, for debugging + purposes. - The compiled mode acts as a proof checker taking a file containing a whole development in order to ensure its correctness. Moreover, |Coq|’s compiler provides an output file containing a compact representation of its input. The compiled mode is run with the `coqc` - command from the operating system. + command. -These two modes are documented in Chapter :ref:`thecoqcommands`. - -Other modes of interaction with |Coq| are possible: through an emacs shell -window, an emacs generic user-interface for proof assistant (Proof -General :cite:`ProofGeneral`) or through a customized -interface (PCoq :cite:`Pcoq`). These facilities are not -documented here. There is also a |Coq| Integrated Development Environment -described in :ref:`coqintegrateddevelopmentenvironment`. +.. seealso:: :ref:`thecoqcommands`. How to read this book ===================== -This is a Reference Manual, not a User Manual, so it is not made for a -continuous reading. However, it has some structure that is explained -below. +This is a Reference Manual, so it is not made for a continuous reading. +We recommend using the various indexes to quickly locate the documentation +you are looking for. There is a global index, and a number of specific indexes +for tactics, vernacular commands, and error messages and warnings. +Nonetheless, the manual has some structure that is explained below. - The first part describes the specification language, |Gallina|. Chapters :ref:`gallinaspecificationlanguage` and :ref:`extensionsofgallina` describe the concrete @@ -68,7 +66,7 @@ below. of the formalism. Chapter :ref:`themodulesystem` describes the module system. -- The second part describes the proof engine. It is divided in five +- The second part describes the proof engine. It is divided in six chapters. Chapter :ref:`vernacularcommands` presents all commands (we call them *vernacular commands*) that are not directly related to interactive proving: requests to the environment, complete or partial @@ -79,42 +77,35 @@ below. *tactics*. The language to combine these tactics into complex proof strategies is given in Chapter :ref:`ltac`. Examples of tactics are described in Chapter :ref:`detailedexamplesoftactics`. + Finally, the |SSR| proof language is presented in + Chapter :ref:`thessreflectprooflanguage`. -- The third part describes how to extend the syntax of |Coq|. It - corresponds to the Chapter :ref:`syntaxextensionsandinterpretationscopes`. +- The third part describes how to extend the syntax of |Coq| in + Chapter :ref:`syntaxextensionsandinterpretationscopes` and how to define + new induction principles in Chapter :ref:`proofschemes`. - In the fourth part more practical tools are documented. First in Chapter :ref:`thecoqcommands`, the usage of `coqc` (batch mode) and `coqtop` (interactive mode) with their options is described. Then, in Chapter :ref:`utilities`, various utilities that come with the |Coq| distribution are presented. Finally, Chapter :ref:`coqintegrateddevelopmentenvironment` - describes the |Coq| integrated development environment. + describes CoqIDE. - The fifth part documents a number of advanced features, including coercions, canonical structures, typeclasses, program extraction, and specialized solvers and tactics. See the table of contents for a complete list. -At the end of the document, after the global index, the user can find -specific indexes for tactics, vernacular commands, and error messages. - List of additional documentation ================================ This manual does not contain all the documentation the user may need about |Coq|. Various informations can be found in the following documents: -Tutorial - A companion volume to this reference manual, the |Coq| Tutorial, is - aimed at gently introducing new users to developing proofs in |Coq| - without assuming prior knowledge of type theory. In a second step, - the user can read also the tutorial on recursive types (document - `RecTutorial.ps`). - Installation A text file `INSTALL` that comes with the sources explains how to install |Coq|. The |Coq| standard library A commented version of sources of the |Coq| standard library - (including only the specifications, the proofs are removed) is given - in the additional document `Library.ps`. + (including only the specifications, the proofs are removed) is + available at https://coq.inria.fr/stdlib/. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ab52c2ce78..6fb73a030f 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -623,7 +623,9 @@ where: + In the occurrence switch :token:`occ_switch`, if the first element of the list is a natural, this element should be a number, and not an Ltac variable. The empty list ``{}`` is not interpreted as a valid occurrence - switch. + switch, it is rather used as a flag to signal the intent of the user to + clear the name following it (see :ref:`ssr_rewrite_occ_switch` and + :ref:`introduction_ssr`) The tactic: @@ -1539,7 +1541,7 @@ whose general syntax is :name: => .. prodn:: - i_item ::= @i_pattern %| @s_item %| @clear_switch %| /@term + i_item ::= @i_pattern %| @s_item %| @clear_switch %| {? %{%} } /@term .. prodn:: s_item ::= /= %| // %| //= @@ -1641,6 +1643,11 @@ The view is applied to the top assumption. While it is good style to use the :token:`i_item` i * to pop the variables and assumptions corresponding to each constructor, this is not enforced by |SSR|. +``/`` :token:`term` + Interprets the top of the stack with the view :token:`term`. + It is equivalent to ``move/term``. The optional flag ``{}`` can + be used to signal that the :token:`term`, when it is a context entry, + has to be cleared. ``-`` does nothing, but counts as an intro pattern. It can also be used to force the interpretation of ``[`` :token:`i_item` * ``| … |`` @@ -3236,6 +3243,7 @@ the equality. Indeed the left hand side of ``H`` does not match the redex identified by the pattern ``x + y * 4``. +.. _ssr_rewrite_occ_switch: Occurrence switches and redex switches `````````````````````````````````````` @@ -3260,6 +3268,9 @@ the rewrite tactic. The effect of the tactic on the initial goal is to rewrite this lemma at the second occurrence of the first matching ``x + y + 0`` of the explicit rewrite redex ``_ + y + 0``. +An empty occurrence switch ``{}`` is not interpreted as a valid occurrence +switch. It has the effect of clearing the :token:`r_item` (when it is the name +of a context entry). Occurrence selection and repetition ``````````````````````````````````` @@ -5279,7 +5290,7 @@ generalization item see :ref:`structure_ssr` intro pattern :ref:`introduction_ssr` -.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| / @term +.. prodn:: i_item ::= @clear_switch %| @s_item %| @i_pattern %| {? %{%} } / @term intro item see :ref:`introduction_ssr` |