path: root/doc/faq/FAQ.tex

\RequirePackage{ifpdf}
\ifpdf   % si on est en pdflatex
\documentclass[a4paper,pdftex]{article}
\else
\documentclass[a4paper]{article}
\fi
\pagestyle{plain}

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

\ifpdf   % si on est en pdflatex
  \usepackage[pdftex]{graphicx}
\else
  \usepackage[dvips]{graphicx}
\fi

%\input{../macros.tex}

% Making hevea happy
%HEVEA \renewcommand{\textbar}{|}
%HEVEA \renewcommand{\textunderscore}{\_}

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

\newcommand{\coqtt}[1]{{\tt #1}}
\newcommand{\coqimp}{{\mbox{\tt ->}}}
\newcommand{\coqequiv}{{\mbox{\tt <->}}}


% 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\existstac{{\tt exists}}
\def\firstorder{{\tt firstorder}}
\def\congruence{{\tt congruence}}
\def\gb{{\tt gb}}
\def\generalize{{\tt generalize}}
\def\abstracttac{{\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\symmetryin{{\tt symmetryin}}
\def\instantiate{{\tt instantiate}}
\def\inversion{{\tt inversion}}
\def\specialize{{\tt specialize}}
\def\Defined{{\tt Defined}}
\def\Qed{{\tt Qed}}
\def\pattern{{\tt pattern}}
\def\Type{{\tt Type}}
\def\Prop{{\tt Prop}}
\def\Set{{\tt Set}}


\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}}
\urldef{\InitWf}\url
  {http://coq.inria.fr/library/Coq.Init.Wf.html}
\urldef{\LogicBerardi}\url
  {http://coq.inria.fr/library/Coq.Logic.Berardi.html}
\urldef{\LogicClassical}\url
  {http://coq.inria.fr/library/Coq.Logic.Classical.html}
\urldef{\LogicClassicalFacts}\url
  {http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html}
\urldef{\LogicClassicalDescription}\url
  {http://coq.inria.fr/library/Coq.Logic.ClassicalDescription.html}
\urldef{\LogicProofIrrelevance}\url
  {http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html}
\urldef{\LogicEqdep}\url
  {http://coq.inria.fr/library/Coq.Logic.Eqdep.html}
\urldef{\LogicEqdepDec}\url
  {http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html}




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

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

\title{Coq Version 8.4 for the Clueless\\
  \large(\protect\ref{lastquestion}
  \ Hints)
}
\author{Pierre Castéran \and 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,
it 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 mathematical objects and programming objects,
    \item to state mathematical theorems and software specifications,
    \item to interactively develop 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{Is {\Coq} a theorem prover?}

{\Coq} comes with decision and semi-decision procedures (
propositional calculus, Presburger's arithmetic, ring and field
simplification, resolution, ...) but the main style for proving
theorems is interactively by using LCF-style tactics.


\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, Agda/Alfa, Twelf, Kiv, Mizar, NqThm, 
\begin{htmlonly}%
Omega\ldots
\end{htmlonly}
\begin{latexonly}%
{$\Omega$}mega\ldots
\end{latexonly}

\Question{What do I have to trust when I see a proof checked by Coq?}

You have to trust:

\begin{description}
\item[The theory behind Coq] The theory of {\Coq} version 8.0 is
generally admitted to be consistent wrt Zermelo-Fraenkel set theory +
inaccessible cardinals. Proofs of consistency of subsystems of the
theory of Coq can be found in the literature.
\item[The Coq kernel implementation] You have to trust that the
implementation of the {\Coq} kernel mirrors the theory behind {\Coq}. The
kernel is intentionally small to limit the risk of conceptual or
accidental implementation bugs.
\item[The Objective Caml compiler] The {\Coq} kernel is written using the
Objective Caml language but it uses only the most standard features
(no object, no label ...), so that it is highly unprobable that an
Objective Caml bug breaks the consistency of {\Coq} without breaking all
other kinds of features of {\Coq} or of other software compiled with
Objective Caml.
\item[Your hardware] In theory, if your hardware does not work
properly, it can accidentally be the case that False becomes
provable. But it is more likely the case that the whole {\Coq} system
will be unusable. You can check your proof using different computers
if you feel the need to.
\item[Your axioms] Your axioms must be consistent with the theory
behind {\Coq}.
\end{description}


\Question{Where can I find information about the theory behind {\Coq}?}
\begin{description}
\item[The Calculus of Inductive Constructions] The
\ahref{http://coq.inria.fr/doc/Reference-Manual006.html}{corresponding}
chapter and the chapter on
\ahref{http://coq.inria.fr/doc/Reference-Manual007.html}{modules} in
the {\Coq} Reference Manual.
\item[Type theory] A book~\cite{ProofsTypes} or some lecture
notes~\cite{Types:Dowek}.
\item[Inductive types]
Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}.
\item[Co-Inductive types]
Eduardo Giménez' thesis~\cite{EGThese}.
\item[Miscellaneous] A
\ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq
\end{description}


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

You can either extract a program from a proof by using the extraction
mechanism or use dedicated tools, such as
\ahref{http://why.lri.fr}{\Why},
\ahref{http://krakatoa.lri.fr}{\Krakatoa},
\ahref{http://why.lri.fr/caduceus/index.en.html}{\Caduceus}, to prove
annotated programs written in other languages.

%\Question{How many {\Coq} users are there?}
%
%An estimation is about 100 regular users.

\Question{How old is {\Coq}?}

The first implementation is from 1985 (it was named {\sf CoC} which is
the acronym of the name of the logic it implemented: the Calculus of
Constructions).  The first official release of {\Coq} (version 4.10)
was distributed in 1989.

\Question{What are the \Coq-related tools?}

There are graphical user interfaces:
\begin{description}
\item[Coqide] A GTK based GUI for \Coq.
\item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing.
\item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files.
\item[Proof General] A emacs mode for {\Coq} and many other proof assistants.
\item[ProofWeb] The ProofWeb online web interface for {\Coq} (and other proof assistants), with a focus on teaching. 
\item[ProverEditor] is an experimental Eclipse plugin with support for {\Coq}. 
\end{description}

There are documentation and browsing tools:

\begin{description}
\item[coq-tex] A tool to insert {\Coq} examples within .tex files. 
\item[coqdoc] A documentation tool for \Coq.
\item[coqgraph] A tool to generate a dependency graph from {\Coq} sources.
\end{description}

There are front-ends for specific languages:

\begin{description}
\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[Zenon] A first-order theorem prover.
\item[Focal] The \ahref{http://focal.inria.fr}{Focal} project aims at building an environment to develop certified computer algebra libraries. 
\item[Concoqtion] is a dependently-typed extension of Objective Caml (and of MetaOCaml) with specifications expressed and proved in Coq. 
\item[Ynot] is an extension of Coq providing a "Hoare Type Theory" for specifying higher-order, imperative and concurrent programs.
\item[Ott]is a tool to translate the descriptions of the syntax and semantics of programming languages to the syntax of Coq, or of other provers.
\end{description}

\Question{What are the high-level tactics of \Coq}

\begin{itemize}
\item Decision of quantifier-free Presburger's Arithmetic
\item Simplification of expressions on rings and fields
\item Decision of closed systems of equations
\item Semi-decision of first-order logic
\item Prolog-style proof search, possibly involving equalities
\end{itemize}

\Question{What are the main libraries available for \Coq}

\begin{itemize}
\item Basic Peano's arithmetic, binary integer numbers, rational numbers,
\item Real analysis,
\item Libraries for lists, boolean, maps, floating-point numbers,
\item Libraries for relations, sets and constructive algebra,
\item Geometry
\end{itemize}


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

{\Coq} is used for formalizing mathematical theories, for teaching,
and for proving properties of algorithms or programs libraries.

The largest mathematical formalization has been done at the University
of Nijmegen (see the
\ahref{http://c-corn.cs.ru.nl}{Constructive Coq
Repository at Nijmegen}).

A symbolic step has also been obtained by formalizing in full a proof
of the Four Color Theorem.

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

{\Coq} is used e.g. to prove properties of the JavaCard system
(especially by Schlumberger and Trusted Logic). It has
also been used to formalize the semantics of the Lucid-Synchrone
data-flow synchronous calculus used by Esterel-Technologies.

\iffalse
todo christine compilo lustre?
\fi

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

\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 
\ahref{http://coq.inria.fr/doc-eng.html}{online}.
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 \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/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 Coq-Club.

\Question{Is there any mailing list about {\Coq}?} 
The main {\Coq} mailing list is \url{coq-club@inria.fr}, which
broadcasts questions and suggestions about the implementation, the
logical formalism or proof developments. See
\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://sympa-roc.inria.fr/wws/info/coq-club}} for
subscription. 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
\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://sympa-roc.inria.fr/wws/arc/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 \ahref{http://freshmeat.net/projects/coq/}{\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 \ahref{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}{\url{http://www.labri.fr/Perso/~casteran/CoqArt/index.html}}.
You can also find large developments using
{\Coq} in the {\Coq} user contributions:
\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}}.

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

You can use the web interface accessible at \ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``contacts''.


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

\section{Installation}

\Question{What is the license of {\Coq}?}
{\Coq} 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
(\ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link
``download''). Development sources can be accessed at
\ahref{http://coq.gforge.inria.fr/}{\url{http://coq.gforge.inria.fr/}}

\Question{On which platform is {\Coq} available?}
Compiled binaries are available for Linux, MacOS X, and Windows. The
sources can be easily compiled on all platforms supporting Objective
Caml.

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

\section{The logic of {\Coq}}

\subsection{General}

\Question{What is the logic of \Coq?}

{\Coq} is based on an axiom-free type theory called
the Calculus of Inductive Constructions (see Coquand \cite{CoHu86},
Luo~\cite{Luo90}
and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order
functions and predicates, inductive and co-inductive datatypes and
predicates, and a stratified hierarchy of sets.

\Question{Is \Coq's logic intuitionistic or classical?}

{\Coq}'s logic is modular. The core logic is intuitionistic
(i.e. excluded-middle $A\vee\neg A$ is not granted by default). It can
be extended to classical logic on demand by requiring an
optional module stating $A\vee\neg A$.

\Question{Can I define non-terminating programs in \Coq?}

All programs in {\Coq} are terminating. Especially, loops
must come with an evidence of their termination. 

Non-terminating programs can be simulated by passing around a
bound on how long the program is allowed to run before dying.

\Question{How is equational reasoning working in {\Coq}?}

 {\Coq} comes with an internal notion of computation called
{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to
$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$
to some expression $t$ converts to the expression $t$ where $x$ is
replaced by $a$). This notion of conversion (which is decidable
because {\Coq} programs are terminating) covers a certain part of
equational reasoning but is limited to sequential evaluation of
expressions of (not necessarily closed) programs. Besides conversion,
equations have to be treated by hand or using specialised tactics.

\subsection{Axioms}

\Question{What axioms can be safely added to {\Coq}?}

There are a few typical useful axioms that are independent from the
Calculus of Inductive Constructions and that are considered consistent with
the theory of {\Coq}.
Most of these axioms are stated in the directory {\tt Logic} of the
standard library of {\Coq}. The most interesting ones are

\begin{itemize}
\item Excluded-middle: $\forall A:Prop, A \vee \neg A$
\item Proof-irrelevance: $\forall A:Prop \forall p_1 p_2:A, p_1=p_2$
\item Unicity of equality proofs (or equivalently Streicher's axiom $K$):
$\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
\item Hilbert's $\epsilon$ operator: if $A \neq \emptyset$, then there is $\epsilon_P$ such that $\exists x P(x) \rightarrow P(\epsilon_P)$
\item Church's $\iota$ operator: if $A \neq \emptyset$, then there is $\iota_P$ such that $\exists! x P(x) \rightarrow P(\iota_P)$
\item The axiom of unique choice: $\forall x \exists! y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
\item The functional axiom of choice: $\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
\item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$
\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
\end{itemize}

Here is a summary of the relative strength of these axioms, most
proofs can be found in directory {\tt Logic} of the standard library.
The justification of their validity relies on the interpretability in
set theory.

%HEVEA\imgsrc{axioms.png}
%BEGIN LATEX
\ifpdf   % si on est en pdflatex
\includegraphics[width=1.0\textwidth]{axioms.png}
\else
\includegraphics[width=1.0\textwidth]{axioms.eps}
\fi
%END LATEX

\Question{What standard axioms are inconsistent with {\Coq}?}

The axiom of unique choice together with classical logic
(e.g. excluded-middle) are inconsistent in the variant of the Calculus
of Inductive Constructions where {\Set} is impredicative.

As a consequence, the functional form of the axiom of choice and
excluded-middle, or any form of the axiom of choice together with
predicate extensionality are inconsistent in the {\Set}-impredicative
version of the Calculus of Inductive Constructions.

The main purpose of the \Set-predicative restriction of the Calculus
of Inductive Constructions is precisely to accommodate these axioms
which are quite standard in mathematical usage.

The $\Set$-predicative system is commonly considered consistent by
interpreting it in a standard set-theoretic boolean model, even with
classical logic, axiom of choice and predicate extensionality added.

\Question{What is Streicher's axiom $K$}
\label{Streicher}

Streicher's axiom $K$~\cite{HofStr98} is an axiom that asserts
dependent elimination of reflexive equality proofs.

\begin{coq_example*}
Axiom Streicher_K :
  forall (A:Type) (x:A) (P: x=x -> Prop),
    P (eq_refl x) -> forall p: x=x, P p.
\end{coq_example*}

In the general case, axiom $K$ is an independent statement of the
Calculus of Inductive Constructions.  However, it is true on decidable
domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also
trivially a consequence of proof-irrelevance (see
\ref{proof-irrelevance}) hence of classical logic.

Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98}

\begin{coq_example*}
Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2.
\end{coq_example*}

Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}

\begin{coq_example*}
Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = eq_refl x.
\end{coq_example*}

Axiom $K$ is also equivalent to 

\begin{coq_example*}
Axiom
  eq_rec_eq :
    forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x),
      p = eq_rect x P p x h.
\end{coq_example*}

It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs).

\begin{coq_example*}
Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) :
forall q:U, P q -> Prop :=
    eq_dep_intro : eq_dep U P p x p x.
Axiom
  eq_dep_eq :
    forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u),
      eq_dep U P u p1 u p2 -> p1 = p2.
\end{coq_example*}

\Question{What is proof-irrelevance}
\label{proof-irrelevance}

A specificity of the Calculus of Inductive Constructions is to permit
statements about proofs. This leads to the question of comparing two
proofs of the same proposition. Identifying all proofs of the same
proposition is called {\em proof-irrelevance}:
$$
\forall A:\Prop, \forall p q:A, p=q
$$ 

Proof-irrelevance (in {\Prop}) can be assumed without contradiction in
{\Coq}. It expresses that only provability matters, whatever the exact
form of the proof is. This is in harmony with the common purely
logical interpretation of {\Prop}. Contrastingly, proof-irrelevance is
inconsistent in {\Set} since there are types in {\Set}, such as the
type of booleans, that provably have at least two distinct elements.

Proof-irrelevance (in {\Prop}) is a consequence of classical logic
(see proofs in file \vfile{\LogicClassical}{Classical} and
\vfile{\LogicBerardi}{Berardi}). Proof-irrelevance is also a
consequence of propositional extensionality (i.e.  \coqtt{(A {\coqequiv} B)
{\coqimp} A=B}, see the proof in file
\vfile{\LogicClassicalFacts}{ClassicalFacts}).

Proof-irrelevance directly implies Streicher's axiom $K$.

\Question{What about functional extensionality?}

Extensionality of functions is admittedly consistent with the
Set-predicative Calculus of Inductive Constructions.

%\begin{coq_example*}
%  Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
%\end{coq_example*}

Let {\tt A}, {\tt B} be types. To deal with extensionality on 
\verb=A->B= without relying on a general extensionality axiom, 
a possible approach is to define one's own extensional equality on
\verb=A->B=.

\begin{coq_eval}
Variables A B : Set.
\end{coq_eval}

\begin{coq_example*}
Definition ext_eq (f g: A->B) := forall x:A, f x = g x.
\end{coq_example*}

and to reason on \verb=A->B= as a setoid (see the Chapter on
Setoids in the Reference Manual).

\Question{Is {\Prop} impredicative?}

Yes, the sort {\Prop} of propositions is {\em
impredicative}. Otherwise said, a statement of the form $\forall
A:Prop, P(A)$ can be instantiated by itself: if $\forall A:\Prop, P(A)$
is provable, then $P(\forall A:\Prop, P(A))$ is.

\Question{Is {\Set} impredicative?}

No, the sort {\Set} lying at the bottom of the hierarchy of
computational types is {\em predicative} in the basic {\Coq} system.
This means that a family of types in {\Set}, e.g. $\forall A:\Set, A
\rightarrow A$, is not a type in {\Set} and it cannot be applied on
itself.

However, the sort {\Set} was impredicative in the original versions of
{\Coq}. For backward compatibility, or for experiments by
knowledgeable users, the logic of {\Coq} can be set impredicative for
{\Set} by calling {\Coq} with the option {\tt -impredicative-set}.

{\Set} has been made predicative from version 8.0 of {\Coq}. The main
reason is to interact smoothly with a classical mathematical world
where both excluded-middle and the axiom of description are valid (see
file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a
proof that excluded-middle and description implies the double negation
of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the
user contribution {\tt Paradoxes} at
\ahref{http://coq.inria.fr/contribs}{\url{http://coq.inria.fr/contribs}}
for a proof that impredicativity of {\Set} implies the simple negation
of excluded-middle in {\Set}).

\Question{Is {\Type} impredicative?}

No, {\Type} is stratified. This is hidden for the
user, but {\Coq} internally maintains a set of constraints ensuring
stratification.

If {\Type} were impredicative then it would be possible to encode
Girard's systems $U-$ and $U$ in {\Coq} and it is known from Girard,
Coquand, Hurkens and Miquel that systems $U-$ and $U$ are inconsistent
[Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding
can be found in file {\tt Logic/Hurkens.v} of {\Coq} standard library.

For instance, when the user see {\tt $\forall$ X:Type, X->X : Type}, each
occurrence of {\Type} is implicitly bound to a different level, say
$\alpha$ and $\beta$ and the actual statement is {\tt
forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint
$\alpha<\beta$.

When a statement violates a constraint, the message {\tt Universe
inconsistency} appears. Example: {\tt fun (x:Type) (y:$\forall$ X:Type, X
{\coqimp} X) => y x x}.

\Question{I have two proofs of the same proposition. Can I prove they are equal?}

In the base {\Coq} system, the answer is generally no. However, if
classical logic is set, the answer is yes for propositions in {\Prop}.
The answer is also yes if proof irrelevance holds (see question
\ref{proof-irrelevance}).

There are also ``simple enough'' propositions for which you can prove
the equality without requiring any extra axioms.  This is typically
the case for propositions defined deterministically as a first-order
inductive predicate on decidable sets. See for instance in question
\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of
the proposition {\tt le m n} (less or equal on {\tt nat}).

%  It is an ongoing work of research to natively include proof
%  irrelevance in {\Coq}.

\Question{I have two proofs of an equality statement. Can I prove they are 
equal?}

 Yes, if equality is decidable on the domain considered (which
is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file
\verb=Eqdep_dec.v=). No otherwise, unless
assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general
assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or
classical logic.

All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}.

\Question{Can I prove that the second components of equal dependent
pairs are equal?}

 The answer is the same as for proofs of equality
statements. It is provable if equality on the domain of the first
component is decidable (look at \verb=inj_right_pair= from file
\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general
case. However, it is consistent (with the Calculus of Constructions)
to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually
provides an axiom (equivalent to Streicher's axiom $K$) which entails
the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).

\subsection{Impredicativity}

\Question{Why {\tt injection} does not work on impredicative {\tt Set}?}

 E.g. in this case (this occurs only in the {\tt Set}-impredicative
 variant of \Coq):

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

\begin{coq_example*}
Inductive I : Type :=
  intro : forall k:Set, k -> I.
Lemma eq_jdef : 
   forall x y:nat, intro _ x = intro _ y -> x = y.
Proof.
   intros x y H; injection H.
\end{coq_example*}

 Injectivity of constructors is restricted to predicative types. If
injectivity on large inductive types were not restricted, we would be
allowed to derive an inconsistency (e.g. following the lines of
Burali-Forti paradox). The question remains open whether injectivity
is consistent on some large inductive types not expressive enough to
encode known paradoxes (such as type I above).


\Question{What is a ``large inductive definition''?}

An inductive definition in {\Prop} or {\Set} is called large
if its constructors embed sets or propositions. As an example, here is
a large inductive type:

\begin{coq_example*}
Inductive sigST (P:Set -> Set) : Type :=
  existST : forall X:Set, P X -> sigST P.
\end{coq_example*}

In the {\tt Set} impredicative variant of {\Coq}, large inductive
definitions in {\tt Set} have restricted elimination schemes to
prevent inconsistencies. Especially, projecting the set or the
proposition content of a large inductive definition is forbidden. If
it were allowed, it would be possible to encode e.g. Burali-Forti
paradox \cite{Gir70,Coq85}.


\Question{Is Coq's logic conservative over Coquand's Calculus of 
Constructions?}

In the {\Set}-impredicative version of the Calculus of Inductive
Constructions (CIC), there are two ways to interpret the Calculus of
Constructions (CC) since the impredicative sort of CC can be
interpreted either as {\Prop} or as {\Set}. In the {\Set}-predicative
CIC, the impredicative sort of CC can only be interpreted as {\Prop}.

If the impredicative sort of CC is interpreted as {\Set}, there is no
conservativity of CIC over CC as the discrimination of
constructors of inductive types in {\Set} transports to a
discrimination of constructors of inductive types encoded
impredicatively. Concretely, considering the impredicative encoding of
Boolean, equality and falsity, we can prove the following CC statement
DISCR in CIC which is not provable in CC, as CC has a
``term-irrelevant'' model.

\begin{coq_example*}
Definition BOOL := forall X:Set, X -> X -> X.
Definition TRUE : BOOL := fun X x1 x2 => x1.
Definition FALSE : BOOL := fun X x1 x2 => x2.
Definition EQBOOL (x1 x2:BOOL) := forall P:BOOL->Set, P x1 -> P x2.
Definition BOT := forall X:Set, X.

Definition BOOL2bool : BOOL -> bool := fun b => b bool true false.

Theorem DISCR : EQBOOL TRUE FALSE -> BOT.
intro X.
assert (H : BOOL2bool TRUE = BOOL2bool FALSE).
{ apply X. trivial. }
discriminate H.
Qed.
\end{coq_example*}

If the impredicative sort of CC is interpreted as {\Prop}, CIC is
presumably conservative over CC. The general idea is that no
proof-relevant information can flow from {\Prop} to {\Set}, even
though singleton elimination can be used. Hence types in {\Set} should
be smashable to the unit type and {\Set} and {\Type} themselves be
mapped to {\Prop}.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\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 disjunction, 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}

An example using classical reasoning:

\begin{coq_example}
Require Import Classical.

Ltac classical_right := 
match goal with 
| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
end.

Ltac classical_left := 
match goal with 
| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
end.


Goal forall A B:Prop, (~A -> B) -> A\/B.
intros.
classical_right.
auto.
Qed.
\end{coq_example}

\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 contains an universally quantified statement, how can I use it?}

If the universally quantified assumption matches the goal you can
use the {\apply} tactic. If it is an equation you can use the
{\rewrite} tactic. Otherwise you can use the {\specialize} tactic
to instantiate the quantified variables with terms. The variant
{\tt assert(Ht := H t)} makes a copy of assumption {\tt H} before
instantiating it.


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

Use some theorem or assumption or exhibit the witness using the {\existstac} 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 hypothesis, 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 {\symmetryin} tactic.

\begin{coq_example}
Goal forall x y : nat, x=y -> y=x.
intros.
symmetry in H.
assumption.
Qed.
\end{coq_example}


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

\iffalse
todo: demander un exemple à Pierre
\fi

\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.
Local Open 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.
Local Open Scope R_scope.
Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1. 
intros.
field.
cut (b*a <>0 -> a<>0).
cut (b*a <>0 -> b<>0).
auto.
auto with real.
auto with real.
Qed.
\end{coq_example}


\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?}


\begin{coq_example}
Require Import ZArith.
Require Omega.
Local Open 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 Loïc Pottier's homepage).

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

\begin{coq_example}
Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
intros.
assert (A->C).
intro;apply H0;apply H;assumption.
apply H2.
assumption.
Qed.

Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C. 
intros.
cut (A->C).
intro.
apply H2;assumption.
intro;apply H0;apply H;assumption.
Qed.
\end{coq_example}




\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 an automation tactic does in my example?}

You can use its {\tt info} variant: info\_auto, info\_trivial, info\_eauto.

\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 relies on {\eapply} instead of \apply.

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

You can use \texttt{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 use Gödel's ``not not'' translation.


\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{How can I prevent the case tactic from losing information ?}

You may want to use the (now standard) {\tt case\_eq} tactic. See the Coq'Art page 159.

\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.
Local Open 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 \ahref{http://helm.cs.unibo.it/library.html}{\url{http://helm.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{What can I do if \Coq can not infer some implicit argument ?}

You can state explicitely what this implicit argument is. See \ref{implicit}.

\Question{How can I explicit some implicit argument ?}\label{implicit}

Just use \texttt{A:=term} where \texttt{A} is the argument.

For instance if you want to use the existence of ``nil'' on nat*nat lists:
\begin{verbatim}
exists (nil (A:=(nat*nat))).
\end{verbatim}

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

todo
\fi

\subsection{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.
You can use the {\tt admit} tactic to omit a portion of a proof.

\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 behavior 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 and Co-inductive types}

\subsection{General}

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

\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?}

Use the {\inversion} tactic.


\Question{How can I prove that 2 terms in an inductive set are equal? Or different?}

Have a look at \coqtt{decide equality} and \coqtt{discriminate} in the \ahref{http://coq.inria.fr/doc/main.html}{Reference Manual}.

\Question{Why is the proof of \coqtt{0+n=n} on natural numbers
trivial but the proof of \coqtt{n+0=n} is not?}

 Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument

\begin{coq_example}
Print plus.
\end{coq_example}

{\noindent} The expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are
considered equal and the theorem \coqtt{0+n=n} is an instance of the
reflexivity of equality. On the other side, \coqtt{n+0} does not
evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is
necessary to trigger the evaluation of \coqtt{+}.

\Question{Why is dependent elimination in Prop not
available by default?}

 
This is just because most of the time it is not needed. To derive a
dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and
apply the elimination scheme using the \verb=using= option of
\verb=elim=, \verb=destruct= or \verb=induction=.


\Question{Argh! I cannot write expressions like ``~{\tt if n <= p then p else n}~'', as in any programming language}
\label{minmax}

The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\

The long answer: That's right, you can't.
If you type for instance the following ``definition'':
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Definition max (n p : nat) := if n <= p then p else n.
\end{coq_example}

As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
statement that belongs to the mathematical world. There are many ways to
prove such a proposition, either by some computation, or using some already
proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
using some theorems on arithmetical operations. If you compute both numbers
before comparing them, you risk to use a lot of time and space.


On the contrary, a function for computing the greatest of two natural numbers
is an algorithm  which, called on two natural numbers
$n$ and $p$, determines wether $n\leq p$ or $p < n$.
Such a function is a \emph{decision  procedure} for the inequality of
 \texttt{nat}.  The possibility of writing such a procedure comes 
directly from de decidability of the order $\leq$ on natural numbers.


When you write a piece of code like 
``~\texttt{if n <= p then \dots{} else \dots}~''
in a
programming language like \emph{ML} or \emph{Java}, a call to such a 
decision procedure is generated. The decision procedure is in general
a primitive function, written in a low-level language, in the correctness
of which you have to trust.

The standard Library of the system \emph{Coq} contains a  
(constructive) proof of decidability of the order $\leq$ on
\texttt{nat} : the function \texttt{le\_lt\_dec} of 
the module \texttt{Compare\_dec} of library \texttt{Arith}.

The following code shows how to define correctly \texttt{min} and
\texttt{max}, and prove some properties of these functions.

\begin{coq_example}
Require Import Compare_dec.

Definition max (n p : nat) := if le_lt_dec n p then p else n.

Definition min (n p : nat) := if le_lt_dec n p then n else p.

Eval compute in (min 4 7).

Theorem min_plus_max : forall n p, min n p + max n p  = n + p.
Proof.
 intros n p; 
 unfold min, max; 
 case (le_lt_dec n p);
 simpl; auto with arith.
Qed.

Theorem max_equiv : forall n p, max n p = p <-> n <= p.
Proof.
 unfold max; intros n p; case (le_lt_dec n p);simpl; auto.
 intuition auto with arith.
 split. 
 intro e; rewrite e; auto with arith.
 intro H; absurd (p < p); eauto with arith.
Qed.
\end{coq_example}

\Question{I wrote my own decision procedure for $\leq$, which
is much  faster than yours, but proving such theorems as
 \texttt{max\_equiv} seems to be quite difficult}

Your code is probably the following one:

\begin{coq_example}
Fixpoint my_le_lt_dec (n p :nat) {struct n}: bool  :=
 match n, p with 0, _ => true
               | S n', S p' => my_le_lt_dec n' p'
               | _   , _    => false
 end.

Definition my_max (n p:nat) := if my_le_lt_dec n p then p else n.

Definition my_min (n p:nat) := if my_le_lt_dec n p then n else p.
\end{coq_example}


For instance, the computation of \texttt{my\_max 567 321} is almost
immediate, whereas one can't wait for  the result of 
\texttt{max 56 32}, using \emph{Coq's} \texttt{le\_lt\_dec}.

This is normal. Your definition is a simple recursive function which
returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
function}, i.e. a complex object, able not only to tell wether $n\leq p$
or $p<n$, but also of building a complete proof of the correct inequality.
What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
and \texttt{max} is the building of a huge proof term.

Nevertheless,  \texttt{le\_lt\_dec} is very useful. Its type 
is a strong specification, using the
\texttt{sumbool} type (look at the reference manual or chapter 9 of
\cite{coqart}). Eliminations of the form
``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of
either $n \leq p$ or $p < n$, allowing easy proofs of some theorems as in
question~\ref{minmax}. Unfortunately, this not the case of your
\texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean
value.


\begin{coq_example}
Check le_lt_dec.
\end{coq_example}

You should keep in mind that \texttt{le\_lt\_dec} is useful to build
certified programs which need to compare natural numbers, and is not
designed to compare quickly two numbers.

Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards 
\emph{OCaml} or \emph{Haskell}, is a reasonable program for comparing two
natural numbers in Peano form in linear time.

It is also possible to keep your boolean function as a decision procedure,
but you have to establish yourself the relationship between \texttt{my\_le\_lt\_dec} and the propositions $n\leq p$ and $p<n$:

\begin{coq_example*}
Theorem my_le_lt_dec_true : 
    forall n p, my_le_lt_dec n p = true <-> n <= p.

Theorem  my_le_lt_dec_false : 
   forall n p, my_le_lt_dec n p = false <-> p < n.
\end{coq_example*}


\subsection{Recursion}

\Question{Why can't I define a non terminating program?}

 Because otherwise the decidability of the type-checking
algorithm (which involves evaluation of programs) is not ensured.  On
another side, if non terminating proofs were allowed, we could get a
proof of {\tt False}:

\begin{coq_example*}
(* This is fortunately not allowed! *)
Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n.
Theorem Paradox : False.
Proof (InfiniteProof O).
\end{coq_example*}


\Question{Why only structurally well-founded loops are allowed?}

 The structural order on inductive types is a simple and
powerful notion of termination. The consistency of the Calculus of
Inductive Constructions relies on it and another consistency proof
would have to be made for stronger termination arguments (such
as the termination of the evaluation of CIC programs themselves!).

In spite of this, all non-pathological termination orders can be mapped
to a structural order. Tools to do this are provided in the file 
\vfile{\InitWf}{Wf} of the standard library of {\Coq}.

\Question{How to define loops based on non structurally smaller
recursive calls?}

 The procedure is as follows (we consider the definition of {\tt
mergesort} as an example).

\begin{itemize}

\item Define the termination order, say {\tt R} on the type {\tt A} of
the arguments of the loop.

\begin{coq_eval}
Open Scope R_scope.
Require Import List.
\end{coq_eval}

\begin{coq_example*}
Definition R (a b:list nat) := length a < length b.
\end{coq_example*}

\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}).

\begin{coq_example*}
Lemma Rwf : well_founded R.
\end{coq_example*}

\item Define the step function (which needs proofs that recursive
calls are on smaller arguments).

\begin{verbatim}
Definition split (l : list nat) 
   : {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
   := (* ... *) .
Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
  let (lH1,lH2) := (split l) in
  let (l1,H1) := lH1 in
  let (l2,H2) := lH2 in
  concat (f l1 H1) (f l2 H2).
\end{verbatim}

\item Define the recursive function by fixpoint on the step function.

\begin{coq_example*}
Definition merge := Fix Rwf (fun _ => list nat) merge_step.
\end{coq_example*}

\end{itemize}

\Question{What is behind the accessibility and well-foundedness proofs?}

 Well-foundedness of some relation {\tt R} on some type {\tt A}
is defined as the accessibility of all elements of {\tt A} along {\tt R}.

\begin{coq_example}
Print well_founded.
Print Acc.
\end{coq_example}

The structure of the accessibility predicate is a well-founded tree
branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'}
less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A}
decreasing along the order {\tt R} are branches in the accessibility
tree. Hence any decreasing along {\tt R} is mapped into a structural
decreasing in the accessibility tree of {\tt R}. This is emphasised in
the definition of {\tt fix} which recurs not on its argument {\tt x:A}
but on the accessibility of this argument along {\tt R}.

See file \vfile{\InitWf}{Wf}.

\Question{How to perform simultaneous double induction?}

 In general a (simultaneous) double induction is simply solved by an
induction on the first hypothesis followed by an inversion over the
second hypothesis. Here is an example

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

\begin{coq_example}
Inductive even : nat -> Prop :=
  | even_O : even 0
  | even_S : forall n:nat, even n -> even (S (S n)).

Inductive odd : nat -> Prop :=
  | odd_SO : odd 1
  | odd_S : forall n:nat, odd n -> odd (S (S n)).

Lemma not_even_and_odd : forall n:nat, even n -> odd n -> False.
induction 1.
  inversion 1.
  inversion 1. apply IHeven; trivial.
\end{coq_example}
\begin{coq_eval}
Qed.
\end{coq_eval}

In case the type of the second induction hypothesis is not
dependent, {\tt inversion} can just be replaced by {\tt destruct}.

\Question{How to define a function by simultaneous double recursion?}

 The same trick applies, you can even use the pattern-matching
compilation algorithm to do the work for you. Here is an example:

\begin{coq_example}
Fixpoint minus (n m:nat) {struct n} : nat :=
  match n, m with
  | O, _ => 0
  | S k, O => S k
  | S k, S l => minus k l
  end.
Print  minus.
\end{coq_example}

In case of dependencies in the type of the induction objects
$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to
the fixpoint definition

\Question{How to perform nested and double induction?}

 To reason by nested (i.e. lexicographic) induction, just reason by
induction on the successive components.

\smallskip

Double induction (or induction on pairs) is a restriction of the
lexicographic induction. Here is an example of double induction.

\begin{coq_example}
Lemma nat_double_ind : 
forall P : nat -> nat -> Prop, P 0 0 -> 
  (forall m n, P m n -> P m (S n)) -> 
  (forall m n, P m n -> P (S m) n) -> 
     forall m n, P m n.
intros P H00 HmS HSn; induction m.
(* case 0 *)
induction n; [assumption | apply HmS; apply IHn].
(* case Sm *)
intro n; apply HSn; apply IHm.
\end{coq_example}
\begin{coq_eval}
Qed.
\end{coq_eval}

\Question{How to define a function by nested recursion?}

 The same trick applies. Here is the example of Ackermann
function.

\begin{coq_example}
Fixpoint ack (n:nat) : nat -> nat :=
  match n with
  | O => S
  | S n' =>
     (fix ack' (m:nat) : nat :=
        match m with
        | O => ack n' 1
        | S m' => ack n' (ack' m')
        end)
  end.
\end{coq_example}


\subsection{Co-inductive types}

\Question{I have a cofixpoint $t:=F(t)$ and I want to prove $t=F(t)$. How to do it?}

Just case-expand $F({\tt t})$ then complete by a trivial case analysis.
Here is what it gives on e.g. the type of streams on naturals

\begin{coq_eval}
Set Implicit Arguments.
\end{coq_eval}
\begin{coq_example}
CoInductive Stream (A:Set) : Set :=
  Cons : A -> Stream A -> Stream A.
CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)).
Lemma Stream_unfold : 
   forall n:nat, nats n = Cons n (nats (S n)).
Proof.
  intro;
  change (nats n = match nats n with
                  | Cons x s => Cons x s
                  end).
  case (nats n); reflexivity.
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{tt}
Notation "x $^²$" := (Rmult x x) (at level 20).
\end{tt}
because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.


\Question{Why ``no associativity'' and  ``left associativity'' at the same level does not work?}

Because we relie on Camlp4 for syntactical analysis and Camlp4 does not really
implement no associativity. By default, non associative operators are defined
as right associative.



\Question{How can I know the associativity associated with a level?}

You can do ``Print Grammar constr'', and decode the output from Camlp4, good luck !

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

The semantics of {\tt match goal} depends on whether it returns
tactics or not.  The {\tt match goal} expression matches the current
goal against a series of patterns: {$hyp_1 {\ldots} hyp_n$ \textbar-
$ccl$}. It uses a first-order unification algorithm and in case of
success, if the right-hand-side is an expression, it tries to type it
while if the right-hand-side is a tactic, it tries to apply it.  If the
typing or the tactic application fails, the {\tt match goal} tries all
the possible combinations of $hyp_i$ before dropping the branch and
moving to the next one. Underscore matches all terms.

\Question{Why can't I use a ``match goal'' returning a tactic in a non
tail-recursive position?}

This is precisely because the semantics of {\tt match goal} is to
apply the tactic on the right as soon as a pattern unifies what is
meaningful only in tail-recursive uses.

The semantics in non tail-recursive call could have been the one used
for terms (i.e. fail if the tactic expression is not typable, but
don't try to apply it). For uniformity of semantics though, this has
been rejected.

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


\iffalse
\Question{How can I access the type of a term?}

You can use typeof.
todo
\fi

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

\section{Tactics written in OCaml}

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

Have a look at the skeleton ``Hello World'' tactic from the next question. 
You also have some examples of tactics written in OCaml in the ``plugins'' directory of {\Coq} sources. 

\Question{Is there a skeleton of OCaml tactic I can reuse somewhere?}

The following steps describe how to write a simplistic ``Hello world'' OCaml
tactic. This takes the form of a dynamically loadable OCaml module, which will
be invoked from the Coq toplevel.
\begin{enumerate}
\item In the \verb+plugins+ directory of the Coq source location, create a
directory \verb+hello+. Proceed to create a grammar and OCaml file, respectively
\verb+plugins/hello/g_hello.ml4+ and \verb+plugins/hello/coq_hello.ml+,
containing:
  \begin{itemize}
  \item in \verb+g_hello.ml4+:
\begin{verbatim}
(*i camlp4deps: "grammar/grammar.cma" i*)
TACTIC EXTEND Hello
| [ "hello" ] -> [ Coq_hello.printHello ]
END
\end{verbatim}
  \item in \verb+coq_hello.ml+:
\begin{verbatim}
let printHello gl =
Tacticals.tclIDTAC_MESSAGE (Pp.str "Hello world") gl
  \end{verbatim}
  \end{itemize}
\item Create a file \verb+plugins/hello/hello_plugin.mllib+, containing the
names of the OCaml modules bundled in the dynamic library:
\begin{verbatim}
Coq_hello
G_hello
\end{verbatim}
\item Append the following lines in \verb+plugins/plugins{byte,opt}.itarget+:
\begin{itemize}
  \item in \verb+pluginsopt.itarget+:
\begin{verbatim}
hello/hello_plugin.cmxa
\end{verbatim}
  \item in \verb+pluginsbyte.itarget+:
\begin{verbatim}
hello/hello_plugin.cma
\end{verbatim}
\end{itemize}
\item In the root directory of the Coq source location, modify the file
\verb+Makefile.common+:
  \begin{itemize}
  \item add \verb+hello+ to the \verb+SRCDIR+ definition (second argument of the
  \verb+addprefix+ function);
  \item in the section ``Object and Source files'', add \verb+HELLOCMA:=plugins/hello/hello_plugin.cma+;
  \item add \verb+$(HELLOCMA)+ to the \verb+PLUGINSCMA+ definition.
  \end{itemize}
\item Modify the file \verb+Makefile.build+, adding in section ``3) plugins'' the
line:
\begin{verbatim}
hello: $(HELLOCMA)
\end{verbatim}
\item From the command line, run \verb+make hello+, then \verb+make plugins/hello/hello_plugin.cmxs+.
\end{enumerate}
The call to the tactic \verb+hello+ from a Coq script has to be preceded by
\verb+Declare ML Module "hello_plugin"+, which will load the dynamic object
\verb+hello_plugin.cmxs+. For instance:
\begin{verbatim}
Declare ML Module "hello_plugin".
Variable A:Prop.
Goal A-> A.
Proof.
hello.
auto.
Qed.
\end{verbatim}


\section{Case studies}

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


\Question{How to prove that 2 sets are different?}

 You need to find a property true on one set and false on the
other one. As an example we show how to prove that {\tt bool} and {\tt
nat} are discriminable. As discrimination property we take the
property to have no more than 2 elements.

\begin{coq_example*}
Theorem nat_bool_discr : bool <> nat.
Proof.
  pose (discr :=
    fun X:Set =>
      ~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))).
  intro Heq; assert (H: discr bool).
  intro H; apply (H true false); destruct x; auto.
  rewrite Heq in H; apply H; clear H.
  destruct a; destruct b as [|n]; intro H0; eauto.
  destruct n; [ apply (H0 2); discriminate | eauto ].
Qed.
\end{coq_example*}

\Question{Is there an axiom-free proof of Streicher's axiom $K$ for
the equality on {\tt nat}?}
\label{K-nat}

Yes, because equality is decidable on {\tt nat}. Here is the proof.

\begin{coq_example*}
Require Import Eqdep_dec.
Require Import Peano_dec.
Theorem K_nat :
  forall (x:nat) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.
Proof.
intros; apply K_dec_set with (p := p).
apply eq_nat_dec.
assumption.
Qed.
\end{coq_example*}

Similarly, we have

\begin{coq_example*}
Theorem eq_rect_eq_nat :
  forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
Proof.
intros; apply K_nat with (p := h); reflexivity.
Qed.
\end{coq_example*}

\Question{How to prove that two proofs of {\tt n<=m} on {\tt nat} are equal?}
\label{le-uniqueness}

This is provable without requiring any axiom because axiom $K$
directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}.

\begin{coq_example*}
Require Import Arith.
Scheme le_ind' := Induction for le Sort Prop.
Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
Proof.
induction p using le_ind'; intro q.
 replace (le_n n) with
  (eq_rect _ (fun n0 => n <= n0) (le_n n) _ eq_refl).
 2:reflexivity.
  generalize (eq_refl n).
    pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
     rewrite <- eq_rect_eq_nat; trivial.
     contradiction (le_Sn_n m); rewrite <- e; assumption.
 replace (le_S n m p) with
  (eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ eq_refl).
 2:reflexivity.
  generalize (eq_refl (S m)).
    pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
     contradiction (le_Sn_n m); rewrite Heq; assumption.
     injection HeqS; intro Heq; generalize l HeqS.
      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
      rewrite (IHp l0); reflexivity.
Qed.
\end{coq_example*}

\Question{How to exploit equalities on sets}

To extract information from an equality on sets, you need to
find a predicate of sets satisfied by the elements of the sets. As an
example, let's consider the following theorem.

\begin{coq_example*}
Theorem interval_discr :
  forall m n:nat,
    {x : nat | x <= m} = {x : nat | x <= n} -> m = n.
\end{coq_example*}

We have a proof requiring the axiom of proof-irrelevance. We
conjecture that proof-irrelevance can be circumvented by introducing a
primitive definition of discrimination of the proofs of
\verb!{x : nat | x <= m}!.

\begin{latexonly}%
The proof can be found in file {\tt interval$\_$discr.v} in this directory.
%Here is the proof
%\begin{small}
%\begin{flushleft}
%\begin{texttt}
%\def_{\ifmmode\sb\else\subscr\fi}
%\include{interval_discr.v}
%%% WARNING semantics of \_ has changed !
%\end{texttt}
%$a\_b\_c$
%\end{flushleft}
%\end{small}
\end{latexonly}%
\begin{htmlonly}%
\ahref{./interval_discr.v}{Here} is the proof.
\end{htmlonly}

\Question{I have a problem of dependent elimination on
proofs, how to solve it?}

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

\begin{coq_example*}
Inductive Def1 : Set := c1 : Def1.
Inductive DefProp : Def1 -> Prop :=
  c2 : forall d:Def1, DefProp d.
Inductive Comb : Set :=
  c3 : forall d:Def1, DefProp d -> Comb.
Lemma eq_comb :
  forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'),
    d1 = d1' -> c3 d1 d2 = c3 d1' d2'.
\end{coq_example*}

 You need to derive the dependent elimination
scheme for DefProp by hand using {\coqtt Scheme}.

\begin{coq_eval}
Abort.
\end{coq_eval}

\begin{coq_example*}
Scheme DefProp_elim := Induction for DefProp Sort Prop.
Lemma eq_comb :
  forall d1 d1':Def1,
    d1 = d1' ->
    forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'.
intros.
destruct H.
destruct d2 using DefProp_elim.
destruct d2' using DefProp_elim.
reflexivity.
Qed.
\end{coq_example*}


\Question{And what if I want to prove the following?}

\begin{coq_example*}
Inductive natProp : nat -> Prop :=
  | p0 : natProp 0
  | pS : forall n:nat, natProp n -> natProp (S n).
Inductive package : Set :=
  pack : forall n:nat, natProp n -> package.
Lemma eq_pack :
 forall n n':nat,
   n = n' ->
   forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
\end{coq_example*}



\begin{coq_eval}
Abort.
\end{coq_eval}
\begin{coq_example*}
Scheme natProp_elim := Induction for natProp Sort Prop.
Definition pack_S : package -> package.
destruct 1.
apply (pack (S n)).
apply pS; assumption.
Defined.
Lemma eq_pack :
  forall n n':nat,
    n = n' ->
    forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
intros n n' Heq np np'.
generalize dependent n'.
induction np using natProp_elim.
induction np' using natProp_elim; intros; auto.
 discriminate Heq.
induction np' using natProp_elim; intros; auto.
 discriminate Heq.
change (pack_S (pack n np) = pack_S (pack n0 np')).
apply (f_equal (A:=package)).
apply IHnp.
auto.
Qed.
\end{coq_example*}







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

You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).

\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.2},
  year =         {2009},
  url =          "http://coq.inria.fr"
}
\end{verbatim}

\Question{Where can I publish my developments in {\Coq}?}

You can submit your developments as a user contribution to the {\Coq}
development team. This ensures its liveness along the evolution and
possible changes of {\Coq}.

You can also submit your developments to the HELM/MoWGLI repository at
the University of Bologna (see
\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}). For
developments submitted in this database, it is possible to visualize
the developments in natural language and execute various retrieving
requests.

\Question{How can I read my proof in natural language?}

You can submit your proof to the HELM/MoWGLI repository and use the
rendering tool provided by the server (see
\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}).

\section{\CoqIde}

\Question{What is {\CoqIde}?}

{\CoqIde} is a gtk based GUI for \Coq.

\Question{How to enable Emacs keybindings?}

If in Gnome, run the gnome configuration editor (\texttt{gconf-editor})
and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category
\texttt{desktop/gnome/interface}.

Otherwise, you need to find where the \verb#gtk-key-theme-name# option is located in
your configuration, and set it to \texttt{Emacs}. Usually, it is in the
\verb#$(HOME)/.gtkrc-2.0# file.


%$ juste pour que la coloration emacs marche

\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{tt}
Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
\end{tt}\\
\begin{tt}
Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident).
\end{tt}

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 $\forall$
using an input method (see \ref{inputmeth}). To try it just use \verb#Require Import 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 \ahref{http://www.unicode.org}{\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, one can add those lines in the file ~/.xmodmaprc :

\begin{verbatim}
! forall
keycode  24 = a A a A U2200 NoSymbol U2200 NoSymbol
! exists
keycode  26 = e E e E U2203 NoSymbol U2203 NoSymbol
\end{verbatim}
and then run xmodmap ~/.xmodmaprc.
\end{itemize}

	Alternatively, you may use an input method editor such as SCIM or iBus.
The latter offers a \LaTeX-like input method.

\Question{How to customize the shortcuts for menus?}
 Two solutions are offered:
\begin{itemize}
\item Edit \verb+$XDG_CONFIG_HOME/coq/coqide.keys+ (which is usually \verb+$HOME/.config/coq/coqide.keys+) by hand or
\item If your system supports it, from \CoqIde, you may select a menu entry and press the desired 
    shortcut. 
\end{itemize}

\Question{What encoding should I use? What is this $\backslash$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 $\backslash$x\{....\} or $\backslash$x\{........\}
 where each dot is an hex. digit. 
 The number between braces is the hexadecimal UNICODE index for the
  missing character.
    
\Question{How to get rid of annoying unwanted automatic templates?}

Some users may experiment problems with unwanted automatic
templates while using Coqide. This is due to a change in the
modifiers keys available through GTK. The straightest way to get
rid of the problem is to edit by hand your coqiderc (either
\verb|/home/<user>/.config/coq/coqiderc| under Linux, or \\
\verb|C:\Documents and Settings\<user>\.config\coq\coqiderc| under Windows) 
    and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.



\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$. Its 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 intuitionistic logic?}

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


\Question{What is proof-irrelevance?}

See question \ref{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 {\abstracttac} tactic, which makes as if you had
stated some local lemma, this speeds up the typing process.

\Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc}?}

The initial state corresponds to the state of \texttt{coqtop} when the interactive
session began. It does not make sense in files to compile.


\Question{What can I do if I get ``No more subgoals but non-instantiated existential variables''?}

This means that {\eauto} or {\eapply} didn't instantiate an
existential variable which eventually got erased by some computation.
You may backtrack to the faulty occurrence of {\eauto} or {\eapply}
and give the missing argument an explicit value. Alternatively, you
can use the commands \texttt{Show Existentials.} and
\texttt{Existential.} to display and instantiate the remainig
existential variables.


\begin{coq_example}
Lemma example_show_existentials :  forall a b c:nat, a=b -> b=c -> a=c.
Proof.
intros.
eapply eq_trans.
Show Existentials.
eassumption.
assumption.
Qed.
\end{coq_example}


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

You can help {\Coq} using the {\pattern} tactic.

\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}

 This is because \texttt{\{x:A|P x\}} is a notation for
\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
$\eta$-conversion, this is different from \texttt{sig P}.


\Question{I copy-paste a term and {\Coq} says it is not convertible
  to the original term. Sometimes it even says the copied term is not
well-typed.}

 This is probably due to invisible implicit information (implicit
arguments, coercions and Cases annotations) in the printed term, which
is not re-synthesised from the copied-pasted term in the same way as
it is in the original term.

  Consider for instance {\tt (@eq Type True True)}. This term is
printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True
True)}. The two terms are not convertible (hence they fool tactics
like {\tt pattern}).

  There is currently no satisfactory answer to the problem. However,
the command {\tt Set Printing All} is useful for diagnosing the
problem.
 
  Due to coercions, one may even face type-checking errors. In some
rare cases, the criterion to hide coercions is a bit too loose, which
may result in a typing error message if the parser is not able to find
again the missing coercion.



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

\Question{What if my question isn't answered here?} 
\label{lastquestion}

Don't panic \verb+:-)+. 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{*********************************************}
\typeout{********* That makes {\thequestion} questions **********}
\typeout{*********************************************}

\end{document}