diff options
Diffstat (limited to 'doc')
15 files changed, 191 insertions, 44 deletions
diff --git a/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst new file mode 100644 index 0000000000..e1fcfb78c4 --- /dev/null +++ b/doc/changelog/03-notations/8808-master+support-binder+term-in-abbrev.rst @@ -0,0 +1,4 @@ +- **Added:** + Abbreviations support arguments occurring both in term and binder position + (`#8808 <https://github.com/coq/coq/pull/8808>`_, + by Hugo Herbelin). diff --git a/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst new file mode 100644 index 0000000000..055006d3b4 --- /dev/null +++ b/doc/changelog/04-tactics/12146-master+fix10812-subst-failure-section-variables.rst @@ -0,0 +1,9 @@ +- **Changed:** + Tactic :tacn:`subst` :n:`@ident` now fails over a section variable which is + indirectly dependent in the goal; the incompatibility can generally + be fixed by first clearing the hypotheses causing an indirect + dependency, as reported by the error message, or by using :tacn:`rewrite` :n:`in *` + instead; similarly, :tacn:`subst` has no more effect on such variables + (`#12146 <https://github.com/coq/coq/pull/12146>`_, + by Hugo Herbelin; fixes `#10812 <https://github.com/coq/coq/pull/10812>`_; + fixes `#12139 <https://github.com/coq/coq/pull/12139>`_). diff --git a/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst new file mode 100644 index 0000000000..dc438f151e --- /dev/null +++ b/doc/changelog/04-tactics/12223-master+fix12152-locating-error-atomic-level.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Loss of location of some tactic errors + (`#12223 <https://github.com/coq/coq/pull/12223>`_, + by Hugo Herbelin; fixes + `#12152 <https://github.com/coq/coq/pull/12152>`_ and + `#12255 <https://github.com/coq/coq/pull/12255>`_). diff --git a/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst new file mode 100644 index 0000000000..0dd0fed4e2 --- /dev/null +++ b/doc/changelog/05-tactic-language/11503-ltac2-rebind-with-value.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 rebinding command :cmd:`Ltac2 Set` has been extended with the ability to + give a name to the old value so as to be able to reuse it inside the + new one + (`#11503 <https://github.com/coq/coq/pull/11503>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst new file mode 100644 index 0000000000..5ab2941446 --- /dev/null +++ b/doc/changelog/07-commands-and-options/11828-obligations+depr_hide_obligation.rst @@ -0,0 +1,9 @@ +- **Deprecated:** + Option :flag:`Hide Obligations` has been deprecated + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). + +- **Removed:** + Deprecated option ``Shrink Obligations`` has been removed + (`#11828 <https://github.com/coq/coq/pull/11828>`_, + by Emilio Jesus Gallego Arias). diff --git a/doc/changelog/10-standard-library/12008-ollibs-bool.rst b/doc/changelog/10-standard-library/12008-ollibs-bool.rst index 7c10d261a7..42e5eb96eb 100644 --- a/doc/changelog/10-standard-library/12008-ollibs-bool.rst +++ b/doc/changelog/10-standard-library/12008-ollibs-bool.rst @@ -1,5 +1,5 @@ - **Added:** - Order relations ``ltb`` and ``compareb`` added in ``Bool.Bool``. + Order relations ``lt`` and ``compare`` added in ``Bool.Bool``. Order properties for ``bool`` added in ``Bool.BoolOrder`` as well as two modules ``Bool_as_OT`` and ``Bool_as_DT`` in ``Structures.OrdersEx`` (`#12008 <https://github.com/coq/coq/pull/12008>`_, by Olivier Laurent). diff --git a/doc/changelog/10-standard-library/12162-bool-leb.rst b/doc/changelog/10-standard-library/12162-bool-leb.rst new file mode 100644 index 0000000000..6a4070a82e --- /dev/null +++ b/doc/changelog/10-standard-library/12162-bool-leb.rst @@ -0,0 +1,4 @@ +- **Deprecated:** + ``Bool.leb`` in favor of ``Bool.le``. The definition of ``Bool.le`` is made local to avoid conflicts with ``Nat.le``. As a consequence, previous calls to ``leb`` based on importing ``Bool`` should now be qualified into ``Bool.le`` even if ``Bool`` is imported. + (`#12162 <https://github.com/coq/coq/pull/12162>`_, + by Olivier Laurent). 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/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 ca167c8b4b..d4ceffac9f 100644 --- a/doc/sphinx/practical-tools/coq-commands.rst +++ b/doc/sphinx/practical-tools/coq-commands.rst @@ -202,14 +202,8 @@ and ``coqtop``, unless stated otherwise: 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 :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files instead of a ``.vo`` file, and to load ``.vos`` files instead of ``.vo`` files 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/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index bc2168411b..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 diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ea5ad79a80..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 |