1
\chapter[The tactic language]{The tactic language\label{TacticLanguage}}
3
%\geometry{a4paper,body={5in,8in}}
5
This chapter gives a compact documentation of Ltac, the tactic
6
language available in {\Coq}. We start by giving the syntax, and next,
7
we present the informal semantics. If you want to know more regarding
8
this language and especially about its foundations, you can refer
9
to~\cite{Del00}. Chapter~\ref{Tactics-examples} is devoted to giving
10
examples of use of this language on small but also with non-trivial
16
\def\tacexpr{\textrm{\textsl{expr}}}
17
\def\tacexprlow{\textrm{\textsl{tacexpr$_1$}}}
18
\def\tacexprinf{\textrm{\textsl{tacexpr$_2$}}}
19
\def\tacexprpref{\textrm{\textsl{tacexpr$_3$}}}
20
\def\atom{\textrm{\textsl{atom}}}
21
%%\def\recclause{\textrm{\textsl{rec\_clause}}}
22
\def\letclause{\textrm{\textsl{let\_clause}}}
23
\def\matchrule{\textrm{\textsl{match\_rule}}}
24
\def\contextrule{\textrm{\textsl{context\_rule}}}
25
\def\contexthyps{\textrm{\textsl{context\_hyps}}}
26
\def\tacarg{\nterm{tacarg}}
27
\def\cpattern{\nterm{cpattern}}
29
The syntax of the tactic language is given Figures~\ref{ltac}
30
and~\ref{ltac_aux}. See Chapter~\ref{BNF-syntax} for a description of
31
the BNF metasyntax used in these grammar rules. Various already
32
defined entries will be used in this chapter: entries
33
{\naturalnumber}, {\integer}, {\ident}, {\qualid}, {\term},
34
{\cpattern} and {\atomictac} represent respectively the natural and
35
integer numbers, the authorized identificators and qualified names,
36
{\Coq}'s terms and patterns and all the atomic tactics described in
37
Chapter~\ref{Tactics}. The syntax of {\cpattern} is the same as that
38
of terms, but it is extended with pattern matching metavariables. In
39
{\cpattern}, a pattern-matching metavariable is represented with the
40
syntax {\tt ?id} where {\tt id} is an {\ident}. The notation {\tt \_}
41
can also be used to denote metavariable whose instance is
42
irrelevant. In the notation {\tt ?id}, the identifier allows us to
43
keep instantiations and to make constraints whereas {\tt \_} shows
44
that we are not interested in what will be matched. On the right hand
45
side of pattern-matching clauses, the named metavariable are used
46
without the question mark prefix. There is also a special notation for
47
second-order pattern-matching problems: in an applicative pattern of
48
the form {\tt @?id id$_1$ \ldots id$_n$}, the variable {\tt id}
49
matches any complex expression with (possible) dependencies in the
50
variables {\tt id$_1$ \ldots id$_n$} and returns a functional term of
51
the form {\tt fun id$_1$ \ldots id$_n$ => {\term}}.
54
The main entry of the grammar is {\tacexpr}. This language is used in
55
proof mode but it can also be used in toplevel definitions as shown in
59
\item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt
60
;} \dots'' are associative.
62
\item In {\tacarg}, there is an overlap between {\qualid} as a
63
direct tactic argument and {\qualid} as a particular case of
64
{\term}. The resolution is done by first looking for a reference of
65
the tactic language and if it fails, for a reference to a term. To
66
force the resolution as a reference of the tactic language, use the
67
form {\tt ltac :} {\qualid}. To force the resolution as a reference to
68
a term, use the syntax {\tt ({\qualid})}.
70
\item As shown by the figure, tactical {\tt ||} binds more than the
71
prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and
72
{\tt abstract} which themselves bind more than the postfix tactical
73
``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;}
78
{\tt try repeat \tac$_1$ ||
79
\tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.}
83
{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\
84
{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).}
93
{\tacexpr} {\tt ;} {\tacexpr}\\
94
& | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
95
& | & {\tacexprpref}\\
97
{\tacexprpref} & ::= &
98
{\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
99
& | & {\tt info} {\tacexprpref}\\
100
& | & {\tt progress} {\tacexprpref}\\
101
& | & {\tt repeat} {\tacexprpref}\\
102
& | & {\tt try} {\tacexprpref}\\
103
& | & {\tacexprinf} \\
105
{\tacexprinf} & ::= &
106
{\tacexprlow} {\tt ||} {\tacexprpref}\\
107
& | & {\tacexprlow}\\
109
{\tacexprlow} & ::= &
110
{\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\
112
{\tt let} \zeroone{\tt rec} \nelist{\letclause}{\tt with} {\tt in}
115
{\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
117
{\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
119
{\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
121
{\tt lazymatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
123
{\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\
125
{\tt lazymatch} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\
126
& | & {\tt abstract} {\atom}\\
127
& | & {\tt abstract} {\atom} {\tt using} {\ident} \\
128
& | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
129
& | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
130
& | & {\tt idtac} \sequence{\messagetoken}{}\\
131
& | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\
132
& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\
133
& | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\
134
& | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\
135
& | & {\tt type of} {\term}\\
136
& | & {\tt external} {\qstring} {\qstring} \nelist{\tacarg}{}\\
137
& | & {\tt constr :} {\term}\\
139
& | & {\qualid} \nelist{\tacarg}{}\\
146
& | & {\tt (} {\tacexpr} {\tt )}\\
148
{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\term} ~|~ {\integer} \\
151
\caption{Syntax of the tactic language}
163
& $|$ & {\tt ltac :} {\atom}\\
166
\letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\
169
\nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\
170
& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\
171
& $|$ & {\tt \_ =>} {\tacexpr}\\
173
\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\
176
{\cpattern} {\tt =>} {\tacexpr}\\
177
& $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\
178
& $|$ & {\tt \_ =>} {\tacexpr}\\
181
\caption{Syntax of the tactic language (continued)}
188
\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\
190
\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=}
192
& $|$ &{\qualid} \sequence{\ident}{} {\tt ::=}{\tacexpr}
195
\caption{Tactic toplevel definitions}
204
%\index[tactic]{Tacticals}
208
Tactic expressions can only be applied in the context of a goal. The
209
evaluation yields either a term, an integer or a tactic. Intermediary
210
results can be terms or integers but the final result must be a tactic
211
which is then applied to the current goal.
213
There is a special case for {\tt match goal} expressions of which
214
the clauses evaluate to tactics. Such expressions can only be used as
215
end result of a tactic expression (never as argument of a non recursive local
216
definition or of an application).
218
The rest of this section explains the semantics of every construction
222
%% \subsection{Values}
224
%% Values are given by Figure~\ref{ltacval}. All these values are tactic values,
225
%% i.e. to be applied to a goal, except {\tt Fun}, {\tt Rec} and $arg$ values.
227
%% \begin{figure}[ht]
228
%% \noindent{}\framebox[6in][l]
231
%% \begin{tabular}{lp{0.1in}l}
232
%% $vexpr$ & ::= & $vexpr$ {\tt ;} $vexpr$\\
233
%% & | & $vexpr$ {\tt ; [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt
237
%% $vatom$ & ::= & {\tt Fun} \nelist{\inputfun}{} {\tt ->} {\tacexpr}\\
238
%% %& | & {\tt Rec} \recclause\\
240
%% {\tt Rec} \nelist{\recclause}{\tt And} {\tt In}
243
%% {\tt Match Context With} {\it (}$context\_rule$ {\tt |}{\it )}$^*$
245
%% & | & {\tt (} $vexpr$ {\tt )}\\
246
%% & | & $vatom$ {\tt Orelse} $vatom$\\
247
%% & | & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} $vatom$\\
248
%% & | & {\tt Repeat} $vatom$\\
249
%% & | & {\tt Try} $vatom$\\
250
%% & | & {\tt First [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
251
%% & | & {\tt Solve [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
252
%% & | & {\tt Idtac}\\
253
%% & | & {\tt Fail}\\
254
%% & | & {\primitivetactic}\\
258
%% \caption{Values of ${\cal L}_{tac}$}
262
%% \subsection{Evaluation}
264
\subsubsection[Sequence]{Sequence\tacindex{;}
265
\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}}}
267
A sequence is an expression of the following form:
269
{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$
271
{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
272
$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied
273
and $v_2$ is applied to every subgoal generated by the application of
274
$v_1$. Sequence is left-associative.
276
\subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}}
278
%\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}}
279
\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}}
281
We can generalize the previous sequence operator as
283
{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |}
284
{\tacexpr}$_n$ {\tt ]}
286
{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is
287
applied and $v_i$ is applied to the $i$-th generated subgoal by the
288
application of $v_0$, for $=1,...,n$. It fails if the application of
289
$v_0$ does not generate exactly $n$ subgoals.
291
\variant If no tactic is given for the $i$-th generated subgoal, it
292
behaves as if the tactic {\tt idtac} were given. For instance, {\tt
293
split ; [ | auto ]} is a shortcut for
294
{\tt split ; [ idtac | auto ]}.
297
\subsubsection[For loop]{For loop\tacindex{do}
298
\index{Tacticals!do@{\tt do}}}
300
There is a for loop that repeats a tactic {\num} times:
302
{\tt do} {\num} {\tacexpr}
304
{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
305
applied {\num} times. Supposing ${\num}>1$, after the first
306
application of $v$, $v$ is applied, at least once, to the generated
307
subgoals and so on. It fails if the application of $v$ fails before
308
the {\num} applications have been completed.
310
\subsubsection[Repeat loop]{Repeat loop\tacindex{repeat}
311
\index{Tacticals!repeat@{\tt repeat}}}
313
We have a repeat loop with:
315
{\tt repeat} {\tacexpr}
317
{\tacexpr} is evaluated to $v$. If $v$ denotes a tactic, this tactic
318
is applied to the goal. If the application fails, the tactic is
319
applied recursively to all the generated subgoals until it eventually
320
fails. The recursion stops in a subgoal when the tactic has failed.
321
The tactic {\tt repeat {\tacexpr}} itself never fails.
323
\subsubsection[Error catching]{Error catching\tacindex{try}
324
\index{Tacticals!try@{\tt try}}}
326
We can catch the tactic errors with:
330
{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
331
applied. If the application of $v$ fails, it catches the error and
332
leaves the goal unchanged. If the level of the exception is positive,
333
then the exception is re-raised with its level decremented.
335
\subsubsection[Detecting progress]{Detecting progress\tacindex{progress}}
337
We can check if a tactic made progress with:
339
{\tt progress} {\tacexpr}
341
{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is
342
applied. If the application of $v$ produced one subgoal equal to the
343
initial goal (up to syntactical equality), then an error of level 0 is
346
\ErrMsg \errindex{Failed to progress}
348
\subsubsection[Branching]{Branching\tacindex{$\mid\mid$}
349
\index{Tacticals!orelse@{\tt $\mid\mid$}}}
351
We can easily branch with the following structure:
353
{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$
355
{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and
356
$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if
357
it fails to progress then $v_2$ is applied. Branching is left-associative.
359
\subsubsection[First tactic to work]{First tactic to work\tacindex{first}
360
\index{Tacticals!first@{\tt first}}}
362
We may consider the first tactic to work (i.e. which does not fail) among a
365
{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
367
{\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for
368
$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it
369
tries to apply $v_2$ and so on. It fails when there is no applicable tactic.
371
\ErrMsg \errindex{No applicable tactic}
373
\subsubsection[Solving]{Solving\tacindex{solve}
374
\index{Tacticals!solve@{\tt solve}}}
376
We may consider the first to solve (i.e. which generates no subgoal) among a
379
{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}
381
{\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for
382
$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it
383
tries to apply $v_2$ and so on. It fails if there is no solving tactic.
385
\ErrMsg \errindex{Cannot solve the goal}
387
\subsubsection[Identity]{Identity\tacindex{idtac}
388
\index{Tacticals!idtac@{\tt idtac}}}
390
The constant {\tt idtac} is the identity tactic: it leaves any goal
391
unchanged but it appears in the proof script.
393
\variant {\tt idtac \nelist{\messagetoken}{}}
395
This prints the given tokens. Strings and integers are printed
396
literally. If a term is given, it is printed, its variables being
397
interpreted in the current environment. In particular, if a variable
398
is given, its value is printed.
401
\subsubsection[Failing]{Failing\tacindex{fail}
402
\index{Tacticals!fail@{\tt fail}}}
404
The tactic {\tt fail} is the always-failing tactic: it does not solve
405
any goal. It is useful for defining other tacticals since it can be
406
catched by {\tt try} or {\tt match goal}.
409
\item {\tt fail $n$}\\
410
The number $n$ is the failure level. If no level is specified, it
411
defaults to $0$. The level is used by {\tt try} and {\tt match goal}.
412
If $0$, it makes {\tt match goal} considering the next clause
413
(backtracking). If non zero, the current {\tt match goal} block or
414
{\tt try} command is aborted and the level is decremented.
416
\item {\tt fail \nelist{\messagetoken}{}}\\
417
The given tokens are used for printing the failure message.
419
\item {\tt fail $n$ \nelist{\messagetoken}{}}\\
420
This is a combination of the previous variants.
423
\ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}.
425
\subsubsection[Local definitions]{Local definitions\index{Ltac!let}
428
\index{let rec!in Ltac}}
430
Local definitions can be done as follows:
432
{\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\
433
{\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\
435
{\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\
438
each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is
439
evaluated by substituting $v_i$ to each occurrence of {\ident}$_i$,
440
for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$
441
and the {\ident}$_i$.
443
Local definitions can be recursive by using {\tt let rec} instead of
444
{\tt let}. In this latter case, the definitions are evaluated lazily
445
so that the {\tt rec} keyword can be used also in non recursive cases
446
so as to avoid the eager evaluation of local definitions.
448
\subsubsection{Application}
450
An application is an expression of the following form:
452
{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$
454
The reference {\qualid} must be bound to some defined tactic
455
definition expecting at least $n$ arguments. The expressions
456
{\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$.
457
%If {\tacexpr} is a {\tt Fun} or {\tt Rec} value then the body is evaluated by
458
%substituting $v_i$ to the formal parameters, for $i=1,...,n$. For recursive
459
%clauses, the bodies are lazily substituted (when an identifier to be evaluated
460
%is the name of a recursive clause).
462
%\subsection{Application of tactic values}
464
\subsubsection[Function construction]{Function construction\index{fun!in Ltac}
467
A parameterized tactic can be built anonymously (without resorting to
468
local definitions) with:
470
{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr}
472
Indeed, local definitions of functions are a syntactic sugar for
473
binding a {\tt fun} tactic to an identifier.
475
\subsubsection[Pattern matching on terms]{Pattern matching on terms\index{Ltac!match}
476
\index{match!in Ltac}}
478
We can carry out pattern matching on terms with:
480
{\tt match} {\tacexpr} {\tt with}\\
481
~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\
482
~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\
484
~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\
485
~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\
488
The expression {\tacexpr} is evaluated and should yield a term which
489
is matched against {\cpattern}$_1$. The matching is non-linear: if a
490
metavariable occurs more than once, it should match the same
491
expression every time. It is first-order except on the
492
variables of the form {\tt @?id} that occur in head position of an
493
application. For these variables, the matching is second-order and
494
returns a functional term.
496
If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is
497
evaluated into some value by substituting the pattern matching
498
instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a
499
tactic and the {\tt match} expression is in position to be applied to
500
a goal (e.g. it is not bound to a variable by a {\tt let in}), then
501
this tactic is applied. If the tactic succeeds, the list of resulting
502
subgoals is the result of the {\tt match} expression. If
503
{\tacexpr}$_1$ does not evaluate to a tactic or if the {\tt match}
504
expression is not in position to be applied to a goal, then the result
505
of the evaluation of {\tacexpr}$_1$ is the result of the {\tt match}
508
If the matching with {\cpattern}$_1$ fails, or if it succeeds but the
509
evaluation of {\tacexpr}$_1$ fails, or if the evaluation of
510
{\tacexpr}$_1$ succeeds but returns a tactic in execution position
511
whose execution fails, then {\cpattern}$_2$ is used and so on. The
512
pattern {\_} matches any term and shunts all remaining patterns if
513
any. If all clauses fail (in particular, there is no pattern {\_})
514
then a no-matching-clause error is raised.
518
\item \errindex{No matching clauses for match}
520
No pattern can be used and, in particular, there is no {\tt \_} pattern.
522
\item \errindex{Argument of match does not evaluate to a term}
524
This happens when {\tacexpr} does not denote a term.
529
\item \index{context!in pattern}
530
There is a special form of patterns to match a subterm against the
533
{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]}
535
It matches any term which one subterm matches {\cpattern}. If there is
536
a match, the optional {\ident} is assign the ``matched context'', that
537
is the initial term where the matched subterm is replaced by a
538
hole. The definition of {\tt context} in expressions below will show
539
how to use such term contexts.
541
If the evaluation of the right-hand-side of a valid match fails, the
542
next matching subterm is tried. If no further subterm matches, the
543
next clause is tried. Matching subterms are considered top-bottom and
544
from left to right (with respect to the raw printing obtained by
545
setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}).
551
idtac X; (* To display the evaluation order *)
552
assert (p := refl_equal 1 : X=1); (* To filter the case X=1 *)
553
let x:= context f[O] in assert (x=O) (* To observe the context *)
559
\item \index{lazymatch!in Ltac}
560
\index{Ltac!lazymatch}
561
Using {\tt lazymatch} instead of {\tt match} has an effect if the
562
right-hand-side of a clause returns a tactic. With {\tt match}, the
563
tactic is applied to the current goal (and the next clause is tried if
564
it fails). With {\tt lazymatch}, the tactic is directly returned as
565
the result of the whole {\tt lazymatch} block without being first
566
tried to be applied to the goal. Typically, if the {\tt lazymatch}
567
block is bound to some variable $x$ in a {\tt let in}, then tactic
568
expression gets bound to the variable $x$.
572
\subsubsection[Pattern matching on goals]{Pattern matching on goals\index{Ltac!match goal}
573
\index{Ltac!match reverse goal}
574
\index{match goal!in Ltac}
575
\index{match reverse goal!in Ltac}}
577
We can make pattern matching on goals using the following expression:
580
{\tt match goal with}\\
581
~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$
582
~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\
583
\>{\tt |} $hyp_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$
584
~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\
586
\>{\tt |} $hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$
587
~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\
588
\>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\
593
If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$
594
is matched (non-linear first order unification) by an hypothesis of
595
the goal and if {\cpattern}$_1$ is matched by the conclusion of the
596
goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the
597
pattern matching to the metavariables and the real hypothesis names
598
bound to the possible hypothesis names occurring in the hypothesis
599
patterns. If $v_1$ is a tactic value, then it is applied to the
600
goal. If this application fails, then another combination of
601
hypotheses is tried with the same proof context pattern. If there is
602
no other combination of hypotheses then the second proof context
603
pattern is tried and so on. If the next to last proof context pattern
604
fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$
605
is applied. Note also that matching against subterms (using the {\tt
606
context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may
607
itself induce extra backtrackings.
609
\ErrMsg \errindex{No matching clauses for match goal}
611
No clause succeeds, i.e. all matching patterns, if any,
612
fail at the application of the right-hand-side.
616
It is important to know that each hypothesis of the goal can be
617
matched by at most one hypothesis pattern. The order of matching is
618
the following: hypothesis patterns are examined from the right to the
619
left (i.e. $hyp_{i,m_i}$ before $hyp_{i,1}$). For each hypothesis
620
pattern, the goal hypothesis are matched in order (fresher hypothesis
621
first), but it possible to reverse this order (older first) with
622
the {\tt match reverse goal with} variant.
625
\index{lazymatch goal!in Ltac}
626
\index{Ltac!lazymatch goal}
627
\index{lazymatch reverse goal!in Ltac}
628
\index{Ltac!lazymatch reverse goal}
629
Using {\tt lazymatch} instead of {\tt match} has an effect if the
630
right-hand-side of a clause returns a tactic. With {\tt match}, the
631
tactic is applied to the current goal (and the next clause is tried if
632
it fails). With {\tt lazymatch}, the tactic is directly returned as
633
the result of the whole {\tt lazymatch} block without being first
634
tried to be applied to the goal. Typically, if the {\tt lazymatch}
635
block is bound to some variable $x$ in a {\tt let in}, then tactic
636
expression gets bound to the variable $x$.
641
| _ => idtac "here"; fail
642
| _ => idtac "wasn't lazy"; trivial
646
| _ => idtac "here"; fail
647
| _ => idtac "wasn't lazy"; trivial
650
test_lazy || idtac "was lazy".
651
test_eager || idtac "was lazy".
654
\subsubsection[Filling a term context]{Filling a term context\index{context!in expression}}
656
The following expression is not a tactic in the sense that it does not
657
produce subgoals but generates a term to be used in tactic
660
{\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]}
662
{\ident} must denote a context variable bound by a {\tt context}
663
pattern of a {\tt match} expression. This expression evaluates
664
replaces the hole of the value of {\ident} by the value of
667
\ErrMsg \errindex{not a context variable}
670
\subsubsection[Generating fresh hypothesis names]{Generating fresh hypothesis names\index{Ltac!fresh}
671
\index{fresh!in Ltac}}
673
Tactics sometimes have to generate new names for hypothesis. Letting
674
the system decide a name with the {\tt intro} tactic is not so good
675
since it is very awkward to retrieve the name the system gave.
676
The following expression returns an identifier:
678
{\tt fresh} \nelist{\textrm{\textsl{component}}}{}
680
It evaluates to an identifier unbound in the goal. This fresh
681
identifier is obtained by concatenating the value of the
682
\textrm{\textsl{component}}'s (each of them is, either an {\ident} which
683
has to refer to a name, or directly a name denoted by a
684
{\qstring}). If the resulting name is already used, it is padded
685
with a number so that it becomes fresh. If no component is
686
given, the name is a fresh derivative of the name {\tt H}.
688
\subsubsection[Computing in a constr]{Computing in a constr\index{Ltac!eval}
689
\index{eval!in Ltac}}
691
Evaluation of a term can be performed with:
693
{\tt eval} {\nterm{redexpr}} {\tt in} {\term}
695
where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt
696
hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold},
697
{\tt fold}, {\tt pattern}.
699
\subsubsection{Type-checking a term}
702
\index{type of!in Ltac}
704
The following returns the type of {\term}:
707
{\tt type of} {\term}
710
\subsubsection[Accessing tactic decomposition]{Accessing tactic decomposition\tacindex{info}
711
\index{Tacticals!info@{\tt info}}}
713
Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For
714
elementary tactics, this is equivalent to \tacexpr. For complex tactic
715
like \texttt{auto}, it displays the operations performed by the
718
\subsubsection[Proving a subgoal as a separate lemma]{Proving a subgoal as a separate lemma\tacindex{abstract}
719
\index{Tacticals!abstract@{\tt abstract}}}
721
From the outside ``\texttt{abstract \tacexpr}'' is the same as
722
{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called
723
{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the
724
current goal and \textit{n} is chosen so that this is a fresh name.
726
This tactical is useful with tactics such as \texttt{omega} or
727
\texttt{discriminate} that generate huge proof terms. With that tool
728
the user can avoid the explosion at time of the \texttt{Save} command
729
without having to cut manually the proof in smaller lemmas.
732
\item \texttt{abstract {\tacexpr} using {\ident}}.\\
733
Give explicitly the name of the auxiliary lemma.
736
\ErrMsg \errindex{Proof is not complete}
738
\subsubsection[Calling an external tactic]{Calling an external tactic\index{Ltac!external}}
740
The tactic {\tt external} allows to run an executable outside the
741
{\Coq} executable. The communication is done via an XML encoding of
742
constructions. The syntax of the command is
745
{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{}
748
The string \textsl{command}, to be interpreted in the default
749
execution path of the operating system, is the name of the external
750
command. The string \textsl{request} is the name of a request to be
751
sent to the external command. Finally the list of tactic arguments
752
have to evaluate to terms. An XML tree of the following form is sent
753
to the standard input of the external command.
757
\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\
758
the XML tree of the first argument\\
760
the XML tree of the last argument\\
761
\texttt{</REQUEST>}\\
765
Conversely, the external command must send on its standard output an
766
XML tree of the following forms:
771
the XML tree of a term\\
780
\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\
781
the XML tree of a first argument\\
783
the XML tree of a last argument\\
788
\noindent where \textsl{ltac\_qualified\_ident} is the name of a
789
defined {\ltac} function and each subsequent XML tree is recursively a
790
\texttt{CALL} or a \texttt{TERM} node.
792
The Document Type Definition (DTD) for terms of the Calculus of
793
Inductive Constructions is the one developed as part of the MoWGLI
794
European project. It can be found in the file {\tt dev/doc/cic.dtd} of
795
the {\Coq} source archive.
797
An example of parser for this DTD, written in the Objective Caml -
798
Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of
799
the {\Coq} source archive.
801
\section[Tactic toplevel definitions]{Tactic toplevel definitions\comindex{Ltac}}
803
\subsection{Defining {\ltac} functions}
805
Basically, {\ltac} toplevel definitions are made as follows:
806
%{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\
808
%{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every
809
%script is evaluated by substituting $v$ to {\ident}.
811
%We can define functional definitions by:\\
813
{\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
816
This defines a new {\ltac} function that can be used in any tactic
817
script or new {\ltac} toplevel definition.
819
\Rem The preceding definition can equivalently be written:
821
{\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$
824
Recursive and mutual recursive function definitions are also
825
possible with the syntax:
827
{\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ...
828
{\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
829
{\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=}
832
{\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
836
It is also possible to \emph{redefine} an existing user-defined tactic
839
{\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=}
842
A previous definition of \qualid must exist in the environment.
843
The new definition will always be used instead of the old one and
844
it goes accross module boundaries.
846
\subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}}
848
Defined {\ltac} functions can be displayed using the command
851
{\tt Print Ltac {\qualid}.}
854
\section[Debugging {\ltac} tactics]{Debugging {\ltac} tactics\comindex{Set Ltac Debug}
855
\comindex{Unset Ltac Debug}
856
\comindex{Test Ltac Debug}}
858
The {\ltac} interpreter comes with a step-by-step debugger. The
859
debugger can be activated using the command
862
{\tt Set Ltac Debug.}
865
\noindent and deactivated using the command
868
{\tt Unset Ltac Debug.}
871
To know if the debugger is on, use the command \texttt{Test Ltac Debug}.
872
When the debugger is activated, it stops at every step of the
873
evaluation of the current {\ltac} expression and it prints information
874
on what it is doing. The debugger stops, prompting for a command which
875
can be one of the following:
879
simple newline: & go to the next step\\
881
x: & exit current evaluation\\
882
s: & continue current evaluation without stopping\\
883
r$n$: & advance $n$ steps further\\
887
\subsection{Permutation on closed lists}
891
\fbox{\begin{minipage}{0.95\textwidth}
896
Inductive permut : list A -> list A -> Prop :=
897
| permut_refl : forall l, permut l l
899
forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1)
900
| permut_append : forall a l, permut (a :: l) (l ++ a :: nil)
902
forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2.
906
\caption{Definition of the permutation predicate}
911
Another more complex example is the problem of permutation on closed
912
lists. The aim is to show that a closed list is a permutation of
913
another one. First, we define the permutation predicate as shown on
914
Figure~\ref{permutpred}.
918
\fbox{\begin{minipage}{0.95\textwidth}
922
| |- (permut _ ?l ?l) => apply permut_refl
923
| |- (permut _ (?a :: ?l1) (?a :: ?l2)) =>
924
let newn := eval compute in (length l1) in
925
(apply permut_cons; Permut newn)
926
| |- (permut ?A (?a :: ?l1) ?l2) =>
927
match eval compute in n with
930
let l1' := constr:(l1 ++ a :: nil) in
931
(apply (permut_trans A (a :: l1) l1' l2);
932
[ apply permut_append | compute; Permut (pred n) ])
937
| |- (permut _ ?l1 ?l2) =>
938
match eval compute in (length l1 = length l2) with
939
| (?n = ?n) => Permut n
945
\caption{Permutation tactic}
951
\fbox{\begin{minipage}{0.95\textwidth}
954
permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil).
961
(0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil)
962
(0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil).
969
\caption{Examples of {\tt PermutProve} use}
973
Next, we can write naturally the tactic and the result can be seen on
974
Figure~\ref{permutltac}. We can notice that we use two toplevel
975
definitions {\tt PermutProve} and {\tt Permut}. The function to be
976
called is {\tt PermutProve} which computes the lengths of the two
977
lists and calls {\tt Permut} with the length if the two lists have the
978
same length. {\tt Permut} works as expected. If the two lists are
979
equal, it concludes. Otherwise, if the lists have identical first
980
elements, it applies {\tt Permut} on the tail of the lists. Finally,
981
if the lists have different first elements, it puts the first element
982
of one of the lists (here the second one which appears in the {\tt
983
permut} predicate) at the end if that is possible, i.e., if the new
984
first element has been at this place previously. To verify that all
985
rotations have been done for a list, we use the length of the list as
986
an argument for {\tt Permut} and this length is decremented for each
987
rotation down to, but not including, 1 because for a list of length
988
$n$, we can make exactly $n-1$ rotations to generate at most $n$
989
distinct lists. Here, it must be noticed that we use the natural
990
numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we
991
can see that it is possible to use usual natural numbers but they are
992
only used as arguments for primitive tactics and they cannot be
993
handled, in particular, we cannot make computations with them. So, a
994
natural choice is to use {\Coq} data structures so that {\Coq} makes
995
the computations (reductions) by {\tt eval compute in} and we can get
996
the terms back by {\tt match}.
998
With {\tt PermutProve}, we can now prove lemmas such those shown on
999
Figure~\ref{permutlem}.
1002
\subsection{Deciding intuitionistic propositional logic}
1006
\fbox{\begin{minipage}{0.95\textwidth}
1010
| |- True => trivial
1011
| _:False |- _ => elimtype False; assumption
1012
| _:?A |- ?A => auto
1018
| id:(~ _) |- _ => red in id
1019
| id:(_ /\ _) |- _ =>
1020
elim id; do 2 intro; clear id
1021
| id:(_ \/ _) |- _ =>
1022
elim id; intro; clear id
1023
| id:(?A /\ ?B -> ?C) |- _ =>
1025
[ intro | intros; apply id; split; assumption ]
1026
| id:(?A \/ ?B -> ?C) |- _ =>
1030
| intro; apply id; left; assumption ]
1031
| intro; apply id; right; assumption ]
1032
| id0:(?A -> ?B),id1:?A |- _ =>
1033
cut B; [ intro; clear id0 | apply id0; assumption ]
1034
| |- (_ /\ _) => split
1040
\caption{Deciding intuitionistic propositions (1)}
1046
\fbox{\begin{minipage}{0.95\textwidth}
1052
| id:((?A -> ?B) -> ?C) |- _ =>
1054
[ intro; cut (A -> B);
1056
[ intro; clear id | apply id; assumption ]
1058
| intro; apply id; intro; assumption ]; TautoProp
1059
| id:(~ ?A -> ?B) |- _ =>
1061
[ intro; cut (A -> False);
1063
[ intro; clear id | apply id; assumption ]
1065
| intro; apply id; red; intro; assumption ]; TautoProp
1066
| |- (_ \/ _) => (left; TautoProp) || (right; TautoProp)
1071
\caption{Deciding intuitionistic propositions (2)}
1075
The pattern matching on goals allows a complete and so a powerful
1076
backtracking when returning tactic values. An interesting application
1077
is the problem of deciding intuitionistic propositional logic.
1078
Considering the contraction-free sequent calculi {\tt LJT*} of
1079
Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic
1080
using the tactic language. On Figure~\ref{tautoltaca}, the tactic {\tt
1081
Axioms} tries to conclude using usual axioms. The {\tt DSimplif}
1082
tactic applies all the reversible rules of Dyckhoff's system.
1083
Finally, on Figure~\ref{tautoltacb}, the {\tt TautoProp} tactic (the
1084
main tactic to be called) simplifies with {\tt DSimplif}, tries to
1085
conclude with {\tt Axioms} and tries several paths using the
1086
backtracking rules (one of the four Dyckhoff's rules for the left
1087
implication to get rid of the contraction and the right or).
1091
\fbox{\begin{minipage}{0.95\textwidth}
1092
\begin{coq_example*}
1093
Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B.
1099
forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B.
1106
\caption{Proofs of tautologies with {\tt TautoProp}}
1110
For example, with {\tt TautoProp}, we can prove tautologies like those of
1111
Figure~\ref{tautolem}.
1114
\subsection{Deciding type isomorphisms}
1116
A more tricky problem is to decide equalities between types and modulo
1117
isomorphisms. Here, we choose to use the isomorphisms of the simply typed
1118
$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example,
1119
\cite{RC95}). The axioms of this $\lb{}$-calculus are given by
1120
Figure~\ref{isosax}.
1124
\fbox{\begin{minipage}{0.95\textwidth}
1128
\begin{coq_example*}
1129
Open Scope type_scope.
1131
Variables A B C : Set.
1132
Axiom Com : A * B = B * A.
1133
Axiom Ass : A * (B * C) = A * B * C.
1134
Axiom Cur : (A * B -> C) = (A -> B -> C).
1135
Axiom Dis : (A -> B * C) = (A -> B) * (A -> C).
1136
Axiom P_unit : A * unit = A.
1137
Axiom AR_unit : (A -> unit) = unit.
1138
Axiom AL_unit : (unit -> A) = A.
1139
Lemma Cons : B = C -> A * B = A * C.
1141
intro Heq; rewrite Heq; apply refl_equal.
1147
\caption{Type isomorphism axioms}
1151
The tactic to judge equalities modulo this axiomatization can be written as
1152
shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite
1153
simple. Types are reduced using axioms that can be oriented (this done by {\tt
1154
MainSimplif}). The normal forms are sequences of Cartesian
1155
products without Cartesian product in the left component. These normal forms
1156
are then compared modulo permutation of the components (this is done by {\tt
1157
CompareStruct}). The main tactic to be called and realizing this algorithm is
1162
\fbox{\begin{minipage}{0.95\textwidth}
1164
Ltac DSimplif trm :=
1167
rewrite <- (Ass A B C); try MainSimplif
1168
| (?A * ?B -> ?C) =>
1169
rewrite (Cur A B C); try MainSimplif
1170
| (?A -> ?B * ?C) =>
1171
rewrite (Dis A B C); try MainSimplif
1173
rewrite (P_unit A); try MainSimplif
1175
rewrite (Com unit B); try MainSimplif
1177
rewrite (AR_unit A); try MainSimplif
1179
rewrite (AL_unit B); try MainSimplif
1181
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1183
(DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif)
1187
| |- (?A = ?B) => try DSimplif A; try DSimplif B
1191
| (_ * ?B) => let succ := Length B in constr:(S succ)
1194
Ltac assoc := repeat rewrite <- Ass.
1198
\caption{Type isomorphism tactic (1)}
1204
\fbox{\begin{minipage}{0.95\textwidth}
1208
| [ |- (?A = ?A) ] => apply refl_equal
1209
| [ |- (?A * ?B = ?A * ?C) ] =>
1210
apply Cons; let newn := Length B in DoCompare newn
1211
| [ |- (?A * ?B = ?C) ] =>
1212
match eval compute in n with
1215
pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n)
1218
Ltac CompareStruct :=
1220
| [ |- (?A = ?B) ] =>
1222
with l2 := Length B in
1223
match eval compute in (l1 = l2) with
1224
| (?n = ?n) => DoCompare n
1227
Ltac IsoProve := MainSimplif; CompareStruct.
1231
\caption{Type isomorphism tactic (2)}
1235
Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.
1239
\fbox{\begin{minipage}{0.95\textwidth}
1240
\begin{coq_example*}
1242
forall A B:Set, A * unit * B = B * (unit * A).
1249
(A * unit -> B * (C * unit)) =
1250
(A * unit -> (C -> unit) * C) * (unit -> A -> B).
1257
\caption{Type equalities solved by {\tt IsoProve}}
1261
%%% Local Variables:
1263
%%% TeX-master: "Reference-Manual"
added
removed
doc/refman/RefMan-ltac.tex
