aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-lib.tex
blob: 5a022c74e527825ec07e7e3631533c11466e0430 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
\chapter{The {\Coq} library}
\index{Theories}\label{Theories}

The \Coq\ library is structured into three parts:

\begin{description}
\item[The initial library:] it contains
  elementary logical notions and datatypes. It constitutes the
  basic state of the system directly available when running
  \Coq;

\item[The standard library:] general-purpose libraries containing
  various developments of \Coq\ axiomatizations about sets, lists,
  sorting, arithmetic, etc. This library comes with the system and its
  modules are directly accessible through the \verb!Require! command
  (see section~\ref{Require});

\item[User contributions:] Other specification and proof developments
  coming from the \Coq\ users' community. These libraries are no
  longer distributed with the system.  They are available by anonymous
  FTP (see section~\ref{Contributions}).
\end{description}

This chapter briefly reviews these libraries.

\section{The basic library}
\label{Prelude}

This section lists the basic notions and results which are directly
available in the standard \Coq\ system
\footnote{Most of these constructions are defined in the
{\tt Prelude} module in directory {\tt theories/Init} at the {\Coq}
root directory; this includes the modules
{\tt Notations},
{\tt Logic},
{\tt Datatypes},
{\tt Specif},
{\tt Peano},
and {\tt Wf}.
Module {\tt Logic\_Type} also makes it in the initial state}.

\subsection{Notations} \label{Notations}

This module defines the parsing and pretty-printing of many symbols
(infixes, prefixes, etc.). However, it does not assign a meaning to these
notations. The purpose of this is to define precedence and
associativity of very common notations, and avoid users to use them
with other precedence, which may be confusing.

\begin{figure}
\begin{center}
\begin{tabular}{|cll|}
\hline
Notation & Precedence & Associativity \\
\hline
\verb!_ <-> _! & 95 & no \\
\verb!_ \/ _!  & 85 & right \\
\verb!_ /\ _!  & 80 & right \\
\verb!~ _!   & 75 & right \\
\verb!_ = _!   & 70 & no \\
\verb!_ = _ = _!   & 70 & no \\
\verb!_ = _ :> _!   & 70 & no \\
\verb!_ <> _!  & 70 & no \\
\verb!_ <> _ :> _!  & 70 & no \\
\verb!_ < _!   & 70 & no \\
\verb!_ > _!   & 70 & no \\
\verb!_ <= _!  & 70 & no \\
\verb!_ >= _!  & 70 & no \\
\verb!_ < _ < _! & 70 & no \\
\verb!_ < _ <= _! & 70 & no \\
\verb!_ <= _ < _! & 70 & no \\
\verb!_ <= _ <= _! & 70 & no \\
\verb!_ + _!   & 50 & left \\
\verb!_ - _!   & 50 & left \\
\verb!_ * _!   & 40 & left \\
\verb!_ / _!   & 40 & left \\
\verb!- _!  & 35 & right \\
\verb!/ _!  & 35 & right \\
\verb!_ ^ _!   & 30 & right \\
\hline
\end{tabular}
\end{center}
\caption{Notations in the initial state}
\label{init-notations}
\end{figure}

\subsection{Logic} 
\label{Logic}

\begin{figure}
\begin{centerframe}
\begin{tabular}{lclr}
{\form} & ::= & {\tt True} & ({\tt True})\\
  & $|$ & {\tt False} & ({\tt False})\\
  & $|$ & {\tt\char'176} {\form} & ({\tt not})\\
  & $|$ & {\form} {\tt /$\backslash$} {\form} & ({\tt and})\\
  & $|$ & {\form} {\tt $\backslash$/} {\form} & ({\tt or})\\
  & $|$ & {\form} {\tt ->} {\form} & (\em{primitive implication})\\
  & $|$ & {\form} {\tt <->} {\form} & ({\tt iff})\\
  & $|$ & {\tt forall} {\ident} {\tt :} {\type} {\tt ,}
  {\form} & (\em{primitive for all})\\
  & $|$ & {\tt exists} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  ,} {\form}  & ({\tt ex})\\
  & $|$ & {\tt exists2} {\ident} \zeroone{{\tt :} {\specif}} {\tt
  ,} {\form}  {\tt \&} {\form} & ({\tt ex2})\\
  & $|$ & {\term} {\tt =} {\term} & ({\tt eq})\\
  & $|$ & {\term} {\tt =} {\term} {\tt :>} {\specif} & ({\tt eq})
\end{tabular}
\end{centerframe}
\caption{Syntax of formulas}
\label{formulas-syntax}
\end{figure}

The basic library of {\Coq} comes with the definitions of standard
(intuitionistic) logical connectives (they are defined as inductive
constructions). They are equipped with an appealing syntax enriching the
(subclass {\form}) of the syntactic class {\term}. The syntax
extension is shown on figure \ref{formulas-syntax}.

% The basic library of {\Coq} comes with the definitions of standard
% (intuitionistic) logical connectives (they are defined as inductive
% constructions). They are equipped with an appealing syntax enriching
% the (subclass {\form}) of the syntactic class {\term}. The syntax
% extension \footnote{This syntax is defined in module {\tt
%     LogicSyntax}} is shown on Figure~\ref{formulas-syntax}.
 
\Rem Implication is not defined but primitive (it is a non-dependent
product of a proposition over another proposition).  There is also a
primitive universal quantification (it is a dependent product over a
proposition). The primitive universal quantification allows both
first-order and higher-order quantification.

\subsubsection{Propositional Connectives} \label{Connectives}
\index{Connectives}

First, we find propositional calculus connectives:
\ttindex{True}
\ttindex{I}
\ttindex{False}
\ttindex{not}
\ttindex{and}
\ttindex{conj}
\ttindex{proj1}
\ttindex{proj2}

\begin{coq_eval}
Set Printing Depth 50.
\end{coq_eval}
\begin{coq_example*}
Inductive True : Prop := I.
Inductive False :  Prop := .
Definition not (A: Prop) := A -> False.
Inductive and (A B:Prop) : Prop := conj (_:A) (_:B).
Section Projections.
Variables A B : Prop.
Theorem proj1 : A /\ B -> A.
Theorem proj2 : A /\ B -> B.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\ttindex{or}
\ttindex{or\_introl}
\ttindex{or\_intror}
\ttindex{iff}
\ttindex{IF\_then\_else}
\begin{coq_example*}
End Projections.
Inductive or (A B:Prop) : Prop :=
  | or_introl (_:A)
  | or_intror (_:B).
Definition iff (P Q:Prop) := (P -> Q) /\ (Q -> P).
Definition IF_then_else (P Q R:Prop) := P /\ Q \/ ~ P /\ R.
\end{coq_example*}

\subsubsection{Quantifiers} \label{Quantifiers}
\index{Quantifiers}

Then we find first-order quantifiers:
\ttindex{all}
\ttindex{ex}
\ttindex{exists}
\ttindex{ex\_intro}
\ttindex{ex2}
\ttindex{exists2}
\ttindex{ex\_intro2}

\begin{coq_example*}
Definition all (A:Set) (P:A -> Prop) := forall x:A, P x.
Inductive ex (A: Set) (P:A -> Prop) : Prop :=
    ex_intro (x:A) (_:P x).
Inductive ex2 (A:Set) (P Q:A -> Prop) : Prop :=
    ex_intro2 (x:A) (_:P x) (_:Q x).
\end{coq_example*}

The following abbreviations are allowed:
\begin{center}
  \begin{tabular}[h]{|l|l|}
    \hline
    \verb+exists x:A, P+     & \verb+ex A (fun x:A => P)+ \\
    \verb+exists x, P+       & \verb+ex _ (fun x => P)+ \\
    \verb+exists2 x:A, P & Q+ & \verb+ex2 A (fun x:A => P) (fun x:A => Q)+ \\
    \verb+exists2 x, P & Q+   & \verb+ex2 _ (fun x => P) (fun x => Q)+ \\
    \hline
  \end{tabular}
\end{center}

The type annotation \texttt{:A} can be omitted when \texttt{A} can be
synthesized by the system.

\subsubsection{Equality} \label{Equality}
\index{Equality}

Then, we find equality, defined as an inductive relation. That is,
given a \verb:Type: \verb:A: and an \verb:x: of type \verb:A:, the
predicate \verb:(eq A x): is the smallest one which contains \verb:x:.
This definition, due to Christine Paulin-Mohring, is equivalent to
define \verb:eq: as the smallest reflexive relation, and it is also
equivalent to Leibniz' equality.

\ttindex{eq}
\ttindex{refl\_equal}

\begin{coq_example*}
Inductive eq (A:Type) (x:A) : A -> Prop :=
    refl_equal : eq A x x.
\end{coq_example*}

\subsubsection{Lemmas} 
\label{PreludeLemmas}

Finally, a few easy lemmas are provided.

\ttindex{absurd}

\begin{coq_example*}
Theorem absurd : forall A C:Prop, A -> ~ A -> C.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}
\ttindex{sym\_eq}
\ttindex{trans\_eq}
\ttindex{f\_equal}
\ttindex{sym\_not\_eq}
\begin{coq_example*}
Section equality.
Variables A B : Type.
Variable f : A -> B.
Variables x y z : A.
Theorem sym_eq : x = y -> y = x.
Theorem trans_eq : x = y -> y = z -> x = z.
Theorem f_equal : x = y -> f x = f y.
Theorem sym_not_eq : x <> y -> y <> x.
\end{coq_example*}
\begin{coq_eval}
Abort.
Abort.
Abort.
Abort.
\end{coq_eval}
\ttindex{eq\_ind\_r}
\ttindex{eq\_rec\_r}
\ttindex{eq\_rect}
\ttindex{eq\_rect\_r}
%Definition eq_rect: (A:Set)(x:A)(P:A->Type)(P x)->(y:A)(x=y)->(P y).
\begin{coq_example*}
End equality.
Definition eq_ind_r :
  forall (A:Type) (x:A) (P:A -> Prop), P x -> forall y:A, y = x -> P y.
Definition eq_rec_r :
  forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
Definition eq_rect_r :
  forall (A:Type) (x:A) (P:A -> Type), P x -> forall y:A, y = x -> P y.
\end{coq_example*}
\begin{coq_eval}
Abort.
Abort.
Abort.
\end{coq_eval}
%Abort (for now predefined eq_rect)
\begin{coq_example*}
Hint Immediate sym_eq sym_not_eq : core.
\end{coq_example*}
\ttindex{f\_equal$i$}

The theorem {\tt f\_equal} is extended to functions with two to five
arguments. The theorem are names {\tt f\_equal2}, {\tt f\_equal3}, 
{\tt f\_equal4} and {\tt f\_equal5}.
For instance {\tt f\_equal3} is defined the following way.
\begin{coq_example*}
Theorem f_equal3 :
 forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1) (x2 y2:A2)
   (x3 y3:A3), x1 = y1 -> x2 = y2 -> x3 = y3 -> f x1 x2 x3 = f y1 y2 y3.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

\subsection{Datatypes}
\label{Datatypes}
\index{Datatypes}

\begin{figure}
\begin{centerframe}
\begin{tabular}{rclr}
{\specif} & ::= & {\specif} {\tt *} {\specif} & ({\tt prod})\\
  & $|$ & {\specif} {\tt +} {\specif} & ({\tt sum})\\
  & $|$ & {\specif} {\tt + \{} {\specif} {\tt \}} & ({\tt sumor})\\
  & $|$ & {\tt \{} {\specif} {\tt \} + \{} {\specif} {\tt \}} &
  ({\tt sumbool})\\  
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form} {\tt \}}
  & ({\tt sig})\\
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt |} {\form}  {\tt \&}
  {\form} {\tt \}} & ({\tt sig2})\\
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
    \}} & ({\tt sigS})\\
  & $|$ & {\tt \{} {\ident} {\tt :} {\specif} {\tt \&} {\specif} {\tt
    \&} {\specif} {\tt \}} & ({\tt sigS2})\\
  &  & & \\
{\term} & ::= & {\tt (} {\term} {\tt ,} {\term} {\tt )} & ({\tt pair})
\end{tabular}
\end{centerframe}
\caption{Syntax of datatypes and specifications}
\label{specif-syntax}
\end{figure}


In the basic library, we find the definition\footnote{They are in {\tt
    Datatypes.v}} of the basic data-types of programming, again
defined as inductive constructions over the sort \verb:Set:. Some of
them come with a special syntax shown on Figure~\ref{specif-syntax}.

\subsubsection{Programming} 
\label{Programming}
\index{Programming}
\label{libnats}

\ttindex{unit}
\ttindex{tt}
\ttindex{bool}
\ttindex{true}
\ttindex{false}
\ttindex{nat}
\ttindex{O}
\ttindex{S}
\ttindex{option}
\ttindex{Some}
\ttindex{None}
\ttindex{identity}
\ttindex{refl\_identity}

\begin{coq_example*}
Inductive unit : Set := tt.
Inductive bool : Set := true | false.
Inductive nat : Set := O | S (n:nat).
Inductive option (A:Set) : Set := Some (_:A) | None.
Inductive identity (A:Type) (a:A) : A -> Type :=
    refl_identity : identity A a a.
\end{coq_example*}

Note that zero is the letter \verb:O:, and {\sl not} the numeral
\verb:0:.

{\tt identity} is logically equivalent to equality but it lives in
sort {\tt Set}. Computationaly, it behaves like {\tt unit}.

We then define the disjoint sum of \verb:A+B: of two sets \verb:A: and
\verb:B:, and their product \verb:A*B:.
\ttindex{sum}
\ttindex{A+B}
\ttindex{+}
\ttindex{inl}
\ttindex{inr}
\ttindex{prod}
\ttindex{A*B}
\ttindex{*}
\ttindex{pair}
\ttindex{fst}
\ttindex{snd}

\begin{coq_example*}
Inductive sum (A B:Set) : Set := inl (_:A) | inr (_:B).
Inductive prod (A B:Set) : Set := pair (_:A) (_:B).
Section projections.
Variables A B : Set.
Definition fst (H: prod A B) := match H with
                                | pair x y => x
                                end.
Definition snd (H: prod A B) := match H with
                                | pair x y => y
                                end.
End projections.
\end{coq_example*}

\subsection{Specification}

The following notions\footnote{They are defined in module {\tt
Specif.v}} allows to build new datatypes and specifications. 
They are available with the syntax shown on
Figure~\ref{specif-syntax}\footnote{This syntax can be found in the module
{\tt SpecifSyntax.v}}.

For instance, given \verb|A:Set| and \verb|P:A->Prop|, the construct
\verb+{x:A | P x}+ (in abstract syntax \verb+(sig A P)+) is a
\verb:Set:. We may build elements of this set as \verb:(exist x p):
whenever we have a witness \verb|x:A| with its justification
\verb|p:P x|.

From such a \verb:(exist x p): we may in turn extract its witness
\verb|x:A| (using an elimination construct such as \verb:match:) but
{\sl not} its justification, which stays hidden, like in an abstract
data type. In technical terms, one says that \verb:sig: is a ``weak
(dependent) sum''.  A variant \verb:sig2: with two predicates is also
provided.

\index{\{x:A "| (P x)\}}
\index{"|}
\ttindex{sig}
\ttindex{exist}
\ttindex{sig2}
\ttindex{exist2}

\begin{coq_example*}
Inductive sig (A:Set) (P:A -> Prop) : Set := exist (x:A) (_:P x).
Inductive sig2 (A:Set) (P Q:A -> Prop) : Set := 
  exist2 (x:A) (_:P x) (_:Q x).
\end{coq_example*}

A ``strong (dependent) sum'' \verb+{x:A & (P x)}+ may be also defined,
when the predicate \verb:P: is now defined as a \verb:Set:
constructor.

\ttindex{\{x:A \& (P x)\}}
\ttindex{\&}
\ttindex{sigS}
\ttindex{existS}
\ttindex{projS1}
\ttindex{projS2}
\ttindex{sigS2}
\ttindex{existS2}

\begin{coq_example*}
Inductive sigS (A:Set) (P:A -> Set) : Set := existS (x:A) (_:P x).
Section sigSprojections.
Variable A : Set.
Variable P : A -> Set.
Definition projS1 (H:sigS A P) := let (x, h) := H in x.
Definition projS2 (H:sigS A P) :=
  match H return P (projS1 H) with
    existS x h => h
  end.
End sigSprojections.
Inductive sigS2 (A: Set) (P Q:A -> Set) : Set :=
    existS2 (x:A) (_:P x) (_:Q x).
\end{coq_example*}

A related non-dependent construct is the constructive sum
\verb"{A}+{B}" of two propositions \verb:A: and \verb:B:.
\label{sumbool}
\ttindex{sumbool}
\ttindex{left}
\ttindex{right}
\ttindex{\{A\}+\{B\}}

\begin{coq_example*}
Inductive sumbool (A B:Prop) : Set := left (_:A) | right (_:B).
\end{coq_example*}

This \verb"sumbool" construct may be used as a kind of indexed boolean
data type. An intermediate between \verb"sumbool" and \verb"sum" is
the mixed \verb"sumor" which combines \verb"A:Set" and \verb"B:Prop"
in the \verb"Set" \verb"A+{B}".
\ttindex{sumor}
\ttindex{inleft}
\ttindex{inright}
\ttindex{A+\{B\}}

\begin{coq_example*}
Inductive sumor (A:Set) (B:Prop) : Set := inleft (_:A) | inright (_:B).
\end{coq_example*}

We may define variants of the axiom of choice, like in Martin-Löf's
Intuitionistic Type Theory.
\ttindex{Choice}
\ttindex{Choice2}
\ttindex{bool\_choice}

\begin{coq_example*}
Lemma Choice :
 forall (S S':Set) (R:S -> S' -> Prop),
   (forall x:S, {y : S' | R x y}) ->
   {f : S -> S' | forall z:S, R z (f z)}.
Lemma Choice2 :
 forall (S S':Set) (R:S -> S' -> Set),
   (forall x:S, {y : S' &  R x y}) ->
   {f : S -> S' &  forall z:S, R z (f z)}.
Lemma bool_choice :
 forall (S:Set) (R1 R2:S -> Prop),
   (forall x:S, {R1 x} + {R2 x}) ->
   {f : S -> bool |
   forall x:S, f x = true /\ R1 x \/ f x = false /\ R2 x}.
\end{coq_example*}
\begin{coq_eval}
Abort.
Abort.
Abort.
\end{coq_eval}

The next constructs builds a sum between a data type \verb|A:Set| and
an exceptional value encoding errors:

\ttindex{Exc}
\ttindex{value}
\ttindex{error}

\begin{coq_example*}
Definition Exc := option.
Definition value := Some.
Definition error := None.
\end{coq_example*}


This module ends with theorems, 
relating the sorts \verb:Set: and
\verb:Prop: in a way which is consistent with the realizability
interpretation.
\ttindex{False\_rec}
\ttindex{eq\_rec}
\ttindex{Except}
\ttindex{absurd\_set}
\ttindex{and\_rec}

%Lemma False_rec : (P:Set)False->P.
%Lemma False_rect : (P:Type)False->P.
\begin{coq_example*}
Definition except := False_rec.
Notation Except := (except _).
Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
Theorem and_rec :
 forall (A B:Prop) (P:Set), (A -> B -> P) -> A /\ B -> P.
\end{coq_example*}
%\begin{coq_eval}
%Abort.
%Abort.
%\end{coq_eval}

\subsection{Basic Arithmetics}

The basic library includes a few elementary properties of natural
numbers, together with the definitions of predecessor, addition and
multiplication\footnote{This is in module {\tt Peano.v}}. It also
provides a scope {\tt nat\_scope} gathering standard notations for
common operations (+,*) and a decimal notation for numbers. That is he
can write \texttt{3} for \texttt{(S (S (S O)))}. This also works on
the left hand side of a \texttt{match} expression (see for example
section~\ref{refine-example}). This scope is opened by default.

%Remove the redefinition of nat
\begin{coq_eval}
Reset Initial.
\end{coq_eval}

The following example is not part of the standard library, but it
shows the usage of the notations:

\begin{coq_example*}
Fixpoint even (n:nat) : bool :=
  match n with
  | 0 => true
  | 1 => false
  | S (S n) => even n
  end.
\end{coq_example*}


\ttindex{eq\_S}
\ttindex{pred}
\ttindex{pred\_Sn}
\ttindex{eq\_add\_S}
\ttindex{not\_eq\_S}
\ttindex{IsSucc}
\ttindex{O\_S}
\ttindex{n\_Sn}
\ttindex{plus}
\ttindex{plus\_n\_O}
\ttindex{plus\_n\_Sm}
\ttindex{mult}
\ttindex{mult\_n\_O}
\ttindex{mult\_n\_Sm}

\begin{coq_example*}
Theorem eq_S : forall x y:nat, x = y -> S x = S y.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}
\begin{coq_example*}
Definition pred (n:nat) : nat :=
  match n with
  | 0 => 0
  | S u => u
  end.
Theorem pred_Sn : forall m:nat, m = pred (S m).
Theorem eq_add_S : forall n m:nat, S n = S m -> n = m.
Hint Immediate eq_add_S : core.
Theorem not_eq_S : forall n m:nat, n <> m -> S n <> S m.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
Definition IsSucc (n:nat) : Prop :=
  match n with
  | 0 => False
  | S p => True
  end.
Theorem O_S : forall n:nat, 0 <> S n.
Theorem n_Sn : forall n:nat, n <> S n.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
Fixpoint plus (n m:nat) {struct n} : nat :=
  match n with
  | 0 => m
  | S p => S (plus p m)
  end.
Lemma plus_n_O : forall n:nat, n = plus n 0.
Lemma plus_n_Sm : forall n m:nat, S (plus n m) = plus n (S m).
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
Fixpoint mult (n m:nat) {struct n} : nat :=
  match n with
  | 0 => 0
  | S p => m + mult p m
  end.
Lemma mult_n_O : forall n:nat, 0 = mult n 0.
Lemma mult_n_Sm : forall n m:nat, plus (mult n m) n = mult n (S m).
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}

Finally, it gives the definition of the usual orderings \verb:le:,
\verb:lt:, \verb:ge:, and \verb:gt:.
\ttindex{le}
\ttindex{le\_n}
\ttindex{le\_S}
\ttindex{lt}
\ttindex{ge}
\ttindex{gt}

\begin{coq_example*}
Inductive le (n:nat) : nat -> Prop :=
  | le_n : le n n
  | le_S : forall m:nat, le n m -> le n (S m).
Infix "+" := plus : nat_scope.
Definition lt (n m:nat) := S n <= m.
Definition ge (n m:nat) := m <= n.
Definition gt (n m:nat) := m < n.
\end{coq_example*}

Properties of these relations are not initially known, but may be
required by the user from modules \verb:Le: and \verb:Lt:.  Finally,
\verb:Peano: gives some lemmas allowing pattern-matching, and a double
induction principle.

\ttindex{nat\_case}
\ttindex{nat\_double\_ind}

\begin{coq_example*}
Theorem nat_case :
 forall (n:nat) (P:nat -> Prop), P 0 -> (forall m:nat, P (S m)) -> P n.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
Theorem nat_double_ind :
 forall R:nat -> nat -> Prop,
   (forall n:nat, R 0 n) ->
   (forall n:nat, R (S n) 0) ->
   (forall n m:nat, R n m -> R (S n) (S m)) -> forall n m:nat, R n m.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}

\subsection{Well-founded recursion}

The basic library contains the basics of well-founded recursion and 
well-founded induction\footnote{This is defined in module {\tt Wf.v}}.
\index{Well foundedness}
\index{Recursion}
\index{Well founded induction}
\ttindex{Acc}
\ttindex{Acc\_inv}
\ttindex{Acc\_rec}
\ttindex{well\_founded}

\begin{coq_example*}
Section Well_founded.
Variable A : Set.
Variable R : A -> A -> Prop.
Inductive Acc : A -> Prop :=
    Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
\end{coq_example*}
\begin{coq_eval}
simple destruct 1; trivial.
Defined.
\end{coq_eval}
\begin{coq_example*}
Section AccRec.
Variable P : A -> Set.
Variable F :
    forall x:A,
      (forall y:A, R y x -> Acc y) -> (forall y:A, R y x -> P y) -> P x.
Fixpoint Acc_rec (x:A) (a:Acc x) {struct a} : P x :=
  F x (Acc_inv x a)
    (fun (y:A) (h:R y x) => Acc_rec y (Acc_inv x a y h)).
End AccRec.
Definition well_founded := forall a:A, Acc a.
Hypothesis Rwf : well_founded.
Theorem well_founded_induction :
 forall P:A -> Set,
   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
Theorem well_founded_ind :
 forall P:A -> Prop,
   (forall x:A, (forall y:A, R y x -> P y) -> P x) -> forall a:A, P a.
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
{\tt Acc\_rec} can be used to define functions by fixpoints using
well-founded relations to  justify termination. Assuming
extensionality of the functional used for the recursive call, the
fixpoint equation can be proved.
\ttindex{Fix\_F}
\ttindex{fix\_eq}
\ttindex{Fix\_F\_inv}
\ttindex{Fix\_F\_eq}
\begin{coq_example*}
Section FixPoint.
Variable P : A -> Set.
Variable F : forall x:A, (forall y:A, R y x -> P y) -> P x.
Fixpoint Fix_F (x:A) (r:Acc x) {struct r} : P x :=
  F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)).
Definition Fix (x:A) := Fix_F x (Rwf x).
Hypothesis F_ext :
    forall (x:A) (f g:forall y:A, R y x -> P y),
      (forall (y:A) (p:R y x), f y p = g y p) -> F x f = F x g.
Lemma Fix_F_eq :
 forall (x:A) (r:Acc x),
   F x (fun (y:A) (p:R y x) => Fix_F y (Acc_inv x r y p)) = Fix_F x r.
Lemma Fix_F_inv : forall (x:A) (r s:Acc x), Fix_F x r = Fix_F x s.
Lemma fix_eq : forall x:A, Fix x = F x (fun (y:A) (p:R y x) => Fix y).
\end{coq_example*}
\begin{coq_eval}
Abort All.
\end{coq_eval}
\begin{coq_example*}
End FixPoint.
End Well_founded.
\end{coq_example*}

\subsection{Accessing the {\Type} level}

The basic library includes the definitions\footnote{This is in module
{\tt Logic\_Type.v}} of the counterparts of some datatypes and logical
quantifiers at the \verb:Type: level: negation, pair, and properties
of {\tt identity}.

\ttindex{notT}
\ttindex{prodT}
\ttindex{pairT}
\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example*}
Definition notT (A:Type) := A -> False.
Inductive prodT (A B:Type) : Type := pairT (_:A) (_:B).
\end{coq_example*}


At the end, it defines datatypes at the {\Type} level.

\section{The standard library}

\subsection{Survey}

The rest of the standard library is structured into the following 
subdirectories:

\begin{tabular}{lp{12cm}}
  {\bf Logic}   & Classical logic and dependent equality \\
  {\bf Arith}   & Basic Peano arithmetic \\
  {\bf ZArith}  & Basic integer arithmetic \\
  {\bf Bool}    &  Booleans (basic functions and results) \\
  {\bf Lists}   & Monomorphic and polymorphic lists (basic functions and
            results), Streams (infinite sequences defined with co-inductive
            types) \\
  {\bf Sets}    & Sets (classical, constructive, finite, infinite, power set,
            etc.) \\
  {\bf IntMap}    & Representation of finite sets by an efficient
  structure of map (trees indexed by binary integers).\\
 {\bf Reals}   & Axiomatization of Real Numbers (classical, basic functions, 
                 integer part, fractional part, limit, derivative, Cauchy 
                 series, power series and results,... Requires the 
                 \textbf{ZArith} library).\\
 {\bf Relations} & Relations (definitions and basic results). \\
 {\bf Sorting} & Sorted list (basic definitions and heapsort correctness). \\
 {\bf Wellfounded} & Well-founded relations (basic results). \\

\end{tabular}
\medskip

These directories belong to the initial load path of the system, and
the modules they provide are compiled at installation time. So they
are directly accessible with the command \verb!Require! (see
chapter~\ref{Other-commands}). 

The different modules of the \Coq\ standard library are described in the
additional document \verb!Library.dvi!. They are also accessible on the WWW
through the \Coq\ homepage
\footnote{\texttt{http://coq.inria.fr}}.

\subsection{Notations for integer arithmetics}
\index{Arithmetical notations}

On figure \ref{zarith-syntax} is described the syntax of expressions
for integer arithmetics. It is provided by requiring and opening the
module {\tt ZArith} and opening scope {\tt Z\_scope}.

\ttindex{+}
\ttindex{*}
\ttindex{-}
\ttindex{/}
\ttindex{<=}
\ttindex{>=}
\ttindex{<}
\ttindex{>}
\ttindex{?=}
\ttindex{mod}

\begin{figure}
\begin{center}
\begin{tabular}{l|l|l|l}
Notation & Interpretation & Precedence & Associativity\\
\hline
\verb!_ < _! & {\tt Zlt} &&\\
\verb!x <= y! & {\tt Zle} &&\\
\verb!_ > _! & {\tt Zgt} &&\\
\verb!x >= y! & {\tt Zge} &&\\
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} &&\\
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} &&\\
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} &&\\
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} &&\\
\verb!_ ?= _! & {\tt Zcompare} & 70 & no\\
\verb!_ + _! & {\tt Zplus} &&\\
\verb!_ - _! & {\tt Zminus} &&\\
\verb!_ * _! & {\tt Zmult} &&\\
\verb!_ / _! & {\tt Zdiv} &&\\
\verb!_ mod _! & {\tt Zmod} & 40 & no \\
\verb!- _!  & {\tt Zopp} &&\\
\verb!_ ^ _! & {\tt Zpower} &&\\
\end{tabular}
\end{center}
\label{zarith-syntax}
\caption{Definition of the scope for integer arithmetics ({\tt Z\_scope})}
\end{figure}

Figure~\ref{zarith-syntax} shows the notations provided by {\tt
Z\_scope}. It specifies how notations are interpreted and, when not
already reserved, the precedence and associativity.

\begin{coq_example}
Require Import ZArith.
Check  (2 + 3)%Z.
Open Scope Z_scope.
Check 2 + 3.
\end{coq_example}

\subsection{Peano's arithmetic (\texttt{nat})}
\index{Peano's arithmetic}
\ttindex{nat\_scope}

While in the initial state, many operations and predicates of Peano's
arithmetic are defined, further operations and results belong to other
modules. For instance, the decidability of the basic predicates are
defined here. This is provided by requiring the module {\tt Arith}.

Figure~\ref{nat-syntax} describes notation available in scope {\tt
nat\_scope}.

\begin{figure}
\begin{center}
\begin{tabular}{l|l}
Notation & Interpretation \\
\hline
\verb!_ < _! & {\tt lt} \\
\verb!x <= y! & {\tt le} \\
\verb!_ > _! & {\tt gt} \\
\verb!x >= y! & {\tt ge} \\
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
\verb!_ + _! & {\tt plus} \\
\verb!_ - _! & {\tt minus} \\
\verb!_ * _! & {\tt mult} \\
\end{tabular}
\end{center}
\label{nat-syntax}
\caption{Definition of the scope for natural numbers ({\tt nat\_scope})}
\end{figure}

\subsection{Real numbers library}

\subsubsection{Notations for real numbers}
\index{Notations for real numbers}

This is provided by requiring and opening the module {\tt Reals} and
opening scope {\tt R\_scope}. This set of notations is very similar to
the notation for integer arithmetics. The inverse function was added.
\begin{figure}
\begin{center}
\begin{tabular}{l|l}
Notation & Interpretation \\
\hline
\verb!_ < _! & {\tt Rlt} \\
\verb!x <= y! & {\tt Rle} \\
\verb!_ > _! & {\tt Rgt} \\
\verb!x >= y! & {\tt Rge} \\
\verb!x < y < z! & {\tt x < y \verb!/\! y < z} \\
\verb!x < y <= z! & {\tt x < y \verb!/\! y <= z} \\
\verb!x <= y < z! & {\tt x <= y \verb!/\! y < z} \\
\verb!x <= y <= z! & {\tt x <= y \verb!/\! y <= z} \\
\verb!_ + _! & {\tt Rplus} \\
\verb!_ - _! & {\tt Rminus} \\
\verb!_ * _! & {\tt Rmult} \\
\verb!_ / _! & {\tt Rdiv} \\
\verb!- _!  & {\tt Ropp} \\
\verb!/ _!  & {\tt Rinv} \\
\verb!_ ^ _! & {\tt pow} \\
\end{tabular}
\end{center}
\label{reals-syntax}
\caption{Definition of the scope for real arithmetics ({\tt R\_scope})}
\end{figure}

\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_example}
Require Import Reals.
Check  (2 + 3)%R.
Open Scope R_scope.
Check 2 + 3.
\end{coq_example}

\subsubsection{Some tactics}

In addition to the \verb|ring|, \verb|field| and \verb|fourier|
tactics (see Chapter~\ref{Tactics}) there are:
\begin{itemize}
\item {\tt discrR} \tacindex{discrR}
  
  Proves that a real integer constant $c_1$ is different from another
  real integer constant $c_2$.  

\begin{coq_example*}
Require Import DiscrR.
Goal 5 <> 0.
\end{coq_example*}

\begin{coq_example}
discrR.
\end{coq_example}

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

\item {\tt split\_Rabs} allows to unfold {\tt Rabs} constant and splits 
corresponding conjonctions.
\tacindex{split\_Rabs}

\begin{coq_example*}
Require Import SplitAbsolu.
Goal forall x:R, x <= Rabs x.
\end{coq_example*}

\begin{coq_example}
intro; split_Rabs.
\end{coq_example}

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

\item {\tt split\_Rmult} allows to split a condition that a product is
  non null into subgoals corresponding to the condition on each
  operand of the product. 
\tacindex{split\_Rmult}

\begin{coq_example*}
Require Import SplitRmult.
Goal forall x y z:R, x * y * z <> 0.
\end{coq_example*}

\begin{coq_example}
intros; split_Rmult.
\end{coq_example}

\end{itemize}

All this tactics has been written with the tactic language Ltac
described in Chapter~\ref{TacticLanguage}.  More details are available
in document \url{http://coq.inria.fr/~desmettr/Reals.ps}.

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

\subsection{List library}
\index{Notations for lists}
\ttindex{length}
\ttindex{head}
\ttindex{tail}
\ttindex{app}
\ttindex{rev}
\ttindex{nth}
\ttindex{map}
\ttindex{flat\_map}
\ttindex{fold\_left}
\ttindex{fold\_right}

Some elementary operations on polymorphic lists are defined here. They
can be accessed by requiring module {\tt List}.

It defines the following notions:
\begin{center}
\begin{tabular}{l|l}
\hline
{\tt length} & length \\
{\tt head} & first element (with default) \\
{\tt tail} & all but first element \\
{\tt app} & concatenation \\
{\tt rev} & reverse \\
{\tt nth} & accessing $n$-th element (with default) \\
{\tt map} & applying a function \\
{\tt flat\_map} & applying a function returning lists \\
{\tt fold\_left} & iterator (from head to tail) \\
{\tt fold\_right} & iterator (from tail to head) \\
\hline
\end{tabular}
\end{center}

Table show notations available when opening scope {\tt list\_scope}.

\begin{figure}
\begin{center}
\begin{tabular}{l|l|l|l}
Notation & Interpretation & Precedence & Associativity\\
\hline
\verb!_ ++ _! & {\tt app} & 60 & right \\
\verb!_ :: _! & {\tt cons} & 60 & right \\
\end{tabular}
\end{center}
\label{list-syntax}
\caption{Definition of the scope for lists ({\tt list\_scope})}
\end{figure}


\section{Users' contributions}
\index{Contributions}
\label{Contributions}

Numerous users' contributions have been collected and are available at
URL \url{coq.inria.fr/contribs/}.  On this web page, you have a list
of all contributions with informations (author, institution, quick
description, etc.) and the possibility to download them one by one.
There is a small search engine to look for keywords in all
contributions.  You will also find informations on how to submit a new
contribution.

The users' contributions may also be obtained by anonymous FTP from site
\verb:ftp.inria.fr:, in directory \verb:INRIA/coq/: and
searchable on-line at \url{http://coq.inria.fr/contribs-eng.html}

% $Id$ 

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End: