path: root/doc/newfaq/main.tex

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

% yay les symboles
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{url}
\usepackage{fullpage}
%\usepackage{hevea}
\input{../macros.tex}

% 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] A book~\cite{ProofsTypes}, some lecture
notes~\cite{Types:Dowek} and the \Coq manual~\cite{Coq:manual}
\item[Inductive types]
Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}
\item[Co-Inductive types]
Eduardo Gim�nez' thesis~\cite{EGThese}
\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, such as \Why and \Krakatoa, to prove
annotated programs written in other langages.

\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 that are missing). 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?}
The archives of the \Coq mailing list are abvailable at
\url{http://pauillac.inria.fr/pipermail/coq-club}.

\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
Coq'Art~\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.
\begin{coq_example}
Goal forall A B:Prop, A->B-> A/\B.
intros.
split.
assumption.
assumption.
Qed.
\end{coq_example}

\Question[conjonctionhyp]{My goal contains a conjunction as an hypothesis, how can I use it ?}

If you want to decompose your hypohtesis into other hypothesis you can use the {\tt decompose} tactic :

\begin{coq_example}
Goal forall A B:Prop, A/\B-> B.
intros.
decompose [and] H.
assumption.
Qed.
\end{coq_example}


\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.

\begin{coq_example}
Goal forall A B:Prop, A-> A\/B.
intros.
left.
assumption.
Qed.
\end{coq_example}



\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. A good habit is to
provide names for these variables: \Coq will do it anyway, but such
automatic naming decreases readability and robustness.

\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.
\begin{coq_example}
Goal forall A B:Prop, A-> A\/B.
intros.
tauto.
Qed.
\end{coq_example}

\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.
\begin{coq_example}
Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
intros.
congruence.
Qed.
\end{coq_example}


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

Just use the {\tt congruence} tactic.
%\begin{coq_example}
%Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
%intros.
%congruence.
%Qed.
%\end{coq_example}


\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.

\begin{coq_example}
Require Import ZArith.
Require Ring.
Open Local Scope Z_scope.
Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b. 
intros.
ring.
Qed.
\end{coq_example}

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

Just use the {\tt field} tactic.

\begin{coq_example}
Require Import Reals.
Require Ring.
Open Local Scope R_scope.
Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
intros.
field.
assumption.
Qed.
\end{coq_example}


\Question[omega]{My goal is an inequality on R, how can I prove it ?}


%\begin{coq_example}
%Require Import ZArith.
%Require Omega.
%Open Local Scope Z_scope.
%Goal forall a : Z, a*a>0. 
%intros.
%omega.
%Qed.
%\end{coq_example}


\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 gb} tactic.

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

Just use the {\tt apply} tactic.

\begin{coq_example}
Lemma mylemma : forall x, x+0 = x.
auto.
Qed.

Goal 3+0 = 3.
apply mylemma.
Qed.
\end{coq_example}

\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.

\begin{coq_example}
Goal 1=1 -> 1=1.
intro.
assumption.
Qed.
\end{coq_example}

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


\Question[namedintros]{Why should I name my intros ?}

When you use the {\tt intro} tactic you don't have to give a name to your hyphothesis. If you do so the names will be generated by \Coq but your scripts won't be modular. If you add some hyphothesis to your theorem (or change their order), you will have to change your proof to adapt to the new names.


\Question[assert]{I want to state a fact that I will use later as an hypothesis, how can I do it ?}

If you want to use forward reasoning (first proving the fact and then using it) You just need to use the {\tt assert} tactic. If you want to use backward reasoning (proving your goal using an assumption and then proving the assumption) use the {\tt cut} tactic.





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

\Question[abstract]{What can I do when {\tt Qed.} is slow ?}

Sometime you can use the {\tt abstract} tactic, which makes as if you had stated one intermediated lemmas, this speeds up the typing process.  


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

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

\Ltac is the tactic language for \Coq. It provides the user with a
high-level ``toolbox'' for tactic creation.

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

If $x_i$ are identifiers and $e_i$ and $expr$ are tactic expressions, then let reads:
\begin{center}
{\tt let $x_1$:=$e_1$ with $x_2$:=$e_2$\ldots with $x_n$:=$e_n$ in
$expr$}.
\end{center}
Beware that if $expr$ is complex (i.e. features at least a sequence) parenthesis
should be added around it. For example: 
\begin{coq_example}
Ltac twoIntro := let x:=intro in (x;x).
\end{coq_example}

\Question[matchltac]{What is the syntax for pattern matching in \Ltac ?}

Pattern matching on a term $expr$ (non-linear first order unification)
with patterns $p_i$ and tactic expressions $e_i$ reads:
\begin{center}
\hspace{10ex}
{\tt match $expr$ with
\hspace*{2ex}$p_1$ => $e_1$
\hspace*{1ex}\textbar$p_2$ => $e_2$
\hspace*{1ex}\ldots
\hspace*{1ex}\textbar$p_n$ => $e_n$
\hspace*{1ex}\textbar\ \textunderscore\ => $e_{n+1}$
end.
}
\end{center}
Underscore matches all terms.

\Question[matchsem]{What is the semantic for match goal ?}

\Question[fresh]{How can I generate a new name ?}

You can use the following syntax :
{\tt Let id:=fresh in \ldots}\\
For example :
\begin{coq_example}
Ltac introIdGen := let id:=fresh in intro id.
\end{coq_example}

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

A meta variable in \Coq represents a ``hole'', i.e. a part of a proof
that is still unknown. 

\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 this case an inductive type denoting arithmetical
expressions).  For more information see~\cite{howe,harrison,boutin}
and the last chapter of the Coq'Art.


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