path: root/doc/newfaq/main.tex

\documentclass[a4paper]{faq}
\pagestyle{plain}

% yay les symboles
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{url}

% version et date
\def\faqversion{0.1}

% les macros d'amour
\def\Coq{\textsc{Coq }}
\def\Why{\textsc{Why }}
\def\Krakatoa{\textsc{Krakatoa }}
\def\Ltac{\textsc{Ltac }}
\def\CoqIde{\textsc{CoqIde }}

\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 ?}

This is any logic which does not assume that ``A or not A''.


\Question[theory]{Where can I find information about the theory behind \Coq ?}

\begin{description}
\item[Type theory]
Proof and Types~\cite{ProofsTypes}
Cours de Gilles~\cite{Types:Dowek}
Manuel de Coq~\cite{Coq:manual}

\item[Inductives]

Habilitation Christine~\cite{Pau96b}

\item[Co-Inductives]
Thèse Eduardo Giménez~\cite{EGThese}

\item[Extraction]
Pierre Letouzey
\end{description}


\Question[provingprograms]{How can I use \Coq to prove programs ?}

You can either extract a program from a proof use the extraction mechanism or use dedicated tools to prove annotated programs writen in another langage such as \Why and \Krakatoa.
\Question[nbusers]{How many \Coq users are there ?}

That's a good question.

\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] A GTK based gui for \Coq.
\item[Pcoq] A gui for \Coq with proof by pointing and pretty printing.
\item[Why] A back-end generator of verification conditions.
\item[Krakatoa] A Java code certification tool that uses both \Coq and \Why to verify the soundness of implementations with regards to the specifications.
\item[coqwc] A tool similar to {\tt wc} to count lines in \Coq files.
\item[coq-tex] A tool to insert \Coq examples within .tex files. 
\item[coqdoc] A documentation tool for \Coq.
\item[Proof General] A emacs mode for \Coq and many other proof assistants.
\item[Foc] The Foc project aims at building an environment to develop certified computer algebra libraries. 
\end{description}

\Question[industrial]{What are industrial application for \Coq ?}

Coq is used by Trusted Logic to prove properties of the JavaCard system.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Documentation}

\Question[coqdocumentation]{Where can I find documentation about \Coq ?} 
All the documentation about \Coq, from the reference manual \cite{Coq:manual} to
friendly tutorials \cite{Coq:Tutorial} and documentation of the standard library, is available online at 
\url{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 ?}

This faq is available online at \url{http://coq.inria.fr/faq.html}.

\Question[faqimprov]{How can I submit suggestions / improvements / additions for this FAQ?}

This FAQ is unfinished (in the sense that there are some obvious sections it needs, some included below). Please send contributions to the authors. 


\Question[coqmailinglist]{Is there any mailing list about \Coq ?} 
The main \Coq mailing list is \url{coq-club@pauillac.inria.fr}, which
broadcasts questions and suggestions about the implementation, the
logical formalism or proof developments. See
\url{http://pauillac.inria.fr/mailman/listinfo/coq-club} for
subsription. Bugs reports should be sent at the \url{coq-bugs@pauillac.inria.fr} mailing-list.

\Question[coqmailinglistarchive]{Where can I find an archive of the 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[coqexamples]{Where can I find some \Coq examples ?} 

There are examples in the manual \cite{Coq:manual} and in the CoqArt \cite{Coq:coqart}. You can also find large developments using \Coq in the \Coq user contributions : \url{http://coq.inria.fr/distrib-eng.html}

\Question[coqbug]{How can I report a bug ?}

You can use the web interface at \url{http://coq.inria.fr/bin/coq-bugs}.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\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
(\url{http://coq.inria.fr/distrib-eng.html}). Most recent sources can
be accessed via anonymous CVS: \url{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 platforms supporting Objective Caml.


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\section{Talkin' with the Rooster}



%%%%%%%
\subsection{My goal is ...,  how can I prove it ?}


\Question[conjonction]{My goal is a conjunction, how can I prove it ?}

Use some theorem or assumption or use the {\tt split} tactic.

\Question[disjonction]{My goal is a disjonction, how can I prove it ?}

You can prove the left part or the right part of the disjunction using {\tt left} or {\tt right} tactics. If you want to do a classical reasoning step, use {\tt }  to prove the right part with the assumption that the left part of the disjunction is false.

\Question[forall]{My goal is an universally quantified statement, how can I prove it ?}

Use some theorem or assumption or introduce the quantified variable in the context using the {\tt intro} tactic. If there are several variables you can use the {\tt intros} tactic. 

\Question[exist]{My goal is an existential, how can I prove it ?}

Use some theorem or assumption or exhibits the witness using {\tt exists} tactic.

\Question[taut]{My goal is a propositional tautology, how can I prove it ?}

Just use the {\tt tauto} tactic.

\Question[firstorder]{My goal is a first order formula, how can I prove it ?}

Just use the {\tt firstorder} tactic.

\Question[cong]{My goal is solvable by a sequence of rewrites, how can I prove it ?}

Just use the {\tt congruence} tactic.

\Question[congnot]{My goal is disequality solvable by a sequence of rewrites, how can I prove it ?}

Just use the {\tt congruence} tactic.

\Question[ring]{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?}

Just use the {\tt ring} tactic.

\Question[field]{My goal is an equality on some field (e.g. reals), how can I prove it ?}

Just use the {\tt field} tactic.

\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 ?}

Just use the {\tt gv} tactic.

\Question[apply]{My goal is solvable by  some lemma, how can I prove it ?}

Just use the {\tt apply} tactic.

\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 ?}

Use a base of Hints.

\Question[assumption]{My goal is one of the hypothesis, how can I prove it ?}

Use the {\tt assumption} tactic.

\Question[trivial]{My goal is ???, how can I prove it ?}

\Question[proofwith]{I want to automatize the use of some tactic how can I do it ?}

You need to use the {\tt proof with T} command.
For instance :

\Question[complete]{I want to execute the proofwith tactic only if it solves the goal, how can I do it ?}

You need to use the {\tt solve} tactic.

\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 ?}


%%%%%%%
\subsection{\Ltac}

\Question[ltac]{What is \Ltac ?}

\Ltac is the tactic language for \Coq.

\Question[ltacerror]{Why do I always get the same error message ?}


\Question[ltacprint]{Is there any printing command in \Ltac ?}

You can use the {\tt Idtac} tactic with a string argument. This string
will be printed out.
The same applies to the {\tt fail} tactic

\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 ?}

You can use the following syntax :
{\tt Let id:=fresh in }

\Question[statdyn]{How can I define static and dynamic code ?}

%%%%%%%
\subsection{Glossary}

\Question[goal]{What is a goal ?}

The goal is the statement to be proved.

\Question[metavariable]{What is a meta variable ?}

\Question[type]{What is Type(i) ?}

\Question[dependanttype]{What is a dependent type ?}


\Question[reflection]{What is a proof by reflection ?}

This is a proof generated by some computation which is done using the internal reduction of Coq (not using the tactic language of \Coq (\Ltac) nor the implementation language for \Coq).
An example of tactic using the reflection mechanism is the {\tt ring} tactic. 
The reflection method consist in reflecting a subset of Coq language (for example the arithmetical expressions) into an object of the Coq language itself (in our case an inductive type denoting arithmetical expressions).
For more information see  \cite{howe,harrison,boutin} and the last chapter of the CoqArt.


\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:manual} 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}