1
\chapter{The {\Coq} library}
2
\index{Theories}\label{Theories}
4
The \Coq\ library is structured into three parts:
7
\item[The initial library:] it contains
8
elementary logical notions and datatypes. It constitutes the
9
basic state of the system directly available when running
12
\item[The standard library:] general-purpose libraries containing
13
various developments of \Coq\ axiomatizations about sets, lists,
14
sorting, arithmetic, etc. This library comes with the system and its
15
modules are directly accessible through the \verb!Require! command
16
(see section~\ref{Require});
18
\item[User contributions:] Other specification and proof developments
19
coming from the \Coq\ users' community. These libraries are
20
available for download at \texttt{http://coq.inria.fr} (see
21
section~\ref{Contributions}).
24
This chapter briefly reviews these libraries.
26
\section{The basic library}
29
This section lists the basic notions and results which are directly
30
available in the standard \Coq\ system\footnote{Most
31
of these constructions are defined in the
32
{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
33
root directory; this includes the modules
40
Module {\tt Logic\_Type} also makes it in the initial state}.
42
\subsection{Notations} \label{Notations}
44
This module defines the parsing and pretty-printing of many symbols
45
(infixes, prefixes, etc.). However, it does not assign a meaning to these
46
notations. The purpose of this is to define precedence and
47
associativity of very common notations, and avoid users to use them
48
with other precedence, which may be confusing.
52
\begin{tabular}{|cll|}
54
Notation & Precedence & Associativity \\
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!_ * _! & 40 & left \\
76
\verb!_ / _! & 40 & left \\
77
\verb!- _! & 35 & right \\
78
\verb!/ _! & 35 & right \\
79
\verb!_ ^ _! & 30 & right \\
83
\caption{Notations in the initial state}
84
\label{init-notations}
93
{\form} & ::= & {\tt True} & ({\tt True})\\
94
& $|$ & {\tt False} & ({\tt False})\\
95
& $|$ & {\tt\char'176} {\form} & ({\tt not})\\
96
& $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\
97
& $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
98
& $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
99
& $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\
100
& $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,}
101
{\form} & (\em{primitive for all})\\
102
& $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt
103
,} {\form} & ({\tt ex})\\
104
& $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
105
,} {\form} {\tt \&} {\form} & ({\tt ex2})\\
106
& $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
107
& $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
110
\caption{Syntax of formulas}
111
\label{formulas-syntax}
114
The basic library of {\Coq} comes with the definitions of standard
115
(intuitionistic) logical connectives (they are defined as inductive
116
constructions). They are equipped with an appealing syntax enriching the
117
(subclass {\form}) of the syntactic class {\term}. The syntax
118
extension is shown on figure \ref{formulas-syntax}.
120
% The basic library of {\Coq} comes with the definitions of standard
121
% (intuitionistic) logical connectives (they are defined as inductive
122
% constructions). They are equipped with an appealing syntax enriching
123
% the (subclass {\form}) of the syntactic class {\term}. The syntax
124
% extension \footnote{This syntax is defined in module {\tt
125
% LogicSyntax}} is shown on Figure~\ref{formulas-syntax}.
127
\Rem Implication is not defined but primitive (it is a non-dependent
128
product of a proposition over another proposition). There is also a
129
primitive universal quantification (it is a dependent product over a
130
proposition). The primitive universal quantification allows both
131
first-order and higher-order quantification.
133
\subsubsection{Propositional Connectives} \label{Connectives}
136
First, we find propositional calculus connectives:
147
Set Printing Depth 50.
150
Inductive True : Prop := I.
151
Inductive False : Prop := .
152
Definition not (A: Prop) := A -> False.
153
Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
155
Variables A B : Prop.
156
Theorem proj1 : A /\ B -> A.
157
Theorem proj2 : A /\ B -> B.
167
\ttindex{IF\_then\_else}
169
Inductive or (A B:Prop) : Prop :=
172
Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
173
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
176
\subsubsection{Quantifiers} \label{Quantifiers}
179
Then we find first-order quantifiers:
189
Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
190
Inductive ex (A: Set) (P:A -> Prop) : Prop :=
191
ex_intro (x:A) (_:P x).
192
Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
193
ex_intro2 (x:A) (_:P x) (_:Q x).
196
The following abbreviations are allowed:
198
\begin{tabular}[h]{|l|l|}
200
\verb+exists x:A, P+ & \verb+ex A (fun x:A => P)+ \\
201
\verb+exists x, P+ & \verb+ex _ (fun x => P)+ \\
202
\verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
203
\verb+exists2 x, P & Q+ & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\
208
The type annotation \texttt{:A} can be omitted when \texttt{A} can be
209
synthesized by the system.
211
\subsubsection{Equality} \label{Equality}
214
Then, we find equality, defined as an inductive relation. That is,
215
given a \verb:Type: \verb:A: and an \verb:x: of type \verb:A:, the
216
predicate \verb:(eq A x): is the smallest one which contains \verb:x:.
217
This definition, due to Christine Paulin-Mohring, is equivalent to
218
define \verb:eq: as the smallest reflexive relation, and it is also
219
equivalent to Leibniz' equality.
222
\ttindex{refl\_equal}
225
Inductive eq (A:Type) (x:A) : A -> Prop :=
226
refl_equal : eq A x x.
229
\subsubsection{Lemmas}
230
\label{PreludeLemmas}
232
Finally, a few easy lemmas are provided.
237
Theorem absurd : forall A C:Prop, A -> ~ A -> C.
245
\ttindex{sym\_not\_eq}
248
Variables A B : Type.
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.
265
\ttindex{eq\_rect\_r}
266
%Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y).
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.
281
%Abort (for now predefined eq_rect)
283
Hint Immediate sym_eq sym_not_eq : core.
285
\ttindex{f\_equal$i$}
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.
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.
300
\subsection{Datatypes}
306
\begin{tabular}{rclr}
307
{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
308
& $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
309
& $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
310
& $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
312
& $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
314
& $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \&}
315
{\form} {\tt \}} & ({\tt sig2})\\
316
& $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
318
& $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
319
\&} {\specif} {\tt \}} & ({\tt sigS2})\\
321
{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
324
\caption{Syntax of datatypes and specifications}
325
\label{specif-syntax}
329
In the basic library, we find the definition\footnote{They are in {\tt
330
Datatypes.v}} of the basic data-types of programming, again
331
defined as inductive constructions over the sort \verb:Set:. Some of
332
them come with a special syntax shown on Figure~\ref{specif-syntax}.
334
\subsubsection{Programming}
351
\ttindex{refl\_identity}
354
Inductive unit : Set := tt.
355
Inductive bool : Set := true | false.
356
Inductive nat : Set := O | S (n:nat).
357
Inductive option (A:Set) : Set := Some (_:A) | None.
358
Inductive identity (A:Type) (a:A) : A -> Type :=
359
refl_identity : identity A a a.
362
Note that zero is the letter \verb:O:, and {\sl not} the numeral
365
{\tt identity} is logically equivalent to equality but it lives in
366
sort {\tt Set}. Computationaly, it behaves like {\tt unit}.
368
We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
369
\verb:B:, and their product \verb:A*B:.
383
Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
384
Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
387
Definition fst (H: prod A B) := match H with
390
Definition snd (H: prod A B) := match H with
396
\subsection{Specification}
398
The following notions\footnote{They are defined in module {\tt
399
Specif.v}} allows to build new datatypes and specifications.
400
They are available with the syntax shown on
401
Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module
402
{\tt SpecifSyntax.v}}.
404
For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct
405
\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a
406
\verb:Set:. We may build elements of this set as \verb:(exist x p):
407
whenever we have a witness \verb|x:A| with its justification
410
From such a \verb:(exist x p): we may in turn extract its witness
411
\verb|x:A| (using an elimination construct such as \verb:match:) but
412
{\sl not} its justification, which stays hidden, like in an abstract
413
data type. In technical terms, one says that \verb:sig: is a ``weak
414
(dependent) sum''. A variant \verb:sig2: with two predicates is also
417
\index{\{x:A "| (P x)\}}
425
Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
426
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set :=
427
exist2 (x:A) (_:P x) (_:Q x).
430
A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
431
when the predicate \verb:P: is now defined as a \verb:Set:
434
\ttindex{\{x:A \& (P x)\}}
444
Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x).
445
Section sigSprojections.
447
Variable P : A -> Set.
448
Definition projS1 (H:sigS A P) := let (x, h) := H in x.
449
Definition projS2 (H:sigS A P) :=
450
match H return P (projS1 H) with
454
Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
455
existS2 (x:A) (_:P x) (_:Q x).
458
A related non-dependent construct is the constructive sum
459
\verb"{A}+{B}" of two propositions \verb:A: and \verb:B:.
464
\ttindex{\{A\}+\{B\}}
467
Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
470
This \verb"sumbool" construct may be used as a kind of indexed boolean
471
data type. An intermediate between \verb"sumbool" and \verb"sum" is
472
the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop"
473
in the \verb"Set" \verb"A+{B}".
480
Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
483
We may define variants of the axiom of choice, like in Martin-L�f's
484
Intuitionistic Type Theory.
487
\ttindex{bool\_choice}
491
forall (S S':Set) (R:S -> S' -> Prop),
492
(forall x:S, {y : S' | R x y}) ->
493
{f : S -> S' | forall z:S, R z (f z)}.
495
forall (S S':Set) (R:S -> S' -> Set),
496
(forall x:S, {y : S' & R x y}) ->
497
{f : S -> S' & forall z:S, R z (f z)}.
499
forall (S:Set) (R1 R2:S -> Prop),
500
(forall x:S, {R1 x} + {R2 x}) ->
502
forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
510
The next constructs builds a sum between a data type \verb|A:Set| and
511
an exceptional value encoding errors:
518
Definition Exc := option.
519
Definition value := Some.
520
Definition error := None.
524
This module ends with theorems,
525
relating the sorts \verb:Set: and
526
\verb:Prop: in a way which is consistent with the realizability
531
\ttindex{absurd\_set}
534
%Lemma False_rec : (P:Set)False->P.
535
%Lemma False_rect : (P:Type)False->P.
537
Definition except := False_rec.
538
Notation Except := (except _).
539
Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
541
forall (A B:Prop) (P:Set), (A -> B -> P) -> A /\ B -> P.
548
\subsection{Basic Arithmetics}
550
The basic library includes a few elementary properties of natural
551
numbers, together with the definitions of predecessor, addition and
552
multiplication\footnote{This is in module {\tt Peano.v}}. It also
553
provides a scope {\tt nat\_scope} gathering standard notations for
554
common operations (+,*) and a decimal notation for numbers. That is he
555
can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on
556
the left hand side of a \texttt{match} expression (see for example
557
section~\ref{refine-example}). This scope is opened by default.
559
%Remove the redefinition of nat
564
The following example is not part of the standard library, but it
565
shows the usage of the notations:
568
Fixpoint even (n:nat) : bool :=
587
\ttindex{plus\_n\_Sm}
590
\ttindex{mult\_n\_Sm}
593
Theorem eq_S : forall x y:nat, x = y -> S x = S y.
599
Definition pred (n:nat) : nat :=
604
Theorem pred_Sn : forall m:nat, m = pred (S m).
605
Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
606
Hint Immediate eq_add_S : core.
607
Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
613
Definition IsSucc (n:nat) : Prop :=
618
Theorem O_S : forall n:nat, 0 <> S n.
619
Theorem n_Sn : forall n:nat, n <> S n.
625
Fixpoint plus (n m:nat) {struct n} : nat :=
628
| S p => S (plus p m)
630
Lemma plus_n_O : forall n:nat, n = plus n 0.
631
Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m).
637
Fixpoint mult (n m:nat) {struct n} : nat :=
640
| S p => m + mult p m
642
Lemma mult_n_O : forall n:nat, 0 = mult n 0.
643
Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m).
649
Finally, it gives the definition of the usual orderings \verb:le:,
650
\verb:lt:, \verb:ge:, and \verb:gt:.
660
Inductive le (n:nat) : nat -> Prop :=
662
| le_S : forall m:nat, le n m -> le n (S m).
663
Infix "+" := plus : nat_scope.
664
Definition lt (n m:nat) := S n <= m.
665
Definition ge (n m:nat) := m <= n.
666
Definition gt (n m:nat) := m < n.
669
Properties of these relations are not initially known, but may be
670
required by the user from modules \verb:Le: and \verb:Lt:. Finally,
671
\verb:Peano: gives some lemmas allowing pattern-matching, and a double
675
\ttindex{nat\_double\_ind}
679
forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
685
Theorem nat_double_ind :
686
forall R:nat -> nat -> Prop,
687
(forall n:nat, R 0 n) ->
688
(forall n:nat, R (S n) 0) ->
689
(forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
695
\subsection{Well-founded recursion}
697
The basic library contains the basics of well-founded recursion and
698
well-founded induction\footnote{This is defined in module {\tt Wf.v}}.
699
\index{Well foundedness}
701
\index{Well founded induction}
705
\ttindex{well\_founded}
708
Section Well_founded.
710
Variable R : A -> A -> Prop.
711
Inductive Acc : A -> Prop :=
712
Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
713
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
716
simple destruct 1; trivial.
721
Variable P : A -> Set.
724
(forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
725
Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
727
(fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
729
Definition well_founded := forall a:A, Acc a.
730
Hypothesis Rwf : well_founded.
731
Theorem well_founded_induction :
733
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
734
Theorem well_founded_ind :
736
(forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
741
{\tt Acc\_rec} can be used to define functions by fixpoints using
742
well-founded relations to justify termination. Assuming
743
extensionality of the functional used for the recursive call, the
744
fixpoint equation can be proved.
747
\ttindex{Fix\_F\_inv}
751
Variable P : A -> Set.
752
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
753
Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
754
F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
755
Definition Fix (x:A) := Fix_F x (Rwf x).
757
forall (x:A) (f g:forall y:A, R y x -> P y),
758
(forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
760
forall (x:A) (r:Acc x),
761
F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
762
Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
763
Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
773
\subsection{Accessing the {\Type} level}
775
The basic library includes the definitions\footnote{This is in module
776
{\tt Logic\_Type.v}} of the counterparts of some datatypes and logical
777
quantifiers at the \verb:Type: level: negation, pair, and properties
787
Definition notT (A:Type) := A -> False.
788
Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
792
At the end, it defines datatypes at the {\Type} level.
794
\section{The standard library}
798
The rest of the standard library is structured into the following
801
\begin{tabular}{lp{12cm}}
802
{\bf Logic} & Classical logic and dependent equality \\
803
{\bf Arith} & Basic Peano arithmetic \\
804
{\bf NArith} & Basic positive integer arithmetic \\
805
{\bf ZArith} & Basic relative integer arithmetic \\
806
{\bf Bool} & Booleans (basic functions and results) \\
807
{\bf Lists} & Monomorphic and polymorphic lists (basic functions and
808
results), Streams (infinite sequences defined with co-inductive
810
{\bf Sets} & Sets (classical, constructive, finite, infinite, power set,
812
{\bf FSets} & Specification and implementations of finite sets and finite
813
maps (by lists and by AVL trees)\\
814
{\bf IntMap} & Representation of finite sets by an efficient
815
structure of map (trees indexed by binary integers).\\
816
{\bf Reals} & Axiomatization of real numbers (classical, basic functions,
817
integer part, fractional part, limit, derivative, Cauchy
818
series, power series and results,...)\\
819
{\bf Relations} & Relations (definitions and basic results). \\
820
{\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
821
{\bf Strings} & 8-bits characters and strings\\
822
{\bf Wellfounded} & Well-founded relations (basic results). \\
827
These directories belong to the initial load path of the system, and
828
the modules they provide are compiled at installation time. So they
829
are directly accessible with the command \verb!Require! (see
830
chapter~\ref{Other-commands}).
832
The different modules of the \Coq\ standard library are described in the
833
additional document \verb!Library.dvi!. They are also accessible on the WWW
834
through the \Coq\ homepage
835
\footnote{\texttt{http://coq.inria.fr}}.
837
\subsection{Notations for integer arithmetics}
838
\index{Arithmetical notations}
840
On figure \ref{zarith-syntax} is described the syntax of expressions
841
for integer arithmetics. It is provided by requiring and opening the
842
module {\tt ZArith} and opening scope {\tt Z\_scope}.
857
\begin{tabular}{l|l|l|l}
858
Notation & Interpretation & Precedence & Associativity\\
860
\verb!_ < _! & {\tt Zlt} &&\\
861
\verb!x <= y! & {\tt Zle} &&\\
862
\verb!_ > _! & {\tt Zgt} &&\\
863
\verb!x >= y! & {\tt Zge} &&\\
864
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
865
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
866
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
867
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
868
\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
869
\verb!_ + _! & {\tt Zplus} &&\\
870
\verb!_ - _! & {\tt Zminus} &&\\
871
\verb!_ * _! & {\tt Zmult} &&\\
872
\verb!_ / _! & {\tt Zdiv} &&\\
873
\verb!_ mod _! & {\tt Zmod} & 40 & no \\
874
\verb!- _! & {\tt Zopp} &&\\
875
\verb!_ ^ _! & {\tt Zpower} &&\\
878
\label{zarith-syntax}
879
\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
882
Figure~\ref{zarith-syntax} shows the notations provided by {\tt
883
Z\_scope}. It specifies how notations are interpreted and, when not
884
already reserved, the precedence and associativity.
887
Require Import ZArith.
893
\subsection{Peano's arithmetic (\texttt{nat})}
894
\index{Peano's arithmetic}
897
While in the initial state, many operations and predicates of Peano's
898
arithmetic are defined, further operations and results belong to other
899
modules. For instance, the decidability of the basic predicates are
900
defined here. This is provided by requiring the module {\tt Arith}.
902
Figure~\ref{nat-syntax} describes notation available in scope {\tt
908
Notation & Interpretation \\
910
\verb!_ < _! & {\tt lt} \\
911
\verb!x <= y! & {\tt le} \\
912
\verb!_ > _! & {\tt gt} \\
913
\verb!x >= y! & {\tt ge} \\
914
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
915
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
916
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
917
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
918
\verb!_ + _! & {\tt plus} \\
919
\verb!_ - _! & {\tt minus} \\
920
\verb!_ * _! & {\tt mult} \\
924
\caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
927
\subsection{Real numbers library}
929
\subsubsection{Notations for real numbers}
930
\index{Notations for real numbers}
932
This is provided by requiring and opening the module {\tt Reals} and
933
opening scope {\tt R\_scope}. This set of notations is very similar to
934
the notation for integer arithmetics. The inverse function was added.
938
Notation & Interpretation \\
940
\verb!_ < _! & {\tt Rlt} \\
941
\verb!x <= y! & {\tt Rle} \\
942
\verb!_ > _! & {\tt Rgt} \\
943
\verb!x >= y! & {\tt Rge} \\
944
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
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!_ + _! & {\tt Rplus} \\
949
\verb!_ - _! & {\tt Rminus} \\
950
\verb!_ * _! & {\tt Rmult} \\
951
\verb!_ / _! & {\tt Rdiv} \\
952
\verb!- _! & {\tt Ropp} \\
953
\verb!/ _! & {\tt Rinv} \\
954
\verb!_ ^ _! & {\tt pow} \\
958
\caption{Definition of the scope for real arithmetics ({\tt R\_scope})}
965
Require Import Reals.
971
\subsubsection{Some tactics}
973
In addition to the \verb|ring|, \verb|field| and \verb|fourier|
974
tactics (see Chapter~\ref{Tactics}) there are:
976
\item {\tt discrR} \tacindex{discrR}
978
Proves that a real integer constant $c_1$ is different from another
979
real integer constant $c_2$.
982
Require Import DiscrR.
994
\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits
995
corresponding conjonctions.
996
\tacindex{split\_Rabs}
999
Require Import SplitAbsolu.
1000
Goal forall x:R, x <= Rabs x.
1011
\item {\tt split\_Rmult} allows to split a condition that a product is
1012
non null into subgoals corresponding to the condition on each
1013
operand of the product.
1014
\tacindex{split\_Rmult}
1016
\begin{coq_example*}
1017
Require Import SplitRmult.
1018
Goal forall x y z:R, x * y * z <> 0.
1022
intros; split_Rmult.
1027
All this tactics has been written with the tactic language Ltac
1028
described in Chapter~\ref{TacticLanguage}. More details are available
1029
in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.
1035
\subsection{List library}
1036
\index{Notations for lists}
1045
\ttindex{fold\_left}
1046
\ttindex{fold\_right}
1048
Some elementary operations on polymorphic lists are defined here. They
1049
can be accessed by requiring module {\tt List}.
1051
It defines the following notions:
1053
\begin{tabular}{l|l}
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) \\
1069
Table show notations available when opening scope {\tt list\_scope}.
1073
\begin{tabular}{l|l|l|l}
1074
Notation & Interpretation & Precedence & Associativity\\
1076
\verb!_ ++ _! & {\tt app} & 60 & right \\
1077
\verb!_ :: _! & {\tt cons} & 60 & right \\
1081
\caption{Definition of the scope for lists ({\tt list\_scope})}
1085
\section{Users' contributions}
1086
\index{Contributions}
1087
\label{Contributions}
1089
Numerous users' contributions have been collected and are available at
1090
URL \url{coq.inria.fr/contribs/}. On this web page, you have a list
1091
of all contributions with informations (author, institution, quick
1092
description, etc.) and the possibility to download them one by one.
1093
There is a small search engine to look for keywords in all
1094
contributions. You will also find informations on how to submit a new
1097
The users' contributions may also be obtained by anonymous FTP from site
1098
\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
1099
searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}
1101
% $Id: RefMan-lib.tex 9594 2007-02-05 15:20:08Z herbelin $
1103
%%% Local Variables:
1105
%%% TeX-master: "Reference-Manual"
added
removed
refman/RefMan-lib.tex
