diff options
| -rw-r--r-- | CONTRIBUTING.md | 23 | ||||
| -rw-r--r-- | dev/build/windows/makecoq_mingw.sh | 2 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 572 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 14 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 103 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 43 | ||||
| -rw-r--r-- | doc/sphinx/addendum/parallel-proof-processing.rst | 17 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 4 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coqide.rst | 29 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 59 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 37 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 278 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4202.v | 10 |
19 files changed, 686 insertions, 640 deletions
diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md index 9bd3d0b7c7..cd4a246bb4 100644 --- a/CONTRIBUTING.md +++ b/CONTRIBUTING.md @@ -56,9 +56,19 @@ Whitespace discipline (do not indent using tabs, no trailing spaces, text files Here are a few tags Coq developers may add to your PR and what they mean. In general feedback and requests for you as the pull request author will be in the comments and tags are only used to organize pull requests. -- [needs: rebase](https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22) indicates the PR should be rebased on top of the latest `master` branch. See the [GitHub documentation](https://help.github.com/articles/about-git-rebase/) for a brief introduction to using `git rebase`. -- [needs: fixing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22) indicates the PR needs a fix, as discussed in the comments. -- [needs: benchmarking](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22) and [needs: testing](https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22) indicate the PR needs testing beyond what the test suite can handle. For example, performance benchmarking is currently performed with a different infrastructure. Unless some followup is specifically requested you aren't expected to do this additional testing. +- [needs: rebase][rebase-label] indicates the PR should be rebased on top of + the latest base branch (usually `master`). See the + [GitHub documentation](https://help.github.com/articles/about-git-rebase/) + for a brief introduction to using `git rebase`. + This label will be automatically added if you open or synchronize your PR and + it is not up-to-date with the base branch. So please, do not forget to rebase + your branch every time you update it. +- [needs: fixing][fixing-label] indicates the PR needs a fix, as discussed in the comments. +- [needs: benchmarking][benchmarking-label] and [needs: testing][testing-label] + indicate the PR needs testing beyond what the test suite can handle. + For example, performance benchmarking is currently performed with a different + infrastructure ([documented in the wiki][jenkins-doc]). Unless some followup + is specifically requested you aren't expected to do this additional testing. To learn more about the merging process, you can read the [merging documentation for Coq maintainers](dev/doc/MERGING.md). @@ -98,3 +108,10 @@ External plugins / libraries contribute to create a successful ecosystem around Ask and answer questions on [Stack Exchange](https://stackexchange.com/filters/299857/questions-tagged-coq-on-stackexchange-sites) which has a helpful community of Coq users. Hang out on the Coq IRC channel, `irc://irc.freenode.net/#coq`, and help answer questions. + +[rebase-label]: https://github.com/coq/coq/pulls?utf8=%E2%9C%93&q=is%3Aopen%20is%3Apr%20label%3A%22needs%3A%20rebase%22 +[fixing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+fixing%22 +[benchmarking-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+benchmarking%22 +[testing-label]: https://github.com/coq/coq/pulls?q=is%3Aopen+is%3Apr+label%3A%22needs%3A+testing%22 + +[jenkins-doc]: https://github.com/coq/coq/wiki/Jenkins-(automated-benchmarking) diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh index da5ac2b15c..aee4dd74d8 100644 --- a/dev/build/windows/makecoq_mingw.sh +++ b/dev/build/windows/makecoq_mingw.sh @@ -793,7 +793,7 @@ function make_ln { function make_ocaml { get_flex_dll_link_bin - if build_prep http://caml.inria.fr/pub/distrib/ocaml-4.07 ocaml-4.07.0 tar.gz 1 ; then + if build_prep https://github.com/ocaml/ocaml/archive/4.07.0 ocaml-4.07.0 tar.gz 1 ; then # See README.win32.adoc cp config/m-nt.h byterun/caml/m.h cp config/s-nt.h byterun/caml/s.h diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index c4f0147728..f7fd4b9146 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -11,7 +11,7 @@ Extended pattern-matching This section describes the full form of pattern-matching in |Coq| terms. -.. |rhs| replace:: right hand side +.. |rhs| replace:: right hand sides Patterns -------- @@ -39,12 +39,12 @@ value. A pattern of the form :n:`pattern | pattern` is called disjunctive. A list of patterns separated with commas is also considered as a pattern and is called *multiple pattern*. However multiple patterns can only occur at the root of pattern-matching equations. Disjunctions of -*multiple pattern* are allowed though. +*multiple patterns* are allowed though. Since extended ``match`` expressions are compiled into the primitive ones, -the expressiveness of the theory remains the same. Once the stage of -parsing has finished only simple patterns remain. Re-nesting of -pattern is performed at printing time. An easy way to see the result +the expressiveness of the theory remains the same. Once parsing has finished +only simple patterns remain. The original nesting of the ``match`` expressions +is recovered at printing time. An easy way to see the result of the expansion is to toggle off the nesting performed at printing (use here :opt:`Printing Matching`), then by printing the term with :cmd:`Print` if the term is a constant, or using the command :cmd:`Check`. @@ -150,12 +150,12 @@ second one and :g:`false` otherwise. We can write it as follows: | S n, S m => lef n m end. -Note that the first and the second multiple pattern superpose because +Note that the first and the second multiple pattern overlap because the couple of values ``O O`` matches both. Thus, what is the result of the function on those values? To eliminate ambiguity we use the *textual -priority rule*: we consider patterns ordered from top to bottom, then -a value is matched by the pattern at the ith row if and only if it is -not matched by some pattern of a previous row. Thus in the example,O O +priority rule:* we consider patterns to be ordered from top to bottom. A +value is matched by the pattern at the ith row if and only if it is +not matched by some pattern from a previous row. Thus in the example, ``O O`` is matched by the first pattern, and so :g:`(lef O O)` yields true. Another way to write this function is: @@ -201,7 +201,7 @@ instance, :g:`max` can be rewritten as follows: | 0, p | p, 0 => p end. -Similarly, factorization of (non necessary multiple) patterns that +Similarly, factorization of (not necessarily multiple) patterns that share the same variables is possible by using the notation :n:`{+| @pattern}`. Here is an example: @@ -312,7 +312,7 @@ Matching objects of dependent types The previous examples illustrate pattern matching on objects of non- dependent types, but we can also use the expansion strategy to -destructure objects of dependent type. Consider the type :g:`listn` of +destructure objects of dependent types. Consider the type :g:`listn` of lists of a certain length: .. coqtop:: in reset @@ -353,12 +353,12 @@ Dependent pattern matching ~~~~~~~~~~~~~~~~~~~~~~~~~~ The examples given so far do not need an explicit elimination -predicate because all the |rhs| have the same type and the strategy +predicate because all the |rhs| have the same type and Coq succeeds to synthesize it. Unfortunately when dealing with dependent -patterns it often happens that we need to write cases where the type +patterns it often happens that we need to write cases where the types of the |rhs| are different instances of the elimination predicate. The -function concat for listn is an example where the branches have -different type and we need to provide the elimination predicate: +function :g:`concat` for :g:`listn` is an example where the branches have +different types and we need to provide the elimination predicate: .. coqtop:: in @@ -374,7 +374,7 @@ In general if :g:`m` has type :g:`(I q1 … qr t1 … ts)` where :g:`q1, …, qr are parameters, the elimination predicate should be of the form :g:`fun y1 … ys x : (I q1 … qr y1 … ys ) => Q`. In the concrete syntax, it should be written : -``match m as x in (I _ … _ y1 … ys) return Q with … end`` +``match m as x in (I _ … _ y1 … ys) return Q with … end``. The variables which appear in the ``in`` and ``as`` clause are new and bounded in the property :g:`Q` in the return clause. The parameters of the inductive definitions should not be mentioned and are replaced by ``_``. @@ -385,9 +385,9 @@ Multiple dependent pattern matching Recall that a list of patterns is also a pattern. So, when we destructure several terms at the same time and the branches have different types we need to provide the elimination predicate for this -multiple pattern. It is done using the same scheme, each term may be -associated to an as and in clause in order to introduce a dependent -product. +multiple pattern. It is done using the same scheme: each term may be +associated to an ``as`` clause and an ``in`` clause in order to introduce +a dependent product. For example, an equivalent definition for :g:`concat` (even though the matching on the second term is trivial) would have been: @@ -414,7 +414,7 @@ length, by writing | consn n' a y, x => consn (n' + m) a (concat n' y m x) end. -I have a copy of :g:`b` in type :g:`listn 0` resp :g:`listn (S n')`. +we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. .. _match-in-patterns: @@ -425,7 +425,7 @@ If the type of the matched term is more precise than an inductive applied to variables, arguments of the inductive in the ``in`` branch can be more complicated patterns than a variable. -Moreover, constructors whose type do not follow the same pattern will +Moreover, constructors whose types do not follow the same pattern will become impossible branches. In an impossible branch, you can answer anything but False_rect unit has the advantage to be subterm of anything. @@ -448,8 +448,8 @@ Using pattern matching to write proofs In all the previous examples the elimination predicate does not depend on the object(s) matched. But it may depend and the typical case is when we write a proof by induction or a function that yields an object -of dependent type. An example of proof using match in given in Section -8.2.3. +of a dependent type. An example of a proof written using ``match`` is given +in the description of the tactic :tacn:`refine`. For example, we can write the function :g:`buildlist` that given a natural number :g:`n` builds a list of length :g:`n` containing zeros as follows: @@ -572,7 +572,7 @@ When does the expansion strategy fail? -------------------------------------- The strategy works very like in ML languages when treating patterns of -non-dependent type. But there are new cases of failure that are due to +non-dependent types. But there are new cases of failure that are due to the presence of dependencies. The error messages of the current implementation may be sometimes diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index e4d24a1f7e..c7df250672 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -25,13 +25,12 @@ The work is a complete rewrite of the previous implementation, based on the type class infrastructure. It also improves on and generalizes the previous implementation in several ways: - -+ User-extensible algorithm. The algorithm is separated in two parts: - generations of the rewriting constraints (done in ML) and solving of ++ User-extensible algorithm. The algorithm is separated into two parts: + generation of the rewriting constraints (written in ML) and solving these constraints using type class resolution. As type class resolution is extensible using tactics, this allows users to define general ways to solve morphism constraints. -+ Sub-relations. An example extension to the base algorithm is the ++ Subrelations. An example extension to the base algorithm is the ability to define one relation as a subrelation of another so that morphism declarations on one relation can be used automatically for the other. This is done purely using tactics and type class search. @@ -58,41 +57,41 @@ Relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~ A parametric *relation* ``R`` is any term of type -``forall (x1 :T1 ) ... (xn :Tn ), relation A``. +``forall (x1 : T1) ... (xn : Tn), relation A``. The expression ``A``, which depends on ``x1 ... xn`` , is called the *carrier* of the relation and ``R`` is said to be a relation over ``A``; the list ``x1,...,xn`` is the (possibly empty) list of parameters of the relation. -**Example 1 (Parametric relation):** +.. example:: Parametric relation -It is possible to implement finite sets of elements of type ``A`` as -unordered list of elements of type ``A``. -The function ``set_eq: forall (A: Type), relation (list A)`` -satisfied by two lists with the same elements is a parametric relation -over ``(list A)`` with one parameter ``A``. The type of ``set_eq`` -is convertible with ``forall (A: Type), list A -> list A -> Prop.`` + It is possible to implement finite sets of elements of type ``A`` as + unordered lists of elements of type ``A``. + The function ``set_eq: forall (A : Type), relation (list A)`` + satisfied by two lists with the same elements is a parametric relation + over ``(list A)`` with one parameter ``A``. The type of ``set_eq`` + is convertible with ``forall (A : Type), list A -> list A -> Prop.`` An *instance* of a parametric relation ``R`` with n parameters is any term -``(R t1 ... tn )``. +``(R t1 ... tn)``. Let ``R`` be a relation over ``A`` with ``n`` parameters. A term is a parametric proof of reflexivity for ``R`` if it has type -``forall (x1 :T1 ) ... (xn :Tn), reflexive (R x1 ... xn )``. +``forall (x1 : T1) ... (xn : Tn), reflexive (R x1 ... xn)``. Similar definitions are given for parametric proofs of symmetry and transitivity. -**Example 2 (Parametric relation (cont.)):** +.. example:: Parametric relation (continued) -The ``set_eq`` relation of the previous example can be proved to be -reflexive, symmetric and transitive. A parametric unary function ``f`` of type -``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2`` covariantly respects two parametric relation instances -``R1`` and ``R2`` if, whenever ``x``, ``y`` satisfy ``R1 x y``, their images (``f x``) and (``f y``) -satisfy ``R2 (f x) (f y)``. An ``f`` that respects its input and output -relations will be called a unary covariant *morphism*. We can also say -that ``f`` is a monotone function with respect to ``R1`` and ``R2`` . The -sequence ``x1 ... xn`` represents the parameters of the morphism. + The ``set_eq`` relation of the previous example can be proved to be + reflexive, symmetric and transitive. A parametric unary function ``f`` of type + ``forall (x1 : T1) ... (xn : Tn), A1 -> A2`` covariantly respects two parametric relation instances + ``R1`` and ``R2`` if, whenever ``x``, ``y`` satisfy ``R1 x y``, their images (``f x``) and (``f y``) + satisfy ``R2 (f x) (f y)``. An ``f`` that respects its input and output + relations will be called a unary covariant *morphism*. We can also say + that ``f`` is a monotone function with respect to ``R1`` and ``R2`` . The + sequence ``x1 ... xn`` represents the parameters of the morphism. Let ``R1`` and ``R2`` be two parametric relations. The *signature* of a -parametric morphism of type ``forall (x1 :T1 ) ... (xn :Tn ), A1 -> A2`` +parametric morphism of type ``forall (x1 : T1) ... (xn : Tn), A1 -> A2`` that covariantly respects two instances :math:`I_{R_1}` and :math:`I_{R_2}` of ``R1`` and ``R2`` is written :math:`I_{R_1} ++> I_{R_2}`. Notice that the special arrow ++>, which reminds the reader of covariance, is placed between the two relation @@ -118,29 +117,29 @@ covariant and contravariant. An instance of a parametric morphism :math:`f` with :math:`n` parameters is any term :math:`f \, t_1 \ldots t_n`. -**Example 3 (Morphisms):** +.. example:: Morphisms -Continuing the previous example, let ``union: forall (A: Type), list A -> list A -> list A`` -perform the union of two sets by appending one list to the other. ``union` is a binary -morphism parametric over ``A`` that respects the relation instance -``(set_eq A)``. The latter condition is proved by showing: + Continuing the previous example, let ``union: forall (A : Type), list A -> list A -> list A`` + perform the union of two sets by appending one list to the other. ``union` is a binary + morphism parametric over ``A`` that respects the relation instance + ``(set_eq A)``. The latter condition is proved by showing: -.. coqtop:: in + .. coqtop:: in - forall (A: Type) (S1 S1’ S2 S2’: list A), - set_eq A S1 S1’ -> - set_eq A S2 S2’ -> - set_eq A (union A S1 S2) (union A S1’ S2’). + forall (A : Type) (S1 S1’ S2 S2’ : list A), + set_eq A S1 S1’ -> + set_eq A S2 S2’ -> + set_eq A (union A S1 S2) (union A S1’ S2’). -The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` -for all ``A``. + The signature of the function ``union A`` is ``set_eq A ==> set_eq A ==> set_eq A`` + for all ``A``. -**Example 4 (Contravariant morphism):** +.. example:: Contravariant morphisms -The division function ``Rdiv: R -> R -> R`` is a morphism of signature -``le ++> le --> le`` where ``le`` is the usual order relation over -real numbers. Notice that division is covariant in its first argument -and contravariant in its second argument. + The division function ``Rdiv : R -> R -> R`` is a morphism of signature + ``le ++> le --> le`` where ``le`` is the usual order relation over + real numbers. Notice that division is covariant in its first argument + and contravariant in its second argument. Leibniz equality is a relation and every function is a morphism that respects Leibniz equality. Unfortunately, Leibniz equality is not @@ -149,180 +148,178 @@ always the intended equality for a given structure. In the next section we will describe the commands to register terms as parametric relations and morphisms. Several tactics that deal with equality in Coq can also work with the registered relations. The exact -list of tactic will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. -For instance, the tactic reflexivity can be used to close a goal ``R n n`` whenever ``R`` +list of tactics will be given :ref:`in this section <tactics-enabled-on-user-provided-relations>`. +For instance, the tactic reflexivity can be used to solve a goal ``R n n`` whenever ``R`` is an instance of a registered reflexive relation. However, the tactics that replace in a context ``C[]`` one term with another one related by ``R`` must verify that ``C[]`` is a morphism that respects the -intended relation. Currently the verification consists in checking +intended relation. Currently the verification consists of checking whether ``C[]`` is a syntactic composition of morphism instances that respects some obvious compatibility constraints. +.. example:: Rewriting -**Example 5 (Rewriting):** - -Continuing the previous examples, suppose that the user must prove -``set_eq int (union int (union int S1 S2) S2) (f S1 S2)`` under the -hypothesis ``H: set_eq int S2 (@nil int)``. It -is possible to use the ``rewrite`` tactic to replace the first two -occurrences of ``S2`` with ``@nil int`` in the goal since the -context ``set_eq int (union int (union int S1 nil) nil) (f S1 S2)``, -being a composition of morphisms instances, is a morphism. However the -tactic will fail replacing the third occurrence of ``S2`` unless ``f`` -has also been declared as a morphism. + Continuing the previous examples, suppose that the user must prove + ``set_eq int (union int (union int S1 S2) S2) (f S1 S2)`` under the + hypothesis ``H : set_eq int S2 (@nil int)``. It + is possible to use the ``rewrite`` tactic to replace the first two + occurrences of ``S2`` with ``@nil int`` in the goal since the + context ``set_eq int (union int (union int S1 nil) nil) (f S1 S2)``, + being a composition of morphisms instances, is a morphism. However the + tactic will fail replacing the third occurrence of ``S2`` unless ``f`` + has also been declared as a morphism. Adding new relations and morphisms ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -A parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm )`, -:g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)` can be -declared with the following command: +.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident -.. cmd:: Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m ) {? reflexivity proved by refl} {? symmetry proved by sym} {? transitivity proved by trans} as @ident - -after having required the ``Setoid`` module with the ``Require Setoid`` -command. + This command declares a parametric relation :g:`Aeq: forall (y1 : β1 ... ym : βm)`, + :g:`relation (A t1 ... tn)` over :g:`(A : αi -> ... αn -> Type)`. -The :g:`@ident` gives a unique name to the morphism and it is used -by the command to generate fresh names for automatically provided -lemmas used internally. + The :token:`ident` gives a unique name to the morphism and it is used + by the command to generate fresh names for automatically provided + lemmas used internally. -Notice that the carrier and relation parameters may refer to the -context of variables introduced at the beginning of the declaration, -but the instances need not be made only of variables. Also notice that -``A`` is *not* required to be a term having the same parameters as ``Aeq``, -although that is often the case in practice (this departs from the -previous implementation). + Notice that the carrier and relation parameters may refer to the + context of variables introduced at the beginning of the declaration, + but the instances need not be made only of variables. Also notice that + ``A`` is *not* required to be a term having the same parameters as ``Aeq``, + although that is often the case in practice (this departs from the + previous implementation). + To use this command, you need to first import the module ``Setoid`` using + the command ``Require Import Setoid``. .. cmd:: Add Relation -In case the carrier and relations are not parametric, one can use this command -instead, whose syntax is the same except there is no local context. + In case the carrier and relations are not parametric, one can use this command + instead, whose syntax is the same except there is no local context. -The proofs of reflexivity, symmetry and transitivity can be omitted if -the relation is not an equivalence relation. The proofs must be -instances of the corresponding relation definitions: e.g. the proof of -reflexivity must have a type convertible to -:g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n )`. -Each proof may refer to the introduced variables as well. + The proofs of reflexivity, symmetry and transitivity can be omitted if + the relation is not an equivalence relation. The proofs must be + instances of the corresponding relation definitions: e.g. the proof of + reflexivity must have a type convertible to + :g:`reflexive (A t1 ... tn) (Aeq t′ 1 …t′ n)`. + Each proof may refer to the introduced variables as well. -**Example 6 (Parametric relation):** +.. example:: Parametric relation -For Leibniz equality, we may declare: + For Leibniz equality, we may declare: -.. coqtop:: in + .. coqtop:: in - Add Parametric Relation (A : Type) : A (@eq A) - [reflexivity proved by @refl_equal A] - ... + Add Parametric Relation (A : Type) : A (@eq A) + [reflexivity proved by @refl_equal A] + ... Some tactics (:tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`transitivity`) work only on relations that respect the expected properties. The remaining tactics -(`replace`, :tacn:`rewrite` and derived tactics such as :tacn:`autorewrite`) do not +(:tacn:`replace`, :tacn:`rewrite` and derived tactics such as :tacn:`autorewrite`) do not require any properties over the relation. However, they are able to replace terms with related ones only in contexts that are syntactic compositions of parametric morphism instances declared with the following command. -.. cmd:: Add Parametric Morphism (x1 : T1 ) ... (xk : Tk ) : (f t1 ... tn ) with signature sig as @ident +.. cmd:: Add Parametric Morphism (x1 : T1) ... (xk : Tk) : (f t1 ... tn) with signature sig as @ident -The command declares ``f`` as a parametric morphism of signature ``sig``. The -identifier ``id`` gives a unique name to the morphism and it is used as -the base name of the type class instance definition and as the name of -the lemma that proves the well-definedness of the morphism. The -parameters of the morphism as well as the signature may refer to the -context of variables. The command asks the user to prove interactively -that ``f`` respects the relations identified from the signature. + This command declares ``f`` as a parametric morphism of signature ``sig``. The + identifier :token:`ident` gives a unique name to the morphism and it is used as + the base name of the type class instance definition and as the name of + the lemma that proves the well-definedness of the morphism. The + parameters of the morphism as well as the signature may refer to the + context of variables. The command asks the user to prove interactively + that ``f`` respects the relations identified from the signature. -**Example 7:** +.. example:: -We start the example by assuming a small theory over -homogeneous sets and we declare set equality as a parametric -equivalence relation and union of two sets as a parametric morphism. + We start the example by assuming a small theory over + homogeneous sets and we declare set equality as a parametric + equivalence relation and union of two sets as a parametric morphism. -.. coqtop:: in + .. coqtop:: in - Require Export Setoid. - Require Export Relation_Definitions. + Require Export Setoid. + Require Export Relation_Definitions. - Set Implicit Arguments. + Set Implicit Arguments. - Parameter set: Type -> Type. - Parameter empty: forall A, set A. - Parameter eq_set: forall A, set A -> set A -> Prop. - Parameter union: forall A, set A -> set A -> set A. + Parameter set : Type -> Type. + Parameter empty : forall A, set A. + Parameter eq_set : forall A, set A -> set A -> Prop. + Parameter union : forall A, set A -> set A -> set A. - Axiom eq_set_refl: forall A, reflexive _ (eq_set (A:=A)). - Axiom eq_set_sym: forall A, symmetric _ (eq_set (A:=A)). - Axiom eq_set_trans: forall A, transitive _ (eq_set (A:=A)). - Axiom empty_neutral: forall A (S: set A), eq_set (union S (empty A)) S. + Axiom eq_set_refl : forall A, reflexive _ (eq_set (A:=A)). + Axiom eq_set_sym : forall A, symmetric _ (eq_set (A:=A)). + Axiom eq_set_trans : forall A, transitive _ (eq_set (A:=A)). + Axiom empty_neutral : forall A (S : set A), eq_set (union S (empty A)) S. - Axiom union_compat: forall (A : Type), - forall x x' : set A, eq_set x x' -> - forall y y' : set A, eq_set y y' -> - eq_set (union x y) (union x' y'). + Axiom union_compat : + forall (A : Type), + forall x x' : set A, eq_set x x' -> + forall y y' : set A, eq_set y y' -> + eq_set (union x y) (union x' y'). - Add Parametric Relation A : (set A) (@eq_set A) - reflexivity proved by (eq_set_refl (A:=A)) - symmetry proved by (eq_set_sym (A:=A)) - transitivity proved by (eq_set_trans (A:=A)) - as eq_set_rel. + Add Parametric Relation A : (set A) (@eq_set A) + reflexivity proved by (eq_set_refl (A:=A)) + symmetry proved by (eq_set_sym (A:=A)) + transitivity proved by (eq_set_trans (A:=A)) + as eq_set_rel. - Add Parametric Morphism A : (@union A) with - signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. - Proof. - exact (@union_compat A). - Qed. + Add Parametric Morphism A : (@union A) + with signature (@eq_set A) ==> (@eq_set A) ==> (@eq_set A) as union_mor. + Proof. + exact (@union_compat A). + Qed. -It is possible to reduce the burden of specifying parameters using -(maximally inserted) implicit arguments. If ``A`` is always set as -maximally implicit in the previous example, one can write: + It is possible to reduce the burden of specifying parameters using + (maximally inserted) implicit arguments. If ``A`` is always set as + maximally implicit in the previous example, one can write: -.. coqtop:: in + .. coqtop:: in - Add Parametric Relation A : (set A) eq_set - reflexivity proved by eq_set_refl - symmetry proved by eq_set_sym - transitivity proved by eq_set_trans - as eq_set_rel. + Add Parametric Relation A : (set A) eq_set + reflexivity proved by eq_set_refl + symmetry proved by eq_set_sym + transitivity proved by eq_set_trans + as eq_set_rel. -.. coqtop:: in + .. coqtop:: in - Add Parametric Morphism A : (@union A) with - signature eq_set ==> eq_set ==> eq_set as union_mor. + Add Parametric Morphism A : (@union A) with + signature eq_set ==> eq_set ==> eq_set as union_mor. -.. coqtop:: in + .. coqtop:: in - Proof. exact (@union_compat A). Qed. + Proof. exact (@union_compat A). Qed. -We proceed now by proving a simple lemma performing a rewrite step and -then applying reflexivity, as we would do working with Leibniz -equality. Both tactic applications are accepted since the required -properties over ``eq_set`` and ``union`` can be established from the two -declarations above. + We proceed now by proving a simple lemma performing a rewrite step and + then applying reflexivity, as we would do working with Leibniz + equality. Both tactic applications are accepted since the required + properties over ``eq_set`` and ``union`` can be established from the two + declarations above. -.. coqtop:: in + .. coqtop:: in - Goal forall (S: set nat), - eq_set (union (union S empty) S) (union S S). + Goal forall (S : set nat), + eq_set (union (union S empty) S) (union S S). -.. coqtop:: in + .. coqtop:: in - Proof. intros. rewrite empty_neutral. reflexivity. Qed. + Proof. intros. rewrite empty_neutral. reflexivity. Qed. -The tables of relations and morphisms are managed by the type class -instance mechanism. The behavior on section close is to generalize the -instances by the variables of the section (and possibly hypotheses -used in the proofs of instance declarations) but not to export them in -the rest of the development for proof search. One can use the -cmd:`Existing Instance` command to do so outside the section, using the name of the -declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier -for the corresponding class instance declaration -(see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at -definition time. When loading a compiled file or importing a module, -all the declarations of this module will be loaded. + The tables of relations and morphisms are managed by the type class + instance mechanism. The behavior on section close is to generalize the + instances by the variables of the section (and possibly hypotheses + used in the proofs of instance declarations) but not to export them in + the rest of the development for proof search. One can use the + cmd:`Existing Instance` command to do so outside the section, using the name of the + declared morphism suffixed by ``_Morphism``, or use the ``Global`` modifier + for the corresponding class instance declaration + (see :ref:`First Class Setoids and Morphisms <first-class-setoids-and-morphisms>`) at + definition time. When loading a compiled file or importing a module, + all the declarations of this module will be loaded. Rewriting and non reflexive relations @@ -332,31 +329,31 @@ To replace only one argument of an n-ary morphism it is necessary to prove that all the other arguments are related to themselves by the respective relation instances. -**Example 8:** +.. example:: -To replace ``(union S empty)`` with ``S`` in ``(union (union S empty) S) (union S S)`` -the rewrite tactic must exploit the monotony of ``union`` (axiom ``union_compat`` -in the previous example). Applying ``union_compat`` by hand we are left with the -goal ``eq_set (union S S) (union S S)``. + To replace ``(union S empty)`` with ``S`` in ``(union (union S empty) S) (union S S)`` + the rewrite tactic must exploit the monotony of ``union`` (axiom ``union_compat`` + in the previous example). Applying ``union_compat`` by hand we are left with the + goal ``eq_set (union S S) (union S S)``. When the relations associated to some arguments are not reflexive, the tactic cannot automatically prove the reflexivity goals, that are left to the user. -Setoids whose relation are partial equivalence relations (PER) are -useful to deal with partial functions. Let ``R`` be a PER. We say that an +Setoids whose relations are partial equivalence relations (PER) are +useful for dealing with partial functions. Let ``R`` be a PER. We say that an element ``x`` is defined if ``R x x``. A partial function whose domain -comprises all the defined elements only is declared as a morphism that +comprises all the defined elements is declared as a morphism that respects ``R``. Every time a rewriting step is performed the user must prove that the argument of the morphism is defined. -**Example 9:** +.. example:: -Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the -smaller PER over non zero elements). Division can be declared as a -morphism of signature ``eq ==> eq0 ==> eq``. Replace ``x`` with -``y`` in ``div x n = div y n`` opens the additional goal ``eq0 n n`` -that is equivalent to ``n = n /\ n <> 0``. + Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the + smallest PER over non zero elements). Division can be declared as a + morphism of signature ``eq ==> eq0 ==> eq``. Replacing ``x`` with + ``y`` in ``div x n = div y n`` opens an additional goal ``eq0 n n`` + which is equivalent to ``n = n /\ n <> 0``. Rewriting and non symmetric relations @@ -371,44 +368,44 @@ a contravariant position. In a similar way, replacement in an hypothesis can be performed only if the replaced term occurs in a covariant position. -**Example 10 (Covariance and contravariance):** - -Suppose that division over real numbers has been defined as a morphism of signature -``Z.div: Z.lt ++> Z.lt --> Z.lt`` (i.e. ``Z.div`` is increasing in -its first argument, but decreasing on the second one). Let ``<`` -denotes ``Z.lt``. Under the hypothesis ``H: x < y`` we have -``k < x / y -> k < x / x``, but not ``k < y / x -> k < x / x``. Dually, -under the same hypothesis ``k < x / y -> k < y / y`` holds, but -``k < y / x -> k < y / y`` does not. Thus, if the current goal is -``k < x / x``, it is possible to replace only the second occurrence of -``x`` (in contravariant position) with ``y`` since the obtained goal -must imply the current one. On the contrary, if ``k < x / x`` is an -hypothesis, it is possible to replace only the first occurrence of -``x`` (in covariant position) with ``y`` since the current -hypothesis must imply the obtained one. - -Contrary to the previous implementation, no specific error message -will be raised when trying to replace a term that occurs in the wrong -position. It will only fail because the rewriting constraints are not -satisfiable. However it is possible to use the at modifier to specify -which occurrences should be rewritten. - -As expected, composing morphisms together propagates the variance -annotations by switching the variance every time a contravariant -position is traversed. - -**Example 11:** - -Let us continue the previous example and let us consider -the goal ``x / (x / x) < k``. The first and third occurrences of -``x`` are in a contravariant position, while the second one is in -covariant position. More in detail, the second occurrence of ``x`` -occurs covariantly in ``(x / x)`` (since division is covariant in -its first argument), and thus contravariantly in ``x / (x / x)`` -(since division is contravariant in its second argument), and finally -covariantly in ``x / (x / x) < k`` (since ``<``, as every -transitive relation, is contravariant in its first argument with -respect to the relation itself). +.. example:: Covariance and contravariance + + Suppose that division over real numbers has been defined as a morphism of signature + ``Z.div : Z.lt ++> Z.lt --> Z.lt`` (i.e. ``Z.div`` is increasing in + its first argument, but decreasing on the second one). Let ``<`` + denote ``Z.lt``. Under the hypothesis ``H : x < y`` we have + ``k < x / y -> k < x / x``, but not ``k < y / x -> k < x / x``. Dually, + under the same hypothesis ``k < x / y -> k < y / y`` holds, but + ``k < y / x -> k < y / y`` does not. Thus, if the current goal is + ``k < x / x``, it is possible to replace only the second occurrence of + ``x`` (in contravariant position) with ``y`` since the obtained goal + must imply the current one. On the contrary, if ``k < x / x`` is an + hypothesis, it is possible to replace only the first occurrence of + ``x`` (in covariant position) with ``y`` since the current + hypothesis must imply the obtained one. + + Contrary to the previous implementation, no specific error message + will be raised when trying to replace a term that occurs in the wrong + position. It will only fail because the rewriting constraints are not + satisfiable. However it is possible to use the at modifier to specify + which occurrences should be rewritten. + + As expected, composing morphisms together propagates the variance + annotations by switching the variance every time a contravariant + position is traversed. + +.. example:: + + Let us continue the previous example and let us consider + the goal ``x / (x / x) < k``. The first and third occurrences of + ``x`` are in a contravariant position, while the second one is in + covariant position. More in detail, the second occurrence of ``x`` + occurs covariantly in ``(x / x)`` (since division is covariant in + its first argument), and thus contravariantly in ``x / (x / x)`` + (since division is contravariant in its second argument), and finally + covariantly in ``x / (x / x) < k`` (since ``<``, as every + transitive relation, is contravariant in its first argument with + respect to the relation itself). Rewriting in ambiguous setoid contexts @@ -417,15 +414,14 @@ Rewriting in ambiguous setoid contexts One function can respect several different relations and thus it can be declared as a morphism having multiple signatures. -**Example 12:** - +.. example:: -Union over homogeneous lists can be given all the -following signatures: ``eq ==> eq ==> eq`` (``eq`` being the -equality over ordered lists) ``set_eq ==> set_eq ==> set_eq`` -(``set_eq`` being the equality over unordered lists up to duplicates), -``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq`` -being the equality over unordered lists). + Union over homogeneous lists can be given all the + following signatures: ``eq ==> eq ==> eq`` (``eq`` being the + equality over ordered lists) ``set_eq ==> set_eq ==> set_eq`` + (``set_eq`` being the equality over unordered lists up to duplicates), + ``multiset_eq ==> multiset_eq ==> multiset_eq`` (``multiset_eq`` + being the equality over unordered lists). To declare multiple signatures for a morphism, repeat the :cmd:`Add Morphism` command. @@ -435,7 +431,7 @@ rewrite request is ambiguous, since it is unclear what relations should be used to perform the rewriting. Contrary to the previous implementation, the tactic will always choose the first possible solution to the set of constraints generated by a rewrite and will not -try to find *all* possible solutions to warn the user about. +try to find *all* the possible solutions to warn the user about them. Commands and tactics @@ -457,7 +453,7 @@ hint database. For example, the declaration: .. coqtop:: in - Add Parametric Relation (x1 : T1) ... (xn : Tk) : (A t1 ... tn) (Aeq t′1 ... t′m) + Add Parametric Relation (x1 : T1) ... (xn : Tn) : (A t1 ... tn) (Aeq t′1 ... t′m) [reflexivity proved by refl] [symmetry proved by sym] [transitivity proved by trans] @@ -468,7 +464,7 @@ is equivalent to an instance declaration: .. coqtop:: in - Instance (x1 : T1) ... (xn : Tk) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := + Instance (x1 : T1) ... (xn : Tn) => id : @Equivalence (A t1 ... tn) (Aeq t′1 ... t′m) := [Equivalence_Reflexive := refl] [Equivalence_Symmetric := sym] [Equivalence_Transitive := trans]. @@ -491,37 +487,37 @@ handled by encoding them as records. In the following example, the projections of the setoid relation and of the morphism function can be registered as parametric relations and morphisms. -**Example 13 (First class setoids):** +.. example:: First class setoids -.. coqtop:: in + .. coqtop:: in - Require Import Relation_Definitions Setoid. + Require Import Relation_Definitions Setoid. - Record Setoid: Type := - { car: Type; - eq: car -> car -> Prop; - refl: reflexive _ eq; - sym: symmetric _ eq; - trans: transitive _ eq - }. + Record Setoid : Type := + { car: Type; + eq: car -> car -> Prop; + refl: reflexive _ eq; + sym: symmetric _ eq; + trans: transitive _ eq + }. - Add Parametric Relation (s : Setoid) : (@car s) (@eq s) - reflexivity proved by (refl s) - symmetry proved by (sym s) - transitivity proved by (trans s) as eq_rel. + Add Parametric Relation (s : Setoid) : (@car s) (@eq s) + reflexivity proved by (refl s) + symmetry proved by (sym s) + transitivity proved by (trans s) as eq_rel. - Record Morphism (S1 S2:Setoid): Type := - { f: car S1 -> car S2; - compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) - }. + Record Morphism (S1 S2 : Setoid) : Type := + { f: car S1 -> car S2; + compat: forall (x1 x2 : car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) + }. - Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : - (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. - Proof. apply (compat S1 S2 M). Qed. + Add Parametric Morphism (S1 S2 : Setoid) (M : Morphism S1 S2) : + (@f S1 S2 M) with signature (@eq S1 ==> @eq S2) as apply_mor. + Proof. apply (compat S1 S2 M). Qed. - Lemma test: forall (S1 S2:Setoid) (m: Morphism S1 S2) - (x y: car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). - Proof. intros. rewrite H. reflexivity. Qed. + Lemma test : forall (S1 S2 : Setoid) (m : Morphism S1 S2) + (x y : car S1), eq S1 x y -> eq S2 (f _ _ m x) (f _ _ m y). + Proof. intros. rewrite H. reflexivity. Qed. .. _tactics-enabled-on-user-provided-relations: @@ -539,33 +535,32 @@ pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity :name: setoid_reflexivity -.. tacv:: setoid_symmetry [in @ident] +.. tacv:: setoid_symmetry {? in @ident} :name: setoid_symmetry .. tacv:: setoid_transitivity :name: setoid_transitivity -.. tacv:: setoid_rewrite [@orientation] @term [at @occs] [in @ident] +.. tacv:: setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} :name: setoid_rewrite -.. tacv:: setoid_replace @term with @term [in @ident] [using relation @term] [by @tactic] +.. tacv:: setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} :name: setoid_replace - -The ``using relation`` arguments cannot be passed to the unprefixed form. -The latter argument tells the tactic what parametric relation should -be used to replace the first tactic argument with the second one. If -omitted, it defaults to the ``DefaultRelation`` instance on the type of -the objects. By default, it means the most recent ``Equivalence`` instance -in the environment, but it can be customized by declaring -new ``DefaultRelation`` instances. As Leibniz equality is a declared -equivalence, it will fall back to it if no other relation is declared -on a given type. + The ``using relation`` arguments cannot be passed to the unprefixed form. + The latter argument tells the tactic what parametric relation should + be used to replace the first tactic argument with the second one. If + omitted, it defaults to the ``DefaultRelation`` instance on the type of + the objects. By default, it means the most recent ``Equivalence`` instance + in the environment, but it can be customized by declaring + new ``DefaultRelation`` instances. As Leibniz equality is a declared + equivalence, it will fall back to it if no other relation is declared + on a given type. Every derived tactic that is based on the unprefixed forms of the tactics considered above will also work up to user defined relations. For instance, it is possible to register hints for :tacn:`autorewrite` that -are not proof of Leibniz equalities. In particular it is possible to +are not proofs of Leibniz equalities. In particular it is possible to exploit :tacn:`autorewrite` to simulate normalization in a term rewriting system up to user defined equalities. @@ -575,39 +570,39 @@ Printing relations and morphisms .. cmd:: Print Instances -This command can be used to show the list of currently -registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric`` -or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms -(implemented as ``Proper`` instances). When the rewriting tactics refuse -to replace a term in a context because the latter is not a composition -of morphisms, the :cmd:`Print Instances` command can be useful to understand -what additional morphisms should be registered. + This command can be used to show the list of currently + registered ``Reflexive`` (using ``Print Instances Reflexive``), ``Symmetric`` + or ``Transitive`` relations, Equivalences, PreOrders, PERs, and Morphisms + (implemented as ``Proper`` instances). When the rewriting tactics refuse + to replace a term in a context because the latter is not a composition + of morphisms, the :cmd:`Print Instances` command can be useful to understand + what additional morphisms should be registered. Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Due to backward compatibility reasons, the following syntax for the -declaration of setoids and morphisms is also accepted. - .. cmd:: Add Setoid @A @Aeq @ST as @ident -where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier -and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record -packing together the reflexivity, symmetry and transitivity lemmas). -Notice that the syntax is not completely backward compatible since the -identifier was not required. + This command for declaring setoids and morphisms is also accepted due + to backward compatibility reasons. + + Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier + and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record + packing together the reflexivity, symmetry and transitivity lemmas). + Notice that the syntax is not completely backward compatible since the + identifier was not required. .. cmd:: Add Morphism f : @ident :name: Add Morphism -The latter command also is restricted to the declaration of morphisms -without parameters. It is not fully backward compatible since the -property the user is asked to prove is slightly different: for n-ary -morphisms the hypotheses of the property are permuted; moreover, when -the morphism returns a proposition, the property is now stated using a -bi-implication in place of a simple implication. In practice, porting -an old development to the new semantics is usually quite simple. + This command is restricted to the declaration of morphisms + without parameters. It is not fully backward compatible since the + property the user is asked to prove is slightly different: for n-ary + morphisms the hypotheses of the property are permuted; moreover, when + the morphism returns a proposition, the property is now stated using a + bi-implication in place of a simple implication. In practice, porting + an old development to the new semantics is usually quite simple. Notice that several limitations of the old implementation have been lifted. In particular, it is now possible to declare several relations @@ -657,9 +652,8 @@ in ``Prop`` are implicitly translated to such applications). Indeed, when rewriting under a lambda, binding variable ``x``, say from ``P x`` to ``Q x`` using the relation iff, the tactic will generate a proof of ``pointwise_relation A iff (fun x => P x) (fun x => Q x)`` from the proof -of ``iff (P x) (Q x)`` and a constraint of the form Proper -``(pointwise_relation A iff ==> ?) m`` will be generated for the -surrounding morphism ``m``. +of ``iff (P x) (Q x)`` and a constraint of the form ``Proper (pointwise_relation A iff ==> ?) m`` +will be generated for the surrounding morphism ``m``. Hence, one can add higher-order combinators as morphisms by providing signatures using pointwise extension for the relations on the @@ -685,11 +679,11 @@ default. The semantics of the previous :tacn:`setoid_rewrite` implementation can almost be recovered using the ``at 1`` modifier. -Sub-relations +Subrelations ~~~~~~~~~~~~~ -Sub-relations can be used to specify that one relation is included in -another, so that morphisms signatures for one can be used for the +Subrelations can be used to specify that one relation is included in +another, so that morphism signatures for one can be used for the other. If a signature mentions a relation ``R`` on the left of an arrow ``==>``, then the signature also applies for any relation ``S`` that is smaller than ``R``, and the inverse applies on the right of an arrow. One @@ -702,7 +696,7 @@ two morphisms for conjunction: ``Proper (impl ==> impl ==> impl) and`` and rewriting constraints arising from a rewrite using ``iff``, ``impl`` or ``inverse impl`` through ``and``. -Sub-relations are implemented in ``Classes.Morphisms`` and are a prime +Subrelations are implemented in ``Classes.Morphisms`` and are a prime example of a mostly user-space extension of the algorithm. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 2407a9051a..d03a31c044 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -20,7 +20,7 @@ rationals ``Require Import Lqa`` and reals ``Require Import Lra``. + :tacn:`nra` is an incomplete proof procedure for non-linear (real or rational) arithmetic; + :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and - ``n`` is an optional integer limiting the proof search depth + ``n`` is an optional integer limiting the proof search depth, is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light driver to the external prover `csdp` [#]_. Note that the `csdp` driver is @@ -32,10 +32,10 @@ arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. The syntax of the formulas is the following: .. productionlist:: `F` - F : A ∣ P ∣ True ∣ False ∣ F 1 ∧ F 2 ∣ F 1 ∨ F 2 ∣ F 1 ↔ F 2 ∣ F 1 → F 2 ∣ ¬ F - A : p 1 = p 2 ∣ p 1 > p 2 ∣ p 1 < p 2 ∣ p 1 ≥ p 2 ∣ p 1 ≤ p 2 - p : c ∣ x ∣ −p ∣ p 1 − p 2 ∣ p 1 + p 2 ∣ p 1 × p 2 ∣ p ^ n - + F : A ∣ P ∣ True ∣ False ∣ F ∧ F ∣ F ∨ F ∣ F ↔ F ∣ F → F ∣ ¬ F + A : p = p ∣ p > p ∣ p < p ∣ p ≥ p ∣ p ≤ p + p : c ∣ x ∣ −p ∣ p − p ∣ p + p ∣ p × p ∣ p ^ n + where :math:`c` is a numeric constant, :math:`x \in D` is a numeric variable, the operators :math:`−, +, ×` are respectively subtraction, addition, and product; :math:`p ^ n` is exponentiation by a constant :math:`n`, :math:`P` is an arbitrary proposition. @@ -81,11 +81,11 @@ If :math:`-1` belongs to :math:`\mathit{Cone}(S)`, then the conjunction A proof based on this theorem is called a *positivstellensatz* refutation. The tactics work as follows. Formulas are normalized into conjunctive normal form :math:`\bigwedge_i C_i` where :math:`C_i` has the -general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False})` and +general form :math:`(\bigwedge_{j\in S_i} p_j \Join 0) \to \mathit{False}` and :math:`\Join \in \{>,\ge,=\}` for :math:`D\in \{\mathbb{Q},\mathbb{R}\}` and :math:`\Join \in \{\ge, =\}` for :math:`\mathbb{Z}`. -For each conjunct :math:`C_i`, the tactic calls a oracle which searches for +For each conjunct :math:`C_i`, the tactic calls an oracle which searches for :math:`-1` within the cone. Upon success, the oracle returns a *cone expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst index 387d614956..9adeca46fc 100644 --- a/doc/sphinx/addendum/nsatz.rst +++ b/doc/sphinx/addendum/nsatz.rst @@ -1,63 +1,55 @@ .. include:: ../preamble.rst -.. _nsatz: +.. _nsatz_chapter: Nsatz: tactics for proving equalities in integral domains =========================================================== :Author: Loïc Pottier -The tactic `nsatz` proves goals of the form +.. tacn:: nsatz + :name: nsatz -:math:`\begin{array}{l} -\forall X_1,\ldots,X_n \in A,\\ -P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) , \ldots , P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ -\vdash P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ -\end{array}` + This tactic is for solving goals of the form -where :math:`P, Q, P₁,Q₁,\ldots,Pₛ, Qₛ` are polynomials and :math:`A` is an integral -domain, i.e. a commutative ring with no zero divisor. For example, :math:`A` -can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. -Note that the equality :math:`=` used in these goals can be -any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibnitz equality. + :math:`\begin{array}{l} + \forall X_1, \ldots, X_n \in A, \\ + P_1(X_1, \ldots, X_n) = Q_1(X_1, \ldots, X_n), \ldots, P_s(X_1, \ldots, X_n) = Q_s(X_1, \ldots, X_n) \\ + \vdash P(X_1, \ldots, X_n) = Q(X_1, \ldots, X_n) \\ + \end{array}` -It also proves formulas + where :math:`P, Q, P_1, Q_1, \ldots, P_s, Q_s` are polynomials and :math:`A` is an integral + domain, i.e. a commutative ring with no zero divisors. For example, :math:`A` + can be :math:`\mathbb{R}`, :math:`\mathbb{Z}`, or :math:`\mathbb{Q}`. + Note that the equality :math:`=` used in these goals can be + any setoid equality (see :ref:`tactics-enabled-on-user-provided-relations`) , not only Leibniz equality. -:math:`\begin{array}{l} -\forall X_1,\ldots,X_n \in A,\\ -P_1(X_1,\ldots,X_n) = Q_1(X_1,\ldots,X_n) \wedge \ldots \wedge P_s(X_1,\ldots,X_n) =Q_s(X_1,\ldots,X_n)\\ -\rightarrow P(X_1,\ldots,X_n) = Q(X_1,\ldots,X_n)\\ -\end{array}` + It also proves formulas -doing automatic introductions. + :math:`\begin{array}{l} + \forall X_1, \ldots, X_n \in A, \\ + P_1(X_1, \ldots, X_n) = Q_1(X_1, \ldots, X_n) \wedge \ldots \wedge P_s(X_1, \ldots, X_n) = Q_s(X_1, \ldots, X_n) \\ + \rightarrow P(X_1, \ldots, X_n) = Q(X_1, \ldots, X_n) \\ + \end{array}` + doing automatic introductions. -Using the basic tactic `nsatz` ------------------------------- - - -Load the Nsatz module: - -.. coqtop:: all - - Require Import Nsatz. - -and use the tactic `nsatz`. + You can load the ``Nsatz`` module with the command ``Require Import Nsatz``. More about `nsatz` --------------------- Hilbert’s Nullstellensatz theorem shows how to reduce proofs of -equalities on polynomials on a commutative ring :math:`A` with no zero divisor +equalities on polynomials on a commutative ring :math:`A` with no zero divisors to algebraic computations: it is easy to see that if a polynomial :math:`P` in :math:`A[X_1,\ldots,X_n]` verifies :math:`c P^r = \sum_{i=1}^{s} S_i P_i`, with :math:`c \in A`, :math:`c \not = 0`, :math:`r` a positive integer, and the :math:`S_i` s in :math:`A[X_1,\ldots,X_n ]`, then :math:`P` is zero whenever polynomials :math:`P_1,\ldots,P_s` are zero -(the converse is also true when :math:`A` is an algebraic closed field: the method is +(the converse is also true when :math:`A` is an algebraically closed field: the method is complete). -So, proving our initial problem can reduce into finding :math:`S_1,\ldots,S_s`, +So, solving our initial problem reduces to finding :math:`S_1, \ldots, S_s`, :math:`c` and :math:`r` such that :math:`c (P-Q)^r = \sum_{i} S_i (P_i-Q_i)`, which will be proved by the tactic ring. @@ -68,34 +60,31 @@ Buchberger algorithm. This computation is done after a step of *reification*, which is performed using :ref:`typeclasses`. -The ``Nsatz`` module defines the tactic `nsatz`, which can be used without -arguments, or with the syntax: - -| nsatz with radicalmax:=num%N strategy:=num%Z parameters:= :n:`{* var}` variables:= :n:`{* var}` +.. tacv:: nsatz with radicalmax:=@num%N strategy:=@num%Z parameters:=[{*, @ident}] variables:=[{*, @ident}] -where: + Most complete syntax for `nsatz`. -* `radicalmax` is a bound when for searching r s.t. - :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)` + * `radicalmax` is a bound when searching for r such that + :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)` -* `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy - used in Buchberger algorithm (see :cite:`sugar` for details): + * `strategy` gives the order on variables :math:`X_1,\ldots,X_n` and the strategy + used in Buchberger algorithm (see :cite:`sugar` for details): - * strategy = 0: reverse lexicographic order and newest s-polynomial. - * strategy = 1: reverse lexicographic order and sugar strategy. - * strategy = 2: pure lexicographic order and newest s-polynomial. - * strategy = 3: pure lexicographic order and sugar strategy. + * strategy = 0: reverse lexicographic order and newest s-polynomial. + * strategy = 1: reverse lexicographic order and sugar strategy. + * strategy = 2: pure lexicographic order and newest s-polynomial. + * strategy = 3: pure lexicographic order and sugar strategy. -* `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among - :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with - rational fractions in these variables, i.e. polynomials are considered - with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient - :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic - produces a goal which states that :math:`c` is not zero. + * `parameters` is the list of variables :math:`X_{i_1},\ldots,X_{i_k}` among + :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with + rational fractions in these variables, i.e. polynomials are considered + with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient + :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic + produces a goal which states that :math:`c` is not zero. -* `variables` is the list of the variables in the decreasing order in - which they will be used in Buchberger algorithm. If `variables` = `(@nil R)`, - then `lvar` is replaced by all the variables which are not in - `parameters`. + * `variables` is the list of the variables in the decreasing order in + which they will be used in the Buchberger algorithm. If `variables` = `(@nil R)`, + then `lvar` is replaced by all the variables which are not in + `parameters`. -See file `Nsatz.v` for many examples, especially in geometry. +See the file `Nsatz.v` for many examples, especially in geometry. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 80ce016200..1ed3bffd2c 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -8,23 +8,20 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic Description of ``omega`` ------------------------ -This tactic does not need any parameter: - .. tacn:: omega -:tacn:`omega` solves a goal in Presburger arithmetic, i.e. a universally -quantified formula made of equations and inequations. Equations may -be specified either on the type ``nat`` of natural numbers or on -the type ``Z`` of binary-encoded integer numbers. Formulas on -``nat`` are automatically injected into ``Z``. The procedure -may use any hypothesis of the current proof session to solve the goal. + :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, + i.e. for proving formulas made of equations and inequations over the + type ``nat`` of natural numbers or the type ``Z`` of binary-encoded integers. + Formulas on ``nat`` are automatically injected into ``Z``. The procedure + may use any hypothesis of the current proof session to solve the goal. -Multiplication is handled by :tacn:`omega` but only goals where at -least one of the two multiplicands of products is a constant are -solvable. This is the restriction meant by "Presburger arithmetic". + Multiplication is handled by :tacn:`omega` but only goals where at + least one of the two multiplicands of products is a constant are + solvable. This is the restriction meant by "Presburger arithmetic". -If the tactic cannot solve the goal, it fails with an error message. -In any case, the computation eventually stops. + If the tactic cannot solve the goal, it fails with an error message. + In any case, the computation eventually stops. .. tacv:: romega :name: romega @@ -34,8 +31,7 @@ In any case, the computation eventually stops. Arithmetical goals recognized by ``omega`` ------------------------------------------ -:tacn:`omega` applied only to quantifier-free formulas built from the -connectors:: +:tacn:`omega` applies only to quantifier-free formulas built from the connectives:: /\ \/ ~ -> @@ -67,8 +63,8 @@ is generated: universally quantified, try :tacn:`intros` first; if it contains existentials quantifiers too, :tacn:`omega` is not strong enough to solve your goal). This may happen also if your goal contains arithmetical - operators unknown from :tacn:`omega`. Finally, your goal may be really - wrong! + operators not recognized by :tacn:`omega`. Finally, your goal may be simply + not true! .. exn:: omega: Not a quantifier-free goal. @@ -145,10 +141,10 @@ Overview of the tactic ~~~~~~~~~~~~~~~~~~~~~~ * The goal is negated twice and the first negation is introduced as an hypothesis. - * Hypothesis are decomposed in simple equations or inequations. Multiple + * Hypotheses are decomposed in simple equations or inequations. Multiple goals may result from this phase. * Equations and inequations over ``nat`` are translated over - ``Z``, multiple goals may result from the translation of substraction. + ``Z``, multiple goals may result from the translation of subtraction. * Equations and inequations are normalized. * Goals are solved by the OMEGA decision procedure. * The script of the solution is replayed. @@ -158,16 +154,15 @@ Overview of the OMEGA decision procedure The OMEGA decision procedure involved in the :tacn:`omega` tactic uses a small subset of the decision procedure presented in :cite:`TheOmegaPaper` -Here is an overview, look at the original paper for more information. +Here is an overview, refer to the original paper for more information. * Equations and inequations are normalized by division by the GCD of their coefficients. * Equations are eliminated, using the Banerjee test to get a coefficient equal to one. - * Note that each inequation defines a half space in the space of real value - of the variables. + * Note that each inequation cuts the Euclidean space in half. * Inequations are solved by projecting on the hyperspace - defined by cancelling one of the variable. They are partitioned + defined by cancelling one of the variables. They are partitioned according to the sign of the coefficient of the eliminated variable. Pairs of inequations from different classes define a new edge in the projection. @@ -177,7 +172,7 @@ Here is an overview, look at the original paper for more information. (success) or there is no more variable to eliminate (failure). It may happen that there is a real solution and no integer one. The last -steps of the Omega procedure (dark shadow) are not implemented, so the +steps of the Omega procedure are not implemented, so the decision procedure is only partial. Bugs diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index edb8676a5b..8ee8f52227 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -68,7 +68,7 @@ to modify the proof script accordingly. Proof blocks and error resilience -------------------------------------- -|Coq| 8.6 introduced a mechanism for error resiliency: in interactive +|Coq| 8.6 introduced a mechanism for error resilience: in interactive mode |Coq| is able to completely check a document containing errors instead of bailing out at the first failure. @@ -92,14 +92,14 @@ Caveats ```````` When a vernacular command fails the subsequent error messages may be -bogus, i.e. caused by the first error. Error resiliency for vernacular +bogus, i.e. caused by the first error. Error resilience for vernacular commands can be switched off by passing ``-async-proofs-command-error-resilience off`` to |CoqIDE|. An incorrect proof block detection can result into an incorrect error recovery and hence in bogus errors. Proof block detection cannot be precise for bullets or any other non well parenthesized proof -structure. Error resiliency can be turned off or selectively activated +structure. Error resilience can be turned off or selectively activated for any set of block kind passing to |CoqIDE| one of the following options: @@ -127,13 +127,14 @@ the very same button, that can also be used to see the list of errors and jump to the corresponding line. If a proof is processed asynchronously the corresponding Qed command -is colored using a lighter color that usual. This signals that the +is colored using a lighter color than usual. This signals that the proof has been delegated to a worker process (or will be processed lazily if the ``-async-proofs lazy`` option is used). Once finished, the worker process will provide the proof object, but this will not be automatically checked by the kernel of the main process. To force the kernel to check all the proof objects, one has to click the button -with the gears. Only then are all the universe constraints checked. +with the gears (Fully check the document) on the top bar. +Only then all the universe constraints are checked. Caveats ``````` @@ -149,7 +150,7 @@ To disable this feature, one can pass the ``-async-proofs off`` flag to default, pass the ``-async-proofs on`` flag to enable it. Proofs that are known to take little time to process are not delegated -to a worker process. The threshold can be configure with +to a worker process. The threshold can be configured with ``-async-proofs-delegation-threshold``. Default is 0.03 seconds. Batch mode @@ -157,7 +158,7 @@ Batch mode When |Coq| is used as a batch compiler by running `coqc` or `coqtop` -compile, it produces a `.vo` file for each `.v` file. A `.vo` file contains, -among other things, theorems statements and proofs. Hence to produce a +among other things, theorem statements and proofs. Hence to produce a .vo |Coq| need to process all the proofs of the `.v` file. The asynchronous processing of proofs can decouple the generation of a @@ -225,5 +226,5 @@ in all the shells from which |Coq| processes will be started. If one uses just one terminal running the bash shell, then ``export ‘coqworkmgr -j 4‘`` will do the job. -After that, all |Coq| processes, e.g. `coqide` and `coqc`, will honor the +After that, all |Coq| processes, e.g. `coqide` and `coqc`, will respect the limit, globally. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 68b5b9d6fe..b7946c6451 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -120,7 +120,7 @@ Following the previous example, one can write: Generalizable Variables A B C. - Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y). + Definition neqb_implicit `{eqa : EqDec A} (x y : A) := negb (eqb x y). Here ``A`` is implicitly generalized, and the resulting function is equivalent to the one above. @@ -193,7 +193,7 @@ superclasses as a binding context: Class Ord `(E : EqDec A) := { le : A -> A -> bool }. Contrary to Haskell, we have no special syntax for superclasses, but -this declaration is morally equivalent to: +this declaration is equivalent to: :: @@ -248,7 +248,7 @@ properties, e.g.: This declares singleton classes for reflexive and transitive relations, (see the :ref:`singleton class <singleton-class>` variant for an -explanation). These may be used as part of other classes: +explanation). These may be used as parts of other classes: .. coqtop:: all @@ -346,7 +346,7 @@ few other commands related to type classes. .. cmd:: Existing Instance {+ @ident} [| priority] - This commands adds an arbitrary list of constants whose type ends with + This command adds an arbitrary list of constants whose type ends with an applied type class to the instance database with an optional priority. It can be used for redeclaring instances at the end of sections, or declaring structure projections as instances. This is @@ -387,14 +387,14 @@ few other commands related to type classes. + When called with specific databases (e.g. with), typeclasses eauto allows shelved goals to remain at any point during search and treat - typeclasses goals like any other. + typeclass goals like any other. + The transparency information of databases is used consistently for all hints declared in them. It is always used when calling the - unifier. When considering the local hypotheses, we use the transparent + unifier. When considering local hypotheses, we use the transparent state of the first hint database given. Using an empty database (created with :cmd:`Create HintDb` for example) with unfoldable variables and - constants as the first argument of typeclasses eauto hence makes + constants as the first argument of ``typeclasses eauto`` hence makes resolution with the local hypotheses use full conversion during unification. @@ -461,8 +461,8 @@ Options .. opt:: Typeclasses Dependency Order This option (on by default since 8.6) respects the dependency order - between subgoals, meaning that subgoals which are depended on by other - subgoals come first, while the non-dependent subgoals were put before + between subgoals, meaning that subgoals on which other subgoals depend + come first, while the non-dependent subgoals were put before the dependent ones previously (Coq 8.5 and below). This can result in quite different performance behaviors of proof search. diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 6e7ccba63c..f245fab5ca 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -72,7 +72,7 @@ different. This can be seen when the :opt:`Printing Universes` option is on: Now :g:`pidentity` is used at two different levels: at the head of the application it is instantiated at ``Top.3`` while in the argument position it is instantiated at ``Top.4``. This definition is only valid as long as -``Top.4`` is strictly smaller than ``Top.3``, as show by the constraints. Note +``Top.4`` is strictly smaller than ``Top.3``, as shown by the constraints. Note that this definition is monomorphic (not universe polymorphic), so the two universes (in this case ``Top.3`` and ``Top.4``) are actually global levels. diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index 30dda2973f..c74d8f540c 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -1,7 +1,7 @@ @String{jfp = "Journal of Functional Programming"} @String{lncs = "Lecture Notes in Computer Science"} @String{lnai = "Lecture Notes in Artificial Intelligence"} -@String{SV = "{Sprin-ger-Verlag}"} +@String{SV = "{Springer-Verlag}"} @InCollection{Asp00, Title = {Proof General: A Generic Tool for Proof Development}, @@ -258,7 +258,7 @@ s}, @InProceedings{Luttik97specificationof, author = {Sebastiaan P. Luttik and Eelco Visser}, booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing}, - publisher = {Springer-Verlag}, + publisher = SV, title = {Specification of Rewriting Strategies}, year = {1997} } diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 6e0c1e1b61..a63400103f 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -747,7 +747,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is is: .. math:: - \ind{~}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} + \ind{0}{\left[\begin{array}{rcl}\tree&:&\Set\\\forest&:&\Set\end{array}\right]} {\left[\begin{array}{rcl} \node &:& \forest → \tree\\ \emptyf &:& \forest\\ @@ -769,7 +769,7 @@ the sort of the inductive type t (not to be confused with :math:`\Sort` which is The declaration for a mutual inductive definition of even and odd is: .. math:: - \ind{1}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ + \ind{0}{\left[\begin{array}{rcl}\even&:&\nat → \Prop \\ \odd&:&\nat → \Prop \end{array}\right]} {\left[\begin{array}{rcl} \evenO &:& \even~0\\ @@ -966,7 +966,7 @@ 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[Γ_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}}{Γ} @@ -1025,7 +1025,7 @@ Template polymorphism +++++++++++++++++++++ Inductive types declared in :math:`\Type` are polymorphic over their arguments -in :math:`\Type`. If :math:`A` is an arity of some sort and math:`s` is a sort, we write :math:`A_{/s}` +in :math:`\Type`. If :math:`A` is an arity of some sort and :math:`s` is a sort, we write :math:`A_{/s}` for the arity obtained from :math:`A` by replacing its sort with :math:`s`. Especially, if :math:`A` is well-typed in some global environment and local context, then :math:`A_{/s}` is typable by typability of all products in the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index ad1f0caa60..0f51b3eba3 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -25,7 +25,7 @@ In the interactive mode, also known as the |Coq| toplevel, the user can develop his theories and proofs step by step. The |Coq| toplevel is run by the command ``coqtop``. -They are two different binary images of |Coq|: the byte-code one and the +There are two different binary images of |Coq|: the byte-code one and the native-code one (if OCaml provides a native-code compiler for your platform, which is supposed in the following). By default, ``coqtop`` executes the native-code version; run ``coqtop.byte`` to get @@ -43,10 +43,11 @@ The ``coqc`` command takes a name *file* as argument. Then it looks for a vernacular file named *file*.v, and tries to compile it into a *file*.vo file (See :ref:`compiled-files`). -.. caution:: The name *file* should be a - regular |Coq| identifier, as defined in Section :ref:'TODO-1.1'. It should contain - only letters, digits or underscores (_). For instance, ``/bar/foo/toto.v`` is valid, but - ``/bar/foo/to-to.v`` is invalid. +.. caution:: + + The name *file* should be a regular |Coq| identifier as defined in Section :ref:`lexical-conventions`. + It should contain only letters, digits or underscores (_). For example ``/bar/foo/toto.v`` is valid, + but ``/bar/foo/to-to.v`` is not. Customization at launch time @@ -59,8 +60,8 @@ When |Coq| is launched, with either ``coqtop`` or ``coqc``, the resource file ``$XDG_CONFIG_HOME/coq/coqrc.xxx``, if it exists, will be implicitly prepended to any document read by Coq, whether it is an interactive session or a file to compile. Here, ``$XDG_CONFIG_HOME`` -is the configuration directory of the user (by default its home -directory ``~/.config``) and ``xxx`` is the version number (e.g. 8.8). If +is the configuration directory of the user (by default it's ``~/.config``) +and ``xxx`` is the version number (e.g. 8.8). If this file is not found, then the file ``$XDG_CONFIG_HOME/coqrc`` is searched. If not found, it is the file ``~/.coqrc.xxx`` which is searched, and, if still not found, the file ``~/.coqrc``. If the latter is also @@ -140,15 +141,15 @@ and ``coqtop``, unless stated otherwise: :-l *file*, -load-vernac-source *file*: Load and execute the |Coq| script from *file.v*. :-lv *file*, -load-vernac-source-verbose *file*: Load and execute the - |Coq| script from *file.v*. Output its content on the standard input as + |Coq| script from *file.v*. Write its contents to the standard output as it is executed. :-load-vernac-object dirpath: Load |Coq| compiled library dirpath. This is equivalent to runningRequire dirpath. :-require dirpath: Load |Coq| compiled library dirpath and import it. This is equivalent to running Require Import dirpath. :-batch: Exit just after argument parsing. Available for `coqtop` only. -:-compile *file.v*: Compile file *file.v* into *file.vo*. This options - imply -batch (exit just after argument parsing). It is available only +:-compile *file.v*: Compile file *file.v* into *file.vo*. This option + implies -batch (exit just after argument parsing). It is available only for `coqtop`, as this behavior is the purpose of `coqc`. :-compile-verbose *file.v*: Same as -compile but also output the content of *file.v* as it is compiled. @@ -237,7 +238,7 @@ relative paths in object files ``-Q`` and ``-R`` have exactly the same meaning. unless explicitly required. :-o: At exit, print a summary about the context. List the names of all assumptions and variables (constants without body). -:-silent: Do not write progress information in standard output. +:-silent: Do not write progress information to the standard output. Environment variable ``$COQLIB`` can be set to override the location of the standard library. @@ -253,7 +254,7 @@ set of reflexive transitive dependencies of set :math:`S`. Then: context without type-checking. Basic integrity checks (checksums) are nonetheless performed. -As a rule of thumb, the -admit can be used to tell that some libraries +As a rule of thumb, -admit can be used to tell Coq that some libraries have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && ``coqchk B -admit A`` without type-checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index f9903e6104..f7f442092f 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -27,7 +27,7 @@ is shown in the figure :ref:`CoqIDE main screen <coqide_mainscreen>`. At the top is a menu bar, and a tool bar below it. The large window on the left is displaying the various *script buffers*. The upper right window is the *goal window*, where -goals to prove are displayed. The lower right window is the *message +goals to be proven are displayed. The lower right window is the *message window*, where various messages resulting from commands are displayed. At the bottom is the status bar. @@ -62,8 +62,8 @@ In the figure :ref:`CoqIDE main screen <coqide_mainscreen>`, the running buffer is `Fermat.v`, all commands until the ``Theorem`` have been already executed, and the user tried to go forward executing ``Induction n``. That command failed because no such -tactic exists (tactics are now in lowercase…), and the wrong word is -underlined. +tactic exists (names of standard tactics are written in lowercase), +and the failing command is underlined. Notice that the processed part of the running buffer is not editable. If you ever want to modify something you have to go backward using the up @@ -82,8 +82,8 @@ background in the error background color (pink by default). The same characterization of error-handling applies when running several commands using the "goto" button. -If you ever try to execute a command which happens to run during a -long time, and would like to abort it before its termination, you may +If you ever try to execute a command that runs for a long time +and would like to abort it before it terminates, you may use the interrupt button (the white cross on a red circle). There are other buttons on the |CoqIDE| toolbar: a button to save the running @@ -141,11 +141,10 @@ Vernacular commands, templates The Templates menu allows using shortcuts to insert vernacular commands. This is a nice way to proceed if you are not sure of the -spelling of the command you want. +syntax of the command you want. -Moreover, this menu offers some *templates* which will automatic -insert a complex command like ``Fixpoint`` with a convenient shape for its -arguments. +Moreover, from this menu you can automatically insert templates of complex +commands like ``Fixpoint`` that you can conveniently fill afterwards. Queries ------------ @@ -177,7 +176,7 @@ The `Compile` menu offers direct commands to: Customizations ------------------- -You may customize your environment using menu Edit/Preferences. A new +You may customize your environment using the menu Edit/Preferences. A new window will be displayed, with several customization sections presented as a notebook. @@ -189,7 +188,7 @@ automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a third party, |CoqIDE| may read it again for you. Note that in the case -you edited that same file, you will be prompt to choose to either +you edited that same file, you will be prompted to choose to either discard your changes or not. The File charset encoding choice is described below in :ref:`character-encoding-saved-files`. @@ -209,7 +208,7 @@ Notice that these settings are saved in the file `.coqiderc` of your home directory. A Gtk2 accelerator keymap is saved under the name `.coqide.keys`. It -is not recommanded to edit this file manually: to modify a given menu +is not recommended to edit this file manually: to modify a given menu shortcut, go to the corresponding menu item without releasing the mouse button, press the key you want for the new shortcut, and release the mouse button afterwards. If your system does not allow it, you may @@ -240,14 +239,14 @@ mathematical symbols ∀ and ∃, you may define: There exists a small set of such notations already defined, in the file `utf8.v` of Coq library, so you may enable them just by -``Require utf8`` inside |CoqIDE|, or equivalently, by starting |CoqIDE| with -``coqide -l utf8``. +``Require Import Unicode.Utf8`` inside |CoqIDE|, or equivalently, +by starting |CoqIDE| with ``coqide -l utf8``. However, there are some issues when using such Unicode symbols: you of course need to use a character font which supports them. In the Fonts section of the preferences, the Preview line displays some Unicode symbols, so you could figure out if the selected font is OK. Related -to this, one thing you may need to do is choose whether GTK+ should +to this, one thing you may need to do is choosing whether GTK+ should use antialiased fonts or not, by setting the environment variable `GDK_USE_XFT` to 1 or 0 respectively. diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 59bc2d22aa..e779515a00 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -438,7 +438,7 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use For users of coq_makefile with version < 8.7 - + Support for “sub-directory” is deprecated. To perform actions before + + Support for "subdirectory" is deprecated. To perform actions before or after the build (like invoking ``make`` on a subdirectory) one can hook in pre-all and post-all extension points. + ``-extra-phony`` and ``-extra`` are deprecated. To provide additional target @@ -446,10 +446,10 @@ To build, say, two targets foo.vo and bar.vo in parallel one can use -Modules dependencies +Module dependencies -------------------- -In order to compute modules dependencies (so to use ``make``), |Coq| comes +In order to compute module dependencies (so to use ``make``), |Coq| comes with an appropriate tool, ``coqdep``. ``coqdep`` computes inter-module dependencies for |Coq| and |OCaml| @@ -464,7 +464,7 @@ command ``Declare ML Module``. Dependencies of |OCaml| modules are computed by looking at `open` commands and the dot notation *module.value*. However, this is done approximately and you are advised to use ``ocamldep`` instead for the -|OCaml| modules dependencies. +|OCaml| module dependencies. See the man page of ``coqdep`` for more details and options. @@ -482,9 +482,9 @@ coqdoc is a documentation tool for the proof assistant |Coq|, similar to ``javadoc`` or ``ocamldoc``. The task of coqdoc is -#. to produce a nice |Latex| and/or HTML document from the |Coq| - sources, readable for a human and not only for the proof assistant; -#. to help the user navigating in his own (or third-party) sources. +#. to produce a nice |Latex| and/or HTML document from |Coq| source files, + readable for a human and not only for the proof assistant; +#. to help the user navigate his own (or third-party) sources. @@ -495,7 +495,7 @@ Documentation is inserted into |Coq| files as *special comments*. Thus your files will compile as usual, whether you use coqdoc or not. coqdoc presupposes that the given |Coq| files are well-formed (at least lexically). Documentation starts with ``(**``, followed by a space, and -ends with the pending ``*)``. The documentation format is inspired by Todd +ends with ``*)``. The documentation format is inspired by Todd A. Coram’s *Almost Free Text (AFT)* tool: it is mainly ``ASCII`` text with some syntax-light controls, described below. coqdoc is robust: it shouldn’t fail, whatever the input is. But remember: “garbage in, @@ -511,7 +511,7 @@ quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun x => u]``). Inside quotations, the code is pretty-printed in the same way as it is in code parts. -Pre-formatted vernacular is enclosed by ``[[`` and ``]]``. The former must be +Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be followed by a newline and the latter must follow a newline. @@ -537,7 +537,7 @@ or It gives the |Latex| and HTML texts to be produced for the given |Coq| -token. One of the |Latex| or HTML text may be omitted, causing the +token. Either the |Latex| or the HTML rule may be omitted, causing the default pretty-printing to be used for this token. The printing for one token can be removed with @@ -577,10 +577,9 @@ commands. Sections ++++++++ -Sections are introduced by 1 to 4 leading stars (i.e. at the beginning -of the line) followed by a space. One star is a section, two stars a -sub-section, etc. The section title is given on the remaining of the -line. +Sections are introduced by 1 to 4 asterisks at the beginning of a line +followed by a space and the title of the section. One asterisk is a section, +two a subsection, etc. .. example:: @@ -628,7 +627,7 @@ More than 4 leading dashes produce a horizontal rule. Emphasis. +++++++++ -Text can be italicized by placing it in underscores. A non-identifier +Text can be italicized by enclosing it in underscores. A non-identifier character must precede the leading underscore and follow the trailing underscore, so that uses of underscores in names aren’t mistaken for emphasis. Usually, these are spaces or punctuation. @@ -683,16 +682,16 @@ Hyperlinks can be inserted into the HTML output, so that any identifier is linked to the place of its definition. ``coqc file.v`` automatically dumps localization information in -``file.glob`` or appends it to a file specified using option ``--dump-glob +``file.glob`` or appends it to a file specified using the option ``--dump-glob file``. Take care of erasing this global file, if any, when starting the whole compilation process. Then invoke coqdoc or ``coqdoc --glob-from file`` to tell coqdoc to look -for name resolutions into the file ``file`` (it will look in ``file.glob`` +for name resolutions in the file ``file`` (it will look in ``file.glob`` by default). -Identifiers from the |Coq| standard library are linked to the Coq web -site at `<http://coq.inria.fr/library/>`_. This behavior can be changed +Identifiers from the |Coq| standard library are linked to the Coq website +`<http://coq.inria.fr/library/>`_. This behavior can be changed using command line options ``--no-externals`` and ``--coqlib``; see below. @@ -735,12 +734,12 @@ file (even if it starts with a ``-``). |Coq| files are identified by the suffixes ``.v`` and ``.g`` and |Latex| files by the suffix ``.tex``. -:HTML output: This is the default output. One HTML file is created for +:HTML output: This is the default output format. One HTML file is created for each |Coq| file given on the command line, together with a file ``index.html`` (unless ``option-no-index is passed``). The HTML pages use a style sheet named ``style.css``. Such a file is distributed with coqdoc. :|Latex| output: A single |Latex| file is created, on standard - output. It can be redirected to a file with option ``-o``. The order of + output. It can be redirected to a file using the option ``-o``. The order of files on the command line is kept in the final document. |Latex| files given on the command line are copied ‘as is’ in the final document . DVI and PostScript can be produced directly with the @@ -766,15 +765,15 @@ Command line options :-o file, --output file: Redirect the output into the file ‘file’ (meaningless with ``-html``). :-d dir, --directory dir: Output files into directory ‘dir’ instead of - current directory (option ``-d`` does not change the filename specified - with option ``-o``, if any). + the current directory (option ``-d`` does not change the filename specified + with the option ``-o``, if any). :--body-only: Suppress the header and trailer of the final document. Thus, you can insert the resulting document into a larger one. :-p string, --preamble string: Insert some material in the |Latex| preamble, right before ``\begin{document}`` (meaningless with ``-html``). :--vernac-file file,--tex-file file: Considers the file ‘file’ respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. - :--files-from file: Read file names to process in file ‘file’ as if + :--files-from file: Read file names to be processed from the file ‘file’ as if they were given on the command line. Useful for program sources split up into several directories. :-q, --quiet: Be quiet. Do not print anything except errors. @@ -785,7 +784,7 @@ Command line options **Index options** - Default behavior is to build an index, for the HTML output only, + The default behavior is to build an index, for the HTML output only, into ``index.html``. :--no-index: Do not output the index. @@ -806,7 +805,7 @@ Command line options contents. -**Hyperlinks options** +**Hyperlink options** :--glob-from file: Make references using |Coq| globalizations from file file. (Such globalizations are obtained with Coq option ``-dump-glob``). @@ -862,9 +861,9 @@ Command line options The behavior of options ``-g`` and ``-l`` can be locally overridden using the ``(* begin show *) … (* end show *)`` environment (see above). - There are a few options to drive the parsing of comments: + There are a few options that control the parsing of comments: - :--parse-comments: Parses regular comments delimited by ``(*`` and ``*)`` as + :--parse-comments: Parse regular comments delimited by ``(*`` and ``*)`` as well. They are typeset inline. :--plain-comments: Do not interpret comments, simply copy them as plain-text. @@ -874,7 +873,7 @@ Command line options **Language options** - Default behavior is to assume ASCII 7 bits input files. + The default behavior is to assume ASCII 7 bit input files. :-latin1, --latin1: Select ISO-8859-1 input files. It is equivalent to --inputenc latin1 --charset iso-8859-1. @@ -939,7 +938,7 @@ macros: Embedded Coq phrases inside |Latex| documents --------------------------------------------- -When writing a documentation about a proof development, one may want +When writing documentation about a proof development, one may want to insert |Coq| phrases inside a |Latex| document, possibly together with the corresponding answers of the system. We provide a mechanical way to process such |Coq| phrases embedded in |Latex| files: the ``coq-tex`` diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index dc355fa013..6fbb2fac6d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -144,10 +144,11 @@ mode but it can also be used in toplevel definitions as shown below. : | `integer` (< | <= | > | >=) `integer` selector : [`ident`] : | `integer` - : (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) + : | (`integer` | `integer` - `integer`), ..., (`integer` | `integer` - `integer`) toplevel_selector : `selector` - : | `all` - : | `par` + : | all + : | par + : | ! .. productionlist:: coq top : [Local] Ltac `ltac_def` with ... with `ltac_def` @@ -177,7 +178,7 @@ Sequence A sequence is an expression of the following form: -.. tacn:: @expr ; @expr +.. tacn:: @expr__1 ; @expr__2 :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be @@ -207,11 +208,11 @@ following form: were given. For instance, ``[> | auto]`` is a shortcut for ``[> idtac | auto ]``. - .. tacv:: [> {*| @expr} | @expr .. | {*| @expr}] + .. tacv:: [> {*| @expr__i} | @expr .. | {*| @expr__j}] - In this variant, token:`expr` is used for each goal coming after those - covered by the first list of :n:`@expr` but before those coevered by the - last list of :n:`@expr`. + In this variant, :n:`@expr` is used for each goal coming after those + covered by the list of :n:`@expr__i` but before those covered by the + list of :n:`@expr__j`. .. tacv:: [> {*| @expr} | .. | {*| @expr}] @@ -225,11 +226,11 @@ following form: tactic is not run at all. A tactic which expects multiple goals, such as ``swap``, would act as if a single goal is focused. - .. tacv:: expr ; [{*| @expr}] + .. tacv:: @expr__0 ; [{*| @expr__i}] This variant of local tactic application is paired with a sequence. In this - variant, there must be as many :n:`@expr` in the list as goals generated - by the application of the first :n:`@expr` to each of the individual goals + variant, there must be as many :n:`@expr__i` as goals generated + by the application of :n:`@expr__0` to each of the individual goals independently. All the above variants work in this form too. Formally, :n:`@expr ; [ ... ]` is equivalent to :n:`[> @expr ; [> ... ] .. ]`. @@ -247,20 +248,20 @@ focused goals with: We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: - .. tacv:: only selector : expr + .. tacv:: only @selector : @expr :name: only ... : ... - When selecting several goals, the tactic expr is applied globally to all + When selecting several goals, the tactic :token:`expr` is applied globally to all selected goals. .. tacv:: [@ident] : @expr - In this variant, :n:`@expr` is applied locally to a goal previously named + In this variant, :token:`expr` is applied locally to a goal previously named by the user (see :ref:`existential-variables`). .. tacv:: @num : @expr - In this variant, :n:`@expr` is applied locally to the :token:`num`-th goal. + In this variant, :token:`expr` is applied locally to the :token:`num`-th goal. .. tacv:: {+, @num-@num} : @expr @@ -271,13 +272,13 @@ focused goals with: .. tacv:: all: @expr :name: all: ... - In this variant, :n:`@expr` is applied to all focused goals. ``all:`` can only + In this variant, :token:`expr` is applied to all focused goals. ``all:`` can only be used at the toplevel of a tactic expression. .. tacv:: !: @expr - In this variant, if exactly one goal is focused :n:`expr` is - applied to it. Otherwise the tactical fails. ``!:`` can only be + In this variant, if exactly one goal is focused, :token:`expr` is + applied to it. Otherwise the tactic fails. ``!:`` can only be used at the toplevel of a tactic expression. .. tacv:: par: @expr diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 838926d651..ab1edc0b27 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -40,8 +40,7 @@ induction for objects in type `identᵢ`. Induction scheme for tree and forest. - The definition of principle of mutual induction for tree and forest - over the sort Set is defined by the command: + A mutual induction principle for tree and forest in sort ``Set`` can be defined using the command .. coqtop:: none @@ -193,10 +192,12 @@ command generates the induction principle for each `identᵢ`, following the recursive structure and case analyses of the corresponding function identᵢ’. -Remark: There is a difference between obtaining an induction scheme by -using ``Functional Scheme`` on a function defined by ``Function`` or not. -Indeed, ``Function`` generally produces smaller principles, closer to the -definition written by the user. +.. warning:: + + There is a difference between induction schemes generated by the command + :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed, + :cmd:`Function` generally produces smaller principles that are closer to how + a user would implement them. See :ref:`advanced-recursive-functions` for details. .. example:: @@ -257,11 +258,6 @@ definition written by the user. auto with arith. Qed. - Remark: There is a difference between obtaining an induction scheme - for a function by using ``Function`` (see :ref:`advanced-recursive-functions`) and by using - ``Functional Scheme`` after a normal definition using ``Fixpoint`` or - ``Definition``. See :ref:`advanced-recursive-functions` for details. - .. example:: Induction scheme for tree_size. @@ -298,15 +294,15 @@ definition written by the user. | cons t f' => (tree_size t + forest_size f') end. - Remark: Function generates itself non mutual induction principles - tree_size_ind and forest_size_ind: + Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind`` + generated by ``Function`` are not mutual. .. coqtop:: all Check tree_size_ind. - The definition of mutual induction principles following the recursive - structure of `tree_size` and `forest_size` is defined by the command: + Mutual induction principles following the recursive structure of ``tree_size`` + and ``forest_size`` can be generated by the following command: .. coqtop:: all @@ -352,10 +348,8 @@ having inverted the instance with the tactic `inversion`. .. example:: - Let us consider the relation `Le` over natural numbers and the following - variable: - - .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning + Consider the relation `Le` over natural numbers and the following + parameter ``P``: .. coqtop:: all @@ -363,7 +357,7 @@ having inverted the instance with the tactic `inversion`. | LeO : forall n:nat, Le 0 n | LeS : forall n m:nat, Le n m -> Le (S n) (S m). - Axiom P : nat -> nat -> Prop. + Parameter P : nat -> nat -> Prop. To generate the inversion lemma for the instance `(Le (S n) m)` and the sort `Prop`, we do: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 37394386e6..d92b9a6794 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -50,11 +50,11 @@ A notation is always surrounded by double quotes (except when the abbreviation has the form of an ordinary applicative expression; see :ref:`Abbreviations`). The notation is composed of *tokens* separated by spaces. Identifiers in the string (such as ``A`` and ``B``) are the *parameters* -of the notation. They must occur at least once each in the denoted term. The +of the notation. Each of them must occur at least once in the denoted term. The other elements of the string (such as ``/\``) are the *symbols*. An identifier can be used as a symbol but it must be surrounded by -simple quotes to avoid the confusion with a parameter. Similarly, +single quotes to avoid the confusion with a parameter. Similarly, every symbol of at least 3 characters and starting with a simple quote must be quoted (then it starts by two single quotes). Here is an example. @@ -119,7 +119,7 @@ command understands. Here is how the previous examples refine. Notation "A /\ B" := (and A B) (at level 80, right associativity). Notation "A \/ B" := (or A B) (at level 85, right associativity). -By default, a notation is considered non associative, but the +By default, a notation is considered non-associative, but the precedence level is mandatory (except for special cases whose level is canonical). The level is either a number or the phrase ``next level`` whose meaning is obvious. @@ -139,7 +139,7 @@ instance define prefix notations. Notation "~ x" := (not x) (at level 75, right associativity). One can also define notations for incomplete terms, with the hole -expected to be inferred at typing time. +expected to be inferred during typechecking. .. coqtop:: in @@ -185,14 +185,14 @@ rules. Some simple left factorization work has to be done. Here is an example. Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70). -In order to factorize the left part of the rules, the sub-expression -referred by ``y`` has to be at the same level in both rules. However the +In order to factorize the left part of the rules, the subexpression +referred to by ``y`` has to be at the same level in both rules. However the default behavior puts ``y`` at the next level below 70 in the first rule -(``no associativity`` is the default), and at the level 200 in the second +(``no associativity`` is the default), and at level 200 in the second rule (``level 200`` is the default for inner expressions). To fix this, we need to force the parsing level of ``y``, as follows. -.. coqtop:: all +.. coqtop:: in Notation "x < y" := (lt x y) (at level 70). Notation "x < y < z" := (x < y /\ y < z) (at level 70, y at next level). @@ -283,7 +283,7 @@ the possible following elements delimited by single quotes: (4 spaces in the example) - well-bracketed pairs of tokens of the form ``'[hv '`` and ``']'`` are - translated into horizontal-orelse-vertical printing boxes; if the + translated into horizontal-or-else-vertical printing boxes; if the content of the box does not fit on a single line, then every breaking point forces a newline and an extra indentation of the number of spaces given after the “ ``[``” is applied at the beginning of each @@ -295,7 +295,7 @@ the possible following elements delimited by single quotes: of the box, and an extra indentation of the number of spaces given after the “``[``” is applied at the beginning of each newline -Notations do not survive the end of sections. No typing of the denoted +Notations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the notation. @@ -350,7 +350,7 @@ Simultaneous definition of terms and notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Thanks to reserved notations, the inductive, co-inductive, record, recursive and -corecursive definitions can benefit of customized notations. To do this, insert +corecursive definitions can benefit from customized notations. To do this, insert a ``where`` notation clause after the definition of the (co)inductive type or (co)recursive term (or after the definition of each of them in case of mutual definitions). The exact syntax is given by :token:`decl_notation` for inductive, @@ -359,17 +359,23 @@ for records. Here are examples: .. coqtop:: in - Inductive and (A B:Prop) : Prop := conj : A -> B -> A /\ B - where "A /\ B" := (and A B). + Reserved Notation "A & B" (at level 80). + +.. coqtop:: in + + Inductive and' (A B : Prop) : Prop := conj' : A -> B -> A & B + where "A & B" := (and' A B). + +.. coqtop:: in - Fixpoint plus (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (p+m) - end + Fixpoint plus (n m : nat) {struct n} : nat := + match n with + | O => m + | S p => S (p+m) + end where "n + m" := (plus n m). -Displaying informations about notations +Displaying information about notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. opt:: Printing Notations @@ -565,7 +571,7 @@ confused with the three-dots notation “``…``” used in this manual to denot a sequence of arbitrary size. On the left-hand side, the part “``x s .. s y``” of the notation parses -any number of times (but at least one time) a sequence of expressions +any number of times (but at least once) a sequence of expressions separated by the sequence of tokens ``s`` (in the example, ``s`` is just “``;``”). The right-hand side must contain a subterm of the form either @@ -608,7 +614,7 @@ Notations with recursive patterns involving binders Recursive notations can also be used with binders. The basic example is: -.. coqtop:: all +.. coqtop:: in Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..)) @@ -627,7 +633,7 @@ repeatedly nested as many times as the number of binders generated. If ever the generalization operator ``'`` (see :ref:`implicit-generalization`) is used in the binding list, the added binders are taken into account too. -Binders parsing exist in two flavors. If ``x`` and ``y`` are marked as binder, +There are two flavors of binder parsing. If ``x`` and ``y`` are marked as binder, then a sequence such as :g:`a b c : T` will be accepted and interpreted as the sequence of binders :g:`(a:T) (b:T) (c:T)`. For instance, in the notation above, the syntax :g:`exists a b : nat, a = b` is valid. @@ -698,42 +704,46 @@ Custom entries This command allows to define new grammar entries, called *custom entries*, that can later be referred to using the entry name - :n:`custom @ident`. For instance, we may want to define an ad hoc - parser for arithmetical operations and proceed as follows: + :n:`custom @ident`. -.. coqtop:: all +.. example:: - Inductive Expr := - | One : Expr - | Mul : Expr -> Expr -> Expr - | Add : Expr -> Expr -> Expr. + For instance, we may want to define an ad hoc + parser for arithmetical operations and proceed as follows: - Declare Custom Entry expr. - Notation "[ e ]" := e (e custom expr at level 2). - Notation "1" := One (in custom expr at level 0). - Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). - Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). - Notation "( x )" := x (in custom expr, x at level 2). - Notation "{ x }" := x (in custom expr, x constr). - Notation "x" := x (in custom expr at level 0, x ident). - - Axiom f : nat -> Expr. - Check fun x y z => [1 + y z + {f x}]. - Unset Printing Notations. - Check fun x y z => [1 + y z + {f x}]. - Set Printing Notations. - Check fun e => match e with - | [1 + 1] => [1] - | [x y + z] => [x + y z] - | y => [y + e] - end. + .. coqtop:: all + + Inductive Expr := + | One : Expr + | Mul : Expr -> Expr -> Expr + | Add : Expr -> Expr -> Expr. + + Declare Custom Entry expr. + Notation "[ e ]" := e (e custom expr at level 2). + Notation "1" := One (in custom expr at level 0). + Notation "x y" := (Mul x y) (in custom expr at level 1, left associativity). + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + Notation "( x )" := x (in custom expr, x at level 2). + Notation "{ x }" := x (in custom expr, x constr). + Notation "x" := x (in custom expr at level 0, x ident). + + Axiom f : nat -> Expr. + Check fun x y z => [1 + y z + {f x}]. + Unset Printing Notations. + Check fun x y z => [1 + y z + {f x}]. + Set Printing Notations. + Check fun e => match e with + | [1 + 1] => [1] + | [x y + z] => [x + y z] + | y => [y + e] + end. Custom entries have levels, like the main grammar of terms and grammar of patterns have. The lower level is 0 and this is the level used by default to put rules delimited with tokens on both ends. The level is -left to be inferred by Coq when using :n:`in custom @ident``. The -level is otherwise given explicitly by using the syntax :n:`in custom -@ident at level @num`, where :n:`@num` refers to the level. +left to be inferred by Coq when using :n:`in custom @ident`. The +level is otherwise given explicitly by using the syntax +:n:`in custom @ident at level @num`, where :n:`@num` refers to the level. Levels are cumulative: a notation at level ``n`` of which the left end is a term shall use rules at level less than ``n`` to parse this @@ -745,16 +755,26 @@ the right end is a term shall use by default rules at level strictly less than ``n`` to parse this sub-term if the rule is declared left associative and rules at level less or equal than ``n`` if the rule is declared right associative. This is what happens for instance in the -rule ``Notation "x + y" := (Add x y) (in custom expr at level 2, left -associativity)`` where ``x`` is any expression parsed in entry +rule + +.. coqtop:: in + + Notation "x + y" := (Add x y) (in custom expr at level 2, left associativity). + +where ``x`` is any expression parsed in entry ``expr`` at level less or equal than ``2`` (including, recursively, the given rule) and ``y`` is any expression parsed in entry ``expr`` at level strictly less than ``2``. Rules associated to an entry can refer different sub-entries. The grammar entry name ``constr`` can be used to refer to the main grammar -of term as in the rule ``Notation "{ x }" := x (in custom expr at -level 0, x constr)`` which indicates that the subterm ``x`` should be +of term as in the rule + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +which indicates that the subterm ``x`` should be parsed using the main grammar. If not indicated, the level is computed as for notations in ``constr``, e.g. using 200 as default level for inner sub-expressions. The level can otherwise be indicated explicitly @@ -763,10 +783,19 @@ level``. Conversely, custom entries can be used to parse sub-expressions of the main grammar, or from another custom entry as is the case in -:g:`Notation "[ e ]" := e (e custom expr at level 2)` to indicate that -``e`` has to be parsed at level ``2`` of the grammar associated to the -custom entry ``expr``. The level can be omitted, as in :g:`Notation "[ e -]" := e (e custom expr)`, in which case Coq tries to infer it. + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr at level 2). + +to indicate that ``e`` has to be parsed at level ``2`` of the grammar +associated to the custom entry ``expr``. The level can be omitted, as in + +.. coqtop:: in + + Notation "[ e ]" := e (e custom expr)`. + +in which case Coq tries to infer it. In the absence of an explicit entry for parsing or printing a sub-expression of a notation in a custom entry, the default is to @@ -779,23 +808,40 @@ level n``. In general, rules are required to be *productive* on the right-hand side, i.e. that they are bound to an expression which is not reduced to a single variable. If the rule is not productive on the -right-hand side, as it is the case above for :g:`Notation "( x )" := x -(in custom expr at level 0, x at level 2)` and :g:`Notation "{ x }" := -x (in custom expr at level 0, x constr)`, it is used as a *grammar -coercion* which means that it is used to parse or print an expression -which is not available in the current grammar at the current level of -parsing or printing for this grammar but which is available in another -grammar or in another level of the current grammar. For instance, -:g:`Notation "( x )" := x (in custom expr at level 0, x at level 2)` +right-hand side, as it is the case above for + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + +and + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +it is used as a *grammar coercion* which means that it is used to parse or +print an expression which is not available in the current grammar at the +current level of parsing or printing for this grammar but which is available +in another grammar or in another level of the current grammar. For instance, + +.. coqtop:: in + + Notation "( x )" := x (in custom expr at level 0, x at level 2). + tells that parentheses can be inserted to parse or print an expression declared at level ``2`` of ``expr`` whenever this expression is expected to be used as a subterm at level 0 or 1. This allows for instance to parse and print :g:`Add x y` as a subterm of :g:`Mul (Add -x y) z` using the syntax ``(x + y) z``. Similarly, :g:`Notation "{ x }" -:= x (in custom expr at level 0, x constr)` gives a way to let any -arbitrary expression which is not in handled by the custom entry -``expr`` be parsed or printed by the main grammar of term up to the -insertion of a pair of curly brackets. +x y) z` using the syntax ``(x + y) z``. Similarly, + +.. coqtop:: in + + Notation "{ x }" := x (in custom expr at level 0, x constr). + +gives a way to let any arbitrary expression which is not handled by the +custom entry ``expr`` be parsed or printed by the main grammar of term +up to the insertion of a pair of curly brackets. .. cmd:: Print Grammar @ident. @@ -876,7 +922,7 @@ notations are given below. The optional :production:`scope` is described in Persistence of notations ++++++++++++++++++++++++ -Neither notations nor custom entries survive the end of sections. +Notations disappear when a section is closed. .. cmd:: Local Notation @notation @@ -894,9 +940,9 @@ Interpretation scopes ---------------------- An *interpretation scope* is a set of notations for terms with their -interpretation. Interpretation scopes provide a weak, purely -syntactical form of notations overloading: the same notation, for -instance the infix symbol ``+`` can be used to denote distinct +interpretations. Interpretation scopes provide a weak, purely +syntactical form of notation overloading: the same notation, for +instance the infix symbol ``+``, can be used to denote distinct definitions of the additive operator. Depending on which interpretation scopes are currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and @@ -907,7 +953,7 @@ See :ref:`above <NotationSyntax>` for the syntax of notations including the possibility to declare them in a given scope. Here is a typical example which declares the notation for conjunction in the scope ``type_scope``. -.. coqdoc:: +.. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. @@ -917,10 +963,10 @@ declares the notation for conjunction in the scope ``type_scope``. Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -At any time, the interpretation of a notation for term is done within +At any time, the interpretation of a notation for a term is done within a *stack* of interpretation scopes and lonely notations. In case a notation has several interpretations, the actual interpretation is the -one defined by (or in) the more recently declared (or open) lonely +one defined by (or in) the more recently declared (or opened) lonely notation (or interpretation scope) which defines this notation. Typically if a given notation is defined in some scope ``scope`` but has also an interpretation not assigned to a scope, then, if ``scope`` is open @@ -946,7 +992,7 @@ lonely notations. These scopes, in opening order, are ``core_scope``, stack by using the command :n:`Close Scope @scope`. Notice that this command does not only cancel the last :n:`Open Scope @scope` - but all the invocations of it. + but all its invocations. .. note:: ``Open Scope`` and ``Close Scope`` do not survive the end of sections where they occur. When defined outside of a section, they are exported @@ -1026,11 +1072,11 @@ Binding arguments of a constant to an interpretation scope the scope is limited to the argument itself. It does not propagate to subterms but the subterms that, after interpretation of the notation, turn to be themselves arguments of a reference are interpreted - accordingly to the arguments scopes bound to this reference. + accordingly to the argument scopes bound to this reference. .. cmdv:: Arguments @qualid : clear scopes - Arguments scopes can be cleared with :n:`Arguments @qualid : clear scopes`. + This command can be used to clear argument scopes of :token:`qualid`. .. cmdv:: Arguments @qualid {+ @name%scope} : extra scopes @@ -1152,34 +1198,34 @@ Scopes` or :cmd:`Print Scope`. ``type_scope`` This scope includes infix * for product types and infix + for sum types. It - is delimited by key ``type``, and bound to the coercion class + is delimited by the key ``type``, and bound to the coercion class ``Sortclass``, as described above. ``function_scope`` - This scope is delimited by key ``function``, and bound to the coercion class + This scope is delimited by the key ``function``, and bound to the coercion class ``Funclass``, as described above. ``nat_scope`` This scope includes the standard arithmetical operators and relations on type nat. Positive numerals in this scope are mapped to their canonical - representent built from :g:`O` and :g:`S`. The scope is delimited by key + representent built from :g:`O` and :g:`S`. The scope is delimited by the key ``nat``, and bound to the type :g:`nat` (see above). ``N_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`N` (binary natural numbers). It is delimited by key ``N`` and comes + type :g:`N` (binary natural numbers). It is delimited by the key ``N`` and comes with an interpretation for numerals as closed terms of type :g:`N`. ``Z_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`Z` (binary integer numbers). It is delimited by key ``Z`` and comes - with an interpretation for numerals as closed term of type :g:`Z`. + type :g:`Z` (binary integer numbers). It is delimited by the key ``Z`` and comes + with an interpretation for numerals as closed terms of type :g:`Z`. ``positive_scope`` This scope includes the standard arithmetical operators and relations on type :g:`positive` (binary strictly positive numbers). It is delimited by key ``positive`` and comes with an interpretation for numerals as closed - term of type :g:`positive`. + terms of type :g:`positive`. ``Q_scope`` This scope includes the standard arithmetical operators and relations on @@ -1196,20 +1242,20 @@ Scopes` or :cmd:`Print Scope`. ``real_scope`` This scope includes the standard arithmetical operators and relations on - type :g:`R` (axiomatic real numbers). It is delimited by key ``R`` and comes + type :g:`R` (axiomatic real numbers). It is delimited by the key ``R`` and comes with an interpretation for numerals using the :g:`IZR` morphism from binary integer numbers to :g:`R`. ``bool_scope`` - This scope includes notations for the boolean operators. It is delimited by + This scope includes notations for the boolean operators. It is delimited by the key ``bool``, and bound to the type :g:`bool` (see above). ``list_scope`` - This scope includes notations for the list operators. It is delimited by key + This scope includes notations for the list operators. It is delimited by the key ``list``, and bound to the type :g:`list` (see above). ``core_scope`` - This scope includes the notation for pairs. It is delimited by key ``core``. + This scope includes the notation for pairs. It is delimited by the key ``core``. ``string_scope`` This scope includes notation for strings as elements of the type string. @@ -1228,7 +1274,7 @@ Scopes` or :cmd:`Print Scope`. the ASCII code 34), all of them being represented in the type :g:`ascii`. -Displaying informations about scopes +Displaying information about scopes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Print Visibility @@ -1236,7 +1282,7 @@ Displaying informations about scopes This displays the current stack of notations in scopes and lonely notations that is used to interpret a notation. The top of the stack is displayed last. Notations in scopes whose interpretation is hidden - by the same notation in a more recently open scope are not displayed. + by the same notation in a more recently opened scope are not displayed. Hence each notation is displayed only once. .. cmdv:: Print Visibility @scope @@ -1249,13 +1295,13 @@ Displaying informations about scopes .. cmd:: Print Scopes This displays all the notations, delimiting keys and corresponding - class of all the existing interpretation scopes. It also displays the + classes of all the existing interpretation scopes. It also displays the lonely notations. .. cmdv:: Print Scope @scope :name: Print Scope - This displays all the notations defined in interpretation scope :token:`scope`. + This displays all the notations defined in the interpretation scope :token:`scope`. It also displays the delimiting key if any and the class to which the scope is bound, if any. @@ -1297,13 +1343,13 @@ Abbreviations much as possible by the Coq printers unless the modifier ``(only parsing)`` is given. - Abbreviations are bound to an absolute name as an ordinary definition - is, and they can be referred by qualified names too. + An abbreviation is bound to an absolute name as an ordinary definition is + and it also can be referred to by a qualified name. Abbreviations are syntactic in the sense that they are bound to expressions which are not typed at the time of the definition of the - abbreviation but at the time it is used. Especially, abbreviations can - be bound to terms with holes (i.e. with “``_``”). For example: + abbreviation but at the time they are used. Especially, abbreviations + can be bound to terms with holes (i.e. with “``_``”). For example: .. coqtop:: none reset @@ -1313,13 +1359,16 @@ Abbreviations .. coqtop:: in Definition explicit_id (A:Set) (a:A) := a. + + .. coqtop:: in + Notation id := (explicit_id _). .. coqtop:: all Check (id 0). - Abbreviations do not survive the end of sections. No typing of the + Abbreviations disappear when a section is closed. No typing of the denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. @@ -1328,8 +1377,7 @@ Abbreviations Tactic Notations ----------------- -Tactic notations allow to customize the syntax of the tactics of the -tactic language. Tactic notations obey the following syntax: +Tactic notations allow to customize the syntax of tactics. They have the following syntax: .. productionlist:: coq tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. @@ -1351,7 +1399,7 @@ tactic language. Tactic notations obey the following syntax: a terminal symbol, i.e. a string, for the first production item. The tactic level indicates the parsing precedence of the tactic notation. This information is particularly relevant for notations of tacticals. - Levels 0 to 5 are available (default is 0). + Levels 0 to 5 are available (default is 5). .. cmd:: Print Grammar tactic @@ -1378,7 +1426,7 @@ tactic language. Tactic notations obey the following syntax: * - ``simple_intropattern`` - intro_pattern - - an intro_pattern + - an intro pattern - intros * - ``hyp`` @@ -1432,7 +1480,7 @@ tactic language. Tactic notations obey the following syntax: - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of simple L tac + entry for argument type must include the case of a simple |Ltac| identifier as part of what it parses. This is naturally the case for ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. This is the reason for introducing a special entry ``int_or_var`` which @@ -1446,18 +1494,16 @@ tactic language. Tactic notations obey the following syntax: .. cmdv:: Local Tactic Notation - Tactic notations do not survive the end of sections. They survive - modules unless the command Local Tactic Notation is used instead of - Tactic Notation. + Tactic notations disappear when a section is closed. They survive when + a module is closed unless the command ``Local Tactic Notation`` is used instead + of :cmd:`Tactic Notation`. .. rubric:: Footnotes .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as ``no - associativity`` but the parser on which Coq is built, namely - Camlp5, currently does not implement ``no associativity`` and - replaces it with ``left associativity``; hence it is the same for - Coq: ``no associativity`` is in fact ``left associativity``, for - the purposes of parsing +.. [#no_associativity] Coq accepts notations declared as non-associative but the parser on + which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and + replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` + is in fact ``left associativity`` for the purposes of parsing diff --git a/test-suite/bugs/closed/4202.v b/test-suite/bugs/closed/4202.v new file mode 100644 index 0000000000..522a3604a3 --- /dev/null +++ b/test-suite/bugs/closed/4202.v @@ -0,0 +1,10 @@ +Parameter g : nat -> Prop. +Axiom a : forall n, g (S n). +Lemma foo (H : True) : exists n, g n /\ g n. +eexists. +clear H. +split. +simple apply a. +(* goal is "g (S ?Goal0@ {H:=H})" while H has long ceased to exist *) +simpl. +Abort. |