%\documentclass[11pt]{article}
%\usepackage{fullpage,euler}
%\usepackage[latin1]{inputenc}
%\begin{document}
%\title{Writing ad-hoc Tactics in Coq}
%\author{} 
%\date{}
%\maketitle
%\tableofcontents
%\clearpage

\chapter{Writing ad-hoc Tactics in Coq}
\label{WritingTactics}

\section{Introduction}

\Coq\ is an open proof environment, in the sense that the collection of
proof strategies offered by the system can be extended by the user.
This feature has two important advantages. First, the user can develop
his/her own ad-hoc proof procedures, customizing the system for a
particular domain of application. Second, the repetitive and tedious
aspects of the proofs can be abstracted away implementing new tactics
for dealing with them. For example, this may be useful when a theorem
needs several lemmas which are all proven in a similar but not exactly
the same way. Let us illustrate this with an example.

Consider the problem of deciding the equality of two booleans. The
theorem establishing that this is always possible is state by 
the following theorem:

\begin{coq_example*}
Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
\end{coq_example*}

The proof proceeds by case analysis on both $x$ and $y$. This yields
four cases to solve. The cases $x=y=\textsl{true}$ and
$x=y=\textsl{false}$ are immediate by the reflexivity of equality.

The other two cases follow by discrimination. The following script
describes the proof:

\begin{coq_example*}
Destruct x.
  Destruct y.
    Left ; Reflexivity.
    Right; Discriminate.
  Destruct y.
    Right; Discriminate.
    Left ; Reflexivity.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

Now, consider the theorem stating the same property but for the
following enumerated type:

\begin{coq_example*}
Inductive Set Color := Blue:Color | White:Color | Red:Color.
Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
\end{coq_example*}

This theorem can be proven in a very similar way, reasoning by case
analysis on $c_1$ and $c_2$. Once more, each of the (now six) cases is
solved either by reflexivity or by discrimination:

\begin{coq_example*}
Destruct c1. 
  Destruct c2.
    Left  ; Reflexivity.
    Right ; Discriminate.
    Right ; Discriminate.
  Destruct c2.  
    Right ; Discriminate.
    Left  ; Reflexivity.
    Right ; Discriminate.
  Destruct c2.  
    Right ; Discriminate.
    Right ; Discriminate.
    Left  ; Reflexivity.
\end{coq_example*}
\begin{coq_eval}
Abort.
\end{coq_eval}

If we face the same theorem for an enumerated datatype corresponding
to the days of the week, it would still follow a similar pattern. In
general, the general pattern for proving the property
$(x,y:R)\{x=y\}+\{\neg x =y\}$ for an enumerated type $R$ proceeds as
follow:
\begin{enumerate}
\item Analyze the cases for $x$. 
\item For each of the sub-goals generated by the first step, analyze
the cases for $y$.
\item The remaining subgoals follow either by reflexivity or
by discrimination.
\end{enumerate}

Let us describe how this general proof procedure can be introduced in
\Coq.

\section{Tactic Macros}

The simplest way to introduce it is to define it as new a
\textsl{tactic macro}, as follows:

\begin{coq_example*}
Tactic Definition DecideEq [$a $b] := 
   [<:tactic:<Destruct $a;
              Destruct $b;
              (Left;Reflexivity) Orelse (Right;Discriminate)>>].
\end{coq_example*}

The general pattern of the proof is abstracted away using the
tacticals ``\texttt{;}'' and \texttt{Orelse}, and introducing two
parameters for the names of the arguments to be analyzed.

Once defined, this tactic can be called like any other tactic, just
supplying the list of terms corresponding to its real arguments. Let us
revisit the proof of the former theorems using the new tactic
\texttt{DecideEq}:

\begin{coq_example*}
Theorem decideBool : (x,y:bool){x=y}+{~x=y}.
DecideEq x y.
Defined.
\end{coq_example*}
\begin{coq_example*}
Theorem decideColor : (c1,c2:Color){c1=c2}+{~c1=c2}.
DecideEq c1 c2.
Defined.
\end{coq_example*}

In general, the command \texttt{Tactic Definition} associates a name
to a parameterized tactic expression, built up from the tactics and
tacticals that are already available. The general syntax rule for this
command is the following:

\begin{tabbing}
\texttt{Tactic Definition} \textit{tactic-name} \= 
\texttt{[}\$$id_1\ldots \$id_n$\texttt{]}\\
\> := \texttt{[<:tactic:<} \textit{tactic-expression} \verb+>>]+
\end{tabbing}

This command provides a quick but also very primitive mechanism for
introducing new tactics. It does not support recursive definitions,
and the arguments of a tactic macro are restricted to term
expressions.  Moreover, there is no static checking of the definition
other than the syntactical one. Any error in the definition of the
tactic ---for instance, a call to an undefined tactic--- will not be
noticed until the tactic is called.

%This command provides a very primitive mechanism for introducing new
%tactics. The arguments of a tactic macro are restricted to term
%expressions.  Hence, it is not possible to define higher order tactics
%with this command. Also, there is no static checking of the definition
%other than syntactical. If the tactic contain errors in its definition
%--for instance, a call to an undefined tactic-- this will be noticed
%during the tactic call.

Let us illustrate the weakness of this way of introducing new tactics
trying to extend our proof procedure to work on a larger class of
inductive types.  Consider for example the decidability of equality
for pairs of booleans and colors:

\begin{coq_example*}
Theorem decideBoolXColor : (p1,p2:bool*Color){p1=p2}+{~p1=p2}.
\end{coq_example*}

The proof still proceeds by a double case analysis, but now the
constructors of the type take two arguments. Therefore, the sub-goals
that can not be solved by discrimination need further considerations
about the equality of such arguments:

\begin{coq_example}
  Destruct p1;
    Destruct p2; Try (Right;Discriminate);Intros.
\end{coq_example}

The half of the disjunction to be chosen depends on whether or not
$b=b_0$ and $c=c_0$. These equalities can be decided automatically
using the previous lemmas about booleans and colors. If both
equalities are satisfied, then it is sufficient to rewrite $b$ into
$b_0$ and $c$ into $c_0$, so that the left half of the goal follows by
reflexivity.  Otherwise, the right half follows by first contraposing
the disequality, and then applying the invectiveness of the pairing
constructor.

As the cases associated to each argument of the pair are very similar,
a tactic macro can be introduced to abstract this part of the proof:

\begin{coq_example*}
Hints Resolve decideBool decideColor.
Tactic Definition SolveArg [$t1 $t2] := 
 [<:tactic:<
   ElimType {$t1=$t2}+{~$t1=$t2};
   [(Intro equality;Rewrite equality;Clear equality) |
    (Intro diseq; Right; Red; Intro absurd;
     Apply diseq;Injection absurd;Trivial) |
    Auto]>>].
\end{coq_example*}

This tactic is applied to each corresponding pair of arguments of the
arguments, until the goal can be solved by reflexivity:

\begin{coq_example*}
SolveArg b b0;
  SolveArg c c0;
    Left; Reflexivity.
Defined.
\end{coq_example*}

Therefore, a more general strategy for deciding the property 
$(x,y:R)\{x=y\}+\{\neg x =y\}$ on $R$ can be sketched as follows:
\begin{enumerate}
\item Eliminate $x$ and then $y$.
\item Try discrimination to solve those goals where $x$ and $y$ has
been introduced by different constructors.
\item If $x$ and $y$ have been introduced by the same constructor,
then iterate the tactic \textsl{SolveArg} for each pair of
arguments. 
\item Finally, solve the left half of the goal by reflexivity.
\end{enumerate}

The implementation of this stronger proof strategy needs to perform a
term decomposition, in order to extract the list of arguments of each
constructor. It also requires the introduction of recursively defined
tactics, so that the \textsl{SolveArg} can be iterated on the lists of
arguments. These features are not supported by the \texttt{Tactic
Definition} command. One possibility could be extended this command in
order to introduce recursion, general parameter passing,
pattern-matching, etc, but this would quickly lead us to introduce the
whole \ocaml{} into \Coq\footnote{This is historically true. In fact,
\ocaml{} is a direct descendent of ML, a functional programming language
conceived language for programming the tactics of the theorem prover
LCF.}.  Instead of doing this, we prefer to give to the user the
possibility of writing his/her own tactics directly in \ocaml{}, and then
to link them dynamically with \Coq's code. This requires a minimal
knowledge about \Coq's implementation. The next section provides an
overview of \Coq's architecture.

%It is important to point out that the introduction of a new tactic
%never endangers the correction of the theorems proven in the extended
%system. In order to understand why, let us introduce briefly the system
%architecture.

\section{An Overview of \Coq's Architecture}

The implementation of \Coq\ is based on eight \textsl{logical
modules}. By ``module'' we mean here a logical piece of code having a
conceptual unity, that may concern several \ocaml{} files. By the sake of
organization, all the \ocaml{} files concerning a logical module are
grouped altogether into the same sub-directory. The eight modules
are:

\begin{tabular}{lll}
1. & The logical framework           & (directory \texttt{src/generic})\\
2. &  The language of constructions  & (directory \texttt{src/constr})\\
3. &  The type-checker               & (directory \texttt{src/typing})\\
4. &  The proof engine               & (directory \texttt{src/proofs})\\
5. &  The language of basic tactics  & (directory \texttt{src/tactics})\\
6. &  The vernacular interpreter     & (directory \texttt{src/env})\\
7. &  The parser and the pretty-printer  & (directory \texttt{src/parsing})\\
8. &  The standard library           & (directory \texttt{src/lib})
\end{tabular}

\vspace{1em}

The following sections briefly present each of the modules above.
This presentation is not intended to be a complete description of \Coq's
implementation, but rather a guideline to be read before taking a look
at the sources. For each of the modules, we also present some of its
most important functions, which are sufficient to implement a large
class of tactics.


\subsection{The Logical Framework}
\label{LogicalFramework}

At the very heart of \Coq there is a generic untyped language for
expressing abstractions, applications and global constants. This
language is used as a meta-language for expressing the terms of the
Calculus of Inductive Constructions. General operations on terms like
collecting the free variables of an expression, substituting a term for
a free variable, etc, are expressed in this language.

The meta-language \texttt{'op term} of terms has seven main
constructors:
\begin{itemize}
\item $(\texttt{VAR}\;id)$, a reference to a global identifier called  $id$;
\item $(\texttt{Rel}\;n)$, a bound variable, whose binder is the $nth$
      binder up in the term;
\item $\texttt{DLAM}\;(x,t)$, a deBruijn's binder on the term $t$;
\item $\texttt{DLAMV}\;(x,vt)$, a deBruijn's binder on all the terms of 
      the vector $vt$;
\item $(\texttt{DOP0}\;op)$, a unary operator $op$;
\item $\texttt{DOP2}\;(op,t_1,t_2)$, the application of a binary
operator $op$ to the terms $t_1$ and $t_2$;
\item $\texttt{DOPN} (op,vt)$, the application of an n-ary operator $op$ to the
vector of terms $vt$.
\end{itemize}

In this meta-language, bound variables are represented using the
so-called deBrujin's indexes. In this representation, an occurrence of
a bound variable is denoted by an integer, meaning the number of
binders that must be traversed to reach its own
binder\footnote{Actually, $(\texttt{Rel}\;n)$ means that $(n-1)$ binders
have to be traversed, since indexes are represented by strictly
positive integers.}. On the other hand, constants are referred by its
name, as usual. For example, if $A$ is a variable of the current
section, then the lambda abstraction $[x:A]x$ of the Calculus of
Constructions is represented in the meta-language by the term:

\begin{displaymath}
(DOP2 (Lambda,(Var\;A),DLAM (x,(Rel\;1)))
\end{displaymath}

In this term, $Lambda$ is a binary operator.  Its first argument
correspond to the type $A$ of the bound variable, while the second is
a body of the abstraction, where $x$ is bound.  The name $x$ is just kept
to pretty-print the occurrences of the bound variable.

%Similarly, the product
%$(A:Prop)A$ of the Calculus of Constructions is represented by the
%term:
%\begin{displaumath}
%DOP2 (Prod, DOP0 (Sort (Prop Null)), DLAM (Name \#A, Rel 1))
%\end{displaymath}

The following functions perform some of the most frequent operations
on the terms of the meta-language:
\begin{description}
\fun{val Generic.subst1 : 'op term -> 'op term -> 'op term}
    {$(\texttt{subst1}\;t_1\;t_2)$ substitutes $t_1$ for 
      $\texttt{(Rel}\;1)$ in $t_2$.}
\fun{val Generic.occur\_var : identifier -> 'op term -> bool}
    {Returns true when the given identifier appears in the term,
    and false otherwise.}
\fun{val Generic.eq\_term : 'op term -> 'op term -> bool}
    {Implements $\alpha$-equality for terms.}  
\fun{val Generic.dependent : 'op term -> 'op term -> bool}
    {Returns true if the first term is a sub-term of the second.}
%\fun{val Generic.subst\_var : identifier -> 'op term -> 'op term}
%    { $(\texttt{subst\_var}\;id\;t)$ substitutes the deBruijn's index
%     associated to $id$ to every occurrence of the term
%    $(\texttt{VAR}\;id)$ in $t$.}
\end{description}

\subsubsection{Identifiers, names and sections paths.} 

Three different kinds of names are used in the meta-language. They are
all defined in the \ocaml{} file \texttt{Names}.

\paragraph{Identifiers.}  The simplest kind of names are
\textsl{identifiers}. An identifier is a string possibly indexed by an
integer. They are used to represent names that are not unique, like
for example the name of a variable in the scope of a section.  The
following operations can be used for handling identifiers:

\begin{description}
\fun{val Names.make\_ident : string -> int -> identifier}
    {The value $(\texttt{make\_ident}\;x\;i)$ creates the
    identifier $x_i$. If $i=-1$, then the identifier has
    is created with no index at all.}
\fun{val Names.repr\_ident : identifier -> string * int}
    {The inverse operation of \texttt{make\_ident}: 
     it yields the string and the index of the identifier.}
\fun{val Names.lift\_ident : identifier -> identifier}
    {Increases the index of the identifier by one.}
\fun{val Names.next\_ident\_away : \\
\qquad identifier -> identifier list -> identifier}
    {\\ Generates a new identifier with the same root string than the
    given one, but with a new index, different from all the indexes of
    a given list of identifiers.} 
\fun{val Names.id\_of\_string : string ->
    identifier} 
    {Creates an identifier from a string.}  
\fun{val  Names.string\_of\_id : identifier -> string} 
    {The inverse operation: transforms an identifier into a string}
\end{description}

\paragraph{Names.} A \textsl{name} is either an identifier or the 
special name \texttt{Anonymous}. Names are used as arguments of
binders, in order to pretty print bound variables.
The following operations can be used for handling names:

\begin{description}
\fun{val Names.Name: identifier -> Name}
    {Constructs a name from  an identifier.}
\fun{val Names.Anonymous : Name}
    {Constructs a special, anonymous identifier, like the variable abstracted 
     in the term $[\_:A]0$.}
\fun{val
     Names.next\_name\_away\_with\_default : \\ \qquad
          string->name->identifier list->identifier}
{\\ If the name is not anonymous, then this function generates a new
    identifier different from all the ones in a given list. Otherwise, it
    generates an identifier from the given string.}
\end{description}

\paragraph{Section paths.} 
\label{SectionPaths}
A \textsl{section-path} is a global name to refer to an object without
ambiguity.  It can be seen as a sort of filename, where open sections
play the role of directories. Each section path is formed by three
components: a \textsl{directory} (the list of open sections); a
\textsl{basename} (the identifier for the object); and a \textsl{kind}
(either CCI for the terms of the Calculus of Constructions, FW for the
the terms of $F_\omega$, or OBJ for other objects). For example, the
name of the following constant:
\begin{verbatim}
     Section A.
     Section B.
     Section C.
     Definition zero := O.
\end{verbatim}

is internally represented by the section path:

$$\underbrace{\mathtt{\#A\#B\#C}}_{\mbox{dirpath}}
\underbrace{\mathtt{\tt \#zero}}_{\mbox{basename}}
\underbrace{\mathtt{\tt .cci}_{\;}}_{\mbox{kind}}$$

When one of the sections is closed, a new constant is created with an
updated section-path,a nd the old one is no longer reachable.  In our
example, after closing the section \texttt{C}, the new section-path
for the constant {\tt zero} becomes:
\begin{center}
\texttt{ \#A\#B\#zero.cci}
\end{center}

The following operations can be used to handle section paths:

\begin{description}
\fun{val Names.string\_of\_path : section\_path -> string}
    {Transforms the section path into a string.}
\fun{val Names.path\_of\_string : string -> section\_path}
    {Parses a string an returns the corresponding section path.}
\fun{val Names.basename : section\_path -> identifier}
    {Provides the basename of a section path}
\fun{val Names.dirpath : section\_path -> string list}
    {Provides the directory of a section path}
\fun{val Names.kind\_of\_path : section\_path -> path\_kind}
    {Provides the kind of a section path}
\end{description}

\subsubsection{Signatures} 

A \textsl{signature} is a mapping associating different informations
to identifiers (for example, its type, its definition, etc). The
following operations could be useful for working with signatures:

\begin{description}
\fun{val Names.ids\_of\_sign  : 'a signature -> identifier list}
    {Gets the list of identifiers of the signature.}
\fun{val Names.vals\_of\_sign : 'a signature -> 'a list}
    {Gets the list of values associated to the identifiers of the signature.}
\fun{val Names.lookup\_glob1 : \\ \qquad
identifier -> 'a signature -> (identifier *
    'a)}
    {\\ Gets the value associated to a given identifier of the signature.}
\end{description}


\subsection{The Terms of the Calculus of Constructions}

The language of the Calculus of Inductive Constructions described in
Chapter \ref{Cic} is implemented on the top of the logical framework,
instantiating the parameter $op$ of the meta-language with a
particular set of operators.  In the implementation this language is
called \texttt{constr}, the language of constructions.

% The only difference
%with respect to the one described in Section \ref{} is that the terms
%of \texttt{constr} may contain \textsl{existential variables}. An
%existential variable is a place holder representing a part of the term
%that is still to be constructed. Such ``open terms'' are necessary
%when building proofs interactively.

\subsubsection{Building Constructions}

The user does not need to know the choices made to represent
\texttt{constr} in the meta-language. They are abstracted away by the
following constructor functions:

\begin{description}
\fun{val Term.mkRel          : int -> constr}
    {$(\texttt{mkRel}\;n)$ represents deBrujin's index $n$.}

\fun{val Term.mkVar : identifier -> constr} 
    {$(\texttt{mkVar}\;id)$
    represents a global identifier named $id$, like a variable
    inside the scope of a section, or a hypothesis in a proof}.

\fun{val Term.mkExistential : constr} 
   {\texttt{mkExistential} represents an implicit sub-term, like the question
    marks in the term \texttt{(pair ? ? O true)}.}

%\fun{val Term.mkMeta         : int -> constr}
%    {$(\texttt{mkMeta}\;n)$ represents an existential variable, whose
%     name is the integer $n$.}

\fun{val Term.mkProp         : constr}
    {$\texttt{mkProp}$ represents the sort \textsl{Prop}.}

\fun{val Term.mkSet          : constr}
    {$\texttt{mkSet}$ represents the sort \textsl{Set}.}

\fun{val Term.mkType         : Impuniv.universe -> constr}
    {$(\texttt{mkType}\;u)$ represents the term
    $\textsl{Type}(u)$. The universe $u$ is represented as a 
    section path indexed by an integer. }

\fun{val Term.mkConst : section\_path -> constr array -> constr}
    {$(\texttt{mkConst}\;c\;v)$ represents a constant whose name is
    $c$. The body of the constant is stored in a global table,
    accessible through the name of the constant. The array of terms
    $v$ corresponds to the variables of the environment appearing in
    the body of the constant when it was defined. For instance, a
    constant defined in the section \textsl{Foo} containing the
    variable $A$, and whose body is $[x:Prop\ra Prop](x\;A)$ is
    represented inside the scope of the section by
    $(\texttt{mkConst}\;\texttt{\#foo\#f.cci}\;[| \texttt{mkVAR}\;A
    |])$.  Once the section is closed, the constant is represented by
    the term $(\texttt{mkConst}\;\#f.cci\;[| |])$, and its body
    becomes $[A:Prop][x:Prop\ra Prop](x\;A)$}.

\fun{val Term.mkMutInd : section\_path -> int -> constr array ->constr}
    {$(\texttt{mkMutInd}\;c\;i)$ represents the $ith$ type
    (starting from zero) of the block of mutually dependent
    (co)inductive types, whose first type is $c$.  Similarly to the
    case of constants, the array of terms represents the current
    environment of the (co)inductive type. The definition of the type
    (its arity, its constructors, whether it is inductive or co-inductive, etc.)
    is stored in a global hash table, accessible through the name of 
    the type.}

\fun{val Term.mkMutConstruct : \\ \qquad section\_path -> int -> int -> constr array
    ->constr} {\\ $(\texttt{mkMutConstruct}\;c\;i\;j)$ represents the
    $jth$ constructor of the $ith$ type of the block of mutually
    dependent (co)inductive types whose first type is $c$. The array
    of terms represents the current environment of the (co)inductive
    type.}

\fun{val Term.mkCast : constr -> constr -> constr}
    {$(\texttt{mkCast}\;t\;T)$ represents the annotated term $t::T$ in
    \Coq's syntax.}  

\fun{val Term.mkProd : name ->constr ->constr -> constr}
    {$(\texttt{mkProd}\;x\;A\;B)$ represents the product $(x:A)B$.
     The free ocurrences of $x$ in $B$ are represented by deBrujin's
     indexes.}

\fun{val Term.mkNamedProd : identifier -> constr -> constr -> constr}
    {$(\texttt{produit}\;x\;A\;B)$ represents the product $(x:A)B$,
     but the bound occurrences of $x$ in $B$ are denoted by 
     the identifier $(\texttt{mkVar}\;x)$. The function automatically 
     changes each occurrences of this identifier into the corresponding 
     deBrujin's index.}

\fun{val Term.mkArrow : constr -> constr -> constr}
    {$(\texttt{arrow}\;A\;B)$ represents the type $(A\rightarrow B)$.}

\fun{val Term.mkLambda       : name -> constr -> constr -> constr}
    {$(\texttt{mkLambda}\;x\;A\;b)$ represents the lambda abstraction 
     $[x:A]b$. The free ocurrences of $x$ in $B$ are represented by deBrujin's
     indexes.}

\fun{val Term.mkNamedLambda : identifier -> constr -> constr -> constr}
    {$(\texttt{lambda}\;x\;A\;b)$ represents the lambda abstraction 
     $[x:A]b$, but the bound occurrences of $x$ in $B$ are denoted by 
     the identifier $(\texttt{mkVar}\;x)$. }

\fun{val Term.mkAppLA        : constr array -> constr}
    {$(\texttt{mkAppLA}\;t\;[|t_1\ldots t_n|])$ represents the application
    $(t\;t_1\;\ldots t_n)$.}

\fun{val Term.mkMutCaseA : \\ \qquad
    case\_info -> constr ->constr
    ->constr array -> constr} 
    {\\ $(\texttt{mkMutCaseA}\;r\;P\;m\;[|f_1\ldots f_n|])$
    represents the term \Case{P}{m}{f_1\ldots f_n}. The first argument
    $r$ is either \texttt{None} or $\texttt{Some}\;(c,i)$, where the
    pair $(c,i)$ refers to the inductive type that $m$ belongs to.}

\fun{val Term.mkFix :  \\ \qquad
int array->int->constr array->name
    list->constr array->constr}
    {\\ $(\texttt{mkFix}\;[|k_1\ldots k_n |]\;i\;[|A_1\ldots
    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
    $\Fix{f_i}{f_1/k_1:A_1:=t_1 \ldots f_n/k_n:A_n:=t_n}$}

\fun{val Term.mkCoFix  : \\ \qquad
    int -> constr array -> name list ->
    constr array -> constr}
    {\\ $(\texttt{mkCoFix}\;i\;[|A_1\ldots
    A_n|]\;[|f_1\ldots f_n|]\;[|t_1\ldots t_n|])$ represents the term
    $\CoFix{f_i}{f_1:A_1:=t_1 \ldots f_n:A_n:=t_n}$. There are no
    decreasing indexes in this case.}
\end{description}

\subsubsection{Decomposing Constructions}

Each of the construction functions above has its corresponding
(partial) destruction function, whose name is obtained changing the
prefix \texttt{mk} by \texttt{dest}. In addition to these functions, a
concrete datatype \texttt{kindOfTerm} can be used to do pattern
matching on terms without dealing with their internal representation
in the meta-language. This concrete datatype is described in the \ocaml{}
file \texttt{term.mli}. The following function transforms a construction
into an element of type \texttt{kindOfTerm}:

\begin{description}
\fun{val Term.kind\_of\_term : constr -> kindOfTerm}
    {Destructs a term of the language \texttt{constr},
yielding the direct components of the term. Hence, in order to do 
pattern matching on an object $c$ of \texttt{constr}, it is sufficient
to do pattern matching on the value $(\texttt{kind\_of\_term}\;c)$.}
\end{description}

Part of the information associated to the constants is stored in 
global tables. The following functions give access to such 
information:

\begin{description}
\fun{val Termenv.constant\_value    : constr -> constr}
    {If the term denotes a constant, projects the body of a constant}
\fun{Termenv.constant\_type     : constr -> constr}
    {If the term denotes a constant, projects the type of the constant}
\fun{val mind\_arity        : constr -> constr}
    {If the term denotes an inductive type, projects its arity (i.e.,
     the type of the inductive type).}
\fun{val Termenv.mis\_is\_finite    : mind\_specif -> bool}
    {Determines whether a recursive type is inductive or co-inductive.}
\fun{val Termenv.mind\_nparams : constr -> int}
    {If the term denotes an inductive type, projects the number of 
     its general parameters.}
\fun{val Termenv.mind\_is\_recursive : constr -> bool}
    {If the term denotes an inductive type, 
     determines if the type has at least one recursive constructor. }
\fun{val Termenv.mind\_recargs : constr -> recarg list array array}
    {If the term denotes an inductive type, returns an array $v$ such 
     that the nth element of $v.(i).(j)$ is
    \texttt{Mrec} if the $nth$ argument of the $jth$ constructor of
    the $ith$ type is recursive, and \texttt{Norec} if it is not.}.
\end{description}

\subsection{The Type Checker}
\label{TypeChecker}

The third logical module is the type checker. It concentrates two main
tasks concerning the language of constructions.

On one hand, it contains the type inference and type-checking
functions.  The type inference function takes a term
$a$ and a signature $\Gamma$, and yields a term $A$ such that
$\Gamma \vdash a:A$.  The type-checking function takes two terms $a$
and $A$ and a signature $\Gamma$, and determines whether or not
$\Gamma \vdash a:A$.

On the other hand, this module is in charge of the compilation of
\Coq's abstract syntax trees into the language \texttt{constr} of
constructions. This compilation seeks to eliminate all the ambiguities
contained in \Coq's abstract syntax, restoring the information
necessary to type-check it.  It concerns at least the following steps:
\begin{enumerate}
\item Compiling the pattern-matching expressions containing 
constructor patterns, wild-cards, etc, into terms that only
use the primitive \textsl{Case} described in Chapter \ref{Cic}
\item Restoring type coercions and synthesizing the implicit arguments
(the one denoted by question marks in
{\Coq} syntax: cf section \ref{Coercions}).
\item Transforming the named bound variables into deBrujin's indexes.
\item Classifying the global names into the different classes of
constants (defined constants, constructors, inductive types, etc).
\end{enumerate}

\subsection{The Proof Engine}

The fourth stage of \Coq's implementation is the \textsl{proof engine}:
the interactive machine for constructing proofs. The aim of the proof
engine is to construct a top-down derivation or \textsl{proof tree},
by the application of \textsl{tactics}. A proof tree has the following
general structure:\\

\begin{displaymath}
\frac{\Gamma \vdash ? = t(?_1,\ldots?_n) : G}
     {\hspace{3ex}\frac{\displaystyle \Gamma_1 \vdash ?_1 = t_1(\ldots) : G_1}
         {\stackrel{\vdots}{\displaystyle {\Gamma_{i_1} \vdash ?_{i_1} 
           : G_{i_1}}}}(tac_1)
      \;\;\;\;\;\;\;\;\;
      \frac{\displaystyle \Gamma_n \vdash ?_n = t_n(\ldots) : G_n}
         {\displaystyle \stackrel{\vdots}{\displaystyle {\Gamma_{i_m} \vdash ?_{i_m} :
     G_{i_m}}}}(tac_n)} (tac)    
\end{displaymath}


\noindent Each node of the tree is called a \textsl{goal}. A goal
is a record type containing the following three fields:
\begin{enumerate}
\item the conclusion $G$ to be proven;
\item a typing signature $\Gamma$ for the free variables in $G$;
\item if the goal is an internal node of the proof tree, the
definition $t(?_1,\ldots?_n)$ of an \textsl{existential variable}
(i.e. a possible undefined constant) $?$ of type $G$ in terms of the
existential variables of the children sub-goals. If the node is a
leaf, the existential variable maybe still undefined.
\end{enumerate}

Once all the existential variables have been defined the derivation is
completed, and a construction can be generated from the proof tree,
replacing each of the existential variables by its definition.  This
is exactly what happens when one of the commands
\texttt{Qed}, \texttt{Save} or \texttt{Defined} is invoked
(cf. Section \ref{Qed}). The saved theorem becomes a defined constant,
whose body is the proof object generated.

\paragraph{Important:} Before being added to the
context, the proof object is type-checked, in order to verify that it is
actually an object of the expected type $G$.  Hence, the correctness
of the proof actually does not depend on the tactics applied to
generate it or the machinery of the proof engine, but only on the
type-checker. In other words, extending the system with a potentially
bugged new tactic never endangers the consistency of the system.

\subsubsection{What is a Tactic?}
\label{WhatIsATactic}
%Let us now explain what is a tactic, and how the user can introduce
%new ones. 

From an operational point of view, the current state of the proof
engine is given by the mapping $emap$ from existential variables into
goals, plus a pointer to one of the leaf goals $g$.  Such a pointer
indicates where the proof tree will be refined by the application of a
\textsl{tactic}. A tactic is a function from the current state
$(g,emap)$ of the proof engine into a pair $(l,val)$. The first
component of this pair is the list of children sub-goals $g_1,\ldots
g_n$ of $g$ to be yielded by the tactic. The second one is a
\textsl{validation function}. Once the proof trees $\pi_1,\ldots
\pi_n$ for $g_1,\ldots g_n$ have been completed, this validation
function must yield a proof tree $(val\;\pi_1,\ldots \pi_n)$ deriving
$g$.

Tactics can be classified into \textsl{primitive} ones and
\textsl{defined} ones. Primitive tactics correspond to the five basic
operations of the proof engine:

\begin{enumerate}
\item Introducing a universally quantified variable into the local
context of the goal.
\item Defining an undefined existential variable 
\item Changing the conclusion of the goal for another
--definitionally equal-- term.
\item Changing the type of a variable in the local context for another
definitionally equal term.
\item Erasing a variable from the local context.
\end{enumerate}

\textsl{Defined} tactics are tactics constructed by combining these
primitive operations.  Defined tactics are registered in a hash table,
so that they can be introduced dynamically. In order to define such a
tactic table, it is necessary to fix what a \textsl{possible argument}
of a tactic may be. The type \texttt{tactic\_arg} of the possible
arguments for tactics is a union type including:
\begin{itemize}
\item quoted strings;
\item integers;
\item identifiers;
\item lists of identifiers;
\item plain terms, represented by its abstract syntax tree;
\item well-typed terms, represented by a construction;
\item a substitution for bound variables, like the
substitution in the tactic \\$\texttt{Apply}\;t\;\texttt{with}\;x:=t_1\ldots
x_n:=t_n$, (cf. Section \ref{Apply});
\item a reduction expression, denoting the reduction strategy to be
followed.
\end{itemize}
Therefore, for each function $tac:a \rightarrow tactic$ implementing a
defined tactic, an associated dynamic tactic $tacargs\_tac:
\texttt{tactic\_arg}\;list \rightarrow tactic$ calling $tac$ must be
written. The aim of the auxiliary function $tacargs\_tac$ is to inject
the arguments of the tactic $tac$ into the type of possible arguments
for a tactic.

The following function can be used for registering and calling a
defined tactic:

\begin{description}
\fun{val Tacmach.add\_tactic : \\ \qquad
string -> (tactic\_arg list ->tactic) -> unit}
    {\\ Registers a dynamic tactic with the given string as access index.}
\fun{val Tacinterp.vernac\_tactic : string*tactic\_arg list -> tactic}
    {Interprets a defined tactic given by its entry in the
     tactics table with a particular list of possible arguments.}
\fun{val Tacinterp.vernac\_interp        : CoqAst.t -> tactic}
    {Interprets a tactic expression formed combining \Coq's tactics and
          tacticals, and described by its abstract syntax tree.}
\end{description}

When programming a new tactic that calls an already defined tactic
$tac$, we have the choice between using the \ocaml{} function
implementing $tac$, or calling the tactic interpreter with the name
and arguments for interpreting $tac$. In the first case, a tactic call
will left the trace of the whole implementation of $tac$ in the proof
tree. In the second, the implementation of $tac$ will be hidden, and
only an invocation of $tac$ will be recalled (cf. the example of
Section \ref{ACompleteExample}.  The following combinators can be used
to hide the implementation of a tactic:

\begin{verbatim}
type 'a hiding_combinator = string -> ('a -> tactic) -> ('a -> tactic)
val Tacmach.hide_atomic_tactic  : string -> tactic -> tactic
val Tacmach.hide_constr_tactic  : constr          hiding_combinator
val Tacmach.hide_constrl_tactic : (constr list)   hiding_combinator
val Tacmach.hide_numarg_tactic  : int             hiding_combinator
val Tacmach.hide_ident_tactic   : identifier      hiding_combinator
val Tacmach.hide_identl_tactic  : identifier      hiding_combinator
val Tacmach.hide_string_tactic  : string          hiding_combinator
val Tacmach.hide_bindl_tactic   : substitution    hiding_combinator
val Tacmach.hide_cbindl_tactic  : 
          (constr * substitution) hiding_combinator
\end{verbatim}

These functions first register the tactic by a side effect, and then
yield a function calling the interpreter with the registered name and
the right injection into the type of possible arguments.

\subsection{Tactics and Tacticals Provided by \Coq}

The fifth logical module is the library of tacticals and basic tactics
provided by \Coq. This library is distributed into the directories
\texttt{tactics} and \texttt{src/tactics}. The former contains those
basic tactics that make use of the types contained in the basic state
of \Coq. For example, inversion or rewriting tactics are in the
directory \texttt{tactics}, since they make use of the propositional
equality type.  Those tactics which are independent from the context
--like for example \texttt{Cut}, \texttt{Intros}, etc-- are defined in
the directory \texttt{src/tactics}. This latter directory also
contains some useful tools for programming new tactics, referred in 
Section \ref{SomeUsefulToolsforWrittingTactics}.

In practice, it is very unusual that the list of sub-goals and the
validation function of the tactic must be explicitly constructed by
the user. In most of the cases, the implementation of a new tactic
consists in supplying the appropriate arguments to the basic tactics
and tacticals.

\subsubsection{Basic Tactics}

The file \texttt{Tactics} contain the implementation of the basic
tactics provided by \Coq. The following tactics are some of the most
used ones:

\begin{verbatim}
val Tactics.intro           : tactic
val Tactics.assumption      : tactic
val Tactics.clear           : identifier list -> tactic
val Tactics.apply           : constr -> constr substitution -> tactic
val Tactics.one_constructor : int -> constr substitution -> tactic
val Tactics.simplest_elim   : constr -> tactic
val Tactics.elimType        : constr -> tactic
val Tactics.simplest_case   : constr -> tactic
val Tactics.caseType        : constr -> tactic
val Tactics.cut             : constr -> tactic
val Tactics.reduce          : redexpr -> tactic
val Tactics.exact           : constr -> tactic
val Auto.auto               : int option -> tactic
val Auto.trivial            : tactic
\end{verbatim}

The functions hiding the implementation of these tactics are defined
in the module \texttt{Hiddentac}. Their names are prefixed by ``h\_''.

\subsubsection{Tacticals}
\label{OcamlTacticals}

The following tacticals can be used to combine already existing
tactics:

\begin{description}
\fun{val Tacticals.tclIDTAC : tactic}
    {The identity tactic: it leaves the goal as it is.}

\fun{val Tacticals.tclORELSE : tactic -> tactic -> tactic}
    {Tries the first tactic and in case of failure applies the second one.}

\fun{val Tacticals.tclTHEN : tactic -> tactic -> tactic}
  {Applies the first tactic and then the second one to each generated subgoal.}

\fun{val Tacticals.tclTHENS : tactic -> tactic list -> tactic}
    {Applies a tactic, and then applies each tactic of the tactic list to the
     corresponding generated subgoal.}

\fun{val Tacticals.tclTHENL : tactic -> tactic -> tactic}
    {Applies the first tactic, and then applies the second one to the last
     generated subgoal.}

\fun{val Tacticals.tclREPEAT : tactic -> tactic}
    {If the given tactic succeeds in producing a subgoal, then it
     is recursively applied to each generated subgoal, 
     and so on until it fails. }

\fun{val Tacticals.tclFIRST : tactic list -> tactic}
    {Tries the tactics of the given list one by one, until one of them
     succeeds.}

\fun{val Tacticals.tclTRY : tactic -> tactic}
    {Tries the given tactic and in case of failure applies the {\tt
    tclIDTAC} tactical to the original goal.}

\fun{val Tacticals.tclDO : int -> tactic -> tactic}
    {Applies the tactic a given number of times.}

\fun{val Tacticals.tclFAIL : tactic}
    {The always failing tactic: it raises a {\tt UserError} exception.}

\fun{val Tacticals.tclPROGRESS  : tactic -> tactic}
    {Applies the given tactic to the current goal and fails if the 
     tactic leaves the goal unchanged}

\fun{val Tacticals.tclNTH\_HYP :  int -> (constr -> tactic) -> tactic}
    {Applies a tactic to the nth hypothesis of the local context.
     The last hypothesis introduced correspond to the integer 1.}

\fun{val Tacticals.tclLAST\_HYP :  (constr -> tactic) -> tactic}
    {Applies a tactic to the last hypothesis introduced.}

\fun{val Tacticals.tclCOMPLETE : tactic -> tactic}
    {Applies a tactic and fails if the tactic did not solve completely the
      goal}

\fun{val Tacticals.tclMAP : ('a -> tactic) -> 'a list -> tactic}
    {Applied to the function \texttt{f} and the list \texttt{[x\_1;
        ... ; x\_n]}, this tactical applies the tactic
      \texttt{tclTHEN (f x1) (tclTHEN (f x2) ... ))))}}
    
\fun{val Tacicals.tclIF : (goal sigma -> bool) -> tactic -> tactic -> tactic}
    {If the condition holds, apply the first tactic; otherwise,
      apply the second one}

\end{description}


\subsection{The Vernacular Interpreter}

The sixth logical module of the implementation corresponds to the
interpreter of the vernacular phrases of \Coq. These phrases may be
expressions from the \gallina{} language (definitions), general
directives (setting commands) or tactics to be applied by the proof
engine. 

\subsection{The Parser and the Pretty-Printer}
\label{PrettyPrinter}

The last logical module is the parser and pretty printer of \Coq,
which is the interface between the vernacular interpreter and the
user. They translate the chains of characters entered at the input
into abstract syntax trees, and vice versa. Abstract syntax trees are
represented by labeled n-ary trees, and its type is called
\texttt{CoqAst.t}.  For instance, the abstract syntax tree associated
to the term $[x:A]x$ is:

\begin{displaymath}
\texttt{Node}
 ((0,6), "LAMBDA",
  [\texttt{Nvar}~((3, 4),"A");~\texttt{Slam}~((0,6),~Some~"x",~\texttt{Nvar}~((5,6),"x"))])
\end{displaymath}

The numbers correspond to \textsl{locations}, used to point to some
input line and character positions in the error messages. As it was
already explained in Section \ref{TypeChecker}, this term is then
translated into a construction term in order to be typed.

The parser of \Coq\ is implemented using \camlpppp. The lexer and the data
used by \camlpppp\ to generate the parser lay in the directory
\texttt{src/parsing}.  This directory also contains \Coq's
pretty-printer. The printing rules lay in the directory
\texttt{src/syntax}.  The different entries of the grammar are
described in the module \texttt{Pcoq.Entry}.  Let us present here two
important functions of this logical module:

\begin{description}
\fun{val Pcoq.parse\_string : 'a Grammar.Entry.e -> string -> 'a}
    {Parses a given string, trying to recognize a phrase
     corresponding to some entry in the grammar. If it succeeds,
     it yields a value associated to the grammar entry. For example,
     applied to the entry \texttt{Pcoq.Command.command}, this function
    parses a term of \Coq's language, and yields a value of type 
    \texttt{CoqAst.t}. When applied to the entry
    \texttt{Pcoq.Vernac.vernac}, it parses a vernacular command and
    returns the corresponding Ast.}
\fun{val gentermpr       : \\ \qquad 
path\_kind -> constr assumptions -> constr -> std\_ppcmds}
    {\\ Pretty-prints a well-typed term of certain kind (cf. Section
    \ref{SectionPaths}) under its context of typing assumption.}
\fun{val gentacpr        : CoqAst.t -> std\_ppcmds}
    {Pretty-prints a given abstract syntax tree representing a tactic
     expression.}
\end{description}

\subsection{The General Library}

In addition to the ones laying in the standard library of \ocaml{},
several useful modules about lists, arrays, sets, mappings, balanced
trees, and other frequently used data structures can be found in the
directory \texttt{lib}. Before writing a new one, check if it is not
already there!

\subsubsection{The module \texttt{Std}}
This module in the directory \texttt{src/lib/util} is opened by almost 
all modules of \Coq{}. Among other things, it contains a definition of 
the different kinds of errors used in \Coq{} :

\begin{description}
\fun{exception UserError of string * std\_ppcmds}
    {This is the class of ``users exceptions''. Such errors arise when 
      the user attempts to do something illegal, for example \texttt{Intro}
      when the current goal conclusion is not a product.}

\fun{val Std.error : string -> 'a}
    {For simple error messages}
\fun{val Std.errorlabstrm : string -> std\_ppcmds -> 'a}
    {See section \ref{PrettyPrinter} : this can be used if the user
      want to display a term or build a complex error message}

\fun{exception Anomaly of string * std\_ppcmds}
    {This for reporting bugs or things that should not
      happen. The tacticals \texttt{tclTRY} and
      \texttt{tclTRY} described in section \ref{OcamlTacticals} catch the
      exceptions of type \texttt{UserError}, but they don't catch the
      anomalies. So, in your code, don't raise any anomaly, unless you
      know what you are doing. We also recommend to avoid constructs
      such as \texttt{try ... with \_ -> ...} : such constructs can trap 
      an anomaly and make the debugging process harder.}

\fun{val Std.anomaly : string -> 'a}{}
\fun{val Std.anomalylabstrm : string -> std\_ppcmds -> 'a}{}
\end{description}

\section{The tactic writer mini-HOWTO}

\subsection{How to add a vernacular command}

The command to register a vernacular command can be found
in module \texttt{Vernacinterp}:

\begin{verbatim}
val vinterp_add : string * (vernac_arg list -> unit -> unit) -> unit;;
\end{verbatim}

The first argument is the name, the second argument is a function that
parses the arguments and returns a function of type
\texttt{unit}$\rightarrow$\texttt{unit} that do the job.

In this section we will show how to add a vernacular command
\texttt{CheckCheck} that print a type of a term and the type of its
type.

File \texttt{dcheck.ml}:

\begin{verbatim}
open Vernacinterp;;
open Trad;;
let _ = 
  vinterp_add 
   ("DblCheck",
    function [VARG_COMMAND com] ->
       (fun () -> 
          let evmap = Evd.mt_evd () 
          and sign = Termenv.initial_sign () in
           let {vAL=c;tYP=t;kIND=k} = 
                 fconstruct_with_univ evmap sign com in
             Pp.mSGNL [< Printer.prterm c; 'sTR ":"; 
                       Printer.prterm t; 'sTR ":"; 
                       Printer.prterm k >] )
      | _ -> bad_vernac_args "DblCheck")
;;
\end{verbatim}

Like for a new tactic, a new syntax entry must be created.

File \texttt{DCheck.v}:

\begin{verbatim}
Declare ML Module "dcheck.ml".

Grammar vernac vernac := 
  dblcheck [ "CheckCheck" comarg($c) ] -> [(DblCheck $c)].
\end{verbatim}

We are now able to test our new command:

\begin{verbatim}
Coq < Require DCheck.
Coq < CheckCheck O.
O:nat:Set
\end{verbatim}

Most Coq vernacular commands are registered in the module 
  \verb+src/env/vernacentries.ml+. One can see more examples here.

\subsection{How to keep a hashtable synchronous with the reset mechanism}

This is far more tricky. Some vernacular commands modify some
sort of state (for example by adding something in a hashtable). One
wants that \texttt{Reset} has the expected behavior with this
commands.

\Coq{} provides a general mechanism to do that. \Coq{} environments
contains objects of three kinds: CCI, FW and OBJ. CCI and FW are for
constants of the calculus. OBJ is a dynamically extensible datatype
that contains sections, tactic definitions, hints for auto, and so
on. 

The simplest example of use of such a mechanism is in file
\verb+src/proofs/macros.ml+ (which implements the \texttt{Tactic
  Definition} command). Tactic macros are stored in the imperative
hashtable \texttt{mactab}. There are two functions freeze and unfreeze
to make a copy of the table and to restore the state of table from the
copy. Then this table is declared using \texttt{Library.declare\_summary}.

What does \Coq{} with that ? \Coq{} defines synchronization points.
At each synchronisation point, the declared tables are frozen (that
is, a copy of this tables is stored).

When \texttt{Reset }$i$ is called, \Coq{} goes back to the first
synchronisation point that is above $i$ and ``replays'' all objects
between that point 
and $i$. It will re-declare constants, re-open section, etc.

So we need to declare a new type of objects, TACTIC-MACRO-DATA. To
``replay'' on object of that type is to add the corresponding tactic
macro to \texttt{mactab}

So, now, we can say that \texttt{mactab} is synchronous with the Reset
mechanism$^{\mathrm{TM}}$.

Notice that this works for hash tables but also for a single integer
(the Undo stack size, modified by the \texttt{Set Undo} command, for
example).

\subsection{The right way to access to Coq constants from your ML code}

With their long names, Coq constants are stored using:

\begin{itemize}
\item a section path
\item an identifier
\end{itemize}

The identifier is exactly the identifier that is used in \Coq{} to
denote the constant; the section path can be known using the
\texttt{Locate} command:

\begin{coq_example}
  Locate S.
  Locate nat.
  Locate eq.
\end{coq_example}

Now it is easy to get a constant by its name and section path:


\begin{verbatim}
let constant sp id = 
  Machops.global_reference (Names.gLOB (Termenv.initial_sign ())) 
    (Names.path_of_string sp) (Names.id_of_string id);;
\end{verbatim}


The only issue is that if one cannot put:


\begin{verbatim}
let coq_S = constant "#Datatypes#nat.cci" "S";;
\end{verbatim}


in his tactic's code. That is because this sentence is evaluated
\emph{before} the module \texttt{Datatypes} is loaded. The solution is
to use the lazy evaluation of \ocaml{}:


\begin{verbatim}
let coq_S = lazy (constant "#Datatypes#nat.cci" "S");;

... (Lazy.force coq_S) ...
\end{verbatim}


Be sure to call always Lazy.force behind a closure -- i.e. inside a
function body or behind the \texttt{lazy} keyword.

One can see examples of that technique in the source code of \Coq{},
for example 
\verb+tactics/contrib/polynom/ring.ml+ or 
\verb+tactics/contrib/polynom/coq_omega.ml+.

\section{Some Useful Tools for Writing Tactics}
\label{SomeUsefulToolsforWrittingTactics}
When the implementation of a tactic is not a straightforward
combination of tactics and tacticals, the module \texttt{Tacmach}
provides several useful functions for handling goals, calling the
type-checker, parsing terms, etc. This module is intended to be 
the interface of the proof engine for the user.

\begin{description}
\fun{val Tacmach.pf\_hyps               : goal sigma -> constr signature}
    {Projects the local typing context $\Gamma$ from a given goal $\Gamma\vdash ?:G$.} 
\fun{val pf\_concl              : goal sigma -> constr}
    {Projects the conclusion $G$ from a given goal $\Gamma\vdash ?:G$.}
\fun{val Tacmach.pf\_nth\_hyp            : goal sigma -> int -> identifier *
    constr}
    {Projects the $ith$ typing constraint $x_i:A_i$ from the local
     context of the given goal.}
\fun{val Tacmach.pf\_fexecute           : goal sigma -> constr -> judgement}
    {Given a goal whose local context is $\Gamma$ and a term $a$, this
     function infers a type $A$ and a kind $K$ such that the judgement
     $a:A:K$ is valid under $\Gamma$, or raises an exception if there
     is no such judgement. A judgement is just a record type containing
     the three terms $a$, $A$ and $K$.}
\fun{val Tacmach.pf\_infexecute : \\
     \qquad
goal sigma -> constr -> judgement * information}
    {\\ In addition to the typing judgement, this function also extracts 
     the $F_{\omega}$ program underlying the term.}
\fun{val Tacmach.pf\_type\_of            : goal sigma -> constr -> constr}
    {Infers a term $A$ such that $\Gamma\vdash a:A$ for a given term
    $a$, where $\Gamma$ is the local typing context of the goal.}
\fun{val Tacmach.pf\_check\_type         : goal sigma -> constr -> constr -> bool}
    {This function yields a type $A$ if the two given terms $a$ and $A$  verify $\Gamma\vdash
     a:A$ in the local typing context $\Gamma$ of the goal. Otherwise,
    it raises an exception.}
\fun{val Tacmach.pf\_constr\_of\_com      : goal sigma -> CoqAst.t -> constr}
    {Transforms an abstract syntax tree into a well-typed term of the
    language of constructions. Raises an exception if the term cannot
    be typed.}
\fun{val Tacmach.pf\_constr\_of\_com\_sort : goal sigma -> CoqAst.t -> constr}
    {Transforms an abstract syntax tree representing a type into
    a well-typed term of the language of constructions. Raises an
    exception if the term cannot be typed.}
\fun{val Tacmach.pf\_parse\_const        : goal sigma -> string -> constr}
    {Constructs the constant whose name is the given string.}
\fun{val
Tacmach.pf\_reduction\_of\_redexp  : \\
         \qquad goal sigma -> red\_expr -> constr -> constr}
    {\\ Applies a certain kind of reduction function, specified by an
     element of the type red\_expr.}
\fun{val Tacmach.pf\_conv\_x      : goal sigma -> constr -> constr -> bool}
    {Test whether  two given terms are definitionally equal.}
\end{description}

\subsection{Patterns}
\label{Patterns}

The \ocaml{} file \texttt{Pattern} provides a quick way for describing a
term pattern and performing second-order, binding-preserving, matching
on it. Patterns are described using an extension of \Coq's concrete
syntax, where the second-order meta-variables of the pattern are
denoted by indexed question marks. 

Patterns may depend on constants, and therefore only to make have
sense when certain theories have been loaded. For this reason, they
are stored with a \textsl{module-marker}, telling us which modules
have to be open in order to use the pattern. The following functions
can be used to store and retrieve patterns form the pattern table:

\begin{description}
\fun{val Pattern.make\_module\_marker : string list -> module\_mark}
    {Constructs a module marker from a list of module names.}
\fun{val Pattern.put\_pat : module\_mark -> string -> marked\_term}
    {Constructs a pattern from a parseable string containing holes
     and a module marker.}
\fun{val Pattern.somatches    : constr ->   marked\_term-> bool}
    {Tests if a term matches a pattern.} 
\fun{val dest\_somatch : constr -> marked\_term -> constr list}
    {If the term matches the pattern, yields the list of sub-terms
     matching the occurrences of the pattern variables (ordered from
     left to right). Raises a \texttt{UserError} exception if the term
     does not match the pattern.} 
\fun{val Pattern.soinstance : marked\_term -> constr list -> constr} 
    {Substitutes each hole in the pattern 
     by the corresponding term of the given the list.}
\end{description}

\paragraph{Warning:} Sometimes, a \Coq\ term may have invisible
sub-terms that the matching functions are nevertheless sensible to.
For example, the \Coq\ term $(?_1,?_2)$ is actually a shorthand for
the expression $(\texttt{pair}\;?\;?\;?_1\;?_2)$.
Hence, matching this term pattern 
with the term $(\texttt{true},\texttt{O})$ actually yields the list
$[?;?;\texttt{true};\texttt{O}]$ as result (and \textbf{not}
$[\texttt{true};\texttt{O}]$, as could be expected).

\subsection{Patterns on Inductive Definitions}

The module \texttt{Pattern} also includes some functions for testing
if the definition of an inductive type satisfies certain
properties. Such functions may be used to perform pattern matching
independently from the name given to the inductive type and the
universe it inhabits.  They yield the value $(\texttt{Some}\;r::l)$ if
the input term reduces into an application of an inductive type $r$ to
a list of terms $l$, and the definition of $r$ satisfies certain
conditions. Otherwise, they yield the value \texttt{None}.

\begin{description}
\fun{val Pattern.match\_with\_non\_recursive\_type : constr list option}
    {Tests if the inductive type $r$ has no recursive constructors}
\fun{val Pattern.match\_with\_disjunction : constr list option}
    {Tests if the inductive type $r$ is a non-recursive type
     such that all its constructors have a single argument.}
\fun{val Pattern.match\_with\_conjunction : constr list option}
    {Tests if the inductive type $r$ is a non-recursive type
     with a unique constructor.}
\fun{val Pattern.match\_with\_empty\_type  : constr list option}
    {Tests if the inductive type $r$ has no constructors at all}
\fun{val Pattern.match\_with\_equation    : constr list option}
    {Tests if the inductive type $r$ has a single constructor
     expressing the property of reflexivity for some type. For
     example, the types $a=b$, $A\mbox{==}B$ and $A\mbox{===}B$ satisfy
     this predicate.}
\end{description}

\subsection{Elimination Tacticals}

It is frequently the case that the subgoals generated by an
elimination can all be solved in a similar way, possibly parametrized
on some information about each case, like for example:
\begin{itemize}
\item the inductive type of the object being eliminated;
\item its arguments (if it is an inductive predicate);
\item the branch number;
\item the predicate to be proven;
\item the number of assumptions to be introduced by the case
\item the signature of the branch, i.e., for each argument of
the branch whether it is recursive or not.
\end{itemize}

The following tacticals can be useful to deal with such situations.
They  

\begin{description}
\fun{val Elim.simple\_elimination\_then : \\ \qquad
(branch\_args -> tactic) -> constr -> tactic}
    {\\ Performs the default elimination on the last argument, and then
     tries to solve the generated subgoals using a given parametrized
     tactic. The type branch\_args is a record type containing all 
     information mentioned above.}
\fun{val Elim.simple\_case\_then : \\ \qquad
(branch\_args -> tactic) -> constr -> tactic}
    {\\ Similarly, but it performs case analysis instead of induction.}
\end{description}

\section{A Complete Example}
\label{ACompleteExample}

In order to illustrate the implementation of a new tactic, let us come
back to the problem of deciding the equality of two elements of an
inductive type.

\subsection{Preliminaries}

Let us call \texttt{newtactic} the directory that will contain the
implementation of the new tactic. In this directory will lay two
files: a file \texttt{eqdecide.ml}, containing the \ocaml{} sources that
implements the tactic, and a \Coq\ file \texttt{Eqdecide.v}, containing
its associated grammar rules and the commands to generate a module
that can be loaded dynamically from \Coq's toplevel. 

To compile our project, we will create a \texttt{Makefile} with the
command \texttt{do\_Makefile} (see section \ref{Makefile}) :

\begin{quotation}
  \texttt{do\_Makefile eqdecide.ml EqDecide.v > Makefile}\\
  \texttt{touch .depend}\\
  \texttt{make depend}
\end{quotation}

We must have kept the sources of \Coq{} somewhere and to set an
environment variable \texttt{COQTOP} that points to that directory.

\subsection{Implementing the Tactic}

The file \texttt{eqdecide.ml} contains the implementation of the
tactic in \ocaml{}. Let us recall the main steps of the proof strategy
for deciding the proposition $(x,y:R)\{x=y\}+\{\neg x=y\}$ on the
inductive type $R$:
\begin{enumerate}
\item Eliminate $x$ and then $y$.
\item Try discrimination to solve those goals where $x$ and $y$ has
been introduced by different constructors.
\item If $x$ and $y$ have been introduced by the same constructor,
      then analyze one by one the corresponding pairs of arguments.
      If they are equal, rewrite one into the other. If they are
      not, derive a contradiction from the invectiveness of the
      constructor.
\item Once all the arguments have been rewritten, solve the left half
of the goal by reflexivity.
\end{enumerate}

In the sequel we implement these steps one by one. We start opening
the modules necessary for the implementation of the tactic:

\begin{verbatim}
open Names
open Term
open Tactics
open Tacticals
open Hiddentac
open Equality
open Auto
open Pattern
open Names
open Termenv
open Std
open Proof_trees
open Tacmach
\end{verbatim}

The first step of the procedure can be straightforwardly implemented as
follows:

\begin{verbatim}
let clear_last = (tclLAST_HYP (fun c -> (clear_one (destVar c))));;
\end{verbatim}

\begin{verbatim}
let mkBranches = 
        (tclTHEN  intro 
        (tclTHEN (tclLAST_HYP h_simplest_elim)
        (tclTHEN  clear_last
        (tclTHEN  intros 
        (tclTHEN (tclLAST_HYP h_simplest_case)
        (tclTHEN  clear_last
                  intros))))));;
\end{verbatim}

Notice the use of the tactical \texttt{tclLAST\_HYP}, which avoids to
give a (potentially clashing) name to the quantified variables of the
goal when they are introduced.

The second step of the procedure is implemented by the following
tactic:

\begin{verbatim}
let solveRightBranch  = (tclTHEN simplest_right discrConcl);;
\end{verbatim}

In order to illustrate how the implementation of a tactic can be 
hidden, let us do it with the tactic above:

\begin{verbatim}
let h_solveRightBranch =
    hide_atomic_tactic "solveRightBranch" solveRightBranch
;;
\end{verbatim}

As it was already mentioned in Section \ref{WhatIsATactic}, the
combinator \texttt{hide\_atomic\_tactic} first registers the tactic
\texttt{solveRightBranch} in the table, and returns a tactic which
calls the interpreter with the used to register it. Hence, when the
tactical \texttt{Info} is used, our tactic will just inform that
\texttt{solveRightBranch} was applied, omitting all the details
corresponding to \texttt{simplest\_right} and \texttt{discrConcl}.



The third step requires some auxiliary functions for constructing the
type $\{c_1=c_2\}+\{\neg c_1=c_2\}$ for a given inductive type $R$ and
two constructions $c_1$ and $c_2$, and for generalizing this type over
$c_1$ and $c_2$:

\begin{verbatim}
let mmk         = make_module_marker ["#Logic.obj";"#Specif.obj"];;
let eqpat       = put_pat mmk "eq";;                 
let sumboolpat  = put_pat mmk "sumbool";;             
let notpat      = put_pat mmk "not";;   
let eq          = get_pat eqpat;;
let sumbool     = get_pat sumboolpat;;
let not         = get_pat notpat;;

let mkDecideEqGoal rectype c1 c2 g = 
     let equality    = mkAppL [eq;rectype;c1;c2] in
     let disequality = mkAppL [not;equality]
     in  mkAppL [sumbool;equality;disequality]
;;
let mkGenDecideEqGoal rectype g = 
      let hypnames = ids_of_sign (pf_hyps g) in 
      let xname    = next_ident_away (id_of_string "x") hypnames
      and yname    = next_ident_away (id_of_string "y") hypnames
      in  (mkNamedProd xname rectype 
           (mkNamedProd yname rectype 
            (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
;;
\end{verbatim}

The tactic will depend on the \Coq modules \texttt{Logic} and
\texttt{Specif}, since we use the constants corresponding to
propositional equality (\texttt{eq}), computational disjunction
(\texttt{sumbool}), and logical negation (\texttt{not}), defined in
that modules. This is specified creating the module maker
\texttt{mmk} (cf. Section \ref{Patterns}).

The third step of the procedure can be divided into three sub-steps.
Assume that both $x$ and $y$ have been introduced by the same
constructor.  For each corresponding pair of arguments of that
constructor, we have to consider whether they are equal or not.  If
they are equal, the following tactic is applied to rewrite one into
the other:

\begin{verbatim}
let eqCase  tac = 
         (tclTHEN intro  
         (tclTHEN (tclLAST_HYP h_rewriteLR)
         (tclTHEN clear_last 
                  tac)))
;;
\end{verbatim}


If they are not equal, then the goal is contraposed and a
contradiction is reached form the invectiveness of the constructor:

\begin{verbatim}
let diseqCase = 
    let diseq  = (id_of_string "diseq") in
    let absurd = (id_of_string "absurd")
    in (tclTHEN (intro_using diseq)
       (tclTHEN  h_simplest_right
       (tclTHEN  red_in_concl
       (tclTHEN  (intro_using absurd)
       (tclTHEN  (h_simplest_apply (mkVar diseq))
       (tclTHEN  (h_injHyp absurd)
                  trivial ))))))
;;
\end{verbatim}

In the tactic above we have chosen to name the hypotheses because
they have to be applied later on. This introduces a potential risk
of name clashing if the context already contains other hypotheses 
also named ``diseq'' or ``absurd''.

We are now ready to implement the tactic \textsl{SolveArg}.  Given the
two arguments $a_1$ and $a_2$ of the constructor, this tactic cuts the
goal with the proposition $\{a_1=a_2\}+\{\neg a_1=a_2\}$, and then
applies the tactics above to each of the generated cases. If the
disjunction cannot be solved automatically, it remains as a sub-goal
to be proven.

\begin{verbatim}
let solveArg a1 a2 tac  g = 
     let rectype = pf_type_of g a1 in
     let decide  = mkDecideEqGoal rectype a1 a2 g
     in  (tclTHENS  (h_elimType decide) 
                      [(eqCase tac);diseqCase;default_auto]) g
;;
\end{verbatim}

The following tactic implements the third and fourth steps of the
proof procedure:

\begin{verbatim}
let conclpatt = put_pat mmk "{<?1>?2=?3}+{?4}"
;;
let solveLeftBranch rectype g = 
      let (_::(lhs::(rhs::_))) = 
               try (dest_somatch (pf_concl g) conclpatt) 
               with UserError ("somatch",_)-> error "Unexpected conclusion!" in
      let nparams   = mind_nparams rectype   in
      let getargs l = snd (chop_list nparams (snd (decomp_app l))) in
      let rargs   = getargs rhs
      and largs   = getargs lhs
      in  List.fold_right2 
             solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
;;
\end{verbatim}

Notice the use of a pattern to decompose the goal and obtain the
inductive type and the left and right hand sides of the equality. A
certain number of arguments correspond to the general parameters of
the type, and must be skipped over. Once the corresponding list of
arguments \texttt{rargs} and \texttt{largs} have been obtained, the
tactic \texttt{solveArg} is iterated on them, leaving a disjunction
whose left half can be solved by reflexivity.

The following tactic joints together the three steps of the 
proof procedure:

\begin{verbatim}
let initialpatt = put_pat mmk "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}"
;;
let decideGralEquality g = 
  let (typ::_) = try (dest_somatch (pf_concl g) initialpatt)
                 with UserError ("somatch",_) -> 
                        error "The goal does not have the expected form" in
  let headtyp = hd_app (pf_compute g typ) in
  let rectype = match (kind_of_term  headtyp) with
                 IsMutInd _ -> headtyp 
               | _          -> error ("This decision procedure only"
                                      " works for inductive objects") 
  in (tclTHEN   mkBranches 
     (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
;;
;;
\end{verbatim}

The tactic above can be specialized in two different ways: either to
decide a particular instance $\{c_1=c_2\}+\{\neg c_1=c_2\}$ of the
universal quantification; or to eliminate this property and obtain two
subgoals containing the hypotheses $c_1=c_2$ and $\neg c_1=c_2$
respectively.

\begin{verbatim}
let decideGralEquality = 
  (tclTHEN mkBranches (tclORELSE h_solveRightBranch solveLeftBranch))
;;
let decideEquality c1 c2 g = 
     let rectype = pf_type_of g c1 in
     let decide  = mkGenDecideEqGoal rectype g
     in  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
;;
let compare c1 c2 g = 
     let rectype = pf_type_of g c1 in
     let decide  = mkDecideEqGoal rectype c1 c2 g
     in  (tclTHENS (cut decide) 
                [(tclTHEN  intro 
                 (tclTHEN (tclLAST_HYP simplest_case)
                          clear_last));
                  decideEquality c1 c2]) g
;;
\end{verbatim}

Next, for each of the tactics that will have an entry in the grammar
we construct the associated dynamic one to be registered in the table
of tactics. This function can be used to overload a tactic name with
several similar tactics.  For example, the tactic proving the general
decidability property and the one proving a particular instance for
two terms can be grouped together with the following convention: if
the user provides two terms as arguments, then the specialized tactic
is used; if no argument is provided then the general tactic is invoked.

\begin{verbatim}
let dyn_decideEquality  args g =
      match args with 
       [(COMMAND com1);(COMMAND com2)]  -> 
          let c1 = pf_constr_of_com g com1
          and c2 = pf_constr_of_com g com2
          in  decideEquality c1 c2 g 
     | [] ->  decideGralEquality g
     | _  ->  error "Invalid arguments for dynamic tactic"
;;
add_tactic "DecideEquality" dyn_decideEquality
;;

let dyn_compare args g =
      match args with 
       [(COMMAND com1);(COMMAND com2)]  -> 
          let c1 = pf_constr_of_com g com1
          and c2 = pf_constr_of_com g com2
          in  compare c1 c2 g
     | _  ->  error "Invalid arguments for dynamic tactic"
;; 
add_tactic "Compare" tacargs_compare
;;
\end{verbatim}

This completes the implementation of the tactic. We turn now to the
\Coq file \texttt{Eqdecide.v}.


\subsection{The Grammar Rules}

Associated to the implementation of the tactic there is a \Coq\ file
containing the grammar and pretty-printing rules for the new tactic,
and the commands to generate an object module that can be then loaded
dynamically during a \Coq\ session. In order to generate an ML module,
the \Coq\ file must contain a
\texttt{Declare ML module} command for all the \ocaml{} files concerning
the implementation of the tactic --in our case there is only one file,
the file \texttt{eqdecide.ml}: 

\begin{verbatim}
Declare ML Module "eqdecide".
\end{verbatim}

The following grammar and pretty-printing rules are
self-explanatory. We refer the reader to the Section \ref{Grammar} for
the details:

\begin{verbatim}
Grammar tactic simple_tactic :=
  EqDecideRuleG1 
       [ "Decide"  "Equality" comarg($com1)  comarg($com2)] -> 
       [(DecideEquality $com1 $com2)]
| EqDecideRuleG2 
       [ "Decide" "Equality"  ] -> 
       [(DecideEquality)]
| CompareRule 
       [ "Compare" comarg($com1) comarg($com2)] -> 
       [(Compare $com1 $com2)].

Syntax tactic level 0:
  EqDecideRulePP1 
       [(DecideEquality)]   -> 
       ["Decide" "Equality"]
| EqDecideRulePP2 
       [(DecideEquality $com1 $com2)]   -> 
       ["Decide" "Equality" $com1 $com2]
| ComparePP 
       [(Compare $com1 $com2)] -> 
       ["Compare" $com1 $com2].
\end{verbatim}


\paragraph{Important:} The names used to label the abstract syntax tree 
in the grammar rules ---in this case ``DecideEquality'' and
``Compare''--- must be the same as the name used to register the
tactic in the tactics table. This is what makes the links between the
input entered by the user and the tactic executed by the interpreter.

\subsection{Loading the Tactic}

Once the module \texttt{EqDecide.v} has been compiled, the tactic can
be dynamically loaded using the \texttt{Require} command. 

\begin{coq_example}
Require EqDecide.
Goal (x,y:nat){x=y}+{~x=y}.
Decide Equality.
\end{coq_example}

The implementation of the tactic can be accessed through the
tactical \texttt{Info}:
\begin{coq_example}
Undo.
Info Decide Equality.
\end{coq_example}
\begin{coq_eval}
Abort.
\end{coq_eval}

Remark that the task performed by the tactic \texttt{solveRightBranch}
is not displayed, since we have chosen to hide its implementation.

\section{Testing and Debugging your Tactic}
\label{test-and-debug}

When your tactic does not behave as expected, it is possible to trace
it dynamically from \Coq. In order to do this, you have first to leave
the toplevel of \Coq, and come back to the \ocaml{} interpreter. This can
be done using the command \texttt{Drop} (cf. Section \ref{Drop}). Once
in the \ocaml{} toplevel, load the file \texttt{tactics/include.ml}.
This file installs several pretty printers for proof trees, goals,
terms, abstract syntax trees, names, etc.  It also contains the
function \texttt{go:unit -> unit} that enables to go back to \Coq's
toplevel. 

The modules \texttt{Tacmach} and \texttt{Pfedit} contain some basic
functions for extracting information from the state of the proof
engine. Such functions can be used to debug your tactic if
necessary. Let us mention here some of them:

\begin{description}
\fun{val get\_pftreestate         : unit -> pftreestate}
    {Projects the current state of the proof engine.}
\fun{val proof\_of\_pftreestate    : pftreestate -> proof}
    {Projects the current state of the proof tree. A pretty-printer 
      displays it in a readable form.  }
\fun{val top\_goal\_of\_pftreestate : pftreestate -> goal sigma}
    {Projects the goal and the existential variables mapping from
     the current state of the proof engine.} 
\fun{val nth\_goal\_of\_pftreestate : int -> pftreestate -> goal sigma}
    {Projects the goal and mapping corresponding to the $nth$ subgoal
     that remains to be proven}
\fun{val traverse                : int -> pftreestate -> pftreestate}
    {Yields the children of the node that the current state of the 
     proof engine points to.}
\fun{val solve\_nth\_pftreestate   : \\ \qquad
int -> tactic -> pftreestate ->  pftreestate}
     {\\ Provides the new state of the proof engine obtained applying 
      a given tactic to some unproven sub-goal.}
\end{description}

Finally, the traditional \ocaml{} debugging tools like the directives
\texttt{trace} and \texttt{untrace} can be used to follow the
execution of your functions. Frequently, a better solution is to use
the \ocaml{} debugger, see Chapter \ref{Utilities}.


%\end{document}