\documentclass[a4paper]{faq} \pagestyle{plain} % yay les symboles \usepackage{stmaryrd} \usepackage{amssymb} % version et date \def\faqversion{0.1} % les macros d'amour \def\Coq{\textsc{Coq }} \def\Ltac{\textsc{Ltac }} \begin{document} \bibliographystyle{plain} %%%%%%% Coq pour les nuls %%%%%%% \title{Coq for the Clueless\\ \large(\ifpdf\ref*{lastquestion}\else\protect\ref{lastquestion}\fi \ Hints) } \author{Florent Kirchner \and Julien Narboux} \maketitle %%%%%%% \begin{abstract} This note intends to provide an easy way to get aquainted with the \Coq theorem prover. It tries to formulate appropriate answers to some of the questions any newcommers will face, and to give pointers to other references when possible. \end{abstract} %%%%%%% \begin{multicols}{2} \tableofcontents \end{multicols} %%%%%%% \newpage \section{Introduction} This FAQ is the sum of the questions that came to mind as we developed proofs in \Coq. Since we are singularly short-minded, we wrote the answers we found on bits of papers to have them at hand whenever the situation occurs again. This, is pretty much the result of that: a collection of tips one can refer to when proofs become intricate. Yes, this means we won't take the blame for the shortcomings of this FAQ. But if you want to contribute and send in your own question and answers, feel free to write to us\ldots %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Presentation} \Question[whatiscoq]{What is \Coq ?} The Coq tool is a proof assistant which: \begin{itemize} \item allows to handle calculus assertions, \item to check mechanically proofs of these assertions, \item helps to find formal proofs, \item extracts a certified program from the constructive proof of its formal specification, \end{itemize} Coq is written in the Objective Caml language and uses the Camlp4 Pre-processor-pretty-printer for Objective Caml. \Question[name]{Did you really need to name it like that ?} Some french computer scientists have a tradition of naming their software as animal species: Caml, Elan, Foc or Krakatoa are examples of this tacit convention. In french, ``coq'' means rooster, and it sounds like the initials of the Calculus of Constructions CoC on which it is based. \Question[theoremprovers]{What are the other theorem provers ?} Many other theorem provers are available for use nowadays. Isabelle / HOL, Lego, Nuprl, PVS are examples of provers that are fairly similar to \Coq by the way they interact with the user. More distant relatives of \Coq are ACL2, ALF, Alfa, Mizar, $\Omega$mega\ldots \Question[intuitionnisticlogic]{What is intuitionnistic logic ?} \Question[theory]{Where can I find informations about the theory behind \Coq ?} \begin{description} \item[Type theory] Proof and Types Cours de Gilles Manuel de Coq \item[Inductives] Habilitation Christine \item[Co-Inductives] Thèse \item[Extraction] Pierre Letouzey \end{description} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Documentation} \Question[coqdocumentation]{Where can I find documentation about \Coq ?} All the documentation about \Coq, from the reference manual to friendly tutorials and documentation of the standard library, is available online at \mbox{\tt http://pauillac.inria.fr/coq/doc-eng.html}. All these documents are viewable either in browsable html, or as downloadable postscripts. \Question[coqfaq]{Where can I find this faq on the web ?} Errr\ldots \Question[coqmailinglist]{Is there any mailing list about \Coq ?} The main \Coq mailing list is {\tt coq-club@pauillac.inria.fr}, which broadcasts questions and suggestions about the implementation, the logical formalism or proof developments. See \mbox{\tt http://pauillac.inria.fr/mailman/listinfo/coq-club} for subsription. Bugs reports should be sent at the {\tt coq-bugs@pauillac.inria.fr} mailing-list. \Question[coqbook]{Is there any book about \Coq ?} The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art will be published by Springer-Verlag in 2004: \begin{quote} ``This book provides a pragmatic introduction to the development of proofs and certified programs using Coq. With its large collection of examples and exercises it is an invaluable tool for researchers, students, and engineers interested in formal methods and the development of zero-default software.'' \end{quote} \Question[nbusers]{How many \Coq users are there ?} \Question[howold]{How old is \Coq ?} The first official release of \Coq (v. 4.1.0) was distributed in 1989. \Question[relatedtools]{What are the \Coq-related tools ?} \begin{description} \item[Coqide] \item[Pcoq] \item[Why] \item[Krakatoa] \item[coqwc] \item[coq-tex] \item[coqdoc] A documentation tool for \Coq. \item[Proof General] \item[Foc] \end{description} \Question[indutrial]{What are industrial application for \Coq ?} Trusted Logic ... %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Installation} \Question[coqlicence]{What is the licence of \Coq ?} It is distributed under the GNU Lesser General Licence (LGPL). \Question[coqsources]{Where can I find the sources of \Coq ?} The sources of \Coq can be found online in the tar.gz'ed packages ({\tt http://coq.inria.fr/distrib-eng.html}). Most recent sources can be accessed via anonymous CVS: {\tt http://coqcvs.inria.fr/cvsserver-eng.html} \Question[platform]{On which platform \Coq is available ?} Compiled binaries are available for Linux, MacOs X, Solaris, and Windows. The sources can be easily adapted to all platform supporting Objective Caml. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \section{Talkin' with the Rooster} \Question[coqexamples]{Where can I find some \Coq examples ?} \Question[goal]{What is a goal ?} \Question[metavariable]{What is a meta variable ?} \Question[type]{What is Type(i) ?} \Question[dependanttype]{What is a dependent type ?} \Question[reflexivity]{What is reflexivity ?} \Question[conjonction]{My goal is a conjonction, how can I prove it ?} \Question[disjonction]{My goal is a disjonction, how can I prove it ?} \Question[forall]{My goal is an universally quantified statement, how can I prove it ?} \Question[exist]{My goal is an existential, how can I prove it ?} \Question[taut]{My goal is a propositional tautology, how can I prove it ?} \Question[firstorder]{My goal is a first order formula, how can I prove it ?} \Question[cong]{My goal is solvable by a sequence of rewrites, how can I prove it ?} \Question[ring]{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?} \Question[field]{My goal is an equality on some field (e.g. reals), how can I prove it ?} \Question[omega]{My goal is an inequality on R, how can I prove it ?} \Question[gb]{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it ?} \Question[apply]{My goal is solvable by some lemma, how can I prove it ?} \Question[autowith]{My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?} \Question[assumption]{My goal is one of the hypothesis, how can I prove it ?} \Question[trivial]{My goal is ???, how can I prove it ?} \Question[proofwith]{I want to automatize the use of a tactic how can I do it ?} \Question[complete]{I want to execute the proofwith tactic only if it solves the goal, how can I do it ?} \Question[subgoalsorder]{How can I change the order of the subgoals ?} \Question[hyphotesisorder]{How can I change the order of the hypothesis ?} \Question[ifsyntax]{What is the syntax for if ?} \Question[letsyntax]{What is the syntax for let ?} \Question[patternmatchingsyntax]{What is the syntax for pattern matching ?} \Question[reflection]{What is a proof by reflection ?} \section{\Ltac} \Question[ltac]{What is \Ltac ?} \Question[letltac]{What is the syntax for let in \Ltac ?} \Question[matchltac]{What is the syntax for pattern matching in \Ltac ?} \Question[matchsem]{What is the semantic for match context ?} \Question[fresh]{How can I generate a new name ?} \Question[statdyn]{How can I define static and dynamic code ?} \section{Coqide} \section{Conclusion and Farewell.} \label{ccl} \Question[NoAns]{What if my question isn't answered here ?} \label{lastquestion} Don't panic. You can try the \Coq manual~\cite{Coq:e} for a technical description of the prover. The Coq'Art~\cite{Coq:coqart} is the first book written on \Coq and provides a comprehensive review of the theorem prover as well as a number of example and exercises. Finally, the tutorial~\cite{Coq:Tutorial} provides a smooth introduction to theorem proving in \Coq. %%%%%%% \newpage \nocite{LaTeX:intro} \nocite{LaTeX:symb} \bibliography{fk} %%%%%%% \typeout{*** That makes \thequestion\space questions ***} \end{document}