diff options
Diffstat (limited to 'doc/refman')
| -rw-r--r-- | doc/refman/Classes.tex | 6 | ||||
| -rw-r--r-- | doc/refman/Program.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 18 | ||||
| -rw-r--r-- | doc/refman/RefMan-ind.tex | 510 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-uti.tex | 165 |
7 files changed, 180 insertions, 526 deletions
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex index 5966ac468c..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 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-ext.tex b/doc/refman/RefMan-ext.tex index f338c30551..713f344cbe 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -705,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} @@ -749,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. @@ -776,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: @@ -848,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} 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 f3bc2dd05e..3ce1d4ecd8 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -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-tac.tex b/doc/refman/RefMan-tac.tex index ecb89b5fb8..a23c432322 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3485,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 diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index fee4de3364..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. @@ -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 @@ -165,7 +324,7 @@ invoke-coqmakefile: CoqMakefile 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} |