diff options
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
-rw-r--r-- | doc/refman/RefMan-cic.tex | 77 |
1 files changed, 45 insertions, 32 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 9660a04b..6a132eba 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -41,7 +41,7 @@ The beginner can skip them. The reader seeking a background on the Calculus of Inductive Constructions may read several papers. Giménez and Castéran~\cite{GimCas05} provide -an introduction to inductive and coinductive definitions in Coq. In +an introduction to inductive and co-inductive definitions in Coq. In their book~\cite{CoqArt}, Bertot and Castéran give a precise description of the \CIC{} based on numerous practical examples. Barras~\cite{Bar99}, Werner~\cite{Wer94} and @@ -80,35 +80,48 @@ type $(P~n)$ and consequently represent proofs of the formula \subsection[Sorts]{Sorts\label{Sorts} \index{Sorts}} -Types are seen as terms of the language and then should belong to -another type. The type of a type is always a constant of the language -called a {\em sort}. - -The two basic sorts in the language of \CIC\ are \Set\ and \Prop. - -The sort \Prop\ intends to be the type of logical propositions. If -$M$ is a logical proposition then it denotes a class, namely the class -of terms representing proofs of $M$. An object $m$ belonging to $M$ -witnesses the fact that $M$ is true. An object of type \Prop\ is -called a {\em proposition}. - -The sort \Set\ intends to be the type of specifications. This includes -programs and the usual sets such as booleans, naturals, lists -etc. - -These sorts themselves can be manipulated as ordinary terms. -Consequently sorts also should be given a type. Because assuming -simply that \Set\ has type \Set\ leads to an inconsistent theory, we -have infinitely many sorts in the language of \CIC. These are, in -addition to \Set\ and \Prop\, a hierarchy of universes \Type$(i)$ -for any integer $i$. We call \Sort\ the set of sorts -which is defined by: +When manipulated as terms, types have themselves a type which is called a sort. + +There is an infinite well-founded typing hierarchy of sorts whose base +sorts are {\Prop} and {\Set}. + +The sort {\Prop} intends to be the type of logical propositions. If +$M$ is a logical proposition then it denotes the class of terms +representing proofs of $M$. An object $m$ belonging to $M$ witnesses +the fact that $M$ is provable. An object of type {\Prop} is called a +proposition. + +The sort {\Set} intends to be the type of small sets. This includes data +types such as booleans and naturals, but also products, subsets, and +function types over these data types. + +{\Prop} and {\Set} themselves can be manipulated as ordinary +terms. Consequently they also have a type. Because assuming simply +that {\Set} has type {\Set} leads to an inconsistent theory, the +language of {\CIC} has infinitely many sorts. There are, in addition +to {\Set} and {\Prop} a hierarchy of universes {\Type$(i)$} for any +integer $i$. + +Like {\Set}, all of the sorts {\Type$(i)$} contain small sets such as +booleans, natural numbers, as well as products, subsets and function +types over small sets. But, unlike {\Set}, they also contain large +sets, namely the sorts {\Set} and {\Type$(j)$} for $j<i$, and all +products, subsets and function types over these sorts. + +Formally, we call {\Sort} the set of sorts which is defined by: \[\Sort \equiv \{\Prop,\Set,\Type(i)| i \in \NN\} \] \index{Type@{\Type}} \index{Prop@{\Prop}} \index{Set@{\Set}} -The sorts enjoy the following properties: {\Prop:\Type(0)}, {\Set:\Type(0)} and - {\Type$(i)$:\Type$(i+1)$}. + +The sorts enjoy the following properties\footnote{In the Reference + Manual of versions of Coq prior to 8.4, the level of {\Type} typing + {\Prop} and {\Set} was numbered $0$. From Coq 8.4, it started to be + numbered $1$ so as to be able to leave room for re-interpreting + {\Set} in the hierarchy as {\Type$(0)$}. This change also put the + reference manual in accordance with the internal conventions adopted + in the implementation.}: {\Prop:\Type$(1)$}, {\Set:\Type$(1)$} and +{\Type$(i)$:\Type$(i+1)$}. The user will never mention explicitly the index $i$ when referring to the universe \Type$(i)$. One only writes \Type. The @@ -420,9 +433,9 @@ convertibility into an order inductively defined by: \begin{enumerate} \item if $\WTEGCONV{t}{u}$ then $\WTEGLECONV{t}{u}$, \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$, -\item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$, \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$, -\item $\WTEGLECONV{\Prop}{\Set}$, +\item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity, + $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$ \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T,T'}{\forall~x:U,U'}$. \end{enumerate} @@ -1650,12 +1663,12 @@ Abort. The principles of mutual induction can be automatically generated using the {\tt Scheme} command described in Section~\ref{Scheme}. -\section{Coinductive types} -The implementation contains also coinductive definitions, which are +\section{Co-inductive types} +The implementation contains also co-inductive definitions, which are types inhabited by infinite objects. -More information on coinductive definitions can be found +More information on co-inductive definitions can be found in~\cite{Gimenez95b,Gim98,GimCas05}. -%They are described in Chapter~\ref{Coinductives}. +%They are described in Chapter~\ref{Co-inductives}. \section[\iCIC : the Calculus of Inductive Construction with impredicative \Set]{\iCIC : the Calculus of Inductive Construction with |