diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 59 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 118 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 31 |
4 files changed, 121 insertions, 90 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index c5ee724caf..2b128b98fe 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -245,7 +245,7 @@ focused goals with: :name: ... : ... (goal selector) We can also use selectors as a tactical, which allows to use them nested - in a tactic expression, by using the keyword :tacn:`only`: + in a tactic expression, by using the keyword ``only``: .. tacv:: only selector : expr :name: only ... : ... @@ -826,6 +826,7 @@ We can make pattern matching on goals using the following expression: .. we should provide the full grammar here .. tacn:: match goal with {+| {+ hyp} |- @cpattern => @expr } | _ => @expr end + :name: match goal If each hypothesis pattern :n:`hyp`\ :sub:`1,i`, with i=1,...,m\ :sub:`1` is matched (non-linear first-order unification) by an hypothesis of the diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 069cf8a6dc..eba0db3ff5 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -60,7 +60,6 @@ list of assertion commands is given in :ref:`Assertions`. The command used for another statement). .. cmd:: Qed - :name: Qed (interactive proof) This command is available in interactive editing proof mode when the proof is completed. Then :cmd:`Qed` extracts a proof term from the proof @@ -82,9 +81,12 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmdv:: Defined - :name: Defined (interactive proof) + :name: Defined - Defines the proved term as a transparent constant. + Same as :cmd:`Qed` but the proof is then declared transparent, which means + that its content can be explicitly used for type-checking and that it can be + unfolded in conversion tactics (see :ref:`performingcomputations`, + :cmd:`Opaque`, :cmd:`Transparent`). .. cmdv:: Save @ident :name: Save @@ -94,7 +96,6 @@ list of assertion commands is given in :ref:`Assertions`. The command has been opened using the :cmd:`Goal` command. .. cmd:: Admitted - :name: Admitted (interactive proof) This command is available in interactive editing mode to give up the current proof and declare the initial goal as an axiom. @@ -112,6 +113,8 @@ list of assertion commands is given in :ref:`Assertions`. The command Aborts the editing of the proof named :token:`ident` (in case you have nested proofs). + .. seealso:: :opt:`Nested Proofs Allowed` + .. cmdv:: Abort All Aborts all current goals. @@ -125,7 +128,6 @@ list of assertion commands is given in :ref:`Assertions`. The command proof term (see Section :ref:`applyingtheorems`). .. cmd:: Proof - :name: Proof (interactive proof) Is a no-op which is useful to delimit the sequence of tactic commands which start a proof, after a :cmd:`Theorem` command. It is a good practice to @@ -542,23 +544,34 @@ Controlling the effect of proof editing commands .. opt:: Hyps Limit @num -This option controls the maximum number of hypotheses displayed in goals -after the application of a tactic. All the hypotheses remain usable -in the proof development. -When unset, it goes back to the default mode which is to print all -available hypotheses. + This option controls the maximum number of hypotheses displayed in goals + after the application of a tactic. All the hypotheses remain usable + in the proof development. + When unset, it goes back to the default mode which is to print all + available hypotheses. .. opt:: Automatic Introduction -This option controls the way binders are handled -in assertion commands such as ``Theorem ident [binders] : form``. When the -option is on, which is the default, binders are automatically put in -the local context of the goal to prove. + This option controls the way binders are handled + in assertion commands such as :n:`Theorem @ident {? @binders} : @term`. When the + option is on, which is the default, binders are automatically put in + the local context of the goal to prove. + + When the option is off, binders are discharged on the statement to be + proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) + has to be used to move the assumptions to the local context. + + +.. opt:: Nested Proofs Allowed -When the option is off, binders are discharged on the statement to be -proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`) -has to be used to move the assumptions to the local context. + When turned on (it is off by default), this option enables support for nested + proofs: a new assertion command can be inserted before the current proof is + finished, in which case Coq will temporarily switch to the proof of this + *nested lemma*. When the proof of the nested lemma is finished (with :cmd:`Qed` + or :cmd:`Defined`), its statement will be made available (as if it had been + proved before starting the previous proof) and Coq will switch back to the + proof of the previous assertion. Controlling memory usage @@ -570,13 +583,13 @@ to force |Coq| to optimize some of its internal data structures. .. cmd:: Optimize Proof -This command forces |Coq| to shrink the data structure used to represent -the ongoing proof. + This command forces |Coq| to shrink the data structure used to represent + the ongoing proof. .. cmd:: Optimize Heap -This command forces the |OCaml| runtime to perform a heap compaction. -This is in general an expensive operation. -See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ -There is also an analogous tactic :tacn:`optimize_heap`. + This command forces the |OCaml| runtime to perform a heap compaction. + This is in general an expensive operation. + See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_ + There is also an analogous tactic :tacn:`optimize_heap`. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index b3537bad80..3835524f0a 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 diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 7ba103b222..c37233734b 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -360,6 +360,7 @@ Requests to the environment Search (?x * _ + ?x * _)%Z outside OmegaLemmas. .. cmdv:: SearchAbout + :name: SearchAbout .. deprecated:: 8.5 @@ -416,7 +417,7 @@ Requests to the environment current goal (if any) and theorems of the current context whose statement’s conclusion or last hypothesis and conclusion matches the expressionterm where holes in the latter are denoted by `_`. - It is a variant of Search @term_pattern that does not look for subterms + It is a variant of :n:`Search @term_pattern` that does not look for subterms but searches for statements whose conclusion has exactly the expected form, or whose statement finishes by the given series of hypothesis/conclusion. @@ -625,6 +626,7 @@ file is a particular case of module called *library file*. .. cmdv:: Require Import @qualid + :name: Require Import This loads and declares the module :n:`@qualid` and its dependencies then imports the contents of :n:`@qualid` as described @@ -637,10 +639,11 @@ file is a particular case of module called *library file*. :cmd:`Import` :n:`@qualid` would. .. cmdv:: Require Export @qualid + :name: Require Export - This command acts as ``Require Import`` :n:`@qualid`, - but if a further module, say `A`, contains a command ``Require Export`` `B`, - then the command ``Require Import`` `A` also imports the module `B.` + This command acts as :cmd:`Require Import` :n:`@qualid`, + but if a further module, say `A`, contains a command :cmd:`Require Export` `B`, + then the command :cmd:`Require Import` `A` also imports the module `B.` .. cmdv:: Require [Import | Export] {+ @qualid } @@ -653,7 +656,7 @@ file is a particular case of module called *library file*. .. cmdv:: From @dirpath Require @qualid - This command acts as ``Require``, but picks + This command acts as :cmd:`Require`, but picks any library whose absolute name is of the form dirpath.dirpath’.qualid for some `dirpath’`. This is useful to ensure that the :n:`@qualid` library comes from a given package by making explicit its absolute root. @@ -895,6 +898,7 @@ interactively, they cannot be part of a vernacular file loaded via necessary. .. cmdv:: Backtrack @num @num @num + :name: Backtrack .. deprecated:: 8.4 @@ -1022,12 +1026,14 @@ Controlling display output, printing only identifiers. .. opt:: Printing Width @num + :name: Printing Width This command sets which left-aligned part of the width of the screen is used for display. At the time of writing this documentation, the default value is 78. .. opt:: Printing Depth @num + :name: Printing Depth This option controls the nesting depth of the formatter used for pretty- printing. Beyond this depth, display of subterms is replaced by dots. At the @@ -1208,28 +1214,29 @@ scope of their effect. There are four kinds of commands: + Commands whose default is to extend their effect both outside the section and the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the - current section or module it occurs in. As an example, the ``Coercion`` - (see Section :ref:`coercions`) and ``Strategy`` (see :ref:`here <vernac-strategy>`) - commands belong to this category. + current section or module it occurs in. As an example, the :cmd:`Coercion` + and :cmd:`Strategy` commands belong to this category. + Commands whose default behavior is to stop their effect at the end of the section they occur in but to extent their effect outside the module or library file they occur in. For these commands, the Local modifier limits the effect of the command to the current module if the command does not occur in a section and the Global modifier extends the effect outside the current sections and current module if the command occurs in a section. As an example, - the :cmd:`Implicit Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong + the :cmd:`Arguments`, :cmd:`Ltac` or :cmd:`Notation` commands belong to this category. Notice that a subclass of these commands do not support extension of their scope outside sections at all and the Global is not applicable to them. + Commands whose default behavior is to stop their effect at the end - of the section or module they occur in. For these commands, the Global + of the section or module they occur in. For these commands, the ``Global`` modifier extends their effect outside the sections and modules they - occurs in. The ``Transparent`` and ``Opaque`` (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands belong to this category. + occurs in. The :cmd:`Transparent` and :cmd:`Opaque` + (see Section :ref:`vernac-controlling-the-reduction-strategies`) commands + belong to this category. + Commands whose default behavior is to extend their effect outside sections but not outside modules when they occur in a section and to extend their effect outside the module or library file they occur in when no section contains them.For these commands, the Local modifier limits the effect to the current section or module while the Global modifier extends the effect outside the module even when the command - occurs in a section. The ``Set`` and ``Unset`` commands belong to this + occurs in a section. The :cmd:`Set` and :cmd:`Unset` commands belong to this category. |