← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to doc/refman/RefMan-lib.tex

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
doc/refman/RefMan-lib.tex
 
1
\chapter[The {\Coq} library]{The {\Coq} library\index{Theories}\label{Theories}}
 
2
 
 
3
The \Coq\ library is structured into two parts:
 
4
 
 
5
\begin{description}
 
6
\item[The initial library:] it contains
 
7
  elementary logical notions and data-types. It constitutes the
 
8
  basic state of the system directly available when running
 
9
  \Coq;
 
10
 
 
11
\item[The standard library:] general-purpose libraries containing
 
12
  various developments of \Coq\ axiomatizations about sets, lists,
 
13
  sorting, arithmetic, etc. This library comes with the system and its
 
14
  modules are directly accessible through the \verb!Require! command
 
15
  (see Section~\ref{Require});
 
16
\end{description}
 
17
 
 
18
In addition, user-provided libraries or developments are provided by
 
19
\Coq\ users' community. These libraries and developments are available
 
20
for download at \texttt{http://coq.inria.fr} (see
 
21
Section~\ref{Contributions}).
 
22
 
 
23
The chapter briefly reviews the \Coq\ libraries.
 
24
 
 
25
\section[The basic library]{The basic library\label{Prelude}}
 
26
 
 
27
This section lists the basic notions and results which are directly
 
28
available in the standard \Coq\ system\footnote{Most 
 
29
of these constructions are defined in the
 
30
{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
 
31
root directory; this includes the modules
 
32
{\tt Notations},
 
33
{\tt Logic},
 
34
{\tt Datatypes},
 
35
{\tt Specif},
 
36
{\tt Peano},
 
37
{\tt Wf} and 
 
38
{\tt Tactics}.
 
39
Module {\tt Logic\_Type} also makes it in the initial state}.
 
40
 
 
41
\subsection[Notations]{Notations\label{Notations}}
 
42
 
 
43
This module defines the parsing and pretty-printing of many symbols
 
44
(infixes, prefixes, etc.). However, it does not assign a meaning to
 
45
these notations. The purpose of this is to define and fix once for all
 
46
the precedence and associativity of very common notations. The main
 
47
notations fixed in the initial state are listed on
 
48
Figure~\ref{init-notations}.
 
49
 
 
50
\begin{figure}
 
51
\begin{center}
 
52
\begin{tabular}{|cll|}
 
53
\hline
 
54
Notation & Precedence & Associativity \\
 
55
\hline
 
56
\verb!_ <-> _! & 95 & no \\
 
57
\verb!_ \/ _!  & 85 & right \\
 
58
\verb!_ /\ _!  & 80 & right \\
 
59
\verb!~ _!   & 75 & right \\
 
60
\verb!_ = _!   & 70 & no \\
 
61
\verb!_ = _ = _!   & 70 & no \\
 
62
\verb!_ = _ :> _!   & 70 & no \\
 
63
\verb!_ <> _!  & 70 & no \\
 
64
\verb!_ <> _ :> _!  & 70 & no \\
 
65
\verb!_ < _!   & 70 & no \\
 
66
\verb!_ > _!   & 70 & no \\
 
67
\verb!_ <= _!  & 70 & no \\
 
68
\verb!_ >= _!  & 70 & no \\
 
69
\verb!_ < _ < _! & 70 & no \\
 
70
\verb!_ < _ <= _! & 70 & no \\
 
71
\verb!_ <= _ < _! & 70 & no \\
 
72
\verb!_ <= _ <= _! & 70 & no \\
 
73
\verb!_ + _!   & 50 & left \\
 
74
\verb!_ || _!  & 50 & left \\
 
75
\verb!_ - _!   & 50 & left \\
 
76
\verb!_ * _!   & 40 & left \\
 
77
\verb!_ && _!  & 40 & left \\
 
78
\verb!_ / _!   & 40 & left \\
 
79
\verb!- _!  & 35 & right \\
 
80
\verb!/ _!  & 35 & right \\
 
81
\verb!_ ^ _!   & 30 & right \\
 
82
\hline
 
83
\end{tabular}
 
84
\end{center}
 
85
\caption{Notations in the initial state}
 
86
\label{init-notations}
 
87
\end{figure}
 
88
 
 
89
\subsection[Logic]{Logic\label{Logic}}
 
90
 
 
91
\begin{figure}
 
92
\begin{centerframe}
 
93
\begin{tabular}{lclr}
 
94
{\form} & ::= & {\tt True} & ({\tt True})\\
 
95
  & $|$ & {\tt False} & ({\tt False})\\
 
96
  & $|$ & {\tt\char'176} {\form} & ({\tt not})\\
 
97
  & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\
 
98
  & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
 
99
  & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
 
100
  & $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\
 
101
  & $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,}
 
102
  {\form} & (\em{primitive for all})\\
 
103
  & $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt
 
104
  ,} {\form}  & ({\tt ex})\\
 
105
  & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
 
106
  ,} {\form}  {\tt \&} {\form} & ({\tt ex2})\\
 
107
  & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
 
108
  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
 
109
\end{tabular}
 
110
\end{centerframe}
 
111
\caption{Syntax of formulas}
 
112
\label{formulas-syntax}
 
113
\end{figure}
 
114
 
 
115
The basic library of {\Coq} comes with the definitions of standard
 
116
(intuitionistic) logical connectives (they are defined as inductive
 
117
constructions). They are equipped with an appealing syntax enriching the
 
118
(subclass {\form}) of the syntactic class {\term}. The syntax
 
119
extension is shown on Figure~\ref{formulas-syntax}.
 
120
 
 
121
% The basic library of {\Coq} comes with the definitions of standard
 
122
% (intuitionistic) logical connectives (they are defined as inductive
 
123
% constructions). They are equipped with an appealing syntax enriching
 
124
% the (subclass {\form}) of the syntactic class {\term}. The syntax
 
125
% extension \footnote{This syntax is defined in module {\tt
 
126
%     LogicSyntax}} is shown on Figure~\ref{formulas-syntax}.
 
127
 
 
128
\Rem Implication is not defined but primitive (it is a non-dependent
 
129
product of a proposition over another proposition).  There is also a
 
130
primitive universal quantification (it is a dependent product over a
 
131
proposition). The primitive universal quantification allows both
 
132
first-order and higher-order quantification.
 
133
 
 
134
\subsubsection[Propositional Connectives]{Propositional Connectives\label{Connectives}
 
135
\index{Connectives}}
 
136
 
 
137
First, we find propositional calculus connectives:
 
138
\ttindex{True}
 
139
\ttindex{I}
 
140
\ttindex{False}
 
141
\ttindex{not}
 
142
\ttindex{and}
 
143
\ttindex{conj}
 
144
\ttindex{proj1}
 
145
\ttindex{proj2}
 
146
 
 
147
\begin{coq_eval}
 
148
Set Printing Depth 50.
 
149
\end{coq_eval}
 
150
\begin{coq_example*}
 
151
Inductive True : Prop := I.
 
152
Inductive False :  Prop := .
 
153
Definition not (A: Prop) := A -> False.
 
154
Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
 
155
Section Projections.
 
156
Variables A B : Prop.
 
157
Theorem proj1 : A /\ B -> A.
 
158
Theorem proj2 : A /\ B -> B.
 
159
End Projections.
 
160
\end{coq_example*}
 
161
\begin{coq_eval}
 
162
Abort All.
 
163
\end{coq_eval}
 
164
\ttindex{or}
 
165
\ttindex{or\_introl}
 
166
\ttindex{or\_intror}
 
167
\ttindex{iff}
 
168
\ttindex{IF\_then\_else}
 
169
\begin{coq_example*}
 
170
Inductive or (A B:Prop) : Prop :=
 
171
  | or_introl (_:A)
 
172
  | or_intror (_:B).
 
173
Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
 
174
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
 
175
\end{coq_example*}
 
176
 
 
177
\subsubsection[Quantifiers]{Quantifiers\label{Quantifiers}
 
178
\index{Quantifiers}}
 
179
 
 
180
Then we find first-order quantifiers:
 
181
\ttindex{all}
 
182
\ttindex{ex}
 
183
\ttindex{exists}
 
184
\ttindex{ex\_intro}
 
185
\ttindex{ex2}
 
186
\ttindex{exists2}
 
187
\ttindex{ex\_intro2}
 
188
 
 
189
\begin{coq_example*}
 
190
Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
 
191
Inductive ex (A: Set) (P:A -> Prop) : Prop :=
 
192
    ex_intro (x:A) (_:P x).
 
193
Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
 
194
    ex_intro2 (x:A) (_:P x) (_:Q x).
 
195
\end{coq_example*}
 
196
 
 
197
The following abbreviations are allowed:
 
198
\begin{center}
 
199
  \begin{tabular}[h]{|l|l|}
 
200
    \hline
 
201
    \verb+exists x:A, P+     & \verb+ex A (fun x:A => P)+ \\
 
202
    \verb+exists x, P+       & \verb+ex _ (fun x => P)+ \\
 
203
    \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
 
204
    \verb+exists2 x, P & Q+   & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\
 
205
    \hline
 
206
  \end{tabular}
 
207
\end{center}
 
208
 
 
209
The type annotation ``\texttt{:A}'' can be omitted when \texttt{A} can be
 
210
synthesized by the system.
 
211
 
 
212
\subsubsection[Equality]{Equality\label{Equality}
 
213
\index{Equality}}
 
214
 
 
215
Then, we find equality, defined as an inductive relation. That is,
 
216
given a type \verb:A: and an \verb:x: of type \verb:A:, the
 
217
predicate \verb:(eq A x): is the smallest one which contains \verb:x:.
 
218
This definition, due to Christine Paulin-Mohring, is equivalent to
 
219
define \verb:eq: as the smallest reflexive relation, and it is also
 
220
equivalent to Leibniz' equality.
 
221
 
 
222
\ttindex{eq}
 
223
\ttindex{refl\_equal}
 
224
 
 
225
\begin{coq_example*}
 
226
Inductive eq (A:Type) (x:A) : A -> Prop :=
 
227
    refl_equal : eq A x x.
 
228
\end{coq_example*}
 
229
 
 
230
\subsubsection[Lemmas]{Lemmas\label{PreludeLemmas}}
 
231
 
 
232
Finally, a few easy lemmas are provided.
 
233
 
 
234
\ttindex{absurd}
 
235
 
 
236
\begin{coq_example*}
 
237
Theorem absurd : forall A C:Prop, A -> ~ A -> C.
 
238
\end{coq_example*}
 
239
\begin{coq_eval}
 
240
Abort.
 
241
\end{coq_eval}
 
242
\ttindex{sym\_eq}
 
243
\ttindex{trans\_eq}
 
244
\ttindex{f\_equal}
 
245
\ttindex{sym\_not\_eq}
 
246
\begin{coq_example*}
 
247
Section equality.
 
248
Variables A B : Type.
 
249
Variable f : A -> B.
 
250
Variables x y z : A.
 
251
Theorem sym_eq : x = y -> y = x.
 
252
Theorem trans_eq : x = y -> y = z -> x = z.
 
253
Theorem f_equal : x = y -> f x = f y.
 
254
Theorem sym_not_eq : x <> y -> y <> x.
 
255
\end{coq_example*}
 
256
\begin{coq_eval}
 
257
Abort.
 
258
Abort.
 
259
Abort.
 
260
Abort.
 
261
\end{coq_eval}
 
262
\ttindex{eq\_ind\_r}
 
263
\ttindex{eq\_rec\_r}
 
264
\ttindex{eq\_rect}
 
265
\ttindex{eq\_rect\_r}
 
266
%Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y).
 
267
\begin{coq_example*}
 
268
End equality.
 
269
Definition eq_ind_r :
 
270
  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
 
271
Definition eq_rec_r :
 
272
  forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
 
273
Definition eq_rect_r :
 
274
  forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
 
275
\end{coq_example*}
 
276
\begin{coq_eval}
 
277
Abort.
 
278
Abort.
 
279
Abort.
 
280
\end{coq_eval}
 
281
%Abort (for now predefined eq_rect)
 
282
\begin{coq_example*}
 
283
Hint Immediate sym_eq sym_not_eq : core.
 
284
\end{coq_example*}
 
285
\ttindex{f\_equal$i$}
 
286
 
 
287
The theorem {\tt f\_equal} is extended to functions with two to five
 
288
arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, 
 
289
{\tt f\_equal4} and {\tt f\_equal5}.
 
290
For instance {\tt f\_equal3} is defined the following way.
 
291
\begin{coq_example*}
 
292
Theorem f_equal3 :
 
293
 forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
 
294
   (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
 
295
\end{coq_example*}
 
296
\begin{coq_eval}
 
297
Abort.
 
298
\end{coq_eval}
 
299
 
 
300
\subsection[Datatypes]{Datatypes\label{Datatypes}
 
301
\index{Datatypes}}
 
302
 
 
303
\begin{figure}
 
304
\begin{centerframe}
 
305
\begin{tabular}{rclr}
 
306
{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
 
307
  & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
 
308
  & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
 
309
  & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
 
310
  ({\tt sumbool})\\  
 
311
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
 
312
  & ({\tt sig})\\
 
313
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form}  {\tt \&}
 
314
  {\form} {\tt \}} & ({\tt sig2})\\
 
315
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
 
316
    \}} & ({\tt sigT})\\
 
317
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
 
318
    \&} {\specif} {\tt \}} & ({\tt sigT2})\\
 
319
  &  & & \\
 
320
{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
 
321
\end{tabular}
 
322
\end{centerframe}
 
323
\caption{Syntax of data-types and specifications}
 
324
\label{specif-syntax}
 
325
\end{figure}
 
326
 
 
327
 
 
328
In the basic library, we find the definition\footnote{They are in {\tt
 
329
    Datatypes.v}} of the basic data-types of programming, again
 
330
defined as inductive constructions over the sort \verb:Set:. Some of
 
331
them come with a special syntax shown on Figure~\ref{specif-syntax}.
 
332
 
 
333
\subsubsection[Programming]{Programming\label{Programming}
 
334
\index{Programming}
 
335
\label{libnats}
 
336
\ttindex{unit}
 
337
\ttindex{tt}
 
338
\ttindex{bool}
 
339
\ttindex{true}
 
340
\ttindex{false}
 
341
\ttindex{nat}
 
342
\ttindex{O}
 
343
\ttindex{S}
 
344
\ttindex{option}
 
345
\ttindex{Some}
 
346
\ttindex{None}
 
347
\ttindex{identity}
 
348
\ttindex{refl\_identity}}
 
349
 
 
350
\begin{coq_example*}
 
351
Inductive unit : Set := tt.
 
352
Inductive bool : Set := true | false.
 
353
Inductive nat : Set := O | S (n:nat).
 
354
Inductive option (A:Set) : Set := Some (_:A) | None.
 
355
Inductive identity (A:Type) (a:A) : A -> Type :=
 
356
    refl_identity : identity A a a.
 
357
\end{coq_example*}
 
358
 
 
359
Note that zero is the letter \verb:O:, and {\sl not} the numeral
 
360
\verb:0:.
 
361
 
 
362
The predicate {\tt identity} is logically 
 
363
equivalent to equality but it lives in sort {\tt
 
364
  Type}. It is mainly maintained for compatibility.
 
365
 
 
366
We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
 
367
\verb:B:, and their product \verb:A*B:.
 
368
\ttindex{sum}
 
369
\ttindex{A+B}
 
370
\ttindex{+}
 
371
\ttindex{inl}
 
372
\ttindex{inr}
 
373
\ttindex{prod}
 
374
\ttindex{A*B}
 
375
\ttindex{*}
 
376
\ttindex{pair}
 
377
\ttindex{fst}
 
378
\ttindex{snd}
 
379
 
 
380
\begin{coq_example*}
 
381
Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
 
382
Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
 
383
Section projections.
 
384
Variables A B : Set.
 
385
Definition fst (H: prod A B) := match H with
 
386
                                | pair x y => x
 
387
                                end.
 
388
Definition snd (H: prod A B) := match H with
 
389
                                | pair x y => y
 
390
                                end.
 
391
End projections.
 
392
\end{coq_example*}
 
393
 
 
394
Some operations on {\tt bool} are also provided: {\tt andb} (with
 
395
infix notation {\tt \&\&}), {\tt orb} (with
 
396
infix notation {\tt ||}), {\tt xorb}, {\tt implb} and {\tt negb}.
 
397
 
 
398
\subsection{Specification}
 
399
 
 
400
The following notions\footnote{They are defined in module {\tt
 
401
Specif.v}} allow to build new data-types and specifications. 
 
402
They are available with the syntax shown on
 
403
Figure~\ref{specif-syntax}.
 
404
 
 
405
For instance, given \verb|A:Type| and \verb|P:A->Prop|, the construct
 
406
\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a
 
407
\verb:Type:. We may build elements of this set as \verb:(exist x p):
 
408
whenever we have a witness \verb|x:A| with its justification
 
409
\verb|p:P x|.
 
410
 
 
411
From such a \verb:(exist x p): we may in turn extract its witness
 
412
\verb|x:A| (using an elimination construct such as \verb:match:) but
 
413
{\sl not} its justification, which stays hidden, like in an abstract
 
414
data-type. In technical terms, one says that \verb:sig: is a ``weak
 
415
(dependent) sum''.  A variant \verb:sig2: with two predicates is also
 
416
provided.
 
417
 
 
418
\index{\{x:A "| (P x)\}}
 
419
\index{"|}
 
420
\ttindex{sig}
 
421
\ttindex{exist}
 
422
\ttindex{sig2}
 
423
\ttindex{exist2}
 
424
 
 
425
\begin{coq_example*}
 
426
Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
 
427
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
 
428
  exist2 (x:A) (_:P x) (_:Q x).
 
429
\end{coq_example*}
 
430
 
 
431
A ``strong (dependent) sum'' \verb+{x:A & P x}+ may be also defined,
 
432
when the predicate \verb:P: is now defined as a 
 
433
constructor of types in \verb:Type:.
 
434
 
 
435
\ttindex{\{x:A \& (P x)\}}
 
436
\ttindex{\&}
 
437
\ttindex{sigT}
 
438
\ttindex{existT}
 
439
\ttindex{projT1}
 
440
\ttindex{projT2}
 
441
\ttindex{sigT2}
 
442
\ttindex{existT2}
 
443
 
 
444
\begin{coq_example*}
 
445
Inductive sigT (A:Type) (P:A -> Type) : Type := existT (x:A) (_:P x).
 
446
Section Projections.
 
447
Variable A : Type.
 
448
Variable P : A -> Type.
 
449
Definition projT1 (H:sigT A P) := let (x, h) := H in x.
 
450
Definition projT2 (H:sigT A P) :=
 
451
  match H return P (projT1 H) with
 
452
    existT x h => h
 
453
  end.
 
454
End Projections.
 
455
Inductive sigT2 (A: Type) (P Q:A -> Type) : Type :=
 
456
    existT2 (x:A) (_:P x) (_:Q x).
 
457
\end{coq_example*}
 
458
 
 
459
A related non-dependent construct is the constructive sum
 
460
\verb"{A}+{B}" of two propositions \verb:A: and \verb:B:.
 
461
\label{sumbool}
 
462
\ttindex{sumbool}
 
463
\ttindex{left}
 
464
\ttindex{right}
 
465
\ttindex{\{A\}+\{B\}}
 
466
 
 
467
\begin{coq_example*}
 
468
Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
 
469
\end{coq_example*}
 
470
 
 
471
This \verb"sumbool" construct may be used as a kind of indexed boolean
 
472
data-type. An intermediate between \verb"sumbool" and \verb"sum" is
 
473
the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop"
 
474
in the \verb"Set" \verb"A+{B}".
 
475
\ttindex{sumor}
 
476
\ttindex{inleft}
 
477
\ttindex{inright}
 
478
\ttindex{A+\{B\}}
 
479
 
 
480
\begin{coq_example*}
 
481
Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
 
482
\end{coq_example*}
 
483
 
 
484
We may define variants of the axiom of choice, like in Martin-L�f's
 
485
Intuitionistic Type Theory.
 
486
\ttindex{Choice}
 
487
\ttindex{Choice2}
 
488
\ttindex{bool\_choice}
 
489
 
 
490
\begin{coq_example*}
 
491
Lemma Choice :
 
492
 forall (S S':Set) (R:S -> S' -> Prop),
 
493
   (forall x:S, {y : S' | R x y}) ->
 
494
   {f : S -> S' | forall z:S, R z (f z)}.
 
495
Lemma Choice2 :
 
496
 forall (S S':Set) (R:S -> S' -> Set),
 
497
   (forall x:S, {y : S' &  R x y}) ->
 
498
   {f : S -> S' &  forall z:S, R z (f z)}.
 
499
Lemma bool_choice :
 
500
 forall (S:Set) (R1 R2:S -> Prop),
 
501
   (forall x:S, {R1 x} + {R2 x}) ->
 
502
   {f : S -> bool |
 
503
   forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
 
504
\end{coq_example*}
 
505
\begin{coq_eval}
 
506
Abort.
 
507
Abort.
 
508
Abort.
 
509
\end{coq_eval}
 
510
 
 
511
The next construct builds a sum between a data-type \verb|A:Type| and
 
512
an exceptional value encoding errors:
 
513
 
 
514
\ttindex{Exc}
 
515
\ttindex{value}
 
516
\ttindex{error}
 
517
 
 
518
\begin{coq_example*}
 
519
Definition Exc := option.
 
520
Definition value := Some.
 
521
Definition error := None.
 
522
\end{coq_example*}
 
523
 
 
524
 
 
525
This module ends with theorems, 
 
526
relating the sorts \verb:Set: or \verb:Type: and
 
527
\verb:Prop: in a way which is consistent with the realizability
 
528
interpretation.
 
529
\ttindex{False\_rect}
 
530
\ttindex{False\_rec}
 
531
\ttindex{eq\_rect}
 
532
\ttindex{absurd\_set}
 
533
\ttindex{and\_rect}
 
534
 
 
535
\begin{coq_example*}
 
536
Definition except := False_rec.
 
537
Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
 
538
Theorem and_rect :
 
539
 forall (A B:Prop) (P:Type), (A -> B -> P) -> A /\ B -> P.
 
540
\end{coq_example*}
 
541
%\begin{coq_eval}
 
542
%Abort.
 
543
%Abort.
 
544
%\end{coq_eval}
 
545
 
 
546
\subsection{Basic Arithmetics}
 
547
 
 
548
The basic library includes a few elementary properties of natural
 
549
numbers, together with the definitions of predecessor, addition and
 
550
multiplication\footnote{This is in module {\tt Peano.v}}. It also
 
551
provides a scope {\tt nat\_scope} gathering standard notations for
 
552
common operations (+, *) and a decimal notation for numbers. That is he
 
553
can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on
 
554
the left hand side of a \texttt{match} expression (see for example
 
555
section~\ref{refine-example}). This scope is opened by default.
 
556
 
 
557
%Remove the redefinition of nat
 
558
\begin{coq_eval}
 
559
Reset Initial.
 
560
\end{coq_eval}
 
561
 
 
562
The following example is not part of the standard library, but it
 
563
shows the usage of the notations:
 
564
 
 
565
\begin{coq_example*}
 
566
Fixpoint even (n:nat) : bool :=
 
567
  match n with
 
568
  | 0 => true
 
569
  | 1 => false
 
570
  | S (S n) => even n
 
571
  end.
 
572
\end{coq_example*}
 
573
 
 
574
 
 
575
\ttindex{eq\_S}
 
576
\ttindex{pred}
 
577
\ttindex{pred\_Sn}
 
578
\ttindex{eq\_add\_S}
 
579
\ttindex{not\_eq\_S}
 
580
\ttindex{IsSucc}
 
581
\ttindex{O\_S}
 
582
\ttindex{n\_Sn}
 
583
\ttindex{plus}
 
584
\ttindex{plus\_n\_O}
 
585
\ttindex{plus\_n\_Sm}
 
586
\ttindex{mult}
 
587
\ttindex{mult\_n\_O}
 
588
\ttindex{mult\_n\_Sm}
 
589
 
 
590
\begin{coq_example*}
 
591
Theorem eq_S : forall x y:nat, x = y -> S x = S y.
 
592
\end{coq_example*}
 
593
\begin{coq_eval}
 
594
Abort.
 
595
\end{coq_eval}
 
596
\begin{coq_example*}
 
597
Definition pred (n:nat) : nat :=
 
598
  match n with
 
599
  | 0 => 0
 
600
  | S u => u
 
601
  end.
 
602
Theorem pred_Sn : forall m:nat, m = pred (S m).
 
603
Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
 
604
Hint Immediate eq_add_S : core.
 
605
Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
 
606
\end{coq_example*}
 
607
\begin{coq_eval}
 
608
Abort All.
 
609
\end{coq_eval}
 
610
\begin{coq_example*}
 
611
Definition IsSucc (n:nat) : Prop :=
 
612
  match n with
 
613
  | 0 => False
 
614
  | S p => True
 
615
  end.
 
616
Theorem O_S : forall n:nat, 0 <> S n.
 
617
Theorem n_Sn : forall n:nat, n <> S n.
 
618
\end{coq_example*}
 
619
\begin{coq_eval}
 
620
Abort All.
 
621
\end{coq_eval}
 
622
\begin{coq_example*}
 
623
Fixpoint plus (n m:nat) {struct n} : nat :=
 
624
  match n with
 
625
  | 0 => m
 
626
  | S p => S (p + m)
 
627
  end.
 
628
where "n + m" := (plus n m) : nat_scope.
 
629
Lemma plus_n_O : forall n:nat, n = n + 0.
 
630
Lemma plus_n_Sm : forall n m:nat, S (n + m) = n + S m.
 
631
\end{coq_example*}
 
632
\begin{coq_eval}
 
633
Abort All.
 
634
\end{coq_eval}
 
635
\begin{coq_example*}
 
636
Fixpoint mult (n m:nat) {struct n} : nat :=
 
637
  match n with
 
638
  | 0 => 0
 
639
  | S p => m + p * m
 
640
  end.
 
641
where "n * m" := (mult n m) : nat_scope.
 
642
Lemma mult_n_O : forall n:nat, 0 = n * 0.
 
643
Lemma mult_n_Sm : forall n m:nat, n * m + n = n * (S m).
 
644
\end{coq_example*}
 
645
\begin{coq_eval}
 
646
Abort All.
 
647
\end{coq_eval}
 
648
 
 
649
Finally, it gives the definition of the usual orderings \verb:le:,
 
650
\verb:lt:, \verb:ge:, and \verb:gt:.
 
651
\ttindex{le}
 
652
\ttindex{le\_n}
 
653
\ttindex{le\_S}
 
654
\ttindex{lt}
 
655
\ttindex{ge}
 
656
\ttindex{gt}
 
657
 
 
658
\begin{coq_example*}
 
659
Inductive le (n:nat) : nat -> Prop :=
 
660
  | le_n : le n n
 
661
  | le_S : forall m:nat, n <= m -> n <= (S m).
 
662
where "n <= m" := (le n m) : nat_scope.
 
663
Definition lt (n m:nat) := S n <= m.
 
664
Definition ge (n m:nat) := m <= n.
 
665
Definition gt (n m:nat) := m < n.
 
666
\end{coq_example*}
 
667
 
 
668
Properties of these relations are not initially known, but may be
 
669
required by the user from modules \verb:Le: and \verb:Lt:.  Finally,
 
670
\verb:Peano: gives some lemmas allowing pattern-matching, and a double
 
671
induction principle.
 
672
 
 
673
\ttindex{nat\_case}
 
674
\ttindex{nat\_double\_ind}
 
675
 
 
676
\begin{coq_example*}
 
677
Theorem nat_case :
 
678
 forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
 
679
\end{coq_example*}
 
680
\begin{coq_eval}
 
681
Abort All.
 
682
\end{coq_eval}
 
683
\begin{coq_example*}
 
684
Theorem nat_double_ind :
 
685
 forall R:nat -> nat -> Prop,
 
686
   (forall n:nat, R 0 n) ->
 
687
   (forall n:nat, R (S n) 0) ->
 
688
   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
 
689
\end{coq_example*}
 
690
\begin{coq_eval}
 
691
Abort All.
 
692
\end{coq_eval}
 
693
 
 
694
\subsection{Well-founded recursion}
 
695
 
 
696
The basic library contains the basics of well-founded recursion and 
 
697
well-founded induction\footnote{This is defined in module {\tt Wf.v}}.
 
698
\index{Well foundedness}
 
699
\index{Recursion}
 
700
\index{Well founded induction}
 
701
\ttindex{Acc}
 
702
\ttindex{Acc\_inv}
 
703
\ttindex{Acc\_rect}
 
704
\ttindex{well\_founded}
 
705
 
 
706
\begin{coq_example*}
 
707
Section Well_founded.
 
708
Variable A : Type.
 
709
Variable R : A -> A -> Prop.
 
710
Inductive Acc (x:A) : Prop :=
 
711
    Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
 
712
Lemma Acc_inv : Acc x -> forall y:A, R y x -> Acc y.
 
713
\end{coq_example*}
 
714
\begin{coq_eval}
 
715
destruct 1; trivial.
 
716
Defined.
 
717
\end{coq_eval}
 
718
%% Acc_rect now primitively defined
 
719
%% Section AccRec.
 
720
%% Variable P : A -> Set.
 
721
%% Variable F :
 
722
%%     forall x:A,
 
723
%%       (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
 
724
%% Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
 
725
%%   F x (Acc_inv x a)
 
726
%%     (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
 
727
%% End AccRec.
 
728
\begin{coq_example*}
 
729
Definition well_founded := forall a:A, Acc a.
 
730
Hypothesis Rwf : well_founded.
 
731
Theorem well_founded_induction :
 
732
 forall P:A -> Set,
 
733
   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 
734
Theorem well_founded_ind :
 
735
 forall P:A -> Prop,
 
736
   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
 
737
\end{coq_example*}
 
738
\begin{coq_eval}
 
739
Abort All.
 
740
\end{coq_eval}
 
741
The automatically generated scheme {\tt Acc\_rect} 
 
742
can be used to define functions by fixpoints using
 
743
well-founded relations to  justify termination. Assuming
 
744
extensionality of the functional used for the recursive call, the
 
745
fixpoint equation can be proved.
 
746
\ttindex{Fix\_F}
 
747
\ttindex{fix\_eq}
 
748
\ttindex{Fix\_F\_inv}
 
749
\ttindex{Fix\_F\_eq}
 
750
\begin{coq_example*}
 
751
Section FixPoint.
 
752
Variable P : A -> Type.
 
753
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
 
754
Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
 
755
  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
 
756
Definition Fix (x:A) := Fix_F x (Rwf x).
 
757
Hypothesis F_ext :
 
758
    forall (x:A) (f g:forall y:A, R y x -> P y),
 
759
      (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
 
760
Lemma Fix_F_eq :
 
761
 forall (x:A) (r:Acc x),
 
762
   F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
 
763
Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
 
764
Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
 
765
\end{coq_example*}
 
766
\begin{coq_eval}
 
767
Abort All.
 
768
\end{coq_eval}
 
769
\begin{coq_example*}
 
770
End FixPoint.
 
771
End Well_founded.
 
772
\end{coq_example*}
 
773
 
 
774
\subsection{Accessing the {\Type} level}
 
775
 
 
776
The basic library includes the definitions\footnote{This is in module
 
777
{\tt Logic\_Type.v}} of the counterparts of some data-types and logical
 
778
quantifiers at the \verb:Type: level: negation, pair, and properties
 
779
of {\tt identity}.
 
780
 
 
781
\ttindex{notT}
 
782
\ttindex{prodT}
 
783
\ttindex{pairT}
 
784
\begin{coq_eval}
 
785
Reset Initial.
 
786
\end{coq_eval}
 
787
\begin{coq_example*}
 
788
Definition notT (A:Type) := A -> False.
 
789
Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
 
790
\end{coq_example*}
 
791
 
 
792
At the end, it defines data-types at the {\Type} level.
 
793
 
 
794
\subsection{Tactics}
 
795
 
 
796
A few tactics defined at the user level are provided in the initial
 
797
state\footnote{This is in module {\tt Tactics.v}}.
 
798
 
 
799
\section{The standard library}
 
800
 
 
801
\subsection{Survey}
 
802
 
 
803
The rest of the standard library is structured into the following 
 
804
subdirectories:
 
805
 
 
806
\begin{tabular}{lp{12cm}}
 
807
  {\bf Logic}   & Classical logic and dependent equality \\
 
808
  {\bf Arith}   & Basic Peano arithmetic \\
 
809
  {\bf NArith}  & Basic positive integer arithmetic \\
 
810
  {\bf ZArith}  & Basic relative integer arithmetic \\
 
811
  {\bf Numbers} & Various approaches to natural, integer and cyclic numbers (currently axiomatically and on top of 2$^{31}$ binary words) \\
 
812
  {\bf Bool}    & Booleans (basic functions and results) \\
 
813
  {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
 
814
            results), Streams (infinite sequences defined with co-inductive
 
815
            types) \\
 
816
  {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
 
817
            etc.) \\
 
818
  {\bf FSets}   & Specification and implementations of finite sets and finite
 
819
                  maps (by lists and by AVL trees)\\
 
820
 {\bf Reals}    & Axiomatization of real numbers (classical, basic functions, 
 
821
                  integer part, fractional part, limit, derivative, Cauchy 
 
822
                  series, power series and results,...)\\
 
823
 {\bf Relations} & Relations (definitions and basic results) \\
 
824
 {\bf Sorting}  & Sorted list (basic definitions and heapsort correctness) \\
 
825
 {\bf Strings}  & 8-bits characters and strings\\
 
826
 {\bf Wellfounded} & Well-founded relations (basic results) \\
 
827
 
 
828
\end{tabular}
 
829
\medskip
 
830
 
 
831
These directories belong to the initial load path of the system, and
 
832
the modules they provide are compiled at installation time. So they
 
833
are directly accessible with the command \verb!Require! (see
 
834
Chapter~\ref{Other-commands}). 
 
835
 
 
836
The different modules of the \Coq\ standard library are described in the
 
837
additional document \verb!Library.dvi!. They are also accessible on the WWW
 
838
through the \Coq\ homepage
 
839
\footnote{\texttt{http://coq.inria.fr}}.
 
840
 
 
841
\subsection[Notations for integer arithmetics]{Notations for integer arithmetics\index{Arithmetical notations}}
 
842
 
 
843
On Figure~\ref{zarith-syntax} is described the syntax of expressions
 
844
for integer arithmetics. It is provided by requiring and opening the
 
845
module {\tt ZArith} and opening scope {\tt Z\_scope}.
 
846
 
 
847
\ttindex{+}
 
848
\ttindex{*}
 
849
\ttindex{-}
 
850
\ttindex{/}
 
851
\ttindex{<=}
 
852
\ttindex{>=}
 
853
\ttindex{<}
 
854
\ttindex{>}
 
855
\ttindex{?=}
 
856
\ttindex{mod}
 
857
 
 
858
\begin{figure}
 
859
\begin{center}
 
860
\begin{tabular}{l|l|l|l}
 
861
Notation & Interpretation & Precedence & Associativity\\
 
862
\hline
 
863
\verb!_ < _! & {\tt Zlt} &&\\
 
864
\verb!x <= y! & {\tt Zle} &&\\
 
865
\verb!_ > _! & {\tt Zgt} &&\\
 
866
\verb!x >= y! & {\tt Zge} &&\\
 
867
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
 
868
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
 
869
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
 
870
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
 
871
\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
 
872
\verb!_ + _! & {\tt Zplus} &&\\
 
873
\verb!_ - _! & {\tt Zminus} &&\\
 
874
\verb!_ * _! & {\tt Zmult} &&\\
 
875
\verb!_ / _! & {\tt Zdiv} &&\\
 
876
\verb!_ mod _! & {\tt Zmod} & 40 & no \\
 
877
\verb!- _!  & {\tt Zopp} &&\\
 
878
\verb!_ ^ _! & {\tt Zpower} &&\\
 
879
\end{tabular}
 
880
\end{center}
 
881
\label{zarith-syntax}
 
882
\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
 
883
\end{figure}
 
884
 
 
885
Figure~\ref{zarith-syntax} shows the notations provided by {\tt
 
886
Z\_scope}. It specifies how notations are interpreted and, when not
 
887
already reserved, the precedence and associativity.
 
888
 
 
889
\begin{coq_example}
 
890
Require Import ZArith.
 
891
Check  (2 + 3)%Z.
 
892
Open Scope Z_scope.
 
893
Check 2 + 3.
 
894
\end{coq_example}
 
895
 
 
896
\subsection[Peano's arithmetic (\texttt{nat})]{Peano's arithmetic (\texttt{nat})\index{Peano's arithmetic}
 
897
\ttindex{nat\_scope}}
 
898
 
 
899
While in the initial state, many operations and predicates of Peano's
 
900
arithmetic are defined, further operations and results belong to other
 
901
modules. For instance, the decidability of the basic predicates are
 
902
defined here. This is provided by requiring the module {\tt Arith}.
 
903
 
 
904
Figure~\ref{nat-syntax} describes notation available in scope {\tt
 
905
nat\_scope}.
 
906
 
 
907
\begin{figure}
 
908
\begin{center}
 
909
\begin{tabular}{l|l}
 
910
Notation & Interpretation \\
 
911
\hline
 
912
\verb!_ < _! & {\tt lt} \\
 
913
\verb!x <= y! & {\tt le} \\
 
914
\verb!_ > _! & {\tt gt} \\
 
915
\verb!x >= y! & {\tt ge} \\
 
916
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
 
917
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
 
918
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
 
919
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
 
920
\verb!_ + _! & {\tt plus} \\
 
921
\verb!_ - _! & {\tt minus} \\
 
922
\verb!_ * _! & {\tt mult} \\
 
923
\end{tabular}
 
924
\end{center}
 
925
\label{nat-syntax}
 
926
\caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
 
927
\end{figure}
 
928
 
 
929
\subsection{Real numbers library}
 
930
 
 
931
\subsubsection[Notations for real numbers]{Notations for real numbers\index{Notations for real numbers}}
 
932
 
 
933
This is provided by requiring and opening the module {\tt Reals} and
 
934
opening scope {\tt R\_scope}. This set of notations is very similar to
 
935
the notation for integer arithmetics. The inverse function was added.
 
936
\begin{figure}
 
937
\begin{center}
 
938
\begin{tabular}{l|l}
 
939
Notation & Interpretation \\
 
940
\hline
 
941
\verb!_ < _! & {\tt Rlt} \\
 
942
\verb!x <= y! & {\tt Rle} \\
 
943
\verb!_ > _! & {\tt Rgt} \\
 
944
\verb!x >= y! & {\tt Rge} \\
 
945
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
 
946
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
 
947
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
 
948
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
 
949
\verb!_ + _! & {\tt Rplus} \\
 
950
\verb!_ - _! & {\tt Rminus} \\
 
951
\verb!_ * _! & {\tt Rmult} \\
 
952
\verb!_ / _! & {\tt Rdiv} \\
 
953
\verb!- _!  & {\tt Ropp} \\
 
954
\verb!/ _!  & {\tt Rinv} \\
 
955
\verb!_ ^ _! & {\tt pow} \\
 
956
\end{tabular}
 
957
\end{center}
 
958
\label{reals-syntax}
 
959
\caption{Definition of the scope for real arithmetics ({\tt R\_scope})}
 
960
\end{figure}
 
961
 
 
962
\begin{coq_eval}
 
963
Reset Initial.
 
964
\end{coq_eval}
 
965
\begin{coq_example}
 
966
Require Import Reals.
 
967
Check  (2 + 3)%R.
 
968
Open Scope R_scope.
 
969
Check 2 + 3.
 
970
\end{coq_example}
 
971
 
 
972
\subsubsection{Some tactics}
 
973
 
 
974
In addition to the \verb|ring|, \verb|field| and \verb|fourier|
 
975
tactics (see Chapter~\ref{Tactics}) there are:
 
976
\begin{itemize}
 
977
\item {\tt discrR} \tacindex{discrR}
 
978
  
 
979
  Proves that a real integer constant $c_1$ is different from another
 
980
  real integer constant $c_2$.  
 
981
 
 
982
\begin{coq_example*}
 
983
Require Import DiscrR.
 
984
Goal 5 <> 0.
 
985
\end{coq_example*}
 
986
 
 
987
\begin{coq_example}
 
988
discrR.
 
989
\end{coq_example}
 
990
 
 
991
\begin{coq_eval}
 
992
Abort.
 
993
\end{coq_eval}
 
994
 
 
995
\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits 
 
996
corresponding conjonctions.
 
997
\tacindex{split\_Rabs}
 
998
 
 
999
\begin{coq_example*}
 
1000
Require Import SplitAbsolu.
 
1001
Goal forall x:R, x <= Rabs x.
 
1002
\end{coq_example*}
 
1003
 
 
1004
\begin{coq_example}
 
1005
intro; split_Rabs.
 
1006
\end{coq_example}
 
1007
 
 
1008
\begin{coq_eval}
 
1009
Abort.
 
1010
\end{coq_eval}
 
1011
 
 
1012
\item {\tt split\_Rmult} allows to split a condition that a product is
 
1013
  non null into subgoals corresponding to the condition on each
 
1014
  operand of the product. 
 
1015
\tacindex{split\_Rmult}
 
1016
 
 
1017
\begin{coq_example*}
 
1018
Require Import SplitRmult.
 
1019
Goal forall x y z:R, x * y * z <> 0.
 
1020
\end{coq_example*}
 
1021
 
 
1022
\begin{coq_example}
 
1023
intros; split_Rmult.
 
1024
\end{coq_example}
 
1025
 
 
1026
\end{itemize}
 
1027
 
 
1028
All this tactics has been written with the tactic language Ltac
 
1029
described in Chapter~\ref{TacticLanguage}.  More details are available
 
1030
in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
 
1031
 
 
1032
\begin{coq_eval}
 
1033
Reset Initial.
 
1034
\end{coq_eval}
 
1035
 
 
1036
\subsection[List library]{List library\index{Notations for lists}
 
1037
\ttindex{length}
 
1038
\ttindex{head}
 
1039
\ttindex{tail}
 
1040
\ttindex{app}
 
1041
\ttindex{rev}
 
1042
\ttindex{nth}
 
1043
\ttindex{map}
 
1044
\ttindex{flat\_map}
 
1045
\ttindex{fold\_left}
 
1046
\ttindex{fold\_right}}
 
1047
 
 
1048
Some elementary operations on polymorphic lists are defined here. They
 
1049
can be accessed by requiring module {\tt List}.
 
1050
 
 
1051
It defines the following notions:
 
1052
\begin{center}
 
1053
\begin{tabular}{l|l}
 
1054
\hline
 
1055
{\tt length} & length \\
 
1056
{\tt head} & first element (with default) \\
 
1057
{\tt tail} & all but first element \\
 
1058
{\tt app} & concatenation \\
 
1059
{\tt rev} & reverse \\
 
1060
{\tt nth} & accessing $n$-th element (with default) \\
 
1061
{\tt map} & applying a function \\
 
1062
{\tt flat\_map} & applying a function returning lists \\
 
1063
{\tt fold\_left} & iterator (from head to tail) \\
 
1064
{\tt fold\_right} & iterator (from tail to head) \\
 
1065
\hline
 
1066
\end{tabular}
 
1067
\end{center}
 
1068
 
 
1069
Table show notations available when opening scope {\tt list\_scope}.
 
1070
 
 
1071
\begin{figure}
 
1072
\begin{center}
 
1073
\begin{tabular}{l|l|l|l}
 
1074
Notation & Interpretation & Precedence & Associativity\\
 
1075
\hline
 
1076
\verb!_ ++ _! & {\tt app} & 60 & right \\
 
1077
\verb!_ :: _! & {\tt cons} & 60 & right \\
 
1078
\end{tabular}
 
1079
\end{center}
 
1080
\label{list-syntax}
 
1081
\caption{Definition of the scope for lists ({\tt list\_scope})}
 
1082
\end{figure}
 
1083
 
 
1084
 
 
1085
\section[Users' contributions]{Users' contributions\index{Contributions}
 
1086
\label{Contributions}}
 
1087
 
 
1088
Numerous users' contributions have been collected and are available at
 
1089
URL \url{coq.inria.fr/contribs/}.  On this web page, you have a list
 
1090
of all contributions with informations (author, institution, quick
 
1091
description, etc.) and the possibility to download them one by one.
 
1092
There is a small search engine to look for keywords in all
 
1093
contributions.  You will also find informations on how to submit a new
 
1094
contribution.
 
1095
 
 
1096
The users' contributions may also be obtained by anonymous FTP from site
 
1097
\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
 
1098
searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}
 
1099
 
 
1100
% $Id: RefMan-lib.tex 11793 2009-01-17 11:39:48Z herbelin $ 
 
1101
 
 
1102
%%% Local Variables: 
 
1103
%%% mode: latex
 
1104
%%% TeX-master: "Reference-Manual"
 
1105
%%% End: