diff options
Diffstat (limited to 'doc')
30 files changed, 1075 insertions, 533 deletions
diff --git a/doc/common/styles/html/coqremote/header.html b/doc/common/styles/html/coqremote/header.html index c6c4509133..2f7ba14753 100644 --- a/doc/common/styles/html/coqremote/header.html +++ b/doc/common/styles/html/coqremote/header.html @@ -4,12 +4,12 @@ <head> <meta http-equiv="Content-Type" content="text/html; charset=utf-8" /> <link rel="shortcut icon" href="/favicon.ico" type="image/x-icon" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/node/node.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/system/defaults.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/system/system.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/modules/user/user.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/style.css" /> -<link type="text/css" rel="stylesheet" media="all" href="/sites/all/themes/coq/coqdoc.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/node/node.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/defaults.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/system/system.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/modules/user/user.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/style.css" /> +<link type="text/css" rel="stylesheet" media="all" href="//coq.inria.fr/sites/all/themes/coq/coqdoc.css" /> <title>Standard Library | The Coq Proof Assistant</title> @@ -21,20 +21,20 @@ <div id="headertop"> <div id="nav"> <ul class="links-menu"> - <li><a href="/" class="active">Home</a></li> - <li><a href="/about-coq" title="More about coq">About Coq</a></li> - <li><a href="/download">Get Coq</a></li> - <li><a href="/documentation">Documentation</a></li> - <li><a href="/community">Community</a></li> + <li><a href="//coq.inria.fr/" class="active">Home</a></li> + <li><a href="//coq.inria.fr/about-coq" title="More about coq">About Coq</a></li> + <li><a href="//coq.inria.fr/download">Get Coq</a></li> + <li><a href="//coq.inria.fr/documentation">Documentation</a></li> + <li><a href="//coq.inria.fr/community">Community</a></li> </ul> </div> </div> <div id="header"> <div id="logoWrapper"> - <div id="logo"><a href="/" title="Home"><img src="/files/barron_logo.png" alt="Home" /></a> + <div id="logo"><a href="//coq.inria.fr/" title="Home"><img src="//coq.inria.fr/files/barron_logo.png" alt="Home" /></a> </div> - <div id="siteName"><a href="/" title="Home">The Coq Proof Assistant</a> + <div id="siteName"><a href="//coq.inria.fr/" title="Home">The Coq Proof Assistant</a> </div> </div> </div> @@ -13,7 +13,7 @@ (source_tree tools) (env_var SPHINXWARNOPT)) (action - (run sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) + (run env COQLIB=%{project_root} sphinx-build -j4 %{env:SPHINXWARNOPT=-W} -b html -d sphinx_build/doctrees sphinx sphinx_build/html))) (alias (name refman-html) diff --git a/doc/plugin_tutorial/tuto1/src/simple_check.ml b/doc/plugin_tutorial/tuto1/src/simple_check.ml index 1f636c531a..2949adde73 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_check.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_check.ml @@ -6,7 +6,7 @@ let simple_check1 value_with_constraints = (* The point of renaming is to make sure the bound names printed by Check can be re-used in `apply with` tactics that use bound names to refer to arguments. *) - let j = Termops.on_judgment EConstr.of_constr + let j = Environ.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing (Global.env()) (EConstr.to_constr evd evalue)) in let {Environ.uj_type=x}=j in x diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 9d10a8ba72..e370d37fc4 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,5 +1,5 @@ (* Ideally coq/coq#8811 would get merged and then this function could be much simpler. *) -let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = +let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps = let sigma = Evd.minimize_universes sigma in let body = EConstr.to_constr sigma body in let tyopt = Option.map (EConstr.to_constr sigma) tyopt in @@ -9,16 +9,17 @@ let edeclare ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps hook = (Option.List.cons tyopt [body]) in let sigma = Evd.restrict_universe_context sigma uvars in let univs = Evd.check_univ_decl ~poly sigma udecl in + let uctx = Evd.evar_universe_context sigma in let ubinders = Evd.universe_binders sigma in let ce = Declare.definition_entry ?types:tyopt ~univs body in - DeclareDef.declare_definition ident k ce ubinders imps ~hook + let hook_data = Option.map (fun hook -> hook, uctx, []) hook in + DeclareDef.declare_definition ident k ce ubinders imps ?hook_data let packed_declare_definition ~poly ident value_with_constraints = let body, ctx = value_with_constraints in let sigma = Evd.from_ctx ctx in let k = (Decl_kinds.Global, poly, Decl_kinds.Definition) in let udecl = UState.default_univ_decl in - let nohook = Lemmas.mk_hook (fun _ x -> ()) in - ignore (edeclare ident k ~opaque:false sigma udecl body None [] nohook) + ignore (edeclare ident k ~opaque:false sigma udecl body None []) (* But this definition cannot be undone by Reset ident *) diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index e4f078c1d6..881f7a310d 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -214,17 +214,17 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo Example:: - .. coqtop:: in reset undo + .. coqtop:: in reset Print nat. Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -234,8 +234,10 @@ In addition to the objects above, the ``coqrst`` Sphinx plugin defines the follo - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Send an ``Undo n`` (``n`` = number of sentences) command after - running all the commands in this block + - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both) + - ``warn``: Don't die if a command emits a warning + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per @@ -509,7 +511,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -519,7 +521,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/README.template.rst b/doc/sphinx/README.template.rst index 81f25bf274..78803a927f 100644 --- a/doc/sphinx/README.template.rst +++ b/doc/sphinx/README.template.rst @@ -265,7 +265,7 @@ Tips and tricks Nested lemmas ------------- -The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas:: +The ``.. coqtop::`` directive does *not* reset Coq after running its contents. That is, the following will create two nested lemmas (which by default results in a failure):: .. coqtop:: all @@ -275,7 +275,7 @@ The ``.. coqtop::`` directive does *not* reset Coq after running its contents. Lemma l2: 2 + 2 <> 1. -Add either ``undo`` to the first block or ``reset`` to the second block to avoid nesting lemmas. +Add either ``abort`` to the first block or ``reset`` to the second block to avoid nesting lemmas. Abbreviations and macros ------------------------ diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3e414a714c..a9d894cab5 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -313,7 +313,9 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. coqtop:: all +.. FIXME shouldn't warn + +.. coqtop:: all warn Module Add_instance_attempt. @@ -418,7 +420,9 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. coqtop:: all +.. FIXME should not warn + +.. coqtop:: all warn Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index d77690458d..3ec6c118af 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -295,7 +295,7 @@ By default, implicit arguments are omitted in patterns. So we write: end). But the possibility to use all the arguments is given by “``@``” implicit -explicitations (as for terms 2.7.11). +explicitations (as for terms, see :ref:`explicit-applications`). .. coqtop:: all diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index cc788b3595..b474c51f17 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -627,14 +627,10 @@ logical equivalence: Instance all_iff_morphism (A : Type) : Proper (pointwise_relation A iff ==> iff) (@all A). -.. coqtop:: all +.. coqtop:: all abort Proof. simpl_relation. -.. coqtop:: none - - Abort. - One then has to show that if two predicates are equivalent at every point, their universal quantifications are equivalent. Once we have declared such a morphism, it will be used by the setoid rewriting diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 43d302114e..c7ea7e326f 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -44,25 +44,20 @@ Leibniz equality on some type. An example implementation is: eqb_leibniz x y H := match x, y return x = y with tt, tt => eq_refl tt end }. -If one does not give all the members in the Instance declaration, Coq -enters the proof-mode and the user is asked to build inhabitants of -the remaining fields, e.g.: +Using :cmd:`Program Instance`, if one does not give all the members in +the Instance declaration, Coq generates obligations for the remaining +fields, e.g.: .. coqtop:: in - Instance eq_bool : EqDec bool := + Require Import Program.Tactics. + Program Instance eq_bool : EqDec bool := { eqb x y := if x then y else negb y }. .. coqtop:: all - Proof. intros x y H. - -.. coqtop:: all - - destruct x ; destruct y ; (discriminate || reflexivity). - -.. coqtop:: all - + Next Obligation. + destruct x ; destruct y ; (discriminate || reflexivity). Defined. One has to take care that the transparency of every field is @@ -131,14 +126,14 @@ the constraints as a binding context before the instance, e.g.: .. coqtop:: in - Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := + Program Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) := { eqb x y := match x, y with | (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb) end }. .. coqtop:: none - Abort. + Admit Obligations. These instances are used just as well as lemmas in the instance hint database. @@ -157,13 +152,13 @@ vernacular, except it accepts any binding context as argument. For example: Context `{EA : EqDec A}. - Global Instance option_eqb : EqDec (option A) := + Global Program Instance option_eqb : EqDec (option A) := { eqb x y := match x, y with | Some x, Some y => eqb x y | None, None => true | _, _ => false end }. - Admitted. + Admit Obligations. End EqDec_defs. @@ -564,12 +559,12 @@ Settings This flag allows to switch the behavior of instance declarations made through the Instance command. - + When it is on (the default), instances that have unsolved holes in + + When it is off (the default), they fail with an error instead. + + + When it is on, instances that have unsolved holes in their proof-term silently open the proof mode with the remaining obligations to prove. - + When it is off, they fail with an error instead. - Typeclasses eauto `:=` ~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index d9eaa2c6c6..0467852b19 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -45,6 +45,58 @@ s}, year = {1972} } +@inproceedings{CH85, + title={Constructions: a higher order proof system for mechanizing mathematics}, + author={Coquand, Thierry and Huet, Gérard}, + booktitle={European Conference on Computer Algebra}, + pages={151--184}, + year={1985}, + issn = {1611-3349}, + doi = {10.1007/3-540-15983-5_13}, + url = {http://dx.doi.org/10.1007/3-540-15983-5_13}, + isbn = 9783540396840, + publisher = {Springer Berlin Heidelberg} +} + +@techreport{CH88 + TITLE = {{The calculus of constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076024}, + NUMBER = {RR-0530}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = May, + PDF = {https://hal.inria.fr/inria-00076024/file/RR-0530.pdf}, + HAL_ID = {inria-00076024}, + HAL_VERSION = {v1}, +} + +@techreport{CH87, + TITLE = {{Concepts mathematiques et informatiques formalises dans le calcul des constructions}}, + AUTHOR = {Coquand, T. and Huet, G{\'e}rard}, + URL = {https://hal.inria.fr/inria-00076039}, + NUMBER = {RR-0515}, + INSTITUTION = {{INRIA}}, + YEAR = {1986}, + MONTH = Apr, + PDF = {https://hal.inria.fr/inria-00076039/file/RR-0515.pdf}, + HAL_ID = {inria-00076039}, + HAL_VERSION = {v1}, +} + +@techreport{C90, + TITLE = {{Metamathematical investigations of a calculus of constructions}}, + AUTHOR = {Coquand, T.}, + URL = {https://hal.inria.fr/inria-00075471}, + NUMBER = {RR-1088}, + INSTITUTION = {{INRIA}}, + YEAR = {1989}, + MONTH = Sep, + PDF = {https://hal.inria.fr/inria-00075471/file/RR-1088.pdf}, + HAL_ID = {inria-00075471}, + HAL_VERSION = {v1}, +} + @PhDThesis{Coq85, author = {Th. Coquand}, month = jan, @@ -80,6 +132,19 @@ s}, bibsource = {DBLP, http://dblp.uni-trier.de} } +@inproceedings{CP90, + title={Inductively defined types}, + author={Coquand, Thierry and Paulin, Christine}, + booktitle={COLOG-88}, + pages={50--66}, + year={1990}, + issn = {1611-3349}, + doi = {10.1007/3-540-52335-9_47}, + url = {http://dx.doi.org/10.1007/3-540-52335-9_47}, + isbn = 9783540469636, + publisher = {Springer Berlin Heidelberg} +} + @Book{Cur58, author = {Haskell B. Curry and Robert Feys and William Craig}, title = {Combinatory Logic}, @@ -216,7 +281,19 @@ s}, year = {1980} } -@InProceedings{Hue88, +@inproceedings{H88, + title={Induction principles formalized in the Calculus of Constructions}, + author={Huet, G{\'e}rard}, + booktitle={Programming of Future Generation Computers. Elsevier Science}, + year={1988}, + issn = {1611-3349}, + doi = {10.1007/3-540-17660-8_62}, + url = {http://dx.doi.org/10.1007/3-540-17660-8_62}, + isbn = 9783540477464, + publisher = {Springer Berlin Heidelberg} +} + +@InProceedings{H89, author = {G. Huet}, booktitle = {A perspective in Theoretical Computer Science. Commemorative Volume for Gift Siromoney}, editor = {R. Narasimhan}, @@ -305,6 +382,50 @@ s}, url = {http://www.xmailserver.org/diff2.pdf} } +@inproceedings{P86, + title={Algorithm development in the calculus of constructions}, + author={Mohring, Christine}, + booktitle={LICS}, + pages={84--91}, + year={1986} +} + +@inproceedings{P89, + title={Extracting $\Omega$'s programs from proofs in the calculus of constructions}, + author={Paulin-Mohring, Christine}, + booktitle={Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages}, + pages={89--104}, + year={1989}, + doi = {10.1145/75277.75285}, + url = {http://dx.doi.org/10.1145/75277.75285}, + isbn = 0897912942, + organization = {ACM Press} +} + +@inproceedings{P93, + title={Inductive definitions in the system coq rules and properties}, + author={Paulin-Mohring, Christine}, + booktitle={International Conference on Typed Lambda Calculi and Applications}, + pages={328--345}, + year={1993}, + doi = {10.1007/bfb0037116}, + url = {http://dx.doi.org/10.1007/bfb0037116}, + isbn = 3540565175, + organization = {Springer-Verlag} +} + +@inproceedings{PP90, + title={Inductively defined types in the Calculus of Constructions}, + author={Pfenning, Frank and Paulin-Mohring, Christine}, + booktitle={International Conference on Mathematical Foundations of Programming Semantics}, + pages={209--228}, + year={1989}, + doi = {10.1007/bfb0040259}, + url = {http://dx.doi.org/10.1007/bfb0040259}, + isbn = 0387973753, + organization = {Springer-Verlag} +} + @InProceedings{Parent95b, author = {C. Parent}, booktitle = {{Mathematics of Program Construction'95}}, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 9d2afc080f..48ad60c6dd 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -142,6 +142,7 @@ exclude_patterns = [ 'introduction.rst', 'refman-preamble.rst', 'README.rst', + 'README.gen.rst', 'README.template.rst' ] + ["*.{}.rst".format(fmt) for fmt in SUPPORTED_FORMATS] diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 909af6e2f2..5873096523 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -2,10 +2,13 @@ Credits ------- +Historical roots +---------------- + Coq is a proof assistant for higher-order logic, allowing the development of computer programs consistent with their formal -specification. It is the result of about ten years of research of the -Coq project. We shall briefly survey here three main aspects: the +specification. It is the result of about ten years [#years]_ of research +of the Coq project. We shall briefly survey here three main aspects: the *logical language* in which we write our axiomatizations and specifications, the *proof assistant* which allows the development of verified mathematical proofs, and the *program extractor* which @@ -21,8 +24,8 @@ prompted Russell to restrict predicate calculus with a stratification of *types*. This effort culminated with *Principia Mathematica*, the first systematic attempt at a formal foundation of mathematics. A simplification of this system along the lines of simply typed -:math:`\lambda`-calculus occurred with Church’s *Simple Theory of -Types*. The :math:`\lambda`-calculus notation, originally used for +λ-calculus occurred with Church’s *Simple Theory of +Types*. The λ-calculus notation, originally used for expressing functionality, could also be used as an encoding of natural deduction proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the *Automath* project, the first full-scale attempt to develop and @@ -32,7 +35,7 @@ Exploiting this Curry-Howard isomorphism, notable achievements in proof theory saw the emergence of two type-theoretic frameworks; the first one, Martin-Löf’s *Intuitionistic Theory of Types*, attempts a new foundation of mathematics on constructive principles. The second one, -Girard’s polymorphic :math:`\lambda`-calculus :math:`F_\omega`, is a +Girard’s polymorphic λ-calculus :math:`F_\omega`, is a very strong functional system in which we may represent higher-order logic proof structures. Combining both systems in a higher-order extension of the Automath language, T. Coquand presented in 1985 the @@ -107,15 +110,27 @@ advantage of special hardware, debuggers, and the like. We hope that |Coq| can be of use to researchers interested in experimenting with this new methodology. +.. [#years] At the time of writting, i.e. 1995. + +Brief summary of the versions up to 5.10 +---------------------------------------- + +.. note:: + This summary was written in 1995 together with the previous + section and formed the initial version of the Credits chapter + (that has since then been appended to, at each new release). + A more comprehensive description of these early versions is + available in the next few sections, which were written in 2015. + A first implementation of CoC was started in 1984 by G. Huet and T. Coquand. Its implementation language was CAML, a functional programming language from the ML family designed at INRIA in Rocquencourt. The core of this system was a proof-checker for CoC seen as a typed -:math:`\lambda`-calculus, called the *Constructive Engine*. This engine +λ-calculus, called the *Constructive Engine*. This engine was operated through a high-level notation permitting the declaration of axioms and parameters, the definition of mathematical types and objects, and the explicit construction of proof objects encoded as -:math:`\lambda`-terms. A section mechanism, designed and implemented by +λ-terms. A section mechanism, designed and implemented by G. Dowek, allowed hierarchical developments of mathematical theories. This high-level language was called the *Mathematical Vernacular*. Furthermore, an interactive *Theorem Prover* permitted the incremental @@ -189,8 +204,324 @@ definitions of “inversion predicates”. | Gérard Huet | -Credits: addendum for version 6.1 ---------------------------------- +Version 1 +--------- + +.. note:: + + These additional notes come from a document written + in September 2015 by Gérard Huet, Thierry Coquand and Christine Paulin + to accompany their public release of the archive of versions 1.10 to 6.2 + of Coq and of its CONSTR ancestor. CONSTR, then Coq, was designed and + implemented in the Formel team, joint between the INRIA Rocquencourt + laboratory and the Ecole Normale Supérieure of Paris, from 1984 + onwards. + +This software is a prototype type-checker for a higher-order logical +formalism known as the Theory of Constructions, presented in his PhD +thesis by Thierry Coquand, with influences from Girard's system F and +de Bruijn's Automath. The metamathematical analysis of the system is +the PhD work of Thierry Coquand. The software is mostly the work of +Gérard Huet. Most of the mathematical examples verified with the +software are due to Thierry Coquand. + +The programming language of the CONSTR software (as it was called at +the time) was a version of ML adapted from the Edinburgh LCF system +and running on a LISP backend. The main improvements from the original +LCF ML were that ML was compiled rather than interpreted (Gérard Huet +building on the original translator by Lockwood Morris), and that it +was enriched by recursively defined types (work of Guy +Cousineau). This ancestor of CAML was used and improved by Larry +Paulson for his implementation of Cambridge LCF. + +Software developments of this prototype occurred from late 1983 to +early 1985. + +Version 1.10 was frozen on December 22nd 1984. It is the version used +for the examples in Thierry Coquand's thesis, defended on January 31st +1985. There was a unique binding operator, used both for universal +quantification (dependent product) at the level of types and +functional abstraction (λ) at the level of terms/proofs, in the manner +of Automath. Substitution (λ-reduction) was implemented using de +Bruijn's indexes. + +Version 1.11 was frozen on February 19th, 1985. It is the version used +for the examples in the paper: T. Coquand, G. Huet. *Constructions: A +Higher Order Proof System for Mechanizing Mathematics* :cite:`CH85`. + +Christine Paulin joined the team at this point, for her DEA research +internship. In her DEA memoir (August 1985) she presents developments +for the *lambo* function – :math:`\text{lambo}(f)(n)` computes the minimal +:math:`m` such that :math:`f(m)` is greater than :math:`n`, for :math:`f` +an increasing integer function, a challenge for constructive mathematics. +She also encoded the majority voting algorithm of Boyer and Moore. + +Version 2 +--------- + +The formal system, now renamed as the *Calculus of Constructions*, was +presented with a proof of consistency and comparisons with proof +systems of Per Martin Löf, Girard, and the Automath family of N. de +Bruijn, in the paper: T. Coquand and G. Huet. *The Calculus of +Constructions* :cite:`CH88`. + +An abstraction of the software design, in the form of an abstract +machine for proof checking, and a fuller sequence of mathematical +developments was presented in: T. Coquand, G. Huet. *Concepts +Mathématiques et Informatiques Formalisés dans le Calcul des +Constructions* :cite:`CH87`. + +Version 2.8 was frozen on December 16th, 1985, and served for +developing the examples in the above papers. + +This calculus was then enriched in version 2.9 with a cumulative +hierarchy of universes. Universe levels were initially explicit +natural numbers. Another improvement was the possibility of automatic +synthesis of implicit type arguments, relieving the user of tedious +redundant declarations. + +Christine Paulin wrote an article *Algorithm development in the +Calculus of Constructions* :cite:`P86`. Besides *lambo* and *majority*, +she presents *quicksort* and a text formatting algorithm. + +Version 2.13 of the Calculus of Constructions with universes was +frozen on June 25th, 1986. + +A synthetic presentation of type theory along constructive lines with +ML algorithms was given by Gérard Huet in his May 1986 CMU course +notes *Formal Structures for Computation and Deduction*. Its chapter +*Induction and Recursion in the Theory of Constructions* was presented +as an invited paper at the Joint Conference on Theory and Practice of +Software Development TAPSOFT’87 at Pise in March 1987, and published +as *Induction Principles Formalized in the Calculus of +Constructions* :cite:`H88`. + +Version 3 +--------- + +This version saw the beginning of proof automation, with a search +algorithm inspired from PROLOG and the applicative logic programming +programs of the course notes *Formal structures for computation and +deduction*. The search algorithm was implemented in ML by Thierry +Coquand. The proof system could thus be used in two modes: proof +verification and proof synthesis, with tactics such as ``AUTO``. + +The implementation language was now called CAML, for Categorical +Abstract Machine Language. It used as backend the LLM3 virtual machine +of Le Lisp by Jérôme Chailloux. The main developers of CAML were +Michel Mauny, Ascander Suarez and Pierre Weis. + +V3.1 was started in the summer of 1986, V3.2 was frozen at the end of +November 1986. V3.4 was developed in the first half of 1987. + +Thierry Coquand held a post-doctoral position in Cambrige University +in 1986-87, where he developed a variant implementation in SML, with +which he wrote some developments on fixpoints in Scott's domains. + +Version 4 +--------- + +This version saw the beginning of program extraction from proofs, with +two varieties of the type ``Prop`` of propositions, indicating +constructive intent. The proof extraction algorithms were implemented +by Christine Paulin-Mohring. + +V4.1 was frozen on July 24th, 1987. It had a first identified library +of mathematical developments (directory ``exemples``), with libraries +``Logic`` (containing impredicative encodings of intuitionistic logic and +algebraic primitives for booleans, natural numbers and list), ``Peano`` +developing second-order Peano arithmetic, ``Arith`` defining addition, +multiplication, euclidean division and factorial. Typical developments +were the Knaster-Tarski theorem and Newman's lemma from rewriting +theory. + +V4.2 was a joint development of a team consisting of Thierry Coquand, +Gérard Huet and Christine Paulin-Mohring. A file V4.2.log records the +log of changes. It was frozen on September 1987 as the last version +implemented in CAML 2.3, and V4.3 followed on CAML 2.5, a more stable +development system. + +V4.3 saw the first top-level of the system. Instead of evaluating +explicit quotations, the user could develop his mathematics in a +high-level language called the mathematical vernacular (following +Automath terminology). The user could develop files in the vernacular +notation (with ``.v`` extension) which were now separate from the ``ml`` +sources of the implementation. Gilles Dowek joined the team to +develop the vernacular language as his DEA internship research. + +A notion of sticky constant was introduced, in order to keep names of +lemmas when local hypotheses of proofs were discharged. This gave a +notion of global mathematical environment with local sections. + +Another significant practical change was that the system, originally +developped on the VAX central computer of our lab, was transferred on +SUN personal workstations, allowing a level of distributed +development. The extraction algorithm was modified, with three +annotations ``Pos``, ``Null`` and ``Typ`` decorating the sorts ``Prop`` +and ``Type``. + +Version 4.3 was frozen at the end of November 1987, and was +distributed to an early community of users (among those were Hugo +Herbelin and Loic Colson). + +V4.4 saw the first version of (encoded) inductive types. Now natural +numbers could be defined as:: + + [source, coq] + Inductive NAT : Prop = O : NAT | Succ : NAT->NAT. + +These inductive types were encoded impredicatively in the calculus, +using a subsystem *rec* due to Christine Paulin. V4.4 was frozen on +March 6th 1988. + +Version 4.5 was the first one to support inductive types and program +extraction. Its banner was *Calcul des Constructions avec +Réalisations et Synthèse*. The vernacular language was enriched to +accommodate extraction commands. + +The verification engine design was presented as: G. Huet. *The +Constructive Engine*. Version 4.5. Invited Conference, 2nd European +Symposium on Programming, Nancy, March 88. The final paper, +describing the V4.9 implementation, appeared in: A perspective in +Theoretical Computer Science, Commemorative Volume in memory of Gift +Siromoney, Ed. R. Narasimhan, World Scientific Publishing, 1989. + +Version 4.5 was demonstrated in June 1988 at the YoP Institute on +Logical Foundations of Functional Programming organized by Gérard Huet +at Austin, Texas. + +Version 4.6 was started during the summer of 1988. Its main +improvement was the complete rehaul of the proof synthesis engine by +Thierry Coquand, with a tree structure of goals. + +Its source code was communicated to Randy Pollack on September 2nd +1988. It evolved progressively into LEGO, proof system for Luo's +formalism of Extended Calculus of Constructions. + +The discharge tactic was modified by Gérard Huet to allow for +inter-dependencies in discharged lemmas. Christine Paulin improved the +inductive definition scheme in order to accommodate predicates of any +arity. + +Version 4.7 was started on September 6th, 1988. + +This version starts exploiting the CAML notion of module in order to +improve the modularity of the implementation. Now the term verifier is +identified as a proper module Machine, which the structure of its +internal data structures being hidden and thus accessible only through +the legitimate operations. This machine (the constructive engine) was +the trusted core of the implementation. The proof synthesis mechanism +was a separate proof term generator. Once a complete proof term was +synthesized with the help of tactics, it was entirely re-checked by +the engine. Thus there was no need to certify the tactics, and the +system took advantage of this fact by having tactics ignore the +universe levels, universe consistency check being relegated to the +final type-checking pass. This induced a certain puzzlement in early +users who saw, after a successful proof search, their ``QED`` followed +by silence, followed by a failure message due to a universe +inconsistency… + +The set of examples comprise set theory experiments by Hugo Herbelin, +and notably the Schroeder-Bernstein theorem. + +Version 4.8, started on October 8th, 1988, saw a major +re-implementation of the abstract syntax type ``constr``, separating +variables of the formalism and metavariables denoting incomplete terms +managed by the search mechanism. A notion of level (with three values +``TYPE``, ``OBJECT`` and ``PROOF``) is made explicit and a type judgement +clarifies the constructions, whose implementation is now fully +explicit. Structural equality is speeded up by using pointer equality, +yielding spectacular improvements. Thierry Coquand adapts the proof +synthesis to the new representation, and simplifies pattern matching +to first-order predicate calculus matching, with important performance +gain. + +A new representation of the universe hierarchy is then defined by +Gérard Huet. Universe levels are now implemented implicitly, through +a hidden graph of abstract levels constrained with an order relation. +Checking acyclicity of the graph insures well-foundedness of the +ordering, and thus consistency. This was documented in a memo *Adding +Type:Type to the Calculus of Constructions* which was never published. + +The development version is released as a stable 4.8 at the end of +1988. + +Version 4.9 is released on March 1st 1989, with the new "elastic" +universe hierarchy. + +The spring of 1989 saw the first attempt at documenting the system +usage, with a number of papers describing the formalism: + +- *Metamathematical Investigations of a Calculus of Constructions*, by + Thierry Coquand :cite:`C90`, + +- *Inductive definitions in the Calculus of Constructions*, by + Christine Paulin-Mohrin, + +- *Extracting Fω's programs from proofs in the Calculus of + Constructions*, by Christine Paulin-Mohring* :cite:`P89`, + +- *The Constructive Engine*, by Gérard Huet :cite:`H89`, + +as well as a number of user guides: + +- *A short user's guide for the Constructions*, Version 4.10, by Gérard Huet +- *A Vernacular Syllabus*, by Gilles Dowek. +- *The Tactics Theorem Prover, User's guide*, Version 4.10, by Thierry + Coquand. + +Stable V4.10, released on May 1st, 1989, was then a mature system, +distributed with CAML V2.6. + +In the mean time, Thierry Coquand and Christine Paulin-Mohring had +been investigating how to add native inductive types to the Calculus +of Constructions, in the manner of Per Martin-Löf's Intuitionistic +Type Theory. The impredicative encoding had already been presented in: +F. Pfenning and C. Paulin-Mohring. *Inductively defined types in the +Calculus of Constructions* :cite:`PP90`. An extension of the calculus +with primitive inductive types appeared in: T. Coquand and +C. Paulin-Mohring. *Inductively defined types* :cite:`CP90`. + +This led to the Calculus of Inductive Constructions, logical formalism +implemented in Versions 5 upward of the system, and documented in: +C. Paulin-Mohring. *Inductive Definitions in the System Coq - Rules +and Properties* :cite:`P93`. + +The last version of CONSTR is Version 4.11, which was last distributed +in the spring of 1990. It was demonstrated at the first workshop of +the European Basic Research Action Logical Frameworks In Sophia +Antipolis in May 1990. + +Version 5 +--------- + +At the end of 1989, Version 5.1 was started, and renamed as the system +Coq for the Calculus of Inductive Constructions. It was then ported to +the new stand-alone implementation of ML called Caml-light. + +In 1990 many changes occurred. Thierry Coquand left for Chalmers +University in Göteborg. Christine Paulin-Mohring took a CNRS +researcher position at the LIP laboratory of École Normale Supérieure +de Lyon. Project Formel was terminated, and gave rise to two teams: +Cristal at INRIA-Roquencourt, that continued developments in +functional programming with Caml-light then OCaml, and Coq, continuing +the type theory research, with a joint team headed by Gérard Huet at +INRIA-Rocquencourt and Christine Paulin-Mohring at the LIP laboratory +of CNRS-ENS Lyon. + +Chetan Murthy joined the team in 1991 and became the main software +architect of Version 5. He completely rehauled the implementation for +efficiency. Versions 5.6 and 5.8 were major distributed versions, +with complete documentation and a library of users' developements. The +use of the RCS revision control system, and systematic ChangeLog +files, allow a more precise tracking of the software developments. + +| September 2015 + +| Thierry Coquand, Gérard Huet and Christine Paulin-Mohring. +| + +Version 6.1 +----------- The present version 6.1 of |Coq| is based on the V5.10 architecture. It was ported to the new language Objective Caml by Bruno Barras. The @@ -226,8 +557,8 @@ Barras. | Christine Paulin | -Credits: addendum for version 6.2 ---------------------------------- +Version 6.2 +----------- In version 6.2 of |Coq|, the parsing is done using camlp4, a preprocessor and pretty-printer for CAML designed by Daniel de Rauglaudre at INRIA. @@ -271,8 +602,8 @@ Loiseleur. | Christine Paulin | -Credits: addendum for version 6.3 ---------------------------------- +Version 6.3 +----------- The main changes in version V6.3 were the introduction of a few new tactics and the extension of the guard condition for fixpoint @@ -304,8 +635,8 @@ Monin from CNET Lannion. | Christine Paulin | -Credits: versions 7 -------------------- +Versions 7 +---------- The version V7 is a new implementation started in September 1999 by Jean-Christophe Filliâtre. This is a major revision with respect to the @@ -393,8 +724,8 @@ J.-F. Monin from France Telecom R & D. | Hugo Herbelin & Christine Paulin | -Credits: version 8.0 --------------------- +Version 8.0 +----------- Coq version 8 is a major revision of the |Coq| proof assistant. First, the underlying logic is slightly different. The so-called *impredicativity* @@ -495,8 +826,8 @@ under the responsibility of Christine Paulin. | (updated Apr. 2006) | -Credits: version 8.1 --------------------- +Version 8.1 +----------- Coq version 8.1 adds various new functionalities. @@ -574,8 +905,8 @@ and Yale University. | Hugo Herbelin | -Credits: version 8.2 --------------------- +Version 8.2 +----------- Coq version 8.2 adds new features, new libraries and improves on many various aspects. @@ -668,8 +999,8 @@ the Coq-Club mailing list. | Hugo Herbelin | -Credits: version 8.3 --------------------- +Version 8.3 +----------- Coq version 8.3 is before all a transition version with refinements or extensions of the existing features and libraries and a new tactic nsatz @@ -742,8 +1073,8 @@ Pierce for the excellent teaching materials they provided. | Hugo Herbelin | -Credits: version 8.4 --------------------- +Version 8.4 +----------- Coq version 8.4 contains the result of three long-term projects: a new modular library of arithmetic by Pierre Letouzey, a new proof engine by @@ -898,8 +1229,8 @@ Eelis van der Weegen. | Hugo Herbelin | -Credits: version 8.5 --------------------- +Version 8.5 +----------- Coq version 8.5 contains the result of five specific long-term projects: @@ -916,7 +1247,7 @@ Coq version 8.5 contains the result of five specific long-term projects: Matthieu Sozeau. - An implementation of primitive projections with - :math:`\eta`-conversion bringing significant performance improvements + :math:`\eta`\-conversion bringing significant performance improvements when using records by Matthieu Sozeau. The full integration of the proof engine, by Arnaud Spiwack and @@ -967,10 +1298,10 @@ messages in case of inconsistencies and allowing higher-level algorithms like unification to be entirely type safe. The internal representation of universes has been modified but this is invisible to the user. -The underlying logic has been extended with :math:`\eta`-conversion for +The underlying logic has been extended with :math:`\eta`\-conversion for records defined with primitive projections by Matthieu Sozeau. This -additional form of :math:`\eta`-conversion is justified using the same -principle than the previously added :math:`\eta`-conversion for function +additional form of :math:`\eta`\-conversion is justified using the same +principle than the previously added :math:`\eta`\-conversion for function types, based on formulations of the Calculus of Inductive Constructions with typed equality. Primitive projections, which do not carry the parameters of the record and are rigid names (not defined as a @@ -1052,8 +1383,8 @@ Tankink. Maxime Dénès coordinated the release process. | Hugo Herbelin, Matthieu Sozeau and the |Coq| development team | -Credits: version 8.6 --------------------- +Version 8.6 +----------- Coq version 8.6 contains the result of refinements, stabilization of 8.5’s features and cleanups of the internals of the system. Over the @@ -1192,8 +1523,8 @@ Dénès to put together a |Coq| consortium. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.7 --------------------- +Version 8.7 +----------- |Coq| version 8.7 contains the result of refinements, stabilization of features and cleanups of the internals of the system along with a few new features. The @@ -1298,8 +1629,8 @@ system, is now upcoming and will rely on Inria’s newly created Foundation. | Matthieu Sozeau and the |Coq| development team | -Credits: version 8.8 --------------------- +Version 8.8 +----------- |Coq| version 8.8 contains the result of refinements and stabilization of features and deprecations, cleanups of the internals of the system along @@ -1405,8 +1736,8 @@ The contacts of the Coq Consortium are Yves Bertot and Maxime Dénès. | Matthieu Sozeau for the |Coq| development team | -Credits: version 8.9 --------------------- +Version 8.9 +----------- |Coq| version 8.9 contains the result of refinements and stabilization of features and deprecations or removals of deprecated features, diff --git a/doc/sphinx/dune b/doc/sphinx/dune index fff025c919..353d58c676 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1 +1,8 @@ (dirs :standard _static) + +(rule (targets README.gen.rst) + (deps (source_tree ../tools/coqrst) README.template.rst) + (action (run ../tools/coqrst/regen_readme.py %{targets}))) + +(alias (name refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 3ef88e6506..e05df65c63 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -963,10 +963,9 @@ such that :math:`Γ_I` is :math:`[I_1 :∀ Γ_P ,A_1 ;~…;~I_k :∀ Γ_P ,A_k]` .. inference:: W-Ind \WFE{Γ_P} - (E[Γ_P ] ⊢ A_j : s_j )_{j=1… k} (E[Γ_I ;Γ_P ] ⊢ C_i : s_{q_i} )_{i=1… n} ------------------------------------------ - \WF{E;~\ind{p}{Γ_I}{Γ_C}}{Γ} + \WF{E;~\ind{p}{Γ_I}{Γ_C}}{} provided that the following side conditions hold: @@ -976,7 +975,7 @@ provided that the following side conditions hold: context of parameters, + for :math:`j=1… k` we have that :math:`A_j` is an arity of sort :math:`s_j` and :math:`I_j ∉ E`, + for :math:`i=1… n` we have that :math:`C_i` is a type of constructor of :math:`I_{q_i}` which - satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ Γ ∪ E`. + satisfies the positivity condition for :math:`I_1 … I_k` and :math:`c_i ∉ E`. One can remark that there is a constraint between the sort of the arity of the inductive type and the sort of the type of its diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 963242ea72..d1b95e6203 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -264,17 +264,13 @@ arguments. The theorem are names ``f_equal2``, ``f_equal3``, ``f_equal4`` and ``f_equal5``. For instance ``f_equal3`` is defined the following way. -.. coqtop:: in +.. coqtop:: in abort Theorem f_equal3 : forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2) (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3. -.. coqtop:: none - - Abort. - .. _datatypes: Datatypes @@ -610,7 +606,10 @@ Finally, it gives the definition of the usual orderings ``le``, single: ge (term) single: gt (term) -.. coqtop:: in +.. This emits a notation already used warning but it won't be shown to + the user. + +.. coqtop:: in warn Inductive le (n:nat) : nat -> Prop := | le_n : le n n diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 437b8e557e..f1733a5ebf 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -247,11 +247,6 @@ Primitive Projections printing time (even though they are absent in the actual AST manipulated by the kernel). -.. flag:: Printing Primitive Projection Compatibility - - This compatibility option (on by default) governs the - printing of pattern matching over primitive records. - Primitive Record Types ++++++++++++++++++++++ @@ -297,8 +292,8 @@ the folded version delta-reduces to the unfolded version. This allows to precisely mimic the usual unfolding rules of constants. Projections obey the usual ``simpl`` flags of the ``Arguments`` command in particular. There is currently no way to input unfolded primitive projections at the -user-level, and one must use the :flag:`Printing Primitive Projection Compatibility` -to display unfolded primitive projections as matches and distinguish them from folded ones. +user-level, and there is no way to display unfolded projections differently +from folded ones. Compatibility Projections and :g:`match` @@ -1924,9 +1919,10 @@ applied to an unknown structure instance (an implicit argument) and a value. The complete documentation of canonical structures can be found in :ref:`canonicalstructures`; here only a simple example is given. -.. cmd:: Canonical Structure @qualid +.. cmd:: Canonical {? Structure } @qualid - This command declares :token:`qualid` as a canonical structure. + This command declares :token:`qualid` as a canonical instance of a + structure (a record). Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. @@ -1961,28 +1957,23 @@ in :ref:`canonicalstructures`; here only a simple example is given. Definition nat_setoid : Setoid := Build_Setoid eq_nat_equiv. - Canonical Structure nat_setoid. + Canonical nat_setoid. Thanks to :g:`nat_setoid` declared as canonical, the implicit arguments :g:`A` and :g:`B` can be synthesized in the next statement. - .. coqtop:: all + .. coqtop:: all abort Lemma is_law_S : is_law S. - .. coqtop:: none - - Abort. - .. note:: If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. - .. cmdv:: Canonical Structure @ident {? : @type } := @term + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the - declaration :n:`Canonical Structure @ident`. - + declaration :n:`Canonical @ident`. .. cmd:: Print Canonical Projections @@ -2269,3 +2260,52 @@ expression as described in :ref:`ltac`. This construction is useful when one wants to define complicated terms using highly automated tactics without resorting to writing the proof-term by means of the interactive proof engine. + +.. _primitive-integers: + +Primitive Integers +-------------------------------- + +The language of terms features 63-bit machine integers as values. The type of +such a value is *axiomatized*; it is declared through the following sentence +(excerpt from the :g:`Int63` module): + +.. coqdoc:: + + Primitive int := #int63_type. + +This type is equipped with a few operators, that must be similarly declared. +For instance, equality of two primitive integers can be decided using the :g:`Int63.eqb` function, +declared and specified as follows: + +.. coqdoc:: + + Primitive eqb := #int63_eq. + Notation "m '==' n" := (eqb m n) (at level 70, no associativity) : int63_scope. + + Axiom eqb_correct : forall i j, (i == j)%int63 = true -> i = j. + +The complete set of such operators can be obtained looking at the :g:`Int63` module. + +These primitive declarations are regular axioms. As such, they must be trusted and are listed by the +:g:`Print Assumptions` command, as in the following example. + +.. coqtop:: in reset + + From Coq Require Import Int63. + Lemma one_minus_one_is_zero : (1 - 1 = 0)%int63. + Proof. apply eqb_correct; vm_compute; reflexivity. Qed. + +.. coqtop:: all + + Print Assumptions one_minus_one_is_zero. + +The reduction machines (:tacn:`vm_compute`, :tacn:`native_compute`) implement +dedicated, efficient, rules to reduce the applications of these primitive +operations. + +These primitives, when extracted to OCaml (see :ref:`extraction`), are mapped to +types and functions of a :g:`Uint63` module. Said module is not produced by +extraction. Instead, it has to be provided by the user (if they want to compile +or execute the extracted code). For instance, an implementation of this module +can be taken from the kernel of Coq. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 9ab3f905e6..9bd41d79b7 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -1023,7 +1023,7 @@ Mutually defined inductive types .. coqtop:: in - Variables A B : Set. + Parameters A B : Set. Inductive tree : Set := node : A -> forest -> tree @@ -1533,7 +1533,7 @@ the following attributes names are recognized: .. example:: - .. coqtop:: all reset + .. coqtop:: all reset warn From Coq Require Program. #[program] Definition one : nat := S _. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 1b4d2315aa..eebf1f11e1 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -34,6 +34,11 @@ allow dynamic linking of tactics). You can switch to the OCaml toplevel with the command ``Drop.``, and come back to the |Coq| toplevel with the command ``Coqloop.loop();;``. +.. flag:: Coqtop Exit On Error + + This option, off by default, causes coqtop to exit with status code + ``1`` if a command produces an error instead of recovering from it. + Batch compilation (coqc) ------------------------ diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index bd16b70d02..b629d15b11 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -33,7 +33,7 @@ example, revisiting the first example of the inversion documentation: | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. Goal forall n m:nat, Le (S n) m -> P n m. @@ -53,7 +53,7 @@ rule of thumb, all the variables that appear inside constructors in the indices of the hypothesis should be generalized. This is exactly what the ``generalize_eqs_vars`` variant does: -.. coqtop:: all +.. coqtop:: all abort generalize_eqs_vars H. induction H. @@ -65,11 +65,11 @@ as well in this case, e.g.: .. coqtop:: none - Abort. + Require Import Coq.Program.Equality. .. coqtop:: in - Variable Q : forall (n m : nat), Le n m -> Prop. + Parameter Q : forall (n m : nat), Le n m -> Prop. Goal forall n m (p : Le (S n) m), Q (S n) m p. .. coqtop:: all @@ -88,11 +88,7 @@ automatically do such simplifications (which may involve the axiom K). This is what the ``simplify_dep_elim`` tactic from ``Coq.Program.Equality`` does. For example, we might simplify the previous goals considerably: -.. coqtop:: all - - Require Import Coq.Program.Equality. - -.. coqtop:: all +.. coqtop:: all abort induction p ; simplify_dep_elim. @@ -105,10 +101,6 @@ are ``dependent induction`` and ``dependent destruction`` that do induction or simply case analysis on the generalized hypothesis. For example we can redo what we’ve done manually with dependent destruction: -.. coqtop:: none - - Abort. - .. coqtop:: in Lemma ex : forall n m:nat, Le (S n) m -> P n m. @@ -117,7 +109,7 @@ redo what we’ve done manually with dependent destruction: intros n m H. -.. coqtop:: all +.. coqtop:: all abort dependent destruction H. @@ -126,17 +118,13 @@ destructed hypothesis actually appeared in the goal, the tactic would still be able to invert it, contrary to dependent inversion. Consider the following example on vectors: -.. coqtop:: none - - Abort. - .. coqtop:: in Set Implicit Arguments. .. coqtop:: in - Variable A : Set. + Parameter A : Set. .. coqtop:: in @@ -230,29 +218,21 @@ name. A term is either an application of: Once we have this datatype we want to do proofs on it, like weakening: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening : forall G D tau, term (G ; D) tau -> forall tau', term (G , tau' ; D) tau. -.. coqtop:: none - - Abort. - The problem here is that we can’t just use induction on the typing derivation because it will forget about the ``G ; D`` constraint appearing in the instance. A solution would be to rewrite the goal as: -.. coqtop:: in +.. coqtop:: in abort Lemma weakening' : forall G' tau, term G' tau -> forall G D, (G ; D) = G' -> forall tau', term (G, tau' ; D) tau. -.. coqtop:: none - - Abort. - With this proper separation of the index from the instance and the right induction loading (putting ``G`` and ``D`` after the inducted-on hypothesis), the proof will go through, but it is a very tedious @@ -349,7 +329,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable Ack : nat -> nat -> nat. + Parameter Ack : nat -> nat -> nat. .. coqtop:: in @@ -377,7 +357,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Variable g : nat -> nat -> nat. + Parameter g : nat -> nat -> nat. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 4f486a777d..52e3029b8f 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -200,7 +200,7 @@ following form: :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for - i = 0, ..., n and all have to be tactics. The :n:`v__i` is applied to the + i = 1, ..., n and all have to be tactics. The :n:`v__i` is applied to the i-th goal, for i = 1, ..., n. It fails if the number of focused goals is not exactly n. @@ -602,7 +602,7 @@ Failing .. example:: - .. coqtop:: all + .. coqtop:: all fail Goal True. Proof. fail. Abort. @@ -701,7 +701,7 @@ tactic .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac time_constr1 tac := let eval_early := match goal with _ => restart_timer "(depth 1)" end in @@ -716,7 +716,6 @@ tactic let y := time_constr1 ltac:(fun _ => eval compute in x) in y) in pose v. - Abort. Local definitions ~~~~~~~~~~~~~~~~~ @@ -847,7 +846,7 @@ We can carry out pattern matching on terms with: .. example:: - .. coqtop:: all + .. coqtop:: all abort Ltac f x := match x with @@ -859,10 +858,6 @@ We can carry out pattern matching on terms with: Goal True. f (3+4). - .. coqtop:: none - - Abort. - .. _ltac-match-goal: Pattern matching on goals @@ -1026,14 +1021,10 @@ Counting the goals Goal True /\ True /\ True. split;[|split]. - .. coqtop:: all + .. coqtop:: all abort all:pr_numgoals. - .. coqtop:: none - - Abort. - Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1162,6 +1153,15 @@ Printing |Ltac| tactics Debugging |Ltac| tactics ------------------------ +Backtraces +~~~~~~~~~~ + +.. flag:: Ltac Backtrace + + Setting this flag displays a backtrace on Ltac failures that can be useful + to find out what went wrong. It is disabled by default for performance + reasons. + Info trace ~~~~~~~~~~ @@ -1309,10 +1309,10 @@ performance issue. .. coqtop:: all - Set Ltac Profiling. - tac. - Show Ltac Profile. - Show Ltac Profile "omega". + Set Ltac Profiling. + tac. + Show Ltac Profile. + Show Ltac Profile "omega". .. coqtop:: in diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 24645a8cc3..27360f02d3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -30,7 +30,7 @@ When a proof is completed, the message ``Proof completed`` is displayed. One can then register this proof as a defined constant in the environment. Because there exists a correspondence between proofs and terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,Hue88`, |Coq| stores proofs as terms of |Cic|. Those +:cite:`How80,Bar81,Gir89,H89`, |Coq| stores proofs as terms of |Cic|. Those terms are called *proof terms*. @@ -529,16 +529,12 @@ Requesting information .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal exists n, n = 0. eexists ?[n]. Show n. - .. coqtop:: none - - Abort. - .. cmdv:: Show Script :name: Show Script @@ -739,14 +735,10 @@ Notes: split. - .. coqtop:: all + .. coqtop:: all abort 2: split. - .. coqtop:: none - - Abort. - .. .. coqtop:: none @@ -759,14 +751,10 @@ Notes: intros n. - .. coqtop:: all + .. coqtop:: all abort intros m. - .. coqtop:: none - - Abort. - This screen shot shows the result of applying a :tacn:`split` tactic that replaces one goal with 2 goals. Notice that the goal ``P 1`` is not highlighted at all after the split because it has not changed. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index ec97377128..b240cef40c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -215,7 +215,7 @@ construct differs from the latter in that .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -275,7 +275,7 @@ example, the null and all list function(al)s can be defined as follows: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -376,7 +376,7 @@ expressions such as .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -401,7 +401,7 @@ each point of use, e.g., the above definition can be written: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -464,7 +464,7 @@ defined by the following declaration: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -518,7 +518,7 @@ For example, the tactic :tacn:`pose <pose (ssreflect)>` supoprts parameters: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -639,7 +639,7 @@ The tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -652,11 +652,7 @@ The tactic: Lemma test x : f x + f x = f x. set t := f _. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart set t := {2}(f _). @@ -694,7 +690,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -715,7 +711,7 @@ conditions: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -736,7 +732,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -756,7 +752,7 @@ Moreover: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -789,7 +785,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -810,7 +806,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -831,7 +827,7 @@ An *occurrence switch* can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -862,7 +858,7 @@ selection. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -879,7 +875,7 @@ only one occurrence of the selected term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -910,7 +906,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -926,7 +922,7 @@ context of a goal thanks to the ``in`` tactical. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. @@ -1042,7 +1038,7 @@ constants to the goal. For example, the proof of [#3]_ - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1104,7 +1100,7 @@ The ``:`` tactical is used to operate on an element in the context. to encapsulate the inductive step in a single command: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1257,7 +1253,7 @@ The elim tactic .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1297,7 +1293,7 @@ existential metavariables of sort :g:`Prop`. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1477,7 +1473,7 @@ context to interpret wildcards; in particular it can accommodate the .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1752,7 +1748,7 @@ Clears are deferred until the end of the intro pattern. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -1813,7 +1809,7 @@ Block introduction .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1866,7 +1862,7 @@ deal with the possible parameters of the constants introduced. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1885,7 +1881,7 @@ under fresh |SSR| names. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1952,7 +1948,7 @@ be substituted. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -1989,19 +1985,17 @@ be substituted. Lemma test l : (length l) * 2 = length (l ++ l). case: (lastP l). - Applied to the same goal, the command: - ``case: l / (lastP l).`` - generates the same subgoals but ``l`` has been cleared from both contexts. + Applied to the same goal, the tactc ``case: l / (lastP l)`` + generates the same subgoals but ``l`` has been cleared from both contexts: - Again applied to the same goal, the command. + .. coqtop:: all restart - .. coqtop:: none + case: l / (lastP l). - Abort. + Again applied to the same goal: - .. coqtop:: all + .. coqtop:: all restart abort - Lemma test l : (length l) * 2 = length (l ++ l). case: {1 3}l / (lastP l). Note that selected occurrences on the left of the ``/`` @@ -2015,10 +2009,6 @@ be substituted. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test l : (length l) * 2 = length (l ++ l). @@ -2104,9 +2094,9 @@ into a closing one (similar to :tacn:`now`). Its general syntax is: :name: by :undocumented: -The Ltac expression :n:`by [@tactic | [@tactic | …]` is equivalent to -:n:`[by @tactic | by @tactic | ...]` and this form should be preferred -to the former. +The Ltac expression :n:`by [@tactic | @tactic | …]` is equivalent to +:n:`do [done | by @tactic | by @tactic | …]`, which corresponds to the +standard Ltac expression :n:`first [done | @tactic; done | @tactic; done | …]`. In the script provided as example in section :ref:`indentation_ssr`, the paragraph corresponding to each sub-case ends with a tactic line prefixed @@ -2260,7 +2250,7 @@ to the others. Here is a small example on lists. We define first a function which adds an element at the end of a given list. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2379,7 +2369,7 @@ between standard Ltac in and the |SSR| tactical in. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2454,7 +2444,7 @@ the holes are abstracted in term. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2468,7 +2458,7 @@ the holes are abstracted in term. The invokation of ``have`` is equivalent to: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2486,7 +2476,7 @@ tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2539,7 +2529,7 @@ the further use of the intermediate step. For instance, .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2567,7 +2557,7 @@ destruction of existential assumptions like in the tactic: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2594,7 +2584,7 @@ term for the intermediate lemma, using tactics of the form: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2615,7 +2605,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. From Coq Require Import Omega. @@ -2634,7 +2624,7 @@ Since the :token:`i_pattern` can be omitted, to avoid ambiguity, bound variables can be surrounded with parentheses even if no type is specified: -.. coqdoc:: +.. coqtop:: all restart have (x) : 2 * x = x + x by omega. @@ -2648,13 +2638,8 @@ copying the goal itself. .. example:: - .. coqtop:: none - - Abort All. + .. coqtop:: all restart abort - .. coqtop:: all - - Lemma test : True. have suff H : 2 + 2 = 3; last first. Note that H is introduced in the second goal. @@ -2675,10 +2660,9 @@ context entry name. .. coqtop:: none - Abort All. Set Printing Depth 15. - .. coqtop:: all + .. coqtop:: all abort Inductive Ord n := Sub x of x < n. Notation "'I_ n" := (Ord n) (at level 8, n at level 2, format "''I_' n"). @@ -2694,11 +2678,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. @@ -2711,11 +2691,7 @@ with have and an explicit term, they must be used as follows: .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. @@ -2734,11 +2710,7 @@ makes use of it). .. example:: - .. coqtop:: none - - Abort All. - - .. coqtop:: all + .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. @@ -2755,21 +2727,21 @@ typeclass inference. .. coqtop:: none - Abort All. - Axiom ty : Type. Axiom t : ty. Goal True. -+ .. coqtop:: in undo + .. coqtop:: all have foo : ty. Full inference for ``ty``. The first subgoal demands a proof of such instantiated statement. -+ .. coqdoc:: + .. A strange bug prevents using the coqtop directive here + + .. coqdoc:: have foo : ty := . @@ -2778,13 +2750,13 @@ typeclass inference. statement. Note that no proof term follows ``:=``, hence two subgoals are generated. -+ .. coqtop:: in undo + .. coqtop:: all restart have foo : ty := t. No inference for ``ty`` and ``t``. -+ .. coqtop:: in undo + .. coqtop:: all restart abort have foo := t. @@ -2833,10 +2805,9 @@ The ``have`` modifier can follow the ``suff`` tactic. .. coqtop:: none - Abort All. Axioms G P : Prop. - .. coqtop:: all + .. coqtop:: all abort Lemma test : G. suff have H : P. @@ -2901,10 +2872,6 @@ are unique. .. example:: - .. coqtop:: none - - Abort All. - .. coqtop:: all Lemma quo_rem_unicity d q1 q2 r1 r2 : @@ -2926,7 +2893,7 @@ pattern will be used to process its instance. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -2935,6 +2902,7 @@ pattern will be used to process its instance. Axiom P : nat -> Prop. Axioms eqn leqn : nat -> nat -> bool. + Declare Scope this_scope. Notation "a != b" := (eqn a b) (at level 70) : this_scope. Notation "a <= b" := (leqn a b) (at level 70) : this_scope. Open Scope this_scope. @@ -2975,7 +2943,7 @@ illustrated in the following example. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -2994,7 +2962,7 @@ illustrated in the following example. the pattern ``id (addx x)``, that would produce the following first subgoal - .. coqtop:: none reset + .. coqtop:: reset none From Coq Require Import ssreflect Omega. Set Implicit Arguments. @@ -3128,14 +3096,14 @@ An :token:`r_item` can be: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. - .. coqtop:: all + .. coqtop:: all abort Definition double x := x + x. Definition ddouble x := double (double x). @@ -3147,21 +3115,16 @@ An :token:`r_item` can be: The |SSR| terms containing holes are *not* typed as abstractions in this context. Hence the following script fails. - .. coqtop:: none - - Abort. - .. coqtop:: all Definition f := fun x y => x + y. Lemma test x y : x + y = f y x. - Fail rewrite -[f y]/(y + _). - but the following script succeeds + .. coqtop:: all fail - .. coqtop:: none + rewrite -[f y]/(y + _). - Restart. + but the following script succeeds .. coqtop:: all @@ -3252,7 +3215,7 @@ proof of basic results on natural numbers arithmetic. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3288,7 +3251,7 @@ side of the equality the user wants to rewrite. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3308,7 +3271,7 @@ the equality. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3331,7 +3294,7 @@ Occurrence switches and redex switches .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3360,7 +3323,7 @@ repetition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3390,7 +3353,7 @@ rewrite operations prescribed by the rules on the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3399,7 +3362,7 @@ rewrite operations prescribed by the rules on the current goal. Section Test. - .. coqtop:: all + .. coqtop:: all abort Variables (a b c : nat). Hypothesis eqab : a = b. @@ -3413,10 +3376,6 @@ rewrite operations prescribed by the rules on the current goal. ``(eqab, eqac)`` is actually a |Coq| term and we can name it with a definition: - .. coqtop:: none - - Abort. - .. coqtop:: all Definition multi1 := (eqab, eqac). @@ -3433,7 +3392,7 @@ literal matches have priority. .. example:: - .. coqtop:: all + .. coqtop:: all abort Definition d := a. Hypotheses eqd0 : d = 0. @@ -3450,11 +3409,7 @@ repeated anew. .. example:: - .. coqtop:: none - - Abort. - - .. coqtop:: all + .. coqtop:: all abort Hypothesis eq_adda_b : forall x, x + a = b. Hypothesis eq_adda_c : forall x, x + a = c. @@ -3477,10 +3432,6 @@ tactic rewrite ``(=~ multi1)`` is equivalent to ``rewrite multi1_rev``. .. example:: - .. coqtop:: none - - Abort. - .. coqtop:: all Hypothesis eqba : b = a. @@ -3536,7 +3487,7 @@ Anyway this tactic is *not* equivalent to .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3552,11 +3503,7 @@ Anyway this tactic is *not* equivalent to while the other tactic results in - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart abort rewrite (_ : forall x, x * 0 = 0). @@ -3590,7 +3537,7 @@ cases: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3613,13 +3560,9 @@ cases: there is no occurrence of the head symbol ``f`` of the rewrite rule in the goal. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart fail - Fail rewrite H. + rewrite H. Rewriting with ``H`` first requires unfolding the occurrences of ``f`` @@ -3627,21 +3570,13 @@ cases: occurrence), using tactic ``rewrite /f`` (for a global replacement of f by g) or ``rewrite pattern/f``, for a finer selection. - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite /f H. alternatively one can override the pattern inferred from ``H`` - .. coqtop:: none - - Undo. - - .. coqtop:: all + .. coqtop:: all restart rewrite [f _]H. @@ -3660,7 +3595,7 @@ corresponding new goals will be generated. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. Set Implicit Arguments. @@ -3668,7 +3603,7 @@ corresponding new goals will be generated. Unset Printing Implicit Defensive. Set Warnings "-notation-overridden". - .. coqtop:: all + .. coqtop:: all abort Axiom leq : nat -> nat -> bool. Notation "m <= n" := (leq m n) : nat_scope. @@ -3691,10 +3626,6 @@ corresponding new goals will be generated. As in :ref:`apply_ssr`, the ``ssrautoprop`` tactic is used to try to solve the existential variable. - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (x : 'I_2) y (H : y < 2) : Some x = insub 2 y. @@ -3743,7 +3674,7 @@ selective rewriting, blocking on the fly the reduction in the term ``t``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrfun ssrbool. From Coq Require Import List. @@ -3767,7 +3698,7 @@ definition. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3877,7 +3808,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3904,7 +3835,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3927,7 +3858,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -3948,7 +3879,7 @@ which the function is supplied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4128,7 +4059,7 @@ parentheses are required around more complex patterns. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4167,7 +4098,7 @@ Contextual patterns in rewrite .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4331,7 +4262,7 @@ generation (see section :ref:`generation_of_equations_ssr`). The following script illustrates a toy example of this feature. Let us define a function adding an element at the end of a list: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect List. Set Implicit Arguments. @@ -4406,7 +4337,7 @@ Here is an example of a regular, but nontrivial, eliminator. Here is a toy example illustrating this feature. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4433,7 +4364,7 @@ Here is an example of a regular, but nontrivial, eliminator. elim/plus_ind: {z}_. elim/plus_ind: z / _. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4458,7 +4389,7 @@ Here is an example of a regular, but nontrivial, eliminator. ``plus (plus x y) z`` thus instantiating the last ``_`` with ``z``. Note that the tactic: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4488,7 +4419,7 @@ Here is an example of a truncated eliminator: Consider the goal: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect FunInd. Set Implicit Arguments. @@ -4552,7 +4483,7 @@ disjunction. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4573,7 +4504,7 @@ disjunction. This operation is so common that the tactic shell has specific syntax for it. The following scripts: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4586,13 +4517,13 @@ disjunction. Lemma test a : P (a || a) -> True. - .. coqtop:: all undo + .. coqtop:: all move=> HPa; move/P2Q: HPa => HQa. or more directly: - .. coqtop:: all undo + .. coqtop:: all restart move/P2Q=> HQa. @@ -4608,7 +4539,7 @@ equation name generation mechanism (see section :ref:`generation_of_equations_ss .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4641,7 +4572,7 @@ relevant for the current goal. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4685,7 +4616,7 @@ assumption to some given arguments. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4714,7 +4645,7 @@ bookkeeping steps. The following example use the ``~~`` prenex notation for boolean negation: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4770,7 +4701,7 @@ analysis: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect. Set Implicit Arguments. @@ -4787,7 +4718,7 @@ analysis .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4842,7 +4773,7 @@ For instance, the following lemma: .. coqdoc:: - Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). + Lemma andP: forall b1 b2, reflect (b1 /\ b2) (b1 && b2). relates the boolean conjunction to the logical one ``/\``. Note that in ``andP``, ``b1`` and ``b2`` are two boolean variables and the @@ -4877,7 +4808,7 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4890,11 +4821,15 @@ Let us compare the respective behaviors of ``andE`` and ``andP``. Lemma test (b1 b2 : bool) : if (b1 && b2) then b1 else ~~(b1||b2). - .. coqtop:: all undo + .. coqtop:: all case: (@andE b1 b2). - .. coqtop:: all undo + .. coqtop:: none + + Restart. + + .. coqtop:: all case: (@andP b1 b2). @@ -4914,7 +4849,7 @@ The view mechanism is compatible with reflect predicates. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -4922,17 +4857,13 @@ The view mechanism is compatible with reflect predicates. Unset Printing Implicit Defensive. Section Test. - .. coqtop:: all + .. coqtop:: all abort Lemma test (a b : bool) (Ha : a) (Hb : b) : a /\ b. apply/andP. Conversely - .. coqtop:: none - - Abort. - .. coqtop:: all Lemma test (a b : bool) : a /\ b -> a. @@ -5036,7 +4967,7 @@ but they also allow complex transformation, involving negations. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5069,7 +5000,7 @@ actually uses its propositional interpretation. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5131,7 +5062,7 @@ In this context, the identity view can be used when no view has to be applied: .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5147,7 +5078,7 @@ In this context, the identity view can be used when no view has to be applied: The same goal can be decomposed in several ways, and the user may choose the most convenient interpretation. - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5223,7 +5154,7 @@ pass a given hypothesis to a lemma. .. example:: - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. @@ -5282,7 +5213,7 @@ equivalences are indeed taken into account, otherwise only single looks for any notation that contains fragment as a substring. If the ``ssrbool.v`` library is imported, the command: ``Search "~~".`` answers : - .. coqtop:: reset + .. coqtop:: reset none From Coq Require Import ssreflect ssrbool. Set Implicit Arguments. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0bcfce2322..7b395900e9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -378,7 +378,7 @@ Examples: .. coqtop:: reset none - Variables (A : Prop) (B: nat -> Prop) (C: Prop). + Parameters (A : Prop) (B: nat -> Prop) (C: Prop). .. coqtop:: out @@ -730,15 +730,15 @@ Applying theorems .. coqtop:: reset in - Variable R : nat -> nat -> Prop. + Parameter R : nat -> nat -> Prop. - Hypothesis Rtrans : forall x y z:nat, R x y -> R y z -> R x z. + Axiom Rtrans : forall x y z:nat, R x y -> R y z -> R x z. - Variables n m p : nat. + Parameters n m p : nat. - Hypothesis Rnm : R n m. + Axiom Rnm : R n m. - Hypothesis Rmp : R m p. + Axiom Rmp : R m p. Consider the goal ``(R n p)`` provable using the transitivity of ``R``: @@ -749,39 +749,39 @@ Applying theorems The direct application of ``Rtrans`` with ``apply`` fails because no value for ``y`` in ``Rtrans`` is found by ``apply``: - .. coqtop:: all + .. coqtop:: all fail - Fail apply Rtrans. + apply Rtrans. A solution is to ``apply (Rtrans n m p)`` or ``(Rtrans n m)``. - .. coqtop:: all undo + .. coqtop:: all apply (Rtrans n m p). Note that ``n`` can be inferred from the goal, so the following would work too. - .. coqtop:: in undo + .. coqtop:: in restart apply (Rtrans _ m). More elegantly, ``apply Rtrans with (y:=m)`` allows only mentioning the unknown m: - .. coqtop:: in undo + .. coqtop:: in restart apply Rtrans with (y := m). Another solution is to mention the proof of ``(R x y)`` in ``Rtrans`` - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (1 := Rnm). ... or the proof of ``(R y z)``. - .. coqtop:: all undo + .. coqtop:: all restart apply Rtrans with (2 := Rmp). @@ -789,7 +789,7 @@ Applying theorems finding ``m``. Then one can apply the hypotheses ``Rnm`` and ``Rmp``. This instantiates the existential variable and completes the proof. - .. coqtop:: all + .. coqtop:: all restart abort eapply Rtrans. @@ -2332,6 +2332,7 @@ and an explanation of the underlying technique. where :n:`@ident` is the identifier for the last introduced hypothesis. .. tacv:: inversion_clear @ident + :name: inversion_clear This behaves as :n:`inversion` and then erases :n:`@ident` from the context. @@ -2490,47 +2491,51 @@ and an explanation of the underlying technique. *Non-dependent inversion*. - Let us consider the relation Le over natural numbers and the following - variables: + Let us consider the relation :g:`Le` over natural numbers: - .. coqtop:: all reset + .. coqtop:: reset in Inductive Le : nat -> nat -> Set := | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Let us consider the following goal: .. coqtop:: none + Section Section. + Variable P : nat -> nat -> Prop. + Variable Q : forall n m:nat, Le n m -> Prop. Goal forall n m, Le (S n) m -> P n m. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - To prove the goal, we may need to reason by cases on H and to derive - that m is necessarily of the form (S m 0 ) for certain m 0 and that - (Le n m 0 ). Deriving these conditions corresponds to proving that the - only possible constructor of (Le (S n) m) isLeS and that we can invert - the-> in the type of LeS. This inversion is possible because Le is the - smallest set closed by the constructors LeO and LeS. + To prove the goal, we may need to reason by cases on :g:`H` and to derive + that :g:`m` is necessarily of the form :g:`(S m0)` for certain :g:`m0` and that + :g:`(Le n m0)`. Deriving these conditions corresponds to proving that the only + possible constructor of :g:`(Le (S n) m)` is :g:`LeS` and that we can invert + the arrow in the type of :g:`LeS`. This inversion is possible because :g:`Le` + is the smallest set closed by the constructors :g:`LeO` and :g:`LeS`. - .. coqtop:: undo all + .. coqtop:: all inversion_clear H. - Note that m has been substituted in the goal for (S m0) and that the - hypothesis (Le n m0) has been added to the context. + Note that :g:`m` has been substituted in the goal for :g:`(S m0)` and that the + hypothesis :g:`(Le n m0)` has been added to the context. - Sometimes it is interesting to have the equality m=(S m0) in the - context to use it after. In that case we can use inversion that does + Sometimes it is interesting to have the equality :g:`m = (S m0)` in the + context to use it after. In that case we can use :tacn:`inversion` that does not clear the equalities: - .. coqtop:: undo all + .. coqtop:: none restart + + intros. + + .. coqtop:: all inversion H. @@ -2540,31 +2545,26 @@ and an explanation of the underlying technique. Let us consider the following goal: - .. coqtop:: reset none + .. coqtop:: none - Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0 n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Variable P : nat -> nat -> Prop. - Variable Q : forall n m:nat, Le n m -> Prop. + Abort. Goal forall n m (H:Le (S n) m), Q (S n) m H. - intros. - .. coqtop:: all + .. coqtop:: out - Show. + intros. - As H occurs in the goal, we may want to reason by cases on its - structure and so, we would like inversion tactics to substitute H by + As :g:`H` occurs in the goal, we may want to reason by cases on its + structure and so, we would like inversion tactics to substitute :g:`H` by the corresponding @term in constructor form. Neither :tacn:`inversion` nor - :n:`inversion_clear` do such a substitution. To have such a behavior we + :tacn:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all dependent inversion_clear H. - Note that H has been substituted by (LeS n m0 l) andm by (S m0). + Note that :g:`H` has been substituted by :g:`(LeS n m0 l)` and :g:`m` by :g:`(S m0)`. .. example:: @@ -2933,6 +2933,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. + .. tacv:: now_show @term + + This is a synonym of :n:`change @term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -3315,7 +3321,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. example:: - .. coqtop:: all + .. coqtop:: all abort Goal ~0=0. unfold not. @@ -3323,10 +3329,6 @@ the conversion in hypotheses :n:`{+ @ident}`. pattern (0 = 0). fold not. - .. coqtop:: none - - Abort. - .. tacv:: fold {+ @term} Equivalent to :n:`fold @term ; ... ; fold @term`. @@ -3681,11 +3683,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Local is useless since hints do not survive anyway to the closure of sections. - .. cmdv:: Local Hint @hint_definition - - Idem for the core database. - - .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} : @ident :name: Hint Resolve This command adds :n:`simple apply @term` to the hint list with the head @@ -3704,16 +3702,16 @@ The general command to add a hint to some databases :n:`{+ @ident}` is typical example of a hint that is used only by :tacn:`eauto` is a transitivity lemma. - .. exn:: @term cannot be used as a hint + .. exn:: @term cannot be used as a hint - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + The head symbol of the type of :n:`@term` is a bound variable + such that this tactic cannot be associated to a constant. - .. cmdv:: Hint Resolve {+ @term} + .. cmdv:: Hint Resolve {+ @term} : @ident Adds each :n:`Hint Resolve @term`. - .. cmdv:: Hint Resolve -> @term + .. cmdv:: Hint Resolve -> @term : @ident Adds the left-to-right implication of an equivalence as a hint (informally the hint will be used as :n:`apply <- @term`, although as mentionned @@ -3724,7 +3722,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds the right-to-left implication of an equivalence as a hint. - .. cmdv:: Hint Immediate @term + .. cmdv:: Hint Immediate @term : @ident :name: Hint Immediate This command adds :n:`simple apply @term; trivial` to the hint list associated @@ -3740,37 +3738,37 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} + .. cmdv:: Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. - .. cmdv:: Hint Constructors @ident + .. cmdv:: Hint Constructors @qualid : @ident :name: Hint Constructors - If :n:`@ident` is an inductive type, this command adds all its constructors as + If :token:`qualid` is an inductive type, this command adds all its constructors as hints of type ``Resolve``. Then, when the conclusion of current goal has the form - :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. + :n:`(@qualid ...)`, :tacn:`auto` will try to apply each constructor. - .. exn:: @ident is not an inductive type - :undocumented: + .. exn:: @qualid is not an inductive type + :undocumented: - .. cmdv:: Hint Constructors {+ @ident} + .. cmdv:: Hint Constructors {+ @qualid} : @ident - Adds each :n:`Hint Constructors @ident`. + Extends the previous command for several inductive types. - .. cmdv:: Hint Unfold @qualid + .. cmdv:: Hint Unfold @qualid : @ident :name: Hint Unfold This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :n:`@ident`. + used when the head constant of the goal is :token:`qualid`. Its cost is 4. - .. cmdv:: Hint Unfold {+ @ident} + .. cmdv:: Hint Unfold {+ @qualid} - Adds each :n:`Hint Unfold @ident`. + Extends the previous command for several defined constants. - .. cmdv:: Hint Transparent {+ @qualid} - Hint Opaque {+ @qualid} + .. cmdv:: Hint Transparent {+ @qualid} : @ident + Hint Opaque {+ @qualid} : @ident :name: Hint Transparent; Hint Opaque This adds transparency hints to the database, making :n:`@qualid` @@ -3779,8 +3777,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is discrimination network to relax or constrain it in the case of discriminated databases. - .. cmdv:: Hint Variables %( Transparent %| Opaque %) - Hint Constants %( Transparent %| Opaque %) + .. cmdv:: Hint Variables %( Transparent %| Opaque %) : @ident + Hint Constants %( Transparent %| Opaque %) : @ident :name: Hint Variables; Hint Constants This sets the transparency flag used during unification of @@ -3788,7 +3786,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is overwritting the existing settings of opacity. It is advised to use this just after a :cmd:`Create HintDb` command. - .. cmdv:: Hint Extern @num {? @pattern} => @tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic : @ident :name: Hint Extern This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and @@ -3799,7 +3797,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. coqtop:: in - Hint Extern 4 (~(_ = _)) => discriminate. + Hint Extern 4 (~(_ = _)) => discriminate : core. Now, when the head of the goal is a disequality, ``auto`` will try discriminate if it does not manage to solve the goal with hints with a @@ -3818,7 +3816,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Goal forall a b:list (nat * nat), {a = b} + {a <> b}. Info 1 auto with eqdec. - .. cmdv:: Hint Cut @regexp + .. cmdv:: Hint Cut @regexp : @ident :name: Hint Cut .. warning:: @@ -3852,7 +3850,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the initial cut expression being `emp`. - .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} : @ident :name: Hint Mode This sets an optional mode of use of the identifier :n:`@qualid`. When diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a98a46ba21..3e8dd25ee0 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1213,10 +1213,19 @@ Controlling the locality of commands occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. +.. _internal-registration-commands: + +Internal registration commands +-------------------------------- + +Due to their internal nature, the commands that are presented in this section +are not for general use. They are meant to appear only in standard libraries and +in support libraries of plug-ins. + .. _exposing-constants-to-ocaml-libraries: Exposing constants to OCaml libraries ----------------------------------------------------------------- +```````````````````````````````````````````````````````````````` .. cmd:: Register @qualid__1 as @qualid__2 @@ -1225,5 +1234,35 @@ Exposing constants to OCaml libraries calling :n:`Coqlib.lib_ref "@qualid__2"`; i.e., there is no need to known where is the constant defined (file, module, library, etc.). - Due to its internal nature, this command is not for general use. It is meant - to appear only in standard libraries and in support libraries of plug-ins. + As a special case, when the first segment of :n:`@qualid__2` is :g:`kernel`, + the constant is exposed to the kernel. For instance, the `Int63` module + features the following declaration: + + .. coqdoc:: + + Register bool as kernel.ind_bool. + + This makes the kernel aware of what is the type of boolean values. This + information is used for instance to define the return type of the + :g:`#int63_eq` primitive. + + .. seealso:: :ref:`primitive-integers` + +Inlining hints for the fast reduction machines +```````````````````````````````````````````````````````````````` + +.. cmd:: Register Inline @qualid + + This command gives as a hint to the reduction machines (VM and native) that + the body of the constant :n:`@qualid` should be inlined in the generated code. + +Registering primitive operations +```````````````````````````````` + +.. cmd:: Primitive @ident__1 := #@ident__2. + + Declares :n:`@ident__1` as the primitive operator :n:`#@ident__2`. When + running this command, the type of the primitive should be already known by + the kernel (this is achieved through this command for primitive types and + through the :cmd:`Register` command with the :g:`kernel` name-space for other + types). diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 4f46a80dcf..e5eb7eb4f5 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1115,6 +1115,8 @@ Binding arguments of a constant to an interpretation scope .. coqtop:: all Parameter g : bool -> bool. + Declare Scope mybool_scope. + Notation "@@" := true (only parsing) : bool_scope. Notation "@@" := false (only parsing): mybool_scope. @@ -1151,6 +1153,7 @@ Binding types of arguments to an interpretation scope .. coqtop:: in reset Parameter U : Set. + Declare Scope U_scope. Bind Scope U_scope with U. Parameter Uplus : U -> U -> U. Parameter P : forall T:Set, T -> U -> Prop. @@ -1575,7 +1578,7 @@ Numeral notations For example - .. coqtop:: all + .. coqtop:: all warn Check 90000. diff --git a/doc/stdlib/dune b/doc/stdlib/dune new file mode 100644 index 0000000000..7fe2493fbf --- /dev/null +++ b/doc/stdlib/dune @@ -0,0 +1,36 @@ +; This is an ad-hoc rule to ease the migration, it should be handled +; natively by Dune in the future. +(rule + (targets index-list.html) + (deps + make-library-index index-list.html.template hidden-files + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins)) + (action + (chdir %{project_root} + ; On windows run will fail + (bash "doc/stdlib/make-library-index doc/stdlib/index-list.html doc/stdlib/hidden-files")))) + +(rule + (targets html) + (deps + ; This will be replaced soon by `theories/**/*.v` soon, thanks to rgrinberg + (source_tree %{project_root}/theories) + (source_tree %{project_root}/plugins) + (:header %{project_root}/doc/common/styles/html/coqremote/header.html) + (:footer %{project_root}/doc/common/styles/html/coqremote/footer.html) + ; For .glob files, should be gone when Coq Dune is smarter. + (package coq)) + (action + (progn + (run mkdir -p html) + (bash "%{bin:coqdoc} -q -d html --with-header %{header} --with-footer %{footer} --multi-index --html -g -R %{project_root}/theories Coq -R %{project_root}/plugins Coq $(find %{project_root}/theories %{project_root}/plugins -name *.v)") + (run mv html/index.html html/genindex.html) + (with-stdout-to + _index.html + (progn (cat %{header}) (cat index-list.html) (cat %{footer}))) + (run cp _index.html html/index.html)))) + +(alias + (name stdlib-html) + (deps html)) diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 0dd9b3aa3e..eaf1b2c2ad 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -30,7 +30,7 @@ from sphinx import addnodes from sphinx.roles import XRefRole from sphinx.errors import ExtensionError from sphinx.util.nodes import set_source_info, set_role_source_info, make_refnode -from sphinx.util.logging import getLogger +from sphinx.util.logging import getLogger, get_node_location from sphinx.directives import ObjectDescription from sphinx.domains import Domain, ObjType, Index from sphinx.domains.std import token_xrefs @@ -38,7 +38,7 @@ from sphinx.ext import mathbase from . import coqdoc from .repl import ansicolors -from .repl.coqtop import CoqTop +from .repl.coqtop import CoqTop, CoqTopError from .notations.sphinx import sphinxify from .notations.plain import stringify_with_ellipses @@ -560,17 +560,17 @@ class CoqtopDirective(Directive): Example:: - .. coqtop:: in undo + .. coqtop:: in reset Print nat. Definition a := 1. The blank line after the directive is required. If you begin a proof, - include an ``Abort`` afterwards to reset coqtop for the next example. + use the ``abort`` option to reset coqtop for the next example. Here is a list of permissible options: - - Display options + - Display options (choose exactly one) - ``all``: Display input and output - ``in``: Display only input @@ -580,15 +580,18 @@ class CoqtopDirective(Directive): - Behavior options - ``reset``: Send a ``Reset Initial`` command before running this block - - ``undo``: Reset state after executing. Not compatible with ``reset``. + - ``fail``: Don't die if a command fails, implies ``warn`` (so no need to put both) + - ``warn``: Don't die if a command emits a warning + - ``restart``: Send a ``Restart`` command before running this block (only works in proof mode) + - ``abort``: Send an ``Abort All`` command after running this block (leaves all pending proofs if any) ``coqtop``\ 's state is preserved across consecutive ``.. coqtop::`` blocks of the same document (``coqrst`` creates a single ``coqtop`` process per reST source file). Use the ``reset`` option to reset Coq's state. """ has_content = True - required_arguments = 0 - optional_arguments = 1 + required_arguments = 1 + optional_arguments = 0 final_argument_whitespace = True option_spec = { 'name': directives.unchanged } directive_name = "coqtop" @@ -597,10 +600,8 @@ class CoqtopDirective(Directive): # Uses a ‘container’ instead of a ‘literal_block’ to disable # Pygments-based post-processing (we could also set rawsource to '') content = '\n'.join(self.content) - args = self.arguments[0].split() if self.arguments else ['in'] - if 'all' in args: - args.extend(['in', 'out']) - node = nodes.container(content, coqtop_options = list(set(args)), + args = self.arguments[0].split() + node = nodes.container(content, coqtop_options = set(args), classes=['coqtop', 'literal-block']) self.add_name(node) return [node] @@ -827,22 +828,45 @@ class CoqtopBlocksTransform(Transform): return re.split(r"(?<=(?<!\.)\.)\s+", source) @staticmethod - def parse_options(options): + def parse_options(node): """Parse options according to the description in CoqtopDirective.""" - opt_undo = 'undo' in options + + options = node['coqtop_options'] + + # Behavior options opt_reset = 'reset' in options - opt_all, opt_none = 'all' in options, 'none' in options - opt_input, opt_output = opt_all or 'in' in options, opt_all or 'out' in options + opt_fail = 'fail' in options + opt_warn = 'warn' in options + opt_restart = 'restart' in options + opt_abort = 'abort' in options + options = options - {'reset', 'fail', 'warn', 'restart', 'abort'} - unexpected_options = list(set(options) - set(('reset', 'undo', 'all', 'none', 'in', 'out'))) + unexpected_options = list(options - {'all', 'none', 'in', 'out'}) if unexpected_options: - raise ValueError("Unexpected options for .. coqtop:: {}".format(unexpected_options)) - elif (opt_input or opt_output) and opt_none: - raise ValueError("Inconsistent options for .. coqtop:: ‘none’ with ‘in’, ‘out’, or ‘all’") - elif opt_reset and opt_undo: - raise ValueError("Inconsistent options for .. coqtop:: ‘undo’ with ‘reset’") - - return opt_undo, opt_reset, opt_input and not opt_none, opt_output and not opt_none + loc = get_node_location(node) + raise ExtensionError("{}: Unexpected options for .. coqtop:: {}".format(loc,unexpected_options)) + + # Display options + if len(options) != 1: + loc = get_node_location(node) + raise ExtensionError("{}: Exactly one display option must be passed to .. coqtop::".format(loc)) + + opt_all = 'all' in options + opt_none = 'none' in options + opt_input = 'in' in options + opt_output = 'out' in options + + return { + 'reset': opt_reset, + 'fail': opt_fail, + # if errors are allowed, then warnings too + # and they should be displayed as warnings, not errors + 'warn': opt_warn or opt_fail, + 'restart': opt_restart, + 'abort': opt_abort, + 'input': opt_input or opt_all, + 'output': opt_output or opt_all + } @staticmethod def block_classes(should_show, contents=None): @@ -866,36 +890,63 @@ class CoqtopBlocksTransform(Transform): blocks.append(re.sub("^", " ", output, flags=re.MULTILINE) + "\n") return '\n'.join(blocks) + def add_coq_output_1(self, repl, node): + options = self.parse_options(node) + + pairs = [] + + if options['restart']: + repl.sendone('Restart.') + if options['reset']: + repl.sendone('Reset Initial.') + repl.send_initial_options() + if options['fail']: + repl.sendone('Unset Coqtop Exit On Error.') + if options['warn']: + repl.sendone('Set Warnings "default".') + for sentence in self.split_sentences(node.rawsource): + pairs.append((sentence, repl.sendone(sentence))) + if options['abort']: + repl.sendone('Abort All.') + if options['fail']: + repl.sendone('Set Coqtop Exit On Error.') + if options['warn']: + repl.sendone('Set Warnings "+default".') + + dli = nodes.definition_list_item() + for sentence, output in pairs: + # Use Coqdoc to highlight input + in_chunks = highlight_using_coqdoc(sentence) + dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(options['input'])) + # Parse ANSI sequences to highlight output + out_chunks = AnsiColorsParser().colorize_str(output) + dli += nodes.definition(output, *out_chunks, classes=self.block_classes(options['output'], output)) + node.clear() + node.rawsource = self.make_rawsource(pairs, options['input'], options['output']) + node['classes'].extend(self.block_classes(options['input'] or options['output'])) + node += nodes.inline('', '', classes=['coqtop-reset'] * options['reset']) + node += nodes.definition_list(node.rawsource, dli) + def add_coqtop_output(self): """Add coqtop's responses to a Sphinx AST Finds nodes to process using is_coqtop_block.""" with CoqTop(color=True) as repl: + repl.send_initial_options() for node in self.document.traverse(CoqtopBlocksTransform.is_coqtop_block): - options = node['coqtop_options'] - opt_undo, opt_reset, opt_input, opt_output = self.parse_options(options) - - if opt_reset: - repl.sendone("Reset Initial.") - pairs = [] - for sentence in self.split_sentences(node.rawsource): - pairs.append((sentence, repl.sendone(sentence))) - if opt_undo: - repl.sendone("Undo {}.".format(len(pairs))) - - dli = nodes.definition_list_item() - for sentence, output in pairs: - # Use Coqdoq to highlight input - in_chunks = highlight_using_coqdoc(sentence) - dli += nodes.term(sentence, '', *in_chunks, classes=self.block_classes(opt_input)) - # Parse ANSI sequences to highlight output - out_chunks = AnsiColorsParser().colorize_str(output) - dli += nodes.definition(output, *out_chunks, classes=self.block_classes(opt_output, output)) - node.clear() - node.rawsource = self.make_rawsource(pairs, opt_input, opt_output) - node['classes'].extend(self.block_classes(opt_input or opt_output)) - node += nodes.inline('', '', classes=['coqtop-reset'] * opt_reset) - node += nodes.definition_list(node.rawsource, dli) + try: + self.add_coq_output_1(repl, node) + except CoqTopError as err: + import textwrap + MSG = ("{}: Error while sending the following to coqtop:\n{}" + + "\n coqtop output:\n{}" + + "\n Full error text:\n{}") + indent = " " + loc = get_node_location(node) + le = textwrap.indent(str(err.last_sentence), indent) + bef = textwrap.indent(str(err.before), indent) + fe = textwrap.indent(str(err.err), indent) + raise ExtensionError(MSG.format(loc, le, bef, fe)) @staticmethod def merge_coqtop_classes(kept_node, discarded_node): diff --git a/doc/tools/coqrst/regen_readme.py b/doc/tools/coqrst/regen_readme.py index e56882a521..0c15d7334c 100755 --- a/doc/tools/coqrst/regen_readme.py +++ b/doc/tools/coqrst/regen_readme.py @@ -10,6 +10,17 @@ SCRIPT_DIR = path.dirname(path.abspath(__file__)) if __name__ == "__main__" and __package__ is None: sys.path.append(path.dirname(SCRIPT_DIR)) +SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") +README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") + +if len(sys.argv) == 1: + README_PATH = path.join(SPHINX_DIR, "README.rst") +elif len(sys.argv) == 2: + README_PATH = sys.argv[1] +else: + print ("usage: {} [FILE]".format(sys.argv[0])) + sys.exit(1) + import sphinx from coqrst import coqdomain @@ -23,10 +34,6 @@ def format_docstring(template, obj, *strs): strs = strs + (FIRST_LINE_BLANKS.sub(r"\1\n", docstring),) return template.format(*strs) -SPHINX_DIR = path.join(SCRIPT_DIR, "../../sphinx/") -README_PATH = path.join(SPHINX_DIR, "README.rst") -README_TEMPLATE_PATH = path.join(SPHINX_DIR, "README.template.rst") - def notation_symbol(d): return " :black_nib:" if issubclass(d, coqdomain.NotationObject) else "" diff --git a/doc/tools/coqrst/repl/coqtop.py b/doc/tools/coqrst/repl/coqtop.py index 3ff00eaaf3..26f6255069 100644 --- a/doc/tools/coqrst/repl/coqtop.py +++ b/doc/tools/coqrst/repl/coqtop.py @@ -20,6 +20,14 @@ import re import pexpect + +class CoqTopError(Exception): + def __init__(self, err, last_sentence, before): + super().__init__() + self.err = err + self.before = before + self.last_sentence = last_sentence + class CoqTop: """Create an instance of coqtop. @@ -41,13 +49,10 @@ class CoqTop: the ansicolors module) :param args: Additional arugments to coqtop. """ - BOOT = True - if os.getenv('COQBOOT') == "no": - BOOT = False self.coqtop_bin = coqtop_bin or os.path.join(os.getenv('COQBIN', ""), "coqtop") if not pexpect.utils.which(self.coqtop_bin): raise ValueError("coqtop binary not found: '{}'".format(self.coqtop_bin)) - self.args = (args or []) + ["-boot"] * BOOT + ["-color", "on"] * color + self.args = (args or []) + ["-color", "on"] * color self.coqtop = None def __enter__(self): @@ -63,7 +68,7 @@ class CoqTop: self.coqtop.kill(9) def next_prompt(self): - "Wait for the next coqtop prompt, and return the output preceeding it." + """Wait for the next coqtop prompt, and return the output preceeding it.""" self.coqtop.expect(CoqTop.COQTOP_PROMPT, timeout = 10) return self.coqtop.before @@ -75,15 +80,18 @@ class CoqTop: """ # Suppress newlines, but not spaces: they are significant in notations sentence = re.sub(r"[\r\n]+", " ", sentence).strip() - self.coqtop.sendline(sentence) try: + self.coqtop.sendline(sentence) output = self.next_prompt() - except: - print("Error while sending the following sentence to coqtop: {}".format(sentence)) - raise - # print("Got {}".format(repr(output))) + except Exception as err: + raise CoqTopError(err, sentence, self.coqtop.before) return output + def send_initial_options(self): + """Options to send when starting the toplevel and after a Reset Initial.""" + self.sendone('Set Coqtop Exit On Error.') + self.sendone('Set Warnings "+default".') + def sendmany(*sentences): """A small demo: send each sentence in sentences and print the output""" with CoqTop() as coqtop: |