path: root/doc/ChangesV6-3.tex

\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$