From 0ea779c11d93d273be35fd07c5e7d4936f3a9468 Mon Sep 17 00:00:00 2001 From: cpaulin Date: Wed, 7 Jun 2006 14:57:22 +0000 Subject: Nouveaux Parametres Inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8914 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/refman/RefMan-cic.tex | 88 ++++++++++++++++++++++++----------------------- 1 file changed, 45 insertions(+), 43 deletions(-) diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index 7f15d57d7..b39577fe0 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... @@ -596,15 +596,15 @@ $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$, suche that $\Gamma_p=p_1:P_1;\ldots;\forall p_r:P_r$ and +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 $A=\forall \Gamma_P,A'$. +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 parameter) can be deduced from 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.} @@ -620,17 +620,16 @@ But the following definition has $0$ parameters: \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)}$.} \paragraph{Concrete syntax.} -In the Coq system, the context of parameters is given explicitely -after the name of the inductive definitions and is shared beween the +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 := @@ -645,7 +644,7 @@ arities and the type of constructors. % {\tt Empty} : \forall A:\Set, {\tt Forest}~A, % {\tt Cons} : \forall A:\Set, {\tt Tree}~A \ra {\tt Forest}~A \ra % {\tt Forest}~A}\] -In the system, we keep track in the syntax of the number of +We keep track in the syntax of the number of parameters. Formally the representation of an inductive declaration @@ -657,7 +656,7 @@ $\Gamma_C$. 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 the number of parameters in +when $p$ is (less or equal than) the number of parameters in \NInd{\Gamma}{\Gamma_I}{\Gamma_C}. \paragraph{Examples} @@ -701,8 +700,6 @@ with forest : Set := % we described theoretically. The difference is that in the type of % constructors the inductive definition is explicitly applied to the % parameters variables. -%% FIXME: TODO: The paragraph below is wrong with the new inductive -%% types implemented by Christine. The indtype below IS accepted. The \Coq\ type-checker verifies that all parameters are applied in the correct manner in the conclusion of the type of each constructors~: @@ -1024,20 +1021,25 @@ 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}\] - -\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 @@ -1054,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 @@ -1242,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} @@ -1257,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@{}} @@ -1267,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} @@ -1326,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} \] @@ -1361,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 @@ -1372,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: @@ -1384,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) @@ -1501,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} -- cgit v1.2.3