diff options
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 1057 |
1 files changed, 1057 insertions, 0 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex new file mode 100644 index 00000000..eced8099 --- /dev/null +++ b/doc/refman/RefMan-ltac.tex @@ -0,0 +1,1057 @@ +\chapter{The tactic language} +\label{TacticLanguage} + +%\geometry{a4paper,body={5in,8in}} + +This chapter gives a compact documentation of Ltac, the tactic +language available in {\Coq}. We start by giving the syntax, and next, +we present the informal semantics. If you want to know more regarding +this language and especially about its fundations, you can refer +to~\cite{Del00}. Chapter~\ref{Tactics-examples} is devoted to giving +examples of use of this language on small but also with non-trivial +problems. + + +\section{Syntax} + +\def\tacexpr{\textrm{\textsl{expr}}} +\def\tacexprlow{\textrm{\textsl{tacexpr$_1$}}} +\def\tacexprinf{\textrm{\textsl{tacexpr$_2$}}} +\def\tacexprpref{\textrm{\textsl{tacexpr$_3$}}} +\def\atom{\textrm{\textsl{atom}}} +\def\recclause{\textrm{\textsl{rec\_clause}}} +\def\letclause{\textrm{\textsl{let\_clause}}} +\def\matchrule{\textrm{\textsl{match\_rule}}} +\def\contextrule{\textrm{\textsl{context\_rule}}} +\def\contexthyps{\textrm{\textsl{context\_hyps}}} +\def\tacarg{\nterm{tacarg}} +\def\cpattern{\nterm{cpattern}} + +The syntax of the tactic language is given Figures~\ref{ltac} +and~\ref{ltac_aux}. See page~\pageref{BNF-syntax} for a description of +the BNF metasyntax used in these grammar rules. Various already defined +entries will be used in this chapter: entries {\naturalnumber}, +{\integer}, {\ident}, {\qualid}, {\term}, {\cpattern} and {\atomictac} +represent respectively the natural and integer numbers, the authorized +identificators and qualified names, {\Coq}'s terms and patterns and +all the atomic tactics described in chapter~\ref{Tactics}. The syntax +of {\cpattern} is the same as that of terms, but there can be specific +variables like {\tt ?id} where {\tt id} is a {\ident} or {\tt \_}, +which are metavariables for pattern matching. {\tt ?id} allows us to +keep instantiations and to make constraints whereas {\tt \_} shows +that we are not interested in what will be matched. On the right hand +side, they are used without the question mark. + +The main entry of the grammar is {\tacexpr}. This language is used in +proof mode but it can also be used in toplevel definitions as shown in +Figure~\ref{ltactop}. + +\begin{Remarks} +\item The infix tacticals ``\dots\ {\tt ||} \dots'' and ``\dots\ {\tt + ;} \dots'' are associative. + +\item As shown by the figure, tactical {\tt ||} binds more than the +prefix tacticals {\tt try}, {\tt repeat}, {\tt do}, {\tt info} and +{\tt abstract} which themselves bind more than the postfix tactical +``{\tt \dots\ ;[ \dots\ ]}'' which binds more than ``\dots\ {\tt ;} +\dots''. + +For instance +\begin{quote} +{\tt try repeat \tac$_1$ || + \tac$_2$;\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$];\tac$_4$.} +\end{quote} +is understood as +\begin{quote} +{\tt (try (repeat (\tac$_1$ || \tac$_2$)));} \\ +{\tt ((\tac$_3$;[\tac$_{31}$|\dots|\tac$_{3n}$]);\tac$_4$).} +\end{quote} +\end{Remarks} + + +\begin{figure}[htbp] +\begin{centerframe} +\begin{tabular}{lcl} +{\tacexpr} & ::= & + {\tacexpr} {\tt ;} {\tacexpr}\\ +& | & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\ +& | & {\tacexprpref}\\ +\\ +{\tacexprpref} & ::= & + {\tt do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\ +& | & {\tt info} {\tacexprpref}\\ +& | & {\tt progress} {\tacexprpref}\\ +& | & {\tt repeat} {\tacexprpref}\\ +& | & {\tt try} {\tacexprpref}\\ +& | & {\tacexprinf} \\ +\\ +{\tacexprinf} & ::= & + {\tacexprlow} {\tt ||} {\tacexprpref}\\ +& | & {\tacexprlow}\\ +\\ +{\tacexprlow} & ::= & +{\tt fun} \nelist{\name}{} {\tt =>} {\atom}\\ +& | & +{\tt let} \nelist{\letclause}{\tt with} {\tt in} +{\atom}\\ +& | & +{\tt let rec} \nelist{\recclause}{\tt with} {\tt in} +{\tacexpr}\\ +& | & +{\tt match goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt match reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ +& | & +{\tt match} {\tacexpr} {\tt with} \nelist{\matchrule}{\tt |} {\tt end}\\ +& | & {\tt abstract} {\atom}\\ +& | & {\tt abstract} {\atom} {\tt using} {\ident} \\ +& | & {\tt first [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ +& | & {\tt solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\ +& | & {\tt idtac} ~|~ {\tt idtac} {\qstring}\\ +& | & {\tt fail} ~|~ {\tt fail} {\naturalnumber} {\qstring}\\ +& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ +& | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ +& | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\ +& | & {\tt type of} {\term}\\ +& | & {\tt constr :} {\term}\\ +& | & \atomictac\\ +& | & {\qualid} \nelist{\tacarg}{}\\ +& | & {\atom}\\ +\\ +{\atom} & ::= & + {\qualid} \\ +& | & ()\\ +& | & {\tt (} {\tacexpr} {\tt )}\\ +\end{tabular} +\end{centerframe} +\caption{Syntax of the tactic language} +\label{ltac} +\end{figure} + + + +\begin{figure}[htbp] +\begin{centerframe} +\begin{tabular}{lcl} +\tacarg & ::= & + {\qualid}\\ +& $|$ & {\tt ()} \\ +& $|$ & {\tt ltac :} {\atom}\\ +& $|$ & {\term}\\ +\\ +\letclause & ::= & {\ident} \sequence{\name}{} {\tt :=} {\tacexpr}\\ +\\ +\recclause & ::= & {\ident} \nelist{\name}{} {\tt :=} {\tacexpr}\\ +\\ +\contextrule & ::= & + \nelist{\contexthyps}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\ +& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\ +& $|$ & {\tt \_ =>} {\tacexpr}\\ +\\ +\contexthyps & ::= & {\name} {\tt :} {\cpattern}\\ +\\ +\matchrule & ::= & + {\cpattern} {\tt =>} {\tacexpr}\\ +& $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} {\tt =>} {\tacexpr}\\ +& $|$ & {\tt \_ =>} {\tacexpr}\\ +\end{tabular} +\end{centerframe} +\caption{Syntax of the tactic language (continued)} +\label{ltac_aux} +\end{figure} + +\begin{figure}[ht] +\begin{centerframe} +\begin{tabular}{lcl} +\nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\ +\\ +\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr} +\end{tabular} +\end{centerframe} +\caption{Tactic toplevel definitions} +\label{ltactop} +\end{figure} + + +%% +%% Semantics +%% +\section{Semantics} +%\index[tactic]{Tacticals} +\index{Tacticals} +%\label{Tacticals} + +Tactic expressions can only be applied in the context of a goal. The +evaluation yields either a term, an integer or a tactic. Intermediary +results can be terms or integers but the final result must be a tactic +which is then applied to the current goal. + +There is a special case for {\tt match goal} expressions of which +the clauses evaluate to tactics. Such expressions can only be used as +end result of a tactic expression (never as argument of a local +definition or of an application). + +The rest of this section explains the semantics of every construction +of Ltac. + + +%% \subsection{Values} + +%% Values are given by Figure~\ref{ltacval}. All these values are tactic values, +%% i.e. to be applied to a goal, except {\tt Fun}, {\tt Rec} and $arg$ values. + +%% \begin{figure}[ht] +%% \noindent{}\framebox[6in][l] +%% {\parbox{6in} +%% {\begin{center} +%% \begin{tabular}{lp{0.1in}l} +%% $vexpr$ & ::= & $vexpr$ {\tt ;} $vexpr$\\ +%% & | & $vexpr$ {\tt ; [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt +%% ]}\\ +%% & | & $vatom$\\ +%% \\ +%% $vatom$ & ::= & {\tt Fun} \nelist{\inputfun}{} {\tt ->} {\tacexpr}\\ +%% %& | & {\tt Rec} \recclause\\ +%% & | & +%% {\tt Rec} \nelist{\recclause}{\tt And} {\tt In} +%% {\tacexpr}\\ +%% & | & +%% {\tt Match Context With} {\it (}$context\_rule$ {\tt |}{\it )}$^*$ +%% $context\_rule$\\ +%% & | & {\tt (} $vexpr$ {\tt )}\\ +%% & | & $vatom$ {\tt Orelse} $vatom$\\ +%% & | & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} $vatom$\\ +%% & | & {\tt Repeat} $vatom$\\ +%% & | & {\tt Try} $vatom$\\ +%% & | & {\tt First [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\ +%% & | & {\tt Solve [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\ +%% & | & {\tt Idtac}\\ +%% & | & {\tt Fail}\\ +%% & | & {\primitivetactic}\\ +%% & | & $arg$ +%% \end{tabular} +%% \end{center}}} +%% \caption{Values of ${\cal L}_{tac}$} +%% \label{ltacval} +%% \end{figure} + +%% \subsection{Evaluation} + +\subsubsection{Sequence} +\tacindex{;} +\index{Tacticals!;@{\tt {\tac$_1$};\tac$_2$}} + +A sequence is an expression of the following form: +\begin{quote} +{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$ +\end{quote} +{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and +$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is then applied +and $v_2$ is applied to every subgoal generated by the application of +$v_1$. Sequence is left associating. + +\subsubsection{General sequence} +\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]} +%\tacindex{; [ | ]} +%\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}} +\index{Tacticals!; [ | ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}} + +We can generalize the previous sequence operator as +\begin{quote} +{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} +{\tacexpr}$_n$ {\tt ]} +\end{quote} +{\tacexpr}$_i$ is evaluated to $v_i$, for $i=0,...,n$. $v_0$ is +applied and $v_i$ is applied to the $i$-th generated subgoal by the +application of $v_0$, for $=1,...,n$. It fails if the application of +$v_0$ does not generate exactly $n$ subgoals. + +\subsubsection{For loop} +\tacindex{do} +\index{Tacticals!do@{\tt do}} + +There is a for loop that repeats a tactic {\num} times: +\begin{quote} +{\tt do} {\num} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied {\num} times. Supposing ${\num}>1$, after the first +application of $v$, $v$ is applied, at least once, to the generated +subgoals and so on. It fails if the application of $v$ fails before +the {\num} applications have been completed. + +\subsubsection{Repeat loop} +\tacindex{repeat} +\index{Tacticals!repeat@{\tt repeat}} + +We have a repeat loop with: +\begin{quote} +{\tt repeat} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied until it fails. Supposing $n>1$, after the first application +of $v$, $v$ is applied, at least once, to the generated subgoals and +so on. It stops when it fails for all the generated subgoals. It never +fails. + +\subsubsection{Error catching} +\tacindex{try} +\index{Tacticals!try@{\tt try}} + +We can catch the tactic errors with: +\begin{quote} +{\tt try} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied. If the application of $v$ fails, it catches the error and +leaves the goal unchanged. If the level of the exception is positive, +then the exception is re-raised with its level decremented. + +\subsubsection{Detecting progress} +\tacindex{progress} + +We can check if a tactic made progress with: +\begin{quote} +{\tt progress} {\tacexpr} +\end{quote} +{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is +applied. If the application of $v$ produced one subgoal equal to the +initial goal (up to syntactical equality), then an error of level 0 is +raised. + +\ErrMsg \errindex{Failed to progress} + +\subsubsection{Branching} +\tacindex{$\mid\mid$} +\index{Tacticals!orelse@{\tt $\mid\mid$}} + +We can easily branch with the following structure: +\begin{quote} +{\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ +\end{quote} +{\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated to $v_1$ and +$v_2$. $v_1$ and $v_2$ must be tactic values. $v_1$ is applied and if +it fails then $v_2$ is applied. Branching is left associating. + +\subsubsection{First tactic to work} +\tacindex{first} +\index{Tacticals!first@{\tt first}} + +We may consider the first tactic to work (i.e. which does not fail) among a +panel of tactics: +\begin{quote} +{\tt first [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} +\end{quote} +{\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for +$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it works, it stops else it +tries to apply $v_2$ and so on. It fails when there is no applicable tactic. + +\ErrMsg \errindex{No applicable tactic} + +\subsubsection{Solving} +\tacindex{solve} +\index{Tacticals!solve@{\tt solve}} + +We may consider the first to solve (i.e. which generates no subgoal) among a +panel of tactics: +\begin{quote} +{\tt solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} +\end{quote} +{\tacexpr}$_i$ are evaluated to $v_i$ and $v_i$ must be tactic values, for +$i=1,...,n$. Supposing $n>1$, it applies $v_1$, if it solves, it stops else it +tries to apply $v_2$ and so on. It fails if there is no solving tactic. + +\ErrMsg \errindex{Cannot solve the goal} + +\subsubsection{Identity} +\tacindex{idtac} +\index{Tacticals!idtac@{\tt idtac}} + +The constant {\tt idtac} is the identity tactic: it leaves any goal +unchanged but it appears in the proof script. +\begin{quote} +{\tt idtac} and {\tt idtac "message"} +\end{quote} +The latter variant prints the string on the standard output. + + +\subsubsection{Failing} +\tacindex{fail} +\index{Tacticals!fail@{\tt fail}} + +The tactic {\tt fail} is the always-failing tactic: it does not solve +any goal. It is useful for defining other tacticals since it can be +catched by {\tt try} or {\tt match goal}. There are three variants: +\begin{quote} +{\tt fail $n$}, {\tt fail "message"} and {\tt fail $n$ "message"} +\end{quote} +The number $n$ is the failure level. If no level is specified, it +defaults to $0$. The level is used by {\tt try} and {\tt match goal}. +If $0$, it makes {\tt match goal} considering the next clause +(backtracking). If non zero, the current {\tt match goal} block or +{\tt try} command is aborted and the level is decremented. + +\ErrMsg \errindex{Tactic Failure "message" (level $n$)}. + +\subsubsection{Local definitions} +\index{Ltac!let} +\index{Ltac!let rec} +\index{let!in Ltac} +\index{let rec!in Ltac} + +Local definitions can be done as follows: +\begin{quote} +{\tt let} {\ident}$_1$ {\tt :=} {\tacexpr}$_1$\\ +{\tt with} {\ident}$_2$ {\tt :=} {\tacexpr}$_2$\\ +...\\ +{\tt with} {\ident}$_n$ {\tt :=} {\tacexpr}$_n$ {\tt in}\\ +{\tacexpr} +\end{quote} +each {\tacexpr}$_i$ is evaluated to $v_i$, then, {\tacexpr} is +evaluated by substituting $v_i$ to each occurrence of {\ident}$_i$, +for $i=1,...,n$. There is no dependencies between the {\tacexpr}$_i$ +and the {\ident}$_i$. + +Local definitions can be recursive by using {\tt let rec} instead of +{\tt let}. Only functions can be defined by recursion, so at least one +argument is required. + +\subsubsection{Application} + +An application is an expression of the following form: +\begin{quote} +{\qualid} {\tacarg}$_1$ ... {\tacarg}$_n$ +\end{quote} +The reference {\qualid} must be bound to some defined tactic +definition expecting at least $n$ arguments. The expressions +{\tacexpr}$_i$ are evaluated to $v_i$, for $i=1,...,n$. +%If {\tacexpr} is a {\tt Fun} or {\tt Rec} value then the body is evaluated by +%substituting $v_i$ to the formal parameters, for $i=1,...,n$. For recursive +%clauses, the bodies are lazily substituted (when an identifier to be evaluated +%is the name of a recursive clause). + +%\subsection{Application of tactic values} + +\subsubsection{Function construction} +\index{fun!in Ltac} +\index{Ltac!fun} + +A parameterized tactic can be built anonymously (without resorting to +local definitions) with: +\begin{quote} +{\tt fun} {\ident${}_1$} ... {\ident${}_n$} {\tt =>} {\tacexpr} +\end{quote} +Indeed, local definitions of functions are a syntactic sugar for +binding a {\tt fun} tactic to an identifier. + +\subsubsection{Pattern matching on terms} +\index{Ltac!match} +\index{match!in Ltac} + +We can carry out pattern matching on terms with: +\begin{quote} +{\tt match} {\tacexpr} {\tt with}\\ +~~~{\cpattern}$_1$ {\tt =>} {\tacexpr}$_1$\\ +~{\tt |} {\cpattern}$_2$ {\tt =>} {\tacexpr}$_2$\\ +~...\\ +~{\tt |} {\cpattern}$_n$ {\tt =>} {\tacexpr}$_n$\\ +~{\tt |} {\tt \_} {\tt =>} {\tacexpr}$_{n+1}$\\ +{\tt end} +\end{quote} +The {\tacexpr} is evaluated and should yield a term which is matched +(non-linear first order unification) against {\cpattern}$_1$ then +{\tacexpr}$_1$ is evaluated into some value by substituting the +pattern matching instantiations to the metavariables. If the matching +with {\cpattern}$_1$ fails, {\cpattern}$_2$ is used and so on. The +pattern {\_} matches any term and shunts all remaining patterns if +any. If {\tacexpr}$_1$ evaluates to a tactic, this tactic is not +immediately applied to the current goal (in contrast with {\tt match +goal}). If all clauses fail (in particular, there is no pattern {\_}) +then a no-matching error is raised. + +\begin{ErrMsgs} + +\item \errindex{No matching clauses for match} + + No pattern can be used and, in particular, there is no {\tt \_} pattern. + +\item \errindex{Argument of match does not evaluate to a term} + + This happens when {\tacexpr} does not denote a term. + +\end{ErrMsgs} + +\index{context!in pattern} +There is a special form of patterns to match a subterm against the +pattern: +\begin{quote} +{\tt context} {\ident} {\tt [} {\cpattern} {\tt ]} +\end{quote} +It matches any term which one subterm matches {\cpattern}. If there is +a match, the optional {\ident} is assign the ``matched context'', that +is the initial term where the matched subterm is replaced by a +hole. The definition of {\tt context} in expressions below will show +how to use such term contexts. + +This operator never makes backtracking. If there are several subterms +matching the pattern, only the first match is considered. Note that +the order of matching is left unspecified. +%% TODO: clarify this point! It *should* be specified + + +\subsubsection{Pattern matching on goals} +\index{Ltac!match goal} +\index{Ltac!match reverse goal} +\index{match goal!in Ltac} +\index{match reverse goal!in Ltac} + +We can make pattern matching on goals using the following expression: +\begin{quote} +\begin{tabbing} +{\tt match goal with}\\ +~~\={\tt |} $hyp_{1,1}${\tt ,}...{\tt ,}$hyp_{1,m_1}$ + ~~{\tt |-}{\cpattern}$_1${\tt =>} {\tacexpr}$_1$\\ + \>{\tt |} $hyp_{2,1}${\tt ,}...{\tt ,}$hyp_{2,m_2}$ + ~~{\tt |-}{\cpattern}$_2${\tt =>} {\tacexpr}$_2$\\ +~~...\\ + \>{\tt |} $hyp_{n,1}${\tt ,}...{\tt ,}$hyp_{n,m_n}$ + ~~{\tt |-}{\cpattern}$_n${\tt =>} {\tacexpr}$_n$\\ + \>{\tt |\_}~~~~{\tt =>} {\tacexpr}$_{n+1}$\\ +{\tt end} +\end{tabbing} +\end{quote} + +% TODO: specify order of hypothesis and explain reverse... + +If each hypothesis pattern $hyp_{1,i}$, with $i=1,...,m_1$ +is matched (non-linear first order unification) by an hypothesis of +the goal and if {\cpattern}$_1$ is matched by the conclusion of the +goal, then {\tacexpr}$_1$ is evaluated to $v_1$ by substituting the +pattern matching to the metavariables and the real hypothesis names +bound to the possible hypothesis names occurring in the hypothesis +patterns. If $v_1$ is a tactic value, then it is applied to the +goal. If this application fails, then another combination of +hypotheses is tried with the same proof context pattern. If there is +no other combination of hypotheses then the second proof context +pattern is tried and so on. If the next to last proof context pattern +fails then {\tacexpr}$_{n+1}$ is evaluated to $v_{n+1}$ and $v_{n+1}$ +is applied. + +\ErrMsg \errindex{No matching clauses for match goal} + + No goal pattern can be used and, in particular, there is no {\tt + \_} goal pattern. + +\medskip + +It is important to know that each hypothesis of the goal can be +matched by at most one hypothesis pattern. The order of matching is +the following: hypothesis patterns are examined from the right to the +left (i.e. $hyp_{i,m_i}$ before $hyp_{i,1}$). For each hypothesis +pattern, the goal hypothesis are matched in order (fresher hypothesis +first), but it possible to reverse this order (older first) with +the {\tt match reverse goal with} variant. + +\subsubsection{Filling a term context} +\index{context!in expression} + +The following expression is not a tactic in the sense that it does not +produce subgoals but generates a term to be used in tactic +expressions: +\begin{quote} +{\tt context} {\ident} {\tt [} {\tacexpr} {\tt ]} +\end{quote} +{\ident} must denote a context variable bound by a {\tt context} +pattern of a {\tt match} expression. This expression evaluates +replaces the hole of the value of {\ident} by the value of +{\tacexpr}. + +\ErrMsg \errindex{not a context variable} + + +\subsubsection{Generating fresh hypothesis names} +\index{Ltac!fresh} +\index{fresh!in Ltac} + +Tactics sometimes have to generate new names for hypothesis. Letting +the system decide a name with the {\tt intro} tactic is not so good +since it is very awkward to retrieve the name the system gave. + +As before, the following expression returns a term: +\begin{quote} +{\tt fresh} {\qstring} +\end{quote} +It evaluates to an identifier unbound in the goal, which is obtained +by padding {\qstring} with a number if necessary. If no name is given, +the prefix is {\tt H}. + +\subsubsection{{\tt type of} {\term}} +%\tacindex{type of} +\index{Ltac!type of} +\index{type of!in Ltac} + +This tactic computes the type of {\term}. + +\subsubsection{Computing in a constr} +\index{Ltac!eval} +\index{eval!in Ltac} + +Evaluation of a term can be performed with: +\begin{quote} +{\tt eval} {\nterm{redexpr}} {\tt in} {\term} +\end{quote} +where \nterm{redexpr} is a reduction tactic among {\tt red}, {\tt +hnf}, {\tt compute}, {\tt simpl}, {\tt cbv}, {\tt lazy}, {\tt unfold}, +{\tt fold}, {\tt pattern}. + + +\subsubsection{Accessing tactic decomposition} +\tacindex{info} +\index{Tacticals!info@{\tt info}} + +Tactical ``{\tt info} {\tacexpr}'' is not really a tactical. For +elementary tactics, this is equivalent to \tacexpr. For complex tactic +like \texttt{auto}, it displays the operations performed by the +tactic. + +\subsubsection{Proving a subgoal as a separate lemma} +\tacindex{abstract} +\index{Tacticals!abstract@{\tt abstract}} + +From the outside ``\texttt{abstract \tacexpr}'' is the same as +{\tt solve \tacexpr}. Internally it saves an auxiliary lemma called +{\ident}\texttt{\_subproof}\textit{n} where {\ident} is the name of the +current goal and \textit{n} is chosen so that this is a fresh name. + +This tactical is useful with tactics such as \texttt{omega} or +\texttt{discriminate} that generate huge proof terms. With that tool +the user can avoid the explosion at time of the \texttt{Save} command +without having to cut manually the proof in smaller lemmas. + +\begin{Variants} +\item \texttt{abstract {\tacexpr} using {\ident}}.\\ + Give explicitly the name of the auxiliary lemma. +\end{Variants} + +\ErrMsg \errindex{Proof is not complete} + +\section{Tactic toplevel definitions} +\comindex{Ltac} + +Basically, tactics toplevel definitions are made as follows: +%{\tt Tactic Definition} {\ident} {\tt :=} {\tacexpr}\\ +% +%{\tacexpr} is evaluated to $v$ and $v$ is associated to {\ident}. Next, every +%script is evaluated by substituting $v$ to {\ident}. +% +%We can define functional definitions by:\\ +\begin{quote} +{\tt Ltac} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=} +{\tacexpr} +\end{quote} +This defines a new tactic that can be used in any tactic script or new +tactic toplevel definition. + +\Rem The preceding definition can equivalently be written: +\begin{quote} +{\tt Ltac} {\ident} {\tt := fun} {\ident}$_1$ ... {\ident}$_n$ +{\tt =>} {\tacexpr} +\end{quote} +Recursive and mutual recursive function definitions are also +possible with the syntax: +\begin{quote} +{\tt Ltac} {\ident}$_1$ {\ident}$_{1,1}$ ... +{\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\ +{\tt with} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=} +{\tacexpr}$_2$\\ +...\\ +{\tt with} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=} +{\tacexpr}$_n$ +\end{quote} + +%This definition bloc is a set of definitions (use of +%the same previous syntactical sugar) and the other scripts are evaluated as +%usual except that the substitutions are lazily carried out (when an identifier +%to be evaluated is the name of a recursive definition). + +\endinput + + +\subsection{Permutation on closed lists} + +\begin{figure}[b] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Require Import List. +Section Sort. +Variable A : Set. +Inductive permut : list A -> list A -> Prop := + | permut_refl : forall l, permut l l + | permut_cons : + forall a l0 l1, permut l0 l1 -> permut (a :: l0) (a :: l1) + | permut_append : forall a l, permut (a :: l) (l ++ a :: nil) + | permut_trans : + forall l0 l1 l2, permut l0 l1 -> permut l1 l2 -> permut l0 l2. +End Sort. +\end{coq_example*} +\end{center} +\caption{Definition of the permutation predicate} +\label{permutpred} +\end{figure} + + +Another more complex example is the problem of permutation on closed +lists. The aim is to show that a closed list is a permutation of +another one. First, we define the permutation predicate as shown on +Figure~\ref{permutpred}. + +\begin{figure}[p] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac Permut n := + match goal with + | |- (permut _ ?l ?l) => apply permut_refl + | |- (permut _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply permut_cons; Permut newn) + | |- (permut ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (permut_trans A (a :: l1) l1' l2); + [ apply permut_append | compute; Permut (pred n) ]) + end + end. +Ltac PermutProve := + match goal with + | |- (permut _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => Permut n + end + end. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Permutation tactic} +\label{permutltac} +\end{figure} + +\begin{figure}[p] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma permut_ex1 : + permut nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). +Proof. +PermutProve. +Qed. + +Lemma permut_ex2 : + permut nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). +Proof. +PermutProve. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Examples of {\tt PermutProve} use} +\label{permutlem} +\end{figure} + +Next, we can write naturally the tactic and the result can be seen on +Figure~\ref{permutltac}. We can notice that we use two toplevel +definitions {\tt PermutProve} and {\tt Permut}. The function to be +called is {\tt PermutProve} which computes the lengths of the two +lists and calls {\tt Permut} with the length if the two lists have the +same length. {\tt Permut} works as expected. If the two lists are +equal, it concludes. Otherwise, if the lists have identical first +elements, it applies {\tt Permut} on the tail of the lists. Finally, +if the lists have different first elements, it puts the first element +of one of the lists (here the second one which appears in the {\tt + permut} predicate) at the end if that is possible, i.e., if the new +first element has been at this place previously. To verify that all +rotations have been done for a list, we use the length of the list as +an argument for {\tt Permut} and this length is decremented for each +rotation down to, but not including, 1 because for a list of length +$n$, we can make exactly $n-1$ rotations to generate at most $n$ +distinct lists. Here, it must be noticed that we use the natural +numbers of {\Coq} for the rotation counter. On Figure~\ref{ltac}, we +can see that it is possible to use usual natural numbers but they are +only used as arguments for primitive tactics and they cannot be +handled, in particular, we cannot make computations with them. So, a +natural choice is to use {\Coq} data structures so that {\Coq} makes +the computations (reductions) by {\tt eval compute in} and we can get +the terms back by {\tt match}. + +With {\tt PermutProve}, we can now prove lemmas such those shown on +Figure~\ref{permutlem}. + + +\subsection{Deciding intuitionistic propositional logic} + +\begin{figure}[tbp] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac Axioms := + match goal with + | |- True => trivial + | _:False |- _ => elimtype False; assumption + | _:?A |- ?A => auto + end. +Ltac DSimplif := + repeat + (intros; + match goal with + | id:(~ _) |- _ => red in id + | id:(_ /\ _) |- _ => + elim id; do 2 intro; clear id + | id:(_ \/ _) |- _ => + elim id; intro; clear id + | id:(?A /\ ?B -> ?C) |- _ => + cut (A -> B -> C); + [ intro | intros; apply id; split; assumption ] + | id:(?A \/ ?B -> ?C) |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear id + | intro; apply id; left; assumption ] + | intro; apply id; right; assumption ] + | id0:(?A -> ?B),id1:?A |- _ => + cut B; [ intro; clear id0 | apply id0; assumption ] + | |- (_ /\ _) => split + | |- (~ _) => red + end). +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Deciding intuitionistic propositions (1)} +\label{tautoltaca} +\end{figure} + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac TautoProp := + DSimplif; + Axioms || + match goal with + | id:((?A -> ?B) -> ?C) |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear id | apply id; assumption ] + | clear id ] + | intro; apply id; intro; assumption ]; TautoProp + | id:(~ ?A -> ?B) |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear id | apply id; assumption ] + | clear id ] + | intro; apply id; red; intro; assumption ]; TautoProp + | |- (_ \/ _) => (left; TautoProp) || (right; TautoProp) + end. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Deciding intuitionistic propositions (2)} +\label{tautoltacb} +\end{figure} + +The pattern matching on goals allows a complete and so a powerful +backtracking when returning tactic values. An interesting application +is the problem of deciding intuitionistic propositional logic. +Considering the contraction-free sequent calculi {\tt LJT*} of +Roy~Dyckhoff (\cite{Dyc92}), it is quite natural to code such a tactic +using the tactic language. On Figure~\ref{tautoltaca}, the tactic {\tt + Axioms} tries to conclude using usual axioms. The {\tt DSimplif} +tactic applies all the reversible rules of Dyckhoff's system. +Finally, on Figure~\ref{tautoltacb}, the {\tt TautoProp} tactic (the +main tactic to be called) simplifies with {\tt DSimplif}, tries to +conclude with {\tt Axioms} and tries several paths using the +backtracking rules (one of the four Dyckhoff's rules for the left +implication to get rid of the contraction and the right or). + +\begin{figure}[tb] +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma tauto_ex1 : forall A B:Prop, A /\ B -> A \/ B. +Proof. +TautoProp. +Qed. + +Lemma tauto_ex2 : + forall A B:Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. +Proof. +TautoProp. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Proofs of tautologies with {\tt TautoProp}} +\label{tautolem} +\end{figure} + +For example, with {\tt TautoProp}, we can prove tautologies like those of +Figure~\ref{tautolem}. + + +\subsection{Deciding type isomorphisms} + +A more tricky problem is to decide equalities between types and modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply typed +$\lb{}$-calculus with Cartesian product and $unit$ type (see, for example, +\cite{RC95}). The axioms of this $\lb{}$-calculus are given by +Figure~\ref{isosax}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_eval} +Reset Initial. +\end{coq_eval} +\begin{coq_example*} +Open Scope type_scope. +Section Iso_axioms. +Variables A B C : Set. +Axiom Com : A * B = B * A. +Axiom Ass : A * (B * C) = A * B * C. +Axiom Cur : (A * B -> C) = (A -> B -> C). +Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). +Axiom P_unit : A * unit = A. +Axiom AR_unit : (A -> unit) = unit. +Axiom AL_unit : (unit -> A) = A. +Lemma Cons : B = C -> A * B = A * C. +Proof. +intro Heq; rewrite Heq; apply refl_equal. +Qed. +End Iso_axioms. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Type isomorphism axioms} +\label{isosax} +\end{figure} + +The tactic to judge equalities modulo this axiomatization can be written as +shown on Figures~\ref{isosltac1} and~\ref{isosltac2}. The algorithm is quite +simple. Types are reduced using axioms that can be oriented (this done by {\tt +MainSimplif}). The normal forms are sequences of Cartesian +products without Cartesian product in the left component. These normal forms +are then compared modulo permutation of the components (this is done by {\tt +CompareStruct}). The main tactic to be called and realizing this algorithm is +{\tt IsoProve}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac DSimplif trm := + match trm with + | (?A * ?B * ?C) => + rewrite <- (Ass A B C); try MainSimplif + | (?A * ?B -> ?C) => + rewrite (Cur A B C); try MainSimplif + | (?A -> ?B * ?C) => + rewrite (Dis A B C); try MainSimplif + | (?A * unit) => + rewrite (P_unit A); try MainSimplif + | (unit * ?B) => + rewrite (Com unit B); try MainSimplif + | (?A -> unit) => + rewrite (AR_unit A); try MainSimplif + | (unit -> ?B) => + rewrite (AL_unit B); try MainSimplif + | (?A * ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) + | (?A -> ?B) => + (DSimplif A; try MainSimplif) || (DSimplif B; try MainSimplif) + end + with MainSimplif := + match goal with + | |- (?A = ?B) => try DSimplif A; try DSimplif B + end. +Ltac Length trm := + match trm with + | (_ * ?B) => let succ := Length B in constr:(S succ) + | _ => constr:1 + end. +Ltac assoc := repeat rewrite <- Ass. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Type isomorphism tactic (1)} +\label{isosltac1} +\end{figure} + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example} +Ltac DoCompare n := + match goal with + | [ |- (?A = ?A) ] => apply refl_equal + | [ |- (?A * ?B = ?A * ?C) ] => + apply Cons; let newn := Length B in DoCompare newn + | [ |- (?A * ?B = ?C) ] => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; DoCompare (pred n) + end + end. +Ltac CompareStruct := + match goal with + | [ |- (?A = ?B) ] => + let l1 := Length A + with l2 := Length B in + match eval compute in (l1 = l2) with + | (?n = ?n) => DoCompare n + end + end. +Ltac IsoProve := MainSimplif; CompareStruct. +\end{coq_example} +\end{minipage}} +\end{center} +\caption{Type isomorphism tactic (2)} +\label{isosltac2} +\end{figure} + +Figure~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}. + +\begin{figure} +\begin{center} +\fbox{\begin{minipage}{0.95\textwidth} +\begin{coq_example*} +Lemma isos_ex1 : + forall A B:Set, A * unit * B = B * (unit * A). +Proof. +intros; IsoProve. +Qed. + +Lemma isos_ex2 : + forall A B C:Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). +Proof. +intros; IsoProve. +Qed. +\end{coq_example*} +\end{minipage}} +\end{center} +\caption{Type equalities solved by {\tt IsoProve}} +\label{isoslem} +\end{figure} + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: |