diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/RecTutorial/coqartmacros.tex | 2 | ||||
| -rw-r--r-- | doc/common/macros.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 24 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 34 | ||||
| -rw-r--r-- | doc/refman/RefMan-tus.tex | 18 |
7 files changed, 61 insertions, 34 deletions
diff --git a/doc/RecTutorial/coqartmacros.tex b/doc/RecTutorial/coqartmacros.tex index 2a2c211963..72d7492690 100644 --- a/doc/RecTutorial/coqartmacros.tex +++ b/doc/RecTutorial/coqartmacros.tex @@ -149,7 +149,7 @@ \newcommand{\PicAbst}[3]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2}\chunk{#3}% \end{bundle}} -% the same in DeBruijn form +% the same in de Bruijn form \newcommand{\PicDbj}[2]{\begin{bundle}{\bf abst}\chunk{#1}\chunk{#2} \end{bundle}} diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 5abdecfc18..0a4251a373 100644 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -145,7 +145,7 @@ \newcommand{\typecstr}{\zeroone{{\tt :}~{\term}}} \newcommand{\typecstrwithoutblank}{\zeroone{{\tt :}{\term}}} - +\newcommand{\typecstrtype}{\zeroone{{\tt :}~{\type}}} \newcommand{\Fwterm}{\nterm{Fwterm}} \newcommand{\Index}{\nterm{index}} @@ -164,6 +164,7 @@ \newcommand{\digit}{\nterm{digit}} \newcommand{\exteqn}{\nterm{ext\_eqn}} \newcommand{\field}{\nterm{field}} +\newcommand{\fielddef}{\nterm{field\_def}} \newcommand{\firstletter}{\nterm{first\_letter}} \newcommand{\fixpg}{\nterm{fix\_pgm}} \newcommand{\fixpointbodies}{\nterm{fix\_bodies}} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b9c17d8148..fdd2725810 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression -$0$) which corresponds, in the arity of sort-polymorphic inductive -types (see Section \ref{Sort-polymorphism-inductive}), +$0$) which corresponds, in the arity of template polymorphic inductive +types (see Section \ref{Template-polymorphism}), to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of @@ -977,8 +977,8 @@ Inductive exType (P:Type->Prop) : Type := %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[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}} -\label{Sort-polymorphism-inductive} +\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} +\label{Template-polymorphism} Inductive types declared in {\Type} are polymorphic over their arguments in {\Type}. @@ -1120,6 +1120,10 @@ 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 diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 74d64497aa..6dd0ddf81d 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -29,8 +29,8 @@ construction allows defining ``signatures''. {\recordkw} & ::= & {\tt Record} $|$ {\tt Inductive} $|$ {\tt CoInductive}\\ & & \\ -{\field} & ::= & {\name} \zeroone{\binders} : {\type} [ {\tt where} {\it notation} ] \\ - & $|$ & {\name} \zeroone{\binders} {\typecstr} := {\term} +{\field} & ::= & {\name} \zeroone{\binders} : {\type} \zeroone{{\tt where} {\it notation}} \\ + & $|$ & {\name} \zeroone{\binders} {\typecstrtype} := {\term}\\ \end{tabular} \end{centerframe} \caption{Syntax for the definition of {\tt Record}} @@ -213,7 +213,21 @@ Record point := { x : nat; y : nat }. Definition a := Build_point 5 3. \end{coq_example} -The following syntax allows creating objects by using named fields. The +\begin{figure}[t] +\begin{centerframe} +\begin{tabular}{lcl} +{\term} & ++= & + \verb!{|! \zeroone{\nelist{\fielddef}{;}} \verb!|}! \\ + & & \\ +{\fielddef} & ::= & {\name} \zeroone{\binders} := {\term} \\ +\end{tabular} +\end{centerframe} +\caption{Syntax for constructing elements of a \texttt{Record} using named fields} +\label{fig:fieldsyntax} +\end{figure} + +A syntax is available for creating objects by using named fields, as +shown on Figure~\ref{fig:fieldsyntax}. The fields do not have to be in any particular order, nor do they have to be all present if the missing ones can be inferred or prompted for (see Section~\ref{Program}). @@ -252,7 +266,7 @@ Eval compute in ( Reset Initial. \end{coq_eval} -\Rem An experimental syntax for projections based on a dot notation is +\Rem A syntax for projections based on a dot notation is available. The command to activate it is \optindex{Printing Projections} \begin{quote} @@ -267,7 +281,7 @@ available. The command to activate it is & $|$ & {\term} {\tt .(} {@}{\qualid} \nelist{\term}{} {\tt )} \end{tabular} \end{centerframe} -\caption{Syntax of \texttt{Record} projections} +\caption{Syntax for \texttt{Record} projections} \label{fig:projsyntax} \end{figure} diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index f36969e821..0441f952df 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -529,7 +529,7 @@ intensive computations. Christine Paulin implemented an extension of inductive types allowing recursively non uniform parameters. Hugo Herbelin implemented -sort-polymorphism for inductive types. +sort-polymorphism for inductive types (now called template polymorphism). Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary compatible equivalence relations. He also generalized rewriting to diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 3f12411863..87b9e4914f 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1275,15 +1275,18 @@ in the list of subgoals remaining to prove. \item{\tt assert ( {\ident} := {\term} )} - This behaves as {\tt assert ({\ident} :\ {\type});[exact - {\term}|idtac]} where {\type} is the type of {\term}. This is - deprecated in favor of {\tt pose proof}. + This behaves as {\tt assert ({\ident} :\ {\type}) by exact {\term}} + where {\type} is the type of {\term}. This is deprecated in favor of + {\tt pose proof}. + + If the head of {\term} is {\ident}, the tactic behaves as + {\tt specialize \term}. \ErrMsg \errindex{Variable {\ident} is already declared} -\item \texttt{pose proof {\term} as {\intropattern}\tacindex{pose proof}} +\item \texttt{pose proof {\term} \zeroone{as {\intropattern}}\tacindex{pose proof}} - This tactic behaves like \texttt{assert T as {\intropattern} by + This tactic behaves like \texttt{assert T \zeroone{as {\intropattern}} by exact {\term}} where \texttt{T} is the type of {\term}. In particular, \texttt{pose proof {\term} as {\ident}} behaves as @@ -1326,8 +1329,8 @@ in the list of subgoals remaining to prove. following subgoals: {\tt U -> T} and \texttt{U}. The subgoal {\tt U -> T} comes first in the list of remaining subgoal to prove. -\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize}} \\ - {\tt specialize {\ident} with \bindinglist} +\item {\tt specialize ({\ident} \term$_1$ \dots\ \term$_n$)\tacindex{specialize} \zeroone{as \intropattern}}\\ + {\tt specialize {\ident} with {\bindinglist} \zeroone{as \intropattern}} The tactic {\tt specialize} works on local hypothesis \ident. The premises of this hypothesis (either universal @@ -1338,14 +1341,19 @@ in the list of subgoals remaining to prove. second form, all instantiation elements must be given, whereas in the first form the application to \term$_1$ {\ldots} \term$_n$ can be partial. The first form is equivalent to - {\tt assert (\ident' := {\ident} {\term$_1$} \dots\ \term$_n$); - clear \ident; rename \ident' into \ident}. + {\tt assert ({\ident} := {\ident} {\term$_1$} \dots\ \term$_n$)}. + + With the {\tt as} clause, the local hypothesis {\ident} is left + unchanged and instead, the modified hypothesis is introduced as + specified by the {\intropattern}. The name {\ident} can also refer to a global lemma or hypothesis. In this case, for compatibility reasons, the behavior of {\tt specialize} is close to that of {\tt generalize}: the instantiated statement becomes an additional - premise of the goal. + premise of the goal. The {\tt as} clause is especially useful + in this case to immediately introduce the instantiated statement + as a local hypothesis. \begin{ErrMsgs} \item \errindexbis{{\ident} is used in hypothesis \ident'}{is used in hypothesis} @@ -2618,9 +2626,9 @@ as the ones described in Section~\ref{Tac-induction}. In the syntax of the tactic, the identifier {\ident} is the name given to the induction hypothesis. The natural number {\num} tells on which premise of the current goal the induction acts, starting -from 1 and counting both dependent and non dependent -products. Especially, the current lemma must be composed of at least -{\num} products. +from 1, counting both dependent and non dependent +products, but skipping local definitions. Especially, the current +lemma must be composed of at least {\num} products. Like in a {\tt fix} expression, the induction hypotheses have to be used on structurally smaller arguments. diff --git a/doc/refman/RefMan-tus.tex b/doc/refman/RefMan-tus.tex index 797b0adedd..017de6d484 100644 --- a/doc/refman/RefMan-tus.tex +++ b/doc/refman/RefMan-tus.tex @@ -288,8 +288,8 @@ constructors: \item $(\texttt{VAR}\;id)$, a reference to a global identifier called $id$; \item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$ binder up in the term; -\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$; -\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of +\item $\texttt{DLAM}\;(x,t)$, a de Bruijn's binder on the term $t$; +\item $\texttt{DLAMV}\;(x,vt)$, a de Bruijn's binder on all the terms of the vector $vt$; \item $(\texttt{DOP0}\;op)$, a unary operator $op$; \item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary @@ -299,7 +299,7 @@ vector of terms $vt$. \end{itemize} In this meta-language, bound variables are represented using the -so-called deBrujin's indexes. In this representation, an occurrence of +so-called de Bruijn's indexes. In this representation, an occurrence of a bound variable is denoted by an integer, meaning the number of binders that must be traversed to reach its own binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders @@ -339,7 +339,7 @@ on the terms of the meta-language: \fun{val Generic.dependent : 'op term -> 'op term -> bool} {Returns true if the first term is a sub-term of the second.} %\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term} -% { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index +% { $(\texttt{subst\_var}\;id\;t)$ substitutes the de Bruijn's index % associated to $id$ to every occurrence of the term % $(\texttt{VAR}\;id)$ in $t$.} \end{description} @@ -482,7 +482,7 @@ following constructor functions: \begin{description} \fun{val Term.mkRel : int -> constr} - {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.} + {$(\texttt{mkRel}\;n)$ represents de Bruijn's index $n$.} \fun{val Term.mkVar : identifier -> constr} {$(\texttt{mkVar}\;id)$ @@ -545,7 +545,7 @@ following constructor functions: \fun{val Term.mkProd : name ->constr ->constr -> constr} {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$. - The free ocurrences of $x$ in $B$ are represented by deBrujin's + The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr} @@ -553,14 +553,14 @@ following constructor functions: but the bound occurrences of $x$ in $B$ are denoted by the identifier $(\texttt{mkVar}\;x)$. The function automatically changes each occurrences of this identifier into the corresponding - deBrujin's index.} + de Bruijn's index.} \fun{val Term.mkArrow : constr -> constr -> constr} {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.} \fun{val Term.mkLambda : name -> constr -> constr -> constr} {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction - $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's + $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by de Bruijn's indexes.} \fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr} @@ -666,7 +666,7 @@ use the primitive \textsl{Case} described in Chapter \ref{Cic} \item Restoring type coercions and synthesizing the implicit arguments (the one denoted by question marks in {\Coq} syntax: see Section~\ref{Coercions}). -\item Transforming the named bound variables into deBrujin's indexes. +\item Transforming the named bound variables into de Bruijn's indexes. \item Classifying the global names into the different classes of constants (defined constants, constructors, inductive types, etc). \end{enumerate} |