aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/refman/RefMan-tus.tex
blob: 3e29886762aff35a921a43cabb42a7c319a4e9f4 (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
1578
1579
1580
1581
1582
1583
1584
1585
1586
1587
1588
1589
1590
1591
1592
1593
1594
1595
1596
1597
1598
1599
1600
1601
1602
1603
1604
1605
1606
1607
1608
1609
1610
1611
1612
1613
1614
1615
1616
1617
1618
1619
1620
1621
1622
1623
1624
1625
1626
1627
1628
1629
1630
1631
1632
1633
1634
1635
1636
1637
1638
1639
1640
1641
1642
1643
1644
1645
1646
1647
1648
1649
1650
1651
1652
1653
1654
1655
1656
1657
1658
1659
1660
1661
1662
1663
1664
1665
1666
1667
1668
1669
1670
1671
1672
1673
1674
1675
1676
1677
1678
1679
1680
1681
1682
1683
1684
1685
1686
1687
1688
1689
1690
1691
1692
1693
1694
1695
1696
1697
1698
1699
1700
1701
1702
1703
1704
1705
1706
1707
1708
1709
1710
1711
1712
1713
1714
1715
1716
1717
1718
1719
1720
1721
1722
1723
1724
1725
1726
1727
1728
1729
1730
1731
1732
1733
1734
1735
1736
1737
1738
1739
1740
1741
1742
1743
1744
1745
1746
1747
1748
1749
1750
1751
1752
1753
1754
1755
1756
1757
1758
1759
1760
1761
1762
1763
1764
1765
1766
1767
1768
1769
1770
1771
1772
1773
1774
1775
1776
1777
1778
1779
1780
1781
1782
1783
1784
1785
1786
1787
1788
1789
1790
1791
1792
1793
1794
1795
1796
1797
1798
1799
1800
1801
1802
1803
1804
1805
1806
1807
1808
1809
1810
1811
1812
1813
1814
1815
1816
1817
1818
1819
1820
1821
1822
1823
1824
1825
1826
1827
1828
1829
1830
1831
1832
1833
1834
1835
1836
1837
1838
1839
1840
1841
1842
1843
1844
1845
1846
1847
1848
1849
1850
1851
1852
1853
1854
1855
1856
1857
1858
1859
1860
1861
1862
1863
1864
1865
1866
1867
1868
1869
1870
1871
1872
1873
1874
1875
1876
1877
1878
1879
1880
1881
1882
1883
1884
1885
1886
1887
1888
1889
1890
1891
1892
1893
1894
1895
1896
1897
1898
1899
1900
1901
1902
1903
1904
1905
1906
1907
1908
1909
1910
1911
1912
1913
1914
1915
1916
1917
1918
1919
1920
1921
1922
1923
1924
1925
1926
1927
1928
1929
1930
1931
1932
1933
1934
1935
1936
1937
1938
1939
1940
1941
1942
1943
1944
1945
1946
1947
1948
1949
1950
1951
1952
1953
1954
1955
1956
1957
1958
1959
1960
1961
1962
1963
1964
1965
1966
1967
1968
1969
1970
1971
1972
1973
1974
1975
1976
1977
1978
1979
1980
1981
1982
1983
1984
1985
1986
1987
1988
1989
1990
1991
1992
1993
1994
1995
1996
1997
1998
1999
2000
2001
%\documentclass[11pt]{article}
%\usepackage{fullpage,euler}
%\usepackage[latin1]{inputenc}
%\begin{document}
%\title{Writing ad-hoc Tactics in Coq}
%\author{} 
%\date{}
%\maketitle
%\tableofcontents
%\clearpage

\chapter[Writing ad-hoc Tactics in Coq]{Writing ad-hoc Tactics in Coq\label{WritingTactics}}

\section{Introduction}

\Coq\ is an open proof environment, in the sense that the collection of
proof strategies offered by the system can be extended by the user.
This feature has two important advantages. First, the user can develop
his/her own ad-hoc proof procedures, customizing the system for a
particular domain of application. Second, the repetitive and tedious
aspects of the proofs can be abstracted away implementing new tactics
for dealing with them. For example, this may be useful when a theorem
needs several lemmas which are all proven in a similar but not exactly
the same way. Let us illustrate this with an example.

Consider the problem of deciding the equality of two booleans. The
theorem establishing that this is always possible is state by 
the following theorem:

\begin{coq_example*}
Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
\end{coq_example*}

The proof proceeds by case analysis on both $x$ and $y$. This yields
four cases to solve. The cases $x=y=\textsl{true}$ and
$x=y=\textsl{false}$ are immediate by the reflexivity of equality.

The other two cases follow by discrimination. The following script
describes the proof:

\begin{coq_example*}
Destruct x.
  Destruct y.
    Left ; Reflexivity.
    Right; Discriminate.
  Destruct y.
    Right; Discriminate.
    Left ; Reflexivity.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

Now, consider the theorem stating the same property but for the
following enumerated type:

\begin{coq_example*}
Inductive Set Color := Blue:Color | White:Color | Red:Color.
Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
\end{coq_example*}

This theorem can be proven in a very similar way, reasoning by case
analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is
solved either by reflexivity or by discrimination:

\begin{coq_example*}
Destruct c1. 
  Destruct c2.
    Left  ; Reflexivity.
    Right ; Discriminate.
    Right ; Discriminate.
  Destruct c2.  
    Right ; Discriminate.
    Left  ; Reflexivity.
    Right ; Discriminate.
  Destruct c2.  
    Right ; Discriminate.
    Right ; Discriminate.
    Left  ; Reflexivity.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

If we face the same theorem for an enumerated datatype corresponding
to the days of the week, it would still follow a similar pattern. In
general, the general pattern for proving the property
$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as
follow:
\begin{enumerate}
\item Analyze the cases for $x$. 
\item For each of the sub-goals generated by the first step, analyze
the cases for $y$.
\item The remaining subgoals follow either by reflexivity or
by discrimination.
\end{enumerate}

Let us describe how this general proof procedure can be introduced in
\Coq.

\section{Tactic Macros}

The simplest way to introduce it is to define it as new a
\textsl{tactic macro}, as follows:

\begin{coq_example*}
Tactic Definition DecideEq [$a $b] := 
   [<:tactic:<Destruct $a;
              Destruct $b;
              (Left;Reflexivity) Orelse (Right;Discriminate)>>].
\end{coq_example*}

The general pattern of the proof is abstracted away using the
tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two
parameters for the names of the arguments to be analyzed.

Once defined, this tactic can be called like any other tactic, just
supplying the list of terms corresponding to its real arguments. Let us
revisit the proof of the former theorems using the new tactic
\texttt{DecideEq}:

\begin{coq_example*}
Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
DecideEq x y.
Defined.
\end{coq_example*}
\begin{coq_example*}
Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
DecideEq c1 c2.
Defined.
\end{coq_example*}

In general, the command \texttt{Tactic Definition} associates a name
to a parameterized tactic expression, built up from the tactics and
tacticals that are already available. The general syntax rule for this
command is the following:

\begin{tabbing}
\texttt{Tactic Definition} \textit{tactic-name} \= 
\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\
\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+
\end{tabbing}

This command provides a quick but also very primitive mechanism for
introducing new tactics. It does not support recursive definitions,
and the arguments of a tactic macro are restricted to term
expressions.  Moreover, there is no static checking of the definition
other than the syntactical one. Any error in the definition of the
tactic ---for instance, a call to an undefined tactic--- will not be
noticed until the tactic is called.

%This command provides a very primitive mechanism for introducing new
%tactics. The arguments of a tactic macro are restricted to term
%expressions.  Hence, it is not possible to define higher order tactics
%with this command. Also, there is no static checking of the definition
%other than syntactical. If the tactic contain errors in its definition
%--for instance, a call to an undefined tactic-- this will be noticed
%during the tactic call.

Let us illustrate the weakness of this way of introducing new tactics
trying to extend our proof procedure to work on a larger class of
inductive types.  Consider for example the decidability of equality
for pairs of booleans and colors:

\begin{coq_example*}
Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}.
\end{coq_example*}

The proof still proceeds by a double case analysis, but now the
constructors of the type take two arguments. Therefore, the sub-goals
that can not be solved by discrimination need further considerations
about the equality of such arguments:

\begin{coq_example}
  Destruct p1;
    Destruct p2; Try (Right;Discriminate);Intros.
\end{coq_example}

The half of the disjunction to be chosen depends on whether or not
$b=b_0$ and $c=c_0$. These equalities can be decided automatically
using the previous lemmas about booleans and colors. If both
equalities are satisfied, then it is sufficient to rewrite $b$ into
$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by
reflexivity.  Otherwise, the right half follows by first contraposing
the disequality, and then applying the invectiveness of the pairing
constructor.

As the cases associated to each argument of the pair are very similar,
a tactic macro can be introduced to abstract this part of the proof:

\begin{coq_example*}
Hints Resolve decideBool decideColor.
Tactic Definition SolveArg [$t1 $t2] := 
 [<:tactic:<
   ElimType {$t1=$t2}+{~$t1=$t2};
   [(Intro equality;Rewrite equality;Clear equality) |
    (Intro diseq; Right; Red; Intro absurd;
     Apply diseq;Injection absurd;Trivial) |
    Auto]>>].
\end{coq_example*}

This tactic is applied to each corresponding pair of arguments of the
arguments, until the goal can be solved by reflexivity:

\begin{coq_example*}
SolveArg b b0;
  SolveArg c c0;
    Left; Reflexivity.
Defined.
\end{coq_example*}

Therefore, a more general strategy for deciding the property 
$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows:
\begin{enumerate}
\item Eliminate $x$ and then $y$.
\item Try discrimination to solve those goals where $x$ and $y$ has
been introduced by different constructors.
\item If $x$ and $y$ have been introduced by the same constructor,
then iterate the tactic \textsl{SolveArg} for each pair of
arguments. 
\item Finally, solve the left half of the goal by reflexivity.
\end{enumerate}

The implementation of this stronger proof strategy needs to perform a
term decomposition, in order to extract the list of arguments of each
constructor. It also requires the introduction of recursively defined
tactics, so that the \textsl{SolveArg} can be iterated on the lists of
arguments. These features are not supported by the \texttt{Tactic
Definition} command. One possibility could be extended this command in
order to introduce recursion, general parameter passing,
pattern-matching, etc, but this would quickly lead us to introduce the
whole \ocaml{} into \Coq\footnote{This is historically true. In fact,
\ocaml{} is a direct descendent of ML, a functional programming language
conceived language for programming the tactics of the theorem prover
LCF.}.  Instead of doing this, we prefer to give to the user the
possibility of writing his/her own tactics directly in \ocaml{}, and then
to link them dynamically with \Coq's code. This requires a minimal
knowledge about \Coq's implementation. The next section provides an
overview of \Coq's architecture.

%It is important to point out that the introduction of a new tactic
%never endangers the correction of the theorems proven in the extended
%system. In order to understand why, let us introduce briefly the system
%architecture.

\section{An Overview of \Coq's Architecture}

The implementation of \Coq\ is based on eight \textsl{logical
modules}. By ``module'' we mean here a logical piece of code having a
conceptual unity, that may concern several \ocaml{} files. By the sake of
organization, all the \ocaml{} files concerning a logical module are
grouped altogether into the same sub-directory. The eight modules
are:

\begin{tabular}{lll}
1. & The logical framework           & (directory \texttt{src/generic})\\
2. &  The language of constructions  & (directory \texttt{src/constr})\\
3. &  The type-checker               & (directory \texttt{src/typing})\\
4. &  The proof engine               & (directory \texttt{src/proofs})\\
5. &  The language of basic tactics  & (directory \texttt{src/tactics})\\
6. &  The vernacular interpreter     & (directory \texttt{src/env})\\
7. &  The parser and the pretty-printer  & (directory \texttt{src/parsing})\\
8. &  The standard library           & (directory \texttt{src/lib})
\end{tabular}

\vspace{1em}

The following sections briefly present each of the modules above.
This presentation is not intended to be a complete description of \Coq's
implementation, but rather a guideline to be read before taking a look
at the sources. For each of the modules, we also present some of its
most important functions, which are sufficient to implement a large
class of tactics.


\subsection[The Logical Framework]{The Logical Framework\label{LogicalFramework}}

At the very heart of \Coq there is a generic untyped language for
expressing abstractions, applications and global constants. This
language is used as a meta-language for expressing the terms of the
Calculus of Inductive Constructions. General operations on terms like
collecting the free variables of an expression, substituting a term for
a free variable, etc, are expressed in this language.

The meta-language \texttt{'op term} of terms has seven main
constructors:
\begin{itemize}
\item $(\texttt{VAR}\;id)$, a reference to a global identifier called  $id$;
\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$
      binder up in the term;
\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$;
\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of 
      the vector $vt$;
\item $(\texttt{DOP0}\;op)$, a unary operator $op$;
\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary
operator $op$ to the terms $t_1$ and $t_2$;
\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the
vector of terms $vt$.
\end{itemize}

In this meta-language, bound variables are represented using the
so-called deBrujin's indexes. In this representation, an occurrence of
a bound variable is denoted by an integer, meaning the number of
binders that must be traversed to reach its own
binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
have to be traversed, since indexes are represented by strictly
positive integers.}. On the other hand, constants are referred by its
name, as usual. For example, if $A$ is a variable of the current
section, then the lambda abstraction $[x:A]x$ of the Calculus of
Constructions is represented in the meta-language by the term:

\begin{displaymath}
(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1)))
\end{displaymath}

In this term, $Lambda$ is a binary operator.  Its first argument
correspond to the type $A$ of the bound variable, while the second is
a body of the abstraction, where $x$ is bound.  The name $x$ is just kept
to pretty-print the occurrences of the bound variable.

%Similarly, the product
%$(A:Prop)A$ of the Calculus of Constructions is represented by the
%term:
%\begin{displaumath}
%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1))
%\end{displaymath}

The following functions perform some of the most frequent operations
on the terms of the meta-language:
\begin{description}
\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term}
    {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for 
      $\texttt{(Rel}\;1)$ in $t_2$.}
\fun{val Generic.occur\_var : identifier -> 'op term -> bool}
    {Returns true when the given identifier appears in the term,
    and false otherwise.}
\fun{val Generic.eq\_term : 'op term -> 'op term -> bool}
    {Implements $\alpha$-equality for terms.}  
\fun{val Generic.dependent : 'op term -> 'op term -> bool}
    {Returns true if the first term is a sub-term of the second.}
%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term}
%    { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index
%     associated to $id$ to every occurrence of the term
%    $(\texttt{VAR}\;id)$ in $t$.}
\end{description}

\subsubsection{Identifiers, names and sections paths.} 

Three different kinds of names are used in the meta-language. They are
all defined in the \ocaml{} file \texttt{Names}.

\paragraph{Identifiers.}  The simplest kind of names are
\textsl{identifiers}. An identifier is a string possibly indexed by an
integer. They are used to represent names that are not unique, like
for example the name of a variable in the scope of a section.  The
following operations can be used for handling identifiers:

\begin{description}
\fun{val Names.make\_ident : string -> int -> identifier}
    {The value $(\texttt{make\_ident}\;x\;i)$ creates the
    identifier $x_i$. If $i=-1$, then the identifier has
    is created with no index at all.}
\fun{val Names.repr\_ident : identifier -> string * int}
    {The inverse operation of \texttt{make\_ident}: 
     it yields the string and the index of the identifier.}
\fun{val Names.lift\_ident : identifier -> identifier}
    {Increases the index of the identifier by one.}
\fun{val Names.next\_ident\_away : \\
\qquad identifier -> identifier list -> identifier}
    {\\ Generates a new identifier with the same root string than the
    given one, but with a new index, different from all the indexes of
    a given list of identifiers.} 
\fun{val Names.id\_of\_string : string ->
    identifier} 
    {Creates an identifier from a string.}  
\fun{val  Names.string\_of\_id : identifier -> string} 
    {The inverse operation: transforms an identifier into a string}
\end{description}

\paragraph{Names.} A \textsl{name} is either an identifier or the 
special name \texttt{Anonymous}. Names are used as arguments of
binders, in order to pretty print bound variables.
The following operations can be used for handling names:

\begin{description}
\fun{val Names.Name: identifier -> Name}
    {Constructs a name from  an identifier.}
\fun{val Names.Anonymous : Name}
    {Constructs a special, anonymous identifier, like the variable abstracted 
     in the term $[\_:A]0$.}
\fun{val
     Names.next\_name\_away\_with\_default : \\ \qquad
          string->name->identifier list->identifier}
{\\ If the name is not anonymous, then this function generates a new
    identifier different from all the ones in a given list. Otherwise, it
    generates an identifier from the given string.}
\end{description}

\paragraph[Section paths.]{Section paths.\label{SectionPaths}}
A \textsl{section-path} is a global name to refer to an object without
ambiguity.  It can be seen as a sort of filename, where open sections
play the role of directories. Each section path is formed by three
components: a \textsl{directory} (the list of open sections); a
\textsl{basename} (the identifier for the object); and a \textsl{kind}
(either CCI for the terms of the Calculus of Constructions, FW for the
the terms of $F_\omega$, or OBJ for other objects). For example, the
name of the following constant:
\begin{verbatim}
     Section A.
     Section B.
     Section C.
     Definition zero := O.
\end{verbatim}

is internally represented by the section path:

$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}}
\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}}
\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$

When one of the sections is closed, a new constant is created with an
updated section-path,a nd the old one is no longer reachable.  In our
example, after closing the section \texttt{C}, the new section-path
for the constant {\tt zero} becomes:
\begin{center}
\texttt{ \#A\#B\#zero.cci}
\end{center}

The following operations can be used to handle section paths:

\begin{description}
\fun{val Names.string\_of\_path : section\_path -> string}
    {Transforms the section path into a string.}
\fun{val Names.path\_of\_string : string -> section\_path}
    {Parses a string an returns the corresponding section path.}
\fun{val Names.basename : section\_path -> identifier}
    {Provides the basename of a section path}
\fun{val Names.dirpath : section\_path -> string list}
    {Provides the directory of a section path}
\fun{val Names.kind\_of\_path : section\_path -> path\_kind}
    {Provides the kind of a section path}
\end{description}

\subsubsection{Signatures} 

A \textsl{signature} is a mapping associating different informations
to identifiers (for example, its type, its definition, etc). The
following operations could be useful for working with signatures:

\begin{description}
\fun{val Names.ids\_of\_sign  : 'a signature -> identifier list}
    {Gets the list of identifiers of the signature.}
\fun{val Names.vals\_of\_sign : 'a signature -> 'a list}
    {Gets the list of values associated to the identifiers of the signature.}
\fun{val Names.lookup\_glob1 : \\ \qquad
identifier -> 'a signature -> (identifier *
    'a)}
    {\\ Gets the value associated to a given identifier of the signature.}
\end{description}


\subsection{The Terms of the Calculus of Constructions}

The language of the Calculus of Inductive Constructions described in
Chapter \ref{Cic} is implemented on the top of the logical framework,
instantiating the parameter $op$ of the meta-language with a
particular set of operators.  In the implementation this language is
called \texttt{constr}, the language of constructions.

% The only difference
%with respect to the one described in Section \ref{} is that the terms
%of \texttt{constr} may contain \textsl{existential variables}. An
%existential variable is a place holder representing a part of the term
%that is still to be constructed. Such ``open terms'' are necessary
%when building proofs interactively.

\subsubsection{Building Constructions}

The user does not need to know the choices made to represent
\texttt{constr} in the meta-language. They are abstracted away by the
following constructor functions:

\begin{description}
\fun{val Term.mkRel          : int -> constr}
    {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.}

\fun{val Term.mkVar : identifier -> constr} 
    {$(\texttt{mkVar}\;id)$
    represents a global identifier named $id$, like a variable
    inside the scope of a section, or a hypothesis in a proof}.

\fun{val Term.mkExistential : constr} 
   {\texttt{mkExistential} represents an implicit sub-term, like the question
    marks in the term \texttt{(pair ? ? O true)}.}

%\fun{val Term.mkMeta         : int -> constr}
%    {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose
%     name is the integer $n$.}

\fun{val Term.mkProp         : constr}
    {$\texttt{mkProp}$ represents the sort \textsl{Prop}.}

\fun{val Term.mkSet          : constr}
    {$\texttt{mkSet}$ represents the sort \textsl{Set}.}

\fun{val Term.mkType         : Impuniv.universe -> constr}
    {$(\texttt{mkType}\;u)$ represents the term
    $\textsl{Type}(u)$. The universe $u$ is represented as a 
    section path indexed by an integer. }

\fun{val Term.mkConst : section\_path -> constr array -> constr}
    {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is
    $c$. The body of the constant is stored in a global table,
    accessible through the name of the constant. The array of terms
    $v$ corresponds to the variables of the environment appearing in
    the body of the constant when it was defined. For instance, a
    constant defined in the section \textsl{Foo} containing the
    variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is
    represented inside the scope of the section by
    $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A
    |])$.  Once the section is closed, the constant is represented by
    the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body
    becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}.

\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr}
    {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type
    (starting from zero) of the block of mutually dependent
    (co)inductive types, whose first type is $c$.  Similarly to the
    case of constants, the array of terms represents the current
    environment of the (co)inductive type. The definition of the type
    (its arity, its constructors, whether it is inductive or co-inductive, etc.)
    is stored in a global hash table, accessible through the name of 
    the type.}

\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array
    ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the
    $jth$ constructor of the $ith$ type of the block of mutually
    dependent (co)inductive types whose first type is $c$. The array
    of terms represents the current environment of the (co)inductive
    type.}

\fun{val Term.mkCast : constr -> constr -> constr}
    {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in
    \Coq's syntax.}  

\fun{val Term.mkProd : name ->constr ->constr -> constr}
    {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
     The free ocurrences of $x$ in $B$ are represented by deBrujin's
     indexes.}

\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
    {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$,
     but the bound occurrences of $x$ in $B$ are denoted by 
     the identifier $(\texttt{mkVar}\;x)$. The function automatically 
     changes each occurrences of this identifier into the corresponding 
     deBrujin's index.}

\fun{val Term.mkArrow : constr -> constr -> constr}
    {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}

\fun{val Term.mkLambda       : name -> constr -> constr -> constr}
    {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's
     indexes.}

\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
    {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction 
     $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by 
     the identifier $(\texttt{mkVar}\;x)$. }

\fun{val Term.mkAppLA        : constr array -> constr}
    {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application
    $(t\;t_1\;\ldots t_n)$.}

\fun{val Term.mkMutCaseA : \\ \qquad
    case\_info -> constr ->constr
    ->constr array -> constr} 
    {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$
    represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument
    $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the
    pair $(c,i)$ refers to the inductive type that $m$ belongs to.}

\fun{val Term.mkFix :  \\ \qquad
int array->int->constr array->name
    list->constr array->constr}
    {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots
    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
    $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$}

\fun{val Term.mkCoFix  : \\ \qquad
    int -> constr array -> name list ->
    constr array -> constr}
    {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots
    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
    $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no
    decreasing indexes in this case.}
\end{description}

\subsubsection{Decomposing Constructions}

Each of the construction functions above has its corresponding
(partial) destruction function, whose name is obtained changing the
prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a
concrete datatype \texttt{kindOfTerm} can be used to do pattern
matching on terms without dealing with their internal representation
in the meta-language. This concrete datatype is described in the \ocaml{}
file \texttt{term.mli}. The following function transforms a construction
into an element of type \texttt{kindOfTerm}:

\begin{description}
\fun{val Term.kind\_of\_term : constr -> kindOfTerm}
    {Destructs a term of the language \texttt{constr},
yielding the direct components of the term. Hence, in order to do 
pattern matching on an object $c$ of \texttt{constr}, it is sufficient
to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.}
\end{description}

Part of the information associated to the constants is stored in 
global tables. The following functions give access to such 
information:

\begin{description}
\fun{val Termenv.constant\_value    : constr -> constr}
    {If the term denotes a constant, projects the body of a constant}
\fun{Termenv.constant\_type     : constr -> constr}
    {If the term denotes a constant, projects the type of the constant}
\fun{val mind\_arity        : constr -> constr}
    {If the term denotes an inductive type, projects its arity (i.e.,
     the type of the inductive type).}
\fun{val Termenv.mis\_is\_finite    : mind\_specif -> bool}
    {Determines whether a recursive type is inductive or co-inductive.}
\fun{val Termenv.mind\_nparams : constr -> int}
    {If the term denotes an inductive type, projects the number of 
     its general parameters.}
\fun{val Termenv.mind\_is\_recursive : constr -> bool}
    {If the term denotes an inductive type, 
     determines if the type has at least one recursive constructor. }
\fun{val Termenv.mind\_recargs : constr -> recarg list array array}
    {If the term denotes an inductive type, returns an array $v$ such 
     that the nth element of $v.(i).(j)$ is
    \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of
    the $ith$ type is recursive, and \texttt{Norec} if it is not.}.
\end{description}

\subsection[The Type Checker]{The Type Checker\label{TypeChecker}}

The third logical module is the type checker. It concentrates two main
tasks concerning the language of constructions.

On one hand, it contains the type inference and type-checking
functions.  The type inference function takes a term
$a$ and a signature $\Gamma$, and yields a term $A$ such that
$\Gamma \vdash a:A$.  The type-checking function takes two terms $a$
and $A$ and a signature $\Gamma$, and determines whether or not
$\Gamma \vdash a:A$.

On the other hand, this module is in charge of the compilation of
\Coq's abstract syntax trees into the language \texttt{constr} of
constructions. This compilation seeks to eliminate all the ambiguities
contained in \Coq's abstract syntax, restoring the information
necessary to type-check it.  It concerns at least the following steps:
\begin{enumerate}
\item Compiling the pattern-matching expressions containing 
constructor patterns, wild-cards, etc, into terms that only
use the primitive \textsl{Case} described in Chapter \ref{Cic}
\item Restoring type coercions and synthesizing the implicit arguments
(the one denoted by question marks in
{\Coq} syntax: see Section~\ref{Coercions}).
\item Transforming the named bound variables into deBrujin's indexes.
\item Classifying the global names into the different classes of
constants (defined constants, constructors, inductive types, etc).
\end{enumerate}

\subsection{The Proof Engine}

The fourth stage of \Coq's implementation is the \textsl{proof engine}:
the interactive machine for constructing proofs. The aim of the proof
engine is to construct a top-down derivation or \textsl{proof tree},
by the application of \textsl{tactics}. A proof tree has the following
general structure:\\

\begin{displaymath}
\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G}
     {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1}
         {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} 
           : G_{i_1}}}}(tac_1)
      \;\;\;\;\;\;\;\;\;
      \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n}
         {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} :
     G_{i_m}}}}(tac_n)} (tac)    
\end{displaymath}


\noindent Each node of the tree is called a \textsl{goal}. A goal
is a record type containing the following three fields:
\begin{enumerate}
\item the conclusion $G$ to be proven;
\item a typing signature $\Gamma$ for the free variables in $G$;
\item if the goal is an internal node of the proof tree, the
definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable}
(i.e. a possible undefined constant) $?$ of type $G$ in terms of the
existential variables of the children sub-goals. If the node is a
leaf, the existential variable maybe still undefined.
\end{enumerate}

Once all the existential variables have been defined the derivation is
completed, and a construction can be generated from the proof tree,
replacing each of the existential variables by its definition.  This
is exactly what happens when one of the commands
\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
(see Section~\ref{Qed}). The saved theorem becomes a defined constant,
whose body is the proof object generated.

\paragraph{Important:} Before being added to the
context, the proof object is type-checked, in order to verify that it is
actually an object of the expected type $G$.  Hence, the correctness
of the proof actually does not depend on the tactics applied to
generate it or the machinery of the proof engine, but only on the
type-checker. In other words, extending the system with a potentially
bugged new tactic never endangers the consistency of the system.

\subsubsection[What is a Tactic?]{What is a Tactic?\label{WhatIsATactic}}
%Let us now explain what is a tactic, and how the user can introduce
%new ones. 

From an operational point of view, the current state of the proof
engine is given by the mapping $emap$ from existential variables into
goals, plus a pointer to one of the leaf goals $g$.  Such a pointer
indicates where the proof tree will be refined by the application of a
\textsl{tactic}. A tactic is a function from the current state
$(g,emap)$ of the proof engine into a pair $(l,val)$. The first
component of this pair is the list of children sub-goals $g_1,\ldots
g_n$ of $g$ to be yielded by the tactic. The second one is a
\textsl{validation function}. Once the proof trees $\pi_1,\ldots
\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation
function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving
$g$.

Tactics can be classified into \textsl{primitive} ones and
\textsl{defined} ones. Primitive tactics correspond to the five basic
operations of the proof engine:

\begin{enumerate}
\item Introducing a universally quantified variable into the local
context of the goal.
\item Defining an undefined existential variable 
\item Changing the conclusion of the goal for another
--definitionally equal-- term.
\item Changing the type of a variable in the local context for another
definitionally equal term.
\item Erasing a variable from the local context.
\end{enumerate}

\textsl{Defined} tactics are tactics constructed by combining these
primitive operations.  Defined tactics are registered in a hash table,
so that they can be introduced dynamically. In order to define such a
tactic table, it is necessary to fix what a \textsl{possible argument}
of a tactic may be. The type \texttt{tactic\_arg} of the possible
arguments for tactics is a union type including:
\begin{itemize}
\item quoted strings;
\item integers;
\item identifiers;
\item lists of identifiers;
\item plain terms, represented by its abstract syntax tree;
\item well-typed terms, represented by a construction;
\item a substitution for bound variables, like the
substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots
x_n:=t_n$, (see Section~\ref{apply});
\item a reduction expression, denoting the reduction strategy to be
followed.
\end{itemize}
Therefore, for each function $tac:a \rightarrow tactic$ implementing a
defined tactic, an associated dynamic tactic $tacargs\_tac:
\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be
written. The aim of the auxiliary function $tacargs\_tac$ is to inject
the arguments of the tactic $tac$ into the type of possible arguments
for a tactic.

The following function can be used for registering and calling a
defined tactic:

\begin{description}
\fun{val Tacmach.add\_tactic : \\ \qquad
string -> (tactic\_arg list ->tactic) -> unit}
    {\\ Registers a dynamic tactic with the given string as access index.}
\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic}
    {Interprets a defined tactic given by its entry in the
     tactics table with a particular list of possible arguments.}
\fun{val Tacinterp.vernac\_interp        : CoqAst.t -> tactic}
    {Interprets a tactic expression formed combining \Coq's tactics and
          tacticals, and described by its abstract syntax tree.}
\end{description}

When programming a new tactic that calls an already defined tactic
$tac$, we have the choice between using the \ocaml{} function
implementing $tac$, or calling the tactic interpreter with the name
and arguments for interpreting $tac$. In the first case, a tactic call
will left the trace of the whole implementation of $tac$ in the proof
tree. In the second, the implementation of $tac$ will be hidden, and
only an invocation of $tac$ will be recalled (cf. the example of
Section \ref{ACompleteExample}.  The following combinators can be used
to hide the implementation of a tactic:

\begin{verbatim}
type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic)
val Tacmach.hide_atomic_tactic  : string -> tactic -> tactic
val Tacmach.hide_constr_tactic  : constr          hiding_combinator
val Tacmach.hide_constrl_tactic : (constr list)   hiding_combinator
val Tacmach.hide_numarg_tactic  : int             hiding_combinator
val Tacmach.hide_ident_tactic   : identifier      hiding_combinator
val Tacmach.hide_identl_tactic  : identifier      hiding_combinator
val Tacmach.hide_string_tactic  : string          hiding_combinator
val Tacmach.hide_bindl_tactic   : substitution    hiding_combinator
val Tacmach.hide_cbindl_tactic  : 
          (constr * substitution) hiding_combinator
\end{verbatim}

These functions first register the tactic by a side effect, and then
yield a function calling the interpreter with the registered name and
the right injection into the type of possible arguments.

\subsection{Tactics and Tacticals Provided by \Coq}

The fifth logical module is the library of tacticals and basic tactics
provided by \Coq. This library is distributed into the directories
\texttt{tactics} and \texttt{src/tactics}. The former contains those
basic tactics that make use of the types contained in the basic state
of \Coq. For example, inversion or rewriting tactics are in the
directory \texttt{tactics}, since they make use of the propositional
equality type.  Those tactics which are independent from the context
--like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in
the directory \texttt{src/tactics}. This latter directory also
contains some useful tools for programming new tactics, referred in 
Section \ref{SomeUsefulToolsforWrittingTactics}.

In practice, it is very unusual that the list of sub-goals and the
validation function of the tactic must be explicitly constructed by
the user. In most of the cases, the implementation of a new tactic
consists in supplying the appropriate arguments to the basic tactics
and tacticals.

\subsubsection{Basic Tactics}

The file \texttt{Tactics} contain the implementation of the basic
tactics provided by \Coq. The following tactics are some of the most
used ones:

\begin{verbatim}
val Tactics.intro           : tactic
val Tactics.assumption      : tactic
val Tactics.clear           : identifier list -> tactic
val Tactics.apply           : constr -> constr substitution -> tactic
val Tactics.one_constructor : int -> constr substitution -> tactic
val Tactics.simplest_elim   : constr -> tactic
val Tactics.elimType        : constr -> tactic
val Tactics.simplest_case   : constr -> tactic
val Tactics.caseType        : constr -> tactic
val Tactics.cut             : constr -> tactic
val Tactics.reduce          : redexpr -> tactic
val Tactics.exact           : constr -> tactic
val Auto.auto               : int option -> tactic
val Auto.trivial            : tactic
\end{verbatim}

The functions hiding the implementation of these tactics are defined
in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''.

\subsubsection[Tacticals]{Tacticals\label{OcamlTacticals}}

The following tacticals can be used to combine already existing
tactics:

\begin{description}
\fun{val Tacticals.tclIDTAC : tactic}
    {The identity tactic: it leaves the goal as it is.}

\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic}
    {Tries the first tactic and in case of failure applies the second one.}

\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic}
  {Applies the first tactic and then the second one to each generated subgoal.}

\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic}
    {Applies a tactic, and then applies each tactic of the tactic list to the
     corresponding generated subgoal.}

\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic}
    {Applies the first tactic, and then applies the second one to the last
     generated subgoal.}

\fun{val Tacticals.tclREPEAT : tactic -> tactic}
    {If the given tactic succeeds in producing a subgoal, then it
     is recursively applied to each generated subgoal, 
     and so on until it fails. }

\fun{val Tacticals.tclFIRST : tactic list -> tactic}
    {Tries the tactics of the given list one by one, until one of them
     succeeds.}

\fun{val Tacticals.tclTRY : tactic -> tactic}
    {Tries the given tactic and in case of failure applies the {\tt
    tclIDTAC} tactical to the original goal.}

\fun{val Tacticals.tclDO : int -> tactic -> tactic}
    {Applies the tactic a given number of times.}

\fun{val Tacticals.tclFAIL : tactic}
    {The always failing tactic: it raises a {\tt UserError} exception.}

\fun{val Tacticals.tclPROGRESS  : tactic -> tactic}
    {Applies the given tactic to the current goal and fails if the 
     tactic leaves the goal unchanged}

\fun{val Tacticals.tclNTH\_HYP :  int -> (constr -> tactic) -> tactic}
    {Applies a tactic to the nth hypothesis of the local context.
     The last hypothesis introduced correspond to the integer 1.}

\fun{val Tacticals.tclLAST\_HYP :  (constr -> tactic) -> tactic}
    {Applies a tactic to the last hypothesis introduced.}

\fun{val Tacticals.tclCOMPLETE : tactic -> tactic}
    {Applies a tactic and fails if the tactic did not solve completely the
      goal}

\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic}
    {Applied to the function \texttt{f} and the list \texttt{[x\_1;
        ... ; x\_n]}, this tactical applies the tactic
      \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}}
    
\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic}
    {If the condition holds, apply the first tactic; otherwise,
      apply the second one}

\end{description}


\subsection{The Vernacular Interpreter}

The sixth logical module of the implementation corresponds to the
interpreter of the vernacular phrases of \Coq. These phrases may be
expressions from the \gallina{} language (definitions), general
directives (setting commands) or tactics to be applied by the proof
engine. 

\subsection[The Parser and the Pretty-Printer]{The Parser and the Pretty-Printer\label{PrettyPrinter}}

The last logical module is the parser and pretty printer of \Coq,
which is the interface between the vernacular interpreter and the
user. They translate the chains of characters entered at the input
into abstract syntax trees, and vice versa. Abstract syntax trees are
represented by labeled n-ary trees, and its type is called
\texttt{CoqAst.t}.  For instance, the abstract syntax tree associated
to the term $[x:A]x$ is:

\begin{displaymath}
\texttt{Node}
 ((0,6), "LAMBDA",
  [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))])
\end{displaymath}

The numbers correspond to \textsl{locations}, used to point to some
input line and character positions in the error messages. As it was
already explained in Section \ref{TypeChecker}, this term is then
translated into a construction term in order to be typed.

The parser of \Coq\ is implemented using \camlpppp. The lexer and the data
used by \camlpppp\ to generate the parser lay in the directory
\texttt{src/parsing}.  This directory also contains \Coq's
pretty-printer. The printing rules lay in the directory
\texttt{src/syntax}.  The different entries of the grammar are
described in the module \texttt{Pcoq.Entry}.  Let us present here two
important functions of this logical module:

\begin{description}
\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a}
    {Parses a given string, trying to recognize a phrase
     corresponding to some entry in the grammar. If it succeeds,
     it yields a value associated to the grammar entry. For example,
     applied to the entry \texttt{Pcoq.Command.command}, this function
    parses a term of \Coq's language, and yields a value of type 
    \texttt{CoqAst.t}. When applied to the entry
    \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and
    returns the corresponding Ast.}
\fun{val gentermpr       : \\ \qquad 
path\_kind -> constr assumptions -> constr -> std\_ppcmds}
    {\\ Pretty-prints a well-typed term of certain kind (cf. Section
    \ref{SectionPaths}) under its context of typing assumption.}
\fun{val gentacpr        : CoqAst.t -> std\_ppcmds}
    {Pretty-prints a given abstract syntax tree representing a tactic
     expression.}
\end{description}

\subsection{The General Library}

In addition to the ones laying in the standard library of \ocaml{},
several useful modules about lists, arrays, sets, mappings, balanced
trees, and other frequently used data structures can be found in the
directory \texttt{lib}. Before writing a new one, check if it is not
already there!

\subsubsection{The module \texttt{Std}}
This module in the directory \texttt{src/lib/util} is opened by almost 
all modules of \Coq{}. Among other things, it contains a definition of 
the different kinds of errors used in \Coq{} :

\begin{description}
\fun{exception UserError of string * std\_ppcmds}
    {This is the class of ``users exceptions''. Such errors arise when 
      the user attempts to do something illegal, for example \texttt{Intro}
      when the current goal conclusion is not a product.}

\fun{val Std.error : string -> 'a}
    {For simple error messages}
\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
    {See Section~\ref{PrettyPrinter} : this can be used if the user
      want to display a term or build a complex error message}

\fun{exception Anomaly of string * std\_ppcmds}
    {This for reporting bugs or things that should not
      happen. The tacticals \texttt{tclTRY} and
      \texttt{tclTRY} described in Section~\ref{OcamlTacticals} catch the
      exceptions of type \texttt{UserError}, but they don't catch the
      anomalies. So, in your code, don't raise any anomaly, unless you
      know what you are doing. We also recommend to avoid constructs
      such as \texttt{try ... with \_ -> ...} : such constructs can trap 
      an anomaly and make the debugging process harder.}

\fun{val Std.anomaly : string -> 'a}{}
\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{}
\end{description}

\section{The tactic writer mini-HOWTO}

\subsection{How to add a vernacular command}

The command to register a vernacular command can be found
in module \texttt{Vernacinterp}:

\begin{verbatim}
val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;;
\end{verbatim}

The first argument is the name, the second argument is a function that
parses the arguments and returns a function of type
\texttt{unit}$\rightarrow$\texttt{unit} that do the job.

In this section we will show how to add a vernacular command
\texttt{CheckCheck} that print a type of a term and the type of its
type.

File \texttt{dcheck.ml}:

\begin{verbatim}
open Vernacinterp;;
open Trad;;
let _ = 
  vinterp_add 
   ("DblCheck",
    function [VARG_COMMAND com] ->
       (fun () -> 
          let evmap = Evd.mt_evd () 
          and sign = Termenv.initial_sign () in
           let {vAL=c;tYP=t;kIND=k} = 
                 fconstruct_with_univ evmap sign com in
             Pp.mSGNL [< Printer.prterm c; 'sTR ":"; 
                       Printer.prterm t; 'sTR ":"; 
                       Printer.prterm k >] )
      | _ -> bad_vernac_args "DblCheck")
;;
\end{verbatim}

Like for a new tactic, a new syntax entry must be created.

File \texttt{DCheck.v}:

\begin{verbatim}
Declare ML Module "dcheck.ml".

Grammar vernac vernac := 
  dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)].
\end{verbatim}

We are now able to test our new command:

\begin{verbatim}
Coq < Require DCheck.
Coq < CheckCheck O.
O:nat:Set
\end{verbatim}

Most Coq vernacular commands are registered in the module 
  \verb+src/env/vernacentries.ml+. One can see more examples here.

\subsection{How to keep a hashtable synchronous with the reset mechanism}

This is far more tricky. Some vernacular commands modify some
sort of state (for example by adding something in a hashtable). One
wants that \texttt{Reset} has the expected behavior with this
commands.

\Coq{} provides a general mechanism to do that. \Coq{} environments
contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for
constants of the calculus. OBJ is a dynamically extensible datatype
that contains sections, tactic definitions, hints for auto, and so
on. 

The simplest example of use of such a mechanism is in file
\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic
  Definition} command). Tactic macros are stored in the imperative
hashtable \texttt{mactab}. There are two functions freeze and unfreeze
to make a copy of the table and to restore the state of table from the
copy. Then this table is declared using \texttt{Library.declare\_summary}.

What does \Coq{} with that ? \Coq{} defines synchronization points.
At each synchronisation point, the declared tables are frozen (that
is, a copy of this tables is stored).

When \texttt{Reset }$i$ is called, \Coq{} goes back to the first
synchronisation point that is above $i$ and ``replays'' all objects
between that point 
and $i$. It will re-declare constants, re-open section, etc.

So we need to declare a new type of objects, TACTIC-MACRO-DATA. To
``replay'' on object of that type is to add the corresponding tactic
macro to \texttt{mactab}

So, now, we can say that \texttt{mactab} is synchronous with the Reset
mechanism$^{\mathrm{TM}}$.

Notice that this works for hash tables but also for a single integer
(the Undo stack size, modified by the \texttt{Set Undo} command, for
example).

\subsection{The right way to access to Coq constants from your ML code}

With their long names, Coq constants are stored using:

\begin{itemize}
\item a section path
\item an identifier
\end{itemize}

The identifier is exactly the identifier that is used in \Coq{} to
denote the constant; the section path can be known using the
\texttt{Locate} command:

\begin{coq_example}
  Locate S.
  Locate nat.
  Locate eq.
\end{coq_example}

Now it is easy to get a constant by its name and section path:


\begin{verbatim}
let constant sp id = 
  Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) 
    (Names.path_of_string sp) (Names.id_of_string id);;
\end{verbatim}


The only issue is that if one cannot put:


\begin{verbatim}
let coq_S = constant "#Datatypes#nat.cci" "S";;
\end{verbatim}


in his tactic's code. That is because this sentence is evaluated
\emph{before} the module \texttt{Datatypes} is loaded. The solution is
to use the lazy evaluation of \ocaml{}:


\begin{verbatim}
let coq_S = lazy (constant "#Datatypes#nat.cci" "S");;

... (Lazy.force coq_S) ...
\end{verbatim}


Be sure to call always Lazy.force behind a closure -- i.e. inside a
function body or behind the \texttt{lazy} keyword.

One can see examples of that technique in the source code of \Coq{},
for example 
\verb+plugins/omega/coq_omega.ml+.

\section[Some Useful Tools for Writing Tactics]{Some Useful Tools for Writing Tactics\label{SomeUsefulToolsforWrittingTactics}}
When the implementation of a tactic is not a straightforward
combination of tactics and tacticals, the module \texttt{Tacmach}
provides several useful functions for handling goals, calling the
type-checker, parsing terms, etc. This module is intended to be 
the interface of the proof engine for the user.

\begin{description}
\fun{val Tacmach.pf\_hyps               : goal sigma -> constr signature}
    {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} 
\fun{val pf\_concl              : goal sigma -> constr}
    {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.}
\fun{val Tacmach.pf\_nth\_hyp            : goal sigma -> int -> identifier *
    constr}
    {Projects the $ith$ typing constraint $x_i:A_i$ from the local
     context of the given goal.}
\fun{val Tacmach.pf\_fexecute           : goal sigma -> constr -> judgement}
    {Given a goal whose local context is $\Gamma$ and a term $a$, this
     function infers a type $A$ and a kind $K$ such that the judgement
     $a:A:K$ is valid under $\Gamma$, or raises an exception if there
     is no such judgement. A judgement is just a record type containing
     the three terms $a$, $A$ and $K$.}
\fun{val Tacmach.pf\_infexecute : \\
     \qquad
goal sigma -> constr -> judgement * information}
    {\\ In addition to the typing judgement, this function also extracts 
     the $F_{\omega}$ program underlying the term.}
\fun{val Tacmach.pf\_type\_of            : goal sigma -> constr -> constr}
    {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term
    $a$, where $\Gamma$ is the local typing context of the goal.}
\fun{val Tacmach.pf\_check\_type         : goal sigma -> constr -> constr -> bool}
    {This function yields a type $A$ if the two given terms $a$ and $A$  verify $\Gamma\vdash
     a:A$ in the local typing context $\Gamma$ of the goal. Otherwise,
    it raises an exception.}
\fun{val Tacmach.pf\_constr\_of\_com      : goal sigma -> CoqAst.t -> constr}
    {Transforms an abstract syntax tree into a well-typed term of the
    language of constructions. Raises an exception if the term cannot
    be typed.}
\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr}
    {Transforms an abstract syntax tree representing a type into
    a well-typed term of the language of constructions. Raises an
    exception if the term cannot be typed.}
\fun{val Tacmach.pf\_parse\_const        : goal sigma -> string -> constr}
    {Constructs the constant whose name is the given string.}
\fun{val
Tacmach.pf\_reduction\_of\_redexp  : \\
         \qquad goal sigma -> red\_expr -> constr -> constr}
    {\\ Applies a certain kind of reduction function, specified by an
     element of the type red\_expr.}
\fun{val Tacmach.pf\_conv\_x      : goal sigma -> constr -> constr -> bool}
    {Test whether  two given terms are definitionally equal.}
\end{description}

\subsection[Patterns]{Patterns\label{Patterns}}

The \ocaml{} file \texttt{Pattern} provides a quick way for describing a
term pattern and performing second-order, binding-preserving, matching
on it. Patterns are described using an extension of \Coq's concrete
syntax, where the second-order meta-variables of the pattern are
denoted by indexed question marks. 

Patterns may depend on constants, and therefore only to make have
sense when certain theories have been loaded. For this reason, they
are stored with a \textsl{module-marker}, telling us which modules
have to be open in order to use the pattern. The following functions
can be used to store and retrieve patterns form the pattern table:

\begin{description}
\fun{val Pattern.make\_module\_marker : string list -> module\_mark}
    {Constructs a module marker from a list of module names.}
\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term}
    {Constructs a pattern from a parseable string containing holes
     and a module marker.}
\fun{val Pattern.somatches    : constr ->   marked\_term-> bool}
    {Tests if a term matches a pattern.} 
\fun{val dest\_somatch : constr -> marked\_term -> constr list}
    {If the term matches the pattern, yields the list of sub-terms
     matching the occurrences of the pattern variables (ordered from
     left to right). Raises a \texttt{UserError} exception if the term
     does not match the pattern.} 
\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} 
    {Substitutes each hole in the pattern 
     by the corresponding term of the given the list.}
\end{description}

\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible
sub-terms that the matching functions are nevertheless sensible to.
For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for
the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$.
Hence, matching this term pattern 
with the term $(\texttt{true},\texttt{O})$ actually yields the list
$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not}
$[\texttt{true};\texttt{O}]$, as could be expected).

\subsection{Patterns on Inductive Definitions}

The module \texttt{Pattern} also includes some functions for testing
if the definition of an inductive type satisfies certain
properties. Such functions may be used to perform pattern matching
independently from the name given to the inductive type and the
universe it inhabits.  They yield the value $(\texttt{Some}\;r::l)$ if
the input term reduces into an application of an inductive type $r$ to
a list of terms $l$, and the definition of $r$ satisfies certain
conditions. Otherwise, they yield the value \texttt{None}.

\begin{description}
\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option}
    {Tests if the inductive type $r$ has no recursive constructors}
\fun{val Pattern.match\_with\_disjunction : constr list option}
    {Tests if the inductive type $r$ is a non-recursive type
     such that all its constructors have a single argument.}
\fun{val Pattern.match\_with\_conjunction : constr list option}
    {Tests if the inductive type $r$ is a non-recursive type
     with a unique constructor.}
\fun{val Pattern.match\_with\_empty\_type  : constr list option}
    {Tests if the inductive type $r$ has no constructors at all}
\fun{val Pattern.match\_with\_equation    : constr list option}
    {Tests if the inductive type $r$ has a single constructor
     expressing the property of reflexivity for some type. For
     example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy
     this predicate.}
\end{description}

\subsection{Elimination Tacticals}

It is frequently the case that the subgoals generated by an
elimination can all be solved in a similar way, possibly parametrized
on some information about each case, like for example:
\begin{itemize}
\item the inductive type of the object being eliminated;
\item its arguments (if it is an inductive predicate);
\item the branch number;
\item the predicate to be proven;
\item the number of assumptions to be introduced by the case
\item the signature of the branch, i.e., for each argument of
the branch whether it is recursive or not.
\end{itemize}

The following tacticals can be useful to deal with such situations.
They  

\begin{description}
\fun{val Elim.simple\_elimination\_then : \\ \qquad
(branch\_args -> tactic) -> constr -> tactic}
    {\\ Performs the default elimination on the last argument, and then
     tries to solve the generated subgoals using a given parametrized
     tactic. The type branch\_args is a record type containing all 
     information mentioned above.}
\fun{val Elim.simple\_case\_then : \\ \qquad
(branch\_args -> tactic) -> constr -> tactic}
    {\\ Similarly, but it performs case analysis instead of induction.}
\end{description}

\section[A Complete Example]{A Complete Example\label{ACompleteExample}}

In order to illustrate the implementation of a new tactic, let us come
back to the problem of deciding the equality of two elements of an
inductive type.

\subsection{Preliminaries}

Let us call \texttt{newtactic} the directory that will contain the
implementation of the new tactic. In this directory will lay two
files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that
implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing
its associated grammar rules and the commands to generate a module
that can be loaded dynamically from \Coq's toplevel. 

To compile our project, we will create a \texttt{Makefile} with the
command \texttt{do\_Makefile} (see Section~\ref{Makefile}) :

\begin{quotation}
  \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\
  \texttt{touch .depend}\\
  \texttt{make depend}
\end{quotation}

We must have kept the sources of \Coq{} somewhere and to set an
environment variable \texttt{COQTOP} that points to that directory.

\subsection{Implementing the Tactic}

The file \texttt{eqdecide.ml} contains the implementation of the
tactic in \ocaml{}. Let us recall the main steps of the proof strategy
for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the
inductive type $R$:
\begin{enumerate}
\item Eliminate $x$ and then $y$.
\item Try discrimination to solve those goals where $x$ and $y$ has
been introduced by different constructors.
\item If $x$ and $y$ have been introduced by the same constructor,
      then analyze one by one the corresponding pairs of arguments.
      If they are equal, rewrite one into the other. If they are
      not, derive a contradiction from the invectiveness of the
      constructor.
\item Once all the arguments have been rewritten, solve the left half
of the goal by reflexivity.
\end{enumerate}

In the sequel we implement these steps one by one. We start opening
the modules necessary for the implementation of the tactic:

\begin{verbatim}
open Names
open Term
open Tactics
open Tacticals
open Hiddentac
open Equality
open Auto
open Pattern
open Names
open Termenv
open Std
open Proof_trees
open Tacmach
\end{verbatim}

The first step of the procedure can be straightforwardly implemented as
follows:

\begin{verbatim}
let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));;
\end{verbatim}

\begin{verbatim}
let mkBranches = 
        (tclTHEN  intro 
        (tclTHEN (tclLAST_HYP h_simplest_elim)
        (tclTHEN  clear_last
        (tclTHEN  intros 
        (tclTHEN (tclLAST_HYP h_simplest_case)
        (tclTHEN  clear_last
                  intros))))));;
\end{verbatim}

Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to
give a (potentially clashing) name to the quantified variables of the
goal when they are introduced.

The second step of the procedure is implemented by the following
tactic:

\begin{verbatim}
let solveRightBranch  = (tclTHEN simplest_right discrConcl);;
\end{verbatim}

In order to illustrate how the implementation of a tactic can be 
hidden, let us do it with the tactic above:

\begin{verbatim}
let h_solveRightBranch =
    hide_atomic_tactic "solveRightBranch" solveRightBranch
;;
\end{verbatim}

As it was already mentioned in Section \ref{WhatIsATactic}, the
combinator \texttt{hide\_atomic\_tactic} first registers the tactic
\texttt{solveRightBranch} in the table, and returns a tactic which
calls the interpreter with the used to register it. Hence, when the
tactical \texttt{Info} is used, our tactic will just inform that
\texttt{solveRightBranch} was applied, omitting all the details
corresponding to \texttt{simplest\_right} and \texttt{discrConcl}.



The third step requires some auxiliary functions for constructing the
type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and
two constructions $c_1$ and $c_2$, and for generalizing this type over
$c_1$ and $c_2$:

\begin{verbatim}
let mmk         = make_module_marker ["#Logic.obj";"#Specif.obj"];;
let eqpat       = put_pat mmk "eq";;                 
let sumboolpat  = put_pat mmk "sumbool";;             
let notpat      = put_pat mmk "not";;   
let eq          = get_pat eqpat;;
let sumbool     = get_pat sumboolpat;;
let not         = get_pat notpat;;

let mkDecideEqGoal rectype c1 c2 g = 
     let equality    = mkAppL [eq;rectype;c1;c2] in
     let disequality = mkAppL [not;equality]
     in  mkAppL [sumbool;equality;disequality]
;;
let mkGenDecideEqGoal rectype g = 
      let hypnames = ids_of_sign (pf_hyps g) in 
      let xname    = next_ident_away (id_of_string "x") hypnames
      and yname    = next_ident_away (id_of_string "y") hypnames
      in  (mkNamedProd xname rectype 
           (mkNamedProd yname rectype 
            (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
;;
\end{verbatim}

The tactic will depend on the \Coq modules \texttt{Logic} and
\texttt{Specif}, since we use the constants corresponding to
propositional equality (\texttt{eq}), computational disjunction
(\texttt{sumbool}), and logical negation (\texttt{not}), defined in
that modules. This is specified creating the module maker
\texttt{mmk} (see Section~\ref{Patterns}).

The third step of the procedure can be divided into three sub-steps.
Assume that both $x$ and $y$ have been introduced by the same
constructor.  For each corresponding pair of arguments of that
constructor, we have to consider whether they are equal or not.  If
they are equal, the following tactic is applied to rewrite one into
the other:

\begin{verbatim}
let eqCase  tac = 
         (tclTHEN intro  
         (tclTHEN (tclLAST_HYP h_rewriteLR)
         (tclTHEN clear_last 
                  tac)))
;;
\end{verbatim}


If they are not equal, then the goal is contraposed and a
contradiction is reached form the invectiveness of the constructor:

\begin{verbatim}
let diseqCase = 
    let diseq  = (id_of_string "diseq") in
    let absurd = (id_of_string "absurd")
    in (tclTHEN (intro_using diseq)
       (tclTHEN  h_simplest_right
       (tclTHEN  red_in_concl
       (tclTHEN  (intro_using absurd)
       (tclTHEN  (h_simplest_apply (mkVar diseq))
       (tclTHEN  (h_injHyp absurd)
                  trivial ))))))
;;
\end{verbatim}

In the tactic above we have chosen to name the hypotheses because
they have to be applied later on. This introduces a potential risk
of name clashing if the context already contains other hypotheses 
also named ``diseq'' or ``absurd''.

We are now ready to implement the tactic \textsl{SolveArg}.  Given the
two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the
goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then
applies the tactics above to each of the generated cases. If the
disjunction cannot be solved automatically, it remains as a sub-goal
to be proven.

\begin{verbatim}
let solveArg a1 a2 tac  g = 
     let rectype = pf_type_of g a1 in
     let decide  = mkDecideEqGoal rectype a1 a2 g
     in  (tclTHENS  (h_elimType decide) 
                      [(eqCase tac);diseqCase;default_auto]) g
;;
\end{verbatim}

The following tactic implements the third and fourth steps of the
proof procedure:

\begin{verbatim}
let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}"
;;
let solveLeftBranch rectype g = 
      let (_::(lhs::(rhs::_))) = 
               try (dest_somatch (pf_concl g) conclpatt) 
               with UserError ("somatch",_)-> error "Unexpected conclusion!" in
      let nparams   = mind_nparams rectype   in
      let getargs l = snd (chop_list nparams (snd (decomp_app l))) in
      let rargs   = getargs rhs
      and largs   = getargs lhs
      in  List.fold_right2 
             solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
;;
\end{verbatim}

Notice the use of a pattern to decompose the goal and obtain the
inductive type and the left and right hand sides of the equality. A
certain number of arguments correspond to the general parameters of
the type, and must be skipped over. Once the corresponding list of
arguments \texttt{rargs} and \texttt{largs} have been obtained, the
tactic \texttt{solveArg} is iterated on them, leaving a disjunction
whose left half can be solved by reflexivity.

The following tactic joints together the three steps of the 
proof procedure:

\begin{verbatim}
let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"
;;
let decideGralEquality g = 
  let (typ::_) = try (dest_somatch (pf_concl g) initialpatt)
                 with UserError ("somatch",_) -> 
                        error "The goal does not have the expected form" in
  let headtyp = hd_app (pf_compute g typ) in
  let rectype = match (kind_of_term  headtyp) with
                 IsMutInd _ -> headtyp 
               | _          -> error ("This decision procedure only"
                                      " works for inductive objects") 
  in (tclTHEN   mkBranches 
     (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
;;
;;
\end{verbatim}

The tactic above can be specialized in two different ways: either to
decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the
universal quantification; or to eliminate this property and obtain two
subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$
respectively.

\begin{verbatim}
let decideGralEquality = 
  (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch))
;;
let decideEquality c1 c2 g = 
     let rectype = pf_type_of g c1 in
     let decide  = mkGenDecideEqGoal rectype g
     in  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
;;
let compare c1 c2 g = 
     let rectype = pf_type_of g c1 in
     let decide  = mkDecideEqGoal rectype c1 c2 g
     in  (tclTHENS (cut decide) 
                [(tclTHEN  intro 
                 (tclTHEN (tclLAST_HYP simplest_case)
                          clear_last));
                  decideEquality c1 c2]) g
;;
\end{verbatim}

Next, for each of the tactics that will have an entry in the grammar
we construct the associated dynamic one to be registered in the table
of tactics. This function can be used to overload a tactic name with
several similar tactics.  For example, the tactic proving the general
decidability property and the one proving a particular instance for
two terms can be grouped together with the following convention: if
the user provides two terms as arguments, then the specialized tactic
is used; if no argument is provided then the general tactic is invoked.

\begin{verbatim}
let dyn_decideEquality  args g =
      match args with 
       [(COMMAND com1);(COMMAND com2)]  -> 
          let c1 = pf_constr_of_com g com1
          and c2 = pf_constr_of_com g com2
          in  decideEquality c1 c2 g 
     | [] ->  decideGralEquality g
     | _  ->  error "Invalid arguments for dynamic tactic"
;;
add_tactic "DecideEquality" dyn_decideEquality
;;

let dyn_compare args g =
      match args with 
       [(COMMAND com1);(COMMAND com2)]  -> 
          let c1 = pf_constr_of_com g com1
          and c2 = pf_constr_of_com g com2
          in  compare c1 c2 g
     | _  ->  error "Invalid arguments for dynamic tactic"
;; 
add_tactic "Compare" tacargs_compare
;;
\end{verbatim}

This completes the implementation of the tactic. We turn now to the
\Coq file \texttt{Eqdecide.v}.


\subsection{The Grammar Rules}

Associated to the implementation of the tactic there is a \Coq\ file
containing the grammar and pretty-printing rules for the new tactic,
and the commands to generate an object module that can be then loaded
dynamically during a \Coq\ session. In order to generate an ML module,
the \Coq\ file must contain a
\texttt{Declare ML module} command for all the \ocaml{} files concerning
the implementation of the tactic --in our case there is only one file,
the file \texttt{eqdecide.ml}: 

\begin{verbatim}
Declare ML Module "eqdecide".
\end{verbatim}

The following grammar and pretty-printing rules are
self-explanatory. We refer the reader to the Section \ref{Grammar} for
the details:

\begin{verbatim}
Grammar tactic simple_tactic :=
  EqDecideRuleG1 
       [ "Decide"  "Equality" comarg($com1)  comarg($com2)] -> 
       [(DecideEquality $com1 $com2)]
| EqDecideRuleG2 
       [ "Decide" "Equality"  ] -> 
       [(DecideEquality)]
| CompareRule 
       [ "Compare" comarg($com1) comarg($com2)] -> 
       [(Compare $com1 $com2)].

Syntax tactic level 0:
  EqDecideRulePP1 
       [(DecideEquality)]   -> 
       ["Decide" "Equality"]
| EqDecideRulePP2 
       [(DecideEquality $com1 $com2)]   -> 
       ["Decide" "Equality" $com1 $com2]
| ComparePP 
       [(Compare $com1 $com2)] -> 
       ["Compare" $com1 $com2].
\end{verbatim}


\paragraph{Important:} The names used to label the abstract syntax tree 
in the grammar rules ---in this case ``DecideEquality'' and
``Compare''--- must be the same as the name used to register the
tactic in the tactics table. This is what makes the links between the
input entered by the user and the tactic executed by the interpreter.

\subsection{Loading the Tactic}

Once the module \texttt{EqDecide.v} has been compiled, the tactic can
be dynamically loaded using the \texttt{Require} command. 

\begin{coq_example}
Require EqDecide.
Goal (x,y:nat){x=y}+{~x=y}.
Decide Equality.
\end{coq_example}

The implementation of the tactic can be accessed through the
tactical \texttt{Info}:
\begin{coq_example}
Undo.
Info Decide Equality.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}

Remark that the task performed by the tactic \texttt{solveRightBranch}
is not displayed, since we have chosen to hide its implementation.

\section[Testing and Debugging your Tactic]{Testing and Debugging your Tactic\label{test-and-debug}}

When your tactic does not behave as expected, it is possible to trace
it dynamically from \Coq. In order to do this, you have first to leave
the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can
be done using the command \texttt{Drop} (see Section~\ref{Drop}). Once
in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}.
This file installs several pretty printers for proof trees, goals,
terms, abstract syntax trees, names, etc.  It also contains the
function \texttt{go:unit -> unit} that enables to go back to \Coq's
toplevel. 

The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic
functions for extracting information from the state of the proof
engine. Such functions can be used to debug your tactic if
necessary. Let us mention here some of them:

\begin{description}
\fun{val get\_pftreestate         : unit -> pftreestate}
    {Projects the current state of the proof engine.}
\fun{val proof\_of\_pftreestate    : pftreestate -> proof}
    {Projects the current state of the proof tree. A pretty-printer 
      displays it in a readable form.  }
\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma}
    {Projects the goal and the existential variables mapping from
     the current state of the proof engine.} 
\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma}
    {Projects the goal and mapping corresponding to the $nth$ subgoal
     that remains to be proven}
\fun{val traverse                : int -> pftreestate -> pftreestate}
    {Yields the children of the node that the current state of the 
     proof engine points to.}
\fun{val solve\_nth\_pftreestate   : \\ \qquad
int -> tactic -> pftreestate ->  pftreestate}
     {\\ Provides the new state of the proof engine obtained applying 
      a given tactic to some unproven sub-goal.}
\end{description}

Finally, the traditional \ocaml{} debugging tools like the directives
\texttt{trace} and \texttt{untrace} can be used to follow the
execution of your functions. Frequently, a better solution is to use
the \ocaml{} debugger, see Chapter \ref{Utilities}.

\section[Concrete syntax for ML tactic and vernacular command]{Concrete syntax for ML tactic and vernacular command\label{Notations-for-ML-command}}

\subsection{The general case}

The standard way to bind an ML-written tactic or vernacular command to
a concrete {\Coq} syntax is to use the
\verb=TACTIC EXTEND= and \verb=VERNAC COMMAND EXTEND= macros.

These macros can be used in any {\ocaml} file defining a (new) ML tactic
or vernacular command. They are expanded into pure {\ocaml} code by
the {\camlpppp} preprocessor of {\ocaml}. Concretely, files that use
these macros need to be compiled by giving to {\tt ocamlc} the option 

\verb=-pp "camlp4o -I $(COQTOP)/parsing grammar.cma pa_extend.cmo"=

\noindent which is the default for every file compiled by means of a Makefile
generated by {\tt coq\_makefile} (see Chapter~\ref{Addoc-coqc}). So,
just do \verb=make= in this latter case.

The syntax of the macros is given on figure
\ref{EXTEND-syntax}. They can be used at any place of an {\ocaml}
files where an ML sentence (called \verb=str_item= in the {\tt ocamlc}
parser) is expected. For each rule, the left-hand-side describes the
grammar production and the right-hand-side its interpretation which
must be an {\ocaml} expression. Each grammar production starts with
the concrete name of the tactic or command in {\Coq} and is followed
by arguments, possibly separated by terminal symbols or words.
Here is an example:

\begin{verbatim}
TACTIC EXTEND Replace
  [ "replace" constr(c1) "with" constr(c2) ] -> [ replace c1 c2 ]
END
\end{verbatim}

\newcommand{\grule}{\textrm{\textsl{rule}}}
\newcommand{\stritem}{\textrm{\textsl{ocaml\_str\_item}}}
\newcommand{\camlexpr}{\textrm{\textsl{ocaml\_expr}}}
\newcommand{\arginfo}{\textrm{\textsl{argument\_infos}}}
\newcommand{\lident}{\textrm{\textsl{lower\_ident}}}
\newcommand{\argument}{\textrm{\textsl{argument}}}
\newcommand{\entry}{\textrm{\textsl{entry}}}
\newcommand{\argtype}{\textrm{\textsl{argtype}}}

\begin{figure}
\begin{tabular}{|lcll|}
\hline
{\stritem}
 & ::= & 
\multicolumn{2}{l|}{{\tt TACTIC EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
 & $|$ & \multicolumn{2}{l|}{{\tt VERNAC COMMAND EXTEND} {\ident} \nelist{\grule}{$|$} {\tt END}}\\
&&\multicolumn{2}{l|}{}\\
{\grule} & ::= & 
\multicolumn{2}{l|}{{\tt [} {\str} \sequence{\argument}{} {\tt ] -> [} {\camlexpr} {\tt ]}}\\
&&\multicolumn{2}{l|}{}\\
{\argument} & ::= & {\str} &\mbox{(terminal)}\\
 & $|$ & {\entry} {\tt (} {\lident} {\tt )} &\mbox{(non-terminal)}\\
&&\multicolumn{2}{l|}{}\\
{\entry} 
 & ::= & {\tt string} & (a string)\\
 & $|$ & {\tt preident} & (an identifier typed as a {\tt string})\\
 & $|$ & {\tt ident} & (an identifier of type {\tt identifier})\\
 & $|$ & {\tt global} & (a qualified identifier)\\
 & $|$ & {\tt constr} & (a {\Coq} term)\\
 & $|$ & {\tt openconstr} & (a {\Coq} term with holes)\\
 & $|$ & {\tt sort} & (a {\Coq} sort)\\
 & $|$ & {\tt tactic} & (an ${\cal L}_{tac}$ expression)\\
 & $|$ & {\tt constr\_with\_bindings} & (a {\Coq} term with a list of bindings\footnote{as for the tactics {\tt apply} and {\tt elim}})\\
 & $|$ & {\tt int\_or\_var} & (an integer or an identifier denoting an integer)\\
 & $|$ & {\tt quantified\_hypothesis} & (a quantified hypothesis\footnote{as for the tactics {\tt intros until}})\\
 & $|$ & {\tt {\entry}\_opt} & (an optional {\entry} )\\
 & $|$ & {\tt ne\_{\entry}\_list} & (a non empty list of {\entry})\\
 & $|$ & {\tt {\entry}\_list} & (a list of {\entry})\\
 & $|$ & {\tt bool} & (a boolean: no grammar rule, just for typing)\\
 & $|$ & {\lident} & (a user-defined entry)\\
\hline
\end{tabular}
\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
\label{EXTEND-syntax}
\end{figure}

There is a set of predefined non-terminal entries which are
automatically translated into an {\ocaml} object of a given type. The
type is not the same for tactics and for vernacular commands. It is
given in the following table:

\begin{small}
\noindent \begin{tabular}{|l|l|l|}
\hline
{\entry} & {\it type for tactics} & {\it type for commands} \\
{\tt string} & {\tt string} & {\tt string}\\
{\tt preident} & {\tt string} & {\tt string}\\
{\tt ident} & {\tt identifier} & {\tt identifier}\\
{\tt global} & {\tt global\_reference} & {\tt qualid}\\
{\tt constr} & {\tt constr} & {\tt constr\_expr}\\
{\tt openconstr} & {\tt open\_constr} & {\tt constr\_expr}\\
{\tt sort} & {\tt sorts} & {\tt rawsort}\\
{\tt tactic} & {\tt glob\_tactic\_expr * tactic} & {\tt raw\_tactic\_expr}\\
{\tt constr\_with\_bindings} & {\tt constr with\_bindings} & {\tt constr\_expr with\_bindings}\\\\
{\tt int\_or\_var} & {\tt int or\_var} & {\tt int or\_var}\\
{\tt quantified\_hypothesis} & {\tt quantified\_hypothesis} & {\tt quantified\_hypothesis}\\
{\tt {\entry}\_opt} & {\it the type of entry} {\tt option} & {\it the type of entry} {\tt option}\\
{\tt ne\_{\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
{\tt {\entry}\_list} & {\it the type of entry} {\tt list} & {\it the type of entry} {\tt list}\\
{\tt bool} & {\tt bool} & {\tt bool}\\
{\lident} & {user-provided, cf next section} & {user-provided, cf next section}\\
\hline
\end{tabular}
\end{small}

\bigskip

Notice that {\entry} consists in a single identifier and that the {\tt
\_opt}, {\tt \_list}, ... modifiers are part of the identifier.
Here is now another example of a tactic which takes either a non empty
list of identifiers and executes the {\ocaml} function {\tt subst} or
takes no arguments and executes the{\ocaml} function {\tt subst\_all}.

\begin{verbatim}
TACTIC EXTEND Subst
| [ "subst" ne_ident_list(l) ] -> [ subst l ]
| [ "subst" ] -> [ subst_all ]
END
\end{verbatim}

\subsection{Adding grammar entries for tactic or command arguments}

In case parsing the arguments of the tactic or the vernacular command
involves grammar entries other than the predefined entries listed
above, you have to declare a new entry using the macros
\verb=ARGUMENT EXTEND= or \verb=VERNAC ARGUMENT EXTEND=. The syntax is
given on Figure~\ref{ARGUMENT-EXTEND-syntax}. Notice that arguments
declared by \verb=ARGUMENT EXTEND= can be used for arguments of both
tactics and vernacular commands while arguments declared by
\verb=VERNAC ARGUMENT EXTEND= can only be used by vernacular commands.

For \verb=VERNAC ARGUMENT EXTEND=, the identifier is the name of the
entry and it must be a valid {\ocaml} identifier (especially it must
be lowercase).  The grammar rules works as before except that they do
not have to start by a terminal symbol or word.  As an example, here
is how the {\Coq} {\tt Extraction Language {\it language}} parses its
argument:

\begin{verbatim}
VERNAC ARGUMENT EXTEND language
| [ "Ocaml" ] -> [ Ocaml ]
| [ "Haskell" ] -> [ Haskell ]
| [ "Scheme" ] -> [ Scheme ]
END
\end{verbatim}

For tactic arguments, and especially for \verb=ARGUMENT EXTEND=, the
procedure is more subtle because tactics are objects of the {\Coq}
environment which can be printed and interpreted. Then the syntax
requires extra information providing a printer and a type telling how
the argument behaves. Here is an example of entry parsing a pair of
optional {\Coq} terms.

\begin{verbatim}
let pp_minus_div_arg pr_constr pr_tactic (omin,odiv) = 
  if omin=None && odiv=None then mt() else
    spc() ++ str "with" ++
    pr_opt (fun c -> str "minus := " ++ pr_constr c) omin ++
    pr_opt (fun c -> str "div := " ++ pr_constr c) odiv

ARGUMENT EXTEND minus_div_arg 
  TYPED AS constr_opt * constr_opt
  PRINTED BY pp_minus_div_arg
| [ "with" minusarg(m) divarg_opt(d) ] -> [ Some m, d ]
| [ "with" divarg(d) minusarg_opt(m) ] -> [ m, Some d ]
| [ ] -> [ None, None ]
END
\end{verbatim}

Notice that the type {\tt constr\_opt * constr\_opt} tells that the
object behaves as a pair of optional {\Coq} terms, i.e. as an object
of {\ocaml} type {\tt constr option * constr option} if in a
\verb=TACTIC EXTEND= macro and of type {\tt constr\_expr option *
constr\_expr option} if in a \verb=VERNAC COMMAND EXTEND= macro.

As for the printer, it must be a function expecting a printer for
terms, a printer for tactics and returning a printer for the created
argument. Especially, each sub-{\term} and each sub-{\tac} in the
argument must be typed by the corresponding printers. Otherwise, the
{\ocaml} code will not be well-typed.

\Rem The entry {\tt bool} is bound to no syntax but it can be used to
give the type of an argument as in the following example:

\begin{verbatim}
let pr_orient _prc _prt = function
  | true -> mt ()
  | false -> str " <-"

ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
| [ "->" ] -> [ true ]
| [ "<-" ] -> [ false ]
| [ ] -> [ true ]
END
\end{verbatim}

\begin{figure}
\begin{tabular}{|lcl|}
\hline
{\stritem} & ::= & 
 {\tt ARGUMENT EXTEND} {\ident} {\arginfo} {\nelist{\grule}{$|$}} {\tt END}\\
& $|$ & {\tt VERNAC ARGUMENT EXTEND} {\ident} {\nelist{\grule}{$|$}} {\tt END}\\
\\
{\arginfo} & ::= & {\tt TYPED AS} {\argtype} \\
&& {\tt PRINTED BY} {\lident} \\
%&& \zeroone{{\tt INTERPRETED BY} {\lident}}\\
%&& \zeroone{{\tt GLOBALIZED BY} {\lident}}\\
%&& \zeroone{{\tt SUBSTITUTED BY} {\lident}}\\
%&& \zeroone{{\tt RAW\_TYPED AS} {\lident} {\tt RAW\_PRINTED BY} {\lident}}\\
%&& \zeroone{{\tt GLOB\_TYPED AS} {\lident} {\tt GLOB\_PRINTED BY} {\lident}}\\
\\
{\argtype} & ::= & {\argtype} {\tt *} {\argtype} \\ 
& $|$ & {\entry} \\
\hline
\end{tabular}
\caption{Syntax of the macros binding {\ocaml} tactics or commands to a {\Coq} syntax}
\label{ARGUMENT-EXTEND-syntax}
\end{figure}

%\end{document}