Review #2

Author: jfehrle

doc/sphinx/addendum/extraction.rst

@@ -106,7 +106,6 @@ Setting the target language
 
    .. prodn::
       language ::= OCaml
-      | Ocaml
       | Haskell
       | Scheme
       | JSON
@@ -232,7 +231,7 @@ principles of extraction (logical parts and types).
    Here :token:`qualid` can be
    any function or inductive constructor, and the :token:`ident`\s are
    the names of the useless arguments.  Arguments can can also be
-   identified positionally by :token:`int`\s starting from 1.
+   identified positionally by :token:`integer`\s starting from 1.
 
 When an actual extraction takes place, an error is normally raised if the
 :cmd:`Extraction Implicit` declarations cannot be honored, that is

doc/sphinx/addendum/generalized-rewriting.rst

@@ -534,8 +534,8 @@ pass additional arguments such as ``using relation``.
 .. tacn:: setoid_reflexivity
           setoid_symmetry {? in @ident }
           setoid_transitivity @one_term
-          setoid_rewrite {? {| -> | <- } } @constr_with_bindings {? at @occurrences } {? in @ident }
-          setoid_rewrite {? {| -> | <- } } @constr_with_bindings in @ident at @occurrences
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @occurrences } {? in @ident }
+          setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @occurrences
           setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 }
    :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace
 

doc/sphinx/addendum/implicit-coercions.rst

@@ -126,43 +126,43 @@ Declaring Coercions
 -------------------------
 
 .. cmd:: Coercion @reference : @class >-> @class
-         Coercion @qualid {? @univ_decl } @def_body
+         Coercion @ident {? @univ_decl } @def_body
 
    :name: Coercion; _
 
   The first form declares the construction denoted by :token:`reference` as a coercion between
   the two given classes.  The second form defines :token:`ident`
-  just like :n:`Definition @ident := term {? @type }`
+  just like :cmd:`Definition` :n:`@ident {? @univ_decl } @def_body`
   and then declares :token:`ident` as a coercion between it source and its target.
   Both forms support the :attr:`local` attribute, which makes the coercion local to the current section.
 
-  .. exn:: @qualid not declared.
+  .. exn:: @ident not declared.
      :undocumented:
 
-  .. exn:: @qualid is already a coercion.
+  .. exn:: @ident is already a coercion.
      :undocumented:
 
   .. exn:: Funclass cannot be a source class.
      :undocumented:
 
-  .. exn:: @qualid is not a function.
+  .. exn:: @ident is not a function.
      :undocumented:
 
-  .. exn:: Cannot find the source class of @qualid.
+  .. exn:: Cannot find the source class of @ident.
      :undocumented:
 
-  .. exn:: Cannot recognize @class as a source class of @qualid.
+  .. exn:: Cannot recognize @class as a source class of @ident.
      :undocumented:
 
-  .. warn:: @qualid does not respect the uniform inheritance condition.
+  .. warn:: @ident does not respect the uniform inheritance condition.
      :undocumented:
 
   .. exn:: Found target class ... instead of ...
      :undocumented:
 
   .. warn:: New coercion path ... is ambiguous with existing ...
 
-     When the coercion :token:`qualid` is added to the inheritance graph, new
+     When the coercion :token:`ident` is added to the inheritance graph, new
      coercion paths which have the same classes as existing ones are ignored.
      The :cmd:`Coercion` command tries to check the convertibility of new ones and
      existing ones. The paths for which this check fails are displayed by a warning
@@ -255,26 +255,9 @@ Classes as Records
 
 .. index:: :> (coercion)
 
-We allow the definition of *Structures with Inheritance* (or classes as records)
-by extending the existing :cmd:`Record` macro. Its new syntax is:
-
-.. todo PR Not sure how to merge this into the main definition...
-
-.. cmdv:: {| Record | Structure } {? >} @ident {* @binder } : @sort := {? @ident} { {+; @ident :{? >} @term } }
-
-   The first identifier :token:`ident` is the name of the defined record and
-   :token:`sort` is its type. The optional identifier after ``:=`` is the name
-   of the constructor (it will be :n:`Build_@ident` if not given).
-   The other identifiers are the names of the fields, and :token:`term`
-   are their respective types. If ``:>`` is used instead of ``:`` in
-   the declaration of a field, then the name of this field is automatically
-   declared as a coercion from the record name to the class of this
-   field type. Note that the fields always verify the uniform
-   inheritance condition. If the optional ``>`` is given before the
-   record name, then the constructor name is automatically declared as
-   a coercion from the class of the last field type to the record name
-   (this may fail if the uniform inheritance condition is not
-   satisfied).
+*Structures with Inheritance* may be defined using the :cmd:`Record` command.  Use `:>`
+in the field type to declare the field as a coercion from the record name to the class
+of the field type.  See :token:`of_type`.
 
 Coercions and Sections
 ----------------------

doc/sphinx/addendum/micromega.rst

@@ -250,7 +250,7 @@ proof by abstracting monomials by variables.
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
-.. tacn:: psatz @term {? @int_or_var }
+.. tacn:: psatz @one_term {? @int_or_var }
    :name: psatz
 
    This tactic explores the *Cone* by increasing degrees – hence the

doc/sphinx/addendum/nsatz.rst

@@ -5,8 +5,16 @@ Nsatz: tactics for proving equalities in integral domains
 
 :Author: Loïc Pottier
 
-.. tacn:: nsatz {? with radicalmax := @term strategy := @term parameters := @term variables := @term }
-   :name: nsatz
+
+To use the tactics described in this secion, load the ``Nsatz`` module with the
+command ``Require Import Nsatz``.  Alternatively, if you prefer not to transitively depend on the
+files that declare the axioms used to define the real numbers, you can
+``Require Import NsatzTactic`` instead; this will still allow
+:tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
+:math:`\mathbb{Q}` and any user-registered rings.
+
+
+.. tacn:: nsatz {? with radicalmax := @one_term strategy := @one_term parameters := @one_term variables := @one_term }
 
    This tactic is for solving goals of the form
 
@@ -34,42 +42,35 @@ Nsatz: tactics for proving equalities in integral domains
 
    `radicalmax`
      bound when searching for r such that
-     :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`
+     :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`.
+     This argument must be of type `N` (binary natural numbers).
 
    `strategy`
      gives the order on variables :math:`X_1,\ldots,X_n` and the strategy
      used in Buchberger algorithm (see :cite:`sugar` for details):
 
-       * strategy = 0: reverse lexicographic order and newest s-polynomial.
-       * strategy = 1: reverse lexicographic order and sugar strategy.
-       * strategy = 2: pure lexicographic order and newest s-polynomial.
-       * strategy = 3: pure lexicographic order and sugar strategy.
+       * `strategy := 0%Z`: reverse lexicographic order and newest s-polynomial.
+       * `strategy := 1%Z`: reverse lexicographic order and sugar strategy.
+       * `strategy := 2%Z`: pure lexicographic order and newest s-polynomial.
+       * `strategy := 3%Z`: pure lexicographic order and sugar strategy.
 
    `parameters`
-     list of variables :math:`X_{i_1},\ldots,X_{i_k}` among
+     a list of lists, each of type `@list R`, containing the variables :math:`X_{i_1},\ldots,X_{i_k}` among
      :math:`X_1,\ldots,X_n` which are considered as parameters: computation will be performed with
      rational fractions in these variables, i.e. polynomials are considered
      with coefficients in :math:`R(X_{i_1},\ldots,X_{i_k})`. In this case, the coefficient
      :math:`c` can be a non constant polynomial in :math:`X_{i_1},\ldots,X_{i_k}`, and the tactic
      produces a goal which states that :math:`c` is not zero.
 
    `variables`
-     list of the variables in the decreasing order in
-     which they will be used in the Buchberger algorithm. If `variables` = :g:`(@nil R)`,
+     a list of lists, each of type `@list R`, containing the variables in the decreasing order in
+     which they will be used in the Buchberger algorithm. If `variables` = :g:`(@[] R)`,
      then `lvar` is replaced by all the variables which are not in
      `parameters`.
 
    See the file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_
    for many examples, especially in geometry.
 
-   You can load the ``Nsatz`` module with the command ``Require Import Nsatz``.
-
-   Alternatively, if you prefer not to transitively depend on the
-   files declaring the axioms used to define the real numbers, you can
-   ``Require Import NsatzTactic`` instead; this will still allow
-   :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
-   :math:`\mathbb{Q}` and any user-registered rings.
-
 More about `nsatz`
 ---------------------
 

doc/sphinx/addendum/program.rst

@@ -33,7 +33,7 @@ obligations which need to be resolved to create the final term.
 .. _elaborating-programs:
 
 Elaborating programs
----------------------
+--------------------
 
 The main difference from |Coq| is that an object in a type :g:`T : Set` can
 be considered as an object of type :g:`{x : T | P}` for any well-formed
@@ -113,7 +113,7 @@ coercions.
 .. _syntactic_control:
 
 Syntactic control over equalities
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 To give more control over the generation of equalities, the
 type checker will fall back directly to |Coq|’s usual typing of dependent
@@ -158,12 +158,8 @@ prove some goals to construct the final definitions.
 Program Definition
 ~~~~~~~~~~~~~~~~~~
 
-.. todo PR need to understand this better.  Is there a reason this only has
-      a subset of the Definition syntax?  Maybe need to ask Matthieu
-
-.. cmd:: Program Definition @ident := @term
-
-   A variant of :cmd:`Definition`.  Types the value term in Russell and generates proof
+   A :cmd:`Definition` command with the :attr:`program` attribute types
+   the value term in Russell and generates proof
    obligations. Once solved using the commands shown below, it binds the
    final |Coq| term to the name :n:`@ident` in the environment.
 
@@ -199,20 +195,8 @@ Program Definition
 Program Fixpoint
 ~~~~~~~~~~~~~~~~
 
-.. cmd:: Program Fixpoint @fix_definition {* with @fix_definition }
-
-   The optional :n:`@fixannot` annotation can be one of:
-
-   + :g:`measure f R` where :g:`f` is a value of type :g:`X` computed on
-     any subset of the arguments and the optional term
-     :g:`R` is a relation on :g:`X`. :g:`X` defaults to :g:`nat` and :g:`R`
-     to :g:`lt`.
-
-   + :g:`wf R x` which is equivalent to :g:`measure x R`.
-
-   The structural fixpoint operator behaves just like the one of |Coq| (see
-   :cmd:`Fixpoint`), except it may also generate obligations. It works
-   with mutually recursive definitions too.
+   A :cmd:`Fixpoint` command with the :attr:`program` attribute may also generate obligations. It works
+   with mutually recursive definitions too.  For example:
 
 .. coqtop:: reset in
 
@@ -249,8 +233,6 @@ using the syntax:
      | _ => O
      end.
 
-
-
 .. caution:: When defining structurally recursive functions, the generated
    obligations should have the prototype of the currently defined
    functional in their context. In this case, the obligations should be
@@ -269,21 +251,20 @@ using the syntax:
 Program Lemma
 ~~~~~~~~~~~~~
 
-.. cmd:: Program Lemma @ident : @type
-
-   A variant of :cmd:`Lemma`. The Russell language can also be used to type statements of logical
-   properties. It will generate obligations, try to solve them
-   automatically and fail if some unsolved obligations remain. In this
-   case, one can first define the lemma’s statement using :cmd:`Program
-   Definition` and use it as the goal afterwards. Otherwise the proof
+   A :cmd:`Lemma` command with the :attr:`program` attribute uses the Russell
+   language to type statements of logical
+   properties. It generates obligations, tries to solve them
+   automatically and fails if some unsolved obligations remain. In this
+   case, one can first define the lemma’s statement using :cmd:`Definition`
+   and use it as the goal afterwards. Otherwise the proof
    will be started with the elaborated version as a goal. The
    :g:`Program` attribute can similarly be used as a prefix for
    :cmd:`Variable`, :cmd:`Hypothesis`, :cmd:`Axiom` etc.
 
 .. _solving_obligations:
 
 Solving obligations
---------------------
+-------------------
 
 The following commands are available to manipulate obligations. The
 optional identifier is used when multiple functions have unsolved
@@ -295,7 +276,7 @@ optional tactic is replaced by the default one if not specified.
 
    Sets the default obligation solving tactic applied to all obligations
    automatically, whether to solve them or when starting to prove one,
-   e.g. using :g:`Next`.
+   e.g. using :cmd:`Next Obligation`.
 
    This command supports the :attr:`local` and :attr:`global` attributes.
    :attr:`local` makes the setting last only for the current
@@ -310,7 +291,7 @@ optional tactic is replaced by the default one if not specified.
 
    Displays all remaining obligations.
 
-.. cmd:: Obligation @natural {? of @ident } {? : @term {? with @ltac_expr } }
+.. cmd:: Obligation @natural {? of @ident } {? : @type {? with @ltac_expr } }
 
    Start the proof of obligation :token:`natural`.