diff options
Diffstat (limited to 'doc')
| -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 | 59 | ||||
| -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, 950 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..04aedd0cf6 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 @@ -441,3 +443,60 @@ underscore or by omitting the annotation to a polymorphic definition. semantics that the first use declares it. In this mode, the universe names are not associated with the definition or proof once it has been defined. This is meant mainly for debugging purposes. + +.. flag:: Private Polymorphic Universes + + This option, on by default, removes universes which appear only in + the body of an opaque polymorphic definition from the definition's + universe arguments. As such, no value needs to be provided for + these universes when instanciating the definition. Universe + constraints are automatically adjusted. + + Consider the following definition: + + .. coqtop:: all + + Lemma foo@{i} : Type@{i}. + Proof. exact Type. Qed. + Print foo. + + The universe :g:`Top.xxx` for the :g:`Type` in the body cannot be accessed, we + only care that one exists for any instantiation of the universes + appearing in the type of :g:`foo`. This is guaranteed when the + transitive constraint ``Set <= Top.xxx < i`` is verified. Then when + using the constant we don't need to put a value for the inner + universe: + + .. coqtop:: all + + Check foo@{_}. + + and when not looking at the body we don't mention the private + universe: + + .. coqtop:: all + + About foo. + + To recover the same behaviour with regard to universes as + :g:`Defined`, the option :flag:`Private Polymorphic Universes` may + be unset: + + .. coqtop:: all + + Unset Private Polymorphic Universes. + + Lemma bar : Type. Proof. exact Type. Qed. + About bar. + Fail Check bar@{_}. + Check bar@{_ _}. + + Note that named universes are always public. + + .. coqtop:: all + + Set Private Polymorphic Universes. + Unset Strict Universe Declaration. + + Lemma baz : Type@{outer}. Proof. exact Type@{inner}. Qed. + About baz. 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 |