diff options
Diffstat (limited to 'doc/refman/RefMan-ltac.tex')
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 1308 |
1 files changed, 0 insertions, 1308 deletions
diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex deleted file mode 100644 index d8747254..00000000 --- a/doc/refman/RefMan-ltac.tex +++ /dev/null @@ -1,1308 +0,0 @@ -\chapter[The tactic language]{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 foundations, 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\contexthyp{\textrm{\textsl{context\_hyp}}} -\def\tacarg{\nterm{tacarg}} -\def\cpattern{\nterm{cpattern}} - -The syntax of the tactic language is given Figures~\ref{ltac} -and~\ref{ltac_aux}. See Chapter~\ref{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 it is extended with pattern matching metavariables. In -{\cpattern}, a pattern-matching metavariable is represented with the -syntax {\tt ?id} where {\tt id} is an {\ident}. The notation {\tt \_} -can also be used to denote metavariable whose instance is -irrelevant. In the notation {\tt ?id}, the identifier 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 of pattern-matching clauses, the named metavariable are used -without the question mark prefix. There is also a special notation for -second-order pattern-matching problems: in an applicative pattern of -the form {\tt @?id id$_1$ \ldots id$_n$}, the variable {\tt id} -matches any complex expression with (possible) dependencies in the -variables {\tt id$_1$ \ldots id$_n$} and returns a functional term of -the form {\tt fun id$_1$ \ldots id$_n$ => {\term}}. - - -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 In {\tacarg}, there is an overlap between {\qualid} as a -direct tactic argument and {\qualid} as a particular case of -{\term}. The resolution is done by first looking for a reference of -the tactic language and if it fails, for a reference to a term. To -force the resolution as a reference of the tactic language, use the -form {\tt ltac :} {\qualid}. To force the resolution as a reference to -a term, use the syntax {\tt ({\qualid})}. - -\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} \zeroone{\tt rec} \nelist{\letclause}{\tt with} {\tt in} -{\atom}\\ -& | & -{\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 lazymatch goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ -& | & -{\tt lazymatch reverse goal with} \nelist{\contextrule}{\tt |} {\tt end}\\ -& | & -{\tt lazymatch} {\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} \sequence{\messagetoken}{}\\ -& | & {\tt fail} \zeroone{\naturalnumber} \sequence{\messagetoken}{}\\ -& | & {\tt fresh} ~|~ {\tt fresh} {\qstring}\\ -& | & {\tt context} {\ident} {\tt [} {\term} {\tt ]}\\ -& | & {\tt eval} {\nterm{redexpr}} {\tt in} {\term}\\ -& | & {\tt type of} {\term}\\ -& | & {\tt external} {\qstring} {\qstring} \nelist{\tacarg}{}\\ -& | & {\tt constr :} {\term}\\ -& | & \atomictac\\ -& | & {\qualid} \nelist{\tacarg}{}\\ -& | & {\atom}\\ -\\ -{\atom} & ::= & - {\qualid} \\ -& | & ()\\ -& | & {\integer}\\ -& | & {\tt (} {\tacexpr} {\tt )}\\ -\\ -{\messagetoken}\!\!\!\!\!\! & ::= & {\qstring} ~|~ {\ident} ~|~ {\integer} \\ -\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}\\ -\\ -\contextrule & ::= & - \nelist{\contexthyp}{\tt ,} {\tt |-}{\cpattern} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt |-} {\cpattern} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt \_ =>} {\tacexpr}\\ -\\ -\contexthyp & ::= & {\name} {\tt :} {\cpattern}\\ - & $|$ & {\name} {\tt :=} {\cpattern} \zeroone{{\tt :} {\cpattern}}\\ -\\ -\matchrule & ::= & - {\cpattern} {\tt =>} {\tacexpr}\\ -& $|$ & {\tt context} {\zeroone{\ident}} {\tt [} {\cpattern} {\tt ]} - {\tt =>} {\tacexpr}\\ -& $|$ & {\tt appcontext} {\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} & ::= & \zeroone{\tt Local} {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\ -\\ -\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} -{\tacexpr}\\ -& $|$ &{\qualid} \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 non recursive 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]{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} -The expressions {\tacexpr}$_1$ and {\tacexpr}$_2$ are evaluated -to $v_1$ and $v_2$ which have to be tactic values. The tactic $v_1$ is -then applied and $v_2$ is applied to every subgoal generated by the -application of $v_1$. Sequence is left-associative. - -\subsubsection[General sequence]{General sequence\tacindex{;[\ldots$\mid$\ldots$\mid$\ldots]}} -%\tacindex{; [ | ]} -%\index{; [ | ]@{\tt ;[\ldots$\mid$\ldots$\mid$\ldots]}} -\index{Tacticals!; [ \mid ]@{\tt {\tac$_0$};[{\tac$_1$}$\mid$\ldots$\mid$\tac$_n$]}} - -A general sequence has the following form: -\begin{quote} -{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} -{\tacexpr}$_n$ {\tt ]} -\end{quote} -The expressions {\tacexpr}$_i$ are evaluated to $v_i$, for $i=0,...,n$ -and all have to be tactics. The tactic $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. - -\begin{Variants} - \item If no tactic is given for the $i$-th generated subgoal, it -behaves as if the tactic {\tt idtac} were given. For instance, {\tt -split ; [ | auto ]} is a shortcut for -{\tt split ; [ idtac | auto ]}. - - \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} - {\tacexpr}$_i$ {\tt |} {\tt ..} {\tt |} {\tacexpr}$_{i+1+j}$ {\tt |} - $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} - - In this variant, {\tt idtac} is used for the subgoals numbered from - $i+1$ to $i+j$ (assuming $n$ is the number of subgoals). - - Note that {\tt ..} is part of the syntax, while $...$ is the meta-symbol used - to describe a list of {\tacexpr} of arbitrary length. - - \item {\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} - {\tacexpr}$_i$ {\tt |} {\tacexpr} {\tt ..} {\tt |} - {\tacexpr}$_{i+1+j}$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]} - - In this variant, {\tacexpr} is used instead of {\tt idtac} for the - subgoals numbered from $i+1$ to $i+j$. - -\end{Variants} - - - -\subsubsection[For loop]{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]{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$. If $v$ denotes a tactic, this tactic -is applied to the goal. If the application fails, the tactic is -applied recursively to all the generated subgoals until it eventually -fails. The recursion stops in a subgoal when the tactic has failed. -The tactic {\tt repeat {\tacexpr}} itself never fails. - -\subsubsection[Error catching]{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]{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]{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 to progress then $v_2$ is applied. Branching is left-associative. - -\subsubsection[First tactic to work]{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]{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]{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. - -\variant {\tt idtac \nelist{\messagetoken}{}} - -This prints the given tokens. Strings and integers are printed -literally. If a (term) variable is given, its contents are printed. - - -\subsubsection[Failing]{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}. - -\begin{Variants} -\item {\tt fail $n$}\\ -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. - -\item {\tt fail \nelist{\messagetoken}{}}\\ -The given tokens are used for printing the failure message. - -\item {\tt fail $n$ \nelist{\messagetoken}{}}\\ -This is a combination of the previous variants. -\end{Variants} - -\ErrMsg \errindex{Tactic Failure {\it message} (level $n$)}. - -\subsubsection[Local definitions]{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}. In this latter case, the definitions are evaluated lazily -so that the {\tt rec} keyword can be used also in non recursive cases -so as to avoid the eager evaluation of local definitions. - -\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]{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]{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 expression {\tacexpr} is evaluated and should yield a term which -is matched against {\cpattern}$_1$. The matching is non-linear: if a -metavariable occurs more than once, it should match the same -expression every time. It is first-order except on the -variables of the form {\tt @?id} that occur in head position of an -application. For these variables, the matching is second-order and -returns a functional term. - -If the matching with {\cpattern}$_1$ succeeds, then {\tacexpr}$_1$ is -evaluated into some value by substituting the pattern matching -instantiations to the metavariables. If {\tacexpr}$_1$ evaluates to a -tactic and the {\tt match} expression is in position to be applied to -a goal (e.g. it is not bound to a variable by a {\tt let in}), then -this tactic is applied. If the tactic succeeds, the list of resulting -subgoals is the result of the {\tt match} expression. If -{\tacexpr}$_1$ does not evaluate to a tactic or if the {\tt match} -expression is not in position to be applied to a goal, then the result -of the evaluation of {\tacexpr}$_1$ is the result of the {\tt match} -expression. - -If the matching with {\cpattern}$_1$ fails, or if it succeeds but the -evaluation of {\tacexpr}$_1$ fails, or if the evaluation of -{\tacexpr}$_1$ succeeds but returns a tactic in execution position -whose execution fails, then {\cpattern}$_2$ is used and so on. The -pattern {\_} matches any term and shunts all remaining patterns if -any. If all clauses fail (in particular, there is no pattern {\_}) -then a no-matching-clause 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} - -\begin{Variants} - -\item \index{lazymatch!in Ltac} -\index{Ltac!lazymatch} -Using {\tt lazymatch} instead of {\tt match} has an effect if the -right-hand-side of a clause returns a tactic. With {\tt match}, the -tactic is applied to the current goal (and the next clause is tried if -it fails). With {\tt lazymatch}, the tactic is directly returned as -the result of the whole {\tt lazymatch} block without being first -tried to be applied to the goal. Typically, if the {\tt lazymatch} -block is bound to some variable $x$ in a {\tt let in}, then tactic -expression gets bound to the variable $x$. - -\item \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. - -If the evaluation of the right-hand-side of a valid match fails, the -next matching subterm is tried. If no further subterm matches, the -next clause is tried. Matching subterms are considered top-bottom and -from left to right (with respect to the raw printing obtained by -setting option {\tt Printing All}, see Section~\ref{SetPrintingAll}). - -\begin{coq_example} -Ltac f x := - match x with - context f [S ?X] => - idtac X; (* To display the evaluation order *) - assert (p := refl_equal 1 : X=1); (* To filter the case X=1 *) - let x:= context f[O] in assert (x=O) (* To observe the context *) - end. -Goal True. -f (3+4). -\end{coq_example} - -\item \index{appcontext!in pattern} -For historical reasons, {\tt context} considers $n$-ary applications -such as {\tt (f 1 2)} as a whole, and not as a sequence of unary -applications {\tt ((f 1) 2)}. Hence {\tt context [f ?x]} will fail -to find a matching subterm in {\tt (f 1 2)}: if the pattern is a partial -application, the matched subterms will be necessarily be -applications with exactly the same number of arguments. -Alternatively, one may now use the following variant of {\tt context}: -\begin{quote} -{\tt appcontext} {\ident} {\tt [} {\cpattern} {\tt ]} -\end{quote} -The behavior of {\tt appcontext} is the same as the one of {\tt - context}, except that a matching subterm could be a partial -part of a longer application. For instance, in {\tt (f 1 2)}, -an {\tt appcontext [f ?x]} will find the matching subterm {\tt (f 1)}. - -\end{Variants} - -\subsubsection[Pattern matching on goals]{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} - -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. Note also that matching against subterms (using the {\tt -context} {\ident} {\tt [} {\cpattern} {\tt ]}) is available and may -itself induce extra backtrackings. - -\ErrMsg \errindex{No matching clauses for match goal} - -No clause succeeds, i.e. all matching patterns, if any, -fail at the application of the right-hand-side. - -\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. - -\variant -\index{lazymatch goal!in Ltac} -\index{Ltac!lazymatch goal} -\index{lazymatch reverse goal!in Ltac} -\index{Ltac!lazymatch reverse goal} -Using {\tt lazymatch} instead of {\tt match} has an effect if the -right-hand-side of a clause returns a tactic. With {\tt match}, the -tactic is applied to the current goal (and the next clause is tried if -it fails). With {\tt lazymatch}, the tactic is directly returned as -the result of the whole {\tt lazymatch} block without being first -tried to be applied to the goal. Typically, if the {\tt lazymatch} -block is bound to some variable $x$ in a {\tt let in}, then tactic -expression gets bound to the variable $x$. - -\begin{coq_example} -Ltac test_lazy := - lazymatch goal with - | _ => idtac "here"; fail - | _ => idtac "wasn't lazy"; trivial - end. -Ltac test_eager := - match goal with - | _ => idtac "here"; fail - | _ => idtac "wasn't lazy"; trivial - end. -Goal True. -test_lazy || idtac "was lazy". -test_eager || idtac "was lazy". -\end{coq_example} - -\subsubsection[Filling a term context]{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]{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. -The following expression returns an identifier: -\begin{quote} -{\tt fresh} \nelist{\textrm{\textsl{component}}}{} -\end{quote} -It evaluates to an identifier unbound in the goal. This fresh -identifier is obtained by concatenating the value of the -\textrm{\textsl{component}}'s (each of them is, either an {\ident} which -has to refer to a name, or directly a name denoted by a -{\qstring}). If the resulting name is already used, it is padded -with a number so that it becomes fresh. If no component is -given, the name is a fresh derivative of the name {\tt H}. - -\subsubsection[Computing in a constr]{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{Type-checking a term} -%\tacindex{type of} -\index{Ltac!type of} -\index{type of!in Ltac} - -The following returns the type of {\term}: - -\begin{quote} -{\tt type of} {\term} -\end{quote} - -\subsubsection[Accessing tactic decomposition]{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]{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} - -\subsubsection[Calling an external tactic]{Calling an external tactic\index{Ltac!external}} - -The tactic {\tt external} allows to run an executable outside the -{\Coq} executable. The communication is done via an XML encoding of -constructions. The syntax of the command is - -\begin{quote} -{\tt external} "\textsl{command}" "\textsl{request}" \nelist{\tacarg}{} -\end{quote} - -The string \textsl{command}, to be interpreted in the default -execution path of the operating system, is the name of the external -command. The string \textsl{request} is the name of a request to be -sent to the external command. Finally the list of tactic arguments -have to evaluate to terms. An XML tree of the following form is sent -to the standard input of the external command. -\medskip - -\begin{tabular}{l} -\texttt{<REQUEST req="}\textsl{request}\texttt{">}\\ -the XML tree of the first argument\\ -{\ldots}\\ -the XML tree of the last argument\\ -\texttt{</REQUEST>}\\ -\end{tabular} -\medskip - -Conversely, the external command must send on its standard output an -XML tree of the following forms: - -\medskip -\begin{tabular}{l} -\texttt{<TERM>}\\ -the XML tree of a term\\ -\texttt{</TERM>}\\ -\end{tabular} -\medskip - -\noindent or - -\medskip -\begin{tabular}{l} -\texttt{<CALL uri="}\textsl{ltac\_qualified\_ident}\texttt{">}\\ -the XML tree of a first argument\\ -{\ldots}\\ -the XML tree of a last argument\\ -\texttt{</CALL>}\\ -\end{tabular} - -\medskip -\noindent where \textsl{ltac\_qualified\_ident} is the name of a -defined {\ltac} function and each subsequent XML tree is recursively a -\texttt{CALL} or a \texttt{TERM} node. - -The Document Type Definition (DTD) for terms of the Calculus of -Inductive Constructions is the one developed as part of the MoWGLI -European project. It can be found in the file {\tt dev/doc/cic.dtd} of -the {\Coq} source archive. - -An example of parser for this DTD, written in the Objective Caml - -Camlp4 language, can be found in the file {\tt parsing/g\_xml.ml4} of -the {\Coq} source archive. - -\section[Tactic toplevel definitions]{Tactic toplevel definitions\comindex{Ltac}} - -\subsection{Defining {\ltac} functions} - -Basically, {\ltac} 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 {\ltac} function that can be used in any tactic -script or new {\ltac} 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} -\medskip -It is also possible to \emph{redefine} an existing user-defined tactic -using the syntax: -\begin{quote} -{\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=} -{\tacexpr} -\end{quote} -A previous definition of \qualid must exist in the environment. -The new definition will always be used instead of the old one and -it goes accross module boundaries. - -If preceded by the keyword {\tt Local} the tactic definition will not -be exported outside the current module. - -\subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}} - -Defined {\ltac} functions can be displayed using the command - -\begin{quote} -{\tt Print Ltac {\qualid}.} -\end{quote} - -\section[Debugging {\ltac} tactics]{Debugging {\ltac} tactics\comindex{Set Ltac Debug} -\comindex{Unset Ltac Debug} -\comindex{Test Ltac Debug}} - -The {\ltac} interpreter comes with a step-by-step debugger. The -debugger can be activated using the command - -\begin{quote} -{\tt Set Ltac Debug.} -\end{quote} - -\noindent and deactivated using the command - -\begin{quote} -{\tt Unset Ltac Debug.} -\end{quote} - -To know if the debugger is on, use the command \texttt{Test Ltac Debug}. -When the debugger is activated, it stops at every step of the -evaluation of the current {\ltac} expression and it prints information -on what it is doing. The debugger stops, prompting for a command which -can be one of the following: - -\medskip -\begin{tabular}{ll} -simple newline: & go to the next step\\ -h: & get help\\ -x: & exit current evaluation\\ -s: & continue current evaluation without stopping\\ -r$n$: & advance $n$ steps further\\ -\end{tabular} -\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: |