diff options
Diffstat (limited to 'doc/sphinx/language')
| -rw-r--r-- | doc/sphinx/language/gallina-extensions.rst | 98 | ||||
| -rw-r--r-- | doc/sphinx/language/gallina-specification-language.rst | 3 |
2 files changed, 76 insertions, 25 deletions
diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index c48964d66c..c93984661e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -603,11 +603,16 @@ The following experimental command is available when the ``FunInd`` library has The meaning of this declaration is to define a function ident, similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. The point of the {} annotation + necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation is to name the decreasing argument *and* to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. + .. productionlist:: + decrease_annot : struct `ident` + : measure `term` `ident` + : wf `term` `ident` + The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work for non structurally recursive functions. @@ -616,31 +621,33 @@ See the documentation of functional induction (:tacn:`function induction`) and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use the induction principle to easily reason about the function. -Remark: To obtain the right principle, it is better to put rigid -parameters of the function as first arguments. For example it is -better to define plus like this: +.. note:: -.. coqtop:: reset none + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: - Require Import FunInd. + .. coqtop:: reset none -.. coqtop:: all + Require Import FunInd. - Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. + .. coqtop:: all -than like this: + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. -.. coqtop:: reset all + than like this: - Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. + .. coqtop:: reset all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. *Limitations* @@ -710,7 +717,7 @@ used by ``Function``. A more precise description is given below. with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. + + The fixpoint equation of :token:`ident`: :token:`ident`\ ``_equation``. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term Function @ident {* @binder } { wf @term @ident } : @type := @term @@ -730,7 +737,7 @@ used by ``Function``. A more precise description is given below. decreases at each recursive call of :token:`term`. The order must be well-founded. Parameters of the function are bound in :token:`term`. - Depending on the annotation, the user is left with some proof + If the annotation is ``measure`` or ``fw``, the user is left with some proof obligations that will be used to define the function. These proofs are: proofs that each recursive call is actually decreasing with respect to the given criteria, and (if the criteria is `wf`) a proof @@ -1662,6 +1669,7 @@ Declaring Implicit Arguments of :token:`qualid`. .. cmd:: Arguments @qualid : clear implicits + :name: Arguments (clear implicits) This command clears implicit arguments. @@ -1738,6 +1746,7 @@ Automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ .. cmd:: Arguments @qualid : default implicits + :name: Arguments (default implicits) This command tells |Coq| to automatically detect what are the implicit arguments of a defined object. @@ -1907,7 +1916,8 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid {* @name} : @rename +.. cmd:: Arguments @qualid {* @name} : rename + :name: Arguments (rename) This command is used to redefine the names of implicit arguments. @@ -2293,7 +2303,7 @@ Printing universes language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. -.. cmdv:: Print Universes Subgraph(@names) +.. cmdv:: Print Universes Subgraph({+ @qualid }) :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting @@ -2438,3 +2448,45 @@ types and functions of a :g:`Uint63` module. Said module is not produced by extraction. Instead, it has to be provided by the user (if they want to compile or execute the extracted code). For instance, an implementation of this module can be taken from the kernel of Coq. + +Bidirectionality hints +---------------------- + +When type-checking an application, Coq normally does not use information from +the context to infer the types of the arguments. It only checks after the fact +that the type inferred for the application is coherent with the expected type. +Bidirectionality hints make it possible to specify that after type-checking the +first arguments of an application, typing information should be propagated from +the context to help inferring the types of the remaining arguments. + +.. cmd:: Arguments @qualid {* @ident__1 } & {* @ident__2} + :name: Arguments (bidirectionality hints) + + This commands tells the typechecking algorithm, when type-checking + applications of :n:`@qualid`, to first type-check the arguments in + :n:`@ident__1` and then propagate information from the typing context to + type-check the remaining arguments (in :n:`@ident__2`). + +.. example:: + + In a context where a coercion was declared from ``bool`` to ``nat``: + + .. coqtop:: in reset + + Definition b2n (b : bool) := if b then 1 else 0. + Coercion b2n : bool >-> nat. + + Coq cannot automatically coerce existential statements over ``bool`` to + statements over ``nat``, because the need for inserting a coercion is known + only from the expected type of a subterm: + + .. coqtop:: all + + Fail Check (ex_intro _ true _ : exists n : nat, n > 0). + + However, a suitable bidirectionality hint makes the example work: + + .. coqtop:: all + + Arguments ex_intro _ _ & _ _. + Check (ex_intro _ true _ : exists n : nat, n > 0). diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8acbcbec8f..ebaa6fde66 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : `qualid` : _ : `num` - : ( `or_pattern` , … , `or_pattern` ) - or_pattern : `pattern` | … | `pattern` + : ( `pattern` | … | `pattern` ) Types |