diff options
Diffstat (limited to 'doc/sphinx/proof-engine/tactics.rst')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 118 |
1 files changed, 64 insertions, 54 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b3537bad8..3835524f0 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -96,10 +96,10 @@ bindings_list`` where ``bindings_list`` may be of two different forms: + 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:`ltac`) 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. @@ -503,7 +503,7 @@ Applying theorems .. 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 @@ -511,15 +511,15 @@ Applying theorems 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 @@ -626,22 +626,21 @@ binder. If the goal is a product, the tactic implements the "Lam" rule given in :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 an existential variable, ``intro`` forces the resolution of the -existential variable into a dependent product :math:`\forall`:g:`x:?X, ?Y`, puts +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`. -If the goal is neither a product, nor starting with a let definition, nor an existential variable, the tactic ``intro`` applies the tactic ``hnf`` until the tactic ``intro`` can be applied or the goal is not head-reducible. @@ -649,11 +648,12 @@ be applied or the goal is not head-reducible. .. 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. @@ -715,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 ... @@ -760,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`: @@ -904,21 +904,21 @@ quantification or an implication. .. tacn:: revert {+ @ident} :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 @@ -1122,7 +1122,7 @@ Controlling the proof flow 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. @@ -1130,7 +1130,7 @@ Controlling the proof flow .. 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 @@ -1139,7 +1139,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`. @@ -1192,9 +1192,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 @@ -2149,13 +2149,13 @@ See also: :ref:`advanced-recursive-functions` :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 @@ -2164,7 +2164,7 @@ See also: :ref:`advanced-recursive-functions` .. 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 @@ -3194,7 +3194,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}} @@ -3240,7 +3240,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 @@ -3444,7 +3446,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Declares each :n:`@ident` as a transparent or opaque constant. - .. cmdv:: Hint Extern @num {? @pattern} => tactic + .. cmdv:: Hint Extern @num {? @pattern} => @tactic + :name: Hint Extern 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 @@ -3665,6 +3668,7 @@ option which accepts three flags allowing for a fine-grained handling of non-imported hints. .. opt:: Loose Hint Behavior %( "Lax" %| "Warn" %| "Strict" %) + :name: Loose Hint Behavior This option accepts three values, which control the behavior of hints w.r.t. :cmd:`Import`: @@ -3809,14 +3813,15 @@ 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. + 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 @@ -3845,11 +3850,14 @@ first- order reasoning, written by Pierre Corbineau. It is not restricted to usual logical connectives but instead may reason about any first-order class inductive definition. -.. opt:: Firstorder Solver +.. 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 and - printed using :cmd:`Print Firstorder Solver`. + :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 @@ -4012,8 +4020,8 @@ 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. @@ -4105,7 +4113,7 @@ symbol :g:`=`. :n:`intro @ident; simplify_eq @ident`. .. tacn:: dependent rewrite -> @ident - :name: dependent rewrite + :name: dependent rewrite -> This tactic applies to any goal. If :n:`@ident` has type :g:`(existT B a b)=(existT B a' b')` in the local context (i.e. each @@ -4116,6 +4124,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. @@ -4375,19 +4384,20 @@ This tactics reverses the list of the focused goals. unification, or they can be called back into focus with the command :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. .. cmd:: Unshelve |