- new tactic subst removes simple non recursive equalities from the context

[helm.git] / components / tactics / doc / body.tex

\section{Tinycals: \MATITA{} tacticals}

\subsection{Introduction}

% outline:
% - script

Most of modern mainstream proof assistants enable input of proofs of
propositions using a textual language. Compilation units written in such
languages are sequence of textual \emph{statements} and are usually called
\emph{scripts} as a whole. Scripts are so entangled with proof assistants that
they drived the design of state of the art of their Graphical User Interfaces
(GUIs). Fig.~\ref{fig:proofgeneral} is a screenshot of Proof General, a generic
proof assistant interface based on Emacs widely used and compatible with systems
like Coq, Isabelle, PhoX, LEGO, and many more. Other system specific GUIs exist
but share the same design, understanding it and they way such GUIs are operated
is relevant to our discussion.

%\begin{figure}[ht]
% \begin{center}
%  \includegraphic{pics/pg-coq-screenshot}
%  \caption{Proof General: a generic interface for proof assistants}
%  \label{fig:proofgeneral}
% \end{center}
%\end{figure}

% - modo di lavorare

The paradigm behind such GUIs is quite simple. The window on the left is an
editable text area containing the script and split in two by an \emph{execution
point} (the point where background color changes). The part starting at the
beginning of the script and ending at the marker (distinguishable for having a
light blue background in the picture) contains the sequence of statements which
have already been fed into the system. We will call this former part
\emph{locked area} since the user is not free to change it as her willing. The
remaining part, which extends until the end of the script, is named
\emph{scratch area} and can be freely modified. The window on the right is
read-only for the user and includes at the top the current proof status, when
some proof is ongoing, and at the bottom a message area used for error messages
or other feedback from the system to the user. The user usually proceed
alternating editing of the scratch area and execution point movements (forward
to evaluate statements and backward to retract statements if she need to change
something in the locked area).

Execution point movements are not free, but constrained by the structure of the
script language used. The granularity is that of statements. In systems like Coq
or \MATITA{} examples of statements are: inductive definitions, theorems, and
tactics. \emph{Tactics} are the building blocks of proofs. For example, the
following script snippet contains a theorem about a relationship of natural
minus with natural plus, along with its proof (line numbers have been added for
the sake of presentation) as it can be found in the standard library of the
\MATITA{} proof assistant:

%\begin{example}
%\begin{Verbatim}
%theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
% intros.
% cut (m+p \le n \or m+p \nleq n).
% elim Hcut.
% symmetry.
% apply plus_to_minus.
% rewrite > assoc_plus.
% rewrite > (sym_plus p).
% rewrite < plus_minus_m_m.
% rewrite > sym_plus.
% rewrite < plus_minus_m_m.
% reflexivity.
% apply (trans_le ? (m+p)).
% rewrite < sym_plus.
% apply le_plus_n.
% assumption.
% apply le_plus_to_minus_r.
% rewrite > sym_plus.
% assumption.   
% rewrite > (eq_minus_n_m_O n (m+p)).
% rewrite > (eq_minus_n_m_O (n-m) p).
% reflexivity.
% apply le_plus_to_minus.
% apply lt_to_le.
% rewrite < sym_plus.
% apply not_le_to_lt.
% assumption.
% apply lt_to_le.
% apply not_le_to_lt.
% assumption.          
% apply (decidable_le (m+p) n).
%qed.
%\end{Verbatim}
%\end{example}

The script snippet is made of 32 statements, one per line (but this is not a
requirement of the \MATITA{} script language, namely \emph{Grafite}). The first
statement is the assertion that the user want to prove a proposition with a
given type, specified after the ``\texttt{:}'', its execution will cause
\MATITA{} to enter the proof state showing to the user the list of goals that
still need to be proved to conclude the proof. The last statement (\texttt{Qed})
is an assertion that the proof is completed. All intertwining statements are
tactic applications.

Given the constraint we mentioned about execution point, while inserting (or
replaying) the above script, the user may position it at the end of any line,
having feedback about the status of the proof in that point. See for example
Fig.~\ref{fig:matita} where an intermediate proof status is shown.

%\begin{figure}[ht]
% \begin{center}
%  \includegraphic{matita_screenshot}
%  \caption{Matita: ongoing proof}
%  \label{fig:matita}
% \end{center}
%\end{figure}

% - script: sorgenti di un linguaggio imperativo, oggetti la loro semantica
% - script = sequenza di comandi

You can create an analogy among scripts and sources written in an imperative
programming language, seeing proofs as the denotational semantics of that
language. In such analogy the language used in the script of
Fig.~\ref{fig:matita} is rather poor offering as the only programming construct
the sequential composition of tactic application. What enables step by step
execution is the operational semantics of each tactic application (i.e. how it
changes the current proof status).

%  - pro: concisi

This kind of scripts have both advantages and drawbacks. Among advantages we can
for sure list the effectiveness of the language. In spite of being longer than
the corresponding informal text version of the proof (a gap hardly fillable with
proof assistants~\cite{debrujinfactor}), the script is fast to write in
interactive use, enable cut and paste approaches, and gives a lot of flexibility
(once the syntax is known of course) in tactic application via additional flags
that can be easily passed to them.

%  - cons: non strutturati, hanno senso solo via reply

Unfortunately, drawbacks are non negligible. Scripts like those of
Fig.~\ref{fig:matita} are completely unstructured and hardly can be assigned a
meaning simply looking at them. Even experienced users, that knows the details
of all involved tactics, can hardly figure what a script mean without replaying
the proof in their heads. This indeed is a key aspect of scripts: they are
meaningful via \emph{reply}. People interested in understanding a formal proof
written as a script usually start the preferred tool and execute it step by
step. A contrasting approach compared to what happens with high level
programming languages where looking at the code is usually enough to understand
its details.

%  - cons: poco robusti (wrt cambiamenti nelle tattiche, nello statement, ...)

Additionally, scripts are usually not robust against changes, intending with
that term both changes in the statement that need to be proved (e.g.
strenghtening of an inductive hypothesis) and changes in the implementation of
involved tactics. This drawback can force backward compatibility and slow down
systems development. A real-life example in the history of \MATITA{} was the
reordering of goals after tactic application; the total time needed to port the
(tiny at the time) standard library of no more that 30 scripts was 2 days work.
Having the scripts being structured the task could have been done in much less
time and even automated.

Tacticals are an attempt at solving this drawbacks.

\subsection{Tacticals}

% - script = sequenza di comandi + tatticali

\ldots descrizione dei tatticali \ldots

%  - pro: fattorizzazione

Tacticals as described above have several advantages with respect to plain
sequential application of tactics. First of all they enable a great amount of
factorization of proofs using the sequential composition ``;'' operator. Think
for example at proofs by induction on inductive types with several constructors,
which are so frequent when formalizing properties from the computer science
field. It is often the case that several, or even all, cases can be dealt with
uniform strategies, which can in turn by coded in a single script snipped which
can appear only once, at the right hand side of a ``;''.

%  - pro: robustezza

Scripts properly written using the tacticals above are even more robust with
respect to changes. The additional amount of flexibility is given by
``conditional'' constructs like \texttt{try}, \texttt{solve}, and
\texttt{first}. Using them the scripts no longer contain a single way of
proceeding from one status of the proof to another, they can list more. The wise
proof coder may exploit this mechanism providing fallbacks in order to be more
robust to future changes in tactics implementation. Of course she is not
required to!

%  - pro: strutturazione delle prove (via branching)

Finally, the branching constructs \texttt{[}, \texttt{|}, and \texttt{]} enable
proof structuring. Consider for example an alternative, branching based, version
of the example above:

%\begin{example}
%\begin{Verbatim}
%...
%\end{Verbatim}
%\end{example}

Tactic applications are the same of the previous version of the script, but
branching tacticals are used. The above version is highly more readable and
without executing it key points of the proofs like induction cases can be
observed.

%  - tradeoff: utilizzo dei tatticali vs granularita' dell'esecuzione
%    (impossibile eseguire passo passo)

One can now wonder why thus all scripts are not written in a robust, concise and
structured fashion. The reason is the existence of an unfortunate tradeoff
between the need of using tacticals and the impossibility of executing step by
step \emph{inside} them. Indeed, trying to mimic the structured version of the
proof above in GUIs like Proof General or CoqIDE will result in a single macro
step that will bring you from the beginning of the proof directly at the end of
it!

Tinycals as implemented in \MATITA{} are a solution to this problem, preserving
the usual tacticals semantics, giving meaning to intermediate execution point
inside complex tacticals.

\subsection{Tinycals}

\subsection{Tinycals semantics}

\subsubsection{Language}

\[
\begin{array}{rcll}
 S & ::= & & \mbox{(\textbf{continuationals})}\\
   &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
   &  |  & \DOT & \mbox{(dot)} \\
   &  |  & \SEMICOLON & \mbox{(semicolon)} \\
   &  |  & \BRANCH & \mbox{(branch)} \\
   &  |  & \SHIFT & \mbox{(shift)} \\
   &  |  & \POS{i} & \mbox{(relative positioning)} \\
   &  |  & \MERGE & \mbox{(merge)} \\[2ex]
   &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
   &  |  & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
   &  |  & S ~ S & \mbox{(sequential composition)} \\[2ex]
   T & : := & & \mbox{(\textbf{tactics})}\\
     &   & \SKIP & \mbox{(skip)} \\
     & | & \mathtt{reflexivity} & \\
     & | & \mathtt{apply}~t & \\
     & | & \dots &
\end{array}
\]

\subsubsection{Status}

\[
\begin{array}{rcll}
 \xi & & & \mbox{(proof status)} \\
 \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]

 \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
 \mathit{locator} & = & \INT\times\SWITCH & \\
 \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]

 \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
 \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
 \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]

 \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
 \\[2ex]

 \mathit{status} & = & \xi\times\mathit{stack} \\
\end{array}
\]

\paragraph{Utilities}
\begin{itemize}
 \item $\ZEROPOS([g_1;\cdots;g_n]) =
  [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
 \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
  [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
 \item $\ISFRESH(s) =
  \left\{
  \begin{array}{ll}
   \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
   \mathit{false} & \mathrm{otherwise} \\
  \end{array}
  \right.$
 \item $\FILTEROPEN(\mathit{locs})=
  \left\{
  \begin{array}{ll}
   [] & \mathrm{if}~\mathit{locs} = [] \\
   \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
   \FILTEROPEN(\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  \end{array}
  \right.$
 \item $\REMOVEGOALS(G,\mathit{locs}) =
  \left\{
  \begin{array}{ll}
   [] & \mathrm{if}~\mathit{locs} = [] \\
   \REMOVEGOALS(G,\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
     \land g\in G\\
   hd :: \REMOVEGOALS(G,\mathit{tl})
   & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
  \end{array}
  \right.$
 \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
  it returns a new stack $S'$ identical to the given one with the exceptions
  that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
  components and removed from $\tau$ and $\kappa$ components.
 \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
  on a given stack $S$, appearing in an \OPEN{} switch.
\end{itemize}

\paragraph{Invariants}
\begin{itemize}
 \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
  \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
  $\tau$ and $\kappa$ components has an \OPEN~switch).
 \item Unless \FOCUS{} is used the stack contains no duplicate goals.
 \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
  top-level $\Gamma$)}, \ISFRESH(l)$.
\end{itemize}

\subsubsection{Semantics}

\[
\begin{array}{rcll}
 \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
  \mbox{(continuationals semantics)} \\
 \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
  \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
\end{array}
\]

\[
\begin{array}{rcl}
 \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
  \xi\times\GOAL~\LIST\times\GOAL~\LIST
\end{array}
\]

\[
\begin{array}{rlcc}
 \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
 \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
\end{array}
\]

\[
\begin{array}{rcl}

 \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 & =
 & \langle
   \xi_n,
   \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
%    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
   :: \DEEPCLOSE(G^c_n,S)
   \rangle
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
  \Gamma' = \ZEROPOS(G^o_n)
  \land \tau' = \REMOVEGOALS(G^c_n,\tau)
  \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
 }
 \\[1ex]
 \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
 \left\{
 \begin{array}{rcll}
  \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
  \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
  & =
  & \langle\xi_i, G^o_i, G^c_i\rangle
  & l_{i+1}\in G^c_i \\
  \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
  & =
  & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
  & l_{i+1}\not\in G^c_i \\[1ex]
  & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
 \end{array}
 \right.
 }
 \\[6ex]

 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
 & =
 & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
 \\[2ex]

 \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
 & =
 & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
 \\[2ex]

 \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]

 \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
 \quad 
 & =
 & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
   ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
 \\[1ex]
 & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
 \\[2ex]

 \SEM{~\SHIFT~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
  ::S}
 & =
 & \langle
   \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
        ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
   \rangle
 \\[1ex]
 & & \mathrm{where} ~ n\geq 1
 \\[2ex]

 \SEM{~\POS{i}~}
  {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 & =
 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
   ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
 \\[1ex]
 & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
 \\[2ex]

 \SEM{~\POS{i}~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
  ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
 & =
 & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
 ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
   \rangle
 \\[1ex]
 & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
 \\[2ex]

 \SEM{~\MERGE~}
  {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
  ::S}
 & =
 & \langle \xi,
   \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
   :: S
   \rangle
 \\[2ex]

 \SEM{\FOCUS{g_1,\dots,g_n}}{S}
 & = 
 & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
   ::\DEEPCLOSE(S)
   \rangle
 \\[1ex]
 & & \mathrm{where} ~
 \forall i=1,\dots,n,~g_i\in\GOALS(S)
 \\[2ex]

 \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
 & = 
 & \langle \xi, S\rangle \\[2ex]

\end{array}
\]

\subsection{Related works}

In~\cite{fk:strata2003}, Kirchner described a small step semantics for Coq
tacticals and PVS strategies.