diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 21:26:55 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-04-16 23:29:00 +0200 |
| commit | a3ee82e80083fff971e382f52d9295fda2210e2d (patch) | |
| tree | c33240b821d78fb63bd0a3bb0a8d2bf17507f6c2 | |
| parent | abd6bbd90753fd98355e551d8dc8ecfd07494639 (diff) | |
[Sphinx] Clean-up indices
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 10 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/addendum/micromega.rst | 64 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 75 | ||||
| -rw-r--r-- | doc/sphinx/biblio.bib | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 62 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 33 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 46 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 524 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 41 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/proof-schemes.rst | 47 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 |
15 files changed, 554 insertions, 388 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index d60387f4f..e4dea3487 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -537,14 +537,19 @@ 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 [in @ident] [using relation @term] [by @tactic] + :name: setoid_replace The ``using relation`` arguments cannot be passed to the unprefixed form. @@ -583,7 +588,7 @@ Deprecated syntax and backward incompatibilities Due to backward compatibility reasons, the following syntax for the declaration of setoids and morphisms is also accepted. -.. tacv:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @A @Aeq @ST as @ident where ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record @@ -818,7 +823,8 @@ Usage ~~~~~ -.. tacv:: rewrite_strat @s [in @ident] +.. tacn:: rewrite_strat @s [in @ident] + :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 19d4ba9ba..c48c2d7ce 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -138,7 +138,7 @@ Declaration of Coercions .. exn:: @qualid does not respect the uniform inheritance condition .. exn:: Found target class ... instead of ... - .. warn:: Ambigous path: + .. warn:: Ambiguous path When the coercion `qualid` is added to the inheritance graph, non valid coercion paths are ignored; they are signaled by a warning @@ -218,6 +218,7 @@ declaration, this constructor is declared as a coercion. Idem but locally to the current section. .. cmdv:: SubClass @ident := @type. + :name: SubClass If `type` is a class `ident'` applied to some arguments then `ident` is defined and an identity coercion of name @@ -291,6 +292,7 @@ by extending the existing :cmd:`Record` macro. Its new syntax is: satisfied). .. cmdv:: Structure {? >} @ident {? @binders} : @sort := {? @ident} { {+; @ident :{? >} @term } }. + :name: Structure This is a synonym of :cmd:`Record`. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index e850587c8..4f8cc34d4 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -13,20 +13,19 @@ tactics for solving arithmetic goals over :math:`\mathbb{Z}`, :math:`\mathbb{Q}` It also possible to get the tactics for integers by a ``Require Import Lia``, rationals ``Require Import Lqa`` and reals ``Require Import Lra``. -+ ``lia`` is a decision procedure for linear integer arithmetic (see Section :ref:`lia <lia>`); -+ ``nia`` is an incomplete proof procedure for integer non-linear - arithmetic (see Section :ref:`nia <nia>`); -+ ``lra`` is a decision procedure for linear (real or rational) arithmetic - (see Section :ref:`lra <lra>`); -+ ``nra`` is an incomplete proof procedure for non-linear (real or - rational) arithmetic (see Section :ref:`nra <nra>`); -+ ``psatz D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ++ :tacn:`lia` is a decision procedure for linear integer arithmetic; ++ :tacn:`nia` is an incomplete proof procedure for integer non-linear + arithmetic; ++ :tacn:`lra` is a decision procedure for linear (real or rational) arithmetic; ++ :tacn:`nra` is an incomplete proof procedure for non-linear (real or + rational) arithmetic; ++ :tacn:`psatz` ``D n`` where ``D`` is :math:`\mathbb{Z}` or :math:`\mathbb{Q}` or :math:`\mathbb{R}`, and ``n`` is an optional integer limiting the proof search depth is an incomplete proof procedure for non-linear arithmetic. It is based on John Harrison’s HOL Light driver to the external prover `csdp` [#]_. Note that the `csdp` driver is generating a *proof cache* which makes it possible to rerun scripts - even without `csdp` (see Section :ref:`psatz <psatz>`). + even without `csdp`. The tactics solve propositional formulas parameterized by atomic arithmetic expressions interpreted over a domain :math:`D` ∈ {ℤ, ℚ, ℝ}. @@ -91,12 +90,13 @@ For each conjunct :math:`C_i`, the tactic calls a oracle which searches for expression* that is normalized by the ring tactic (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`. -.. _lra: - `lra`: a decision procedure for linear real and rational arithmetic ------------------------------------------------------------------- -The `lra` tactic is searching for *linear* refutations using Fourier +.. tacn:: lra + :name: lra + +This tactic is searching for *linear* refutations using Fourier elimination [#]_. As a result, this tactic explores a subset of the *Cone* defined as @@ -107,16 +107,17 @@ The deductive power of `lra` is the combined deductive power of tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`. -.. _lia: - `lia`: a tactic for linear integer arithmetic --------------------------------------------- -The tactic lia offers an alternative to the omega and romega tactic -(see :ref:`omega`). Roughly speaking, the deductive power of lia is -the combined deductive power of `ring_simplify` and `omega`. However, it -solves linear goals that `omega` and `romega` do not solve, such as the -following so-called *omega nightmare* :cite:`TheOmegaPaper`. +.. tacn:: lia + :name: lia + +This tactic offers an alternative to the :tacn:`omega` and :tac:`romega` +tactics. Roughly speaking, the deductive power of lia is the combined deductive +power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear +goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following +so-called *omega nightmare* :cite:`TheOmegaPaper`. .. coqtop:: in @@ -124,8 +125,8 @@ following so-called *omega nightmare* :cite:`TheOmegaPaper`. 27 <= 11 * x + 13 * y <= 45 -> -10 <= 7 * x - 9 * y <= 4 -> False. -The estimation of the relative efficiency of `lia` *vs* `omega` and `romega` -is under evaluation. +The estimation of the relative efficiency of :tacn:`lia` *vs* :tacn:`omega` and +:tacn:`romega` is under evaluation. High level view of `lia` ~~~~~~~~~~~~~~~~~~~~~~~~ @@ -182,12 +183,13 @@ Our current oracle tries to find an expression :math:`e` with a small range with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for a proof. -.. _nra: - `nra`: a proof procedure for non-linear arithmetic -------------------------------------------------- -The `nra` tactic is an *experimental* proof procedure for non-linear +.. tacn:: nra + :name: nra + +This tactic is an *experimental* proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear reasoning before running the linear prover of `lra`. This pre-processing does the following: @@ -202,21 +204,23 @@ does the following: After this pre-processing, the linear prover of `lra` searches for a proof by abstracting monomials by variables. -.. _nia: - `nia`: a proof procedure for non-linear integer arithmetic ---------------------------------------------------------- -The `nia` tactic is a proof procedure for non-linear integer arithmetic. +.. tacn:: nia + :name: nia + +This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to `nra`. The obtained goal is solved using the linear integer prover `lia`. -.. _psatz: - `psatz`: a proof procedure for non-linear arithmetic ---------------------------------------------------- -The `psatz` tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the +.. tacn:: psatz + :name: psatz + +This tactic explores the :math:`\mathit{Cone}` by increasing degrees – hence the depth parameter :math:`n`. In theory, such a proof search is complete – if the goal is provable the search eventually stops. Unfortunately, the external oracle is using numeric (approximate) optimization techniques diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 1c3fdeb43..be30d1bc4 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -151,7 +151,7 @@ Program Definition obligations. Once solved using the commands shown below, it binds the final |Coq| term to the name ``ident`` in the environment. - .. exn:: ident already exists + .. exn:: @ident already exists (Program Definition) .. cmdv:: Program Definition @ident : @type := @term @@ -276,6 +276,7 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: {? Local|Global} Obligation Tactic := @tactic + :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index d6955b310..3e95bd8c4 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -314,28 +314,25 @@ optional priority can be declared, 0 being the highest priority as for auto hints. If the priority is not specified, it defaults to the number of non-dependent binders of the instance. -Variants: - - -.. cmd:: Instance ident {? @binders} : forall {? @binders}, Class t1 … tn [| priority] := @term +..cmdv:: Instance @ident {? @binders} : forall {? @binders}, Class t1 … tn [| 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 singleton classes. -.. cmd:: Global Instance +..cmdv:: Global Instance One can use the ``Global`` modifier on instances declared in a section so that their generalization is automatically redeclared after the section is closed. -.. cmd:: Program Instance +..cmdv:: Program Instance Switches the type-checking to Program (chapter :ref:`programs`) and uses the obligation mechanism to manage missing fields. -.. cmd:: Declare Instance +..cmdv:: Declare Instance In a Module Type, this command states that a corresponding concrete instance should exist in any implementation of thisModule Type. This @@ -370,14 +367,10 @@ Context Declares variables according to the given binding context, which might use :ref:`implicit-generalization`. +.. tacn:: typeclasses eauto -.. _typeclasses-eauto: - -``typeclasses eauto`` -~~~~~~~~~~~~~~~~~~~~~ - -The ``typeclasses eauto`` tactic uses a different resolution engine than -eauto and auto. The main differences are the following: +This tactic uses a different resolution engine than :tacn:`eauto` and +:tacn:`auto`. The main differences are the following: + Contrary to ``eauto`` and ``auto``, the resolution is done entirely in the new proof engine (as of Coq v8.6), meaning that backtracking is @@ -428,42 +421,46 @@ Variants: typeclass subgoals the same as other subgoals (no shelving of non-typeclass goals in particular). -.. _autoapply: +.. tacn:: autoapply @term with @ident + :name: autoapply -``autoapply term with ident`` -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The tactic autoapply applies a term using the transparency information -of the hint database ident, and does *no* typeclass resolution. This can -be used in ``Hint Extern``’s for typeclass instances (in the hint -database ``typeclass_instances``) to allow backtracking on the typeclass -subgoals created by the lemma application, rather than doing type class -resolution locally at the hint application time. + The tactic autoapply applies a term using the transparency information + of the hint database ident, and does *no* typeclass resolution. This can + be used in :cmd:`Hint Extern`’s for typeclass instances (in the hint + database ``typeclass_instances``) to allow backtracking on the typeclass + subgoals created by the lemma application, rather than doing type class + resolution locally at the hint application time. .. _TypeclassesTransparent: Typeclasses Transparent, Typclasses Opaque ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Typeclasses { Transparent | Opaque } {+ @ident} +.. cmd:: Typeclasses Transparent {+ @ident} - This commands defines the transparency of the given identifiers - during type class resolution. It is useful when some constants - prevent some unifications and make resolution fail. It is also useful - to declare constants which should never be unfolded during - proof-search, like fixpoints or anything which does not look like an - abbreviation. This can additionally speed up proof search as the - typeclass map can be indexed by such rigid constants (see - :ref:`thehintsdatabasesforautoandeauto`). By default, all constants - and local variables are considered transparent. One should take care - not to make opaque any constant that is used to abbreviate a type, - like: + This command defines makes the identifiers transparent during type class + resolution. -:: + .. cmdv:: Typeclasses Opaque {+ @ident} + :name: Typeclasses Opaque + + Make the identifiers opaque for typeclass search. It is useful when some + constants prevent some unifications and make resolution fail. It is also + useful to declare constants which should never be unfolded during + proof-search, like fixpoints or anything which does not look like an + abbreviation. This can additionally speed up proof search as the typeclass + map can be indexed by such rigid constants (see + :ref:`thehintsdatabasesforautoandeauto`). + + By default, all constants and local variables are considered transparent. One + should take care not to make opaque any constant that is used to abbreviate a + type, like: + + :: - relation A := A -> A -> Prop. + relation A := A -> A -> Prop. -This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. + This is equivalent to ``Hint Transparent, Opaque ident : typeclass_instances``. .. opt:: Typeclasses Dependency Order diff --git a/doc/sphinx/biblio.bib b/doc/sphinx/biblio.bib index ef50923c7..97231c9ec 100644 --- a/doc/sphinx/biblio.bib +++ b/doc/sphinx/biblio.bib @@ -790,8 +790,7 @@ Matching and Term Rewriting}, @TechReport{Leroy90, author = {X. Leroy}, - title = {The {ZINC} experiment: an economical implementation -of the {ML} language}, + title = {The {ZINC} experiment: an economical implementation of the {ML} language}, institution = {INRIA}, number = {117}, year = {1990} diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 8d47949db..1a7628d89 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -955,7 +955,8 @@ Reserved commands inside an interactive module type: is a shortcut for the command ``Include`` `module` for each `module`. -.. cmd:: @assumption_keyword Inline @assums. +.. cmd:: @assumption_keyword Inline @assums + :name: Inline The instance of this assumption will be automatically expanded at functor application, except when this functor application is prefixed by a ``!`` annotation. diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 246f45b3e..a9c4dd758 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -557,9 +557,10 @@ has type :token:`type`. the global context. The fact asserted by *term* is thus assumed as a postulate. -.. exn:: @ident already exists +.. exn:: @ident already exists (Axiom) .. cmdv:: Parameter @ident : @term. + :name: Parameter Is equivalent to ``Axiom`` :token:`ident` : :token:`term` @@ -582,6 +583,7 @@ has type :token:`type`. qualified name to refer to them. .. cmdv:: Conjecture @ident : @term + :name: Conjecture Is equivalent to ``Axiom`` :token:`ident` : :token:`term`. @@ -594,7 +596,7 @@ will be unknown and every object using this variable will be explicitly parametrized (the variable is *discharged*). Using the ``Variable`` command out of any section is equivalent to using ``Local Parameter``. -.. exn:: @ident already exists +.. exn:: @ident already exists (Variable) .. cmdv:: Variable {+ @ident } : @term. @@ -607,6 +609,7 @@ of any section is equivalent to using ``Local Parameter``. .. cmdv:: Variables {+ ( {+ @ident } : @term) }. .. cmdv:: Hypothesis {+ ( {+ @ident } : @term) }. + :name: Hypothesis .. cmdv:: Hypotheses {+ ( {+ @ident } : @term) }. @@ -643,7 +646,7 @@ Section :ref:`typing-rules`. This command binds :token:`term` to the name :token:`ident` in the environment, provided that :token:`term` is well-typed. -.. exn:: @ident already exists +.. exn:: @ident already exists (Definition) .. cmdv:: Definition @ident : @term := @term. @@ -687,7 +690,7 @@ prefixed by the let-in definition ``let`` :token:`ident` ``:=`` :token:`term` ``in``. Using the ``Let`` command out of any section is equivalent to using ``Local Definition``. -.. exn:: @ident already exists +.. exn:: @ident already exists (Let) .. cmdv:: Let @ident : @term := @term. @@ -1245,20 +1248,25 @@ the theorem is bound to the name :token:`ident` in the environment. .. exn:: The term @term has type @type which should be Set, Prop or Type -.. exn:: @ident already exists +.. exn:: @ident already exists (Theorem) The name you provided is already defined. You have then to choose another name. .. cmdv:: Lemma @ident : @type. + :name: Lemma .. cmdv:: Remark @ident : @type. + :name: Remark .. cmdv:: Fact @ident : @type. + :name: Fact .. cmdv:: Corollary @ident : @type. + :name: Corollary .. cmdv:: Proposition @ident : @type. + :name: Proposition These commands are synonyms of ``Theorem`` :token:`ident` : :token:`type`. @@ -1273,16 +1281,16 @@ the theorem is bound to the name :token:`ident` in the environment. coinduction has to be done is assumed to be non ambiguous and is guessed by the system. - Like in a ``Fixpoint`` or ``CoFixpoint`` definition, the induction hypotheses - have to be used on *structurally smaller* arguments (for a ``Fixpoint``) or - be *guarded by a constructor* (for a ``CoFixpoint``). The verification that + Like in a :cmd:`Fixpoint` or :cmd:`CoFixpoint` definition, the induction hypotheses + have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or + be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that recursive proof arguments are correct is done only at the time of registering the lemma in the environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. - The command can be used also with ``Lemma``, ``Remark``, etc. instead of - ``Theorem``. + The command can be used also with :cmd:`Lemma`, :cmd:`Remark`, etc. instead of + :cmd:`Theorem`. .. cmdv:: Definition @ident : @type. @@ -1313,16 +1321,20 @@ the theorem is bound to the name :token:`ident` in the environment. This generalizes the syntax of CoFixpoint so that one or more bodies can be defined interactively using the proof editing mode. -.. cmd:: Proof. … Qed. +.. cmd:: Proof -A proof starts by the keyword Proof. Then Coq enters the proof editing mode -until the proof is completed. The proof editing mode essentially contains -tactics that are described in chapter :ref:`Tactics`. Besides tactics, there are -commands to manage the proof editing mode. They are described in Chapter -:ref:`proofhandling`. When the proof is completed it should be validated and -put in the environment using the keyword Qed. + A proof starts by the keyword Proof. Then Coq enters the proof editing mode + until the proof is completed. The proof editing mode essentially contains + tactics that are described in chapter :ref:`Tactics`. Besides tactics, there + are commands to manage the proof editing mode. They are described in Chapter + :ref:`proofhandling`. -.. exn:: @ident already exists +.. cmd:: Qed + + When the proof is completed it should be validated and put in the environment + using the keyword Qed. + +.. exn:: @ident already exists (Qed) .. note:: @@ -1341,14 +1353,16 @@ put in the environment using the keyword Qed. realizing some form of *proof-irrelevance*. To be able to unfold a proof, the proof should be ended by Defined (see below). -.. cmdv:: Proof. … Defined. +.. cmdv:: Defined + :name: Defined - Same as ``Proof. … Qed.`` but the proof is then declared transparent, - which means that its content can be explicitly used for - type-checking and that it can be unfolded in conversion tactics - (see :ref:`performingcomputations`, :cmd:`Opaque`, :cmd:`Transparent`). + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). -.. cmdv:: Proof. … Admitted. +.. cmdv:: Admitted. + :name: Admitted Turns the current asserted statement into an axiom and exits the proof mode. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 247d5d899..009758319 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,6 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr + :name: ; The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, @@ -193,6 +194,7 @@ Different tactics can be applied to the different goals using the following form: .. tacn:: [> {*| @expr }] + :name: [> ... | ... | ... ] (dispatch) The expressions :n:`@expr__i` are evaluated to :n:`v__i`, for i=0,...,n and all have to be tactics. The :n:`v__i` is applied to the @@ -240,6 +242,7 @@ We can restrict the application of a tactic to a subset of the currently focused goals with: .. tacn:: @toplevel_selector : @expr + :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested in a tactic expression, by using the keyword ``only``: @@ -290,6 +293,7 @@ For loop There is a for loop that repeats a tactic :token:`num` times: .. tacn:: do @num @expr + :name: do :n:`@expr` is evaluated to ``v`` which must be a tactic value. This tactic value ``v`` is applied :token:`num` times. Supposing :token:`num` > 1, after the @@ -303,6 +307,7 @@ Repeat loop We have a repeat loop with: .. tacn:: repeat @expr + :name: repeat :n:`@expr` is evaluated to ``v``. If ``v`` denotes a tactic, this tactic is applied to each focused goal independently. If the application succeeds, the @@ -316,6 +321,7 @@ Error catching We can catch the tactic errors with: .. tacn:: try @expr + :name: try :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of @@ -329,6 +335,7 @@ Detecting progress We can check if a tactic made progress with: .. tacn:: progress expr + :name: progress :n:`@expr` is evaluated to v which must be a tactic value. The tactic value ``v`` is applied to each focued subgoal independently. If the application of ``v`` @@ -343,6 +350,7 @@ Backtracking branching We can branch with the following structure: .. tacn:: @expr__1 + @expr__2 + :name: + (backtracking branching) :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is applied to @@ -365,6 +373,7 @@ restrict to a local, left biased, branching and consider the first tactic to work (i.e. which does not fail) among a panel of tactics: .. tacn:: first [{*| @expr}] + :name: first The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i=1,...,n. Supposing n>1, it applies, in each focused @@ -396,6 +405,7 @@ Yet another way of branching without backtracking is the following structure: .. tacn:: @expr__1 || @expr__2 + :name: || (left-biased branching) :n:`@expr__1` and :n:`@expr__2` are evaluated respectively to :n:`v__1` and :n:`v__2` which must be tactic values. The tactic value :n:`v__1` is @@ -410,6 +420,7 @@ Generalized biased branching The tactic .. tacn:: tryif @expr__1 then @expr__2 else @expr__3 + :name: tryif is a generalization of the biased-branching tactics above. The expression :n:`@expr__1` is evaluated to :n:`v__1`, which is then @@ -430,6 +441,7 @@ Another way of restricting backtracking is to restrict a tactic to a single success *a posteriori*: .. tacn:: once @expr + :name: once :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, @@ -443,6 +455,7 @@ Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @expr + :name: exactly_once :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, @@ -467,6 +480,7 @@ Checking the failure Coq provides a derived tactic to check that a tactic *fails*: .. tacn:: assert_fails @expr + :name: assert_fails This behaves like :n:`tryif @expr then fail 0 tac "succeeds" else idtac`. @@ -477,6 +491,7 @@ Coq provides a derived tactic to check that a tactic has *at least one* success: .. tacn:: assert_succeeds @expr + :name: assert_suceeds This behaves like :n:`tryif (assert_fails tac) then fail 0 tac "fails" else idtac`. @@ -488,6 +503,7 @@ We may consider the first to solve (i.e. which generates no subgoal) among a panel of tactics: .. tacn:: solve [{*| @expr}] + :name: solve The :n:`@expr__i` are evaluated to :n:`v__i` and :n:`v__i` must be tactic values, for i=1,...,n. Supposing n>1, it applies :n:`v__1` to @@ -508,6 +524,7 @@ The constant :n:`idtac` is the identity tactic: it leaves any goal unchanged but it appears in the proof script. .. tacn:: idtac {* message_token} + :name: idtac This prints the given tokens. Strings and integers are printed literally. If a (term) variable is given, its contents are printed. @@ -516,6 +533,7 @@ Failing ~~~~~~~ .. tacn:: fail + :name: fail This is the always-failing tactic: it does not solve any goal. It is useful for defining other tacticals since it can be caught by @@ -543,6 +561,7 @@ Failing This is a combination of the previous variants. .. tacv:: gfail + :name: gfail This variant fails even if there are no goals left. @@ -565,6 +584,7 @@ We can force a tactic to stop if it has not finished after a certain amount of time: .. tacn:: timeout @num @expr + :name: timeout :n:`@expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied normally, except that it is interrupted after :n:`@num` seconds @@ -586,6 +606,7 @@ Timing a tactic A tactic execution can be timed: .. tacn:: time @string @expr + :name: time evaluates :n:`@expr` and displays the time the tactic expression ran, whether it fails or successes. In case of several successes, the time for each successive @@ -600,6 +621,7 @@ Tactic expressions that produce terms can be timed with the experimental tactic .. tacn:: time_constr expr + :name: time_constr which evaluates :n:`@expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is @@ -610,10 +632,12 @@ tactic implemented using the tactics .. tacn:: restart_timer @string + :name: restart_timer and .. 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 @@ -951,6 +975,7 @@ Testing boolean expressions ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: guard @test + :name: guard The :tacn:`guard` tactic tests a boolean expression, and fails if the expression evaluates to false. If the expression evaluates to true, it succeeds @@ -976,6 +1001,7 @@ Proving a subgoal as a separate lemma ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: abstract @expr + :name: abstract From the outside, :n:`abstract @expr` is the same as :n:`solve @expr`. Internally it saves an auxiliary lemma called ``ident_subproofn`` where @@ -1000,6 +1026,7 @@ Proving a subgoal as a separate lemma don’t play well with asynchronous proofs. .. tacv:: transparent_abstract @expr + :name: transparent_abstract Save the subproof in a transparent lemma rather than an opaque one. @@ -1220,28 +1247,33 @@ performance bug. Unset Ltac Profiling. .. tacn:: start ltac profiling + :name: start ltac profiling This tactic behaves like :tacn:`idtac` but enables the profiler. .. tacn:: stop ltac profiling + :name: stop ltac profiling Similarly to :tacn:`start ltac profiling`, this tactic behaves like :tacn:`idtac`. Together, they allow you to exclude parts of a proof script from profiling. .. tacn:: reset ltac profile + :name: reset ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile + :name: show ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile @string + :name: show ltac profile This tactic behaves like the corresponding vernacular command and allow displaying and resetting the profile from tactic scripts for @@ -1261,6 +1293,7 @@ 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 diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index a77b127eb..86c94bab3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -58,13 +58,14 @@ statement is eventually completed and validated, the statement is then bound to the name ``Unnamed_thm`` (or a variant of this name not already used for another statement). -.. cmd:: Qed. +.. cmd:: Qed + :name: Qed (interactive proof) This command is available in interactive editing proof mode when the proof is completed. Then ``Qed`` extracts a proof term from the proof script, switches back to Coq top-level and attaches the extracted proof term to the declared name of the original goal. This name is -added to the environment as an ``Opaque`` constant. +added to the environment as an opaque constant. .. exn:: Attempt to save an incomplete proof @@ -81,6 +82,7 @@ a while when the proof is large. In some exceptional cases one may even incur a memory overflow. .. cmdv:: Defined. + :name: Defined (interactive proof) Defines the proved term as a transparent constant. @@ -91,6 +93,7 @@ command (and the following ones) can only be used if the original goal has been opened using the ``Goal`` command. .. cmd:: Admitted. + :name: Admitted (interactive proof) This command is available in interactive editing proof mode to give up the current proof and declare the initial goal as an axiom. @@ -105,8 +108,8 @@ This command applies in proof editing mode. It is equivalent to That is, you have to give the full proof in one gulp, as a proof term (see Section :ref:`applyingtheorems`). - .. cmdv:: Proof. + :name: Proof (interactive proof) Is a noop which is useful to delimit the sequence of tactic commands which start a proof, after a ``Theorem`` command. It is a good practice to @@ -182,49 +185,51 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. cmdv:: Set Default Proof Using "@expression". +.. opt:: Default Proof Using "@expression". -Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default -Proof Using "a b"``. will complete all ``Proof`` commands not followed by a -using part with using ``a`` ``b``. + Use :n:`@expression` as the default ``Proof``` using value. E.g. ``Set Default + Proof Using "a b"``. will complete all ``Proof`` commands not followed by a + using part with using ``a`` ``b``. -.. cmdv:: Set Suggest Proof Using. +.. opt:: Suggest Proof Using. -When ``Qed`` is performed, suggest a using annotation if the user did not -provide one. + When ``Qed`` is performed, suggest a using annotation if the user did not + provide one. .. _`nameaset`: Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` +.. cmd:: Collection @ident := @section_subset_expr + The command ``Collection`` can be used to name a set of section hypotheses, with the purpose of making ``Proof using`` annotations more compact. -.. cmdv:: Collection Some := x y z. +.. cmdv:: Collection Some := x y z Define the collection named "Some" containing ``x``, ``y`` and ``z``. -.. cmdv:: Collection Fewer := Some - z. +.. cmdv:: Collection Fewer := Some - z Define the collection named "Fewer" containing only ``x`` and ``y``. -.. cmdv:: Collection Many := Fewer + Some. -.. cmdv:: Collection Many := Fewer - Some. +.. cmdv:: Collection Many := Fewer + Some +.. cmdv:: Collection Many := Fewer - Some Define the collection named "Many" containing the set union or set difference of "Fewer" and "Some". -.. cmdv:: Collection Many := Fewer - (x y). +.. cmdv:: Collection Many := Fewer - (x y) Define the collection named "Many" containing the set difference of -"Fewer" and the unnamed collection ``x`` ``y``. +"Fewer" and the unnamed collection ``x`` ``y`` .. cmd:: Abort. @@ -288,6 +293,7 @@ backtracks one step. Repeats Undo :n:`@num` times. .. cmdv:: Restart. + :name: Restart This command restores the proof editing process to the original goal. @@ -424,11 +430,11 @@ Set Bullet Behavior The bullet behavior can be controlled by the following commands. -.. opt:: Bullet Behavior "None". +.. opt:: Bullet Behavior "None" This makes bullets inactive. -.. opt:: Bullet Behavior "Strict Subproofs". +.. opt:: Bullet Behavior "Strict Subproofs" This makes bullets active (this is the default behavior). @@ -551,7 +557,7 @@ Controlling the effect of proof editing commands ------------------------------------------------ -.. opt:: Hyps Limit @num. +.. opt:: Hyps Limit @num This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -560,7 +566,7 @@ When unset, it goes back to the default mode which is to print all available hypotheses. -.. opt:: Automatic Introduction. +.. opt:: Automatic Introduction This option controls the way binders are handled in assertion commands such as ``Theorem ident [binders] : form``. When the diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 6ddb0b027..977a5b8fa 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -493,7 +493,10 @@ inferred from the whole context of the goal (see for example section Definitions ~~~~~~~~~~~ -The pose tactic allows to add a defined constant to a proof context. +.. tacn:: pose + :name: pose (ssreflect) + +This tactic allows to add a defined constant to a proof context. |SSR| generalizes this tactic in several ways. In particular, the |SSR| pose tactic supports *open syntax*: the body of the definition does not need surrounding parentheses. For instance: @@ -1349,6 +1352,7 @@ Discharge The general syntax of the discharging tactical ``:`` is: .. tacn:: @tactic {? @ident } : {+ @d_item } {? @clear_switch } + :name: ... : ... (ssreflect) .. prodn:: d_item ::= {? @occ_switch %| @clear_switch } @term @@ -1500,9 +1504,11 @@ side of an equation. The abstract tactic ``````````````````` -The ``abstract`` tactic assigns an ``abstract`` constant previously -introduced with the ``[: name ]`` intro pattern -(see section :ref:`introduction_ssr`). +.. tacn:: abstract: {+ d_item} + :name abstract (ssreflect) + +This tactic assigns an abstract constant previously introduced with the ``[: +name ]`` intro pattern (see section :ref:`introduction_ssr`). In a goal like the following:: @@ -1809,6 +1815,8 @@ of a :token:`d_item` immediately following this ``/`` switch, using the syntax: .. tacv:: case: {+ @d_item } / {+ @d_item } + :name: case (ssreflect) + .. tacv:: elim: {+ @d_item } / {+ @d_item } The :token:`d_item` on the right side of the ``/`` switch are discharged as @@ -2132,7 +2140,7 @@ tactic using the given second tactic, and fails if it does not succeed. Its analogue .. tacn:: @tactic ; first by @tactic - :name: first + :name: first (ssreflect) tries to solve the first subgoal generated by the first tactic using the second given tactic, and fails if it does not succeed. @@ -2212,7 +2220,7 @@ Iteration thanks to the do tactical, whose general syntax is: .. tacn:: do {? @mult } ( @tactic | [ {+| @tactic } ] ) - :name: do + :name: do (ssreflect) where :token:`mult` is a *multiplier*. @@ -3724,6 +3732,7 @@ We provide a special tactic unlock for unfolding such definitions while removing “locks”, e.g., the tactic: .. tacn:: unlock {? @occ_switch } @ident + :name: unlock replaces the occurrence(s) of :token:`ident` coded by the :token:`occ_switch` with the corresponding body. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 1868f4b9d..7a45272f2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -51,7 +51,7 @@ specified, the default selector is used. tactic_invocation : toplevel_selector : tactic. : |tactic . -.. opt:: Default Goal Selector @toplevel_selector. +.. opt:: Default Goal Selector @toplevel_selector This option controls the default selector – used when no selector is specified when applying a tactic – is set to the chosen value. The initial @@ -168,6 +168,7 @@ term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then .. exn:: Not an exact proof. .. tacv:: eexact @term. + :name: eexact This tactic behaves like exact but is able to handle terms and goals with meta-variables. @@ -181,6 +182,7 @@ the goal. If it is the case, the subgoal is proved. Otherwise, it fails. .. exn:: No such assumption. .. tacv:: eassumption + :name: eassumption This tactic behaves like assumption but is able to handle goals with meta-variables. @@ -233,6 +235,7 @@ useful to advanced users. cast around it. .. tacv:: simple refine @term + :name: simple refine This tactic behaves like refine, but it does not shelve any subgoal. It does not perform any beta-reduction either. @@ -243,6 +246,7 @@ useful to advanced users. resolution of typeclasses. .. tacv:: simple notypeclasses refine @term + :name: simple notypeclasses refine This tactic behaves like ``simple refine`` except it performs typechecking without resolution of typeclasses. @@ -313,6 +317,7 @@ instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. .. tacv:: simple apply @term. + :name: simple apply This behaves like ``apply`` but it reasons modulo conversion only on subterms that contain no variables to instantiate. For instance, the following example @@ -335,6 +340,7 @@ does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} + :name: simple eapply This summarizes the different syntaxes for ``apply`` and ``eapply``. @@ -515,8 +521,8 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. constructor of :g:`I`, then ``constructor i`` is equivalent to ``intros; apply c``:sub:`i`. -.. exn:: Not an inductive product. -.. exn:: Not enough constructors. +.. exn:: Not an inductive product +.. exn:: Not enough constructors .. tacv:: constructor @@ -534,34 +540,39 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. The terms in the @bindings_list are checked in the context where constructor is executed and not in the context where @apply is executed (the introductions are not taken into account). .. tacv:: split + :name: split This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`constructor 1.`. It is typically used in the case of a conjunction :g:`A` :math:`\wedge` :g:`B`. -.. exn:: Not an inductive goal with 1 constructor. +.. exn:: Not an inductive goal with 1 constructor .. tacv:: exists @val + :name: exists This applies only if :g:`I` has a single constructor. It is then equivalent to :n:`intros; constructor 1 with @bindings_list.` It is typically used in the case of an existential quantification :math:`\exists`:g:`x, P(x).` -.. exn:: Not an inductive goal with 1 constructor. +.. exn:: Not an inductive goal with 1 constructor .. tacv:: exists @bindings_list This iteratively applies :n:`exists @bindings_list`. .. tacv:: left + :name: left + .. tacv:: right + :name: right These tactics apply only if :g:`I` has two constructors, for instance in the case of a disjunction :g:`A` :math:`\vee` :g:`B`. Then, they are respectively equivalent to ``constructor 1`` and ``constructor 2``. -.. exn:: Not an inductive goal with 2 constructors. +.. exn:: Not an inductive goal with 2 constructors .. tacv:: left with @bindings_list .. tacv:: right with @bindings_list @@ -572,15 +583,25 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. for the appropriate ``i``. .. tacv:: econstructor + :name: econstructor + .. tacv:: eexists + :name: eexists + .. tacv:: esplit + :name: esplit + .. tacv:: eleft + :name: eleft + .. tacv:: eright + :name: eright - These tactics and their variants behave like ``constructor``, ``exists``, - ``split``, ``left``, ``right`` and their variants but they introduce - existential variables instead of failing when the instantiation of a - variable cannot be found (cf. :tacn:`eapply` and :tacn:`apply`). + These tactics and their variants behave like :tacn:`constructor`, + :tacn:`exists`, :tacn:`split`, :tacn:`left`, :tacn:`right` and their variants + but they introduce existential variables instead of failing when the + instantiation of a variable cannot be found (cf. :tacn:`eapply` and + :tacn:`apply`). .. _managingthelocalcontext: @@ -611,7 +632,7 @@ the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. .. exn:: No product even after head-reduction. -.. exn:: ident is already used. +.. exn:: @ident is already used. .. tacv:: intros @@ -845,6 +866,7 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` .. tacv:: clearbody @ident + :name: clearbody This tactic expects :n:`@ident` to be a local definition then clears its body. Otherwise said, this tactic turns a definition into an assumption. @@ -866,7 +888,7 @@ quantification or an implication. it. .. tacn:: revert {+ @ident} - :name: revert ... + :name: revert This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses (possibly defined) to the goal, if this respects dependencies. This tactic is @@ -982,6 +1004,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: eset (@ident {+ @binder} := @term ) in @goal_occurrences .. tacv:: eset @term in @goal_occurrences + :name: eset While the different variants of :tacn:`set` expect that no existential variables are generated by the tactic, :n:`eset` removes this constraint. In @@ -989,6 +1012,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. :tacn:`epose`, i.e. when the :`@term` does not occur in the goal. .. tacv:: remember @term as @ident + :name: remember This behaves as :n:`set (@ident:= @term ) in *` and using a logical (Leibniz’s) equality instead of a local definition. @@ -1006,6 +1030,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged. .. tacv:: eremember @term as @ident .. tacv:: eremember @term as @ident in @goal_occurrences .. tacv:: eremember @term as @ident eqn:@ident + :name: eremember + While the different variants of :n:`remember` expect that no existential variables are generated by the tactic, :n:`eremember` removes this constraint. @@ -1112,6 +1138,7 @@ Controlling the proof flow .. exn:: Variable @ident is already declared .. tacv:: eassert form as intro_pattern by tactic + :name: eassert .. tacv:: assert (@ident := @term) @@ -1121,6 +1148,7 @@ Controlling the proof flow to prove it. .. 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, @@ -1134,6 +1162,7 @@ Controlling the proof flow the tactic, :n:`epose proof` removes this constraint. .. tacv:: enough (@ident : form) + :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 @@ -1159,13 +1188,17 @@ Controlling the proof flow applied to all of them. .. tacv:: eenough (@ident : form) by tactic + :name: eenough + .. tacv:: eenough form by tactic + .. tacv:: eenough form as intro_pattern by tactic 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 @form + :name: cut This tactic applies to any goal. It implements the non-dependent case of the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference @@ -1175,6 +1208,7 @@ Controlling the proof flow .. tacv:: specialize (ident {* @term}) {? as intro_pattern} .. tacv:: specialize ident with @bindings_list {? as intro_pattern} + :name: specialize The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or @@ -1416,6 +1450,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) dependent premises of the type of :n:`@term` (see :ref:`syntax of bindings <bindingslist>`). .. tacv:: edestruct @term + :name: edestruct This tactic behaves like :n:`destruct @term` except that it does not fail if the instance of a dependent premises of the type of :n:`@term` is not @@ -1442,6 +1477,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) the effects of the `with`, `as`, `eqn:`, `using`, and `in` clauses. .. tacv:: case term + :name: case The tactic :n:`case` is a more basic tactic to perform case analysis without recursion. It behaves as :n:`elim @term` but using a case-analysis @@ -1451,14 +1487,15 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Analogous to :n:`elim @term with @bindings_list` above. -.. tacv:: ecase @term -.. tacv:: ecase @term with @bindings_list +.. tacv:: ecase @term {? with @bindings_list } + :name: ecase In case the type of :n:`@term` has dependent premises, or dependent premises whose values are not inferable from the :n:`with @bindings_list` clause, :n:`ecase` turns them into existential variables to be resolved later on. .. tacv:: simple destruct @ident + :name: simple destruct This tactic behaves as :n:`intros until @ident; case @ident` when :n:`@ident` is a quantified variable of the goal. @@ -1549,6 +1586,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) premises of the type of :n:`term` (see :ref:`bindings list <bindingslist>`). .. tacv:: einduction @term + :name: einduction This tactic behaves like :tacn:`induction` except that it does not fail if some dependent premise of the type of :n:`@term` is not inferable. Instead, @@ -1621,6 +1659,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) (see :ref:`bindings list <bindingslist>`). .. tacv:: eelim @term + :name: eelim In case the type of :n:`@term` has dependent premises, this turns them into existential variables to be resolved later on. @@ -1639,7 +1678,8 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) These are the most general forms of ``elim`` and ``eelim``. It combines the effects of the ``using`` clause and of the two uses of the ``with`` clause. -.. tacv:: elimtype form +.. tacv:: elimtype @form + :name: elimtype The argument :n:`form` must be inductively defined. :n:`elimtype I` is equivalent to :n:`cut I. intro Hn; elim Hn; clear Hn.` Therefore the @@ -1649,6 +1689,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) :n:`elimtype I; 2:exact t.` .. tacv:: simple induction @ident + :name: simple induction This tactic behaves as :n:`intros until @ident; elim @ident` when :n:`@ident` is a quantified variable of the goal. @@ -1733,6 +1774,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) other ones need not be further generalized. .. tacv:: dependent destruction @ident + :name: dependent destruction This performs the generalization of the instance :n:`@ident` but uses ``destruct`` instead of induction on the generalized hypothesis. This gives @@ -1842,6 +1884,7 @@ See also: :ref:`advanced-recursive-functions` .. tacv:: ediscriminate @num .. tacv:: 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 @@ -1921,6 +1964,7 @@ the use of a sigma type is avoided. .. tacv:: einjection @num .. tacv:: 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 @@ -1948,17 +1992,19 @@ the use of a sigma type is avoided. to the number of new equalities. The original equality is erased if it corresponds to an hypothesis. -It is possible to ensure that :n:`injection @term` erases the original -hypothesis and leaves the generated equalities in the context rather -than putting them as antecedents of the current goal, as if giving -:n:`injection @term as` (with an empty list of names). To obtain this -behavior, the option :opt:`Structural Injection` must be activated. This -option is off by default. +.. opt:: Structural Injection + + This option ensure that :n:`injection @term` erases the original hypothesis + and leaves the generated equalities in the context rather than putting them + as antecedents of the current goal, as if giving :n:`injection @term as` + (with an empty list of names). This option is off by default. -By default, :tacn:`injection` only creates new equalities between :n:`@terms` whose -type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for -objects that are proofs of a statement in :g:`Prop`. This behavior can be -turned off by setting the option :opt:`Keep Proof Equalities`. +.. opt:: Keep Proof Equalities + + By default, :tacn:`injection` only creates new equalities between :n:`@terms` + whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special + behavior for objects that are proofs of a statement in :g:`Prop`. This option + controls this behavior. .. tacn:: inversion @ident :name: inversion @@ -2110,6 +2156,7 @@ turned off by setting the option :opt:`Keep Proof Equalities`. :n:`dependent inversion_clear @ident with @term`. .. tacv:: simple inversion @ident + :name: simple inversion It is a very primitive inversion tactic that derives all the necessary equalities but it does not simplify the constraints as ``inversion`` does. @@ -2410,6 +2457,7 @@ subgoals. leading to failure if these n rewrites are not possible. .. tacv:: erewrite @term + :name: erewrite This tactic works as :n:`rewrite @term` but turning unresolved bindings into existential variables, if any, instead of @@ -2456,6 +2504,7 @@ subgoals. clause argument must not contain any type of nor value of. .. tacv:: cutrewrite <- (@term = @term) + :cutrewrite: This tactic is deprecated. It acts like :n:`replace @term with @term`, or, equivalently as :n:`enough (@term = @term) as <-`. @@ -2499,30 +2548,30 @@ unfolded and cleared. context for which an equality of the form :n:`@ident = t` or :n:`t = @ident` or :n:`@ident := t` exists, with :n:`@ident` not occurring in `t`. - .. note:: - The behavior of subst can be controlled using option :opt:`Regular Subst - Tactic`. When this option is activated, subst also deals with the - following corner cases: + .. opt:: Regular Subst Tactic + + This option controls the behavior of :tacn:`subst`. When it is + activated, :tacn:`subst` also deals with the following corner cases: - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the option, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or - `t′` respectively. - + The presence of a recursive equation which without the option would - be a cause of failure of :tacn:`subst`. - + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` - and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the - option would be a cause of failure of :tacn:`subst`. + + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` + and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` + or :n:`u = @ident`:sub:`2`; without the option, a second call to + subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + `t′` respectively. + + The presence of a recursive equation which without the option would + be a cause of failure of :tacn:`subst`. + + A context with cyclic dependencies as with hypotheses :n:`@ident`:sub:`1` :n:`= f @ident`:sub:`2` + and :n:`@ident`:sub:`2` :n:`= g @ident`:sub:`1` which without the + option would be a cause of failure of :tacn:`subst`. - Additionally, it prevents a local definition such as :n:`@ident := t` to be - unfolded which otherwise it would exceptionally unfold in configurations - containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` - with `u′` not a variable. Finally, it preserves the initial order of - hypotheses, which without the option it may break. The option is on by - default. + Additionally, it prevents a local definition such as :n:`@ident := t` to be + unfolded which otherwise it would exceptionally unfold in configurations + containing hypotheses of the form :n:`@ident = u`, or :n:`u′ = @ident` + with `u′` not a variable. Finally, it preserves the initial order of + hypotheses, which without the option it may break. The option is on by + default. .. tacn:: stepl @term @@ -2536,30 +2585,37 @@ where `eq` is typically a setoid equality. The application of :n:`stepl @term` then replaces the goal by :n:`R @term @term` and adds a new goal stating :n:`eq @term @term`. -Lemmas are added to the database using the command ``Declare Left Step @term.`` +.. cmd:: Declare Left Step @term + + Adds :n:`@term` to the database used by :tacn:`stepl`. + The tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). .. tacv:: stepl @term by tactic - This applies :n:`stepl @term` then applies tactic to the second goal. + This applies :n:`stepl @term` then applies tactic to the second goal. .. tacv:: stepr @term stepr @term by tactic + :name: stepr + + This behaves as :tacn:`stepl` but on the right-hand-side of the binary + relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq + y z -> R x z`. - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form :g:`forall x y z, R x y -> eq - y z -> R x z` and are registered using the command ``Declare Right Step - @term.`` + .. cmd:: Declare Right Step @term + + Adds :n:`@term` to the database used by :tacn:`stepr`. .. tacn:: change @term :name: change - This tactic applies to any goal. It implements the rule ``Conv`` given in - :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` - with `U` providing that `U` is well-formed and that `T` and `U` are - convertible. + This tactic applies to any goal. It implements the rule ``Conv`` given in + :ref:`subtyping-rules`. :g:`change U` replaces the current goal `T` + with `U` providing that `U` is well-formed and that `T` and `U` are + convertible. .. exn:: Not convertible @@ -2697,6 +2753,7 @@ the conversion in hypotheses :n:`{+ @ident}`. and :n:`lazy beta delta -{+ @qualid} iota zeta`. .. tacv:: vm_compute + :name: vm_compute This tactic evaluates the goal using the optimized call-by-value evaluation bytecode-based virtual machine described in :cite:`CompiledStrongReduction`. @@ -2706,6 +2763,7 @@ the conversion in hypotheses :n:`{+ @ident}`. reflection-based tactics. .. tacv:: native_compute + :name: native_compute This tactic evaluates the goal by compilation to Objective Caml as described in :cite:`FullReduction`. If Coq is running in native code, it can be @@ -3096,7 +3154,7 @@ the :tacn:`auto` and :tacn:`trivial` tactics: .. opt:: Info Auto .. opt:: Debug Auto .. opt:: Info Trivial -.. opt:: Info Trivial +.. opt:: Debug Trivial See also: :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` @@ -3251,188 +3309,203 @@ observationally different from the legacy one. The general command to add a hint to some databases :n:`{+ @ident}` is -.. cmd:: Hint hint_definition : {+ @ident} +.. cmd:: Hint @hint_definition : {+ @ident} -**Variants:** + .. cmdv:: Hint @hint_definition -.. cmd:: Hint hint_definition + No database name is given: the hint is registered in the core database. - No database name is given: the hint is registered in the core database. + .. cmdv:: Local Hint @hint_definition : {+ @ident} -.. cmd:: Local Hint hint_definition : {+ @ident} + This is used to declare hints that must not be exported to the other modules + that require and import the current module. Inside a section, the option + Local is useless since hints do not survive anyway to the closure of + sections. - This is used to declare hints that must not be exported to the other modules - that require and import the current module. Inside a section, the option - Local is useless since hints do not survive anyway to the closure of - sections. + .. cmdv:: Local Hint @hint_definition -.. cmd:: Local Hint hint_definition + Idem for the core database. - Idem for the core database. + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + :name: Hint Resolve -The ``hint_definition`` is one of the following expressions: + This command adds :n:`simple apply @term` to the hint list with the head + symbol of the type of :n:`@term`. The cost of that hint is the number of + subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The + associated :n:`@pattern` is inferred from the conclusion of the type of + :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type + of :n:`@term` does not start with a product the tactic added in the hint list + is :n:`exact @term`. In case this type can however be reduced to a type + starting with a product, the tactic :n:`simple apply @term` is also stored in + the hints list. If the inferred type of :n:`@term` contains a dependent + quantification on a variable which occurs only in the premisses of the type + and not in its conclusion, no instance could be inferred for the variable by + unification with the goal. In this case, the hint is added to the hint list + of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A + typical example of a hint that is used only by :tacn:`eauto` is a transitivity + lemma. -+ :n:`Resolve @term {? | {? @num} {? @pattern}}` - This command adds :n:`simple apply @term` to the hint list with the head symbol of the type of - :n:`@term`. The cost of that hint is the number of subgoals generated by - :n:`simple apply @term` or :n:`@num` if specified. The associated :n:`@pattern` - is inferred from the conclusion of the type of :n:`@term` or the given - :n:`@pattern` if specified. In case the inferred type of :n:`@term` does not - start with a product the tactic added in the hint list is :n:`exact @term`. - In case this type can however be reduced to a type starting with a product, - the tactic :n:`simple apply @term` is also stored in the hints list. If the - inferred type of :n:`@term` contains a dependent quantification on a variable - which occurs only in the premisses of the type and not in its conclusion, no - instance could be inferred for the variable by unification with the goal. In - this case, the hint is added to the hint list of :tacn:`eauto` instead of the - hint list of auto and a warning is printed. A typical example of a hint that - is used only by ``eauto`` is a transitivity lemma. + .. exn:: @term cannot be used as a hint - .. exn:: @term cannot be used as a hint + The head symbol of the type of :n:`@term` is a bound variable such that + this tactic cannot be associated to a constant. - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + .. cmdv:: Hint Resolve {+ @term} - **Variants:** + Adds each :n:`Hint Resolve @term`. - + :n:`Resolve {+ @term}` - Adds each :n:`Resolve @term`. + .. cmdv:: Hint Resolve -> @term - + :n:`Resolve -> @term` - Adds the left-to-right implication of an equivalence as a hint (informally - the hint will be used as :n:`apply <- @term`, although as mentionned - before, the tactic actually used is a restricted version of ``apply``). + Adds the left-to-right implication of an equivalence as a hint (informally + the hint will be used as :n:`apply <- @term`, although as mentionned + before, the tactic actually used is a restricted version of + :tacn:`apply`). - + :n:`Resolve <- @term` - Adds the right-to-left implication of an equivalence as a hint. + .. cmdv:: Resolve <- @term -+ :n:`Immediate @term` - This command adds :n:`simple apply @term; trivial` to the hint list associated - with the head symbol of the type of :n:`@ident` in the given database. This - tactic will fail if all the subgoals generated by :n:`simple apply @term` are - not solved immediately by the ``trivial`` tactic (which only tries tactics - with cost 0).This command is useful for theorems such as the symmetry of - equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited - use in order to avoid useless proof-search.The cost of this tactic (which - never generates subgoals) is always 1, so that it is not used by ``trivial`` - itself. + Adds the right-to-left implication of an equivalence as a hint. - .. exn:: @term cannot be used as a hint + .. cmdv:: Hint Immediate @term + :name: Hint Immediate - **Variants:** + This command adds :n:`simple apply @term; trivial` to the hint list associated + with the head symbol of the type of :n:`@ident` in the given database. This + tactic will fail if all the subgoals generated by :n:`simple apply @term` are + not solved immediately by the ``trivial`` tactic (which only tries tactics + with cost 0).This command is useful for theorems such as the symmetry of + equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited + use in order to avoid useless proof-search. The cost of this tactic (which + never generates subgoals) is always 1, so that it is not used by :tacn:`trivial` + itself. - + :n:`Immediate {+ @term}` - Adds each :n:`Immediate @term`. + .. exn:: @term cannot be used as a hint -+ :n:`Constructors @ident` - If :n:`@ident` is an inductive type, this command adds all its constructors as - hints of type Resolve. Then, when the conclusion of current goal has the form - :n:`(@ident ...)`, ``auto`` will try to apply each constructor. + .. cmdv:: Immediate {+ @term} - .. exn:: @ident is not an inductive type + Adds each :n:`Hint Immediate @term`. - **Variants:** + .. cmdv:: Hint Constructors @ident + :name: Hint Constructors - + :n:`Constructors {+ @ident}` - Adds each :n:`Constructors @ident`. + If :n:`@ident` is an inductive type, this command adds all its constructors as + hints of type ``Resolve``. Then, when the conclusion of current goal has the form + :n:`(@ident ...)`, :tacn:`auto` will try to apply each constructor. -+ :n:`Unfold @qualid` - This adds the tactic :n:`unfold @qualid` to the hint list that will only be - used when the head constant of the goal is :n:`@ident`. - Its cost is 4. + .. exn:: @ident is not an inductive type - **Variants:** + .. cmdv:: Hint Constructors {+ @ident} - + :n:`Unfold {+ @ident}` - Adds each :n:`Unfold @ident`. + Adds each :n:`Hint Constructors @ident`. -+ :n:`Transparent`, :n:`Opaque @qualid` - This adds a transparency hint to the database, making :n:`@qualid` a - transparent or opaque constant during resolution. This information is used - during unification of the goal with any lemma in the database and inside the - discrimination network to relax or constrain it in the case of discriminated - databases. + .. cmdv:: Hint Unfold @qualid + :name: Hint Unfold - **Variants:** + This adds the tactic :n:`unfold @qualid` to the hint list that will only be + used when the head constant of the goal is :n:`@ident`. + Its cost is 4. - + :n:`Transparent`, :n:`Opaque {+ @ident}` - Declares each :n:`@ident` as a transparent or opaque constant. + .. cmdv:: Hint Unfold {+ @ident} -+ :n:`Extern @num {? @pattern} => tactic` - This hint type is to extend ``auto`` with tactics other than ``apply`` and - ``unfold``. For that, we must specify a cost, an optional :n:`@pattern` and a - :n:`tactic` to execute. Here is an example:: - - Hint Extern 4 (~(_ = _)) => discriminate. - - Now, when the head of the goal is a disequality, ``auto`` will try - discriminate if it does not manage to solve the goal with hints with a - cost less than 4. One can even use some sub-patterns of the pattern in - the tactic script. A sub-pattern is a question mark followed by an - identifier, like ``?X1`` or ``?X2``. Here is an example: - - .. example:: - .. coqtop:: reset all - - Require Import List. - Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. - Goal forall a b:list (nat * nat), {a = b} + {a <> b}. - Info 1 auto with eqdec. - -+ :n:`Cut @regexp` - - .. warning:: these hints currently only apply to typeclass - proof search and the ``typeclasses eauto`` tactic (:ref:`typeclasses-eauto`). - - This command can be used to cut the proof-search tree according to a regular - expression matching paths to be cut. The grammar for regular expressions is - the following. Beware, there is no operator precedence during parsing, one can - check with ``Print HintDb`` to verify the current cut expression: - - .. productionlist:: `regexp` - e : ident hint or instance identifier - :|_ any hint - :| e\|e′ disjunction - :| e e′ sequence - :| e * Kleene star - :| emp empty - :| eps epsilon - :| ( e ) - - The `emp` regexp does not match any search path while `eps` - matches the empty path. During proof search, the path of - successive successful hints on a search branch is recorded, as a - list of identifiers for the hints (note Hint Extern’s do not have - an associated identifier). - Before applying any hint :n:`@ident` the current path `p` extended with - :n:`@ident` is matched against the current cut expression `c` associated to - the hint database. If matching succeeds, the hint is *not* applied. The - semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the - initial cut expression being `emp`. - -+ :n:`Mode @qualid {* (+ | ! | -)}` - This sets an optional mode of use of the identifier :n:`@qualid`. When - proof-search faces a goal that ends in an application of :n:`@qualid` to - arguments :n:`@term ... @term`, the mode tells if the hints associated to - :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, - ``!`` or ``-`` items that specify if an argument of the identifier is to be - treated as an input (``+``), if its head only is an input (``!``) or an output - (``-``) of the identifier. For a mode to match a list of arguments, input - terms and input heads *must not* contain existential variables or be - existential variables respectively, while outputs can be any term. Multiple - modes can be declared for a single identifier, in that case only one mode - needs to match the arguments for the hints to be applied.The head of a term - is understood here as the applicative head, or the match or projection - scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is - especially useful for typeclasses, when one does not want to support default - instances and avoid ambiguity in general. Setting a parameter of a class as an - input forces proof-search to be driven by that index of the class, with ``!`` - giving more flexibility by allowing existentials to still appear deeper in the - index but not at its head. + Adds each :n:`Hint Unfold @ident`. -.. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on - hypotheses using ``match goal`` with inside the tactic. + .. cmdv:: Hint %( Transparent %| Opaque %) @qualid + :name: Hint ( Transparent | Opaque ) + + This adds a transparency hint to the database, making :n:`@qualid` a + transparent or opaque constant during resolution. This information is used + during unification of the goal with any lemma in the database and inside the + discrimination network to relax or constrain it in the case of discriminated + databases. + + .. cmdv:: Hint %(Transparent | Opaque) {+ @ident} + + Declares each :n:`@ident` as a transparent or opaque constant. + + .. cmdv:: Hint Extern @num {? @pattern} => tactic + + This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and + :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a + :n:`@tactic` to execute. + + .. example:: + + .. coqtop:: in + + Hint Extern 4 (~(_ = _)) => discriminate. + + Now, when the head of the goal is a disequality, ``auto`` will try + discriminate if it does not manage to solve the goal with hints with a + cost less than 4. One can even use some sub-patterns of the pattern in + the tactic script. A sub-pattern is a question mark followed by an + identifier, like ``?X1`` or ``?X2``. Here is an example: + + .. example:: + + .. coqtop:: reset all + + Require Import List. + Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize X1, X2; decide equality : eqdec. + Goal forall a b:list (nat * nat), {a = b} + {a <> b}. + Info 1 auto with eqdec. + + .. cmdv:: Hint Cut @regexp + + .. warning:: + + These hints currently only apply to typeclass proof search and the + :tacn:`typeclasses eauto` tactic. + + This command can be used to cut the proof-search tree according to a regular + expression matching paths to be cut. The grammar for regular expressions is + the following. Beware, there is no operator precedence during parsing, one can + check with :cmd:`Print HintDb` to verify the current cut expression: + + .. productionlist:: `regexp` + e : ident hint or instance identifier + :|_ any hint + :| e\|e′ disjunction + :| e e′ sequence + :| e * Kleene star + :| emp empty + :| eps epsilon + :| ( e ) + + The `emp` regexp does not match any search path while `eps` + matches the empty path. During proof search, the path of + successive successful hints on a search branch is recorded, as a + list of identifiers for the hints (note Hint Extern’s do not have + an associated identifier). + Before applying any hint :n:`@ident` the current path `p` extended with + :n:`@ident` is matched against the current cut expression `c` associated to + the hint database. If matching succeeds, the hint is *not* applied. The + semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the + initial cut expression being `emp`. + + .. cmdv:: Hint Mode @qualid {* (+ | ! | -)} + + This sets an optional mode of use of the identifier :n:`@qualid`. When + proof-search faces a goal that ends in an application of :n:`@qualid` to + arguments :n:`@term ... @term`, the mode tells if the hints associated to + :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``, + ``!`` or ``-`` items that specify if an argument of the identifier is to be + treated as an input (``+``), if its head only is an input (``!``) or an output + (``-``) of the identifier. For a mode to match a list of arguments, input + terms and input heads *must not* contain existential variables or be + existential variables respectively, while outputs can be any term. Multiple + modes can be declared for a single identifier, in that case only one mode + needs to match the arguments for the hints to be applied.The head of a term + is understood here as the applicative head, or the match or projection + scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is + especially useful for typeclasses, when one does not want to support default + instances and avoid ambiguity in general. Setting a parameter of a class as an + input forces proof-search to be driven by that index of the class, with ``!`` + giving more flexibility by allowing existentials to still appear deeper in the + index but not at its head. + + .. note:: + + One can use an ``Extern`` hint with no pattern to do pattern-matching on + hypotheses using ``match goal`` with inside the tactic. Hint databases defined in the Coq standard library @@ -3587,7 +3660,7 @@ non-imported hints. Setting implicit automation tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Proof with tactic +.. cmd:: Proof with @tactic This command may be used to start a proof. It defines a default tactic to be used each time a tactic command ``tactic``:sub:`1` is ended by ``...``. @@ -3601,11 +3674,11 @@ Setting implicit automation tactics Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmdv:: Proof using {+ @ident} with tactic + .. cmdv:: Proof using {+ @ident} with @tactic Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` - .. cmd:: Declare Implicit Tactic tactic + .. cmd:: Declare Implicit Tactic @tactic This command declares a tactic to be used to solve implicit arguments that Coq does not know how to solve by unification. It is used every @@ -3669,11 +3742,12 @@ Therefore, the use of :tacn:`intros` in the previous proof is unnecessary. an instantiation of `x` is necessary. .. tacv:: dtauto + :name: dtauto - While :tacn:`tauto` recognizes inductively defined connectives isomorphic to - the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, - :tacn:`dtauto` recognizes also all inductive types with one constructors and - no indices, i.e. record-style connectives. + While :tacn:`tauto` recognizes inductively defined connectives isomorphic to + the standard connective ``and, prod, or, sum, False, Empty_set, unit, True``, + :tacn:`dtauto` recognizes also all inductive types with one constructors and + no indices, i.e. record-style connectives. .. tacn:: intuition @tactic :name: intuition @@ -3746,13 +3820,15 @@ 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 default tactic used by :tacn:`firstorder` when no rule applies is :g:`auto -with \*`, it can be reset locally or globally using the :opt:`Firstorder Solver` -option and printed using :cmd:`Print Firstorder Solver`. +.. opt:: Firstorder Solver + + The default tactic used by :tacn:`firstorder` when no rule applies is + :g:`auto with *`, it can be reset locally or globally using this option and + printed using :cmd:`Print Firstorder Solver`. .. tacv:: firstorder @tactic - Tries to solve the goal with :n:`@tactic` when no logical rule may apply. + Tries to solve the goal with :n:`@tactic` when no logical rule may apply. .. tacv:: firstorder using {+ @qualid} @@ -3991,6 +4067,7 @@ symbol :g:`=`. .. tacv:: esimplify_eq @num .. tacv:: 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 type of the hypothesis referred to by :n:`@num`, has uninstantiated @@ -4002,7 +4079,7 @@ symbol :g:`=`. :n:`intro @ident; simplify_eq @ident`. .. tacn:: dependent rewrite -> @ident - :name: dependent rewrite -> + :name: dependent rewrite This tactic applies to any goal. If :n:`@ident` has type :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each @@ -4270,7 +4347,7 @@ This tactics reverses the list of the focused goals. This tactic moves all goals under focus to a shelf. While on the shelf, goals will not be focused on. They can be solved by unification, or they can be called back into focus with the command - :tacn:`Unshelve`. + :cmd:`Unshelve`. .. tacv:: shelve_unifiable @@ -4286,8 +4363,7 @@ This tactics reverses the list of the focused goals. all:shelve_unifiable. reflexivity. -.. tacn:: Unshelve - :name: Unshelve +.. cmd:: Unshelve This command moves all the goals on the shelf (see :tacn:`shelve`) from the shelf into focus, by appending them to the end of the current diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 6a20c0466..d0d7d74af 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -39,6 +39,7 @@ This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid` denotes a global constant. .. cmdv:: About @qualid. + :name: About This displays various information about the object denoted by :n:`@qualid`: its kind (module, constant, assumption, inductive, @@ -61,6 +62,7 @@ Variants: .. cmdv:: Inspect @num. + :name: Inspect This command displays the :n:`@num` last objects of the current environment, including sections and modules. @@ -186,9 +188,17 @@ This command prints the current value of :n:`@option`. .. TODO : table is not a syntax entry .. cmd:: Add @table @value. + :name: Add `table` `value` + .. cmd:: Remove @table @value. + :name: Remove `table` `value` + .. cmd:: Test @table @value. + :name: Test `table` `value` + .. cmd:: Test @table for @value. + :name: Test `table` for `value` + .. cmd:: Print Table @table. These are general commands for tables. @@ -693,9 +703,9 @@ The command did not find the file foo.vo. Either foo.v exists but is not compiled or foo.vo is in a directory which is not in your LoadPath (see Section :ref:`libraries-and-filesystem`). -.. exn:: Compiled library ident.vo makes inconsistent assumptions over library qualid +.. exn:: Compiled library @ident.vo makes inconsistent assumptions over library qualid -The command tried to load library file `ident.vo` that +The command tried to load library file :n:`@ident`.vo that depends on some specific version of library :n:`@qualid` which is not the one already loaded in the current |Coq| session. Probably `ident.v` was not properly recompiled with the last version of the file containing @@ -761,7 +771,7 @@ Error messages: .. exn:: File not found on loadpath : @string -.. exn:: Loading of ML object file forbidden in a native |Coq| +.. exn:: Loading of ML object file forbidden in a native Coq @@ -1025,16 +1035,13 @@ to |Coq| with the command: go();; +.. warning:: - -Warnings: - - -#. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, - see Section `interactive-use`). -#. You must have compiled |Coq| from the source package and set the - environment variable COQTOP to the root of your copy of the sources - (see Section `customization-by-environment-variables`). + #. It only works with the bytecode version of |Coq| (i.e. `coqtop.byte`, + see Section `interactive-use`). + #. You must have compiled |Coq| from the source package and set the + environment variable COQTOP to the root of your copy of the sources + (see Section `customization-by-environment-variables`). @@ -1089,7 +1096,7 @@ Controlling display This option controls the normal displaying. -.. opt:: Warnings "@ident {* , @ident }" +.. opt:: Warnings "{+, {? %( - %| + %) } @ident }" This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -1129,10 +1136,10 @@ Controlling display .. opt:: Printing Unfocused This option controls whether unfocused goals are displayed. Such goals are - created by focusing other goals with bullets (see :ref:`bullets`) or curly - braces (see `here <curly-braces>`). It is off by default. + created by focusing other goals with bullets (see :ref:`bullets` or + :ref:`curly braces <curly-braces>`). It is off by default. -.. cmd:: Printing Dependent Evars Line +.. opt:: Printing Dependent Evars Line This option controls the printing of the “(dependent evars: …)” line when ``-emacs`` is passed. @@ -1150,7 +1157,7 @@ conversion algorithm lazily compares applicative terms while the other is a brute-force but efficient algorithm that first normalizes the terms before comparing them. The second algorithm is based on a bytecode representation of terms similar to the bytecode -representation used in the ZINC virtual machine [`98`]. It is +representation used in the ZINC virtual machine :cite:`Leroy90`. It is especially useful for intensive computation of algebraic values, such as numbers, and for reflection-based tactics. The commands to fine- tune the reduction strategies and the lazy conversion algorithm are diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst index 8a24a382a..e12e4d897 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 := Induction for ident' Sort sort {* with ident := Induction for ident' Sort sort} +.. cmd:: Scheme @ident := Induction for @ident Sort sort {* with @ident := Induction for @ident Sort sort} where each `ident'ᵢ` is a different inductive type identifier belonging to the same package of mutual inductive definitions. This @@ -20,17 +20,17 @@ command generates the `identᵢ`s to be mutually recursive definitions. Each term `identᵢ` proves a general principle of mutual induction for objects in type `identᵢ`. -.. 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. -.. cmdv:: Scheme Equality for ident +.. cmdv:: Scheme Equality for @ident 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). @@ -103,6 +103,8 @@ induction for objects in type `identᵢ`. Automatic declaration of schemes ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Elimination Schemes + It is possible to deactivate the automatic declaration of the induction principles when defining a new inductive type with the ``Unset Elimination Schemes`` command. It may be reactivated at any time with @@ -113,15 +115,22 @@ induction principles when defining a new inductive type with the This option controls whether types declared with the keywords :cmd:`Variant` and :cmd:`Record` get an automatic declaration of the induction principles. -In addition, the ``Case Analysis Schemes`` flag governs the generation of -case analysis lemmas for inductive types, i.e. corresponding to the -pattern-matching term alone and without fixpoint. -You can also activate the automatic declaration of those Boolean -equalities (see the second variant of ``Scheme``) with respectively the -commands ``Set Boolean Equality Schemes`` and ``Set Decidable Equality -Schemes``. However you have to be careful with this option since Coq may -now reject well-defined inductive types because it cannot compute a -Boolean equality for them. +.. opt:: Case Analysis Schemes + + This flag governs the generation of case analysis lemmas for inductive types, + i.e. corresponding to the pattern-matching term alone and without fixpoint. + +.. opt:: Boolean Equality Schemes + +.. opt:: Decidable Equality Schemes + +These flags control the automatic declaration of those Boolean equalities (see +the second variant of ``Scheme``). + +.. warning:: + + You have to be careful with this option since Coq may now reject well-defined + inductive types because it cannot compute a Boolean equality for them. .. opt:: Rewriting Schemes @@ -134,7 +143,7 @@ The ``Combined Scheme`` command is a tool for combining induction principles generated by the ``Scheme command``. Its syntax follows the schema : -.. cmd:: Combined Scheme ident from {+, ident} +.. cmd:: Combined Scheme @ident from {+, ident} where each identᵢ after the ``from`` is a different inductive principle that must belong to the same package of mutual inductive principle definitions. @@ -175,7 +184,7 @@ generating automatically induction principles corresponding to 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 := Induction for ident' Sort sort {* with @ident := Induction for @ident 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 @@ -316,7 +325,7 @@ Generation of inversion principles with ``Derive`` ``Inversion`` The syntax of ``Derive`` ``Inversion`` follows the schema: -.. cmd:: Derive Inversion ident with forall (x : T), I t Sort sort +.. cmd:: Derive Inversion @ident with forall (x : T), I t Sort sort This command generates an inversion principle for the `inversion … using` tactic. Let `I` be an inductive predicate and `x` the variables occurring @@ -325,17 +334,17 @@ sort `sort` corresponding to the instance `∀ (x:T), I t` with the name `ident` in the global environment. When applied, it is equivalent to having inverted the instance with the tactic `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`. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 9965d5002..c4a7121ce 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -32,6 +32,8 @@ Notations Basic notations ~~~~~~~~~~~~~~~ +.. cmd:: Notation + A *notation* is a symbolic expression denoting some term or term pattern. @@ -1200,7 +1202,7 @@ Tactic notations allow to customize the syntax of the tactics of the tactic language. Tactic notations obey the following syntax: .. productionlist:: coq - tacn : [Local] Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. + tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `natural`) tactic_argument_type : ident | simple_intropattern | reference @@ -1211,7 +1213,7 @@ tactic language. Tactic notations obey the following syntax: : | tactic | tactic0 | tactic1 | tactic2 | tactic3 : | tactic4 | tactic5 -.. cmd:: {? Local} Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. +.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the |