X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2Fdoc%2Fbody.tex;h=424dee225871b7188ae0e7b3ad53080d316fb4ba;hb=5fd3862ee12950c8441a313bdc1e0c2cb4078cf0;hp=3c537d43be048b5702b0eaefe49e8556d46535a5;hpb=a8a60abba413c68ee65f3322f6b4028af34ed9e6;p=helm.git

diff --git a/helm/ocaml/tactics/doc/body.tex b/helm/ocaml/tactics/doc/body.tex
index 3c537d43b..424dee225 100644
--- a/helm/ocaml/tactics/doc/body.tex
+++ b/helm/ocaml/tactics/doc/body.tex
@@ -1,7 +1,229 @@
 
-\section{Semantics}
+\section{Tinycals: \MATITA{} tacticals}
 
-\subsection{Language}
+\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}
+  \resizebox{\textwidth}{!}{\includegraphics{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}
+  \resizebox{\textwidth}{!}{\includegraphics{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}
@@ -24,7 +246,7 @@
 \end{array}
 \]
 
-\subsection{Status}
+\subsubsection{Status}
 
 \[
 \begin{array}{rcll}
@@ -98,7 +320,7 @@
   top-level $\Gamma$)}, \ISFRESH(l)$.
 \end{itemize}
 
-\subsection{Semantics}
+\subsubsection{Semantics}
 
 \[
 \begin{array}{rcll}
@@ -245,3 +467,8 @@
 \end{array}
 \]
 
+\subsection{Related works}
+
+In~\cite{fk:strata2003}, Kirchner described a small step semantics for Coq
+tacticals and PVS strategies.
+