diff options
Diffstat (limited to 'doc/refman/RefMan-pre.tex')
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 605 |
1 files changed, 0 insertions, 605 deletions
diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex deleted file mode 100644 index 8b6e29b5..00000000 --- a/doc/refman/RefMan-pre.tex +++ /dev/null @@ -1,605 +0,0 @@ -\setheaders{Credits} -\chapter*{Credits} -%\addcontentsline{toc}{section}{Credits} - -\Coq{}~ is a proof assistant for higher-order logic, allowing the -development of computer programs consistent with their formal -specification. It is the result of about ten years of research of the -Coq project. We shall briefly survey here three main aspects: the -\emph{logical language} in which we write our axiomatizations and -specifications, the \emph{proof assistant} which allows the development -of verified mathematical proofs, and the \emph{program extractor} which -synthesizes computer programs obeying their formal specifications, -written as logical assertions in the language. - -The logical language used by {\Coq} is a variety of type theory, -called the \emph{Calculus of Inductive Constructions}. Without going -back to Leibniz and Boole, we can date the creation of what is now -called mathematical logic to the work of Frege and Peano at the turn -of the century. The discovery of antinomies in the free use of -predicates or comprehension principles prompted Russell to restrict -predicate calculus with a stratification of \emph{types}. This effort -culminated with \emph{Principia Mathematica}, the first systematic -attempt at a formal foundation of mathematics. A simplification of -this system along the lines of simply typed $\lambda$-calculus -occurred with Church's \emph{Simple Theory of Types}. The -$\lambda$-calculus notation, originally used for expressing -functionality, could also be used as an encoding of natural deduction -proofs. This Curry-Howard isomorphism was used by N. de Bruijn in the -\emph{Automath} project, the first full-scale attempt to develop and -mechanically verify mathematical proofs. This effort culminated with -Jutting's verification of Landau's \emph{Grundlagen} in the 1970's. -Exploiting this Curry-Howard isomorphism, notable achievements in -proof theory saw the emergence of two type-theoretic frameworks; the -first one, Martin-L\"of's \emph{Intuitionistic Theory of Types}, -attempts a new foundation of mathematics on constructive principles. -The second one, Girard's polymorphic $\lambda$-calculus $F_\omega$, is -a very strong functional system in which we may represent higher-order -logic proof structures. Combining both systems in a higher-order -extension of the Automath languages, T. Coquand presented in 1985 the -first version of the \emph{Calculus of Constructions}, CoC. This strong -logical system allowed powerful axiomatizations, but direct inductive -definitions were not possible, and inductive notions had to be defined -indirectly through functional encodings, which introduced -inefficiencies and awkwardness. The formalism was extended in 1989 by -T. Coquand and C. Paulin with primitive inductive definitions, leading -to the current \emph{Calculus of Inductive Constructions}. This -extended formalism is not rigorously defined here. Rather, numerous -concrete examples are discussed. We refer the interested reader to -relevant research papers for more information about the formalism, its -meta-theoretic properties, and semantics. However, it should not be -necessary to understand this theoretical material in order to write -specifications. It is possible to understand the Calculus of Inductive -Constructions at a higher level, as a mixture of predicate calculus, -inductive predicate definitions presented as typed PROLOG, and -recursive function definitions close to the language ML. - -Automated theorem-proving was pioneered in the 1960's by Davis and -Putnam in propositional calculus. A complete mechanization (in the -sense of a semi-decision procedure) of classical first-order logic was -proposed in 1965 by J.A. Robinson, with a single uniform inference -rule called \emph{resolution}. Resolution relies on solving equations -in free algebras (i.e. term structures), using the \emph{unification - algorithm}. Many refinements of resolution were studied in the -1970's, but few convincing implementations were realized, except of -course that PROLOG is in some sense issued from this effort. A less -ambitious approach to proof development is computer-aided -proof-checking. The most notable proof-checkers developed in the -1970's were LCF, designed by R. Milner and his colleagues at U. -Edinburgh, specialized in proving properties about denotational -semantics recursion equations, and the Boyer and Moore theorem-prover, -an automation of primitive recursion over inductive data types. While -the Boyer-Moore theorem-prover attempted to synthesize proofs by a -combination of automated methods, LCF constructed its proofs through -the programming of \emph{tactics}, written in a high-level functional -meta-language, ML. - -The salient feature which clearly distinguishes our proof assistant -from say LCF or Boyer and Moore's, is its possibility to extract -programs from the constructive contents of proofs. This computational -interpretation of proof objects, in the tradition of Bishop's -constructive mathematics, is based on a realizability interpretation, -in the sense of Kleene, due to C. Paulin. The user must just mark his -intention by separating in the logical statements the assertions -stating the existence of a computational object from the logical -assertions which specify its properties, but which may be considered -as just comments in the corresponding program. Given this information, -the system automatically extracts a functional term from a consistency -proof of its specifications. This functional term may be in turn -compiled into an actual computer program. This methodology of -extracting programs from proofs is a revolutionary paradigm for -software engineering. Program synthesis has long been a theme of -research in artificial intelligence, pioneered by R. Waldinger. The -Tablog system of Z. Manna and R. Waldinger allows the deductive -synthesis of functional programs from proofs in tableau form of their -specifications, written in a variety of first-order logic. Development -of a systematic \emph{programming logic}, based on extensions of -Martin-L\"of's type theory, was undertaken at Cornell U. by the Nuprl -team, headed by R. Constable. The first actual program extractor, PX, -was designed and implemented around 1985 by S. Hayashi from Kyoto -University. It allows the extraction of a LISP program from a proof -in a logical system inspired by the logical formalisms of S. Feferman. -Interest in this methodology is growing in the theoretical computer -science community. We can foresee the day when actual computer systems -used in applications will contain certified modules, automatically -generated from a consistency proof of their formal specifications. We -are however still far from being able to use this methodology in a -smooth interaction with the standard tools from software engineering, -i.e. compilers, linkers, run-time systems taking advantage of special -hardware, debuggers, and the like. We hope that {\Coq} can be of use -to researchers interested in experimenting with this new methodology. - -A first implementation of CoC was started in 1984 by G. Huet and T. -Coquand. Its implementation language was CAML, a functional -programming language from the ML family designed at INRIA in -Rocquencourt. The core of this system was a proof-checker for CoC seen -as a typed $\lambda$-calculus, called the \emph{Constructive Engine}. -This engine was operated through a high-level notation permitting the -declaration of axioms and parameters, the definition of mathematical -types and objects, and the explicit construction of proof objects -encoded as $\lambda$-terms. A section mechanism, designed and -implemented by G. Dowek, allowed hierarchical developments of -mathematical theories. This high-level language was called the -\emph{Mathematical Vernacular}. Furthermore, an interactive -\emph{Theorem Prover} permitted the incremental construction of proof -trees in a top-down manner, subgoaling recursively and backtracking -from dead-alleys. The theorem prover executed tactics written in CAML, -in the LCF fashion. A basic set of tactics was predefined, which the -user could extend by his own specific tactics. This system (Version -4.10) was released in 1989. Then, the system was extended to deal -with the new calculus with inductive types by C. Paulin, with -corresponding new tactics for proofs by induction. A new standard set -of tactics was streamlined, and the vernacular extended for tactics -execution. A package to compile programs extracted from proofs to -actual computer programs in CAML or some other functional language was -designed and implemented by B. Werner. A new user-interface, relying -on a CAML-X interface by D. de Rauglaudre, was designed and -implemented by A. Felty. It allowed operation of the theorem-prover -through the manipulation of windows, menus, mouse-sensitive buttons, -and other widgets. This system (Version 5.6) was released in 1991. - -\Coq{} was ported to the new implementation Caml-light of X. Leroy and -D. Doligez by D. de Rauglaudre (Version 5.7) in 1992. A new version -of \Coq{} was then coordinated by C. Murthy, with new tools designed -by C. Parent to prove properties of ML programs (this methodology is -dual to program extraction) and a new user-interaction loop. This -system (Version 5.8) was released in May 1993. A Centaur interface -\textsc{CTCoq} was then developed by Y. Bertot from the Croap project -from INRIA-Sophia-Antipolis. - -In parallel, G. Dowek and H. Herbelin developed a new proof engine, -allowing the general manipulation of existential variables -consistently with dependent types in an experimental version of \Coq{} -(V5.9). - -The version V5.10 of \Coq{} is based on a generic system for -manipulating terms with binding operators due to Chet Murthy. A new -proof engine allows the parallel development of partial proofs for -independent subgoals. The structure of these proof trees is a mixed -representation of derivation trees for the Calculus of Inductive -Constructions with abstract syntax trees for the tactics scripts, -allowing the navigation in a proof at various levels of details. The -proof engine allows generic environment items managed in an -object-oriented way. This new architecture, due to C. Murthy, -supports several new facilities which make the system easier to extend -and to scale up: - -\begin{itemize} -\item User-programmable tactics are allowed -\item It is possible to separately verify development modules, and to - load their compiled images without verifying them again - a quick - relocation process allows their fast loading -\item A generic parsing scheme allows user-definable notations, with a - symmetric table-driven pretty-printer -\item Syntactic definitions allow convenient abbreviations -\item A limited facility of meta-variables allows the automatic - synthesis of certain type expressions, allowing generic notations - for e.g. equality, pairing, and existential quantification. -\end{itemize} - -In the Fall of 1994, C. Paulin-Mohring replaced the structure of -inductively defined types and families by a new structure, allowing -the mutually recursive definitions. P. Manoury implemented a -translation of recursive definitions into the primitive recursive -style imposed by the internal recursion operators, in the style of the -ProPre system. C. Mu{\~n}oz implemented a decision procedure for -intuitionistic propositional logic, based on results of R. Dyckhoff. -J.C. Filli{\^a}tre implemented a decision procedure for first-order -logic without contraction, based on results of J. Ketonen and R. -Weyhrauch. Finally C. Murthy implemented a library of inversion -tactics, relieving the user from tedious definitions of ``inversion -predicates''. - -\begin{flushright} -Rocquencourt, Feb. 1st 1995\\ -Gérard Huet -\end{flushright} - -\section*{Credits: addendum for version 6.1} -%\addcontentsline{toc}{section}{Credits: addendum for version V6.1} - -The present version 6.1 of \Coq{} is based on the V5.10 architecture. It -was ported to the new language Objective Caml by Bruno Barras. The -underlying framework has slightly changed and allows more conversions -between sorts. - -The new version provides powerful tools for easier developments. - -Cristina Cornes designed an extension of the \Coq{} syntax to allow -definition of terms using a powerful pattern-matching analysis in the -style of ML programs. - -Amokrane Saïbi wrote a mechanism to simulate -inheritance between types families extending a proposal by Peter -Aczel. He also developed a mechanism to automatically compute which -arguments of a constant may be inferred by the system and consequently -do not need to be explicitly written. - -Yann Coscoy designed a command which explains a proof term using -natural language. Pierre Cr{\'e}gut built a new tactic which solves -problems in quantifier-free Presburger Arithmetic. Both -functionalities have been integrated to the \Coq{} system by Hugo -Herbelin. - -Samuel Boutin designed a tactic for simplification of commutative -rings using a canonical set of rewriting rules and equality modulo -associativity and commutativity. - -Finally the organisation of the \Coq{} distribution has been supervised -by Jean-Christophe Filliâtre with the help of Judicaël Courant -and Bruno Barras. - -\begin{flushright} -Lyon, Nov. 18th 1996\\ -Christine Paulin -\end{flushright} - -\section*{Credits: addendum for version 6.2} -%\addcontentsline{toc}{section}{Credits: addendum for version V6.2} - -In version 6.2 of \Coq{}, the parsing is done using camlp4, a -preprocessor and pretty-printer for CAML designed by Daniel de -Rauglaudre at INRIA. Daniel de Rauglaudre made the first adaptation -of \Coq{} for camlp4, this work was continued by Bruno Barras who also -changed the structure of \Coq{} abstract syntax trees and the primitives -to manipulate them. The result of -these changes is a faster parsing procedure with greatly improved -syntax-error messages. The user-interface to introduce grammar or -pretty-printing rules has also changed. - -Eduardo Giménez redesigned the internal -tactic libraries, giving uniform names -to Caml functions corresponding to \Coq{} tactic names. - -Bruno Barras wrote new more efficient reductions functions. - -Hugo Herbelin introduced more uniform notations in the \Coq{} -specification language: the definitions by fixpoints and -pattern-matching have a more readable syntax. Patrick Loiseleur -introduced user-friendly notations for arithmetic expressions. - -New tactics were introduced: Eduardo Giménez improved a mechanism to -introduce macros for tactics, and designed special tactics for -(co)inductive definitions; Patrick Loiseleur designed a tactic to -simplify polynomial expressions in an arbitrary commutative ring which -generalizes the previous tactic implemented by Samuel Boutin. -Jean-Christophe Filli\^atre introduced a tactic for refining a goal, -using a proof term with holes as a proof scheme. - -David Delahaye designed the \textsf{SearchIsos} tool to search an -object in the library given its type (up to isomorphism). - -Henri Laulhère produced the \Coq{} distribution for the Windows environment. - -Finally, Hugo Herbelin was the main coordinator of the \Coq{} -documentation with principal contributions by Bruno Barras, David Delahaye, -Jean-Christophe Filli\^atre, Eduardo -Giménez, Hugo Herbelin and Patrick Loiseleur. - -\begin{flushright} -Orsay, May 4th 1998\\ -Christine Paulin -\end{flushright} - -\section*{Credits: addendum for version 6.3} -The main changes in version V6.3 was the introduction of a few new tactics -and the extension of the guard condition for fixpoint definitions. - - -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. - -\begin{flushright} -Orsay, Dec. 1999\\ -Christine Paulin -\end{flushright} - -%\newpage - -\section*{Credits: versions 7} - -The version V7 is a new implementation started in September 1999 by -Jean-Christophe Filliâtre. This is a major revision with respect to -the internal architecture of the system. The \Coq{} version 7.0 was -distributed in March 2001, version 7.1 in September 2001, version -7.2 in January 2002, version 7.3 in May 2002 and version 7.4 in -February 2003. - -Jean-Christophe Filliâtre designed the architecture of the new system, he -introduced a new representation for environments and wrote a new kernel -for type-checking terms. His approach was to use functional -data-structures in order to get more sharing, to prepare the addition -of modules and also to get closer to a certified kernel. - -Hugo Herbelin introduced a new structure of terms with local -definitions. He introduced ``qualified'' names, wrote a new -pattern-matching compilation algorithm and designed a more compact -algorithm for checking the logical consistency of universes. He -contributed to the simplification of {\Coq} internal structures and the -optimisation of the system. He added basic tactics for forward -reasoning and coercions in patterns. - -David Delahaye introduced a new language for tactics. General tactics -using pattern-matching on goals and context can directly be written -from the {\Coq} toplevel. He also provided primitives for the design -of user-defined tactics in \textsc{Caml}. - -Micaela Mayero contributed the library on real numbers. -Olivier Desmettre extended this library with axiomatic -trigonometric functions, square, square roots, finite sums, Chasles -property and basic plane geometry. - -Jean-Christophe Filliâtre and Pierre Letouzey redesigned a new -extraction procedure from \Coq{} terms to \textsc{Caml} or -\textsc{Haskell} programs. This new -extraction procedure, unlike the one implemented in previous version -of \Coq{} is able to handle all terms in the Calculus of Inductive -Constructions, even involving universes and strong elimination. P. -Letouzey adapted user contributions to extract ML programs when it was -sensible. -Jean-Christophe Filliâtre wrote \verb=coqdoc=, a documentation -tool for {\Coq} libraries usable from version 7.2. - -Bruno Barras improved the reduction algorithms efficiency and -the confidence level in the correctness of {\Coq} critical type-checking -algorithm. - -Yves Bertot designed the \texttt{SearchPattern} and -\texttt{SearchRewrite} tools and the support for the \textsc{pcoq} interface -(\url{http://www-sop.inria.fr/lemme/pcoq/}). - -Micaela Mayero and David Delahaye introduced {\tt Field}, a decision tactic for commutative fields. - -Christine Paulin changed the elimination rules for empty and singleton -propositional inductive types. - -Loïc Pottier developed {\tt Fourier}, a tactic solving linear inequalities on real numbers. - -Pierre Crégut developed a new version based on reflexion of the {\tt Omega} -decision tactic. - -Claudio Sacerdoti Coen designed an XML output for the {\Coq} -modules to be used in the Hypertextual Electronic Library of -Mathematics (HELM cf \url{http://www.cs.unibo.it/helm}). - -A library for efficient representation of finite maps using binary trees -contributed by Jean Goubault was integrated in the basic theories. - -Pierre Courtieu developed a command and a tactic to reason on the -inductive structure of recursively defined functions. - -Jacek Chrz\k{a}szcz designed and implemented the module system of -{\Coq} whose foundations are in Judicaël Courant's PhD thesis. - -\bigskip - -The development was coordinated by C. Paulin. - -Many discussions within the Démons team and the LogiCal project -influenced significantly the design of {\Coq} especially with -%J. Chrz\k{a}szcz, P. Courtieu, -J. Courant, J. Duprat, J. Goubault, A. Miquel, -C. Marché, B. Monate and B. Werner. - -Intensive users suggested improvements of the system : -Y. Bertot, L. Pottier, L. Théry, P. Zimmerman from INRIA, -C. Alvarado, P. Crégut, J.-F. Monin from France Telecom R \& D. -\begin{flushright} -Orsay, May. 2002\\ -Hugo Herbelin \& Christine Paulin -\end{flushright} - -\section*{Credits: version 8.0} - -{\Coq} version 8 is a major revision of the {\Coq} proof assistant. -First, the underlying logic is slightly different. The so-called {\em -impredicativity} of the sort {\tt Set} has been dropped. The main -reason is that it is inconsistent with the principle of description -which is quite a useful principle for formalizing %classical -mathematics within classical logic. Moreover, even in an constructive -setting, the impredicativity of {\tt Set} does not add so much in -practice and is even subject of criticism from a large part of the -intuitionistic mathematician community. Nevertheless, the -impredicativity of {\tt Set} remains optional for users interested in -investigating mathematical developments which rely on it. - -Secondly, the concrete syntax of terms has been completely -revised. The main motivations were - -\begin{itemize} -\item a more uniform, purified style: all constructions are now lowercase, - with a functional programming perfume (e.g. abstraction is now - written {\tt fun}), and more directly accessible to the novice - (e.g. dependent product is now written {\tt forall} and allows - omission of types). Also, parentheses and are no longer mandatory - for function application. -\item extensibility: some standard notations (e.g. ``<'' and ``>'') were - incompatible with the previous syntax. Now all standard arithmetic - notations (=, +, *, /, <, <=, ... and more) are directly part of the - syntax. -\end{itemize} - -Together with the revision of the concrete syntax, a new mechanism of -{\em interpretation scopes} permits to reuse the same symbols -(typically +, -, *, /, <, <=) in various mathematical theories without -any ambiguities for {\Coq}, leading to a largely improved readability of -{\Coq} scripts. New commands to easily add new symbols are also -provided. - -Coming with the new syntax of terms, a slight reform of the tactic -language and of the language of commands has been carried out. The -purpose here is a better uniformity making the tactics and commands -easier to use and to remember. - -Thirdly, a restructuration and uniformisation of the standard library -of {\Coq} has been performed. There is now just one Leibniz' equality -usable for all the different kinds of {\Coq} objects. Also, the set of -real numbers now lies at the same level as the sets of natural and -integer numbers. Finally, the names of the standard properties of -numbers now follow a standard pattern and the symbolic -notations for the standard definitions as well. - -The fourth point is the release of \CoqIDE{}, a new graphical -gtk2-based interface fully integrated to {\Coq}. Close in style from -the Proof General Emacs interface, it is faster and its integration -with {\Coq} makes interactive developments more friendly. All -mathematical Unicode symbols are usable within \CoqIDE{}. - -Finally, the module system of {\Coq} completes the picture of {\Coq} -version 8.0. Though released with an experimental status in the previous -version 7.4, it should be considered as a salient feature of the new -version. - -Besides, {\Coq} comes with its load of novelties and improvements: new -or improved tactics (including a new tactic for solving first-order -statements), new management commands, extended libraries. - -\bigskip - -Bruno Barras and Hugo Herbelin have been the main contributors of the -reflexion and the implementation of the new syntax. The smart -automatic translator from old to new syntax released with {\Coq} is also -their work with contributions by Olivier Desmettre. - -Hugo Herbelin is the main designer and implementor of the notion of -interpretation scopes and of the commands for easily adding new notations. - -Hugo Herbelin is the main implementor of the restructuration of the -standard library. - -Pierre Corbineau is the main designer and implementor of the new -tactic for solving first-order statements in presence of inductive -types. He is also the maintainer of the non-domain specific automation -tactics. - -Benjamin Monate is the developer of the \CoqIDE{} graphical -interface with contributions by Jean-Christophe Filliâtre, Pierre -Letouzey, Claude Marché and Bruno Barras. - -Claude Marché coordinated the edition of the Reference Manual for - \Coq{} V8.0. - -Pierre Letouzey and Jacek Chrz\k{a}szcz respectively maintained the -extraction tool and module system of {\Coq}. - -Jean-Christophe Filliâtre, Pierre Letouzey, Hugo Herbelin and -contributors from Sophia-Antipolis and Nijmegen participated to the -extension of the library. - -Julien Narboux built a NSIS-based automatic {\Coq} installation tool for -the Windows platform. - -Hugo Herbelin and Christine Paulin coordinated the development which -was under the responsability of Christine Paulin. - -\begin{flushright} -Palaiseau \& Orsay, Apr. 2004\\ -Hugo Herbelin \& Christine Paulin\\ -(updated Apr. 2006) -\end{flushright} - -\section*{Credits: version 8.1} - -{\Coq} version 8.1 adds various new functionalities. - -Benjamin Grégoire implemented an alternative algorithm to check the -convertibility of terms in the {\Coq} type-checker. This alternative -algorithm works by compilation to an efficient bytecode that is -interpreted in an abstract machine similar to Xavier Leroy's ZINC -machine. Convertibility is performed by comparing the normal -forms. This alternative algorithm is specifically interesting for -proofs by reflection. More generally, it is convenient in case of -intensive computations. - -Christine Paulin implemented an extension of inductive types allowing -recursively non uniform parameters. Hugo Herbelin implemented -sort-polymorphism for inductive types. - -Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary -compatible equivalence relations. He also generalized rewriting to -arbitrary transition systems. - -Claudio Sacerdoti Coen added new features to the module system. - -Benjamin Grégoire, Assia Mahboubi and Bruno Barras developed a new -more efficient and more general simplification algorithm on rings and -semi-rings. - -Laurent Théry and Bruno Barras developed a new significantly more efficient -simplification algorithm on fields. - -Hugo Herbelin, Pierre Letouzey, Julien Forest, Julien Narboux and -Claudio Sacerdoti Coen added new tactic features. - -Hugo Herbelin implemented matching on disjunctive patterns. - -New mechanisms made easier the communication between {\Coq} and external -provers. Nicolas Ayache and Jean-Christophe Filliâtre implemented -connections with the provers {\sc cvcl}, {\sc Simplify} and {\sc -zenon}. Hugo Herbelin implemented an experimental protocol for calling -external tools from the tactic language. - -Matthieu Sozeau developed \textsc{Russell}, an experimental language -to specify the behavior of programs with subtypes. - -A mechanism to automatically use some specific tactic to solve -unresolved implicit has been implemented by Hugo Herbelin. - -Laurent Théry's contribution on strings and Pierre Letouzey and -Jean-Christophe Filliâtre's contribution on finite maps have been -integrated to the {\Coq} standard library. Pierre Letouzey developed a -library about finite sets ``à la Objective Caml''. With Jean-Marc -Notin, he extended the library on lists. Pierre Letouzey's -contribution on rational numbers has been integrated and extended.. - -Pierre Corbineau extended his tactic for solving first-order -statements. He wrote a reflection-based intuitionistic tautology -solver. - -Pierre Courtieu, Julien Forest and Yves Bertot added extra support to -reason on the inductive structure of recursively defined functions. - -Jean-Marc Notin significantly contributed to the general maintenance -of the system. He also took care of {\textsf{coqdoc}}. - -Pierre Castéran contributed to the documentation of (co-)inductive -types and suggested improvements to the libraries. - -Pierre Corbineau implemented a declarative mathematical proof -language, usable in combination with the tactic-based style of proof. - -Finally, many users suggested improvements of the system through the -Coq-Club mailing list and bug-tracker systems, especially user groups -from INRIA Rocquencourt, Radbout University, University of -Pennsylvania and Yale University. - -\begin{flushright} -Palaiseau, July 2006\\ -Hugo Herbelin -\end{flushright} - -%\newpage - -% Integration of ZArith lemmas from Sophia and Nijmegen. - - -% $Id: RefMan-pre.tex 9283 2006-10-26 08:13:51Z herbelin $ - -%%% Local Variables: -%%% mode: latex -%%% TeX-master: "Reference-Manual" -%%% End: |