Chapter 4: Fixing ambiguity about whether the return predicate refers

explicitly or implicitly to the variables in the as and in clauses +
formatting.

1 files changed, 24 insertions, 14 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 069f9fe185..69059a8fc9 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -1115,7 +1115,7 @@ conversion rule.
 From the logical point of view, we have built a type family by giving
 a set of constructors.  We want to capture the fact that we do not
 have any other way to build an object in this type. So when trying to
-prove a property $(P~m)$ for $m$ in an inductive definition it is
+prove a property about an object $m$ in an inductive definition it is
 enough to enumerate all the cases where $m$ starts with a different
 constructor.
 
@@ -1156,41 +1156,51 @@ in~\cite{Coq92}.  One is the definition by pattern-matching. The second one is a
 \subsubsection[The {\tt match\ldots with \ldots end} construction.]{The {\tt match\ldots with \ldots end} construction.\label{Caseexpr}
 \index{match@{\tt match\ldots with\ldots end}}}
 
-The basic idea of this destructor operation is that we have an object
-$m$ in an inductive type $I$ and we want to prove a property $(P~m)$
-which in general depends on $m$. For this, it is enough to prove the
+The basic idea of this operator is that we have an object
+$m$ in an inductive type $I$ and we want to prove a property
+which possibly depends on $m$. For this, it is enough to prove the
+property for $m = (c_i~u_1\ldots  u_{p_i})$ for each constructor of $I$.
+
+
+The basic idea of this operator is that we have an object
+$m$ in an inductive type $I$ and we want to prove a property
+which possibly depends on $m$. For this, it is enough to prove the
 property for $m = (c_i~u_1\ldots  u_{p_i})$ for each constructor of $I$.
 
 The \Coq{} term for this proof will be written~:
 \[\kw{match}~m~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
-  (c_n~x_{n1}...x_{np_n}) \Ra f_n~ \kw{end}\]
+  (c_n~x_{n1}~...~x_{np_n}) \Ra f_n~ \kw{end}\]
 In this expression, if
-$m$ is a term built from a constructor $(c_i~u_1\ldots u_{p_i})$ then
-the expression will behave as it is specified with $i$-th branch and
-will reduce to $f_i$ where the $x_{i1}$\ldots $x_{ip_i}$ are replaced
+$m$ eventually happens to evaluate to $(c_i~u_1\ldots u_{p_i})$ then
+the expression will behave as specified in its $i$-th branch and
+it will reduce to $f_i$ where the $x_{i1}$\ldots $x_{ip_i}$ are replaced
 by the $u_1\ldots u_p$ according to the $\iota$-reduction.
 
 Actually, for type-checking a \kw{match\ldots with\ldots end}
 expression we also need to know the predicate $P$ to be proved by case
 analysis. In the general case where $I$ is an inductively defined
-$n$-ary relation, $P$ is a $n+1$-ary relation: the $n$ first arguments
+$n$-ary relation, $P$ is a predicate over $n+1$ arguments: the $n$ first ones
 correspond to the arguments of $I$ (parameters excluded), and the last
 one corresponds to object $m$. \Coq{} can sometimes infer this
 predicate but sometimes not. The concrete syntax for describing this
 predicate uses the \kw{as\ldots in\ldots return} construction. For
 instance, let us assume that $I$ is an unary predicate with one
 parameter. The predicate is made explicit using the syntax~:
-\[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ (P~ x)
+\[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ P
  ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
-  (c_n~x_{n1}...x_{np_n}) \Ra f_n \kw{end}\]
+  (c_n~x_{n1}~...~x_{np_n}) \Ra f_n \kw{end}\]
 The \kw{as} part can be omitted if either the result type does not
 depend on $m$ (non-dependent elimination) or $m$ is a variable (in
-this case, the result type can depend on $m$). The \kw{in} part can be
+this case, $m$ can occur in $P$ where it is considered a bound variable).
+The \kw{in} part can be
 omitted if the result type does not depend on the arguments of
 $I$. Note that the arguments of $I$ corresponding to parameters
 \emph{must} be \verb!_!, because the result type is not generalized to
-all possible values of the parameters. The expression after \kw{in}
-must be seen as an \emph{inductive type pattern}. As a final remark,
+all possible values of the parameters. The other arguments of $I$
+(sometimes called indices in the litterature) have to be variables
+($a$ above) and these variables can occur in $P$ and bound in it.
+The expression after \kw{in}
+must be seen as an \emph{inductive type pattern}. Notice that
 expansion of implicit arguments and notations apply to this pattern.
 
 For the purpose of presenting the inference rules, we use a more