\documentclass[11pt]{article} \usepackage[latin1]{inputenc} \usepackage[T1]{fontenc} \input{./title} \input{./macros} \begin{document} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Changes 6.2 ===> 6.3 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \shorttitle{Changes from {\Coq} V6.2 to {\Coq} V6.3} This document describes the main differences between Coq V6.2 and V6.3. This new version of Coq is characterized by new tactics and a more flexible guard condition in fixpoints definitions. We refer to the reference manual for a more precise description of the new features. %See the ASCII file \texttt{CHANGES} available by FTP with \Coq\ for %the minor changes of the bug-fix releases 6.2.1 and 6.2.2. \section{Changes overview} \subsection{New Tactics} \begin{itemize} \item The \texttt{AutoRewrite} tactic uses a set of theorems as rewrite rules that are applied sequentially in order to solve the goal. This tactic is still experimental and subject to changes. \item \texttt{First} and \texttt{Solve} are two tacticals which apply to a sequence of tactics written \texttt{[ \textit{tac}$_1$ | ... | \textit{tac}$_n$ ]}. \texttt{First} applies the first tactic in the given list which does not fail while \texttt{Solve} applies the first tactic in the list which completely solves the goal. \item \texttt{Quote} this new tactic does automatic inversion of interpretation function for people using Barengregt's so-called `2-level approach'. See examples in \texttt{theories/DEMOS/DemoQuote.v}. \item \texttt{Change} \textit{term} \texttt{in} \textit{hyp} is now available. \item \texttt{Move} \textit{hyp} \texttt{after} \textit{hyp} allows to reorder the hypotheses of the local context. \end{itemize} \subsection{Changes in existing tactics} \begin{itemize} \item \texttt{Intro} or \texttt{Intros} with explicit names will force an head reduction of the goal in case it does not start with a product. \\ \texttt{Intro} or \texttt{Intros} without explicit names generate automatically names for the hypothesis or variable to be introduced. The algorithm to generate these names has been slightly changed, this may be a source of incompatibility in the proofs script. The new variant \texttt{Intro \textit{ident} after \textit{hyp}} allows to tell the place where an hypothesis is introduced in the context. \item \texttt{Auto} the structure of the hints databases for the Auto tactic was changed in version V6.2.3. In version V6.3, the following new features were added to Auto~: \begin{itemize} \item \texttt{Print} \textit{HintDbname} prints out the contents of a the hint database \textit{HintDbname}; \item \texttt{Constructors} \textit{Indname} is a new hint tactic which is equivalent to introduce the \texttt{Resolve} hint tactic for each constructor of the \textit{Indname} inductive definition. \end{itemize} \item \texttt{Induction} \textit{var} now also performs induction on a variable \textit{var} of the local context. This extension is more ``user-friendly'' in the sense it generalizes automatically above the other hypotheses dependent on the original variable. It does not duplicate any longer the name of the variable to which it applies. It should avantageously replaces "Elim" on an hypothesis/variable or a typical sequence "Generalize" followed by "Induction" on the generalized variable. But this extension is experimental and susceptible of change in next releases. \item \texttt{Let} \textit{ident} \texttt{:=} \textit{term} \texttt{in} \textit{occurlist} \textit{hyps} replaces the given occurrences of \texttt{term} in the hypotheses \textit{hyps} (or in the goal) by the variable \textit{ident} and keep the equality \textit{ident=term} in the context. This is actually a variant of \texttt{Generalize} which keeps track of the original term. As the new \texttt{Induction} to which it can be combined, it is susceptible of change in next releases. \item The \texttt{Ring} tactic has been extended and works now also when the ring is in the \Type{} sort. \item The tactic \texttt{Correctness} has been improved. \end{itemize} \subsection{New toplevel commands} \begin{description} \item[\texttt{Time}] Any vernacular command (including invocation of tactics) can be prefixed by the word \texttt{Time}; then the time spent is printed after having executed the command. For example : \texttt{Time Save.} or \texttt{Time Omega.} \item[\texttt{Focus} $n$] It is now possible to focus on a specific goal using the command \texttt{Focus} $n$, with $n$ being the range of the selected subgoal. All the tactics will be applied to this goal and only the subgoals inherited from the selected goal are displayed. When the subgoal is completed, the message \texttt{"Subtree proved"} is printed out then the focus goes back to the initial goal and the corresponding remaining subgoals are printed out. The focus commands are reseted by the \texttt{Undo} command or \texttt{Unfocus}. \texttt{Focus} without argument keeps its old meaning to only disply the first subgoal. \item[Evaluation in Definition] It is now possible to apply a reduction function to a term inside a definition. Just replace the term to be defined by \[ \texttt{Eval}~ \textit{reduction-function}~ \texttt{in}~ \textit{term}\] at the right hand side of the \texttt{:=} sign in a definition. \end{description} \subsection{Language extensions} \begin{description} \item[Type reconstruction] The algorithm to solve incomplete information in terms has been improved. In particular question marks can be put in place of the type of universally quantified variables. \item[Guarded fixpoints] The condition for well-formed fixpoints has been extended, it is now possible to define structural fixpoints for positive inductive definitions with nested recursion (like \texttt{Inductive term : Set := cons : (list term)->term}) \end{description} \subsection{Libraries} \begin{description} \item[Reals] The library of real numbers has been extended and obeys to the same naming convention than ARITH and ZARITH: addition is \texttt{Rplus}, theorems stating commutativity are postfixed by \texttt{\_sym} like \texttt{plus\_sym}, \texttt{Rmult\_sym}, etc. The tactic \texttt{Ring} has been instantiated on the reals; one can use it to normalize polynomial expressions over the reals. The library \texttt{Reals} has been completed by a definition of limit, derivative and by others properties and functions. \end{description} \subsection{Documentation} The documentation includes now an index of errors. \section{Incompatibilities} You could have to modify your vernacular source for the following reasons: \begin{itemize} \item Some names of variables have changed. Typically, a sequence "Generalize n; Induction n" should become a "Generalize n; Induction n0", or better, simply "Induction n" since Induction now works with hypotheses of the context and generalizes automatically. \item In the library ZArith, "Zinv" has been renamed as "Zopp", in order to be coherent with the Reals library. Theorems whose name includes "Zinv" have been renamed too. A global search-and-replace of "Zinv" by "Zopp" should be sufficient to update user's developments. \item In the library Reals, some names has been changed. In the file README of the library, there is a script which can be used to update user's developments. \item The definition of Exists has changed in LISTS/Streams. \end{itemize} \section{New contributions} We integrated new contributions : \begin{description} \item[Finite sets and graphs] This contribution is due to J. Goubault-Larrecq from Dyade (INRIA-Bull). It contains a development of finite sets implemented efficiently as trees indexed by binary numbers. This representation is used to implement graphs corresponding to arithmetic formulas and prove the correctness of a decision procedure testing the satisfiability of formula by detecting cycles of positive weigth in the graph \item[$\pi$-calculus] A development of $\pi$-calculus due to I. Scagnetto from University of Udine. \item[The three gap theorem] A Proof of the Three Gap Theorem (Steinhaus Conjecture) by M. Mayero from INRIA Rocquencourt. \item[Floating point numbers] An axiomatisation of the IEEE 754 norm for Floating point numbers done by P. Loiseleur fron LRI Orsay. \item[Algebra] Basic notions of algebra designed by L. Pottier from INRIA Sophia-Antipolis. \item[Heapsort] A proof of an imperative version of the Heapsort sorting algorithm developed by J-C. Filli\^atre from LRI Orsay. \end{description} \section{Installation procedure} \subsection{Uninstalling Coq} \paragraph{Warning} It is strongly recommended to clean-up the V6.2 Coq library directory before you install the new version. Use the option to coqtop \texttt{-uninstall} that will remove the binaries and the library files of Coq V6.2 on a Unix system. \subsection{OS Issues -- Requirements} \subsubsection{Unix users} You need Objective Caml version 2.01 or 2.02, and the corresponding Camlp4 version to compile the system. Both are available by anonymous ftp at: \\ \verb|ftp://ftp.inria.fr/Projects/Cristal|. \bigskip \noindent Binary distributions are available for the following architectures: \bigskip \begin{tabular}{l|c|r} {\bf OS } & {\bf Processor} & {name of the package}\\ \hline Linux & 80386 and higher & coq-6.3-linux-i386.tar.gz \\ Solaris & Sparc & coq-6.3-solaris-sparc.tar.gz\\ Digital & Alpha & coq-6.3-OSF1.tar.gz\\ \end{tabular} \bigskip If your configuration is in the above list, you don't need to install Caml and Camlp4 and to compile the system: just download the package and install the binaries in the right place. \subsubsection{MS Windows users} A binary distribution is available for PC under MS Windows 95/98/NT. The package is named coq-6.3-win.zip. For installation information see the files INSTALL.win and README.win. %users will get the 6.2 version at the same time than %Unix users ! %A binary distribution is available for Windows 95/NT. Windows 3.1 %users may run the binaries if they install the Win32s module, freely %available at \verb|ftp.inria.fr|. \section{Credits} B. Barras extended the unification algorithm to complete partial terms and solved various tricky bugs related to universes.\\ D. Delahaye developed the \texttt{AutoRewrite} tactic. He also designed the new behavior of \texttt{Intro} and provided the tacticals \texttt{First} and \texttt{Solve}.\\ J.-C. Filli\^atre developed the \texttt{Correctness} tactic.\\ E. Gim\'enez extended the guard condition in fixpoints.\\ H. Herbelin designed the new syntax for definitions and extended the \texttt{Induction} tactic.\\ P. Loiseleur developed the \texttt{Quote} tactic and the new design of the \texttt{Auto} tactic, he also introduced the index of errors in the documentation.\\ C. Paulin wrote the \texttt{Focus} command and introduced the reduction functions in definitions, this last feature was proposed by J.-F. Monin from CNET Lannion. \end{document} % Local Variables: % mode: LaTeX % TeX-master: t % End: % $Id$