diff options
author | 2003-12-14 23:50:31 +0000 | |
---|---|---|
committer | 2003-12-14 23:50:31 +0000 | |
commit | a73344798c51422a6f00507c42b0c07b37f3fb7e (patch) | |
tree | 177b65a0a7bbab99b764cd46d2c21c12bff66b76 | |
parent | c300b326fa29e2c3a9a530d494a06d555733d335 (diff) |
debut de mise a jour CIC
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8396 85f007b7-540e-0410-9357-904b9bb8a0f7
-rwxr-xr-x | doc/RefMan-cic.tex | 226 | ||||
-rw-r--r-- | doc/RefMan-ide.tex | 2 | ||||
-rwxr-xr-x | doc/RefMan-pre.tex | 7 | ||||
-rwxr-xr-x | doc/macros.tex | 3 |
4 files changed, 130 insertions, 108 deletions
diff --git a/doc/RefMan-cic.tex b/doc/RefMan-cic.tex index a1633a80a..27c01d4d6 100755 --- a/doc/RefMan-cic.tex +++ b/doc/RefMan-cic.tex @@ -7,6 +7,8 @@ The underlying formal language of {\Coq} is the {\em Calculus of (Co)Inductive Constructions}\index{Calculus of (Co)Inductive Constructions} (\CIC\ in short). It is presented in this chapter. +% Changement de la predicativite de Set + In \CIC\, all objects 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. @@ -25,17 +27,17 @@ says {\em convertible}). Convertibility is presented in section The remaining sections are concerned with the type-checking of terms. The beginner can skip them. -The reader seeking a background on the {\CIC} may read several -papers. Giménez~\cite{Gim98} -provides an introduction to inductive and coinductive -definitions in Coq, Werner~\cite{Wer94} and Paulin-Mohring~\cite{Moh97} are the -most recent theses on the +The reader seeking a background on the {\CIC} may read several papers. +Giménez~\cite{Gim98} provides an introduction to inductive and +coinductive definitions in Coq. In their book~\cite{CoqArt}, Bertot +and Castéran give a precise description of the \CIC{} based on +numerous practical examples. Barras~\cite{Bar99}, Werner~\cite{Wer94} +and Paulin-Mohring~\cite{Moh97} are the most recent theses on the {\CIC}. Coquand-Huet~\cite{CoHu85a,CoHu85b,CoHu86} introduces the Calculus of Constructions. Coquand-Paulin~\cite{CoPa89} introduces inductive definitions. The {\CIC} is a formulation of type theory -including the possibility of inductive -constructions. Barendregt~\cite{Bar91} studies the modern form of type -theory. +including the possibility of inductive constructions. +Barendregt~\cite{Bar91} studies the modern form of type theory. \section{The terms}\label{Terms} @@ -52,11 +54,12 @@ type of natural numbers. Then $\ra$ is used both to denote $\nat\ra\nat$ which is the type of functions from \nat\ to \nat, and to denote $\nat \ra \Prop$ which is the type of unary predicates over the natural numbers. Consider abstraction which builds functions. It -serves to build ``ordinary'' functions as $[x:\nat]({\tt mult} ~x~x)$ (assuming {\tt mult} is already defined) but may build also -predicates over the natural numbers. For instance $[x:\nat](x=x)$ will +serves to build ``ordinary'' functions as $\kw{fun}~x:\nat \Ra ({\tt mult} ~x~x)$ (assuming {\tt mult} is already defined) but may build also +predicates over the natural numbers. For instance $\kw{fun}~x:\nat \Ra +(x=x)$ will represent a predicate $P$, informally written in mathematics $P(x)\equiv x=x$. If $P$ has type $\nat \ra \Prop$, $(P~x)$ is a -proposition, furthermore $(x:\nat)(P~x)$ will represent the type of +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 proofs of the formula ``$\forall x.P(x)$''. @@ -64,7 +67,7 @@ type $(P~n)$ and consequently represent proofs of the formula \subsection{Sorts}\label{Sorts} \index{Sorts} Types are seen as terms of the language and then should belong to -another type. The type of a type is a always a constant of the language +another type. The type of a type is always a constant of the language called a {\em sort}. The two basic sorts in the language of \CIC\ are \Set\ and \Prop. @@ -145,20 +148,22 @@ More precisely the language of the {\em Calculus of Inductive \item the sorts {\sf Set, Prop, Type} are terms. \item names for global constant of the environment are terms. \item variables are terms. -\item if $x$ is a variable and $T$, $U$ are terms then $(x:T)U$ is a - term. If $x$ occurs in $U$, $(x:T)U$ reads as {\it ``for all x of - type T, U''}. As $U$ depends on $x$, one says that $(x:T)U$ is a - {\em dependent product}. If $x$ doesn't occurs in $U$ then $(x:T)U$ +\item if $x$ is a variable and $T$, $U$ are terms then $\kw{forall}~x:T,U$ is a + term. If $x$ occurs in $U$, $\kw{forall}~x:T,U$ reads as {\it ``for all x of + type T, U''}. As $U$ depends on $x$, one says that $\kw{forall}~x:T,U$ is a + {\em dependent product}. If $x$ doesn't occurs in $U$ then + $\kw{forall}~x:T,U$ reads as {\it ``if T then U''}. A non dependent product can be written: $T \rightarrow U$. -\item if $x$ is a variable and $T$, $U$ are terms then $[x:T]U$ is a - term. This is a notation for the $\lambda$-abstraction of - $\lambda$-calculus\index{lambda-calculus@$\lambda$-calculus} - \cite{Bar81}. The term $[x:T]U$ is a function which maps elements of - $T$ to $U$. +\item if $x$ is a variable and $T$, $U$ are terms then $\kw{fun}~x:T + \Ra U$ is a term. This is a notation for the $\lambda$-abstraction + of $\lambda$-calculus\index{lambda-calculus@$\lambda$-calculus} + \cite{Bar81}. The term $\kw{fun}~x:T \Ra U$ is a function which maps + elements of $T$ to $U$. \item if $T$ and $U$ are terms then $(T\ U)$ is a term. The term $(T\ U)$ reads as {\it ``T applied to U''}. -\item if $x$ is a variable, and $T$, $U$ are terms then $[x:=T]U$ is a +\item if $x$ is a variable, and $T$, $U$ are terms then + $\kw{let}~x:=T~\kw{in}~U$ is a term which denotes the term $U$ where the variable $x$ is locally bound to $T$. This stands for the common ``let-in'' construction of functional programs such as ML or Scheme. @@ -166,17 +171,18 @@ More precisely the language of the {\em Calculus of Inductive \paragraph{Notations.} Application associates to the left such that $(t~t_1\ldots t_n)$ represents $(\ldots (t~t_1)\ldots t_n)$. The -products and arrows associate to the right such that $(x:A)B\ra C\ra -D$ represents $(x:A)(B\ra (C\ra D))$. One uses sometimes $(x,y:A)B$ or -$[x,y:A]B$ to denote the abstraction or product of several variables -of the same type. The equivalent formulation is $(x:A)(y:A)B$ or -$[x:A][y:A]B$ +products and arrows associate to the right such that $\kw{forall}~x:A,B\ra C\ra +D$ represents $\kw{forall}~x:A,(B\ra (C\ra D))$. One uses sometimes +$\kw{forall}~x~y:A,B$ or +$\kw{fun}~x~y:A\Ra B$ to denote the abstraction or product of several variables +of the same type. The equivalent formulation is $\kw{forall}~(x:A)(y:A),B$ or +$\kw{fun}~(x:A)(y:A) \Ra B$ \paragraph{Free variables.} The notion of free variables is defined as usual. In the expressions -$[x:T]U$ and $(x:T)U$ the occurrences of $x$ in $U$ are bound. They -are represented by de Bruijn indexes in the internal structure of -terms. +$\kw{fun}~x:T\Ra U$ and $\forall x:T, U$ the occurrences of $x$ in $U$ +are bound. They are represented by de Bruijn indexes in the internal +structure of terms. \paragraph{Substitution.} \index{Substitution} The notion of substituting a term $t$ to free occurrences of a @@ -207,11 +213,14 @@ $\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... -% -% We define the inclusion of two 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 +% Si dans l'explication WF(E)[Gamma] concernant les constantes +% definies ds un contexte + +We define the inclusion of two 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$. @@ -283,26 +292,29 @@ be derived from the following rules. \inference{\frac{\WFE{\Gamma}~~~~(c:T) \in E}{\WTEG{c}{T}}} \item [Prod] \index{Typing rules!Prod} \inference{\frac{\WTEG{T}{s_1}~~~~ - \WTE{\Gamma::(x:T)}{U}{s_2}~~~s_1\in\{\Prop, \Set\}~\mbox{or}~ - s_2\in\{\Prop, \Set\}} - { \WTEG{(x:T)U}{s_2}}} + \WTE{\Gamma::(x:T)}{U}{\Prop}} + { \WTEG{\kw{forall}~x:T,U}{\Prop}}} +\inference{\frac{\WTEG{T}{s_1}~~~~ + \WTE{\Gamma::(x:T)}{U}{\Set}~~~s_1\in\{\Prop, \Set\}} + { \WTEG{\kw{forall}~x:T,U}{\Set}}} \inference{\frac{\WTEG{T}{\Type(i)}~~~~ \WTE{\Gamma::(x:T)}{U}{\Type(j)}~~~i\leq - k~~~j \leq k}{ \WTEG{(x:T)U}{\Type(k)}}} + k~~~j \leq k}{ \WTEG{\kw{forall}~x:T,U}{\Type(k)}}} \item [Lam]\index{Typing rules!Lam} -\inference{\frac{\WTEG{(x:T)U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}} - {\WTEG{[x:T]t}{(x:T)U}}} +\inference{\frac{\WTEG{\kw{forall}~x:T,U}{s}~~~~ \WTE{\Gamma::(x:T)}{t}{U}} + {\WTEG{\kw{fun}~x:T\Ra t}{(x:T)U}}} \item [App]\index{Typing rules!App} - \inference{\frac{\WTEG{t}{(x:U)T}~~~~\WTEG{u}{U}} + \inference{\frac{\WTEG{t}{\kw{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{[x:=t]u}{\subst{U}{x}{t}}}} + {\WTEG{\kw{let}~x:=t~\kw{in}~u}{\subst{U}{x}{t}}}} \end{itemize} -\noindent {\bf Remark. } We may have $[x:=t]u$ well-typed without -having $([x:T]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}). +\noindent {\bf Remark. } We may have $\kw{let}~x:=t~\kw{in}~u$ +well-typed without having $(\kw{fun}~x:T\Ra 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} \index{Conversion rules} @@ -313,14 +325,14 @@ the value $t$ associated to $x$ may be used in a conversion rule (see section \r 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 -$[x:T]x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the -application $([x:T]x~a)$. We define for this a {\em reduction} (or a +$\kw{fun}~x:T\Ra x$. In any environment $E$ and context $\Gamma$, we want to identify any object $a$ (of type $T$) with the +application $(\kw{fun}~x:T\Ra x)~a$. We define for this a {\em reduction} (or a {\em conversion}) rule we call $\beta$: -\[ \WTEGRED{([x:T]t~u)}{\triangleright_{\beta}}{\subst{t}{x}{u}} \] - +\[ \WTEGRED{((\kw{fun}~x:T\Ra + t)~u)}{\triangleright_{\beta}}{\subst{t}{x}{u}} \] We say that $\subst{t}{x}{u}$ is the {\em $\beta$-contraction} of -$([x:T]t~u)$ and, conversely, that $([x:T]t~u)$ is the {\em - $\beta$-expansion} of $\subst{t}{x}{u}$. +$(\kw{fun}~x:T\Ra t)~u$ and, conversely, that $(\kw{fun}~x:T\Ra 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 @@ -357,7 +369,7 @@ 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{[x:=u]t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ +$$\WTEGRED{\kw{let}~x:=u~\kw{in}~t}{\triangleright_{\zeta}}{\subst{t}{x}{u}}$$ \paragraph{Convertibility.} \label{convertibility} @@ -384,7 +396,7 @@ convertibility into an order inductively defined by: \item if $i \leq j$ then $\WTEGLECONV{\Type(i)}{\Type(j)}$, \item for any $i$, $\WTEGLECONV{\Prop}{\Type(i)}$, \item for any $i$, $\WTEGLECONV{\Set}{\Type(i)}$, -\item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{(x:T)T'}{(x:U)U'}$. +\item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\kw{forall}~x:T,T'}{\kw{forall}~x:U,U'}$. \end{enumerate} The conversion rule is now exactly: @@ -401,10 +413,10 @@ An other important rule is the $\eta$-conversion. It is to identify terms over a dummy abstraction of a variable followed by an application of this variable. Let $T$ be a type, $t$ be a term in which the variable $x$ doesn't occurs free. We have -\[ \WTEGRED{[x:T](t\ x)}{\triangleright}{t} \] +\[ \WTEGRED{\kw{fun}~x:T\Ra (t\ x)}{\triangleright}{t} \] Indeed, as $x$ doesn't occur free in $t$, for any $u$ one -applies to $[x:T](t\ x)$, it $\beta$-reduces to $(t\ u)$. So -$[x:T](t\ x)$ and $t$ can be identified. +applies to $\kw{fun}~x:T\Ra (t\ x)$, it $\beta$-reduces to $(t\ u)$. So +$\kw{fun}~x:T\Ra (t\ x)$ and $t$ can be identified. \Rem The $\eta$-reduction is not taken into account in the convertibility rule of \Coq. @@ -414,16 +426,19 @@ 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 rule. 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 $[x_1:T_1]\ldots[x_k:T_k](t_0\ t_1\ldots t_n)$ where +be written as $\kw{fun}~(x_1:T_1)\ldots (x_k:T_k) \Ra +(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 $[x:T]u_0$ then one step of + of $t$}. If we assume that $t_0$ is $\kw{fun}~x:T\Ra u_0$ then one step of $\beta$-head reduction of $t$ is: -\[[x_1:T_1]\ldots[x_k:T_k]([x:T]u_0\ t_1\ldots t_n) -~\triangleright ~ [x_1:T_1]\ldots[x_k:T_k](\subst{u_0}{x}{t_1}\ t_2 \ldots t_n)\] +\[\kw{fun}~(x_1:T_1)\ldots(x_k:T_k)\Ra (\kw{fun}~x:T\Ra u_0\ t_1\ldots t_n) +~\triangleright ~ \kw{fun}~(x_1:T_1)\ldots(x_k:T_k)\Ra +(\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 [x_1:T_1]\ldots[x_k:T_k](v\ u_1 +\[ t \triangleright \ldots \triangleright +\kw{fun}~(x_1:T_1)\ldots(x_k:T_k)\Ra (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 @@ -467,7 +482,7 @@ variable $x$ is available at each stage where $c$ is mentioned. \paragraph{Abstracting property:} \inference{\frac{\WF{E; \Def{\Gamma::(x:U)}{c}{t}{T}; F}{\Delta}~~~~\WFE{\Gamma}} - {\WF{E;\Def{\Gamma}{c}{[x:U]t}{(x:U)T}; + {\WF{E;\Def{\Gamma}{c}{\kw{fun}~x:U\Ra t}{\kw{forall}~x:U,T}; \subst{F}{c}{(c~x)}}{\subst{\Delta}{c}{(c~x)}}}} \paragraph{Pruning the context.} @@ -643,18 +658,18 @@ contains an inductive declaration. $[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:(p_1:P_1)\ldots(p_r:P_r)A_j) \in E}} + ~~j=1\ldots k}{(I_j:\kw{forall}~(p_1:P_1)\ldots(p_r:P_r),A_j) \in E}} \inference{\frac{\Ind{\Gamma}{\Gamma_P}{\Gamma_I}{\Gamma_C} \in E ~~~~i=1.. n} - {(c_i:(p_1:P_1)\ldots(p_r:P_r)\subst{C_i}{I_j}{(I_j~p_1\ldots + {(c_i:\kw{forall}~(p_1:P_1)\ldots(p_r:P_r),\subst{C_i}{I_j}{(I_j~p_1\ldots p_r)}_{j=1\ldots k})\in E}} \end{description} \paragraph{Example.} -We have $(\List:\Set \ra \Set), (\cons:(A:\Set)A\ra(\List~A)\ra +We have $(\List:\Set \ra \Set), (\cons:\kw{forall}~A:\Set,A\ra(\List~A)\ra (\List~A))$, \\ -$(\Length:(A:\Set)(\List~A)\ra\nat\ra\Prop)$, $\tree:\Set$ and $\forest:\Set$. +$(\Length:\kw{forall}~A:\Set, (\List~A)\ra\nat\ra\Prop)$, $\tree:\Set$ and $\forest:\Set$. From now on, we write $\ListA$ instead of $(\List~A)$ and $\LengthA$ for $(\Length~A)$. @@ -681,14 +696,13 @@ rules, we need a few definitions: \paragraph{Definitions}\index{Positivity}\label{Positivity} -A type $T$ is an {\em arity of sort $s$}\index{Arity} -if it converts to the sort $s$ or to a -product $(x:T)U$ with $U$ an arity of sort $s$. (For instance $A\ra -\Set$ or $(A:\Prop)A\ra \Prop$ are arities of sort respectively \Set\ -and \Prop). -A {\em type of constructor of $I$}\index{Type of constructor} - is either a term $(I~t_1\ldots ~t_n)$ or -$(x:T)C$ with $C$ a {\em type of constructor of $I$}. +A type $T$ is an {\em arity of sort $s$}\index{Arity} if it converts +to the sort $s$ or to a product $\kw{forall}~x:T,U$ with $U$ an arity +of sort $s$. (For instance $A\ra \Set$ or $\kw{forall}~A:\Prop,A\ra +\Prop$ are arities of sort respectively \Set\ and \Prop). A {\em type + of constructor of $I$}\index{Type of constructor} is either a term +$(I~t_1\ldots ~t_n)$ or $(x:T)C$ with $C$ a {\em type of constructor + of $I$}. \smallskip @@ -698,7 +712,7 @@ 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=(x:T)U$ and $X$ occurs only strictly positively in $T$ and +\item $T=\kw{forall}~x:T,U$ and $X$ occurs only strictly positively in $T$ and the type $U$ satisfies the positivity condition for $X$ \end{itemize} @@ -707,15 +721,17 @@ 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 $(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}{[p_1:P_1;\ldots;p_m:P_m]}{[I:A]}{[c_1:C_1;\ldots;c_n: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 the imbricated positivity condition for $X$ +\item $T$ converts to $(X~t_1 \ldots ~t_n)$ and $X$ does not occur in + any of $t_i$ +\item $T$ converts to $\kw{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}{[p_1:P_1;\ldots;p_m:P_m]}{[I:A]}{[c_1:C_1;\ldots;c_n: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 + the imbricated 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$ @@ -728,7 +744,7 @@ cases: \begin{itemize} \item $T=(I~t_1\ldots ~t_n)$ and $X$ does not occur in any $t_i$ -\item $T=(x:T)U$ and $X$ occurs only strictly positively in $T$ and +\item $T=\kw{forall}~x:T,U$ and $X$ occurs only strictly positively in $T$ and the type $U$ satisfies the imbricated positivity condition for $X$ \end{itemize} @@ -736,9 +752,9 @@ the type $U$ satisfies the imbricated positivity condition for $X$ $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$ assuming the notion of product and lists were already defined. Assuming $X$ has arity ${\tt -nat \ra Prop}$ and {\tt ex} is inductively defined existential -quantifier, the occurrence of $X$ in ${\tt (ex~ nat~ [n:nat](X~ n))}$ is -also strictly positive. + nat \ra Prop}$ and {\tt ex} is the inductively defined existential +quantifier, the occurrence of $X$ in ${\tt (ex~ nat~ \kw{fun}~n:nat\ra + (X~ n))}$ is also strictly positive. \paragraph{Correctness rules.} We shall now describe the rules allowing the introduction of a new @@ -844,9 +860,9 @@ into two more primitive operations as was first suggested by Th. Coquand in~\cite{Coq92}. One is the definition by case analysis. The second one is a definition by guarded fixpoints. -\subsubsection{The {\tt Cases\ldots of \ldots end} construction.} +\subsubsection{The {\tt match\ldots with \ldots end} construction.} \label{Caseexpr} -\index{Cases@{\tt Cases\ldots of\ldots end}} +\index{match@{\tt match\ldots with\ldots end}} The basic idea of this destructor operation is that we have an object $m$ in an inductive type $I$ and we want to prove a property $(P~m)$ @@ -854,8 +870,8 @@ which in general 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$. This proof will be denoted by a generic term: -\[\Case{P}{m}{(c_1~x_{11}~...~x_{1p_1}) \mbox{\tt =>} f_1 ~|~\ldots~|~ - (c_n~x_{n1}...x_{np_n}) \mbox{\tt =>} f_n }\] In this expression, if +\[\Case{P~x}{m~\kw{as}~x}{(c_1~x_{11}~...~x_{1p_1}) \Ra f_1 ~|~\ldots~|~ + (c_n~x_{n1}...x_{np_n}) \Ra f_n }\] In this expression, if $m$ is a term built from a constructor $(c_i~u_1\ldots u_{p_i})$ then the expression will behave as it is specified with $i$-th branch and will reduce to $f_i$ where the $x_{i1}$\ldots $x_{ip_i}$ are replaced @@ -877,17 +893,19 @@ For instance, a function testing whether a list is empty can be defined as: -\[[l:\ListA]\Case{[H:\ListA]\bool}{l}{\Nil~ \mbox{\tt =>}~\true~ |~ (\cons~a~m)~ \mbox{\tt =>}~\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} +\[\kw{fun}~l:\ListA \Ra\Case{\bool}{l}{\Nil~ \Ra~\true~ |~ (\cons~a~m)~ \Ra~\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.} \index{Elimination sorts} -An important question for building the typing rule for {\tt Case} is +An important question for building the typing rule for \kw{match} is what can be the type of $P$ with respect to the type of the inductive definitions. @@ -908,7 +926,7 @@ 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 $(x:T)C$ is a +$(I~t_1\ldots t_s)$ is a {\em small type of constructor} and $\kw{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} @@ -993,7 +1011,7 @@ branch corresponding to the $c:C$ constructor. \[ \begin{array}{ll} \CI{c:(I_i~p_1\ldots p_r\ t_1 \ldots t_p)}{P} &\equiv (P~t_1\ldots ~t_p~c) \\[2mm] -\CI{c:(x: T)C}{P} &\equiv (x:T)\CI{(c~x):C}{P} +\CI{c:\kw{forall}~x:T,C}{P} &\equiv \kw{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$. @@ -1027,7 +1045,7 @@ for \] \begin{description} -\item[Cases] \label{elimdep} \index{Typing rules!Cases} +\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} @@ -1221,7 +1239,7 @@ The following is not a conversion but can be proved after a case analysis. Goal forall t:tree, sizet t = S (sizef (sont t)). (** this one fails **)reflexivity. -olddestruct t. +destruct t. reflexivity. \end{coq_example} \begin{coq_eval} diff --git a/doc/RefMan-ide.tex b/doc/RefMan-ide.tex index c38388c54..aa80bcb5a 100644 --- a/doc/RefMan-ide.tex +++ b/doc/RefMan-ide.tex @@ -1,5 +1,5 @@ \chapter{\Coq{} Integrated Development Environment} -%\label{Addoc-coqide} +\label{Addoc-coqide} \ttindex{coqide} The \Coq{} Integrated Development Environment is a graphical tool, to diff --git a/doc/RefMan-pre.tex b/doc/RefMan-pre.tex index 73f6eb5b7..15dd54be2 100755 --- a/doc/RefMan-pre.tex +++ b/doc/RefMan-pre.tex @@ -493,6 +493,9 @@ tactics. Benjamin Monate is the developer of the \CoqIde{} graphical interface with contributions by Claude Marché. +Claude Marché coordinated the update of the Reference Manual for + \Coq{} V8.0. + Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the extraction tool and module system of {\Coq}. @@ -500,7 +503,7 @@ Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and contributors from Sophia-Antipolis and Nijmegen participated to the extension of the library. -Hugo Herbelin and Christine Paulin coordinated the developement which +Hugo Herbelin and Christine Paulin coordinated the development which was under the responsability of Christine Paulin. \begin{flushright} @@ -509,7 +512,7 @@ Hugo Herbelin \& Christine Paulin \end{flushright} -\newpage +%\newpage % Integration of ZArith lemmas from Sophia and Nijmegen. diff --git a/doc/macros.tex b/doc/macros.tex index 4ee407abb..69488bfb3 100755 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -320,7 +320,8 @@ \newcommand{\Def}[4]{\mbox{{\sf Def}$(#1)(#2:=#3:#4)$}} \newcommand{\Assum}[3]{\mbox{{\sf Assum}$(#1)(#2:#3)$}} \newcommand{\Match}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Match}}~#2~{\mbox{\tt with}}~#3~{\mbox{\tt end}}$}} -\newcommand{\Case}[3]{\mbox{$<\!#1\!>\!{\mbox{\tt Cases}}~#2~{\mbox{\tt of}}~#3~{\mbox{\tt end}}$}} +\newcommand{\Case}[3]{\mbox{$\kw{match}~#2~\kw{return}~#1~\kw{with}~#3~ +\kw{end}$}} \newcommand{\Fix}[2]{\mbox{\tt Fix}~#1\{#2\}} \newcommand{\CoFix}[2]{\mbox{\tt CoFix}~#1\{#2\}} \newcommand{\With}[2]{\mbox{\tt ~with~}} |