diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/_templates/versions.html | 48 | ||||
| -rw-r--r-- | doc/sphinx/addendum/program.rst | 12 | ||||
| -rwxr-xr-x | doc/sphinx/conf.py | 22 | ||||
| -rw-r--r-- | doc/sphinx/language/cic.rst | 69 | ||||
| -rw-r--r-- | doc/sphinx/language/coq-library.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/language/core/basic.rst | 39 | ||||
| -rw-r--r-- | doc/sphinx/practical-tools/coq-commands.rst | 83 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 48 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 154 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 87 | ||||
| -rw-r--r-- | doc/sphinx/using/libraries/writing.rst | 2 |
15 files changed, 505 insertions, 81 deletions
diff --git a/doc/sphinx/_templates/versions.html b/doc/sphinx/_templates/versions.html new file mode 100644 index 0000000000..967d00d2bf --- /dev/null +++ b/doc/sphinx/_templates/versions.html @@ -0,0 +1,48 @@ +{# Forked from versions.html in sphinx_rtd_theme 0.4.3 #} + +{# +The MIT License (MIT) + +Copyright (c) 2013-2018 Dave Snider, Read the Docs, Inc. & contributors + +Permission is hereby granted, free of charge, to any person obtaining a copy of +this software and associated documentation files (the "Software"), to deal in +the Software without restriction, including without limitation the rights to +use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies of +the Software, and to permit persons to whom the Software is furnished to do so, +subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS +FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR +COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER +IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN +CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +#} + +{% if not READTHEDOCS %} + <div class="rst-versions" data-toggle="rst-versions" role="note" aria-label="versions"> + <span class="rst-current-version" data-toggle="rst-current-version"> + <span class="fa fa-book"> Other versions</span> + v: {{ version }} + <span class="fa fa-caret-down"></span> + </span> + <div class="rst-other-versions"> + <dl> + <dt>{{ _('Versions') }}</dt> + {% for slug, url in versions %} + <dd><a href="{{ url }}">{{ slug }}</a></dd> + {% endfor %} + </dl> + <dl> + <dt>{{ _('Downloads') }}</dt> + {% for type, url in downloads %} + <dd><a href="{{ url }}">{{ type }}</a></dd> + {% endfor %} + </dl> + </div> + </div> +{% endif %} diff --git a/doc/sphinx/addendum/program.rst b/doc/sphinx/addendum/program.rst index 52862dea47..b5618c5721 100644 --- a/doc/sphinx/addendum/program.rst +++ b/doc/sphinx/addendum/program.rst @@ -342,17 +342,11 @@ optional tactic is replaced by the default one if not specified. .. flag:: Hide Obligations + .. deprecated:: 8.12 + Controls whether obligations appearing in the term should be hidden as implicit arguments of the special - constantProgram.Tactics.obligation. - -.. flag:: Shrink Obligations - - .. deprecated:: 8.7 - - This flag (on by default) controls whether obligations should have - their context minimized to the set of variables used in the proof of - the obligation, to avoid unnecessary dependencies. + constant ``Program.Tactics.obligation``. The module :g:`Coq.Program.Tactics` defines the default tactic for solving obligations called :g:`program_simpl`. Importing :g:`Coq.Program.Program` also diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index dbe582df95..4136b406de 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -202,6 +202,7 @@ html_theme = 'sphinx_rtd_theme' # Theme options are theme-specific and customize the look and feel of a theme # further. For a list of options available for each theme, see the # documentation. +PDF_URL = "https://github.com/coq/coq/releases/download/V{version}/coq-{version}-reference-manual.pdf" html_theme_options = { 'collapse_navigation': False } @@ -210,7 +211,26 @@ html_context = { 'github_user': 'coq', 'github_repo': 'coq', 'github_version': 'master', - 'conf_py_path': '/doc/sphinx/' + 'conf_py_path': '/doc/sphinx/', + # Versions and downloads listed in the versions menu (see _templates/versions.html) + 'versions': [ + ("master", "https://coq.github.io/doc/master/refman/"), + ("stable", "https://coq.inria.fr/distrib/current/refman/"), + ("v8.11", "https://coq.github.io/doc/v8.11/refman/"), + ("v8.10", "https://coq.github.io/doc/v8.10/refman/"), + ("v8.9", "https://coq.github.io/doc/v8.9/refman/"), + ("8.8", "https://coq.inria.fr/distrib/V8.8.2/refman/"), + ("8.7", "https://coq.inria.fr/distrib/V8.7.2/refman/"), + ("8.6", "https://coq.inria.fr/distrib/V8.6.1/refman/"), + ("8.5", "https://coq.inria.fr/distrib/V8.5pl3/refman/"), + ("8.4", "https://coq.inria.fr/distrib/V8.4pl6/refman/"), + ("8.3", "https://coq.inria.fr/distrib/V8.3pl5/refman/"), + ("8.2", "https://coq.inria.fr/distrib/V8.2pl3/refman/"), + ("8.1", "https://coq.inria.fr/distrib/V8.1pl6/refman/"), + ("8.0", "https://coq.inria.fr/distrib/V8.0/doc/") + ], + 'downloads': ([("PDF", PDF_URL.format(version=version))] + if coq_config.is_a_released_version else []) } # Add any paths that contain custom themes here, relative to this directory. diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index e5af39c8fb..b125d21a3c 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -1108,6 +1108,75 @@ between universes for inductive types in the Type hierarchy. Check infinite_loop (lam (@id Lam)) : False. +.. example:: Non strictly positive occurrence + + It is less obvious why inductive type definitions with occurences + that are positive but not strictly positive are harmful. + We will see that in presence of an impredicative type they + are unsound: + + .. coqtop:: all + + Fail Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. + + If we were to accept this definition we could derive a contradiction + by creating an injective function from :math:`A → \Prop` to :math:`A`. + + This function is defined by composing the injective constructor of + the type :math:`A` with the function :math:`λx. λz. z = x` injecting + any type :math:`T` into :math:`T → \Prop`. + + .. coqtop:: none + + Unset Positivity Checking. + Inductive A: Type := introA: ((A -> Prop) -> Prop) -> A. + Set Positivity Checking. + + .. coqtop:: all + + Definition f (x: A -> Prop): A := introA (fun z => z = x). + + .. coqtop:: in + + Lemma f_inj: forall x y, f x = f y -> x = y. + Proof. + unfold f; intros ? ? H; injection H. + set (F := fun z => z = y); intro HF. + symmetry; replace (y = x) with (F y). + + unfold F; reflexivity. + + rewrite <- HF; reflexivity. + Qed. + + The type :math:`A → \Prop` can be understood as the powerset + of the type :math:`A`. To derive a contradiction from the + injective function :math:`f` we use Cantor's classic diagonal + argument. + + .. coqtop:: all + + Definition d: A -> Prop := fun x => exists s, x = f s /\ ~s x. + Definition fd: A := f d. + + .. coqtop:: in + + Lemma cantor: (d fd) <-> ~(d fd). + Proof. + split. + + intros [s [H1 H2]]; unfold fd in H1. + replace d with s. + * assumption. + * apply f_inj; congruence. + + intro; exists d; tauto. + Qed. + + Lemma bad: False. + Proof. + pose cantor; tauto. + Qed. + + This derivation was first presented by Thierry Coquand and Christine + Paulin in :cite:`CP90`. + .. _Template-polymorphism: Template polymorphism diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index acdd4408ed..899173a83a 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -9,11 +9,11 @@ The |Coq| library The |Coq| library has two parts: - * **The basic library**: definitions and theorems for + * The :gdef:`prelude`: definitions and theorems for the most commonly used elementary logical notions and data types. |Coq| normally loads these files automatically when it starts. - * **The standard library**: general-purpose libraries with + * The :gdef:`standard library`: general-purpose libraries with definitions and theorems for sets, lists, sorting, arithmetic, etc. To use these files, users must load them explicitly with the ``Require`` command (see :ref:`compiled-files`) @@ -28,8 +28,8 @@ also be browsed at http://coq.inria.fr/stdlib/. -The basic library ------------------ +The prelude +----------- This section lists the basic notions and results which are directly available in the standard |Coq| system. Most of these constructions diff --git a/doc/sphinx/language/core/basic.rst b/doc/sphinx/language/core/basic.rst index 9473cc5a15..aa93b4d21f 100644 --- a/doc/sphinx/language/core/basic.rst +++ b/doc/sphinx/language/core/basic.rst @@ -130,30 +130,37 @@ Strings identified with :production:`string`. Keywords - The following character sequences are reserved keywords that cannot be - used as identifiers:: + The following character sequences are keywords defined in the main Coq grammar + that cannot be used as identifiers (even when starting Coq with the `-noinit` + command-line flag):: _ Axiom CoFixpoint Definition Fixpoint Hypothesis Parameter Prop - SProp Set Theorem Type Variable as at cofix discriminated else end + SProp Set Theorem Type Variable as at cofix else end fix for forall fun if in let match return then where with - Note that notations and plugins may define additional keywords. + The following are keywords defined in notations or plugins loaded in the :term:`prelude`:: -Other tokens - The set of - tokens defined at any given time can vary because the :cmd:`Notation` - command can define new tokens. A :cmd:`Require` command may load more notation definitions, - while the end of a :cmd:`Section` may remove notations. Some notations - are defined in the standard library (see :ref:`thecoqlibrary`) and are generally - loaded automatically at startup time. + IF by exists exists2 using + + Note that loading additional modules or plugins may expand the set of reserved + keywords. - Here are the character sequences that |Coq| directly defines as tokens - without using :cmd:`Notation`:: +Other tokens + The following character sequences are tokens defined in the main Coq grammar + (even when starting Coq with the `-noinit` command-line flag):: - ! #[ % & ' ( () (bfs) (dfs) ) * ** + , - -> + ! #[ % & ' ( () ) * + , - -> . .( .. ... / : ::= := :> :>> ; < <+ <- <: - <<: <= = => > >-> >= ? @ @{ [ [= ] _ - `( `{ { {| | |- || } + <<: <= = => > >-> >= ? @ @{ [ ] _ + `( `{ { {| | } + + The following character sequences are tokens defined in notations or plugins + loaded in the :term:`prelude`:: + + ** [= |- || -> + + Note that loading additional modules or plugins may expand the set of defined + tokens. When multiple tokens match the beginning of a sequence of characters, the longest matching token is used. diff --git a/doc/sphinx/practical-tools/coq-commands.rst b/doc/sphinx/practical-tools/coq-commands.rst index 545bba4930..d4ceffac9f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -151,7 +151,7 @@ and ``coqtop``, unless stated otherwise: while processing options such as -R and -Q. By default, only the conventional version control management directories named CVS and_darcs are excluded. -:-nois: Start from an empty state instead of loading the Init.Prelude +:-nois, -noinit: Start from an empty state instead of loading the `Init.Prelude` module. :-init-file *file*: Load *file* as the resource file instead of loading the default resource file from the standard configuration @@ -163,32 +163,53 @@ and ``coqtop``, unless stated otherwise: |Coq| script from *file.v*. Write its contents to the standard output as it is executed. :-load-vernac-object *qualid*: Load |Coq| compiled library :n:`@qualid`. This - is equivalent to running :cmd:`Require` :n:`qualid`. + is equivalent to running :cmd:`Require` :n:`@qualid`. + + .. _interleave-command-line: + + .. note:: + + Note that the relative order of this command-line option and its + variants (`-rfrom`, `-ri`, `-re`, etc.) and of the `-set` and + `-unset` options matters since the various :cmd:`Require`, + :cmd:`Require Import`, :cmd:`Require Export`, :cmd:`Set` and + :cmd:`Unset` commands will be executed in the order specified on + the command-line. + :-rfrom *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid`. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. + This is equivalent to running :cmd:`From <From ... Require>` + :n:`@dirpath` :cmd:`Require <From ... Require>` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-ri *qualid*, -require-import *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. This is equivalent to running :cmd:`Require Import` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-re *qualid*, -require-export *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. This is equivalent to running :cmd:`Require Export` :n:`@qualid`. -:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and import it. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Import` :n:`@qualid`. -:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: Load |Coq| compiled library :n:`@qualid` and transitively import it. - This is equivalent to running :n:`From` :n:`@dirpath` :cmd:`Require Export` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. +:-rifrom *dirpath* *qualid*, -require-import-from *dirpath* *qualid*: + Load |Coq| compiled library :n:`@qualid` and import it. This is + equivalent to running :cmd:`From <From ... Require>` :n:`@dirpath` + :cmd:`Require Import <From ... Require>` :n:`@qualid`. See the + :ref:`note above <interleave-command-line>` regarding the order of + command-line options. +:-refrom *dirpath* *qualid*, -require-export-from *dirpath* *qualid*: + Load |Coq| compiled library :n:`@qualid` and transitively import it. + This is equivalent to running :cmd:`From <From ... Require>` + :n:`@dirpath` :cmd:`Require Export <From ... Require>` :n:`@qualid`. + See the :ref:`note above <interleave-command-line>` regarding the + order of command-line options. :-batch: Exit just after argument parsing. Available for ``coqtop`` only. -:-compile *file.v*: Deprecated; use ``coqc`` instead. Compile file *file.v* into *file.vo*. This option - implies -batch (exit just after argument parsing). It is available only - for `coqtop`, as this behavior is the purpose of ``coqc``. -:-compile-verbose *file.v*: Deprecated. Use ``coqc -verbose``. Same as -compile but also output the - content of *file.v* as it is compiled. :-verbose: Output the content of the input file as it is compiled. - This option is available for ``coqc`` only; it is the counterpart of - -compile-verbose. + This option is available for ``coqc`` only. :-vos: Indicate |Coq| to skip the processing of opaque proofs - (i.e., proofs ending with ``Qed`` or ``Admitted``), output a ``.vos`` files + (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files - when interpreting ``Require`` commands. + when interpreting :cmd:`Require` commands. :-vok: Indicate |Coq| to check a file completely, to load ``.vos`` files instead - of ``.vo`` files when interpreting ``Require`` commands, and to output an empty + of ``.vo`` files when interpreting :cmd:`Require` commands, and to output an empty ``.vok`` files upon success instead of writing a ``.vo`` file. :-w (all|none|w₁,…,wₙ): Configure the display of warnings. This option expects all, none or a comma-separated list of warning names or @@ -198,7 +219,7 @@ and ``coqtop``, unless stated otherwise: the output channel supports ANSI escape sequences. :-diffs (on|off|removed): *Coqtop only*. Controls highlighting of differences between proof steps. ``on`` highlights added tokens, ``removed`` highlights both added and - removed tokens. Requires that ``–color`` is enabled. (see Section + removed tokens. Requires that ``-color`` is enabled. (see Section :ref:`showing_diffs`). :-beautify: Pretty-print each command to *file.beautified* when compiling *file.v*, in order to get old-fashioned @@ -224,17 +245,25 @@ and ``coqtop``, unless stated otherwise: changes in the auto-generated name scheme. The options are provided to facilitate tracking down problems. :-set *string*: Enable flags and set options. *string* should be - ``Option Name=value``, the value is interpreted according to the - type of the option. For flags ``Option Name`` is equivalent to - ``Option Name=true``. For instance ``-set "Universe Polymorphism"`` + :n:`@setting_name=value`, the value is interpreted according to the + type of the option. For flags :n:`@setting_name` is equivalent to + :n:`@setting_name=true`. For instance ``-set "Universe Polymorphism"`` will enable :flag:`Universe Polymorphism`. Note that the quotes are - shell syntax, Coq does not see them. Flags are processed after initialization - of the document. This includes the `Prelude` if loaded and any libraries loaded - through the `-l`, `-lv`, `-r`, `-re`, `-ri`, `rfrom`, `-refrom` and `-rifrom` - options. + shell syntax, Coq does not see them. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. :-unset *string*: As ``-set`` but used to disable options and flags. -:-compat *version*: Attempt to maintain some backward-compatibility - with a previous version. + *string* must be :n:`"@setting_name"`. + See the :ref:`note above <interleave-command-line>` regarding the order + of command-line options. +:-compat *version*: Load a file that sets a few options to maintain + partial backward-compatibility with a previous version. This is + equivalent to :cmd:`Require Import` `Coq.Compat.CoqXXX` with `XXX` + one of the last three released versions (including the current + version). Note that the :ref:`explanations above + <interleave-command-line>` regarding the order of command-line + options apply, and this could be relevant if you are resetting some + of the compatibility options. :-dump-glob *file*: Dump references for global names in file *file* (to be used by coqdoc, see :ref:`coqdoc`). By default, if *file.v* is being compiled, *file.glob* is used. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index b184311bef..90173d65bf 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -57,6 +57,8 @@ mode but it can also be used in toplevel definitions as shown below. .. note:: + - The grammar reserves the token ``||``. + - The infix tacticals ``… || …`` , ``… + …`` , and ``… ; …`` are associative. .. example:: diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index 35062e0057..1e35160205 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -213,25 +213,63 @@ There is dedicated syntax for list and array literals. Ltac Definitions ~~~~~~~~~~~~~~~~ -.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_term +.. cmd:: Ltac2 {? mutable} {? rec} @lident := @ltac2_value :name: Ltac2 This command defines a new global Ltac2 value. - For semantic reasons, the body of the Ltac2 definition must be a syntactical - value, that is, a function, a constant or a pure constructor recursively applied to - values. + The body of an Ltac2 definition is required to be a syntactical value + that is, a function, a constant, a pure constructor recursively applied to + values or a (non-recursive) let binding of a value in a value. + + .. productionlist:: coq + ltac2_value: fun `ltac2_var` => `ltac2_term` + : `ltac2_qualid` + : `ltac2_constructor` `ltac2_value` ... `ltac2_value` + : `ltac2_var` + : let `ltac2_var` := `ltac2_value` in `ltac2_value` If ``rec`` is set, the tactic is expanded into a recursive binding. If ``mutable`` is set, the definition can be redefined at a later stage (see below). -.. cmd:: Ltac2 Set @qualid := @ltac2_term +.. cmd:: Ltac2 Set @qualid {? as @lident} := @ltac2_term :name: Ltac2 Set This command redefines a previous ``mutable`` definition. Mutable definitions act like dynamic binding, i.e. at runtime, the last defined value for this entry is chosen. This is useful for global flags and the like. + The previous value of the binding can be optionally accessed using the `as` + binding syntax. + + .. example:: Dynamic nature of mutable cells + + .. coqtop:: all + + Ltac2 mutable x := true. + Ltac2 y := x. + Ltac2 Eval y. + Ltac2 Set x := false. + Ltac2 Eval y. + + .. example:: Interaction with recursive calls + + + .. coqtop:: all + + Ltac2 mutable rec f b := match b with true => 0 | _ => f true end. + Ltac2 Set f := fun b => + match b with true => 1 | _ => f true end. + Ltac2 Eval (f false). + Ltac2 Set f as oldf := fun b => + match b with true => 2 | _ => oldf false end. + Ltac2 Eval (f false). + + In the definition, the `f` in the body is resolved statically + because the definition is marked recursive. In the first re-definition, + the `f` in the body is resolved dynamically. This is witnessed by + the second re-definition. + Reduction ~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 3b5233502d..cf4d432f64 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -90,9 +90,7 @@ list of assertion commands is given in :ref:`Assertions`. The command .. cmd:: Save @ident :name: Save - Forces the name of the original goal to be :token:`ident`. This - command can only be used if the original goal - was opened using the :cmd:`Goal` command. + Forces the name of the original goal to be :token:`ident`. .. cmd:: Admitted @@ -821,7 +819,7 @@ in compacted hypotheses: .. .. image:: ../_static/diffs-coqide-compacted.png - :alt: coqide with Set Diffs on with compacted hyptotheses + :alt: coqide with Set Diffs on with compacted hypotheses Controlling the effect of proof editing commands ------------------------------------------------ diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 28c5359a04..4be18ccda9 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -286,7 +286,7 @@ example, the null and all list function(al)s can be defined as follows: .. coqtop:: all Variable d: Set. - Fixpoint null (s : list d) := + Definition null (s : list d) := if s is nil then true else false. Variable a : d -> bool. Fixpoint all (s : list d) : bool := diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8989dd29ab..127e4c6dbe 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -36,6 +36,18 @@ language will be described in Chapter :ref:`ltac`. Common elements of tactics -------------------------- +Reserved keywords +~~~~~~~~~~~~~~~~~ + +The tactics described in this chapter reserve the following keywords:: + + by using + +Thus, these keywords cannot be used as identifiers. It also declares +the following character sequences as tokens:: + + ** [= |- + .. _invocation-of-tactics: Invocation of tactics @@ -2832,6 +2844,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. If :n:`@ident` is a local definition of the form :n:`@ident := t`, 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 + goal. + .. note:: + When several hypotheses have the form :n:`@ident = t` or :n:`t = @ident`, the first one is used. @@ -2845,9 +2862,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: subst - This applies subst repeatedly from top to bottom to all identifiers of the + 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``. + 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. .. flag:: Regular Subst Tactic @@ -2873,6 +2892,15 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. hypotheses, which without the flag it may break. default. + .. exn:: Cannot find any non-recursive equality over :n:`@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. + + Raised when the variable is a section variable with indirect + dependencies in the goal. + .. tacn:: stepl @term :name: stepl @@ -3355,6 +3383,128 @@ the conversion in hypotheses :n:`{+ @ident}`. This is the most general syntax that combines the different variants. +.. tacn:: with_strategy @strategy_level_or_var [ {+ @smart_qualid } ] @ltac_expr3 + :name: with_strategy + + Executes :token:`ltac_expr3`, applying the alternate unfolding + behavior that the :cmd:`Strategy` command controls, but only for + :token:`ltac_expr3`. This can be useful for guarding calls to + reduction in tactic automation to ensure that certain constants are + never unfolded by tactics like :tacn:`simpl` and :tacn:`cbn` or to + ensure that unfolding does not fail. + + .. note:: + + This tactic unfortunately does not yet play well with tactic + internalization, resulting in interpretation-time errors when + you try to use it directly with opaque identifiers, as seen in + the first (failing) use of :tacn:`with_strategy` in the + following example. This can be worked around by binding the + identifier to an |Ltac| variable, and this issue should + disappear in a future version of |Coq|; see `#12179 + <https://github.com/coq/coq/issues/12179>`_. + + .. example:: + + .. coqtop:: all reset abort + + Opaque id. + Goal id 10 = 10. + Fail unfold id. + Fail with_strategy transparent [id] unfold id. + let id' := id in with_strategy transparent [id] unfold id'. + + .. warning:: + + Use this tactic with care, as effects do not persist past the + end of the proof script. Notably, this fine-tuning of the + conversion strategy is not in effect during :cmd:`Qed` nor + :cmd:`Defined`, so this tactic is most useful either in + combination with :tacn:`abstract`, which will check the proof + early while the fine-tuning is still in effect, or to guard + calls to conversion in tactic automation to ensure that, e.g., + :tacn:`unfold` does not fail just because the user made a + constant :cmd:`Opaque`. + + This can be illustrated with the following example involving the + factorial function. + + .. coqtop:: in reset + + Fixpoint fact (n : nat) : nat := + match n with + | 0 => 1 + | S n' => n * fact n' + end. + + Suppose now that, for whatever reason, we want in general to + unfold the :g:`id` function very late during conversion: + + .. coqtop:: in + + Strategy 1000 [id]. + + If we try to prove :g:`id (fact n) = fact n` by + :tacn:`reflexivity`, it will now take time proportional to + :math:`n!`, because |Coq| will keep unfolding :g:`fact` and + :g:`*` and :g:`+` before it unfolds :g:`id`, resulting in a full + computation of :g:`fact n` (in unary, because we are using + :g:`nat`), which takes time :math:`n!`. We can see this cross + the relevant threshold at around :math:`n = 9`: + + .. coqtop:: all abort + + Goal True. + Time assert (id (fact 8) = fact 8) by reflexivity. + Time assert (id (fact 9) = fact 9) by reflexivity. + + Note that behavior will be the same if you mark :g:`id` as + :g:`Opaque` because while most reduction tactics refuse to + unfold :g:`Opaque` constants, conversion treats :g:`Opaque` as + merely a hint to unfold this constant last. + + We can get around this issue by using :tacn:`with_strategy`: + + .. coqtop:: all + + Goal True. + Fail Timeout 1 assert (id (fact 100) = fact 100) by reflexivity. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] reflexivity. + + However, when we go to close the proof, we will run into + trouble, because the reduction strategy changes are local to the + tactic passed to :tacn:`with_strategy`. + + .. coqtop:: all abort fail + + exact I. + Timeout 1 Defined. + + We can fix this issue by using :tacn:`abstract`: + + .. coqtop:: all + + Goal True. + Time assert (id (fact 100) = fact 100) by with_strategy -1 [id] abstract reflexivity. + exact I. + Time Defined. + + On small examples this sort of behavior doesn't matter, but + because |Coq| is a super-linear performance domain in so many + places, unless great care is taken, tactic automation using + :tacn:`with_strategy` may not be robustly performant when + scaling the size of the input. + + .. warning:: + + In much the same way this tactic does not play well with + :cmd:`Qed` and :cmd:`Defined` without using :tacn:`abstract` as + an intermediary, this tactic does not play well with ``coqchk``, + even when used with :tacn:`abstract`, due to the inability of + tactics to persist information about conversion hints in the + proof term. See `#12200 + <https://github.com/coq/coq/issues/12200>`_ for more details. + Conversion tactics applied to hypotheses ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 1759264e87..7191444bac 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -817,13 +817,15 @@ described first. .. cmd:: Strategy {+ @strategy_level [ {+ @smart_qualid } ] } - .. insertprodn strategy_level strategy_level + .. insertprodn strategy_level strategy_level_or_var .. prodn:: strategy_level ::= opaque | @int | expand | transparent + strategy_level_or_var ::= @strategy_level + | @ident This command accepts the :attr:`local` attribute, which limits its effect to the current section or module, in which case the section and module diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index d72409e0d9..c5ec636d5f 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -618,6 +618,41 @@ the next command fails because p does not bind in the instance of n. Notation "[> a , .. , b <]" := (cons a .. (cons b nil) .., cons b .. (cons a nil) ..). +Notations with expressions used both as binder and term ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ + +It is possible to use parameters of the notation both in term and +binding position. Here is an example: + +.. coqtop:: in + + Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'. + Notation "▢_ n P" := (force n (fun n => P)) + (at level 0, n ident, P at level 9, format "▢_ n P"). + +.. coqtop:: all + + Check exists p, ▢_p (p >= 1). + +More generally, the parameter can be a pattern, as in the following +variant: + +.. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation "▢_ p P" := (force2 p (fun p => P)) + (at level 0, p pattern at level 0, P at level 9, format "▢_ p P"). + +.. coqtop:: all + + Check exists x y, ▢_(x,y) (x >= 1 /\ y >= 2). + +This support is experimental. For instance, the notation is used for +printing only if the occurrence of the parameter in term position +comes in the right-hand side before the occurrence in binding position. + .. _RecursiveNotations: Notations with recursive patterns @@ -1383,6 +1418,17 @@ Abbreviations exception, if the right-hand side is just of the form :n:`@@qualid`, this conventionally stops the inheritance of implicit arguments. + Like for notations, it is possible to bind binders in + abbreviations. Here is an example: + + .. coqtop:: in reset + + Definition force2 q (P:nat*nat -> Prop) := + (forall n', n' >= fst q -> forall p', p' >= snd q -> P q). + + Notation F p P := (force2 p (fun p => P)). + Check exists x y, F (x,y) (x >= 1 /\ y >= 2). + .. _numeral-notations: Numeral notations @@ -1714,6 +1760,11 @@ Tactic notations allow customizing the syntax of tactics. - a global reference of term - :tacn:`unfold` + * - ``smart_global`` + - :token:`smart_qualid` + - a global reference of term + - :tacn:`with_strategy` + * - ``constr`` - :token:`term` - a term @@ -1734,6 +1785,16 @@ Tactic notations allow customizing the syntax of tactics. - an integer - :tacn:`do` + * - ``strategy_level`` + - :token:`strategy_level` + - a strategy level + - + + * - ``strategy_level_or_var`` + - :token:`strategy_level_or_var` + - a strategy level + - :tacn:`with_strategy` + * - ``tactic`` - :token:`ltac_expr` - a tactic @@ -1766,18 +1827,24 @@ Tactic notations allow customizing the syntax of tactics. .. todo: notation doesn't support italics - .. note:: In order to be bound in tactic definitions, each syntactic - entry for argument type must include the case of a simple |Ltac| - identifier as part of what it parses. This is naturally the case for - ``ident``, ``simple_intropattern``, ``reference``, ``constr``, ... but not for ``integer``. - This is the reason for introducing a special entry ``int_or_var`` which - evaluates to integers only but which syntactically includes + .. note:: In order to be bound in tactic definitions, each + syntactic entry for argument type must include the case + of a simple |Ltac| identifier as part of what it + parses. This is naturally the case for ``ident``, + ``simple_intropattern``, ``reference``, ``constr``, ... + but not for ``integer`` nor for ``strategy_level``. This + is the reason for introducing special entries + ``int_or_var`` and ``strategy_level_or_var`` which + evaluate to integers or strategy levels only, + respectively, but which syntactically includes identifiers in order to be usable in tactic definitions. - .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` entries can be used in - primitive tactics or in other notations at places where a list of the - underlying entry can be used: entry is either ``constr``, ``hyp``, ``integer`` - or ``int_or_var``. + .. note:: The *entry*\ ``_list*`` and ``ne_``\ *entry*\ ``_list*`` + entries can be used in primitive tactics or in other + notations at places where a list of the underlying entry + can be used: entry is either ``constr``, ``hyp``, + ``integer``, ``smart_qualid``, ``strategy_level``, + ``strategy_level_or_var``, or ``int_or_var``. .. rubric:: Footnotes diff --git a/doc/sphinx/using/libraries/writing.rst b/doc/sphinx/using/libraries/writing.rst index 801d492acb..325ea2af60 100644 --- a/doc/sphinx/using/libraries/writing.rst +++ b/doc/sphinx/using/libraries/writing.rst @@ -62,7 +62,7 @@ deprecated compatibility alias using :cmd:`Notation (abbreviation)` Definition bar x := S x. #[deprecated(since="1.2", note="Use bar instead.")] - Notation foo := bar. + Notation foo := bar (only parsing). Then, the following code still works, but emits a warning: |