path: root/doc/newfaq/main.tex

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

% yay les symboles
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{url}
\usepackage{multicol}
\usepackage{fullpage}
%\usepackage{hevea}
%\usepackage[latin1]{inputenc}
%\usepackage[english]{babel}

%\input{../macros.tex}

\def\Question#1{\stepcounter{question}\subsubsection{#1}}

% version et date
\def\faqversion{0.1}

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

% macro pour les tactics
\def\split{{\tt split }}
\def\assumption{{\tt assumption }}
\def\auto{{\tt auto }}
\def\trivial{{\tt trivial }}
\def\tauto{{\tt tauto }}
\def\left{{\tt left }}
\def\right{{\tt right }}
\def\decompose{{\tt decompose }}
\def\intro{{\tt intro }}
\def\intros{{\tt intros }}
\def\field{{\tt field }}
\def\ring{{\tt ring }}
\def\apply{{\tt apply }}
\def\exact{{\tt exact }}
\def\cut{{\tt cut }}
\def\assert{{\tt assert }}
\def\solve{{\tt solve }}
\def\idtac{{\tt idtac }}
\def\fail{{\tt fail }}
\def\exists{{\tt exists }}
\def\firstorder{{\tt firstorder }}
\def\congruence{{\tt congruence }}
\def\gb{{\tt gb }}
\def\generalize{{\tt generalize }}
\def\abstractt{{\tt abstract }}
\def\eapply{{\tt eapply }}
\def\unfold{{\tt unfold }}
\def\rewrite{{\tt rewrite }}
\def\replace{{\tt replace }}
\def\simpl{{\tt simpl }}
\def\elim{{\tt elim }}
\def\set{{\tt set }}
\def\pose{{\tt pose }}
\def\case{{\tt case }}
\def\destruct{{\tt destruct }}
\def\reflexivity{{\tt reflexivity }}
\def\transitivity{{\tt transitivity }}
\def\symmetry{{\tt symmetry }}
\def\Focus{{\tt Focus }}
\def\discriminate{{\tt discriminate }}
\def\contradiction{{\tt contradiction }}
\def\intuition{{\tt intuition }}
\def\try{{\tt try }}
\def\repeat{{\tt repeat }}
\def\eauto{{\tt eauto }}
\def\subst{{\tt subst }}
\def\instantiate{{\tt instantiate }}
\def\Defined{{\tt Defined }}
\def\Qed{{\tt Qed }}
\def\pattern{{\tt pattern }}




\begin{document}
\bibliographystyle{plain}
\newcounter{question}
\renewcommand{\thesubsubsection}{\arabic{question}}

%%%%%%% Coq pour les nuls %%%%%%%

\title{Coq Version 8.0 for the Clueless\\
  \large(\protect\ref{lastquestion}
  \ Hints)
}
\author{Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux}
\maketitle

%%%%%%%

\begin{abstract}
This note intends to provide an easy way to get acquainted with the
\Coq theorem prover. It tries to formulate appropriate answers
to some of the questions any newcomers 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{What is \Coq ?}\label{whatiscoq} 
The Coq tool is a formal proof management system: a proof done with Coq is mechanically checked by the machine. 
In particular, Coq allows:
\begin{itemize}
    \item the definition of functions or predicates,
    \item to state mathematical theorems and software specifications,
    \item to develop interactively formal proofs of these theorems,
    \item to check these proofs by a small certification "kernel".
\end{itemize}
Coq is based on a logical framework called "Calculus of Inductive Constructions" extended by a modular development system for theories.

\Question{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 Phox 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{What are the other theorem provers ?} 
Many other theorem provers are available for use nowadays. 
Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar
to \Coq by the way they interact with the user. Other relatives of
\Coq are ACL2, Alfa, Elf, Kiv, Mizar, NqThm, $\Omega$mega\ldots


\Question{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{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, \Krakatoa, \Caduceus, to prove
annotated programs written in other languages.

\Question{How many \Coq users are there ?}

Estimation is about 100 regular users.


\Question{How old is \Coq ?}
The first official release of \Coq (v. 4.10) was distributed in 1989.

\Question{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[Helm/Mowgli] A rendering, searching and publishing tool.
\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[Caduceus] A C code certification tool that uses both \Coq and \Why.
\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{What are the academic applications for \Coq ?}

Coq is used by mathematicians for formalizing large parts of mathematics, by teachers, and computer scientists to prove programs and APIs.

\Question{What are the industrial applications for \Coq ?}

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

todo christine compilo lustre ?


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

\section{Documentation}

\Question{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://coq.inria.fr/coq/doc-eng.html}.
All these documents are viewable either in browsable HTML, or as
downloadable postscripts.

\Question{Where can I find this FAQ on the web ?}

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

\Question{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 \texttt{Florent.Kirchner at lix.polytechnique.fr} and \texttt{Julien.Narboux at inria.fr}.

\Question{Is there any mailing list about \Coq ?} 
The main \Coq mailing list is \url{coq-club@coq.inria.fr}, which
broadcasts questions and suggestions about the implementation, the
logical formalism or proof developments. See
\url{http://coq.inria.fr/mailman/listinfo/coq-club} for
subsription. For bugs reports see question \ref{coqbug}.

\Question{Where can I find an archive of the list?}
The archives of the \Coq mailing list are available at
\url{http://coq.inria.fr/pipermail/coq-club}.


\Question{How can I be kept informed of new releases of \Coq ?}

New versions of \Coq are announced on the coq-club mailing list. If you only want to receive information about new releases, you can subscribe to \Coq on \url{http://freshmeat.net/projects/coq/}.


\Question{Is there any book about \Coq ?}
The first book on \Coq, Yves Bertot and Pierre Castéran's Coq'Art has been 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{Where can I find some \Coq examples ?} 

There are examples in the manual~\cite{Coq:manual} and in the
Coq'Art~\cite{Coq:coqart} exercises \url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}.
You can also find large developments using
\Coq in the \Coq user contributions :
\url{http://coq.inria.fr/distrib-eng.html}.

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

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



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

\section{Installation}

\Question{What is the license of \Coq ?}
It is distributed under the GNU Lesser General License (LGPL).

\Question{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}). Development sources can
be accessed via anonymous CVS : \url{http://coqcvs.inria.fr/}

\Question{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{My goal is a conjunction, how can I prove it ?}

Use some theorem or assumption or use the \split tactic.
\begin{coq_example}
Goal forall A B:Prop, A->B-> A/\B.
intros.
split.
assumption.
assumption.
Qed.
\end{coq_example}

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

If you want to decompose your hypothesis into other hypothesis you can use the \decompose tactic :

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


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

You can prove the left part or the right part of the disjunction using
\left or \right tactics. If you want to do a classical
reasoning step, use the {\tt classic} axiom 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}


todo exemple classique et rajouter dans classical prop.


\Question{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 \intro tactic. If there are several
variables you can use the \intros tactic. A good habit is to
provide names for these variables: \Coq will do it anyway, but such
automatic naming decreases legibility and robustness.


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

Use some theorem or assumption or exhibit the witness using the \exists tactic.
\begin{coq_example}
Goal exists x:nat, forall y, x+y=y.
exists 0.
intros.
auto.
Qed.
\end{coq_example}


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

Just use the \apply tactic.

\begin{coq_eval}
Reset Initial.
\end{coq_eval}

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

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



\Question{My goal contains False as an hypotheses, how can I prove it ?}

You can use the \contradiction or \intuition tactics.


\Question{My goal is an equality of two convertible terms, how can I prove it ?}

Just use the \reflexivity tactic.

\begin{coq_example}
Goal forall x, 0+x = x.
intros.
reflexivity.
Qed.
\end{coq_example}

\Question{My goal is a {\tt let x := a in ...}, how can I prove it ?}

Just use the \intro tactic.


\Question{My goal is a {\tt let (a, ..., b) := c in}, how can I prove it ?}

Just use the \destruct c as (a,...,b) tactic.


\Question{My goal contains some existential hypotheses, how can I use it ?}

You can use the tactic \elim with you hypotheses as an argument.

\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses ?}

\begin{verbatim}
Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.
\end{verbatim}


\Question{My goal is an equality, how can I swap the left and right hand terms ?}

Just use the \symmetry tactic.
%\begin{coq_example}
%Goal forall x y : nat, x=y -> y=x.
%intros.
%symmetry.
%assumption.
%Qed.
%\end{coq_example}

\Question{My hypothesis is an equality, how can I swap the left and right hand terms ?}

Just use the \symmetry in tactic.


\Question{My goal is an equality, how can I prove it by transitivity ?}

Just use the \transitivity tactic.
\begin{coq_example}
Goal forall x y z : nat, x=y -> y=z -> x=z.
intros.
transitivity y.
assumption.
assumption.
Qed.
\end{coq_example}


\Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it ?}

You can use {\tt eapply yourtheorem;eauto} but it won't work in all cases ! (for example if more than one hypothesis match one of the subgoals generated by \eapply) so you should rather use  {\tt try solve [eapply yourtheorem;eauto]}, otherwise some metavariables may be incorrectly instantiated.

\begin{coq_example}
Lemma trans : forall x y z : nat, x=y -> y=z -> x=z.
intros.
transitivity y;assumption.
Qed.

Goal forall x y z : nat, x=y -> y=z -> x=z.
intros.
eapply trans;eauto.
Qed.

Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
intros.
eapply trans;eauto.
Undo.
eapply trans.
apply H.
auto.
Qed.

Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
intros.
eapply trans;eauto.
Undo.
try solve [eapply trans;eauto].
eapply trans.
apply H.
auto.
Qed.

\end{coq_example}

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

You can use a what is called a hints' base.

\begin{coq_example}
Require Import ZArith.
Require Ring.
Open Local Scope Z_scope.
Lemma toto1 : 1+1 = 2.
ring.
Qed.
Lemma toto2 : 2+2 = 4.
ring.
Qed.
Lemma toto3 : 2+1 = 3.
ring.
Qed.

Hint Resolve toto1 toto2 toto3 : mybase.

Goal 2+(1+1)=4. 
auto with mybase.
Qed.
\end{coq_example}


\Question{My goal is one of the hypotheses, how can I prove it ?}

Use the \assumption tactic.

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


\Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it ?}

Use the \exact tactic.
\begin{coq_example}
Goal 1=1 -> 1=1 -> 1=1.
intros.
exact H0.
Qed.
\end{coq_example}

\Question{What can be the difference between applying one hypothesis or another in the context of the last question ?}

From a proof point of view it is equivalent but if you want to extract
a program from your proof, the two hypotheses can lead to different
programs.


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

Just use the \tauto tactic.
\begin{coq_example}
Goal forall A B:Prop, A-> (A\/B) /\ A.
intros.
tauto.
Qed.
\end{coq_example}

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

Just use the semi-decision tactic : \firstorder.


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

Just use the \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{My goal is a disequality solvable by a sequence of rewrites, how can I prove it ?}

Just use the \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{My goal is an equality on some ring (e.g. natural numbers), how can I prove it ?}

Just use the \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{My goal is an equality on some field (e.g. real numbers), how can I prove it ?}

Just use the \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{My goal is an inequality on integers in Presburger arithmetic (an expression build from +,-,constants and variables), how can I prove it ?}


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


\Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it ?}

You need the \gb tactic see \url{todo}.

\subsection{Tactics usage}


\Question{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 \assert tactic. If you want to use
backward reasoning (proving your goal using an assumption and then
proving the assumption) use the \cut tactic.

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

You can use \cut followed by \intro or you can use the following \Ltac command :
\begin{verbatim}
Ltac assert_later t := cut t;[intro|idtac]. 
\end{verbatim}

\Question{What is the difference between \Qed and \Defined ?}

These two commands perform type checking, but when \Defined is used the new definition is set as transparent, otherwise it is defined as opaque (see \ref{opaque}).


\Question{How can I know what a tactic does ?}

You can use the {\tt info} command.

\Question{Why \auto does not work ? How can I fix it ?}

You can increase the depth of the proof search or add some lemmas in the base of hints.
Perhaps you may need to use \eauto.

\Question{What is \eauto ?}

This is the same tactic as \auto, but it does some \eapply instead of \apply.

todo les espaces


\Question{How can I speed up \auto ?}

You can use info \auto to replace \auto by the tactics it generates.
You can split your hint bases into smaller ones.


\Question{What is the equivalent of \tauto for classical logic ?}

Currently there are no equivalent tactic for classical logic. You can todo godel


\Question{I want to replace some term with another in the goal, how can I do it ?}

If one of your hypothesis (say {\tt H}) states that the terms are equal you can use the \rewrite tactic. Otherwise you can use the \replace {\tt with} tactic. 

\Question{I want to replace some term with another in an hypothesis, how can I do it ?}

You can use the \rewrite {\tt in} tactic.

\Question{I want to replace some symbol with its definition, how can I do it ?}

You can use the \unfold tactic.

\Question{How can I reduce some term ?}

You can use the \simpl tactic.

\Question{How can I declare a shortcut for some term ?}

You can use the \set or \pose tactics.

\Question{How can I perform case analysis ?}

You can use the \case or \destruct tactics.


\Question{Why should I name my intros ?}

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

\Question{How can I automatize the naming ?}

You can use the {\tt Show Intro.} or  {\tt Show Intros.} commands to generate the names and use your editor to generate a fully named \intro tactic. 
This can be automatized within {\tt xemacs}.

\begin{coq_example}
Goal forall A B C : Prop, A -> B -> C -> A/\B/\C.
Show Intros.
(*
A B C H H0
H1
*)
intros A B C H H0 H1.
repeat split;assumption.
Qed.
\end{coq_example}

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

You need to use the {\tt proof with T} command and add \ldots at the
end of your sentences.

For instance :
\begin{coq_example}
Goal forall A B C : Prop, A -> B/\C -> A/\B/\C.
Proof with assumption.
intros.
split...
Qed.
\end{coq_example}

\Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it ?}

You need to use the \try and \solve tactics. For instance :
\begin{coq_example}
Require Import ZArith.
Require Ring.
Open Local Scope Z_scope.
Goal forall a b c : Z, a+b=b+a.
Proof with try solve [ring].
intros...
Qed.
\end{coq_example}

\Question{How can I do the opposite of the \intro tactic ?}

You can use the \generalize tactic.

\begin{coq_example}
Goal forall A B : Prop, A->B-> A/\B.
intros.
generalize H.
intro.
auto.
Qed.
\end{coq_example}

\Question{One of the hypothesis is an equality between a variable and some term, I want to get rid of this variable, how can I do it ?}

You can use the \subst tactic. This will rewrite the equality everywhere and clear the assumption.

\Question{What can I do if I get ``{\tt generated subgoal term has metavariables in it }'' ?}

You should use the \eapply tactic, this will generate some goals containing metavariables. 

\Question{How can I instantiate some metavariable ?}

Just use the \instantiate tactic.


\Question{What is the use of the \pattern tactic ?}

The \pattern tactic transforms the current goal, performing
beta-expansion on all the applications featuring this tactic's
argument. For instance, if the current goal includes a subterm {\tt
phi(t)}, then {\tt pattern t} transforms the subterm into {\tt (fun
x:A => phi(x)) t}. This can be useful when \apply fails on matching,
to abstract the appropriate terms.

\Question{What is the difference between assert, cut and generalize ?}

PS: Notice for people that are interested in proof rendering that Assert
and Pose (and Cut) are not rendered the same as Generalize (see the
HELM experimental rendering tool at \url{http://mowgli.cs.unibo.it}, link
HELM, link COQ Online). Indeed \generalize builds a beta-expanded term
while \assert, \pose and \cut uses a let-in.

\begin{verbatim}
  (* Goal is T *)
  generalize (H1 H2).
  (* Goal is A->T *)
  ... a proof of A->T ...
\end{verbatim}

is rendered into something like
\begin{verbatim}
  (h) ... the proof of A->T ...
      we proved A->T
  (h0) by (H1 H2) we proved A
  by (h h0) we proved T
\end{verbatim}
while 
\begin{verbatim}
  (* Goal is T *)
  assert q := (H1 H2).
  (* Goal is A *)
  ... a proof of A ...
  (* Goal is A |- T *)
  ... a proof of T ...
\end{verbatim}
is rendered into something like
\begin{verbatim}
  (q) ... the proof of A ...
      we proved A
  ... the proof of T ...
  we proved T
\end{verbatim}
Otherwise said, \generalize is not rendered in a forward-reasoning way,
while \assert is.



\Question{Is there anyway to do pattern matching with dependent types ?}



\section{Proof management}



\Question{How can I change the order of the subgoals ?}

You can use the \Focus command to concentrate on some goal. When the goal is proved you will see the remaining goals.

\Question{How can I change the order of the hypothesis ?}

You can use the {\tt Move ... after} command.

\Question{How can I change the name of an hypothesis ?}

You can use the {\tt Rename ... into} command.

\Question{How can I delete some hypothesis ?}

You can use the {\tt Clear} command.

\Question{How can use a proof which is not finished ?}

You can use the {\tt Admitted} command to state your current proof as an axiom.

\Question{How can I state a conjecture ?}

You can use the {\tt Admitted} command to state your current proof as an axiom.


\Question{What is the difference between a lemma, a fact and a theorem ?}

From \Coq point of view there are no difference. But some tools can
have a different behaviour when you use a lemma rather than a
theorem. For instance {\tt coqdoc} will not generate documentation for
the lemmas within your development.

\Question{How can I organize my proofs ?}

You can organize your proofs using the section mechanism of \Coq. Have
a look at the manual for further information.


\section{Inductive types}


\Question{How can I define a fixpoint when no argument is structurally smaller ?}

todo

\Question{How can I prove that two constructors are different ?}

You can use the \discriminate tactic.

\begin{coq_example}
Inductive toto : Set := | C1 : toto | C2 : toto.
Goal C1 <> C2.
discriminate.
Qed.
\end{coq_example}




\section{Syntax and notations}

\Question{I do not want to type ``forall'' because it is too long, what can I do ?}

You can define your own notation for forall :
\begin{verbatim}
Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).
\end{verbatim}
or if your are using \CoqIde you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}).



\Question{How can I define a notation for square ?}

You can use for instance :
\begin{verbatim}
Notation "x ^2" := (Rmult x x) (at level 20).
\end{verbatim}
Note that you can not use :
\begin{texttt}
Notation "x $^²$" := (Rmult x x) (at level 20).
\end{texttt}
because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.



\section{Modules}




%%%%%%%
\section{\Ltac}

\Question{What is \Ltac ?}

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

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


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

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

\Question{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{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{What is the semantics for match goal ?}

{\tt match goal} matches the current goal against a series of
patterns: {$hyp_1 \ldots hyp_n$ \textbar- $ccl$}. It uses a
first-order unification algorithm, and tries all the possible
combinations of $hyp_i$ before dropping the branch and moving to the
next one. Underscore matches all terms.

\Question{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{How can I access the type of a term ?}

You can use typeof.
todo

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

\section{Tactics writen in Ocaml}

\Question{Can you show me an example of a tactic writen in OCaml ?}

You have some examples of tactics written in Ocaml in the ``contrib'' directory of \Coq sources. 




\section{Case studies}


\Question{How can I define vectors or lists of size n ?}









\section{Publishing tools}

\Question{How can I generate some latex from my development ?}

You can use {\tt coqdoc}.

\Question{How can I generate some HTML from my development ?}

You can use {\tt coqdoc}.

\Question{How can I generate some dependency graph from my development ?}

\Question{How can I cite some \Coq in my latex document ?}

You can use {\tt coq\_tex}.

\Question{How can I cite the \Coq reference manual ?}

You can use this bibtex entry :
\begin{verbatim}
@Manual{Coq:manual,
  title =        {The Coq proof assistant reference manual},
  author =       {\mbox{The Coq development team}},
  organization = {LogiCal Project},
  note =         {Version 8.0},
  year =         {2004},
  url =          "http://coq.inria.fr"
}
\end{verbatim}


\section{\CoqIde}

\Question{What is \CoqIde ?}

\CoqIde is a gtk based gui for \Coq.

\Question{How to enable Emacs keybindings ?}
 Insert \texttt{gtk-key-theme-name = "Emacs"}
    in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
    or in \verb#$HOME# dir. This is done by default.

\Question{How to enable antialiased fonts ?}

 Set the \verb#GDK_USE_XFT# variable to \verb#1#. This is by default with \verb#Gtk >= 2.2#.
    If some of your fonts are not available, set \verb#GDK_USE_XFT# to \verb#0#.

\Question{How to use those Forall and Exists pretty symbols ?}\label{forallcoqide}
 Thanks to the notation features in \Coq, you just need to insert these
lines in your \Coq buffer :
\begin{texttt}
======================================================================\\
Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident).
======================================================================
\end{texttt}
Copy/Paste of these lines from this file will not work outside of \CoqIde.
You need to load a file containing these lines or to enter the "∀" 
using an input method (see \ref{inputmeth}). To try it just use \verb#Require utf8# from inside
\CoqIde. 
To enable these notations automatically start coqide with
\begin{verbatim}
	coqide -l utf8
\end{verbatim}
In the ide subdir of \Coq library, you will find a sample utf8.v with some 
pretty simple notations.

\Question{How to define an input method for non ASCII symbols ?}\label{inputmeth}

\begin{itemize}
\item First solution : type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow. 
	2200 is the hexadecimal code for forall in unicode charts and is encoded as "∀"	
	in UTF-8.
	2203 is for exists. See \url{http://www.unicode.org} for more codes.
\item Second solution : rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists. 
	Under X11, you need to use something like
\begin{verbatim}
		xmodmap -e "keycode  24 = a A F13 F13" 
		xmodmap -e "keycode  26 = e E F14 F14"
\end{verbatim}
	and then to add   
\begin{verbatim}
		bind "F13" {"insert-at-cursor" ("∀")}
		bind "F14" {"insert-at-cursor" ("∃")}
\end{verbatim}
	to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
	The strange ("∀") argument is the UTF-8 encoding for
	0x2200. 
	You can compute these encodings using the lablgtk2 toplevel with 
\begin{verbatim}		
Glib.Utf8.from_unichar 0x2200;;
\end{verbatim}
	Further symbols can be bound on higher Fxx keys or on even on other keys you
	do not need .
\end{itemize}

\Question{How to build a custom \CoqIde with user ml code ?}
 Use 
	coqmktop -ide -byte m1.cmo...mi.cmo
    or 
	coqmktop -ide -opt m1.cmx...mi.cmx

\Question{How to customize the shortcuts for menus ?}
 Two solutions are offered:
\begin{itemize}
\item Edit \$HOME/.coqide.keys by hand or
\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
    from \CoqIde, you may select a menu entry and press the desired 
    shortcut. 
\end{itemize}

\Question{What encoding should I use? What is this x{iiii} in my file?}
 The encoding option is related to the way files are saved. 
 Keep it as UTF-8 until it becomes important for you to exchange files 
 with non UTF-8 aware applications.
 If you choose something else than UTF-8, then missing characters will 
 be encoded by \\x{....} or \\x{........} where each dot is an hex. digit. 
 The number between braces is the hexadecimal UNICODE index for the
  missing character.
    



\section{Extraction}

\Question{What is program extraction ?}

Program extraction consist in generating a program from a constructive proof.

\Question{Which language can I extract to ?}

You can extract your programs to Objective Caml and Haskell.

\Question{How can I extract an incomplete proof ?}

You can provide programs for your axioms.



%%%%%%%
\section{Glossary}

\Question{Can you explain me what an evaluable constant is ?}

An evaluable constant is a constant which is unfoldable.

\Question{What is a goal ?}

The goal is the statement to be proved.

\Question{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{What is Gallina ?}  

Gallina is the specification language of \Coq. Complete documentation
of this language can be found in the Reference Manual.

\Question{What is The Vernacular ?}  

It is the language of commands of Gallina i.e. definitions, lemmas, \ldots  


\Question{What is a dependent type ?}

A dependant type is a type which depends on some term. For instance
``vector of size n'' is a dependant type representing all the vectors
of size $n$. Theis type depends on $n$

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

\Question{What is intuitionnistic logic ?}

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


\Question{What is proof-irrelevance ?}


\Question{What is the difference between opaque and transparent ?}{\label{opaque}}	

Opaque definitions can not be unfolded but transparent ones can.



\section{Troubleshooting}

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

Sometime you can use the \abstractt tactic, which makes as if you had
stated some local lemma, this speeds up the typing process.

\Question{What can I do if I get ``Cannot solve a second-order unification problem'' ?}

You can help coq using the \pattern tactic.



\section{Conclusion and Farewell.}
\label{ccl}

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