diff options
| -rw-r--r-- | doc/sphinx/addendum/extraction.rst | 11 | ||||
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 18 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 69 | ||||
| -rw-r--r-- | doc/sphinx/addendum/miscellaneous-extensions.rst | 32 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 25 | ||||
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 322 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 26 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 255 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 40 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 740 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 89 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 41 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 4 |
16 files changed, 893 insertions, 794 deletions
diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3d58f522dd..f523a39477 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -99,12 +99,12 @@ Extraction Options Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The ability to fix target language is the first and more important -of the extraction options. Default is ``OCaml``. +.. cmd:: Extraction Language ( OCaml | Haskell | Scheme ) + :name: Extraction Language + + The ability to fix target language is the first and more important + of the extraction options. Default is ``OCaml``. -.. cmd:: Extraction Language OCaml -.. cmd:: Extraction Language Haskell -.. cmd:: Extraction Language Scheme Inlining and optimizations ~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -283,6 +283,7 @@ arity, that is a sequence of product finished by a sort), then some type variables have to be given (as quoted strings). The syntax is then: .. cmdv:: Extract Constant @qualid @string ... @string => @string + :undocumented: The number of type variables is checked by the system. For example: diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 403b163196..e468cc63cd 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -530,19 +530,11 @@ Notice, however, that using the prefixed tactics it is possible to pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity - :name: setoid_reflexivity - -.. tacv:: setoid_symmetry {? in @ident} - :name: setoid_symmetry - -.. tacv:: setoid_transitivity - :name: setoid_transitivity - -.. tacv:: setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} - :name: setoid_rewrite - -.. tacv:: setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} - :name: setoid_replace + setoid_symmetry {? in @ident} + setoid_transitivity + setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} + :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace The ``using relation`` arguments cannot be passed to the unprefixed form. The latter argument tells the tactic what parametric relation should diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index fc5a366caf..c8fb4bd00e 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -128,13 +128,28 @@ Declaring Coercions the two given classes. .. exn:: @qualid not declared. + :undocumented: + .. exn:: @qualid is already a coercion. + :undocumented: + .. exn:: Funclass cannot be a source class. + :undocumented: + .. exn:: @qualid is not a function. + :undocumented: + .. exn:: Cannot find the source class of @qualid. + :undocumented: + .. exn:: Cannot recognize @class as a source class of @qualid. + :undocumented: + .. exn:: @qualid does not respect the uniform inheritance condition. + :undocumented: + .. exn:: Found target class ... instead of ... + :undocumented: .. warn:: Ambiguous path. @@ -202,34 +217,34 @@ declaration, this constructor is declared as a coercion. .. cmd:: Identity Coercion @ident : @class >-> @class - If ``C`` is the source `class` and ``D`` the destination, we check - that ``C`` is a constant with a body of the form - :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the - number of parameters of ``D``. Then we define an identity - function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, - and we declare it as an identity coercion between ``C`` and ``D``. - - .. exn:: @class must be a transparent constant. + If ``C`` is the source `class` and ``D`` the destination, we check + that ``C`` is a constant with a body of the form + :g:`fun (x₁:T₁)..(xₙ:Tₙ) => D t₁..tₘ` where `m` is the + number of parameters of ``D``. Then we define an identity + function with type :g:`forall (x₁:T₁)..(xₙ:Tₙ)(y:C x₁..xₙ),D t₁..tₘ`, + and we declare it as an identity coercion between ``C`` and ``D``. - .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident + .. exn:: @class must be a transparent constant. + :undocumented: - Same as ``Identity Coercion`` but locally to the current section. + .. cmdv:: Local Identity Coercion @ident : @ident >-> @ident - .. cmdv:: SubClass @ident := @type - :name: SubClass + Same as :cmd:`Identity Coercion` but locally to the current section. - If `type` is a class `ident'` applied to some arguments then - `ident` is defined and an identity coercion of name - `Id_ident_ident'` is - declared. Otherwise said, this is an abbreviation for + .. cmdv:: SubClass @ident := @type + :name: SubClass - ``Definition`` `ident` ``:=`` `type`. + If :n:`@type` is a class :n:`@ident'` applied to some arguments then + :n:`@ident` is defined and an identity coercion of name + :n:`Id_@ident_@ident'` is + declared. Otherwise said, this is an abbreviation for - ``Identity Coercion`` `Id_ident_ident'` : `ident` ``>->`` `ident'`. + :n:`Definition @ident := @type.` + :n:`Identity Coercion Id_@ident_@ident' : @ident >-> @ident'`. - .. cmdv:: Local SubClass @ident := @type + .. cmdv:: Local SubClass @ident := @type - Same as before but locally to the current section. + Same as before but locally to the current section. Displaying Available Coercions @@ -237,19 +252,19 @@ Displaying Available Coercions .. cmd:: Print Classes - Print the list of declared classes in the current context. + Print the list of declared classes in the current context. .. cmd:: Print Coercions - Print the list of declared coercions in the current context. + Print the list of declared coercions in the current context. .. cmd:: Print Graph - Print the list of valid coercion paths in the current context. + Print the list of valid coercion paths in the current context. .. cmd:: Print Coercion Paths @class @class - Print the list of valid coercion paths between the two given classes. + Print the list of valid coercion paths between the two given classes. Activating the Printing of Coercions ------------------------------------- @@ -322,9 +337,9 @@ Coercions and Modules .. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. - This warning is emitted when typechecking relies on a coercion - contained in a module that has not been explicitely imported. It helps - migrating code and stop relying on the option above. + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. Examples -------- diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index 2cde65dcdc..db8c09d88f 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -12,22 +12,22 @@ of program refinements. To use the Derive extension it must first be required with ``Require Coq.derive.Derive``. When the extension is loaded, it provides the following command: -.. cmd:: Derive @ident SuchThat @term As @ident - -The first `ident` can appear in `term`. This command opens a new proof -presenting the user with a goal for term in which the name `ident` is -bound to an existential variable `?x` (formally, there are other goals -standing for the existential variables but they are shelved, as -described in :tacn:`shelve`). - -When the proof ends two constants are defined: - -+ The first one is named using the first `ident` and is defined as the proof of the - shelved goal (which is also the value of `?x`). It is always - transparent. -+ The second one is named using the second `ident`. It has type `term`, and its body is - the proof of the initially visible goal. It is opaque if the proof - ends with ``Qed``, and transparent if the proof ends with ``Defined``. +.. cmd:: Derive @ident__1 SuchThat @type As @ident__2 + + :n:`@ident__1` can appear in :n:`@type`. This command opens a new proof + presenting the user with a goal for :n:`@type` in which the name :n:`@ident__1` is + bound to an existential variable :g:`?x` (formally, there are other goals + standing for the existential variables but they are shelved, as + described in :tacn:`shelve`). + + When the proof ends two constants are defined: + + + The first one is named :n:`@ident__1` and is defined as the proof of the + shelved goal (which is also the value of :g:`?x`). It is always + transparent. + + The second one is named :n:`@ident__2`. It has type :n:`@type`, and its body is + the proof of the initially visible goal. It is opaque if the proof + ends with :cmd:`Qed`, and transparent if the proof ends with :cmd:`Defined`. .. example:: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 03d4f148e3..b008508bbc 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -67,16 +67,22 @@ is generated: :tacn:`intro` as many times as needed. .. exn:: omega: Unrecognized predicate or connective: @ident. + :undocumented: .. exn:: omega: Unrecognized atomic proposition: ... + :undocumented: .. exn:: omega: Can't solve a goal with proposition variables. + :undocumented: .. exn:: omega: Unrecognized proposition. + :undocumented: .. exn:: omega: Can't solve a goal with non-linear products. + :undocumented: .. exn:: omega: Can't solve a goal with equality on type ... + :undocumented: Using ``omega`` diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index fad45995d2..cc8870e2e4 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -150,6 +150,7 @@ Program Definition .. exn:: @ident already exists. :name: @ident already exists. (Program Definition) + :undocumented: .. cmdv:: Program Definition @ident : @type := @term @@ -162,7 +163,7 @@ Program Definition and the aforementioned coercion derivation are solved. .. exn:: In environment … the term: @term does not have type @type. Actually, it has type ... - + :undocumented: .. cmdv:: Program Definition @ident @binders : @type := @term @@ -181,21 +182,21 @@ Program Fixpoint .. cmd:: Program Fixpoint @ident @params {? {@order}} : @type := @term -The optional order annotation follows the grammar: + The optional order annotation follows the grammar: -.. productionlist:: orderannot - order : measure `term` (`term`)? | wf `term` `term` + .. productionlist:: orderannot + order : measure `term` (`term`)? | wf `term` `term` -+ :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on - any subset of the arguments and the optional (parenthesised) term - ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` - to ``lt``. + + :g:`measure f ( R )` where :g:`f` is a value of type :g:`X` computed on + any subset of the arguments and the optional (parenthesised) term + ``(R)`` is a relation on ``X``. By default ``X`` defaults to ``nat`` and ``R`` + to ``lt``. -+ :g:`wf R x` which is equivalent to :g:`measure x (R)`. + + :g:`wf R x` which is equivalent to :g:`measure x (R)`. -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. + 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 in diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 58617916c0..5bab63f6d0 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -100,26 +100,26 @@ Concrete usage in Coq .. tacn:: ring -The ``ring`` tactic solves equations upon polynomial expressions of a ring -(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. + This tactic solves equations upon polynomial expressions of a ring + (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. .. tacn:: ring_simplify -``ring_simplify`` applies the normalization procedure described above to -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 -sides are normalized. The tactic can also be applied in a hypothesis. + This tactic applies the normalization procedure described above to + 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 + sides are normalized. The tactic can also be applied in a hypothesis. -The tactic must be loaded by ``Require Import Ring``. The ring structures -must be declared with the ``Add Ring`` command (see below). The ring of -booleans is predefined; if one wants to use the tactic on |nat| one must -first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do -``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do -``Require Import NArithRing`` or ``Require Import NArith``. + The tactic must be loaded by ``Require Import Ring``. The ring structures + must be declared with the ``Add Ring`` command (see below). The ring of + booleans is predefined; if one wants to use the tactic on |nat| one must + first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do + ``Require Import ZArithRing`` or simply ``Require Import ZArith``; for |N|, do + ``Require Import NArithRing`` or ``Require Import NArith``. .. example:: @@ -141,25 +141,24 @@ first require the module ``ArithRing`` exported by ``Arith``); for |Z|, do .. tacv:: ring [{* @term }] -decides the equality of two terms modulo ring operations and -the equalities defined by the :n:`@term`\ s. -Each :n:`@term` has to be a proof of some equality `m = p`, where `m` is a monomial (after “abstraction”), `p` a polynomial and `=` the corresponding equality of the ring structure. + This tactic decides the equality of two terms modulo ring operations and + the equalities defined by the :token:`term`\ s. + Each :token:`term` has to be a proof of some equality :g:`m = p`, where :g:`m` + is a monomial (after “abstraction”), :g:`p` a polynomial and :g:`=` the + corresponding equality of the ring structure. .. tacv:: ring_simplify [{* @term }] {* @term } in @ident -performs the simplification in the hypothesis named :n:`@ident`. + This tactic performs the simplification in the hypothesis named :token:`ident`. .. note:: - .. tacn:: ring_simplify @term1; ring_simplify @term2 + :n:`ring_simplify @term__1; ring_simplify @term__2` is not equivalent to + :n:`ring_simplify @term__1 @term__2`. - is not equivalent to - - .. tacn:: ring_simplify @term1 @term2 - - In the latter case the variables map - is shared between the two terms, and common subterm `t` of :n:`@term1` and :n:`@term2` + In the latter case the variables map is shared between the two terms, and + common subterm :g:`t` of :n:`@term__1` and :n:`@term__2` will have the same associated variable number. So the first alternative should be avoided for terms belonging to the same ring theory. @@ -174,17 +173,17 @@ Error messages: .. exn:: Arguments of ring_simplify do not have all the same type. - ``ring_simplify`` cannot simplify terms of several rings at the same + :tacn:`ring_simplify` cannot simplify terms of several rings at the same time. Invoke the tactic once per ring structure. .. exn:: Cannot find a declared ring structure over @term. No ring has been declared for the type of the terms to be simplified. - Use ``Add Ring`` first. + Use :cmd:`Add Ring` first. .. exn:: Cannot find a declared ring structure for equality @term. - Same as above in the case of the ``ring`` tactic. + Same as above in the case of the :tacn:`ring` tactic. Adding a ring structure @@ -302,93 +301,93 @@ 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 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: - -.. productionlist:: coq - ring_mod : abstract | decidable `term` | morphism `term` - : | setoid `term` `term` - : | constants [`ltac`] - : | preprocess [`ltac`] - : | postprocess [`ltac`] - : | power_tac `term` [`ltac`] - : | sign `term` - : | div `term` - -abstract - declares the ring as abstract. This is the default. - -decidable :n:`@term` - declares the ring as computational. The expression - :n:`@term` is the correctness proof of an equality test ``?=!`` - (which hould be evaluable). Its type should be of the form - ``forall x y, x ?=! y = true → x == y``. - -morphism :n:`@term` - declares the ring as a customized one. The expression - :n:`@term` is a proof that there exists a morphism between a set of - coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and - ``Ring_theory.semi_morph``). - -setoid :n:`@term` :n:`@term` - forces the use of given setoid. The first - :n:`@term` is a proof that the equality is indeed a setoid (see - ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the - ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and - ``Ring_theory.sring_eq_ext``). - This modifier needs not be used if the setoid and morphisms have been - declared. - -constants [:n:`@ltac`] - specifies a tactic expression :n:`@ltac` that, given a - term, returns either an object of the coefficient set that is mapped - to the expression via the morphism, or returns - ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 - to their counterpart in the coefficient set. This is generally not - desirable for non trivial computational rings. - -preprocess [:n:`@ltac`] - specifies a tactic :n:`@ltac` that is applied as a - preliminary step for ``ring`` and ``ring_simplify``. It can be used to - transform a goal so that it is better recognized. For instance, ``S n`` - can be changed to ``plus 1 n``. - -postprocess [:n:`@ltac`] - specifies a tactic :n:`@ltac` that is applied as a final - step for ``ring_simplify``. For instance, it can be used to undo - modifications of the preprocessor. - -power_tac :n:`@term` [:n:`@ltac`] - allows ``ring`` and ``ring_simplify`` to recognize - power expressions with a constant positive integer exponent (example: - ::math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies - the specification of a power function (term has to be a proof of - ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression - that, given a term, “abstracts” it into an object of type |N| whose - interpretation via ``Cp_phi`` (the evaluation function of power - coefficient) is the original term, or returns ``InitialRing.NotConstant`` - if not a constant coefficient (i.e. |L_tac| is the inverse function of - ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` - and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic - does not recognize power expressions as ring expressions. - -sign :n:`@term` - allows ``ring_simplify`` to use a minus operation when - outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The - term `:n:`@term` is a proof that a given sign function indicates expressions - that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See - ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. - -div :n:`@term` - allows ``ring`` and ``ring_simplify`` to use monomials with - 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 - trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See - ``plugins/setoid_ring/InitialRing.v`` for examples of div function. + The :token:`ident` is not relevant. It is used just for error messages. The + :token:`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: + + .. productionlist:: coq + ring_mod : abstract | decidable `term` | morphism `term` + : | setoid `term` `term` + : | constants [`ltac`] + : | preprocess [`ltac`] + : | postprocess [`ltac`] + : | power_tac `term` [`ltac`] + : | sign `term` + : | div `term` + + abstract + declares the ring as abstract. This is the default. + + decidable :n:`@term` + declares the ring as computational. The expression + :n:`@term` is the correctness proof of an equality test ``?=!`` + (which hould be evaluable). Its type should be of the form + ``forall x y, x ?=! y = true → x == y``. + + morphism :n:`@term` + declares the ring as a customized one. The expression + :n:`@term` is a proof that there exists a morphism between a set of + coefficient and the ring carrier (see ``Ring_theory.ring_morph`` and + ``Ring_theory.semi_morph``). + + setoid :n:`@term` :n:`@term` + forces the use of given setoid. The first + :n:`@term` is a proof that the equality is indeed a setoid (see + ``Setoid.Setoid_Theory``), and the second :n:`@term` a proof that the + ring operations are morphisms (see ``Ring_theory.ring_eq_ext`` and + ``Ring_theory.sring_eq_ext``). + This modifier needs not be used if the setoid and morphisms have been + declared. + + constants [ :n:`@ltac` ] + specifies a tactic expression :n:`@ltac` that, given a + term, returns either an object of the coefficient set that is mapped + to the expression via the morphism, or returns + ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 + to their counterpart in the coefficient set. This is generally not + desirable for non trivial computational rings. + + preprocess [ :n:`@ltac` ] + specifies a tactic :n:`@ltac` that is applied as a + preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to + transform a goal so that it is better recognized. For instance, ``S n`` + can be changed to ``plus 1 n``. + + postprocess [ :n:`@ltac` ] + specifies a tactic :n:`@ltac` that is applied as a final + step for :tacn:`ring_simplify`. For instance, it can be used to undo + modifications of the preprocessor. + + power_tac :n:`@term` [ :n:`@ltac` ] + allows :tacn:`ring` and :tacn:`ring_simplify` to recognize + power expressions with a constant positive integer exponent (example: + :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies + the specification of a power function (term has to be a proof of + ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + that, given a term, “abstracts” it into an object of type |N| whose + interpretation via ``Cp_phi`` (the evaluation function of power + coefficient) is the original term, or returns ``InitialRing.NotConstant`` + if not a constant coefficient (i.e. |L_tac| is the inverse function of + ``Cp_phi``). See files ``plugins/setoid_ring/ZArithRing.v`` + and ``plugins/setoid_ring/RealField.v`` for examples. By default the tactic + does not recognize power expressions as ring expressions. + + sign :n:`@term` + allows :tacn:`ring_simplify` to use a minus operation when + outputting its normal form, i.e writing ``x − y`` instead of ``x + (− y)``. The + term `:n:`@term` is a proof that a given sign function indicates expressions + that are signed (`term` has to be a proof of ``Ring_theory.get_sign``). See + ``plugins/setoid_ring/InitialRing.v`` for examples of sign function. + + div :n:`@term` + allows :tacn:`ring` and :tacn:`ring_simplify` to use monomials with + 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 + trying to rewrite :math:`7x` by :math:`2x = z` to tell that :math:`7 = 3 \times 2 + 1`. See + ``plugins/setoid_ring/InitialRing.v`` for examples of div function. Error messages: @@ -497,30 +496,31 @@ Dealing with fields .. tacn:: field -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 -:math:`N = 0`. -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. 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 -a field is an integral domain, and when the equality test on -coefficients is complete w.r.t. the equality of the target field, -constants can be proven different from zero automatically. - -The tactic must be loaded by ``Require Import Field``. New field -structures can be declared to the system with the ``Add Field`` command -(see below). The field of real numbers is defined in module ``RealField`` -(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 the module ``Qcanon``. + This tactic is an extension of the :tacn:`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 + :math:`N = 0`. + + Note that :n:`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. 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 + a field is an integral domain, and when the equality test on + coefficients is complete w.r.t. the equality of the target field, + constants can be proven different from zero automatically. + + The tactic must be loaded by ``Require Import Field``. New field + structures can be declared to the system with the ``Add Field`` command + (see below). The field of real numbers is defined in module ``RealField`` + (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 the module ``Qcanon``. .. example:: @@ -654,27 +654,25 @@ 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 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. - -.. productionlist:: coq - field_mod : `ring_mod` | completeness `term` - -Since field tactics are built upon ``ring`` -tactics, all modifiers of the ``Add Ring`` apply. There is only one -specific modifier: - -completeness :n:`@term` - allows the field tactic to prove automatically - 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``, - - which is the completeness of equality on coefficients - w.r.t. the field equality. + 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. + + .. productionlist:: coq + field_mod : `ring_mod` | completeness `term` + + Since field tactics are built upon ``ring`` + tactics, all modifiers of the ``Add Ring`` apply. There is only one + specific modifier: + + completeness :n:`@term` + allows the field tactic to prove automatically + that the image of nonzero coefficients are mapped to nonzero + elements of the field. :n:`@term` is a proof of + :g:`forall x y, [x] == [y] -> x ?=! y = true`, + which is the completeness of equality on coefficients + w.r.t. the field equality. History of ring diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 369dae0ead..15a55d9e72 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -298,24 +298,24 @@ Variants: This command has no effect when used on a typeclass. -.. cmd:: Instance @ident {? @binders} : Class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } +.. cmd:: Instance @ident {? @binders} : @class t1 … tn [| priority] := { field1 := b1 ; …; fieldi := bi } -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. + This command is used to declare a typeclass instance named + :token:`ident` of the class :token:`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. -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 -:tacn:`auto` hints. If the priority is not specified, it defaults to the number -of non-dependent binders of the instance. + An arbitrary context of :token:`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 + :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 +.. cmdv:: Instance @ident {? @binders} : forall {? @binders}, @class @term__1 … @term__n [| priority] := @term This syntax is used for declaration of singleton class instances or - for directly giving an explicit term of type ``forall binders, Class - t1 … tn``. One need not even mention the unique field name for + for directly giving an explicit term of type :n:`forall @binders, @class + @term__1 … @term__n`. One need not even mention the unique field name for singleton classes. .. cmdv:: Global Instance diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 41afe3c312..99b883d23c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -386,8 +386,10 @@ to universes and explicitly instantiate polymorphic definitions. global constraint on polymorphic universes. .. exn:: Undeclared universe @ident. + :undocumented: .. exn:: Universe inconsistency. + :undocumented: Polymorphic definitions diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 391afcb1f7..562ed48171 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -27,22 +27,20 @@ expressions. In this sense, the :cmd:`Record` construction allows defining field : `ident` [ `binders` ] : `type` [ where `notation` ] : | `ident` [ `binders` ] [: `type` ] := `term` -In the expression: - .. cmd:: Record @ident @binders {? : @sort} := {? @ident} { {*; @ident @binders : @type } } -the first identifier :token:`ident` is the name of the defined record and :token:`sort` is its -type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, -the default name ``Build_``\ :token:`ident`, where :token:`ident` is the record name, is used. If :token:`sort` is -omitted, the default sort is `\Type`. The identifiers inside the brackets are the names of -fields. For a given field :token:`ident`, its type is :g:`forall binders, type`. -Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the -order of the fields is important. Finally, :token:`binders` are parameters of the record. + The first identifier :token:`ident` is the name of the defined record and :token:`sort` is its + type. The optional identifier following ``:=`` is the name of its constructor. If it is omitted, + the default name :n:`Build_@ident`, where :token:`ident` is the record name, is used. If :token:`sort` is + omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the names of + fields. For a given field :token:`ident`, its type is :n:`forall @binders, @type`. + Remark that the type of a particular identifier may depend on a previously-given identifier. Thus the + order of the fields is important. Finally, :token:`binders` are parameters of the record. More generally, a record may have explicitly defined (a.k.a. manifest) fields. For instance, we might have: -:n:`Record @ident @binders : @sort := { @ident₁ : @type₁ ; @ident₂ := @term₂ ; @ident₃ : @type₃ }`. -in which case the correctness of :n:`@type₃` may rely on the instance :n:`@term₂` of :n:`@ident₂` and :n:`@term₂` may in turn depend on :n:`@ident₁`. +:n:`Record @ident @binders : @sort := { @ident__1 : @type__1 ; @ident__2 := @term__2 ; @ident__3 : @type__3 }`. +in which case the correctness of :n:`@type__3` may rely on the instance :n:`@term__2` of :n:`@ident__2` and :n:`@term__2` may in turn depend on :n:`@ident__1`. .. example:: @@ -149,16 +147,16 @@ available: Eval compute in half.(top). -It can be activated for printing with - .. flag:: Printing Projections -.. example:: + This flag activates the dot notation for printing. - .. coqtop:: all + .. example:: + + .. coqtop:: all - Set Printing Projections. - Check top half. + Set Printing Projections. + Check top half. .. FIXME: move this to the main grammar in the spec chapter @@ -601,17 +599,17 @@ The following experimental command is available when the ``FunInd`` library has .. cmd:: Function @ident {* @binder} { @decrease_annot } : @type := @term -This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper -for several ways of defining a function *and other useful related -objects*, namely: an induction principle that reflects the recursive -structure of the function (see :tacn:`function induction`) and its fixpoint equality. -The meaning of this declaration is to define a function ident, -similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must -be given (unless the function is not recursive), but it might not -necessarily be *structurally* decreasing. The point of the {} annotation -is to name the decreasing argument *and* to describe which kind of -decreasing criteria must be used to ensure termination of recursive -calls. + This command can be seen as a generalization of ``Fixpoint``. It is actually a wrapper + for several ways of defining a function *and other useful related + objects*, namely: an induction principle that reflects the recursive + structure of the function (see :tacn:`function induction`) and its fixpoint equality. + The meaning of this declaration is to define a function ident, + similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must + be given (unless the function is not recursive), but it might not + necessarily be *structurally* decreasing. The point of the {} annotation + is to name the decreasing argument *and* to describe which kind of + decreasing criteria must be used to ensure termination of recursive + calls. The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work @@ -667,27 +665,32 @@ For now, dependent cases are not treated for non structurally terminating functions. .. exn:: The recursive argument must be specified. + :undocumented: + .. exn:: No argument name @ident. + :undocumented: + .. exn:: Cannot use mutual definition with well-founded recursion or measure. + :undocumented: .. warn:: Cannot define graph for @ident. - The generation of the graph relation (`R_ident`) used to compute the induction scheme of ident - raised a typing error. Only `ident` is defined; the induction scheme - will not be generated. This error happens generally when: + The generation of the graph relation (:n:`R_@ident`) used to compute the induction scheme of ident + raised a typing error. Only :token:`ident` is defined; the induction scheme + will not be generated. This error happens generally when: - - the definition uses pattern matching on dependent types, - which ``Function`` cannot deal with yet. - - the definition is not a *pattern matching tree* as explained above. + - the definition uses pattern matching on dependent types, + which ``Function`` cannot deal with yet. + - the definition is not a *pattern matching tree* as explained above. .. warn:: Cannot define principle(s) for @ident. - The generation of the graph relation (`R_ident`) succeeded but the induction principle - could not be built. Only `ident` is defined. Please report. + The generation of the graph relation (:n:`R_@ident`) succeeded but the induction principle + could not be built. Only :token:`ident` is defined. Please report. .. warn:: Cannot build functional inversion principle. - `functional inversion` will not be available for the function. + :tacn:`functional inversion` will not be available for the function. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` @@ -713,7 +716,7 @@ used by ``Function``. A more precise description is given below. + The fixpoint equation of `ident`: `ident_equation`. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term -.. cmdv:: Function @ident {* @binder } { wf @term @ident } : @type := @term + Function @ident {* @binder } { wf @term @ident } : @type := @term Defines a recursive function by well-founded recursion. The module ``Recdef`` of the standard library must be loaded for this feature. The ``{}`` @@ -799,10 +802,10 @@ Section :ref:`gallina-definitions`). `s1` and outside. .. exn:: This is not the last opened section. + :undocumented: -**Remarks:** - -#. Most commands, like ``Hint``, ``Notation``, option management, … which +.. note:: + Most commands, like ``Hint``, ``Notation``, option management, … which appear inside a section are canceled when the section is closed. @@ -874,52 +877,55 @@ Reserved commands inside an interactive module .. cmd:: Include {+<+ @module} - is a shortcut for the commands ``Include`` `module` for each `module`. + is a shortcut for the commands :n:`Include @module` for each :token:`module`. .. cmd:: End @ident - This command closes the interactive module `ident`. If the module type + This command closes the interactive module :token:`ident`. If the module type was given the content of the module is matched against it and an error is signaled if the matching fails. If the module is basic (is not a functor) its components (constants, inductive types, submodules etc.) are now available through the dot notation. .. exn:: No such label @ident. + :undocumented: .. exn:: Signature components for label @ident do not match. + :undocumented: .. exn:: This is not the last opened module. + :undocumented: .. cmd:: Module @ident := @module_expression - This command defines the module identifier `ident` to be equal - to `module_expression`. + This command defines the module identifier :token:`ident` to be equal + to :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} := @module_expression - Defines a functor with parameters given by the list of `module_binding` and body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` and body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} : @module_type := @module_expression - Defines a functor with parameters given by the list of `module_binding` (possibly none), and output module type `module_type`, - with body `module_expression`. + Defines a functor with parameters given by the list of :token:`module_binding` (possibly none), and output module type :token:`module_type`, + with body :token:`module_expression`. .. cmdv:: Module @ident {* @module_binding} <: {+<: @module_type} := @module_expression - Defines a functor with parameters given by module_bindings (possibly none) with body `module_expression`. + Defines a functor with parameters given by module_bindings (possibly none) with body :token:`module_expression`. The body is checked against each |module_type_i|. .. cmdv:: Module @ident {* @module_binding} := {+<+ @module_expression} - is equivalent to an interactive module where each `module_expression` is included. + is equivalent to an interactive module where each :token:`module_expression` is included. .. cmd:: Module Type @ident -This command is used to start an interactive module type `ident`. + This command is used to start an interactive module type :token:`ident`. - .. cmdv:: Module Type @ident {* @module_binding} + .. cmdv:: Module Type @ident {* @module_binding} - Starts an interactive functor type with parameters given by `module_bindings`. + Starts an interactive functor type with parameters given by :token:`module_bindings`. Reserved commands inside an interactive module type: @@ -931,7 +937,7 @@ Reserved commands inside an interactive module type: .. cmd:: Include {+<+ @module} - is a shortcut for the command ``Include`` `module` for each `module`. + This is a shortcut for the command :n:`Include @module` for each :token:`module`. .. cmd:: @assumption_keyword Inline @assums :name: Inline @@ -941,31 +947,32 @@ Reserved commands inside an interactive module type: .. cmd:: End @ident - This command closes the interactive module type `ident`. + This command closes the interactive module type :token:`ident`. .. exn:: This is not the last opened module type. + :undocumented: .. cmd:: Module Type @ident := @module_type - Defines a module type `ident` equal to `module_type`. + Defines a module type :token:`ident` equal to :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := @module_type - Defines a functor type `ident` specifying functors taking arguments `module_bindings` and - returning `module_type`. + Defines a functor type :token:`ident` specifying functors taking arguments :token:`module_bindings` and + returning :token:`module_type`. .. cmdv:: Module Type @ident {* @module_binding} := {+<+ @module_type } - is equivalent to an interactive module type were each `module_type` is included. + is equivalent to an interactive module type were each :token:`module_type` is included. .. cmd:: Declare Module @ident : @module_type - Declares a module `ident` of type `module_type`. + Declares a module :token:`ident` of type :token:`module_type`. .. cmdv:: Declare Module @ident {* @module_binding} : @module_type - Declares a functor with parameters given by the list of `module_binding` and output module type - `module_type`. + Declares a functor with parameters given by the list of :token:`module_binding` and output module type + :token:`module_type`. .. example:: @@ -1205,8 +1212,10 @@ component is equal ``nat`` and hence ``M1.T`` as specified. is imported, qualid is imported as well. .. exn:: @qualid is not a module. + :undocumented: .. warn:: Trying to mask the absolute name @qualid! + :undocumented: .. cmd:: Print Module @ident @@ -1506,6 +1515,7 @@ possible, the correct argument will be automatically generated. .. exn:: Cannot infer a term for this placeholder. :name: Cannot infer a term for this placeholder. (Casual use of implicit arguments) + :undocumented: |Coq| was not able to deduce an instantiation of a “_”. @@ -1566,38 +1576,39 @@ usual implicit arguments disambiguation syntax. Declaring Implicit Arguments ++++++++++++++++++++++++++++ -To set implicit arguments *a posteriori*, one can use the command: -.. cmd:: Arguments @qualid {* @possibly_bracketed_ident } - :name: Arguments (implicits) -where the list of `possibly_bracketed_ident` is a prefix of the list of -arguments of `qualid` where the ones to be declared implicit are -surrounded by square brackets and the ones to be declared as maximally -inserted implicits are surrounded by curly braces. +.. cmd:: Arguments @qualid {* [ @ident ] | @ident } + :name: Arguments (implicits) -After the above declaration is issued, implicit arguments can just -(and have to) be skipped in any expression involving an application -of `qualid`. + This command is used to set implicit arguments *a posteriori*, + where the list of possibly bracketed :token:`ident` is a prefix of the list of + arguments of :token:`qualid` where the ones to be declared implicit are + surrounded by square brackets and the ones to be declared as maximally + inserted implicits are surrounded by curly braces. -Implicit arguments can be cleared with the following syntax: + After the above declaration is issued, implicit arguments can just + (and have to) be skipped in any expression involving an application + of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits -.. cmdv:: Global Arguments @qualid {* @possibly_bracketed_ident } + This command clears implicit arguments. + +.. cmdv:: Global Arguments @qualid {* [ @ident ] | @ident } - Says to recompute the implicit arguments of - `qualid` after ending of the current section if any, enforcing the + This command is used to recompute the implicit arguments of + :token:`qualid` after ending of the current section if any, enforcing the implicit arguments known from inside the section to be the ones declared by the command. -.. cmdv:: Local Arguments @qualid {* @possibly_bracketed_ident } +.. cmdv:: Local Arguments @qualid {* [ @ident ] | @ident } When in a module, tell not to activate the - implicit arguments ofqualid declared by this command to contexts that + implicit arguments of :token:`qualid` declared by this command to contexts that require the module. -.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ @possibly_bracketed_ident } } +.. cmdv:: {? Global | Local } Arguments @qualid {*, {+ [ @ident ] | @ident } } For names of constants, inductive types, constructors, lemmas which can only be applied to a fixed number of @@ -1639,33 +1650,34 @@ Implicit arguments can be cleared with the following syntax: Check (fun l => map length l = map (list nat) nat length l). -Remark: To know which are the implicit arguments of an object, use the -command ``Print Implicit`` (see :ref:`displaying-implicit-args`). +.. note:: + To know which are the implicit arguments of an object, use the + command :cmd:`Print Implicit` (see :ref:`displaying-implicit-args`). Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -|Coq| can also automatically detect what are the implicit arguments of a -defined object. The command is just - .. cmd:: Arguments @qualid : default implicits -The auto-detection is governed by options telling if strict, -contextual, or reversible-pattern implicit arguments must be -considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, -:ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). + This command tells |Coq| to automatically detect what are the implicit arguments of a + defined object. + + The auto-detection is governed by options telling if strict, + contextual, or reversible-pattern implicit arguments must be + considered or not (see :ref:`controlling-strict-implicit-args`, :ref:`controlling-strict-implicit-args`, + :ref:`controlling-rev-pattern-implicit-args`, and also :ref:`controlling-insertion-implicit-args`). -.. cmdv:: Global Arguments @qualid : default implicits + .. cmdv:: Global Arguments @qualid : default implicits - Tell to recompute the - implicit arguments of qualid after ending of the current section if - any. + Tell to recompute the + implicit arguments of qualid after ending of the current section if + any. -.. cmdv:: Local Arguments @qualid : default implicits + .. cmdv:: Local Arguments @qualid : default implicits - When in a module, tell not to activate the implicit arguments of `qualid` computed by this - declaration to contexts that requires the module. + When in a module, tell not to activate the implicit arguments of :token:`qualid` computed by this + declaration to contexts that requires the module. .. example:: @@ -1820,10 +1832,10 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Implicit arguments names can be redefined using the following syntax: - .. cmd:: Arguments @qualid {* @name} : @rename + This command is used to redefine the names of implicit arguments. + With the assert flag, ``Arguments`` can be used to assert that a given object has the expected number of arguments and that these arguments are named as expected. @@ -1845,11 +1857,12 @@ are named as expected. Displaying what the implicit arguments are ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -To display the implicit arguments associated to an object, and to know -if each of them is to be used maximally or not, use the command - .. cmd:: Print Implicit @qualid + Use this command to display the implicit arguments associated to an object, + and to know if each of them is to be used maximally or not. + + Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1984,16 +1997,16 @@ Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ It is possible to bind variable names to a given type (e.g. in a -development using arithmetic, it may be convenient to bind the names `n` -or `m` to the type ``nat`` of natural numbers). The command for that is +development using arithmetic, it may be convenient to bind the names :g:`n` +or :g:`m` to the type :g:`nat` of natural numbers). .. cmd:: Implicit Types {+ @ident } : @type -The effect of the command is to automatically set the type of bound -variables starting with `ident` (either `ident` itself or `ident` followed by -one or more single quotes, underscore or digits) to be `type` (unless -the bound variable is already declared with an explicit type in which -case, this latter type is considered). + The effect of the command is to automatically set the type of bound + variables starting with :token:`ident` (either :token:`ident` itself or + :token:`ident` followed by one or more single quotes, underscore or + digits) to be :token:`type` (unless the bound variable is already declared + with an explicit type in which case, this latter type is considered). .. example:: @@ -2137,29 +2150,29 @@ Printing universes terms apparently identical but internally different in the Calculus of Inductive Constructions. -The constraints on the internal level of the occurrences of Type -(see :ref:`Sorts`) can be printed using the command - .. cmd:: Print {? Sorted} Universes :name: Print Universes -If the optional ``Sorted`` option is given, each universe will be made -equivalent to a numbered label reflecting its level (with a linear -ordering) in the universe hierarchy. + This command can be used to print the constraints on the internal level + of the occurrences of :math:`\Type` (see :ref:`Sorts`). + + If the optional ``Sorted`` option is given, each universe will be made + equivalent to a numbered label reflecting its level (with a linear + ordering) in the universe hierarchy. -This command also accepts an optional output filename: + .. cmdv:: Print {? Sorted} Universes @string -.. cmdv:: Print {? Sorted} Universes @string + This variant accepts an optional output filename. -If `string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT -language, and can be processed by Graphviz tools. The format is -unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. + If :token:`string` ends in ``.dot`` or ``.gv``, the constraints are printed in the DOT + language, and can be processed by Graphviz tools. The format is + unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. .. cmdv:: Print Universes Subgraph(@names) -Prints the graph restricted to the requested names (adjusting -constraints to preserve the implied transitive constraints between -kept universes). + Prints the graph restricted to the requested names (adjusting + constraints to preserve the implied transitive constraints between + kept universes). .. _existential-variables: diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index edd83b7cee..0ea8c7be2d 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -292,6 +292,7 @@ focused goals with: .. exn:: No such goal. :name: No such goal. (Goal selector) + :undocumented: .. TODO change error message index entry @@ -351,6 +352,7 @@ We can check if a tactic made progress with: goals (up to syntactical equality), then an error of level 0 is raised. .. exn:: Failed to progress. + :undocumented: Backtracking branching ~~~~~~~~~~~~~~~~~~~~~~ @@ -393,6 +395,7 @@ tactic to work (i.e. which does not fail) among a panel of tactics: :n:`v__i` to have *at least* one success. .. exn:: No applicable tactic. + :undocumented: .. tacv:: first @expr @@ -482,6 +485,7 @@ one* success: immediately. .. exn:: This tactic has more than one success. + :undocumented: Checking the failure ~~~~~~~~~~~~~~~~~~~~ @@ -521,6 +525,7 @@ among a panel of tactics: apply :n:`v__2` and so on. It fails if there is no solving tactic. .. exn:: Cannot solve the goal. + :undocumented: .. tacv:: solve @expr @@ -576,8 +581,7 @@ Failing goals left. See the example for clarification. .. tacv:: gfail {* message_token} - - .. tacv:: gfail @num {* message_token} + gfail @num {* message_token} These variants fail with an error message or an error level even if there are no goals left. Be careful however if Coq terms have to be @@ -586,9 +590,11 @@ Failing evaluated, a tactic call like :n:`let x := H in fail 0 x` will succeed. .. exn:: Tactic Failure message (level @num). + :undocumented: .. exn:: No such goal. :name: No such goal. (fail) + :undocumented: .. example:: @@ -670,24 +676,24 @@ tactic This tactic currently does not support nesting, and will report times based on the innermost execution. This is due to the fact that it is - implemented using the tactics + implemented using the following internal tactics: .. tacn:: restart_timer @string :name: restart_timer - and + Reset a timer - .. tacn:: finish_timing {? @string} @string + .. tacn:: finish_timing {? (@string)} @string :name: finish_timing - which (re)set and display an optionally named timer, respectively. The - parenthesized string argument to :n:`finish_timing` is also optional, and - determines the label associated with the timer for printing. + Display an optionally named timer. The parenthesized string argument + is also optional, and determines the label associated with the timer + for printing. - By copying the definition of :n:`time_constr` from the standard library, + By copying the definition of :tacn:`time_constr` from the standard library, users can achive support for a fixed pattern of nesting by passing - different :n:`@string` parameters to :n:`restart_timer` and :n:`finish_timing` - at each level of nesting. + different :token:`string` parameters to :tacn:`restart_timer` and + :tacn:`finish_timing` at each level of nesting. .. example:: @@ -967,10 +973,10 @@ Evaluation of a term can be performed with: Recovering the type of a term ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The following returns the type of term: - .. tacn:: type of @term + This tactic returns the type of :token:`term`. + Manipulating untyped terms ~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1041,6 +1047,7 @@ Testing boolean expressions Fail all:let n:= numgoals in guard n=2. .. exn:: Condition not satisfied. + :undocumented: Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -1092,6 +1099,7 @@ Proving a subgoal as a separate lemma .. exn:: Proof is not complete. :name: Proof is not complete. (abstract) + :undocumented: Tactic toplevel definitions --------------------------- @@ -1348,6 +1356,6 @@ Run-time optimization tactic .. tacn:: optimize_heap :name: optimize_heap -This tactic behaves like :n:`idtac`, except that running it compacts the -heap in the OCaml run-time system. It is analogous to the Vernacular -command :cmd:`Optimize Heap`. + This tactic behaves like :n:`idtac`, except that running it compacts the + heap in the OCaml run-time system. It is analogous to the Vernacular + command :cmd:`Optimize Heap`. diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 0b059f92ee..590d71b5f3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -67,6 +67,7 @@ list of assertion commands is given in :ref:`Assertions`. The command added to the environment as an opaque constant. .. exn:: Attempt to save an incomplete proof. + :undocumented: .. note:: @@ -106,6 +107,7 @@ list of assertion commands is given in :ref:`Assertions`. The command proof was edited. .. exn:: No focused proof (No proof-editing in progress). + :undocumented: .. cmdv:: Abort @ident @@ -282,6 +284,7 @@ Navigation in the proof tree This command restores the proof editing process to the original goal. .. exn:: No focused proof to restart. + :undocumented: .. cmd:: Focus @@ -473,13 +476,14 @@ Requesting information This command displays the current goals. .. exn:: No focused proof. + :undocumented: .. cmdv:: Show @num Displays only the :token:`num`\-th subgoal. .. exn:: No such goal. - + :undocumented: .. cmdv:: Show @ident @@ -565,6 +569,7 @@ Requesting information Show Match nat. .. exn:: Unknown inductive type. + :undocumented: .. cmdv:: Show Universes :name: Show Universes diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 041f1bc966..150aadc15a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -91,6 +91,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: of ``term``. .. exn:: No such binder. + :undocumented: + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are @@ -102,6 +103,7 @@ bindings_list`` where ``bindings_list`` may be of two different forms: are required. .. exn:: Not the right number of missing arguments. + :undocumented: .. _occurrencessets: @@ -589,6 +591,7 @@ Applying theorems :n:`constructor 2 {? with @bindings_list }`. .. exn:: Not an inductive goal with 2 constructors. + :undocumented: .. tacv:: econstructor eexists @@ -1081,8 +1084,8 @@ Managing the local context generated by Coq. .. tacv:: epose (@ident {? @binders} := @term) - .. tacv:: epose term - :name: epose + epose @term + :name: epose; _ While the different variants of :tacn:`pose` expect that no existential variables are generated by the tactic, :tacn:`epose` @@ -1124,7 +1127,7 @@ Managing the local context Controlling the proof flow ------------------------------ -.. tacn:: assert (@ident : form) +.. tacn:: assert (@ident : @type) :name: assert This tactic applies to any goal. :n:`assert (H : U)` adds a new hypothesis @@ -1132,106 +1135,104 @@ Controlling the proof flow :g:`U` [2]_. The subgoal :g:`U` comes first in the list of subgoals remaining to prove. -.. exn:: Not a proposition or a type. + .. exn:: Not a proposition or a type. - Arises when the argument form is neither of type :g:`Prop`, :g:`Set` nor - :g:`Type`. + Arises when the argument :token:`type` is neither of type :g:`Prop`, + :g:`Set` nor :g:`Type`. -.. tacv:: assert form + .. tacv:: assert @type - This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by - Coq. + This behaves as :n:`assert (@ident : @type)` but :n:`@ident` is + generated by Coq. -.. tacv:: assert @form by @tactic + .. tacv:: assert @type by @tactic - This tactic behaves like :n:`assert` but applies tactic to solve the subgoals - generated by assert. + This tactic behaves like :tacn:`assert` but applies tactic to solve the + subgoals generated by assert. - .. exn:: Proof is not complete. - :name: Proof is not complete. (assert) + .. exn:: Proof is not complete. + :name: Proof is not complete. (assert) + :undocumented: -.. tacv:: assert @form as @intro_pattern + .. tacv:: assert @type as @intro_pattern - If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), - the hypothesis is named after this introduction pattern (in particular, if - :n:`intro_pattern` is :n:`@ident`, the tactic behaves like - :n:`assert (@ident : form)`). If :n:`intro_pattern` is an action - introduction pattern, the tactic behaves like :n:`assert form` followed by - the action done by this introduction pattern. + If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`), + the hypothesis is named after this introduction pattern (in particular, if + :n:`intro_pattern` is :n:`@ident`, the tactic behaves like + :n:`assert (@ident : @type)`). If :n:`intro_pattern` is an action + introduction pattern, the tactic behaves like :n:`assert @type` followed by + the action done by this introduction pattern. -.. tacv:: assert @form as @intro_pattern by @tactic + .. tacv:: assert @type as @intro_pattern by @tactic - This combines the two previous variants of :n:`assert`. + This combines the two previous variants of :tacn:`assert`. -.. tacv:: assert (@ident := @term ) + .. tacv:: assert (@ident := @term) - This behaves as :n:`assert (@ident : type) by exact @term` where :g:`type` is - the type of :g:`term`. This is deprecated in favor of :n:`pose proof`. If the - head of term is :n:`@ident`, the tactic behaves as :n:`specialize @term`. + This behaves as :n:`assert (@ident : @type) by exact @term` where + :token:`type` is the type of :token:`term`. This is equivalent to using + :tacn:`pose proof`. If the head of term is :token:`ident`, the tactic + behaves as :tacn:`specialize`. - .. exn:: Variable @ident is already declared. + .. exn:: Variable @ident is already declared. + :undocumented: -.. tacv:: eassert form as intro_pattern by tactic +.. tacv:: eassert @type as @intro_pattern by @tactic :name: eassert -.. tacv:: assert (@ident := @term) - - While the different variants of :n:`assert` expect that no existential - variables are generated by the tactic, :n:`eassert` removes this constraint. + While the different variants of :tacn:`assert` expect that no existential + variables are generated by the tactic, :tacn:`eassert` removes this constraint. This allows not to specify the asserted statement completeley before starting to prove it. -.. tacv:: pose proof @term {? as intro_pattern} +.. tacv:: pose proof @term {? as @intro_pattern} :name: pose proof - This tactic behaves like :n:`assert T {? as intro_pattern} by exact @term` - where :g:`T` is the type of :g:`term`. In particular, + This tactic behaves like :n:`assert @type {? as @intro_pattern} by exact @term` + where :token:`type` is the type of :token:`term`. In particular, :n:`pose proof @term as @ident` behaves as :n:`assert (@ident := @term)` - and :n:`pose proof @term as intro_pattern` is the same as applying the - intro_pattern to :n:`@term`. + and :n:`pose proof @term as @intro_pattern` is the same as applying the + :token:`intro_pattern` to :token:`term`. -.. tacv:: epose proof term {? as intro_pattern} +.. tacv:: epose proof @term {? as @intro_pattern} + :name: epose proof - While :n:`pose proof` expects that no existential variables are generated by - the tactic, :n:`epose proof` removes this constraint. + While :tacn:`pose proof` expects that no existential variables are generated by + the tactic, :tacn:`epose proof` removes this constraint. -.. tacv:: enough (@ident : form) +.. tacv:: enough (@ident : @type) :name: enough - This adds a new hypothesis of name :n:`@ident` asserting :n:`form` to the - goal the tactic :n:`enough` is applied to. A new subgoal stating :n:`form` is - inserted after the initial goal rather than before it as :n:`assert` would do. + This adds a new hypothesis of name :token:`ident` asserting :token:`type` to the + goal the tactic :tacn:`enough` is applied to. A new subgoal stating :token:`type` is + inserted after the initial goal rather than before it as :tacn:`assert` would do. -.. tacv:: enough form +.. tacv:: enough @type - This behaves like :n:`enough (@ident : form)` with the name :n:`@ident` of + This behaves like :n:`enough (@ident : @type)` with the name :token:`ident` of the hypothesis generated by Coq. -.. tacv:: enough form as intro_pattern +.. tacv:: enough @type as @intro_pattern - This behaves like :n:`enough form` using :n:`intro_pattern` to name or + This behaves like :n:`enough @type` using :token:`intro_pattern` to name or destruct the new hypothesis. -.. tacv:: enough (@ident : @form) by @tactic -.. tacv:: enough @form by @tactic -.. tacv:: enough @form as @intro_pattern by @tactic +.. tacv:: enough (@ident : @type) by @tactic + enough @type {? as @intro_pattern } by @tactic - This behaves as above but with :n:`tactic` expected to solve the initial goal - after the extra assumption :n:`form` is added and possibly destructed. If the - :n:`as intro_pattern` clause generates more than one subgoal, :n:`tactic` is + This behaves as above but with :token:`tactic` expected to solve the initial goal + after the extra assumption :token:`type` is added and possibly destructed. If the + :n:`as @intro_pattern` clause generates more than one subgoal, :token:`tactic` is applied to all of them. -.. tacv:: eenough (@ident : form) by tactic - :name: eenough - -.. tacv:: eenough form by tactic +.. tacv:: eenough @type {? as @intro_pattern } {? by @tactic } + eenough (@ident : @type) {? by @tactic } + :name: eenough; _ -.. tacv:: eenough form as intro_pattern by tactic + While the different variants of :tacn:`enough` expect that no existential + variables are generated by the tactic, :tacn:`eenough` removes this constraint. - While the different variants of :n:`enough` expect that no existential - variables are generated by the tactic, :n:`eenough` removes this constraint. - -.. tacv:: cut @form +.. tacv:: cut @type :name: cut This tactic applies to any goal. It implements the non-dependent case of @@ -1240,11 +1241,11 @@ Controlling the proof flow subgoals: :g:`U -> T` and :g:`U`. The subgoal :g:`U -> T` comes first in the list of remaining subgoal to prove. -.. tacv:: specialize (ident {* @term}) {? as intro_pattern} -.. tacv:: specialize ident with @bindings_list {? as intro_pattern} - :name: specialize +.. tacv:: specialize (@ident {* @term}) {? as @intro_pattern} + specialize @ident with @bindings_list {? as @intro_pattern} + :name: specialize; _ - The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The + This tactic works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments :n:`{* @term}` or from a :ref:`bindings list <bindingslist>`. @@ -1254,15 +1255,18 @@ Controlling the proof flow uninstantiated arguments are inferred by unification if possible or left quantified in the hypothesis otherwise. With the :n:`as` clause, the local hypothesis :n:`@ident` is left unchanged and instead, the modified hypothesis - is introduced as specified by the :n:`intro_pattern`. The name :n:`@ident` + is introduced as specified by the :token:`intro_pattern`. The name :n:`@ident` can also refer to a global lemma or hypothesis. In this case, for - compatibility reasons, the behavior of :n:`specialize` is close to that of - :n:`generalize`: the instantiated statement becomes an additional premise of - the goal. The :n:`as` clause is especially useful in this case to immediately + compatibility reasons, the behavior of :tacn:`specialize` is close to that of + :tacn:`generalize`: the instantiated statement becomes an additional premise of + the goal. The ``as`` clause is especially useful in this case to immediately introduce the instantiated statement as a local hypothesis. .. exn:: @ident is used in hypothesis @ident. + :undocumented: + .. exn:: @ident is used in conclusion. + :undocumented: .. tacn:: generalize @term :name: generalize @@ -1343,8 +1347,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) + instantiate ( @num := @term ) in ( value of @ident ) + instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. @@ -1360,13 +1364,13 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. .. tacn:: admit :name: admit -The admit tactic allows temporarily skipping a subgoal so as to -progress further in the rest of the proof. A proof containing admitted -goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. + This tactic allows temporarily skipping a subgoal so as to + progress further in the rest of the proof. A proof containing admitted + goals cannot be closed with :cmd:`Qed` but only with :cmd:`Admitted`. .. tacv:: give_up - Synonym of :n:`admit`. + Synonym of :tacn:`admit`. .. tacn:: absurd @term :name: absurd @@ -1387,7 +1391,8 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. a singleton inductive type (e.g. :g:`True` or :g:`x=x`), or two contradictory hypotheses. -.. exn:: No such assumption. + .. exn:: No such assumption. + :undocumented: .. tacv:: contradiction @ident @@ -1602,6 +1607,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) induction n. .. exn:: Not an inductive product. + :undocumented: .. exn:: Unable to find an instance for the variables @ident ... @ident. @@ -1672,10 +1678,9 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Show 2. .. tacv:: induction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences + einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences -.. tacv:: einduction @term with @bindings_list as @disj_conj_intro_pattern using @term with @bindings_list in @goal_occurrences - - These are the most general forms of ``induction`` and ``einduction``. It combines the + These are the most general forms of :tacn:`induction` and :tacn:`einduction`. It combines the effects of the with, as, using, and in clauses. .. tacv:: elim @term @@ -1709,7 +1714,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) existential variables to be resolved later on. .. tacv:: elim @term using @term -.. tacv:: elim @term using @term with @bindings_list + elim @term using @term with @bindings_list Allows the user to give explicitly an induction principle :n:`@term` that is not the standard one for the underlying inductive type of :n:`@term`. The @@ -1717,15 +1722,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`@term`. .. tacv:: elim @term with @bindings_list using @term with @bindings_list -.. tacv:: eelim @term with @bindings_list using @term with @bindings_list + eelim @term with @bindings_list using @term with @bindings_list - These are the most general forms of ``elim`` and ``eelim``. It combines the + These are the most general forms of :tacn:`elim` and :tacn:`eelim`. It combines the effects of the ``using`` clause and of the two uses of the ``with`` clause. -.. tacv:: elimtype @form +.. tacv:: elimtype @type :name: elimtype - The argument :n:`form` must be inductively defined. :n:`elimtype I` is + The argument :token:`type` must be inductively defined. :n:`elimtype I` is equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the hypothesis :g:`Hn` will not appear in the context(s) of the subgoal(s). Conversely, if :g:`t` is a :n:`@term` of (inductive) type :g:`I` that does @@ -1879,7 +1884,10 @@ and an explanation of the underlying technique. .. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion` .. exn:: Cannot find induction information on @qualid. + :undocumented: + .. exn:: Not the right number of induction arguments. + :undocumented: .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list @@ -1913,7 +1921,10 @@ and an explanation of the underlying technique. :n:`intros until @ident`. .. exn:: No primitive equality found. + :undocumented: + .. exn:: Not a discriminable equality. + :undocumented: .. tacv:: discriminate @num @@ -1927,11 +1938,11 @@ and an explanation of the underlying technique. bindings to instantiate parameters or hypotheses of :n:`@term`. .. tacv:: ediscriminate @num -.. tacv:: ediscriminate @term {? with @bindings_list} - :name: ediscriminate + ediscriminate @term {? with @bindings_list} + :name: ediscriminate; _ - This works the same as ``discriminate`` but if the type of :n:`@term`, or the - type of the hypothesis referred to by :n:`@num`, has uninstantiated + This works the same as :tacn:`discriminate` but if the type of :token:`term`, or the + type of the hypothesis referred to by :token:`num`, has uninstantiated parameters, these parameters are left as existential variables. .. tacv:: discriminate @@ -1942,6 +1953,7 @@ and an explanation of the underlying technique. :n:`intro @ident; discriminate @ident`. .. exn:: No discriminable equalities. + :undocumented: .. tacn:: injection @term :name: injection @@ -1994,9 +2006,16 @@ and an explanation of the underlying technique. context using :n:`intros until @ident`. .. exn:: Not a projectable equality but a discriminable one. - .. exn:: Nothing to do, it is an equality between convertible @terms. + :undocumented: + + .. exn:: Nothing to do, it is an equality between convertible terms. + :undocumented: + .. exn:: Not a primitive equality. + :undocumented: + .. exn:: Nothing to inject. + :undocumented: .. tacv:: injection @num @@ -2010,8 +2029,8 @@ and an explanation of the underlying technique. instantiate parameters or hypotheses of :n:`@term`. .. tacv:: einjection @num - :name: einjection - .. tacv:: einjection @term {? with @bindings_list} + einjection @term {? with @bindings_list} + :name: einjection; _ This works the same as :n:`injection` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated @@ -2023,21 +2042,22 @@ and an explanation of the underlying technique. :n:`intro @ident; injection @ident`. .. exn:: goal does not satisfy the expected preconditions. + :undocumented: .. tacv:: injection @term {? with @bindings_list} as {+ @intro_pattern} - .. tacv:: injection @num as {+ intro_pattern} - .. tacv:: injection as {+ intro_pattern} - .. tacv:: einjection @term {? with @bindings_list} as {+ intro_pattern} - .. tacv:: einjection @num as {+ intro_pattern} - .. tacv:: einjection as {+ intro_pattern} - - These variants apply :n:`intros {+ @intro_pattern}` after the call to - :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in - the context of hypotheses. The number of :n:`@intro_pattern` must not exceed - 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 a hypothesis. + injection @num as {+ intro_pattern} + injection as {+ intro_pattern} + einjection @term {? with @bindings_list} as {+ intro_pattern} + einjection @num as {+ intro_pattern} + einjection as {+ intro_pattern} + + These variants apply :n:`intros {+ @intro_pattern}` after the call to + :tacn:`injection` or :tacn:`einjection` so that all equalities generated are moved in + the context of hypotheses. The number of :n:`@intro_pattern` must not exceed + 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 a hypothesis. .. flag:: Structural Injection @@ -2444,8 +2464,10 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. subgoals. .. exn:: The @term provided does not end with an equation. + :undocumented: .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + :undocumented: .. tacv:: rewrite -> @term @@ -2522,6 +2544,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. :n:`cut @term = @term’; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. .. exn:: Terms do not have convertible types. + :undocumented: .. tacv:: replace @term with @term’ by @tactic @@ -2544,8 +2567,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. the form :n:`@term’ = @term` .. tacv:: replace @term {? with @term} in clause {? by @tactic} - .. tacv:: replace -> @term in clause - .. tacv:: replace <- @term in clause + replace -> @term in clause + replace <- @term in clause Acts as before but the replacements take place in the specified clause (see :ref:`performingcomputations`) and not only in the conclusion of the goal. The @@ -2658,6 +2681,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. convertible. .. exn:: Not convertible. + :undocumented: .. tacv:: change @term with @term’ @@ -2670,6 +2694,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. .. exn:: Too few occurrences. + :undocumented: .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident @@ -2712,12 +2737,9 @@ following: For backward compatibility, the notation :n:`in {+ @ident}` performs the conversion in hypotheses :n:`{+ @ident}`. -.. tacn:: cbv {* flag} - :name: cbv -.. tacn:: lazy {* flag} - :name: lazy -.. tacn:: compute - :name: compute +.. tacn:: cbv {* @flag} + lazy {* @flag} + :name: cbv; lazy These parameterized reduction tactics apply to any goal and perform the normalization of the goal according to the specified flags. In @@ -2765,7 +2787,8 @@ the conversion in hypotheses :n:`{+ @ident}`. evaluating purely computational expressions (i.e. with little dead code). .. tacv:: compute -.. tacv:: cbv + cbv + :name: compute; _ These are synonyms for ``cbv beta delta iota zeta``. @@ -2774,17 +2797,17 @@ the conversion in hypotheses :n:`{+ @ident}`. This is a synonym for ``lazy beta delta iota zeta``. .. tacv:: compute {+ @qualid} -.. tacv:: cbv {+ @qualid} + cbv {+ @qualid} These are synonyms of :n:`cbv beta delta {+ @qualid} iota zeta`. .. tacv:: compute -{+ @qualid} -.. tacv:: cbv -{+ @qualid} + cbv -{+ @qualid} These are synonyms of :n:`cbv beta delta -{+ @qualid} iota zeta`. .. tacv:: lazy {+ @qualid} -.. tacv:: lazy -{+ @qualid} + lazy -{+ @qualid} These are respectively synonyms of :n:`lazy beta delta {+ @qualid} iota zeta` and :n:`lazy beta delta -{+ @qualid} iota zeta`. @@ -2864,9 +2887,8 @@ the conversion in hypotheses :n:`{+ @ident}`. on transparency and opacity). .. tacn:: cbn - :name: cbn -.. tacn:: simpl - :name: simpl + simpl + :name: cbn; simpl These tactics apply to any goal. They try to reduce a term to something still readable instead of fully normalizing it. They perform @@ -2962,7 +2984,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :g:`succ t` is reduced to :g:`S t`. .. tacv:: cbn {+ @qualid} -.. tacv:: cbn -{+ @qualid} + cbn -{+ @qualid} These are respectively synonyms of :n:`cbn beta delta {+ @qualid} iota zeta` and :n:`cbn beta delta -{+ @qualid} iota zeta` (see :tacn:`cbn`). @@ -2978,16 +3000,17 @@ the conversion in hypotheses :n:`{+ @ident}`. matching :n:`@pattern` in the current goal. .. exn:: Too few occurrences. + :undocumented: .. tacv:: simpl @qualid -.. tacv:: simpl @string + simpl @string - This applies ``simpl`` only to the applicative subterms whose head occurrence + This applies :tacn:`simpl` only to the applicative subterms whose head occurrence is the unfoldable constant :n:`@qualid` (the constant can be referred to by its notation using :n:`@string` if such a notation exists). .. tacv:: simpl @qualid at {+ @num} -.. tacv:: simpl @string at {+ @num} + simpl @string at {+ @num} This applies ``simpl`` only to the :n:`{+ @num}` applicative subterms whose head occurrence is :n:`@qualid` (or :n:`@string`). @@ -3008,6 +3031,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :math:`\beta`:math:`\iota`-normal form. .. exn:: @qualid does not denote an evaluable constant. + :undocumented: .. tacv:: unfold @qualid in @ident @@ -3025,8 +3049,10 @@ the conversion in hypotheses :n:`{+ @ident}`. unfolded. Occurrences are located from left to right. .. exn:: Bad occurrence number of @qualid. + :undocumented: .. exn:: @qualid does not occur. + :undocumented: .. tacv:: unfold @string @@ -3117,6 +3143,7 @@ Conversion tactics applied to hypotheses Example: :n:`unfold not in (type of H1) (type of H3)`. .. exn:: No such hypothesis: @ident. + :undocumented: .. _automation: @@ -3127,38 +3154,41 @@ Automation .. tacn:: auto :name: auto -This tactic implements a Prolog-like resolution procedure to solve the -current goal. It first tries to solve the goal using the assumption -tactic, then it reduces the goal to an atomic one using intros and -introduces the newly generated hypotheses as hints. Then it looks at -the list of tactics associated to the head symbol of the goal and -tries to apply one of them (starting from the tactics with lower -cost). This process is recursively applied to the generated subgoals. + This tactic implements a Prolog-like resolution procedure to solve the + current goal. It first tries to solve the goal using the assumption + tactic, then it reduces the goal to an atomic one using intros and + introduces the newly generated hypotheses as hints. Then it looks at + the list of tactics associated to the head symbol of the goal and + tries to apply one of them (starting from the tactics with lower + cost). This process is recursively applied to the generated subgoals. -By default, auto only uses the hypotheses of the current goal and the -hints of the database named core. + By default, auto only uses the hypotheses of the current goal and the + hints of the database named core. .. tacv:: auto @num - Forces the search depth to be :n:`@num`. The maximal search depth - is `5` by default. + Forces the search depth to be :token:`num`. The maximal search depth + is 5 by default. .. tacv:: auto with {+ @ident} - Uses the hint databases :n:`{+ @ident}` in addition to the database core. See - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of - pre-defined databases and the way to create or extend a database. + Uses the hint databases :n:`{+ @ident}` in addition to the database core. + + .. seealso:: + :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of + pre-defined databases and the way to create or extend a database. .. tacv:: auto with * - Uses all existing hint databases. See - :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` + Uses all existing hint databases. + + .. seealso:: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` -.. tacv:: auto using {+ @lemma} +.. tacv:: auto using {+ @ident__i} {? with {+ @ident } } - Uses :n:`{+ @lemma}` in addition to hints (can be combined with the with - :n:`@ident` option). If :n:`@lemma` is an inductive type, it is the - collection of its constructors which is added as hints. + Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + inductive type, it is the collection of its constructors which are added + as hints. .. tacv:: info_auto @@ -3184,13 +3214,24 @@ hints of the database named core. equalities like :g:`X=X`. .. tacv:: trivial with {+ @ident} + :undocumented: + .. tacv:: trivial with * + :undocumented: + .. tacv:: trivial using {+ @lemma} + :undocumented: + .. tacv:: debug trivial :name: debug trivial + :undocumented: + .. tacv:: info_trivial :name: info_trivial + :undocumented: + .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + :undocumented: .. note:: :tacn:`auto` either solves completely the goal or else leaves it @@ -3210,26 +3251,26 @@ the :tacn:`auto` and :tacn:`trivial` tactics: .. tacn:: eauto :name: eauto -This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try -resolution hints which would leave existential variables in the goal, -:tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` -where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` -can solve such a goal: + This tactic generalizes :tacn:`auto`. While :tacn:`auto` does not try + resolution hints which would leave existential variables in the goal, + :tacn:`eauto` does try them (informally speaking, it usessimple :tacn:`eapply` + where :tacn:`auto` uses simple :tacn:`apply`). As a consequence, :tacn:`eauto` + can solve such a goal: -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Hint Resolve ex_intro. - Goal forall P:nat -> Prop, P 0 -> exists n, P n. - eauto. + Hint Resolve ex_intro. + Goal forall P:nat -> Prop, P 0 -> exists n, P n. + eauto. -Note that ``ex_intro`` should be declared as a hint. + Note that ``ex_intro`` should be declared as a hint. .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} - The various options for eauto are the same as for auto. + The various options for :tacn:`eauto` are the same as for :tacn:`auto`. :tacn:`eauto` also obeys the following options: @@ -3243,13 +3284,12 @@ Note that ``ex_intro`` should be declared as a hint. .. tacn:: autounfold with {+ @ident} :name: autounfold - -This tactic unfolds constants that were declared through a ``Hint Unfold`` -in the given databases. + This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` + in the given databases. .. tacv:: autounfold with {+ @ident} in clause - Performs the unfolding in the given clause. + Performs the unfolding in the given clause. .. tacv:: autounfold with * @@ -3258,18 +3298,18 @@ in the given databases. .. tacn:: autorewrite with {+ @ident} :name: autorewrite -This tactic [4]_ carries out rewritings according to the rewriting rule -bases :n:`{+ @ident}`. + This tactic [4]_ carries out rewritings according to the rewriting rule + bases :n:`{+ @ident}`. -Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until -it fails. Once all the rules have been processed, if the main subgoal has -progressed (e.g., if it is distinct from the initial main goal) then the rules -of this base are processed again. If the main subgoal has not progressed then -the next base is processed. For the bases, the behavior is exactly similar to -the processing of the rewriting rules. + Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until + it fails. Once all the rules have been processed, if the main subgoal has + progressed (e.g., if it is distinct from the initial main goal) then the rules + of this base are processed again. If the main subgoal has not progressed then + the next base is processed. For the bases, the behavior is exactly similar to + the processing of the rewriting rules. -The rewriting rule bases are built with the ``Hint Rewrite vernacular`` -command. + The rewriting rule bases are built with the :cmd:`Hint Rewrite` + command. .. warning:: @@ -3435,6 +3475,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is itself. .. exn:: @term cannot be used as a hint + :undocumented: .. cmdv:: Immediate {+ @term} @@ -3448,6 +3489,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. .. exn:: @ident is not an inductive type + :undocumented: .. cmdv:: Hint Constructors {+ @ident} @@ -3616,16 +3658,16 @@ use one or several databases specific to your development. .. cmd:: Remove Hints {+ @term} : {+ @ident} -This command removes the hints associated to terms :n:`{+ @term}` in databases -:n:`{+ @ident}`. + This command removes the hints associated to terms :n:`{+ @term}` in databases + :n:`{+ @ident}`. .. _printhint: .. cmd:: Print Hint -This command displays all hints that apply to the current goal. It -fails if no proof is being edited, while the two variants can be used -at every moment. + This command displays all hints that apply to the current goal. It + fails if no proof is being edited, while the two variants can be used + at every moment. **Variants:** @@ -3753,17 +3795,17 @@ Decision procedures .. tacn:: tauto :name: tauto -This tactic implements a decision procedure for intuitionistic propositional -calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff -:cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an -intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and -logical equivalence but does not unfold any other definition. - -The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would -fail: + This tactic implements a decision procedure for intuitionistic propositional + calculus based on the contraction-free sequent calculi LJT* of Roy Dyckhoff + :cite:`Dyc92`. Note that :tacn:`tauto` succeeds on any instance of an + intuitionistic tautological proposition. :tacn:`tauto` unfolds negations and + logical equivalence but does not unfold any other definition. .. example:: + The following goal can be proved by :tacn:`tauto` whereas :tacn:`auto` would + fail: + .. coqtop:: reset all Goal forall (x:nat) (P:nat -> Prop), x = 0 \/ P x -> x <> 0 -> P x. @@ -3799,27 +3841,24 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. .. tacn:: intuition @tactic :name: intuition -The tactic :tacn:`intuition` takes advantage of the search-tree built by the -decision procedure involved in the tactic :tacn:`tauto`. It uses this -information to generate a set of subgoals equivalent to the original one (but -simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If -this tactic fails on some goals then :tacn:`intuition` fails. In fact, -:tacn:`tauto` is simply :g:`intuition fail`. + The tactic :tacn:`intuition` takes advantage of the search-tree built by the + decision procedure involved in the tactic :tacn:`tauto`. It uses this + information to generate a set of subgoals equivalent to the original one (but + simpler than it) and applies the tactic :n:`@tactic` to them :cite:`Mun94`. If + this tactic fails on some goals then :tacn:`intuition` fails. In fact, + :tacn:`tauto` is simply :g:`intuition fail`. -For instance, the tactic :g:`intuition auto` applied to the goal - -:: - - (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O + .. example:: + For instance, the tactic :g:`intuition auto` applied to the goal:: -internally replaces it by the equivalent one: -:: + (forall (x:nat), P x) /\ B -> (forall (y:nat), P y) /\ P O \/ B /\ P O - (forall (x:nat), P x), B |- P O + internally replaces it by the equivalent one:: + (forall (x:nat), P x), B |- P O -and then uses :tacn:`auto` which completes the proof. + and then uses :tacn:`auto` which completes the proof. Originally due to César Muñoz, these tactics (:tacn:`tauto` and :tacn:`intuition`) have been completely re-engineered by David Delahaye using @@ -3849,25 +3888,25 @@ some incompatibilities. .. tacn:: rtauto :name: rtauto -The :tacn:`rtauto` tactic solves propositional tautologies similarly to what -:tacn:`tauto` does. The main difference is that the proof term is built using a -reflection scheme applied to a sequent calculus proof of the goal. The search -procedure is also implemented using a different technique. + The :tacn:`rtauto` tactic solves propositional tautologies similarly to what + :tacn:`tauto` does. The main difference is that the proof term is built using a + reflection scheme applied to a sequent calculus proof of the goal. The search + procedure is also implemented using a different technique. -Users should be aware that this difference may result in faster proof-search -but slower proof-checking, and :tacn:`rtauto` might not solve goals that -:tacn:`tauto` would be able to solve (e.g. goals involving universal -quantifiers). + Users should be aware that this difference may result in faster proof-search + but slower proof-checking, and :tacn:`rtauto` might not solve goals that + :tacn:`tauto` would be able to solve (e.g. goals involving universal + quantifiers). -Note that this tactic is only available after a ``Require Import Rtauto``. + Note that this tactic is only available after a ``Require Import Rtauto``. .. tacn:: firstorder :name: firstorder -The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to -first- order reasoning, written by Pierre Corbineau. It is not restricted to -usual logical connectives but instead may reason about any first-order class -inductive definition. + The tactic :tacn:`firstorder` is an experimental extension of :tacn:`tauto` to + first- order reasoning, written by Pierre Corbineau. It is not restricted to + usual logical connectives but instead may reason about any first-order class + inductive definition. .. opt:: Firstorder Solver @tactic :name: Firstorder Solver @@ -3906,20 +3945,20 @@ inductive definition. .. tacn:: congruence :name: congruence -The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard -Nelson and Oppen congruence closure algorithm, which is a decision procedure -for ground equalities with uninterpreted symbols. It also includes -constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal -is a non-quantified equality, congruence tries to prove it with non-quantified -equalities in the context. Otherwise it tries to infer a discriminable equality -from those in the context. Alternatively, congruence tries to prove that a -hypothesis is equal to the goal or to the negation of another hypothesis. - -:tacn:`congruence` is also able to take advantage of hypotheses stating -quantified equalities, but you have to provide a bound for the number of extra -equalities generated that way. Please note that one of the sides of the -equality must contain all the quantified variables in order for congruence to -match against it. + The tactic :tacn:`congruence`, by Pierre Corbineau, implements the standard + Nelson and Oppen congruence closure algorithm, which is a decision procedure + for ground equalities with uninterpreted symbols. It also includes + constructor theory (see :tacn:`injection` and :tacn:`discriminate`). If the goal + is a non-quantified equality, congruence tries to prove it with non-quantified + equalities in the context. Otherwise it tries to infer a discriminable equality + from those in the context. Alternatively, congruence tries to prove that a + hypothesis is equal to the goal or to the negation of another hypothesis. + + :tacn:`congruence` is also able to take advantage of hypotheses stating + quantified equalities, but you have to provide a bound for the number of extra + equalities generated that way. Please note that one of the sides of the + equality must contain all the quantified variables in order for congruence to + match against it. .. example:: @@ -3980,7 +4019,10 @@ succeeds, and results in an error otherwise. conversion, casts and universe constraints. It may unify universes. .. exn:: Not equal. + :undocumented: + .. exn:: Not equal (due to universes). + :undocumented: .. tacn:: constr_eq_strict @term @term :name: constr_eq_strict @@ -3990,7 +4032,10 @@ succeeds, and results in an error otherwise. constraints. .. exn:: Not equal. + :undocumented: + .. exn:: Not equal (due to universes). + :undocumented: .. tacn:: unify @term @term :name: unify @@ -3999,6 +4044,7 @@ succeeds, and results in an error otherwise. instantiating existential variables. .. exn:: Unable to unify @term with @term. + :undocumented: .. tacv:: unify @term @term with @ident @@ -4013,6 +4059,7 @@ succeeds, and results in an error otherwise. by :tacn:`eapply` and some other tactics. .. exn:: Not an evar. + :undocumented: .. tacn:: has_evar @term :name: has_evar @@ -4022,6 +4069,7 @@ succeeds, and results in an error otherwise. scans all subterms, including those under binders. .. exn:: No evars. + :undocumented: .. tacn:: is_var @term :name: is_var @@ -4030,6 +4078,7 @@ succeeds, and results in an error otherwise. the current goal context or in the opened sections. .. exn:: Not a variable or hypothesis. + :undocumented: .. _equality: @@ -4041,45 +4090,46 @@ Equality .. tacn:: f_equal :name: f_equal -This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n` -:g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`. Using :tacn:`f_equal` on such a goal -leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up -to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones -(e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically -solved by :tacn:`f_equal`. + This tactic applies to a goal of the form :g:`f a`:sub:`1` :g:`... a`:sub:`n` + :g:`= f′a′`:sub:`1` :g:`... a′`:sub:`n`. Using :tacn:`f_equal` on such a goal + leads to subgoals :g:`f=f′` and :g:`a`:sub:`1` = :g:`a′`:sub:`1` and so on up + to :g:`a`:sub:`n` :g:`= a′`:sub:`n`. Amongst these subgoals, the simple ones + (e.g. provable by :tacn:`reflexivity` or :tacn:`congruence`) are automatically + solved by :tacn:`f_equal`. .. tacn:: reflexivity :name: reflexivity -This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` -and `u` are convertible and then solves the goal. It is equivalent to -``apply refl_equal``. + This tactic applies to a goal that has the form :g:`t=u`. It checks that `t` + and `u` are convertible and then solves the goal. It is equivalent to + ``apply refl_equal``. -.. exn:: The conclusion is not a substitutive equation. + .. exn:: The conclusion is not a substitutive equation. + :undocumented: -.. exn:: Unable to unify ... with ... + .. exn:: Unable to unify ... with ... + :undocumented: .. tacn:: symmetry :name: symmetry -This tactic applies to a goal that has the form :g:`t=u` and changes it into -:g:`u=t`. + This tactic applies to a goal that has the form :g:`t=u` and changes it into + :g:`u=t`. .. tacv:: symmetry in @ident - If the statement of the hypothesis ident has the form :g:`t=u`, the tactic - changes it to :g:`u=t`. - + If the statement of the hypothesis ident has the form :g:`t=u`, the tactic + changes it to :g:`u=t`. .. tacn:: transitivity @term :name: transitivity -This tactic applies to a goal that has the form :g:`t=u` and transforms it -into the two subgoals :n:`t=@term` and :n:`@term=u`. + This tactic applies to a goal that has the form :g:`t=u` and transforms it + into the two subgoals :n:`t=@term` and :n:`@term=u`. Equality and inductive sets @@ -4133,10 +4183,10 @@ symbol :g:`=`. instantiate parameters or hypotheses of :n:`@term`. .. tacv:: esimplify_eq @num -.. tacv:: esimplify_eq @term {? with @bindings_list} - :name: esimplify_eq + esimplify_eq @term {? with @bindings_list} + :name: esimplify_eq; _ - This works the same as ``simplify_eq`` but if the type of :n:`@term`, or the + This works the same as :tacn:`simplify_eq` but if the type of :n:`@term`, or the type of the hypothesis referred to by :n:`@num`, has uninstantiated parameters, these parameters are left as existential variables. @@ -4168,35 +4218,35 @@ Inversion .. tacn:: functional inversion @ident :name: functional inversion -:tacn:`functional inversion` is a tactic that performs inversion on hypothesis -:n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid -{+ @term}` where :n:`@qualid` must have been defined using Function (see -:ref:`advanced-recursive-functions`). Note that this tactic is only -available after a ``Require Import FunInd``. + :tacn:`functional inversion` is a tactic that performs inversion on hypothesis + :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid + {+ @term}` where :n:`@qualid` must have been defined using Function (see + :ref:`advanced-recursive-functions`). Note that this tactic is only + available after a ``Require Import FunInd``. + .. exn:: Hypothesis @ident must contain at least one Function. + :undocumented: -.. exn:: Hypothesis @ident must contain at least one Function. -.. exn:: Cannot find inversion information for hypothesis @ident. + .. exn:: Cannot find inversion information for hypothesis @ident. - This error may be raised when some inversion lemma failed to be generated by - Function. + This error may be raised when some inversion lemma failed to be generated by + Function. -.. tacv:: functional inversion @num + .. tacv:: functional inversion @num - 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. + 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 + .. tacv:: functional inversion @ident @qualid + functional inversion @num @qualid - If the hypothesis :n:`@ident` (or :n:`@num`) has a type of the form - :n:`@qualid`:sub:`1` :n:`@term`:sub:`1` ... :n:`@term`:sub:`n` :n:`= - @qualid`:sub:`2` :n:`@term`:sub:`n+1` ... :n:`@term`:sub:`n+m` where - :n:`@qualid`:sub:`1` and :n:`@qualid`:sub:`2` are valid candidates to - functional inversion, this variant allows choosing which :n:`@qualid` is - inverted. + If the hypothesis :token:`ident` (or :token:`num`) has a type of the form + :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where + :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to + functional inversion, this variant allows choosing which :token:`qualid` + is inverted. Classical tactics ----------------- @@ -4206,15 +4256,14 @@ loaded. A few more tactics are available. Make sure to load the module using the ``Require Import`` command. .. tacn:: classical_left - :name: classical_left -.. tacv:: classical_right - :name: classical_right + classical_right + :name: classical_left; classical_right - The tactics ``classical_left`` and ``classical_right`` are the analog of the - left and right but using classical logic. They can only be used for - disjunctions. Use ``classical_left`` to prove the left part of the + These tactics are the analog of :tacn:`left` and :tacn:`right` + but using classical logic. They can only be used for + disjunctions. Use :tacn:`classical_left` to prove the left part of the disjunction with the assumption that the negation of right part holds. - Use ``classical_right`` to prove the right part of the disjunction with + Use :tacn:`classical_right` to prove the right part of the disjunction with the assumption that the negation of left part holds. .. _tactics-automating: @@ -4226,93 +4275,92 @@ Automating .. tacn:: btauto :name: btauto -The tactic :tacn:`btauto` implements a reflexive solver for boolean -tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are -constructed over the following grammar: + The tactic :tacn:`btauto` implements a reflexive solver for boolean + tautologies. It solves goals of the form :g:`t = u` where `t` and `u` are + constructed over the following grammar: -.. _btauto_grammar: + .. _btauto_grammar: - .. productionlist:: `sentence` - t : x - :∣ true - :∣ false - :∣ orb t1 t2 - :∣ andb t1 t2 - :∣ xorb t1 t2 - :∣ negb t - :∣ if t1 then t2 else t3 + .. productionlist:: `sentence` + t : x + :∣ true + :∣ false + :∣ orb t1 t2 + :∣ andb t1 t2 + :∣ xorb t1 t2 + :∣ negb t + :∣ if t1 then t2 else t3 - Whenever the formula supplied is not a tautology, it also provides a - counter-example. + Whenever the formula supplied is not a tautology, it also provides a + counter-example. - Internally, it uses a system very similar to the one of the ring - tactic. + Internally, it uses a system very similar to the one of the ring + tactic. - Note that this tactic is only available after a ``Require Import Btauto``. + Note that this tactic is only available after a ``Require Import Btauto``. -.. exn:: Cannot recognize a boolean equality. + .. exn:: Cannot recognize a boolean equality. - The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` - doesn't introduce variables into the context on its own. + The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` + doesn't introduce variables into the context on its own. .. tacn:: omega :name: omega -The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision -procedure for Presburger arithmetic. It solves quantifier-free -formulas built with `~`, `\/`, `/\`, `->` on top of equalities, -inequalities and disequalities on both the type :g:`nat` of natural numbers -and :g:`Z` of binary integers. This tactic must be loaded by the command -``Require Import Omega``. See the additional documentation about omega -(see Chapter :ref:`omega`). + The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision + procedure for Presburger arithmetic. It solves quantifier-free + formulas built with `~`, `\/`, `/\`, `->` on top of equalities, + inequalities and disequalities on both the type :g:`nat` of natural numbers + and :g:`Z` of binary integers. This tactic must be loaded by the command + ``Require Import Omega``. See the additional documentation about omega + (see Chapter :ref:`omega`). .. tacn:: ring :name: ring + + This tactic solves equations upon polynomial expressions of a ring + (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. + .. tacn:: ring_simplify {+ @term} :name: ring_simplify -The :n:`ring` tactic solves equations upon polynomial expressions of a ring -(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. - -:n:`ring_simplify` applies the normalization procedure described above to -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 -sides are normalized. + This tactic applies the normalization procedure described above to + 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 + sides are normalized. See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to declare new ring structures. All declared field structures can be printed with the ``Print Rings`` command. .. tacn:: field - :name: field -.. tacn:: field_simplify {+ @term} - :name: field_simplify -.. tacn:: field_simplify_eq - :name: field_simplify_eq - -The field tactic is built on the same ideas as ring: this is a -reflexive tactic that solves or simplifies equations in a field -structure. The main idea is to reduce a field expression (which is an -extension of ring expressions with the inverse and division -operations) to a fraction made of two polynomial expressions. - -Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` -replaces the provided terms by their reduced fraction. -:n:`field_simplify_eq` applies when the conclusion is an equation: it -simplifies both hand sides and multiplies so as to cancel -denominators. So it produces an equation without division nor inverse. - -All of these 3 tactics may generate a subgoal in order to prove that -denominators are different from zero. - -See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to -declare new field structures. All declared field structures can be -printed with the Print Fields command. + field_simplify {+ @term} + field_simplify_eq + :name: field; field_simplify; field_simplify_eq + + The field tactic is built on the same ideas as ring: this is a + reflexive tactic that solves or simplifies equations in a field + structure. The main idea is to reduce a field expression (which is an + extension of ring expressions with the inverse and division + operations) to a fraction made of two polynomial expressions. + + Tactic :n:`field` is used to solve subgoals, whereas :n:`field_simplify {+ @term}` + replaces the provided terms by their reduced fraction. + :n:`field_simplify_eq` applies when the conclusion is an equation: it + simplifies both hand sides and multiplies so as to cancel + denominators. So it produces an equation without division nor inverse. + + All of these 3 tactics may generate a subgoal in order to prove that + denominators are different from zero. + + See :ref:`Theringandfieldtacticfamilies` for more information on the tactic and how to + declare new field structures. All declared field structures can be + printed with the Print Fields command. .. example:: @@ -4373,16 +4421,16 @@ Non-logical tactics .. tacn:: revgoals :name: revgoals -This tactics reverses the list of the focused goals. + This tactics reverses the list of the focused goals. -.. example:: + .. example:: - .. coqtop:: all reset + .. coqtop:: all reset - Parameter P : nat -> Prop. - Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. - repeat split. - all: revgoals. + Parameter P : nat -> Prop. + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. + repeat split. + all: revgoals. .. tacn:: shelve :name: shelve diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a69cf209c7..4bc85f386d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -20,10 +20,13 @@ Displaying Error messages: .. exn:: @qualid not a defined object. + :undocumented: .. exn:: Universe instance should have length @num. + :undocumented: .. exn:: This object does not support universe names. + :undocumented: .. cmdv:: Print Term @qualid @@ -81,9 +84,9 @@ and tables: * A :production:`flag` has a boolean value, such as :flag:`Asymmetric Patterns`. * An :production:`option` generally has a numeric or string value, such as :opt:`Firstorder Depth`. * A :production:`table` contains a set of strings or qualids. -* In addition, some commands provide settings, such as :cmd:`Extraction Language OCaml`. +* In addition, some commands provide settings, such as :cmd:`Extraction Language`. -.. FIXME Convert `Extraction Language OCaml` to an option. +.. FIXME Convert "Extraction Language" to an option. Flags, options and tables are identified by a series of identifiers, each with an initial capital letter. @@ -538,8 +541,7 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard will use the default extension ``.v``. .. cmdv:: Load Verbose @ident - - .. cmdv:: Load Verbose @string + Load Verbose @string Display, while loading, the answers of |Coq| to each command (including tactics) contained in @@ -548,10 +550,13 @@ toplevel. This kind of file is called a *script* for |Coq|. The standard .. seealso:: Section :ref:`controlling-display`. .. exn:: Can’t find file @ident on loadpath. + :undocumented: .. exn:: Load is not supported inside proofs. + :undocumented: .. exn:: Files processed by Load cannot leave open proofs. + :undocumented: .. _compiled-files: @@ -620,6 +625,7 @@ file is a particular case of module called *library file*. comes from a given package by making explicit its absolute root. .. exn:: Cannot load qualid: no physical path bound to dirpath. + :undocumented: .. exn:: Cannot find library foo in loadpath. @@ -684,8 +690,10 @@ file is a particular case of module called *library file*. where they occur, even if outside a section. .. exn:: File not found on loadpath: @string. + :undocumented: .. exn:: Loading of ML object file forbidden in a native Coq. + :undocumented: .. cmd:: Print ML Modules @@ -812,6 +820,7 @@ interactively, they cannot be part of a vernacular file loaded via over the name of a module or of an object inside a module. .. exn:: @ident: no such entry. + :undocumented: .. cmdv:: Reset Initial @@ -953,6 +962,7 @@ Quitting and debugging it prints a message indicating that the failure did not occur. .. exn:: The command has not failed! + :undocumented: .. _controlling-display: @@ -1136,6 +1146,7 @@ described first. variable nor a constant. .. exn:: The reference is not unfoldable. + :undocumented: .. cmdv:: Print Strategies @@ -1166,41 +1177,41 @@ Controlling the locality of commands .. cmd:: Local @command -.. cmd:: Global @command - -Some commands support a Local or Global prefix modifier to control the -scope of their effect. There are four kinds of commands: - - -+ Commands whose default is to extend their effect both outside the - section and the module or library file they occur in. For these - commands, the Local modifier limits the effect of the command to the - current section or module it occurs in. As an example, the :cmd:`Coercion` - and :cmd:`Strategy` commands belong to this category. -+ Commands whose default behavior is to stop their effect at the end - of the section they occur in but to extend their effect outside the module or - library file they occur in. For these commands, the Local modifier limits the - effect of the command to the current module if the command does not occur in a - section and the Global modifier extends the effect outside the current - sections and current module if the command occurs in a section. As an example, - the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong - to this category. Notice that a subclass of these commands do not support - extension of their scope outside sections at all and the Global modifier is not - applicable to them. -+ Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the ``Global`` - modifier extends their effect outside the sections and modules they - occur in. The :cmd:`Transparent` and :cmd:`Opaque` - (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands - belong to this category. -+ Commands whose default behavior is to extend their effect outside - sections but not outside modules when they occur in a section and to - extend their effect outside the module or library file they occur in - when no section contains them.For these commands, the Local modifier - limits the effect to the current section or module while the Global - modifier extends the effect outside the module even when the command - occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this - category. + Global @command + + Some commands support a Local or Global prefix modifier to control the + scope of their effect. There are four kinds of commands: + + + + Commands whose default is to extend their effect both outside the + section and the module or library file they occur in. For these + commands, the Local modifier limits the effect of the command to the + current section or module it occurs in. As an example, the :cmd:`Coercion` + and :cmd:`Strategy` commands belong to this category. + + Commands whose default behavior is to stop their effect at the end + of the section they occur in but to extend their effect outside the module or + library file they occur in. For these commands, the Local modifier limits the + effect of the command to the current module if the command does not occur in a + section and the Global modifier extends the effect outside the current + sections and current module if the command occurs in a section. As an example, + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + to this category. Notice that a subclass of these commands do not support + extension of their scope outside sections at all and the Global modifier is not + applicable to them. + + Commands whose default behavior is to stop their effect at the end + of the section or module they occur in. For these commands, the ``Global`` + modifier extends their effect outside the sections and modules they + occur in. The :cmd:`Transparent` and :cmd:`Opaque` + (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + belong to this category. + + Commands whose default behavior is to extend their effect outside + sections but not outside modules when they occur in a section and to + extend their effect outside the module or library file they occur in + when no section contains them.For these commands, the Local modifier + limits the effect to the current section or module while the Global + modifier extends the effect outside the module even when the command + occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this + category. .. _exposing-constants-to-ocaml-libraries: diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 8f76085d88..418922e9b3 100644 --- a/doc/sphinx/user-extensions/proof-schemes.rst +++ b/doc/sphinx/user-extensions/proof-schemes.rst @@ -12,7 +12,7 @@ The ``Scheme`` command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. Its syntax follows the schema: -.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort sort {* with @ident__i := Induction for @ident__j Sort sort} +.. cmd:: Scheme @ident__1 := Induction for @ident__2 Sort @sort {* with @ident__i := Induction for @ident__j Sort @sort} This command is a high-level tool for generating automatically (possibly mutual) induction principles for given types and sorts. @@ -22,10 +22,10 @@ syntax follows the schema: definitions. Each term :n:`@ident__i` proves a general principle of mutual induction for objects in type :n:`@ident__j`. -.. cmdv:: Scheme @ident := Minimality for @ident Sort sort {* with @ident := Minimality for @ident' Sort sort} +.. cmdv:: Scheme @ident := Minimality for @ident Sort @sort {* with @ident := Minimality for @ident' Sort @sort} - Same as before but defines a non-dependent elimination principle more - natural in case of inductively defined relations. + Same as before but defines a non-dependent elimination principle more + natural in case of inductively defined relations. .. cmdv:: Scheme Equality for @ident :name: Scheme Equality @@ -33,7 +33,7 @@ syntax follows the schema: Tries to generate a Boolean equality and a proof of the decidability of the usual equality. If `ident` involves some other inductive types, their equality has to be defined first. -.. cmdv:: Scheme Induction for @ident Sort sort {* with Induction for @ident Sort sort} +.. cmdv:: Scheme Induction for @ident Sort @sort {* with Induction for @ident Sort @sort} If you do not provide the name of the schemes, they will be automatically computed from the sorts involved (works also with Minimality). @@ -195,19 +195,18 @@ Combined Scheme Generation of induction principles with ``Functional`` ``Scheme`` ----------------------------------------------------------------- -The ``Functional Scheme`` command is a high-level experimental tool for -generating automatically induction principles corresponding to -(possibly mutually recursive) functions. First, it must be made -available via ``Require Import FunInd``. Its syntax then follows the -schema: -.. cmd:: Functional Scheme @ident := Induction for ident' Sort sort {* with @ident := Induction for @ident Sort sort} +.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort} -where each `ident'ᵢ` is a different mutually defined function -name (the names must be in the same order as when they were defined). This -command generates the induction principle for each `identᵢ`, following -the recursive structure and case analyses of the corresponding function -identᵢ’. + This command is a high-level experimental tool for + generating automatically induction principles corresponding to + (possibly mutually recursive) functions. First, it must be made + available via ``Require Import FunInd``. + Each :n:`@ident__i` is a different mutually defined function + name (the names must be in the same order as when they were defined). This + command generates the induction principle for each :n:`@ident__i`, following + the recursive structure and case analyses of the corresponding function + :n:`@ident__i'`. .. warning:: @@ -349,17 +348,17 @@ Generation of inversion principles with ``Derive`` ``Inversion`` :g:`inversion`. -.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort sort +.. cmdv:: Derive Inversion_clear @ident with forall (x:T), I t Sort @sort When applied, it is equivalent to having inverted the instance with the tactic inversion replaced by the tactic `inversion_clear`. -.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort sort +.. cmdv:: Derive Dependent Inversion @ident with forall (x:T), I t Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion`. -.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort sort +.. cmdv:: Derive Dependent Inversion_clear @ident with forall(x:T), I t Sort @sort When applied, it is equivalent to having inverted the instance with the tactic `dependent inversion_clear`. @@ -377,8 +376,8 @@ Generation of inversion principles with ``Derive`` ``Inversion`` Parameter P : nat -> nat -> Prop. - To generate the inversion lemma for the instance `(Le (S n) m)` and the - sort `Prop`, we do: + To generate the inversion lemma for the instance :g:`(Le (S n) m)` and the + sort :g:`Prop`, we do: .. coqtop:: all diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 2214cbfb34..65df89da6c 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -31,8 +31,8 @@ Basic notations .. cmd:: Notation -A *notation* is a symbolic expression denoting some term or term -pattern. + A *notation* is a symbolic expression denoting some term or term + pattern. A typical notation is the use of the infix symbol ``/\`` to denote the logical conjunction (and). Such a notation is declared by |