aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-04-12 17:17:18 +0200
committerGravatar Matej Kosik <m4tej.kosik@gmail.com>2016-04-12 17:30:49 +0200
commit2bd36760f84f1d79af63cdee4d5d53f289a51204 (patch)
treeb4ae97b2a8399cd1bb7b90232de0f9fcc3c2ab5d
parent4b4fc278887d33299aea32aceea93e9849a65855 (diff)
FIX: HTML version of Chapter 4 of the Reference Manual
-rw-r--r--doc/common/macros.tex4
-rw-r--r--doc/refman/RefMan-cic.tex257
2 files changed, 202 insertions, 59 deletions
diff --git a/doc/common/macros.tex b/doc/common/macros.tex
index 3b12f259b..bbc78a851 100644
--- a/doc/common/macros.tex
+++ b/doc/common/macros.tex
@@ -405,8 +405,8 @@
\newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](\begin{array}[t]{@{}l@{}}#3:=#4
\,)\end{array}$}}
%END LATEX
-%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#1)(#2:=#3\,)$}}
-%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$(#1)[#2](#3:=#4\,)$}}
+%HEVEA \newcommand{\NInd}[3]{\mbox{{\sf Ind}$(#2\,:=\,#3)$}}
+%HEVEA \newcommand{\Ind}[4]{\mbox{{\sf Ind}$[#2](#3\,:=\,#4)$}}
\newcommand{\Indp}[5]{\mbox{{\sf Ind}$_{#5}(#1)[#2](\begin{array}[t]{@{}l}#3:=#4
\,)\end{array}$}}
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 50f4dc133..b9c17d814 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -544,14 +544,43 @@ $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of param
\def\colon{@{\hskip.5em:\hskip.5em}}
The declaration for parameterized lists is:
+\begin{latexonly}
\vskip.5em
-\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]}
+\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
-
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎝</td>
+ <td style="width:120pt;text-align:center">[ <span style="font-family:monospace">list : Set → Set</span> ]</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">nil</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="text-align:left;font-family:monospace">∀A : Set, list A</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">cons</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="text-align:left;font-family:monospace">∀A : Set, A → list A → list A</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
\noindent which corresponds to the result of the \Coq\ declaration:
\begin{coq_example*}
Inductive list (A:Set) : Set :=
@@ -559,16 +588,64 @@ Inductive list (A:Set) : Set :=
| cons : A -> list A -> list A.
\end{coq_example*}
-\noindent The declaration for a mutual inductive definition of forests and trees is:
+\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is:
+\begin{latexonly}
\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]}
+\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
-
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">tree</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">Set</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">forest</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">Set</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">node</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">forest → tree</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">emptyf</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">forest</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">consf</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">tree → forest → forest</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
\noindent which corresponds to the result of the \Coq\
declaration:
\begin{coq_example*}
@@ -579,7 +656,8 @@ with forest : Set :=
| consf : tree -> forest -> forest.
\end{coq_example*}
-\noindent The declaration for a mutual inductive definition of even and odd is:
+\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is:
+\begin{latexonly}
\newcommand\GammaI{\left[\begin{array}{r \colon l}
\even & \nat\ra\Prop \\
\odd & \nat\ra\Prop
@@ -594,6 +672,54 @@ with forest : Set :=
\vskip.5em
\ind{1}{\GammaI}{\GammaC}
\vskip.5em
+\end{latexonly}
+\begin{rawhtml}<pre><table style="border-spacing:0">
+ <tr style="vertical-align:middle">
+ <td style="width:10pt;text-align:center;font-family:sans-serif;font-style:italic">Ind</td>
+ <td style="width:20pt;text-align:center">[1]</td>
+ <td style="width:5pt;text-align:center">⎛<br>⎜<br>⎝</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">nat → Prop</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">odd</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">nat → Prop</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎦</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:=</td>
+ <td style="width:10pt;text-align:center">⎡<br>⎢<br>⎣</td>
+ <td>
+ <table style="border-spacing:0">
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even_O</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">even O</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">even_S</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">∀n : nat, odd n → even (S n)</td>
+ </tr>
+ <tr>
+ <td style="width:20pt;text-align:right;font-family:monospace">odd_S</td>
+ <td style="width:20pt;text-align:center;font-family:monospace">:</td>
+ <td style="text-align:left;font-family:monospace">∀n : nat, even n → odd (S n)</td>
+ </tr>
+ </table>
+ </td>
+ <td style="width:10pt;text-align:center">⎤<br>⎥<br>⎦</td>
+ <td style="width:5pt;text-align:center">⎞<br>⎟<br>⎠</td>
+ </tr>
+</table></pre>
+\end{rawhtml}
\noindent which corresponds to the result of the \Coq\
declaration:
\begin{coq_example*}
@@ -610,9 +736,9 @@ contains an inductive declaration.
\begin{description}
\item[Ind] \index{Typing rules!Ind}
- \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
+ \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(a:A)\in\Gamma_I}{\WTEG{a}{A}}}
\item[Constr] \index{Typing rules!Constr}
- \inference{\frac{\WFE{\Gamma}\hskip2em\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\hskip2em(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
+ \inference{\frac{\WFE{\Gamma}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}}
\end{description}
\begin{latexonly}%
@@ -726,19 +852,16 @@ 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{}}
+\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)}}
-%% \begin{figure}[H]
-For instance, if one considers the type
+\noindent For instance, if one considers the type
\begin{verbatim}
Inductive tree (A:Type) : Type :=
@@ -746,29 +869,49 @@ Inductive tree (A:Type) : Type :=
| node : A -> (nat -> tree A) -> tree A
\end{verbatim}
-Then every instantiated constructor of $\ListA$ satisfies the nested positivity condition for $\List$
-
+\begin{latexonly}
+\noindent 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 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 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 $\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\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}%
+\ws\ws\vv\\
+\ws\ws\vh\hh\ws concerning type $\ListA$ of constructor $\Nil$:\\
+\ws\ws\vv\ws\ws\ws\ws Type $\ListA$ of constructor $\Nil$ satisfies the positivity condition for $\List$\\
+\ws\ws\vv\ws\ws\ws\ws because $\List$ does not appear in any (real) arguments of the type of that constructor\\
+\ws\ws\vv\ws\ws\ws\ws (primarily because $\List$ does not have any (real) arguments)\ruleref1\\
+\ws\ws\vv\\
+\ws\ws\hv\hh\ws concerning type $\forall~A\ra\ListA\ra\ListA$ of constructor $\cons$:\\
+\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 satisfies the positivity condition for $\List$ because:\\
+\ws\ws\ws\ws\ws\ws\ws\vv\\
+\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\vv\\
+\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\vv\\
+\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\vv\\
+\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\List$ satisfies the positivity condition for $\ListA$\ruleref1
+\end{latexonly}
+\begin{rawhtml}
+<pre>
+<span style="font-family:serif">Then every instantiated constructor of <span style="font-family:monospace">list A</span> satisfies the nested positivity condition for <span style="font-family:monospace">list</span></span>
+ │
+ ├─ <span style="font-family:serif">concerning type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span>:</span>
+ │ <span style="font-family:serif">Type <span style="font-family:monospace">list A</span> of constructor <span style="font-family:monospace">nil</span> satisfies the positivity condition for <span style="font-family:monospace">list</span></span>
+ │ <span style="font-family:serif">because <span style="font-family:monospace">list</span> does not appear in any (real) arguments of the type of that constructor</span>
+ │ <span style="font-family:serif">(primarily because list does not have any (real) arguments) ... <span style="font-style:italic">(bullet 1)</span></span>
+ │
+ ╰─ <span style="font-family:serif">concerning type <span style="font-family:monospace">∀ A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span>:</span>
+ <span style="font-family:serif">Type <span style="font-family:monospace">∀ A : Type, A → list A → list A</span> of constructor <span style="font-family:monospace">cons</span></span>
+ <span style="font-family:serif">satisfies the positivity condition for <span style="font-family:monospace">list</span> because:</span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">Type</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">A</span> ... <span style="font-style:italic">(bullet 3)</span></span>
+ │
+ ├─ <span style="font-family:serif"><span style="font-family:monospace">list</span> occurs only strictly positively in <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 4)</span></span>
+ │
+ ╰─ <span style="font-family:serif"><span style="font-family:monospace">list</span> satisfies the positivity condition for <span style="font-family:monospace">list A</span> ... <span style="font-style:italic">(bullet 1)</span></span>
+</pre>
+\end{rawhtml}
\paragraph{Correctness rules.}
We shall now describe the rules allowing the introduction of a new
@@ -783,7 +926,7 @@ inductive definition.
\inference{
\frac{
(\WTE{\Gamma_P}{A_j}{s'_j})_{j=1\ldots k}
- ~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n}
+ ~~~~~~~~ (\WTE{\Gamma_I;\Gamma_P}{C_i}{s_{q_i}})_{i=1\ldots n}
}
{\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
provided that the following side conditions hold:
@@ -811,23 +954,23 @@ inductive definition.
The following declaration introduces the second-order existential
quantifier $\exists X.P(X)$.
\begin{coq_example*}
-Inductive exProp (P:Prop->Prop) : Prop
- := exP_intro : forall X:Prop, P X -> exProp P.
+Inductive exProp (P:Prop->Prop) : Prop :=
+ exP_intro : forall X:Prop, P X -> exProp P.
\end{coq_example*}
The same definition on \Set{} is not allowed and fails:
% (********** The following is not correct and should produce **********)
% (*** Error: Large non-propositional inductive types must be in Type***)
\begin{coq_example}
-Fail Inductive exSet (P:Set->Prop) : Set
- := exS_intro : forall X:Set, P X -> exSet P.
+Fail Inductive exSet (P:Set->Prop) : Set :=
+ exS_intro : forall X:Set, P X -> exSet P.
\end{coq_example}
It is possible to declare the same inductive definition in the
universe \Type.
The \texttt{exType} inductive definition has type $(\Type_i \ra\Prop)\ra
\Type_j$ with the constraint that the parameter \texttt{X} of \texttt{exT\_intro} has type $\Type_k$ with $k<j$ and $k\leq i$.
\begin{coq_example*}
-Inductive exType (P:Type->Prop) : Type
- := exT_intro : forall X:Type, P X -> exType P.
+Inductive exType (P:Type->Prop) : Type :=
+ exT_intro : forall X:Type, P X -> exType P.
\end{coq_example*}
%We shall assume for the following definitions that, if necessary, we
%annotated the type of constructors such that we know if the argument