From b247e84d1de761ffddb1c66414080ed3396b36ad Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Thu, 12 Mar 2020 22:34:01 -0700 Subject: [PATCH] Review #2 --- doc/sphinx/language/gallina-extensions.rst | 149 +++++++++--------- .../gallina-specification-language.rst | 10 +- 2 files changed, 78 insertions(+), 81 deletions(-) diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index bacc8b06d8f40..25fad8c0e078e 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -28,9 +28,9 @@ expressions. In this sense, the :cmd:`Record` construction allows defining If the constructor name is not specified, then the default name :n:`Build_@ident` is used, where :n:`@ident` is the record name. - If :n:`@type` (which must be a :n:`sort`??) is + If :n:`@type` is omitted, the default sort is :math:`\Type`. The identifiers inside the brackets are the field names. - The type of each field :n:`@ident`, its type is :n:`forall {* @binder }, @type`. + The type of each field :n:`@ident` is :n:`forall {* @binder }, @type`. Notice that the type of an identifier can depend on a previously-given identifier. Thus the order of the fields is important. :n:`@binder` parameters may be applied to the record as a whole or to individual fields. @@ -593,8 +593,8 @@ The following command is available when the ``FunInd`` library has been loaded v .. cmd:: Function @fix_definition {* with @fix_definition } This command is a generalization of :cmd:`Fixpoint`. It is a wrapper - for several ways of defining a function and other useful *related - objects*, namely: an induction principle that reflects the recursive + for several ways of defining a function *and* other useful related + objects, namely: an induction principle that reflects the recursive structure of the function (see :tacn:`function induction`) and its fixpoint equality. This defines a function similar to those defined by :cmd:`Fixpoint`. As in :cmd:`Fixpoint`, the decreasing argument must @@ -604,13 +604,69 @@ The following command is available when the ``FunInd`` library has been loaded v decreasing criteria must be used to ensure termination of recursive calls. -:cmd:`Function` also supports the :n:`with` clause to create -mutually recursive definitions, however this feature is limited -to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` -clause). - -See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use -the induction principle to reason easily about the function. + :cmd:`Function` also supports the :n:`with` clause to create + mutually recursive definitions, however this feature is limited + to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct` + clause). + + See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use + the induction principle to reason easily about the function. + + The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses: + + * If :n:`@fixannot` is not specified, :cmd:`Function` + defines the nonrecursive function :token:`ident` as if it was declared with + :cmd:`Definition`. In addition, the following are defined: + + + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, + which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); + + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); + + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which + are inversion information linking the function and its graph. + + * If :n:`{ struct ... }` is specified, :cmd:`Function` + defines the structural recursive function :token:`ident` as if it was declared + with :cmd:`Fixpoint`. In addition, the following are defined: + + + The same objects as above; + + The fixpoint equation of :token:`ident`: :n:`@ident`\_equation`. + + .. todo: these idents above are the not the one in { struct ident }, right? + AFAIK we don't describe the ident for struct anywhere + + * If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` + defines a recursive function by well-founded recursion. The module ``Recdef`` + of the standard library must be loaded for this feature. + + + :n:`{measure @one_term {? @ident } {? @one_term } }`\: where :n:`@ident` is the decreasing argument + and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which + the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) + for each recursive call of :n:`@one_term__1`. Parameters of the function are + bound in :n:`@one_term`. + + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and + :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type + `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument + decreases for each recursive call of :n:`@one_term`. The order must be well-founded. + Parameters of the function are bound in :n:`@one_term`. + + 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 + that the ordering relation is well-founded. Once proof obligations are + discharged, the following objects are defined: + + + The same objects as with the struct; + + The lemma `ident`\ :math:`_{\sf tcc}` which collects all proof obligations in one + property; + + The lemmas `ident`\ :math:`_{\sf terminate}` and `ident`\ :math:`_{\sf F}` which is needed to be inlined + during extraction of ident. + + The way this recursive function is defined is the subject of several + papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles + Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other + hand. Remark: Proof obligations are presented as several subgoals + belonging to a Lemma `ident`\ :math:`_{\sf tcc}`. .. note:: @@ -697,64 +753,6 @@ terminating functions. .. seealso:: :ref:`functional-scheme` and :tacn:`function induction` -.. todo I think everything from here to "Section mechanism" should appear before the Note above - -The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses: - -* If :n:`@fixannot` is not specified, :cmd:`Function` - defines the nonrecursive function :token:`ident` as if it was declared with - :cmd:`Definition`. In addition, the following are defined: - - + :token:`ident`\ ``_rect``, :token:`ident`\ ``_rec`` and :token:`ident`\ ``_ind``, - which reflect the pattern matching structure of :token:`term` (see :cmd:`Inductive`); - + The inductive :n:`R_@ident` corresponding to the graph of :token:`ident` (silently); - + :token:`ident`\ ``_complete`` and :token:`ident`\ ``_correct`` which - are inversion information linking the function and its graph. - -* If :n:`{ struct ... }` is specified, :cmd:`Function` - defines the structural recursive function :token:`ident` as if it was declared - with :cmd:`Fixpoint`. In addition, the following are defined: - - + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident`\_equation`. - - .. todo: these idents above are the not the one in { struct ident }, right? - AFAIK we don't describe the ident for struct anywhere - -* If :n:`{ measure ... }` or :n:`{ wf ... }` are specified, :cmd:`Function` - defines a recursive function by well-founded recursion. The module ``Recdef`` - of the standard library must be loaded for this feature. - - + :n:`{measure @one_term {? @ident } {? @one_term } }`\: where :n:`@ident` is the decreasing argument - and :n:`@one_term__1` is a function from the type of :n:`@ident` to :g:`nat` for which - the decreasing argument decreases (for the :g:`lt` order on :g:`nat`) - for each recursive call of :n:`@one_term__1`. Parameters of the function are - bound in :n:`@one_term`. - + :n:`{wf @one_term @ident }`\: where :n:`@ident` is the decreasing argument and - :n:`@one_term` is an ordering relation on the type of :n:`@ident` (i.e. of type - `T`\ :math:`_{\sf ident}` → `T`\ :math:`_{\sf ident}` → ``Prop``) for which the decreasing argument - decreases for each recursive call of :n:`@one_term`. The order must be well-founded. - Parameters of the function are bound in :n:`@one_term`. - - 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 - that the ordering relation is well-founded. Once proof obligations are - discharged, the following objects are defined: - - + The same objects as with the struct; - + The lemma `ident`\ :math:`_{\sf tcc}` which collects all proof obligations in one - property; - + The lemmas `ident`\ :math:`_{\sf terminate}` and `ident`\ :math:`_{\sf F}` which is needed to be inlined - during extraction of ident. - - The way this recursive function is defined is the subject of several - papers by Yves Bertot and Antonia Balaa on the one hand, and Gilles - Barthe, Julien Forest, David Pichardie, and Vlad Rusu on the other - hand. Remark: Proof obligations are presented as several subgoals - belonging to a Lemma `ident`\ :math:`_{\sf tcc}`. - .. _section-mechanism: Section mechanism @@ -827,21 +825,18 @@ 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 commands behave like :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 :token:`ident` - will be prefixed with a :n:`term_let` with the same declaration. + definitions and theorems within it that depend on the constant + will be prefixed with a :n:`@term_let` with the same declaration. - If :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing mode. + As for :cmd:`Definition`, :cmd:`Fixpoint` and :cmd:`CoFixpoint`, + if :n:`@term` is omitted, :n:`@type` is required and Coq enters proof editing 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`. - .. exn:: @ident already exists. - :name: @ident already exists. (Let) - :undocumented: - .. cmd:: Context {+ @binder } Declare variables in the context of the current section, like :cmd:`Variable`, diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 000253341fe59..8742160c34689 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -620,10 +620,11 @@ The association of a single fixpoint and a local definition have a special syntax: :n:`let fix @ident {* @binder } := @term in` stands for :n:`let @ident := fix @ident {* @binder } := @term in`. The same applies for co-fixpoints. -The :n:`wf` and :n:`measure` clauses are Gallina extensions. They can't be used in -commands that are processed by the |Coq| kernel, which doesn't support Gallina extensions. +Some options of :n:`@fixannot` are only supported in specific constructs. :n:`let fix` +only supports the :n:`struct` option, while :n:`wf` and :n:`measure` are only supported in +commands such as :cmd:`Function` and :cmd:`Program Fixpoint`. -.. todo what commands don't support them? I could list some or all of them +.. todo what commands don't support them? SVP, define "like". Is this a complete description? .. insertprodn term_cofix cofix_body @@ -1334,7 +1335,8 @@ constructions. system successively tries arguments from left to right until it finds one that satisfies the decreasing condition. - :cmd:`Fixpoint` does not support the the :n:`wf` or :n:`measure` clauses of :n:`fixannot`. + :cmd:`Fixpoint` without the :attr:`program` attribute does not support the + :n:`wf` or :n:`measure` clauses of :n:`@fixannot`. The :n:`with` clause allows simultaneously defining several mutual fixpoints. It is especially useful when defining functions over mutually defined