aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/tutorial/Tutorial.tex
blob: 219706e35d54a4ca605ec41d815e5a0ef3b267ac (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
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
1464
1465
1466
1467
1468
1469
1470
1471
1472
1473
1474
1475
1476
1477
1478
1479
1480
1481
1482
1483
1484
1485
1486
1487
1488
1489
1490
1491
1492
1493
1494
1495
1496
1497
1498
1499
1500
1501
1502
1503
1504
1505
1506
1507
1508
1509
1510
1511
1512
1513
1514
1515
1516
1517
1518
1519
1520
1521
1522
1523
1524
1525
1526
1527
1528
1529
1530
1531
1532
1533
1534
1535
1536
1537
1538
1539
1540
1541
1542
1543
1544
1545
1546
1547
1548
1549
1550
1551
1552
1553
1554
1555
1556
1557
1558
1559
1560
1561
1562
1563
1564
1565
1566
1567
1568
1569
1570
1571
1572
1573
1574
1575
1576
1577
\documentclass[11pt,a4paper]{book}
\usepackage[T1]{fontenc}
\usepackage[latin1]{inputenc}
\usepackage{pslatex}

\input{../common/version.tex}
\input{../common/macros.tex}
\input{../common/title.tex}

%\makeindex

\begin{document}
\coverpage{A Tutorial}{Gérard Huet, Gilles Kahn and Christine Paulin-Mohring}{}

%\tableofcontents

\chapter*{Getting started}

\Coq\ is a Proof Assistant for a Logical Framework known as the Calculus
of Inductive Constructions. It allows the interactive construction of
formal proofs, and also the manipulation of functional programs 
consistently with their specifications. It runs as a computer program
on many architectures.
%, and mainly on Unix machines. 
It is available with a variety of user interfaces. The present
document does not attempt to present a comprehensive view of all the
possibilities of \Coq, but rather to present in the most elementary
manner a tutorial on the basic specification language, called Gallina,
in which formal axiomatisations may be developed, and on the main
proof tools.  For more advanced information, the reader could refer to
the \Coq{} Reference Manual or the \textit{Coq'Art}, a new book by Y.
Bertot and P. Castéran on practical uses of the \Coq{} system.

Coq can be used from a standard teletype-like shell window but
preferably through the graphical user interface
CoqIde\footnote{Alternative graphical interfaces exist: Proof General
and Pcoq.}.

Instructions on installation procedures, as well as more comprehensive
documentation, may be found in the standard distribution of \Coq,
which may be obtained from \Coq{} web site \texttt{http://coq.inria.fr}.

In the following, we assume that \Coq~ is called from a standard
teletype-like shell window. All examples preceded by the prompting
sequence \verb:Coq < : represent user input, terminated by a
period. 

The following lines usually show \Coq's answer as it appears on the
users screen. When used from a graphical user interface such as
CoqIde, the prompt is not displayed: user input is given in one window
and \Coq's answers are displayed in a different window.

The sequence of such examples is a valid \Coq~
session, unless otherwise specified. This version of the tutorial has
been prepared on a PC workstation running Linux.  The standard
invocation of \Coq\ delivers a message such as:

\begin{small}
\begin{flushleft}
\begin{verbatim}
unix:~> coqtop
Welcome to Coq 8.2 (January 2009)

Coq < 
\end{verbatim}
\end{flushleft}
\end{small}

The first line gives a banner stating the precise version of \Coq~
used. You should always return this banner when you report an anomaly
to our bug-tracking system
\verb|http://logical.futurs.inria.fr/coq-bugs|

\chapter{Basic Predicate Calculus}

\section{An overview of the specification language Gallina}

A formal development in Gallina consists in a sequence of {\sl declarations}
and {\sl definitions}. You may also send \Coq~ {\sl commands} which are
not really part of the formal development, but correspond to information
requests, or service routine invocations. For instance, the command:
\begin{verbatim}
Coq < Quit.
\end{verbatim}
terminates the current session.

\subsection{Declarations}

A declaration associates a {\sl name} with 
a {\sl specification}. 
A name corresponds roughly to an identifier in a programming
language, i.e. to a string of letters, digits, and a few ASCII symbols like
underscore (\verb"_") and prime (\verb"'"), starting with a letter. 
We use case distinction, so that the names \verb"A" and \verb"a" are distinct.
Certain strings are reserved as key-words of \Coq, and thus are forbidden 
as user identifiers.

A specification is a formal expression which classifies the notion which is
being declared. There are basically three kinds of specifications: 
{\sl logical propositions}, {\sl mathematical collections}, and
{\sl abstract types}. They are classified by the three basic sorts
of the system, called respectively \verb:Prop:, \verb:Set:, and
\verb:Type:, which are themselves atomic abstract types.

Every valid expression $e$ in Gallina is associated with a specification,
itself a valid expression, called its {\sl type} $\tau(E)$. We write
$e:\tau(E)$ for the judgment that $e$ is of type $E$. 
You may request \Coq~ to return to you the type of a valid expression by using
the command \verb:Check::

\begin{coq_eval}
Set Printing Width 60.
\end{coq_eval}

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

Thus we know that the identifier \verb:O: (the name `O', not to be
confused with the numeral `0' which is not a proper identifier!) is
known in the current context, and that its type is the specification 
\verb:nat:. This specification is itself classified as a mathematical
collection, as we may readily check:

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

The specification \verb:Set: is an abstract type, one of the basic
sorts of the Gallina language, whereas the notions $nat$ and $O$ are
notions which are defined in the arithmetic prelude,
automatically loaded when running the \Coq\ system.

We start by introducing a so-called section name. The role of sections
is to structure the modelisation by limiting the scope of parameters,
hypotheses and definitions. It will also give a convenient way to
reset part of the development.

\begin{coq_example}
Section Declaration.
\end{coq_example}
With what we already know, we may now enter in the system a declaration,
corresponding to the informal mathematics {\sl let n be a natural
  number}. 

\begin{coq_example}
Variable n : nat.
\end{coq_example}

If we want to translate a more precise statement, such as
{\sl let n be a positive natural number},
we have to add another declaration, which will declare explicitly the
hypothesis \verb:Pos_n:, with specification the proper logical
proposition:
\begin{coq_example}
Hypothesis Pos_n : (gt n 0).
\end{coq_example}

Indeed we may check that the relation \verb:gt: is known with the right type
in the current context:

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

which tells us that \verb:gt: is a function expecting two arguments of
type \verb:nat: in order to build a logical proposition.
What happens here is similar to what we are used to in a functional
programming language: we may compose the (specification) type \verb:nat:
with the (abstract) type \verb:Prop: of logical propositions through the
arrow function constructor, in order to get a functional type
\verb:nat->Prop::
\begin{coq_example}
Check (nat -> Prop).
\end{coq_example}
which may be composed one more times with \verb:nat: in order to obtain the
type \verb:nat->nat->Prop: of binary relations over natural numbers.
Actually the type \verb:nat->nat->Prop: is an abbreviation for 
\verb:nat->(nat->Prop):. 

Functional notions may be composed in the usual way. An expression $f$
of type $A\ra B$ may be applied to an expression $e$ of type $A$ in order
to form the expression $(f~e)$ of type $B$. Here we get that
the expression \verb:(gt n): is well-formed of type \verb:nat->Prop:,
and thus that the expression \verb:(gt n O):, which abbreviates
\verb:((gt n) O):, is a well-formed proposition.
\begin{coq_example}
Check gt n O.
\end{coq_example}

\subsection{Definitions}

The initial prelude contains a few arithmetic definitions:
\verb:nat: is defined as a mathematical collection (type \verb:Set:), constants
\verb:O:, \verb:S:, \verb:plus:, are defined as objects of types
respectively \verb:nat:, \verb:nat->nat:, and \verb:nat->nat->nat:.
You may introduce new definitions, which link a name to a well-typed value.
For instance, we may introduce the constant \verb:one: as being defined
to be equal to the successor of zero:
\begin{coq_example}
Definition one := (S O).
\end{coq_example}
We may optionally indicate the required type:
\begin{coq_example}
Definition two : nat := S one.
\end{coq_example}

Actually \Coq~ allows several possible syntaxes:
\begin{coq_example}
Definition three : nat := S two.
\end{coq_example}

Here is a way to define the doubling function, which expects an
argument \verb:m: of type \verb:nat: in order to build its result as
\verb:(plus m m)::

\begin{coq_example}
Definition double (m:nat) := plus m m.
\end{coq_example}
This introduces the constant \texttt{double} defined as the
expression \texttt{fun m:nat => plus m m}.
The abstraction introduced by \texttt{fun} is explained as follows. The expression
\verb+fun x:A => e+ is well formed of type \verb+A->B+ in a context
whenever the expression \verb+e+ is well-formed of type \verb+B+ in 
the given context to which we add the declaration that \verb+x+
is of type \verb+A+. Here \verb+x+ is a bound, or dummy variable in
the expression \verb+fun x:A => e+. For instance we could as well have
defined \verb:double: as \verb+fun n:nat => (plus n n)+.

Bound (local) variables and free (global) variables may be mixed.
For instance, we may define the function which adds the constant \verb:n:
to its argument as
\begin{coq_example}
Definition add_n (m:nat) := plus m n.
\end{coq_example}
However, note that here we may not rename the formal argument $m$ into $n$
without capturing the free occurrence of $n$, and thus changing the meaning
of the defined notion.

Binding operations are well known for instance in logic, where they
are called quantifiers.  Thus we may universally quantify a
proposition such as $m>0$ in order to get a universal proposition
$\forall m\cdot m>0$. Indeed this operator is available in \Coq, with
the following syntax: \verb+forall m:nat, gt m O+. Similarly to the
case of the functional abstraction binding, we are obliged to declare
explicitly the type of the quantified variable. We check:
\begin{coq_example}
Check (forall m:nat, gt m 0).
\end{coq_example}
We may clean-up the development by removing the contents of the
current section:
\begin{coq_example}
Reset Declaration.
\end{coq_example}

\section{Introduction to the proof engine: Minimal Logic}

In the following, we are going to consider various propositions, built
from atomic propositions $A, B, C$. This may be done easily, by
introducing these atoms as global variables declared of type \verb:Prop:.
It is easy to declare several names with the same specification:
\begin{coq_example}
Section Minimal_Logic.
Variables A B C : Prop.
\end{coq_example}

We shall consider simple implications, such as $A\ra B$, read as 
``$A$ implies $B$''. Remark that we overload the arrow symbol, which
has been used above as the functionality type constructor, and which
may be used as well as propositional connective:
\begin{coq_example}
Check (A -> B).
\end{coq_example}

Let us now embark on a simple proof. We want to prove the easy tautology
$((A\ra (B\ra C))\ra (A\ra B)\ra (A\ra C)$. 
We enter the proof engine by the command
\verb:Goal:, followed by the conjecture we want to verify:
\begin{coq_example}
Goal (A -> B -> C) -> (A -> B) -> A -> C.
\end{coq_example}

The system displays the current goal below a double line, local hypotheses
(there are none initially) being displayed above the line. We call 
the combination of local hypotheses with a goal a {\sl judgment}.
We are now in an inner 
loop of the system, in proof mode. 
New commands are available in this
mode, such as {\sl tactics}, which are proof combining primitives.
A tactic operates on the current goal by attempting to construct a proof
of the corresponding judgment, possibly from proofs of some
hypothetical judgments, which are then added to the current
list of conjectured judgments.
For instance, the \verb:intro: tactic is applicable to any judgment
whose goal is an implication, by moving the proposition to the left
of the application to the list of local hypotheses:
\begin{coq_example}
intro H.
\end{coq_example}

Several introductions may be done in one step:
\begin{coq_example}
intros H' HA.
\end{coq_example}

We notice that $C$, the current goal, may be obtained from hypothesis
\verb:H:, provided the truth of $A$ and $B$ are established.
The tactic \verb:apply: implements this piece of reasoning:
\begin{coq_example}
apply H.
\end{coq_example}

We are now in the situation where we have two judgments as conjectures
that remain to be proved. Only the first is listed in full, for the
others the system displays only the corresponding subgoal, without its
local hypotheses list. Remark that \verb:apply: has kept the local
hypotheses of its father judgment, which are still available for
the judgments it generated.

In order to solve the current goal, we just have to notice that it is
exactly available as hypothesis $HA$:
\begin{coq_example}
exact HA.
\end{coq_example}

Now $H'$ applies:
\begin{coq_example}
apply H'.
\end{coq_example}

And we may now conclude the proof as before, with \verb:exact HA.:
Actually, we may not bother with the name \verb:HA:, and just state that
the current goal is solvable from the current local assumptions:
\begin{coq_example}
assumption.
\end{coq_example}

The proof is now finished. We may either discard it, by using the
command \verb:Abort: which returns to the standard \Coq~ toplevel loop
without further ado, or else save it as a lemma in the current context,
under name say \verb:trivial_lemma::
\begin{coq_example}
Save trivial_lemma.
\end{coq_example}

As a comment, the system shows the proof script listing all tactic
commands used in the proof. 

Let us redo the same proof with a few variations. First of all we may name
the initial goal as a conjectured lemma:
\begin{coq_example}
Lemma distr_impl : (A -> B -> C) -> (A -> B) -> A -> C.
\end{coq_example}

Next, we may omit the names of local assumptions created by the introduction
tactics, they can be automatically created by the proof engine as new
non-clashing names.
\begin{coq_example}
intros.
\end{coq_example}

The \verb:intros: tactic, with no arguments, effects as many individual
applications of \verb:intro: as is legal.

Then, we may compose several tactics together in sequence, or in parallel,
through {\sl tacticals}, that is tactic combinators. The main constructions
are the following:
\begin{itemize}
\item $T_1 ; T_2$ (read $T_1$ then $T_2$) applies tactic $T_1$ to the current
goal, and then tactic $T_2$ to all the subgoals generated by $T_1$.
\item $T; [T_1 | T_2 | ... | T_n]$ applies tactic $T$ to the current
goal, and then tactic $T_1$ to the first newly generated subgoal, 
..., $T_n$ to the nth.
\end{itemize}

We may thus complete the proof of \verb:distr_impl: with one composite tactic:
\begin{coq_example}
apply H; [ assumption | apply H0; assumption ].
\end{coq_example}

Let us now save lemma \verb:distr_impl::
\begin{coq_example}
Save.
\end{coq_example}

Here \verb:Save: needs no argument, since we gave the name \verb:distr_impl: 
in advance;
it is however possible to override the given name by giving a different 
argument to command \verb:Save:.

Actually, such an easy combination of tactics \verb:intro:, \verb:apply:
and \verb:assumption: may be found completely automatically by an automatic
tactic, called \verb:auto:, without user guidance:
\begin{coq_example}
Lemma distr_imp : (A -> B -> C) -> (A -> B) -> A -> C.
auto.
\end{coq_example}

This time, we do not save the proof, we just discard it with the \verb:Abort: 
command:

\begin{coq_example}
Abort.
\end{coq_example}

At any point during a proof, we may use \verb:Abort: to exit the proof mode
and go back to Coq's main loop. We may also use \verb:Restart: to restart
from scratch the proof of the same lemma. We may also use \verb:Undo: to
backtrack one step, and more generally \verb:Undo n: to
backtrack n steps.

We end this section by showing a useful command, \verb:Inspect n.:,
which inspects the global \Coq~ environment, showing the last \verb:n: declared
notions: 
\begin{coq_example}
Inspect 3.
\end{coq_example}

The declarations, whether global parameters or axioms, are shown preceded by 
\verb:***:; definitions and lemmas are stated with their specification, but
their value (or proof-term) is omitted.

\section{Propositional Calculus}

\subsection{Conjunction}

We have seen how \verb:intro: and \verb:apply: tactics could be combined
in order to prove implicational statements. More generally, \Coq~ favors a style
of reasoning, called {\sl Natural Deduction}, which decomposes reasoning into 
so called {\sl introduction rules}, which tell how to prove a goal whose main 
operator is a given propositional connective, and {\sl elimination rules},
which tell how to use an hypothesis whose main operator is the propositional 
connective. Let us show how to use these ideas for the propositional connectives
\verb:/\: and \verb:\/:.

\begin{coq_example}
Lemma and_commutative : A /\ B -> B /\ A.
intro.
\end{coq_example}

We make use of the conjunctive hypothesis \verb:H: with the \verb:elim: tactic,
which breaks it into its components:
\begin{coq_example}
elim H.
\end{coq_example}

We now use the conjunction introduction tactic \verb:split:, which splits the 
conjunctive goal into the two subgoals:
\begin{coq_example}
split.
\end{coq_example}
and the proof is now trivial. Indeed, the whole proof is obtainable as follows:
\begin{coq_example}
Restart.
intro H; elim H; auto.
Qed.
\end{coq_example}

The tactic \verb:auto: succeeded here because it knows as a hint the 
conjunction introduction operator \verb+conj+
\begin{coq_example}
Check conj.
\end{coq_example}

Actually, the tactic \verb+Split+ is just an abbreviation for \verb+apply conj.+

What we have just seen is that the \verb:auto: tactic is more powerful than
just a simple application of local hypotheses; it tries to apply as well 
lemmas which have been specified as hints. A 
\verb:Hint Resolve: command registers a
lemma as a hint to be used from now on by the \verb:auto: tactic, whose power 
may thus be incrementally augmented.

\subsection{Disjunction}

In a similar fashion, let us consider disjunction:

\begin{coq_example}
Lemma or_commutative : A \/ B -> B \/ A.
intro H; elim H.
\end{coq_example}

Let us prove the first subgoal in detail. We use \verb:intro: in order to
be left to prove \verb:B\/A: from \verb:A::

\begin{coq_example}
intro HA.
\end{coq_example}

Here the hypothesis \verb:H: is not needed anymore. We could choose to
actually erase it with the tactic \verb:clear:; in this simple proof it
does not really matter, but in bigger proof developments it is useful to
clear away unnecessary hypotheses which may clutter your screen.
\begin{coq_example}
clear H.
\end{coq_example}

The disjunction connective has two introduction rules, since \verb:P\/Q:
may be obtained from \verb:P: or from \verb:Q:; the two corresponding
proof constructors are called respectively \verb:or_introl: and
\verb:or_intror:; they are applied to the current goal by tactics
\verb:left: and \verb:right: respectively. For instance:
\begin{coq_example}
right.
trivial.
\end{coq_example}
The tactic \verb:trivial: works like \verb:auto: with the hints
database, but it only tries those tactics that can solve the goal in one
step. 

As before, all these tedious elementary steps may be performed automatically,
as shown for the second symmetric case:

\begin{coq_example}
auto.
\end{coq_example}

However, \verb:auto: alone does not succeed in proving the full lemma, because
it does not try any elimination step.
It is a bit disappointing that \verb:auto: is not able to prove automatically 
such a simple tautology. The reason is that we want to keep
\verb:auto: efficient, so that it is always effective to use. 

\subsection{Tauto}

A complete tactic for propositional
tautologies is indeed available in \Coq~ as the \verb:tauto: tactic. 
\begin{coq_example}
Restart.
tauto.
Qed.
\end{coq_example}

It is possible to inspect the actual proof tree constructed by \verb:tauto:,
using a standard command of the system, which prints the value of any notion 
currently defined in the context:
\begin{coq_example}
Print or_commutative.
\end{coq_example}

It is not easy to understand the notation for proof terms without a few
explanations. The \texttt{fun} prefix, such as \verb+fun H:A\/B =>+, 
corresponds
to \verb:intro H:, whereas a subterm such as 
\verb:(or_intror: \verb:B H0):
corresponds to the sequence of tactics \verb:apply or_intror; exact H0:. 
The generic combinator \verb:or_intror: needs to be instantiated by
the two properties \verb:B: and \verb:A:. Because \verb:A: can be
deduced from the type of \verb:H0:, only  \verb:B: is printed.
The two instantiations are effected automatically by the tactic
\verb:apply: when pattern-matching a goal. The specialist will of course
recognize our proof term as a $\lambda$-term, used as notation for the
natural deduction proof term through the Curry-Howard isomorphism. The
naive user of \Coq~ may safely ignore these formal details.

Let us exercise the \verb:tauto: tactic on a more complex example:
\begin{coq_example}
Lemma distr_and : A -> B /\ C -> (A -> B) /\ (A -> C).
tauto.
Qed.
\end{coq_example}

\subsection{Classical reasoning}

The tactic \verb:tauto: always comes back with an answer. Here is an example where it 
fails:
\begin{coq_example}
Lemma Peirce : ((A -> B) -> A) -> A.
try tauto.
\end{coq_example}

Note the use of the \verb:Try: tactical, which does nothing if its tactic
argument fails.

This may come as a surprise to someone familiar with classical reasoning. 
Peirce's lemma is true in Boolean logic, i.e. it evaluates to \verb:true: for 
every truth-assignment to \verb:A: and \verb:B:. Indeed the double negation
of Peirce's law may be proved in \Coq~ using \verb:tauto::
\begin{coq_example}
Abort.
Lemma NNPeirce : ~ ~ (((A -> B) -> A) -> A).
tauto.
Qed.
\end{coq_example}

In classical logic, the double negation of a proposition is equivalent to this 
proposition, but in the constructive logic of \Coq~ this is not so. If you 
want to use classical logic in \Coq, you have to import explicitly the
\verb:Classical: module, which will declare the axiom \verb:classic:
of excluded middle, and classical tautologies such as de Morgan's laws.
The \verb:Require: command is used to import a module from \Coq's library:
\begin{coq_example}
Require Import Classical.
Check NNPP.
\end{coq_example}

and it is now easy (although admittedly not the most direct way) to prove
a classical law such as Peirce's:
\begin{coq_example}
Lemma Peirce : ((A -> B) -> A) -> A.
apply NNPP; tauto.
Qed.
\end{coq_example}

Here is one more example of propositional reasoning, in the shape of
a Scottish puzzle. A private club has the following rules:
\begin{enumerate}
\item Every non-scottish member wears red socks
\item Every member wears a kilt or doesn't wear red socks
\item The married members don't go out on Sunday
\item A member goes out on Sunday if and only if he is Scottish
\item Every member who wears a kilt is Scottish and married
\item Every scottish member wears a kilt
\end{enumerate}
Now, we show that these rules are so strict that no one can be accepted.
\begin{coq_example}
Section club.
Variables Scottish RedSocks WearKilt Married GoOutSunday : Prop.
Hypothesis rule1 : ~ Scottish -> RedSocks.
Hypothesis rule2 : WearKilt \/ ~ RedSocks.
Hypothesis rule3 : Married -> ~ GoOutSunday.
Hypothesis rule4 : GoOutSunday <-> Scottish.
Hypothesis rule5 : WearKilt -> Scottish /\ Married.
Hypothesis rule6 : Scottish -> WearKilt.
Lemma NoMember : False.
tauto.
Qed.
\end{coq_example}
At that point \verb:NoMember: is a proof of the absurdity depending on
hypotheses.
We may end the section, in that case, the variables and hypotheses
will be discharged, and the type of \verb:NoMember: will be
generalised.

\begin{coq_example}
End club.
Check NoMember.
\end{coq_example}

\section{Predicate Calculus}

Let us now move into predicate logic, and first of all into first-order
predicate calculus. The essence of predicate calculus is that to try to prove 
theorems in the most abstract possible way, without using the definitions of 
the mathematical notions, but by formal manipulations of uninterpreted 
function and predicate symbols. 

\subsection{Sections and signatures}

Usually one works in some domain of discourse, over which range the individual 
variables and function symbols. In \Coq~ we speak in a language with a rich 
variety of types, so me may mix several domains of discourse, in our 
multi-sorted language. For the moment, we just do a few exercises, over a 
domain of discourse \verb:D: axiomatised as a \verb:Set:, and we consider two 
predicate symbols  \verb:P: and \verb:R: over \verb:D:, of arities 
respectively 1 and 2. Such abstract entities may be entered in the context
as global variables. But we must be careful about the pollution of our
global environment by such declarations. For instance, we have already 
polluted our \Coq~ session by declaring the variables
\verb:n:, \verb:Pos_n:, \verb:A:, \verb:B:, and \verb:C:. If we want to revert to the clean state of
our initial session, we may use the \Coq~ \verb:Reset: command, which returns
to the state just prior the given global notion as we did before to
remove a section, or we may return to the initial state using~:
\begin{coq_example}
Reset Initial.
\end{coq_example}
\begin{coq_eval}
Set Printing Width 60.
\end{coq_eval}

We shall now declare a new \verb:Section:, which will allow us to define
notions local to a well-delimited scope. We start by assuming a domain of
discourse \verb:D:, and a binary relation \verb:R:  over \verb:D:: 
\begin{coq_example}
Section Predicate_calculus.
Variable D : Set.
Variable R : D -> D -> Prop.
\end{coq_example}

As a simple example of predicate calculus reasoning, let us assume
that relation \verb:R: is symmetric and transitive, and let us show that
\verb:R: is reflexive in any point \verb:x: which has an \verb:R: successor.
Since we do not want to make the assumptions about \verb:R: global axioms of 
a theory, but rather local hypotheses to a theorem, we open a specific
section to this effect.
\begin{coq_example}
Section R_sym_trans.
Hypothesis R_symmetric : forall x y:D, R x y -> R y x.
Hypothesis R_transitive : forall x y z:D, R x y -> R y z -> R x z.
\end{coq_example}

Remark the syntax \verb+forall x:D,+ which stands for universal quantification
$\forall x : D$.

\subsection{Existential quantification}

We now state our lemma, and enter proof mode.
\begin{coq_example}
Lemma refl_if : forall x:D, (exists y, R x y) -> R x x.
\end{coq_example}

Remark that the hypotheses which are local to the currently opened sections
are listed as local hypotheses to the current goals.
The rationale is that these hypotheses are going to be discharged, as we
shall see, when we shall close the corresponding sections.

Note the functional syntax for existential quantification. The existential
quantifier is built from the operator \verb:ex:, which expects a 
predicate as argument:
\begin{coq_example}
Check ex.
\end{coq_example}
and the notation \verb+(exists x:D, P x)+ is just concrete syntax for 
the expression \verb+(ex D (fun x:D => P x))+. 
Existential quantification is handled in \Coq~ in a similar
fashion to the connectives \verb:/\: and \verb:\/: : it is introduced by
the proof combinator \verb:ex_intro:, which is invoked by the specific 
tactic \verb:Exists:, and its elimination provides a witness \verb+a:D+ to
\verb:P:, together with an assumption \verb+h:(P a)+ that indeed \verb+a+
verifies \verb:P:. Let us see how this works on this simple example.
\begin{coq_example}
intros x x_Rlinked.
\end{coq_example}

Remark that \verb:intros: treats universal quantification in the same way
as the premises of implications. Renaming of bound variables occurs
when it is needed; for instance, had we started with \verb:intro y:,
we would have obtained the goal:
\begin{coq_eval}
Undo.
\end{coq_eval}
\begin{coq_example}
intro y.
\end{coq_example}
\begin{coq_eval}
Undo.
intros x x_Rlinked.
\end{coq_eval}

Let us now use the existential hypothesis \verb:x_Rlinked: to 
exhibit an R-successor y of x. This is done in two steps, first with
\verb:elim:, then with \verb:intros:

\begin{coq_example}
elim x_Rlinked.
intros y Rxy.
\end{coq_example}

Now we want to use \verb:R_transitive:. The \verb:apply: tactic will know
how to match \verb:x: with \verb:x:, and \verb:z: with \verb:x:, but needs
help on how to instantiate \verb:y:, which appear in the hypotheses of
\verb:R_transitive:, but not in its conclusion. We give the proper hint
to \verb:apply: in a \verb:with: clause, as follows:
\begin{coq_example}
apply R_transitive with y.
\end{coq_example}

The rest of the proof is routine:
\begin{coq_example}
assumption.
apply R_symmetric; assumption.
\end{coq_example}
\begin{coq_example*}
Qed.
\end{coq_example*}

Let us now close the current section.
\begin{coq_example}
End R_sym_trans.
\end{coq_example}

Here \Coq's printout is a warning that all local hypotheses have been 
discharged in the statement of \verb:refl_if:, which now becomes a general
theorem in the first-order language declared in section 
\verb:Predicate_calculus:. In this particular example, the use of section
\verb:R_sym_trans: has not been really significant, since we could have
instead stated theorem \verb:refl_if: in its general form, and done 
basically the same proof, obtaining \verb:R_symmetric: and
\verb:R_transitive: as local hypotheses by initial \verb:intros: rather
than as global hypotheses in the context. But if we had pursued the
theory by proving more theorems about relation \verb:R:,
we would have obtained all general statements at the closing of the section,
with minimal dependencies on the hypotheses of symmetry and transitivity.

\subsection{Paradoxes of classical predicate calculus}

Let us illustrate this feature by pursuing our \verb:Predicate_calculus:
section with an enrichment of our language: we declare a unary predicate
\verb:P: and a constant \verb:d::
\begin{coq_example}
Variable P :  D -> Prop.
Variable d : D.
\end{coq_example}

We shall now prove a well-known fact from first-order logic: a universal 
predicate is non-empty, or in other terms existential quantification 
follows from universal quantification.
\begin{coq_example}
Lemma weird : (forall x:D, P x) ->  exists a, P a.
 intro UnivP.
\end{coq_example}

First of all, notice the pair of parentheses around
\verb+forall x:D, P x+ in
the statement of lemma \verb:weird:.
If we had omitted them, \Coq's parser would have interpreted the
statement as a truly trivial fact, since we would 
postulate an \verb:x: verifying \verb:(P x):. Here the situation is indeed
more problematic. If we have some element in \verb:Set: \verb:D:, we may
apply \verb:UnivP: to it and conclude, otherwise we are stuck. Indeed
such an element \verb:d: exists, but this is just by virtue of our
new signature. This points out a subtle difference between standard
predicate calculus and \Coq. In standard first-order logic,
the equivalent of lemma \verb:weird: always holds, 
because such a rule is wired in the inference rules for quantifiers, the
semantic justification being that the interpretation domain is assumed to
be non-empty. Whereas in \Coq, where types are not assumed to be 
systematically inhabited, lemma \verb:weird: only holds in signatures
which allow the explicit construction of an element in the domain of
the predicate. 

Let us conclude the proof, in order to show the use of the \verb:Exists:
tactic:
\begin{coq_example}
exists d; trivial.
Qed.
\end{coq_example}

Another fact which illustrates the sometimes disconcerting rules of
classical 
predicate calculus is Smullyan's drinkers' paradox: ``In any non-empty
bar, there is a person such that if she drinks, then everyone drinks''.
We modelize the bar by Set \verb:D:, drinking by predicate \verb:P:.
We shall need classical reasoning. Instead of loading the \verb:Classical:
module as we did above, we just state the law of excluded middle as a
local hypothesis schema at this point:
\begin{coq_example}
Hypothesis EM : forall A:Prop, A \/ ~ A.
Lemma drinker :  exists x:D, P x -> forall x:D, P x.
\end{coq_example}
The proof goes by cases on whether or not
there is someone who does not drink. Such reasoning by cases proceeds
by invoking the excluded middle principle, via \verb:elim: of the
proper instance of \verb:EM::
\begin{coq_example}
elim (EM (exists x, ~ P x)).
\end{coq_example}

We first look at the first case. Let Tom be the non-drinker:
\begin{coq_example}
intro Non_drinker; elim Non_drinker;
  intros Tom Tom_does_not_drink.
\end{coq_example}

We conclude in that case by considering Tom, since his drinking leads to
a contradiction:
\begin{coq_example}
exists Tom; intro Tom_drinks.
\end{coq_example}

There are several ways in which we may eliminate a contradictory case;
a simple one is to use the \verb:absurd: tactic as follows:
\begin{coq_example}
absurd (P Tom); trivial.
\end{coq_example}

We now proceed with the second case, in which actually any person will do;
such a John Doe is given by the non-emptiness witness \verb:d::
\begin{coq_example}
intro No_nondrinker; exists d; intro d_drinks.
\end{coq_example}

Now we consider any Dick in the bar, and reason by cases according to its
drinking or not:
\begin{coq_example}
intro Dick; elim (EM (P Dick)); trivial.
\end{coq_example}

The only non-trivial case is again treated by contradiction:
\begin{coq_example}
intro Dick_does_not_drink; absurd (exists x, ~ P x); trivial.
exists Dick; trivial.
Qed.
\end{coq_example}

Now, let us close the main section and look at the complete statements
we proved:
\begin{coq_example}
End Predicate_calculus.
Check refl_if.
Check weird.
Check drinker.
\end{coq_example}

Remark how the three theorems are completely generic in the most general 
fashion;
the domain \verb:D: is discharged in all of them, \verb:R: is discharged in
\verb:refl_if: only, \verb:P: is discharged only in \verb:weird: and
\verb:drinker:, along with the hypothesis that \verb:D: is inhabited. 
Finally, the excluded middle hypothesis is discharged only in 
\verb:drinker:.

Note that the name \verb:d: has vanished as well from
the statements of \verb:weird: and \verb:drinker:, 
since \Coq's pretty-printer replaces
systematically a quantification such as \verb+forall d:D, E+, where \verb:d:
does not occur in \verb:E:, by the functional notation \verb:D->E:. 
Similarly the name \verb:EM: does not appear in \verb:drinker:. 

Actually, universal quantification, implication, 
as well as function formation, are
all special cases of one general construct of type theory called
{\sl dependent product}. This is the mathematical construction 
corresponding to an indexed family of functions. A function 
$f\in \Pi x:D\cdot Cx$ maps an element $x$ of its domain $D$ to its
(indexed) codomain $Cx$. Thus a proof of $\forall x:D\cdot Px$ is
a function mapping an element $x$ of $D$ to a proof of proposition $Px$.


\subsection{Flexible use of local assumptions}

Very often during the course of a proof we want to retrieve a local
assumption and reintroduce it explicitly in the goal, for instance
in order to get a more general induction hypothesis. The tactic
\verb:generalize: is what is needed here:

\begin{coq_example}
Section Predicate_Calculus.
Variables P Q : nat -> Prop.
Variable R :  nat -> nat -> Prop.
Lemma PQR :
 forall x y:nat, (R x x -> P x -> Q x) -> P x -> R x y -> Q x.
intros.
generalize H0.
\end{coq_example}

Sometimes it may be convenient to use a lemma, although we do not have
a direct way to appeal to such an already proven fact. The tactic \verb:cut:
permits to use the lemma at this point, keeping the corresponding proof
obligation as a new subgoal:
\begin{coq_example}
cut (R x x); trivial.
\end{coq_example}
We clean the goal by doing an \verb:Abort: command.
\begin{coq_example*}
Abort.
\end{coq_example*}


\subsection{Equality}

The basic equality provided in \Coq~ is Leibniz equality, noted infix like
\verb+x=y+, when \verb:x: and \verb:y: are two expressions of
type the same Set. The replacement of \verb:x: by \verb:y: in any
term is effected by a variety of tactics, such as \verb:rewrite:
and \verb:replace:. 

Let us give a few examples of equality replacement. Let us assume that
some arithmetic function \verb:f: is null in zero:
\begin{coq_example}
Variable f : nat -> nat.
Hypothesis foo : f 0 = 0.
\end{coq_example}

We want to prove the following conditional equality:
\begin{coq_example*}
Lemma L1 : forall k:nat, k = 0 -> f k = k.
\end{coq_example*}

As usual, we first get rid of local assumptions with \verb:intro::
\begin{coq_example}
intros k E.
\end{coq_example}

Let us now use equation \verb:E: as a left-to-right rewriting:
\begin{coq_example}
rewrite E.
\end{coq_example}
This replaced both occurrences of \verb:k: by \verb:O:. 

Now \verb:apply foo: will finish the proof:

\begin{coq_example}
apply foo.
Qed.
\end{coq_example}

When one wants to rewrite an equality in a right to left fashion, we should
use \verb:rewrite <- E: rather than \verb:rewrite E: or the equivalent
\verb:rewrite -> E:. 
Let us now illustrate the tactic \verb:replace:.
\begin{coq_example}
Hypothesis f10 : f 1 = f 0.
Lemma L2 : f (f 1) = 0.
replace (f 1) with 0.
\end{coq_example}
What happened here is that the replacement left the first subgoal to be
proved, but another proof obligation was generated by the \verb:replace:
tactic, as the second subgoal. The first subgoal is solved immediately
by applying lemma \verb:foo:; the second one transitivity and then 
symmetry of equality, for instance with tactics \verb:transitivity: and 
\verb:symmetry::
\begin{coq_example}
apply foo.
transitivity (f 0); symmetry; trivial.
\end{coq_example}
In case the equality $t=u$ generated by \verb:replace: $u$ \verb:with:
$t$ is an assumption
(possibly modulo symmetry), it will be automatically proved and the
corresponding goal will not appear. For instance:
\begin{coq_example}
Restart.
replace (f 0) with 0.
rewrite f10; rewrite foo; trivial.
Qed.
\end{coq_example}

\section{Using definitions}

The development of mathematics does not simply proceed by logical 
argumentation from first principles: definitions are used in an essential way.
A formal development proceeds by a dual process of abstraction, where one
proves abstract statements in predicate calculus, and use of definitions, 
which in the contrary one instantiates general statements with particular 
notions in order to use the structure of mathematical values for the proof of
more specialised properties.

\subsection{Unfolding definitions}

Assume that we want to develop the theory of sets represented as characteristic
predicates over some universe \verb:U:. For instance:
\begin{coq_example}
Variable U : Type.
Definition set := U -> Prop.
Definition element (x:U) (S:set) := S x.
Definition subset (A B:set) := 
  forall x:U, element x A -> element x B.
\end{coq_example}

Now, assume that we have loaded a module of general properties about
relations over some abstract type \verb:T:, such as transitivity:

\begin{coq_example}
Definition transitive (T:Type) (R:T -> T -> Prop) :=
  forall x y z:T, R x y -> R y z -> R x z.
\end{coq_example}

Now, assume that we want to prove that \verb:subset: is a \verb:transitive:
relation. 
\begin{coq_example}
Lemma subset_transitive : transitive set subset.
\end{coq_example}

In order to make any progress, one needs to use the definition of
\verb:transitive:. The \verb:unfold: tactic, which replaces all
occurrences of a defined notion by its definition in the current goal,
may be used here.
\begin{coq_example}
unfold transitive.
\end{coq_example}

Now, we must unfold \verb:subset::
\begin{coq_example}
unfold subset.
\end{coq_example}
Now, unfolding \verb:element: would be a mistake, because indeed a simple proof
can be found by \verb:auto:, keeping \verb:element: an abstract predicate:
\begin{coq_example}
auto.
\end{coq_example}

Many variations on \verb:unfold: are provided in \Coq. For instance,
we may selectively unfold one designated occurrence:
\begin{coq_example}
Undo 2.
unfold subset at 2.
\end{coq_example}

One may also unfold a definition in a given local hypothesis, using the
\verb:in: notation:
\begin{coq_example}
intros.
unfold subset in H.
\end{coq_example}

Finally, the tactic \verb:red: does only unfolding of the head occurrence
of the current goal:
\begin{coq_example}
red.
auto.
Qed.
\end{coq_example}


\subsection{Principle of proof irrelevance}

Even though in principle the proof term associated with a verified lemma
corresponds to a defined value of the corresponding specification, such
definitions cannot be unfolded in \Coq: a lemma is considered an {\sl opaque}
definition. This conforms to the mathematical tradition of {\sl proof
irrelevance}: the proof of a logical proposition does not matter, and the
mathematical justification of a logical development relies only on
{\sl provability} of the lemmas used in the formal proof. 

Conversely, ordinary mathematical definitions can be unfolded at will, they
are {\sl transparent}. 
\chapter{Induction}

\section{Data Types as Inductively Defined Mathematical Collections}

All the notions which were studied until now pertain to traditional
mathematical logic. Specifications of objects were abstract properties
used in reasoning more or less constructively; we are now entering
the realm of inductive types, which specify the existence of concrete
mathematical constructions.

\subsection{Booleans}

Let us start with the collection of booleans, as they are specified
in the \Coq's \verb:Prelude: module: 
\begin{coq_example}
Inductive bool :  Set := true | false.
\end{coq_example}

Such a declaration defines several objects at once. First, a new
\verb:Set: is declared, with name \verb:bool:. Then the {\sl constructors}
of this \verb:Set: are declared, called \verb:true: and \verb:false:.
Those are analogous to introduction rules of the new Set \verb:bool:.
Finally, a specific elimination rule for \verb:bool: is now available, which
permits to reason by cases on \verb:bool: values. Three instances are
indeed defined as new combinators in the global context: \verb:bool_ind:,
a proof combinator corresponding to reasoning by cases,
\verb:bool_rec:, an if-then-else programming construct,
and \verb:bool_rect:, a similar combinator at the level of types.
Indeed:
\begin{coq_example}
Check bool_ind.
Check bool_rec.
Check bool_rect.
\end{coq_example}

Let us for instance prove that every Boolean is true or false.
\begin{coq_example}
Lemma duality : forall b:bool, b = true \/ b = false.
intro b.
\end{coq_example}

We use the knowledge that \verb:b: is a \verb:bool: by calling tactic
\verb:elim:, which is this case will appeal to combinator \verb:bool_ind:
in order to split the proof according to the two cases:
\begin{coq_example}
elim b.
\end{coq_example}

It is easy to conclude in each case:
\begin{coq_example}
left; trivial.
right; trivial.
\end{coq_example}

Indeed, the whole proof can be done with the combination of the
 \verb:simple: \verb:induction:, which combines \verb:intro: and \verb:elim:,
with good old \verb:auto::
\begin{coq_example}
Restart.
simple induction b; auto.
Qed.
\end{coq_example}

\subsection{Natural numbers}

Similarly to Booleans, natural numbers are defined in the \verb:Prelude:
module with constructors \verb:S: and \verb:O::
\begin{coq_example}
Inductive nat : Set :=
  | O : nat
  | S : nat -> nat.
\end{coq_example}

The elimination principles which are automatically generated are Peano's
induction principle, and a recursion operator:
\begin{coq_example}
Check nat_ind.
Check nat_rec.
\end{coq_example}

Let us start by showing how to program the standard primitive recursion
operator \verb:prim_rec: from the more general \verb:nat_rec::
\begin{coq_example}
Definition prim_rec := nat_rec (fun i:nat => nat).
\end{coq_example}

That is, instead of computing for natural \verb:i: an element of the indexed
\verb:Set: \verb:(P i):, \verb:prim_rec: computes uniformly an element of 
\verb:nat:. Let us check the type of \verb:prim_rec::
\begin{coq_example}
Check prim_rec.
\end{coq_example}

Oops! Instead of the expected type \verb+nat->(nat->nat->nat)->nat->nat+ we
get an apparently more complicated expression. Indeed the type of
\verb:prim_rec: is equivalent by rule $\beta$ to its expected type; this may
be checked in \Coq~ by command \verb:Eval Cbv Beta:, which $\beta$-reduces
an expression to its {\sl normal form}:
\begin{coq_example}
Eval cbv beta in
  ((fun _:nat => nat) O ->
   (forall y:nat, 
      (fun _:nat => nat) y -> (fun _:nat => nat) (S y)) ->
   forall n:nat, (fun _:nat => nat) n).
\end{coq_example}

Let us now show how to program addition with primitive recursion:
\begin{coq_example}
Definition addition (n m:nat) :=
    prim_rec m (fun p rec:nat => S rec) n.
\end{coq_example}

That is, we specify that \verb+(addition n m)+ computes by cases on \verb:n:
according to its main constructor; when \verb:n = O:, we get \verb:m:;
 when \verb:n = S p:, we get \verb:(S rec):, where \verb:rec: is the result
of the recursive computation \verb+(addition p m)+. Let us verify it by
asking \Coq~to compute for us say $2+3$:
\begin{coq_example}
Eval compute in (addition (S (S O)) (S (S (S O)))).
\end{coq_example}

Actually, we do not have to do all explicitly. {\Coq} provides a
special syntax {\tt Fixpoint/match} for generic primitive recursion,
and we could thus have defined directly addition as:

\begin{coq_example}
Fixpoint plus (n m:nat) {struct n} : nat :=
  match n with
  | O => m
  | S p => S (plus p m)
  end.
\end{coq_example}

For the rest of the session, we shall clean up what we did so far with 
types \verb:bool: and \verb:nat:, in order to use the initial definitions
given in \Coq's \verb:Prelude: module, and not to get confusing error
messages due to our redefinitions. We thus revert to the state before
our definition of \verb:bool: with the \verb:Reset: command:
\begin{coq_example}
Reset bool.
\end{coq_example}


\subsection{Simple proofs by induction}

\begin{coq_eval}
Reset Initial.
\end{coq_eval}
\begin{coq_eval}
Set Printing Width 60.
\end{coq_eval}

Let us now show how to do proofs by structural induction. We start with easy
properties of the \verb:plus: function we just defined. Let us first
show that $n=n+0$.
\begin{coq_example}
Lemma plus_n_O : forall n:nat, n = n + 0.
intro n; elim n.
\end{coq_example}

What happened was that \verb:elim n:, in order to construct a \verb:Prop:
(the initial goal) from a \verb:nat: (i.e. \verb:n:), appealed to the
corresponding induction principle \verb:nat_ind: which we saw was indeed
exactly Peano's induction scheme. Pattern-matching instantiated the 
corresponding predicate \verb:P: to \verb+fun n:nat => n = n + 0+, and we get
as subgoals the corresponding instantiations of the base case \verb:(P O): ,
and of the inductive step \verb+forall y:nat, P y -> P (S y)+.
In each case we get an instance of function \verb:plus: in which its second
argument starts with a constructor, and is thus amenable to simplification
by primitive recursion. The \Coq~tactic \verb:simpl: can be used for
this purpose:
\begin{coq_example}
simpl.
auto.
\end{coq_example}

We proceed in the same way for the base step:
\begin{coq_example}
simpl; auto.
Qed.
\end{coq_example}

Here \verb:auto: succeeded, because it used as a hint lemma \verb:eq_S:,
which say that successor preserves equality:
\begin{coq_example}
Check eq_S.
\end{coq_example}

Actually, let us see how to declare our lemma \verb:plus_n_O: as a hint
to be used by \verb:auto::
\begin{coq_example}
Hint Resolve plus_n_O .
\end{coq_example}

We now proceed to the similar property concerning the other constructor
\verb:S::
\begin{coq_example}
Lemma plus_n_S : forall n m:nat, S (n + m) = n + S m.
\end{coq_example}

We now go faster, remembering that tactic \verb:simple induction: does the
necessary \verb:intros: before applying \verb:elim:. Factoring simplification
and automation in both cases thanks to tactic composition, we prove this
lemma in one line:
\begin{coq_example}
simple induction n; simpl; auto.
Qed.
Hint Resolve plus_n_S .
\end{coq_example}

Let us end this exercise with the commutativity of \verb:plus::

\begin{coq_example}
Lemma plus_com : forall n m:nat, n + m = m + n.
\end{coq_example}

Here we have a choice on doing an induction on \verb:n: or on \verb:m:, the
situation being symmetric. For instance:
\begin{coq_example}
simple induction m; simpl; auto.
\end{coq_example}

Here \verb:auto: succeeded on the base case, thanks to our hint
\verb:plus_n_O:, but the induction step requires rewriting, which
\verb:auto: does not handle:

\begin{coq_example}
intros m' E; rewrite <- E; auto.
Qed.
\end{coq_example}

\subsection{Discriminate}

It is also possible to define new propositions by primitive recursion.
Let us for instance define the predicate which discriminates between
the constructors \verb:O: and \verb:S:: it computes to \verb:False: 
when its argument is \verb:O:, and to \verb:True: when its argument is 
of the form \verb:(S n)::
\begin{coq_example}
Definition Is_S (n:nat) := match n with
                           | O => False
                           | S p => True
                           end.
\end{coq_example}

Now we may use the computational power of \verb:Is_S: in order to prove
trivially that \verb:(Is_S (S n))::
\begin{coq_example}
Lemma S_Is_S : forall n:nat, Is_S (S n).
simpl; trivial.
Qed.
\end{coq_example}

But we may also use it to transform a \verb:False: goal into 
\verb:(Is_S O):. Let us show a particularly important use of this feature;
we want to prove that \verb:O: and \verb:S: construct different values, one
of Peano's axioms:
\begin{coq_example}
Lemma no_confusion : forall n:nat, 0 <> S n.
\end{coq_example}

First of all, we replace negation by its definition, by reducing the
goal with tactic \verb:red:; then we get contradiction by successive
\verb:intros::
\begin{coq_example}
red; intros n H.
\end{coq_example}

Now we use our trick:
\begin{coq_example}
change (Is_S 0).
\end{coq_example}

Now we use equality in order to get a subgoal which computes out to 
\verb:True:, which finishes the proof:
\begin{coq_example}
rewrite H; trivial.
simpl; trivial.
\end{coq_example}

Actually, a specific tactic \verb:discriminate: is provided
to produce mechanically such proofs, without the need for the user to define
explicitly the relevant discrimination predicates:

\begin{coq_example}
Restart.
intro n; discriminate.
Qed.
\end{coq_example}


\section{Logic programming}

In the same way as we defined standard data-types above, we
may define inductive families, and for instance inductive predicates.
Here is the definition of predicate $\le$ over type \verb:nat:, as
given in \Coq's \verb:Prelude: module:
\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).
\end{coq_example*}

This definition introduces a new predicate \verb+le:nat->nat->Prop+,
and the two constructors \verb:le_n: and \verb:le_S:, which are the
defining clauses of \verb:le:. That is, we get not only the ``axioms''
\verb:le_n: and \verb:le_S:, but also the converse property, that 
\verb:(le n m): if and only if this statement can be obtained as a
consequence of these defining clauses; that is, \verb:le: is the
minimal predicate verifying clauses \verb:le_n: and \verb:le_S:. This is
insured, as in the case of inductive data types, by an elimination principle,
which here amounts to an induction principle \verb:le_ind:, stating this 
minimality property:
\begin{coq_example}
Check le.
Check le_ind.
\end{coq_example}

Let us show how proofs may be conducted with this principle.
First we show that $n\le m \Rightarrow n+1\le m+1$:
\begin{coq_example}
Lemma le_n_S : forall n m:nat, le n m -> le (S n) (S m).
intros n m n_le_m.
elim n_le_m.
\end{coq_example}

What happens here is similar to the behaviour of \verb:elim: on natural
numbers: it appeals to the relevant induction principle, here \verb:le_ind:,
which generates the two subgoals, which may then be solved easily
with the help of the defining clauses of \verb:le:.
\begin{coq_example}
apply le_n; trivial.
intros; apply le_S; trivial.
\end{coq_example}

Now we know that it is a good idea to give the defining clauses as hints,
so that the proof may proceed with a simple combination of 
\verb:induction: and \verb:auto:.
\begin{coq_example}
Restart.
Hint Resolve le_n le_S .
\end{coq_example}

We have a slight problem however. We want to say ``Do an induction on
hypothesis \verb:(le n m):'', but we have no explicit name for it. What we
do in this case is to say ``Do an induction on the first unnamed hypothesis'',
as follows.
\begin{coq_example}
simple induction 1; auto.
Qed.
\end{coq_example}

Here is a more tricky problem. Assume we want to show that
$n\le 0 \Rightarrow n=0$. This reasoning ought to follow simply from the
fact that only the first defining clause of \verb:le: applies.
\begin{coq_example} 
Lemma tricky : forall n:nat, le n 0 -> n = 0.
\end{coq_example}

However, here trying something like \verb:induction 1: would lead
nowhere (try it and see what happens). 
An induction on \verb:n: would not be convenient either.
What we must do here is analyse the definition of \verb"le" in order
to match hypothesis \verb:(le n O): with the defining clauses, to find
that only \verb:le_n: applies, whence the result. 
This analysis may be performed by the ``inversion'' tactic
\verb:inversion_clear: as follows:
\begin{coq_example} 
intros n H; inversion_clear H.
trivial.
Qed.
\end{coq_example}

\chapter{Modules}

\section{Opening library modules}

When you start \Coq~ without further requirements in the command line,
you get a bare system with few libraries loaded.  As we saw, a standard
prelude module provides the standard logic connectives, and a few
arithmetic notions. If you want to load and open other modules from
the library, you have to use the \verb"Require" command, as we saw for
classical logic above. For instance, if you want more arithmetic
constructions, you should request:
\begin{coq_example*}
Require Import Arith.
\end{coq_example*}

Such a command looks for a (compiled) module file \verb:Arith.vo: in
the libraries registered by \Coq. Libraries inherit the structure of
the file system of the operating system and are registered with the
command \verb:Add LoadPath:. Physical directories are mapped to
logical directories. Especially the standard library of \Coq~ is
pre-registered as a library of name \verb=Coq=.  Modules have absolute
unique names denoting their place in \Coq~ libraries.  An absolute
name is a sequence of single identifiers separated by dots.  E.g. the
module \verb=Arith= has full name \verb=Coq.Arith.Arith= and because
it resides in eponym subdirectory \verb=Arith= of the standard
library, it can be as well required by the command

\begin{coq_example*}
Require Import Coq.Arith.Arith.
\end{coq_example*}

This may be useful to avoid ambiguities if somewhere, in another branch
of the libraries known by Coq, another module is also called
\verb=Arith=. Notice that by default, when a library is registered,
all its contents, and all the contents of its subdirectories recursively are
visible and accessible by a short (relative) name as \verb=Arith=.
Notice also that modules or definitions not explicitly registered in
a library are put in a default library called \verb=Top=.

The loading of a compiled file is quick, because the corresponding
development is not type-checked again. 

\section{Creating your own modules}

You may create your own module files, by writing {\Coq} commands in a file,
say \verb:my_module.v:. Such a module may be simply loaded in the current
context, with command \verb:Load my_module:. It may also be compiled,
in ``batch'' mode, using the UNIX command
\verb:coqc:. Compiling the module \verb:my_module.v: creates a 
file \verb:my_module.vo:{} that can be reloaded with command
\verb:Require: \verb:Import: \verb:my_module:. 

If a required module depends on other modules then the latters are
automatically required beforehand. However their contents is not
automatically visible.  If you want a module \verb=M= required in a
module \verb=N= to be automatically visible when \verb=N= is required,
you should use \verb:Require Export M: in your module \verb:N:.

\section{Managing the context}

It is often difficult to remember the names of all lemmas and
definitions available in the current context, especially if large
libraries have been loaded. A convenient \verb:SearchAbout: command
is available to lookup all known facts 
concerning a given predicate. For instance, if you want to know all the
known lemmas about the less or equal relation, just ask:
\begin{coq_example}
SearchAbout le.
\end{coq_example}
Another command \verb:Search: displays only lemmas where the searched
predicate appears at the head position in the conclusion.
\begin{coq_example}
Search le.
\end{coq_example}

A new and more convenient search tool is \textsf{SearchPattern}
developed by Yves Bertot. It allows to find the theorems with a
conclusion matching a given pattern, where \verb:\_: can be used in
place of an arbitrary term. We remark in this example, that \Coq{}
provides usual infix notations for arithmetic operators.

\begin{coq_example}
SearchPattern (_ + _ = _).
\end{coq_example}

\section{Now you are on your own}

This tutorial is necessarily incomplete. If you wish to pursue serious
proving in \Coq, you should now get your hands on \Coq's Reference Manual,
which contains a complete description of all the tactics we saw, 
plus many more.
You also should look in the library of developed theories which is distributed
with \Coq, in order to acquaint yourself with various proof techniques.


\end{document}

% $Id$