2
\ifpdf % si on est en pdflatex
3
\documentclass[a4paper,pdftex]{article}
5
\documentclass[a4paper]{article}
13
%\usepackage{multicol}
16
\usepackage[latin1]{inputenc}
17
\usepackage[english]{babel}
19
\ifpdf % si on est en pdflatex
20
\usepackage[pdftex]{graphicx}
22
\usepackage[dvips]{graphicx}
25
%\input{../macros.tex}
28
%HEVEA \renewcommand{\textbar}{|}
29
%HEVEA \renewcommand{\textunderscore}{\_}
31
\def\Question#1{\stepcounter{question}\subsubsection{#1}}
37
\def\Coq{\textsc{Coq}}
38
\def\Why{\textsc{Why}}
39
\def\Caduceus{\textsc{Caduceus}}
40
\def\Krakatoa{\textsc{Krakatoa}}
41
\def\Ltac{\textsc{Ltac}}
42
\def\CoqIde{\textsc{CoqIde}}
44
\newcommand{\coqtt}[1]{{\tt #1}}
45
\newcommand{\coqimp}{{\mbox{\tt ->}}}
46
\newcommand{\coqequiv}{{\mbox{\tt <->}}}
49
% macro pour les tactics
50
\def\split{{\tt split}}
51
\def\assumption{{\tt assumption}}
53
\def\trivial{{\tt trivial}}
54
\def\tauto{{\tt tauto}}
56
\def\right{{\tt right}}
57
\def\decompose{{\tt decompose}}
58
\def\intro{{\tt intro}}
59
\def\intros{{\tt intros}}
60
\def\field{{\tt field}}
62
\def\apply{{\tt apply}}
63
\def\exact{{\tt exact}}
65
\def\assert{{\tt assert}}
66
\def\solve{{\tt solve}}
67
\def\idtac{{\tt idtac}}
69
\def\existstac{{\tt exists}}
70
\def\firstorder{{\tt firstorder}}
71
\def\congruence{{\tt congruence}}
73
\def\generalize{{\tt generalize}}
74
\def\abstracttac{{\tt abstract}}
75
\def\eapply{{\tt eapply}}
76
\def\unfold{{\tt unfold}}
77
\def\rewrite{{\tt rewrite}}
78
\def\replace{{\tt replace}}
79
\def\simpl{{\tt simpl}}
84
\def\destruct{{\tt destruct}}
85
\def\reflexivity{{\tt reflexivity}}
86
\def\transitivity{{\tt transitivity}}
87
\def\symmetry{{\tt symmetry}}
88
\def\Focus{{\tt Focus}}
89
\def\discriminate{{\tt discriminate}}
90
\def\contradiction{{\tt contradiction}}
91
\def\intuition{{\tt intuition}}
93
\def\repeat{{\tt repeat}}
94
\def\eauto{{\tt eauto}}
95
\def\subst{{\tt subst}}
96
\def\symmetryin{{\tt symmetryin}}
97
\def\instantiate{{\tt instantiate}}
98
\def\inversion{{\tt inversion}}
99
\def\Defined{{\tt Defined}}
101
\def\pattern{{\tt pattern}}
102
\def\Type{{\tt Type}}
103
\def\Prop{{\tt Prop}}
107
\newcommand\vfile[2]{\ahref{#1}{\tt {#2}.v}}
109
{http://coq.inria.fr/library/Coq.Init.Wf.html}
110
\urldef{\LogicBerardi}\url
111
{http://coq.inria.fr/library/Coq.Logic.Berardi.html}
112
\urldef{\LogicClassical}\url
113
{http://coq.inria.fr/library/Coq.Logic.Classical.html}
114
\urldef{\LogicClassicalFacts}\url
115
{http://coq.inria.fr/library/Coq.Logic.ClassicalFacts.html}
116
\urldef{\LogicClassicalDescription}\url
117
{http://coq.inria.fr/library/Coq.Logic.ClassicalDescription.html}
118
\urldef{\LogicProofIrrelevance}\url
119
{http://coq.inria.fr/library/Coq.Logic.ProofIrrelevance.html}
120
\urldef{\LogicEqdep}\url
121
{http://coq.inria.fr/library/Coq.Logic.Eqdep.html}
122
\urldef{\LogicEqdepDec}\url
123
{http://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html}
129
\bibliographystyle{plain}
130
\newcounter{question}
131
\renewcommand{\thesubsubsection}{\arabic{question}}
133
%%%%%%% Coq pour les nuls %%%%%%%
135
\title{Coq Version 8.2 for the Clueless\\
136
\large(\protect\ref{lastquestion}
139
\author{Pierre Cast�ran \and Hugo Herbelin \and Florent Kirchner \and Benjamin Monate \and Julien Narboux}
145
This note intends to provide an easy way to get acquainted with the
146
{\Coq} theorem prover. It tries to formulate appropriate answers
147
to some of the questions any newcomers will face, and to give
148
pointers to other references when possible.
153
%\begin{multicols}{2}
161
\section{Introduction}
162
This FAQ is the sum of the questions that came to mind as we developed
163
proofs in \Coq. Since we are singularly short-minded, we wrote the
164
answers we found on bits of papers to have them at hand whenever the
165
situation occurs again. This is pretty much the result of that: a
166
collection of tips one can refer to when proofs become intricate. Yes,
167
this means we won't take the blame for the shortcomings of this
168
FAQ. But if you want to contribute and send in your own question and
169
answers, feel free to write to us\ldots
171
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
173
\section{Presentation}
175
\Question{What is {\Coq}?}\label{whatiscoq}
176
The {\Coq} tool is a formal proof management system: a proof done with {\Coq} is mechanically checked by the machine.
177
In particular, {\Coq} allows:
179
\item the definition of mathematical objects and programming objects,
180
\item to state mathematical theorems and software specifications,
181
\item to interactively develop formal proofs of these theorems,
182
\item to check these proofs by a small certification ``kernel''.
184
{\Coq} is based on a logical framework called ``Calculus of Inductive
185
Constructions'' extended by a modular development system for theories.
187
\Question{Did you really need to name it like that?}
188
Some French computer scientists have a tradition of naming their
189
software as animal species: Caml, Elan, Foc or Phox are examples
190
of this tacit convention. In French, ``coq'' means rooster, and it
191
sounds like the initials of the Calculus of Constructions CoC on which
194
\Question{Is {\Coq} a theorem prover?}
196
{\Coq} comes with decision and semi-decision procedures (
197
propositional calculus, Presburger's arithmetic, ring and field
198
simplification, resolution, ...) but the main style for proving
199
theorems is interactively by using LCF-style tactics.
202
\Question{What are the other theorem provers?}
203
Many other theorem provers are available for use nowadays.
204
Isabelle, HOL, HOL Light, Lego, Nuprl, PVS are examples of provers that are fairly similar
205
to {\Coq} by the way they interact with the user. Other relatives of
206
{\Coq} are ACL2, Agda/Alfa, Twelf, Kiv, Mizar, NqThm,
214
\Question{What do I have to trust when I see a proof checked by Coq?}
219
\item[The theory behind Coq] The theory of {\Coq} version 8.0 is
220
generally admitted to be consistent wrt Zermelo-Fraenkel set theory +
221
inaccessible cardinals. Proofs of consistency of subsystems of the
222
theory of Coq can be found in the literature.
223
\item[The Coq kernel implementation] You have to trust that the
224
implementation of the {\Coq} kernel mirrors the theory behind {\Coq}. The
225
kernel is intentionally small to limit the risk of conceptual or
226
accidental implementation bugs.
227
\item[The Objective Caml compiler] The {\Coq} kernel is written using the
228
Objective Caml language but it uses only the most standard features
229
(no object, no label ...), so that it is highly unprobable that an
230
Objective Caml bug breaks the consistency of {\Coq} without breaking all
231
other kinds of features of {\Coq} or of other software compiled with
233
\item[Your hardware] In theory, if your hardware does not work
234
properly, it can accidentally be the case that False becomes
235
provable. But it is more likely the case that the whole {\Coq} system
236
will be unusable. You can check your proof using different computers
237
if you feel the need to.
238
\item[Your axioms] Your axioms must be consistent with the theory
243
\Question{Where can I find information about the theory behind {\Coq}?}
245
\item[The Calculus of Inductive Constructions] The
246
\ahref{http://coq.inria.fr/doc/Reference-Manual006.html}{corresponding}
247
chapter and the chapter on
248
\ahref{http://coq.inria.fr/doc/Reference-Manual007.html}{modules} in
249
the {\Coq} Reference Manual.
250
\item[Type theory] A book~\cite{ProofsTypes} or some lecture
251
notes~\cite{Types:Dowek}.
252
\item[Inductive types]
253
Christine Paulin-Mohring's habilitation thesis~\cite{Pau96b}.
254
\item[Co-Inductive types]
255
Eduardo Gim�nez' thesis~\cite{EGThese}.
256
\item[Miscellaneous] A
257
\ahref{http://coq.inria.fr/doc/biblio.html}{bibliography} about Coq
261
\Question{How can I use {\Coq} to prove programs?}
263
You can either extract a program from a proof by using the extraction
264
mechanism or use dedicated tools, such as
265
\ahref{http://why.lri.fr}{\Why},
266
\ahref{http://krakatoa.lri.fr}{\Krakatoa},
267
\ahref{http://why.lri.fr/caduceus/index.en.html}{\Caduceus}, to prove
268
annotated programs written in other languages.
270
%\Question{How many {\Coq} users are there?}
272
%An estimation is about 100 regular users.
274
\Question{How old is {\Coq}?}
276
The first implementation is from 1985 (it was named {\sf CoC} which is
277
the acronym of the name of the logic it implemented: the Calculus of
278
Constructions). The first official release of {\Coq} (version 4.10)
279
was distributed in 1989.
281
\Question{What are the \Coq-related tools?}
283
There are graphical user interfaces:
285
\item[Coqide] A GTK based GUI for \Coq.
286
\item[Pcoq] A GUI for {\Coq} with proof by pointing and pretty printing.
287
\item[coqwc] A tool similar to {\tt wc} to count lines in {\Coq} files.
288
\item[Proof General] A emacs mode for {\Coq} and many other proof assistants.
289
\item[ProofWeb] The ProofWeb online web interface for {\Coq} (and other proof assistants), with a focus on teaching.
290
\item[ProverEditor] is an experimental Eclipse plugin with support for {\Coq}.
293
There are documentation and browsing tools:
296
\item[Helm/Mowgli] A rendering, searching and publishing tool.
297
\item[coq-tex] A tool to insert {\Coq} examples within .tex files.
298
\item[coqdoc] A documentation tool for \Coq.
299
\item[coqgraph] A tool to generate a dependency graph from {\Coq} sources.
302
There are front-ends for specific languages:
305
\item[Why] A back-end generator of verification conditions.
306
\item[Krakatoa] A Java code certification tool that uses both {\Coq} and {\Why} to verify the soundness of implementations with regards to the specifications.
307
\item[Caduceus] A C code certification tool that uses both {\Coq} and \Why.
308
\item[Zenon] A first-order theorem prover.
309
\item[Focal] The \ahref{http://focal.inria.fr}{Focal} project aims at building an environment to develop certified computer algebra libraries.
310
\item[Concoqtion] is a dependently-typed extension of Objective Caml (and of MetaOCaml) with specifications expressed and proved in Coq.
311
\item[Ynot] is an extension of Coq providing a "Hoare Type Theory" for specifying higher-order, imperative and concurrent programs.
312
\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.
315
\Question{What are the high-level tactics of \Coq}
318
\item Decision of quantifier-free Presburger's Arithmetic
319
\item Simplification of expressions on rings and fields
320
\item Decision of closed systems of equations
321
\item Semi-decision of first-order logic
322
\item Prolog-style proof search, possibly involving equalities
325
\Question{What are the main libraries available for \Coq}
328
\item Basic Peano's arithmetic, binary integer numbers, rational numbers,
330
\item Libraries for lists, boolean, maps, floating-point numbers,
331
\item Libraries for relations, sets and constructive algebra,
336
\Question{What are the mathematical applications for {\Coq}?}
338
{\Coq} is used for formalizing mathematical theories, for teaching,
339
and for proving properties of algorithms or programs libraries.
341
The largest mathematical formalization has been done at the University
343
\ahref{http://c-corn.cs.ru.nl}{Constructive Coq
344
Repository at Nijmegen}).
346
A symbolic step has also been obtained by formalizing in full a proof
347
of the Four Color Theorem.
349
\Question{What are the industrial applications for {\Coq}?}
351
{\Coq} is used e.g. to prove properties of the JavaCard system
352
(especially by Schlumberger and Trusted Logic). It has
353
also been used to formalize the semantics of the Lucid-Synchrone
354
data-flow synchronous calculus used by Esterel-Technologies.
357
todo christine compilo lustre?
360
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
362
\section{Documentation}
364
\Question{Where can I find documentation about {\Coq}?}
365
All the documentation about \Coq, from the reference manual~\cite{Coq:manual} to
366
friendly tutorials~\cite{Coq:Tutorial} and documentation of the standard library, is available
367
\ahref{http://coq.inria.fr/doc-eng.html}{online}.
368
All these documents are viewable either in browsable HTML, or as
369
downloadable postscripts.
371
\Question{Where can I find this FAQ on the web?}
373
This FAQ is available online at \ahref{http://coq.inria.fr/doc/faq.html}{\url{http://coq.inria.fr/doc/faq.html}}.
375
\Question{How can I submit suggestions / improvements / additions for this FAQ?}
377
This FAQ is unfinished (in the sense that there are some obvious
378
sections that are missing). Please send contributions to Coq-Club.
380
\Question{Is there any mailing list about {\Coq}?}
381
The main {\Coq} mailing list is \url{coq-club@pauillac.inria.fr}, which
382
broadcasts questions and suggestions about the implementation, the
383
logical formalism or proof developments. See
384
\ahref{http://coq.inria.fr/mailman/listinfo/coq-club}{\url{http://pauillac.inria.fr/mailman/listinfo/coq-club}} for
385
subscription. For bugs reports see question \ref{coqbug}.
387
\Question{Where can I find an archive of the list?}
388
The archives of the {\Coq} mailing list are available at
389
\ahref{http://pauillac.inria.fr/pipermail/coq-club}{\url{http://coq.inria.fr/pipermail/coq-club}}.
392
\Question{How can I be kept informed of new releases of {\Coq}?}
394
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/}}.
397
\Question{Is there any book about {\Coq}?}
399
The first book on \Coq, Yves Bertot and Pierre Cast�ran's Coq'Art has been published by Springer-Verlag in 2004:
401
``This book provides a pragmatic introduction to the development of
402
proofs and certified programs using \Coq. With its large collection of
403
examples and exercises it is an invaluable tool for researchers,
404
students, and engineers interested in formal methods and the
405
development of zero-default software.''
408
\Question{Where can I find some {\Coq} examples?}
410
There are examples in the manual~\cite{Coq:manual} and in the
411
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}}.
412
You can also find large developments using
413
{\Coq} in the {\Coq} user contributions:
414
\ahref{http://coq.inria.fr/contribs-eng.html}{\url{http://coq.inria.fr/contribs-eng.html}}.
416
\Question{How can I report a bug?}\label{coqbug}
418
You can use the web interface accessible at \ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link ``contacts''.
421
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
423
\section{Installation}
425
\Question{What is the license of {\Coq}?}
426
{\Coq} is distributed under the GNU Lesser General License
429
\Question{Where can I find the sources of {\Coq}?}
430
The sources of {\Coq} can be found online in the tar.gz'ed packages
431
(\ahref{http://coq.inria.fr}{\url{http://coq.inria.fr}}, link
432
``download''). Development sources can be accessed at
433
\ahref{http://coq.gforge.inria.fr/}{\url{http://coq.gforge.inria.fr/}}
435
\Question{On which platform is {\Coq} available?}
436
Compiled binaries are available for Linux, MacOS X, and Windows. The
437
sources can be easily compiled on all platforms supporting Objective
440
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
442
\section{The logic of {\Coq}}
446
\Question{What is the logic of \Coq?}
448
{\Coq} is based on an axiom-free type theory called
449
the Calculus of Inductive Constructions (see Coquand \cite{CoHu86},
451
and Coquand--Paulin-Mohring \cite{CoPa89}). It includes higher-order
452
functions and predicates, inductive and co-inductive datatypes and
453
predicates, and a stratified hierarchy of sets.
455
\Question{Is \Coq's logic intuitionistic or classical?}
457
{\Coq}'s logic is modular. The core logic is intuitionistic
458
(i.e. excluded-middle $A\vee\neg A$ is not granted by default). It can
459
be extended to classical logic on demand by requiring an
460
optional module stating $A\vee\neg A$.
462
\Question{Can I define non-terminating programs in \Coq?}
464
All programs in {\Coq} are terminating. Especially, loops
465
must come with an evidence of their termination.
467
Non-terminating programs can be simulated by passing around a
468
bound on how long the program is allowed to run before dying.
470
\Question{How is equational reasoning working in {\Coq}?}
472
{\Coq} comes with an internal notion of computation called
473
{\em conversion} (e.g. $(x+1)+y$ is internally equivalent to
474
$(x+y)+1$; similarly applying argument $a$ to a function mapping $x$
475
to some expression $t$ converts to the expression $t$ where $x$ is
476
replaced by $a$). This notion of conversion (which is decidable
477
because {\Coq} programs are terminating) covers a certain part of
478
equational reasoning but is limited to sequential evaluation of
479
expressions of (not necessarily closed) programs. Besides conversion,
480
equations have to be treated by hand or using specialised tactics.
484
\Question{What axioms can be safely added to {\Coq}?}
486
There are a few typical useful axioms that are independent from the
487
Calculus of Inductive Constructions and that are considered consistent with
488
the theory of {\Coq}.
489
Most of these axioms are stated in the directory {\tt Logic} of the
490
standard library of {\Coq}. The most interesting ones are
493
\item Excluded-middle: $\forall A:Prop, A \vee \neg A$
494
\item Proof-irrelevance: $\forall A:Prop \forall p_1 p_2:A, p_1=p_2$
495
\item Unicity of equality proofs (or equivalently Streicher's axiom $K$):
496
$\forall A \forall x y:A \forall p_1 p_2:x=y, p_1=p_2$
497
\item Hilbert's $\epsilon$ operator: if $A \neq \emptyset$, then there is $\epsilon_P$ such that $\exists x P(x) \rightarrow P(\epsilon_P)$
498
\item Church's $\iota$ operator: if $A \neq \emptyset$, then there is $\iota_P$ such that $\exists! x P(x) \rightarrow P(\iota_P)$
499
\item The axiom of unique choice: $\forall x \exists! y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
500
\item The functional axiom of choice: $\forall x \exists y R(x,y) \rightarrow \exists f \forall x R(x,f(x))$
501
\item Extensionality of predicates: $\forall P Q:A\rightarrow Prop, (\forall x, P(x) \leftrightarrow Q(x)) \rightarrow P=Q$
502
\item Extensionality of functions: $\forall f g:A\rightarrow B, (\forall x, f(x)=g(x)) \rightarrow f=g$
505
Here is a summary of the relative strength of these axioms, most
506
proofs can be found in directory {\tt Logic} of the standard library.
507
The justification of their validity relies on the interpretability in
510
%HEVEA\imgsrc{axioms.png}
512
\ifpdf % si on est en pdflatex
513
\includegraphics[width=1.0\textwidth]{axioms.png}
515
\includegraphics[width=1.0\textwidth]{axioms.eps}
519
\Question{What standard axioms are inconsistent with {\Coq}?}
521
The axiom of unique choice together with classical logic
522
(e.g. excluded-middle) are inconsistent in the variant of the Calculus
523
of Inductive Constructions where {\Set} is impredicative.
525
As a consequence, the functional form of the axiom of choice and
526
excluded-middle, or any form of the axiom of choice together with
527
predicate extensionality are inconsistent in the {\Set}-impredicative
528
version of the Calculus of Inductive Constructions.
530
The main purpose of the \Set-predicative restriction of the Calculus
531
of Inductive Constructions is precisely to accommodate these axioms
532
which are quite standard in mathematical usage.
534
The $\Set$-predicative system is commonly considered consistent by
535
interpreting it in a standard set-theoretic boolean model, even with
536
classical logic, axiom of choice and predicate extensionality added.
538
\Question{What is Streicher's axiom $K$}
541
Streicher's axiom $K$~\cite{HofStr98} is an axiom that asserts
542
dependent elimination of reflexive equality proofs.
546
forall (A:Type) (x:A) (P: x=x -> Prop),
547
P (refl_equal x) -> forall p: x=x, P p.
550
In the general case, axiom $K$ is an independent statement of the
551
Calculus of Inductive Constructions. However, it is true on decidable
552
domains (see file \vfile{\LogicEqdepDec}{Eqdep\_dec}). It is also
553
trivially a consequence of proof-irrelevance (see
554
\ref{proof-irrelevance}) hence of classical logic.
556
Axiom $K$ is equivalent to {\em Uniqueness of Identity Proofs} \cite{HofStr98}
559
Axiom UIP : forall (A:Set) (x y:A) (p1 p2: x=y), p1 = p2.
562
Axiom $K$ is also equivalent to {\em Uniqueness of Reflexive Identity Proofs} \cite{HofStr98}
565
Axiom UIP_refl : forall (A:Set) (x:A) (p: x=x), p = refl_equal x.
568
Axiom $K$ is also equivalent to
573
forall (A:Set) (x:A) (P: A->Set) (p:P x) (h: x=x),
574
p = eq_rect x P p x h.
577
It is also equivalent to the injectivity of dependent equality (dependent equality is itself equivalent to equality of dependent pairs).
580
Inductive eq_dep (U:Set) (P:U -> Set) (p:U) (x:P p) :
581
forall q:U, P q -> Prop :=
582
eq_dep_intro : eq_dep U P p x p x.
585
forall (U:Set) (u:U) (P:U -> Set) (p1 p2:P u),
586
eq_dep U P u p1 u p2 -> p1 = p2.
589
\Question{What is proof-irrelevance}
590
\label{proof-irrelevance}
592
A specificity of the Calculus of Inductive Constructions is to permit
593
statements about proofs. This leads to the question of comparing two
594
proofs of the same proposition. Identifying all proofs of the same
595
proposition is called {\em proof-irrelevance}:
597
\forall A:\Prop, \forall p q:A, p=q
600
Proof-irrelevance (in {\Prop}) can be assumed without contradiction in
601
{\Coq}. It expresses that only provability matters, whatever the exact
602
form of the proof is. This is in harmony with the common purely
603
logical interpretation of {\Prop}. Contrastingly, proof-irrelevance is
604
inconsistent in {\Set} since there are types in {\Set}, such as the
605
type of booleans, that provably have at least two distinct elements.
607
Proof-irrelevance (in {\Prop}) is a consequence of classical logic
608
(see proofs in file \vfile{\LogicClassical}{Classical} and
609
\vfile{\LogicBerardi}{Berardi}). Proof-irrelevance is also a
610
consequence of propositional extensionality (i.e. \coqtt{(A {\coqequiv} B)
611
{\coqimp} A=B}, see the proof in file
612
\vfile{\LogicClassicalFacts}{ClassicalFacts}).
614
Proof-irrelevance directly implies Streicher's axiom $K$.
616
\Question{What about functional extensionality?}
618
Extensionality of functions is admittedly consistent with the
619
Set-predicative Calculus of Inductive Constructions.
621
%\begin{coq_example*}
622
% Axiom extensionality : (A,B:Set)(f,g:(A->B))(x:A)(f x)=(g x)->f=g.
625
Let {\tt A}, {\tt B} be types. To deal with extensionality on
626
\verb=A->B= without relying on a general extensionality axiom,
627
a possible approach is to define one's own extensional equality on
635
Definition ext_eq (f g: A->B) := forall x:A, f x = g x.
638
and to reason on \verb=A->B= as a setoid (see the Chapter on
639
Setoids in the Reference Manual).
641
\Question{Is {\Prop} impredicative?}
643
Yes, the sort {\Prop} of propositions is {\em
644
impredicative}. Otherwise said, a statement of the form $\forall
645
A:Prop, P(A)$ can be instantiated by itself: if $\forall A:\Prop, P(A)$
646
is provable, then $P(\forall A:\Prop, P(A))$ is.
648
\Question{Is {\Set} impredicative?}
650
No, the sort {\Set} lying at the bottom of the hierarchy of
651
computational types is {\em predicative} in the basic {\Coq} system.
652
This means that a family of types in {\Set}, e.g. $\forall A:\Set, A
653
\rightarrow A$, is not a type in {\Set} and it cannot be applied on
656
However, the sort {\Set} was impredicative in the original versions of
657
{\Coq}. For backward compatibility, or for experiments by
658
knowledgeable users, the logic of {\Coq} can be set impredicative for
659
{\Set} by calling {\Coq} with the option {\tt -impredicative-set}.
661
{\Set} has been made predicative from version 8.0 of {\Coq}. The main
662
reason is to interact smoothly with a classical mathematical world
663
where both excluded-middle and the axiom of description are valid (see
664
file \vfile{\LogicClassicalDescription}{ClassicalDescription} for a
665
proof that excluded-middle and description implies the double negation
666
of excluded-middle in {\Set} and file {\tt Hurkens\_Set.v} from the
667
user contribution {\tt Rocq/PARADOXES} for a proof that
668
impredicativity of {\Set} implies the simple negation of
669
excluded-middle in {\Set}).
671
\Question{Is {\Type} impredicative?}
673
No, {\Type} is stratified. This is hidden for the
674
user, but {\Coq} internally maintains a set of constraints ensuring
677
If {\Type} were impredicative then it would be possible to encode
678
Girard's systems $U-$ and $U$ in {\Coq} and it is known from Girard,
679
Coquand, Hurkens and Miquel that systems $U-$ and $U$ are inconsistent
680
[Girard 1972, Coquand 1991, Hurkens 1993, Miquel 2001]. This encoding
681
can be found in file {\tt Logic/Hurkens.v} of {\Coq} standard library.
683
For instance, when the user see {\tt $\forall$ X:Type, X->X : Type}, each
684
occurrence of {\Type} is implicitly bound to a different level, say
685
$\alpha$ and $\beta$ and the actual statement is {\tt
686
forall X:Type($\alpha$), X->X : Type($\beta$)} with the constraint
689
When a statement violates a constraint, the message {\tt Universe
690
inconsistency} appears. Example: {\tt fun (x:Type) (y:$\forall$ X:Type, X
691
{\coqimp} X) => y x x}.
693
\Question{I have two proofs of the same proposition. Can I prove they are equal?}
695
In the base {\Coq} system, the answer is generally no. However, if
696
classical logic is set, the answer is yes for propositions in {\Prop}.
697
The answer is also yes if proof irrelevance holds (see question
698
\ref{proof-irrelevance}).
700
There are also ``simple enough'' propositions for which you can prove
701
the equality without requiring any extra axioms. This is typically
702
the case for propositions defined deterministically as a first-order
703
inductive predicate on decidable sets. See for instance in question
704
\ref{le-uniqueness} an axiom-free proof of the unicity of the proofs of
705
the proposition {\tt le m n} (less or equal on {\tt nat}).
707
% It is an ongoing work of research to natively include proof
708
% irrelevance in {\Coq}.
710
\Question{I have two proofs of an equality statement. Can I prove they are
713
Yes, if equality is decidable on the domain considered (which
714
is the case for {\tt nat}, {\tt bool}, etc): see {\Coq} file
715
\verb=Eqdep_dec.v=). No otherwise, unless
716
assuming Streicher's axiom $K$ (see \cite{HofStr98}) or a more general
717
assumption such as proof-irrelevance (see \ref{proof-irrelevance}) or
720
All of these statements can be found in file \vfile{\LogicEqdep}{Eqdep}.
722
\Question{Can I prove that the second components of equal dependent
725
The answer is the same as for proofs of equality
726
statements. It is provable if equality on the domain of the first
727
component is decidable (look at \verb=inj_right_pair= from file
728
\vfile{\LogicEqdepDec}{Eqdep\_dec}), but not provable in the general
729
case. However, it is consistent (with the Calculus of Constructions)
730
to assume it is true. The file \vfile{\LogicEqdep}{Eqdep} actually
731
provides an axiom (equivalent to Streicher's axiom $K$) which entails
732
the result (look at \verb=inj_pair2= in \vfile{\LogicEqdep}{Eqdep}).
734
\subsection{Impredicativity}
736
\Question{Why {\tt injection} does not work on impredicative {\tt Set}?}
738
E.g. in this case (this occurs only in the {\tt Set}-impredicative
746
Inductive I : Type :=
747
intro : forall k:Set, k -> I.
749
forall x y:nat, intro _ x = intro _ y -> x = y.
751
intros x y H; injection H.
754
Injectivity of constructors is restricted to predicative types. If
755
injectivity on large inductive types were not restricted, we would be
756
allowed to derive an inconsistency (e.g. following the lines of
757
Burali-Forti paradox). The question remains open whether injectivity
758
is consistent on some large inductive types not expressive enough to
759
encode known paradoxes (such as type I above).
762
\Question{What is a ``large inductive definition''?}
764
An inductive definition in {\Prop} or {\Set} is called large
765
if its constructors embed sets or propositions. As an example, here is
766
a large inductive type:
769
Inductive sigST (P:Set -> Set) : Type :=
770
existST : forall X:Set, P X -> sigST P.
773
In the {\tt Set} impredicative variant of {\Coq}, large inductive
774
definitions in {\tt Set} have restricted elimination schemes to
775
prevent inconsistencies. Especially, projecting the set or the
776
proposition content of a large inductive definition is forbidden. If
777
it were allowed, it would be possible to encode e.g. Burali-Forti
778
paradox \cite{Gir70,Coq85}.
781
\Question{Is Coq's logic conservative over Coquand's Calculus of
784
Yes for the non Set-impredicative version of the Calculus of Inductive
785
Constructions. Indeed, the impredicative sort of the Calculus of
786
Constructions can only be interpreted as the sort {\Prop} since {\Set}
787
is predicative. But {\Prop} can be
790
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
791
\section{Talkin' with the Rooster}
795
\subsection{My goal is ..., how can I prove it?}
798
\Question{My goal is a conjunction, how can I prove it?}
800
Use some theorem or assumption or use the {\split} tactic.
802
Goal forall A B:Prop, A->B-> A/\B.
810
\Question{My goal contains a conjunction as an hypothesis, how can I use it?}
812
If you want to decompose your hypothesis into other hypothesis you can use the {\decompose} tactic:
815
Goal forall A B:Prop, A/\B-> B.
823
\Question{My goal is a disjunction, how can I prove it?}
825
You can prove the left part or the right part of the disjunction using
826
{\left} or {\right} tactics. If you want to do a classical
827
reasoning step, use the {\tt classic} axiom to prove the right part with the assumption
828
that the left part of the disjunction is false.
831
Goal forall A B:Prop, A-> A\/B.
838
An example using classical reasoning:
841
Require Import Classical.
843
Ltac classical_right :=
845
| _:_ |-?X1 \/ _ => (elim (classic X1);intro;[left;trivial|right])
848
Ltac classical_left :=
850
| _:_ |- _ \/?X1 => (elim (classic X1);intro;[right;trivial|left])
854
Goal forall A B:Prop, (~A -> B) -> A\/B.
861
\Question{My goal is an universally quantified statement, how can I prove it?}
863
Use some theorem or assumption or introduce the quantified variable in
864
the context using the {\intro} tactic. If there are several
865
variables you can use the {\intros} tactic. A good habit is to
866
provide names for these variables: {\Coq} will do it anyway, but such
867
automatic naming decreases legibility and robustness.
870
\Question{My goal is an existential, how can I prove it?}
872
Use some theorem or assumption or exhibit the witness using the {\existstac} tactic.
874
Goal exists x:nat, forall y, x+y=y.
882
\Question{My goal is solvable by some lemma, how can I prove it?}
884
Just use the {\apply} tactic.
891
Lemma mylemma : forall x, x+0 = x.
902
\Question{My goal contains False as an hypothesis, how can I prove it?}
904
You can use the {\contradiction} or {\intuition} tactics.
907
\Question{My goal is an equality of two convertible terms, how can I prove it?}
909
Just use the {\reflexivity} tactic.
912
Goal forall x, 0+x = x.
918
\Question{My goal is a {\tt let x := a in ...}, how can I prove it?}
920
Just use the {\intro} tactic.
923
\Question{My goal is a {\tt let (a, ..., b) := c in}, how can I prove it?}
925
Just use the {\destruct} c as (a,...,b) tactic.
928
\Question{My goal contains some existential hypotheses, how can I use it?}
930
You can use the tactic {\elim} with you hypotheses as an argument.
932
\Question{My goal contains some existential hypotheses, how can I use it and decompose my knowledge about this new thing into different hypotheses?}
935
Ltac DecompEx H P := elim H;intro P;intro TO;decompose [and] TO;clear TO;clear H.
939
\Question{My goal is an equality, how can I swap the left and right hand terms?}
941
Just use the {\symmetry} tactic.
943
Goal forall x y : nat, x=y -> y=x.
950
\Question{My hypothesis is an equality, how can I swap the left and right hand terms?}
952
Just use the {\symmetryin} tactic.
955
Goal forall x y : nat, x=y -> y=x.
963
\Question{My goal is an equality, how can I prove it by transitivity?}
965
Just use the {\transitivity} tactic.
967
Goal forall x y z : nat, x=y -> y=z -> x=z.
976
\Question{My goal would be solvable using {\tt apply;assumption} if it would not create meta-variables, how can I prove it?}
978
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.
981
Lemma trans : forall x y z : nat, x=y -> y=z -> x=z.
983
transitivity y;assumption.
986
Goal forall x y z : nat, x=y -> y=z -> x=z.
991
Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
1000
Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z.
1004
try solve [eapply trans;eauto].
1012
\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?}
1014
You can use a what is called a hints' base.
1017
Require Import ZArith.
1019
Open Local Scope Z_scope.
1020
Lemma toto1 : 1+1 = 2.
1023
Lemma toto2 : 2+2 = 4.
1026
Lemma toto3 : 2+1 = 3.
1030
Hint Resolve toto1 toto2 toto3 : mybase.
1038
\Question{My goal is one of the hypotheses, how can I prove it?}
1040
Use the {\assumption} tactic.
1050
\Question{My goal appears twice in the hypotheses and I want to choose which one is used, how can I do it?}
1052
Use the {\exact} tactic.
1054
Goal 1=1 -> 1=1 -> 1=1.
1060
\Question{What can be the difference between applying one hypothesis or another in the context of the last question?}
1062
From a proof point of view it is equivalent but if you want to extract
1063
a program from your proof, the two hypotheses can lead to different
1067
\Question{My goal is a propositional tautology, how can I prove it?}
1069
Just use the {\tauto} tactic.
1071
Goal forall A B:Prop, A-> (A\/B) /\ A.
1077
\Question{My goal is a first order formula, how can I prove it?}
1079
Just use the semi-decision tactic: \firstorder.
1082
todo: demander un exemple � Pierre
1085
\Question{My goal is solvable by a sequence of rewrites, how can I prove it?}
1087
Just use the {\congruence} tactic.
1089
Goal forall a b c d e, a=d -> b=e -> c+b=d -> c+e=a.
1096
\Question{My goal is a disequality solvable by a sequence of rewrites, how can I prove it?}
1098
Just use the {\congruence} tactic.
1101
Goal forall a b c d, a<>d -> b=a -> d=c+b -> b<>c+b.
1108
\Question{My goal is an equality on some ring (e.g. natural numbers), how can I prove it?}
1110
Just use the {\ring} tactic.
1113
Require Import ZArith.
1115
Open Local Scope Z_scope.
1116
Goal forall a b : Z, (a+b)*(a+b) = a*a + 2*a*b + b*b.
1122
\Question{My goal is an equality on some field (e.g. real numbers), how can I prove it?}
1124
Just use the {\field} tactic.
1127
Require Import Reals.
1129
Open Local Scope R_scope.
1130
Goal forall a b : R, b*a<>0 -> (a/b) * (b/a) = 1.
1133
cut (b*a <>0 -> a<>0).
1134
cut (b*a <>0 -> b<>0).
1142
\Question{My goal is an inequality on integers in Presburger's arithmetic (an expression build from +,-,constants and variables), how can I prove it?}
1146
Require Import ZArith.
1148
Open Local Scope Z_scope.
1149
Goal forall a : Z, a>0 -> a+a > a.
1156
\Question{My goal is an equation solvable using equational hypothesis on some ring (e.g. natural numbers), how can I prove it?}
1158
You need the {\gb} tactic (see Lo�c Pottier's homepage).
1160
\subsection{Tactics usage}
1162
\Question{I want to state a fact that I will use later as an hypothesis, how can I do it?}
1164
If you want to use forward reasoning (first proving the fact and then
1165
using it) you just need to use the {\assert} tactic. If you want to use
1166
backward reasoning (proving your goal using an assumption and then
1167
proving the assumption) use the {\cut} tactic.
1170
Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C.
1173
intro;apply H0;apply H;assumption.
1178
Goal forall A B C D : Prop, (A -> B) -> (B->C) -> A -> C.
1182
apply H2;assumption.
1183
intro;apply H0;apply H;assumption.
1190
\Question{I want to state a fact that I will use later as an hypothesis and prove it later, how can I do it?}
1192
You can use {\cut} followed by {\intro} or you can use the following {\Ltac} command:
1194
Ltac assert_later t := cut t;[intro|idtac].
1197
\Question{What is the difference between {\Qed} and {\Defined}?}
1199
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}).
1202
\Question{How can I know what a tactic does?}
1204
You can use the {\tt info} command.
1208
\Question{Why {\auto} does not work? How can I fix it?}
1210
You can increase the depth of the proof search or add some lemmas in the base of hints.
1211
Perhaps you may need to use \eauto.
1213
\Question{What is {\eauto}?}
1215
This is the same tactic as \auto, but it relies on {\eapply} instead of \apply.
1217
\Question{How can I speed up {\auto}?}
1219
You can use \texttt{info }{\auto} to replace {\auto} by the tactics it generates.
1220
You can split your hint bases into smaller ones.
1223
\Question{What is the equivalent of {\tauto} for classical logic?}
1225
Currently there are no equivalent tactic for classical logic. You can use G�del's ``not not'' translation.
1228
\Question{I want to replace some term with another in the goal, how can I do it?}
1230
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.
1232
\Question{I want to replace some term with another in an hypothesis, how can I do it?}
1234
You can use the {\rewrite} {\tt in} tactic.
1236
\Question{I want to replace some symbol with its definition, how can I do it?}
1238
You can use the {\unfold} tactic.
1240
\Question{How can I reduce some term?}
1242
You can use the {\simpl} tactic.
1244
\Question{How can I declare a shortcut for some term?}
1246
You can use the {\set} or {\pose} tactics.
1248
\Question{How can I perform case analysis?}
1250
You can use the {\case} or {\destruct} tactics.
1252
\Question{How can I prevent the case tactic from losing information ?}
1254
You may want to use the (now standard) {\tt case\_eq} tactic. See the Coq'Art page 159.
1256
\Question{Why should I name my intros?}
1258
When you use the {\intro} tactic you don't have to give a name to your
1259
hypothesis. If you do so the name will be generated by {\Coq} but your
1260
scripts may be less robust. If you add some hypothesis to your theorem
1261
(or change their order), you will have to change your proof to adapt
1264
\Question{How can I automatize the naming?}
1266
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.
1267
This can be automatized within {\tt xemacs}.
1270
Goal forall A B C : Prop, A -> B -> C -> A/\B/\C.
1276
intros A B C H H0 H1.
1277
repeat split;assumption.
1281
\Question{I want to automatize the use of some tactic, how can I do it?}
1283
You need to use the {\tt proof with T} command and add {\ldots} at the
1284
end of your sentences.
1288
Goal forall A B C : Prop, A -> B/\C -> A/\B/\C.
1289
Proof with assumption.
1295
\Question{I want to execute the {\texttt proof with} tactic only if it solves the goal, how can I do it?}
1297
You need to use the {\try} and {\solve} tactics. For instance:
1299
Require Import ZArith.
1301
Open Local Scope Z_scope.
1302
Goal forall a b c : Z, a+b=b+a.
1303
Proof with try solve [ring].
1308
\Question{How can I do the opposite of the {\intro} tactic?}
1310
You can use the {\generalize} tactic.
1313
Goal forall A B : Prop, A->B-> A/\B.
1321
\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?}
1323
You can use the {\subst} tactic. This will rewrite the equality everywhere and clear the assumption.
1325
\Question{What can I do if I get ``{\tt generated subgoal term has metavariables in it }''?}
1327
You should use the {\eapply} tactic, this will generate some goals containing metavariables.
1329
\Question{How can I instantiate some metavariable?}
1331
Just use the {\instantiate} tactic.
1334
\Question{What is the use of the {\pattern} tactic?}
1336
The {\pattern} tactic transforms the current goal, performing
1337
beta-expansion on all the applications featuring this tactic's
1338
argument. For instance, if the current goal includes a subterm {\tt
1339
phi(t)}, then {\tt pattern t} transforms the subterm into {\tt (fun
1340
x:A => phi(x)) t}. This can be useful when {\apply} fails on matching,
1341
to abstract the appropriate terms.
1343
\Question{What is the difference between assert, cut and generalize?}
1345
PS: Notice for people that are interested in proof rendering that \assert
1346
and {\pose} (and \cut) are not rendered the same as {\generalize} (see the
1347
HELM experimental rendering tool at \ahref{http://helm.cs.unibo.it/library.html}{\url{http://helm.cs.unibo.it}}, link
1348
HELM, link COQ Online). Indeed {\generalize} builds a beta-expanded term
1349
while \assert, {\pose} and {\cut} uses a let-in.
1355
... a proof of A->T ...
1358
is rendered into something like
1360
(h) ... the proof of A->T ...
1362
(h0) by (H1 H2) we proved A
1363
by (h h0) we proved T
1368
assert q := (H1 H2).
1370
... a proof of A ...
1371
(* Goal is A |- T *)
1372
... a proof of T ...
1374
is rendered into something like
1376
(q) ... the proof of A ...
1378
... the proof of T ...
1381
Otherwise said, {\generalize} is not rendered in a forward-reasoning way,
1384
\Question{What can I do if \Coq can not infer some implicit argument ?}
1386
You can state explicitely what this implicit argument is. See \ref{implicit}.
1388
\Question{How can I explicit some implicit argument ?}\label{implicit}
1390
Just use \texttt{A:=term} where \texttt{A} is the argument.
1392
For instance if you want to use the existence of ``nil'' on nat*nat lists:
1394
exists (nil (A:=(nat*nat))).
1398
\Question{Is there anyway to do pattern matching with dependent types?}
1403
\subsection{Proof management}
1406
\Question{How can I change the order of the subgoals?}
1408
You can use the {\Focus} command to concentrate on some goal. When the goal is proved you will see the remaining goals.
1410
\Question{How can I change the order of the hypothesis?}
1412
You can use the {\tt Move ... after} command.
1414
\Question{How can I change the name of an hypothesis?}
1416
You can use the {\tt Rename ... into} command.
1418
\Question{How can I delete some hypothesis?}
1420
You can use the {\tt Clear} command.
1422
\Question{How can use a proof which is not finished?}
1424
You can use the {\tt Admitted} command to state your current proof as an axiom.
1425
You can use the {\tt admit} tactic to omit a portion of a proof.
1427
\Question{How can I state a conjecture?}
1429
You can use the {\tt Admitted} command to state your current proof as an axiom.
1431
\Question{What is the difference between a lemma, a fact and a theorem?}
1433
From {\Coq} point of view there are no difference. But some tools can
1434
have a different behavior when you use a lemma rather than a
1435
theorem. For instance {\tt coqdoc} will not generate documentation for
1436
the lemmas within your development.
1438
\Question{How can I organize my proofs?}
1440
You can organize your proofs using the section mechanism of \Coq. Have
1441
a look at the manual for further information.
1444
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
1445
\section{Inductive and Co-inductive types}
1447
\subsection{General}
1449
\Question{How can I prove that two constructors are different?}
1451
You can use the {\discriminate} tactic.
1454
Inductive toto : Set := | C1 : toto | C2 : toto.
1460
\Question{During an inductive proof, how to get rid of impossible cases of an inductive definition?}
1462
Use the {\inversion} tactic.
1465
\Question{How can I prove that 2 terms in an inductive set are equal? Or different?}
1467
Have a look at \coqtt{decide equality} and \coqtt{discriminate} in the \ahref{http://coq.inria.fr/doc/main.html}{Reference Manual}.
1469
\Question{Why is the proof of \coqtt{0+n=n} on natural numbers
1470
trivial but the proof of \coqtt{n+0=n} is not?}
1472
Since \coqtt{+} (\coqtt{plus}) on natural numbers is defined by analysis on its first argument
1478
{\noindent} The expression \coqtt{0+n} evaluates to \coqtt{n}. As {\Coq} reasons
1479
modulo evaluation of expressions, \coqtt{0+n} and \coqtt{n} are
1480
considered equal and the theorem \coqtt{0+n=n} is an instance of the
1481
reflexivity of equality. On the other side, \coqtt{n+0} does not
1482
evaluate to \coqtt{n} and a proof by induction on \coqtt{n} is
1483
necessary to trigger the evaluation of \coqtt{+}.
1485
\Question{Why is dependent elimination in Prop not
1486
available by default?}
1489
This is just because most of the time it is not needed. To derive a
1490
dependent elimination principle in {\tt Prop}, use the command {\tt Scheme} and
1491
apply the elimination scheme using the \verb=using= option of
1492
\verb=elim=, \verb=destruct= or \verb=induction=.
1495
\Question{Argh! I cannot write expressions like ``~{\tt if n <= p then p else n}~'', as in any programming language}
1498
The short answer : You should use {\texttt le\_lt\_dec n p} instead.\\
1500
That's right, you can't.
1501
If you type for instance the following ``definition'':
1506
Definition max (n p : nat) := if n <= p then p else n.
1509
As \Coq~ says, the term ``~\texttt{n <= p}~'' is a proposition, i.e. a
1510
statement that belongs to the mathematical world. There are many ways to
1511
prove such a proposition, either by some computation, or using some already
1512
proven theoremas. For instance, proving $3-2 \leq 2^{45503}$ is very easy,
1513
using some theorems on arithmetical operations. If you compute both numbers
1514
before comparing them, you risk to use a lot of time and space.
1517
On the contrary, a function for computing the greatest of two natural numbers
1518
is an algorithm which, called on two natural numbers
1519
$n$ and $p$, determines wether $n\leq p$ or $p < n$.
1520
Such a function is a \emph{decision procedure} for the inequality of
1521
\texttt{nat}. The possibility of writing such a procedure comes
1522
directly from de decidability of the order $\leq$ on natural numbers.
1525
When you write a piece of code like
1526
``~\texttt{if n <= p then \dots{} else \dots}~''
1528
programming language like \emph{ML} or \emph{Java}, a call to such a
1529
decision procedure is generated. The decision procedure is in general
1530
a primitive function, written in a low-level language, in the correctness
1531
of which you have to trust.
1533
The standard Library of the system \emph{Coq} contains a
1534
(constructive) proof of decidability of the order $\leq$ on
1535
\texttt{nat} : the function \texttt{le\_lt\_dec} of
1536
the module \texttt{Compare\_dec} of library \texttt{Arith}.
1538
The following code shows how to define correctly \texttt{min} and
1539
\texttt{max}, and prove some properties of these functions.
1542
Require Import Compare_dec.
1544
Definition max (n p : nat) := if le_lt_dec n p then p else n.
1546
Definition min (n p : nat) := if le_lt_dec n p then n else p.
1548
Eval compute in (min 4 7).
1550
Theorem min_plus_max : forall n p, min n p + max n p = n + p.
1554
case (le_lt_dec n p);
1555
simpl; auto with arith.
1558
Theorem max_equiv : forall n p, max n p = p <-> n <= p.
1560
unfold max; intros n p; case (le_lt_dec n p);simpl; auto.
1561
intuition auto with arith.
1563
intro e; rewrite e; auto with arith.
1564
intro H; absurd (p < p); eauto with arith.
1568
\Question{I wrote my own decision procedure for $\leq$, which
1569
is much faster than yours, but proving such theorems as
1570
\texttt{max\_equiv} seems to be quite difficult}
1572
Your code is probably the following one:
1575
Fixpoint my_le_lt_dec (n p :nat) {struct n}: bool :=
1576
match n, p with 0, _ => true
1577
| S n', S p' => my_le_lt_dec n' p'
1581
Definition my_max (n p:nat) := if my_le_lt_dec n p then p else n.
1583
Definition my_min (n p:nat) := if my_le_lt_dec n p then n else p.
1587
For instance, the computation of \texttt{my\_max 567 321} is almost
1588
immediate, whereas one can't wait for the result of
1589
\texttt{max 56 32}, using \emph{Coq's} \texttt{le\_lt\_dec}.
1591
This is normal. Your definition is a simple recursive function which
1592
returns a boolean value. Coq's \texttt{le\_lt\_dec} is a \emph{certified
1593
function}, i.e. a complex object, able not only to tell wether $n\leq p$
1594
or $p<n$, but also of building a complete proof of the correct inequality.
1595
What make \texttt{le\_lt\_dec} inefficient for computing \texttt{min}
1596
and \texttt{max} is the building of a huge proof term.
1598
Nevertheless, \texttt{le\_lt\_dec} is very useful. Its type
1599
is a strong specification, using the
1600
\texttt{sumbool} type (look at the reference manual or chapter 9 of
1601
\cite{coqart}). Eliminations of the form
1602
``~\texttt{case (le\_lt\_dec n p)}~'' provide proofs of
1603
either $n \leq p$ or $p < n$, allowing to prove easily theorems as in
1604
question~\ref{minmax}. Unfortunately, this not the case of your
1605
\texttt{my\_le\_lt\_dec}, which returns a quite non-informative boolean
1613
You should keep in mind that \texttt{le\_lt\_dec} is useful to build
1614
certified programs which need to compare natural numbers, and is not
1615
designed to compare quickly two numbers.
1617
Nevertheless, the \emph{extraction} of \texttt{le\_lt\_dec} towards
1618
\emph{Ocaml} or \emph{Haskell}, is a reasonable program for comparing two
1619
natural numbers in Peano form in linear time.
1621
It is also possible to keep your boolean function as a decision procedure,
1622
but you have to establish yourself the relationship between \texttt{my\_le\_lt\_dec} and the propositions $n\leq p$ and $p<n$:
1624
\begin{coq_example*}
1625
Theorem my_le_lt_dec_true :
1626
forall n p, my_le_lt_dec n p = true <-> n <= p.
1628
Theorem my_le_lt_dec_false :
1629
forall n p, my_le_lt_dec n p = false <-> p < n.
1633
\subsection{Recursion}
1635
\Question{Why can't I define a non terminating program?}
1637
Because otherwise the decidability of the type-checking
1638
algorithm (which involves evaluation of programs) is not ensured. On
1639
another side, if non terminating proofs were allowed, we could get a
1640
proof of {\tt False}:
1642
\begin{coq_example*}
1643
(* This is fortunately not allowed! *)
1644
Fixpoint InfiniteProof (n:nat) : False := InfiniteProof n.
1645
Theorem Paradox : False.
1646
Proof (InfiniteProof O).
1650
\Question{Why only structurally well-founded loops are allowed?}
1652
The structural order on inductive types is a simple and
1653
powerful notion of termination. The consistency of the Calculus of
1654
Inductive Constructions relies on it and another consistency proof
1655
would have to be made for stronger termination arguments (such
1656
as the termination of the evaluation of CIC programs themselves!).
1658
In spite of this, all non-pathological termination orders can be mapped
1659
to a structural order. Tools to do this are provided in the file
1660
\vfile{\InitWf}{Wf} of the standard library of {\Coq}.
1662
\Question{How to define loops based on non structurally smaller
1665
The procedure is as follows (we consider the definition of {\tt
1666
mergesort} as an example).
1670
\item Define the termination order, say {\tt R} on the type {\tt A} of
1671
the arguments of the loop.
1675
Require Import List.
1678
\begin{coq_example*}
1679
Definition R (a b:list nat) := length a < length b.
1682
\item Prove that this order is well-founded (in fact that all elements in {\tt A} are accessible along {\tt R}).
1684
\begin{coq_example*}
1685
Lemma Rwf : well_founded R.
1688
\item Define the step function (which needs proofs that recursive
1689
calls are on smaller arguments).
1691
\begin{coq_example*}
1692
Definition split (l : list nat)
1693
: {l1: list nat | R l1 l} * {l2 : list nat | R l2 l}
1695
Definition concat (l1 l2 : list nat) : list nat := (* ... *) .
1696
Definition merge_step (l : list nat) (f: forall l':list nat, R l' l -> list nat) :=
1697
let (lH1,lH2) := (split l) in
1698
let (l1,H1) := lH1 in
1699
let (l2,H2) := lH2 in
1700
concat (f l1 H1) (f l2 H2).
1703
\item Define the recursive function by fixpoint on the step function.
1705
\begin{coq_example*}
1706
Definition merge := Fix Rwf (fun _ => list nat) merge_step.
1711
\Question{What is behind the accessibility and well-foundedness proofs?}
1713
Well-foundedness of some relation {\tt R} on some type {\tt A}
1714
is defined as the accessibility of all elements of {\tt A} along {\tt R}.
1721
The structure of the accessibility predicate is a well-founded tree
1722
branching at each node {\tt x} in {\tt A} along all the nodes {\tt x'}
1723
less than {\tt x} along {\tt R}. Any sequence of elements of {\tt A}
1724
decreasing along the order {\tt R} are branches in the accessibility
1725
tree. Hence any decreasing along {\tt R} is mapped into a structural
1726
decreasing in the accessibility tree of {\tt R}. This is emphasised in
1727
the definition of {\tt fix} which recurs not on its argument {\tt x:A}
1728
but on the accessibility of this argument along {\tt R}.
1730
See file \vfile{\InitWf}{Wf}.
1732
\Question{How to perform simultaneous double induction?}
1734
In general a (simultaneous) double induction is simply solved by an
1735
induction on the first hypothesis followed by an inversion over the
1736
second hypothesis. Here is an example
1743
Inductive even : nat -> Prop :=
1745
| even_S : forall n:nat, even n -> even (S (S n)).
1747
Inductive odd : nat -> Prop :=
1749
| odd_S : forall n:nat, odd n -> odd (S (S n)).
1751
Lemma not_even_and_odd : forall n:nat, even n -> odd n -> False.
1754
inversion 1. apply IHeven; trivial.
1760
In case the type of the second induction hypothesis is not
1761
dependent, {\tt inversion} can just be replaced by {\tt destruct}.
1763
\Question{How to define a function by simultaneous double recursion?}
1765
The same trick applies, you can even use the pattern-matching
1766
compilation algorithm to do the work for you. Here is an example:
1769
Fixpoint minus (n m:nat) {struct n} : nat :=
1773
| S k, S l => minus k l
1778
In case of dependencies in the type of the induction objects
1779
$t_1$ and $t_2$, an extra argument stating $t_1=t_2$ must be given to
1780
the fixpoint definition
1782
\Question{How to perform nested and double induction?}
1784
To reason by nested (i.e. lexicographic) induction, just reason by
1785
induction on the successive components.
1789
Double induction (or induction on pairs) is a restriction of the
1790
lexicographic induction. Here is an example of double induction.
1793
Lemma nat_double_ind :
1794
forall P : nat -> nat -> Prop, P 0 0 ->
1795
(forall m n, P m n -> P m (S n)) ->
1796
(forall m n, P m n -> P (S m) n) ->
1798
intros P H00 HmS HSn; induction m.
1800
induction n; [assumption | apply HmS; apply IHn].
1802
intro n; apply HSn; apply IHm.
1808
\Question{How to define a function by nested recursion?}
1810
The same trick applies. Here is the example of Ackermann
1814
Fixpoint ack (n:nat) : nat -> nat :=
1818
(fix ack' (m:nat) : nat :=
1821
| S m' => ack n' (ack' m')
1827
\subsection{Co-inductive types}
1829
\Question{I have a cofixpoint $t:=F(t)$ and I want to prove $t=F(t)$. How to do it?}
1831
Just case-expand $F({\tt t})$ then complete by a trivial case analysis.
1832
Here is what it gives on e.g. the type of streams on naturals
1835
Set Implicit Arguments.
1838
CoInductive Stream (A:Set) : Set :=
1839
Cons : A -> Stream A -> Stream A.
1840
CoFixpoint nats (n:nat) : Stream nat := Cons n (nats (S n)).
1841
Lemma Stream_unfold :
1842
forall n:nat, nats n = Cons n (nats (S n)).
1845
change (nats n = match nats n with
1846
| Cons x s => Cons x s
1848
case (nats n); reflexivity.
1854
\section{Syntax and notations}
1856
\Question{I do not want to type ``forall'' because it is too long, what can I do?}
1858
You can define your own notation for forall:
1860
Notation "fa x : t, P" := (forall x:t, P) (at level 200, x ident).
1862
or if your are using {\CoqIde} you can define a pretty symbol for for all and an input method (see \ref{forallcoqide}).
1866
\Question{How can I define a notation for square?}
1868
You can use for instance:
1870
Notation "x ^2" := (Rmult x x) (at level 20).
1872
Note that you can not use:
1874
Notation "x $^�$" := (Rmult x x) (at level 20).
1876
because ``$^2$'' is an iso-latin character. If you really want this kind of notation you should use UTF-8.
1879
\Question{Why ``no associativity'' and ``left associativity'' at the same level does not work?}
1881
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.
1885
\Question{How can I know the associativity associated with a level?}
1887
You can do ``Print Grammar constr'', and decode the output from camlp4, good luck !
1897
\Question{What is {\Ltac}?}
1899
{\Ltac} is the tactic language for \Coq. It provides the user with a
1900
high-level ``toolbox'' for tactic creation.
1902
\Question{Is there any printing command in {\Ltac}?}
1904
You can use the {\idtac} tactic with a string argument. This string
1905
will be printed out. The same applies to the {\fail} tactic
1907
\Question{What is the syntax for let in {\Ltac}?}
1909
If $x_i$ are identifiers and $e_i$ and $expr$ are tactic expressions, then let reads:
1911
{\tt let $x_1$:=$e_1$ with $x_2$:=$e_2$\ldots with $x_n$:=$e_n$ in
1914
Beware that if $expr$ is complex (i.e. features at least a sequence) parenthesis
1915
should be added around it. For example:
1917
Ltac twoIntro := let x:=intro in (x;x).
1920
\Question{What is the syntax for pattern matching in {\Ltac}?}
1922
Pattern matching on a term $expr$ (non-linear first order unification)
1923
with patterns $p_i$ and tactic expressions $e_i$ reads:
1926
{\tt match $expr$ with
1927
\hspace*{2ex}$p_1$ => $e_1$
1928
\hspace*{1ex}\textbar$p_2$ => $e_2$
1930
\hspace*{1ex}\textbar$p_n$ => $e_n$
1931
\hspace*{1ex}\textbar\ \textunderscore\ => $e_{n+1}$
1935
Underscore matches all terms.
1937
\Question{What is the semantics for ``match goal''?}
1939
The semantics of {\tt match goal} depends on whether it returns
1940
tactics or not. The {\tt match goal} expression matches the current
1941
goal against a series of patterns: {$hyp_1 {\ldots} hyp_n$ \textbar-
1942
$ccl$}. It uses a first-order unification algorithm and in case of
1943
success, if the right-hand-side is an expression, it tries to type it
1944
while if the right-hand-side is a tactic, it tries to apply it. If the
1945
typing or the tactic application fails, the {\tt match goal} tries all
1946
the possible combinations of $hyp_i$ before dropping the branch and
1947
moving to the next one. Underscore matches all terms.
1949
\Question{Why can't I use a ``match goal'' returning a tactic in a non
1950
tail-recursive position?}
1952
This is precisely because the semantics of {\tt match goal} is to
1953
apply the tactic on the right as soon as a pattern unifies what is
1954
meaningful only in tail-recursive uses.
1956
The semantics in non tail-recursive call could have been the one used
1957
for terms (i.e. fail if the tactic expression is not typable, but
1958
don't try to apply it). For uniformity of semantics though, this has
1961
\Question{How can I generate a new name?}
1963
You can use the following syntax:
1964
{\tt let id:=fresh in \ldots}\\
1967
Ltac introIdGen := let id:=fresh in intro id.
1972
\Question{How can I access the type of a term?}
1979
\Question{How can I define static and dynamic code?}
1982
\section{Tactics written in Ocaml}
1984
\Question{Can you show me an example of a tactic written in OCaml?}
1986
You have some examples of tactics written in Ocaml in the ``contrib'' directory of {\Coq} sources.
1991
\section{Case studies}
1994
\Question{How can I define vectors or lists of size n?}
1998
\Question{How to prove that 2 sets are different?}
2000
You need to find a property true on one set and false on the
2001
other one. As an example we show how to prove that {\tt bool} and {\tt
2002
nat} are discriminable. As discrimination property we take the
2003
property to have no more than 2 elements.
2005
\begin{coq_example*}
2006
Theorem nat_bool_discr : bool <> nat.
2010
~ (forall a b:X, ~ (forall x:X, x <> a -> x <> b -> False))).
2011
intro Heq; assert (H: discr bool).
2012
intro H; apply (H true false); destruct x; auto.
2013
rewrite Heq in H; apply H; clear H.
2014
destruct a; destruct b as [|n]; intro H0; eauto.
2015
destruct n; [ apply (H0 2); discriminate | eauto ].
2019
\Question{Is there an axiom-free proof of Streicher's axiom $K$ for
2020
the equality on {\tt nat}?}
2023
Yes, because equality is decidable on {\tt nat}. Here is the proof.
2025
\begin{coq_example*}
2026
Require Import Eqdep_dec.
2027
Require Import Peano_dec.
2029
forall (x:nat) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.
2031
intros; apply K_dec_set with (p := p).
2039
\begin{coq_example*}
2040
Theorem eq_rect_eq_nat :
2041
forall (p:nat) (Q:nat->Type) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
2043
intros; apply K_nat with (p := h); reflexivity.
2047
\Question{How to prove that two proofs of {\tt n<=m} on {\tt nat} are equal?}
2048
\label{le-uniqueness}
2050
This is provable without requiring any axiom because axiom $K$
2051
directly holds on {\tt nat}. Here is a proof using question \ref{K-nat}.
2053
\begin{coq_example*}
2054
Require Import Arith.
2055
Scheme le_ind' := Induction for le Sort Prop.
2056
Theorem le_uniqueness_proof : forall (n m : nat) (p q : n <= m), p = q.
2058
induction p using le_ind'; intro q.
2059
replace (le_n n) with
2060
(eq_rect _ (fun n0 => n <= n0) (le_n n) _ (refl_equal n)).
2062
generalize (refl_equal n).
2063
pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
2064
rewrite <- eq_rect_eq_nat; trivial.
2065
contradiction (le_Sn_n m); rewrite <- e; assumption.
2066
replace (le_S n m p) with
2067
(eq_rect _ (fun n0 => n <= n0) (le_S n m p) _ (refl_equal (S m))).
2069
generalize (refl_equal (S m)).
2070
pattern (S m) at 1 3 4 6, q; case q; [intro Heq | intros m0 l HeqS].
2071
contradiction (le_Sn_n m); rewrite Heq; assumption.
2072
injection HeqS; intro Heq; generalize l HeqS.
2073
rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
2074
rewrite (IHp l0); reflexivity.
2078
\Question{How to exploit equalities on sets}
2080
To extract information from an equality on sets, you need to
2081
find a predicate of sets satisfied by the elements of the sets. As an
2082
example, let's consider the following theorem.
2084
\begin{coq_example*}
2085
Theorem interval_discr :
2087
{x : nat | x <= m} = {x : nat | x <= n} -> m = n.
2090
We have a proof requiring the axiom of proof-irrelevance. We
2091
conjecture that proof-irrelevance can be circumvented by introducing a
2092
primitive definition of discrimination of the proofs of
2093
\verb!{x : nat | x <= m}!.
2096
The proof can be found in file {\tt interval$\_$discr.v} in this directory.
2101
%\def_{\ifmmode\sb\else\subscr\fi}
2102
%\include{interval_discr.v}
2103
%%% WARNING semantics of \_ has changed !
2110
\ahref{./interval_discr.v}{Here} is the proof.
2113
\Question{I have a problem of dependent elimination on
2114
proofs, how to solve it?}
2120
\begin{coq_example*}
2121
Inductive Def1 : Set := c1 : Def1.
2122
Inductive DefProp : Def1 -> Prop :=
2123
c2 : forall d:Def1, DefProp d.
2124
Inductive Comb : Set :=
2125
c3 : forall d:Def1, DefProp d -> Comb.
2127
forall (d1 d1':Def1) (d2:DefProp d1) (d2':DefProp d1'),
2128
d1 = d1' -> c3 d1 d2 = c3 d1' d2'.
2131
You need to derive the dependent elimination
2132
scheme for DefProp by hand using {\coqtt Scheme}.
2138
\begin{coq_example*}
2139
Scheme DefProp_elim := Induction for DefProp Sort Prop.
2143
forall (d2:DefProp d1) (d2':DefProp d1'), c3 d1 d2 = c3 d1' d2'.
2146
destruct d2 using DefProp_elim.
2147
destruct d2' using DefProp_elim.
2153
\Question{And what if I want to prove the following?}
2155
\begin{coq_example*}
2156
Inductive natProp : nat -> Prop :=
2158
| pS : forall n:nat, natProp n -> natProp (S n).
2159
Inductive package : Set :=
2160
pack : forall n:nat, natProp n -> package.
2164
forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
2172
\begin{coq_example*}
2173
Scheme natProp_elim := Induction for natProp Sort Prop.
2174
Definition pack_S : package -> package.
2177
apply pS; assumption.
2182
forall (np:natProp n) (np':natProp n'), pack n np = pack n' np'.
2183
intros n n' Heq np np'.
2184
generalize dependent n'.
2185
induction np using natProp_elim.
2186
induction np' using natProp_elim; intros; auto.
2188
induction np' using natProp_elim; intros; auto.
2190
change (pack_S (pack n np) = pack_S (pack n0 np')).
2191
apply (f_equal (A:=package)).
2203
\section{Publishing tools}
2205
\Question{How can I generate some latex from my development?}
2207
You can use {\tt coqdoc}.
2209
\Question{How can I generate some HTML from my development?}
2211
You can use {\tt coqdoc}.
2213
\Question{How can I generate some dependency graph from my development?}
2215
You can use the tool \verb|coqgraph| developped by Philippe Audebaud in 2002.
2216
This tool transforms dependancies generated by \verb|coqdep| into 'dot' files which can be visualized using the Graphviz software (http://www.graphviz.org/).
2218
\Question{How can I cite some {\Coq} in my latex document?}
2220
You can use {\tt coq\_tex}.
2222
\Question{How can I cite the {\Coq} reference manual?}
2224
You can use this bibtex entry:
2227
title = {The Coq proof assistant reference manual},
2228
author = {\mbox{The Coq development team}},
2229
organization = {LogiCal Project},
2230
note = {Version 8.2},
2232
url = "http://coq.inria.fr"
2236
\Question{Where can I publish my developments in {\Coq}?}
2238
You can submit your developments as a user contribution to the {\Coq}
2239
development team. This ensures its liveness along the evolution and
2240
possible changes of {\Coq}.
2242
You can also submit your developments to the HELM/MoWGLI repository at
2243
the University of Bologna (see
2244
\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}). For
2245
developments submitted in this database, it is possible to visualize
2246
the developments in natural language and execute various retrieving
2249
\Question{How can I read my proof in natural language?}
2251
You can submit your proof to the HELM/MoWGLI repository and use the
2252
rendering tool provided by the server (see
2253
\ahref{http://mowgli.cs.unibo.it}{\url{http://mowgli.cs.unibo.it}}).
2257
\Question{What is {\CoqIde}?}
2259
{\CoqIde} is a gtk based GUI for \Coq.
2261
\Question{How to enable Emacs keybindings?}
2263
Depending on your configuration, use either one of these two methods
2267
\item Insert \texttt{gtk-key-theme-name = "Emacs"}
2268
in your \texttt{.coqide-gtk2rc} file. It may be in the current dir
2269
or in \verb#$HOME# dir. This is done by default.
2271
\item If in Gnome, run the gnome configuration editor (\texttt{gconf-editor})
2272
and set key \texttt{gtk-key-theme} to \texttt{Emacs} in the category
2273
\texttt{desktop/gnome/interface}.
2279
%$ juste pour que la coloration emacs marche
2281
\Question{How to enable antialiased fonts?}
2283
Set the \verb#GDK_USE_XFT# variable to \verb#1#. This is by default
2284
with \verb#Gtk >= 2.2#. If some of your fonts are not available,
2285
set \verb#GDK_USE_XFT# to \verb#0#.
2287
\Question{How to use those Forall and Exists pretty symbols?}\label{forallcoqide}
2288
Thanks to the notation features in \Coq, you just need to insert these
2289
lines in your {\Coq} buffer:\\
2291
Notation "$\forall$ x : t, P" := (forall x:t, P) (at level 200, x ident).
2294
Notation "$\exists$ x : t, P" := (exists x:t, P) (at level 200, x ident).
2297
Copy/Paste of these lines from this file will not work outside of \CoqIde.
2298
You need to load a file containing these lines or to enter the $\forall$
2299
using an input method (see \ref{inputmeth}). To try it just use \verb#Require Import utf8# from inside
2301
To enable these notations automatically start coqide with
2305
In the ide subdir of {\Coq} library, you will find a sample utf8.v with some
2306
pretty simple notations.
2308
\Question{How to define an input method for non ASCII symbols?}\label{inputmeth}
2311
\item First solution: type \verb#<CONTROL><SHIFT>2200# to enter a forall in the script widow.
2312
2200 is the hexadecimal code for forall in unicode charts and is encoded as
2314
2203 is for exists. See \ahref{http://www.unicode.org}{\url{http://www.unicode.org}} for more codes.
2315
\item Second solution: rebind \verb#<AltGr>a# to forall and \verb#<AltGr>e# to exists.
2316
Under X11, you need to use something like
2318
xmodmap -e "keycode 24 = a A F13 F13"
2319
xmodmap -e "keycode 26 = e E F14 F14"
2323
bind "F13" {"insert-at-cursor" ("")}
2324
bind "F14" {"insert-at-cursor" ("")}
2326
to your "binding "text"" section in \verb#.coqiderc-gtk2rc.#
2327
The strange ("") argument is the UTF-8 encoding for
2329
You can compute these encodings using the lablgtk2 toplevel with
2331
Glib.Utf8.from_unichar 0x2200;;
2333
Further symbols can be bound on higher Fxx keys or on even on other keys you
2337
\Question{How to build a custom {\CoqIde} with user ml code?}
2339
coqmktop -ide -byte m1.cmo...mi.cmo
2341
coqmktop -ide -opt m1.cmx...mi.cmx
2343
\Question{How to customize the shortcuts for menus?}
2344
Two solutions are offered:
2346
\item Edit \$HOME/.coqide.keys by hand or
2347
\item Add "gtk-can-change-accels = 1" in your .coqide-gtk2rc file. Then
2348
from \CoqIde, you may select a menu entry and press the desired
2352
\Question{What encoding should I use? What is this $\backslash$x\{iiii\} in my file?}
2353
The encoding option is related to the way files are saved.
2354
Keep it as UTF-8 until it becomes important for you to exchange files
2355
with non UTF-8 aware applications.
2356
If you choose something else than UTF-8, then missing characters will
2357
be encoded by $\backslash$x\{....\} or $\backslash$x\{........\}
2358
where each dot is an hex. digit.
2359
The number between braces is the hexadecimal UNICODE index for the
2362
\Question{How to get rid of annoying unwanted automatic templates?}
2364
Some users may experiment problems with unwanted automatic
2365
templates while using Coqide. This is due to a change in the
2366
modifiers keys available through GTK. The straightest way to get
2367
rid of the problem is to edit by hand your .coqiderc (either
2368
\verb|/home/<user>/.coqiderc| under Linux, or \\
2369
\verb|C:\Documents and Settings\<user>\.coqiderc| under Windows)
2370
and replace any occurence of \texttt{MOD4} by \texttt{MOD1}.
2374
\section{Extraction}
2376
\Question{What is program extraction?}
2378
Program extraction consist in generating a program from a constructive proof.
2380
\Question{Which language can I extract to?}
2382
You can extract your programs to Objective Caml and Haskell.
2384
\Question{How can I extract an incomplete proof?}
2386
You can provide programs for your axioms.
2393
\Question{Can you explain me what an evaluable constant is?}
2395
An evaluable constant is a constant which is unfoldable.
2397
\Question{What is a goal?}
2399
The goal is the statement to be proved.
2401
\Question{What is a meta variable?}
2403
A meta variable in {\Coq} represents a ``hole'', i.e. a part of a proof
2404
that is still unknown.
2406
\Question{What is Gallina?}
2408
Gallina is the specification language of \Coq. Complete documentation
2409
of this language can be found in the Reference Manual.
2411
\Question{What is The Vernacular?}
2413
It is the language of commands of Gallina i.e. definitions, lemmas, {\ldots}
2416
\Question{What is a dependent type?}
2418
A dependant type is a type which depends on some term. For instance
2419
``vector of size n'' is a dependant type representing all the vectors
2420
of size $n$. Its type depends on $n$
2422
\Question{What is a proof by reflection?}
2424
This is a proof generated by some computation which is done using the
2425
internal reduction of {\Coq} (not using the tactic language of {\Coq}
2426
(\Ltac) nor the implementation language for \Coq). An example of
2427
tactic using the reflection mechanism is the {\ring} tactic. The
2428
reflection method consist in reflecting a subset of {\Coq} language (for
2429
example the arithmetical expressions) into an object of the {\Coq}
2430
language itself (in this case an inductive type denoting arithmetical
2431
expressions). For more information see~\cite{howe,harrison,boutin}
2432
and the last chapter of the Coq'Art.
2434
\Question{What is intuitionistic logic?}
2436
This is any logic which does not assume that ``A or not A''.
2439
\Question{What is proof-irrelevance?}
2441
See question \ref{proof-irrelevance}
2444
\Question{What is the difference between opaque and transparent?}{\label{opaque}}
2446
Opaque definitions can not be unfolded but transparent ones can.
2449
\section{Troubleshooting}
2451
\Question{What can I do when {\tt Qed.} is slow?}
2453
Sometime you can use the {\abstracttac} tactic, which makes as if you had
2454
stated some local lemma, this speeds up the typing process.
2456
\Question{Why \texttt{Reset Initial.} does not work when using \texttt{coqc}?}
2458
The initial state corresponds to the state of \texttt{coqtop} when the interactive
2459
session began. It does not make sense in files to compile.
2462
\Question{What can I do if I get ``No more subgoals but non-instantiated existential variables''?}
2464
This means that {\eauto} or {\eapply} didn't instantiate an
2465
existential variable which eventually got erased by some computation.
2466
You may backtrack to the faulty occurrence of {\eauto} or {\eapply}
2467
and give the missing argument an explicit value. Alternatively, you
2468
can use the commands \texttt{Show Existentials.} and
2469
\texttt{Existential.} to display and instantiate the remainig
2470
existential variables.
2474
Lemma example_show_existentials : forall a b c:nat, a=b -> b=c -> a=c.
2485
\Question{What can I do if I get ``Cannot solve a second-order unification problem''?}
2487
You can help {\Coq} using the {\pattern} tactic.
2489
\Question{Why does {\Coq} tell me that \texttt{\{x:A|(P x)\}} is not convertible with \texttt{(sig A P)}?}
2491
This is because \texttt{\{x:A|P x\}} is a notation for
2492
\texttt{sig (fun x:A => P x)}. Since {\Coq} does not reason up to
2493
$\eta$-conversion, this is different from \texttt{sig P}.
2496
\Question{I copy-paste a term and {\Coq} says it is not convertible
2497
to the original term. Sometimes it even says the copied term is not
2500
This is probably due to invisible implicit information (implicit
2501
arguments, coercions and Cases annotations) in the printed term, which
2502
is not re-synthesised from the copied-pasted term in the same way as
2503
it is in the original term.
2505
Consider for instance {\tt (@eq Type True True)}. This term is
2506
printed as {\tt True=True} and re-parsed as {\tt (@eq Prop True
2507
True)}. The two terms are not convertible (hence they fool tactics
2508
like {\tt pattern}).
2510
There is currently no satisfactory answer to the problem. However,
2511
the command {\tt Set Printing All} is useful for diagnosing the
2514
Due to coercions, one may even face type-checking errors. In some
2515
rare cases, the criterion to hide coercions is a bit too loose, which
2516
may result in a typing error message if the parser is not able to find
2517
again the missing coercion.
2521
\section{Conclusion and Farewell.}
2524
\Question{What if my question isn't answered here?}
2525
\label{lastquestion}
2527
Don't panic \verb+:-)+. You can try the {\Coq} manual~\cite{Coq:manual} for a technical
2528
description of the prover. The Coq'Art~\cite{Coq:coqart} is the first
2529
book written on {\Coq} and provides a comprehensive review of the
2530
theorem prover as well as a number of example and exercises. Finally,
2531
the tutorial~\cite{Coq:Tutorial} provides a smooth introduction to
2532
theorem proving in \Coq.
2537
\nocite{LaTeX:intro}
2542
\typeout{*********************************************}
2543
\typeout{********* That makes {\thequestion} questions **********}
2544
\typeout{*********************************************}
added
removed
doc/faq/FAQ.tex
