summaryrefslogtreecommitdiff
path: root/doc/refman/RefMan-cic.tex
diff options
context:
space:
mode:
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
-rw-r--r--doc/refman/RefMan-cic.tex267
1 files changed, 175 insertions, 92 deletions
diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex
index 18b6ed9c..e288cdfb 100644
--- a/doc/refman/RefMan-cic.tex
+++ b/doc/refman/RefMan-cic.tex
@@ -223,8 +223,8 @@ 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$. Contexts must be
themselves {\em well formed}. For the rest of the chapter, the
-notation $\Gamma::(y:T)$ (resp $\Gamma::(y:=t:T)$) denotes the context
-$\Gamma$ enriched with the declaration $y:T$ (resp $y:=t:T$). The
+notation $\Gamma::(y:T)$ (resp. $\Gamma::(y:=t:T)$) denotes the context
+$\Gamma$ enriched with the declaration $y:T$ (resp. $y:=t:T$). The
notation $[]$ denotes the empty context. \index{Context}
% Does not seem to be used further...
@@ -579,46 +579,95 @@ inductively as being an inductive family of type $\Set\ra\Set$:
\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
\ra (\List~A) \ra (\List~A)}\]
There are drawbacks to this point of view. The
-information which says that $(\List~\nat)$ is an inductively defined
+information which says that for any $A$, $(\List~A)$ is an inductively defined
\Set\ has been lost.
+So we introduce two important definitions.
+
+\paragraph{Inductive parameters, real arguments.}
+An inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits
+$r$ inductive parameters if each type of constructors $(c:C)$ in
+$\Gamma_C$ is such that
+\[C\equiv \forall
+p_1:P_1,\ldots,\forall p_r:P_r,\forall a_1:A_1, \ldots \forall a_n:A_n,
+(I~p_1~\ldots p_r~t_1\ldots t_q)\]
+with $I$ one of the inductive definitions in $\Gamma_I$.
+We say that $n$ is the number of real arguments of the constructor
+$c$.
+\paragraph{Context of parameters}
+If an inductive definition $\NInd{\Gamma}{\Gamma_I}{\Gamma_C}$ admits
+$r$ inductive parameters, then there exists a context $\Gamma_P$ of
+size $r$, such that $\Gamma_P=p_1:P_1;\ldots;\forall p_r:P_r$ and
+if $(t:A)\in\Gamma_I,\Gamma_C$ then $A$ can be written as
+$\forall p_1:P_1,\ldots \forall p_r:P_r,A'$.
+We call $\Gamma_P$ the context of parameters of the inductive
+definition and use the notation $\forall \Gamma_P,A'$ for the term $A$.
+\paragraph{Remark.}
+If we have a term $t$ in an instance of an
+inductive definition $I$ which starts with a constructor $c$, then the
+$r$ first arguments of $c$ (the parameters) can be deduced from the
+type $T$ of $t$: these are exactly the $r$ first arguments of $I$ in
+the head normal form of $T$.
+\paragraph{Examples.}
+The \List{} definition has $1$ parameter:
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+ \ra (\List~A) \ra (\List~A)}\]
+This is also the case for this more complex definition where there is
+a recursive argument on a different instance of \List:
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+ \ra (\List~A\ra A) \ra (\List~A)}\]
+But the following definition has $0$ parameters:
+\[\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
+ \ra (\List~A) \ra (\List~A*A)}\]
+
%\footnote{
-%The interested reader may look at the compare the above definition with the two
+%The interested reader may compare the above definition with the two
%following ones which have very different logical meaning:\\
%$\NInd{}{\List:\Set}{\Nil:\List,\cons : (A:\Set)A
% \ra \List \ra \List}$ \\
%$\NInd{}{\List:\Set\ra\Set}{\Nil:(A:\Set)(\List~A),\cons : (A:\Set)A
% \ra (\List~A\ra A) \ra (\List~A)}$.}
-
-In the system, we keep track in the syntax of the context of
-parameters. The idea of these parameters is that they can be
-instantiated and still we have an inductive definition for which we
-know the specification.
+\paragraph{Concrete syntax.}
+In the Coq system, the context of parameters is given explicitly
+after the name of the inductive definitions and is shared between the
+arities and the type of constructors.
+% The vernacular declaration of polymorphic trees and forests will be:\\
+% \begin{coq_example*}
+% Inductive Tree (A:Set) : Set :=
+% Node : A -> Forest A -> Tree A
+% with Forest (A : Set) : Set :=
+% Empty : Forest A
+% | Cons : Tree A -> Forest A -> Forest A
+% \end{coq_example*}
+% will correspond in our formalism to:
+% \[\NInd{}{{\tt Tree}:\Set\ra\Set;{\tt Forest}:\Set\ra \Set}
+% {{\tt Node} : \forall A:\Set, A \ra {\tt Forest}~A \ra {\tt Tree}~A,
+% {\tt Empty} : \forall A:\Set, {\tt Forest}~A,
+% {\tt Cons} : \forall A:\Set, {\tt Tree}~A \ra {\tt Forest}~A \ra
+% {\tt Forest}~A}\]
+We keep track in the syntax of the number of
+parameters.
Formally the representation of an inductive declaration
will be
-\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} for an inductive
-definition valid in a context $\Gamma$ with parameters $\Gamma_P$, a
+\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} for an inductive
+definition valid in a context $\Gamma$ with $p$ parameters, a
context of definitions $\Gamma_I$ and a context of constructors
$\Gamma_C$.
-The occurrences of the variables of $\Gamma_P$ in the contexts
-$\Gamma_I$ and $\Gamma_C$ are bound.
-The definition \Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} will be
-well-formed exactly when \NInd{\Gamma,\Gamma_P}{\Gamma_I}{\Gamma_C} is.
-If $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$, an object in
-\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} applied to $q_1,\ldots,q_r$
-will behave as the corresponding object of
-\NInd{\Gamma}{\substs{\Gamma_I}{p_i}{q_i}{i=1..r}}{\substs{\Gamma_C}{p_i}{q_i}{i=1..r}}.
+The definition \Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} will be
+well-formed exactly when \NInd{\Gamma}{\Gamma_I}{\Gamma_C} is and
+when $p$ is (less or equal than) the number of parameters in
+\NInd{\Gamma}{\Gamma_I}{\Gamma_C}.
\paragraph{Examples}
The declaration for parameterized lists is:
-\[\Ind{}{A:\Set}{\List:\Set}{\Nil:\List,\cons : A \ra \List \ra
- \List}\]
+\[\Ind{}{1}{\List:\Set\ra\Set}{\Nil:\forall A:\Set,\List~A,\cons : \forall
+ A:\Set, A \ra \List~A \ra \List~A}\]
The declaration for the length of lists is:
-\[\Ind{}{A:\Set}{\Length:(\List~A)\ra \nat\ra\Prop}
- {\LNil:(\Length~(\Nil~A)~\nO),\\
- \LCons :\forall a:A, \forall l:(\List~A),\forall n:\nat, (\Length~l~n)\ra (\Length~(\cons~A~a~l)~(\nS~n))}\]
+\[\Ind{}{1}{\Length:\forall A:\Set, (\List~A)\ra \nat\ra\Prop}
+ {\LNil:\forall A:\Set, \Length~A~(\Nil~A)~\nO,\\
+ \LCons :\forall A:\Set,\forall a:A, \forall l:(\List~A),\forall n:\nat, (\Length~A~l~n)\ra (\Length~A~(\cons~A~a~l)~(\nS~n))}\]
The declaration for a mutual inductive definition of forests and trees is:
\[\NInd{}{\tree:\Set,\forest:\Set}
@@ -647,14 +696,17 @@ with forest : Set :=
| emptyf : forest
| consf : tree -> forest -> forest.
\end{coq_example*}
-The inductive declaration in \Coq\ is slightly different from the one
-we described theoretically. The difference is that in the type of
-constructors the inductive definition is explicitly applied to the
-parameters variables. The \Coq\ type-checker verifies that all
-parameters are applied in the correct manner in each recursive call.
+% The inductive declaration in \Coq\ is slightly different from the one
+% we described theoretically. The difference is that in the type of
+% constructors the inductive definition is explicitly applied to the
+% parameters variables.
+The \Coq\ type-checker verifies that all
+parameters are applied in the correct manner in the conclusion of the
+type of each constructors~:
+
In particular, the following definition will not be accepted because
there is an occurrence of \List\ which is not applied to the parameter
-variable:
+variable in the conclusion of the type of {\tt cons'}:
\begin{coq_eval}
Set Printing Depth 50.
(********** The following is not correct and should produce **********)
@@ -663,25 +715,33 @@ Set Printing Depth 50.
\begin{coq_example}
Inductive list' (A:Set) : Set :=
| nil' : list' A
- | cons' : A -> list' (A -> A) -> list' A.
+ | cons' : A -> list' A -> list' (A*A).
+\end{coq_example}
+Since \Coq{} version 8.1, there is no restriction about parameters in
+the types of arguments of constructors. The following definition is
+valid:
+\begin{coq_example}
+Inductive list' (A:Set) : Set :=
+ | nil' : list' A
+ | cons' : A -> list' (A->A) -> list' A.
\end{coq_example}
+
\subsection{Types of inductive objects}
We have to give the type of constants in an environment $E$ which
contains an inductive declaration.
\begin{description}
-\item[Ind-Const] Assuming $\Gamma_P$ is $[p_1:P_1;\ldots;p_r:P_r]$,
+\item[Ind-Const] Assuming
$\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]$,
-\inference{\frac{\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} \in E
- ~~j=1\ldots k}{(I_j:\forall~p_1:P_1,\ldots\forall p_r:P_r,A_j) \in E}}
+\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
+ ~~j=1\ldots k}{(I_j:A_j) \in E}}
-\inference{\frac{\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} \in E
+\inference{\frac{\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C} \in E
~~~~i=1.. n}
- {(c_i:\forall~p_1:P_1,\ldots \forall p_r:P_r,\subst{C_i}{I_j}{(I_j~p_1\ldots
- p_r)}_{j=1\ldots k})\in E}}
+ {(c_i:C_i)\in E}}
\end{description}
\paragraph{Example.}
@@ -745,10 +805,13 @@ following cases:
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}{p_1:P_1;\ldots;p_m:P_m}{I:A}{c_1:C_1;\ldots;c_n:C_n}$
+ $\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
- types of constructor $C_i\{p_j/a_j\}_{j=1\ldots m}$ of $I$ satisfy
+ (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
@@ -760,15 +823,16 @@ positivity condition} for a constant $X$ in the following
cases:
\begin{itemize}
-\item $T=(I~t_1\ldots ~t_n)$ and $X$ does not occur in
-any $t_i$
+\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}
\paragraph{Example}
-$X$ occurs strictly positively in $A\ra X$ or $X*A$ or $({\tt list}
+$X$ occurs strictly positively in $A\ra X$ or $X*A$ or $({\tt list}~
X)$ but not in $X \ra A$ or $(X \ra A)\ra A$ nor $({\tt neg}~A)$
assuming the notion of product and lists were already defined and {\tt
neg} is an inductive definition with declaration \Ind{}{A:\Set}{{\tt
@@ -784,17 +848,20 @@ inductive definition.
\begin{description}
\item[W-Ind] Let $E$ be an environment and
$\Gamma,\Gamma_P,\Gamma_I,\Gamma_C$ are contexts such that
- $\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]$.
+ $\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;\Gamma_P}{A_j}{s'_j})_{j=1\ldots k}
- ~~ (\WTE{\Gamma;\Gamma_P;\Gamma_I}{C_i}{s_{p_i}})_{i=1\ldots n}
+ ~~ (\WTE{\Gamma;\Gamma_I;\Gamma_P}{C_i}{s_{p_i}})_{i=1\ldots n}
}
- {\WF{E;\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
+ {\WF{E;\Ind{\Gamma}{p}{\Gamma_I}{\Gamma_C}}{\Gamma}}}
providing the following side conditions hold:
\begin{itemize}
\item $k>0$, $I_j$, $c_i$ are different names for $j=1\ldots k$ and $i=1\ldots n$,
+\item $p$ is the number of parameters of \NInd{\Gamma}{\Gamma_I}{\Gamma_C}
+ and $\Gamma_P$ is the context of parameters,
\item for $j=1\ldots k$ we have $A_j$ is an arity of sort $s_j$ and $I_j
\notin \Gamma \cup E$,
\item for $i=1\ldots n$ we have $C_i$ is a type of constructor of
@@ -809,7 +876,7 @@ constructors which will always be satisfied for the impredicative sort
on sort \Set{} and generate constraints between universes for
inductive definitions in types.
-\paragraph{Examples}
+\paragraph{Examples.}
It is well known that existential quantifier can be encoded as an
inductive definition.
The following declaration introduces the second-order existential
@@ -862,7 +929,7 @@ ourselves to primitive recursive functions and functionals.
For instance, assuming a parameter $A:\Set$ exists in the 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) = \nO$
+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.
@@ -883,7 +950,7 @@ principles.
For instance, in order to prove $\forall l:\ListA,(\LengthA~l~(\length~l))$
it is enough to prove:
-\noindent $(\LengthA~\Nil~(\length~\Nil))$ and
+\noindent $(\LengthA~(\Nil~A)~(\length~(\Nil~A)))$ and
\smallskip
$\forall a:A, \forall l:\ListA, (\LengthA~l~(\length~l)) \ra
@@ -892,7 +959,7 @@ $\forall a:A, \forall l:\ListA, (\LengthA~l~(\length~l)) \ra
\noindent which given the conversion equalities satisfied by \length\ is the
same as proving:
-$(\LengthA~\Nil~\nO)$ and $\forall a:A, \forall l:\ListA,
+$(\LengthA~(\Nil~A)~\nO)$ and $\forall a:A, \forall l:\ListA,
(\LengthA~l~(\length~l)) \ra
(\LengthA~(\cons~A~a~l)~(\nS~(\length~l)))$.
@@ -928,35 +995,51 @@ by the $u_1\ldots u_p$ according to the $\iota$-reduction.
Actually, for type-checking a \kw{match\ldots with\ldots end}
expression we also need to know the predicate $P$ to be proved by case
-analysis. \Coq{} can sometimes infer this predicate but sometimes
-not. The concrete syntax for describing this predicate uses the
-\kw{as\ldots return} construction.
-The predicate is made explicit using the syntax~:
-\[\kw{match}~m~\kw{as}~ x~ \kw{return}~ (P~ x) ~\kw{with}~ (c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~
+analysis. In the general case where $I$ is an inductively defined
+$n$-ary relation, $P$ is a $n+1$-ary relation: the $n$ first arguments
+correspond to the arguments of $I$ (parameters excluded), and the last
+one corresponds to object $m$. \Coq{} can sometimes infer this
+predicate but sometimes not. The concrete syntax for describing this
+predicate uses the \kw{as\ldots in\ldots return} construction. For
+instance, let us assume that $I$ is an unary predicate with one
+parameter. The predicate is made explicit using the syntax~:
+\[\kw{match}~m~\kw{as}~ x~ \kw{in}~ I~\verb!_!~a~ \kw{return}~ (P~ x)
+ ~\kw{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, the result type can depend on $m$). The \kw{in} part can be
+omitted if the result type does not depend on the arguments of
+$I$. Note that the arguments of $I$ corresponding to parameters
+\emph{must} be \verb!_!, because the result type is not generalized to
+all possible values of the parameters. The expression after \kw{in}
+must be seen as an \emph{inductive type pattern}. As a final remark,
+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 x \mto P)}{m}{ \lb x_{11}~...~x_{1p_1} \mto f_1 ~|~\ldots~|~
+\[ \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}\]
-This is the basic idea which is generalized to the case where $I$ is
-an inductively defined $n$-ary relation (in which case the property
-$P$ to be proved will be a $n+1$-ary relation).
-
-
-\paragraph{Non-dependent elimination.}
-When defining a function by case analysis, we build an object of type $I
-\ra C$ and the minimality principle on an inductively defined logical
-predicate of type $A \ra \Prop$ is often used to prove a property
-$\forall x:A,(I~x)\ra (C~x)$. This is a particular case 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:
-
-\[\lb~l:\ListA \mto\Case{\bool}{l}{\Nil~ \Ra~\true~ |~ (\cons~a~m)~ \Ra~\false}\]
+%% 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
@@ -973,9 +1056,9 @@ what can be the type of $P$ with respect to the type of the inductive
definitions.
We define now a relation \compat{I:A}{B} between an inductive
-definition $I$ of type $A$, an arity $B$ which says that an object in
-the inductive definition $I$ can be eliminated for proving a property
-$P$ of type $B$.
+definition $I$ of type $A$ and an arity $B$. This relation states that
+an object in the inductive definition $I$ can be eliminated for
+proving a property $P$ of type $B$.
The case of inductive definitions in sorts \Set\ or \Type{} is simple.
There is no restriction on the sort of the predicate to be
@@ -995,7 +1078,7 @@ $I$.
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
+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.
@@ -1161,10 +1244,10 @@ following typing rule
\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]
+{\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 declaration
-\Ind{\Delta}{\Gamma_P}{\Gamma_I}{\Gamma_C} with $|\Gamma_P| = r$,
+\Ind{\Delta}{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}
@@ -1176,7 +1259,7 @@ context being the same in all the judgments).
\[\frac{l:\ListA~~P:\ListA\ra s~~~f_1:(P~(\Nil~A))~~
f_2:\forall a:A, \forall l:\ListA, (P~(\cons~A~a~l))}
- {\Case{P}{l}{f_1~f_2}:(P~l)}\]
+ {\Case{P}{l}{f_1~|~f_2}:(P~l)}\]
\[\frac{
\begin{array}[b]{@{}c@{}}
@@ -1186,21 +1269,21 @@ H:(\LengthA~L~N) \\ P:\forall l:\ListA, \forall n:\nat, (\LengthA~l~n)\ra
f_2:\forall a:A, \forall l:\ListA, \forall n:\nat, \forall
h:(\LengthA~l~n), (P~(\cons~A~a~n)~(\nS~n)~(\LCons~A~a~l~n~h))
\end{array}}
- {\Case{P}{H}{f_1~f_2}:(P~L~N~H)}\]
+ {\Case{P}{H}{f_1~|~f_2}:(P~L~N~H)}\]
\paragraph{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
+\[\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
+\[ \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}
@@ -1245,13 +1328,13 @@ 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((n:\nat)(P~n)\ra(P~(\nS~n)))\ra
+\[\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
+\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}
\]
@@ -1280,8 +1363,8 @@ 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{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C},
-the type of a constructor $c$ have the form
+For an inductive definition \Ind{\Gamma}{r}{\Gamma_I}{\Gamma_C},
+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)$ the recursive arguments will correspond to $T_i$ in
@@ -1291,7 +1374,7 @@ 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{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C}
+\Ind{\Gamma}{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:
@@ -1303,7 +1386,7 @@ The terms structurally smaller than $y$ are:
definition $I_p$ part of the inductive
declaration corresponding to $y$.
Each $f_i$ corresponds to a type of constructor $C_q \equiv
- \forall y_1:B_1, \ldots \forall y_k:B_k, (I~a_1\ldots a_k)$
+ \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)
@@ -1420,7 +1503,7 @@ The implementation contains also coinductive definitions, which are
types inhabited by infinite objects.
More information on coinductive definitions can be found
in~\cite{Gimenez95b,Gim98}.
-%They are described inchapter~\ref{Coinductives}.
+%They are described in chapter~\ref{Coinductives}.
\section{\iCIC : the Calculus of Inductive Construction with
impredicative \Set}\label{impredicativity}
@@ -1470,7 +1553,7 @@ impredicative system for sort \Set{} become~:
-% $Id: RefMan-cic.tex 8609 2006-02-24 13:32:57Z notin,no-port-forwarding,no-agent-forwarding,no-X11-forwarding,no-pty $
+% $Id: RefMan-cic.tex 8914 2006-06-07 14:57:22Z cpaulin $
%%% Local Variables:
%%% mode: latex
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-13 14:47:28 +0000