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

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}). Non-terminal symbols are set in italic font ($like\sm{}that$). ... {\it
|} ... denotes the or operation. ...$^*$ denotes zero, one or several
repetitions. ...$^+$ denotes one or several repetitions. Parentheses {\it
(}...{\it )} denote grouping. The main entry is $expr$ and the entries $nat$,
$ident$, $term$ and $primitive\_tactic$ represent respectively the natural
numbers, the authorized identificators, {\Coq}'s terms and all the basic
tactics. In $term$, there can be specific variables like {\sf ?n} where {\sf n}
is a $nat$ or {\sf ?}, which are metavariables for pattern matching. {\sf ?n}
allows us to keep instantiations and to make constraints whereas {\sf ?} 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}
$expr$ & \cn{}::= & $expr$ {\sf ;} $expr$\\
& \cn{}| & $expr$ {\sf ; [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
& \cn{}| & $atom$\\
\\
$atom$ & \cn{}::= & {\sf Fun} $input\_fun^+$  {\sf ->} $expr$\\
& \cn{}| &
{\sf Let} {\it (}$let\_clause$ {\sf And}{\it )}$^*$ $let\_clause$ {\sf In}
$expr$\\
& \cn{}| & {\sf Rec} $rec\_clause$\\
& \cn{}| &
{\sf Rec} {\it (}$rec\_clause$ {\sf And}{\it )}$^*$ $rec\_clause$ {\sf In}
$expr$\\
& \cn{}| &
{\sf Match Context With} {\it (}$context\_rule$ {\sf |}{\it )}$^*$
$context\_rule$\\
& \cn{}| &
{\sf Match} $term$ {\sf With} {\it (}$match\_rule$ {\sf |}{\it
)}$^*$ $match\_rule$\\
& \cn{}| & {\sf (} $expr$ {\sf )}\\
& \cn{}| & {\sf (} $expr$ $expr^+$ {\sf )}\\
& \cn{}| & $atom$ {\sf Orelse} $atom$\\
& \cn{}| & {\sf Do} {\it (}$int$ {\it |} $ident${\it )} $atom$\\
& \cn{}| & {\sf Repeat} $atom$\\
& \cn{}| & {\sf Try} $atom$\\
& \cn{}| & {\sf First [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
& \cn{}| & {\sf Solve [} {\it (}$expr$ {\sf |}{\it )}$^*$ $expr$ {\sf ]}\\
& \cn{}| & {\sf Idtac}\\
& \cn{}| & {\sf Fail}\\
& \cn{}| & $primitive\_tactic$\\
& \cn{}| & $arg$\\
\\
$input\_fun$ & \cn{}::= & $ident$\\
& \cn{}| & {\sf ()}\\
\\
$let\_clause$ & \cn{}::= & $ident$ {\sf =} $expr$\\
\\
$rec\_clause$ & \cn{}::= & $ident$ $input\_fun^+$ {\sf ->} $expr$\\
\\
$context\_rule$ & \cn{}::= &
{\sf [} {\it (}$context\_hyps$ {\sf ;}{\it )}$^*$ $context\_hyps$ {\sf |-}
$term$ {\sf ] ->} $expr$\\
& \cn{}| & {\sf [ |-} $term$ {\sf ] ->} $expr$\\
& \cn{}| & {\sf \_ ->} $expr$\\
\\
$context\_hyps$ & \cn{}::= & $ident$ {\sf :} $term$\\
& \cn{}| & {\sf \_ :} $term$\\
\\
$match\_rule$ & \cn{}::= & {\sf [} $term$ {\sf ] ->} $expr$\\
& \cn{}| & {\sf \_ ->} $expr$\\
\\
$arg$ & \cn{}::= & {\sf ()}\\
& \cn{}| & $nat$\\
& \cn{}| & $ident$\\
& \cn{}| & {\sf '}$term$
\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{}::= & {\sf Tactic Definition} $ident$ $input\_fun^*$ {\sf :=}
$expr$ \\
& \cn{}| & {\sf Recursive Tactic Definition} {\it (}$trec\_clause$ {\sf
And}{\it )}$^*$ $trec\_clause$\\
\\
$trec\_clause$ & \cn{}::= & $ident$ $input\_fun^+$ {\sf :=} $expr$
\end{tabular}
\end{center}}}
\caption{Tactic toplevel definitions}
\label{ltactop}
\end{table}

\section{Semantic}

\subsection{Values}

Values are given by table~\ref{ltacval}. All these values are tactic values,
i.e. to be applied to a goal, except {\sf Fun}, {\sf Rec} and $arg$ values.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{center}
\begin{tabular}{lp{0.1in}l}
$vexpr$ & \cn{}::= & $vexpr$ {\sf ;} $vexpr$\\
& \cn{}| & $vexpr$ {\sf ; [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf
]}\\
& \cn{}| & $vatom$\\
\\
$vatom$ & \cn{}::= & {\sf Fun} $input\_fun^+$  {\sf ->} $expr$\\
& \cn{}| & {\sf Rec} $rec\_clause$\\
& \cn{}| &
{\sf Rec} {\it (}$rec\_clause$ {\sf And}{\it )}$^*$ $rec\_clause$ {\sf In}
$expr$\\
& \cn{}| &
{\sf Match Context With} {\it (}$context\_rule$ {\sf |}{\it )}$^*$
$context\_rule$\\
& \cn{}| & {\sf (} $vexpr$ {\sf )}\\
& \cn{}| & $vatom$ {\sf Orelse} $vatom$\\
& \cn{}| & {\sf Do} {\it (}$int$ {\it |} $ident${\it )} $vatom$\\
& \cn{}| & {\sf Repeat} $vatom$\\
& \cn{}| & {\sf Try} $vatom$\\
& \cn{}| & {\sf First [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf ]}\\
& \cn{}| & {\sf Solve [} {\it (}$vexpr$ {\sf |}{\it )}$^*$ $vexpr$ {\sf ]}\\
& \cn{}| & {\sf Idtac}\\
& \cn{}| & {\sf Fail}\\
& \cn{}| & $primitive\_tactic$\\
& \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{tabbing}
{\sf And} \=\kill
{\sf Let}\>$ident_1$ {\sf =} $expr_1$\\
{\sf And} $ident_2$ {\sf =} $expr_2$\\
...\\
{\sf And} $ident_n$ {\sf =} $expr_n$ {\sf In}\\
\>$expr$
\end{tabbing}

$expr_i$ is evaluated to $v_i$, then, $expr$ is evaluated by subsituting $v_i$
to each occurrence of $ident_i$, for $i=1,...,n$. There is no dependencies
between the $expr_i$ and the $ident_i$.

\subsubsection{Pattern matching on terms}

We can carry out pattern matching on terms with:

\newpage{}

\begin{tabbing}
\hx{3}\={\sf |} \=$term_n$ \=\kill
{\sf Match} $term$ {\sf With}\\
\>\>$term_1$ {\sf ->} $expr_1$\\
\>{\sf |} $term_2$ {\sf ->} $expr_2$\\
\>...\\
\>{\sf |} $term_n$ {\sf ->} $expr_n$\\
\>{\sf |} {\sf \_}\>\>{\sf ->} $expr_{n+1}$
\end{tabbing}

if $term$ is matched (non-linear first order unification) by $term_1$ then
$expr_1$ is evaluated by substituting the pattern matching instantiations to
the metavariables. Else, $term_2$ is tried and so on. If no $term_i$, with
$i=1,...,n$, matches $term$ then the last clause is used and $expr_{n+1}$ is
evaluated.\\

{\sf Error message:}\\

{\tt No matching clauses for Match}

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

\subsubsection{Application}

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

{\sf (} $expr$ $expr_1$ ... $expr_n$ {\sf )}\\

$expr$ is evaluated to $v$ and $expr_i$ is evaluated to $v_i$, for $i=1,...,n$.
If $expr$ is a {\sf Fun} or {\sf 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:\\

$expr_1$ {\sf ;} $expr_2$\\

$expr_1$ and $expr_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:\\

$expr_0$ {\sf ; [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\

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

$expr_1$ {\sf Orelse} $expr_2$\\

$expr_1$ and $expr_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:\\

{\sf Do} $n$ $expr$\\

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

{\sf Repeat} $expr$\\

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

{\sf Try} $expr$\\

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

{\sf First [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\

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

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

{\sf Solve [} $expr_1$ {\sf |} $...$ {\sf |} $expr_n$ {\sf ]}\\

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

{\sf Error message:}\\

{\tt Cannot solve the goal}

\subsubsection{Identity}

We have the identity tactic:\\

{\sf Idtac}\\

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

\subsubsection{Failing}

We have the failing tactic:\\

{\sf Fail}\\

It always fails and leaves the goal unchanged. It does not appear in the proof
script and can be catched by {\sf Try}.

\subsubsection{Pattern matching on proof contexts}

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

\begin{tabbing}
\hx{3}\={\sf |}\={\sf [}$context\_hyps_{n,1}${\sf ;}...{\sf ;}$context\_hyps_{n,m_n}$\={\sf |-}$term_n${\sf ] }\=\kill
{\sf Match Context With}\\
\>\>{\sf [}$context\_hyps_{1,1}${\sf ;}...{\sf ;}$context\_hyps_{1,m_1}$\>{\sf
|-}$term_1${\sf ] ->} $expr_1$\\
\>{\sf |[}$context\_hyps_{2,1}${\sf ;}...{\sf ;}$context\_hyps_{2,m_2}$\>\>{\sf
|-}$term_2${\sf ] ->} $expr_2$\\
\>...\\
\>{\sf |[}$context\_hyps_{n,1}${\sf ;}...{\sf ;}$context\_hyps_{n,m_n}$\>\>{\sf
|-}$term_n${\sf ] ->} $expr_n$\\
\>{\sf |\_}\>\>\>{\sf ->} $expr_{n+1}$
\end{tabbing}

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
$term_1$ is matched by the conclusion of the goal, then $expr_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 $expr_{n+1}$ is evaluated to
$v_{n+1}$ and $v_{n+1}$ is applied.\\

{\sf Error message:}\\

{\tt No matching clauses for Match Context}

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

\hx{4}context pattern.

\subsection{Tactic toplevel definitions}

Basically, tactics toplevel definitions are made as follows:\\

{\sf Tactic Definition} $ident$ {\sf :=} $expr$\\

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

{\sf Tactic Definition} $ident$ $input\_fun_1$ ... $input\_fun_n$ {\sf :=}
$expr$\\

This definition is nothing else than syntactical sugar for:\\

{\sf Tactic Definition} $ident$ {\sf := Fun} $input\_fun_1$ ... $input\_fun_n$
{\sf ->} $expr$\\

Then, this definition is treated as above.

Finally, mutal recursive function definitions are possible with:

\begin{tabbing}
\hx{4}\={\sf And} \=$ident_n$ $input\_fun_{n,1}$ ... $input\_fun_{n,m_n}$ \=\kill
\>{\sf Recursive Tactic Definition}\\
\>\>$ident_1$ $input\_fun_{1,1}$ ...
$input\_fun_{1,m_1}$\>{\sf :=} $expr_1$\\
\>{\sf And} $ident_2$ $input\_fun_{2,1}$ ... $input\_fun_{2,m_2}$\>\>{\sf :=}
$expr_2$\\
\>...\\
\>{\sf And} $ident_n$ $input\_fun_{n,1}$ ... $input\_fun_{n,m_n}$ {\sf :=}
$expr_n$
\end{tabbing}

This definition bloc is a set of simultaneous functional 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{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
\>{\sf Lemma card\_nat: \~{}(EX x:nat|(EX y:nat|(z:nat)(x=z)$\bs{}$/(y=z))).}\\
\>{\sf Proof.}\\
\>\>{\sf Red;Intro H.}\\
\>\>{\sf Elim H;Intros a Ha.}\\
\>\>{\sf Elim Ha;Intros b Hb.}\\
\>\>{\sf Elim (Hb (0));Elim (Hb (1));Elim (Hb (2));Intros;}\\
\>\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [\_:?1=?2;\_:?1=?3|-?] ->}\\
\>\>\>\>\>{\sf Cut ?2=?3;[Discriminate|Apply trans\_equal with ?1;Auto].}\\
\>{\sf Save.}
\end{tabbing}}}
\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 {\sf 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{tabbing}
\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\kill
\>{\sf Section Sort.}\\
\\
\>{\sf Variable A:Set.}\\
\\
\>{\sf Inductive permut:(list A)->(list A)->Prop:=}\\
\>\>\>{\sf  permut\_refl:(l:(list A))(permut l l)}\\
\>\>{\sf |permut\_cons:}\\
\>\>\>\>{\sf (a:A)(l0,l1:(list A))(permut l0 l1)->(permut (cons a l0) (cons a
l1))}\\
\>\>{\sf |permut\_append:(a:A)(l:(list A))(permut (cons a l) (l\^{}(cons a (nil
A))))}\\
\>\>{\sf |permut\_trans:}\\
\>\>\>\>{\sf (l0,l1,l2:(list A))(permut l0 l1)->(permut l1 l2)->(permut l0
l2).}\\
\\
\>{\sf End Sort.}
\end{tabbing}}}
\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 {\sf
PermutProve} and {\sf Permut}. The function to be called is {\sf PermutProve}
which computes the lengths of the two lists and calls {\sf Permut} with the
length if the two lists have the same length. {\sf Permut} works as expected.
If the two lists are equal, it concludes. Otherwise, if the lists have
identical first elements, it applies {\sf 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 {\sf 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 {\sf 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 {\sf Eval
Compute in} and we can get the terms back by {\sf Match}.
 
\begin{table}[p]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\=
\hx{4}\=\kill
\>{\sf Tactic Definition Permut n:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|-(permut ? ?1 ?1)] -> Apply permut\_refl}\\
\>\>\>{\sf |[|-(permut ? (cons ?1 ?2) (cons ?1 ?3))] ->}\\
\>\>\>\>\>{\sf Let newn=Eval Compute in (length ?2)}\\
\>\>\>\>\>{\sf In}\\
\>\>\>\>\>\>{\sf Apply permut\_cons;(Permut newn)}\\
\>\>\>{\sf |[|-(permut ?1 (cons ?2 ?3) ?4)] ->}\\
\>\>\>\>\>{\sf (Match Eval Compute in n With}\\
\>\>\>\>\>\>\>{\sf [(1)] -> Fail}\\
\>\>\>\>\>\>{\sf |\_ ->}\\
\>\>\>\>\>\>\>\>{\sf Let l0'='(?3\^{}(cons ?2 (nil ?1)))}\\
\>\>\>\>\>\>\>\>{\sf In}\\
\>\>\>\>\>\>\>\>\>{\sf Apply (permut\_trans ?1 (cons ?2 ?3) l0' ?4);}\\
\>\>\>\>\>\>\>\>\>\>{\sf [Apply permut\_append|}\\
\>\>\>\>\>\>\>\>\>\>{\sf Compute;(Permut (pred n))]).}\\
\\
\>{\sf Tactic Definition PermutProve:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|-(permut ? ?1 ?2)] ->}\\
\>\>\>\>\>{\sf (Match Eval Compute in ((length ?1)=(length ?2)) With}\\
\>\>\>\>\>\>\>{\sf [?1=?1] -> (Permut ?1)).}
\end{tabbing}}}
\caption{Permutation tactic}
\label{permutltac}
\end{table}

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

\begin{table}[p]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
\>{\sf Lemma permut\_ex1:}\\
\>\>{\sf (permut nat (cons (1) (cons (2) (cons (3) (nil nat))))}\\
\>\>\>{\sf (cons (3) (cons (2) (cons (1) (nil nat))))).}\\
\>{\sf Proof.}\\
\>\>{\sf PermutProve.}\\
\>{\sf Save.}\\
\\
\>{\sf Lemma permut\_ex2:}\\
\>\>{\sf (permut nat}\\
\>\>\>{\sf (cons (0) (cons (1) (cons (2) (cons (3) (cons (4) (cons (5) (cons (6)}\\
\>\>\>\>{\sf (cons (7) (cons (8) (cons (9) (nil nat)))))))))))}\\
\>\>\>{\sf (cons (0) (cons (2) (cons (4) (cons (6) (cons (8) (cons (9) (cons (7)}\\
\>\>\>\>{\sf (cons (5) (cons (3) (cons (1) (nil nat)))))))))))).}\\
\>{\sf Proof.}\\
\>\>{\sf PermutProve.}\\
\>{\sf Save.}
\end{tabbing}}}
\caption{Examples of {\sf PermutProve} use}
\label{permutlem}
\end{table}

\subsection{Deciding intuitionnistic 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 intuitionnistic propositional logic. Considering the
contraction-free sequent calculi {\sf 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 {\sf Axioms} tries to conclude using usual
axioms. The tactic {\sf Simplif} applies all the reversible rules of Dyckhoff's
system. Finally, the tactic {\sf TautoProp} (the main tactic to be called)
simplifies with {\sf Simplif}, tries to conclude with {\sf 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{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\={\sf |}\=\hx{3}\={\sf |}\=\hx{3}\=\hx{4}\=\hx{4}\=\kill
\>{\sf Tactic Definition Axioms:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|-True] -> Trivial}\\
\>\>\>{\sf |[\_:False|- ?] -> ElimType False;Assumption}\\
\>\>\>{\sf |[\_:?1|-?1] -> Auto.}\\
\\
\>{\sf Tactic Definition Simplif:=}\\
\>\>{\sf Repeat}\\
\>\>\>{\sf (Intros;}\\
\>\>\>\>\>{\sf (Match Context With}\\
\>\>\>\>\>\>\>\>{\sf [id:\~{}?|-?] -> Red in id}\\
\>\>\>\>\>\>\>{\sf |[id:?/$\bs{}$?|-?] -> Elim id;Do 2 Intro;Clear id}\\
\>\>\>\>\>\>\>{\sf |[id:?$\bs{}$/?|-?] -> Elim id;Intro;Clear id}\\
\>\>\>\>\>\>\>{\sf |[id:?1/$\bs{}$?2->?3|-?] ->}\\
\>\>\>\>\>\>\>\>\>{\sf Cut ?1->?2->?3;[Intro|Intros;Apply id;Split;Assumption]}\\
\>\>\>\>\>\>\>{\sf |[id:?1$\bs{}$/?2->?3|-?] ->}\\
\>\>\>\>\>\>\>\>\>{\sf Cut ?2->?3;[Cut ?1->?3;[Intros|}\\
\>\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Left;Assumption]|}\\
\>\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Right;Assumption]}\\
\>\>\>\>\>\>\>{\sf |[id0:?1->?2;id1:?1|-?] ->}\\
\>\>\>\>\>\>\>\>\>{\sf Cut ?2;[Intro;Clear id0|Apply id0;Assumption]}\\
\>\>\>\>\>\>\>{\sf |[|-?/$\bs{}$?] -> Split}\\
\>\>\>\>\>\>\>{\sf |[|-\~{}?] -> Red)).}\\
\\
\>{\sf Recursive Tactic Definition TautoProp:=}\\
\>\>{\sf Simplif;}\\
\>\>{\sf Axioms}\\
\>\>{\sf Orelse}\\
\>\>\>{\sf Match Context With}\\
\>\>\>\>\>\>{\sf [id:(?1->?2)->?3|-?] ->}\\
\>\>\>\>\>\>\>{\sf Cut ?2->?3;[Intro;Cut ?1->?2;[Intro;Cut ?3;[Intro;Clear id|}\\
\>\>\>\>\>\>\>\>\>{\sf Apply id;Assumption]|Clear id]|}\\
\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Intro;Assumption];TautoProp}\\
\>\>\>\>\>{\sf |[id:\~{}?1->?2|-?]->}\\
\>\>\>\>\>\>\>{\sf Cut False->?2;[Intro;Cut ?1->False;[Intro;Cut ?2;[Intro;Clear id|}\\
\>\>\>\>\>\>\>\>\>{\sf Apply id;Assumption]|Clear id]|}\\
\>\>\>\>\>\>\>\>\>{\sf Intro;Apply id;Red;Intro;Assumption];TautoProp}\\
\>\>\>\>\>{\sf |[|-?$\bs{}$/?] ->}\\
\>\>\>\>\>\>\>{\sf (Left;TautoProp) Orelse (Right;TautoProp).}
\end{tabbing}}}
\caption{Deciding intuitionnistic propositions}
\label{tautoltac}
\end{table}

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

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\=\hx{4}\=\kill
\>{\sf Lemma tauto\_ex1:(A,B:Prop)A/$\bs{}$B->A$\bs{}$/B.}\\
\>{\sf Proof.}\\
\>\>{\sf TautoProp.}\\
\>{\sf Save.}\\
\\
\>{\sf Lemma tauto\_ex2:(A,B:Prop)(\~{}\~{}B->B)->(A->B)->\~{}\~{}A->B.}\\
\>{\sf Proof.}\\
\>\>{\sf TautoProp.}\\
\>{\sf Save.}
\end{tabbing}}}
\caption{Proofs of tautologies with {\sf 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{tabbing}
\hx{4}\=\hx{4}\=\kill
\>{\sf Section Iso\_axioms.}\\
\\
\>{\sf Variable A,B,C:Set.}\\
\\
\>{\sf Axiom Com:(A*B)==(B*A).}\\
\>{\sf Axiom Ass:(A*(B*C))==((A*B)*C).}\\
\>{\sf Axiom Cur:((A*B)->C)==(A->B->C).}\\
\>{\sf Axiom Dis:(A->(B*C))==((A->B)*(A->C)).}\\
\>{\sf Axiom P\_unit:(A*unit)==A.}\\
\>{\sf Axiom AR\_unit:(A->unit)==unit.}\\
\>{\sf Axiom AL\_unit:(unit->A)==A.}\\
\\
\>{\sf Lemma Cons:B==C->(A*B)==(A*C).}\\
\>{\sf Proof.}\\
\>\>{\sf Intro Heq;Rewrite Heq;Apply refl\_eqT.}\\
\>{\sf Save.}\\
\\
\>{\sf End Iso\_axioms.}
\end{tabbing}}}
\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 {\sf
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 {\sf
Compare}). The main tactic to be called and realizing this algorithm is
{\sf IsoProve}.

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\=\kill
\>{\sf Recursive Tactic Definition Simplif trm:=}\\
\>\>{\sf Match trm With}\\
\>\>\>\>{\sf [(?1*?2)*?3] -> Rewrite <- (Ass ?1 ?2 ?3);Try MainSimplif}\\
\>\>\>{\sf |[(?1*?2)->?3] -> Rewrite (Cur ?1 ?2 ?3);Try MainSimplif}\\
\>\>\>{\sf |[?1->(?2*?3)] -> Rewrite (Dis ?1 ?2 ?3);Try MainSimplif}\\
\>\>\>{\sf |[?1*unit] -> Rewrite (P\_unit ?1);Try MainSimplif}\\
\>\>\>{\sf |[unit*?1] -> Rewrite (Com unit ?1);Try MainSimplif}\\
\>\>\>{\sf |[?1->unit] -> Rewrite (AR\_unit ?1);Try MainSimplif}\\
\>\>\>{\sf |[unit-> ?1] -> Rewrite (AL\_unit ?1);Try MainSimplif}\\
\>\>\>{\sf |[?1*?2] ->}\\
\>\>\>\>\>{\sf ((Simplif ?1);Try MainSimplif) Orelse}\\
\>\>\>\>\>\>{\sf ((Simplif ?2);Try MainSimplif)}\\
\>\>\>{\sf |[?1-> ?2] ->}\\
\>\>\>\>\>{\sf ((Simplif ?1);Try MainSimplif) Orelse}\\
\>\>\>\>\>\>{\sf ((Simplif ?2);Try MainSimplif)}\\
\>{\sf And MainSimplif:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|- ?1== ?2] -> Try (Simplif ?1);Try (Simplif ?2).}\\
\\
\>{\sf Tactic Definition Length trm:=}\\
\>\>{\sf Match trm With}\\
\>\>\>\>{\sf [?*?1] ->}\\
\>\>\>\>\>{\sf Let succ=(Length ?1)}\\
\>\>\>\>\>{\sf In}\\
\>\>\>\>\>\>{\sf '(S succ)}\\
\>\>\>{\sf |\_ -> '(1).}\\
\\
\>{\sf Tactic Definition Assoc:= Repeat Rewrite <- Ass.}
\end{tabbing}}}
\caption{Type isomorphism tactic (1)}
\label{isosltac1}
\end{table}

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{4}\={\sf |}\=\hx{3}\=\hx{1}\=\hx{3}\=\kill
\>{\sf Recursive Tactic Definition DoCompare n:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|-?1==?1] -> Apply refl\_eqT}\\
\>\>\>{\sf |[|-(?1*?2)==(?1*?3)] ->}\\
\>\>\>\>\>{\sf Apply Cons;}\\
\>\>\>\>\>\>{\sf Let newn=(Length ?2)}\\
\>\>\>\>\>\>{\sf  In}\\
\>\>\>\>\>\>\>\>{\sf (DoCompare newn)}\\
\>\>\>{\sf |[|-(?1*?2)==?3] ->}\\
\>\>\>\>\>{\sf (Match Eval Compute in n With}\\
\>\>\>\>\>\>\>{\sf [(1)] -> Fail}\\
\>\>\>\>\>\>{\sf |\_ -> }\\
\>\>\>\>\>\>\>\>{\sf Pattern 1 (?1*?2);Rewrite Com;Assoc;}\\
\>\>\>\>\>\>\>\>\>\>{\sf (DoCompare '(pred n))).}\\
\\
\>{\sf Tactic Definition Compare:=}\\
\>\>{\sf Match Context With}\\
\>\>\>\>{\sf [|-?1==?2] ->}\\
\>\>\>\>\>{\sf Let l1=(Length ?1)}\\
\>\>\>\>\>{\sf And l2=(Length ?2)}\\
\>\>\>\>\>{\sf In}\\
\>\>\>\>\>\>{\sf (Match Eval Compute in l1=l2 With}\\
\>\>\>\>\>\>\>\>\>{\sf [?1=?1] -> (DoCompare ?1)).}\\
\\
\>{\sf Tactic Definition IsoProve:=MainSimplif;Compare.}
\end{tabbing}}}
\caption{Type isomorphism tactic (2)}
\label{isosltac2}
\end{table}

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

\begin{table}[ht]
\noindent{}\framebox[6in][l]
{\parbox{6in}
{\begin{tabbing}
\hx{4}\=\hx{4}\=\kill
\>{\sf Lemma isos\_ex1:(A,B:Set)((A*unit)*B)==(B*(unit*A)).}\\
\>{\sf Proof.}\\
\>\>{\sf Intros;IsoProve.}\\
\>{\sf Save.}\\
\\
\>{\sf Lemma isos\_ex2:(A,B,C:Set)}\\
\>\>{\sf ((A*unit)->(B*C*unit))==(((A*unit)->((C->unit)*C))*(unit->(A->B))).}\\
\>{\sf Proof.}\\
\>\>{\sf Intros;IsoProve.}\\
\>{\sf Save.}
\end{tabbing}}}
\caption{Type equalities solved by {\sf IsoProve}}
\label{isoslem}
\end{table}