diff options
author | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-06-16 14:41:51 +0000 |
commit | e978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch) | |
tree | 0de2a907ee93c795978f3c843155bee91c11ed60 /doc/refman/RefMan-cic.tex | |
parent | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff) |
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'doc/refman/RefMan-cic.tex')
-rw-r--r-- | doc/refman/RefMan-cic.tex | 267 |
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 |