diff options
Diffstat (limited to 'doc/ChangesV6-2.tex')
| -rwxr-xr-x | doc/ChangesV6-2.tex | 921 |
1 files changed, 0 insertions, 921 deletions
diff --git a/doc/ChangesV6-2.tex b/doc/ChangesV6-2.tex deleted file mode 100755 index 3a0f7ef17..000000000 --- a/doc/ChangesV6-2.tex +++ /dev/null @@ -1,921 +0,0 @@ -\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$ - |