Refman, ch. 4: A few fixes.

1 files changed, 89 insertions, 66 deletions

diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 3e50ac0de0..e3e49e115d 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -533,51 +533,76 @@ Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$
 such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as:
 $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}.
 
-\begin{latexonly}%
-  \def\captionstrut{\vbox to 1.5em{}}
-  \newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
+\paragraph{Examples}
+
+    \newcommand\ind[3]{$\mathsf{Ind}~[#1]\left(\hskip-.4em
     \begin{array}{r @{\mathrm{~:=~}} l}
       #2 & #3 \\
     \end{array}
     \hskip-.4em
     \right)$}
+    \def\colon{@{\hskip.5em:\hskip.5em}}
 
-  \def\colon{@{\hskip.5em:\hskip.5em}}
+The declaration for parameterized lists is:
+    \vskip.5em
 
-  \begin{figure}[H]
-    \strut If we take the following inductive definition:
-\begin{verbatim}
-Inductive even : nat -> Prop :=
-  | even_O : even 0
-  | even_S : forall n, odd n -> even (S n)
-with odd : nat -> Prop :=
-  | odd_S : forall n, even n -> odd (S n).
-\end{verbatim}
-    then:
-    \def\GammaI{\left[\begin{array}{r \colon l}
+\ind{1}{\List:\Set\ra\Set}{\left[\begin{array}{r \colon l}
+                        \Nil & \forall A:\Set,\List~A \\
+                        \cons & \forall A:\Set, A \ra \List~A \ra \List~A
+                        \end{array}\right]}
+    \vskip.5em
+
+which corresponds to the result of the \Coq\ declaration:
+\begin{coq_example*}
+Inductive list (A:Set) : Set :=
+  | nil : list A
+  | cons : A -> list A -> list A.
+\end{coq_example*}
+
+The declaration for a mutual inductive definition of forests and trees is:
+    \vskip.5em
+\ind{}{\left[\begin{array}{r \colon l}\tree&\Set\\\forest&\Set\end{array}\right]}
+      {\left[\begin{array}{r \colon l}
+            \node & \forest \ra \tree\\
+            \emptyf & \forest\\
+            \consf & \tree \ra \forest \ra \forest\\
+                      \end{array}\right]}
+    \vskip.5em
+ 
+which corresponds to the result of the \Coq\ 
+declaration:
+\begin{coq_example*}
+Inductive tree : Set :=
+    node : forest -> tree
+with forest : Set :=
+  | emptyf : forest
+  | consf : tree -> forest -> forest.
+\end{coq_example*}
+
+The declaration for a mutual inductive definition of even and odd is:
+    \newcommand\GammaI{\left[\begin{array}{r \colon l}
                         \even & \nat\ra\Prop \\
                         \odd & \nat\ra\Prop
                       \end{array}
                 \right]}
-    \def\GammaC{\left[\begin{array}{r \colon l}
+    \newcommand\GammaC{\left[\begin{array}{r \colon l}
                         \evenO & \even~\nO \\
                         \evenS & \forall n : \nat, \odd~n \ra \even~(\nS~n)\\
                         \oddS & \forall n : \nat, \even~n \ra \odd~(\nS~n)
                       \end{array}
                 \right]}
-    \begin{itemize}
-      \item $p = 1$
-      \item $\Gamma_I = \GammaI$
-      \item $\Gamma_C = \GammaC$
-      \item $\Gamma_P=[A:\Type]$.
-    \end{itemize}
-    and thus it enriches the global environment with the following entry:
     \vskip.5em
     \ind{1}{\GammaI}{\GammaC}
-    \caption{\captionstrut Formal representation of the {\even} and {\odd} inductive types.}
-    \label{fig:even:odd}
-  \end{figure}
-\end{latexonly}%
+    \vskip.5em
+which corresponds to the result of the \Coq\ 
+declaration:
+\begin{coq_example*}
+Inductive even : nat -> Prop :=
+  | even_O : even 0
+  | even_S : forall n, odd n -> even (S n)
+with odd : nat -> Prop :=
+  | odd_S : forall n, even n -> odd (S n).
+\end{coq_example*}
 
 \subsection{Types of inductive objects}
 We have to give the type of constants in a global environment $E$ which
@@ -595,7 +620,7 @@ contains an inductive declaration.
 Provided that our environment $E$ contains inductive definitions we showed before,
 these two inference rules above enable us to conclude that:
 \vskip.5em
-\def\prefix{E[\Gamma]\vdash\hskip.25em}
+\newcommand\prefix{E[\Gamma]\vdash\hskip.25em}
 $\begin{array}{@{} l}
    \prefix\even : \nat\ra\Prop\\
    \prefix\odd : \nat\ra\Prop\\
@@ -701,51 +726,49 @@ any $u_i$
 the type $V$ satisfies the nested positivity condition for $X$
 \end{itemize}
 
-\begin{latexonly}%
-  \newcommand\vv{\textSFxi}    % │
-  \newcommand\hh{\textSFx}     %   ─
-  \newcommand\vh{\textSFviii}  % ├
-  \newcommand\hv{\textSFii}    %   └
-  \newlength\framecharacterwidth
-  \settowidth\framecharacterwidth{\hh}
-  \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
-  \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
-  \def\captionstrut{\vbox to 1.5em{}}
-
-  \begin{figure}[H]
-    \ws\strut $X$ occurs strictly positively in $\ListA$\ruleref6\\
-    \ws\vv\\
-    \ws\vv\ws\verb|Inductive list (A:Type) : Type :=|\\
-    \ws\vv\ws\verb$  | nil : list A$\\
-    \ws\vv\ws\verb$  | cons : A -> list A -> list A$\\
-    \ws\vv\\
-    \ws\vh\hh $X$ does not occur in any (real) arguments of $\List$\\
-    \ws\vv\\
-    \ws\hv\hh\ws Every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $X$\\
+%% \begin{latexonly}%
+   \newcommand\vv{\textSFxi}    % │
+   \newcommand\hh{\textSFx}     %   ─
+   \newcommand\vh{\textSFviii}  % ├
+   \newcommand\hv{\textSFii}    %   └
+   \newlength\framecharacterwidth
+   \settowidth\framecharacterwidth{\hh}
+   \newcommand\ws{\hbox{}\hskip\the\framecharacterwidth}
+   \newcommand\ruleref[1]{\hskip.25em\dots\hskip.2em{\em (bullet #1)}}
+%%   \def\captionstrut{\vbox to 1.5em{}}
+
+%%   \begin{figure}[H]
+For instance, if one considers the type
+
+\begin{verbatim}
+Inductive tree (A:Type) : Type :=
+ | leaf : list A
+ | node : A -> (nat -> tree A) -> tree A
+\end{verbatim}
+
+Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$
+
+\noindent
     \ws\ws\ws\ws\vv\\
     \ws\ws\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the nested positivity condition for $X$\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws because $X$ does not appear in any (real) arguments of the type of that constructor\\
-    \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref7\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
+    \ws\ws\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
     \ws\ws\ws\ws\vv\\
     \ws\ws\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
     \ws\ws\ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra\ListA\ra\ListA$ of constructor $\cons$\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the nested positivity condition for $X$\ruleref8\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\List$ because:\\
     \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\Type$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\Type$\ruleref3\\
     \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $A\ra\ListA\ra\ListA$\ruleref8\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $A$\ruleref3\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA\ra\ListA$\ruleref8\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $X$ occurs only strictly positively in $\ListA$\ruleref4\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
-    \ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $X$ satisfies the nested positivity condition for $\ListA$\ruleref7
-    \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
-  \end{figure}
-\end{latexonly}%
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $A$\ruleref3\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\List$ occurs only strictly positively in $\ListA$\ruleref4\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\vv\\
+    \ws\ws\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+%%     \caption{\captionstrut A proof that $X$ occurs strictly positively in $\ListA$}
+%%   \end{figure}
+%% \end{latexonly}%
 
 \paragraph{Correctness rules.}
 We shall now describe the rules allowing the introduction of a new