path: root/doc/ChangesV6-2.tex

\documentclass[11pt]{article}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}

\input{./title}
\input{./macros}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Changes 6.1 ===> 6.2
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\coverpage{Changes from {\Coq} V6.1 to {\Coq} V6.2}{\ }

This document describes the main differences between Coq V6.1 and
V6.2.  This new version of Coq is characterized by an acceleration of
parsing, loading and reduction, by a more user-friendly syntax, and by
new tactics and management tools.  
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}

\begin{itemize}

\item \textbf{Syntax}

\begin{description}

  \item[New syntax for defining parsing and pretty-printing rules.]{\ 

  The \texttt{Grammar} and
    \texttt{Syntax} declarations are more readable and more symmetric.}

  \item[\texttt{Cases} vs \texttt{Case}]{\ 

   The constructions defined by cases are
    now printed with the ML-style \texttt{Cases} syntax. The
    \texttt{Case} syntax should no longer be used.}

  \item[New syntax for the existential and universal quantifiers.]{\ 

   \texttt{(EX x:A | P)}, \texttt{(EX x| P)}, \texttt{(EX x:A | P \&
   Q)}, \texttt{(EX x | P \& Q)},
   \texttt{(ALL x:A | P)} and 
   \texttt{(ALL x | P)} are alternative
    syntax for \texttt{(Ex [x:A]P)},  \texttt{(Ex2 [x:A]P [x:A]Q)}
    and  \texttt{(All [x:A]P)}, the syntax \texttt{<A>Ex(P),
    <A>Ex(P,Q)} and \texttt{<A>All(P)} are no longer supported.}

  \item[Natural syntax for the ... naturals.]{\ 

   With the {\tt Arith} theory, you can
    now type \texttt{(3)} for \texttt{(S (S (S O)))}}.

  \item[Natural syntax for expressions of integer arithmetic.]{\ 

   With the {\tt ZArith} theory, you can
    type e.g. \texttt{`3 <= x - 4 < 7`}.}
  
\end{description}

\item \textbf{Tactics}

  \begin{itemize}

  \item New mechanism to define parameterized tactics (see
  section~\ref{parameterised}).

  \item New tactic \texttt{Decompose} to decompose a
  complex proposition in atomic ones (see
  section~\ref{decompose}).

  \item New tactics \texttt{Decide Equality} and 
  \texttt{Compare} for deciding the equality of two
  inductive objects. 

  \item \texttt{Intros} has been extended such that it takes arguments
  denoting patterns and accordingly to this patterns, performs decomposition of arguments ranging
  over inductive definitions as well as introduction (see section~\ref{intros}).
  
  \item \texttt{Tauto} is extended to
  work also on connectives defined by the user and on informative
  types (see section~\ref{tauto}).

  \item The {\bf equality} tactics, especially \texttt{Rewrite},
  \texttt{Transitivity}, \texttt{Symmetry} and \texttt{Reflexivity},
  works now independently of the universe that the equality
  inhabits (see section~\ref{equality}).

  \item New experimental tactic \texttt{Refine}: a kind of
    \texttt{exact} with typed holes that are transformed into
    subgoals (see
  section~\ref{refine}).

  \item The tactical \texttt{Abstract} allow to automatically 
    divide a big proof into smaller lemmas. It may improve the
    efficiency of the \texttt{Save} procedure (see section~\ref{abstract}).

  \item The tactics \texttt{Rewrite} and \texttt{Rewrite in} now
    accept bindings as tactics \texttt{Apply} and \texttt{Elim}.

  \item The tactic \texttt{Rewrite} now fails when no rewriting can be
    done. So you must use \texttt{Try Rewrite} to get the old behavior.

  \end{itemize}

\item \textbf{New toplevel commands.}

  \begin{description}

  \item[Precise location of errors.]{\ 

  At toplevel, when possible, \Coq\
    underlines the portion of erroneous vernac source. When compiling,
    it tells the line and characters where the error took place. The
    output is compatible with the \texttt{next-error} mechanism of GNU
    Emacs.}

  \item[New reduction functions.]{\ 
  A more precise control on what is reduced is now
    possible in tactics. All toplevel reductions are performed through the
    \texttt{Eval} command. The commands \texttt{Compute} and
    \texttt{Simplify} do not exist any longer, they are replaced by
    the commands \texttt{Eval Compute in} and \texttt{Eval Simpl in}. 
    In addition,
    \texttt{Eval} now takes into consideration the hypotheses of the
    current goal in order to type-check the term to be reduced 
    (see section~\ref{reductions}).}

  \end{description}

\item \textbf{Libraries}

  \begin{description}

  \item[Arithmetic on Z.]{\ 

  Pierre Cr\'egut's arithmetical library on integers (the set Z) is now
    integrated to the standard library. 
  \texttt{ZArith} contains basic
   definitions, theorems, and syntax rules that allow users of \texttt{ZArith}
   to write formulas such as $3+(x*y) < z \le 3+(x*y+1)$ in the
   natural way~(see section~\ref{zarith}).
  }

  \item[\texttt{SearchIsos} : a tool to search through the standard library]{

   The \texttt{SearchIsos} tool se\-arches terms by their
        types and modulo type isomorphisms. There are two ways to use
        \texttt{SearchIsos}:

    \begin{itemize} 
    \item Search a theorem in the current environment with the new
    \texttt{SearchIsos} command in an interactive session
    \item Search a theorem in the whole Library using the external tool
    \texttt{coqtop -searchisos} 
    \end{itemize} }

  \item The \texttt{Locate} vernac command can now locate the
    module in which a term is defined in a \texttt{coqtop} session. You can
    also ask for the exact location of a file or a module that lies
    somewhere in the load path.

\end{description}

\item \textbf{Extraction}

  \begin{description}

  \item Extraction to Haskell available

  \end{description}

\item \textbf{Improved Coq efficiency}

  \begin{description}

  \item[Parsing]

 Thanks to a new grammar implementation based on Daniel de
  Rauglaudre's Camlp4 system, parsing is now several times faster. The
  report of syntax errors is more precise.

  \item[Cleaning up the tactics source]{\ 

  Source code of the tactics has been revisited, so that the user can
    implement his/her own tactics more easily. The internal ML names
    for tactics have been normalized, and they are organized in
    different files. See chapter ``Writing your own tactics'' in the
    Coq reference manual.}

  \end{description}

\item \textbf{Incompatibilities}

  You could have to modify your vernacular source for the following
  reasons:

  \begin{itemize}
 
  \item You use the name \texttt{Sum} which is now a keyword.
  \item You use the syntax \texttt{<A>Ex(P)}, \texttt{<A>Ex2(P,Q)} or 
        \texttt{<A>All(P)}. 

  \item You use Coq \texttt{Grammar} or \texttt{Syntax} commands. 
  In this case, see section
  \ref{parsing-printing} to know how to modify your parsing or printing
  rules.

  \item You use Coq \texttt{Call} to apply a tactic abbreviation
    declared using \texttt{Tactic Definition}. These tactics can be
    directly called, just remove the \texttt{Call} prefix.

  \item \texttt{Require} semantics. The Coq V6.1 \texttt{Require}
    command did not behave as described in the reference manual. 
    It has been corrected.\\
    The Coq V6.2 behavior is now the following.
    Assume a file \texttt{A} containing a
    command \texttt{Require B} is compiled. Then the command
    \texttt{Require A} loads the module \texttt{B} but the definitions
    in \texttt{B} are not visible. In order to see theses definitions,
    a further \texttt{Require B} is
    needed or you should write \texttt{Require Export B} instead of 
    \texttt{Require B} inside the file \texttt{A}. \\
    The Coq V6.1 behavior of \texttt{Require} was equivalent to the
    Coq V6.2 \texttt{Require Export} command.
   \item \texttt{Print Hint} now works only in proof mode and displays
     the hints that apply to the current goal. \texttt{Print Hint *}
     works as the old \texttt{Print Hint} command and displays  the complete
     hints table.

  \end{itemize}

  In addition, it is strongly recommended to use now the {\tt Cases}
  pattern-matching operator rather than the intended to disappear {\tt
  Case} operator.

\item \textbf{Documentation}
 The Reference Manual has been rearranged and
  updated. The chapters on syntactic extensions, and user-defined
  tactics have been completely rewritten.

  \begin{itemize}
  \item We made a big effort to make the Reference Manual better and
    more precise. The paper documentation is now divided in three
    parts:
    \begin{enumerate}
    \item The Reference Manual, that documents the language (part I), 
      a brief explanation of each command and tactic (part II), the
      users extensions for syntax and tactics (part III), the tools
      (part IV);

    \item The Addendum to Reference Manual (part V), that contains
      more detailed explanations about extraction, printing proofs in
      natural language, tactics such as Omega, Ring and Program,
      coercions and Cases compilation.

    \item The Tutorial, an introduction to Coq for the new user, that
      has not much changed
    \end{enumerate}

  \item The Hyper-Text documentation has been much improved. Please
    check our web page \verb!http://pauillac.inria.fr/coq!. It is
    possible to perform searches in the standard Library by name or by
    type (with SearchIsos), and of course to read the HTML version
    of the documentation.
  \end{itemize}

\end{itemize}

\section{New tactics}


\subsection{Proof of imperative programs}

A new tactic to establish correctness and termination of imperative
(and functional) programs is now available, in the \Coq\ module
\texttt{Programs}. This tactic, called \texttt{Correctness}, is
described in the chapter 18 of the \Coq\ Reference Manual.


\subsection{Defining parameterized tactics}
\label{parameterised}
It is possible to define tactics macros, taking terms as arguments
using the \texttt{Tactic Definition} command. 

These macros can be called directly (in Coq V6.1, a prefix
\texttt{Call} was used).
Example:

\begin{coq_example*}
Tactic Definition DecideEq [$a $b] := 
   [<:tactic:<
      Destruct $a;
      Destruct $b;
      Auto;
      (Left;Discriminate) Orelse (Right;Discriminate)>>].
Inductive Set Color := Blue:Color | White:Color | Red:Color | Black:Color.
\end{coq_example*}

\begin{coq_example}
Theorem eqColor: (c1,c2:Color){c1=c2}+{~c1=c2}.
DecideEq c1 c2.
\end{coq_example}
\begin{coq_example*}
Qed.
\end{coq_example*}

\subsection{Intros}\label{intros}
The tactic \texttt{Intros} can now take a pattern as argument. A
pattern is either 
\begin{itemize}
\item a variable
\item a list of patterns : $p_1~\ldots~p_n$
\item a disjunction of patterns : $[p_1~|~~\ldots~|~p_n]$
\item a conjunction of patterns : $(p_1,\ldots,p_n)$
\end{itemize}

The behavior of \texttt{Intros} is defined inductively over the
structure of the pattern given as argument:
\begin{itemize}
\item introduction on a variable behaves like before; 
\item introduction over a
list of patterns $p_1~\ldots~p_n$ is equivalent to the sequence of
introductions over the patterns namely :
\texttt{Intros $p_1$;\ldots; Intros $p_n$}, the goal should start with
at least $n$ products;
\item introduction over a
disjunction of patterns $[p_1~|~~\ldots~|~p_n]$, it 
introduces a new variable $X$, its type should be an inductive definition with $n$
constructors, then it performs a case analysis over $X$ 
(which generates $n$ subgoals), it 
clears $X$ and performs on each generated subgoals the corresponding
\texttt{Intros}~$p_i$ tactic;
\item introduction over a 
conjunction  of patterns $(p_1,\ldots,p_n)$, it
introduces a new variable $X$, its type should be an inductive definition with $1$
constructor with (at least) $n$ arguments, then it performs a case analysis over $X$ 
(which generates $1$ subgoal with at least $n$ products), it 
clears $X$ and performs an introduction over the list of patterns $p_1~\ldots~p_n$.
\end{itemize}
\begin{coq_example}
Lemma intros_test : (A,B,C:Prop)(A\/(B/\C))->(A->C)->C.
Intros A B C [a|(b,c)] f.
Apply (f a).
Proof c.
\end{coq_example}
\subsection{Refine}\label{refine}
This tactics takes a term with holes as argument.

It is still experimental and not automatically loaded. It can
be dynamically loaded if you use the byte-code version of Coq;
with the version in native code, you have to use the \texttt{-full} option.

\Example
\begin{coq_example*}
Require Refine.
Inductive Option: Set := Fail : Option | Ok : bool->Option.
\end{coq_example}
\begin{coq_example}
Definition get: (x:Option)~x=Fail->bool.
Refine
  [x:Option]<[x:Option]~x=Fail->bool>Cases x of
        Fail   =>  ?
      | (Ok b) =>  [_:?]b end.
Intros;Absurd Fail=Fail;Trivial.
\end{coq_example}
\begin{coq_example*}
Defined.
\end{coq_example*}

\subsection{Decompose}\label{decompose}
This tactic allows to recursively decompose a
complex proposition in order to obtain atomic ones.
Example: 

\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Lemma ex1: (A,B,C:Prop)(A/\B/\C \/ B/\C \/ C/\A) -> C.
Intros A B C H; Decompose [and or] H; Assumption.
\end{coq_example}
\begin{coq_example*}
Qed.
\end{coq_example*}


\subsection{Tauto}\label{tauto}
This tactic has been extended to work also on 
connectives defined by the user as well as on informative types.
Example:

\begin{coq_example*}
Inductive AND4   [A:Set;B,C,D:Prop] : Set := 
      tuple4 : A->B->C->D->(AND4 A B C D).
\end{coq_example*} 
\begin{coq_example}
Lemma ex2: (B,C,D:Prop)(AND4 nat B C D)->(AND4 nat C D B).
Tauto.
\end{coq_example}
\begin{coq_example*}
Qed.
\end{coq_example*} 

\subsection{Tactics about Equality}\label{equality}
\texttt{Rewrite}, \texttt{Transitivity}, \texttt{Symmetry},
\texttt{Reflexivity} and other tactics associated to equality predicates work
now independently of the universe that the equality inhabits.
Example:

\begin{coq_example*} 
Inductive EQ [A:Type] : Type->Prop := reflEQ : (EQ A A).
\end{coq_example*} 
\begin{coq_example} 
Lemma sym_EQ: (A,B:Type)(EQ A B)->(EQ B A).
Intros;Symmetry;Assumption.
\end{coq_example} 
\begin{coq_example*} 
Qed.
\end{coq_example*} 

\begin{coq_example} 
Lemma trans_idT: (A,B:Type)(A===Set)->(B===Set)->A===B.
Intros A B X Y;Rewrite X;Symmetry;Assumption.
\end{coq_example} 
\begin{coq_example*} 
Qed.
\end{coq_example*} 


\subsection{The tactical \texttt{Abstract}}~\label{abstract}
From outside, typing \texttt{Abstract \tac} is the same that
typing \tac. If \tac{} completely solves the current goal, it saves an auxiliary lemma called 
{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
current goal and \textit{n} is chosen so that this is a fresh
name. This lemma is a proof of the current goal, generalized over the
local hypotheses.

This tactical is useful with tactics such that \texttt{Omega} and
\texttt{Discriminate} that generate big proof terms. With that tool
the user can avoid the explosion at time of the \texttt{Save} command
without having to cut ``by hand'' the proof in smaller lemmas.

\begin{Variants}
\item \texttt{Abstract {\tac} using {\ident}}. Gives explicitly the
  name of the auxiliary lemma.
\end{Variants}
\begin{coq_example*} 
Lemma abstract_test : (A,B:Prop)A/\B -> A\/B.
\end{coq_example*} 
\begin{coq_example} 
Intros.
Abstract Tauto using sub_proof.
Check sub_proof.
\end{coq_example} 
\begin{coq_example*} 
Qed.
\end{coq_example*} 
\begin{coq_example} 
Print abstract_test.
\end{coq_example} 


\subsection{Conditional $tac$ Rewrite $c$}
This tactics acts as \texttt{Rewrite} and applies a given tactic on the
subgoals corresponding to conditions of the rewriting.
See the Reference Manual for more details.


\section{Changes in concrete syntax}

\subsection{The natural grammar for arithmetic}
\label{zarith}
There is a  new syntax of signed integer arithmetic. However the
syntax delimiters were \verb=[|= and \verb=|]= in the beta-version. In
the final release of 6.2, it's two back-quotes \texttt{`} and \texttt{`}.

Here is an example: 
\begin{coq_eval}
Reset Initial. 
\end{coq_eval}

\begin{coq_example*}
Require ZArith.
Variables x,y,z:Z.
Variables f,g:Z->Z.
\end{coq_example*}
\begin{coq_example}
Check ` 23 + (f x)*45 - 34 `.
Check Zplus_sym.
Check ` x < (g y) <= z+3 `.
Check ` 3+ [if true then ` 4 ` else (f x)] `.
SearchIsos (x,y,z:Z) ` x+(y+z) = (x+y)+z `.
\end{coq_example}

\begin{coq_eval}
Reset x.
\end{coq_eval}

Arithmetic expressions are enclosed between \verb=`= and \verb=`=. It can
be:
\begin{itemize}
\item integers
\item any of the operators \verb|+|, \verb|-| and \verb|*|
\item functional application
\item any of the relations \verb|<|, \verb|<=|, \verb|>=|, \verb|>|,
\verb|=| and \verb|<>|
\end{itemize}

Inside an arithmetic expression, you can type an arbitrary Coq
expression provided it is escaped with \verb|[ ]|. There is also
shortcuts such as $x < y \le z$ which means $x<y \wedge y \le z$.

\begin{coq_example}
Lemma ex3 : (x:Z)` x>0 ` -> ` x <= 2*x <= 4*x `.
Split.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}
\subsection{The new \texttt{Grammar} and \texttt{Syntax}}
\label{parsing-printing}

The leading idea in the {\tt Grammar} and {\tt Syntax} command syntax
changes is to unify and simplify them.

\subsubsection{Syntax changes for \texttt{Grammar} declarations (parsing rules)}

Each \texttt{Grammar} rule now needs to be named, as \texttt{Syntax}
rules do. Although they are just comments, it is advised to use distinct
names for rules.

The syntax of an ordinary grammar rule is now:

\[
\texttt{Grammar}~\textit{GrammarName}~\textit{EntryName}~\texttt{:=}~
 \textit{RuleName}~ \texttt{[} \textit{Pattern}  \texttt{] -> [} \textit{Action}
\texttt{]}.
\]
\paragraph{Parametric rules}

Parametric grammars does not exist any longer. Their main use was to
write left associative rules. For that, there is a simplest way based
on a new grammar builder \texttt{LEFTA} (and grammar builder
\texttt{RIGHTA} and \texttt{NONA} as well).

For instance, the grammar in V6.1 style

\begin{verbatim}
Grammar natural fact :=
  [ final($c) factprod[[$c]]($r) ] -> [$r].

Grammar natural factprod[$p] :=
  [ ] -> [$p]
| [ "*" final($c) factprod[[<<(mult $p $c)>>]]($r)] -> [$r].
\end{verbatim}
should now be written
\begin{verbatim}
Grammar natural fact :=
  LEFTA
    fact_final [ final($c) ] -> [$c]
  | fact_prod  [ final($p) "*" final($c) ] -> [ <<(mult $p $c)>> ].
\end{verbatim}

\subsubsection{Internal abstract syntax tree (ast) changes}

The syntax of internal abstract syntax tree (ast) has also been
modified. Most users, which only uses \verb|<<| ... \verb|>>| in the
right-hand side of the grammar rules are not concerned with that.
For the others, it should be noted that now there are two kinds of
production for grammar rules: ast and lists of asts.

A rule that produces a list of asts should be declared of this type by
inserting ``\texttt{:List}'' just after the grammar name.

The ast constructors \verb!$CONS!, \verb!$NIL!, \verb!$APPEND!,
\verb!$PRIM!, \verb!SOME!  and \verb!$OPER! do not
exist any longer. A simple juxtaposition is used to build ast lists. 
For an empty
list, just put nothing. The old \verb!($OPER{Foo} ($CONS $c1 $c2))!
becomes \verb!(Foo $c1 $c2)!. The old \verb!$SLAML! is now \verb!$SLAM!.

The constructor \verb!$LIST! has a new meaning. It serves to cast an
ast list variable into an ast.

For instance, the following grammar rules in V6.1 style:
\begin{verbatim}
Grammar vernac eqns :=
  [ "|" ne_command_list($ts) "=>" command($u) eqns($es) ]
      -> [($CONS ($OPER{COMMANDLIST} ($CONS $u $ts)) $es)].
| [ ] -> [($LIST)]

with vernac :=
  [ "Foo"  "Definition" identarg($idf) command($c) ":=" eqns($eqs) "." ]
  -> [($OPER{FooDefinition} ($CONS $idf ($CONS $c $eqs)))]
\end{verbatim}
can be written like this in V6.2
\begin{verbatim}
Grammar vernac eqns : List :=
  eqns_cons [ "|" ne_command_list($ts) "=>" command($u) eqns($es) ]
                -> [ (COMMANDLIST $u ($LIST $ts)) ($LIST $es)]
| eqns_nil  [ ] -> [ ].

with vernac :=
  rec_def [ "Foo" "Definition" identarg($idf) command($c) ":=" eqns($eqs) "." ]
   -> [(FooDefinition $idf $c ($LIST $eqs))].
\end{verbatim}


\subsubsection{Syntax changes for \texttt{Syntax} declarations 
  (printing rules)}

The new syntax for printing rules follows the one for parsing rules. In
addition, there are indications of associativity, precedences and
formatting.

Rules are classified by strength: the keyword is \verb-level-. The
non-terminal items are written in a simplest way: a non-terminal
\verb!<$t:dummy-name:*>! is now just written \verb!$t!. For left or
right associativity, the modifiers \verb!:L! or 
 \verb!:E! have to be given as in  \verb!$t:E!. The expression \verb!$t:L! prints the
ast \verb!$t! with a level strictly lower than the current one.
The expression \verb!$t:E! calls the printer with the same level. Thus, for left
associative operators, the left term must be called with \verb!:E!, and the
right one with \verb!:L!. It is the opposite for the right associative
operators. Non associative operators use \verb!:L! for both sub-terms.

For instance, the following rules in V6.1 syntax

\begin{verbatim}
Syntax constr Zplus <<(Zplus $n1 $n2)>> 8
       [<hov 0> "`" <$nn1:"dummy":E> "+" <$n2:"dummy":L> "`" ]
   with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2).

Syntax constr Zminus <<(Zminus $n1 $n2)>> 8
       [<hov 0> "`" <$nn1:"dummy":E> "-" <$n2:"dummy":L> "`" ]
   with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2).

Syntax constr Zmult <<(Zmult $n1 $n2)>> 7
       [<hov 0> "`" <$nn1:"dummy":E> "*" <$n2:"dummy":L> "`" ]
   with $nn1 := (ZEXPR $n1) $nn2 := (ZEXPR $n2).
\end{verbatim}
are now written
\begin{verbatim}
Syntax constr

  level 8:
    Zplus [<<(Zplus $n1 $n2)>>]
      -> [ [<hov 0> "`"(ZEXPR $n1):E "+"(ZEXPR $n2):L "`"] ]
  | Zminus [<<(Zminus $n1 $n2)>>]
      -> [ [<hov 0> "`"(ZEXPR $n1):E "-"(ZEXPR $n2):L "`"] ]
   ;

  level 7:
    Zmult [<<(Zmult $n1 $n2)>>]
      -> [ [<hov 0> "`"(ZEXPR $n1):E "*"(ZEXPR $n2):L "`"] ]
  .
\end{verbatim}

\section{How to use \texttt{SearchIsos}}

As shown in the overview, \texttt{SearchIsos} is made up of two tools: new
commands integrated in Coq and a separated program.

\subsection{In the {\Coq} toplevel}

Under \Coq, \texttt{SearchIsos} is called upon with the following command:

\begin{tabbing}
\ \ \ \ \=\kill
\>{\tt SearchIsos} {\it term}.
\end{tabbing}

This command displays the full name (modules, sections and identifiers) of all
the constants, variables, inductive types and constructors of inductive types
of the current context (not necessarily in the specialized
buffers) whose type is equal to {\it term} up to isomorphisms. These
isomorphisms of types are characterized by the contextual part of a theory
which is a generalization of the axiomatization for the typed lambda-calculus
associated with the Closed Cartesian Categories taking into account
polymorphism and dependent types.

\texttt{SearchIsos} is twined with two other commands which allow to have some
informations about the search time:

\begin{tabbing}
\ \ \ \ \=\kill
\>{\tt Time}.\\
\>{\tt UnTime}.
\end{tabbing}

As expected, these two commands respectively sets and disconnects the Time
Search Display mode.

The following example shows a possibility of use:

\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Time.
Variables A,B:Set.
Hypothesis H0:(x:A)(y:B)(x=x/\y=y).
SearchIsos (b:B)(a:A)(b=b/\a=a).
\end{coq_example}

For more informations, see the sections 5.6.7, 5.6.8 and 5.6.9 in the Reference
Manual.

\subsection{In the whole library hierarchy}

To extend the search to a {\Coq} library, you must use \textsf{Coq\_SearchIsos}
which is an independent tool compared to {\Coq} and can be invoked by the shell
command as follows:

\begin{tabbing}
\ \ \ \ \=\kill
\>{\tt coqtop -searchisos}
\end{tabbing}

Under this new toplevel (which contains your {\Coq} library), the three
commands {\tt SearchIsos}, {\tt Time} and {\tt UnTime} (described previously)
are then available and have always the same behavior.

Likewise, this little sample (about the Euclidean division) shows a possible
request to the standard library of {\Coq}:

\begin{verbatim}
Coq_SearchIsos < Time.

Coq_SearchIsos < SearchIsos (b,a:nat)(gt b O)
Coq_SearchIsos <   ->{q:nat&{r:nat|a=(plus (mult q b) r)/\(gt b r)}}.
#Div#--* [div1 : (b:nat)(gt b (0))->(a:nat)(diveucl a b)]
#Div#--* [div2 : (b:nat)(gt b (0))->(a:nat)(diveucl a b)]
#Euclid_proof#--* [eucl_dev : (b:nat)(gt b (0))->(a:nat)(diveucl a b)]
#Euclid_proof#--* [quotient : 
(b:nat)
 (gt b (0))
  ->(a:nat){q:nat | (EX r:nat | a=(plus (mult q b) r)/\(gt b r))}]
#Euclid_proof#--* [modulo : 
(b:nat)
 (gt b (0))
  ->(a:nat){r:nat | (EX q:nat | a=(plus (mult q b) r)/\(gt b r))}]
Finished transaction in 4 secs (2.27u,0s)
\end{verbatim}

For more informations about \textsf{Coq\_SearchIsos}, see the section 15.4 in
the Reference Manual.

\section{The new reduction functions} \label{reductions}

\subsection{\texttt{Cbv}, \texttt{Lazy}}
The usual reduction or conversion tactics are \verb!Red!, \verb!Hnf!,
\verb!Simpl!, \verb!Unfold!, \verb!Change! and \verb!Pattern!.  It is
now possible to normalize a goal with a parametric reduction function,
by specifying which of $\beta$,$\delta$ and $\iota$ must be
performed. In the case of $\delta$, a list of identifiers to unfold,
or a list of identifiers not to unfold, may follow. Moreover, two
strategies are available: a call-by-value reduction, efficient for
computations, and a lazy reduction, i.e. a call-by-name strategy with
sharing of reductions. 

To apply a reduction tactic, use one of the two strategies
\texttt{Cbv} for call-by value or \texttt{Lazy} for lazy reduction
applied to one or more ``flags'' designing which reduction to perform 
\texttt{Beta} for $\beta$-reduction, \texttt{Iota} for
$\iota$-reduction (reduction of \texttt{Cases}) and \texttt{Delta} for
$\delta$-reduction (expansion of constants).

The function  \verb!Compute! is simply an alias for
\verb!Cbv Beta Delta Iota!. 

The following tactic applies on the current goal, 
the $\beta\iota$-reduction, and
$\delta$-reduction of any constants except \verb!minus!, using the
call-by-value strategy.
\begin{verbatim}
Cbv Beta Iota Delta - [ minus ]
\end{verbatim}

\subsection{\texttt{Fold}}
A specific function \verb!Fold!  was designed:
\verb!Fold! takes as argument a list of
terms. These terms are reduced using \verb!Red!, and the result is
replaced by the expanded term. For example,
\begin{coq_example*}
Require Arith.
Lemma ex4 : (n:nat)(le (S O) n)->(le (S n) (plus n n)).
Intros.
\end{coq_example*}
\begin{coq_example}
Fold (plus (1) n).
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}

\subsection{\texttt{Eval}}

The reduction may be applied to a given term (not only the goal) with
the vernac command \verb!Eval!. 
The syntax is:
\[\texttt{Eval}~ \textit{ReductionFunction}~ \texttt{in}~
\textit{term}.\]
To compute the reduced value of $t$ using the reduction strategy 
\textit{ReductionFunction}.

It may happen that the term to be
reduced depends on hypothesis introduced in a goal. The default
behavior is that the term is interpreted in the current goal (if
any). \texttt{Eval} can take an extra argument specifying an
alternative goal.

Here are a few examples of reduction commands:
\begin{coq_example}
Eval Simpl in [n:nat]n=(plus O n).
\end{coq_example}
Simplifies the expression.
\begin{coq_example*}
Lemma ex5 : O=O /\ (x:nat)x=x.
Split; Intros.
\end{coq_example*}
\begin{coq_example}
Eval 2 Lazy Beta Delta [ mult ] Iota in ([n:nat](mult n (plus n x)) (3)).
\end{coq_example}

$\beta\iota$-reduces the given term and $\delta$-reduces \verb+mult+ in the
context of the second goal.

\begin{coq_example}
Eval Compute in `18446744073709551616 * 18446744073709551616`.
\end{coq_example}

Computes $2^{128}$.

\section{Installation procedure}

\subsection{Uninstalling Coq}

\paragraph{Warning} 
It is strongly recommended to clean-up the V6.1 Coq library directory
by hand, before you install the new version.
\paragraph{Uninstalling Coq V6.2}
There is a new option to coqtop \texttt{-uninstall} that will remove
the 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 1.06 or 1.07, and Camlp4 version 1.07.2
to compile the system. Both are available by anonymous ftp
at:

\bigskip
\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.2-linux-i386.tar.gz \\
Solaris & Sparc & coq-6.2-solaris-sparc.tar.gz\\
Digital & Alpha & coq-6.2-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}

The MS Windows version will be soon available.

%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}

The new parsing mechanism and the new syntax for extensible grammars
and pretty-printing rules are from Bruno Barras and Daniel de
Rauglaudre.

The rearrangement of tactics, the extension of \texttt{Tauto}, \texttt{Intros} and
equality tactics, and the tactic definition mechanism are from Eduardo
Gim\'enez. Jean-Christophe Filli\^atre designed and implemented the
tactic \texttt{Refine} and the tactic \texttt{Correctness}.

Bruno Barras improved the reduction functions and introduced new
uniform commands for reducing a goal or an expression.  David Delahaye
designed and implemented {\tt SearchIsos}.

Patrick Loiseleur introduced syntax rules to
manipulate natural numbers and binary integers expression.
Hugo Herbelin improved the loading mechanism and contributed to a more
user-friendly syntax.

\end{document}

% Local Variables: 
% mode: LaTeX
% TeX-master: t
% End: 


% $Id$