diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 1634 |
1 files changed, 862 insertions, 772 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 2af73c28e..29c2f8b81 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -24,7 +24,7 @@ Each (sub)goal is denoted with a number. The current goal is numbered 1. By default, a tactic is applied to the current goal, but one can address a particular goal in the list by writing n:tactic which means “apply tactic tactic to goal number n”. We can show the list of -subgoals by typing Show (see Section :ref:`TODO-7.3.1-Show`). +subgoals by typing Show (see Section :ref:`requestinginformation`). Since not every rule applies to a given statement, every tactic cannot be used to reduce any goal. In other words, before applying a tactic @@ -34,15 +34,16 @@ satisfied. If it is not the case, the tactic raises an error message. Tactics are built from atomic tactics and tactic expressions (which extends the folklore notion of tactical) to combine those atomic tactics. This chapter is devoted to atomic tactics. The tactic -language will be described in Chapter :ref:`TODO-9-Thetacticlanguage`. +language will be described in Chapter :ref:`ltac`. + +.. _invocation-of-tactics: Invocation of tactics ------------------------- A tactic is applied as an ordinary command. It may be preceded by a -goal selector (see Section :ref:`TODO-9.2-Semantics`). If no selector is -specified, the default selector (see Section -:ref:`TODO-8.1.1-Setdefaultgoalselector`) is used. +goal selector (see Section :ref:`ltac-semantics`). If no selector is +specified, the default selector is used. .. _tactic_invocation_grammar: @@ -50,20 +51,22 @@ specified, the default selector (see Section tactic_invocation : toplevel_selector : tactic. : |tactic . -.. cmd:: Set 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. The initial value is 1, hence the + tactics are, by default, applied to the first goal. -After using this command, the default selector – used when no selector -is specified when applying a tactic – is set to the chosen value. The -initial value is 1, hence the tactics are, by default, applied to the -first goal. Using Set Default Goal Selector ‘‘all’’ will make is so -that tactics are, by default, applied to every goal simultaneously. -Then, to apply a tactic tac to the first goal only, you can write -1:tac. Although more selectors are available, only ‘‘all’’ or a single -natural number are valid default goal selectors. + Using value ``all`` will make it so that tactics are, by default, + applied to every goal simultaneously. Then, to apply a tactic tac + to the first goal only, you can write ``1:tac``. -.. cmd:: Test Default Goal Selector. + Using value ``!`` enforces that all tactics are used either on a + single focused goal or with a local selector (’’strict focusing + mode’’). -This command displays the current default selector. + Although more selectors are available, only ``all``, ``!`` or a + single natural number are valid default goal selectors. .. _bindingslist: @@ -89,14 +92,14 @@ bindings_list`` where ``bindings_list`` may be of two different forms: the ``n``-th non dependent premise of the ``term``, as determined by the type of ``term``. - .. exn:: No such binder + .. exn:: No such binder. + A bindings list can also be a simple list of terms :n:`{* term}`. In that case the references to which these terms correspond are - determined by the tactic. In case of ``induction``, ``destruct``, ``elim`` - and ``case`` (see :ref:`TODO-9-Thetacticlanguage`) the terms have to + determined by the tactic. In case of :tacn:`induction`, :tacn:`destruct`, :tacn:`elim` + and :tacn:`case`, the terms have to provide instances for all the dependent products in the type of term while in - the case of ``apply``, or of ``constructor`` and its variants, only instances + the case of :tacn:`apply`, or of :tacn:`constructor` and its variants, only instances for the dependent products that are not bound in the conclusion of the type are required. @@ -122,14 +125,12 @@ following syntax: The role of an occurrence clause is to select a set of occurrences of a term in a goal. In the first case, the :n:`@ident {? at {* num}}` parts indicate that -occurrences have to be selected in the hypotheses named :n:`@ident`. If no numbers -are given for hypothesis :n:`@ident`, then all the occurrences of `term` in the -hypothesis are selected. If numbers are given, they refer to occurrences of -`term` when the term is printed using option ``Set Printing All`` (see -:ref:`TODO-2.9-Printingconstructionsinfull`), counting from left to right. In -particular, occurrences of `term` in implicit arguments (see -:ref:`TODO-2.7-Implicitarguments`) or coercions (see :ref:`TODO-2.8-Coercions`) -are counted. +occurrences have to be selected in the hypotheses named :n:`@ident`. If no +numbers are given for hypothesis :n:`@ident`, then all the occurrences of `term` +in the hypothesis are selected. If numbers are given, they refer to occurrences +of `term` when the term is printed using option :opt:`Printing All`, counting +from left to right. In particular, occurrences of `term` in implicit arguments +(see :ref:`ImplicitArguments`) or coercions (see :ref:`Coercions`) are counted. If a minus sign is given between at and the list of occurrences, it negates the condition so that the clause denotes all the occurrences @@ -150,14 +151,15 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected. Finally, the last notation is an abbreviation for ``* |- *``. Note also that ``|-`` is optional in the first case when no ``*`` is given. -Here are some tactics that understand occurrences clauses: ``set``, ``remember`` -, ``induction``, ``destruct``. +Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember` +, :tacn:`induction`, :tacn:`destruct`. -See also: :ref:`TODO-8.3.7-Managingthelocalcontext`, -:ref:`TODO-8.5.2-Caseanalysisandinduction`, -:ref:`TODO-2.9-Printingconstructionsinfull`. +See also: :ref:`Managingthelocalcontext`, +:ref:`caseanalysisandinduction`, +:ref:`printing_constructions_full`. +.. _applyingtheorems: Applying theorems --------------------- @@ -165,195 +167,203 @@ Applying theorems .. tacn:: exact @term :name: exact -This tactic applies to any goal. It gives directly the exact proof -term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then -``exact p`` succeeds iff ``T`` and ``U`` are convertible (see -:ref:`TODO-4.3-Conversionrules`). + This tactic applies to any goal. It gives directly the exact proof + term of the goal. Let ``T`` be our goal, let ``p`` be a term of type ``U`` then + ``exact p`` succeeds iff ``T`` and ``U`` are convertible (see + :ref:`Conversion-rules`). -.. exn:: Not an exact proof. + .. exn:: Not an exact proof. -.. tacv:: eexact @term. + .. tacv:: eexact @term. + :name: eexact -This tactic behaves like exact but is able to handle terms and goals with -meta-variables. + This tactic behaves like exact but is able to handle terms and goals with + meta-variables. .. tacn:: assumption :name: assumption -This tactic looks in the local context for an hypothesis which type is equal to -the goal. If it is the case, the subgoal is proved. Otherwise, it fails. + This tactic looks in the local context for an hypothesis which type is equal to + the goal. If it is the case, the subgoal is proved. Otherwise, it fails. -.. exn:: No such assumption. + .. exn:: No such assumption. -.. tacv:: eassumption + .. tacv:: eassumption + :name: eassumption -This tactic behaves like assumption but is able to handle goals with -meta-variables. + This tactic behaves like assumption but is able to handle goals with + meta-variables. .. tacn:: refine @term :name: refine -This tactic applies to any goal. It behaves like exact with a big -difference: the user can leave some holes (denoted by ``_`` or``(_:type)``) in -the term. refine will generate as many subgoals as there are holes in -the term. The type of holes must be either synthesized by the system -or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that -occurs in other subgoals is automatically shelved, as if calling -shelve_unifiable (see Section 8.17.4). This low-level tactic can be -useful to advanced users. + This tactic applies to any goal. It behaves like :tacn:`exact` with a big + difference: the user can leave some holes (denoted by ``_`` or ``(_:type)``) in + the term. :tacn:`refine` will generate as many subgoals as there are holes in + the term. The type of holes must be either synthesized by the system + or declared by an explicit cast like ``(_:nat->Prop)``. Any subgoal that + occurs in other subgoals is automatically shelved, as if calling + :tacn:`shelve_unifiable`. This low-level tactic can be + useful to advanced users. -.. example:: - .. coqtop:: reset all + .. example:: + .. coqtop:: reset all - Inductive Option : Set := - | Fail : Option - | Ok : bool -> Option. + Inductive Option : Set := + | Fail : Option + | Ok : bool -> Option. - Definition get : forall x:Option, x <> Fail -> bool. + Definition get : forall x:Option, x <> Fail -> bool. - refine - (fun x:Option => - match x return x <> Fail -> bool with - | Fail => _ - | Ok b => fun _ => b - end). + refine + (fun x:Option => + match x return x <> Fail -> bool with + | Fail => _ + | Ok b => fun _ => b + end). - intros; absurd (Fail = Fail); trivial. + intros; absurd (Fail = Fail); trivial. - Defined. + Defined. -.. exn:: invalid argument + .. exn:: Invalid argument. - The tactic ``refine`` does not know what to do with the term you gave. + The tactic :tacn:`refine` does not know what to do with the term you gave. -.. exn:: Refine passed ill-formed term + .. exn:: Refine passed ill-formed term. - The term you gave is not a valid proof (not easy to debug in general). This - message may also occur in higher-level tactics that call ``refine`` - internally. + The term you gave is not a valid proof (not easy to debug in general). This + message may also occur in higher-level tactics that call :tacn:`refine` + internally. -.. exn:: Cannot infer a term for this placeholder + .. exn:: Cannot infer a term for this placeholder. + :name: Cannot infer a term for this placeholder. (refine) - There is a hole in the term you gave which type cannot be inferred. Put a - cast around it. + There is a hole in the term you gave whose type cannot be inferred. Put a + cast around it. -.. tacv:: simple refine @term + .. 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. + This tactic behaves like refine, but it does not shelve any subgoal. It does + not perform any beta-reduction either. -.. tacv:: notypeclasses refine @term + .. tacv:: notypeclasses refine @term + :name: notypeclasses refine - This tactic behaves like ``refine`` except it performs typechecking without - resolution of typeclasses. + This tactic behaves like :tacn:`refine` except it performs typechecking without + resolution of typeclasses. -.. tacv:: simple notypeclasses refine @term + .. tacv:: simple notypeclasses refine @term + :name: simple notypeclasses refine - This tactic behaves like ``simple refine`` except it performs typechecking - without resolution of typeclasses. + This tactic behaves like :tacn:`simple refine` except it performs typechecking + without resolution of typeclasses. -.. tacv:: apply @term +.. tacn:: apply @term :name: apply -This tactic applies to any goal. The argument term is a term well-formed in the -local context. The tactic apply tries to match the current goal against the -conclusion of the type of term. If it succeeds, then the tactic returns as many -subgoals as the number of non-dependent premises of the type of term. If the -conclusion of the type of term does not match the goal *and* the conclusion is -an inductive type isomorphic to a tuple type, then each component of the tuple -is recursively matched to the goal in the left-to-right order. + This tactic applies to any goal. The argument term is a term well-formed in the + local context. The tactic apply tries to match the current goal against the + conclusion of the type of term. If it succeeds, then the tactic returns as many + subgoals as the number of non-dependent premises of the type of term. If the + conclusion of the type of term does not match the goal *and* the conclusion is + an inductive type isomorphic to a tuple type, then each component of the tuple + is recursively matched to the goal in the left-to-right order. -The tactic ``apply`` relies on first-order unification with dependent types -unless the conclusion of the type of ``term`` is of the form :g:`P (t`:sub:`1` -:g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior -depends on the form of the goal. If the goal is of the form -:g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and -:g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, -``apply`` tries to define :g:`P` by abstracting over :g:`t`:sub:`1` :g:`...` -:g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it -gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. + The tactic :tacn:`apply` relies on first-order unification with dependent types + unless the conclusion of the type of :token:`term` is of the form :g:`P (t`:sub:`1` + :g:`...` :g:`t`:sub:`n` :g:`)` with `P` to be instantiated. In the latter case, the behavior + depends on the form of the goal. If the goal is of the form + :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n` and the :g:`t`:sub:`i` and + :g:`u`:sub:`i` unifies, then :g:`P` is taken to be :g:`(fun x => Q)`. Otherwise, + :tacn:`apply` tries to define :g:`P` by abstracting over :g:`t`:sub:`1` :g:`...` + :g:`t`:sub:`n` in the goal. See :tacn:`pattern` to transform the goal so that it + gets the form :g:`(fun x => Q) u`:sub:`1` :g:`...` :g:`u`:sub:`n`. -.. exn:: Unable to unify ... with ... . + .. exn:: Unable to unify ... with ... . -The apply tactic failed to match the conclusion of term and the current goal. -You can help the apply tactic by transforming your goal with the -:ref:`change <change_term>` or :tacn:`pattern` tactics. + The apply tactic failed to match the conclusion of :token:`term` and the + current goal. You can help the apply tactic by transforming your goal with + the :tacn:`change` or :tacn:`pattern` tactics. -.. exn:: Unable to find an instance for the variables {+ @ident}. + .. exn:: Unable to find an instance for the variables {+ @ident}. -This occurs when some instantiations of the premises of term are not deducible -from the unification. This is the case, for instance, when you want to apply a -transitivity property. In this case, you have to use one of the variants below: + This occurs when some instantiations of the premises of :token:`term` are not deducible + from the unification. This is the case, for instance, when you want to apply a + transitivity property. In this case, you have to use one of the variants below: -.. cmd:: apply @term with {+ @term} + .. tacv:: apply @term with {+ @term} -Provides apply with explicit instantiations for all dependent premises of the -type of term that do not occur in the conclusion and consequently cannot be -found by unification. Notice that the collection :n:`{+ @term}` must be given -according to the order of these dependent premises of the type of term. + Provides apply with explicit instantiations for all dependent premises of the + type of term that do not occur in the conclusion and consequently cannot be + found by unification. Notice that the collection :n:`{+ @term}` must be given + according to the order of these dependent premises of the type of term. -.. exn:: Not the right number of missing arguments. + .. exn:: Not the right number of missing arguments. -.. tacv:: apply @term with @bindings_list + .. tacv:: apply @term with @bindings_list -This also provides apply with values for instantiating premises. Here, variables -are referred by names and non-dependent products by increasing numbers (see -:ref:`bindings list <bindingslist>`). + This also provides apply with values for instantiating premises. Here, variables + are referred by names and non-dependent products by increasing numbers (see + :ref:`bindings list <bindingslist>`). -.. tacv:: apply {+, @term} + .. tacv:: apply {+, @term} -This is a shortcut for ``apply term``:sub:`1` -``; [.. | ... ; [ .. | apply`` ``term``:sub:`n` ``] ... ]``, -i.e. for the successive applications of ``term``:sub:`i+1` on the last subgoal -generated by ``apply term``:sub:`i` , starting from the application of -``term``:sub:`1`. + This is a shortcut for :n:`apply @term`:sub:`1` + :n:`; [.. | ... ; [ .. | apply @term`:sub:`n` :n:`] ... ]`, + i.e. for the successive applications of :token:`term`:sub:`i+1` on the last subgoal + generated by :n:`apply @term`:sub:`i` , starting from the application of + :token:`term`:sub:`1`. -.. tacv:: eapply @term - :name: eapply + .. tacv:: eapply @term + :name: eapply -The tactic ``eapply`` behaves like ``apply`` but it does not fail when no -instantiations are deducible for some variables in the premises. Rather, it -turns these variables into existential variables which are variables still to -instantiate (see :ref:`TODO-2.11-ExistentialVariables`). The instantiation is -intended to be found later in the proof. + The tactic :tacn:`eapply` behaves like :tacn:`apply` but it does not fail when no + instantiations are deducible for some variables in the premises. Rather, it + turns these variables into existential variables which are variables still to + instantiate (see :ref:`Existential-Variables`). The instantiation is + intended to be found later in the proof. -.. tacv:: simple apply @term. + .. 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 -does not succeed because it would require the conversion of ``id ?foo`` and -``O``. + This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms + that contain no variables to instantiate. For instance, the following example + does not succeed because it would require the conversion of ``id ?foo`` and + :g:`O`. -.. example:: + .. example:: - .. coqtop:: all + .. coqtop:: all - Definition id (x : nat) := x. - Hypothesis H : forall y, id y = y. - Goal O = O. - Fail simple apply H. + Definition id (x : nat) := x. + Parameter H : forall y, id y = y. + Goal O = O. + Fail simple apply H. -Because it reasons modulo a limited amount of conversion, ``simple apply`` fails -quicker than ``apply`` and it is then well-suited for uses in user-defined -tactics that backtrack often. Moreover, it does not traverse tuples as ``apply`` -does. + Because it reasons modulo a limited amount of conversion, :tacn:`simple apply` fails + quicker than :tacn:`apply` and it is then well-suited for uses in user-defined + tactics that backtrack often. Moreover, it does not traverse tuples as :tacn:`apply` + does. -.. tacv:: {? simple} apply {+, @term {? with @bindings_list}} -.. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} + .. 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``. + This summarizes the different syntaxes for :tacn:`apply` and :tacn:`eapply`. -.. tacv:: lapply @term - :name: `lapply + .. tacv:: lapply @term + :name: lapply -This tactic applies to any goal, say :g:`G`. The argument term has to be -well-formed in the current context, its type being reducible to a non-dependent -product :g:`A -> B` with :g:`B` possibly containing products. Then it generates -two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type -:g:`A->B` and :g:`B` does not start with a product) does the same as giving the -sequence ``cut B. 2:apply H.`` where ``cut`` is described below. + This tactic applies to any goal, say :g:`G`. The argument term has to be + well-formed in the current context, its type being reducible to a non-dependent + product :g:`A -> B` with :g:`B` possibly containing products. Then it generates + two subgoals :g:`B->G` and :g:`A`. Applying ``lapply H`` (where :g:`H` has type + :g:`A->B` and :g:`B` does not start with a product) does the same as giving the + sequence ``cut B. 2:apply H.`` where ``cut`` is described below. -.. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. + .. warn:: When @term contains more than one non dependent product the tactic lapply only takes into account the first product. .. example:: Assume we have a transitive relation ``R`` on ``nat``: @@ -435,7 +445,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. ``forall A, ... -> A``. Excluding this kind of lemma can be avoided by setting the following option: -.. opt:: Set Universal Lemma Under Conjunction. +.. opt:: Universal Lemma Under Conjunction This option, which preserves compatibility with versions of Coq prior to 8.4 is also available for :n:`apply @term in @ident` (see :tacn:`apply ... in`). @@ -493,7 +503,7 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. .. tacv:: eapply {+, @term with @bindings_list} in @ident as @intro_pattern. - This works as :tacn:`apply ... in as` but using ``eapply``. + This works as :tacn:`apply ... in ... as` but using ``eapply``. .. tacv:: simple apply @term in @ident @@ -501,15 +511,15 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. on subterms that contain no variables to instantiate. For instance, if :g:`id := fun x:nat => x` and :g:`H: forall y, id y = y -> True` and :g:`H0 : O = O` then ``simple apply H in H0`` does not succeed because it - would require the conversion of :g:`id ?1234` and :g:`O` where :g:`?1234` is - a variable to instantiate. Tactic :n:`simple apply @term in @ident` does not + would require the conversion of :g:`id ?x` and :g:`O` where :g:`?x` is + an existential variable to instantiate. Tactic :n:`simple apply @term in @ident` does not either traverse tuples as :n:`apply @term in @ident` does. .. tacv:: {? simple} apply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} .. tacv:: {? simple} eapply {+, @term {? with @bindings_list}} in @ident {? as @intro_pattern} - This summarizes the different syntactic variants of :n:`apply @term in - @ident` and :n:`eapply @term in @ident`. + This summarizes the different syntactic variants of :n:`apply @term in @ident` + and :n:`eapply @term in @ident`. .. tacn:: constructor @num :name: constructor @@ -539,14 +549,16 @@ 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 @@ -559,7 +571,10 @@ sequence ``cut B. 2:apply H.`` where ``cut`` is described below. 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`. @@ -577,15 +592,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: @@ -598,48 +623,53 @@ Managing the local context This tactic applies to a goal that is either a product or starts with a let binder. If the goal is a product, the tactic implements the "Lam" rule given in -:ref:`TODO-4.2-Typing-rules` [1]_. If the goal starts with a let binder, then the +:ref:`Typing-rules` [1]_. If the goal starts with a let binder, then the tactic implements a mix of the "Let" and "Conv". -If the current goal is a dependent product :math:`\forall` :g:`x:T, U` (resp +If the current goal is a dependent product :g:`forall x:T, U` (resp :g:`let x:=t in U`) then ``intro`` puts :g:`x:T` (resp :g:`x:=t`) in the local context. The new subgoal is :g:`U`. If the goal is a non-dependent product :g:`T`:math:`\rightarrow`:g:`U`, then it puts in the local context either :g:`Hn:T` (if :g:`T` is of type :g:`Set` or -:g:`Prop`) or Xn:T (if the type of :g:`T` is :g:`Type`). The optional index +:g:`Prop`) or :g:`Xn:T` (if the type of :g:`T` is :g:`Type`). The optional index ``n`` is such that ``Hn`` or ``Xn`` is a fresh identifier. In both cases, the new subgoal is :g:`U`. -If the goal is neither a product nor starting with a let definition, +If the goal is an existential variable, ``intro`` forces the resolution of the +existential variable into a dependent product :math:`forall`:g:`x:?X, ?Y`, puts +:g:`x:?X` in the local context and leaves :g:`?Y` as a new subgoal allowed to +depend on :g:`x`. + 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 + :name: intros This repeats ``intro`` until it meets the head-constant. It never reduces head-constants and it never fails. -.. tac:: intro @ident +.. tacn:: intro @ident This applies ``intro`` but forces :n:`@ident` to be the name of the introduced hypothesis. -.. exn:: name @ident is already used +.. exn:: Name @ident is already used. .. note:: If a name used by intro hides the base name of a global constant then the latter can still be referred to by a qualified name - (see :ref:`TODO-2.6.2-Qualified-names`). + (see :ref:`Qualified-names`). .. tacv:: intros {+ @ident}. This is equivalent to the composed tactic :n:`intro @ident; ... ; intro @ident`. More generally, the ``intros`` tactic takes a pattern as argument in order to introduce names for components of an inductive definition or to clear introduced hypotheses. This is - explained in :ref:`TODO-8.3.2`. + explained in :ref:`Managingthelocalcontext`. .. tacv:: intros until @ident @@ -647,7 +677,7 @@ be applied or the goal is not head-reducible. `(@ident:term)` and discharges the variable named `ident` of the current goal. -.. exn:: No such hypothesis in current goal +.. exn:: No such hypothesis in current goal. .. tacv:: intros until @num @@ -676,7 +706,7 @@ be applied or the goal is not head-reducible. too so as to respect the order of dependencies between hypotheses. Note that :n:`intro at bottom` is a synonym for :n:`intro` with no argument. -.. exn:: No such hypothesis : @ident. +.. exn:: No such hypothesis: @ident. .. tacv:: intro @ident after @ident .. tacv:: intro @ident before @ident @@ -685,7 +715,7 @@ be applied or the goal is not head-reducible. These tactics behave as previously but naming the introduced hypothesis :n:`@ident`. It is equivalent to :n:`intro @ident` followed by the - appropriate call to move (see :tacn:`move ... after`). + appropriate call to ``move`` (see :tacn:`move ... after ...`). .. tacn:: intros @intro_pattern_list :name: intros ... @@ -730,7 +760,7 @@ be applied or the goal is not head-reducible. Assuming a goal of type :g:`Q → P` (non-dependent product), or of type - :math:`\forall`:g:`x:T, P` (dependent product), the behavior of + :g:`forall x:T, P` (dependent product), the behavior of :n:`intros p` is defined inductively over the structure of the introduction pattern :n:`p`: @@ -827,15 +857,10 @@ quantification or an implication. so that all the arguments of the i-th constructors of the corresponding inductive type are introduced can be controlled with the following option: - .. cmd:: Set Bracketing Last Introduction Pattern. - - Force completion, if needed, when the last introduction pattern is a - disjunctive or conjunctive pattern (this is the default). + .. opt:: Bracketing Last Introduction Pattern - .. cmd:: Unset Bracketing Last Introduction Pattern. - - Deactivate completion when the last introduction pattern is a disjunctive or - conjunctive pattern. + Force completion, if needed, when the last introduction pattern is a + disjunctive or conjunctive pattern (on by default). .. tacn:: clear @ident :name: clear @@ -854,13 +879,6 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clearbody @ident - - This tactic expects :n:`@ident` to be a local definition then clears its - body. Otherwise said, this tactic turns a definition into an assumption. - -.. exn:: @ident is not a local definition - .. tacv:: clear - {+ @ident} This tactic clears all the hypotheses except the ones depending in the @@ -875,24 +893,33 @@ quantification or an implication. This clears the hypothesis :n:`@ident` and all the hypotheses that depend on it. +.. tacv:: clearbody {+ @ident} + :name: clearbody + + This tactic expects :n:`{+ @ident}` to be local definitions and clears their + respective bodies. + In other words, it turns the given definitions into assumptions. + +.. exn:: @ident is not a local definition. + .. 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 -the inverse of :tacn:`intro`. + 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 + the inverse of :tacn:`intro`. .. exn:: No such hypothesis. .. exn:: @ident is used in the hypothesis @ident. -.. tac:: revert dependent @ident +.. tacn:: revert dependent @ident This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that depend on it. .. tacn:: move @ident after @ident - :name: move .. after ... + :name: move ... after ... This moves the hypothesis named :n:`@ident` in the local context after the hypothesis named :n:`@ident`, where “after” is in reference to the @@ -926,9 +953,9 @@ the inverse of :tacn:`intro`. This moves ident at the bottom of the local context (at the end of the context). -.. exn:: No such hypothesis -.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident -.. exn:: Cannot move @ident after @ident : it depends on @ident +.. exn:: No such hypothesis. +.. exn:: Cannot move @ident after @ident : it occurs in the type of @ident. +.. exn:: Cannot move @ident after @ident : it depends on @ident. .. example:: .. coqtop:: all @@ -944,7 +971,7 @@ the inverse of :tacn:`intro`. move H0 before H. .. tacn:: rename @ident into @ident - :name: rename ... into ... + :name: rename This renames hypothesis :n:`@ident` into :n:`@ident` in the current context. The name of the hypothesis in the proof-term, however, is left unchanged. @@ -955,8 +982,8 @@ The name of the hypothesis in the proof-term, however, is left unchanged. particular, the target identifiers may contain identifiers that exist in the source context, as long as the latter are also renamed by the same tactic. -.. exn:: No such hypothesis -.. exn:: @ident is already used +.. exn:: No such hypothesis. +.. exn:: @ident is already used. .. tacn:: set (@ident := @term) :name: set @@ -968,7 +995,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. first checks that all subterms matching the pattern are compatible before doing the replacement using the leftmost subterm matching the pattern. -.. exn:: The variable @ident is already defined +.. exn:: The variable @ident is already defined. .. tacv:: set (@ident := @term ) in @goal_occurrences @@ -992,6 +1019,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 @@ -999,6 +1027,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. @@ -1016,6 +1045,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. @@ -1067,7 +1098,7 @@ The name of the hypothesis in the proof-term, however, is left unchanged. This decomposes record types (inductive types with one constructor, like "and" and "exists" and those defined with the Record macro, see - :ref:`TODO-2.1`). + :ref:`record-types`). .. _controllingtheproofflow: @@ -1082,24 +1113,25 @@ 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`. .. tacv:: assert form - This behaves as :n:`assert (@ident : form ) but :n:`@ident` is generated by + This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by Coq. -.. tacv:: assert form by tactic +.. tacv:: assert @form by @tactic This tactic behaves like :n:`assert` but applies tactic to solve the subgoals generated by assert. - .. exn:: Proof is not complete + .. exn:: Proof is not complete. + :name: Proof is not complete. (assert) -.. tacv:: assert form as intro_pattern +.. tacv:: assert @form 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 @@ -1108,7 +1140,7 @@ Controlling the proof flow introduction pattern, the tactic behaves like :n:`assert form` followed by the action done by this introduction pattern. -.. tacv:: assert form as intro_pattern by tactic +.. tacv:: assert @form as @intro_pattern by @tactic This combines the two previous variants of :n:`assert`. @@ -1118,9 +1150,10 @@ Controlling the proof flow 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`. - .. exn:: Variable @ident is already declared + .. exn:: Variable @ident is already declared. .. tacv:: eassert form as intro_pattern by tactic + :name: eassert .. tacv:: assert (@ident := @term) @@ -1130,6 +1163,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, @@ -1143,6 +1177,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 @@ -1158,9 +1193,9 @@ Controlling the proof flow This behaves like :n:`enough form` using :n:`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 : @form) by @tactic +.. tacv:: enough @form by @tactic +.. tacv:: enough @form 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 @@ -1168,22 +1203,27 @@ 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:`TODO-4.2`. (This is Modus Ponens inference + the “App” rule given in :ref:`typing-rules`. (This is Modus Ponens inference rule.) :n:`cut U` transforms the current goal :g:`T` into the two following 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 The tactic :n:`specialize` works on local hypothesis :n:`@ident`. The premises of this hypothesis (either universal quantifications or @@ -1202,8 +1242,8 @@ Controlling the proof flow the goal. The :n:`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 - .. exn:: @ident is used in conclusion + .. exn:: @ident is used in hypothesis @ident. + .. exn:: @ident is used in conclusion. .. tacn:: generalize @term :name: generalize @@ -1236,7 +1276,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. This is equivalent to :n:`generalize @term` but it generalizes only over the specified occurrences of :n:`@term` (counting from left to right on the - expression printed using option :g:`Set Printing All`). + expression printed using option :opt:`Printing All`). .. tacv:: generalize @term as @ident @@ -1268,7 +1308,7 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. :n:`refine @term` (preferred alternative). .. note:: To be able to refer to an existential variable by name, the user - must have given the name explicitly (see :ref:`TODO-2.11`). + must have given the name explicitly (see :ref:`Existential-Variables`). .. note:: When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to @@ -1327,7 +1367,7 @@ 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. .. tacv:: contradiction @ident @@ -1353,11 +1393,13 @@ goals cannot be closed with :g:`Qed` but only with :g:`Admitted`. then required to prove that False is indeed provable in the current context. This tactic is a macro for :n:`elimtype False`. +.. _CaseAnalysisAndInduction: + Case analysis and induction ------------------------------- The tactics presented in this section implement induction or case -analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). +analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`). .. tacn:: destruct @term :name: destruct @@ -1423,6 +1465,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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 @@ -1449,6 +1492,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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 @@ -1458,14 +1502,15 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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. @@ -1528,9 +1573,9 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). intros n H. induction n. -.. exn:: Not an inductive product +.. exn:: Not an inductive product. -.. exn:: Unable to find an instance for the variables @ident ... @ident +.. exn:: Unable to find an instance for the variables @ident ... @ident. Use in this case the variant :tacn:`elim ... with` below. @@ -1556,6 +1601,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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, @@ -1628,6 +1674,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). (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. @@ -1646,7 +1693,8 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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 @@ -1656,6 +1704,7 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). :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. @@ -1740,13 +1789,14 @@ analysis on inductive or co-inductive objects (see :ref:`TODO-4.5`). 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 results equivalent to ``inversion`` or ``dependent inversion`` if the hypothesis is dependent. -See also :ref:`TODO-10.1-dependentinduction` for a larger example of ``dependent induction`` +See also the larger example of :tacn:`dependent induction` and an explanation of the underlying technique. .. tacn:: function induction (@qualid {+ @term}) @@ -1754,8 +1804,8 @@ and an explanation of the underlying technique. The tactic functional induction performs case analysis and induction following the definition of a function. It makes use of a principle - generated by ``Function`` (see :ref:`TODO-2.3-Advancedrecursivefunctions`) or - ``Functional Scheme`` (see :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme`). + generated by ``Function`` (see :ref:`advanced-recursive-functions`) or + ``Functional Scheme`` (see :ref:`functional-scheme`). Note that this tactic is only available after a .. example:: @@ -1781,26 +1831,26 @@ and an explanation of the underlying technique. :n:`functional induction (f x1 x2 x3)` is actually a wrapper for :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning phase, where :n:`@qualid` is the induction principle registered for :g:`f` - (by the ``Function`` (see :ref:`TODO-2.3-Advancedrecursivefunctions`) or - ``Functional Scheme`` (see :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme`) + (by the ``Function`` (see :ref:`advanced-recursive-functions`) or + ``Functional Scheme`` (see :ref:`functional-scheme`) command) corresponding to the sort of the goal. Therefore ``functional induction`` may fail if the induction scheme :n:`@qualid` is not - defined. See also :ref:`TODO-2.3-Advancedrecursivefunctions` for the function + defined. See also :ref:`advanced-recursive-functions` for the function terms accepted by ``Function``. .. note:: There is a difference between obtaining an induction scheme - for a function by using :g:`Function` (see :ref:`TODO-2.3-Advancedrecursivefunctions`) + for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`) and by using :g:`Functional Scheme` after a normal definition using - :g:`Fixpoint` or :g:`Definition`. See :ref:`TODO-2.3-Advancedrecursivefunctions` + :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions` for details. -See also: :ref:`TODO-2.3-Advancedrecursivefunctions` - :ref:`TODO-13.2-Generationofinductionschemeswithfunctionalscheme` +See also: :ref:`advanced-recursive-functions` + :ref:`functional-scheme` :tacn:`inversion` -.. exn:: Cannot find induction information on @qualid -.. exn:: Not the right number of induction arguments +.. exn:: Cannot find induction information on @qualid. +.. exn:: Not the right number of induction arguments. .. tacv:: functional induction (@qualid {+ @term}) as @disj_conj_intro_pattern using @term with @bindings_list @@ -1833,8 +1883,8 @@ See also: :ref:`TODO-2.3-Advancedrecursivefunctions` :n:`@ident` is first introduced in the local context using :n:`intros until @ident`. -.. exn:: No primitive equality found -.. exn:: Not a discriminable equality +.. exn:: No primitive equality found. +.. exn:: Not a discriminable equality. .. tacv:: discriminate @num @@ -1849,6 +1899,7 @@ See also: :ref:`TODO-2.3-Advancedrecursivefunctions` .. 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 @@ -1861,7 +1912,7 @@ See also: :ref:`TODO-2.3-Advancedrecursivefunctions` the form :n:`@term <> @term`, this behaves as :n:`intro @ident; discriminate @ident`. - .. exn:: No discriminable equalities + .. exn:: No discriminable equalities. .. tacn:: injection @term :name: injection @@ -1872,7 +1923,7 @@ See also: :ref:`TODO-2.3-Advancedrecursivefunctions` :g:`t`:sub:`1` and :g:`t`:sub:`2` are equal too. If :n:`@term` is a proof of a statement of conclusion :n:`@term = @term`, - then ``injection`` applies the injectivity of constructors as deep as + then :tacn:`injection` applies the injectivity of constructors as deep as possible to derive the equality of all the subterms of :n:`@term` and :n:`@term` at positions where the terms start to differ. For example, from :g:`(S p, S n) = (q, S (S m))` we may derive :g:`S p = q` and @@ -1882,90 +1933,96 @@ See also: :ref:`TODO-2.3-Advancedrecursivefunctions` equality of all the subterms at positions where they differ and adds them as antecedents to the conclusion of the current goal. -.. example:: + .. example:: - Consider the following goal: + Consider the following goal: - .. coqtop:: reset all + .. coqtop:: in - Inductive list : Set := - | nil : list - | cons : nat -> list -> list. - Variable P : list -> Prop. - Goal forall l n, P nil -> cons n l = cons 0 nil -> P l. - intros. - injection H0. + Inductive list : Set := + | nil : list + | cons : nat -> list -> list. + Parameter P : list -> Prop. + Goal forall l n, P nil -> cons n l = cons 0 nil -> P l. + .. coqtop:: all -Beware that injection yields an equality in a sigma type whenever the -injected object has a dependent type :g:`P` with its two instances in -different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and -:g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and -:g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable -equality has been declared using the command ``Scheme Equality`` (see :ref:`TODO-13.1-GenerationofinductionprincipleswithScheme`), -the use of a sigma type is avoided. + intros. + injection H0. -.. note:: - If some quantified hypothesis of the goal is named :n:`@ident`, - then :n:`injection @ident` first introduces the hypothesis in the local - context using :n:`intros until @ident`. + Beware that injection yields an equality in a sigma type whenever the + injected object has a dependent type :g:`P` with its two instances in + different types :g:`(P t`:sub:`1` :g:`... t`:sub:`n` :g:`)` and + :g:`(P u`:sub:`1` :g:`... u`:sub:`n` :sub:`)`. If :g:`t`:sub:`1` and + :g:`u`:sub:`1` are the same and have for type an inductive type for which a decidable + equality has been declared using the command :cmd:`Scheme Equality` + (see :ref:`proofschemes-induction-principles`), + the use of a sigma type is avoided. -.. exn:: Not a projectable equality but a discriminable one -.. exn:: Nothing to do, it is an equality between convertible @terms -.. exn:: Not a primitive equality -.. exn:: Nothing to inject + .. note:: + If some quantified hypothesis of the goal is named :n:`@ident`, + then :n:`injection @ident` first introduces the hypothesis in the local + context using :n:`intros until @ident`. -.. tacv:: injection @num + .. exn:: Not a projectable equality but a discriminable one. + .. exn:: Nothing to do, it is an equality between convertible @terms. + .. exn:: Not a primitive equality. + .. exn:: Nothing to inject. - This does the same thing as :n:`intros until @num` followed by - :n:`injection @ident` where :n:`@ident` is the identifier for the last - introduced hypothesis. + .. tacv:: injection @num -.. tacv:: injection @term with @bindings_list + This does the same thing as :n:`intros until @num` followed by + :n:`injection @ident` where :n:`@ident` is the identifier for the last + introduced hypothesis. - This does the same as :n:`injection @term` but using the given bindings to - instantiate parameters or hypotheses of :n:`@term`. + .. tacv:: injection @term with @bindings_list -.. tacv:: einjection @num -.. tacv:: einjection @term {? with @bindings_list} + This does the same as :n:`injection @term` but using the given bindings to + instantiate parameters or hypotheses of :n:`@term`. - 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 - parameters, these parameters are left as existential variables. + .. tacv:: einjection @num + :name: einjection + .. tacv:: einjection @term {? with @bindings_list} + + 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 + parameters, these parameters are left as existential variables. -.. tacv:: injection + .. tacv:: injection - If the current goal is of the form :n:`@term <> @term` , this behaves as - :n:`intro @ident; injection @ident`. + If the current goal is of the form :n:`@term <> @term` , this behaves as + :n:`intro @ident; injection @ident`. - .. exn:: goal does not satisfy the expected preconditions + .. exn:: goal does not satisfy the expected preconditions. -.. 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} + .. 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 - ``injection`` or ``einjection`` so that all equalities generated are moved in + :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 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 ``Set Structural Injection`` must be activated. This -option is off by default. + .. opt:: Structural Injection -By default, ``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 ``Set Keep Proof Equalities``. + 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. + + .. 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 @@ -1984,15 +2041,15 @@ turned off by setting the option ``Set Keep Proof Equalities``. .. note:: As ``inversion`` proofs may be large in size, we recommend the user to stock the lemmas whenever the same instance needs to be - inverted several times. See :ref:`TODO-13.3-Generationofinversionprincipleswithderiveinversion`. + inverted several times. See :ref:`derive-inversion`. .. note:: Part of the behavior of the ``inversion`` tactic is to generate equalities between expressions that appeared in the hypothesis that is being processed. By default, no equalities are generated if they relate two proofs (i.e. equalities between :n:`@terms` whose type is in sort - :g:`Prop`). This behavior can be turned off by using the option ``Set Keep - Proof Equalities``. + :g:`Prop`). This behavior can be turned off by using the option + :opt`Keep Proof Equalities`. .. tacv:: inversion @num @@ -2093,13 +2150,13 @@ turned off by setting the option ``Set Keep Proof Equalities``. :n:`dependent inversion_clear @ident`. .. tacv:: dependent inversion @ident with @term - :name: dependent inversion ... + :name: dependent inversion ... with ... This variant allows you to specify the generalization of the goal. It is useful when the system fails to generalize the goal automatically. If - :n:`@ident` has type :g:`(I t)` and :g:`I` has type :math:`\forall` - :g:`(x:T), s`, then :n:`@term` must be of type :g:`I:`:math:`\forall` - :g:`(x:T), I x -> s'` where :g:`s'` is the type of the goal. + :n:`@ident` has type :g:`(I t)` and :g:`I` has type :g:`forall (x:T), s`, + then :n:`@term` must be of type :g:`I:forall (x:T), I x -> s'` where + :g:`s'` is the type of the goal. .. tacv:: dependent inversion @ident as @intro_pattern with @term @@ -2108,7 +2165,7 @@ turned off by setting the option ``Set Keep Proof Equalities``. .. tacv:: dependent inversion_clear @ident with @term - Like :tacn:`dependent inversion ...` with but clears :n:`@ident` from the + Like :tacn:`dependent inversion ... with ...` with but clears :n:`@ident` from the local context. .. tacv:: dependent inversion_clear @ident as @intro_pattern with @term @@ -2117,6 +2174,7 @@ turned off by setting the option ``Set 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. @@ -2300,7 +2358,7 @@ turned off by setting the option ``Set Keep Proof Equalities``. 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 ``Guarded`` (see :ref:`TODO-7.3.2-Guarded`). + the command ``Guarded`` (see Section :ref:`requestinginformation`). .. tacv:: fix @ident @num with {+ (ident {+ @binder} [{struct @ident}] : @type)} @@ -2321,7 +2379,7 @@ turned off by setting the option ``Set Keep Proof Equalities``. done only at the time of registering the lemma in the environment. To know if the use of coinduction hypotheses is correct at some time of the interactive development of a proof, use the command ``Guarded`` - (see :ref:`TODO-7.3.2-Guarded`). + (see Section :ref:`requestinginformation`). .. tacv:: cofix @ident with {+ (@ident {+ @binder} : @type)} @@ -2335,41 +2393,41 @@ Rewriting expressions --------------------- These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in -file ``Logic.v`` (see :ref:`TODO-3.1.2-Logic`). The notation for :g:`eq T t u` is +file ``Logic.v`` (see :ref:`coq-library-logic`). The notation for :g:`eq T t u` is simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacn:: rewrite @term :name: rewrite -This tactic applies to any goal. The type of :n:`@term` must have the form + This tactic applies to any goal. The type of :token:`term` must have the form -``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` + ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``). eq term``:sub:`1` ``term``:sub:`2` ``.`` -where :g:`eq` is the Leibniz equality or a registered setoid equality. + where :g:`eq` is the Leibniz equality or a registered setoid equality. -Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, -resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then -replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. -Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, -and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new -subgoals. + Then :n:`rewrite @term` finds the first subterm matching `term`\ :sub:`1` in the goal, + resulting in instances `term`:sub:`1`' and `term`:sub:`2`' and then + replaces every occurrence of `term`:subscript:`1`' by `term`:subscript:`2`'. + Hence, some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :g:`A`\ :sub:`1`:g:`, ..., A`\ :sub:`n` become new + subgoals. -.. exn:: The @term provided does not end with an equation + .. exn:: The @term provided does not end with an equation. -.. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. + .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. -.. tacv:: rewrite -> @term + .. tacv:: rewrite -> @term - Is equivalent to :n:`rewrite @term` + Is equivalent to :n:`rewrite @term` -.. tacv:: rewrite <- @term + .. tacv:: rewrite <- @term - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left -.. tacv:: rewrite @term in clause + .. tacv:: rewrite @term in clause - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following clause + (similarly to :ref:`performing computations <performingcomputations>`). For instance: + :n:`rewrite H in H`:sub:`1` will rewrite `H` in the hypothesis `H`:sub:`1` instead of the current goal. @@ -2378,218 +2436,215 @@ subgoals. In particular a failure will happen if any of these three simpler tactics fails. + :n:`rewrite H in * |-` will do :n:`rewrite H in H`:sub:`i` for all hypotheses - :g:`H`:sub:`i` :g:`<> H`. A success will happen as soon as at least one of these - simpler tactics succeeds. + :g:`H`:sub:`i` different from :g:`H`. + A success will happen as soon as at least one of these simpler tactics succeeds. + :n:`rewrite H in *` is a combination of :n:`rewrite H` and :n:`rewrite H in * |-` that succeeds if at least one of these two tactics succeeds. - Orientation :g:`->` or :g:`<-` can be inserted before the :n:`@term` to rewrite. + Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. -.. tacv:: rewrite @term at occurrences + .. tacv:: rewrite @term at occurrences - Rewrite only the given occurrences of :n:`@term`. Occurrences are - specified from left to right as for pattern (:tacn:`pattern`). The rewrite is - always performed using setoid rewriting, even for Leibniz’s equality, so one - has to ``Import Setoid`` to use this variant. + Rewrite only the given occurrences of :token:`term`. Occurrences are + specified from left to right as for pattern (:tacn:`pattern`). The rewrite is + always performed using setoid rewriting, even for Leibniz’s equality, so one + has to ``Import Setoid`` to use this variant. -.. tacv:: rewrite @term by tactic + .. tacv:: rewrite @term by tactic - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + Use tactic to completely solve the side-conditions arising from the + :tacn:`rewrite`. -.. tacv:: rewrite {+ @term} + .. tacv:: rewrite {+, @term} - Is equivalent to the `n` successive tactics :n:`{+ rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :n:`@term` to rewrite. One - unique clause can be added at the end after the keyword in; it will then - affect all rewrite operations. + Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one + working on the first subgoal generated by the previous one. Orientation + :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + unique clause can be added at the end after the keyword in; it will then + affect all rewrite operations. - In all forms of rewrite described above, a :n:`@term` to rewrite can be - immediately prefixed by one of the following modifiers: + In all forms of rewrite described above, a :token:`term` to rewrite can be + immediately prefixed by one of the following modifiers: - + `?` : the tactic rewrite :n:`?@term` performs the rewrite of :n:`@term` as many - times as possible (perhaps zero time). This form never fails. - + `n?` : works similarly, except that it will do at most `n` rewrites. - + `!` : works as ?, except that at least one rewrite should succeed, otherwise - the tactic fails. - + `n!` (or simply `n`) : precisely `n` rewrites of :n:`@term` will be done, - leading to failure if these n rewrites are not possible. + + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many + times as possible (perhaps zero time). This form never fails. + + :n:`@num?` : works similarly, except that it will do at most :token:`num` rewrites. + + `!` : works as `?`, except that at least one rewrite should succeed, otherwise + the tactic fails. + + :n:`@num!` (or simply :n:`@num`) : precisely :token:`num` rewrites of :token:`term` will be done, + leading to failure if these :token:`num` rewrites are not possible. -.. tacv:: erewrite @term + .. tacv:: erewrite @term + :name: erewrite - This tactic works as :n:`rewrite @term` but turning - unresolved bindings into existential variables, if any, instead of - failing. It has the same variants as :tacn:`rewrite` has. + This tactic works as :n:`rewrite @term` but turning + unresolved bindings into existential variables, if any, instead of + failing. It has the same variants as :tacn:`rewrite` has. -.. tacn:: replace @term with @term +.. tacn:: replace @term with @term’ :name: replace This tactic applies to any goal. It replaces all free occurrences of :n:`@term` - in the current goal with :n:`@term` and generates the equality :n:`@term = - @term` as a subgoal. This equality is automatically solved if it occurs among - the assumption, or if its symmetric form occurs. It is equivalent to - :n:`cut @term = @term; [intro H`:sub:`n` :n:`; rewrite <- H`:sub:`n` :n:`; clear H`:sub:`n`:n:`|| assumption || symmetry; try assumption]`. + in the current goal with :n:`@term’` and generates an equality :n:`@term = @term’` + as a subgoal. This equality is automatically solved if it occurs among + the assumptions, or if its symmetric form occurs. It is equivalent to + :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 + .. exn:: Terms do not have convertible types. -.. tacv:: replace @term with @term by tactic + .. tacv:: replace @term with @term’ by @tactic - This acts as :n:`replace @term` with :n:`@term` but applies tactic to solve the generated - subgoal :n:`@term = @term`. + This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated + subgoal :n:`@term = @term’`. -.. tacv:: replace @term + .. tacv:: replace @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` or :n:`@term’ = @term`. -.. tacv:: replace -> @term + .. tacv:: replace -> @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term = @term’` -.. tacv:: replace <- @term + .. tacv:: replace <- @term - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has + the form :n:`@term’ = @term` -.. tacv:: replace @term with @term in clause -.. tacv:: replace @term with @term in clause by tactic -.. tacv:: replace @term in clause replace -> @term in clause -.. tacv:: replace <- @term in clause + .. tacv:: replace @term {? with @term} in clause {? by @tactic} + .. tacv:: replace -> @term in clause + .. tacv:: replace <- @term in clause - Acts as before but the replacements take place inclause (see - :ref:`performingcomputations`) and not only in the conclusion of the goal. The - clause argument must not contain any type of nor value of. + 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 + clause argument must not contain any ``type of`` nor ``value of``. -.. tacv:: cutrewrite <- (@term = @term) + .. tacv:: cutrewrite <- (@term = @term’) + :name: cutrewrite - This tactic is deprecated. It acts like :n:`replace @term with @term`, or, - equivalently as :n:`enough (@term = @term) as <-`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as <-`. -.. tacv:: cutrewrite -> (@term = @term) + .. tacv:: cutrewrite -> (@term = @term’) - This tactic is deprecated. It can be replaced by enough :n:`(@term = @term) as ->`. + This tactic is deprecated. It can be replaced by :n:`enough (@term = @term’) as ->`. .. tacn:: subst @ident :name: subst + This tactic applies to a goal that has :n:`@ident` in its context and (at + least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` + with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by + :g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and + clears :n:`@ident` and :g:`H` from the context. -This tactic applies to a goal that has :n:`@ident` in its context and (at -least) one hypothesis, say :g:`H`, of type :n:`@ident = t` or :n:`t = @ident` -with :n:`@ident` not occurring in :g:`t`. Then it replaces :n:`@ident` by -:g:`t` everywhere in the goal (in the hypotheses and in the conclusion) and -clears :n:`@ident` and :g:`H` from the context. - -If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also -unfolded and cleared. + If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + unfolded and cleared. + .. note:: + + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the + first one is used. -.. note:: - When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the - first one is used. + + If :g:`H` is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. + .. tacv:: subst {+ @ident} -.. note:: - If `H` is itself dependent in the goal, it is replaced by the proof of - reflexivity of equality. + This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + .. tacv:: subst -.. tacv:: subst {+ @ident} + This applies subst repeatedly from top to bottom to all identifiers of the + 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``. - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. + .. opt:: Regular Subst Tactic -.. tacv:: subst + This option controls the behavior of :tacn:`subst`. When it is + activated (it is by default), :tacn:`subst` also deals with the following corner cases: - This applies subst repeatedly from top to bottom to all identifiers of the - 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`. + + 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`. - .. note:: + 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. + default. - The behavior of subst can be controlled using option ``Set Regular Subst - Tactic.`` When this option is activated, 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`. +.. tacn:: stepl @term + :name: stepl - 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. + This tactic is for chaining rewriting steps. It assumes a goal of the + form :n:`R @term @term` where ``R`` is a binary relation and relies on a + database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` + 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`. + .. cmd:: Declare Left Step @term -.. tacn:: stepl @term - :name: stepl + 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`). -This tactic is for chaining rewriting steps. It assumes a goal of the -form :n:`R @term @term` where `R` is a binary relation and relies on a -database of lemmas of the form :g:`forall x y z, R x y -> eq x z -> R z y` -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`. + .. tacv:: stepl @term by @tactic -Lemmas are added to the database using the command ``Declare Left Step @term.`` -The tactic is especially useful for parametric setoids which are not accepted -as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see -:ref:`TODO-27-Generalizedrewriting`). + This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. -.. tacv:: stepl @term by tactic + .. tacv:: stepr @term stepr @term by tactic + :name: stepr - This applies :n:`stepl @term` then applies tactic to the second goal. + 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`. -.. tacv:: stepr @term stepr @term by tactic + .. cmd:: Declare Right Step @term - 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.`` + 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:`TODO-4.4-Subtypingrules`. :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 + 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. -.. tacv:: change @term with @term + .. tacv:: change @term with @term’ - This replaces the occurrences of :n:`@term` by :n:`@term` in the current goal. - The term :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. + The term :n:`@term` and :n:`@term’` must be convertible. -.. tacv:: change @term at {+ @num} with @term + .. tacv:: change @term at {+ @num} with @term’ - This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term by @term` - in the current goal. The terms :n:`@term` and :n:`@term` must be convertible. + This replaces the occurrences numbered :n:`{+ @num}` of :n:`@term` by :n:`@term’` + in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. -.. exn:: Too few occurrences + .. exn:: Too few occurrences. -.. tacv:: change @term in @ident -.. tacv:: change @term with @term in @ident -.. tacv:: change @term at {+ @num} with @term in @ident + .. tacv:: change @term {? {? at {+ @num}} with @term} in @ident - This applies the change tactic not to the goal but to the hypothesis :n:`@ident`. + This applies the :tacn:`change` tactic not to the goal but to the hypothesis :n:`@ident`. -See also: :ref:`Performing computations <performingcomputations>` + .. seealso:: :ref:`Performing computations <performingcomputations>` .. _performingcomputations: @@ -2637,7 +2692,7 @@ the conversion in hypotheses :n:`{+ @ident}`. the normalization of the goal according to the specified flags. In correspondence with the kinds of reduction considered in Coq namely :math:`\beta` (reduction of functional application), :math:`\delta` - (unfolding of transparent constants, see :ref:`TODO-6.10.2-Transparent`), + (unfolding of transparent constants, see :ref:`vernac-controlling-the-reduction-strategies`), :math:`\iota` (reduction of pattern-matching over a constructed term, and unfolding of :g:`fix` and :g:`cofix` expressions) and :math:`\zeta` (contraction of local definitions), the @@ -2649,7 +2704,7 @@ the conversion in hypotheses :n:`{+ @ident}`. second case the constant to unfold to all but the ones explicitly mentioned. Notice that the ``delta`` flag does not apply to variables bound by a let-in construction inside the :n:`@term` itself (use here the ``zeta`` flag). In - any cases, opaque constants are not unfolded (see :ref:`TODO-6.10.1-Opaque`). + any cases, opaque constants are not unfolded (see :ref:`vernac-controlling-the-reduction-strategies`). Normalization according to the flags is done by first evaluating the head of the expression into a *weak-head* normal form, i.e. until the @@ -2704,6 +2759,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`. @@ -2713,6 +2769,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 @@ -2754,7 +2811,7 @@ the conversion in hypotheses :n:`{+ @ident}`. definition (say :g:`t`) and then reduces :g:`(t t`:sub:`1` :g:`... t`:sub:`n` :g:`)` according to :math:`\beta`:math:`\iota`:math:`\zeta`-reduction rules. -.. exn:: Not reducible +.. exn:: Not reducible. .. tacn:: hnf :name: hnf @@ -2768,7 +2825,7 @@ the conversion in hypotheses :n:`{+ @ident}`. :n:`hnf`. .. note:: - The :math:`\delta` rule only applies to transparent constants (see :ref:`TODO-6.10.1-Opaque` + The :math:`\delta` rule only applies to transparent constants (see :ref:`vernac-controlling-the-reduction-strategies` on transparency and opacity). .. tacn:: cbn @@ -2811,8 +2868,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). - Notation "f \o g" := (fcomp f g) (at level 50). Arguments fcomp {A B C} f g x /. + Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. @@ -2881,7 +2938,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This applies ``simpl`` only to the :n:`{+ @num}` occurrences of the subterms matching :n:`@pattern` in the current goal. - .. exn:: Too few occurrences + .. exn:: Too few occurrences. .. tacv:: simpl @qualid .. tacv:: simpl @string @@ -2906,12 +2963,12 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see - :ref:`TODO-1.3.2-Definitions` and :ref:`TODO-6.10.2-Transparent`). The tactic + :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which :n:`@qualid` refers in the current goal and then replaces it with its :math:`\beta`:math:`\iota`-normal form. -.. exn:: @qualid does not denote an evaluable constant +.. exn:: @qualid does not denote an evaluable constant. .. tacv:: unfold @qualid in @ident @@ -2928,9 +2985,9 @@ the conversion in hypotheses :n:`{+ @ident}`. The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be unfolded. Occurrences are located from left to right. - .. exn:: bad occurrence number of @qualid + .. exn:: Bad occurrence number of @qualid. - .. exn:: @qualid does not occur + .. exn:: @qualid does not occur. .. tacv:: unfold @string @@ -2942,7 +2999,7 @@ the conversion in hypotheses :n:`{+ @ident}`. This is variant of :n:`unfold @string` where :n:`@string` gets its interpretation from the scope bound to the delimiting key :n:`key` - instead of its default interpretation (see :ref:`TODO-12.2.2-Localinterpretationrulesfornotations`). + instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`). .. tacv:: unfold {+, qualid_or_string at {+, @num}} This is the most general form, where :n:`qualid_or_string` is either a @@ -3020,7 +3077,7 @@ Conversion tactics applied to hypotheses Example: :n:`unfold not in (Type of H1) (Type of H3)`. -.. exn:: No such hypothesis : ident. +.. exn:: No such hypothesis: @ident. .. _automation: @@ -3071,6 +3128,7 @@ hints of the database named core. to know what lemmas/assumptions were used. .. tacv:: debug auto + :name: debug auto Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. @@ -3090,7 +3148,9 @@ hints of the database named core. .. tacv:: trivial with * .. tacv:: trivial using {+ @lemma} .. tacv:: debug trivial + :name: debug trivial .. tacv:: info_trivial + :name: info_trivial .. tacv:: {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} .. note:: @@ -3103,7 +3163,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>` @@ -3123,7 +3183,7 @@ can solve such a goal: Goal forall P:nat -> Prop, P 0 -> exists n, P n. eauto. -Note that :tacn:`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}} @@ -3169,7 +3229,9 @@ the processing of the rewriting rules. The rewriting rule bases are built with the ``Hint Rewrite vernacular`` command. -.. warn:: This tactic may loop if you build non terminating rewriting systems. +.. warning:: + + This tactic may loop if you build non terminating rewriting systems. .. tacv:: autorewrite with {+ @ident} using @tactic @@ -3200,7 +3262,8 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic. This tactic tries to solve the current goal by a number of standard closing steps. In particular, it tries to close the current goal using the closing tactics - :tacn:`trivial`, reflexivity, symmetry, contradiction and inversion of hypothesis. + :tacn:`trivial`, :tacn:`reflexivity`, :tacn:`symmetry`, :tacn:`contradiction` + and :tacn:`inversion` of hypothesis. If this fails, it tries introducing variables and splitting and-hypotheses, using the closing tactics afterwards, and splitting the goal using :tacn:`split` and recursing. @@ -3211,7 +3274,7 @@ See also: :tacn:`autorewrite` for examples showing the use of this tactic. .. tacv:: now @tactic :name: now - Run :n:`@tac` followed by ``easy``. This is a notation for :n:`@tactic; easy`. + Run :n:`@tactic` followed by :tacn:`easy`. This is a notation for :n:`@tactic; easy`. Controlling automation -------------------------- @@ -3221,225 +3284,245 @@ Controlling automation The hints databases for auto and eauto ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The hints for ``auto`` and ``eauto`` are stored in databases. Each database -maps head symbols to a list of hints. One can use the command +The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database +maps head symbols to a list of hints. .. cmd:: Print Hint @ident -to display the hints associated to the head symbol :n:`@ident` -(see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative -integer, and an optional pattern. The hints with lower cost are tried first. A -hint is tried by ``auto`` when the conclusion of the current goal matches its -pattern or when it has no pattern. + Use this command + to display the hints associated to the head symbol :n:`@ident` + (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative + integer, and an optional pattern. The hints with lower cost are tried first. A + hint is tried by :tacn:`auto` when the conclusion of the current goal matches its + pattern or when it has no pattern. Creating Hint databases ``````````````````````` -One can optionally declare a hint database using the command ``Create -HintDb``. If a hint is added to an unknown database, it will be +One can optionally declare a hint database using the command +:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be automatically created. -.. cmd:: Create HintDb @ident {? discriminated}. - -This command creates a new database named :n:`@ident`. The database is -implemented by a Discrimination Tree (DT) that serves as an index of -all the lemmas. The DT can use transparency information to decide if a -constant should be indexed or not (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), -making the retrieval more efficient. The legacy implementation (the default one -for new databases) uses the DT only on goals without existentials (i.e., ``auto`` -goals), for non-Immediate hints and do not make use of transparency -hints, putting more work on the unification that is run after -retrieval (it keeps a list of the lemmas in case the DT is not used). -The new implementation enabled by the discriminated option makes use -of DTs in all cases and takes transparency information into account. -However, the order in which hints are retrieved from the DT may differ -from the order in which they were inserted, making this implementation -observationally different from the legacy one. +.. cmd:: Create HintDb @ident {? discriminated} + + This command creates a new database named :n:`@ident`. The database is + implemented by a Discrimination Tree (DT) that serves as an index of + all the lemmas. The DT can use transparency information to decide if a + constant should be indexed or not + (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`), + making the retrieval more efficient. The legacy implementation (the default one + for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto` + goals), for non-Immediate hints and do not make use of transparency + hints, putting more work on the unification that is run after + retrieval (it keeps a list of the lemmas in case the DT is not used). + The new implementation enabled by the discriminated option makes use + of DTs in all cases and takes transparency information into account. + However, the order in which hints are retrieved from the DT may differ + from the order in which they were inserted, making this implementation + 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 + + No database name is given: the hint is registered in the core database. + + .. cmdv:: 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. + + .. cmdv:: Local Hint @hint_definition -.. cmd:: Hint hint_definition + Idem for the core database. - No database name is given: the hint is registered in the core database. + .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}} + :name: Hint Resolve -.. cmd:: Local Hint hint_definition : {+ @ident} + 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. - 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. + .. exn:: @term cannot be used as a hint -.. cmd:: Local Hint hint_definition + The head symbol of the type of :n:`@term` is a bound variable such that + this tactic cannot be associated to a constant. - Idem for the core database. + .. cmdv:: Hint Resolve {+ @term} -The ``hint_definition`` is one of the following expressions: + Adds each :n:`Hint Resolve @term`. -+ :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. + .. cmdv:: Hint Resolve -> @term - .. exn:: @term cannot be used as a hint + 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`). - The head symbol of the type of :n:`@term` is a bound variable such that - this tactic cannot be associated to a constant. + .. cmdv:: Resolve <- @term - **Variants:** + Adds the right-to-left implication of an equivalence as a hint. - + :n:`Resolve {+ @term}` - Adds each :n:`Resolve @term`. + .. cmdv:: Hint Immediate @term + :name: Hint Immediate - + :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``). + 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 :tacn:`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:`Resolve <- @term` - Adds the right-to-left implication of an equivalence as a hint. + .. exn:: @term cannot be used as a hint -+ :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. + .. cmdv:: Immediate {+ @term} - .. exn:: @term cannot be used as a hint + Adds each :n:`Hint Immediate @term`. - **Variants:** + .. cmdv:: Hint Constructors @ident + :name: Hint Constructors - + :n:`Immediate {+ @term}` - Adds each :n:`Immediate @term`. + 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:`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. + .. exn:: @ident is not an inductive type - .. exn:: @ident is not an inductive type + .. cmdv:: Hint Constructors {+ @ident} - **Variants:** + Adds each :n:`Hint Constructors @ident`. - + :n:`Constructors {+ @ident}` - Adds each :n:`Constructors @ident`. + .. cmdv:: Hint Unfold @qualid + :name: Hint Unfold -+ :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. + 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. - **Variants:** + .. cmdv:: Hint Unfold {+ @ident} - + :n:`Unfold {+ @ident}` - Adds each :n:`Unfold @ident`. + Adds each :n:`Hint Unfold @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 %( Transparent %| Opaque %) @qualid + :name: Hint ( Transparent | Opaque ) - **Variants:** + 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} - + :n:`Transparent`, :n:`Opaque {+ @ident}` Declares each :n:`@ident` as a transparent or opaque constant. -+ :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:`TODO-20.6.5-typeclasseseauto`). - - 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. + .. cmdv:: Hint Extern @num {? @pattern} => @tactic + :name: Hint Extern -.. note:: - One can use an ``Extern`` hint with no pattern to do pattern-matching on - hypotheses using ``match goal`` with inside the 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 @@ -3521,7 +3604,7 @@ at every moment. (left to right). Notice that the rewriting bases are distinct from the ``auto`` hint bases and thatauto does not take them into account. - This command is synchronous with the section mechanism (see :ref:`TODO-2.4-Sectionmechanism`): + This command is synchronous with the section mechanism (see :ref:`section-mechanism`): when closing a section, all aliases created by ``Hint Rewrite`` in that section are lost. Conversely, when loading a module, all ``Hint Rewrite`` declarations at the global level of that module are loaded. @@ -3561,7 +3644,7 @@ described above: either they disappear at the end of a section scope, or they remain global forever. This causes a scalability issue, because hints coming from an unrelated part of the code may badly influence another development. It can be mitigated to some extent -thanks to the ``Remove Hints`` command (see :ref:`Remove Hints <removehints>`), +thanks to the :cmd:`Remove Hints` command, but this is a mere workaround and has some limitations (for instance, external hints cannot be removed). @@ -3569,73 +3652,75 @@ A proper way to fix this issue is to bind the hints to their module scope, as for most of the other objects Coq uses. Hints should only made available when the module they are defined in is imported, not just required. It is very difficult to change the historical behavior, as it would break a lot of scripts. -We propose a smooth transitional path by providing the ``Loose Hint Behavior`` +We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior` option which accepts three flags allowing for a fine-grained handling of non-imported hints. -**Variants:** - -.. cmd:: Set Loose Hint Behavior "Lax" +.. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) + :name: Loose Hint Behavior - This is the default, and corresponds to the historical behavior, that - is, hints defined outside of a section have a global scope. + This option accepts three values, which control the behavior of hints w.r.t. + :cmd:`Import`: -.. cmd:: Set Loose Hint Behavior "Warn" + - "Lax": this is the default, and corresponds to the historical behavior, + that is, hints defined outside of a section have a global scope. - When set, it outputs a warning when a non-imported hint is used. Note that - this is an over-approximation, because a hint may be triggered by a run that - will eventually fail and backtrack, resulting in the hint not being actually - useful for the proof. + - "Warn": outputs a warning when a non-imported hint is used. Note that this + is an over-approximation, because a hint may be triggered by a run that + will eventually fail and backtrack, resulting in the hint not being + actually useful for the proof. -.. cmd:: Set Loose Hint Behavior "Strict" + - "Strict": changes the behavior of an unloaded hint to a immediate fail + tactic, allowing to emulate an import-scoped hint mechanism. - When set, it changes the behavior of an unloaded hint to a immediate fail - tactic, allowing to emulate an import-scoped hint mechanism. +.. _tactics-implicit-automation: 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 ``...``. In this case the tactic command typed by the user is equivalent to ``tactic``:sub:`1` ``;tactic``. -See also: Proof. in :ref:`TODO-7.1.4-Proofterm`. + See also: ``Proof.`` in :ref:`proof-editing-mode`. -**Variants:** -.. cmd:: Proof with tactic using {+ @ident} + .. cmdv:: Proof with tactic using {+ @ident} - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing` + Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`proof-editing-mode` -.. cmd:: Proof using {+ @ident} with tactic + .. cmdv:: Proof using {+ @ident} with @tactic - Combines in a single line ``Proof with`` and ``Proof using``, see :ref:`TODO-7.1.5-Proofusing` + 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 - time the term argument of a tactic has one of its holes not fully - resolved. + 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 + time the term argument of a tactic has one of its holes not fully + resolved. -Here is an example: + .. deprecated:: 8.9 -.. example:: + This command is deprecated. Use :ref:`typeclasses <typeclasses>` or + :ref:`tactics-in-terms <tactics-in-terms>` instead. - .. coqtop:: all + .. example:: - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. coqtop:: all - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). + + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: @@ -3680,11 +3765,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 @@ -3713,7 +3799,7 @@ 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 -mainly the tactic language (see :ref:`TODO-9-thetacticlanguage`). The code is +mainly the tactic language (see :ref:`ltac`). The code is now much shorter and a significant increase in performance has been noticed. The general behavior with respect to dependent types, unfolding and introductions has slightly changed to get clearer semantics. This may lead to @@ -3721,26 +3807,20 @@ some incompatibilities. .. tacv:: intuition - Is equivalent to :g:`intuition auto with *`. + Is equivalent to :g:`intuition auto with *`. .. tacv:: dintuition + :name: dintuition - While :tacn:`intuition` recognizes inductively defined connectives - isomorphic to the standard connective ``and, prod, or, sum, False, - Empty_set, unit, True``, :tacn:`dintuition` recognizes also all inductive - types with one constructors and no indices, i.e. record-style connectives. - -Some aspects of the tactic :tacn:`intuition` can be controlled using options. -To avoid that inner negations which do not need to be unfolded are -unfolded, use: - -.. cmd:: Unset Intuition Negation Unfolding + While :tacn:`intuition` recognizes inductively defined connectives + isomorphic to the standard connective ``and``, ``prod``, ``or``, ``sum``, ``False``, + ``Empty_set``, ``unit``, ``True``, :tacn:`dintuition` recognizes also all inductive + types with one constructors and no indices, i.e. record-style connectives. +.. opt:: Intuition Negation Unfolding -To do that all negations of the goal are unfolded even inner ones -(this is the default), use: - -.. cmd:: Set Intuition Negation Unfolding + Controls whether :tacn:`intuition` unfolds inner negations which do not need + to be unfolded. This option is on by default. .. tacn:: rtauto :name: rtauto @@ -3764,14 +3844,18 @@ 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 ``Set Firstorder -Solver`` tactic vernacular command and printed using ``Print Firstorder -Solver``. +.. opt:: Firstorder Solver @tactic + + 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. + + .. cmd:: Print Firstorder Solver + + Prints the default tactic used by :tacn:`firstorder` when no rule applies. .. 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} @@ -3788,8 +3872,9 @@ Solver``. This combines the effects of the different variants of :tacn:`firstorder`. -Proof-search is bounded by a depth parameter which can be set by -typing the ``Set Firstorder Depth n`` vernacular command. +.. opt:: Firstorder Depth @num + + This option controls the proof-search depth bound. .. tacn:: congruence :name: congruence @@ -3830,11 +3915,12 @@ match against it. hypotheses using assert in order for :tacn:`congruence` to use them. .. tacv:: congruence with {+ @term} + :name: congruence with - Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps - in case you have partially applied constructors in your goal. + Adds :n:`{+ @term}` to the pool of terms used by :tacn:`congruence`. This helps + in case you have partially applied constructors in your goal. -.. exn:: I don’t know how to handle dependent equality +.. exn:: I don’t know how to handle dependent equality. The decision procedure managed to find a proof of the goal or of a discriminable equality but this proof could not be built in Coq because of @@ -3846,7 +3932,7 @@ match against it. arguments are supplied for some partially applied constructors. Any term of an appropriate type will allow the tactic to successfully solve the goal. Those additional arguments can be given to congruence by filling in the holes in the - terms given in the error message, using the with variant described above. + terms given in the error message, using the :tacn:`congruence with` variant described above. .. opt:: Congruence Verbose @@ -3865,7 +3951,7 @@ succeeds, and results in an error otherwise. This tactic checks whether its arguments are equal modulo alpha conversion and casts. -.. exn:: Not equal +.. exn:: Not equal. .. tacn:: unify @term @term :name: unify @@ -3873,12 +3959,12 @@ succeeds, and results in an error otherwise. This tactic checks whether its arguments are unifiable, potentially instantiating existential variables. -.. exn:: Not unifiable +.. exn:: Not unifiable. .. tacv:: unify @term @term with @ident Unification takes the transparency information defined in the hint database - :n:`@ident` into account (see :ref:`the hints databases for auto and eauto <the-hints-databases-for-auto-and-eauto>`). + :n:`@ident` into account (see :ref:`the hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`). .. tacn:: is_evar @term :name: is_evar @@ -3887,7 +3973,7 @@ succeeds, and results in an error otherwise. variable. Existential variables are uninstantiated variables generated by :tacn:`eapply` and some other tactics. -.. exn:: Not an evar +.. exn:: Not an evar. .. tacn:: has_evar @term :name: has_evar @@ -3896,7 +3982,7 @@ succeeds, and results in an error otherwise. a subterm. Unlike context patterns combined with ``is_evar``, this tactic scans all subterms, including those under binders. -.. exn:: No evars +.. exn:: No evars. .. tacn:: is_var @term :name: is_var @@ -3904,7 +3990,7 @@ succeeds, and results in an error otherwise. This tactic checks whether its argument is a variable or hypothesis in the current goal context or in the opened sections. -.. exn:: Not a variable or hypothesis +.. exn:: Not a variable or hypothesis. .. _equality: @@ -3928,10 +4014,10 @@ solved by :tacn:`f_equal`. :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 -:tacn:`refl_equal`. +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. .. exn:: Unable to unify ... with ... @@ -4009,6 +4095,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 @@ -4031,6 +4118,7 @@ symbol :g:`=`. :tacn:`injection` and :tacn:`inversion` tactics. .. tacv:: dependent rewrite <- @ident + :name: dependent rewrite <- Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to left. @@ -4044,12 +4132,12 @@ 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:`TODO-2.3-advancedrecursivefunctions`). Note that this tactic is only +: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 -.. exn:: Cannot find inversion information for hypothesis @ident +.. exn:: Hypothesis @ident must contain at least one Function. +.. exn:: Cannot find inversion information for hypothesis @ident. This error may be raised when some inversion lemma failed to be generated by Function. @@ -4077,10 +4165,10 @@ This kind of inversion has nothing to do with the tactic :tacn:`inversion` above. This tactic does :g:`change (@ident t)`, where `t` is a term built in order to ensure the convertibility. In other words, it does inversion of the function :n:`@ident`. This function must be a fixpoint on a simple recursive -datatype: see :ref:`TODO-10.3-quote` for the full details. +datatype: see :ref:`quote` for the full details. -.. exn:: quote: not a simple fixpoint +.. exn:: quote: not a simple fixpoint. Happens when quote is not able to perform inversion properly. @@ -4109,6 +4197,8 @@ using the ``Require Import`` command. Use ``classical_right`` to prove the right part of the disjunction with the assumption that the negation of left part holds. +.. _tactics-automatizing: + Automatizing ------------ @@ -4148,7 +4238,7 @@ 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:`TODO-21-omega`). +(see Chapter :ref:`omega`). .. tacn:: ring @@ -4168,7 +4258,7 @@ 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:`TODO-Chapter-25-Theringandfieldtacticfamilies` for more information on +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. @@ -4194,7 +4284,7 @@ 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:`TODO-Chapter-25-Theringandfieldtacticfamilies` for more information on the tactic and how to +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. @@ -4286,24 +4376,24 @@ 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 + .. tacv:: shelve_unifiable + :name: shelve_unifiable - Shelves only the goals under focus that are mentioned in other goals. - Goals that appear in the type of other goals can be solved by unification. + Shelves only the goals under focus that are mentioned in other goals. + Goals that appear in the type of other goals can be solved by unification. -.. example:: + .. example:: - .. coqtop:: all reset + .. coqtop:: all reset - Goal exists n, n=0. - refine (ex_intro _ _ _). - all:shelve_unifiable. - reflexivity. + Goal exists n, n=0. + refine (ex_intro _ _ _). + 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 @@ -4334,11 +4424,11 @@ A simple example has more value than a long explanation: The tactics macros are synchronous with the Coq section mechanism: a tactic definition is deleted from the current environment when you -close the section (see also :ref:`TODO-2.4Sectionmechanism`) where it was +close the section (see also :ref:`section-mechanism`) where it was defined. If you want that a tactic macro defined in a module is usable in the modules that require it, you should put it outside of any section. -:ref:`TODO-9-Thetacticlanguage` gives examples of more complex +:ref:`ltac` gives examples of more complex user-defined tactics. .. [1] Actually, only the second subgoal will be generated since the |