diff options
Diffstat (limited to 'doc')
24 files changed, 250 insertions, 228 deletions
diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index 3af3115a59..2cc1f95c08 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -75,7 +75,7 @@ We amend that by equipping ``nat`` with a comparison relation. Check 3 == 3. Eval compute in 3 == 4. -This last test shows that |Coq| is now not only able to typecheck ``3 == 3``, +This last test shows that |Coq| is now not only able to type check ``3 == 3``, but also that the infix relation was bound to the ``nat_eq`` relation. This relation is selected whenever ``==`` is used on terms of type nat. This can be read in the line declaring the canonical structure diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 8c1eacf085..e3d25cf5cf 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -423,7 +423,7 @@ a generic type ``'a`` to any term. First, if some part of the program is *very* polymorphic, there may be no ML type for it. In that case the extraction to ML works alright but the generated code may be refused by the ML -type-checker. A very well known example is the ``distr-pair`` +type checker. A very well known example is the ``distr-pair`` function: .. coqtop:: in @@ -458,7 +458,7 @@ In |OCaml|, we must cast any argument of the constructor dummy Even with those unsafe castings, you should never get error like ``segmentation fault``. In fact even if your program may seem -ill-typed to the |OCaml| type-checker, it can't go wrong : it comes +ill-typed to the |OCaml| type checker, it can't go wrong : it comes from a Coq well-typed terms, so for example inductive types will always have the correct number of arguments, etc. Of course, when launching manually some extracted function, you should apply it to arguments @@ -469,7 +469,7 @@ found in :cite:`Let02`. We have to say, though, that in most "realistic" programs, these problems do not occur. For example all the programs of Coq library are accepted by the |OCaml| -type-checker without any ``Obj.magic`` (see examples below). +type checker without any ``Obj.magic`` (see examples below). Some examples ------------- diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index c7df250672..e0babb6c4e 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -22,18 +22,18 @@ The new implementation is a drop-in replacement for the old one [#tabareau]_, hence most of the documentation still applies. The work is a complete rewrite of the previous implementation, based -on the type class infrastructure. It also improves on and generalizes +on the typeclass infrastructure. It also improves on and generalizes the previous implementation in several ways: + 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 + these constraints using typeclass resolution. As typeclass resolution is extensible using tactics, this allows users to define general ways to solve morphism constraints. + 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. + the other. This is done purely using tactics and typeclass search. + Rewriting under binders. It is possible to rewrite under binders in the new implementation, if one provides the proper morphisms. Again, most of the work is handled in the tactics. @@ -226,7 +226,7 @@ following command. 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 base name of the typeclass 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 @@ -309,7 +309,7 @@ following command. Proof. intros. rewrite empty_neutral. reflexivity. Qed. - The tables of relations and morphisms are managed by the type class + The tables of relations and morphisms are managed by the typeclass 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 @@ -350,7 +350,7 @@ prove that the argument of the morphism is defined. .. example:: Let ``eqO`` be ``fun x y => x = y /\ x <> 0`` (the - smallest PER over non zero elements). Division can be declared as a + smallest PER over nonzero 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``. @@ -446,7 +446,7 @@ First class setoids and morphisms The implementation is based on a first-class representation of -properties of relations and morphisms as type classes. That is, the +properties of relations and morphisms as typeclasses. That is, the various combinations of properties on relations and morphisms are represented as records and instances of theses classes are put in a hint database. For example, the declaration: @@ -472,9 +472,9 @@ is equivalent to an instance declaration: The declaration itself amounts to the definition of an object of the record type ``Coq.Classes.RelationClasses.Equivalence`` and a hint added to the ``typeclass_instances`` hint database. Morphism declarations are -also instances of a type class defined in ``Classes.Morphisms``. See the -documentation on type classes :ref:`typeclasses` -and the theories files in Classes for further explanations. +also instances of a typeclass defined in ``Classes.Morphisms``. See the +documentation on :ref:`typeclasses` and the theories files in Classes +for further explanations. One can inform the rewrite tactic about morphisms and relations just by using the typeclass mechanism to declare them using Instance and @@ -703,7 +703,7 @@ example of a mostly user-space extension of the algorithm. Constant unfolding ~~~~~~~~~~~~~~~~~~ -The resolution tactic is based on type classes and hence regards user- +The resolution tactic is based on typeclasses and hence regards user- defined constants as transparent by default. This may slow down the resolution due to a lot of unifications (all the declared ``Proper`` instances are tried at each node of the search tree). To speed it up, diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index f134022eb6..c0c4539564 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -352,7 +352,7 @@ We first give an example of coercion between atomic inductive types .. warning:: - Note that ``Check true=O`` would fail. This is "normal" behaviour of + Note that ``Check true=O`` would fail. This is "normal" behavior of coercions. To validate ``true=O``, the coercion is searched from ``nat`` to ``bool``. There is none. diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1ed3bffd2c..1e92d01125 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -11,7 +11,7 @@ Description of ``omega`` .. tacn:: omega :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, - i.e. for proving formulas made of equations and inequations over the + i.e. for proving formulas made of equations and inequalities 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. @@ -140,12 +140,12 @@ Technical data Overview of the tactic ~~~~~~~~~~~~~~~~~~~~~~ - * The goal is negated twice and the first negation is introduced as an hypothesis. - * Hypotheses are decomposed in simple equations or inequations. Multiple + * The goal is negated twice and the first negation is introduced as a hypothesis. + * Hypotheses are decomposed in simple equations or inequalities. Multiple goals may result from this phase. - * Equations and inequations over ``nat`` are translated over + * Equations and inequalities over ``nat`` are translated over ``Z``, multiple goals may result from the translation of subtraction. - * Equations and inequations are normalized. + * Equations and inequalities are normalized. * Goals are solved by the OMEGA decision procedure. * The script of the solution is replayed. @@ -156,17 +156,17 @@ 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, refer to the original paper for more information. - * Equations and inequations are normalized by division by the GCD of their + * Equations and inequalities 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 cuts the Euclidean space in half. - * Inequations are solved by projecting on the hyperspace + * Note that each inequality cuts the Euclidean space in half. + * Inequalities are solved by projecting on the hyperspace 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 + variable. Pairs of inequalities from different classes define a new edge in the projection. - * Redundant inequations are eliminated or merged in new + * Redundant inequalities are eliminated or merged in new equations that can be eliminated by the Banerjee test. * The last two steps are iterated until a contradiction is reached (success) or there is no more variable to eliminate (failure). diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 28fe68d78d..d6895f5fe5 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -18,7 +18,7 @@ program as in a regular functional programming language whilst using as rich a specification as desired and proving that the code meets the specification using the whole |Coq| proof apparatus. This is done using a technique originating from the “Predicate subtyping” mechanism of -PVS :cite:`Rushby98`, which generates type-checking conditions while typing a +PVS :cite:`Rushby98`, which generates type checking conditions while typing a term constrained to a particular type. Here we insert existential variables in the term, which must be filled with proofs to get a complete |Coq| term. |Program| replaces the |Program| tactic by Catherine @@ -72,8 +72,8 @@ operation (see :ref:`extendedpatternmatching`). This permits to get the proper equalities in the context of proof obligations inside clauses, without which reasoning is very limited. -+ Generation of inequalities. If a pattern intersects with a previous - one, an inequality is added in the context of the second branch. See ++ Generation of disequalities. If a pattern intersects with a previous + one, a disequality 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 :g:`∀ p, _ <> S (S p)`. + Coercion. If the object being matched is coercible to an inductive @@ -87,7 +87,7 @@ coercions. .. opt:: Program Cases This controls the special treatment of pattern-matching generating equalities - and inequalities when using |Program| (it is on by default). All + and disequalities when using |Program| (it is on by default). All pattern-matches and let-patterns are handled using the standard algorithm of |Coq| (see :ref:`extendedpatternmatching`) when this option is deactivated. @@ -104,7 +104,7 @@ Syntactic control over equalities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ To give more control over the generation of equalities, the -typechecker will fall back directly to |Coq|’s usual typing of dependent +type checker 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 @@ -175,7 +175,7 @@ Program Definition .. TODO refer to production in alias -See also: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` +.. seealso:: Sections :ref:`vernac-controlling-the-reduction-strategies`, :tacn:`unfold` .. _program_fixpoint: diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index d5c33dc1d4..8cb86e2267 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -19,7 +19,7 @@ field equations. What does this tactic do? ------------------------------ -``ring`` does associative-commutative rewriting in ring and semi-ring +``ring`` does associative-commutative rewriting in ring and semiring structures. Assume you have two binary functions :math:`\oplus` and :math:`\otimes` that are associative and commutative, with :math:`\oplus` distributive on :math:`\otimes`, and two constants 0 and 1 that are unities for @@ -37,7 +37,7 @@ 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 the ``ring`` tactic do? It normalizes polynomials over -any ring or semi-ring structure. The basic use of ``ring`` is to simplify ring +any ring or semiring 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. @@ -103,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 sides +(or semiring) 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. @@ -264,13 +264,13 @@ are the implementations of the ring operations, ``==`` is the equality of the coefficients, ``?+!`` is an implementation of this equality, and ``[x]`` is a notation for the image of ``x`` by the ring morphism. -Since |Z| is an initial ring (and |N| is an initial semi-ring), it can +Since |Z| is an initial ring (and |N| is an initial semiring), it can always be considered as a set of coefficients. There are basically three kinds of (semi-)rings: abstract rings to be used when operations are not effective. The set - of coefficients is |Z| (or |N| for semi-rings). + of coefficients is |Z| (or |N| for semirings). computational rings to be used when operations are effective. The @@ -505,10 +505,10 @@ 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 :math:`N = 0`. -Note that ``field`` also generates non-zero conditions for all the +Note that ``field`` also generates nonzero conditions for all the denominators it encounters in the reduction. In our example, it generates the condition :math:`x \neq 0`. These conditions appear as one subgoal -which is a conjunction if there are several denominators. Non-zero +which is a conjunction if there are several denominators. Nonzero conditions are always polynomial expressions. For example when reducing the expression :math:`1/(1 + 1/x)`, two side conditions are generated: :math:`x \neq 0` and :math:`x + 1 \neq 0`. Factorized expressions are broken since @@ -616,7 +616,7 @@ carrier set, an equality, and field operations: satisfies the field axioms. Semi-fields (fields 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 -fields and semi-fields is: +fields and semifields is: .. coqtop:: in @@ -670,7 +670,7 @@ specific modifier: completeness :n:`@term` allows the field tactic to prove automatically - that the image of non-zero coefficients are mapped to non-zero + that the image of nonzero coefficients are mapped to nonzero elements of the field. :n:`@term` is a proof of ``forall x y, [x] == [y] -> x ?=! y = true``, @@ -684,7 +684,7 @@ History of ring First Samuel Boutin designed the tactic ``ACDSimpl``. This tactic did lot of rewriting. But the proofs terms generated by rewriting were too big -for |Coq|’s type-checker. Let us see why: +for |Coq|’s type checker. Let us see why: .. coqtop:: all @@ -707,7 +707,7 @@ interleaving of computation and reasoning (see :ref:`discussion_reflection`). He 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 +number of :math:`\oplus` and :math:`\otimes` operations in the normalized terms. Type checking those terms requires some time because it makes a large use of the conversion rule, but memory requirements are much smaller. diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index b7946c6451..d26105b651 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -6,7 +6,7 @@ Type Classes ============ This chapter presents a quick reference of the commands related to type -classes. For an actual introduction to type classes, there is a +classes. For an actual introduction to typeclasses, there is a description of the system :cite:`sozeau08` and the literature on type classes in Haskell which also applies. @@ -76,7 +76,7 @@ for dealing with obligations. Binding classes --------------- -Once a type class is declared, one can use it in class binders: +Once a typeclass is declared, one can use it in class binders: .. coqtop:: all @@ -92,7 +92,7 @@ found, an error is raised: Fail Definition neqb' (A : Type) (x y : A) := negb (eqb x y). -The algorithm used to solve constraints is a variant of the eauto +The algorithm used to solve constraints is a variant of the :tacn:`eauto` tactic that does proof search with a set of lemmas (the instances). It will use local hypotheses as well as declared lemmas in the ``typeclass_instances`` database. Hence the example can also be @@ -103,13 +103,13 @@ written: Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y). However, the generalizing binders should be used instead as they have -particular support for type classes: +particular support for typeclasses: -+ They automatically set the maximally implicit status for type class ++ They automatically set the maximally implicit status for typeclass arguments, making derived functions as easy to use as class methods. In the example above, ``A`` and ``eqa`` should be set maximally implicit. + They support implicit quantification on partially applied type - classes (:ref:`implicit-generalization`). Any argument not given as part of a type class + classes (:ref:`implicit-generalization`). Any argument not given as part of a typeclass binder will be automatically generalized. + They also support implicit quantification on :ref:`superclasses`. @@ -148,7 +148,7 @@ database. Sections and contexts --------------------- -To ease the parametrization of developments by type classes, we provide a new +To ease the parametrization of developments by typeclasses, we provide a new way to introduce variables into section contexts, compatible with the implicit argument mechanism. The new command works similarly to the :cmd:`Variables` vernacular, except it accepts any binding context as argument. For example: @@ -271,7 +271,7 @@ Summary of the commands .. cmd:: Class @ident {? @binders} : {? @sort} := {? @ident} { {+; @ident :{? >} @term } } - The :cmd:`Class` command is used to declare a type class with parameters + The :cmd:`Class` command is used to declare a typeclass with parameters ``binders`` and fields the declared record fields. Variants: @@ -302,7 +302,7 @@ Variants: .. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } -The :cmd:`Instance` command is used to declare a type class instance named +The :cmd:`Instance` command is used to declare a typeclass instance named ``ident`` of the class :cmd:`Class` with parameters ``t1`` to ``tn`` and fields ``b1`` to ``bi``, where each field must be a declared field of the class. Missing fields must be filled in interactive proof mode. @@ -310,7 +310,7 @@ the class. Missing fields must be filled in interactive proof mode. An arbitrary context of ``binders`` can be put after the name of the instance and before the colon to declare a parameterized instance. An optional priority can be declared, 0 being the highest priority as for -auto hints. If the priority is not specified, it defaults to the number +:tacn:`auto` hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. .. cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term @@ -329,7 +329,7 @@ of non-dependent binders of the instance. .. cmdv:: Program Instance :name: Program Instance - Switches the type-checking to Program (chapter :ref:`programs`) and + Switches the type checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. .. cmdv:: Declare Instance @@ -342,12 +342,12 @@ of non-dependent binders of the instance. Besides the :cmd:`Class` and :cmd:`Instance` vernacular commands, there are a -few other commands related to type classes. +few other commands related to typeclasses. .. cmd:: Existing Instance {+ @ident} [| priority] This command adds an arbitrary list of constants whose type ends with - an applied type class to the instance database with an optional + an applied typeclass 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 equivalent to ``Hint Resolve ident : typeclass_instances``, except it @@ -367,11 +367,11 @@ few other commands related to type classes. + Contrary to :tacn:`eauto` and :tacn:`auto`, the resolution is done entirely in the new proof engine (as of Coq 8.6), meaning that backtracking is available among dependent subgoals, and shelving goals is supported. - typeclasses eauto is a multi-goal tactic. It analyses the dependencies + ``typeclasses eauto`` is a multi-goal tactic. It analyses the dependencies between subgoals to avoid backtracking on subgoals that are entirely independent. - + When called with no arguments, typeclasses eauto uses + + When called with no arguments, ``typeclasses eauto`` uses the ``typeclass_instances`` database by default (instead of core). Dependent subgoals are automatically shelved, and shelved goals can remain after resolution ends (following the behavior of Coq 8.5). @@ -379,13 +379,13 @@ few other commands related to type classes. .. note:: As of Coq 8.6, ``all:once (typeclasses eauto)`` faithfully mimicks what happens during typeclass resolution when it is called - during refinement/type-inference, except that *only* declared class + during refinement/type inference, except that *only* declared class subgoals are considered at the start of resolution during type inference, while ``all`` can select non-class subgoals as well. It might move to ``all:typeclasses eauto`` in future versions when the refinement engine will be able to backtrack. - + When called with specific databases (e.g. with), typeclasses eauto + + When called with specific databases (e.g. with), ``typeclasses eauto`` allows shelved goals to remain at any point during search and treat typeclass goals like any other. @@ -403,10 +403,10 @@ few other commands related to type classes. .. warning:: The semantics for the limit :n:`@num` - is different than for auto. By default, if no limit is given the - search is unbounded. Contrary to auto, introduction steps (intro) are + is different than for auto. By default, if no limit is given, the + search is unbounded. Contrary to :tacn:`auto`, introduction steps are counted, which might result in larger limits being necessary when - searching with typeclasses eauto than auto. + searching with ``typeclasses eauto`` than with :tacn:`auto`. .. cmdv:: typeclasses eauto with {+ @ident} @@ -417,11 +417,11 @@ few other commands related to type classes. .. tacn:: autoapply @term with @ident :name: autoapply - The tactic autoapply applies a term using the transparency information + The tactic ``autoapply`` applies a term using the transparency information of the hint database ident, and does *no* typeclass resolution. This can be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint database ``typeclass_instances``) to allow backtracking on the typeclass - subgoals created by the lemma application, rather than doing type class + subgoals created by the lemma application, rather than doing typeclass resolution locally at the hint application time. .. _TypeclassesTransparent: @@ -431,7 +431,7 @@ Typeclasses Transparent, Typclasses Opaque .. cmd:: Typeclasses Transparent {+ @ident} - This command defines makes the identifiers transparent during type class + This command defines makes the identifiers transparent during typeclass resolution. .. cmd:: Typeclasses Opaque {+ @ident} @@ -487,16 +487,18 @@ Options avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an introduction. - *Warning:* this can be expensive as it requires rebuilding hint - clauses dynamically, and does not benefit from the invertibility - status of the product introduction rule, resulting in potentially more - expensive proof-search (i.e. more useless backtracking). + .. warning:: + + This can be expensive as it requires rebuilding hint + clauses dynamically, and does not benefit from the invertibility + status of the product introduction rule, resulting in potentially more + expensive proof-search (i.e. more useless backtracking). .. opt:: Typeclass Resolution For Conversion This option (on by default) controls the use of typeclass resolution - when a unification problem cannot be solved during elaboration/type- + when a unification problem cannot be solved during elaboration/type inference. With this option on, when a unification fails, typeclass resolution is tried before launching unification once again. @@ -548,7 +550,7 @@ Typeclasses eauto `:=` .. cmd:: Typeclasses eauto := {? debug} {? {dfs | bfs}} depth - This command allows more global customization of the type class + This command allows more global customization of the typeclass resolution tactic. The semantics of the options are: + ``debug`` In debug mode, the trace of successfully applied tactics is diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index f245fab5ca..7e77dea457 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -36,7 +36,7 @@ error: Fail Definition selfid := identity (@identity). Indeed, the global level ``Top.1`` would have to be strictly smaller than -itself for this self-application to typecheck, as the type of +itself for this self-application to type check, as the type of :g:`(@identity)` is :g:`forall (A : Type@{Top.1}), A -> A` whose type is itself :g:`Type@{Top.1+1}`. diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index 2988b194e2..be0b5d5f12 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -60,7 +60,7 @@ the language ML. Automated theorem-proving was pioneered in the 1960’s by Davis and Putnam in propositional calculus. A complete mechanization (in the sense -of a semi-decision procedure) of classical first-order logic was +of a semidecision procedure) of classical first-order logic was proposed in 1965 by J.A. Robinson, with a single uniform inference rule called *resolution*. Resolution relies on solving equations in free algebras (i.e. term structures), using the *unification algorithm*. Many @@ -320,7 +320,7 @@ in March 2001, version 7.1 in September 2001, version 7.2 in January Jean-Christophe Filliâtre designed the architecture of the new system. He introduced a new representation for environments and wrote a new -kernel for type-checking terms. His approach was to use functional +kernel for type checking terms. His approach was to use functional data-structures in order to get more sharing, to prepare the addition of modules and also to get closer to a certified kernel. @@ -352,7 +352,7 @@ sensible. Jean-Christophe Filliâtre wrote ``coqdoc``, a documentation tool for |Coq| libraries usable from version 7.2. Bruno Barras improved the efficiency of the reduction algorithm and the -confidence level in the correctness of |Coq| critical type-checking +confidence level in the correctness of |Coq| critical type checking algorithm. Yves Bertot designed the ``SearchPattern`` and ``SearchRewrite`` tools @@ -506,7 +506,7 @@ Credits: version 8.1 Coq version 8.1 adds various new functionalities. Benjamin Grégoire implemented an alternative algorithm to check the -convertibility of terms in the |Coq| type-checker. This alternative +convertibility of terms in the |Coq| type checker. This alternative algorithm works by compilation to an efficient bytecode that is interpreted in an abstract machine similar to Xavier Leroy’s ZINC machine. Convertibility is performed by comparing the normal forms. This @@ -526,7 +526,7 @@ Claudio Sacerdoti Coen added new features to the module system. Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new, more efficient and more general simplification algorithm for rings and -semi-rings. +semirings. Laurent Théry and Bruno Barras developed a new, significantly more efficient simplification algorithm for fields. @@ -586,11 +586,11 @@ Coq version 8.2 adds new features, new libraries and improves on many various aspects. Regarding the language of |Coq|, the main novelty is the introduction by -Matthieu Sozeau of a package of commands providing Haskell-style type -classes. Type classes, that come with a few convenient features such as +Matthieu Sozeau of a package of commands providing Haskell-style typeclasses. +Typeclasses, which come with a few convenient features such as type-based resolution of implicit arguments, play a new landmark role in the architecture of |Coq| with respect to automation. For -instance, thanks to type classes support, Matthieu Sozeau could +instance, thanks to typeclass support, Matthieu Sozeau could implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. @@ -648,7 +648,7 @@ maintenance and coqdoc support, Vincent Siles contributed extensions of the Scheme command and of injection. Bruno Barras implemented the `coqchk` tool: this is a stand-alone -type-checker that can be used to certify .vo files. Especially, as this +type checker that can be used to certify .vo files. Especially, as this verifier runs in a separate process, it is granted not to be “hijacked” by virtually malicious extensions added to |Coq|. @@ -712,7 +712,7 @@ The new tactic nsatz is due to Loïc Pottier. It works by computing Gröbner bases. Regarding the existing tactics, various improvements have been done by Matthieu Sozeau, Hugo Herbelin and Pierre Letouzey. -Matthieu Sozeau extended and refined the type classes and Program +Matthieu Sozeau extended and refined the typeclasses and Program features (the Russell language). Pierre Letouzey maintained and improved the extraction mechanism. Bruno Barras and Élie Soubiran maintained the Coq checker, Julien Forest maintained the Function mechanism for @@ -810,7 +810,7 @@ Regarding the high-level specification language, Pierre Boutillier introduced the ability to give implicit arguments to anonymous functions, Hugo Herbelin introduced the ability to define notations with several binders (e.g. ``exists x y z, P``), Matthieu Sozeau made the -type classes inference mechanism more robust and predictable, Enrico +typeclass inference mechanism more robust and predictable, Enrico Tassi introduced a command Arguments that generalizes Implicit Arguments and Arguments Scope for assigning various properties to arguments of constants. Various improvements in the type inference algorithm were @@ -831,7 +831,7 @@ vm\_compute. Bug fixes and miscellaneous improvements of the tactic language came from Hugo Herbelin, Pierre Letouzey and Matthieu Sozeau. Regarding decision tactics, Loïc Pottier maintained nsatz, moving in -particular to a type-class based reification of goals while Frédéric +particular to a typeclass based reification of goals while Frédéric Besson maintained Micromega, adding in particular support for division. Regarding vernacular commands, Stéphane Glondu provided new commands to @@ -1074,7 +1074,7 @@ over 100 contributions integrated. The main user visible changes are: document. - More access to the proof engine features from Ltac: goal management - primitives, range selectors and a typeclasses eauto engine handling + primitives, range selectors and a ``typeclasses eauto`` engine handling multiple goals and multiple successes, by Cyprien Mangin, Matthieu Sozeau and Arnaud Spiwack. @@ -1234,7 +1234,7 @@ The efficiency of the whole system has been significantly improved thanks to contributions from Pierre-Marie Pédrot, Maxime Dénès and Matthieu Sozeau and performance issue tracking by Jason Gross and Paul Steckler. -Thomas Sibut-Pinote and Hugo Herbelin added support for side effects hooks in +Thomas Sibut-Pinote and Hugo Herbelin added support for side effect hooks in cbv, cbn and simpl. The side effects are provided via a plugin available at https://github.com/herbelin/reduction-effects/. @@ -1292,7 +1292,7 @@ integration of new features, with an important focus given to compatibility and performance issues, resulting in a hopefully more robust release than |Coq| 8.6 while maintaining compatibility. -|Coq| Enhancement Proposals (CEPs for short) and open pull-requests discussions +|Coq| Enhancement Proposals (CEPs for short) and open pull request discussions were used to discuss publicly the new features. The |Coq| consortium, an organization directed towards users and supporters of the diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 1a610396e5..b57e4b209c 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -7,8 +7,8 @@ Introduction This document is the Reference Manual of the |Coq| proof assistant. To start using Coq, it is advised to first read a tutorial. Links to several tutorials can be found at -https://coq.inria.fr/documentation (see also -https://github.com/coq/coq/wiki#coq-tutorials). +https://coq.inria.fr/documentation and +https://github.com/coq/coq/wiki#coq-tutorials The |Coq| system is designed to develop mathematical proofs, and especially to write formal specifications, programs and to verify that @@ -20,7 +20,7 @@ properties and proofs are formalized in the same language called *Calculus of Inductive Constructions*, that is a :math:`\lambda`-calculus with a rich type system. All logical judgments in |Coq| are typing judgments. The very heart of the |Coq| system is the -type-checking algorithm that checks the correctness of proofs, in other +type checking algorithm that checks the correctness of proofs, in other words that checks that a program complies to its specification. |Coq| also provides an interactive proof assistant to build proofs using specific programs called *tactics*. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index b0ba2bcc31..3d3a1b11b1 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -96,8 +96,9 @@ constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of constraints must remain acyclic. Typing expressions that violate the acyclicity of the graph of constraints -results in a Universe inconsistency error (see also Section -:ref:`printing-universes`). +results in a Universe inconsistency error. + +.. seealso:: Section :ref:`printing-universes`. .. _Terms: @@ -1252,7 +1253,7 @@ In this expression, if :math:`m` eventually happens to evaluate to and it will reduce to :math:`f_i` where the :math:`x_{i1} …x_{ip_i}` are replaced by the :math:`u_1 … u_{p_i}` according to the ι-reduction. -Actually, for type-checking a :math:`\Match…\with…\endkw` expression we also need +Actually, for type checking a :math:`\Match…\with…\endkw` expression we also need to know the predicate P to be proved by case analysis. In the general case where :math:`I` is an inductively defined :math:`n`-ary relation, :math:`P` is a predicate over :math:`n+1` arguments: the :math:`n` first ones correspond to the arguments of :math:`I` @@ -1398,7 +1399,7 @@ arguments of this constructor have type :math:`\Prop`. In that case, there is a canonical way to interpret the informative extraction on an object in that type, such that the elimination on any sort :math:`s` is legal. Typical examples are the conjunction of non-informative propositions and the -equality. If there is an hypothesis :math:`h:a=b` in the local context, it can +equality. If there is a hypothesis :math:`h:a=b` in the local context, it can be used for rewriting not only in logical propositions but also in any type. @@ -1821,7 +1822,7 @@ definitions can be found in :cite:`Gimenez95b,Gim98,GimCas05`. The Calculus of Inductive Constructions with impredicative Set ----------------------------------------------------------------- -|Coq| can be used as a type-checker for the Calculus of Inductive +|Coq| can be used as a type checker for the Calculus of Inductive Constructions with an impredicative sort :math:`\Set` by using the compiler option ``-impredicative-set``. For example, using the ordinary `coqtop` command, the following is rejected, @@ -1832,7 +1833,7 @@ command, the following is rejected, Fail Definition id: Set := forall X:Set,X->X. -while it will type-check, if one uses instead the `coqtop` +while it will type check, if one uses instead the `coqtop` ``-impredicative-set`` option.. The major change in the theory concerns the rule for product formation diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 7dd0a6e383..0fbe7ac70b 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -212,7 +212,7 @@ During the definition of the one-constructor inductive definition, all the errors of inductive definitions, as described in Section :ref:`gallina-inductive-definitions`, may also occur. -**See also** Coercions and records in Section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. +.. seealso:: Coercions and records in section :ref:`coercions-classes-as-records` of the chapter devoted to coercions. .. _primitive_projections: @@ -229,7 +229,7 @@ term constructor `r.(p)` representing a primitive projection `p` applied to a record object `r` (i.e., primitive projections are always applied). Even if the record type has parameters, these do not appear at applications of the projection, considerably reducing the sizes of -terms when manipulating parameterized records and typechecking time. +terms when manipulating parameterized records and type checking time. On the user level, primitive projections can be used as a replacement for the usual defined ones, although there are a few notable differences. @@ -328,7 +328,7 @@ into a sequence of match on simple patterns. Especially, a construction defined using the extended match is generally printed under its expanded form (see :opt:`Printing Matching`). -See also: :ref:`extendedpatternmatching`. +.. seealso:: :ref:`extendedpatternmatching`. .. _if-then-else: @@ -711,7 +711,7 @@ terminating functions. `functional inversion` will not be available for the function. -See also: :ref:`functional-scheme` and :tacn:`function induction` +.. seealso:: :ref:`functional-scheme` and :tacn:`function induction` Depending on the ``{…}`` annotation, different definition mechanisms are used by ``Function``. A more precise description is given below. @@ -1260,7 +1260,7 @@ identifiers qualid, i.e. as list of identifiers separated by dots (see |Coq| library ``Arith`` is named ``Coq.Arith.Mult``. The identifier that starts the name of a library is called a *library root*. All library files of the standard library of |Coq| have the reserved root |Coq| but library -file names based on other roots can be obtained by using |Coq| commands +filenames based on other roots can be obtained by using |Coq| commands (coqc, coqtop, coqdep, …) options ``-Q`` or ``-R`` (see :ref:`command-line-options`). Also, when an interactive |Coq| session starts, a library of root ``Top`` is started, unless option ``-top`` or ``-notop`` is set (see :ref:`command-line-options`). @@ -1294,7 +1294,7 @@ short name (or even same partially qualified names as soon as the full names are different). Notice that the notion of absolute, partially qualified and short -names also applies to library file names. +names also applies to library filenames. **Visibility** @@ -1328,7 +1328,7 @@ accessible, absolute names can never be hidden. Locate nat. -See also: Commands :cmd:`Locate` and :cmd:`Locate Library`. +.. seealso:: Commands :cmd:`Locate` and :cmd:`Locate Library`. .. _libraries-and-filesystem: @@ -1514,7 +1514,8 @@ says that the implicit argument is maximally inserted. Each implicit argument can be declared to have to be inserted maximally or non maximally. This can be governed argument per argument by the command :cmd:`Arguments (implicits)` or globally by the :opt:`Maximal Implicit Insertion` option. -See also :ref:`displaying-implicit-args`. + +.. seealso:: :ref:`displaying-implicit-args`. Casual use of implicit arguments @@ -1887,7 +1888,7 @@ arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can be deactivated by turning this option off. -See also: :opt:`Printing All`. +.. seealso:: :opt:`Printing All`. Interaction with subtyping ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1937,7 +1938,7 @@ in :ref:`canonicalstructures`; here only a simple example is given. Assume that :token:`qualid` denotes an object ``(Build_struct`` |c_1| … |c_n| ``)`` in the structure :g:`struct` of which the fields are |x_1|, …, |x_n|. Then, each time an equation of the form ``(``\ |x_i| ``_)`` |eq_beta_delta_iota_zeta| |c_i| has to be - solved during the type-checking process, :token:`qualid` is used as a solution. + solved during the type checking process, :token:`qualid` is used as a solution. Otherwise said, :token:`qualid` is canonically used to extend the field |c_i| into a complete structure built on |c_i|. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index da5cd00d72..075235a8e2 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -920,7 +920,7 @@ Parametrized inductive types When this option is set (it is off by default), inductive definitions are abstracted over their parameters - before typechecking constructors, allowing to write: + before type checking constructors, allowing to write: .. coqtop:: all undo @@ -1124,7 +1124,7 @@ constructions. arguments, and this choice influences the reduction of the fixpoint. Hence an explicit annotation must be used if the leftmost decreasing argument is not the desired one. Writing explicit annotations can also - speed up type-checking of large mutual fixpoints. + speed up type checking of large mutual fixpoints. + In order to keep the strong normalization property, the fixed point reduction will only be performed when the argument in position of the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 4e42bddee2..9498f37c7e 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -104,8 +104,12 @@ The following command-line options are recognized by the commands ``coqc`` and ``coqtop``, unless stated otherwise: :-I *directory*, -include *directory*: Add physical path *directory* - to the OCaml loadpath. See also: :ref:`names-of-libraries` and the - command Declare ML Module Section :ref:`compiled-files`. + to the OCaml loadpath. + + .. seealso:: + + :ref:`names-of-libraries` and the + command Declare ML Module Section :ref:`compiled-files`. :-Q *directory* dirpath: Add physical path *directory* to the list of directories where |Coq| looks for a file and bind it to the logical directory *dirpath*. The subdirectory structure of *directory* is @@ -115,14 +119,17 @@ and ``coqtop``, unless stated otherwise: an :n:`@ident` are taken into account. Conversely, the underlying file systems or operating systems may be more restrictive than |Coq|. While Linux’s ext4 file system supports any |Coq| recursive - layout (within the limit of 255 bytes per file name), the default on + layout (within the limit of 255 bytes per filename), the default on NTFS (Windows) or HFS+ (MacOS X) file systems is on the contrary to disallow two files differing only in the case in the same directory. - See also: Section :ref:`names-of-libraries`. + + .. seealso:: Section :ref:`names-of-libraries`. :-R *directory* dirpath: Do as -Q *directory* dirpath but make the subdirectory structure of *directory* recursively visible so that the recursive contents of physical *directory* is available from |Coq| using - short or partially qualified names. See also: Section :ref:`names-of-libraries`. + short or partially qualified names. + + .. seealso:: Section :ref:`names-of-libraries`. :-top dirpath: Set the toplevel module name to dirpath instead of Top. Not valid for `coqc` as the toplevel module name is inferred from the name of the output file. @@ -168,11 +175,16 @@ and ``coqtop``, unless stated otherwise: :-emacs, -ide-slave: Start a special toplevel to communicate with a specific IDE. :-impredicative-set: Change the logical theory of |Coq| by declaring the - sort Set impredicative. Warning: This is known to be inconsistent with some - standard axioms of classical mathematics such as the functional - axiom of choice or the principle of description. -:-type-in-type: Collapse the universe hierarchy of |Coq|. Warning: This makes the logic - inconsistent. + sort Set impredicative. + + .. warning:: + + This is known to be inconsistent with some + standard axioms of classical mathematics such as the functional + axiom of choice or the principle of description. +:-type-in-type: Collapse the universe hierarchy of |Coq|. + + .. warning:: This makes the logic inconsistent. :-mangle-names *ident*: Experimental: Do not depend on this option. Replace Coq's auto-generated name scheme with names of the form *ident0*, *ident1*, etc. The command ``Set Mangle Names`` turns the behavior on in a document, @@ -208,7 +220,7 @@ The ``coqchk`` command takes a list of library paths as argument, described eith by their logical name or by their physical filename, hich must end in ``.vo``. The corresponding compiled libraries (``.vo`` files) are searched in the path, recursively processing the libraries they depend on. The content of all these -libraries is then type-checked. The effect of ``coqchk`` is only to return with +libraries is then type checked. The effect of ``coqchk`` is only to return with normal exit code in case of success, and with positive exit code if an error has been found. Error messages are not deemed to help the user understand what is wrong. In the current version, it does not modify the compiled libraries to mark @@ -248,15 +260,15 @@ the following: assuming that ``coqchk`` is called with argument ``M``, option ``-norec N``, and ``-admit A``. Let us write :math:`\overline{S}` for the set of reflexive transitive dependencies of set :math:`S`. Then: -+ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type-checked before being added ++ Modules :math:`C = \overline{M} \backslash \overline{A} \cup M \cup N` are loaded and type checked before being added to the context. + And :math:`M \cup N \backslash C` is the set of modules that are loaded and added to the - context without type-checking. Basic integrity checks (checksums) are + context without type checking. Basic integrity checks (checksums) are nonetheless performed. As a rule of thumb, -admit can be used to tell Coq that some libraries have already been checked. So ``coqchk A B`` can be split in ``coqchk A`` && -``coqchk B -admit A`` without type-checking any definition twice. Of +``coqchk B -admit A`` without type checking any definition twice. Of course, the latter is slightly slower since it makes more disk access. It is also less secure since an attacker might have replaced the compiled library ``A`` after it has been read by the first command, but diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index f7f442092f..bc6a074a27 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -12,7 +12,7 @@ file, executing corresponding commands or undoing them respectively. |CoqIDE| is run by typing the command `coqide` on the command line. Without argument, the main screen is displayed with an “unnamed -buffer”, and with a file name as argument, another buffer displaying +buffer”, and with a filename as argument, another buffer displaying the contents of that file. Additionally, `coqide` accepts the same options as `coqtop`, given in :ref:`thecoqcommands`, the ones having obviously no meaning for |CoqIDE| being ignored. @@ -92,7 +92,7 @@ buffers (left and right arrows); an "information" button; and a "gears" button. The "information" button is described in Section :ref:`try-tactics-automatically`. -The "gears" button submits proof terms to the |Coq| kernel for type-checking. +The "gears" button submits proof terms to the |Coq| kernel for type checking. When |Coq| uses asynchronous processing (see Chapter :ref:`asynchronousandparallelproofprocessing`), proofs may have been completed without kernel-checking of generated proof terms. The presence of unchecked proof terms is indicated by ``Qed`` statements that diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index e779515a00..218a19c2e5 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -43,7 +43,7 @@ Building a |Coq| project with coq_makefile The majority of |Coq| projects are very similar: a collection of ``.v`` files and eventually some ``.ml`` ones (a |Coq| plugin). The main piece of metadata needed in order to build the project are the command line -options to ``coqc`` (e.g. ``-R``, ``-I``, see also: Section +options to ``coqc`` (e.g. ``-R``, ``-I``, see also: section :ref:`command-line-options`). Collecting the list of files and options is the job of the ``_CoqProject`` file. @@ -107,7 +107,7 @@ decide how to build them. In particular: The use of ``.mlpack`` files has to be preferred over ``.mllib`` files, since it results in a “packed” plugin: All auxiliary modules (as -``Baz`` and ``Bazaux``) are hidden inside the plugin’s “name space” +``Baz`` and ``Bazaux``) are hidden inside the plugin’s "namespace" (``Qux_plugin``). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names. @@ -773,7 +773,7 @@ Command line options preamble, right before ``\begin{document}`` (meaningless with ``-html``). :--vernac-file file,--tex-file file: Considers the file ‘file’ respectively as a ``.v`` (or ``.g``) file or a ``.tex`` file. - :--files-from file: Read file names to be processed from the file ‘file’ as if + :--files-from file: Read filenames to be processed from the file ‘file’ as if they were given on the command line. Useful for program sources split up into several directories. :-q, --quiet: Be quiet. Do not print anything except errors. diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 225df8d54c..344134b6f9 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -21,7 +21,7 @@ applied to the abstracted instance and after simplification of the equalities we get the expected goals. The abstracting tactic is called generalize_eqs and it takes as -argument an hypothesis to generalize. It uses the JMeq datatype +argument a hypothesis to generalize. It uses the JMeq datatype defined in Coq.Logic.JMeq, hence we need to require it before. For example, revisiting the first example of the inversion documentation: diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0310dbead5..7608ea7245 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -556,9 +556,9 @@ Failing The number is the failure level. If no level is specified, it defaults to 0. The level is used by :tacn:`try`, :tacn:`repeat`, :tacn:`match goal` and the branching tacticals. If 0, it makes :tacn:`match goal` consider the next clause - (backtracking). If non zero, the current :tacn:`match goal` block, :tacn:`try`, + (backtracking). If nonzero, the current :tacn:`match goal` block, :tacn:`try`, :tacn:`repeat`, or branching command is aborted and the level is decremented. In - the case of :n:`+`, a non-zero level skips the first backtrack point, even if + the case of :n:`+`, a nonzero level skips the first backtrack point, even if the call to :n:`fail @num` is not enclosed in a :n:`+` command, respecting the algebraic identity. @@ -863,7 +863,7 @@ We can perform pattern matching on goals using the following expression: :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i = 1, ..., m\ :sub:`1` is - matched (non-linear first-order unification) by an hypothesis of the + matched (non-linear first-order unification) by a hypothesis of the goal and if :n:`cpattern_1` is matched by the conclusion of the goal, then :n:`@expr__1` is evaluated to :n:`v__1` by substituting the pattern matching to the metavariables and the real hypothesis names @@ -989,7 +989,7 @@ Manipulating untyped terms An untyped term, in |Ltac|, can contain references to hypotheses or to |Ltac| variables containing typed or untyped terms. An untyped term can be - type-checked using the function type_term whose argument is parsed as an + type checked using the function type_term whose argument is parsed as an untyped term and returns a well-typed term which can be used in tactics. Untyped terms built using :n:`uconstr :` can also be used as arguments to the diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index fe2124502a..b1e769c571 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -84,7 +84,7 @@ list of assertion commands is given in :ref:`Assertions`. The command :name: Defined Same as :cmd:`Qed` but the proof is then declared transparent, which means - that its content can be explicitly used for type-checking and that it can be + that its content can be explicitly used for type checking and that it can be unfolded in conversion tactics (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`). diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index be30f69704..7c3ea1a28c 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -37,7 +37,7 @@ bookkeeping is performed on the conclusion of the goal, using for that purpose a couple of syntactic constructions behaving similar to tacticals (and often named as such in this chapter). The ``:`` tactical moves hypotheses from the context to the conclusion, while ``=>`` moves hypotheses from the -conclusion to the context, and ``in`` moves back and forth an hypothesis from the +conclusion to the context, and ``in`` moves back and forth a hypothesis from the context to the conclusion for the time of applying an action to it. While naming hypotheses is commonly done by means of an ``as`` clause in the @@ -303,7 +303,7 @@ the ``if`` construct to all binary data types; compare The latter appears to be marginally shorter, but it is quite ambiguous, and indeed often requires an explicit annotation -``(term : {_} + {_})`` to type-check, which evens the character count. +``(term : {_} + {_})`` to type check, which evens the character count. Therefore, |SSR| restricts by default the condition of a plain if construct to the standard ``bool`` type; this avoids spurious type @@ -385,7 +385,7 @@ expressions such as Unfortunately, such higher-order expressions are quite frequent in representation functions, especially those which use |Coq|'s -``Structures`` to emulate Haskell type classes. +``Structures`` to emulate Haskell typeclasses. Therefore, |SSR| provides a variant of |Coq|’s implicit argument declaration, which causes |Coq| to fill in some implicit parameters at @@ -1285,7 +1285,7 @@ catch the appropriate number of wildcards to be inserted. Note that this use of the refine tactic implies that the tactic tries to match the goal up to expansion of constants and evaluation of subterms. -|SSR|’s apply has a special behaviour on goals containing +|SSR|’s apply has a special behavior on goals containing existential metavariables of sort Prop. .. example:: @@ -2064,26 +2064,27 @@ is equivalent to: (see section :ref:`discharge_ssr` for the documentation of the apply: combination). -Warning The list of tactics, possibly chained by semicolons, that -follows a by keyword is considered as a parenthesized block applied to -the current goal. Hence for example if the tactic: +.. warning:: -.. coqtop:: in + The list of tactics (possibly chained by semicolons) that + follows the ``by`` keyword is considered to be a parenthesized block applied to + the current goal. Hence for example if the tactic: - by rewrite my_lemma1. + .. coqtop:: in -succeeds, then the tactic: + by rewrite my_lemma1. -.. coqtop:: in + succeeds, then the tactic: - by rewrite my_lemma1; apply my_lemma2. + .. coqtop:: in -usually fails since it is equivalent to: + by rewrite my_lemma1; apply my_lemma2. -.. coqtop:: in + usually fails since it is equivalent to: - by (rewrite my_lemma1; apply my_lemma2). + .. coqtop:: in + by (rewrite my_lemma1; apply my_lemma2). .. _selectors_ssr: @@ -2653,11 +2654,11 @@ Last, notice that the use of intro patterns for abstract constants is orthogonal to the transparent flag ``@`` for have. -The have tactic and type classes resolution +The have tactic and typeclass resolution ``````````````````````````````````````````` -Since |SSR| 1.5 the have tactic behaves as follows with respect to -type classes inference. +Since |SSR| 1.5 the ``have`` tactic behaves as follows with respect to +typeclass inference. .. coqtop:: none @@ -2699,7 +2700,7 @@ type classes inference. .. opt:: SsrHave NoTCResolution - This option restores the behavior of |SSR| 1.4 and below (never resolve type classes). + This option restores the behavior of |SSR| 1.4 and below (never resolve typeclasses). Variants: the suff and wlog tactics ``````````````````````````````````` @@ -3009,6 +3010,15 @@ An :token:`r_item` can be: is equivalent to: ``change term1 with term2.`` If ``term2`` is a single constant and ``term1`` head symbol is not ``term2``, then the head symbol of ``term1`` is repeatedly unfolded until ``term2`` appears. ++ A :token:`term`, which can be: + + A term whose type has the form: + ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where + ``eq`` is the Leibniz equality or a registered setoid + equality. + + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above. + The tactic: ``rewrite r_prefix (t1 ,…,tn ).`` + is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].`` + + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``. .. example:: @@ -3026,9 +3036,10 @@ An :token:`r_item` can be: Lemma test x : ddouble x = 4 * x. rewrite [ddouble _]/double. - *Warning* The |SSR| - terms containing holes are *not* typed as abstractions in this - context. Hence the following script fails. + .. warning:: + + The |SSR| terms containing holes are *not* typed as + abstractions in this context. Hence the following script fails. .. coqtop:: none @@ -3050,17 +3061,6 @@ An :token:`r_item` can be: rewrite -[f y x]/(y + _). -+ A :token:`term`, which can be: - - + A term whose type has the form: - ``forall (x1 : A1 )…(xn : An ), eq term1 term2`` where - ``eq`` is the Leibniz equality or a registered setoid - equality. - + A list of terms ``(t1 ,…,tn)``, each ``ti`` having a type above. - The tactic: ``rewrite r_prefix (t1 ,…,tn ).`` - is equivalent to: ``do [rewrite r_prefix t1 | … | rewrite r_prefix tn ].`` - + An anonymous rewrite lemma ``(_ : term)``, where term has a type as above. tactic: ``rewrite (_ : term)`` is in fact synonym of: ``cutrewrite (term).``. - Remarks and examples ~~~~~~~~~~~~~~~~~~~~ @@ -3701,20 +3701,22 @@ Note that ``nosimpl bar`` is simply notation for a term that reduces to ``bar``; hence ``unfold foo`` will replace ``foo`` by ``bar``, and ``fold foo`` will replace ``bar`` by ``foo``. -*Warning* The ``nosimpl`` trick only works if no reduction is apparent in -``t``; in particular, the declaration: +.. warning:: -.. coqtop:: in + The ``nosimpl`` trick only works if no reduction is apparent in + ``t``; in particular, the declaration: - Definition foo x := nosimpl (bar x). + .. coqtop:: in -will usually not work. Anyway, the common practice is to tag only the -function, and to use the following definition, which blocks the -reduction as expected: + Definition foo x := nosimpl (bar x). -.. coqtop:: in + will usually not work. Anyway, the common practice is to tag only the + function, and to use the following definition, which blocks the + reduction as expected: + + .. coqtop:: in - Definition foo x := nosimpl bar x. + Definition foo x := nosimpl bar x. A standard example making this technique shine is the case of arithmetic operations. We define for instance: @@ -4757,7 +4759,7 @@ equivalence property has been defined. Lemma andE (b1 b2 : bool) : (b1 /\ b2) <-> (b1 && b2). -Let us compare the respective behaviours of ``andE`` and ``andP``. +Let us compare the respective behaviors of ``andE`` and ``andP``. .. example:: @@ -4870,7 +4872,7 @@ The term , called the *view lemma* can be: Let ``top`` be the top assumption in the goal. -There are three steps in the behaviour of an assumption view tactic: +There are three steps in the behavior of an assumption view tactic: + It first introduces ``top``. + If the type of :token:`term` is neither a double implication nor an diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index fcb52cf275..854c3c919c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -186,7 +186,7 @@ Applying theorems .. tacn:: assumption :name: assumption - This tactic looks in the local context for an hypothesis whose type is + This tactic looks in the local context for a hypothesis whose type is convertible to the goal. If it is the case, the subgoal is proved. Otherwise, it fails. @@ -255,13 +255,13 @@ Applying theorems .. tacv:: notypeclasses refine @term :name: notypeclasses refine - This tactic behaves like :tacn:`refine` except it performs typechecking without + This tactic behaves like :tacn:`refine` except it performs type checking without resolution of typeclasses. .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs typechecking + This tactic behaves like :tacn:`simple refine` except it performs type checking without resolution of typeclasses. .. tacn:: apply @term @@ -797,7 +797,7 @@ Managing the local context Introduction via :n:`({+& p})` is a shortcut for introduction via :n:`(p,( ... ,( ..., p ) ... ))`; it expects the hypothesis to be a sequence of right-associative binary inductive constructors such as :g:`conj` or - :g:`ex_intro`; for instance, an hypothesis with type + :g:`ex_intro`; for instance, a hypothesis with type :g:`A /\(exists x, B /\ C /\ D)` can be introduced via pattern :n:`(a & x & b & c & d)`; @@ -1384,7 +1384,7 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. :name: contradiction This tactic applies to any goal. The contradiction tactic attempts to - find in the current context (after all intros) an hypothesis that is + find in the current context (after all intros) a hypothesis that is equivalent to an empty inductive type (e.g. :g:`False`), to the negation of a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory hypotheses. @@ -1440,7 +1440,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) anymore dependent in the goal after application of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). - If :token:`ident` is an hypothesis of the context, and :token:`ident` + If :token:`ident` is a hypothesis of the context, and :token:`ident` is not anymore dependent in the goal after application of :tacn:`destruct`, it is erased (to avoid erasure, use parentheses, as in :n:`destruct (@ident)`). @@ -1477,7 +1477,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) enough names, :tacn:`destruct` invents names for the remaining variables to introduce. More generally, the :n:`pij` can be any introduction pattern (see :tacn:`intros`). This provides a concise notation for - chaining destruction of an hypothesis. + chaining destruction of a hypothesis. .. tacv:: destruct @term eqn:@naming_intro_pattern :name: destruct ... eqn: @@ -1586,7 +1586,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) For simple induction on a numeral, use syntax induction (num) (not very interesting anyway). - + In case term is an hypothesis :n:`@ident` of the context, and :n:`@ident` + + In case term is a hypothesis :n:`@ident` of the context, and :n:`@ident` is not anymore dependent in the goal after application of :n:`induction`, it is erased (to avoid erasure, use parentheses, as in :n:`induction (@ident)`). @@ -1878,9 +1878,7 @@ and an explanation of the underlying technique. :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` for details. -See also: :ref:`advanced-recursive-functions` - :ref:`functional-scheme` - :tacn:`inversion` +.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` .. exn:: Cannot find induction information on @qualid. .. exn:: Not the right number of induction arguments. @@ -2041,7 +2039,7 @@ See also: :ref:`advanced-recursive-functions` the number of equalities newly generated. If it is smaller, fresh names are automatically generated to adjust the list of :n:`@intro_pattern` to the number of new equalities. The original equality is erased if it - corresponds to an hypothesis. + corresponds to a hypothesis. .. opt:: Structural Injection @@ -2312,8 +2310,8 @@ See also: :ref:`advanced-recursive-functions` As H occurs in the goal, we may want to reason by cases on its structure and so, we would like inversion tactics to substitute H by - the corresponding @term in constructor form. Neither Inversion nor - Inversion_clear make such a substitution. To have such a behavior we + the corresponding @term in constructor form. Neither :tacn:`inversion` nor + :n:`inversion_clear` do such a substitution. To have such a behavior we use the dependent inversion tactics: .. coqtop:: all @@ -3205,7 +3203,7 @@ the :tacn:`auto` and :tacn:`trivial` tactics: .. opt:: Info Trivial .. opt:: Debug Trivial -See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` +.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: eauto :name: eauto @@ -3236,7 +3234,7 @@ Note that ``ex_intro`` should be declared as a hint. .. opt:: Info Eauto .. opt:: Debug Eauto -See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` +.. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` .. tacn:: autounfold with {+ @ident} @@ -3293,10 +3291,10 @@ command. Performs all the rewriting in the clause :n:`@clause`. The clause argument must not contain any ``type of`` nor ``value of``. -See also: :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by -:tacn:`autorewrite`. +.. seealso: -See also: :tacn:`autorewrite` for examples showing the use of this tactic. + :ref:`Hint-Rewrite <hintrewrite>` for feeding the database of lemmas used by + :tacn:`autorewrite` and :tacn:`autorewrite` for examples showing the use of this tactic. .. tacn:: easy :name: easy @@ -3592,7 +3590,7 @@ At Coq startup, only the core database is nonempty and can be used. :zarith: contains lemmas about binary signed integers from the directories theories/ZArith. When required, the module Omega also extends the database zarith with a high-cost hint that calls ``omega`` on equations - and inequalities in nat or Z. + and inequalities in ``nat`` or ``Z``. :bool: contains lemmas about booleans, mostly from directory theories/Bool. @@ -3602,7 +3600,7 @@ At Coq startup, only the core database is nonempty and can be used. :sets: contains lemmas about sets and relations from the directories Sets and Relations. -:typeclass_instances: contains all the type class instances declared in the +:typeclass_instances: contains all the typeclass instances declared in the environment, including those used for ``setoid_rewrite``, from the Classes directory. @@ -3731,7 +3729,7 @@ Setting implicit automation tactics In this case the tactic command typed by the user is equivalent to ``tactic``:sub:`1` ``;tactic``. - See also: ``Proof.`` in :ref:`proof-editing-mode`. + .. seealso:: ``Proof`` in :ref:`proof-editing-mode`. .. cmdv:: Proof with tactic using {+ @ident} @@ -4205,8 +4203,9 @@ available after a ``Require Import FunInd``. .. tacv:: functional inversion @num - This does the same thing as intros until num thenfunctional inversion ident - where ident is the identifier for the last introduced hypothesis. + This does the same thing as :n:`intros until @num` folowed by + :n:`functional inversion @ident` where :token:`ident` is the + identifier for the last introduced hypothesis. .. tacv:: functional inversion ident qualid .. tacv:: functional inversion num qualid @@ -4313,7 +4312,7 @@ and :g:`Z` of binary integers. This tactic must be loaded by the command :name: ring_simplify The :n:`ring` tactic solves equations upon polynomial expressions of a ring -(or semi-ring) structure. It proceeds by normalizing both hand sides +(or semiring) structure. It proceeds by normalizing both hand sides of the equation (w.r.t. associativity, commutativity and distributivity, constant propagation) and comparing syntactically the results. @@ -4366,8 +4365,10 @@ printed with the Print Fields command. intros; field. -See also: file plugins/setoid_ring/RealField.v for an example of instantiation, -theory theories/Reals for many examples of use of field. +.. seealso:: + + File plugins/setoid_ring/RealField.v for an example of instantiation, + theory theories/Reals for many examples of use of field. Non-logical tactics ------------------------ @@ -4488,7 +4489,7 @@ user-defined tactics. other one can be automatically checked. .. [2] This corresponds to the cut rule of sequent calculus. .. [3] Reminder: opaque constants will not be expanded by δ reductions. -.. [4] The behavior of this tactic has much changed compared to the +.. [4] The behavior of this tactic has changed a lot compared to the versions available in the previous distributions (V6). This may cause significant changes in your theories to obtain the same result. As a drawback of the re-engineering of the code, this tactic has also been diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 0a517973c2..87131879e2 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -246,7 +246,7 @@ Requests to the environment hypothesis introduced in the first subgoal (if a proof is in progress). - See also: Section :ref:`performingcomputations`. + .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Compute @term @@ -255,7 +255,7 @@ Requests to the environment bytecode-based virtual machine. It is a shortcut for ``Eval vm_compute in`` :n:`@term`. - See also: Section :ref:`performingcomputations`. + .. seealso:: Section :ref:`performingcomputations`. .. cmd:: Print Assumptions @qualid @@ -521,7 +521,7 @@ Requests to the environment This command displays the full name of objects whose name is a prefix of the qualified identifier :n:`@qualid`, and consequently the |Coq| module in which they are defined. It searches for objects from the different - qualified name spaces of |Coq|: terms, modules, Ltac, etc. + qualified namespaces of |Coq|: terms, modules, Ltac, etc. .. example:: @@ -549,7 +549,7 @@ Requests to the environment As Locate but restricted to tactics. -See also: Section :ref:`locating-notations` +.. seealso:: Section :ref:`locating-notations` .. _loading-files: @@ -587,7 +587,9 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard Display, while loading, the answers of |Coq| to each command (including tactics) contained in - the loaded file See also: Section :ref:`controlling-display`. + the loaded file. + + .. seealso:: Section :ref:`controlling-display`. .. exn:: Can’t find file @ident on loadpath. @@ -699,10 +701,7 @@ file is a particular case of module called *library file*. that the commands ``Import`` and ``Export`` alone can be used inside modules (see Section :ref:`Import <import_qualid>`). - - -See also: Chapter :ref:`thecoqcommands` - + .. seealso:: Chapter :ref:`thecoqcommands` .. cmd:: Print Libraries @@ -930,7 +929,7 @@ Quitting and debugging .. cmd:: Drop - This is used mostly as a debug facility by |Coq|’s implementors and does + This is used mostly as a debug facility by |Coq|’s implementers and does not concern the casual user. This command permits to leave |Coq| temporarily and enter the OCaml toplevel. The OCaml command: @@ -1097,8 +1096,10 @@ described first. The scope of :cmd:`Opaque` is limited to the current section, or current file, unless the variant :cmd:`Global Opaque` is used. - See also: sections :ref:`performingcomputations`, :ref:`tactics-automating`, - :ref:`proof-editing-mode` + .. seealso:: + + Sections :ref:`performingcomputations`, :ref:`tactics-automating`, + :ref:`proof-editing-mode` .. exn:: The reference @qualid was not found in the current environment. @@ -1130,8 +1131,10 @@ described first. There is no constant referred by :n:`@qualid` in the environment. - See also: sections :ref:`performingcomputations`, - :ref:`tactics-automating`, :ref:`proof-editing-mode` + .. seealso: + + Sections :ref:`performingcomputations`, + :ref:`tactics-automating`, :ref:`proof-editing-mode` .. _vernac-strategy: @@ -1195,7 +1198,7 @@ described first. nothing prevents the user to also perform a ``Ltac`` `ident` ``:=`` `convtactic`. - See also: sections :ref:`performingcomputations` + .. seealso: :ref:`performingcomputations` .. _controlling-locality-of-commands: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d92b9a6794..5089a1b3e3 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -119,7 +119,7 @@ command understands. Here is how the previous examples refine. Notation "A /\ B" := (and A B) (at level 80, right associativity). Notation "A \/ B" := (or A B) (at level 85, right associativity). -By default, a notation is considered non-associative, but the +By default, a notation is considered nonassociative, but the precedence level is mandatory (except for special cases whose level is canonical). The level is either a number or the phrase ``next level`` whose meaning is obvious. @@ -139,7 +139,7 @@ instance define prefix notations. Notation "~ x" := (not x) (at level 75, right associativity). One can also define notations for incomplete terms, with the hole -expected to be inferred during typechecking. +expected to be inferred during type checking. .. coqtop:: in @@ -296,7 +296,7 @@ the possible following elements delimited by single quotes: after the “``[``” is applied at the beginning of each newline Notations disappear when a section is closed. No typing of the denoted -expression is performed at definition time. Type-checking is done only +expression is performed at definition time. Type checking is done only at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do @@ -899,7 +899,7 @@ notations are given below. The optional :production:`scope` is described in : | as strict pattern .. note:: No typing of the denoted expression is performed at definition - time. Type-checking is done only at the time of use of the notation. + time. Type checking is done only at the time of use of the notation. .. note:: Some examples of Notation may be found in the files composing the initial state of Coq (see directory :file:`$COQLIB/theories/Init`). @@ -1369,7 +1369,7 @@ Abbreviations Check (id 0). Abbreviations disappear when a section is closed. No typing of the - denoted expression is performed at definition time. Type-checking is + denoted expression is performed at definition time. Type checking is done only at the time of use of the abbreviation. .. _TacticNotation: @@ -1431,7 +1431,7 @@ Tactic notations allow to customize the syntax of tactics. They have the followi * - ``hyp`` - identifier - - an hypothesis defined in context + - a hypothesis defined in context - clear * - ``reference`` @@ -1503,7 +1503,7 @@ Tactic notations allow to customize the syntax of tactics. They have the followi .. [#and_or_levels] which are the levels effectively chosen in the current implementation of Coq -.. [#no_associativity] Coq accepts notations declared as non-associative but the parser on +.. [#no_associativity] Coq accepts notations declared as nonassociative but the parser on which Coq is built, namely Camlp5, currently does not implement ``no associativity`` and replaces it with ``left associativity``; hence it is the same for Coq: ``no associativity`` is in fact ``left associativity`` for the purposes of parsing |