diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/extended-pattern-matching.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 42 | ||||
| -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/miscellaneous-extensions.rst | 1 | ||||
| -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/program.rst | 34 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 88 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 |
12 files changed, 480 insertions, 502 deletions
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/extraction.rst b/doc/sphinx/addendum/extraction.rst index cb93d48a41..8c1eacf085 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -116,13 +116,13 @@ be optimized in order to be efficient (for instance, when using induction principles we do not want to compute all the recursive calls but only the needed ones). So the extraction mechanism provides an automatic optimization routine that will be called each time the user -want to generate |OCaml| programs. The optimizations can be split in two +wants to generate an |OCaml| program. The optimizations can be split in two groups: the type-preserving ones (essentially constant inlining and reductions) and the non type-preserving ones (some function abstractions of dummy types are removed when it is deemed safe in order to have more elegant types). Therefore some constants may not appear in the resulting monolithic |OCaml| program. In the case of modular extraction, -even if some inlining is done, the inlined constant are nevertheless +even if some inlining is done, the inlined constants are nevertheless printed, to ensure session-independent programs. Concerning Haskell, type-preserving optimizations are less useful @@ -185,7 +185,7 @@ The type-preserving optimizations are controlled by the following |Coq| options: **Inlining and printing of a constant declaration:** -A user can explicitly ask for a constant to be extracted by two means: +The user can explicitly ask for a constant to be extracted by two means: * by mentioning it on the extraction command line @@ -224,19 +224,18 @@ principles of extraction (logical parts and types). When an actual extraction takes place, an error is normally raised if the :cmd:`Extraction Implicit` declarations cannot be honored, that is -if any of the implicited variables still occurs in the final code. +if any of the implicit arguments still occurs in the final code. This behavior can be relaxed via the following option: .. opt:: Extraction SafeImplicits Default is on. When this option is off, a warning is emitted - instead of an error if some implicited variables still occur in the + instead of an error if some implicit arguments still occur in the final code of an extraction. This way, the extracted code may be obtained nonetheless and reviewed manually to locate the source of the issue - (in the code, some comments mark the location of these remaining - implicited variables). + (in the code, some comments mark the location of these remaining implicit arguments). Note that this extracted code might not compile or run properly, - depending of the use of these remaining implicited variables. + depending of the use of these remaining implicit arguments. Realizing axioms ~~~~~~~~~~~~~~~~ @@ -296,7 +295,7 @@ The number of type variables is checked by the system. For example: Realizing an axiom via :cmd:`Extract Constant` is only useful in the case of an informative axiom (of sort ``Type`` or ``Set``). A logical axiom -have no computational content and hence will not appears in extracted +has no computational content and hence will not appear in extracted terms. But a warning is nonetheless issued if extraction encounters a logical axiom. This warning reminds user that inconsistent logical axioms may lead to incorrect or non-terminating extracted terms. @@ -312,7 +311,7 @@ Realizing inductive types The system also provides a mechanism to specify ML terms for inductive types and constructors. For instance, the user may want to use the ML -native boolean type instead of |Coq| one. The syntax is the following: +native boolean type instead of the |Coq| one. The syntax is the following: .. cmd:: Extract Inductive @qualid => @string [ {+ @string } ] @@ -332,10 +331,10 @@ native boolean type instead of |Coq| one. The syntax is the following: branches in functional form, and then the inductive element to destruct. For instance, the match branch ``| S n => foo`` gives the functional form ``(fun n -> foo)``. Note that a constructor with no - argument is considered to have one unit argument, in order to block + arguments is considered to have one unit argument, in order to block early evaluation of the branch: ``| O => bar`` leads to the functional form ``(fun () -> bar)``. For instance, when extracting ``nat`` - into |OCaml| ``int``, the code to provide has type: + into |OCaml| ``int``, the code to be provided has type: ``(unit->'a)->(int->'a)->int->'a``. .. caution:: As for :cmd:`Extract Constant`, this command should be used with care: @@ -371,7 +370,7 @@ Typical examples are the following: When extracting to |OCaml|, if an inductive constructor or type has arity 2 and the corresponding string is enclosed by parentheses, and the string meets |OCaml|'s lexical criteria for an infix symbol, then the rest of the string is - used as infix constructor or type. + used as an infix constructor or type. .. coqtop:: in @@ -389,7 +388,7 @@ Avoiding conflicts with existing filenames ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ When using :cmd:`Extraction Library`, the names of the extracted files -directly depends from the names of the |Coq| files. It may happen that +directly depend on the names of the |Coq| files. It may happen that these filenames are in conflict with already existing files, either in the standard library of the target language or in other code that is meant to be linked with the extracted code. @@ -475,17 +474,18 @@ type-checker without any ``Obj.magic`` (see examples below). Some examples ------------- -We present here two examples of extractions, taken from the -|Coq| Standard Library. We choose |OCaml| as target language, -but all can be done in the other dialects with slight modifications. +We present here two examples of extraction, taken from the +|Coq| Standard Library. We choose |OCaml| as the target language, +but everything, with slight modifications, can also be done in the +other languages supported by extraction. We then indicate where to find other examples and tests of extraction. A detailed example: Euclidean division ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ The file ``Euclid`` contains the proof of Euclidean division. -The natural numbers used there are unary integers of type ``nat``, -defined by two constructors ``O`` and ``S``. +The natural numbers used here are unary, represented by the type``nat``, +which is defined by two constructors ``O`` and ``S``. This module contains a theorem ``eucl_dev``, whose type is:: forall b:nat, b > 0 -> forall a:nat, diveucl a b @@ -579,7 +579,7 @@ extraction test: * ``stalmarck`` : https://github.com/coq-contribs/stalmarck Note that ``continuations`` and ``multiplier`` are a bit particular. They are -examples of developments where ``Obj.magic`` are needed. This is -probably due to an heavy use of impredicativity. After compilation, those +examples of developments where ``Obj.magic`` is needed. This is +probably due to a heavy use of impredicativity. After compilation, those two examples run nonetheless, thanks to the correction of the extraction :cite:`Let02`. 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/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b6c35d8fa7..0f2d35d044 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -32,6 +32,7 @@ When the proof ends two constants are defined: ends with ``Qed``, and transparent if the proof ends with ``Defined``. .. example:: + .. coqtop:: all Require Coq.derive.Derive. 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/program.rst b/doc/sphinx/addendum/program.rst index b685e68e43..28fe68d78d 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -38,12 +38,12 @@ obligations which need to be resolved to create the final term. Elaborating programs --------------------- -The main difference from |Coq| is that an object in a type T : Set can -be considered as an object of type { x : T | P} for any wellformed P : -Prop. If we go from T to the subset of T verifying property P, we must -prove that the object under consideration verifies it. Russell will -generate an obligation for every such coercion. In the other -direction, Russell will automatically insert a projection. +The main difference from |Coq| is that an object in a type :g:`T : Set` can +be considered as an object of type :g:`{x : T | P}` for any well-formed +:g:`P : Prop`. If we go from :g:`T` to the subset of :g:`T` verifying property +:g:`P`, we must prove that the object under consideration verifies it. Russell +will generate an obligation for every such coercion. In the other direction, +Russell will automatically insert a projection. Another distinction is the treatment of pattern-matching. Apart from the following differences, it is equivalent to the standard match @@ -67,7 +67,7 @@ operation (see :ref:`extendedpatternmatching`). (match x as y return (x = y -> _) with | 0 => fun H : x = 0 -> t | S n => fun H : x = S n -> u - end) (eq_refl n). + end) (eq_refl x). This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. @@ -75,7 +75,7 @@ operation (see :ref:`extendedpatternmatching`). + Generation of inequalities. If a pattern intersects with a previous one, an inequality is added in the context of the second branch. See for example the definition of div2 below, where the second branch is - typed in a context where ∀ p, _ <> S (S p). + typed in a context where :g:`∀ p, _ <> S (S p)`. + Coercion. If the object being matched is coercible to an inductive type, the corresponding coercion will be automatically inserted. This also works with the previous mechanism. @@ -88,7 +88,7 @@ coercions. This controls the special treatment of pattern-matching generating equalities and inequalities when using |Program| (it is on by default). All - pattern-matchings and let-patterns are handled using the standard algorithm + pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. @@ -108,9 +108,9 @@ typechecker will fall back directly to |Coq|’s usual typing of dependent pattern-matching if a return or in clause is specified. Likewise, the if construct is not treated specially by |Program| so boolean tests in the code are not automatically reflected in the obligations. One can -use the dec combinator to get the correct hypotheses as in: +use the :g:`dec` combinator to get the correct hypotheses as in: -.. coqtop:: none +.. coqtop:: in Require Import Program Arith. @@ -120,7 +120,7 @@ use the dec combinator to get the correct hypotheses as in: if dec (leb n 0) then 0 else S (pred n). -The let tupling construct :g:`let (x1, ..., xn) := t in b` does not +The :g:`let` tupling construct :g:`let (x1, ..., xn) := t in b` does not produce an equality, contrary to the let pattern construct :g:`let ’(x1, ..., xn) := t in b`. Also, :g:`term :>` explicitly asks the system to coerce term to its support type. It can be useful in notations, for @@ -200,7 +200,7 @@ The structural fixpoint operator behaves just like the one of |Coq| (see :cmd:`Fixpoint`), except it may also generate obligations. It works with mutually recursive definitions too. -.. coqtop:: reset none +.. coqtop:: reset in Require Import Program Arith. @@ -264,7 +264,7 @@ Program Lemma Definition` and use it as the goal afterwards. Otherwise the proof will be started with the elaborated version as a goal. The :g:`Program` prefix can similarly be used as a prefix for - :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc... + :g:`Variable`, :g:`Hypothesis`, :g:`Axiom` etc. .. _solving_obligations: @@ -300,7 +300,7 @@ optional tactic is replaced by the default one if not specified. Start the proof of the next unsolved obligation. -.. cmd:: Solve Obligations {? of @ident} {? with @tactic} +.. cmd:: Solve Obligations {? {? of @ident} with @tactic} Tries to solve each obligation of ``ident`` using the given ``tactic`` or the default one. @@ -322,13 +322,13 @@ optional tactic is replaced by the default one if not specified. .. opt:: Transparent Obligations - Control whether all obligations should be declared as transparent + Controls whether all obligations should be declared as transparent (the default), or if the system should infer which obligations can be declared opaque. .. opt:: Hide Obligations - Control whether obligations appearing in the + Controls whether obligations appearing in the term should be hidden as implicit arguments of the special constantProgram.Tactics.obligation. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 6a9b343ba8..d5c33dc1d4 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -13,7 +13,7 @@ The ring and field tactic families :Author: Bruno Barras, Benjamin Grégoire, Assia Mahboubi, Laurent Théry [#f1]_ -This chapter presents the tactics dedicated to deal with ring and +This chapter presents the tactics dedicated to dealing with ring and field equations. What does this tactic do? @@ -36,7 +36,7 @@ is strictly less than the following monomial according to the lexicographic order. It is an easy theorem to show that every polynomial is equivalent (modulo the ring properties) to exactly one canonical sum. This canonical sum is called the normal form of the polynomial. In fact, the actual representation shares -monomials with same prefixes. So what does ring? It normalizes polynomials over +monomials with same prefixes. So what does the ``ring`` tactic do? It normalizes polynomials over any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring expressions, so that the user does not have to deal manually with the theorems of associativity and commutativity. @@ -59,9 +59,8 @@ The variables map It is frequent to have an expression built with :math:`+` and :math:`\times`, but rarely on variables only. Let us associate a number to each subterm of a -ring expression in the Gallina language. For example in the ring |nat|, consider -the expression: - +ring expression in the Gallina language. For example, consider this expression +in the semiring ``nat``: :: @@ -104,7 +103,7 @@ Concrete usage in Coq .. tacn:: ring The ``ring`` tactic solves equations upon polynomial expressions of a ring -(or semi-ring) structure. It proceeds by normalizing both hand sides +(or semi-ring) structure. It proceeds by normalizing both sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation, rewriting of monomials) and comparing syntactically the results. @@ -112,9 +111,9 @@ comparing syntactically the results. .. tacn:: ring_simplify ``ring_simplify`` applies the normalization procedure described above to -the terms given. The tactic then replaces all occurrences of the terms +the given terms. The tactic then replaces all occurrences of the terms given in the conclusion of the goal by their normal forms. If no term -is given, then the conclusion should be an equation and both hand +is given, then the conclusion should be an equation and both sides are normalized. The tactic can also be applied in a hypothesis. The tactic must be loaded by ``Require Import Ring``. The ring structures @@ -187,7 +186,7 @@ Error messages: .. exn:: Cannot find a declared ring structure for equality @term. - Same as above is the case of the ``ring`` tactic. + Same as above in the case of the ``ring`` tactic. Adding a ring structure @@ -198,8 +197,8 @@ carrier set, an equality, and ring operations: ``Ring_theory.ring_theory`` and ``Ring_theory.semi_ring_theory``) satisfies the ring axioms. Semi- rings (rings without + inverse) are also supported. The equality can be either Leibniz equality, or any relation declared as a setoid (see -:ref:`tactics-enabled-on-user-provided-relations`). The definition of ring and semi-rings (see module -``Ring_theory``) is: +:ref:`tactics-enabled-on-user-provided-relations`). +The definitions of ring and semiring (see module ``Ring_theory``) are: .. coqtop:: in @@ -305,7 +304,7 @@ The syntax for adding a new ring is .. cmd:: Add Ring @ident : @term {? ( @ring_mod {* , @ring_mod } )} -The :n:`@ident` is not relevant. It is just used for error messages. The +The :n:`@ident` is not relevant. It is used just for error messages. The :n:`@term` is a proof that the ring signature satisfies the (semi-)ring axioms. The optional list of modifiers is used to tailor the behavior of the tactic. The following list describes their syntax and effects: @@ -386,7 +385,7 @@ sign :n:`@term` div :n:`@term` allows ``ring`` and ``ring_simplify`` to use monomials with - coefficient other than 1 in the rewriting. The term :n:`@term` is a proof + coefficients other than 1 in the rewriting. The term :n:`@term` is a proof that a given division function satisfies the specification of an euclidean division function (:n:`@term` has to be a proof of ``Ring_theory.div_theory``). For example, this function is called when @@ -414,13 +413,13 @@ Error messages: How does it work? ---------------------- -The code of ring is a good example of tactic written using *reflection*. -What is reflection? Basically, it is writing |Coq| tactics in |Coq|, rather -than in |OCaml|. From the philosophical point of view, it is -using the ability of the Calculus of Constructions to speak and reason -about itself. For the ring tactic we used Coq as a programming -language and also as a proof environment to build a tactic and to -prove it correctness. +The code of ``ring`` is a good example of a tactic written using *reflection*. +What is reflection? Basically, using it means that a part of a tactic is written +in Gallina, Coq's language of terms, rather than |Ltac| or |OCaml|. From the +philosophical point of view, reflection is using the ability of the Calculus of +Constructions to speak and reason about itself. For the ``ring`` tactic we used +Coq as a programming language and also as a proof environment to build a tactic +and to prove its correctness. The interested reader is strongly advised to have a look at the file ``Ring_polynom.v``. Here a type for polynomials is defined: @@ -452,7 +451,7 @@ Polynomials in normal form are defined as: where ``Pinj n P`` denotes ``P`` in which :math:`V_i` is replaced by :math:`V_{i+n}` , and ``PX P n Q`` denotes :math:`P \otimes V_1^n \oplus Q'`, `Q'` being `Q` where :math:`V_i` is replaced by :math:`V_{i+1}`. -Variables maps are represented by list of ring elements, and two +Variable maps are represented by lists of ring elements, and two interpretation functions, one that maps a variables map and a polynomial to an element of the concrete ring, and the second one that does the same for normal forms: @@ -490,18 +489,18 @@ concrete expression `p’`, which is the concrete normal form of `p`. This is su `p’` |la| |le| ========= ====== ==== -The user do not see the right part of the diagram. From outside, the -tactic behaves like a |bdi| simplification extended with AC rewriting -rules. Basically, the proof is only the application of the main -correctness theorem to well-chosen arguments. +The user does not see the right part of the diagram. From outside, the +tactic behaves like a |bdi| simplification extended with rewriting rules +for associativity and commutativity. Basically, the proof is only the +application of the main correctness theorem to well-chosen arguments. Dealing with fields ------------------------ .. tacn:: field -The ``field`` tactic is an extension of the ``ring`` to deal with rational -expression. Given a rational expression :math:`F = 0`. It first reduces the +The ``field`` tactic is an extension of the ``ring`` tactic that deals with rational +expressions. Given a rational expression :math:`F = 0`. It first reduces the expression `F` to a common denominator :math:`N/D = 0` where `N` and `D` are two ring expressions. For example, if we take :math:`F = (1 − 1/x) x − x + 1`, this gives :math:`N = (x − 1) x − x^2 + x` and :math:`D = x`. It then calls ring to solve @@ -523,7 +522,7 @@ structures can be declared to the system with the ``Add Field`` command (in ``plugins/setoid_ring``). It is exported by module ``Rbase``, so that requiring ``Rbase`` or ``Reals`` is enough to use the field tactics on real numbers. Rational numbers in canonical form are also declared as -a field in module ``Qcanon``. +a field in the module ``Qcanon``. .. example:: @@ -559,8 +558,8 @@ a field in module ``Qcanon``. performs the simplification in the conclusion of the goal, :math:`F_1 = F_2` becomes :math:`N_1 / D_1 = N_2 / D_2`. A normalization step (the same as the one for rings) is then applied to :math:`N_1`, :math:`D_1`, - :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during the - fraction simplifications. This yields smaller expressions when + :math:`N_2` and :math:`D_2`. This way, polynomials remain in factorized form during + fraction simplification. This yields smaller expressions when reducing to the same denominator since common factors can be canceled. .. tacv:: field_simplify [{* @term }] @@ -657,7 +656,7 @@ The syntax for adding a new field is .. cmd:: Add Field @ident : @term {? ( @field_mod {* , @field_mod } )} -The :n:`@ident` is not relevant. It is just used for error +The :n:`@ident` is not relevant. It is used just for error messages. :n:`@term` is a proof that the field signature satisfies the (semi-)field axioms. The optional list of modifiers is used to tailor the behavior of the tactic. @@ -704,9 +703,8 @@ it using reflection (see :cite:`Bou97`). Later, it was rewritten by Patrick Loiseleur: the new tactic does not any more require ``ACDSimpl`` to compile and it makes use of |bdi|-reduction not only to replace the rewriting steps, but also to achieve the -interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote a -few |ML| code for the ``Add Ring`` command, that allow to register new rings -dynamically. +interleaving of computation and reasoning (see :ref:`discussion_reflection`). He also wrote +some |ML| code for the ``Add Ring`` command that allows registering new rings dynamically. Proofs terms generated by ring are quite small, they are linear in the number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type-checking @@ -733,15 +731,15 @@ Then it is rewritten to ``34 − x + 2 * x + 12``, very far from the expected re Here rewriting is not sufficient: you have to do some kind of reduction (some kind of computation) to achieve the normalization. -The tactic ``ring`` is not only faster than a classical one: using -reflection, we get for free integration of computation and reasoning -that would be very complex to implement in the classic fashion. +The tactic ``ring`` is not only faster than the old one: by using +reflection, we get for free the integration of computation and reasoning +that would be very difficult to implement without it. Is it the ultimate way to write tactics? The answer is: yes and no. -The ``ring`` tactic uses intensively the conversion rule of |Cic|, that is -replaces proof by computation the most as it is possible. It can be -useful in all situations where a classical tactic generates huge proof -terms. Symbolic Processing and Tautologies are in that case. But there +The ``ring`` tactic intensively uses the conversion rules of the Calculus of +Inductive Constructions, i.e. it replaces proofs by computations as much as possible. +It can be useful in all situations where a classical tactic generates huge proof +terms, like symbolic processing and tautologies. But there are also tactics like ``auto`` or ``linear`` that do many complex computations, using side-effects and backtracking, and generate a small proof term. Clearly, it would be significantly less efficient to replace them by @@ -750,12 +748,12 @@ tactics using reflection. Another idea suggested by Benjamin Werner: reflection could be used to couple an external tool (a rewriting program or a model checker) with |Coq|. We define (in |Coq|) a type of terms, a type of *traces*, and -prove a correction theorem that states that *replaying traces* is safe -w.r.t some interpretation. Then we let the external tool do every +prove a correctness theorem that states that *replaying traces* is safe +with respect to some interpretation. Then we let the external tool do every computation (using side-effects, backtracking, exception, or others features that are not available in pure lambda calculus) to produce -the trace: now we can check in |Coq| that the trace has the expected -semantic by applying the correction lemma. +the trace. Now we can check in |Coq| that the trace has the expected +semantics by applying the correctness theorem. 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. |