diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Classes.tex | 8 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 24 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 282 | ||||
| -rw-r--r-- | doc/refman/RefMan-gal.tex | 2 | ||||
| -rw-r--r-- | doc/refman/RefMan-ind.tex | 510 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 7 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 98 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 151 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 204 | ||||
| -rw-r--r-- | doc/refman/Universes.tex | 46 |
12 files changed, 618 insertions, 735 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index acfc4bea93..7e07868a38 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -486,15 +486,17 @@ where there is a hole in that place. \subsection{\tt Set Typeclasses Legacy Resolution} \optindex{Typeclasses Legacy Resolution} +\emph{Deprecated since 8.7} This option (off by default) uses the 8.5 implementation of resolution. Use for compatibility purposes only (porting and debugging). \subsection{\tt Set Typeclasses Module Eta} \optindex{Typeclasses Modulo Eta} +\emph{Deprecated since 8.7} This option allows eta-conversion for functions and records during -unification of type-classes. This option is now unsupported in 8.6 with +unification of type-classes. This option is unsupported since 8.6 with {\tt Typeclasses Filtered Unification} set, but still affects the default unification strategy, and the one used in {\tt Legacy Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses @@ -505,7 +507,7 @@ pattern-matching is not up-to eta. \subsection{\tt Set Typeclasses Limit Intros} \optindex{Typeclasses Limit Intros} -This option (on by default in Coq 8.6 and below) controls the ability to +This option (on by default) controls the ability to apply hints while avoiding (functional) eta-expansions in the generated proof term. It does so by allowing hints that conclude in a product to apply to a goal with a matching product directly, avoiding an @@ -554,7 +556,7 @@ more efficient resolution behavior (the option is off by default). When a solution to the typeclass goal of this class is found, we never backtrack on it, assuming that it is canonical. -\subsection{\tt Typeclasses eauto := [debug] [dfs | bfs] [\emph{depth}]} +\subsection{\tt Typeclasses eauto := [debug] [(dfs) | (bfs)] [\emph{depth}]} \comindex{Typeclasses eauto} \label{TypeclassesEauto} diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex index 2fc1c8764a..f60908da6c 100644 --- a/doc/refman/Program.tex +++ b/doc/refman/Program.tex @@ -278,7 +278,8 @@ tactic is replaced by the default one if not specified. as implicit arguments of the special constant \texttt{Program.Tactics.obligation}. \item {\tt Set Shrink Obligations}\optindex{Shrink Obligations} - Control whether obligations should have their +\emph{Deprecated since 8.7} + This option (on by default) controls whether obligations should have their context minimized to the set of variables used in the proof of the obligation, to avoid unnecessary dependencies. \end{itemize} diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index fdd2725810..96fb1eb752 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -461,6 +461,13 @@ recursively convertible to $u'_1$, or, symmetrically, $u_2$ is $\lb x:T\mto u'_2$ and $u_1\,x$ is recursively convertible to $u'_2$. We then write $\WTEGCONV{t_1}{t_2}$. +Apart from this we consider two instances of polymorphic and cumulative (see Chapter~\ref{Universes-full}) inductive types (see below) +convertible $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ if we have subtypings (see below) in both directions, i.e., +$\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ and $\WTEGLECONV{t\ w_1' \dots w_m'}{t\ w_1 \dots w_m}$. +Furthermore, we consider $\WTEGCONV{c\ v_1 \dots v_m}{c'\ v_1' \dots v_m'}$ convertible if $\WTEGCONV{v_i}{v_i'}$ +and we have that $c$ and $c'$ are the same constructors of different instances the same inductive types (differing only in universe levels) +such that $\WTEG{c\ v_1 \dots v_m}{t\ w_1 \dots w_m}$ and $\WTEG{c'\ v_1' \dots v_m'}{t'\ w_1' \dots w_m'}$ and we have $\WTEGCONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$. + The convertibility relation allows introducing a new typing rule which says that two convertible well-formed types have the same inhabitants. @@ -480,6 +487,17 @@ convertibility into a {\em subtyping} relation inductively defined by: \item $\WTEGLECONV{\Prop}{\Set}$, hence, by transitivity, $\WTEGLECONV{\Prop}{\Type(i)}$, for any $i$ \item if $\WTEGCONV{T}{U}$ and $\WTELECONV{\Gamma::(x:T)}{T'}{U'}$ then $\WTEGLECONV{\forall~x:T, T'}{\forall~x:U, U'}$. +\item if $\Ind{}{p}{\Gamma_I}{\Gamma_C}$ is a universe polymorphic and cumulative (see Chapter~\ref{Universes-full}) + inductive type (see below) and $(t : \forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort)\in\Gamma_I$ + and $(t' : \forall\Gamma_P',\forall\Gamma_{\mathit{Arr}(t)}', \Sort')\in\Gamma_I$ + are two different instances of \emph{the same} inductive type (differing only in universe levels) with constructors + \[[c_1: \forall\Gamma_P,\forall T_{1,1} \dots T_{1,n_1},t\ v_{1,1} \dots v_{1,m}; \dots; c_k: \forall\Gamma_P,\forall T_{k, 1} \dots T_{k,n_k},t\ v_{n,1}\dots v_{n,m}]\] + and + \[[c_1: \forall\Gamma_P',\forall T_{1,1}' \dots T_{1,n_1}',t'\ v_{1,1}' \dots v_{1,m}'; \dots; c_k: \forall\Gamma_P',\forall T_{k, 1}' \dots T_{k,n_k}',t\ v_{n,1}'\dots v_{n,m}']\] + respectively then $\WTEGLECONV{t\ w_1 \dots w_m}{t\ w_1' \dots w_m'}$ (notice that $t$ and $t'$ are both fully applied, i.e., they have a sort as a type) + if $\WTEGCONV{w_i}{w_i'}$ for $1 \le i \le m$ and we have + \[ \WTEGLECONV{T_{i,j}}{T_{i,j}'} \text{ and } \WTEGLECONV{A_i}{A_i'}\] + where $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1; a_1 : A_l]$ and $\Gamma_{\mathit{Arr}(t)} = [a_1 : A_1'; a_1 : A_l']$. \end{enumerate} The conversion rule up to subtyping is now exactly: @@ -530,8 +548,12 @@ Formally, we can represent any {\em inductive definition\index{definition!induct These inductive definitions, together with global assumptions and global definitions, then form the global environment. % Additionally, for any $p$ there always exists $\Gamma_P=[a_1:A_1;\dots;a_p:A_p]$ -such that each $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: +such that each $T$ in $(t:T)\in\Gamma_I\cup\Gamma_C$ can be written as: $\forall\Gamma_P, T^\prime$ where $\Gamma_P$ is called the {\em context of parameters\index{context of parameters}}. +Furthermore, we must have that each $T$ in $(t:T)\in\Gamma_I$ can be written as: +$\forall\Gamma_P,\forall\Gamma_{\mathit{Arr}(t)}, \Sort$ where $\Gamma_{\mathit{Arr}(t)}$ is called the +{\em Arity} of the inductive type\index{arity of inductive type} $t$ and +$\Sort$ is called the sort of the inductive type $t$. \paragraph{Examples} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index 939fc87a6e..713f344cbe 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -38,21 +38,19 @@ construction allows defining ``signatures''. \end{figure} \noindent In the expression - -\smallskip -{\tt Record} {\ident} {\params} \texttt{:} - {\sort} := {\ident$_0$} \verb+{+ - {\ident$_1$} \binders$_1$ \texttt{:} {\term$_1$}; - \dots - {\ident$_n$} \binders$_n$ \texttt{:} {\term$_n$} \verb+}+. -\smallskip - +\begin{quote} +{\tt Record {\ident} {\params} : {\sort} := {\ident$_0$} \{ \\ + {\ident$_1$} \binders$_1$ : {\term$_1$} ; ... ; \\ + {\ident$_n$} \binders$_n$ : {\term$_n$} \}.} +\end{quote} \noindent the identifier {\ident} is the name of the defined record and {\sort} is its type. The identifier {\ident$_0$} is the name of its constructor. If {\ident$_0$} is omitted, the default name {\tt -Build\_{\ident}} is used. If {\sort} is omitted, the default sort is ``{\Type}''. -The identifiers {\ident$_1$}, .., -{\ident$_n$} are the names of fields and {\tt forall} \binders$_1${\tt ,} {\term$_1$}, ..., {\tt forall} \binders$_n${\tt ,} {\term$_n$} +Build\_{\ident}} is used. +If {\sort} is omitted, the default sort is {\Type}. +The identifiers {\ident$_1$}, \dots, {\ident$_n$} are the names of +fields and {\tt forall {\binders$_1$}, {\term$_1$}}, \dots, +{\tt forall {\binders$_n$}, {\term$_n$}} their respective types. Remark that the type of {\ident$_i$} may depend on the previous {\ident$_j$} (for $j<i$). Thus the order of the fields is important. Finally, {\params} are the parameters of the @@ -82,26 +80,15 @@ Record Rat : Set := mkRat forall x y z:nat, (x * y) = top /\ (x * z) = bottom -> x = 1}. \end{coq_example} -Remark here that the field -\verb+Rat_cond+ depends on the field \verb+bottom+. - -%Let us now see the work done by the {\tt Record} macro. -%First the macro generates an inductive definition -%with just one constructor: -% -%\medskip -%\noindent -%{\tt Inductive {\ident} \zeroone{\binders} : {\sort} := \\ -%\mbox{}\hspace{0.4cm} {\ident$_0$} : forall ({\ident$_1$}:{\term$_1$}) .. -%({\ident$_n$}:{\term$_n$}), {\ident} {\rm\sl params}.} -%\medskip +Remark here that the field \verb+Rat_bottom_cond+ depends +on the field \verb+bottom+ and \verb+Rat_irred_cond+ depends +on both \verb+top+ and \verb+bottom+. Let us now see the work done by the {\tt Record} macro. First the macro generates a variant type definition with just one constructor: \begin{quote} -{\tt Variant {\ident} {\params} :{\sort} :=} \\ -\qquad {\tt - {\ident$_0$} ({\ident$_1$}:{\term$_1$}) .. ({\ident$_n$}:{\term$_n$}).} +{\tt Variant {\ident} {\params} : {\sort} := \\ + {\ident$_0$} ({\ident$_1$} : {\term$_1$}) ... ({\ident$_n$} : {\term$_n$}).} \end{quote} To build an object of type {\ident}, one should provide the constructor {\ident$_0$} with $n$ terms filling the fields of @@ -109,28 +96,9 @@ the record. As an example, let us define the rational $1/2$: \begin{coq_example*} -Require Import Arith. Theorem one_two_irred : forall x y z:nat, x * y = 1 /\ x * z = 2 -> x = 1. -\end{coq_example*} -\begin{coq_eval} -Lemma mult_m_n_eq_m_1 : forall m n:nat, m * n = 1 -> m = 1. -destruct m; trivial. -intros; apply f_equal with (f := S). -destruct m; trivial. -destruct n; simpl in H. - rewrite <- mult_n_O in H. - discriminate. - rewrite <- plus_n_Sm in H. - discriminate. -Qed. - -intros x y z [H1 H2]. - apply mult_m_n_eq_m_1 with (n := y); trivial. -\end{coq_eval} -\ldots -\begin{coq_example*} -Qed. +Admitted. \end{coq_example*} \begin{coq_example} Definition half := mkRat true 1 2 (O_S 1) one_two_irred. @@ -139,80 +107,6 @@ Definition half := mkRat true 1 2 (O_S 1) one_two_irred. Check half. \end{coq_example} -The macro generates also, when it is possible, the projection -functions for destructuring an object of type {\ident}. These -projection functions have the same name that the corresponding -fields. If a field is named ``\verb=_='' then no projection is built -for it. In our example: - -\begin{coq_example} -Eval compute in half.(top). -Eval compute in half.(bottom). -Eval compute in half.(Rat_bottom_cond). -\end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} - -Records defined with the {\tt Record} keyword are not allowed to be -recursive (references to the record's name in the type of its field -raises an error). To define recursive records, one can use the {\tt - Inductive} and {\tt CoInductive} keywords, resulting in an inductive -or co-inductive record. A \emph{caveat}, however, is that records -cannot appear in mutually inductive (or co-inductive) definitions. -Induction schemes are automatically generated for inductive records. -Automatic generation of induction schemes for non-recursive records -defined with the {\tt Record} keyword can be activated with the -{\tt Nonrecursive Elimination Schemes} option -(see~\ref{set-nonrecursive-elimination-schemes}). - -\begin{Warnings} -\item {\tt {\ident$_i$} cannot be defined.} - - It can happen that the definition of a projection is impossible. - This message is followed by an explanation of this impossibility. - There may be three reasons: - \begin{enumerate} - \item The name {\ident$_i$} already exists in the environment (see - Section~\ref{Axiom}). - \item The body of {\ident$_i$} uses an incorrect elimination for - {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). - \item The type of the projections {\ident$_i$} depends on previous - projections which themselves could not be defined. - \end{enumerate} -\end{Warnings} - -\begin{ErrMsgs} - -\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} - - The record name {\ident} appears in the type of its fields, but uses - the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt - CoInductive} instead. -\item \errindex{Cannot handle mutually (co)inductive records.} - - Records cannot be defined as part of mutually inductive (or - co-inductive) definitions, whether with records only or mixed with - standard definitions. -\item During the definition of the one-constructor inductive - definition, all the errors of inductive definitions, as described in - Section~\ref{gal-Inductive-Definitions}, may also occur. - -\end{ErrMsgs} - -\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} -of the chapter devoted to coercions. - -\Rem {\tt Structure} is a synonym of the keyword {\tt Record}. - -\Rem Creation of an object of record type can be done by calling {\ident$_0$} -and passing arguments in the correct order. - -\begin{coq_example} -Record point := { x : nat; y : nat }. -Definition a := Build_point 5 3. -\end{coq_example} - \begin{figure}[t] \begin{centerframe} \begin{tabular}{lcl} @@ -226,15 +120,17 @@ Definition a := Build_point 5 3. \label{fig:fieldsyntax} \end{figure} -A syntax is available for creating objects by using named fields, as +Alternatively, the following syntax allows 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}). \begin{coq_example} -Definition b := {| x := 5; y := 3 |}. -Definition c := {| y := 3; x := 5 |}. +Definition half' := + {| sign := true; + Rat_bottom_cond := O_S 1; + Rat_irred_cond := one_two_irred |}. \end{coq_example} This syntax can be disabled globally for printing by @@ -256,23 +152,52 @@ This syntax can also be used for pattern matching. \begin{coq_example} Eval compute in ( - match b with - | {| y := S n |} => n + match half with + | {| sign := true; top := n |} => n | _ => 0 end). \end{coq_example} -\begin{coq_eval} -Reset Initial. -\end{coq_eval} +The macro generates also, when it is possible, the projection +functions for destructuring an object of type {\ident}. These +projection functions are given the names of the corresponding +fields. If a field is named ``\verb=_='' then no projection is built +for it. In our example: + +\begin{coq_example} +Eval compute in top half. +Eval compute in bottom half. +Eval compute in Rat_bottom_cond half. +\end{coq_example} + +An alternative syntax for projections based on a dot notation is +available: + +\begin{coq_example} +Eval compute in half.(top). +\end{coq_example} -\Rem A syntax for projections based on a dot notation is -available. The command to activate it is +It can be activated for printing with the command \optindex{Printing Projections} \begin{quote} {\tt Set Printing Projections.} \end{quote} +\begin{coq_example} +Set Printing Projections. +Check top half. +\end{coq_example} + +The corresponding grammar rules are given in Figure~\ref{fig:projsyntax}. +When {\qualid} denotes a projection, the syntax {\tt + {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax +{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to +{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax +{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to +{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} +is the object projected and the other arguments are the parameters of +the inductive type. + \begin{figure}[t] \begin{centerframe} \begin{tabular}{lcl} @@ -285,18 +210,66 @@ available. The command to activate it is \label{fig:projsyntax} \end{figure} -The corresponding grammar rules are given Figure~\ref{fig:projsyntax}. -When {\qualid} denotes a projection, the syntax {\tt - {\term}.({\qualid})} is equivalent to {\qualid~\term}, the syntax -{\term}{\tt .(}{\qualid}~{\termarg}$_1$ {\ldots} {\termarg}$_n${\tt )} to -{\qualid~{\termarg}$_1$ {\ldots} {\termarg}$_n$~\term}, and the syntax -{\term}{\tt .(@}{\qualid}~{\term}$_1$~\ldots~{\term}$_n${\tt )} to -{@\qualid~{\term}$_1$ {\ldots} {\term}$_n$~\term}. In each case, {\term} -is the object projected and the other arguments are the parameters of -the inductive type. +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{Remarks} + +\item Records defined with the {\tt Record} keyword are not allowed to be +recursive (references to the record's name in the type of its field +raises an error). To define recursive records, one can use the {\tt +Inductive} and {\tt CoInductive} keywords, resulting in an inductive +or co-inductive record. +A \emph{caveat}, however, is that records +cannot appear in mutually inductive (or co-inductive) definitions. + +\item Induction schemes are automatically generated for inductive records. +Automatic generation of induction schemes for non-recursive records +defined with the {\tt Record} keyword can be activated with the +{\tt Nonrecursive Elimination Schemes} option +(see~\ref{set-nonrecursive-elimination-schemes}). + +\item {\tt Structure} is a synonym of the keyword {\tt Record}. -To deactivate the printing of projections, use -{\tt Unset Printing Projections}. +\end{Remarks} + +\begin{Warnings} +\item {\tt {\ident$_i$} cannot be defined.} + + It can happen that the definition of a projection is impossible. + This message is followed by an explanation of this impossibility. + There may be three reasons: + \begin{enumerate} + \item The name {\ident$_i$} already exists in the environment (see + Section~\ref{Axiom}). + \item The body of {\ident$_i$} uses an incorrect elimination for + {\ident} (see Sections~\ref{Fixpoint} and~\ref{Caseexpr}). + \item The type of the projections {\ident$_i$} depends on previous + projections which themselves could not be defined. + \end{enumerate} +\end{Warnings} + +\begin{ErrMsgs} + +\item \errindex{Records declared with the keyword Record or Structure cannot be recursive.} + + The record name {\ident} appears in the type of its fields, but uses + the keyword {\tt Record}. Use the keyword {\tt Inductive} or {\tt + CoInductive} instead. +\item \errindex{Cannot handle mutually (co)inductive records.} + + Records cannot be defined as part of mutually inductive (or + co-inductive) definitions, whether with records only or mixed with + standard definitions. +\item During the definition of the one-constructor inductive + definition, all the errors of inductive definitions, as described in + Section~\ref{gal-Inductive-Definitions}, may also occur. + +\end{ErrMsgs} + +\SeeAlso Coercions and records in Section~\ref{Coercions-and-records} +of the chapter devoted to coercions. \subsection{Primitive Projections} \optindex{Primitive Projections} @@ -732,20 +705,20 @@ when the {\tt FunInd} library has been loaded via {\tt Require Import FunInd}: This command can be seen as a generalization of {\tt Fixpoint}. It is actually a wrapper for several ways of defining a function \emph{and other useful related objects}, namely: an induction principle that reflects the -recursive structure of the function (see \ref{FunInduction}), and its +recursive structure of the function (see \ref{FunInduction}) and its fixpoint equality. The meaning of this declaration is to define a function {\it ident}, similarly to {\tt Fixpoint}. Like in {\tt Fixpoint}, the decreasing argument must be -given (unless the function is not recursive), but it must not -necessary be \emph{structurally} decreasing. The point of the {\tt +given (unless the function is not recursive), but it might not +necessarily be \emph{structurally} decreasing. The point of the {\tt \{\}} annotation is to name the decreasing argument \emph{and} to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. -The {\tt Function} construction enjoys also the {\tt with} extension +The {\tt Function} construction also enjoys the {\tt with} extension to define mutually recursive definitions. However, this feature does -not work for non structural recursive functions. % VRAI?? +not work for non structurally recursive functions. % VRAI?? See the documentation of {\tt functional induction} (see Section~\ref{FunInduction}) and {\tt Functional Scheme} @@ -776,7 +749,7 @@ Function plus (n m : nat) {struct n} : nat := \end{coq_example*} \paragraph[Limitations]{Limitations\label{sec:Function-limitations}} -\term$_0$ must be build as a \emph{pure pattern-matching tree} +\term$_0$ must be built as a \emph{pure pattern-matching tree} (\texttt{match...with}) with applications only \emph{at the end} of each branch. @@ -803,7 +776,7 @@ For now dependent cases are not treated for non structurally terminating functio The generation of the graph relation \texttt{(R\_\ident)} used to compute the induction scheme of \ident\ raised a typing error. Only - the ident is defined, the induction scheme will not be generated. + the ident is defined; the induction scheme will not be generated. This error happens generally when: @@ -875,14 +848,14 @@ the following: being the decreasing argument and \term$_1$ being a function from type of \ident$_0$ to \texttt{nat} for which value on the decreasing argument decreases (for the {\tt lt} order on {\tt - nat}) at each recursive call of \term$_0$, parameters of the + nat}) at each recursive call of \term$_0$. Parameters of the function are bound in \term$_0$; \item {\tt \{wf} \term$_1$ \ident$_0${\tt\}} with \ident$_0$ being the decreasing argument and \term$_1$ an ordering relation on the type of \ident$_0$ (i.e. of type T$_{\ident_0}$ $\to$ T$_{\ident_0}$ $\to$ {\tt Prop}) for which the decreasing argument decreases at each recursive call of - \term$_0$. The order must be well founded. parameters of the + \term$_0$. The order must be well founded. Parameters of the function are bound in \term$_0$. \end{itemize} @@ -2011,6 +1984,11 @@ Check (fun x y => _) 0 1. Unset Printing Existential Instances. \end{coq_eval} +Existential variables can be named by the user upon creation using +the syntax {\tt ?[\ident]}. This is useful when the existential +variable needs to be explicitly handled later in the script (e.g. +with a named-goal selector, see~\ref{ltac:selector}). + \subsection{Explicit displaying of existential instances for pretty-printing \label{SetPrintingExistentialInstances} \optindex{Printing Existential Instances}} diff --git a/doc/refman/RefMan-gal.tex b/doc/refman/RefMan-gal.tex index 3814e4403a..71977d3e9d 100644 --- a/doc/refman/RefMan-gal.tex +++ b/doc/refman/RefMan-gal.tex @@ -3,7 +3,7 @@ \label{BNF-syntax} % Used referred to as a chapter label This chapter describes \gallina, the specification language of {\Coq}. -It allows developing mathematical theories and to prove specifications +It allows developing mathematical theories and proofs of specifications of programs. The theories are built from axioms, hypotheses, parameters, lemmas, theorems and definitions of constants, functions, predicates and sets. The syntax of logical objects involved in diff --git a/doc/refman/RefMan-ind.tex b/doc/refman/RefMan-ind.tex deleted file mode 100644 index 43bd2419f0..0000000000 --- a/doc/refman/RefMan-ind.tex +++ /dev/null @@ -1,510 +0,0 @@ - -%\documentstyle[11pt]{article} -%\input{title} - -%\include{macros} -%\makeindex - -%\begin{document} -%\coverpage{The module {\tt Equality}}{Cristina CORNES} - -%\tableofcontents - -\chapter[Tactics for inductive types and families]{Tactics for inductive types and families\label{Addoc-equality}} - -This chapter details a few special tactics useful for inferring facts -from inductive hypotheses. They can be considered as tools that -macro-generate complicated uses of the basic elimination tactics for -inductive types. - -Sections \ref{inversion_introduction} to \ref{inversion_using} present -inversion tactics and Section~\ref{scheme} describes -a command {\tt Scheme} for automatic generation of induction schemes -for mutual inductive types. - -%\end{document} -%\documentstyle[11pt]{article} -%\input{title} - -%\begin{document} -%\coverpage{Module Inv: Inversion Tactics}{Cristina CORNES} - -\section[Generalities about inversion]{Generalities about inversion\label{inversion_introduction}} -When working with (co)inductive predicates, we are very often faced to -some of these situations: -\begin{itemize} -\item we have an inconsistent instance of an inductive predicate in the - local context of hypotheses. Thus, the current goal can be trivially - proved by absurdity. - -\item we have a hypothesis that is an instance of an inductive - predicate, and the instance has some variables whose constraints we - would like to derive. -\end{itemize} - -The inversion tactics are very useful to simplify the work in these -cases. Inversion tools can be classified in three groups: -\begin{enumerate} -\item tactics for inverting an instance without stocking the inversion - lemma in the context: - (\texttt{Dependent}) \texttt{Inversion} and - (\texttt{Dependent}) \texttt{Inversion\_clear}. -\item commands for generating and stocking in the context the inversion - lemma corresponding to an instance: \texttt{Derive} - (\texttt{Dependent}) \texttt{Inversion}, \texttt{Derive} - (\texttt{Dependent}) \texttt{Inversion\_clear}. -\item tactics for inverting an instance using an already defined - inversion lemma: \texttt{Inversion \ldots using}. -\end{enumerate} - -These tactics work for inductive types of arity $(\vec{x}:\vec{T})s$ -where $s \in \{Prop,Set,Type\}$. Sections \ref{inversion_primitive}, -\ref{inversion_derivation} and \ref{inversion_using} -describe respectively each group of tools. - -As inversion proofs may be large in size, we recommend the user to -stock the lemmas whenever the same instance needs to be inverted -several times.\\ - -Let's consider the relation \texttt{Le} over natural numbers and the -following variables: - -\begin{coq_eval} -Restore State "Initial". -\end{coq_eval} - -\begin{coq_example*} -Inductive Le : nat -> nat -> Set := - | LeO : forall n:nat, Le 0%N n - | LeS : forall n m:nat, Le n m -> Le (S n) (S m). -Variable P : nat -> nat -> Prop. -Variable Q : forall n m:nat, Le n m -> Prop. -\end{coq_example*} - -For example purposes we defined \verb+Le: nat->nat->Set+ - but we may have defined -it \texttt{Le} of type \verb+nat->nat->Prop+ or \verb+nat->nat->Type+. - - -\section[Inverting an instance]{Inverting an instance\label{inversion_primitive}} -\subsection{The non dependent case} -\begin{itemize} - -\item \texttt{Inversion\_clear} \ident~\\ -\index{Inversion-clear@{\tt Inversion\_clear}} - Let the type of \ident~ in the local context be $(I~\vec{t})$, - where $I$ is a (co)inductive predicate. Then, - \texttt{Inversion} applied to \ident~ derives for each possible - constructor $c_i$ of $(I~\vec{t})$, {\bf all} the necessary - conditions that should hold for the instance $(I~\vec{t})$ to be - proved by $c_i$. Finally it erases \ident~ from the context. - - - -For example, consider the goal: -\begin{coq_eval} -Lemma ex : forall n m:nat, Le (S n) m -> P n m. -intros. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} - -To prove the goal we may need to reason by cases on \texttt{H} and to - derive that \texttt{m} is necessarily of -the form $(S~m_0)$ for certain $m_0$ and that $(Le~n~m_0)$. -Deriving these conditions corresponds to prove that the -only possible constructor of \texttt{(Le (S n) m)} is -\texttt{LeS} and that we can invert the -\texttt{->} in the type of \texttt{LeS}. -This inversion is possible because \texttt{Le} is the smallest set closed by -the constructors \texttt{LeO} and \texttt{LeS}. - - -\begin{coq_example} -inversion_clear H. -\end{coq_example} - -Note that \texttt{m} has been substituted in the goal for \texttt{(S m0)} -and that the hypothesis \texttt{(Le n m0)} has been added to the -context. - -\item \texttt{Inversion} \ident~\\ -\index{Inversion@{\tt Inversion}} - This tactic differs from {\tt Inversion\_clear} in the fact that - it adds the equality constraints in the context and - it does not erase the hypothesis \ident. - - -In the previous example, {\tt Inversion\_clear} -has substituted \texttt{m} by \texttt{(S m0)}. Sometimes it is -interesting to have the equality \texttt{m=(S m0)} in the -context to use it after. In that case we can use \texttt{Inversion} that -does not clear the equalities: - -\begin{coq_example*} -Undo. -\end{coq_example*} -\begin{coq_example} -inversion H. -\end{coq_example} - -\begin{coq_eval} -Undo. -\end{coq_eval} - -Note that the hypothesis \texttt{(S m0)=m} has been deduced and -\texttt{H} has not been cleared from the context. - -\end{itemize} - -\begin{Variants} - -\item \texttt{Inversion\_clear } \ident~ \texttt{in} \ident$_1$ \ldots - \ident$_n$\\ -\index{Inversion_clear...in@{\tt Inversion\_clear...in}} - Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This - tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing - {\tt Inversion\_clear}. - -\item \texttt{Inversion } \ident~ \texttt{in} \ident$_1$ \ldots \ident$_n$\\ -\index{Inversion ... in@{\tt Inversion ... in}} - Let \ident$_1$ \ldots \ident$_n$, be identifiers in the local context. This - tactic behaves as generalizing \ident$_1$ \ldots \ident$_n$, and then performing - \texttt{Inversion}. - - -\item \texttt{Simple Inversion} \ident~ \\ -\index{Simple Inversion@{\tt Simple Inversion}} - It is a very primitive inversion tactic that derives all the necessary - equalities but it does not simplify - the constraints as \texttt{Inversion} and - {\tt Inversion\_clear} do. - -\end{Variants} - - -\subsection{The dependent case} -\begin{itemize} -\item \texttt{Dependent Inversion\_clear} \ident~\\ -\index{Dependent Inversion-clear@{\tt Dependent Inversion\_clear}} - Let the type of \ident~ in the local context be $(I~\vec{t})$, - where $I$ is a (co)inductive predicate, and let the goal depend both on - $\vec{t}$ and \ident. Then, - \texttt{Dependent Inversion\_clear} applied to \ident~ derives - for each possible constructor $c_i$ of $(I~\vec{t})$, {\bf all} the - necessary conditions that should hold for the instance $(I~\vec{t})$ to be - proved by $c_i$. It also substitutes \ident~ for the corresponding - term in the goal and it erases \ident~ from the context. - - -For example, consider the goal: -\begin{coq_eval} -Lemma ex_dep : forall (n m:nat) (H:Le (S n) m), Q (S n) m H. -intros. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} - -As \texttt{H} occurs in the goal, we may want to reason by cases on its -structure and so, we would like inversion tactics to -substitute \texttt{H} by the corresponding term in constructor form. -Neither \texttt{Inversion} nor {\tt Inversion\_clear} make such a -substitution. To have such a behavior we use the dependent inversion tactics: - -\begin{coq_example} -dependent inversion_clear H. -\end{coq_example} - -Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and -\texttt{m} by \texttt{(S m0)}. - - -\end{itemize} - -\begin{Variants} - -\item \texttt{Dependent Inversion\_clear } \ident~ \texttt{ with } \term\\ -\index{Dependent Inversion_clear...with@{\tt Dependent Inversion\_clear...with}} - \noindent Behaves as \texttt{Dependent Inversion\_clear} but allows giving - explicitly the good generalization of the goal. It is useful when - the system fails to generalize the goal automatically. If - \ident~ has type $(I~\vec{t})$ and $I$ has type - $(\vec{x}:\vec{T})s$, then \term~ must be of type - $I:(\vec{x}:\vec{T})(I~\vec{x})\rightarrow s'$ where $s'$ is the - type of the goal. - - - -\item \texttt{Dependent Inversion} \ident~\\ -\index{Dependent Inversion@{\tt Dependent Inversion}} - This tactic differs from \texttt{Dependent Inversion\_clear} in the fact that - it also adds the equality constraints in the context and - it does not erase the hypothesis \ident~. - -\item \texttt{Dependent Inversion } \ident~ \texttt{ with } \term \\ -\index{Dependent Inversion...with@{\tt Dependent Inversion...with}} - Analogous to \texttt{Dependent Inversion\_clear .. with..} above. -\end{Variants} - - - -\section[Deriving the inversion lemmas]{Deriving the inversion lemmas\label{inversion_derivation}} -\subsection{The non dependent case} - -The tactics (\texttt{Dependent}) \texttt{Inversion} and (\texttt{Dependent}) -{\tt Inversion\_clear} work on a -certain instance $(I~\vec{t})$ of an inductive predicate. At each -application, they inspect the given instance and derive the -corresponding inversion lemma. If we have to invert the same -instance several times it is recommended to stock the lemma in the -context and to reuse it whenever we need it. - -The families of commands \texttt{Derive Inversion}, \texttt{Derive -Dependent Inversion}, \texttt{Derive} \\ {\tt Inversion\_clear} and \texttt{Derive Dependent Inversion\_clear} -allow to generate inversion lemmas for given instances and sorts. Next -section describes the tactic \texttt{Inversion}$\ldots$\texttt{using} that refines the -goal with a specified inversion lemma. - -\begin{itemize} - -\item \texttt{Derive Inversion\_clear} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Inversion_clear...with@{\tt Derive Inversion\_clear...with}} - Let $I$ be an inductive predicate and $\vec{x}$ the variables - occurring in $\vec{t}$. This command generates and stocks - the inversion lemma for the sort \sort~ corresponding to the instance - $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf - global} environment. When applied it is equivalent to have - inverted the instance with the tactic {\tt Inversion\_clear}. - - - For example, to generate the inversion lemma for the instance - \texttt{(Le (S n) m)} and the sort \texttt{Prop} we do: -\begin{coq_example} -Derive Inversion_clear leminv with (forall n m:nat, Le (S n) m) Sort - Prop. -\end{coq_example} - -Let us inspect the type of the generated lemma: -\begin{coq_example} -Check leminv. -\end{coq_example} - - - -\end{itemize} - -%\variants -%\begin{enumerate} -%\item \verb+Derive Inversion_clear+ \ident$_1$ \ident$_2$ \\ -%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}} -% Let \ident$_1$ have type $(I~\vec{t})$ in the local context ($I$ -% an inductive predicate). Then, this command has the same semantics -% as \verb+Derive Inversion_clear+ \ident$_2$~ \verb+with+ -% $(\vec{x}:\vec{T})(I~\vec{t})$ \verb+Sort Prop+ where $\vec{x}$ are the free -% variables of $(I~\vec{t})$ declared in the local context (variables -% of the global context are considered as constants). -%\item \verb+Derive Inversion+ \ident$_1$~ \ident$_2$~\\ -%\index{Derive Inversion@{\tt Derive Inversion}} -% Analogous to the previous command. -%\item \verb+Derive Inversion+ $num$ \ident~ \ident~ \\ -%\index{Derive Inversion@{\tt Derive Inversion}} -% This command behaves as \verb+Derive Inversion+ \ident~ {\it -% namehyp} performed on the goal number $num$. -% -%\item \verb+Derive Inversion_clear+ $num$ \ident~ \ident~ \\ -%\index{Derive Inversion_clear@{\tt Derive Inversion\_clear}} -% This command behaves as \verb+Derive Inversion_clear+ \ident~ -% \ident~ performed on the goal number $num$. -%\end{enumerate} - - - -A derived inversion lemma is adequate for inverting the instance -with which it was generated, \texttt{Derive} applied to -different instances yields different lemmas. In general, if we generate -the inversion lemma with -an instance $(\vec{x}:\vec{T})(I~\vec{t})$ and a sort $s$, the inversion lemma will -expect a predicate of type $(\vec{x}:\vec{T})s$ as first argument. \\ - -\begin{Variant} -\item \texttt{Derive Inversion} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort\\ -\index{Derive Inversion...with@{\tt Derive Inversion...with}} - Analogous of \texttt{Derive Inversion\_clear .. with ..} but - when applied it is equivalent to having - inverted the instance with the tactic \texttt{Inversion}. -\end{Variant} - -\subsection{The dependent case} -\begin{itemize} -\item \texttt{Derive Dependent Inversion\_clear} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Dependent Inversion\_clear...with@{\tt Derive Dependent Inversion\_clear...with}} - Let $I$ be an inductive predicate. This command generates and stocks - the dependent inversion lemma for the sort \sort~ corresponding to the instance - $(\vec{x}:\vec{T})(I~\vec{t})$ with the name \ident~ in the {\bf - global} environment. When applied it is equivalent to having - inverted the instance with the tactic \texttt{Dependent Inversion\_clear}. -\end{itemize} - -\begin{coq_example} -Derive Dependent Inversion_clear leminv_dep with - (forall n m:nat, Le (S n) m) Sort Prop. -\end{coq_example} - -\begin{coq_example} -Check leminv_dep. -\end{coq_example} - -\begin{Variants} -\item \texttt{Derive Dependent Inversion} \ident~ \texttt{with} - $(\vec{x}:\vec{T})(I~\vec{t})$ \texttt{Sort} \sort~ \\ -\index{Derive Dependent Inversion...with@{\tt Derive Dependent Inversion...with}} - Analogous to \texttt{Derive Dependent Inversion\_clear}, but when - applied it is equivalent to having - inverted the instance with the tactic \texttt{Dependent Inversion}. - -\end{Variants} - -\section[Using already defined inversion lemmas]{Using already defined inversion lemmas\label{inversion_using}} -\begin{itemize} -\item \texttt{Inversion} \ident \texttt{ using} \ident$'$ \\ -\index{Inversion...using@{\tt Inversion...using}} - Let \ident~ have type $(I~\vec{t})$ ($I$ an inductive - predicate) in the local context, and \ident$'$ be a (dependent) inversion - lemma. Then, this tactic refines the current goal with the specified - lemma. - - -\begin{coq_eval} -Abort. -\end{coq_eval} - -\begin{coq_example} -Show. -\end{coq_example} -\begin{coq_example} -inversion H using leminv. -\end{coq_example} - - -\end{itemize} -\variant -\begin{enumerate} -\item \texttt{Inversion} \ident~ \texttt{using} \ident$'$ \texttt{in} \ident$_1$\ldots \ident$_n$\\ -\index{Inversion...using...in@{\tt Inversion...using...in}} -This tactic behaves as generalizing \ident$_1$\ldots \ident$_n$, -then doing \texttt{Use Inversion} \ident~\ident$'$. -\end{enumerate} - -\section[\tt Scheme ...]{\tt Scheme ...\index{Scheme@{\tt Scheme}}\label{Scheme} -\label{scheme}} -The {\tt Scheme} command is a high-level tool for generating -automatically (possibly mutual) induction principles for given types -and sorts. Its syntax follows the schema : - -\noindent -{\tt Scheme {\ident$_1$} := Induction for \term$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} .. \\ - with {\ident$_m$} := Induction for {\term$_m$} Sort - {\sort$_m$}}\\ -\term$_1$ \ldots \term$_m$ are different inductive types belonging to -the same package of mutual inductive definitions. This command -generates {\ident$_1$}\ldots{\ident$_m$} to be mutually recursive -definitions. Each term {\ident$_i$} proves a general principle -of mutual induction for objects in type {\term$_i$}. - -\Example -The definition of principle of mutual induction for {\tt tree} and -{\tt forest} over the sort {\tt Set} is defined by the command: -\begin{coq_eval} -Restore State "Initial". -Variables A B : Set. -Inductive tree : Set := - node : A -> forest -> tree -with forest : Set := - | leaf : B -> forest - | cons : tree -> forest -> forest. -\end{coq_eval} -\begin{coq_example*} -Scheme tree_forest_rec := Induction for tree - Sort Set - with forest_tree_rec := Induction for forest Sort Set. -\end{coq_example*} -You may now look at the type of {\tt tree\_forest\_rec} : -\begin{coq_example} -Check tree_forest_rec. -\end{coq_example} -This principle involves two different predicates for {\tt trees} and -{\tt forests}; it also has three premises each one corresponding to a -constructor of one of the inductive definitions. - -The principle {\tt tree\_forest\_rec} shares exactly the same -premises, only the conclusion now refers to the property of forests. -\begin{coq_example} -Check forest_tree_rec. -\end{coq_example} - -\begin{Variant} -\item {\tt Scheme {\ident$_1$} := Minimality for \term$_1$ Sort {\sort$_1$} \\ - with\\ - \mbox{}\hspace{0.1cm} .. \\ - with {\ident$_m$} := Minimality for {\term$_m$} Sort - {\sort$_m$}}\\ -Same as before but defines a non-dependent elimination principle more -natural in case of inductively defined relations. -\end{Variant} - -\Example -With the predicates {\tt odd} and {\tt even} inductively defined as: -% \begin{coq_eval} -% Restore State "Initial". -% \end{coq_eval} -\begin{coq_example*} -Inductive odd : nat -> Prop := - oddS : forall n:nat, even n -> odd (S n) -with even : nat -> Prop := - | evenO : even 0%N - | evenS : forall n:nat, odd n -> even (S n). -\end{coq_example*} -The following command generates a powerful elimination -principle: -\begin{coq_example*} -Scheme odd_even := Minimality for odd Sort Prop - with even_odd := Minimality for even Sort Prop. -\end{coq_example*} -The type of {\tt odd\_even} for instance will be: -\begin{coq_example} -Check odd_even. -\end{coq_example} -The type of {\tt even\_odd} shares the same premises but the -conclusion is {\tt (n:nat)(even n)->(Q n)}. - -\subsection[\tt Combined Scheme ...]{\tt Combined Scheme ...\index{CombinedScheme@{\tt Combined Scheme}}\label{CombinedScheme} -\label{combinedscheme}} -The {\tt Combined Scheme} command is a tool for combining -induction principles generated by the {\tt Scheme} command. -Its syntax follows the schema : - -\noindent -{\tt Combined Scheme {\ident$_0$} from {\ident$_1$}, .., {\ident$_n$}}\\ -\ident$_1$ \ldots \ident$_n$ are different inductive principles that must belong to -the same package of mutual inductive principle definitions. This command -generates {\ident$_0$} to be the conjunction of the principles: it is -build from the common premises of the principles and concluded by the -conjunction of their conclusions. For exemple, we can combine the -induction principles for trees and forests: - -\begin{coq_example*} -Combined Scheme tree_forest_mutind from tree_ind, forest_ind. -Check tree_forest_mutind. -\end{coq_example*} - -%\end{document} - diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index bb679ecba7..3ce1d4ecd8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -392,7 +392,7 @@ all selected goals. \item{} [{\ident}] {\tt :} {\tacexpr} In this variant, {\tacexpr} is applied locally to a goal - previously named by the user. + previously named by the user (see~\ref{ExistentialVariables}). \item {\num} {\tt :} {\tacexpr} @@ -891,7 +891,7 @@ behavior can be retrieved with the {\tt Tactic Compat Context} flag. \end{Variants} -\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}} +\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal@\texttt{match goal}}\label{ltac-match-goal} \index{Ltac!match reverse goal@\texttt{match reverse goal}} \index{match goal@\texttt{match goal}!in Ltac} \index{match reverse goal@\texttt{match reverse goal}!in Ltac}} @@ -1131,8 +1131,9 @@ on. This can be obtained thanks to the option below. \optindex{Shrink Abstract} {\tt Set Shrink Abstract} \end{quote} +\emph{Deprecated since 8.7} -When set, all lemmas generated through \texttt{abstract {\tacexpr}} +When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the variables that appear in the term constructed by \texttt{\tacexpr}. diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index b66659dc8c..95fee3241c 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -421,6 +421,24 @@ This command displays the current goals. \item \errindex{No focused proof} \end{ErrMsgs} +\item {\tt Show {\ident}.}\\ + Displays the named goal {\ident}. + This is useful in particular to display a shelved goal but only works + if the corresponding existential variable has been named by the user + (see~\ref{ExistentialVariables}) as in the following example. + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + +\begin{coq_example*} +Goal exists n, n = 0. + eexists ?[n]. +\end{coq_example*} +\begin{coq_example} + Show n. +\end{coq_example} + \item {\tt Show Script.}\comindex{Show Script}\\ Displays the whole list of tactics applied from the beginning of the current proof. diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index ecaf82806e..084317776b 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -13,7 +13,7 @@ described in Section~\ref{scopes}. were present for a while in {\Coq} are no longer available from {\Coq} version 8.0. The underlying AST structure is also no longer available. The functionalities of the command {\tt Syntactic Definition} are -still available, see Section~\ref{Abbreviations}. +still available; see Section~\ref{Abbreviations}. \section[Notations]{Notations\label{Notation} \comindex{Notation}} @@ -35,8 +35,8 @@ The expression \texttt{(and A B)} is the abbreviated term and the string \verb="A /\ B"= (called a {\em notation}) tells how it is symbolically written. -A notation is always surrounded by double quotes (excepted when the -abbreviation is a single identifier, see \ref{Abbreviations}). The +A notation is always surrounded by double quotes (except when the +abbreviation is a single identifier; see \ref{Abbreviations}). The notation is composed of {\em tokens} separated by spaces. Identifiers in the string (such as \texttt{A} and \texttt{B}) are the {\em parameters} of the notation. They must occur at least once each in the @@ -68,7 +68,7 @@ declaration of the notation. \subsection[Precedences and associativity]{Precedences and associativity\index{Precedences} \index{Associativity}} -Mixing different symbolic notations in a same text may cause serious +Mixing different symbolic notations in the same text may cause serious parsing ambiguity. To deal with the ambiguity of notations, {\Coq} uses precedence levels ranging from 0 to 100 (plus one extra level numbered 200) and associativity rules. @@ -88,8 +88,8 @@ precedence level to each notation, knowing that a lower level binds more than a higher level. Hence the level for disjunction must be higher than the level for conjunction. -Since connectives are the less tight articulation points of a text, it -is reasonable to choose levels not so far from the higher level which +Since connectives are not tight articulation points of a text, it +is reasonable to choose levels not so far from the highest level which is 100, for example 85 for disjunction and 80 for conjunction\footnote{which are the levels effectively chosen in the current implementation of {\Coq}}. @@ -102,10 +102,10 @@ even consider that the expression is not well-formed and that parentheses are mandatory (this is a ``no associativity'')\footnote{ {\Coq} accepts notations declared as no associative but the parser on which {\Coq} is built, namely {\camlpppp}, currently does not implement the -no-associativity and replace it by a left associativity; hence it is +no-associativity and replaces it by a left associativity; hence it is the same for {\Coq}: no-associativity is in fact left associativity}. We don't know of a special convention of the associativity of -disjunction and conjunction, let's apply for instance a right +disjunction and conjunction, so let's apply for instance a right associativity (which is the choice of {\Coq}). Precedence levels and associativity rules of notations have to be @@ -701,11 +701,11 @@ Notation}. % Introduction An {\em interpretation scope} is a set of notations for terms with -their interpretation. Interpretation scopes provides with a weak, -purely syntactical form of notations overloading: a same notation, for -instance the infix symbol \verb=+= can be used to denote distinct -definitions of an additive operator. Depending on which interpretation -scopes is currently open, the interpretation is different. +their interpretation. Interpretation scopes provide a weak, +purely syntactical form of notation overloading: the same notation, for +instance the infix symbol \verb=+=, can be used to denote distinct +definitions of the additive operator. Depending on which interpretation +scope is currently open, the interpretation is different. Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the {\ocaml} level. @@ -889,7 +889,8 @@ statically. For instance, if {\tt f} is a polymorphic function of type recognized as an argument to be interpreted in scope {\scope}. \comindex{Bind Scope} -More generally, any {\class} (see Chapter~\ref{Coercions-full}) can be +\label{bindscope} +More generally, any coercion {\class} (see Chapter~\ref{Coercions-full}) can be bound to an interpretation scope. The command to do it is \begin{quote} {\tt Bind Scope} {\scope} \texttt{with} {\class} @@ -908,7 +909,7 @@ Open Scope nat_scope. (* Define + on the nat as the default for + *) Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). \end{coq_example} -\Rem The scope {\tt type\_scope} has also a local effect on +\Rem The scopes {\tt type\_scope} and {\tt function\_scope} also have a local effect on interpretation. See the next section. \SeeAlso The command to show the scopes bound to the arguments of a @@ -940,10 +941,21 @@ Check # @@%mybool #. The scope {\tt type\_scope} has a special status. It is a primitive interpretation scope which is temporarily activated each time a -subterm of an expression is expected to be a type. This includes goals -and statements, types of binders, domain and codomain of implication, -codomain of products, and more generally any type argument of a -declared or defined constant. +subterm of an expression is expected to be a type. It is delimited by +the key {\tt type}, and bound to the coercion class {\tt Sortclass}. It is also +used in certain situations where an expression is statically known to +be a type, including the conclusion and the type of hypotheses within +an {\tt Ltac} goal match (see Section~\ref{ltac-match-goal}) +the statement of a theorem, the type of +a definition, the type of a binder, the domain and codomain of +implication, the codomain of products, and more generally any type +argument of a declared or defined constant. + +\subsection[The {\tt function\_scope} interpretation scope]{The {\tt function\_scope} interpretation scope\index{function\_scope@\texttt{function\_scope}}} + +The scope {\tt function\_scope} also has a special status. +It is temporarily activated each time the argument of a global reference is +recognized to be a {\tt Funclass instance}, i.e., of type {\tt forall x:A, B} or {\tt A -> B}. \subsection{Interpretation scopes used in the standard library of {\Coq}} @@ -953,38 +965,39 @@ commands {\tt Print Scopes} or {\tt Print Scope {\scope}}. \subsubsection{\tt type\_scope} -This includes infix {\tt *} for product types and infix {\tt +} for -sum types. It is delimited by key {\tt type}. +This scope includes infix {\tt *} for product types and infix {\tt +} for +sum types. It is delimited by key {\tt type}, and bound to the coercion class +{\tt Sortclass}, as described at \ref{bindscope}. \subsubsection{\tt nat\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt nat}. Positive numerals in this scope are mapped to their canonical representent built from {\tt O} and {\tt S}. The scope is -delimited by key {\tt nat}. +delimited by key {\tt nat}, and bound to the type {\tt nat} (see \ref{bindscope}). \subsubsection{\tt N\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt N} (binary natural numbers). It is delimited by key {\tt N} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt Z\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Z} (binary integer numbers). It is delimited by key {\tt Z} and comes with an interpretation for numerals as closed term of type {\tt Z}. \subsubsection{\tt positive\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt positive} (binary strictly positive numbers). It is delimited by key {\tt positive} and comes with an interpretation for numerals as closed term of type {\tt positive}. \subsubsection{\tt Q\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt Q} (rational numbers defined as fractions of an integer and a strictly positive integer modulo the equality of the numerator-denominator cross-product). As for numerals, only $0$ and @@ -993,13 +1006,13 @@ interpretations are $\frac{0}{1}$ and $\frac{1}{1}$ respectively). \subsubsection{\tt Qc\_scope} -This includes the standard arithmetical operators and relations on the +This scope includes the standard arithmetical operators and relations on the type {\tt Qc} of rational numbers defined as the type of irreducible fractions of an integer and a strictly positive integer. \subsubsection{\tt real\_scope} -This includes the standard arithmetical operators and relations on +This scope includes the standard arithmetical operators and relations on type {\tt R} (axiomatic real numbers). It is delimited by key {\tt R} and comes with an interpretation for numerals as term of type {\tt R}. The interpretation is based on the binary decomposition. The @@ -1014,35 +1027,40 @@ those of {\tt R}. \subsubsection{\tt bool\_scope} -This includes notations for the boolean operators. It is -delimited by key {\tt bool}. +This scope includes notations for the boolean operators. It is +delimited by key {\tt bool}, and bound to the type {\tt bool} (see \ref{bindscope}). \subsubsection{\tt list\_scope} -This includes notations for the list operators. It is -delimited by key {\tt list}. +This scope includes notations for the list operators. It is +delimited by key {\tt list}, and bound to the type {\tt list} (see \ref{bindscope}). + +\subsubsection{\tt function\_scope} + +This scope is delimited by the key {\tt function}, and bound to the coercion class {\tt Funclass}, +as described at \ref{bindscope}. \subsubsection{\tt core\_scope} -This includes the notation for pairs. It is delimited by key {\tt core}. +This scope includes the notation for pairs. It is delimited by key {\tt core}. \subsubsection{\tt string\_scope} -This includes notation for strings as elements of the type {\tt +This scope includes notation for strings as elements of the type {\tt string}. Special characters and escaping follow {\Coq} conventions on strings (see Section~\ref{strings}). Especially, there is no convention to visualize non printable characters of a string. The file {\tt String.v} shows an example that contains quotes, a newline -and a beep (i.e. the ascii character of code 7). +and a beep (i.e. the ASCII character of code 7). \subsubsection{\tt char\_scope} -This includes interpretation for all strings of the form -\verb!"!$c$\verb!"! where $c$ is an ascii character, or of the form +This scope includes interpretation for all strings of the form +\verb!"!$c$\verb!"! where $c$ is an ASCII character, or of the form \verb!"!$nnn$\verb!"! where $nnn$ is a three-digits number (possibly with leading 0's), or of the form \verb!""""!. Their respective -denotations are the ascii code of $c$, the decimal ascii code $nnn$, -or the ascii code of the character \verb!"! (i.e. the ascii code +denotations are the ASCII code of $c$, the decimal ASCII code $nnn$, +or the ASCII code of the character \verb!"! (i.e. the ASCII code 34), all of them being represented in the type {\tt ascii}. \subsection{Displaying informations about scopes} diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2bab04e90a..a23c432322 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -352,7 +352,7 @@ Section~\ref{pattern} to transform the goal so that it gets the form The tactic {\tt eapply} behaves like {\tt apply} but it does not fail when no instantiations are deducible for some variables in the - premises. Rather, it turns these variables into + premises. Rather, it turns these variables into existential variables which are variables still to instantiate (see Section~\ref{evars}). The instantiation is intended to be found later in the proof. @@ -1053,21 +1053,31 @@ dependencies. This tactic is the inverse of {\tt intro}. \label{move} This moves the hypothesis named {\ident$_1$} in the local context -after the hypothesis named {\ident$_2$}. The proof term is not changed. +after the hypothesis named {\ident$_2$}, where ``after'' is in +reference to the direction of the move. The proof term is not changed. -If {\ident$_1$} comes before {\ident$_2$} in the order of dependencies, -then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) depend on {\ident$_1$} are moved too. +If {\ident$_1$} comes before {\ident$_2$} in the order of +dependencies, then all the hypotheses between {\ident$_1$} and +{\ident$_2$} that (possibly indirectly) depend on {\ident$_1$} are +moved too, and all of them are thus moved after {\ident$_2$} in the +order of dependencies. If {\ident$_1$} comes after {\ident$_2$} in the order of dependencies, then all the hypotheses between {\ident$_1$} and {\ident$_2$} that -(possibly indirectly) occur in {\ident$_1$} are moved too. +(possibly indirectly) occur in the type of {\ident$_1$} are moved +too, and all of them are thus moved before {\ident$_2$} in the order +of dependencies. \begin{Variants} \item {\tt move {\ident$_1$} before {\ident$_2$}} -This moves {\ident$_1$} towards and just before the hypothesis named {\ident$_2$}. +This moves {\ident$_1$} towards and just before the hypothesis named +{\ident$_2$}. As for {\tt move {\ident$_1$} after {\ident$_2$}}, +dependencies over {\ident$_1$} (when {\ident$_1$} comes before +{\ident$_2$} in the order of dependencies) or in the type of +{\ident$_1$} (when {\ident$_1$} comes after {\ident$_2$} in the order +of dependencies) are moved too. \item {\tt move {\ident} at top} @@ -1084,13 +1094,30 @@ This moves {\ident} at the bottom of the local context (at the end of the contex \item \errindex{No such hypothesis} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: - it occurs in {\ident$_2$}} + it occurs in the type of {\ident$_2$}} \item \errindex{Cannot move {\ident$_1$} after {\ident$_2$}: it depends on {\ident$_2$}} \end{ErrMsgs} +\Example + +\begin{coq_example} +Goal forall x :nat, x = 0 -> forall z y:nat, y=y-> 0=x. +intros x H z y H0. +move x after H0. +Undo. +move x before H0. +Undo. +move H0 after H. +Undo. +move H0 before H. +\end{coq_example} +\begin{coq_eval} +Abort. +\end{coq_eval} + \subsection{\tt rename {\ident$_1$} into {\ident$_2$}} \tacindex{rename} @@ -1384,7 +1411,7 @@ in the list of subgoals remaining to prove. quantifications or non-dependent implications) are instantiated by concrete terms coming either from arguments \term$_1$ $\ldots$ \term$_n$ or from a bindings list (see - Section~\ref{Binding-list} for more about bindings lists). + Section~\ref{Binding-list} for more about bindings lists). 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$)}. @@ -1488,23 +1515,33 @@ The {\tt evar} tactic creates a new local definition named \ident\ with type \term\ in the context. The body of this binding is a fresh existential variable. -\subsection{\tt instantiate ( {\num} := {\term} )} +\subsection{\tt instantiate ( {\ident} := {\term} )} \tacindex{instantiate} \label{instantiate} The {\tt instantiate} tactic refines (see Section~\ref{refine}) -an existential variable -with the term \term. The \num\ argument is the position of the -existential variable from right to left in the conclusion. This cannot be -the number of the existential variable since this number is different -in every session. +an existential variable {\ident} with the term {\term}. +It is equivalent to {\tt only [\ident]: refine \term} (preferred alternative). + +\begin{Remarks} +\item To be able to refer to an existential variable by name, the +user must have given the name explicitly (see~\ref{ExistentialVariables}). -When you are referring to hypotheses which you did not name +\item When you are referring to hypotheses which you did not name explicitly, be aware that Coq may make a different decision on how to name the variable in the current goal and in the context of the existential variable. This can lead to surprising behaviors. +\end{Remarks} \begin{Variants} + + \item {\tt instantiate ( {\num} := {\term} )} + This variant allows to refer to an existential variable which was not + named by the user. The {\num} argument is the position of the + existential variable from right to left in the goal. + Because this variant is not robust to slight changes in the goal, + its use is strongly discouraged. + \item {\tt instantiate ( {\num} := {\term} ) in \ident} \item {\tt instantiate ( {\num} := {\term} ) in ( Value of {\ident} )} @@ -2567,6 +2604,21 @@ Abort. This tactic behaves as generalizing \ident$_1$\dots\ \ident$_n$, then doing \texttt{inversion {\ident} using \ident$'$}. +\item \tacindex{inversion\_sigma} \texttt{inversion\_sigma} + + This tactic turns equalities of dependent pairs (e.g., + \texttt{existT P x p = existT P y q}, frequently left over by + \texttt{inversion} on a dependent type family) into pairs of + equalities (e.g., a hypothesis \texttt{H : x = y} and a hypothesis + of type \texttt{rew H in p = q}); these hypotheses can subsequently + be simplified using \texttt{subst}, without ever invoking any kind + of axiom asserting uniqueness of identity proofs. If you want to + explicitly specify the hypothesis to be inverted, or name the + generated hypotheses, you can invoke \texttt{induction H as [H1 H2] + using eq\_sigT\_rect}. This tactic also works for \texttt{sig}, + \texttt{sigT2}, and \texttt{sig2}, and there are similar + \texttt{eq\_sig\emph{*}\_rect} induction lemmas. + \end{Variants} \firstexample @@ -2661,6 +2713,64 @@ dependent inversion_clear H. Note that \texttt{H} has been substituted by \texttt{(LeS n m0 l)} and \texttt{m} by \texttt{(S m0)}. +\example{Using \texorpdfstring{\texttt{inversion\_sigma}}{inversion\_sigma}} + +Let us consider the following inductive type of length-indexed lists, +and a lemma about inverting equality of \texttt{cons}: + +\begin{coq_eval} +Reset Initial. +Set Printing Compact Contexts. +\end{coq_eval} + +\begin{coq_example*} +Require Coq.Logic.Eqdep_dec. + +Inductive vec A : nat -> Type := +| nil : vec A O +| cons {n} (x : A) (xs : vec A n) : vec A (S n). + +Lemma invert_cons : forall A n x xs y ys, + @cons A n x xs = @cons A n y ys + -> xs = ys. +Proof. +\end{coq_example*} + +\begin{coq_example} +intros A n x xs y ys H. +\end{coq_example} + +After performing \texttt{inversion}, we are left with an equality of +\texttt{existT}s: + +\begin{coq_example} +inversion H. +\end{coq_example} + +We can turn this equality into a usable form with +\texttt{inversion\_sigma}: + +\begin{coq_example} +inversion_sigma. +\end{coq_example} + +To finish cleaning up the proof, we will need to use the fact that +that all proofs of \texttt{n = n} for \texttt{n} a \texttt{nat} are +\texttt{eq\_refl}: + +\begin{coq_example} +let H := match goal with H : n = n |- _ => H end in +pose proof (Eqdep_dec.UIP_refl_nat _ H); subst H. +simpl in *. +\end{coq_example} + +Finally, we can finish the proof: + +\begin{coq_example} +assumption. +Qed. +\end{coq_example} + \subsection{\tt fix {\ident} {\num}} \tacindex{fix} \label{tactic:fix} @@ -2961,7 +3071,7 @@ activated, {\tt subst} also deals with the following corner cases: \item The presence of a recursive equation which without the option would be a cause of failure of {\tt subst}. - + \item A context with cyclic dependencies as with hypotheses {\tt \ident$_1$ = f~\ident$_2$} and {\tt \ident$_2$ = g~\ident$_1$} which without the option would be a cause of failure of {\tt subst}. @@ -3256,7 +3366,7 @@ a sort of strong normalization with two key differences: \begin{itemize} \item They unfold a constant if and only if it leads to a $\iota$-reduction, i.e. reducing a match or unfolding a fixpoint. -\item While reducing a constant unfolding to (co)fixpoints, +\item While reducing a constant unfolding to (co)fixpoints, the tactics use the name of the constant the (co)fixpoint comes from instead of the (co)fixpoint definition in recursive calls. @@ -3375,6 +3485,7 @@ reduced to \texttt{S t}. \optindex{Refolding Reduction} {\tt Refolding Reduction} \end{quote} +\emph{Deprecated since 8.7} This option (off by default) controls the use of the refolding strategy of {\tt cbn} while doing reductions in unification, type inference and @@ -3987,7 +4098,7 @@ Abort. & & e * & \text{ Kleene star } \\ & & \texttt{emp} & \text{ empty } \\ & & \texttt{eps} & \text{ epsilon } \\ - & & \texttt{(} e \texttt{)} & + & & \texttt{(} e \texttt{)} & \end{array}\] The \texttt{emp} regexp does not match any search path while @@ -5151,7 +5262,7 @@ Reset Initial. \subsection[\tt swap \num$_1$ \num$_2$]{\tt swap \num$_1$ \num$_2$\tacindex{swap}} -This tactic switches the position of the goals of indices $\num_1$ and $\num_2$. If either $\num_1$ or $\num_2$ is negative then goals are counted from the end of the focused goal list. Goals are indexed from $1$, there is no goal with position $0$. +This tactic switches the position of the goals of indices $\num_1$ and $\num_2$. If either $\num_1$ or $\num_2$ is negative then goals are counted from the end of the focused goal list. Goals are indexed from $1$, there is no goal with position $0$. \Example \begin{coq_example*} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 08cdbee503..768d0df763 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -60,7 +60,7 @@ subdirectory of the sources. The majority of \Coq\ projects are very similar: a collection of {\tt .v} files and eventually some {\tt .ml} ones (a \Coq\ plugin). The main piece -of metadata needed in order to build the project are the command +of metadata needed in order to build the project are the command line options to {\tt coqc} (e.g. {\tt -R, -I}, \SeeAlso Section~\ref{coqoptions}). Collecting the list of files and options is the job of the {\tt \_CoqProject} file. @@ -98,7 +98,7 @@ Such command generates the following files: An optional file {\bf {\tt CoqMakefile.local}} can be provided by the user in order to extend {\tt CoqMakefile}. In particular one can declare custom actions to be performed before or after the build process. Similarly one can customize the install target or even provide new targets. Extension points are documented in the {\tt CoqMakefile} file. The extensions of the files listed in {\tt \_CoqProject} is -used in order to decide how to build them In particular: +used in order to decide how to build them. In particular: \begin{itemize} \item {\Coq} files must use the \texttt{.v} extension @@ -108,12 +108,171 @@ used in order to decide how to build them In particular: \end{itemize} The use of \texttt{.mlpack} files has to be preferred over \texttt{.mllib} -files, since it results in a ``packed'' plugin: All auxiliary +files, since it results in a ``packed'' plugin: All auxiliary modules (as {\tt Baz} and {\tt Bazaux}) are hidden inside the plugin's ``name space'' ({\tt Qux\_plugin}). This reduces the chances of begin unable to load two distinct plugins because of a clash in their auxiliary module names. +\paragraph{Timing targets and performance testing} +The generated \texttt{Makefile} supports the generation of two kinds +of timing data: per-file build-times, and per-line times for an +individual file. + +The following targets and \texttt{Makefile} variables allow collection +of per-file timing data: +\begin{itemize} +\item \texttt{TIMED=1} --- passing this variable will cause + \texttt{make} to emit a line describing the user-space build-time + and peak memory usage for each file built. + + \texttt{Note}: On Mac OS, this works best if you've installed + \texttt{gnu-time}. + + \texttt{Example}: For example, the output of \texttt{make TIMED=1} + may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.34 mem: 395448 ko) +COQC Fast.v +Fast (user: 0.01 mem: 45184 ko) +\end{verbatim} +\item \texttt{pretty-timed} --- this target stores the output of + \texttt{make TIMED=1} into \texttt{time-of-build.log}, and displays + a table of the times, sorted from slowest to fastest, which is also + stored in \texttt{time-of-build-pretty.log}. If you want to + construct the log for targets other than the default one, you can + pass them via the variable \texttt{TGTS}, e.g., \texttt{make + pretty-timed TGTS="a.vo b.vo"}. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: This target will \emph{append} to the timing log; if + you want a fresh start, you must remove the file + \texttt{time-of-build.log} or run \texttt{make cleanall}. + + \texttt{Example}: For example, the output of \texttt{make + pretty-timed} may look like this: +\begin{verbatim} +COQDEP Fast.v +COQDEP Slow.v +COQC Slow.v +Slow (user: 0.36 mem: 393912 ko) +COQC Fast.v +Fast (user: 0.05 mem: 45992 ko) +Time | File Name +-------------------- +0m00.41s | Total +-------------------- +0m00.36s | Slow +0m00.05s | Fast +\end{verbatim} +\item \texttt{print-pretty-timed-diff} --- this target builds a table + of timing changes between two compilations; run \texttt{make + make-pretty-timed-before} to build the log of the ``before'' + times, and run \texttt{make make-pretty-timed-after} to build the + log of the ``after'' times. The table is printed on the command + line, and stored in \texttt{time-of-build-both.log}. This target is + most useful for profiling the difference between two commits to a + repo. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Note}: The \texttt{make-pretty-timed-before} and + \texttt{make-pretty-timed-after} targets will \emph{append} to the + timing log; if you want a fresh start, you must remove the files + \texttt{time-of-build-before.log} and + \texttt{time-of-build-after.log} or run \texttt{make cleanall} + \emph{before} building either the ``before'' or ``after'' targets. + + \texttt{Note}: The table will be sorted first by absolute time + differences rounded towards zero to a whole-number of seconds, then + by times in the ``after'' column, and finally lexicographically by + file name. This will put the biggest changes in either direction + first, and will prefer sorting by build-time over subsecond changes + in build time (which are frequently noise); lexicographic sorting + forces an order on files which take effectively no time to compile. + + \texttt{Example}: For example, the output table from \texttt{make + print-pretty-timed-diff} may look like this: +\begin{verbatim} +After | File Name | Before || Change | % Change +-------------------------------------------------------- +0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% +-------------------------------------------------------- +0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% +0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% +\end{verbatim} +\end{itemize} + +The following targets and \texttt{Makefile} variables allow collection +of per-line timing data: +\begin{itemize} +\item \texttt{TIMING=1} --- passing this variable will cause + \texttt{make} to use \texttt{coqc -time} to write to a + \texttt{.v.timing} file for each \texttt{.v} file compiled, which + contains line-by-line timing information. + + \texttt{Example}: For example, running \texttt{make all TIMING=1} may + result in a file like this: +\begin{verbatim} +Chars 0 - 26 [Require~Coq.ZArith.BinInt.] 0.157 secs (0.128u,0.028s) +Chars 27 - 68 [Declare~Reduction~comp~:=~vm_c...] 0. secs (0.u,0.s) +Chars 69 - 162 [Definition~foo0~:=~Eval~comp~i...] 0.153 secs (0.136u,0.019s) +Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] 0.239 secs (0.236u,0.s) +\end{verbatim} + +\item \texttt{print-pretty-single-time-diff + BEFORE=path/to/file.v.before-timing + AFTER=path/to/file.v.after-timing} --- this target will make a + sorted table of the per-line timing differences between the timing + logs in the \texttt{BEFORE} and \texttt{AFTER} files, display it, + and save it to the file specified by the + \texttt{TIME\_OF\_PRETTY\_BUILD\_FILE} variable, which defaults to + \texttt{time-of-build-pretty.log}. + + To generate the \texttt{.v.before-timing} or + \texttt{.v.after-timing} files, you should pass + \texttt{TIMING=before} or \texttt{TIMING=after} rather than + \texttt{TIMING=1}. + + \texttt{Note}: The sorting used here is the same as in the + \texttt{print-pretty-timed-diff} target. + + \texttt{Note}: This target requires \texttt{python} to build the table. + + \texttt{Example}: For example, running + \texttt{print-pretty-single-time-diff} might give a table like this: +\begin{verbatim} +After | Code | Before || Change | % Change +--------------------------------------------------------------------------------------------------- +0m00.50s | Total | 0m04.17s || -0m03.66s | -87.96% +--------------------------------------------------------------------------------------------------- +0m00.145s | Chars 069 - 162 [Definition~foo0~:=~Eval~comp~i...] | 0m00.192s || -0m00.04s | -24.47% +0m00.126s | Chars 000 - 026 [Require~Coq.ZArith.BinInt.] | 0m00.143s || -0m00.01s | -11.88% + N/A | Chars 027 - 068 [Declare~Reduction~comp~:=~nati...] | 0m00.s || +0m00.00s | N/A +0m00.s | Chars 027 - 068 [Declare~Reduction~comp~:=~vm_c...] | N/A || +0m00.00s | N/A +0m00.231s | Chars 163 - 208 [Definition~foo1~:=~Eval~comp~i...] | 0m03.836s || -0m03.60s | -93.97% +\end{verbatim} + +\item \texttt{all.timing.diff}, \texttt{path/to/file.v.timing.diff} + --- The \texttt{path/to/file.v.timing.diff} target will make a + \texttt{.v.timing.diff} file for the corresponding \texttt{.v} file, + with a table as would be generated by the + \texttt{print-pretty-single-time-diff} target; it depends on having + already made the corresponding \texttt{.v.before-timing} and + \texttt{.v.after-timing} files, which can be made by passing + \texttt{TIMING=before} and \texttt{TIMING=after}. The + \texttt{all.timing.diff} target will make such timing difference + files for all of the \texttt{.v} files that the \texttt{Makefile} + knows about. It will fail if some \texttt{.v.before-timing} or + \texttt{.v.after-timing} files don't exist. + + \texttt{Note}: This target requires \texttt{python} to build the table. +\end{itemize} + \paragraph{Notes about including the generated Makefile} This practice is discouraged. The contents of this file, including variable names @@ -121,6 +280,43 @@ and status of rules shall change in the future. Users are advised to include {\tt Makefile.conf} or call a target of the generated Makefile as in {\tt make -f Makefile target} from another Makefile. +One way to get access to all targets of the generated +\texttt{CoqMakefile} is to have a generic target for invoking unknown +targets. For example: +\begin{verbatim} +# KNOWNTARGETS will not be passed along to CoqMakefile +KNOWNTARGETS := CoqMakefile extra-stuff extra-stuff2 +# KNOWNFILES will not get implicit targets from the final rule, and so +# depending on them won't invoke the submake +# Warning: These files get declared as PHONY, so any targets depending +# on them always get rebuilt +KNOWNFILES := Makefile _CoqProject + +.DEFAULT_GOAL := invoke-coqmakefile + +CoqMakefile: Makefile _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o CoqMakefile + +invoke-coqmakefile: CoqMakefile + $(MAKE) --no-print-directory -f CoqMakefile $(filter-out $(KNOWNTARGETS),$(MAKECMDGOALS)) + +.PHONY: invoke-coqmakefile $(KNOWNFILES) + +#################################################################### +#################################################################### +#################################################################### +#################################################################### +## Your targets here ## +#################################################################### +#################################################################### +#################################################################### +#################################################################### + +# This should be the last rule, to handle any targets not declared above +%: invoke-coqmakefile + @true +\end{verbatim} + \paragraph{Notes for users of {\tt coq\_makefile} with version $<$ 8.7} \begin{itemize} @@ -128,7 +324,7 @@ as in {\tt make -f Makefile target} from another Makefile. or after the build (like invoking make on a subdirectory) one can hook in {\tt pre-all} and {\tt post-all} extension points \item \texttt{-extra-phony} and \texttt{-extra} are deprecated. To provide - additional target ({\tt .PHONY} or not) please use + additional target ({\tt .PHONY} or not) please use {\tt CoqMakefile.local} \end{itemize} diff --git a/doc/refman/Universes.tex b/doc/refman/Universes.tex index 36518e6fae..2bb1301c79 100644 --- a/doc/refman/Universes.tex +++ b/doc/refman/Universes.tex @@ -131,6 +131,52 @@ producing global universe constraints, one can use the polymorphically, not at a single instance. \end{itemize} +\asection{{\tt Cumulative, NonCumulative}} +\comindex{Cumulative} +\comindex{NonCumulative} +\optindex{Inductive Cumulativity} + +Inductive types, coinductive types, variants and records can be +declared cumulative using the \texttt{Cumulative}. Alternatively, +there is an option \texttt{Set Inductive Cumulativity} which when set, +makes all subsequent inductive definitions cumulative. Consider the examples below. +\begin{coq_example*} +Polymorphic Cumulative Inductive list {A : Type} := +| nil : list +| cons : A -> list -> list. +\end{coq_example*} +\begin{coq_example} +Print list. +\end{coq_example} +When printing \texttt{list}, the part of the output of the form +\texttt{$\mathtt{\sim}$@\{i\} <= $\mathtt{\sim}$@\{j\} iff } +indicates the universe constraints in order to have the subtyping +$\WTEGLECONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ +(for fully applied instances of \texttt{list}) whenever $\WTEGCONV{A}{B}$. +In the case of \texttt{list} there is no constraint! +This also means that any two instances of \texttt{list} are convertible: +$\WTEGCONV{\mathtt{list@\{i\}} A}{\mathtt{list@\{j\}} B}$ whenever $\WTEGCONV{A}{B}$ and +furthermore their corresponding (when fully applied to convertible arguments) constructors. +See Chapter~\ref{Cic} for more details on convertibility and subtyping. +Also notice the subtyping constraints for the \emph{non-cumulative} version of list: +\begin{coq_example*} +Polymorphic NonCumulative Inductive list' {A : Type} := +| nil' : list' +| cons' : A -> list' -> list'. +\end{coq_example*} +\begin{coq_example} +Print list'. +\end{coq_example} +The following is an example of a record with non-trivial subtyping relation: +\begin{coq_example*} +Polymorphic Cumulative Record packType := {pk : Type}. +\end{coq_example*} +\begin{coq_example} +Print packType. +\end{coq_example} +Notice that as expected, \texttt{packType@\{i\}} and \texttt{packType@\{j\}} are convertible if and only if \texttt{i $=$ j}. + + \asection{Global and local universes} Each universe is declared in a global or local environment before it can |