Review #2

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`,

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