From 765bbc6d35457050a631f311e2fa1220529268df Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 13 Mar 2018 13:19:05 +0100 Subject: [Sphinx] Move chapter 4 to new infrastructure --- Makefile.doc | 2 +- doc/refman/RefMan-cic.tex | 1881 --------------------------------------- doc/refman/Reference-Manual.tex | 1 - doc/sphinx/language/cic.rst | 1881 +++++++++++++++++++++++++++++++++++++++ 4 files changed, 1882 insertions(+), 1883 deletions(-) delete mode 100644 doc/refman/RefMan-cic.tex create mode 100644 doc/sphinx/language/cic.rst diff --git a/Makefile.doc b/Makefile.doc index 0f424af09..10e8522d8 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -59,7 +59,7 @@ DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex REFMANCOQTEXFILES:=$(addprefix doc/refman/, \ RefMan-gal.v.tex \ RefMan-tac.v.tex \ - RefMan-cic.v.tex RefMan-lib.v.tex \ + RefMan-lib.v.tex \ RefMan-tacex.v.tex RefMan-syn.v.tex \ RefMan-oth.v.tex RefMan-ltac.v.tex \ RefMan-pro.v.tex RefMan-sch.v.tex \ diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex deleted file mode 100644 index 2695c5eee..000000000 --- a/doc/refman/RefMan-cic.tex +++ /dev/null @@ -1,1881 +0,0 @@ -\chapter[Calculus of Inductive Constructions]{Calculus of Inductive Constructions -\label{Cic} -\index{Cic@\textsc{CIC}} -\index{Calculus of Inductive Constructions}} -%HEVEA\cutname{cic.html} - -The underlying formal language of {\Coq} is a {\em Calculus of -Inductive Constructions} (\CIC) whose inference rules are presented in -this chapter. The history of this formalism as well as pointers to related work -are provided in a separate chapter; see {\em Credits}. - -\section[The terms]{The terms\label{Terms}} - -The expressions of the {\CIC} are {\em terms} and all terms have a {\em type}. -There are types for functions (or -programs), there are atomic types (especially datatypes)... but also -types for proofs and types for the types themselves. -Especially, any object handled in the formalism must belong to a -type. For instance, universal quantification is relative to a type and -takes the form {\it ``for all x -of type T, P''}. The expression {\it ``x of type T''} is -written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as -{\it ``x belongs to T''}. - -The types of types are {\em sorts}. Types and sorts are themselves -terms so that terms, types and sorts are all components of a common -syntactic language of terms which is described in -Section~\ref{cic:terms} but, first, we describe sorts. - -\subsection[Sorts]{Sorts\label{Sorts} -\index{Sorts}} -All sorts have a type and 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~\cite{Coq86}, 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}~ u$ in \Coq{} concrete syntax) is a term. This is a - notation for the $\lambda$-abstraction of - $\lambda$-calculus\index{lambda-calculus@$\lambda$-calculus} - \cite{Bar81}. The term $\lb x:T \mto u$ is a function which maps - elements of $T$ to the expression $u$. -\item if $t$ and $u$ are terms then $(t\ u)$ is a term - ($t~u$ in \Coq{} concrete syntax). The term $(t\ - u)$ reads as {\it ``t applied to u''}. -\item if $x$ is a variable, and $t$, $T$ and $u$ are terms then - $\kw{let}~x:=t:T~\kw{in}~u$ is a - term which denotes the term $u$ where the variable $x$ is locally - bound to $t$ of type $T$. This stands for the common ``let-in'' - construction of functional programs such as ML or Scheme. -%\item case ... -%\item fixpoint ... -%\item cofixpoint ... -\end{enumerate} - -\paragraph{Free variables.} -The notion of free variables is defined as usual. In the expressions -$\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$ -are bound. - -\paragraph[Substitution.]{Substitution.\index{Substitution}} -The notion of substituting a term $t$ to free occurrences of a -variable $x$ in a term $u$ is defined as usual. The resulting term -is written $\subst{u}{x}{t}$. - -\paragraph[The logical vs programming readings.]{The logical vs programming readings.} - -The constructions of the {\CIC} can be used to express both logical -and programming notions, accordingly to the Curry-Howard -correspondence between proofs and programs, and between propositions -and types~\cite{Cur58,How80,Bru72}. - -For instance, let us assume that \nat\ is the type of natural numbers -with zero element written $0$ and that ${\tt True}$ is the always true -proposition. Then $\ra$ is used both to denote $\nat\ra\nat$ which is -the type of functions from \nat\ to \nat, to denote ${\tt True}\ra{\tt - True}$ which is an implicative proposition, to denote $\nat \ra -\Prop$ which is the type of unary predicates over the natural numbers, -etc. - -Let us assume that ${\tt mult}$ is a function of type $\nat\ra\nat\ra -\nat$ and ${\tt eqnat}$ a predicate of type $\nat\ra\nat\ra \Prop$. -The $\lambda$-abstraction can serve to build ``ordinary'' functions as -in $\lambda x:\nat.({\tt mult}~x~x)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~ -{\tt mult} ~x~x$ in {\Coq} notation) but may build also predicates -over the natural numbers. For instance $\lambda x:\nat.({\tt eqnat}~ -x~0)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~ {\tt eqnat}~ x~0$ in {\Coq} -notation) will represent the predicate of one variable $x$ which -asserts the equality of $x$ with $0$. This predicate has type $\nat -\ra \Prop$ and it can be applied to any expression of type ${\nat}$, -say $t$, to give an object $P~t$ of type \Prop, namely a proposition. - -Furthermore $\kw{forall}~x:\nat,\,P\;x$ will represent the type of -functions which associate to each natural number $n$ an object of type -$(P~n)$ and consequently represent the type of proofs of the formula -``$\forall x.\,P(x)$''. - -\section[Typing rules]{Typing rules\label{Typed-terms}} - -As objects of type theory, terms are subjected to {\em type -discipline}. The well typing of a term depends on -a global environment and a local context. - -\paragraph{Local context.\index{Local context}} -A {\em local context} is an ordered list of -{\em local declarations\index{declaration!local}} of names which we call {\em variables\index{variable}}. -The declaration of some variable $x$ is -either a {\em local assumption\index{assumption!local}}, written $x:T$ ($T$ is a type) or a {\em local definition\index{definition!local}}, -written $x:=t:T$. We use brackets to write local contexts. A -typical example is $[x:T;y:=u:U;z:V]$. Notice that the variables -declared in a local context must be distinct. If $\Gamma$ declares some $x$, -we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that -either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such -that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some -$x:=t:T$, we also write $(x:=t:T) \in \Gamma$. -For the rest of the chapter, the $\Gamma::(y:T)$ denotes the local context -$\Gamma$ enriched with the local assumption $y:T$. -Similarly, $\Gamma::(y:=t:T)$ denotes the local context -$\Gamma$ enriched with the local definition $(y:=t:T)$. -The notation $[]$ denotes the empty local context. -By $\Gamma_1; \Gamma_2$ we mean concatenation of the local context $\Gamma_1$ -and the local context $\Gamma_2$. - -% Does not seem to be used further... -% Si dans l'explication WF(E)[Gamma] concernant les constantes -% definies ds un contexte - -%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written -%as $\Gamma \subset \Delta$) as the property, for all variable $x$, -%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$ -%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. -%We write -% $|\Delta|$ for the length of the context $\Delta$, that is for the number -% of declarations (assumptions or definitions) in $\Delta$. - -\paragraph[Global environment.]{Global environment.\index{Global environment}} -%Because we are manipulating global declarations (global constants and global -%assumptions), we also need to consider a global environment $E$. - -A {\em global environment} is an ordered list of {\em global declarations\index{declaration!global}}. -Global declarations are either {\em global assumptions\index{assumption!global}} or {\em global -definitions\index{definition!global}}, but also declarations of inductive objects. Inductive objects themselves declare both inductive or coinductive types and constructors -(see Section~\ref{Cic-inductive-definitions}). - -A {\em global assumption} will be represented in the global environment as -$(c:T)$ which assumes the name $c$ to be of some type $T$. -A {\em global definition} will -be represented in the global environment as $c:=t:T$ which defines -the name $c$ to have value $t$ and type $T$. -We shall call such names {\em constants}. -For the rest of the chapter, the $E;c:T$ denotes the global environment -$E$ enriched with the global assumption $c:T$. -Similarly, $E;c:=t:T$ denotes the global environment -$E$ enriched with the global definition $(c:=t:T)$. - -The rules for inductive definitions (see Section -\ref{Cic-inductive-definitions}) have to be considered as assumption -rules to which the following definitions apply: if the name $c$ is -declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is -declared in $E$, we write $(c : T) \in E$. - -\paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}} -In the following, we define simultaneously two -judgments. The first one \WTEG{t}{T} means the term $t$ is well-typed -and has type $T$ in the global environment $E$ and local context $\Gamma$. The -second judgment \WFE{\Gamma} means that the global environment $E$ is -well-formed and the local context $\Gamma$ is a valid local context in this -global environment. -% HH: This looks to me complicated. I think it would be better to talk -% about ``discharge'' as a transformation of global environments, -% rather than as keeping a local context next to global constants. -% -%% It also means a third property which makes sure that any -%%constant in $E$ was defined in an environment which is included in -%%$\Gamma$ -%%\footnote{This requirement could be relaxed if we instead introduced -%% an explicit mechanism for instantiating constants. At the external -%% level, the Coq engine works accordingly to this view that all the -%% definitions in the environment were built in a local sub-context of the -%% current local context.}. - -A term $t$ is well typed in a global environment $E$ iff there exists a -local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can -be derived from the following rules. -\begin{description} -\item[W-Empty] \inference{\WF{[]}{}} -\item[W-Local-Assum] % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma -\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E - }{\WFE{\Gamma::(x:T)}}} -\item[W-Local-Def] -\inference{\frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E - }{\WFE{\Gamma::(x:=t:T)}}} -\item[W-Global-Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E} - {\WF{E;c:T}{}}} -\item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E} - {\WF{E;c:=t:T}{}}} -\item[Ax-Prop] \index{Typing rules!Ax-Prop} -\inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}} -\item[Ax-Set] \index{Typing rules!Ax-Set} -\inference{\frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}} -\item[Ax-Type] \index{Typing rules!Ax-Type} -\inference{\frac{\WFE{\Gamma}}{\WTEG{\Type(i)}{\Type(i+1)}}} -\item[Var]\index{Typing rules!Var} - \inference{\frac{ \WFE{\Gamma}~~~~~(x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}} -\item[Const] \index{Typing rules!Const} -\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} }{\WTEG{c}{T}}} -\item[Prod-Prop] \index{Typing rules!Prod-Prop} -\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~ - \WTE{\Gamma::(x:T)}{U}{\Prop}} - { \WTEG{\forall~x:T,U}{\Prop}}} -\item[Prod-Set] \index{Typing rules!Prod-Set} -\inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~ - \WTE{\Gamma::(x:T)}{U}{\Set}} - { \WTEG{\forall~x:T,U}{\Set}}} -\item[Prod-Type] \index{Typing rules!Prod-Type} -\inference{\frac{\WTEG{T}{\Type(i)}~~~~ - \WTE{\Gamma::(x:T)}{U}{\Type(i)}} - {\WTEG{\forall~x:T,U}{\Type(i)}}} -\item[Lam]\index{Typing rules!Lam} -\inference{\frac{\WTEG{\forall~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}} - {\WTEG{\lb x:T\mto t}{\forall x:T, U}}} -\item[App]\index{Typing rules!App} - \inference{\frac{\WTEG{t}{\forall~x:U,T}~~~~\WTEG{u}{U}} - {\WTEG{(t\ u)}{\subst{T}{x}{u}}}} -\item[Let]\index{Typing rules!Let} -\inference{\frac{\WTEG{t}{T}~~~~ \WTE{\Gamma::(x:=t:T)}{u}{U}} - {\WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}}} -\end{description} - -\Rem Prod$_1$ and Prod$_2$ typing-rules make sense if we consider the semantic -difference between {\Prop} and {\Set}: -\begin{itemize} - \item All values of a type that has a sort {\Set} are extractable. - \item No values of a type that has a sort {\Prop} are extractable. -\end{itemize} - -\Rem We may have $\kw{let}~x:=t:T~\kw{in}~u$ -well-typed without having $((\lb x:T\mto u)~t)$ well-typed (where -$T$ is a type of $t$). This is because the value $t$ associated to $x$ -may be used in a conversion rule (see Section~\ref{conv-rules}). - -\section[Conversion rules]{Conversion rules\index{Conversion rules} -\label{conv-rules}} - -In \CIC, there is an internal reduction mechanism. In particular, it -can decide if two programs are {\em intentionally} equal (one -says {\em convertible}). Convertibility is described in this section. - -\paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}} - -We want to be able to identify some terms as we can identify the -application of a function to a given argument with its result. For -instance the identity function over a given type $T$ can be written -$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the -application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a -{\em conversion}) rule we call $\beta$: -\[ \WTEGRED{((\lb x:T\mto - t)~u)}{\triangleright_{\beta}}{\subst{t}{x}{u}} \] -We say that $\subst{t}{x}{u}$ is the {\em $\beta$-contraction} of -$((\lb x:T\mto t)~u)$ and, conversely, that $((\lb x:T\mto t)~u)$ -is the {\em $\beta$-expansion} of $\subst{t}{x}{u}$. - -According to $\beta$-reduction, terms of the {\em Calculus of - Inductive Constructions} enjoy some fundamental properties such as -confluence, strong normalization, subject reduction. These results are -theoretically of great importance but we will not detail them here and -refer the interested reader to \cite{Coq85}. - -\paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}} -A specific conversion rule is associated to the inductive objects in -the global environment. We shall give later on (see Section~\ref{iotared}) the -precise rules but it just says that a destructor applied to an object -built from a constructor behaves as expected. This reduction is -called $\iota$-reduction and is more precisely studied in -\cite{Moh93,Wer94}. - - -\paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}} - -We may have variables defined in local contexts or constants defined in the global -environment. It is legal to identify such a reference with its value, -that is to expand (or unfold) it into its value. This -reduction is called $\delta$-reduction and shows as follows. - -$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T) \in \Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T) \in E$}$$ - - -\paragraph[$\zeta$-reduction.]{$\zeta$-reduction.\label{zeta}\index{zeta-reduction@$\zeta$-reduction}} - -{\Coq} allows also to remove local definitions occurring in terms by -replacing the defined variable by its value. The declaration being -destroyed, this reduction differs from $\delta$-reduction. It is -called $\zeta$-reduction and shows as follows. - -$$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ - -\paragraph{$\eta$-expansion.% -\label{eta}% -\index{eta-expansion@$\eta$-expansion}% -%\index{eta-reduction@$\eta$-reduction} -}% -Another important concept is $\eta$-expansion. It is legal to identify any -term $t$ of functional type $\forall x:T, U$ with its so-called -$\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable -name fresh in $t$. - -\Rem We deliberately do not define $\eta$-reduction: -\begin{latexonly}% - $$\lb x:T\mto (t\ x)\not\triangleright_\eta\hskip.3em t$$ -\end{latexonly}% -\begin{htmlonly} - $$\lb x:T\mto (t\ x)~\not\triangleright_\eta~t$$ -\end{htmlonly} -This is because, in general, the type of $t$ need not to be convertible to the type of $\lb x:T\mto (t\ x)$. -E.g., if we take $f$ such that: -\begin{latexonly}% - $$f\hskip.5em:\hskip.5em\forall x:Type(2),Type(1)$$ -\end{latexonly}% -\begin{htmlonly} - $$f~:~\forall x:Type(2),Type(1)$$ -\end{htmlonly} -then -\begin{latexonly}% - $$\lb x:Type(1),(f\, x)\hskip.5em:\hskip.5em\forall x:Type(1),Type(1)$$ -\end{latexonly}% -\begin{htmlonly} - $$\lb x:Type(1),(f\, x)~:~\forall x:Type(1),Type(1)$$ -\end{htmlonly} -We could not allow -\begin{latexonly}% - $$\lb x:Type(1),(f\,x)\hskip.4em\not\triangleright_\eta\hskip.6em f$$ -\end{latexonly}% -\begin{htmlonly} - $$\lb x:Type(1),(f\,x)~\not\triangleright_\eta~f$$ -\end{htmlonly} -because the type of the reduced term $\forall x:Type(2),Type(1)$ -would not be convertible to the type of the original term $\forall x:Type(1),Type(1)$. - -\paragraph[Convertibility.]{Convertibility.\label{convertibility} -\index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}} - -Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$. - -We say that two terms $t_1$ and $t_2$ are {\em - $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em - convertible}, or {\em equivalent}, in the global environment $E$ and -local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that -$\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and -$\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either -$u_1$ and $u_2$ are identical, or they are convertible up to -$\eta$-expansion, i.e. $u_1$ is $\lb x:T\mto u'_1$ and $u_2\,x$ is -recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb -x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We -then write $\WTEGCONV{t_1}{t_2}$. - -Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below) -convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e., -$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$. -Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$ -and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels) -such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$. - -The convertibility relation allows introducing a new typing rule -which says that two convertible well-formed types have the same -inhabitants. - -\section[Subtyping rules]{Subtyping rules\index{Subtyping rules} -\label{subtyping-rules}} - -At the moment, we did not take into account one rule between universes -which says that any term in a universe of index $i$ is also a term in -the universe of index $i+1$ (this is the {\em cumulativity} rule of -{\CIC}). This property extends the equivalence relation of -convertibility into a {\em subtyping} relation 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{\Set}{\Type(i)}$, -\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'}$. -\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full}) - inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$ - and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$ - are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors - \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\] - and - \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\] - respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) - if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have - \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\] - where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$. -\end{enumerate} - -The conversion rule up to subtyping is now exactly: - -\begin{description}\label{Conv} -\item[Conv]\index{Typing rules!Conv} - \inference{ - \frac{\WTEG{U}{s}~~~~\WTEG{t}{T}~~~~\WTEGLECONV{T}{U}}{\WTEG{t}{U}}} - \end{description} - - -\paragraph[Normal form.]{Normal form.\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}} -A term which cannot be any more reduced is said to be in {\em normal - form}. There are several ways (or strategies) to apply the reduction -rules. Among them, we have to mention the {\em head reduction} which -will play an important role (see Chapter~\ref{Tactics}). Any term can -be written as $\lb x_1:T_1\mto \ldots \lb x_k:T_k \mto -(t_0\ t_1\ldots t_n)$ where -$t_0$ is not an application. We say then that $t_0$ is the {\em head - of $t$}. If we assume that $t_0$ is $\lb x:T\mto u_0$ then one step of -$\beta$-head reduction of $t$ is: -\[\lb x_1:T_1\mto \ldots \lb x_k:T_k\mto (\lb x:T\mto u_0\ t_1\ldots t_n) -~\triangleright ~ \lb (x_1:T_1)\ldots(x_k:T_k)\mto -(\subst{u_0}{x}{t_1}\ t_2 \ldots t_n)\] -Iterating the process of head reduction until the head of the reduced -term is no more an abstraction leads to the {\em $\beta$-head normal - form} of $t$: -\[ t \triangleright \ldots \triangleright -\lb x_1:T_1\mto \ldots\lb x_k:T_k\mto (v\ u_1 -\ldots u_m)\] -where $v$ is not an abstraction (nor an application). Note that the -head normal form must not be confused with the normal form since some -$u_i$ can be reducible. -% -Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$ -reductions or any combination of those can also be defined. - -\section[Inductive definitions]{Inductive Definitions\label{Cic-inductive-definitions}} - -% Here we assume that the reader knows what is an inductive definition. - -Formally, we can represent any {\em inductive definition\index{definition!inductive}} as \Ind{}{p}{\Gamma_I}{\Gamma_C} where: -\begin{itemize} - \item $\Gamma_I$ determines the names and types of inductive types; - \item $\Gamma_C$ determines the names and types of constructors of these inductive types; - \item $p$ determines the number of parameters of these inductive types. -\end{itemize} -These inductive definitions, together with global assumptions and global definitions, then form the global environment. -% -Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$ -such that each $T$ in $(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}}. -Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as: -$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the -{\em Arity} of the inductive type\index{arity of inductive type} $t$ and -$\Sort$ is called the sort of the inductive type $t$. - -\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}} - -The declaration for parameterized lists is: -\begin{latexonly} - \vskip.5em - - \ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r@{:}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}

-  
-    
-    
-    
-    
-    
-    
-    
-    
-    
-  
-
Ind[1]⎛
⎝		[ list : Set → Set ]:=⎡
⎣		
-      
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-      
nil:=∀A : Set, list A
cons:=∀A : Set, A → list A → list A

-    		⎤
⎦		⎞
⎠
-\end{rawhtml} -\noindent 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*} - -\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is: -\begin{latexonly} - \vskip.5em -\ind{~}{\left[\begin{array}{r@{:}l}\tree&\Set\\\forest&\Set\end{array}\right]} - {\left[\begin{array}{r@{:}l} - \node & \forest \ra \tree\\ - \emptyf & \forest\\ - \consf & \tree \ra \forest \ra \forest\\ - \end{array}\right]} - \vskip.5em -\end{latexonly} -\begin{rawhtml}

-  
-    
-    
-    
-    
-    
-    
-    
-    
-    
-    
-    
-  
-
Ind[1]⎛
⎜
⎝		⎡
⎣		
-      
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-      
tree:Set
forest:Set

-    		⎤
⎦		:=⎡
⎢
⎣		
-      
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-      
node:forest → tree
emptyf:forest
consf:tree → forest → forest

-    		⎤
⎥
⎦		⎞
⎟
⎠
-\end{rawhtml} -\noindent 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*} - -\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is: -\begin{latexonly} - \newcommand\GammaI{\left[\begin{array}{r@{:}l} - \even & \nat\ra\Prop \\ - \odd & \nat\ra\Prop - \end{array} - \right]} - \newcommand\GammaC{\left[\begin{array}{r@{:}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]} - \vskip.5em - \ind{1}{\GammaI}{\GammaC} - \vskip.5em -\end{latexonly} -\begin{rawhtml}

-  
-    
-    
-    
-    
-    
-    
-    
-    
-    
-    
-    
-  
-
Ind[1]⎛
⎜
⎝		⎡
⎣		
-      
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-      
even:nat → Prop
odd:nat → Prop

-    		⎤
⎦		:=⎡
⎢
⎣		
-      
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-        
-          
-          
-          
-        
-      
even_O:even O
even_S:∀n : nat, odd n → even (S n)
odd_S:∀n : nat, even n → odd (S n)

-    		⎤
⎥
⎦		⎞
⎟
⎠
-\end{rawhtml} -\noindent 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 -contains an inductive declaration. - -\begin{description} -\item[Ind] \index{Typing rules!Ind} - \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}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}} -\end{description} - -\begin{latexonly}% -\paragraph{Example.} -Provided that our environment $E$ contains inductive definitions we showed before, -these two inference rules above enable us to conclude that: -\vskip.5em -\newcommand\prefix{E[\Gamma]\vdash\hskip.25em} -$\begin{array}{@{}l} - \prefix\even : \nat\ra\Prop\\ - \prefix\odd : \nat\ra\Prop\\ - \prefix\evenO : \even~\nO\\ - \prefix\evenS : \forall~n:\nat, \odd~n \ra \even~(\nS~n)\\ - \prefix\oddS : \forall~n:\nat, \even~n \ra \odd~(\nS~n) - \end{array}$ -\end{latexonly}% - -%\paragraph{Parameters.} -%%The parameters introduce a distortion between the inside specification -%%of the inductive declaration where parameters are supposed to be -%%instantiated (this representation is appropriate for checking the -%%correctness or deriving the destructor principle) and the outside -%%typing rules where the inductive objects are seen as objects -%%abstracted with respect to the parameters. - -%In the definition of \List\ or \haslength\, $A$ is a parameter because -%what is effectively inductively defined is $\ListA$ or $\haslengthA$ for -%a given $A$ which is constant in the type of constructors. But when -%we define $(\haslengthA~l~n)$, $l$ and $n$ are not parameters because the -%constructors manipulate different instances of this family. - -\subsection{Well-formed inductive definitions} -We cannot accept any inductive declaration because some of them lead -to inconsistent systems. -We restrict ourselves to definitions which -satisfy a syntactic criterion of positivity. Before giving the formal -rules, we need a few definitions: - -\paragraph[Definition]{Definition\index{Arity}\label{Arity}} -A type $T$ is an {\em arity of sort $s$} if it converts -to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity -of sort $s$. - -\paragraph[Examples]{Examples} -$A\ra \Set$ is an arity of sort $\Set$. -$\forall~A:\Prop,A\ra \Prop$ is an arity of sort \Prop. - -\paragraph[Definition]{Definition} -A type $T$ is an {\em arity} if there is a $s\in\Sort$ -such that $T$ is an arity of sort $s$. - -\paragraph[Examples]{Examples} -$A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities. - -\paragraph[Definition]{Definition\index{type of constructor}} -We say that $T$ is a {\em type of constructor of $I$\index{type of constructor}} -in one of the following two cases: -\begin{itemize} - \item $T$ is $(I~t_1\ldots ~t_n)$ - \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$ -\end{itemize} - -\paragraph[Examples]{Examples} -$\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\ -$\forall A:\Type,\List~A$ and $\forall A:\Type,A\ra\List~A\ra\List~A$ are constructors of $\List$. - -\paragraph[Definition]{Definition\index{Positivity}\label{Positivity}} -The type of constructor $T$ will be said to {\em satisfy the positivity -condition} for a constant $X$ in the following cases: - -\begin{itemize} -\item $T=(X~t_1\ldots ~t_n)$ and $X$ does not occur free in -any $t_i$ -\item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and -the type $V$ satisfies the positivity condition for $X$ -\end{itemize} -% -The constant $X$ {\em occurs strictly positively} in $T$ in the -following cases: -% -\begin{itemize} -\item $X$ does not occur in $T$ -\item $T$ converts to $(X~t_1 \ldots ~t_n)$ and $X$ does not occur in - any of $t_i$ -\item $T$ converts to $\forall~x:U,V$ and $X$ does not occur in - type $U$ but occurs strictly positively in type $V$ -\item $T$ converts to $(I~a_1 \ldots ~a_m ~ t_1 \ldots ~t_p)$ where - $I$ is the name of an inductive declaration of the form - $\Ind{\Gamma}{m}{I:A}{c_1:\forall p_1:P_1,\ldots \forall - p_m:P_m,C_1;\ldots;c_n:\forall p_1:P_1,\ldots \forall - p_m:P_m,C_n}$ - (in particular, it is not mutually defined and it has $m$ - parameters) and $X$ does not occur in any of the $t_i$, and the - (instantiated) types of constructor $C_i\{p_j/a_j\}_{j=1\ldots m}$ - of $I$ satisfy - the nested positivity condition for $X$ -%\item more generally, when $T$ is not a type, $X$ occurs strictly -%positively in $T[x:U]u$ if $X$ does not occur in $U$ but occurs -%strictly positively in $u$ -\end{itemize} -% -The type of constructor $T$ of $I$ {\em satisfies the nested -positivity condition} for a constant $X$ in the following -cases: - -\begin{itemize} -\item $T=(I~b_1\ldots b_m~u_1\ldots ~u_{p})$, $I$ is an inductive - definition with $m$ parameters and $X$ does not occur in -any $u_i$ -\item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and -the type $V$ satisfies the nested positivity condition for $X$ -\end{itemize} - -\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)}} -\newcommand{\NatTree}{\mbox{\textsf{nattree}}} -\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}} -\newcommand{\cnode}{\mbox{\textsf{node}}} -\newcommand{\cleaf}{\mbox{\textsf{leaf}}} - -\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers - -\begin{verbatim} -Inductive nattree (A:Type) : Type := - | leaf : nattree A - | node : A -> (nat -> nattree A) -> nattree A -\end{verbatim} - -\begin{latexonly} -\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\ -\noindent -\ws\ws\vv\\ -\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\ -\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\ -\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\ -\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\ -\ws\ws\vv\\ -\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\ - \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\ -\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\ -\ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\ -\ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\ -\ws\ws\ws\ws\ws\ws\ws\vv\\ - \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\ -\ws\ws\ws\ws\ws\ws\ws\vv\\ -\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1 -\end{latexonly} -\begin{rawhtml} -
-Then every instantiated constructor of nattree A satisfies the nested positivity condition for nattree
-  │
-  ├─ concerning type nattree A of constructor nil:
-  │    Type nattree A of constructor nil satisfies the positivity condition for nattree
-  │    because nattree does not appear in any (real) arguments of the type of that constructor
-  │    (primarily because nattree does not have any (real) arguments) ... (bullet 1)
-  │
-  ╰─ concerning type ∀ A → (nat → nattree A) → nattree A of constructor cons:
-       Type ∀ A : Type, A → (nat → nattree A) → nattree A of constructor cons
-       satisfies the positivity condition for nattree because:
-       │
-       ├─ nattree occurs only strictly positively in Type ... (bullet 1)
-       │
-       ├─ nattree occurs only strictly positively in A ... (bullet 1)
-       │
-       ├─ nattree occurs only strictly positively in nat → nattree A ... (bullet 3+2)
-       │
-       ╰─ nattree satisfies the positivity condition for nattree A ... (bullet 1)
-
-\end{rawhtml} - -\paragraph{Correctness rules.} -We shall now describe the rules allowing the introduction of a new -inductive definition. - -\begin{description} -\item[W-Ind] Let $E$ be a global environment and - $\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that - $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall - \Gamma_P,A_k]$ and $\Gamma_C$ is - $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$. -\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} -} - {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}} -provided that the following side conditions hold: -\begin{itemize} -\item $k>0$ and all of $I_j$ and $c_i$ are distinct names for $j=1\ldots k$ and $i=1\ldots n$, -\item $p$ is the number of parameters of \NInd{}{\Gamma_I}{\Gamma_C} - and $\Gamma_P$ is the context of parameters, -\item for $j=1\ldots k$ we have that $A_j$ is an arity of sort $s_j$ and $I_j - \notin E$, -\item for $i=1\ldots n$ we have that $C_i$ is a type of constructor of - $I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots I_k$ - and $c_i \notin \Gamma \cup E$. -\end{itemize} -\end{description} -One can remark that there is a constraint between the sort of the -arity of the inductive type and the sort of the type of its -constructors which will always be satisfied for the impredicative sort -{\Prop} but may fail to define inductive definition -on sort \Set{} and generate constraints between universes for -inductive definitions in the {\Type} hierarchy. - -\paragraph{Examples.} -It is well known that existential quantifier can be encoded as an -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. -\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. -\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 $kProp) : 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 -%is recursive or not. We shall write the type $(x:_R T)C$ if it is -%a recursive argument and $(x:_P T)C$ if the argument is not recursive. - -\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} -\label{Template-polymorphism} - -Inductive types declared in {\Type} are -polymorphic over their arguments in {\Type}. -If $A$ is an arity of some sort and $s$ is a sort, we write $A_{/s}$ for the arity -obtained from $A$ by replacing its sort with $s$. Especially, if $A$ -is well-typed in some global environment and local context, then $A_{/s}$ is typable -by typability of all products in the Calculus of Inductive Constructions. -The following typing rule is added to the theory. - -\begin{description} -\item[Ind-Family] Let $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ be an - inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$ - be its context of parameters, $\Gamma_I = [I_1:\forall - \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of - definitions and $\Gamma_C = [c_1:\forall - \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of - constructors, with $c_i$ a constructor of $I_{q_i}$. - - Let $m \leq p$ be the length of the longest prefix of parameters - such that the $m$ first arguments of all occurrences of all $I_j$ in - all $C_k$ (even the occurrences in the hypotheses of $C_k$) are - exactly applied to $p_1~\ldots~p_m$ ($m$ is the number of {\em - recursively uniform parameters} and the $p-m$ remaining parameters - are the {\em recursively non-uniform parameters}). Let $q_1$, - \ldots, $q_r$, with $0\leq r\leq m$, be a (possibly) partial - instantiation of the recursively uniform parameters of - $\Gamma_P$. We have: - -\inference{\frac -{\left\{\begin{array}{l} -\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\\ -(E[] \vdash q_l : P'_l)_{l=1\ldots r}\\ -(\WTELECONV{}{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\ -1 \leq j \leq k -\end{array} -\right.} -{E[] \vdash I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j}} -} - -provided that the following side conditions hold: - -\begin{itemize} -\item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by -replacing each $P_l$ that is an arity with $P'_l$ for $1\leq l \leq r$ (notice that -$P_l$ arity implies $P'_l$ arity since $\WTELECONV{}{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$); -\item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for - $\Gamma_{I'} = [I_1:\forall - \Gamma_{P'},(A_1)_{/s_1};\ldots;I_k:\forall \Gamma_{P'},(A_k)_{/s_k}]$ -we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots n}$; -\item the sorts $s_i$ are such that all eliminations, to {\Prop}, {\Set} and - $\Type(j)$, are allowed (see Section~\ref{allowedeleminationofsorts}). -\end{itemize} -\end{description} -% -Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf -Ind-Const} and {\bf App}, then it is typable using the rule {\bf -Ind-Family}. Conversely, the extended theory is not stronger than the -theory without {\bf Ind-Family}. We get an equiconsistency result by -mapping each $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ occurring into a -given derivation into as many different inductive types and constructors -as the number of different (partial) replacements of sorts, needed for -this derivation, in the parameters that are arities (this is possible -because $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ well-formed implies -that $\Ind{}{p}{\Gamma_{I'}}{\Gamma_{C'}}$ is well-formed and -has the same allowed eliminations, where -$\Gamma_{I'}$ is defined as above and $\Gamma_{C'} = [c_1:\forall -\Gamma_{P'},C_1;\ldots;c_n:\forall \Gamma_{P'},C_n]$). That is, -the changes in the types of each partial instance -$q_1\,\ldots\,q_r$ can be characterized by the ordered sets of arity -sorts among the types of parameters, and to each signature is -associated a new inductive definition with fresh names. Conversion is -preserved as any (partial) instance $I_j\,q_1\,\ldots\,q_r$ or -$C_i\,q_1\,\ldots\,q_r$ is mapped to the names chosen in the specific -instance of $\Ind{}{p}{\Gamma_I}{\Gamma_C}$. - -\newcommand{\Single}{\mbox{\textsf{Set}}} - -In practice, the rule {\bf Ind-Family} is used by {\Coq} only when all the -inductive types of the inductive definition are declared with an arity whose -sort is in the $\Type$ -hierarchy. Then, the polymorphism is over the parameters whose -type is an arity of sort in the {\Type} hierarchy. -The sort $s_j$ are -chosen canonically so that each $s_j$ is minimal with respect to the -hierarchy ${\Prop}\subset{\Set_p}\subset\Type$ where $\Set_p$ is -predicative {\Set}. -%and ${\Prop_u}$ is the sort of small singleton -%inductive types (i.e. of inductive types with one single constructor -%and that contains either proofs or inhabitants of singleton types -%only). -More precisely, an empty or small singleton inductive definition -(i.e. an inductive definition of which all inductive types are -singleton -- see paragraph~\ref{singleton}) is set in -{\Prop}, a small non-singleton inductive type is set in {\Set} (even -in case {\Set} is impredicative -- see Section~\ref{impredicativity}), -and otherwise in the {\Type} hierarchy. - -Note that the side-condition about allowed elimination sorts in the -rule~{\bf Ind-Family} is just to avoid to recompute the allowed -elimination sorts at each instance of a pattern-matching (see -section~\ref{elimdep}). -As an example, let us consider the following definition: -\begin{coq_example*} -Inductive option (A:Type) : Type := -| None : option A -| Some : A -> option A. -\end{coq_example*} -% -As the definition is set in the {\Type} hierarchy, it is used -polymorphically over its parameters whose types are arities of a sort -in the {\Type} hierarchy. Here, the parameter $A$ has this property, -hence, if \texttt{option} is applied to a type in {\Set}, the result is -in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop}, -then, the result is not set in \texttt{Prop} but in \texttt{Set} -still. This is because \texttt{option} is not a singleton type (see -section~\ref{singleton}) and it would lose the elimination to {\Set} and -{\Type} if set in {\Prop}. - -\begin{coq_example} -Check (fun A:Set => option A). -Check (fun A:Prop => option A). -\end{coq_example} -% -Here is another example. -% -\begin{coq_example*} -Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. -\end{coq_example*} -% -As \texttt{prod} is a singleton type, it will be in {\Prop} if applied -twice to propositions, in {\Set} if applied twice to at least one type -in {\Set} and none in {\Type}, and in {\Type} otherwise. In all cases, -the three kind of eliminations schemes are allowed. - -\begin{coq_example} -Check (fun A:Set => prod A). -Check (fun A:Prop => prod A A). -Check (fun (A:Prop) (B:Set) => prod A B). -Check (fun (A:Type) (B:Prop) => prod A B). -\end{coq_example} - -\Rem Template polymorphism used to be called ``sort-polymorphism of -inductive types'' before universe polymorphism (see -Chapter~\ref{Universes-full}) was introduced. - -\subsection{Destructors} -The specification of inductive definitions with arities and -constructors is quite natural. But we still have to say how to use an -object in an inductive type. - -This problem is rather delicate. There are actually several different -ways to do that. Some of them are logically equivalent but not always -equivalent from the computational point of view or from the user point -of view. - -From the computational point of view, we want to be able to define a -function whose domain is an inductively defined type by using a -combination of case analysis over the possible constructors of the -object and recursion. - -Because we need to keep a consistent theory and also we prefer to keep -a strongly normalizing reduction, we cannot accept any sort of -recursion (even terminating). So the basic idea is to restrict -ourselves to primitive recursive functions and functionals. - -For instance, assuming a parameter $A:\Set$ exists in the local context, we -want to build a function \length\ of type $\ListA\ra \nat$ which -computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$ -and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$. We want these -equalities to be recognized implicitly and taken into account in the -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 about an object $m$ in an inductive definition it is -enough to enumerate all the cases where $m$ starts with a different -constructor. - -In case the inductive definition is effectively a recursive one, we -want to capture the extra property that we have built the smallest -fixed point of this recursive equation. This says that we are only -manipulating finite objects. This analysis provides induction -principles. -For instance, in order to prove $\forall l:\ListA,(\haslengthA~l~(\length~l))$ -it is enough to prove: -% -\begin{itemize} - \item $(\haslengthA~(\Nil~A)~(\length~(\Nil~A)))$ - \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\ - \ra (\haslengthA~(\cons~A~a~l)~(\length~(\cons~A~a~l)))$ -\end{itemize} -% -which given the conversion equalities satisfied by \length\ is the -same as proving: -% -\begin{itemize} - \item $(\haslengthA~(\Nil~A)~\nO)$ - \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\ - \ra (\haslengthA~(\cons~A~a~l)~(\nS~(\length~l)))$ -\end{itemize} -% -One conceptually simple way to do that, following the basic scheme -proposed by Martin-L\"of in his Intuitionistic Type Theory, is to -introduce for each inductive definition an elimination operator. At -the logical level it is a proof of the usual induction principle and -at the computational level it implements a generic operator for doing -primitive recursion over the structure. - -But this operator is rather tedious to implement and use. We choose in -this version of {\Coq} to factorize the operator for primitive recursion -into two more primitive operations as was first suggested by Th. Coquand -in~\cite{Coq92}. One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. - -\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 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}\] -In this expression, if -$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_i}$ 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 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 and one argument. The predicate is made explicit using the syntax: -\[\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}\] -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, $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 other arguments of $I$ -(sometimes called indices in the literature) -% NOTE: e.g. http://www.qatar.cmu.edu/~sacchini/papers/types08.pdf -have to be variables -($a$ above) and these variables can occur in $P$. -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 -compact notation: -\[ \Case{(\lb a x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~ - \lb x_{n1}...x_{np_n} \mto f_n}\] - -%% CP 06/06 Obsolete avec la nouvelle syntaxe et incompatible avec la -%% presentation theorique qui suit -% \paragraph{Non-dependent elimination.} -% -% When defining a function of codomain $C$ by case analysis over an -% object in an inductive type $I$, we build an object of type $I -% \ra C$. The minimality principle on an inductively defined logical -% predicate $I$ of type $A \ra \Prop$ is often used to prove a property -% $\forall x:A,(I~x)\ra (C~x)$. These are particular cases of the dependent -% principle that we stated before with a predicate which does not depend -% explicitly on the object in the inductive definition. - -% For instance, a function testing whether a list is empty -% can be -% defined as: -% \[\kw{fun} l:\ListA \Ra \kw{match}~l~\kw{with}~ \Nil \Ra \true~ -% |~(\cons~a~m) \Ra \false \kw{end}\] -% represented by -% \[\lb l:\ListA \mto\Case{\bool}{l}{\true~ |~ \lb a~m,~\false}\] -%\noindent {\bf Remark. } - -% In the system \Coq\ the expression above, can be -% written without mentioning -% the dummy abstraction: -% \Case{\bool}{l}{\Nil~ \mbox{\tt =>}~\true~ |~ (\cons~a~m)~ -% \mbox{\tt =>}~ \false} - -\paragraph[Allowed elimination sorts.]{Allowed elimination sorts.\index{Elimination sorts}} -\label{allowedeleminationofsorts} - -An important question for building the typing rule for \kw{match} is -what can be the type of $\lb a x \mto P$ with respect to the type of $m$. If -$m:I$ and -$I:A$ and -$\lb a x \mto P : B$ -then by \compat{I:A}{B} we mean that one can use $\lb a x \mto P$ with $m$ in the above -match-construct. - -\paragraph{Notations.} -The \compat{I:A}{B} is defined as the smallest relation satisfying the -following rules: -We write \compat{I}{B} for \compat{I:A}{B} where $A$ is the type of -$I$. - -The case of inductive definitions in sorts \Set\ or \Type{} is simple. -There is no restriction on the sort of the predicate to be -eliminated. -% -\begin{description} -\item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}} - {\compat{I:\forall x:A, A'}{\forall x:A, B'}}} -\item[{\Set} \& \Type] \inference{\frac{ - s_1 \in \{\Set,\Type(j)\}~~~~~~~~s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}} -\end{description} -% -The case of Inductive definitions of sort \Prop{} is a bit more -complicated, because of our interpretation of this sort. The only -harmless allowed elimination, is the one when predicate $P$ is also of -sort \Prop. -\begin{description} -\item[\Prop] \inference{\compat{I:\Prop}{I\ra\Prop}} -\end{description} -\Prop{} is the type of logical propositions, the proofs of properties -$P$ in \Prop{} could not be used for computation and are consequently -ignored by the extraction mechanism. -Assume $A$ and $B$ are two propositions, and the logical disjunction -$A\vee B$ is defined inductively by: -\begin{coq_example*} -Inductive or (A B:Prop) : Prop := - or_introl : A -> or A B | or_intror : B -> or A B. -\end{coq_example*} -The following definition which computes a boolean value by case over -the proof of \texttt{or A B} is not accepted: -% (***************************************************************) -% (*** This example should fail with ``Incorrect elimination'' ***) -\begin{coq_example} -Fail Definition choice (A B: Prop) (x:or A B) := - match x with or_introl _ _ a => true | or_intror _ _ b => false end. -\end{coq_example} -From the computational point of view, the structure of the proof of -\texttt{(or A B)} in this term is needed for computing the boolean -value. - -In general, if $I$ has type \Prop\ then $P$ cannot have type $I\ra -\Set$, because it will mean to build an informative proof of type -$(P~m)$ doing a case analysis over a non-computational object that -will disappear in the extracted program. But the other way is safe -with respect to our interpretation we can have $I$ a computational -object and $P$ a non-computational one, it just corresponds to proving -a logical property of a computational object. - -% Also if $I$ is in one of the sorts \{\Prop, \Set\}, one cannot in -% general allow an elimination over a bigger sort such as \Type. But -% this operation is safe whenever $I$ is a {\em small inductive} type, -% which means that all the types of constructors of -% $I$ are small with the following definition:\\ -% $(I~t_1\ldots t_s)$ is a {\em small type of constructor} and -% $\forall~x:T,C$ is a small type of constructor if $C$ is and if $T$ -% has type \Prop\ or \Set. \index{Small inductive type} - -% We call this particular elimination which gives the possibility to -% compute a type by induction on the structure of a term, a {\em strong -% elimination}\index{Strong elimination}. - -In the same spirit, elimination on $P$ of type $I\ra -\Type$ cannot be allowed because it trivially implies the elimination -on $P$ of type $I\ra \Set$ by cumulativity. It also implies that there -are two proofs of the same property which are provably different, -contradicting the proof-irrelevance property which is sometimes a -useful axiom: -\begin{coq_example} -Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. -\end{coq_example} -\begin{coq_eval} -Reset proof_irrelevance. -\end{coq_eval} -The elimination of an inductive definition of type \Prop\ on a -predicate $P$ of type $I\ra \Type$ leads to a paradox when applied to -impredicative inductive definition like the second-order existential -quantifier \texttt{exProp} defined above, because it give access to -the two projections on this type. - -%\paragraph{Warning: strong elimination} -%\index{Elimination!Strong elimination} -%In previous versions of Coq, for a small inductive definition, only the -%non-informative strong elimination on \Type\ was allowed, because -%strong elimination on \Typeset\ was not compatible with the current -%extraction procedure. In this version, strong elimination on \Typeset\ -%is accepted but a dummy element is extracted from it and may generate -%problems if extracted terms are explicitly used such as in the -%{\tt Program} tactic or when extracting ML programs. - -\paragraph[Empty and singleton elimination]{Empty and singleton elimination\label{singleton} -\index{Elimination!Singleton elimination} -\index{Elimination!Empty elimination}} - -There are special inductive definitions in \Prop\ for which more -eliminations are allowed. -\begin{description} -\item[\Prop-extended] -\inference{ - \frac{I \mbox{~is an empty or singleton - definition}~~~s \in \Sort}{\compat{I:\Prop}{I\ra s}} -} -\end{description} -% -% A {\em singleton definition} has always an informative content, -% even if it is a proposition. -% -A {\em singleton -definition} has only one constructor and all the arguments of this -constructor have type \Prop. In that case, there is a canonical -way to interpret the informative extraction on an object in that type, -such that the elimination on any sort $s$ is legal. Typical examples are -the conjunction of non-informative propositions and the equality. -If there is an hypothesis $h:a=b$ in the local context, it can be used for -rewriting not only in logical propositions but also in any type. -% In that case, the term \verb!eq_rec! which was defined as an axiom, is -% now a term of the calculus. -\begin{coq_eval} -Require Extraction. -\end{coq_eval} -\begin{coq_example} -Print eq_rec. -Extraction eq_rec. -\end{coq_example} -An empty definition has no constructors, in that case also, -elimination on any sort is allowed. - -\paragraph{Type of branches.} -Let $c$ be a term of type $C$, we assume $C$ is a type of constructor -for an inductive type $I$. Let $P$ be a term that represents the -property to be proved. -We assume $r$ is the number of parameters and $p$ is the number of arguments. - -We define a new type \CI{c:C}{P} which represents the type of the -branch corresponding to the $c:C$ constructor. -\[ -\begin{array}{ll} -\CI{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm] -\CI{c:\forall~x:T,C}{P} &\equiv \forall~x:T,\CI{(c~x):C}{P} -\end{array} -\] -We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$. - -\paragraph{Example.} -The following term in concrete syntax: -\begin{verbatim} -match t as l return P' with -| nil _ => t1 -| cons _ hd tl => t2 -end -\end{verbatim} -can be represented in abstract syntax as $$\Case{P}{t}{f_1\,|\,f_2}$$ -where -\begin{eqnarray*} - P & = & \lambda~l~.~P^\prime\\ - f_1 & = & t_1\\ - f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 -\end{eqnarray*} -According to the definition: -\begin{latexonly}\vskip.5em\noindent\end{latexonly}% -\begin{htmlonly} - -\end{htmlonly} -$ \CI{(\Nil~\nat)}{P} \equiv \CI{(\Nil~\nat) : (\List~\nat)}{P} \equiv (P~(\Nil~\nat))$ -\begin{latexonly}\vskip.5em\noindent\end{latexonly}% -\begin{htmlonly} - -\end{htmlonly} -$ \CI{(\cons~\nat)}{P} - \equiv\CI{(\cons~\nat) : (\nat\ra\List~\nat\ra\List~\nat)}{P} \equiv\\ - \equiv\forall n:\nat, \CI{(\cons~\nat~n) : \List~\nat\ra\List~\nat)}{P} \equiv\\ - \equiv\forall n:\nat, \forall l:\List~\nat, \CI{(\cons~\nat~n~l) : \List~\nat)}{P} \equiv\\ -\equiv\forall n:\nat, \forall l:\List~\nat,(P~(\cons~\nat~n~l))$. -\begin{latexonly}\vskip.5em\noindent\end{latexonly}% -\begin{htmlonly} - -\end{htmlonly} -Given some $P$, then \CI{(\Nil~\nat)}{P} represents the expected type of $f_1$, and -\CI{(\cons~\nat)}{P} represents the expected type of $f_2$. - -\paragraph{Typing rule.} - -Our very general destructor for inductive definition enjoys the -following typing rule -% , where we write -% \[ -% \Case{P}{c}{[x_{11}:T_{11}]\ldots[x_{1p_1}:T_{1p_1}]g_1\ldots -% [x_{n1}:T_{n1}]\ldots[x_{np_n}:T_{np_n}]g_n} -% \] -% for -% \[ -% \Case{P}{c}{(c_1~x_{11}~...~x_{1p_1}) \Ra g_1 ~|~\ldots~|~ -% (c_n~x_{n1}...x_{np_n}) \Ra g_n } -% \] - -\begin{description} -\item[match] \label{elimdep} \index{Typing rules!match} -\inference{ -\frac{\WTEG{c}{(I~q_1\ldots q_r~t_1\ldots t_s)}~~ - \WTEG{P}{B}~~\compat{(I~q_1\ldots q_r)}{B} - ~~ -(\WTEG{f_i}{\CI{(c_{p_i}~q_1\ldots q_r)}{P}})_{i=1\ldots l}} -{\WTEG{\Case{P}{c}{f_1|\ldots |f_l}}{(P\ t_1\ldots t_s\ c)}}}%\\[3mm] - -provided $I$ is an inductive type in a definition -\Ind{}{r}{\Gamma_I}{\Gamma_C} with -$\Gamma_C = [c_1:C_1;\ldots;c_n:C_n]$ and $c_{p_1}\ldots c_{p_l}$ are the -only constructors of $I$. -\end{description} - -\paragraph{Example.} - -Below is a typing rule for the term shown in the previous example: -\inference{ - \frac{% - \WTEG{t}{(\List~\nat)}~~~~% - \WTEG{P}{B}~~~~% - \compat{(\List~\nat)}{B}~~~~% - \WTEG{f_1}{\CI{(\Nil~\nat)}{P}}~~~~% - \WTEG{f_2}{\CI{(\cons~\nat)}{P}}% - } -{\WTEG{\Case{P}{t}{f_1|f_2}}{(P~t)}}} - -\paragraph[Definition of $\iota$-reduction.]{Definition of $\iota$-reduction.\label{iotared} -\index{iota-reduction@$\iota$-reduction}} -We still have to define the $\iota$-reduction in the general case. - -A $\iota$-redex is a term of the following form: -\[\Case{P}{(c_{p_i}~q_1\ldots q_r~a_1\ldots a_m)}{f_1|\ldots | - f_l}\] -with $c_{p_i}$ the $i$-th constructor of the inductive type $I$ with $r$ -parameters. - -The $\iota$-contraction of this term is $(f_i~a_1\ldots a_m)$ leading -to the general reduction rule: -\[ \Case{P}{(c_{p_i}~q_1\ldots q_r~a_1\ldots a_m)}{f_1|\ldots | - f_n} \triangleright_{\iota} (f_i~a_1\ldots a_m) \] - -\subsection[Fixpoint definitions]{Fixpoint definitions\label{Fix-term} \index{Fix@{\tt Fix}}} -The second operator for elimination is fixpoint definition. -This fixpoint may involve several mutually recursive definitions. -The basic concrete syntax for a recursive set of mutually recursive -declarations is (with $\Gamma_i$ contexts): -\[\kw{fix}~f_1 (\Gamma_1) :A_1:=t_1~\kw{with} \ldots \kw{with}~ f_n -(\Gamma_n) :A_n:=t_n\] -The terms are obtained by projections from this set of declarations -and are written -\[\kw{fix}~f_1 (\Gamma_1) :A_1:=t_1~\kw{with} \ldots \kw{with}~ f_n -(\Gamma_n) :A_n:=t_n~\kw{for}~f_i\] -In the inference rules, we represent such a -term by -\[\Fix{f_i}{f_1:A_1':=t_1' \ldots f_n:A_n':=t_n'}\] -with $t_i'$ (resp. $A_i'$) representing the term $t_i$ abstracted -(resp. generalized) with -respect to the bindings in the context $\Gamma_i$, namely -$t_i'=\lb \Gamma_i \mto t_i$ and $A_i'=\forall \Gamma_i, A_i$. - -\subsubsection{Typing rule} -The typing rule is the expected one for a fixpoint. - -\begin{description} -\item[Fix] \index{Typing rules!Fix} -\inference{\frac{(\WTEG{A_i}{s_i})_{i=1\ldots n}~~~~ - (\WTE{\Gamma,f_1:A_1,\ldots,f_n:A_n}{t_i}{A_i})_{i=1\ldots n}} - {\WTEG{\Fix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}}{A_i}}} -\end{description} -% -Any fixpoint definition cannot be accepted because non-normalizing terms -allow proofs of absurdity. -% -The basic scheme of recursion that should be allowed is the one needed for -defining primitive -recursive functionals. In that case the fixpoint enjoys a special -syntactic restriction, namely one of the arguments belongs to an -inductive type, the function starts with a case analysis and recursive -calls are done on variables coming from patterns and representing subterms. -% -For instance in the case of natural numbers, a proof of the induction -principle of type -\[\forall P:\nat\ra\Prop, (P~\nO)\ra(\forall n:\nat, (P~n)\ra(P~(\nS~n)))\ra -\forall n:\nat, (P~n)\] -can be represented by the term: -\[\begin{array}{l} -\lb P:\nat\ra\Prop\mto\lb f:(P~\nO)\mto \lb g:(\forall n:\nat, -(P~n)\ra(P~(\nS~n))) \mto\\ -\Fix{h}{h:\forall n:\nat, (P~n):=\lb n:\nat\mto \Case{P}{n}{f~|~\lb - p:\nat\mto (g~p~(h~p))}} -\end{array} -\] -% -Before accepting a fixpoint definition as being correctly typed, we -check that the definition is ``guarded''. A precise analysis of this -notion can be found in~\cite{Gim94}. -% -The first stage is to precise on which argument the fixpoint will be -decreasing. The type of this argument should be an inductive -definition. -% -For doing this, the syntax of fixpoints is extended and becomes - \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\] -where $k_i$ are positive integers. -Each $k_i$ represents the index of pararameter of $f_i$, on which $f_i$ is decreasing. -Each $A_i$ should be a type (reducible to a term) starting with at least -$k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ -and $B_{k_i}$ an is unductive type. - -Now in the definition $t_i$, if $f_j$ occurs then it should be applied -to at least $k_j$ arguments and the $k_j$-th argument should be -syntactically recognized as structurally smaller than $y_{k_i}$ - - -The definition of being structurally smaller is a bit technical. -One needs first to define the notion of -{\em recursive arguments of a constructor}\index{Recursive arguments}. -For an inductive definition \Ind{}{r}{\Gamma_I}{\Gamma_C}, -if the type of a constructor $c$ has the form -$\forall p_1:P_1,\ldots \forall p_r:P_r, -\forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots -p_r~t_1\ldots t_s)$, then the recursive arguments will correspond to $T_i$ in -which one of the $I_l$ occurs. - -The main rules for being structurally smaller are the following:\\ -Given a variable $y$ of type an inductive -definition in a declaration -\Ind{}{r}{\Gamma_I}{\Gamma_C} -where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is - $[c_1:C_1;\ldots;c_n:C_n]$. -The terms structurally smaller than $y$ are: -\begin{itemize} -\item $(t~u)$ and $\lb x:u \mto t$ when $t$ is structurally smaller than $y$. -\item \Case{P}{c}{f_1\ldots f_n} when each $f_i$ is structurally - smaller than $y$. \\ - If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive - definition $I_p$ part of the inductive - declaration corresponding to $y$. - Each $f_i$ corresponds to a type of constructor $C_q \equiv - \forall p_1:P_1,\ldots,\forall p_r:P_r, \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$ - and can consequently be - written $\lb y_1:B'_1\mto \ldots \lb y_k:B'_k\mto g_i$. - ($B'_i$ is obtained from $B_i$ by substituting parameters variables) - the variables $y_j$ occurring - in $g_i$ corresponding to recursive arguments $B_i$ (the ones in - which one of the $I_l$ occurs) are structurally smaller than $y$. -\end{itemize} -The following definitions are correct, we enter them using the -{\tt Fixpoint} command as described in Section~\ref{Fixpoint} and show -the internal representation. -\begin{coq_example} -Fixpoint plus (n m:nat) {struct n} : nat := - match n with - | O => m - | S p => S (plus p m) - end. -Print plus. -Fixpoint lgth (A:Set) (l:list A) {struct l} : nat := - match l with - | nil _ => O - | cons _ a l' => S (lgth A l') - end. -Print lgth. -Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f) - with sizef (f:forest) : nat := - match f with - | emptyf => O - | consf t f => plus (sizet t) (sizef f) - end. -Print sizet. -\end{coq_example} - - -\subsubsection[Reduction rule]{Reduction rule\index{iota-reduction@$\iota$-reduction}} -Let $F$ be the set of declarations: $f_1/k_1:A_1:=t_1 \ldots -f_n/k_n:A_n:=t_n$. -The reduction for fixpoints is: -\[ (\Fix{f_i}{F}~a_1\ldots -a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n} -~a_1\ldots a_{k_i}\] -when $a_{k_i}$ starts with a constructor. -This last restriction is needed in order to keep strong normalization -and corresponds to the reduction for primitive recursive operators. -% -The following reductions are now possible: -\def\plus{\mathsf{plus}} -\def\tri{\triangleright_\iota} -\begin{eqnarray*} - \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ - & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ - & \tri & \nS~(\nS~(\nS~\nO))\\ -\end{eqnarray*} - -% La disparition de Program devrait rendre la construction Match obsolete -% \subsubsection{The {\tt Match \ldots with \ldots end} expression} -% \label{Matchexpr} -% %\paragraph{A unary {\tt Match\ldots with \ldots end}.} -% \index{Match...with...end@{\tt Match \ldots with \ldots end}} -% The {\tt Match} operator which was a primitive notion in older -% presentations of the Calculus of Inductive Constructions is now just a -% macro definition which generates the good combination of {\tt Case} -% and {\tt Fix} operators in order to generate an operator for primitive -% recursive definitions. It always considers an inductive definition as -% a single inductive definition. - -% The following examples illustrates this feature. -% \begin{coq_example} -% Definition nat_pr : (C:Set)C->(nat->C->C)->nat->C -% :=[C,x,g,n]Match n with x g end. -% Print nat_pr. -% \end{coq_example} -% \begin{coq_example} -% Definition forest_pr -% : (C:Set)C->(tree->forest->C->C)->forest->C -% := [C,x,g,n]Match n with x g end. -% \end{coq_example} - -% Cet exemple faisait error (HH le 12/12/96), j'ai change pour une -% version plus simple -%\begin{coq_example} -%Definition forest_pr -% : (P:forest->Set)(P emptyf)->((t:tree)(f:forest)(P f)->(P (consf t f))) -% ->(f:forest)(P f) -% := [C,x,g,n]Match n with x g end. -%\end{coq_example} - -\subsubsection{Mutual induction} - -The principles of mutual induction can be automatically generated -using the {\tt Scheme} command described in Section~\ref{Scheme}. - -\section{Admissible rules for global environments} - -From the original rules of the type system, one can show the -admissibility of rules which change the local context of definition of -objects in the global environment. We show here the admissible rules -that are used used in the discharge mechanism at the end of a section. - -% This is obsolete: Abstraction over defined constants actually uses a -% let-in since there are let-ins in Coq - -%% \paragraph{Mechanism of substitution.} - -%% One rule which can be proved valid, is to replace a term $c$ by its -%% value in the global environment. As we defined the substitution of a term for -%% a variable in a term, one can define the substitution of a term for a -%% constant. One easily extends this substitution to local contexts and global -%% environments. - -%% \paragraph{Substitution Property:} -%% \inference{\frac{\WF{E;c:=t:T; E'}{\Gamma}} -%% {\WF{E; \subst{E'}{c}{t}}{\subst{\Gamma}{c}{t}}}} - -\paragraph{Abstraction.} - -One can modify a global declaration by generalizing it over a -previously assumed constant $c$. For doing that, we need to modify the -reference to the global declaration in the subsequent global -environment and local context by explicitly applying this constant to -the constant $c'$. - -Below, if $\Gamma$ is a context of the form -$[y_1:A_1;\ldots;y_n:A_n]$, we write $\forall -x:U,\subst{\Gamma}{c}{x}$ to mean -$[y_1:\forall~x:U,\subst{A_1}{c}{x};\ldots;y_n:\forall~x:U,\subst{A_n}{c}{x}]$ -and -$\subst{E}{|\Gamma|}{|\Gamma|c}$. -to mean the parallel substitution -$\subst{\subst{E}{y_1}{(y_1~c)}\ldots}{y_n}{(y_n~c)}$. - -\paragraph{First abstracting property:} - \inference{\frac{\WF{E;c:U;E';c':=t:T;E''}{\Gamma}} - {\WF{E;c:U;E';c':=\lb x:U\mto \subst{t}{c}{x}:\forall~x:U,\subst{T}{c}{x}; - \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}} - - \inference{\frac{\WF{E;c:U;E';c':T;E''}{\Gamma}} - {\WF{E;c:U;E';c':\forall~x:U,\subst{T}{c}{x}; - \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}} - - \inference{\frac{\WF{E;c:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}} - {\WFTWOLINES{E;c:U;E';\Ind{}{p+1}{\forall x:U,\subst{\Gamma_I}{c}{x}}{\forall x:U,\subst{\Gamma_C}{c}{x}};\subst{E''}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}{\subst{\Gamma}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}}} -% -One can similarly modify a global declaration by generalizing it over -a previously defined constant~$c'$. Below, if $\Gamma$ is a context -of the form $[y_1:A_1;\ldots;y_n:A_n]$, we write $ -\subst{\Gamma}{c}{u}$ to mean -$[y_1:\subst{A_1}{c}{u};\ldots;y_n:\subst{A_n}{c}{u}]$. - -\paragraph{Second abstracting property:} - \inference{\frac{\WF{E;c:=u:U;E';c':=t:T;E''}{\Gamma}} - {\WF{E;c:=u:U;E';c':=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};E''}{\Gamma}}} - - \inference{\frac{\WF{E;c:=u:U;E';c':T;E''}{\Gamma}} - {\WF{E;c:=u:U;E';c':\subst{T}{c}{u};E''}{\Gamma}}} - - \inference{\frac{\WF{E;c:=u:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}} - {\WF{E;c:=u:U;E';\Ind{}{p}{\subst{\Gamma_I}{c}{u}}{\subst{\Gamma_C}{c}{u}};E''}{\Gamma}}} - -\paragraph{Pruning the local context.} -If one abstracts or substitutes constants with the above rules then it -may happen that some declared or defined constant does not occur any -more in the subsequent global environment and in the local context. One can -consequently derive the following property. - -\paragraph{First pruning property:} -\inference{\frac{\WF{E;c:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}} - {\WF{E;E'}{\Gamma}}} - -\paragraph{Second pruning property:} -\inference{\frac{\WF{E;c:=u:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}} - {\WF{E;E'}{\Gamma}}} - -\section{Co-inductive types} -The implementation contains also co-inductive definitions, which are -types inhabited by infinite objects. -More information on co-inductive definitions can be found -in~\cite{Gimenez95b,Gim98,GimCas05}. -%They are described in Chapter~\ref{Co-inductives}. - -\section[The Calculus of Inductive Construction with - impredicative \Set]{The Calculus of Inductive Construction with - impredicative \Set\label{impredicativity}} - -\Coq{} can be used as a type-checker for the -Calculus of Inductive Constructions with an impredicative sort \Set{} -by using the compiler option \texttt{-impredicative-set}. -% -For example, using the ordinary \texttt{coqtop} command, the following -is rejected. -% (** This example should fail ******************************* -% Error: The term forall X:Set, X -> X has type Type -% while it is expected to have type Set ***) -\begin{coq_example} -Fail Definition id: Set := forall X:Set,X->X. -\end{coq_example} -while it will type-check, if one uses instead the \texttt{coqtop - -impredicative-set} command. - -The major change in the theory concerns the rule for product formation -in the sort \Set, which is extended to a domain in any sort: -\begin{description} -\item [Prod] \index{Typing rules!Prod (impredicative Set)} -\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~~~ - \WTE{\Gamma::(x:T)}{U}{\Set}} - { \WTEG{\forall~x:T,U}{\Set}}} -\end{description} -This extension has consequences on the inductive definitions which are -allowed. -In the impredicative system, one can build so-called {\em large inductive - definitions} like the example of second-order existential -quantifier (\texttt{exSet}). - -There should be restrictions on the eliminations which can be -performed on such definitions. The eliminations rules in the -impredicative system for sort \Set{} become: -\begin{description} -\item[\Set] \inference{\frac{s \in - \{\Prop, \Set\}}{\compat{I:\Set}{I\ra s}} -~~~~\frac{I \mbox{~is a small inductive definition}~~~~s \in - \{\Type(i)\}} - {\compat{I:\Set}{I\ra s}}} -\end{description} - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: - - diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index c7a98fce4..ec36304a6 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -96,7 +96,6 @@ Options A and B of the licence are {\em not} elected.} %END LATEX \include{RefMan-gal.v}% Gallina \include{RefMan-lib.v}% The coq library -\include{RefMan-cic.v}% The Calculus of Constructions \include{RefMan-modr}% The module system diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst new file mode 100644 index 000000000..2695c5eee --- /dev/null +++ b/doc/sphinx/language/cic.rst @@ -0,0 +1,1881 @@ +\chapter[Calculus of Inductive Constructions]{Calculus of Inductive Constructions +\label{Cic} +\index{Cic@\textsc{CIC}} +\index{Calculus of Inductive Constructions}} +%HEVEA\cutname{cic.html} + +The underlying formal language of {\Coq} is a {\em Calculus of +Inductive Constructions} (\CIC) whose inference rules are presented in +this chapter. The history of this formalism as well as pointers to related work +are provided in a separate chapter; see {\em Credits}. + +\section[The terms]{The terms\label{Terms}} + +The expressions of the {\CIC} are {\em terms} and all terms have a {\em type}. +There are types for functions (or +programs), there are atomic types (especially datatypes)... but also +types for proofs and types for the types themselves. +Especially, any object handled in the formalism must belong to a +type. For instance, universal quantification is relative to a type and +takes the form {\it ``for all x +of type T, P''}. The expression {\it ``x of type T''} is +written {\it ``x:T''}. Informally, {\it ``x:T''} can be thought as +{\it ``x belongs to T''}. + +The types of types are {\em sorts}. Types and sorts are themselves +terms so that terms, types and sorts are all components of a common +syntactic language of terms which is described in +Section~\ref{cic:terms} but, first, we describe sorts. + +\subsection[Sorts]{Sorts\label{Sorts} +\index{Sorts}} +All sorts have a type and 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~\cite{Coq86}, 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}~ u$ in \Coq{} concrete syntax) is a term. This is a + notation for the $\lambda$-abstraction of + $\lambda$-calculus\index{lambda-calculus@$\lambda$-calculus} + \cite{Bar81}. The term $\lb x:T \mto u$ is a function which maps + elements of $T$ to the expression $u$. +\item if $t$ and $u$ are terms then $(t\ u)$ is a term + ($t~u$ in \Coq{} concrete syntax). The term $(t\ + u)$ reads as {\it ``t applied to u''}. +\item if $x$ is a variable, and $t$, $T$ and $u$ are terms then + $\kw{let}~x:=t:T~\kw{in}~u$ is a + term which denotes the term $u$ where the variable $x$ is locally + bound to $t$ of type $T$. This stands for the common ``let-in'' + construction of functional programs such as ML or Scheme. +%\item case ... +%\item fixpoint ... +%\item cofixpoint ... +\end{enumerate} + +\paragraph{Free variables.} +The notion of free variables is defined as usual. In the expressions +$\lb x:T\mto U$ and $\forall x:T, U$ the occurrences of $x$ in $U$ +are bound. + +\paragraph[Substitution.]{Substitution.\index{Substitution}} +The notion of substituting a term $t$ to free occurrences of a +variable $x$ in a term $u$ is defined as usual. The resulting term +is written $\subst{u}{x}{t}$. + +\paragraph[The logical vs programming readings.]{The logical vs programming readings.} + +The constructions of the {\CIC} can be used to express both logical +and programming notions, accordingly to the Curry-Howard +correspondence between proofs and programs, and between propositions +and types~\cite{Cur58,How80,Bru72}. + +For instance, let us assume that \nat\ is the type of natural numbers +with zero element written $0$ and that ${\tt True}$ is the always true +proposition. Then $\ra$ is used both to denote $\nat\ra\nat$ which is +the type of functions from \nat\ to \nat, to denote ${\tt True}\ra{\tt + True}$ which is an implicative proposition, to denote $\nat \ra +\Prop$ which is the type of unary predicates over the natural numbers, +etc. + +Let us assume that ${\tt mult}$ is a function of type $\nat\ra\nat\ra +\nat$ and ${\tt eqnat}$ a predicate of type $\nat\ra\nat\ra \Prop$. +The $\lambda$-abstraction can serve to build ``ordinary'' functions as +in $\lambda x:\nat.({\tt mult}~x~x)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~ +{\tt mult} ~x~x$ in {\Coq} notation) but may build also predicates +over the natural numbers. For instance $\lambda x:\nat.({\tt eqnat}~ +x~0)$ (i.e. $\kw{fun}~x:\nat ~{\tt =>}~ {\tt eqnat}~ x~0$ in {\Coq} +notation) will represent the predicate of one variable $x$ which +asserts the equality of $x$ with $0$. This predicate has type $\nat +\ra \Prop$ and it can be applied to any expression of type ${\nat}$, +say $t$, to give an object $P~t$ of type \Prop, namely a proposition. + +Furthermore $\kw{forall}~x:\nat,\,P\;x$ will represent the type of +functions which associate to each natural number $n$ an object of type +$(P~n)$ and consequently represent the type of proofs of the formula +``$\forall x.\,P(x)$''. + +\section[Typing rules]{Typing rules\label{Typed-terms}} + +As objects of type theory, terms are subjected to {\em type +discipline}. The well typing of a term depends on +a global environment and a local context. + +\paragraph{Local context.\index{Local context}} +A {\em local context} is an ordered list of +{\em local declarations\index{declaration!local}} of names which we call {\em variables\index{variable}}. +The declaration of some variable $x$ is +either a {\em local assumption\index{assumption!local}}, written $x:T$ ($T$ is a type) or a {\em local definition\index{definition!local}}, +written $x:=t:T$. We use brackets to write local contexts. A +typical example is $[x:T;y:=u:U;z:V]$. Notice that the variables +declared in a local context must be distinct. If $\Gamma$ declares some $x$, +we write $x \in \Gamma$. By writing $(x:T) \in \Gamma$ we mean that +either $x:T$ is an assumption in $\Gamma$ or that there exists some $t$ such +that $x:=t:T$ is a definition in $\Gamma$. If $\Gamma$ defines some +$x:=t:T$, we also write $(x:=t:T) \in \Gamma$. +For the rest of the chapter, the $\Gamma::(y:T)$ denotes the local context +$\Gamma$ enriched with the local assumption $y:T$. +Similarly, $\Gamma::(y:=t:T)$ denotes the local context +$\Gamma$ enriched with the local definition $(y:=t:T)$. +The notation $[]$ denotes the empty local context. +By $\Gamma_1; \Gamma_2$ we mean concatenation of the local context $\Gamma_1$ +and the local context $\Gamma_2$. + +% Does not seem to be used further... +% Si dans l'explication WF(E)[Gamma] concernant les constantes +% definies ds un contexte + +%We define the inclusion of two local contexts $\Gamma$ and $\Delta$ (written +%as $\Gamma \subset \Delta$) as the property, for all variable $x$, +%type $T$ and term $t$, if $(x:T) \in \Gamma$ then $(x:T) \in \Delta$ +%and if $(x:=t:T) \in \Gamma$ then $(x:=t:T) \in \Delta$. +%We write +% $|\Delta|$ for the length of the context $\Delta$, that is for the number +% of declarations (assumptions or definitions) in $\Delta$. + +\paragraph[Global environment.]{Global environment.\index{Global environment}} +%Because we are manipulating global declarations (global constants and global +%assumptions), we also need to consider a global environment $E$. + +A {\em global environment} is an ordered list of {\em global declarations\index{declaration!global}}. +Global declarations are either {\em global assumptions\index{assumption!global}} or {\em global +definitions\index{definition!global}}, but also declarations of inductive objects. Inductive objects themselves declare both inductive or coinductive types and constructors +(see Section~\ref{Cic-inductive-definitions}). + +A {\em global assumption} will be represented in the global environment as +$(c:T)$ which assumes the name $c$ to be of some type $T$. +A {\em global definition} will +be represented in the global environment as $c:=t:T$ which defines +the name $c$ to have value $t$ and type $T$. +We shall call such names {\em constants}. +For the rest of the chapter, the $E;c:T$ denotes the global environment +$E$ enriched with the global assumption $c:T$. +Similarly, $E;c:=t:T$ denotes the global environment +$E$ enriched with the global definition $(c:=t:T)$. + +The rules for inductive definitions (see Section +\ref{Cic-inductive-definitions}) have to be considered as assumption +rules to which the following definitions apply: if the name $c$ is +declared in $E$, we write $c \in E$ and if $c:T$ or $c:=t:T$ is +declared in $E$, we write $(c : T) \in E$. + +\paragraph[Typing rules.]{Typing rules.\label{Typing-rules}\index{Typing rules}} +In the following, we define simultaneously two +judgments. The first one \WTEG{t}{T} means the term $t$ is well-typed +and has type $T$ in the global environment $E$ and local context $\Gamma$. The +second judgment \WFE{\Gamma} means that the global environment $E$ is +well-formed and the local context $\Gamma$ is a valid local context in this +global environment. +% HH: This looks to me complicated. I think it would be better to talk +% about ``discharge'' as a transformation of global environments, +% rather than as keeping a local context next to global constants. +% +%% It also means a third property which makes sure that any +%%constant in $E$ was defined in an environment which is included in +%%$\Gamma$ +%%\footnote{This requirement could be relaxed if we instead introduced +%% an explicit mechanism for instantiating constants. At the external +%% level, the Coq engine works accordingly to this view that all the +%% definitions in the environment were built in a local sub-context of the +%% current local context.}. + +A term $t$ is well typed in a global environment $E$ iff there exists a +local context $\Gamma$ and a term $T$ such that the judgment \WTEG{t}{T} can +be derived from the following rules. +\begin{description} +\item[W-Empty] \inference{\WF{[]}{}} +\item[W-Local-Assum] % Ce n'est pas vrai : x peut apparaitre plusieurs fois dans Gamma +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~x \not\in \Gamma % \cup E + }{\WFE{\Gamma::(x:T)}}} +\item[W-Local-Def] +\inference{\frac{\WTEG{t}{T}~~~~x \not\in \Gamma % \cup E + }{\WFE{\Gamma::(x:=t:T)}}} +\item[W-Global-Assum] \inference{\frac{\WTE{}{T}{s}~~~~s \in \Sort~~~~c \notin E} + {\WF{E;c:T}{}}} +\item[W-Global-Def] \inference{\frac{\WTE{}{t}{T}~~~c \notin E} + {\WF{E;c:=t:T}{}}} +\item[Ax-Prop] \index{Typing rules!Ax-Prop} +\inference{\frac{\WFE{\Gamma}}{\WTEG{\Prop}{\Type(1)}}} +\item[Ax-Set] \index{Typing rules!Ax-Set} +\inference{\frac{\WFE{\Gamma}}{\WTEG{\Set}{\Type(1)}}} +\item[Ax-Type] \index{Typing rules!Ax-Type} +\inference{\frac{\WFE{\Gamma}}{\WTEG{\Type(i)}{\Type(i+1)}}} +\item[Var]\index{Typing rules!Var} + \inference{\frac{ \WFE{\Gamma}~~~~~(x:T) \in \Gamma~~\mbox{or}~~(x:=t:T) \in \Gamma~\mbox{for some $t$}}{\WTEG{x}{T}}} +\item[Const] \index{Typing rules!Const} +\inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E~~\mbox{or}~~(c:=t:T) \in E~\mbox{for some $t$} }{\WTEG{c}{T}}} +\item[Prod-Prop] \index{Typing rules!Prod-Prop} +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~ + \WTE{\Gamma::(x:T)}{U}{\Prop}} + { \WTEG{\forall~x:T,U}{\Prop}}} +\item[Prod-Set] \index{Typing rules!Prod-Set} +\inference{\frac{\WTEG{T}{s}~~~~s \in\{\Prop, \Set\}~~~~~~ + \WTE{\Gamma::(x:T)}{U}{\Set}} + { \WTEG{\forall~x:T,U}{\Set}}} +\item[Prod-Type] \index{Typing rules!Prod-Type} +\inference{\frac{\WTEG{T}{\Type(i)}~~~~ + \WTE{\Gamma::(x:T)}{U}{\Type(i)}} + {\WTEG{\forall~x:T,U}{\Type(i)}}} +\item[Lam]\index{Typing rules!Lam} +\inference{\frac{\WTEG{\forall~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}} + {\WTEG{\lb x:T\mto t}{\forall x:T, U}}} +\item[App]\index{Typing rules!App} + \inference{\frac{\WTEG{t}{\forall~x:U,T}~~~~\WTEG{u}{U}} + {\WTEG{(t\ u)}{\subst{T}{x}{u}}}} +\item[Let]\index{Typing rules!Let} +\inference{\frac{\WTEG{t}{T}~~~~ \WTE{\Gamma::(x:=t:T)}{u}{U}} + {\WTEG{\letin{x}{t:T}{u}}{\subst{U}{x}{t}}}} +\end{description} + +\Rem Prod$_1$ and Prod$_2$ typing-rules make sense if we consider the semantic +difference between {\Prop} and {\Set}: +\begin{itemize} + \item All values of a type that has a sort {\Set} are extractable. + \item No values of a type that has a sort {\Prop} are extractable. +\end{itemize} + +\Rem We may have $\kw{let}~x:=t:T~\kw{in}~u$ +well-typed without having $((\lb x:T\mto u)~t)$ well-typed (where +$T$ is a type of $t$). This is because the value $t$ associated to $x$ +may be used in a conversion rule (see Section~\ref{conv-rules}). + +\section[Conversion rules]{Conversion rules\index{Conversion rules} +\label{conv-rules}} + +In \CIC, there is an internal reduction mechanism. In particular, it +can decide if two programs are {\em intentionally} equal (one +says {\em convertible}). Convertibility is described in this section. + +\paragraph[$\beta$-reduction.]{$\beta$-reduction.\label{beta}\index{beta-reduction@$\beta$-reduction}} + +We want to be able to identify some terms as we can identify the +application of a function to a given argument with its result. For +instance the identity function over a given type $T$ can be written +$\lb x:T\mto x$. In any global environment $E$ and local context $\Gamma$, we want to identify any object $a$ (of type $T$) with the +application $((\lb x:T\mto x)~a)$. We define for this a {\em reduction} (or a +{\em conversion}) rule we call $\beta$: +\[ \WTEGRED{((\lb x:T\mto + t)~u)}{\triangleright_{\beta}}{\subst{t}{x}{u}} \] +We say that $\subst{t}{x}{u}$ is the {\em $\beta$-contraction} of +$((\lb x:T\mto t)~u)$ and, conversely, that $((\lb x:T\mto t)~u)$ +is the {\em $\beta$-expansion} of $\subst{t}{x}{u}$. + +According to $\beta$-reduction, terms of the {\em Calculus of + Inductive Constructions} enjoy some fundamental properties such as +confluence, strong normalization, subject reduction. These results are +theoretically of great importance but we will not detail them here and +refer the interested reader to \cite{Coq85}. + +\paragraph[$\iota$-reduction.]{$\iota$-reduction.\label{iota}\index{iota-reduction@$\iota$-reduction}} +A specific conversion rule is associated to the inductive objects in +the global environment. We shall give later on (see Section~\ref{iotared}) the +precise rules but it just says that a destructor applied to an object +built from a constructor behaves as expected. This reduction is +called $\iota$-reduction and is more precisely studied in +\cite{Moh93,Wer94}. + + +\paragraph[$\delta$-reduction.]{$\delta$-reduction.\label{delta}\index{delta-reduction@$\delta$-reduction}} + +We may have variables defined in local contexts or constants defined in the global +environment. It is legal to identify such a reference with its value, +that is to expand (or unfold) it into its value. This +reduction is called $\delta$-reduction and shows as follows. + +$$\WTEGRED{x}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(x:=t:T) \in \Gamma$}~~~~~~~~~\WTEGRED{c}{\triangleright_{\delta}}{t}~~~~~\mbox{if $(c:=t:T) \in E$}$$ + + +\paragraph[$\zeta$-reduction.]{$\zeta$-reduction.\label{zeta}\index{zeta-reduction@$\zeta$-reduction}} + +{\Coq} allows also to remove local definitions occurring in terms by +replacing the defined variable by its value. The declaration being +destroyed, this reduction differs from $\delta$-reduction. It is +called $\zeta$-reduction and shows as follows. + +$$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ + +\paragraph{$\eta$-expansion.% +\label{eta}% +\index{eta-expansion@$\eta$-expansion}% +%\index{eta-reduction@$\eta$-reduction} +}% +Another important concept is $\eta$-expansion. It is legal to identify any +term $t$ of functional type $\forall x:T, U$ with its so-called +$\eta$-expansion $\lb x:T\mto (t\ x)$ for $x$ an arbitrary variable +name fresh in $t$. + +\Rem We deliberately do not define $\eta$-reduction: +\begin{latexonly}% + $$\lb x:T\mto (t\ x)\not\triangleright_\eta\hskip.3em t$$ +\end{latexonly}% +\begin{htmlonly} + $$\lb x:T\mto (t\ x)~\not\triangleright_\eta~t$$ +\end{htmlonly} +This is because, in general, the type of $t$ need not to be convertible to the type of $\lb x:T\mto (t\ x)$. +E.g., if we take $f$ such that: +\begin{latexonly}% + $$f\hskip.5em:\hskip.5em\forall x:Type(2),Type(1)$$ +\end{latexonly}% +\begin{htmlonly} + $$f~:~\forall x:Type(2),Type(1)$$ +\end{htmlonly} +then +\begin{latexonly}% + $$\lb x:Type(1),(f\, x)\hskip.5em:\hskip.5em\forall x:Type(1),Type(1)$$ +\end{latexonly}% +\begin{htmlonly} + $$\lb x:Type(1),(f\, x)~:~\forall x:Type(1),Type(1)$$ +\end{htmlonly} +We could not allow +\begin{latexonly}% + $$\lb x:Type(1),(f\,x)\hskip.4em\not\triangleright_\eta\hskip.6em f$$ +\end{latexonly}% +\begin{htmlonly} + $$\lb x:Type(1),(f\,x)~\not\triangleright_\eta~f$$ +\end{htmlonly} +because the type of the reduced term $\forall x:Type(2),Type(1)$ +would not be convertible to the type of the original term $\forall x:Type(1),Type(1)$. + +\paragraph[Convertibility.]{Convertibility.\label{convertibility} +\index{beta-reduction@$\beta$-reduction}\index{iota-reduction@$\iota$-reduction}\index{delta-reduction@$\delta$-reduction}\index{zeta-reduction@$\zeta$-reduction}} + +Let us write $\WTEGRED{t}{\triangleright}{u}$ for the contextual closure of the relation $t$ reduces to $u$ in the global environment $E$ and local context $\Gamma$ with one of the previous reduction $\beta$, $\iota$, $\delta$ or $\zeta$. + +We say that two terms $t_1$ and $t_2$ are {\em + $\beta\iota\delta\zeta\eta$-convertible}, or simply {\em + convertible}, or {\em equivalent}, in the global environment $E$ and +local context $\Gamma$ iff there exist terms $u_1$ and $u_2$ such that +$\WTEGRED{t_1}{\triangleright \ldots \triangleright}{u_1}$ and +$\WTEGRED{t_2}{\triangleright \ldots \triangleright}{u_2}$ and either +$u_1$ and $u_2$ are identical, or they are convertible up to +$\eta$-expansion, i.e. $u_1$ is $\lb x:T\mto u'_1$ and $u_2\,x$ is +recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb +x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We +then write $\WTEGCONV{t_1}{t_2}$. + +Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below) +convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e., +$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$. +Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$ +and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels) +such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$. + +The convertibility relation allows introducing a new typing rule +which says that two convertible well-formed types have the same +inhabitants. + +\section[Subtyping rules]{Subtyping rules\index{Subtyping rules} +\label{subtyping-rules}} + +At the moment, we did not take into account one rule between universes +which says that any term in a universe of index $i$ is also a term in +the universe of index $i+1$ (this is the {\em cumulativity} rule of +{\CIC}). This property extends the equivalence relation of +convertibility into a {\em subtyping} relation 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{\Set}{\Type(i)}$, +\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'}$. +\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full}) + inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$ + and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$ + are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors + \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\] + and + \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\] + respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) + if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have + \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\] + where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$. +\end{enumerate} + +The conversion rule up to subtyping is now exactly: + +\begin{description}\label{Conv} +\item[Conv]\index{Typing rules!Conv} + \inference{ + \frac{\WTEG{U}{s}~~~~\WTEG{t}{T}~~~~\WTEGLECONV{T}{U}}{\WTEG{t}{U}}} + \end{description} + + +\paragraph[Normal form.]{Normal form.\index{Normal form}\label{Normal-form}\label{Head-normal-form}\index{Head normal form}} +A term which cannot be any more reduced is said to be in {\em normal + form}. There are several ways (or strategies) to apply the reduction +rules. Among them, we have to mention the {\em head reduction} which +will play an important role (see Chapter~\ref{Tactics}). Any term can +be written as $\lb x_1:T_1\mto \ldots \lb x_k:T_k \mto +(t_0\ t_1\ldots t_n)$ where +$t_0$ is not an application. We say then that $t_0$ is the {\em head + of $t$}. If we assume that $t_0$ is $\lb x:T\mto u_0$ then one step of +$\beta$-head reduction of $t$ is: +\[\lb x_1:T_1\mto \ldots \lb x_k:T_k\mto (\lb x:T\mto u_0\ t_1\ldots t_n) +~\triangleright ~ \lb (x_1:T_1)\ldots(x_k:T_k)\mto +(\subst{u_0}{x}{t_1}\ t_2 \ldots t_n)\] +Iterating the process of head reduction until the head of the reduced +term is no more an abstraction leads to the {\em $\beta$-head normal + form} of $t$: +\[ t \triangleright \ldots \triangleright +\lb x_1:T_1\mto \ldots\lb x_k:T_k\mto (v\ u_1 +\ldots u_m)\] +where $v$ is not an abstraction (nor an application). Note that the +head normal form must not be confused with the normal form since some +$u_i$ can be reducible. +% +Similar notions of head-normal forms involving $\delta$, $\iota$ and $\zeta$ +reductions or any combination of those can also be defined. + +\section[Inductive definitions]{Inductive Definitions\label{Cic-inductive-definitions}} + +% Here we assume that the reader knows what is an inductive definition. + +Formally, we can represent any {\em inductive definition\index{definition!inductive}} as \Ind{}{p}{\Gamma_I}{\Gamma_C} where: +\begin{itemize} + \item $\Gamma_I$ determines the names and types of inductive types; + \item $\Gamma_C$ determines the names and types of constructors of these inductive types; + \item $p$ determines the number of parameters of these inductive types. +\end{itemize} +These inductive definitions, together with global assumptions and global definitions, then form the global environment. +% +Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$ +such that each $T$ in $(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}}. +Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as: +$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the +{\em Arity} of the inductive type\index{arity of inductive type} $t$ and +$\Sort$ is called the sort of the inductive type $t$. + +\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}} + +The declaration for parameterized lists is: +\begin{latexonly} + \vskip.5em + + \ind{1}{[\List:\Set\ra\Set]}{\left[\begin{array}{r@{:}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}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎝		[ list : Set → Set ]:=⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
nil:=∀A : Set, list A
cons:=∀A : Set, A → list A → list A

+    		⎤
⎦		⎞
⎠
+\end{rawhtml} +\noindent 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*} + +\noindent The declaration for a mutual inductive definition of {\tree} and {\forest} is: +\begin{latexonly} + \vskip.5em +\ind{~}{\left[\begin{array}{r@{:}l}\tree&\Set\\\forest&\Set\end{array}\right]} + {\left[\begin{array}{r@{:}l} + \node & \forest \ra \tree\\ + \emptyf & \forest\\ + \consf & \tree \ra \forest \ra \forest\\ + \end{array}\right]} + \vskip.5em +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
tree:Set
forest:Set

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
node:forest → tree
emptyf:forest
consf:tree → forest → forest

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} +\noindent 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*} + +\noindent The declaration for a mutual inductive definition of {\even} and {\odd} is: +\begin{latexonly} + \newcommand\GammaI{\left[\begin{array}{r@{:}l} + \even & \nat\ra\Prop \\ + \odd & \nat\ra\Prop + \end{array} + \right]} + \newcommand\GammaC{\left[\begin{array}{r@{:}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]} + \vskip.5em + \ind{1}{\GammaI}{\GammaC} + \vskip.5em +\end{latexonly} +\begin{rawhtml}

+  
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+    
+  
+
Ind[1]⎛
⎜
⎝		⎡
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even:nat → Prop
odd:nat → Prop

+    		⎤
⎦		:=⎡
⎢
⎣		
+      
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+        
+          
+          
+          
+        
+      
even_O:even O
even_S:∀n : nat, odd n → even (S n)
odd_S:∀n : nat, even n → odd (S n)

+    		⎤
⎥
⎦		⎞
⎟
⎠
+\end{rawhtml} +\noindent 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 +contains an inductive declaration. + +\begin{description} +\item[Ind] \index{Typing rules!Ind} + \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}~~~~~~~~\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E~~~~~~~~(c:C)\in\Gamma_C}{\WTEG{c}{C}}} +\end{description} + +\begin{latexonly}% +\paragraph{Example.} +Provided that our environment $E$ contains inductive definitions we showed before, +these two inference rules above enable us to conclude that: +\vskip.5em +\newcommand\prefix{E[\Gamma]\vdash\hskip.25em} +$\begin{array}{@{}l} + \prefix\even : \nat\ra\Prop\\ + \prefix\odd : \nat\ra\Prop\\ + \prefix\evenO : \even~\nO\\ + \prefix\evenS : \forall~n:\nat, \odd~n \ra \even~(\nS~n)\\ + \prefix\oddS : \forall~n:\nat, \even~n \ra \odd~(\nS~n) + \end{array}$ +\end{latexonly}% + +%\paragraph{Parameters.} +%%The parameters introduce a distortion between the inside specification +%%of the inductive declaration where parameters are supposed to be +%%instantiated (this representation is appropriate for checking the +%%correctness or deriving the destructor principle) and the outside +%%typing rules where the inductive objects are seen as objects +%%abstracted with respect to the parameters. + +%In the definition of \List\ or \haslength\, $A$ is a parameter because +%what is effectively inductively defined is $\ListA$ or $\haslengthA$ for +%a given $A$ which is constant in the type of constructors. But when +%we define $(\haslengthA~l~n)$, $l$ and $n$ are not parameters because the +%constructors manipulate different instances of this family. + +\subsection{Well-formed inductive definitions} +We cannot accept any inductive declaration because some of them lead +to inconsistent systems. +We restrict ourselves to definitions which +satisfy a syntactic criterion of positivity. Before giving the formal +rules, we need a few definitions: + +\paragraph[Definition]{Definition\index{Arity}\label{Arity}} +A type $T$ is an {\em arity of sort $s$} if it converts +to the sort $s$ or to a product $\forall~x:T,U$ with $U$ an arity +of sort $s$. + +\paragraph[Examples]{Examples} +$A\ra \Set$ is an arity of sort $\Set$. +$\forall~A:\Prop,A\ra \Prop$ is an arity of sort \Prop. + +\paragraph[Definition]{Definition} +A type $T$ is an {\em arity} if there is a $s\in\Sort$ +such that $T$ is an arity of sort $s$. + +\paragraph[Examples]{Examples} +$A\ra \Set$ and $\forall~A:\Prop,A\ra \Prop$ are arities. + +\paragraph[Definition]{Definition\index{type of constructor}} +We say that $T$ is a {\em type of constructor of $I$\index{type of constructor}} +in one of the following two cases: +\begin{itemize} + \item $T$ is $(I~t_1\ldots ~t_n)$ + \item $T$ is $\forall x:U,T^\prime$ where $T^\prime$ is also a type of constructor of $I$ +\end{itemize} + +\paragraph[Examples]{Examples} +$\nat$ and $\nat\ra\nat$ are types of constructors of $\nat$.\\ +$\forall A:\Type,\List~A$ and $\forall A:\Type,A\ra\List~A\ra\List~A$ are constructors of $\List$. + +\paragraph[Definition]{Definition\index{Positivity}\label{Positivity}} +The type of constructor $T$ will be said to {\em satisfy the positivity +condition} for a constant $X$ in the following cases: + +\begin{itemize} +\item $T=(X~t_1\ldots ~t_n)$ and $X$ does not occur free in +any $t_i$ +\item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and +the type $V$ satisfies the positivity condition for $X$ +\end{itemize} +% +The constant $X$ {\em occurs strictly positively} in $T$ in the +following cases: +% +\begin{itemize} +\item $X$ does not occur in $T$ +\item $T$ converts to $(X~t_1 \ldots ~t_n)$ and $X$ does not occur in + any of $t_i$ +\item $T$ converts to $\forall~x:U,V$ and $X$ does not occur in + type $U$ but occurs strictly positively in type $V$ +\item $T$ converts to $(I~a_1 \ldots ~a_m ~ t_1 \ldots ~t_p)$ where + $I$ is the name of an inductive declaration of the form + $\Ind{\Gamma}{m}{I:A}{c_1:\forall p_1:P_1,\ldots \forall + p_m:P_m,C_1;\ldots;c_n:\forall p_1:P_1,\ldots \forall + p_m:P_m,C_n}$ + (in particular, it is not mutually defined and it has $m$ + parameters) and $X$ does not occur in any of the $t_i$, and the + (instantiated) types of constructor $C_i\{p_j/a_j\}_{j=1\ldots m}$ + of $I$ satisfy + the nested positivity condition for $X$ +%\item more generally, when $T$ is not a type, $X$ occurs strictly +%positively in $T[x:U]u$ if $X$ does not occur in $U$ but occurs +%strictly positively in $u$ +\end{itemize} +% +The type of constructor $T$ of $I$ {\em satisfies the nested +positivity condition} for a constant $X$ in the following +cases: + +\begin{itemize} +\item $T=(I~b_1\ldots b_m~u_1\ldots ~u_{p})$, $I$ is an inductive + definition with $m$ parameters and $X$ does not occur in +any $u_i$ +\item $T=\forall~x:U,V$ and $X$ occurs only strictly positively in $U$ and +the type $V$ satisfies the nested positivity condition for $X$ +\end{itemize} + +\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)}} +\newcommand{\NatTree}{\mbox{\textsf{nattree}}} +\newcommand{\NatTreeA}{\mbox{\textsf{nattree}}~\ensuremath{A}} +\newcommand{\cnode}{\mbox{\textsf{node}}} +\newcommand{\cleaf}{\mbox{\textsf{leaf}}} + +\noindent For instance, if one considers the following variant of a tree type branching over the natural numbers + +\begin{verbatim} +Inductive nattree (A:Type) : Type := + | leaf : nattree A + | node : A -> (nat -> nattree A) -> nattree A +\end{verbatim} + +\begin{latexonly} +\noindent Then every instantiated constructor of $\NatTreeA$ satisfies the nested positivity condition for $\NatTree$\\ +\noindent +\ws\ws\vv\\ +\ws\ws\vh\hh\ws concerning type $\NatTreeA$ of constructor $\cleaf$:\\ +\ws\ws\vv\ws\ws\ws\ws Type $\NatTreeA$ of constructor $\cleaf$ satisfies the positivity condition for $\NatTree$\\ +\ws\ws\vv\ws\ws\ws\ws because $\NatTree$ does not appear in any (real) arguments of the type of that constructor\\ +\ws\ws\vv\ws\ws\ws\ws (primarily because $\NatTree$ does not have any (real) arguments)\ruleref1\\ +\ws\ws\vv\\ +\ws\ws\hv\hh\ws concerning type $\forall~A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$:\\ + \ws\ws\ws\ws\ws\ws\ws Type $\forall~A:\Type,A\ra(\NN\ra\NatTreeA)\ra\NatTreeA$ of constructor $\cnode$\\ +\ws\ws\ws\ws\ws\ws\ws satisfies the positivity condition for $\NatTree$ because:\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\Type$\ruleref1\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $A$\ruleref1\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ + \ws\ws\ws\ws\ws\ws\ws\vh\hh\ws $\NatTree$ occurs only strictly positively in $\NN\ra\NatTreeA$\ruleref{3+2}\\ +\ws\ws\ws\ws\ws\ws\ws\vv\\ +\ws\ws\ws\ws\ws\ws\ws\hv\hh\ws $\NatTree$ satisfies the positivity condition for $\NatTreeA$\ruleref1 +\end{latexonly} +\begin{rawhtml} +
+Then every instantiated constructor of nattree A satisfies the nested positivity condition for nattree
+  │
+  ├─ concerning type nattree A of constructor nil:
+  │    Type nattree A of constructor nil satisfies the positivity condition for nattree
+  │    because nattree does not appear in any (real) arguments of the type of that constructor
+  │    (primarily because nattree does not have any (real) arguments) ... (bullet 1)
+  │
+  ╰─ concerning type ∀ A → (nat → nattree A) → nattree A of constructor cons:
+       Type ∀ A : Type, A → (nat → nattree A) → nattree A of constructor cons
+       satisfies the positivity condition for nattree because:
+       │
+       ├─ nattree occurs only strictly positively in Type ... (bullet 1)
+       │
+       ├─ nattree occurs only strictly positively in A ... (bullet 1)
+       │
+       ├─ nattree occurs only strictly positively in nat → nattree A ... (bullet 3+2)
+       │
+       ╰─ nattree satisfies the positivity condition for nattree A ... (bullet 1)
+
+\end{rawhtml} + +\paragraph{Correctness rules.} +We shall now describe the rules allowing the introduction of a new +inductive definition. + +\begin{description} +\item[W-Ind] Let $E$ be a global environment and + $\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that + $\Gamma_I$ is $[I_1:\forall \Gamma_P,A_1;\ldots;I_k:\forall + \Gamma_P,A_k]$ and $\Gamma_C$ is + $[c_1:\forall \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$. +\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} +} + {\WF{E;\Ind{}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}} +provided that the following side conditions hold: +\begin{itemize} +\item $k>0$ and all of $I_j$ and $c_i$ are distinct names for $j=1\ldots k$ and $i=1\ldots n$, +\item $p$ is the number of parameters of \NInd{}{\Gamma_I}{\Gamma_C} + and $\Gamma_P$ is the context of parameters, +\item for $j=1\ldots k$ we have that $A_j$ is an arity of sort $s_j$ and $I_j + \notin E$, +\item for $i=1\ldots n$ we have that $C_i$ is a type of constructor of + $I_{q_i}$ which satisfies the positivity condition for $I_1 \ldots I_k$ + and $c_i \notin \Gamma \cup E$. +\end{itemize} +\end{description} +One can remark that there is a constraint between the sort of the +arity of the inductive type and the sort of the type of its +constructors which will always be satisfied for the impredicative sort +{\Prop} but may fail to define inductive definition +on sort \Set{} and generate constraints between universes for +inductive definitions in the {\Type} hierarchy. + +\paragraph{Examples.} +It is well known that existential quantifier can be encoded as an +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. +\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. +\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 $kProp) : 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 +%is recursive or not. We shall write the type $(x:_R T)C$ if it is +%a recursive argument and $(x:_P T)C$ if the argument is not recursive. + +\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} +\label{Template-polymorphism} + +Inductive types declared in {\Type} are +polymorphic over their arguments in {\Type}. +If $A$ is an arity of some sort and $s$ is a sort, we write $A_{/s}$ for the arity +obtained from $A$ by replacing its sort with $s$. Especially, if $A$ +is well-typed in some global environment and local context, then $A_{/s}$ is typable +by typability of all products in the Calculus of Inductive Constructions. +The following typing rule is added to the theory. + +\begin{description} +\item[Ind-Family] Let $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ be an + inductive definition. Let $\Gamma_P = [p_1:P_1;\ldots;p_{p}:P_{p}]$ + be its context of parameters, $\Gamma_I = [I_1:\forall + \Gamma_P,A_1;\ldots;I_k:\forall \Gamma_P,A_k]$ its context of + definitions and $\Gamma_C = [c_1:\forall + \Gamma_P,C_1;\ldots;c_n:\forall \Gamma_P,C_n]$ its context of + constructors, with $c_i$ a constructor of $I_{q_i}$. + + Let $m \leq p$ be the length of the longest prefix of parameters + such that the $m$ first arguments of all occurrences of all $I_j$ in + all $C_k$ (even the occurrences in the hypotheses of $C_k$) are + exactly applied to $p_1~\ldots~p_m$ ($m$ is the number of {\em + recursively uniform parameters} and the $p-m$ remaining parameters + are the {\em recursively non-uniform parameters}). Let $q_1$, + \ldots, $q_r$, with $0\leq r\leq m$, be a (possibly) partial + instantiation of the recursively uniform parameters of + $\Gamma_P$. We have: + +\inference{\frac +{\left\{\begin{array}{l} +\Ind{}{p}{\Gamma_I}{\Gamma_C} \in E\\ +(E[] \vdash q_l : P'_l)_{l=1\ldots r}\\ +(\WTELECONV{}{P'_l}{\subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}})_{l=1\ldots r}\\ +1 \leq j \leq k +\end{array} +\right.} +{E[] \vdash I_j\,q_1\,\ldots\,q_r:\forall [p_{r+1}:P_{r+1};\ldots;p_{p}:P_{p}], (A_j)_{/s_j}} +} + +provided that the following side conditions hold: + +\begin{itemize} +\item $\Gamma_{P'}$ is the context obtained from $\Gamma_P$ by +replacing each $P_l$ that is an arity with $P'_l$ for $1\leq l \leq r$ (notice that +$P_l$ arity implies $P'_l$ arity since $\WTELECONV{}{P'_l}{ \subst{P_l}{p_u}{q_u}_{u=1\ldots l-1}}$); +\item there are sorts $s_i$, for $1 \leq i \leq k$ such that, for + $\Gamma_{I'} = [I_1:\forall + \Gamma_{P'},(A_1)_{/s_1};\ldots;I_k:\forall \Gamma_{P'},(A_k)_{/s_k}]$ +we have $(\WTE{\Gamma_{I'};\Gamma_{P'}}{C_i}{s_{q_i}})_{i=1\ldots n}$; +\item the sorts $s_i$ are such that all eliminations, to {\Prop}, {\Set} and + $\Type(j)$, are allowed (see Section~\ref{allowedeleminationofsorts}). +\end{itemize} +\end{description} +% +Notice that if $I_j\,q_1\,\ldots\,q_r$ is typable using the rules {\bf +Ind-Const} and {\bf App}, then it is typable using the rule {\bf +Ind-Family}. Conversely, the extended theory is not stronger than the +theory without {\bf Ind-Family}. We get an equiconsistency result by +mapping each $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ occurring into a +given derivation into as many different inductive types and constructors +as the number of different (partial) replacements of sorts, needed for +this derivation, in the parameters that are arities (this is possible +because $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ well-formed implies +that $\Ind{}{p}{\Gamma_{I'}}{\Gamma_{C'}}$ is well-formed and +has the same allowed eliminations, where +$\Gamma_{I'}$ is defined as above and $\Gamma_{C'} = [c_1:\forall +\Gamma_{P'},C_1;\ldots;c_n:\forall \Gamma_{P'},C_n]$). That is, +the changes in the types of each partial instance +$q_1\,\ldots\,q_r$ can be characterized by the ordered sets of arity +sorts among the types of parameters, and to each signature is +associated a new inductive definition with fresh names. Conversion is +preserved as any (partial) instance $I_j\,q_1\,\ldots\,q_r$ or +$C_i\,q_1\,\ldots\,q_r$ is mapped to the names chosen in the specific +instance of $\Ind{}{p}{\Gamma_I}{\Gamma_C}$. + +\newcommand{\Single}{\mbox{\textsf{Set}}} + +In practice, the rule {\bf Ind-Family} is used by {\Coq} only when all the +inductive types of the inductive definition are declared with an arity whose +sort is in the $\Type$ +hierarchy. Then, the polymorphism is over the parameters whose +type is an arity of sort in the {\Type} hierarchy. +The sort $s_j$ are +chosen canonically so that each $s_j$ is minimal with respect to the +hierarchy ${\Prop}\subset{\Set_p}\subset\Type$ where $\Set_p$ is +predicative {\Set}. +%and ${\Prop_u}$ is the sort of small singleton +%inductive types (i.e. of inductive types with one single constructor +%and that contains either proofs or inhabitants of singleton types +%only). +More precisely, an empty or small singleton inductive definition +(i.e. an inductive definition of which all inductive types are +singleton -- see paragraph~\ref{singleton}) is set in +{\Prop}, a small non-singleton inductive type is set in {\Set} (even +in case {\Set} is impredicative -- see Section~\ref{impredicativity}), +and otherwise in the {\Type} hierarchy. + +Note that the side-condition about allowed elimination sorts in the +rule~{\bf Ind-Family} is just to avoid to recompute the allowed +elimination sorts at each instance of a pattern-matching (see +section~\ref{elimdep}). +As an example, let us consider the following definition: +\begin{coq_example*} +Inductive option (A:Type) : Type := +| None : option A +| Some : A -> option A. +\end{coq_example*} +% +As the definition is set in the {\Type} hierarchy, it is used +polymorphically over its parameters whose types are arities of a sort +in the {\Type} hierarchy. Here, the parameter $A$ has this property, +hence, if \texttt{option} is applied to a type in {\Set}, the result is +in {\Set}. Note that if \texttt{option} is applied to a type in {\Prop}, +then, the result is not set in \texttt{Prop} but in \texttt{Set} +still. This is because \texttt{option} is not a singleton type (see +section~\ref{singleton}) and it would lose the elimination to {\Set} and +{\Type} if set in {\Prop}. + +\begin{coq_example} +Check (fun A:Set => option A). +Check (fun A:Prop => option A). +\end{coq_example} +% +Here is another example. +% +\begin{coq_example*} +Inductive prod (A B:Type) : Type := pair : A -> B -> prod A B. +\end{coq_example*} +% +As \texttt{prod} is a singleton type, it will be in {\Prop} if applied +twice to propositions, in {\Set} if applied twice to at least one type +in {\Set} and none in {\Type}, and in {\Type} otherwise. In all cases, +the three kind of eliminations schemes are allowed. + +\begin{coq_example} +Check (fun A:Set => prod A). +Check (fun A:Prop => prod A A). +Check (fun (A:Prop) (B:Set) => prod A B). +Check (fun (A:Type) (B:Prop) => prod A B). +\end{coq_example} + +\Rem Template polymorphism used to be called ``sort-polymorphism of +inductive types'' before universe polymorphism (see +Chapter~\ref{Universes-full}) was introduced. + +\subsection{Destructors} +The specification of inductive definitions with arities and +constructors is quite natural. But we still have to say how to use an +object in an inductive type. + +This problem is rather delicate. There are actually several different +ways to do that. Some of them are logically equivalent but not always +equivalent from the computational point of view or from the user point +of view. + +From the computational point of view, we want to be able to define a +function whose domain is an inductively defined type by using a +combination of case analysis over the possible constructors of the +object and recursion. + +Because we need to keep a consistent theory and also we prefer to keep +a strongly normalizing reduction, we cannot accept any sort of +recursion (even terminating). So the basic idea is to restrict +ourselves to primitive recursive functions and functionals. + +For instance, assuming a parameter $A:\Set$ exists in the local context, we +want to build a function \length\ of type $\ListA\ra \nat$ which +computes the length of the list, so such that $(\length~(\Nil~A)) = \nO$ +and $(\length~(\cons~A~a~l)) = (\nS~(\length~l))$. We want these +equalities to be recognized implicitly and taken into account in the +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 about an object $m$ in an inductive definition it is +enough to enumerate all the cases where $m$ starts with a different +constructor. + +In case the inductive definition is effectively a recursive one, we +want to capture the extra property that we have built the smallest +fixed point of this recursive equation. This says that we are only +manipulating finite objects. This analysis provides induction +principles. +For instance, in order to prove $\forall l:\ListA,(\haslengthA~l~(\length~l))$ +it is enough to prove: +% +\begin{itemize} + \item $(\haslengthA~(\Nil~A)~(\length~(\Nil~A)))$ + \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\ + \ra (\haslengthA~(\cons~A~a~l)~(\length~(\cons~A~a~l)))$ +\end{itemize} +% +which given the conversion equalities satisfied by \length\ is the +same as proving: +% +\begin{itemize} + \item $(\haslengthA~(\Nil~A)~\nO)$ + \item $\forall a:A, \forall l:\ListA, (\haslengthA~l~(\length~l)) \ra\\ + \ra (\haslengthA~(\cons~A~a~l)~(\nS~(\length~l)))$ +\end{itemize} +% +One conceptually simple way to do that, following the basic scheme +proposed by Martin-L\"of in his Intuitionistic Type Theory, is to +introduce for each inductive definition an elimination operator. At +the logical level it is a proof of the usual induction principle and +at the computational level it implements a generic operator for doing +primitive recursion over the structure. + +But this operator is rather tedious to implement and use. We choose in +this version of {\Coq} to factorize the operator for primitive recursion +into two more primitive operations as was first suggested by Th. Coquand +in~\cite{Coq92}. One is the definition by pattern-matching. The second one is a definition by guarded fixpoints. + +\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 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}\] +In this expression, if +$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_i}$ 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 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 and one argument. The predicate is made explicit using the syntax: +\[\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}\] +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, $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 other arguments of $I$ +(sometimes called indices in the literature) +% NOTE: e.g. http://www.qatar.cmu.edu/~sacchini/papers/types08.pdf +have to be variables +($a$ above) and these variables can occur in $P$. +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 +compact notation: +\[ \Case{(\lb a x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~ + \lb x_{n1}...x_{np_n} \mto f_n}\] + +%% CP 06/06 Obsolete avec la nouvelle syntaxe et incompatible avec la +%% presentation theorique qui suit +% \paragraph{Non-dependent elimination.} +% +% When defining a function of codomain $C$ by case analysis over an +% object in an inductive type $I$, we build an object of type $I +% \ra C$. The minimality principle on an inductively defined logical +% predicate $I$ of type $A \ra \Prop$ is often used to prove a property +% $\forall x:A,(I~x)\ra (C~x)$. These are particular cases of the dependent +% principle that we stated before with a predicate which does not depend +% explicitly on the object in the inductive definition. + +% For instance, a function testing whether a list is empty +% can be +% defined as: +% \[\kw{fun} l:\ListA \Ra \kw{match}~l~\kw{with}~ \Nil \Ra \true~ +% |~(\cons~a~m) \Ra \false \kw{end}\] +% represented by +% \[\lb l:\ListA \mto\Case{\bool}{l}{\true~ |~ \lb a~m,~\false}\] +%\noindent {\bf Remark. } + +% In the system \Coq\ the expression above, can be +% written without mentioning +% the dummy abstraction: +% \Case{\bool}{l}{\Nil~ \mbox{\tt =>}~\true~ |~ (\cons~a~m)~ +% \mbox{\tt =>}~ \false} + +\paragraph[Allowed elimination sorts.]{Allowed elimination sorts.\index{Elimination sorts}} +\label{allowedeleminationofsorts} + +An important question for building the typing rule for \kw{match} is +what can be the type of $\lb a x \mto P$ with respect to the type of $m$. If +$m:I$ and +$I:A$ and +$\lb a x \mto P : B$ +then by \compat{I:A}{B} we mean that one can use $\lb a x \mto P$ with $m$ in the above +match-construct. + +\paragraph{Notations.} +The \compat{I:A}{B} is defined as the smallest relation satisfying the +following rules: +We write \compat{I}{B} for \compat{I:A}{B} where $A$ is the type of +$I$. + +The case of inductive definitions in sorts \Set\ or \Type{} is simple. +There is no restriction on the sort of the predicate to be +eliminated. +% +\begin{description} +\item[Prod] \inference{\frac{\compat{(I~x):A'}{B'}} + {\compat{I:\forall x:A, A'}{\forall x:A, B'}}} +\item[{\Set} \& \Type] \inference{\frac{ + s_1 \in \{\Set,\Type(j)\}~~~~~~~~s_2 \in \Sort}{\compat{I:s_1}{I\ra s_2}}} +\end{description} +% +The case of Inductive definitions of sort \Prop{} is a bit more +complicated, because of our interpretation of this sort. The only +harmless allowed elimination, is the one when predicate $P$ is also of +sort \Prop. +\begin{description} +\item[\Prop] \inference{\compat{I:\Prop}{I\ra\Prop}} +\end{description} +\Prop{} is the type of logical propositions, the proofs of properties +$P$ in \Prop{} could not be used for computation and are consequently +ignored by the extraction mechanism. +Assume $A$ and $B$ are two propositions, and the logical disjunction +$A\vee B$ is defined inductively by: +\begin{coq_example*} +Inductive or (A B:Prop) : Prop := + or_introl : A -> or A B | or_intror : B -> or A B. +\end{coq_example*} +The following definition which computes a boolean value by case over +the proof of \texttt{or A B} is not accepted: +% (***************************************************************) +% (*** This example should fail with ``Incorrect elimination'' ***) +\begin{coq_example} +Fail Definition choice (A B: Prop) (x:or A B) := + match x with or_introl _ _ a => true | or_intror _ _ b => false end. +\end{coq_example} +From the computational point of view, the structure of the proof of +\texttt{(or A B)} in this term is needed for computing the boolean +value. + +In general, if $I$ has type \Prop\ then $P$ cannot have type $I\ra +\Set$, because it will mean to build an informative proof of type +$(P~m)$ doing a case analysis over a non-computational object that +will disappear in the extracted program. But the other way is safe +with respect to our interpretation we can have $I$ a computational +object and $P$ a non-computational one, it just corresponds to proving +a logical property of a computational object. + +% Also if $I$ is in one of the sorts \{\Prop, \Set\}, one cannot in +% general allow an elimination over a bigger sort such as \Type. But +% this operation is safe whenever $I$ is a {\em small inductive} type, +% which means that all the types of constructors of +% $I$ are small with the following definition:\\ +% $(I~t_1\ldots t_s)$ is a {\em small type of constructor} and +% $\forall~x:T,C$ is a small type of constructor if $C$ is and if $T$ +% has type \Prop\ or \Set. \index{Small inductive type} + +% We call this particular elimination which gives the possibility to +% compute a type by induction on the structure of a term, a {\em strong +% elimination}\index{Strong elimination}. + +In the same spirit, elimination on $P$ of type $I\ra +\Type$ cannot be allowed because it trivially implies the elimination +on $P$ of type $I\ra \Set$ by cumulativity. It also implies that there +are two proofs of the same property which are provably different, +contradicting the proof-irrelevance property which is sometimes a +useful axiom: +\begin{coq_example} +Axiom proof_irrelevance : forall (P : Prop) (x y : P), x=y. +\end{coq_example} +\begin{coq_eval} +Reset proof_irrelevance. +\end{coq_eval} +The elimination of an inductive definition of type \Prop\ on a +predicate $P$ of type $I\ra \Type$ leads to a paradox when applied to +impredicative inductive definition like the second-order existential +quantifier \texttt{exProp} defined above, because it give access to +the two projections on this type. + +%\paragraph{Warning: strong elimination} +%\index{Elimination!Strong elimination} +%In previous versions of Coq, for a small inductive definition, only the +%non-informative strong elimination on \Type\ was allowed, because +%strong elimination on \Typeset\ was not compatible with the current +%extraction procedure. In this version, strong elimination on \Typeset\ +%is accepted but a dummy element is extracted from it and may generate +%problems if extracted terms are explicitly used such as in the +%{\tt Program} tactic or when extracting ML programs. + +\paragraph[Empty and singleton elimination]{Empty and singleton elimination\label{singleton} +\index{Elimination!Singleton elimination} +\index{Elimination!Empty elimination}} + +There are special inductive definitions in \Prop\ for which more +eliminations are allowed. +\begin{description} +\item[\Prop-extended] +\inference{ + \frac{I \mbox{~is an empty or singleton + definition}~~~s \in \Sort}{\compat{I:\Prop}{I\ra s}} +} +\end{description} +% +% A {\em singleton definition} has always an informative content, +% even if it is a proposition. +% +A {\em singleton +definition} has only one constructor and all the arguments of this +constructor have type \Prop. In that case, there is a canonical +way to interpret the informative extraction on an object in that type, +such that the elimination on any sort $s$ is legal. Typical examples are +the conjunction of non-informative propositions and the equality. +If there is an hypothesis $h:a=b$ in the local context, it can be used for +rewriting not only in logical propositions but also in any type. +% In that case, the term \verb!eq_rec! which was defined as an axiom, is +% now a term of the calculus. +\begin{coq_eval} +Require Extraction. +\end{coq_eval} +\begin{coq_example} +Print eq_rec. +Extraction eq_rec. +\end{coq_example} +An empty definition has no constructors, in that case also, +elimination on any sort is allowed. + +\paragraph{Type of branches.} +Let $c$ be a term of type $C$, we assume $C$ is a type of constructor +for an inductive type $I$. Let $P$ be a term that represents the +property to be proved. +We assume $r$ is the number of parameters and $p$ is the number of arguments. + +We define a new type \CI{c:C}{P} which represents the type of the +branch corresponding to the $c:C$ constructor. +\[ +\begin{array}{ll} +\CI{c:(I~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm] +\CI{c:\forall~x:T,C}{P} &\equiv \forall~x:T,\CI{(c~x):C}{P} +\end{array} +\] +We write \CI{c}{P} for \CI{c:C}{P} with $C$ the type of $c$. + +\paragraph{Example.} +The following term in concrete syntax: +\begin{verbatim} +match t as l return P' with +| nil _ => t1 +| cons _ hd tl => t2 +end +\end{verbatim} +can be represented in abstract syntax as $$\Case{P}{t}{f_1\,|\,f_2}$$ +where +\begin{eqnarray*} + P & = & \lambda~l~.~P^\prime\\ + f_1 & = & t_1\\ + f_2 & = & \lambda~(hd:\nat)~.~\lambda~(tl:\List~\nat)~.~t_2 +\end{eqnarray*} +According to the definition: +\begin{latexonly}\vskip.5em\noindent\end{latexonly}% +\begin{htmlonly} + +\end{htmlonly} +$ \CI{(\Nil~\nat)}{P} \equiv \CI{(\Nil~\nat) : (\List~\nat)}{P} \equiv (P~(\Nil~\nat))$ +\begin{latexonly}\vskip.5em\noindent\end{latexonly}% +\begin{htmlonly} + +\end{htmlonly} +$ \CI{(\cons~\nat)}{P} + \equiv\CI{(\cons~\nat) : (\nat\ra\List~\nat\ra\List~\nat)}{P} \equiv\\ + \equiv\forall n:\nat, \CI{(\cons~\nat~n) : \List~\nat\ra\List~\nat)}{P} \equiv\\ + \equiv\forall n:\nat, \forall l:\List~\nat, \CI{(\cons~\nat~n~l) : \List~\nat)}{P} \equiv\\ +\equiv\forall n:\nat, \forall l:\List~\nat,(P~(\cons~\nat~n~l))$. +\begin{latexonly}\vskip.5em\noindent\end{latexonly}% +\begin{htmlonly} + +\end{htmlonly} +Given some $P$, then \CI{(\Nil~\nat)}{P} represents the expected type of $f_1$, and +\CI{(\cons~\nat)}{P} represents the expected type of $f_2$. + +\paragraph{Typing rule.} + +Our very general destructor for inductive definition enjoys the +following typing rule +% , where we write +% \[ +% \Case{P}{c}{[x_{11}:T_{11}]\ldots[x_{1p_1}:T_{1p_1}]g_1\ldots +% [x_{n1}:T_{n1}]\ldots[x_{np_n}:T_{np_n}]g_n} +% \] +% for +% \[ +% \Case{P}{c}{(c_1~x_{11}~...~x_{1p_1}) \Ra g_1 ~|~\ldots~|~ +% (c_n~x_{n1}...x_{np_n}) \Ra g_n } +% \] + +\begin{description} +\item[match] \label{elimdep} \index{Typing rules!match} +\inference{ +\frac{\WTEG{c}{(I~q_1\ldots q_r~t_1\ldots t_s)}~~ + \WTEG{P}{B}~~\compat{(I~q_1\ldots q_r)}{B} + ~~ +(\WTEG{f_i}{\CI{(c_{p_i}~q_1\ldots q_r)}{P}})_{i=1\ldots l}} +{\WTEG{\Case{P}{c}{f_1|\ldots |f_l}}{(P\ t_1\ldots t_s\ c)}}}%\\[3mm] + +provided $I$ is an inductive type in a definition +\Ind{}{r}{\Gamma_I}{\Gamma_C} with +$\Gamma_C = [c_1:C_1;\ldots;c_n:C_n]$ and $c_{p_1}\ldots c_{p_l}$ are the +only constructors of $I$. +\end{description} + +\paragraph{Example.} + +Below is a typing rule for the term shown in the previous example: +\inference{ + \frac{% + \WTEG{t}{(\List~\nat)}~~~~% + \WTEG{P}{B}~~~~% + \compat{(\List~\nat)}{B}~~~~% + \WTEG{f_1}{\CI{(\Nil~\nat)}{P}}~~~~% + \WTEG{f_2}{\CI{(\cons~\nat)}{P}}% + } +{\WTEG{\Case{P}{t}{f_1|f_2}}{(P~t)}}} + +\paragraph[Definition of $\iota$-reduction.]{Definition of $\iota$-reduction.\label{iotared} +\index{iota-reduction@$\iota$-reduction}} +We still have to define the $\iota$-reduction in the general case. + +A $\iota$-redex is a term of the following form: +\[\Case{P}{(c_{p_i}~q_1\ldots q_r~a_1\ldots a_m)}{f_1|\ldots | + f_l}\] +with $c_{p_i}$ the $i$-th constructor of the inductive type $I$ with $r$ +parameters. + +The $\iota$-contraction of this term is $(f_i~a_1\ldots a_m)$ leading +to the general reduction rule: +\[ \Case{P}{(c_{p_i}~q_1\ldots q_r~a_1\ldots a_m)}{f_1|\ldots | + f_n} \triangleright_{\iota} (f_i~a_1\ldots a_m) \] + +\subsection[Fixpoint definitions]{Fixpoint definitions\label{Fix-term} \index{Fix@{\tt Fix}}} +The second operator for elimination is fixpoint definition. +This fixpoint may involve several mutually recursive definitions. +The basic concrete syntax for a recursive set of mutually recursive +declarations is (with $\Gamma_i$ contexts): +\[\kw{fix}~f_1 (\Gamma_1) :A_1:=t_1~\kw{with} \ldots \kw{with}~ f_n +(\Gamma_n) :A_n:=t_n\] +The terms are obtained by projections from this set of declarations +and are written +\[\kw{fix}~f_1 (\Gamma_1) :A_1:=t_1~\kw{with} \ldots \kw{with}~ f_n +(\Gamma_n) :A_n:=t_n~\kw{for}~f_i\] +In the inference rules, we represent such a +term by +\[\Fix{f_i}{f_1:A_1':=t_1' \ldots f_n:A_n':=t_n'}\] +with $t_i'$ (resp. $A_i'$) representing the term $t_i$ abstracted +(resp. generalized) with +respect to the bindings in the context $\Gamma_i$, namely +$t_i'=\lb \Gamma_i \mto t_i$ and $A_i'=\forall \Gamma_i, A_i$. + +\subsubsection{Typing rule} +The typing rule is the expected one for a fixpoint. + +\begin{description} +\item[Fix] \index{Typing rules!Fix} +\inference{\frac{(\WTEG{A_i}{s_i})_{i=1\ldots n}~~~~ + (\WTE{\Gamma,f_1:A_1,\ldots,f_n:A_n}{t_i}{A_i})_{i=1\ldots n}} + {\WTEG{\Fix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}}{A_i}}} +\end{description} +% +Any fixpoint definition cannot be accepted because non-normalizing terms +allow proofs of absurdity. +% +The basic scheme of recursion that should be allowed is the one needed for +defining primitive +recursive functionals. In that case the fixpoint enjoys a special +syntactic restriction, namely one of the arguments belongs to an +inductive type, the function starts with a case analysis and recursive +calls are done on variables coming from patterns and representing subterms. +% +For instance in the case of natural numbers, a proof of the induction +principle of type +\[\forall P:\nat\ra\Prop, (P~\nO)\ra(\forall n:\nat, (P~n)\ra(P~(\nS~n)))\ra +\forall n:\nat, (P~n)\] +can be represented by the term: +\[\begin{array}{l} +\lb P:\nat\ra\Prop\mto\lb f:(P~\nO)\mto \lb g:(\forall n:\nat, +(P~n)\ra(P~(\nS~n))) \mto\\ +\Fix{h}{h:\forall n:\nat, (P~n):=\lb n:\nat\mto \Case{P}{n}{f~|~\lb + p:\nat\mto (g~p~(h~p))}} +\end{array} +\] +% +Before accepting a fixpoint definition as being correctly typed, we +check that the definition is ``guarded''. A precise analysis of this +notion can be found in~\cite{Gim94}. +% +The first stage is to precise on which argument the fixpoint will be +decreasing. The type of this argument should be an inductive +definition. +% +For doing this, the syntax of fixpoints is extended and becomes + \[\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}\] +where $k_i$ are positive integers. +Each $k_i$ represents the index of pararameter of $f_i$, on which $f_i$ is decreasing. +Each $A_i$ should be a type (reducible to a term) starting with at least +$k_i$ products $\forall y_1:B_1,\ldots \forall y_{k_i}:B_{k_i}, A'_i$ +and $B_{k_i}$ an is unductive type. + +Now in the definition $t_i$, if $f_j$ occurs then it should be applied +to at least $k_j$ arguments and the $k_j$-th argument should be +syntactically recognized as structurally smaller than $y_{k_i}$ + + +The definition of being structurally smaller is a bit technical. +One needs first to define the notion of +{\em recursive arguments of a constructor}\index{Recursive arguments}. +For an inductive definition \Ind{}{r}{\Gamma_I}{\Gamma_C}, +if the type of a constructor $c$ has the form +$\forall p_1:P_1,\ldots \forall p_r:P_r, +\forall x_1:T_1, \ldots \forall x_r:T_r, (I_j~p_1\ldots +p_r~t_1\ldots t_s)$, then the recursive arguments will correspond to $T_i$ in +which one of the $I_l$ occurs. + +The main rules for being structurally smaller are the following:\\ +Given a variable $y$ of type an inductive +definition in a declaration +\Ind{}{r}{\Gamma_I}{\Gamma_C} +where $\Gamma_I$ is $[I_1:A_1;\ldots;I_k:A_k]$, and $\Gamma_C$ is + $[c_1:C_1;\ldots;c_n:C_n]$. +The terms structurally smaller than $y$ are: +\begin{itemize} +\item $(t~u)$ and $\lb x:u \mto t$ when $t$ is structurally smaller than $y$. +\item \Case{P}{c}{f_1\ldots f_n} when each $f_i$ is structurally + smaller than $y$. \\ + If $c$ is $y$ or is structurally smaller than $y$, its type is an inductive + definition $I_p$ part of the inductive + declaration corresponding to $y$. + Each $f_i$ corresponds to a type of constructor $C_q \equiv + \forall p_1:P_1,\ldots,\forall p_r:P_r, \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$ + and can consequently be + written $\lb y_1:B'_1\mto \ldots \lb y_k:B'_k\mto g_i$. + ($B'_i$ is obtained from $B_i$ by substituting parameters variables) + the variables $y_j$ occurring + in $g_i$ corresponding to recursive arguments $B_i$ (the ones in + which one of the $I_l$ occurs) are structurally smaller than $y$. +\end{itemize} +The following definitions are correct, we enter them using the +{\tt Fixpoint} command as described in Section~\ref{Fixpoint} and show +the internal representation. +\begin{coq_example} +Fixpoint plus (n m:nat) {struct n} : nat := + match n with + | O => m + | S p => S (plus p m) + end. +Print plus. +Fixpoint lgth (A:Set) (l:list A) {struct l} : nat := + match l with + | nil _ => O + | cons _ a l' => S (lgth A l') + end. +Print lgth. +Fixpoint sizet (t:tree) : nat := let (f) := t in S (sizef f) + with sizef (f:forest) : nat := + match f with + | emptyf => O + | consf t f => plus (sizet t) (sizef f) + end. +Print sizet. +\end{coq_example} + + +\subsubsection[Reduction rule]{Reduction rule\index{iota-reduction@$\iota$-reduction}} +Let $F$ be the set of declarations: $f_1/k_1:A_1:=t_1 \ldots +f_n/k_n:A_n:=t_n$. +The reduction for fixpoints is: +\[ (\Fix{f_i}{F}~a_1\ldots +a_{k_i}) \triangleright_{\iota} \substs{t_i}{f_k}{\Fix{f_k}{F}}{k=1\ldots n} +~a_1\ldots a_{k_i}\] +when $a_{k_i}$ starts with a constructor. +This last restriction is needed in order to keep strong normalization +and corresponds to the reduction for primitive recursive operators. +% +The following reductions are now possible: +\def\plus{\mathsf{plus}} +\def\tri{\triangleright_\iota} +\begin{eqnarray*} + \plus~(\nS~(\nS~\nO))~(\nS~\nO) & \tri & \nS~(\plus~(\nS~\nO)~(\nS~\nO))\\ + & \tri & \nS~(\nS~(\plus~\nO~(\nS~\nO)))\\ + & \tri & \nS~(\nS~(\nS~\nO))\\ +\end{eqnarray*} + +% La disparition de Program devrait rendre la construction Match obsolete +% \subsubsection{The {\tt Match \ldots with \ldots end} expression} +% \label{Matchexpr} +% %\paragraph{A unary {\tt Match\ldots with \ldots end}.} +% \index{Match...with...end@{\tt Match \ldots with \ldots end}} +% The {\tt Match} operator which was a primitive notion in older +% presentations of the Calculus of Inductive Constructions is now just a +% macro definition which generates the good combination of {\tt Case} +% and {\tt Fix} operators in order to generate an operator for primitive +% recursive definitions. It always considers an inductive definition as +% a single inductive definition. + +% The following examples illustrates this feature. +% \begin{coq_example} +% Definition nat_pr : (C:Set)C->(nat->C->C)->nat->C +% :=[C,x,g,n]Match n with x g end. +% Print nat_pr. +% \end{coq_example} +% \begin{coq_example} +% Definition forest_pr +% : (C:Set)C->(tree->forest->C->C)->forest->C +% := [C,x,g,n]Match n with x g end. +% \end{coq_example} + +% Cet exemple faisait error (HH le 12/12/96), j'ai change pour une +% version plus simple +%\begin{coq_example} +%Definition forest_pr +% : (P:forest->Set)(P emptyf)->((t:tree)(f:forest)(P f)->(P (consf t f))) +% ->(f:forest)(P f) +% := [C,x,g,n]Match n with x g end. +%\end{coq_example} + +\subsubsection{Mutual induction} + +The principles of mutual induction can be automatically generated +using the {\tt Scheme} command described in Section~\ref{Scheme}. + +\section{Admissible rules for global environments} + +From the original rules of the type system, one can show the +admissibility of rules which change the local context of definition of +objects in the global environment. We show here the admissible rules +that are used used in the discharge mechanism at the end of a section. + +% This is obsolete: Abstraction over defined constants actually uses a +% let-in since there are let-ins in Coq + +%% \paragraph{Mechanism of substitution.} + +%% One rule which can be proved valid, is to replace a term $c$ by its +%% value in the global environment. As we defined the substitution of a term for +%% a variable in a term, one can define the substitution of a term for a +%% constant. One easily extends this substitution to local contexts and global +%% environments. + +%% \paragraph{Substitution Property:} +%% \inference{\frac{\WF{E;c:=t:T; E'}{\Gamma}} +%% {\WF{E; \subst{E'}{c}{t}}{\subst{\Gamma}{c}{t}}}} + +\paragraph{Abstraction.} + +One can modify a global declaration by generalizing it over a +previously assumed constant $c$. For doing that, we need to modify the +reference to the global declaration in the subsequent global +environment and local context by explicitly applying this constant to +the constant $c'$. + +Below, if $\Gamma$ is a context of the form +$[y_1:A_1;\ldots;y_n:A_n]$, we write $\forall +x:U,\subst{\Gamma}{c}{x}$ to mean +$[y_1:\forall~x:U,\subst{A_1}{c}{x};\ldots;y_n:\forall~x:U,\subst{A_n}{c}{x}]$ +and +$\subst{E}{|\Gamma|}{|\Gamma|c}$. +to mean the parallel substitution +$\subst{\subst{E}{y_1}{(y_1~c)}\ldots}{y_n}{(y_n~c)}$. + +\paragraph{First abstracting property:} + \inference{\frac{\WF{E;c:U;E';c':=t:T;E''}{\Gamma}} + {\WF{E;c:U;E';c':=\lb x:U\mto \subst{t}{c}{x}:\forall~x:U,\subst{T}{c}{x}; + \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}} + + \inference{\frac{\WF{E;c:U;E';c':T;E''}{\Gamma}} + {\WF{E;c:U;E';c':\forall~x:U,\subst{T}{c}{x}; + \subst{E''}{c'}{(c'~c)}}{\subst{\Gamma}{c}{(c~c')}}}} + + \inference{\frac{\WF{E;c:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}} + {\WFTWOLINES{E;c:U;E';\Ind{}{p+1}{\forall x:U,\subst{\Gamma_I}{c}{x}}{\forall x:U,\subst{\Gamma_C}{c}{x}};\subst{E''}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}{\subst{\Gamma}{|\Gamma_I,\Gamma_C|}{|\Gamma_I,\Gamma_C|~c}}}} +% +One can similarly modify a global declaration by generalizing it over +a previously defined constant~$c'$. Below, if $\Gamma$ is a context +of the form $[y_1:A_1;\ldots;y_n:A_n]$, we write $ +\subst{\Gamma}{c}{u}$ to mean +$[y_1:\subst{A_1}{c}{u};\ldots;y_n:\subst{A_n}{c}{u}]$. + +\paragraph{Second abstracting property:} + \inference{\frac{\WF{E;c:=u:U;E';c':=t:T;E''}{\Gamma}} + {\WF{E;c:=u:U;E';c':=(\letin{x}{u:U}{\subst{t}{c}{x}}):\subst{T}{c}{u};E''}{\Gamma}}} + + \inference{\frac{\WF{E;c:=u:U;E';c':T;E''}{\Gamma}} + {\WF{E;c:=u:U;E';c':\subst{T}{c}{u};E''}{\Gamma}}} + + \inference{\frac{\WF{E;c:=u:U;E';\Ind{}{p}{\Gamma_I}{\Gamma_C};E''}{\Gamma}} + {\WF{E;c:=u:U;E';\Ind{}{p}{\subst{\Gamma_I}{c}{u}}{\subst{\Gamma_C}{c}{u}};E''}{\Gamma}}} + +\paragraph{Pruning the local context.} +If one abstracts or substitutes constants with the above rules then it +may happen that some declared or defined constant does not occur any +more in the subsequent global environment and in the local context. One can +consequently derive the following property. + +\paragraph{First pruning property:} +\inference{\frac{\WF{E;c:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}} + {\WF{E;E'}{\Gamma}}} + +\paragraph{Second pruning property:} +\inference{\frac{\WF{E;c:=u:U;E'}{\Gamma} \qquad c \mbox{ does not occur in $E'$ and $\Gamma$}} + {\WF{E;E'}{\Gamma}}} + +\section{Co-inductive types} +The implementation contains also co-inductive definitions, which are +types inhabited by infinite objects. +More information on co-inductive definitions can be found +in~\cite{Gimenez95b,Gim98,GimCas05}. +%They are described in Chapter~\ref{Co-inductives}. + +\section[The Calculus of Inductive Construction with + impredicative \Set]{The Calculus of Inductive Construction with + impredicative \Set\label{impredicativity}} + +\Coq{} can be used as a type-checker for the +Calculus of Inductive Constructions with an impredicative sort \Set{} +by using the compiler option \texttt{-impredicative-set}. +% +For example, using the ordinary \texttt{coqtop} command, the following +is rejected. +% (** This example should fail ******************************* +% Error: The term forall X:Set, X -> X has type Type +% while it is expected to have type Set ***) +\begin{coq_example} +Fail Definition id: Set := forall X:Set,X->X. +\end{coq_example} +while it will type-check, if one uses instead the \texttt{coqtop + -impredicative-set} command. + +The major change in the theory concerns the rule for product formation +in the sort \Set, which is extended to a domain in any sort: +\begin{description} +\item [Prod] \index{Typing rules!Prod (impredicative Set)} +\inference{\frac{\WTEG{T}{s}~~~~s \in \Sort~~~~~~ + \WTE{\Gamma::(x:T)}{U}{\Set}} + { \WTEG{\forall~x:T,U}{\Set}}} +\end{description} +This extension has consequences on the inductive definitions which are +allowed. +In the impredicative system, one can build so-called {\em large inductive + definitions} like the example of second-order existential +quantifier (\texttt{exSet}). + +There should be restrictions on the eliminations which can be +performed on such definitions. The eliminations rules in the +impredicative system for sort \Set{} become: +\begin{description} +\item[\Set] \inference{\frac{s \in + \{\Prop, \Set\}}{\compat{I:\Set}{I\ra s}} +~~~~\frac{I \mbox{~is a small inductive definition}~~~~s \in + \{\Type(i)\}} + {\compat{I:\Set}{I\ra s}}} +\end{description} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: + + -- cgit v1.2.3