\chapter{The tactic language}
\label{TacticLanguage}

% Très très provisoire
% À articuler notamment avec le chapitre "Tactiques utilisateurs"

%\geometry{a4paper,body={5in,8in}}

This chapter gives a compact documentation of the tactic language available in
the toplevel of {\Coq}. We start by giving the syntax and, next, we present the
informal semantic. Finally, we show some examples which deal with small but
also with non-trivial problems. If you want to know more regarding this
language and especially about its fundations, you can refer to~\cite{Del00}.

\section{Syntax}

\def\tacexpr{\textrm{\textsl{expr}}}
\def\tacexprinf{\textrm{\textsl{tacexpr$_i$}}}
\def\tacexprpref{\textrm{\textsl{tacexpr$_p$}}}
\def\atom{\textrm{\textsl{atom}}}
\def\inputfun{\textrm{\textsl{input\_fun}}}
\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\primitivetactic{\textrm{\textsl{primitive\_tactic}}}
\def\tacarg{\textrm{\textsl{arg}}}

The syntax of the tactic language is given in table~\ref{ltac}.
% We use a \bn{}-like notation. 
Terminal symbols are set in 
%sans serif font ({\sf like this}).
typewriter font ({\tt like this}).
Non-terminal symbols are set in italic font ($like\sm{}that$). ... {\it
|} ... denotes the or operation. \nelist{$entry$}{} denotes one or several
repetitions of entry $entry$. \nelist{$entry$}{$sep$} denotes one or several repetitions separated by $sep$. 
%Parentheses {\it (}...{\it )} denote grouping. 
The main entry is {\tacexpr} and the entries {\naturalnumber}, {\integer},
{\ident}, {\qualid}, {\term}, {\pattern} and {\primitivetactic} represent respectively the natural and integer
numbers, the authorized identificators and qualified names, {\Coq}'s terms and patterns and all the basic
tactics. In {\pattern}, there can be specific variables like {\tt ?n} where {\tt n}
is a {\naturalnumber} or {\tt ?}, which are metavariables for pattern matching. {\tt ?n}
allows us to keep instantiations and to make constraints whereas {\tt ?} shows
that we are not interested in what will be matched.

This language is used in proof mode but it can also be used in toplevel
definitions as shown in table~\ref{ltactop}.

\begin{table}[htbp]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{center}
\begin{tabular}{lp{0.1in}l}
{\tacexpr} & \cn{}::= & {\tacexpr} {\tt ;} {\tacexpr}\\
& \cn{}| & {\tacexpr} {\tt ; [} \nelist{\tacexpr}{|} {\tt ]}\\
& \cn{}| & {\tacexprpref}\\
\\
{\tacexprpref} & \cn{}::= & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} {\tacexprpref}\\
& \cn{}| & {\tt Repeat} {\tacexprpref}\\
& \cn{}| & {\tt Try} {\tacexprpref}\\
& \cn{}| & {\tt Progress} {\tacexprpref}\\
& \cn{}| & {\tt Info} {\tacexprpref}\\
& \cn{}| & {\tacexprinf} \\
\\
{\tacexprinf} & \cn{}::= & {\atom} {\tt Orelse} {\tacexprpref}\\
& \cn{}| & {\atom}\\
\\
{\atom} & \cn{}::= & {\tt Fun} \nelist{\ident}{} {\tt ->} {\tacexpr}\\
& \cn{}| &
{\tt Let} \nelist{\letclause}{\tt And} {\tt In}
{\tacexpr}\\
% & \cn{}| & {\tt Rec} {\recclause}\\
& \cn{}| &
{\tt Rec} \nelist{\recclause}{\tt And} {\tt In}
{\tacexpr}\\
& \cn{}| &
{\tt Match Context With} \nelist{\contextrule}{\tt |}\\
& \cn{}| &
{\tt Match} {\term} {\tt With} \nelist{\matchrule}{\tt |}\\
& \cn{}| & {\tt (} {\tacexpr} {\tt )}\\
& \cn{}| & {\tt (} {\qualid} \nelist{\tacarg}{} {\tt )}\\
& \cn{}| & {\tt First [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
& \cn{}| & {\tt Solve [} \nelist{\tacexpr}{\tt |} {\tt ]}\\
& \cn{}| & {\tt Idtac}\\
& \cn{}| & {\tt Fail} ~|~ {\tt Fail} {\naturalnumber}\\
& \cn{}| & \primitivetactic\\
& \cn{}| & \tacarg\\
\\
%{\inputfun} & \cn{}::= & {\ident}\\
%& \cn{}| & {\tt ()}\\
%\\
\letclause & \cn{}::= & {\ident} {\tt =} {\tacarg}\\
\\
\recclause & \cn{}::= & {\ident} \nelist{\ident}{} {\tt ->} {\tacexpr}\\
\\
\contextrule & \cn{}::= &
{\tt [} \nelist{\contexthyps}{\tt ;} {\tt |-}
{\pattern} {\tt ] ->} {\tacexpr}\\
& \cn{}| & {\tt [ |-} {\pattern} {\tt ] ->} {\tacexpr}\\
& \cn{}| & {\tt \_ ->} {\tacexpr}\\
\\
\contexthyps & \cn{}::= & {\ident} {\tt :} {\pattern}\\
& \cn{}| & {\tt \_ :} {\pattern}\\
\\
\matchrule & \cn{}::= & {\tt [} {\pattern} {\tt ] ->} {\tacexpr}\\
& \cn{}| & {\tt \_ ->} {\tacexpr}\\
\\
\tacarg 
%& \cn{}::= & {\tt ()}\\
& \cn{}| & {integer}\\
& \cn{}| & {\ident}\\
& \cn{}| & {\tt '}{\term}\\
& \cn{}| & {\tacexpr}\\
\end{tabular}
\end{center}}}
\caption{Syntax of the tactic language}
\label{ltac}
\end{table}

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{center}
\begin{tabular}{lp{0.1in}l}
$top$ & \cn{}::= & {\tt Tactic Definition} {\ident} \nelist{\ident}{} {\tt :=}
{\tacexpr} \\
& \cn{}| & {\tt Recursive Tactic Definition} \nelist{$trec\_clause$}{\tt
And}\\
\\
$trec\_clause$ & \cn{}::= & {\ident} \nelist{\ident}{} {\tt :=} {\tacexpr}
\end{tabular}
\end{center}}}
\caption{Tactic toplevel definitions}
\label{ltactop}
\end{table}

\section{Semantics}

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 Context} 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).

%% \subsection{Values}

%% Values are given by table~\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{table}[ht]
%% \noindent{}\framebox[6in][l]
%% {\parbox{6in}
%% {\begin{center}
%% \begin{tabular}{lp{0.1in}l}
%% $vexpr$ & \cn{}::= & $vexpr$ {\tt ;} $vexpr$\\
%% & \cn{}| & $vexpr$ {\tt ; [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt
%% ]}\\
%% & \cn{}| & $vatom$\\
%% \\
%% $vatom$ & \cn{}::= & {\tt Fun} \nelist{\inputfun}{}  {\tt ->} {\tacexpr}\\
%% %& \cn{}| & {\tt Rec} \recclause\\
%% & \cn{}| &
%% {\tt Rec} \nelist{\recclause}{\tt And} {\tt In}
%% {\tacexpr}\\
%% & \cn{}| &
%% {\tt Match Context With} {\it (}$context\_rule$ {\tt |}{\it )}$^*$
%% $context\_rule$\\
%% & \cn{}| & {\tt (} $vexpr$ {\tt )}\\
%% & \cn{}| & $vatom$ {\tt Orelse} $vatom$\\
%% & \cn{}| & {\tt Do} {\it (}{\naturalnumber} {\it |} {\ident}{\it )} $vatom$\\
%% & \cn{}| & {\tt Repeat} $vatom$\\
%% & \cn{}| & {\tt Try} $vatom$\\
%% & \cn{}| & {\tt First [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
%% & \cn{}| & {\tt Solve [} {\it (}$vexpr$ {\tt |}{\it )}$^*$ $vexpr$ {\tt ]}\\
%% & \cn{}| & {\tt Idtac}\\
%% & \cn{}| & {\tt Fail}\\
%% & \cn{}| & {\primitivetactic}\\
%% & \cn{}| & $arg$
%% \end{tabular}
%% \end{center}}}
%% \caption{Values of ${\cal L}_{tac}$}
%% \label{ltacval}
%% \end{table}

%% \subsection{Evaluation}

\subsubsection{Local definitions}

Local definitions can be done as follows:

%\newpage{}

%\phantom{}
%\vfill{}

\begin{tabular}{l}
{\tt Let} {\ident}$_1$ {\tt =} {\tacexpr}$_1$\\
{\tt And} {\ident}$_2$ {\tt =} {\tacexpr}$_2$\\
...\\
{\tt And} {\ident}$_n$ {\tt =} {\tacexpr}$_n$ {\tt In}\\
{\tacexpr}
\end{tabular}

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$.

\subsubsection{Pattern matching on terms}

We can carry out pattern matching on terms with:

\begin{tabular}{l}
{\tt Match} {\term} {\tt With}\\
~~~{\pattern}$_1$ {\tt ->} {\tacexpr}$_1$\\
~{\tt |} {\pattern}$_2$ {\tt ->} {\tacexpr}$_2$\\
~...\\
~{\tt |} {\pattern}$_n$ {\tt ->} {\tacexpr}$_n$\\
~{\tt |} {\tt \_} {\tt ->} {\tacexpr}$_{n+1}$
\end{tabular}

the {\term} is matched (non-linear first order unification) against
{\pattern}$_1$ then {\tacexpr}$_1$ is evaluated into some value by
substituting the pattern matching instantiations to the
metavariables. If the matching with {\pattern}$_1$ fails,
{\pattern}$_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 Context}). If all clauses fail (in
particular, there is no pattern {\_}) then a no-matching error is
raised. \\

{\tt Error message:}\\

{\tt No matching clauses for Match}

\hx{4}No pattern can be used and, in particular, there is no {\tt \_} pattern.

\subsubsection{Application}

An application is an expression of the following form:\\

{\tt (} {\qualid} {\tacexpr}$_1$ ... {\tacexpr}$_n$ {\tt )}\\

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{Sequence}

A sequence is an expression of the following form:\\

{\tacexpr}$_1$ {\tt ;} {\tacexpr}$_2$\\

{\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 the subgoals
generated by the application of $v_1$. Sequence is left associating.

\subsubsection{General sequence}

We can generalize the previous sequence operator by:\\

{\tacexpr}$_0$ {\tt ; [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\

{\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{Branching}

We can easily branch with the following structure:\\

{\tacexpr}$_1$ {\tt Orelse} {\tacexpr}$_2$\\

{\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{For loop}

We have a for loop with:\\

{\tt Do} $n$ {\tacexpr}\\

{\tacexpr} is evaluated to $v$. $v$ must be a tactic value. $v$ is applied $n$
times. Supposing $n>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 $n$ applications have been completed.

\subsubsection{Repeat loop}

We have a repeat loop with:\\

{\tt Repeat} {\tacexpr}\\

{\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}

We can catch the tactic errors with:\\

{\tt Try} {\tacexpr}\\

{\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.
It never fails.

\subsubsection{First tactic to work}

We may consider the first tactic to work (i.e. which does not fail) among a
panel of tactics:\\

{\tt First [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\

{\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.\\

{\tt Error message:}\\

{\tt No applicable tactic}

\subsubsection{Solving}

We may consider the first to solve (i.e. which generates no subgoal) among a
panel of tactics:\\

{\tt Solve [} {\tacexpr}$_1$ {\tt |} $...$ {\tt |} {\tacexpr}$_n$ {\tt ]}\\

{\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.\\

{\tt Error message:}\\

{\tt Cannot solve the goal}

\subsubsection{Identity}

We have the identity tactic:\\

{\tt Idtac}\\

It leaves the goal unchanged but it appears in the proof script.

\subsubsection{Failing}

We have the failing tactic:\\

{\tt Fail} and {\tt Fail $n$} \\

It always fails and leaves the goal unchanged. It does not appear in
the proof script and can be catched by {\tt Try}. The number $n$ is
the failure level. If no level is specified, it defaults to $0$.  The
level is used in {\tt Match Context}.  If $0$, it makes {\tt Match
Context} considering the next clause. If non zero, the current {\tt
Match Context} block is aborted and the level is decremented.

{\tt Error message:}\\

{\tt Fail tactic always fails (level $n$)}.

\subsubsection{Pattern matching on proof contexts}

We can make pattern matching on proof contexts using the following
expression:

\begin{tabular}{l}
{\tt Match Context With}\\
~~~{\tt [}$context\_hyps_{1,1}${\tt ;}...{\tt ;}$context\_hyps_{1,m_1}$
   ~~{\tt |-}{\pattern}$_1${\tt ] ->} {\tacexpr}$_1$\\
~~{\tt |[}$context\_hyps_{2,1}${\tt ;}...{\tt ;}$context\_hyps_{2,m_2}$
   ~~{\tt |-}{\pattern}$_2${\tt ] ->} {\tacexpr}$_2$\\
~~...\\
~~{\tt |[}$context\_hyps_{n,1}${\tt ;}...{\tt ;}$context\_hyps_{n,m_n}$
   ~~{\tt |-}{\pattern}$_n${\tt ] ->} {\tacexpr}$_n$\\
~~{\tt |\_}~~~~{\tt ->} {\tacexpr}$_{n+1}$
\end{tabular}

If each hypothesis pattern $context\_hyps_{1,i}$, with $i=1,...,m_1$ is matched
(non-linear first order unification) by an hypothesis of the goal and if
{\pattern}$_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.\\

{\tt Error message:}\\

{\tt No matching clauses for Match Context}

\hx{4}No proof context pattern can be used and, in particular, there is no {\tt
\_} proof

\hx{4}context pattern.

\subsection{Tactic toplevel definitions}

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:\\

{\tt Tactic Definition} {\ident} {\ident}$_1$ ... {\ident}$_n$ {\tt :=}
{\tacexpr}\\

\noindent 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:\\

{\tt Tactic Definition} {\ident} {\tt := Fun} {\ident}$_1$ ... {\ident}$_n$
{\tt ->} {\tacexpr}\\

\noindent Recursive and mutual recursive function definitions are also possible with the syntax:
\medskip

\begin{tabular}{l}
{\tt Recursive Tactic Definition} {\ident}$_1$ {\ident}$_{1,1}$ ...
{\ident}$_{1,m_1}$~~{\tt :=} {\tacexpr}$_1$\\
{\tt And} {\ident}$_2$ {\ident}$_{2,1}$ ... {\ident}$_{2,m_2}$~~{\tt :=}
{\tacexpr}$_2$\\
...\\
{\tt And} {\ident}$_n$ {\ident}$_{n,1}$ ... {\ident}$_{n,m_n}$~~{\tt :=}
{\tacexpr}$_n$
\end{tabular}

%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).

\section{Examples}

\subsection{About the cardinality of the natural number set}

A first example which shows how to use the pattern matching over the proof
contexts is the proof that natural numbers have more than two elements. The
proof of such a lemma can be done as shown in table~\ref{cnatltac}.

\begin{coq_eval}
Reset Initial.
Require Arith.
Require PolyList.
Require PolyListSyntax.
\end{coq_eval}

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example*}
Lemma card_nat: ~(EX x:nat|(EX y:nat|(z:nat)(x=z)/\(y=z))).
Proof.
Red;Intro H.
Elim H;Intros a Ha.
Elim Ha;Intros b Hb.
Elim (Hb (0));Elim (Hb (1));Elim (Hb (2));Intros;
  Match Context With
    [_:?1=?2;_:?1=?3|-?] ->
      Cut ?2=?3;[Discriminate|Apply trans_equal with ?1;Auto].
Qed.
\end{coq_example*}
}}
\caption{A proof on cardinality of natural numbers}
\label{cnatltac}
\end{table}

We can notice that all the (very similar) cases coming from the three
eliminations (with three distinct natural numbers) are successfully solved by
a {\tt Match Context} structure and, in particular, with only one pattern (use
of non-linear unification).

\subsection{Permutation on closed lists}

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 in table~\ref{permutpred}.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example*}
Section Sort.
Variable A:Set.

Inductive permut:(list A)->(list A)->Prop:=
  permut_refl:(l:(list A))(permut l l)
 |permut_cons:
    (a:A)(l0,l1:(list A))(permut l0 l1)->
      (permut (cons a l0) (cons a l1))
 |permut_append:
    (a:A)(l:(list A))(permut (cons a l) (l^(cons a (nil A))))
 |permut_trans:
    (l0,l1,l2:(list A))(permut l0 l1)->(permut l1 l2)->
      (permut l0 l2).
End Sort.
\end{coq_example*}
}}
\caption{Definition of the permutation predicate}
\label{permutpred}
\end{table}

Next, we can write naturally the tactic and the result can be seen in
table~\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. In table~\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}.
 
\begin{table}[p]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example}
Recursive Tactic Definition Permut n:=
 Match Context With
   [|-(permut ? ?1 ?1)] -> Apply permut_refl
  |[|-(permut ? (cons ?1 ?2) (cons ?1 ?3))] ->
     Let newn=Eval Compute in (length ?2) In
     Apply permut_cons;(Permut newn)
  |[|-(permut ?1 (cons ?2 ?3) ?4)] ->
     (Match Eval Compute in n With
        [(1)] -> Fail
       |_ ->
         Let l0'='(?3^(cons ?2 (nil ?1))) In
         Apply (permut_trans ?1 (cons ?2 ?3) l0' ?4);
         [Apply permut_append|
          Compute;(Permut '(pred n))]).

Tactic Definition PermutProve:=
 Match Context With
   [|-(permut ? ?1 ?2)] ->
     (Match Eval Compute in ((length ?1)=(length ?2)) With
        [?1=?1] -> (Permut ?1)).
\end{coq_example}
}}
\caption{Permutation tactic}
\label{permutltac}
\end{table}

With {\tt PermutProve}, we can now prove lemmas such those shown in
table~\ref{permutlem}.

\begin{table}[p]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example*}
Lemma permut_ex1:
  (permut nat (cons (1) (cons (2) (cons (3) (nil nat))))
     (cons (3) (cons (2) (cons (1) (nil nat))))).
Proof.
PermutProve.
Save.

Lemma permut_ex2:
 (permut nat
   (cons (0) (cons (1) (cons (2) (cons (3) (cons (4) (cons (5)
     (cons (6) (cons (7) (cons (8) (cons (9) (nil nat)))))))))))
   (cons (0) (cons (2) (cons (4) (cons (6) (cons (8) (cons (9)
     (cons (7) (cons (5) (cons (3) (cons (1) (nil nat)))))))))))).
Proof.
PermutProve.
Save.
\end{coq_example*}
}}
\caption{Examples of {\tt PermutProve} use}
\label{permutlem}
\end{table}

\subsection{Deciding intuitionistic propositional logic}

The pattern matching on proof contexts 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 as shown in
table~\ref{tautoltac}. The tactic {\tt Axioms} tries to conclude using usual
axioms. The tactic {\tt DSimplif} applies all the reversible rules of Dyckhoff's
system. Finally, the tactic {\tt TautoProp} (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{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example}
Tactic Definition Axioms:=
  Match Context With
   [|-True] -> Trivial
  |[_:False|- ?] -> ElimType False;Assumption
  |[_:?1|-?1] -> Auto.

Tactic Definition DSimplif:=
 Repeat
  (Intros;
   (Match Context With
     [id:~?|-?] -> Red in id
    |[id:?/\?|-?] -> Elim id;Do 2 Intro;Clear id
    |[id:?\/?|-?] -> Elim id;Intro;Clear id
    |[id:?1/\?2->?3|-?] ->
       Cut ?1->?2->?3;[Intro|Intros;Apply id;Split;Assumption]
    |[id:?1\/?2->?3|-?] ->
       Cut ?2->?3;[Cut ?1->?3;[Intros|
                               Intro;Apply id;Left;Assumption]|
                   Intro;Apply id;Right;Assumption]
    |[id0:?1->?2;id1:?1|-?] ->
       Cut ?2;[Intro;Clear id0|Apply id0;Assumption]
    |[|-?/\?] -> Split
    |[|-~?] -> Red)).

Recursive Tactic Definition TautoProp:=
  DSimplif;
   Axioms
   Orelse
   Match Context With
    [id:(?1->?2)->?3|-?] ->
      Cut ?2->?3;[Intro;Cut ?1->?2;[Intro;Cut ?3;[Intro;Clear id|
                              Apply id;Assumption]|Clear id]|
                  Intro;Apply id;Intro;Assumption];TautoProp
   |[id:~?1->?2|-?]->
      Cut False->?2;
      [Intro;Cut ?1->False;[Intro;Cut ?2;[Intro;Clear id|
                               Apply id;Assumption]|Clear id]|
       Intro;Apply id;Red;Intro;Assumption];TautoProp
   |[|-?\/?] ->
      (Left;TautoProp) Orelse (Right;TautoProp).
\end{coq_example}
}}
\caption{Deciding intuitionistic propositions}
\label{tautoltac}
\end{table}

For example, with {\tt TautoProp}, we can prove tautologies like those in
table~\ref{tautolem}.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example*}
Lemma tauto_ex1:(A,B:Prop)A/\B->A\/B.
Proof.
TautoProp.
Save.

Lemma tauto_ex2:(A,B:Prop)(~~B->B)->(A->B)->~~A->B.
Proof.
TautoProp.
Save.
\end{coq_example*}
}}
\caption{Proofs of tautologies with {\tt TautoProp}}
\label{tautolem}
\end{table}

\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
table~\ref{isosax}.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_eval}
Reset Initial.
Require Arith.
\end{coq_eval}
\begin{coq_example*}
Section Iso_axioms.

Variable 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_eqT.
Save.

End Iso_axioms.
\end{coq_example*}
}}
\caption{Type isomorphism axioms}
\label{isosax}
\end{table}

The tactic to judge equalities modulo this axiomatization can be written as
shown in tables~\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{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example}
Recursive Tactic Definition DSimplif trm:=
  Match trm With
   [(?1*?2)*?3] -> Rewrite <- (Ass ?1 ?2 ?3);Try MainSimplif
  |[(?1*?2)->?3] -> Rewrite (Cur ?1 ?2 ?3);Try MainSimplif
  |[?1->(?2*?3)] -> Rewrite (Dis ?1 ?2 ?3);Try MainSimplif
  |[?1*unit] -> Rewrite (P_unit ?1);Try MainSimplif
  |[unit*?1] -> Rewrite (Com unit ?1);Try MainSimplif
  |[?1->unit] -> Rewrite (AR_unit ?1);Try MainSimplif
  |[unit-> ?1] -> Rewrite (AL_unit ?1);Try MainSimplif
  |[?1*?2] ->
     ((DSimplif ?1);Try MainSimplif) Orelse
     ((DSimplif ?2);Try MainSimplif)
  |[?1-> ?2] ->
     ((DSimplif ?1);Try MainSimplif) Orelse
     ((DSimplif ?2);Try MainSimplif)
And MainSimplif:=
  Match Context With
   [|- ?1== ?2] -> Try (DSimplif ?1);Try (DSimplif ?2).

Recursive Tactic Definition Length trm:=
  Match trm With
   [?*?1] ->
     Let succ=(Length ?1) In
     '(S succ)
  |_ -> '(1).

Tactic Definition Assoc:= Repeat Rewrite <- Ass.
\end{coq_example}
}}
\caption{Type isomorphism tactic (1)}
\label{isosltac1}
\end{table}

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example}
Recursive Tactic Definition DoCompare n:=
  Match Context With
   [|-?1==?1] -> Apply refl_eqT
  |[|-(?1*?2)==(?1*?3)] ->
     Apply Cons;
     Let newn=(Length ?2) In
     (DoCompare newn)
  |[|-(?1*?2)==?3] ->
     (Match Eval Compute in n With
       [(1)] -> Fail
      |_ -> 
        Pattern 1 (?1*?2);Rewrite Com;Assoc;
        (DoCompare '(pred n))).

Tactic Definition CompareStruct:=
  Match Context With
   [|-?1==?2] ->
     Let l1=(Length ?1)
     And l2=(Length ?2) In
     (Match Eval Compute in l1=l2 With
        [?1=?1] -> (DoCompare ?1)).

Tactic Definition IsoProve:=MainSimplif;CompareStruct.
\end{coq_example}
}}
\caption{Type isomorphism tactic (2)}
\label{isosltac2}
\end{table}

Table~\ref{isoslem} gives examples of what can be solved by {\tt IsoProve}.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{
\begin{coq_example*}
Lemma isos_ex1:(A,B:Set)((A*unit)*B)==(B*(unit*A)).
Proof.
Intros;IsoProve.
Save.

Lemma isos_ex2:(A,B,C:Set)
  ((A*unit)->(B*C*unit))==
  (((A*unit)->((C->unit)*C))*(unit->(A->B))).
Proof.
Intros;IsoProve.
Save.
\end{coq_example*}
}}
\caption{Type equalities solved by {\tt IsoProve}}
\label{isoslem}
\end{table}