diff options
| author | Jim Fehrle | 2020-09-12 20:54:22 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-12-30 11:48:37 -0800 |
| commit | e02120ed6580733db2276f0c11b4f432ea670ee3 (patch) | |
| tree | 19c809eeea61fe131e4b4b15bc0bc72c617cce53 | |
| parent | 532cbed036c48ed2c77528b79fc947c4bc7e1c10 (diff) | |
Convert rewriting and proof-mode chapters to prodn
49 files changed, 725 insertions, 681 deletions
diff --git a/doc/sphinx/README.rst b/doc/sphinx/README.rst index bfdbc4c4db..9495fd0e45 100644 --- a/doc/sphinx/README.rst +++ b/doc/sphinx/README.rst @@ -107,7 +107,7 @@ Here is the list of all objects of the Coq domain (The symbol :black_nib: indica .. cmd:: Axiom @ident : @term. This command links :token:`term` to the name :token:`term` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + the global environment. The fact asserted by :token:`term` is thus assumed as a postulate. .. cmdv:: Parameter @ident : @term. diff --git a/doc/sphinx/addendum/extraction.rst b/doc/sphinx/addendum/extraction.rst index 3662822a5e..8e72bb4ffd 100644 --- a/doc/sphinx/addendum/extraction.rst +++ b/doc/sphinx/addendum/extraction.rst @@ -100,7 +100,6 @@ Setting the target language ~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Extraction Language @language - :name: Extraction Language .. insertprodn language language @@ -431,12 +430,10 @@ Additional settings ~~~~~~~~~~~~~~~~~~~ .. opt:: Extraction File Comment @string - :name: Extraction File Comment Provides a comment that is included at the beginning of the output files. .. opt:: Extraction Flag @natural - :name: Extraction Flag Controls which optimizations are used during extraction, providing a finer-grained control than :flag:`Extraction Optimize`. The bits of :token:`natural` are used as a bit mask. diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 039a23e8c2..c54db36691 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -101,7 +101,7 @@ morphisms, that are required to be simultaneously monotone on every argument. Morphisms can also be contravariant in one or more of their arguments. -A morphism is contravariant on an argument associated to the relation +A morphism is contravariant on an argument associated with the relation instance :math:`R` if it is covariant on the same argument when the inverse relation :math:`R^{−1}` (``inverse R`` in Coq) is considered. The special arrow ``-->`` is used in signatures for contravariant morphisms. @@ -336,7 +336,7 @@ respective relation instances. in the previous example). Applying ``union_compat`` by hand we are left with the goal ``eq_set (union S S) (union S S)``. -When the relations associated to some arguments are not reflexive, the +When the relations associated with some arguments are not reflexive, the tactic cannot automatically prove the reflexivity goals, that are left to the user. @@ -477,8 +477,8 @@ documentation on :ref:`typeclasses` and the theories files in Classes for further explanations. One can inform the rewrite tactic about morphisms and relations just -by using the typeclass mechanism to declare them using Instance and -Context vernacular commands. Any object of type Proper (the type of +by using the typeclass mechanism to declare them using the :cmd:`Instance` and +:cmd:`Context` commands. Any object of type Proper (the type of morphism declarations) in the local context will also be automatically used by the rewriting tactic to solve constraints. @@ -553,7 +553,7 @@ pass additional arguments such as ``using relation``. be used to replace the first tactic argument with the second one. If omitted, it defaults to the ``DefaultRelation`` instance on the type of the objects. By default, it means the most recent ``Equivalence`` instance - in the environment, but it can be customized by declaring + in the global environment, but it can be customized by declaring new ``DefaultRelation`` instances. As Leibniz equality is a declared equivalence, it will fall back to it if no other relation is declared on a given type. @@ -608,7 +608,6 @@ Deprecated syntax and backward incompatibilities an old development to the new semantics is usually quite simple. .. cmd:: Declare Morphism @one_term : @ident - :name: Declare Morphism Declares a parameter in a module type that is a morphism. @@ -686,7 +685,7 @@ Note that when one does rewriting with a lemma under a binder using variable, as the semantics are different from rewrite where the lemma is first matched on the whole term. With the new :tacn:`setoid_rewrite`, matching is done on each subterm separately and in its local -environment, and all matches are rewritten *simultaneously* by +context, and all matches are rewritten *simultaneously* by default. The semantics of the previous :tacn:`setoid_rewrite` implementation can almost be recovered using the ``at 1`` modifier. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 0f0ccd6a20..09b2bb003a 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -202,7 +202,6 @@ Use :n:`:>` instead of :n:`:` before the :undocumented: .. cmd:: SubClass @ident_decl @def_body - :name: SubClass If :n:`@type` is a class :n:`@ident'` applied to some arguments then :n:`@ident` is defined and an identity coercion of name @@ -243,7 +242,6 @@ Activating the Printing of Coercions By default, coercions are not printed. .. table:: Printing Coercion @qualid - :name: Printing Coercion Specifies a set of qualids for which coercions are always displayed. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index 28b60878d2..38c4886e0f 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -140,7 +140,6 @@ and checked to be :math:`-1`. ------------------------------------------------------------------- .. tacn:: lra - :name: lra This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone* defined as @@ -154,7 +153,6 @@ and checked to be :math:`-1`. --------------------------------------------- .. tacn:: lia - :name: lia This tactic solves linear goals over :g:`Z` by searching for *linear* refutations and cutting planes. :tacn:`lia` provides support for :g:`Z`, :g:`nat`, :g:`positive` and :g:`N` by pre-processing via the :tacn:`zify` tactic. @@ -220,7 +218,6 @@ a proof. -------------------------------------------------- .. tacn:: nra - :name: nra This tactic is an *experimental* proof procedure for non-linear arithmetic. The tactic performs a limited amount of non-linear @@ -241,7 +238,6 @@ proof by abstracting monomials by variables. ---------------------------------------------------------- .. tacn:: nia - :name: nia This tactic is a proof procedure for non-linear integer arithmetic. It performs a pre-processing similar to :tacn:`nra`. The obtained goal is @@ -251,7 +247,6 @@ proof by abstracting monomials by variables. ---------------------------------------------------- .. tacn:: psatz @one_term {? @nat_or_var } - :name: psatz This tactic explores the *Cone* by increasing degrees – hence the depth parameter :token:`nat_or_var`. In theory, such a proof search is complete – if the @@ -281,7 +276,6 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid. ------------------------------------------ .. tacn:: zify - :name: zify This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`. Additional support is provided by the following modules: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 2b10f5671d..0997c5e868 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -28,7 +28,6 @@ Description of ``omega`` ------------------------ .. tacn:: omega - :name: omega .. deprecated:: 8.12 diff --git a/doc/sphinx/addendum/parallel-proof-processing.rst b/doc/sphinx/addendum/parallel-proof-processing.rst index e824ae152d..ea506cec84 100644 --- a/doc/sphinx/addendum/parallel-proof-processing.rst +++ b/doc/sphinx/addendum/parallel-proof-processing.rst @@ -70,7 +70,7 @@ Coq 8.6 introduced a mechanism for error resilience: in interactive mode Coq is able to completely check a document containing errors instead of bailing out at the first failure. -Two kind of errors are supported: errors occurring in vernacular +Two kind of errors are supported: errors occurring in commands and errors occurring in proofs. To properly recover from a failing tactic, Coq needs to recognize the @@ -89,8 +89,8 @@ kind of proof blocks, and an ML API to add new ones. Caveats ```````` -When a vernacular command fails the subsequent error messages may be -bogus, i.e. caused by the first error. Error resilience for vernacular +When a command fails the subsequent error messages may be +bogus, i.e. caused by the first error. Error resilience for commands can be switched off by passing ``-async-proofs-command-error-resilience off`` to CoqIDE. diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 104f84a253..2b24ced8a1 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -161,7 +161,7 @@ Program Definition A :cmd:`Definition` command with the :attr:`program` attribute types the value term in Russell and generates proof obligations. Once solved using the commands shown below, it binds the -final Coq term to the name :n:`@ident` in the environment. +final Coq term to the name :n:`@ident` in the global environment. :n:`Program Definition @ident : @type := @term` @@ -268,7 +268,6 @@ obligations (e.g. when defining mutually recursive blocks). The optional tactic is replaced by the default one if not specified. .. cmd:: Obligation Tactic := @ltac_expr - :name: Obligation Tactic Sets the default obligation solving tactic applied to all obligations automatically, whether to solve them or when starting to prove one, diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index c93d621048..954c2c1446 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -421,7 +421,7 @@ Error messages: .. exn:: Ring operation should be declared as a morphism. - A setoid associated to the carrier of the ring structure has been found, + A setoid associated with the carrier of the ring structure has been found, but the ring operation should be declared as morphism. See :ref:`tactics-enabled-on-user-provided-relations`. How does it work? diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst index 2b1f343e14..8c20e08154 100644 --- a/doc/sphinx/addendum/sprop.rst +++ b/doc/sphinx/addendum/sprop.rst @@ -19,7 +19,6 @@ Use of |SProp| may be disabled by passing ``-disallow-sprop`` to the Coq program or by turning the :flag:`Allow StrictProp` flag off. .. flag:: Allow StrictProp - :name: Allow StrictProp Enables or disables the use of |SProp|. It is enabled by default. The command-line flag ``-disallow-sprop`` disables |SProp| at @@ -283,7 +282,6 @@ This means that some errors will be delayed until ``Qed``: Abort. .. flag:: Elaboration StrictProp Cumulativity - :name: Elaboration StrictProp Cumulativity Unset this flag (it is on by default) to be strict with regard to :math:`\SProp` cumulativity during elaboration. @@ -320,7 +318,6 @@ so correctly converts ``x`` and ``y``. it to find when your tactics are producing incorrect marks. .. flag:: Cumulative StrictProp - :name: Cumulative StrictProp Set this flag (it is off by default) to make the kernel accept cumulativity between |SProp| and other universes. This makes diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 4143d836c4..8dc0030115 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -160,7 +160,7 @@ Sections and contexts --------------------- To ease developments parameterized by many instances, one can use the -:cmd:`Context` command to introduce these parameters into section contexts, +:cmd:`Context` command to introduce the parameters into the :term:`local context`, it works similarly to the command :cmd:`Variable`, except it accepts any binding context as an argument, so variables can be implicit, and :ref:`implicit-generalization` can be used. @@ -422,7 +422,7 @@ Summary of the commands resolution with the local hypotheses use full conversion during unification. - + The mode hints (see :cmd:`Hint Mode`) associated to a class are + + The mode hints (see :cmd:`Hint Mode`) associated with a class are taken into account by :tacn:`typeclasses eauto`. When a goal does not match any of the declared modes for its head (if any), instead of failing like :tacn:`eauto`, the goal is suspended and @@ -470,7 +470,6 @@ Summary of the commands refinement engine will be able to backtrack. .. tacn:: autoapply @one_term with @ident - :name: autoapply The tactic ``autoapply`` applies :token:`one_term` using the transparency information of the hint database :token:`ident`, and does *no* typeclass resolution. This can @@ -590,7 +589,6 @@ Settings :cmd:`Typeclasses eauto` is another way to set this flag. .. opt:: Typeclasses Depth @natural - :name: Typeclasses Depth Sets the maximum proof search depth. The default is unbounded. :cmd:`Typeclasses eauto` is another way to set this option. @@ -602,7 +600,6 @@ Settings is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @natural - :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving @@ -613,7 +610,6 @@ Typeclasses eauto ~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug } {? ( {| bfs | dfs } ) } {? @natural } - :name: Typeclasses eauto Allows more global customization of the :tacn:`typeclasses eauto` tactic. The options are: diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index bb78b142ca..d0b05a03f9 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -328,7 +328,7 @@ Cumulativity Weak Constraints Global and local universes --------------------------- -Each universe is declared in a global or local environment before it +Each universe is declared in a global or local context before it can be used. To ensure compatibility, every *global* universe is set to be strictly greater than :g:`Set` when it is introduced, while every *local* (i.e. polymorphically quantified) universe is introduced as @@ -617,7 +617,7 @@ definitions in the section sharing a common variable will both get parameterized by the universes produced by the variable declaration. This is in contrast to a “mononorphic” variable which introduces global universes and constraints, making the two definitions depend on -the *same* global universes associated to the variable. +the *same* global universes associated with the variable. It is possible to mix universe polymorphism and monomorphism in sections, except in the following ways: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index fcb150e3da..b9a3c1973c 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -943,7 +943,7 @@ Notations by Hugo Herbelin). - **Fixed:** Different interpretations in different scopes of the same notation - string can now be associated to different printing formats (`#10832 + string can now be associated with different printing formats (`#10832 <https://github.com/coq/coq/pull/10832>`_, by Hugo Herbelin, fixes `#6092 <https://github.com/coq/coq/issues/6092>`_ and `#7766 <https://github.com/coq/coq/issues/7766>`_). @@ -2222,7 +2222,7 @@ Changes in 8.11+beta1 documentation. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) - **Added:** - The :cmd:`Section` vernacular command now accepts the "universes" attribute. In + The :cmd:`Section` command now accepts the "universes" attribute. In addition to setting the section universe polymorphism, it also locally sets the universe polymorphic option inside the section. (`#10441 <https://github.com/coq/coq/pull/10441>`_, by Pierre-Marie Pédrot) @@ -3221,7 +3221,7 @@ Other changes in 8.10+beta1 New `relpre R f` definition for the preimage of a relation R under f (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). -- Vernacular commands: +- Commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. Names may not be repeated, and may not overlap with section variable names @@ -3553,7 +3553,7 @@ Changes in 8.10.2 **Notations** -- Fixed an 8.10 regression related to the printing of coercions associated to notations +- Fixed an 8.10 regression related to the printing of coercions associated with notations (`#11090 <https://github.com/coq/coq/pull/11090>`_, fixes `#11033 <https://github.com/coq/coq/issues/11033>`_, by Hugo Herbelin). @@ -3794,7 +3794,7 @@ Focusing - Focusing bracket `{` now supports named goal selectors, e.g. `[x]: {` will focus on a goal (existential variable) named `x`. - As usual, unfocus with `}` once the sub-goal is fully solved. + As usual, unfocus with `}` once the subgoal is fully solved. Specification language @@ -3859,7 +3859,7 @@ Tools please open an issue. We can help set up external maintenance as part of Proof-General, or independently as part of coq-community. -Vernacular Commands +Commands - Removed deprecated commands `Arguments Scope` and `Implicit Arguments` (not the option). Use the `Arguments` command instead. @@ -4130,11 +4130,11 @@ Tactics Focusing - Focusing bracket `{` now supports single-numbered goal selector, - e.g. `2: {` will focus on the second sub-goal. As usual, unfocus - with `}` once the sub-goal is fully solved. + e.g. `2: {` will focus on the second subgoal. As usual, unfocus + with `}` once the subgoal is fully solved. The `Focus` and `Unfocus` commands are now deprecated. -Vernacular Commands +Commands - Proofs ending in "Qed exporting ident, .., ident" are not supported anymore. Constants generated during `abstract` are kept private to the @@ -4508,7 +4508,7 @@ Gallina - Now supporting all kinds of binders, including 'pat, in syntax of record fields. -Vernacular Commands +Commands - Goals context can be printed in a more compact way when `Set Printing Compact Contexts` is activated. @@ -5340,7 +5340,7 @@ Logic the dependent one. To recover the old behavior, explicitly define your inductive types in Set. -Vernacular commands +Commands - A command "Variant" allows to define non-recursive variant types. - The command "Record foo ..." does not generate induction principles @@ -5797,7 +5797,7 @@ API Details of changes in 8.5beta3 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - New command "Redirect" to redirect the output of a command to a file. - New command "Undelimit Scope" to remove the delimiter of a scope. @@ -6176,7 +6176,7 @@ Regarding decision tactics, Loïc Pottier maintained nsatz, moving in particular to a typeclass based reification of goals while Frédéric Besson maintained Micromega, adding in particular support for division. -Regarding vernacular commands, Stéphane Glondu provided new commands to +Regarding commands, Stéphane Glondu provided new commands to analyze the structure of type universes. Regarding libraries, a new library about lists of a given length (called @@ -6373,7 +6373,7 @@ Tactics constructor. Last one can mark a constant so that it is unfolded only if the simplified term does not expose a match in head position. -Vernacular commands +Commands - It is now mandatory to have a space (or tabulation or newline or end-of-file) after a "." ending a sentence. @@ -6563,7 +6563,7 @@ Tools Details of changes in 8.4beta2 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - Commands "Back" and "BackTo" are now handling the proof states. They may perform some extra steps of backtrack to avoid states where the proof @@ -6612,7 +6612,7 @@ CoqIDE Details of changes in 8.4 ~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - The "Reset" command is now supported again in files given to coqc or Load. - "Show Script" now indents again the displayed scripts. It can also work @@ -6916,7 +6916,7 @@ Type classes anonymous instances, declarations giving terms, better handling of sections and [Context]. -Vernacular commands +Commands - New command "Timeout <n> <command>." interprets a command and a timeout interrupts the execution after <n> seconds. @@ -7089,7 +7089,7 @@ implement a new resolution-based version of the tactics dedicated to rewriting on arbitrary transitive relations. Another major improvement of Coq 8.2 is the evolution of the arithmetic -libraries and of the tools associated to them. Benjamin Grégoire and +libraries and of the tools associated with them. Benjamin Grégoire and Laurent Théry contributed a modular library for building arbitrarily large integers from bounded integers while Evgeny Makarov contributed a modular library of abstract natural and integer arithmetic together @@ -7197,7 +7197,7 @@ Language of easily fixed incompatibility in case of manual definition of a recursor in a recursive singleton inductive type]. -Vernacular commands +Commands - Added option Global to "Arguments Scope" for section surviving. - Added option "Unset Elimination Schemes" to deactivate the automatic @@ -7797,7 +7797,7 @@ Syntax - Support for primitive interpretation of string literals - Extended support for Unicode ranges -Vernacular commands +Commands - Added "Print Ltac qualid" to print a user defined tactic. - Added "Print Rewrite HintDb" to print the content of a DB used by @@ -7975,7 +7975,7 @@ Libraries - Acc in Wf.v and clos_refl_trans in Relation_Operators.v now rely on the allowance for recursively non uniform parameters (possible source of incompatibilities: explicit pattern-matching on these - types may require to remove the occurrence associated to their + types may require to remove the occurrence associated with their recursively non uniform parameter). - Coq.List.In_dec has been set transparent (this may exceptionally break proof scripts, set it locally opaque for compatibility). @@ -8194,7 +8194,7 @@ Syntax for arithmetic - Locate applied to a simple string (e.g. "+") searches for all notations containing this string -Vernacular commands +Commands - "Declare ML Module" now allows to import .cma files. This avoids to use a bunch of "Declare ML Module" statements when using several ML files. @@ -8355,7 +8355,7 @@ New concrete syntax - A completely new syntax for terms - A more uniform syntax for tactics and the tactic language -- A few syntactic changes for vernacular commands +- A few syntactic changes for commands - A smart automatic translator translating V8.0 files in old syntax to files valid for V8.0 @@ -8426,7 +8426,7 @@ Known problems of the automatic translation Details of changes in 8.0 ~~~~~~~~~~~~~~~~~~~~~~~~~ -Vernacular commands +Commands - New option "Set Printing All" to deactivate all high-level forms of printing (implicit arguments, coercions, destructing let, diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index bce88cebde..e2e37ec438 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -183,11 +183,8 @@ todo_include_todos = False nitpicky = True nitpick_ignore = [ ('token', token) for token in [ - 'tactic', 'induction_clause', - 'conversion', 'where', - 'oriented_rewriter', 'bindings_with_parameters', 'destruction_arg' ]] diff --git a/doc/sphinx/history.rst b/doc/sphinx/history.rst index c5ef92a1bf..44f2d23801 100644 --- a/doc/sphinx/history.rst +++ b/doc/sphinx/history.rst @@ -954,7 +954,7 @@ Parsing and grammar extension for Time and to write grammar rules abbreviating several commands) (+) - The default parser for actions in the grammar rules (and for - patterns in the pretty-printing rules) is now the one associated to + patterns in the pretty-printing rules) is now the one associated with the grammar (i.e. vernac, tactic or constr); no need then for quotations as in <:vernac:<...>>; to return an "ast", the grammar must be explicitly typed with tag ": ast" or ": ast list", or if a @@ -1346,12 +1346,12 @@ Language instead to simulate the old behaviour of Local (the section part of the name is not kept though) -ML tactic and vernacular commands +ML tactics and commands - "Grammar tactic" and "Grammar vernac" of type "ast" are no longer supported (only "Grammar tactic simple_tactic" of type "tactic" remains available). -- Concrete syntax for ML written vernacular commands and tactics is +- Concrete syntax for ML written commands and tactics is now declared at ML level using camlp4 macros TACTIC EXTEND et VERNAC COMMAND EXTEND. - "Check n c" now "n:Check c", "Eval n ..." now "n:Eval ..." diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 06a677d837..0b183d3f3f 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -45,9 +45,9 @@ This manual is organized in three main parts, plus an appendix: translated down to the language of the kernel by means of an "elaboration process". -- **The second part presents the interactive proof mode**, the central +- **The second part presents proof mode**, the central feature of Coq. :ref:`writing-proofs` introduces this interactive - proof mode and the available proof languages. + mode and the available proof languages. :ref:`automatic-tactics` presents some more advanced tactics, while :ref:`writing-tactics` is about the languages that allow a user to combine tactics together and develop new ones. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 85b04f6df0..1cfd8dac50 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -101,7 +101,7 @@ and it can be applied to any expression of type :math:`\nat`, say :math:`t`, to object :math:`P~t` of type :math:`\Prop`, namely a proposition. Furthermore :g:`forall x:nat, P x` will represent the type of functions -which associate to each natural number :math:`n` an object of type :math:`(P~n)` and +which associate with each natural number :math:`n` an object of type :math:`(P~n)` and consequently represent the type of proofs of the formula “:math:`∀ x.~P(x)`”. @@ -111,51 +111,49 @@ Typing rules ---------------- As objects of type theory, terms are subjected to *type discipline*. -The well typing of a term depends on a global environment and a local -context. - +The well typing of a term depends on a local context and a global environment. .. _Local-context: **Local context.** -A *local context* is an ordered list of *local declarations* of names -which we call *variables*. The declaration of some variable :math:`x` is -either a *local assumption*, written :math:`x:T` (:math:`T` is a type) or a *local -definition*, written :math:`x:=t:T`. We use brackets to write local contexts. -A typical example is :math:`[x:T;~y:=u:U;~z:V]`. Notice that the variables +A :term:`local context` is an ordered list of declarations of *variables*. +The declaration of a variable :math:`x` is +either an *assumption*, written :math:`x:T` (where :math:`T` is a type) or a +*definition*, written :math:`x:=t:T`. Local contexts are written in brackets, +for example :math:`[x:T;~y:=u:U;~z:V]`. The variables declared in a local context must be distinct. If :math:`Γ` is a local context -that declares some :math:`x`, we -write :math:`x ∈ Γ`. By writing :math:`(x:T) ∈ Γ` we mean that either :math:`x:T` is an -assumption in :math:`Γ` or that there exists some :math:`t` such that :math:`x:=t:T` is a -definition in :math:`Γ`. If :math:`Γ` defines some :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`. +that declares :math:`x`, we +write :math:`x ∈ Γ`. Writing :math:`(x:T) ∈ Γ` means there is an assumption +or a definition giving the type :math:`T` to :math:`x` in :math:`Γ`. +If :math:`Γ` defines :math:`x:=t:T`, we also write :math:`(x:=t:T) ∈ Γ`. For the rest of the chapter, :math:`Γ::(y:T)` denotes the local context :math:`Γ` enriched with the local assumption :math:`y:T`. Similarly, :math:`Γ::(y:=t:T)` denotes the local context :math:`Γ` enriched with the local definition :math:`(y:=t:T)`. The -notation :math:`[]` denotes the empty local context. By :math:`Γ_1 ; Γ_2` we mean +notation :math:`[]` denotes the empty local context. Writing :math:`Γ_1 ; Γ_2` means concatenation of the local context :math:`Γ_1` and the local context :math:`Γ_2`. - .. _Global-environment: **Global environment.** -A *global environment* is an ordered list of *global declarations*. -Global declarations are either *global assumptions* or *global -definitions*, but also declarations of inductive objects. Inductive -objects themselves declare both inductive or coinductive types and -constructors (see Section :ref:`inductive-definitions`). - -A *global assumption* will be represented in the global environment as -:math:`(c:T)` which assumes the name :math:`c` to be of some type :math:`T`. A *global -definition* will be represented in the global environment as :math:`c:=t:T` -which defines the name :math:`c` to have value :math:`t` and type :math:`T`. We shall call +A :term:`global environment` is an ordered list of *declarations*. +Global declarations are either *assumptions*, *definitions* +or declarations of inductive objects. Inductive +objects declare both constructors and inductive or +coinductive types (see Section :ref:`inductive-definitions`). + +In the global environment, +*assumptions* are written as +:math:`(c:T)`, indicating that :math:`c` is of the type :math:`T`. *Definitions* +are written as :math:`c:=t:T`, indicating that :math:`c` has the value :math:`t` +and type :math:`T`. We shall call such names *constants*. For the rest of the chapter, the :math:`E;~c:T` denotes -the global environment :math:`E` enriched with the global assumption :math:`c:T`. +the global environment :math:`E` enriched with the assumption :math:`c:T`. Similarly, :math:`E;~c:=t:T` denotes the global environment :math:`E` enriched with the -global definition :math:`(c:=t:T)`. +definition :math:`(c:=t:T)`. The rules for inductive definitions (see Section :ref:`inductive-definitions`) have to be considered as assumption -rules to which the following definitions apply: if the name :math:`c` +rules in which the following definitions apply: if the name :math:`c` is declared in :math:`E`, we write :math:`c ∈ E` and if :math:`c:T` or :math:`c:=t:T` is declared in :math:`E`, we write :math:`(c : T) ∈ E`. @@ -315,7 +313,7 @@ following rules. .. note:: We may have :math:`\letin{x}{t:T}{u}` well-typed without having :math:`((λ x:T.~u)~t)` well-typed (where :math:`T` is a type of - :math:`t`). This is because the value :math:`t` associated to + :math:`t`). This is because the value :math:`t` associated with :math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index d061ed41f1..4f54e33758 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -902,7 +902,6 @@ In addition to the powerful ``ring``, ``field`` and ``lra`` tactics (see Chapter :ref:`tactics`), there are also: .. tacn:: discrR - :name: discrR Proves that two real integer constants are different. @@ -916,7 +915,6 @@ tactics (see Chapter :ref:`tactics`), there are also: discrR. .. tacn:: split_Rabs - :name: split_Rabs Allows unfolding the ``Rabs`` constant and splits corresponding conjunctions. @@ -930,7 +928,6 @@ tactics (see Chapter :ref:`tactics`), there are also: intro; split_Rabs. .. tacn:: split_Rmult - :name: split_Rmult Splits a condition that a product is non null into subgoals corresponding to the condition on each operand of the product. diff --git a/doc/sphinx/language/core/assumptions.rst b/doc/sphinx/language/core/assumptions.rst index e86a6f4a67..8dbc1626ba 100644 --- a/doc/sphinx/language/core/assumptions.rst +++ b/doc/sphinx/language/core/assumptions.rst @@ -115,10 +115,10 @@ Section :ref:`explicit-applications`). Assumptions ----------- -Assumptions extend the environment with axioms, parameters, hypotheses +Assumptions extend the global environment with axioms, parameters, hypotheses or variables. An assumption binds an :n:`@ident` to a :n:`@type`. It is accepted -by Coq if and only if this :n:`@type` is a correct type in the environment -preexisting the declaration and if :n:`@ident` was not previously defined in +by Coq only if :n:`@type` is a correct type in the global environment +before the declaration and if :n:`@ident` was not previously defined in the same module. This :n:`@type` is considered to be the type (or specification, or statement) assumed by :n:`@ident` and we say that :n:`@ident` has type :n:`@type`. @@ -141,7 +141,7 @@ has type :n:`@type`. of_type ::= {| : | :> } @type These commands bind one or more :n:`@ident`\(s) to specified :n:`@type`\(s) as their specifications in - the global context. The fact asserted by :n:`@type` (or, equivalently, the existence + the global environment. The fact asserted by :n:`@type` (or, equivalently, the existence of an object of this type) is accepted as a postulate. They accept the :attr:`program` attribute. :cmd:`Axiom`, :cmd:`Conjecture`, :cmd:`Parameter` and their plural forms diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 2b262b89c0..0a61c4ce22 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -64,7 +64,7 @@ appending the level to the nonterminal name (as in :n:`@term100` or populated by notations or plugins. Furthermore, some parsing rules are only activated in certain - contexts (:ref:`interactive proof mode <proofhandling>`, + contexts (:ref:`proof mode <proofhandling>`, :ref:`custom entries <custom-entries>`...). .. warning:: @@ -332,9 +332,9 @@ rest of the Coq manual: :term:`terms <term>` and :term:`types tactic - Tactics specify how to transform the current proof state as a + A :production:`tactic` specifies how to transform the current proof state as a step in creating a proof. They are syntactically valid only when - Coq is in proof mode, such as after a :cmd:`Theorem` command + Coq is in :term:`proof mode`, such as after a :cmd:`Theorem` command and before any subsequent proof-terminating command such as :cmd:`Qed`. See :ref:`proofhandling` for more on proof mode. @@ -450,7 +450,6 @@ they appear after a boldface label. They are listed in the :ref:`options_index`. .. cmd:: Set @setting_name {? {| @integer | @string } } - :name: Set If :n:`@setting_name` is a flag, no value may be provided; the flag is set to on. @@ -471,7 +470,6 @@ they appear after a boldface label. They are listed in the Coq versions. .. cmd:: Unset @setting_name - :name: Unset If :n:`@setting_name` is a flag, it is set to off. If :n:`@setting_name` is an option, it is set to its default value. diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index cf46580bdb..e742139134 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -194,7 +194,7 @@ Top-level definitions of co-recursive functions As in the :cmd:`Fixpoint` command, the :n:`with` clause allows simultaneously defining several mutual cofixpoints. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. diff --git a/doc/sphinx/language/core/conversion.rst b/doc/sphinx/language/core/conversion.rst index 7395b12339..09c619338b 100644 --- a/doc/sphinx/language/core/conversion.rst +++ b/doc/sphinx/language/core/conversion.rst @@ -47,7 +47,7 @@ refer the interested reader to :cite:`Coq85`. ι-reduction ~~~~~~~~~~~ -A specific conversion rule is associated to the inductive objects in +A specific conversion rule is associated with the inductive objects in the global environment. We shall give later on (see Section :ref:`Well-formed-inductive-definitions`) the precise rules but it just says that a destructor applied to an object built from a @@ -159,7 +159,8 @@ relation :math:`t` reduces to :math:`u` in the global environment reductions β, δ, ι or ζ. We say that two terms :math:`t_1` and :math:`t_2` are -*βδιζη-convertible*, or simply :gdef:`convertible`, or *equivalent*, in the +*βδιζη-convertible*, or simply :gdef:`convertible`, or +:term:`definitionally equal <definitional equality>`, in the global environment :math:`E` and local context :math:`Γ` iff there exist terms :math:`u_1` and :math:`u_2` such that :math:`E[Γ] ⊢ t_1 \triangleright … \triangleright u_1` and :math:`E[Γ] ⊢ t_2 \triangleright … \triangleright u_2` and either :math:`u_1` and diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 6da1f90ecb..7196c082ed 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -56,7 +56,7 @@ has type :n:`@type`. Top-level definitions --------------------- -Definitions extend the environment with associations of names to terms. +Definitions extend the global environment with associations of names to terms. A definition can be seen as a way to give a meaning to a name or as a way to abbreviate a term. In any case, the name can later be replaced at any time by its definition. @@ -82,7 +82,7 @@ Section :ref:`typing-rules`. | {* @binder } : @type reduce ::= Eval @red_expr in - These commands bind :n:`@term` to the name :n:`@ident` in the environment, + These commands bind :n:`@term` to the name :n:`@ident` in the global environment, provided that :n:`@term` is well-typed. They can take the :attr:`local` :term:`attribute`, which makes the defined :n:`@ident` accessible by :cmd:`Import` and its variants only through their fully qualified names. @@ -94,7 +94,7 @@ Section :ref:`typing-rules`. :attr:`bypass_check(universes)`, :attr:`bypass_check(guard)`, and :attr:`using` attributes. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -120,10 +120,11 @@ Section :ref:`typing-rules`. Assertions and proofs --------------------- -An assertion states a proposition (or a type) of which the proof (or an -inhabitant of the type) is interactively built using tactics. The interactive -proof mode is described in Chapter :ref:`proofhandling` and the tactics in -Chapter :ref:`Tactics`. The basic assertion command is: +An assertion states a proposition (or a type) for which the proof (or an +inhabitant of the type) is interactively built using :term:`tactics <tactic>`. +Assertions cause Coq to enter :term:`proof mode` (see :ref:`proofhandling`). +Common tactics are described in the :ref:`writing-proofs` chapter. +The basic assertion command is: .. cmd:: @thm_token @ident_decl {* @binder } : @type {* with @ident_decl {* @binder } : @type } :name: Theorem; Lemma; Fact; Remark; Corollary; Proposition; Property @@ -142,7 +143,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: After the statement is asserted, Coq needs a proof. Once a proof of :n:`@type` under the assumptions represented by :n:`@binder`\s is given and validated, the proof is generalized into a proof of :n:`forall {* @binder }, @type` and - the theorem is bound to the name :n:`@ident` in the environment. + the theorem is bound to the name :n:`@ident` in the global environment. These commands accept the :attr:`program` attribute. See :ref:`program_lemma`. @@ -159,7 +160,7 @@ Chapter :ref:`Tactics`. The basic assertion command is: have to be used on *structurally smaller* arguments (for a :cmd:`Fixpoint`) or be *guarded by a constructor* (for a :cmd:`CoFixpoint`). The verification that recursive proof arguments are correct is done only at the time of registering - the lemma in the environment. To know if the use of induction hypotheses is + the lemma in the global environment. To know if the use of induction hypotheses is correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. @@ -178,25 +179,24 @@ Chapter :ref:`Tactics`. The basic assertion command is: .. exn:: Nested proofs are discouraged and not allowed by default. This error probably means that you forgot to close the last "Proof." with "Qed." or "Defined.". \ If you really intended to use nested proofs, you can do so by turning the "Nested Proofs Allowed" flag on. - You are asserting a new statement while already being in proof editing mode. + You are asserting a new statement when you're already in proof mode. This feature, called nested proofs, is disabled by default. To activate it, turn the :flag:`Nested Proofs Allowed` flag on. -Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof editing mode -until the proof is completed. In proof editing mode, the user primarily enters -tactics, which are described in chapter :ref:`Tactics`. The user may also enter -commands to manage the proof editing mode. They are described in Chapter -:ref:`proofhandling`. +Proofs start with the keyword :cmd:`Proof`. Then Coq enters the proof mode +until the proof is completed. In proof mode, the user primarily enters +tactics (see :ref:`writing-proofs`). The user may also enter +commands to manage the proof mode (see :ref:`proofhandling`). When the proof is complete, use the :cmd:`Qed` command so the kernel verifies -the proof and adds it to the environment. +the proof and adds it to the global environment. .. note:: #. Several statements can be simultaneously asserted provided the :flag:`Nested Proofs Allowed` flag was turned on. - #. Not only other assertions but any vernacular command can be given + #. Not only other assertions but any command can be given while in the process of proving a given assertion. In this case, the command is understood as if it would have been given before the statements still to be proved. Nonetheless, this practice is discouraged @@ -211,4 +211,4 @@ the proof and adds it to the environment. side, :cmd:`Qed` (or :cmd:`Defined`) is mandatory to validate a proof. #. One can also use :cmd:`Admitted` in place of :cmd:`Qed` to turn the - current asserted statement into an axiom and exit the proof editing mode. + current asserted statement into an axiom and exit proof mode. diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index 4bee7cc1b1..4e892f709d 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -36,7 +36,7 @@ Inductive types :attr:`private(matching)` attributes. Mutually inductive types can be defined by including multiple :n:`@inductive_definition`\s. - The :n:`@ident`\s are simultaneously added to the environment before the types of constructors are checked. + The :n:`@ident`\s are simultaneously added to the global environment before the types of constructors are checked. Each :n:`@ident` can be used independently thereafter. See :ref:`mutually_inductive_types`. @@ -86,7 +86,7 @@ A simple inductive type belongs to a universe that is a simple :n:`@sort`. The type nat is defined as the least :g:`Set` containing :g:`O` and closed by the :g:`S` constructor. The names :g:`nat`, :g:`O` and :g:`S` are added to the - environment. + global environment. This definition generates four elimination principles: :g:`nat_rect`, :g:`nat_ind`, :g:`nat_rec` and :g:`nat_sind`. The type of :g:`nat_ind` is: @@ -413,7 +413,7 @@ constructions. It is especially useful when defining functions over mutually defined inductive types. Example: :ref:`Mutual Fixpoints<example_mutual_fixpoints>`. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -636,7 +636,7 @@ contains an inductive definition. .. example:: - Provided that our environment :math:`E` contains inductive definitions we showed before, + Provided that our global environment :math:`E` contains inductive definitions we showed before, these two inference rules above enable us to conclude that: .. math:: diff --git a/doc/sphinx/language/core/modules.rst b/doc/sphinx/language/core/modules.rst index 6d96e15202..93d70c773f 100644 --- a/doc/sphinx/language/core/modules.rst +++ b/doc/sphinx/language/core/modules.rst @@ -283,7 +283,6 @@ are now available through the dot notation. Check A.B.U. .. cmd:: Export {+ @filtered_import } - :name: Export Similar to :cmd:`Import`, except that when the module containing this command is imported, the :n:`{+ @qualid }` are imported as well. @@ -465,7 +464,7 @@ We also need additional typing judgments: + :math:`\WFT{E}{S}`, denoting that a structure :math:`S` is well-formed, + :math:`\WTM{E}{p}{S}`, denoting that the module pointed by :math:`p` has type :math:`S` in - environment :math:`E`. + the global environment :math:`E`. + :math:`\WEV{E}{S}{\ovl{S}}`, denoting that a structure :math:`S` is evaluated to a structure :math:`S` in weak head normal form. + :math:`\WS{E}{S_1}{S_2}` , denoting that a structure :math:`S_1` is a subtype of a @@ -965,7 +964,7 @@ names. A logical prefix Lib can be associated with a physical path using the command line option ``-Q`` `path` ``Lib``. All subfolders of path are -recursively associated to the logical path ``Lib`` extended with the +recursively associated with the logical path ``Lib`` extended with the corresponding suffix coming from the physical path. For instance, the folder ``path/fOO/Bar`` maps to ``Lib.fOO.Bar``. Subdirectories corresponding to invalid Coq identifiers are skipped, and, by convention, @@ -973,7 +972,7 @@ subdirectories named ``CVS`` or ``_darcs`` are skipped too. Thanks to this mechanism, ``.vo`` files are made available through the logical name of the folder they are in, extended with their own -basename. For example, the name associated to the file +basename. For example, the name associated with the file ``path/fOO/Bar/File.vo`` is ``Lib.fOO.Bar.File``. The same caveat applies for invalid identifiers. When compiling a source file, the ``.vo`` file stores its logical name, so that an error is issued if it is loaded with the diff --git a/doc/sphinx/language/core/records.rst b/doc/sphinx/language/core/records.rst index 7eedbcd59a..6671c67fb2 100644 --- a/doc/sphinx/language/core/records.rst +++ b/doc/sphinx/language/core/records.rst @@ -119,13 +119,11 @@ The following settings let you control the display format for types: You can override the display format for specified types by adding entries to these tables: .. table:: Printing Record @qualid - :name: Printing Record Specifies a set of qualids which are displayed as records. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. .. table:: Printing Constructor @qualid - :name: Printing Constructor Specifies a set of qualids which are displayed as constructors. Use the :cmd:`Add` and :cmd:`Remove` commands to update the set of qualids. @@ -208,7 +206,7 @@ other arguments are the parameters of the inductive type. This message is followed by an explanation of this impossibility. There may be three reasons: - #. The name :token:`ident` already exists in the environment (see :cmd:`Axiom`). + #. The name :token:`ident` already exists in the global environment (see :cmd:`Axiom`). #. The body of :token:`ident` uses an incorrect elimination for :token:`ident` (see :cmd:`Fixpoint` and :ref:`Destructors`). #. The type of the projections :token:`ident` depends on previous diff --git a/doc/sphinx/language/core/sections.rst b/doc/sphinx/language/core/sections.rst index 75389bb259..c16152ff4f 100644 --- a/doc/sphinx/language/core/sections.rst +++ b/doc/sphinx/language/core/sections.rst @@ -3,57 +3,33 @@ Section mechanism ----------------- -Sections create local contexts which can be shared across multiple definitions. - -.. example:: - - Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. - - .. coqtop:: all - - Section s1. - - Inside a section, local parameters can be introduced using :cmd:`Variable`, - :cmd:`Hypothesis`, or :cmd:`Context` (there are also plural variants for - the first two). - - .. coqtop:: all - - Variables x y : nat. - - The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions - won't persist when the section is closed, and all persistent definitions which - depend on `y'` will be prefixed with `let y' := y in`. - - .. coqtop:: in - - Let y' := y. - Definition x' := S x. - Definition x'' := x' + y'. - - .. coqtop:: all - - Print x'. - Print x''. - - End s1. - - Print x'. - Print x''. - - Notice the difference between the value of :g:`x'` and :g:`x''` inside section - :g:`s1` and outside. +Sections are naming scopes that permit creating section-local declarations that can +be used by other declarations in the section. Declarations made +with :cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Context`, +:cmd:`Let`, :cmd:`Let Fixpoint` and +:cmd:`Let CoFixpoint` (or the plural variants of the first two) within sections +are local to the section. + +In proofs done within the section, section-local declarations +are included in the :term:`local context` of the initial goal of the proof. +They are also accessible in definitions made with the :cmd:`Definition` command. + +Sections are opened by the :cmd:`Section` command, and closed by :cmd:`End`. +Sections can be nested. +When a section is closed, its local declarations are no longer available. +Global declarations that refer to them will be adjusted so they're still +usable outside the section as shown in this :ref:`example <section_local_declarations>`. .. cmd:: Section @ident - This command is used to open a section named :token:`ident`. + Opens the section named :token:`ident`. Section names do not need to be unique. .. cmd:: End @ident - This command closes the section or module named :token:`ident`. - See :ref:`Terminating an interactive module or module type definition<terminating_module>` + Closes the section or module named :token:`ident`. + See :ref:`Terminating an interactive module or module type definition <terminating_module>` for a description of its use with modules. After closing the @@ -78,14 +54,14 @@ Sections create local contexts which can be shared across multiple definitions. Let CoFixpoint @cofix_definition {* with @cofix_definition } :name: Let; Let Fixpoint; Let CoFixpoint - These commands behave like :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that + These are similar to :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, except that the declared constant is local to the current section. When the section is closed, all persistent definitions and theorems within it that depend on the constant will be wrapped with a :n:`@term_let` with the same declaration. As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, - if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. @@ -103,3 +79,38 @@ Sections create local contexts which can be shared across multiple definitions. Context (b' := b). .. seealso:: Section :ref:`binders`. Section :ref:`contexts` in chapter :ref:`typeclasses`. + +.. _section_local_declarations: + +.. example:: Section-local declarations + + .. coqtop:: all + + Section s1. + + .. coqtop:: all + + Variables x y : nat. + + The command :cmd:`Let` introduces section-wide :ref:`let-in`. These definitions + won't persist when the section is closed, and all persistent definitions which + depend on `y'` will be prefixed with `let y' := y in`. + + .. coqtop:: in + + Let y' := y. + Definition x' := S x. + Definition x'' := x' + y'. + + .. coqtop:: all + + Print x'. + Print x''. + + End s1. + + Print x'. + Print x''. + + Notice the difference between the value of :g:`x'` and :g:`x''` inside section + :g:`s1` and outside. diff --git a/doc/sphinx/language/extensions/arguments-command.rst b/doc/sphinx/language/extensions/arguments-command.rst index d178311b4c..214541570c 100644 --- a/doc/sphinx/language/extensions/arguments-command.rst +++ b/doc/sphinx/language/extensions/arguments-command.rst @@ -4,7 +4,6 @@ Setting properties of a function's arguments ++++++++++++++++++++++++++++++++++++++++++++ .. cmd:: Arguments @reference {* @arg_specs } {* , {* @implicits_alt } } {? : {+, @args_modifier } } - :name: Arguments .. insertprodn argument_spec args_modifier diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst index aa754ab63d..4cc35794cc 100644 --- a/doc/sphinx/language/extensions/canonical.rst +++ b/doc/sphinx/language/extensions/canonical.rst @@ -199,8 +199,8 @@ but also that the infix relation was bound to the ``nat_eq`` relation. This relation is selected whenever ``==`` is used on terms of type nat. This can be read in the line declaring the canonical structure ``nat_EQty``, where the first argument to ``Pack`` is the key and its second -argument a group of canonical values associated to the key. In this -case we associate to nat only one canonical value (since its class, +argument a group of canonical values associated with the key. In this +case we associate with nat only one canonical value (since its class, ``nat_EQcl`` has just one member). The use of the projection ``op`` requires its argument to be in the class ``EQ``, and uses such a member (function) to actually compare its arguments. @@ -530,7 +530,7 @@ instances of the ``LEQ`` class. The object ``Pack`` takes a type ``T`` (the key) and a mixin ``m``. It infers all the other pieces of the class ``LEQ`` and declares them as canonical -values associated to the ``T`` key. All in all, the only new piece of +values associated with the ``T`` key. All in all, the only new piece of information we add in the ``LEQ`` class is the mixin, all the rest is already canonical for ``T`` and hence can be inferred by Coq. diff --git a/doc/sphinx/language/extensions/evars.rst b/doc/sphinx/language/extensions/evars.rst index fd9695e270..7206fb8581 100644 --- a/doc/sphinx/language/extensions/evars.rst +++ b/doc/sphinx/language/extensions/evars.rst @@ -5,6 +5,9 @@ Existential variables --------------------- +:gdef:`Existential variables <existential variable>` represent as yet unknown +values. + .. insertprodn term_evar term_evar .. prodn:: diff --git a/doc/sphinx/language/extensions/implicit-arguments.rst b/doc/sphinx/language/extensions/implicit-arguments.rst index 23ba5f703a..765d04ec88 100644 --- a/doc/sphinx/language/extensions/implicit-arguments.rst +++ b/doc/sphinx/language/extensions/implicit-arguments.rst @@ -66,7 +66,7 @@ would be a solution of the inference problem. **Contextual Implicit Arguments** An implicit argument can be *contextual* or not. An implicit argument -is said *contextual* if it can be inferred only from the knowledge of +is said to be *contextual* if it can be inferred only from the knowledge of the type of the context of the current expression. For instance, the only argument of:: @@ -384,7 +384,7 @@ Displaying implicit arguments when pretty-printing .. flag:: Printing Implicit - By default, the basic pretty-printing rules hide the inferrable implicit + By default, the basic pretty-printing rules hide the inferable implicit arguments of an application. Turn this flag on to force printing all implicit arguments. @@ -506,7 +506,7 @@ or :g:`m` to the type :g:`nat` of natural numbers). .. flag:: Printing Use Implicit Types By default, the type of bound variables is not printed when - the variable name is associated to an implicit type which matches the + the variable name is associated with an implicit type which matches the actual type of the variable. This feature can be deactivated by turning this flag off. diff --git a/doc/sphinx/language/extensions/match.rst b/doc/sphinx/language/extensions/match.rst index 8e62c2af13..1c022448b0 100644 --- a/doc/sphinx/language/extensions/match.rst +++ b/doc/sphinx/language/extensions/match.rst @@ -252,7 +252,6 @@ If an inductive type has just one constructor, pattern matching can be written using the first destructuring let syntax. .. table:: Printing Let @qualid - :name: Printing Let Specifies a set of qualids for which pattern matching is displayed using a let expression. Note that this only applies to pattern matching instances entered with :g:`match`. @@ -269,7 +268,6 @@ can be written using ``if`` … ``then`` … ``else`` …. This table controls which types are written this way: .. table:: Printing If @qualid - :name: Printing If Specifies a set of qualids for which pattern matching is displayed using ``if`` … ``then`` … ``else`` …. Use the :cmd:`Add` and :cmd:`Remove` @@ -720,7 +718,7 @@ Recall that a list of patterns is also a pattern. So, when we destructure several terms at the same time and the branches have different types we need to provide the elimination predicate for this multiple pattern. It is done using the same scheme: each term may be -associated to an ``as`` clause and an ``in`` clause in order to introduce +associated with an ``as`` clause and an ``in`` clause in order to introduce a dependent product. For example, an equivalent definition for :g:`concat` (even though the diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index d20a82e6c0..7ad2605f4a 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -43,7 +43,7 @@ Batch compilation (coqc) ------------------------ The ``coqc`` command takes a name *file* as argument. Then it looks for a -vernacular file named *file*.v, and tries to compile it into a +file named *file*.v, and tries to compile it into a *file*.vo file (See :ref:`compiled-files`). .. caution:: @@ -434,7 +434,7 @@ wrong. In the current version, it does not modify the compiled libraries to mark them as successfully checked. Note that non-logical information is not checked. By logical -information, we mean the type and optional body associated to names. +information, we mean the type and optional body associated with names. It excludes for instance anything related to the concrete syntax of objects (customized syntax rules, association between short and long names), implicit arguments, etc. diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index c239797cc2..dcc60195ed 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -7,7 +7,7 @@ Coq Integrated Development Environment The Coq Integrated Development Environment is a graphical tool, to be used as a user-friendly replacement to `coqtop`. Its main purpose is to -allow the user to navigate forward and backward into a Coq vernacular +allow the user to navigate forward and backward into a Coq file, executing corresponding commands or undoing them respectively. CoqIDE is run by typing the command `coqide` on the command line. @@ -100,10 +100,10 @@ processed color, though their preceding proofs have the processed color. Notice that for all these buttons, except for the "gears" button, their operations are also available in the menu, where their keyboard shortcuts are given. -Vernacular commands, templates ------------------------------------ +Commands and templates +---------------------- -The Templates menu allows using shortcuts to insert vernacular +The Templates menu allows using shortcuts to insert commands. This is a nice way to proceed if you are not sure of the syntax of the command you want. @@ -116,7 +116,7 @@ Queries .. image:: ../_static/coqide-queries.png :alt: CoqIDE queries -We call *query* any vernacular command that does not change the current state, +We call *query* any command that does not change the current state, such as ``Check``, ``Search``, etc. To run such commands interactively, without writing them in scripts, CoqIDE offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 87a367fc93..8b627c29a4 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -284,6 +284,8 @@ A sequence is an expression of the following form: .. tacn:: @ltac_expr3__1 ; {| @ltac_expr3__2 | @binder_tactic } :name: ltac-seq + .. todo: can't use "… ; …" as the name because of the semicolon + The expression :n:`@ltac_expr3__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goals, possibly producing more goals. Then the right-hand side is evaluated to @@ -481,7 +483,6 @@ Do loop ~~~~~~~ .. tacn:: do @nat_or_var @ltac_expr3 - :name: do The do loop repeats a tactic :token:`nat_or_var` times: @@ -497,7 +498,6 @@ Repeat loop ~~~~~~~~~~~ .. tacn:: repeat @ltac_expr3 - :name: repeat The repeat loop repeats a tactic until it fails. @@ -515,7 +515,6 @@ Catching errors: try We can catch the tactic errors with: .. tacn:: try @ltac_expr3 - :name: try :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused goal independently. If the application of @@ -531,7 +530,6 @@ Detecting progress We can check if a tactic made progress with: .. tacn:: progress @ltac_expr3 - :name: progress :n:`@ltac_expr` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied to each focused subgoal independently. If the application of ``v`` @@ -641,7 +639,6 @@ First tactic to succeed In some cases backtracking may be too expensive. .. tacn:: first [ {*| @ltac_expr } ] - :name: first For each focused goal, independently apply the first :token:`ltac_expr` that succeeds. The :n:`@ltac_expr`\s must evaluate to tactic values. @@ -701,7 +698,6 @@ Selects and applies the first tactic that solves each goal (i.e. leaves no subgo in a series of alternative tactics: .. tacn:: solve [ {*| @ltac_expr__i } ] - :name: solve For each current subgoal: evaluates and applies each :n:`@ltac_expr` in order until one is found that solves the subgoal. @@ -743,7 +739,6 @@ Conditional branching: tryif ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: tryif @ltac_expr__test then @ltac_expr__then else @ltac_expr2__else - :name: tryif For each focused goal, independently: Evaluate and apply :n:`@ltac_expr__test`. If :n:`@ltac_expr__test` succeeds at least once, evaluate and apply :n:`@ltac_expr__then` @@ -772,7 +767,6 @@ Another way of restricting backtracking is to restrict a tactic to a single success: .. tacn:: once @ltac_expr3 - :name: once :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied but only its first success is used. If ``v`` fails, @@ -788,7 +782,6 @@ Coq provides an experimental way to check that a tactic has *exactly one* success: .. tacn:: exactly_once @ltac_expr3 - :name: exactly_once :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied if it has at most one success. If ``v`` fails, @@ -816,7 +809,6 @@ Checking for failure: assert_fails Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic *fails*: .. tacn:: assert_fails @ltac_expr3 - :name: assert_fails If :n:`@ltac_expr3` fails, the proof state is unchanged and no message is printed. If :n:`@ltac_expr3` unexpectedly has at least one success, the tactic performs @@ -863,7 +855,6 @@ Coq defines an |Ltac| tactic in `Init.Tactics` to check that a tactic has *at le success: .. tacn:: assert_succeeds @ltac_expr3 - :name: assert_succeeds If :n:`@ltac_expr3` has at least one success, the proof state is unchanged and no message is printed. If :n:`@ltac_expr3` fails, the tactic performs @@ -877,7 +868,6 @@ Print/identity tactic: idtac .. tacn:: idtac {* {| @ident | @string | @natural } } - :name: idtac Leaves the proof unchanged and prints the given tokens. :token:`String<string>`\s and :token:`natural`\s are printed @@ -974,7 +964,6 @@ We can force a tactic to stop if it has not finished after a certain amount of time: .. tacn:: timeout @nat_or_var @ltac_expr3 - :name: timeout :n:`@ltac_expr3` is evaluated to ``v`` which must be a tactic value. The tactic value ``v`` is applied normally, except that it is interrupted after :n:`@nat_or_var` seconds @@ -998,7 +987,6 @@ Timing a tactic A tactic execution can be timed: .. tacn:: time {? @string } @ltac_expr3 - :name: time evaluates :n:`@ltac_expr3` and displays the running time of the tactic expression, whether it fails or succeeds. In case of several successes, the time for each successive @@ -1015,7 +1003,6 @@ Tactic expressions that produce terms can be timed with the experimental tactic .. tacn:: time_constr @ltac_expr - :name: time_constr which evaluates :n:`@ltac_expr ()` and displays the time the tactic expression evaluated, assuming successful evaluation. Time is in seconds and is @@ -1026,12 +1013,10 @@ tactic implemented using the following internal tactics: .. tacn:: restart_timer {? @string } - :name: restart_timer Reset a timer .. tacn:: finish_timing {? ( @string ) } {? @string } - :name: finish_timing Display an optionally named timer. The parenthesized string argument is also optional, and determines the label associated with the timer @@ -1362,7 +1347,7 @@ Pattern matching on goals and hypotheses: match goal :tacn:`lazymatch goal`, :tacn:`match goal` and :tacn:`multimatch goal` are :token:`l1_tactic`\s. - Use this form to match hypotheses and/or goals in the proof context. These patterns have zero or + Use this form to match hypotheses and/or goals in the local context. These patterns have zero or more subpatterns to match hypotheses followed by a subpattern to match the conclusion. Except for the differences noted below, this works the same as the corresponding :n:`@match_key @ltac_expr` construct (see :tacn:`match`). Each current goal is processed independently. @@ -1533,7 +1518,7 @@ expression returns an identifier: .. todo you can't have a :tacn: with the same name as a :gdef: for now, eg `fresh` can't be both - Returns a fresh identifier name (i.e. one that is not already used in the context + Returns a fresh identifier name (i.e. one that is not already used in the local context and not previously returned by :tacn:`fresh` in the current :token:`ltac_expr`). The fresh identifier is formed by concatenating the final :token:`ident` of each :token:`qualid` (dropping any qualified components) and each specified :token:`string`. @@ -1541,11 +1526,11 @@ expression returns an identifier: If no arguments are given, the name is a fresh derivative of the name ``H``. .. note:: We recommend generating the fresh identifier immediately before - adding it in the proof context. Using :tacn:`fresh` in a local function + adding it to the local context. Using :tacn:`fresh` in a local function may not work as you expect: - Successive :tacn:`fresh`\es give distinct names even if the names haven't - yet been added to the proof context: + Successive calls to :tacn:`fresh` give distinct names even if the names haven't + yet been added to the local context: .. coqtop:: reset none @@ -1635,7 +1620,6 @@ Testing boolean expressions: guard ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: guard @int_or_var @comparison @int_or_var - :name: guard .. insertprodn int_or_var comparison @@ -1734,7 +1718,6 @@ Defining |Ltac| symbols .. index:: ::= .. cmd:: Ltac @tacdef_body {* with @tacdef_body } - :name: Ltac .. insertprodn tacdef_body tacdef_body @@ -2248,7 +2231,6 @@ Tracing execution not printed. .. opt:: Info Level @natural - :name: Info Level This option is an alternative to the :cmd:`Info` command. @@ -2269,17 +2251,17 @@ The debugger stops, prompting for a command which can be one of the following: +-----------------+-----------------------------------------------+ -| simple newline: | go to the next step | +| newline | go to the next step | +-----------------+-----------------------------------------------+ -| h: | get help | +| h | get help | +-----------------+-----------------------------------------------+ -| x: | exit current evaluation | +| r n | advance n steps further | +-----------------+-----------------------------------------------+ -| s: | continue current evaluation without stopping | +| r string | advance up to the next call to “idtac string” | +-----------------+-----------------------------------------------+ -| r n: | advance n steps further | +| s | continue current evaluation without stopping | +-----------------+-----------------------------------------------+ -| r string: | advance up to the next call to “idtac string” | +| x | exit current evaluation | +-----------------+-----------------------------------------------+ .. exn:: Debug mode not available in the IDE @@ -2366,25 +2348,21 @@ performance issue. Unset Ltac Profiling. .. tacn:: start ltac profiling - :name: start ltac profiling This tactic behaves like :tacn:`idtac` but enables the profiler. .. tacn:: stop ltac profiling - :name: stop ltac profiling Similarly to :tacn:`start ltac profiling`, this tactic behaves like :tacn:`idtac`. Together, they allow you to exclude parts of a proof script from profiling. .. tacn:: reset ltac profile - :name: reset ltac profile Equivalent to the :cmd:`Reset Ltac Profile` command, which allows resetting the profile from tactic scripts for benchmarking purposes. .. tacn:: show ltac profile {? {| cutoff @integer | @string } } - :name: show ltac profile Equivalent to the :cmd:`Show Ltac Profile` command, which allows displaying the profile from tactic scripts for @@ -2410,11 +2388,10 @@ Run-time optimization tactic ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. tacn:: optimize_heap - :name: optimize_heap This tactic behaves like :tacn:`idtac`, except that running it compacts the - heap in the OCaml run-time system. It is analogous to the Vernacular - command :cmd:`Optimize Heap`. + heap in the OCaml run-time system. It is analogous to the + :cmd:`Optimize Heap` command. .. tacn:: infoH @ltac_expr3 diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 375129c02d..3646a32a79 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -173,7 +173,6 @@ Type declarations One can define new types with the following commands. .. cmd:: Ltac2 Type {? rec } @tac2typ_def {* with @tac2typ_def } - :name: Ltac2 Type .. insertprodn tac2typ_def tac2rec_field @@ -301,7 +300,6 @@ Ltac2 Definitions ~~~~~~~~~~~~~~~~~ .. cmd:: Ltac2 {? mutable } {? rec } @tac2def_body {* with @tac2def_body } - :name: Ltac2 .. insertprodn tac2def_body tac2def_body @@ -322,7 +320,6 @@ Ltac2 Definitions If ``mutable`` is set, the definition can be redefined at a later stage (see below). .. cmd:: Ltac2 Set @qualid {? as @ident } := @ltac2_expr - :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined @@ -598,7 +595,7 @@ modes, the *strict* and the *non-strict* mode. hypotheses. If this doesn't hold, internalization will fail. To work around this error, one has to specifically use the ``&`` notation. - In non-strict mode, any simple identifier appearing in a term quotation which - is not bound in the global context is turned into a dynamic reference to a + is not bound in the global environment is turned into a dynamic reference to a hypothesis. That is to say, internalization will succeed, but the evaluation of the term at runtime will fail if there is no such variable in the dynamic context. @@ -982,7 +979,7 @@ Match over goals gmatch_hyp_pattern ::= @name : @ltac2_match_pattern Matches over goals, similar to Ltac1 :tacn:`match goal`. - Use this form to match hypotheses and/or goals in the proof context. These patterns have zero or + Use this form to match hypotheses and/or goals in the local context. These patterns have zero or more subpatterns to match hypotheses followed by a subpattern to match the conclusion. Except for the differences noted below, this works the same as the corresponding :n:`@ltac2_match_key @ltac2_expr` construct (see :tacn:`match!`). Each current goal is processed independently. @@ -1164,7 +1161,6 @@ Notations --------- .. cmd:: Ltac2 Notation {+ @ltac2_scope } {? : @natural } := @ltac2_expr - :name: Ltac2 Notation .. todo seems like name maybe should use lident rather than ident, considering: @@ -1487,7 +1483,7 @@ Other nonterminals that have syntactic classes are listed here. * - :n:`conversion` - :token:`ltac2_conversion` - - :token:`conversion` + - * - :n:`rewriting` - :token:`ltac2_oriented_rewriter` @@ -1679,7 +1675,6 @@ Evaluation Ltac2 features a toplevel loop that can be used to evaluate expressions. .. cmd:: Ltac2 Eval @ltac2_expr - :name: Ltac2 Eval This command evaluates the term in the current proof if there is one, or in the global environment otherwise, and displays the resulting value to the user @@ -1877,9 +1872,9 @@ In Ltac expressions .. exn:: Unbound {| value | constructor } X - * if `X` is meant to be a term from the current stactic environment, replace + * if `X` is meant to be a term from the current static environment, replace the problematic use by `'X`. - * if `X` is meant to be a hypothesis from the goal context, replace the + * if `X` is meant to be a hypothesis from the local context, replace the problematic use by `&X`. In quotations @@ -1889,7 +1884,7 @@ In quotations * if `X` is meant to be a tactic expression bound by a Ltac2 let or function, replace the problematic use by `$X`. - * if `X` is meant to be a hypothesis from the goal context, replace the + * if `X` is meant to be a hypothesis from the local context, replace the problematic use by `&X`. Exception catching diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 07c2d268c6..bab9d35099 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -116,8 +116,8 @@ compatible with the rest of Coq, up to a few discrepancies: + New keywords (``is``) might clash with variable, constant, tactic or - tactical names, or with quasi-keywords in tactic or vernacular - notations. + tactical names, or with quasi-keywords in tactic or + notation commands. + New tactic(al)s names (:tacn:`last`, :tacn:`done`, :tacn:`have`, :tacn:`suffices`, :tacn:`suff`, :tacn:`without loss`, :tacn:`wlog`, :tacn:`congr`, :tacn:`unlock`) might clash with user tactic names. @@ -799,8 +799,9 @@ An *occurrence switch* can be: set x := {+1 3}(f 2). Notice that some occurrences of a given term may be - hidden to the user, for example because of a notation. The vernacular - ``Set Printing All`` command displays all these hidden occurrences and + hidden to the user, for example because of a notation. Setting the + :flag:`Printing All` flag causes these hidden occurrences to + be shown when the term is displayed. This setting should be used to find the correct coding of the occurrences to be selected [#1]_. @@ -1023,7 +1024,7 @@ conversely in between deductive steps. In |SSR| these moves are performed by two *tacticals* ``=>`` and ``:``, so that the bookkeeping required by a deductive step can be -directly associated to that step, and that tactics in an |SSR| +directly associated with that step, and that tactics in an |SSR| script correspond to actual logical steps in the proof rather than merely shuffle facts. Still, some isolated bookkeeping is unavoidable, such as naming variables and assumptions at the beginning of a @@ -1189,7 +1190,7 @@ The move tactic. ```````````````` .. tacn:: move - :name: move + :name: move (ssreflect) This tactic, in its defective form, behaves like the :tacn:`hnf` tactic. @@ -5502,7 +5503,7 @@ equivalences are indeed taken into account, otherwise only single string that contains symbols or is followed by a scope key, is interpreted as the constant whose notation involves that string (e.g., :g:`+` for :g:`addn`), if this is unambiguous; otherwise the diagnostic - includes the output of the :cmd:`Locate` vernacular command. + includes the output of the :cmd:`Locate` command. + whose statement, including assumptions and types, contains a subterm matching the next patterns. If a pattern is prefixed by ``-``, the test is reversed; diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index d8c4fb61c2..a750ce2892 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3,35 +3,46 @@ Tactics ======== -A deduction rule is a link between some (unique) formula, that we call -the *conclusion* and (several) formulas that we call the *premises*. A -deduction rule can be read in two ways. The first one says: “if I know -this and this then I can deduce this”. For instance, if I have a proof -of A and a proof of B then I have a proof of A ∧ B. This is forward -reasoning from premises to conclusion. The other way says: “to prove -this I have to prove this and this”. For instance, to prove A ∧ B, I -have to prove A and I have to prove B. This is backward reasoning from -conclusion to premises. We say that the conclusion is the *goal* to -prove and premises are the *subgoals*. The tactics implement *backward -reasoning*. When applied to a goal, a tactic replaces this goal with -the subgoals it generates. We say that a tactic reduces a goal to its -subgoal(s). - -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:`requestinginformation`). - -Since not every rule applies to a given statement, not every tactic can -be used to reduce a given goal. In other words, before applying a tactic -to a given goal, the system checks that some *preconditions* are -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:`ltac`. +Tactics specify how to transform the :term:`proof state` of an +incomplete proof to eventually generate a complete proof. + +Proofs can be developed in two basic ways: In :gdef:`forward reasoning`, +the proof begins by proving simple statements that are then combined to prove the +theorem statement as the last step of the proof. With forward reasoning, +for example, +the proof of `A /\\ B` would begin with proofs of `A` and `B`, which are +then used to prove `A /\\ B`. Forward reasoning is probably the most common +approach in human-generated proofs. + +In :gdef:`backward reasoning`, the proof begins with the theorem statement +as the goal, which is then gradually transformed until every subgoal generated +along the way has been proven. In this case, the proof of `A /\\ B` begins +with that formula as the goal. This can be transformed into two subgoals, +`A` and `B`, followed by the proofs of `A` and `B`. Coq and its tactics +use backward reasoning. + +A tactic may fully prove a goal, in which case the goal is removed +from the proof state. +More commonly, a tactic replaces a goal with one or more :term:`subgoals <subgoal>`. +(We say that a tactic reduces a goal to its subgoals.) + +Most tactics require specific elements or preconditions to reduce a goal; +they display error messages if they can't be applied to the goal. +A few tactics, such as :tacn:`auto`, don't fail even if the proof state +is unchanged. + +Goals are identified by number. The current goal is number +1. Tactics are applied to the current goal by default. (The +default can be changed with the :opt:`Default Goal Selector` +option.) They can +be applied to another goal or to multiple goals with a +:ref:`goal selector <goal-selectors>` such as :n:`2: @tactic`. + +This chapter describes many of the most common built-in tactics. +Built-in tactics can be combined to form tactic expressions, which are +described in the :ref:`Ltac` chapter. Since tactic expressions can +be used anywhere that a built-in tactic can be used, "tactic" may +refer to both built-in tactics and tactic expressions. Common elements of tactics -------------------------- @@ -529,8 +540,21 @@ one or more of its hypotheses. which is equivalent to `in * |- *`. Use `* |-` to select all occurrences in all hypotheses. -Tactics that use occurrence clauses include :tacn:`set`, -:tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. + Tactics that select a specific hypothesis H to apply to other hypotheses, + such as :tacn:`rewrite` `H in * |-`, won't apply H to itself. + + If multiple + occurrences are given, such as in :tacn:`rewrite` `H at 1 2 3`, the tactic + must match at least one occurrence in order to succeed. The tactic will fail + if no occurrences match. Occurrence numbers that are out of range (e.g. + `at 1 3` when there are only 2 occurrences in the hypothesis or conclusion) + are ignored. + + .. todo: remove last sentence above and add "Invalid occurrence number @natural" exn for 8.14 + per #13568. + + Tactics that use occurrence clauses include :tacn:`set`, + :tacn:`remember`, :tacn:`induction` and :tacn:`destruct`. .. seealso:: @@ -1979,7 +2003,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) This is a more basic induction tactic. Again, the type of the argument :n:`@term` must be an inductive type. Then, according to the type of the goal, the tactic ``elim`` chooses the appropriate destructor and applies it - as the tactic :tacn:`apply` would do. For instance, if the proof context + as the tactic :tacn:`apply` would do. For instance, if the local context contains :g:`n:nat` and the current goal is :g:`T` of type :g:`Prop`, then :n:`elim n` is equivalent to :n:`apply nat_ind with (n:=n)`. The tactic ``elim`` does not modify the context of the goal, neither introduces the @@ -2651,7 +2675,7 @@ and an explanation of the underlying technique. Like in a fix expression, the induction hypotheses have to be used on structurally smaller arguments. The verification that inductive proof arguments are correct is done only at the time of registering the - lemma in the environment. To know if the use of induction hypotheses + lemma in the global 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 Section :ref:`requestinginformation`). @@ -2671,7 +2695,7 @@ and an explanation of the underlying technique. name given to the coinduction hypothesis. Like in a cofix expression, the use of induction hypotheses have to guarded by a constructor. The verification that the use of co-inductive hypotheses is correct is - done only at the time of registering the lemma in the environment. To + done only at the time of registering the lemma in the global 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 Section :ref:`requestinginformation`). @@ -2752,14 +2776,11 @@ succeeds, and results in an error otherwise. :name: is_var This tactic checks whether its argument is a variable or hypothesis in - the current goal context or in the opened sections. + the current local context. .. exn:: Not a variable or hypothesis. :undocumented: - -.. _equality: - Equality -------- @@ -2954,59 +2975,7 @@ references to automatically generated names. Performance-oriented tactic variants ------------------------------------ -.. tacn:: change_no_check @term - :name: change_no_check - - For advanced usage. Similar to :tacn:`change` :n:`@term`, but as an optimization, - it skips checking that :n:`@term` is convertible to the goal. - - Recall that the Coq kernel typechecks proofs again when they are concluded to - ensure safety. Hence, using :tacn:`change` checks convertibility twice - overall, while :tacn:`change_no_check` can produce ill-typed terms, - but checks convertibility only once. - Hence, :tacn:`change_no_check` can be useful to speed up certain proof - scripts, especially if one knows by construction that the argument is - indeed convertible to the goal. - - In the following example, :tacn:`change_no_check` replaces :g:`False` by - :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency. - - .. example:: - - .. coqtop:: all abort - - Goal False. - change_no_check True. - exact I. - Fail Qed. - - :tacn:`change_no_check` supports all of :tacn:`change`'s variants. - - .. tacv:: change_no_check @term with @term’ - :undocumented: - - .. tacv:: change_no_check @term at {+ @natural} with @term’ - :undocumented: - - .. tacv:: change_no_check @term {? {? at {+ @natural}} with @term} in @ident - - .. example:: - - .. coqtop:: all abort - - Goal True -> False. - intro H. - change_no_check False in H. - exact H. - Fail Qed. - - .. tacv:: convert_concl_no_check @term - :name: convert_concl_no_check - - .. deprecated:: 8.11 - - Deprecated old name for :tacn:`change_no_check`. Does not support any of its - variants. +.. todo: move the following adjacent to the `exact` tactic in the rewriting chapter? .. tacn:: exact_no_check @term :name: exact_no_check diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index e866e4c624..8e2f577f6b 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1,7 +1,7 @@ .. _vernacularcommands: -Vernacular commands -============================= +Commands +======== .. _displaying: @@ -60,7 +60,7 @@ Query commands -------------- Unlike other commands, :production:`query_command`\s may be prefixed with -a goal selector (:n:`@natural:`) to specify which goal context it applies to. +a goal selector (:n:`@natural:`) to specify which goals it applies to. If no selector is provided, the command applies to the current goal. If no proof is open, then the command only applies to accessible objects. (see Section :ref:`invocation-of-tactics`). @@ -382,7 +382,6 @@ to accessible objects. (see Section :ref:`invocation-of-tactics`). SearchRewrite (_ + _ + _). .. table:: Search Blacklist @string - :name: Search Blacklist Specifies a set of strings used to exclude lemmas from the results of :cmd:`Search`, :cmd:`SearchHead`, :cmd:`SearchPattern` and :cmd:`SearchRewrite` queries. A lemma whose @@ -668,8 +667,8 @@ Loadpath ------------ Loadpaths are preferably managed using Coq command line options (see -Section :ref:`libraries-and-filesystem`) but there remain vernacular commands to manage them -for practical purposes. Such commands are only meant to be issued in +Section :ref:`libraries-and-filesystem`), but there are also commands +to manage them within Coq. These commands are only meant to be issued in the toplevel, and using them in source files is discouraged. @@ -740,7 +739,7 @@ Backtracking ------------ The backtracking commands described in this section can only be used -interactively, they cannot be part of a vernacular file loaded via +interactively, they cannot be part of a Coq file loaded via ``Load`` or compiled by ``coqc``. @@ -844,7 +843,6 @@ Quitting and debugging displayed. .. opt:: Default Timeout @natural - :name: Default Timeout If set, each :n:`@sentence` is treated as if it was prefixed with :cmd:`Timeout` :n:`@natural`, except for :cmd:`Timeout` commands themselves. If unset, @@ -883,7 +881,6 @@ Controlling display This flag controls the normal displaying. .. opt:: Warnings "{+, {? {| - | + } } @ident }" - :name: Warnings This option configures the display of warnings. It is experimental, and expects, between quotes, a comma-separated list of warning names or @@ -894,14 +891,12 @@ Controlling display right have higher priority, meaning that `A,-A` is equivalent to `-A`. .. opt:: Printing Width @natural - :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 @natural - :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 diff --git a/doc/sphinx/proofs/automatic-tactics/auto.rst b/doc/sphinx/proofs/automatic-tactics/auto.rst index 472df2bd91..d7228a3907 100644 --- a/doc/sphinx/proofs/automatic-tactics/auto.rst +++ b/doc/sphinx/proofs/automatic-tactics/auto.rst @@ -335,7 +335,7 @@ Creating Hints .. exn:: @qualid cannot be used as a hint The head symbol of the type of :n:`@qualid` is a bound variable - such that this tactic cannot be associated to a constant. + such that this tactic cannot be associated with a constant. .. cmd:: Hint Immediate {+ {| @qualid | @one_term } } {? : {+ @ident } } diff --git a/doc/sphinx/proofs/writing-proofs/proof-mode.rst b/doc/sphinx/proofs/writing-proofs/proof-mode.rst index 40d032543f..931ac905f6 100644 --- a/doc/sphinx/proofs/writing-proofs/proof-mode.rst +++ b/doc/sphinx/proofs/writing-proofs/proof-mode.rst @@ -1,74 +1,175 @@ .. _proofhandling: -------------------- - Proof handling -------------------- +---------- +Proof mode +---------- -In Coq’s proof editing mode all top-level commands documented in -Chapter :ref:`vernacularcommands` remain available and the user has access to specialized -commands dealing with proof development pragmas documented in this -section. They can also use some other specialized commands called -*tactics*. They are the very tools allowing the user to deal with -logical reasoning. They are documented in Chapter :ref:`tactics`. +:gdef:`Proof mode <proof mode>` is used to prove theorems. +Coq enters proof mode when you begin a proof, +such as with the :cmd:`Theorem` command. It exits proof mode when +you complete a proof, such as with the :cmd:`Qed` command. Tactics, +which are available only in proof mode, incrementally transform incomplete +proofs to eventually generate a complete proof. -Coq user interfaces usually have a way of marking whether the user has -switched to proof editing mode. For instance, in coqtop the prompt ``Coq <`` is changed into -:n:`@ident <` where :token:`ident` is the declared name of the theorem currently edited. +When you run Coq interactively, such as through CoqIDE, Proof General or +coqtop, Coq shows the current proof state (the incomplete proof) as you +enter tactics. This information isn't shown when you run Coq in batch +mode with `coqc`. -At each stage of a proof development, one has a list of goals to -prove. Initially, the list consists only in the theorem itself. After -having applied some tactics, the list of goals contains the subgoals -generated by the tactics. +Proof State +----------- -To each subgoal is associated a number of hypotheses called the *local context* -of the goal. Initially, the local context contains the local variables and -hypotheses of the current section (see Section :ref:`gallina-assumptions`) and -the local variables and hypotheses of the theorem statement. It is enriched by -the use of certain tactics (see e.g. :tacn:`intro`). +The :gdef:`proof state` consists of one or more unproven goals. +Each goal has a :gdef:`conclusion` (the statement that is to be proven) +and a :gdef:`local context`, which contains named :term:`hypotheses <hypothesis>` +(which are propositions), variables and local definitions that can be used in +proving the conclusion. The proof may also use *constants* from the :term:`global environment` +such as definitions and proven theorems. -When a proof is completed, the message ``Proof completed`` is displayed. -One can then register this proof as a defined constant in the -environment. Because there exists a correspondence between proofs and -terms of λ-calculus, known as the *Curry-Howard isomorphism* -:cite:`How80,Bar81,Gir89,H89`, Coq stores proofs as terms of |Cic|. Those -terms are called *proof terms*. +The term ":gdef:`goal`" may refer to an entire goal or to the conclusion +of a goal, depending on the context. +The conclusion appears below a line and the local context appears above the line. +The conclusion is a type. Each item in the local context begins with a name +and ends, after a colon, with an associated type. +Local definitions are shown in the form `n := 0 : nat`, for example, in which `nat` is the +type of `0`. -.. exn:: No focused proof. +The local context of a goal contains items specific to the goal as well +as section-local variables and hypotheses (see :ref:`gallina-assumptions`) defined +in the current :ref:`section <section-mechanism>`. The latter are included in the +initial proof state. +Items in the local context are ordered; an item can only refer to items that appear +before it. (A more mathematical description of the *local context* is +:ref:`here <Local-context>`.) - Coq raises this error message when one attempts to use a proof editing command - out of the proof editing mode. +The :gdef:`global environment` has definitions and proven theorems that are global in scope. +(A more mathematical description of the *global environment* is :ref:`here <Global-environment>`.) + +When you begin proving a theorem, the proof state shows +the statement of the theorem below the line and often nothing in the +local context: + +.. coqtop:: none + + Parameter P: nat -> Prop. + +.. coqtop:: out + + Goal forall n m: nat, n > m -> P 1 /\ P 2. + +After applying the :tacn:`intros` :term:`tactic`, we see hypotheses above the line. +The names of variables (`n` and `m`) and hypotheses (`H`) appear before a colon, followed by +the type they represent. + +.. coqtop:: all + + intros. + +Some tactics, such as :tacn:`split`, create new goals, which may +be referred to as :gdef:`subgoals <subgoal>` for clarity. +Goals are numbered from 1 to N at each step of the proof to permit applying a +tactic to specific goals. The local context is only shown for the first goal. + +.. coqtop:: all + + split. + +"Variables" may refer specifically to local context items for which the type of their type +is `Set` or `Type`, and :gdef:`"hypotheses" <hypothesis>` refers to items that are +:term:`propositions <proposition>`, +for which the type of their type is `Prop` or `SProp`, +but these terms are also used interchangeably. + +.. coqtop:: out + + let t_n := type of n in idtac "type of n :" t_n; + let tt_n := type of t_n in idtac "type of" t_n ":" tt_n. + let t_H := type of H in idtac "type of H :" t_H; + let tt_H := type of t_H in idtac "type of" t_H ":" tt_H. + +A proof script, consisting of the tactics that are applied to prove a +theorem, is often informally referred to as a "proof". +The real proof, whether complete or incomplete, is a term, the :gdef:`proof term`, +which users may occasionally want to examine. (This is based on the +*Curry-Howard isomorphism* :cite:`How80,Bar81,Gir89,H89`, which is +a correspondence between between proofs and terms and between +propositions and types of λ-calculus. The isomorphism is also +sometimes called the "propositions-as-types correspondence".) + +The :cmd:`Show Proof` command displays the incomplete proof term +before you've completed the proof. For example, here's the proof +term after using the :tacn:`split` tactic above: + +.. coqtop:: all + + Show Proof. + +The incomplete parts, the goals, are represented by +:term:`existential variables <existential variable>` +with names that begin with `?Goal`. The :cmd:`Show Existentials` command +shows each existential with the hypotheses and conclusion for the associated goal. + +.. coqtop:: all + + Show Existentials. + +Coq's kernel verifies the correctness of proof terms when it exits +proof mode by checking that the proof term is :term:`well-typed` and +that its type is the same as the theorem statement. + +After a proof is completed, :cmd:`Print` `<theorem_name>` +shows the proof term and its type. The type appears after +the colon (`forall ...`), as for this theorem from Coq's standard library: + +.. coqtop:: all + + Print proj1. .. _proof-editing-mode: -Entering and leaving proof editing mode ---------------------------------------- +Entering and exiting proof mode +------------------------------- + +Coq enters :term:`proof mode` when you begin a proof through +commands such as :cmd:`Theorem` or :cmd:`Goal`. Coq user interfaces +usually have a way to indicate that you're in proof mode. + +:term:`Tactics <tactic>` are available only in proof mode (currently they give syntax +errors outside of proof mode). Most :term:`commands <command>` can be used both in and out of +proof mode, but some commands only work in or outside of proof mode. -The proof editing mode is entered by asserting a statement, which typically is -the assertion of a theorem using an assertion command like :cmd:`Theorem`. The -list of assertion commands is given in :ref:`Assertions`. The command -:cmd:`Goal` can also be used. +When the proof is completed, you can exit proof mode with commands such as +:cmd:`Qed`, :cmd:`Defined` and :cmd:`Save`. .. cmd:: Goal @type - This is intended for quick assertion of statements, without knowing in - advance which name to give to the assertion, typically for quick - testing of the provability of a statement. If the proof of the - statement is eventually completed and validated, the statement is then - bound to the name ``Unnamed_thm`` (or a variant of this name not already - used for another statement). + Asserts an unnamed proposition. This is intended for quick tests that + a proposition is provable. If the proof is eventually completed and + validated, you can assign a name with the :cmd:`Save` or :cmd:`Defined` + commands. If no name is given, the name will be `Unnamed_thm` (or, + if that name is already defined, a variant of that). .. cmd:: Qed - This command is available in interactive editing proof mode when the - proof is completed. Then :cmd:`Qed` extracts a proof term from the proof - script, switches back to Coq top-level and attaches the extracted - proof term to the declared name of the original goal. The name is - added to the environment as an opaque constant. + Passes a completed :term:`proof term` to Coq's kernel + to check that the proof term is :term:`well-typed` and + to verify that its type matches the theorem statement. If it's verified, the + proof term is added to the global environment as an opaque constant + using the declared name from the original goal. + + It's very rare for a proof term to fail verification. Generally this + indicates a bug in a tactic you used or that you misused some + unsafe tactics. .. exn:: Attempt to save an incomplete proof. :undocumented: + .. exn:: No focused proof (No proof-editing in progress). + + You tried to use a proof mode command such as :cmd:`Qed` outside of proof + mode. + .. note:: Sometimes an error occurs when building the proof term, because @@ -81,9 +182,9 @@ list of assertion commands is given in :ref:`Assertions`. The command even incur a memory overflow. .. cmd:: Save @ident - :name: Save - Saves a completed proof with the name :token:`ident`, which + Similar to :cmd:`Qed`, except that the proof term is added to the global + context with the name :token:`ident`, which overrides any name provided by the :cmd:`Theorem` command or its variants. @@ -98,7 +199,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Admitted - This command is available in interactive editing mode to give up + This command is available in proof mode to give up the current proof and declare the initial goal as an axiom. .. cmd:: Abort {? {| All | @ident } } @@ -120,7 +221,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Proof @term :name: Proof `term` - This command applies in proof editing mode. It is equivalent to + This command applies in proof mode. It is equivalent to :n:`exact @term. Qed.` That is, you have to give the full proof in one gulp, as a proof term (see Section :ref:`applyingtheorems`). @@ -159,7 +260,7 @@ list of assertion commands is given in :ref:`Assertions`. The command | Type {? * } | All - Opens proof editing mode, declaring the set of + Opens proof mode, declaring the set of section variables (see :ref:`gallina-assumptions`) used by the proof. At :cmd:`Qed` time, the system verifies that the set of section variables used in @@ -210,7 +311,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. example:: - .. coqtop:: all + .. coqtop:: all reset Section Test. Variable n : nat. @@ -232,7 +333,6 @@ The following options modify the behavior of ``Proof using``. .. opt:: Default Proof Using "@section_var_expr" - :name: Default Proof Using Use :n:`@section_var_expr` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a @@ -301,7 +401,7 @@ Name a set of section hypotheses for ``Proof using`` Use :cmd:`Unshelve` instead. Proof modes -``````````` +----------- When entering proof mode through commands such as :cmd:`Goal` and :cmd:`Proof`, Coq picks by default the |Ltac| mode. Nonetheless, there exist other proof modes @@ -312,8 +412,8 @@ be changed using the following option. .. opt:: Default Proof Mode @string Select the proof mode to use when starting a proof. Depending on the proof - mode, various syntactic constructs are allowed when writing an interactive - proof. All proof modes support vernacular commands; the proof mode determines + mode, various syntactic constructs are allowed when writing a + proof. All proof modes support commands; the proof mode determines which tactic language and set of tactic definitions are available. The possible option values are: @@ -349,16 +449,16 @@ Navigation in the proof tree .. cmd:: Restart - Restores the proof editing process to the original goal. + Restores the proof to the original goal. .. exn:: No focused proof to restart. :undocumented: .. cmd:: Focus {? @natural } - Focuses the attention on the first subgoal to prove or, if :token:`natural` is + Focuses the attention on the first goal to prove or, if :token:`natural` is specified, the :token:`natural`\-th. The - printing of the other subgoals is suspended until the focused subgoal + printing of the other goals is suspended until the focused goal is solved or unfocused. .. deprecated:: 8.8 @@ -379,14 +479,9 @@ Navigation in the proof tree .. _curly-braces: -.. index:: { - } - -.. todo: :name: "{"; "}" doesn't work, nor does :name: left curly bracket; right curly bracket, - hence the verbose names - .. tacn:: {? {| @natural | [ @ident ] } : } %{ - %} + %} + :name: {; } .. todo See https://github.com/coq/coq/issues/12004 and @@ -403,7 +498,7 @@ Navigation in the proof tree or focus the next one. :n:`@natural:` - Focuses on the :token:`natural`\-th subgoal to prove. + Focuses on the :token:`natural`\-th goal to prove. :n:`[ @ident ]: %{` Focuses on the named goal :token:`ident`. @@ -477,7 +572,7 @@ Navigation in the proof tree Brackets are used to focus on a single goal given either by its position or by its name if it has one. - .. seealso:: The error messages for bullets below. + .. seealso:: The error messages for bullets below. .. _bullets: @@ -567,7 +662,6 @@ Set Bullet Behavior ~~~~~~~~~~~~~~~~~~~ .. opt:: Bullet Behavior {| "None" | "Strict Subproofs" } - :name: Bullet Behavior This option controls the bullet behavior and can take two possible values: @@ -577,8 +671,7 @@ Set Bullet Behavior Modifying the order of goals ```````````````````````````` -.. tacn:: cycle @integer - :name: cycle +.. tacn:: cycle @int_or_var Reorders the selected goals so that the first :n:`@integer` goals appear after the other selected goals. @@ -601,8 +694,7 @@ Modifying the order of goals all: cycle 2. all: cycle -3. -.. tacn:: swap @integer @integer - :name: swap +.. tacn:: swap @int_or_var @int_or_var Exchanges the position of the specified goals. Negative values for :n:`@integer` indicate counting goals @@ -621,7 +713,6 @@ Modifying the order of goals all: swap 1 -1. .. tacn:: revgoals - :name: revgoals Reverses the order of the selected goals. The tactic is only useful with a goal selector, most commonly `all :`. Note that other selectors reorder goals; @@ -638,16 +729,17 @@ Modifying the order of goals Postponing the proof of some goals `````````````````````````````````` +Goals can be :gdef:`shelved` so they are no longer displayed in the proof state. +They can then be :gdef:`unshelved` to make them visible again. + .. tacn:: shelve - :name: shelve 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 :cmd:`Unshelve`. - .. tacv:: shelve_unifiable - :name: shelve_unifiable + .. tacn:: 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. @@ -667,14 +759,12 @@ Postponing the proof of some goals from the shelf into focus, by appending them to the end of the current list of focused goals. -.. tacn:: unshelve @tactic - :name: unshelve +.. tacn:: unshelve @ltac_expr1 Performs :n:`@tactic`, then unshelves existential variables added to the shelf by the execution of :n:`@tactic`, prepending them to the current goal. .. tacn:: give_up - :name: give_up This tactic removes the focused goals from the proof. They are not solved, and cannot be solved later in the proof. As the goals are not @@ -694,7 +784,7 @@ Requesting information Displays the current goals. :n:`@natural` - Display only the :token:`natural`\-th subgoal. + Display only the :token:`natural`\-th goal. :n:`@ident` Displays the named goal :token:`ident`. This is useful in @@ -791,7 +881,7 @@ Requesting information Some tactics (e.g. :tacn:`refine`) allow to build proofs using fixpoint or co-fixpoint constructions. Due to the incremental nature - of interactive proof construction, the check of the termination (or + of proof construction, the check of the termination (or guardedness) of the recursive calls in the fixpoint or cofixpoint constructions is postponed to the time of the completion of the proof. @@ -854,7 +944,6 @@ How to enable diffs ``````````````````` .. opt:: Diffs {| "on" | "off" | "removed" } - :name: Diffs The “on” setting highlights added tokens in green, while the “removed” setting additionally reprints items with removed tokens in red. Unchanged tokens in @@ -983,12 +1072,11 @@ To show differences in the proof term: .. image:: ../../_static/diffs-show-proof.png :alt: coqide with Set Diffs on with compacted hypotheses -Controlling the effect of proof editing commands ------------------------------------------------- +Controlling proof mode +---------------------- .. opt:: Hyps Limit @natural - :name: Hyps Limit This option controls the maximum number of hypotheses displayed in goals after the application of a tactic. All the hypotheses remain usable @@ -1009,7 +1097,7 @@ Controlling the effect of proof editing commands .. flag:: Printing Goal Names - When turned on, the name of the goal is printed in interactive + When turned on, the name of the goal is printed in proof mode, which can be useful in cases of cross references between goals. diff --git a/doc/sphinx/proofs/writing-proofs/rewriting.rst b/doc/sphinx/proofs/writing-proofs/rewriting.rst index 3649202b45..c54701b153 100644 --- a/doc/sphinx/proofs/writing-proofs/rewriting.rst +++ b/doc/sphinx/proofs/writing-proofs/rewriting.rst @@ -1,102 +1,123 @@ -================================= -Term rewriting and simplification -================================= +========================= +Reasoning with equalities +========================= -.. _rewritingexpressions: +There are multiple notions of :gdef:`equality` in Coq: -Rewriting expressions ---------------------- +- :gdef:`Leibniz equality` is the standard + way to define equality in Coq and the Calculus of Inductive Constructions, + which is in terms of a binary relation, i.e. a binary function that returns + a `Prop`. The standard library + defines `eq` similar to this: -These tactics use the equality :g:`eq:forall A:Type, A->A->Prop` defined in -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`. + .. coqdoc:: -.. tacn:: rewrite @term - :name: rewrite + Inductive eq {A : Type} (x : A) : A -> Prop := eq_refl : eq x x. - This tactic applies to any goal. The type of :token:`term` must have the form + The notation `x = y` represents the term `eq x y`. The notation `x = y :> A` + gives the type of x and y explicitly. - ``forall (x``:sub:`1` ``:A``:sub:`1` ``) ... (x``:sub:`n` ``:A``:sub:`n` ``), eq term``:sub:`1` ``term``:sub:`2` ``.`` +- :gdef:`Setoid equality <setoid equality>` defines equality in terms of an equivalence + relation. A :gdef:`setoid` is a set that is equipped with an equivalence relation + (see https://en.wikipedia.org/wiki/Setoid). These are needed to form a :gdef:`quotient set` + or :gdef:`quotient` + (see https://en.wikipedia.org/wiki/Equivalence_Class). In Coq, users generally work + with setoids rather than constructing quotients, for which there is no specific support. - where :g:`eq` is the Leibniz equality or a registered setoid equality. +- :gdef:`Definitional equality <definitional equality>` is equality based on the + :ref:`conversion rules <Conversion-rules>`, which Coq can determine automatically. + When two terms are definitionally equal, Coq knows it can + replace one with the other, such as with :tacn:`change` `X with Y`, among many + other advantages. ":term:`Convertible <convertible>`" is another way of saying that + two terms are definitionally equal. - 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. +.. _rewritingexpressions: - .. exn:: The @term provided does not end with an equation. - :undocumented: +Rewriting with Leibniz and setoid equality +------------------------------------------ - .. exn:: Tactic generated a subgoal identical to the original goal. This happens if @term does not occur in the goal. - :undocumented: +.. tacn:: rewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 } - .. tacv:: rewrite -> @term + .. insertprodn oriented_rewriter one_term_with_bindings - Is equivalent to :n:`rewrite @term` + .. prodn:: + oriented_rewriter ::= {? {| -> | <- } } {? @natural } {? {| ? | ! } } @one_term_with_bindings + one_term_with_bindings ::= {? > } @one_term {? with @bindings } - .. tacv:: rewrite <- @term + Rewrites terms based on equalities. The type of :n:`@one_term` must have the form: - Uses the equality :n:`@term`:sub:`1` :n:`= @term` :sub:`2` from right to left + :n:`{? forall {+ (x__i: A__i) } , } EQ @term__1 @term__2` - .. tacv:: rewrite @term in @goal_occurrences + where :g:`EQ` is the Leibniz equality `eq` or a registered setoid equality. + Note that :n:`eq @term__1 @term__2` is typically written with the infix notation + :n:`@term__1 = @term__2`. You must `Require Setoid` to use the tactic + with a setoid equality or with :ref:`setoid rewriting <generalizedrewriting>`. + In the general form, any :n:`@binder` may be used, not just :n:`(x__i: A__i)`. - Analogous to :n:`rewrite @term` but rewriting is done following - the clause :token:`goal_occurrences`. For instance: + .. todo doublecheck the @binder comment is correct. - + :n:`rewrite H in H'` will rewrite `H` in the hypothesis - ``H'`` instead of the current goal. - + :n:`rewrite H in H' at 1, H'' at - 2 |- *` means - :n:`rewrite H; rewrite H in H' at 1; rewrite H in H'' at - 2.` - 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'` for all hypotheses - :g:`H'` 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. + :n:`rewrite @one_term` finds subterms matching :n:`@term__1` in the goal, + and replaces them with :n:`@term__2` (or the reverse if `<-` is given). + Some of the variables :g:`x`\ :sub:`i` are solved by unification, + and some of the types :n:`A__1, ..., A__n` may become new + subgoals. :tacn:`rewrite` won't find occurrences inside `forall` that refer + to variables bound by the `forall`; use :tacn:`setoid_rewrite` + if you want to find such occurrences. - Orientation :g:`->` or :g:`<-` can be inserted before the :token:`term` to rewrite. + :n:`{+, @oriented_rewriter }` + The :n:`@oriented_rewriter`\s are applied sequentially + to the first goal generated by the previous :n:`@oriented_rewriter`. If any of them fail, + the tactic fails. - .. tacv:: rewrite @term at @occurrences + :n:`{? {| -> | <- } }` + For `->` (the default), :n:`@term__1` is rewritten + into :n:`@term__2`. For `<-`, :n:`@term__2` is rewritten into :n:`@term__1`. - Rewrite only the given :token:`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. + :n:`{? @natural } {? {| ? | ! } }` + :n:`@natural` is the number of rewrites to perform. If `?` is given, :n:`@natural` + is the maximum number of rewrites to perform; otherwise :n:`@natural` is the exact number + of rewrites to perform. - .. tacv:: rewrite @term by @tactic + `?` (without :n:`@natural`) performs the rewrite as many times as possible + (possibly zero times). + This form never fails. `!` (without :n:`@natural`) performs the rewrite as many + times as possible + and at least once. The tactic fails if the requested number of rewrites can't + be performed. :n:`@natural !` is equivalent to :n:`@natural`. - Use tactic to completely solve the side-conditions arising from the - :tacn:`rewrite`. + :n:`@occurrences` + If :n:`@occurrences` specifies multiple occurrences, the tactic succeeds if + any of them can be rewritten. If not specified, only the first occurrence + in the conclusion is replaced. - .. tacv:: rewrite {+, @orientation @term} {? in @ident } + If :n:`at @occs_nums` is specified, rewriting is always done with + :ref:`setoid rewriting <generalizedrewriting>`, even for Leibniz’s equality. - Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. An :production:`orientation` - ``->`` or ``<-`` 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. + :n:`by @ltac_expr3` + If specified, is used to resolve all side conditions generated by the tactic. - In all forms of rewrite described above, a :token:`term` to rewrite can be - immediately prefixed by one of the following modifiers: + .. exn:: Tactic failure: Setoid library not loaded. + :undocumented: - + `?` : the tactic :n:`rewrite ?@term` performs the rewrite of :token:`term` as many - times as possible (perhaps zero time). This form never fails. - + :n:`@natural?` : works similarly, except that it will do at most :token:`natural` rewrites. - + `!` : works as `?`, except that at least one rewrite should succeed, otherwise - the tactic fails. - + :n:`@natural!` (or simply :n:`@natural`) : precisely :token:`natural` rewrites of :token:`term` will be done, - leading to failure if these :token:`natural` rewrites are not possible. + .. todo You can use Typeclasses Debug to tell whether rewrite used + setoid rewriting. Example here: https://github.com/coq/coq/pull/13470#discussion_r539230973 - .. tacv:: erewrite @term - :name: erewrite + .. exn:: Cannot find a relation to rewrite. + :undocumented: + + .. exn:: Tactic generated a subgoal identical to the original goal. + :undocumented: + + .. exn:: Found no subterm matching @term in @ident. + Found no subterm matching @term in the current goal. - 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 happens if :n:`@term` does not occur in, respectively, the named hypothesis or the goal. + + .. tacn:: erewrite {+, @oriented_rewriter } {? @occurrences } {? by @ltac_expr3 } + + Works like :tacn:`rewrite`, but turns + unresolved bindings, if any, into existential variables instead of + failing. It has the same parameters as :tacn:`rewrite`. .. flag:: Keyed Unification @@ -105,197 +126,221 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. the same key as the left- or right-hand side of the lemma given to rewrite, and the arguments are then unified up to full reduction. -.. 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 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. - :undocumented: - - .. tacv:: replace @term with @term’ by @tactic - - This acts as :n:`replace @term with @term’` but applies :token:`tactic` to solve the generated - subgoal :n:`@term = @term’`. +.. tacn:: rewrite * {? {| -> | <- } } @one_term {? in @ident } {? at @rewrite_occs } {? by @ltac_expr3 } + rewrite * {? {| -> | <- } } @one_term at @rewrite_occs in @ident {? by @ltac_expr3 } + :name: rewrite *; _ + :undocumented: - .. tacv:: replace @term +.. tacn:: rewrite_db @ident {? in @ident } + :undocumented: - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` or :n:`@term’ = @term`. +.. tacn:: replace @one_term__from with @one_term__to {? @occurrences } {? by @ltac_expr3 } + replace {? {| -> | <- } } @one_term__from {? @occurrences } + :name: replace; _ - .. tacv:: replace -> @term + The first form replaces all free occurrences of :n:`@one_term__from` + in the current goal with :n:`@one_term__to` and generates an equality + :n:`@one_term__to = @one_term__from` + as a subgoal. (Note the generated equality is reversed with respect + to the order of the two terms in the tactic syntax; see + issue `#13480 <https://github.com/coq/coq/issues/13480>`_.) + This equality is automatically solved if it occurs among + the hypotheses, or if its symmetric form occurs. - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term = @term’` + The second form, with `->` or no arrow, replaces :n:`@one_term__from` + with :n:`@term__to` using + the first hypothesis whose type has the form :n:`@one_term__from = @term__to`. + If `<-` is given, the tactic uses the first hypothesis with the reverse form, + i.e. :n:`@term__to = @one_term__from`. - .. tacv:: replace <- @term + :n:`@occurrences` + The `type of` and `value of` forms are not supported. + Note you must `Require Setoid` to use the `at` clause in :n:`@occurrences`. - Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has - the form :n:`@term’ = @term` + :n:`by @ltac_expr3` + Applies the :n:`@ltac_expr3` to solve the generated equality. - .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} - replace -> @term in @goal_occurrences - replace <- @term in @goal_occurrences + .. exn:: Terms do not have convertible types. + :undocumented: - Acts as before but the replacements take place in the specified clauses - (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not - only in the conclusion of the goal. The clause argument must not contain - any ``type of`` nor ``value of``. + .. tacn:: cutrewrite {? {| -> | <- } } @one_term {? in @ident } - .. tacv:: cutrewrite {? {| <- | -> } } (@term__1 = @term__2) {? in @ident } - :name: cutrewrite + Where :n:`@one_term` is an equality. .. deprecated:: 8.5 Use :tacn:`replace` instead. -.. tacn:: subst @ident - :name: subst +.. tacn:: substitute {? {| -> | <- } } @one_term {? with @bindings } + :undocumented: + +.. tacn:: subst {* @ident } - 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. + For each :n:`@ident`, in order, for which there is a hypothesis in the form + :n:`@ident = @term` or :n:`@term = @ident`, replaces :n:`@ident` with :n:`@term` + everywhere in the hypotheses and the conclusion and clears :n:`@ident` and the hypothesis + from the context. If there are multiple hypotheses that match the :n:`@ident`, + the first one is used. If no :n:`@ident` is given, replacement is done for all + hypotheses in the appropriate form in top to bottom order. - If :n:`@ident` is a local definition of the form :n:`@ident := t`, it is also + If :n:`@ident` is a local definition of the form :n:`@ident := @term`, it is also unfolded and cleared. - If :n:`@ident` is a section variable it is expected to have no - indirect occurrences in the goal, i.e. that no global declarations - implicitly depending on the section variable must be present in the + If :n:`@ident` is a section variable it must have no + indirect occurrences in the goal, i.e. no global declarations + implicitly depending on the section variable may be present in the goal. .. 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} - - This is equivalent to :n:`subst @ident`:sub:`1`:n:`; ...; subst @ident`:sub:`n`. - - .. tacv:: subst - - This applies :tacn:`subst` repeatedly from top to bottom to all hypotheses 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`` and :n:`@ident` not a section variable with indirect - dependencies in the goal. + If the hypothesis is itself dependent in the goal, it is replaced by the proof of + reflexivity of equality. .. flag:: Regular Subst Tactic This flag controls the behavior of :tacn:`subst`. When it is activated (it is by default), :tacn:`subst` also deals with the following corner cases: - + A context with ordered hypotheses :n:`@ident`:sub:`1` :n:`= @ident`:sub:`2` - and :n:`@ident`:sub:`1` :n:`= t`, or :n:`t′ = @ident`:sub:`1`` with `t′` not - a variable, and no other hypotheses of the form :n:`@ident`:sub:`2` :n:`= u` - or :n:`u = @ident`:sub:`2`; without the flag, a second call to - subst would be necessary to replace :n:`@ident`:sub:`2` by `t` or + + A context with ordered hypotheses :n:`@ident__1 = @ident__2` + and :n:`@ident__1 = t`, or :n:`t′ = @ident__1` with `t′` not + a variable, and no other hypotheses of the form :n:`@ident__2 = u` + or :n:`u = @ident__2`; without the flag, a second call to + subst would be necessary to replace :n:`@ident__2` by `t` or `t′` respectively. + The presence of a recursive equation which without the flag 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 + + A context with cyclic dependencies as with hypotheses :n:`@ident__1 = f @ident__2` + and :n:`@ident__2 = g @ident__1` which without the flag would be a cause of failure of :tacn:`subst`. - Additionally, it prevents a local definition such as :n:`@ident := t` to be + Additionally, it prevents a local definition such as :n:`@ident := t` from being 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 flag it may break. - default. - .. exn:: Cannot find any non-recursive equality over :n:`@ident`. + .. exn:: Cannot find any non-recursive equality over @ident. :undocumented: - .. exn:: Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in hypothesis :n:`@ident`. - Section variable :n:`@ident` occurs implicitly in global declaration :n:`@qualid` present in the conclusion. + .. exn:: Section variable @ident occurs implicitly in global declaration @qualid present in hypothesis @ident. + Section variable @ident occurs implicitly in global declaration @qualid present in the conclusion. Raised when the variable is a section variable with indirect dependencies in the goal. + If :n:`@ident` is a section variable, it must not have any + indirect occurrences in the goal, i.e. no global declarations + implicitly depending on the section variable may be present in the + goal. +.. tacn:: simple subst + :undocumented: -.. tacn:: stepl @term - :name: stepl +.. tacn:: stepl @one_term {? by @ltac_expr } - 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 + For chaining rewriting steps. It assumes a goal in the + form :n:`R @term__1 @term__2` 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`. + where `eq` is typically a setoid equality. The application of :n:`stepl @one_term` + then replaces the goal by :n:`R @one_term @term__2` and adds a new goal stating + :n:`eq @one_term @term__1`. - .. cmd:: Declare Left Step @term + If :n:`@ltac_expr` is specified, it is applied to the side condition. - Adds :n:`@term` to the database used by :tacn:`stepl`. + .. cmd:: Declare Left Step @one_term + + Adds :n:`@one_term` to the database used by :tacn:`stepl`. This tactic is especially useful for parametric setoids which are not accepted as regular setoids for :tacn:`rewrite` and :tacn:`setoid_replace` (see :ref:`Generalizedrewriting`). - .. tacv:: stepl @term by @tactic - - This applies :n:`stepl @term` then applies :token:`tactic` to the second goal. - - .. tacv:: stepr @term by @tactic - :name: stepr + .. tacn:: stepr @one_term {? by @ltac_expr } - This behaves as :tacn:`stepl` but on the right-hand-side of the binary - relation. Lemmas are expected to be of the form + This behaves like :tacn:`stepl` but on the right hand side of the binary + relation. Lemmas are expected to be in the form :g:`forall x y z, R x y -> eq y z -> R x z`. - .. cmd:: Declare Right Step @term + .. cmd:: Declare Right Step @one_term Adds :n:`@term` to the database used by :tacn:`stepr`. +Rewriting with definitional equality +------------------------------------ -.. tacn:: change @term - :name: change +.. tacn:: change {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences } - 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. + Replaces terms with other :term:`convertible` terms. + If :n:`@one_term__from` is not specified, then :n:`@one_term__from` replaces the conclusion and/or + the specified hypotheses. If :n:`@one_term__from` is specified, the tactic replaces occurrences + of :n:`@one_term__to` within the conclusion and/or the specified hypotheses. + + :n:`{? @one_term__from {? at @occs_nums } with }` + Replaces the occurrences of :n:`@one_term__from` specified by :n:`@occs_nums` + with :n:`@one_term__to`, provided that the two :n:`@one_term`\s are + convertible. :n:`@one_term__from` may contain pattern variables such as `?x`, + whose value which will substituted for `x` in :n:`@one_term__to`, such as in + `change (f ?x ?y) with (g (x, y))` or `change (fun x => ?f x) with f`. + + :n:`@occurrences` + If `with` is not specified, :n:`@occurrences` must only specify + entire hypotheses and/or the goal; it must not include any + :n:`at @occs_nums` clauses. .. exn:: Not convertible. :undocumented: - .. tacv:: change @term with @term’ + .. exn:: Found an "at" clause without "with" clause + :undocumented: - This replaces the occurrences of :n:`@term` by :n:`@term’` in the current goal. - The term :n:`@term` and :n:`@term’` must be convertible. + .. tacn:: now_show @one_term - .. tacv:: change @term at {+ @natural} with @term’ + A synonym for :n:`change @one_term`. It can be used to + make some proof steps explicit when refactoring a proof script + to make it readable. - This replaces the occurrences numbered :n:`{+ @natural}` of :n:`@term` by :n:`@term’` - in the current goal. The terms :n:`@term` and :n:`@term’` must be convertible. + .. seealso:: :ref:`Performing computations <performingcomputations>` - .. exn:: Too few occurrences. - :undocumented: +.. tacn:: change_no_check {? @one_term__from {? at @occs_nums } with } @one_term__to {? @occurrences } - .. tacv:: change @term {? {? at {+ @natural}} with @term} in @goal_occurrences + For advanced usage. Similar to :tacn:`change`, but as an optimization, + it skips checking that :n:`@one_term__to` is convertible with the goal or + :n:`@one_term__from`. - In the presence of :n:`with`, this applies :tacn:`change` to the - occurrences specified by :n:`@goal_occurrences`. In the - absence of :n:`with`, :n:`@goal_occurrences` is expected to - only list hypotheses (and optionally the conclusion) without - specifying occurrences (i.e. no :n:`at` clause). + Recall that the Coq kernel typechecks proofs again when they are concluded to + ensure correctness. Hence, using :tacn:`change` checks convertibility twice + overall, while :tacn:`change_no_check` can produce ill-typed terms, + but checks convertibility only once. + Hence, :tacn:`change_no_check` can be useful to speed up certain proof + scripts, especially if one knows by construction that the argument is + indeed convertible to the goal. - .. tacv:: now_show @term + In the following example, :tacn:`change_no_check` replaces :g:`False` with + :g:`True`, but :cmd:`Qed` then rejects the proof, ensuring consistency. - This is a synonym of :n:`change @term`. It can be used to - make some proof steps explicit when refactoring a proof script - to make it readable. + .. example:: - .. seealso:: :ref:`Performing computations <performingcomputations>` + .. coqtop:: all abort fail + + Goal False. + change_no_check True. + exact I. + Qed. + + .. example:: + + .. coqtop:: all abort fail + + Goal True -> False. + intro H. + change_no_check False in H. + exact H. + Qed. + + .. tacn:: convert_concl_no_check @one_term + + .. deprecated:: 8.11 + + Deprecated old name for :tacn:`change_no_check`. Does not support any of its + variants. .. _performingcomputations: diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index f454f4313d..609884ce1d 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1073,7 +1073,7 @@ main grammar, or from another custom entry as is the case in Notation "[ e ]" := e (e custom expr at level 2). to indicate that ``e`` has to be parsed at level ``2`` of the grammar -associated to the custom entry ``expr``. The level can be omitted, as in +associated with the custom entry ``expr``. The level can be omitted, as in .. coqdoc:: @@ -1159,7 +1159,6 @@ Similarly, to indicate that a custom entry should parse global references Notation "x" := x (in custom expr at level 0, x global). .. cmd:: Print Custom Grammar @ident - :name: Print Custom Grammar This displays the state of the grammar for terms associated with the custom entry :token:`ident`. @@ -1551,7 +1550,6 @@ Displaying information about scopes Use the :cmd:`Print Visibility` command to display the current notation scope stack. .. cmd:: Print Scope @scope_name - :name: Print Scope Displays all notations defined in the notation scope :n:`@scope_name`. It also displays the delimiting key and the class to which the @@ -1685,7 +1683,6 @@ Number notations ~~~~~~~~~~~~~~~~ .. cmd:: Number Notation @qualid__type @qualid__parse @qualid__print {? ( {+, @number_modifier } ) } : @scope_name - :name: Number Notation .. insertprodn number_modifier number_string_via @@ -1842,12 +1839,12 @@ Number notations .. exn:: @qualid__parse should go from Number.int to @type or (option @type). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The parsing function given to the :cmd:`Number Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: @qualid__print should go from @type to Number.int or (option Number.int). Instead of Number.int, the types Number.uint or Z or Int63.int or Number.number could be used (you may need to require BinNums or Number or Int63 first). The printing function given to the :cmd:`Number Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: Unexpected term @term while parsing a number notation. @@ -1877,7 +1874,6 @@ String notations ~~~~~~~~~~~~~~~~ .. cmd:: String Notation @qualid__type @qualid__parse @qualid__print {? ( @number_string_via ) } : @scope_name - :name: String Notation Allows the user to customize how strings are parsed and printed. @@ -1921,12 +1917,12 @@ String notations .. exn:: @qualid__parse should go from Byte.byte or (list Byte.byte) to @type or (option @type). The parsing function given to the :cmd:`String Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: @qualid__print should go from @type to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)). The printing function given to the :cmd:`String Notation` - vernacular is not of the right type. + command is not of the right type. .. exn:: Unexpected term @term while parsing a string notation. diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst index 93571ecebb..0f0edc6bdd 100644 --- a/doc/sphinx/using/libraries/funind.rst +++ b/doc/sphinx/using/libraries/funind.rst @@ -170,7 +170,6 @@ Tactics ------- .. tacn:: functional induction @term {? using @one_term {? with @bindings } } {? as @simple_intropattern } - :name: functional induction Performs case analysis and induction following the definition of a function :token:`qualid`, which must be fully applied to its arguments as part of @@ -221,7 +220,6 @@ Tactics :undocumented: .. tacn:: functional inversion {| @ident | @natural } {? @qualid } - :name: functional inversion Performs inversion on hypothesis :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst index b68b2ed2a7..78ac17bda1 100644 --- a/doc/sphinx/using/tools/coqdoc.rst +++ b/doc/sphinx/using/tools/coqdoc.rst @@ -34,9 +34,9 @@ Coq material inside documentation. Coq material is quoted between the delimiters ``[`` and ``]``. Square brackets may be nested, the inner ones being understood as being part of the -quoted code (thus you can quote a term like ``fun x => u`` by writing ``[fun -x => u]``). Inside quotations, the code is pretty-printed in the same -way as it is in code parts. +quoted code (thus you can quote a term like ``let id := fun [T : Type] (x : t) => x in id 0`` +by writing ``[let id := fun [T : Type] (x : t) => x in id 0]``). +Inside quotations, the code is pretty-printed the same way as in code parts. Preformatted vernacular is enclosed by ``[[`` and ``]]``. The former must be followed by a newline and the latter must follow a newline. diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index 8f642df8fd..e24e534024 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -348,7 +348,7 @@ class VernacVariantObject(VernacObject): .. cmd:: Axiom @ident : @term. This command links :token:`term` to the name :token:`term` as its specification in - the global context. The fact asserted by :token:`term` is thus assumed as a + the global environment. The fact asserted by :token:`term` is thus assumed as a postulate. .. cmdv:: Parameter @ident : @term. diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index 75b3260166..f267cdb697 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -1003,7 +1003,7 @@ simple_tactic: [ | DELETE "replace" uconstr clause | "replace" orient uconstr clause | REPLACE "rewrite" "*" orient uconstr "in" hyp "at" occurrences by_arg_tac -| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences by_arg_tac ) +| WITH "rewrite" "*" orient uconstr OPT ( "in" hyp ) OPT ( "at" occurrences ) by_arg_tac | DELETE "rewrite" "*" orient uconstr "in" hyp by_arg_tac | DELETE "rewrite" "*" orient uconstr "at" occurrences by_arg_tac | DELETE "rewrite" "*" orient uconstr by_arg_tac @@ -1814,6 +1814,7 @@ ltac_defined_tactics: [ | "lia" | "lra" | "nia" +| "now_show" constr | "nra" | "over" TAG SSR | "split_Rabs" @@ -2373,7 +2374,7 @@ ssrapplyarg: [ ] constr_with_bindings_arg: [ -| EDIT ADD_OPT ">" constr_with_bindings TAG SSR +| EDIT ADD_OPT ">" constr_with_bindings ] destruction_arg: [ @@ -2469,6 +2470,15 @@ variance_identref: [ | EDIT ADD_OPT variance identref ] +conversion: [ +| DELETE constr +| DELETE constr "with" constr +| PRINT +| REPLACE constr "at" occs_nums "with" constr +| WITH OPT ( constr OPT ( "at" occs_nums ) "with" ) constr +| PRINT +] + SPLICE: [ | clause | noedit_mode @@ -2694,6 +2704,8 @@ SPLICE: [ | cumul_ident_decl | variance | variance_identref +| rewriter +| conversion ] (* end SPLICE *) RENAME: [ @@ -2751,6 +2763,7 @@ RENAME: [ | pattern_occ pattern_occs | hypident_occ hyp_occs | concl_occ concl_occs +| constr_with_bindings_arg one_term_with_bindings ] simple_tactic: [ diff --git a/doc/tools/docgram/doc_grammar.ml b/doc/tools/docgram/doc_grammar.ml index dd7990368e..a1c1d87763 100644 --- a/doc/tools/docgram/doc_grammar.ml +++ b/doc/tools/docgram/doc_grammar.ml @@ -1726,8 +1726,6 @@ let process_rst g file args seen tac_prods cmd_prods = let cmd_exclude_files = [ "doc/sphinx/proof-engine/ssreflect-proof-language.rst"; - "doc/sphinx/proofs/writing-proofs/rewriting.rst"; - "doc/sphinx/proofs/writing-proofs/proof-mode.rst"; "doc/sphinx/proof-engine/tactics.rst"; ] in diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index d950b32160..72e101446c 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -1247,11 +1247,7 @@ lident: [ destruction_arg: [ | natural -| constr_with_bindings_arg -] - -constr_with_bindings_arg: [ -| OPT ">" one_term OPT ( "with" bindings ) (* SSR plugin *) +| one_term_with_bindings ] occurrences: [ @@ -1691,7 +1687,7 @@ simple_tactic: [ | "absurd" one_term | "contradiction" OPT ( one_term OPT ( "with" bindings ) ) | "autorewrite" OPT "*" "with" LIST1 ident OPT occurrences OPT ( "using" ltac_expr ) -| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs OPT ( "by" ltac_expr3 ) ) +| "rewrite" "*" OPT [ "->" | "<-" ] one_term OPT ( "in" ident ) OPT ( "at" rewrite_occs ) OPT ( "by" ltac_expr3 ) | "rewrite" "*" OPT [ "->" | "<-" ] one_term "at" rewrite_occs "in" ident OPT ( "by" ltac_expr3 ) | "refine" one_term | "simple" "refine" one_term @@ -1783,12 +1779,12 @@ simple_tactic: [ | "eintros" LIST0 intropattern | "decide" "equality" | "compare" one_term one_term -| "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "simple" "apply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "simple" "eapply" LIST1 constr_with_bindings_arg SEP "," OPT in_hyp_as -| "elim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) -| "eelim" constr_with_bindings_arg OPT ( "using" one_term OPT ( "with" bindings ) ) +| "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "simple" "apply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "simple" "eapply" LIST1 one_term_with_bindings SEP "," OPT in_hyp_as +| "elim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) ) +| "eelim" one_term_with_bindings OPT ( "using" one_term OPT ( "with" bindings ) ) | "case" induction_clause_list | "ecase" induction_clause_list | "fix" ident natural OPT ( "with" LIST1 fixdecl ) @@ -1842,8 +1838,8 @@ simple_tactic: [ | "unfold" LIST1 reference_occs SEP "," OPT occurrences | "fold" LIST1 one_term OPT occurrences | "pattern" LIST1 pattern_occs SEP "," OPT occurrences -| "change" conversion OPT occurrences -| "change_no_check" conversion OPT occurrences +| "change" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences +| "change_no_check" OPT ( one_term OPT ( "at" occs_nums ) "with" ) one_term OPT occurrences | "btauto" | "rtauto" | "congruence" OPT natural OPT ( "with" LIST1 one_term ) @@ -1922,6 +1918,7 @@ simple_tactic: [ | "lia" | "lra" | "nia" +| "now_show" one_term | "nra" | "over" (* SSR plugin *) | "split_Rabs" @@ -1977,11 +1974,11 @@ as_name: [ ] oriented_rewriter: [ -| OPT [ "->" | "<-" ] rewriter +| OPT [ "->" | "<-" ] OPT natural OPT [ "?" | "!" ] one_term_with_bindings ] -rewriter: [ -| OPT natural OPT [ "?" | "!" ] constr_with_bindings_arg +one_term_with_bindings: [ +| OPT ">" one_term OPT ( "with" bindings ) ] induction_clause_list: [ @@ -2454,12 +2451,6 @@ cofixdecl: [ | "(" ident LIST0 simple_binder ":" term ")" ] -conversion: [ -| one_term -| one_term "with" one_term -| one_term "at" occs_nums "with" one_term -] - func_scheme_def: [ | ident ":=" "Induction" "for" qualid "Sort" sort_family (* funind plugin *) ] |