X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=components%2Ftactics%2Fdoc%2Fbody.tex;fp=components%2Ftactics%2Fdoc%2Fbody.tex;h=8b7bbc9b043d1aa3a679131050c593ca1d17afd2;hp=0000000000000000000000000000000000000000;hb=f61af501fb4608cc4fb062a0864c774e677f0d76;hpb=58ae1809c352e71e7b5530dc41e2bfc834e1aef1 diff --git a/components/tactics/doc/body.tex b/components/tactics/doc/body.tex new file mode 100644 index 000000000..8b7bbc9b0 --- /dev/null +++ b/components/tactics/doc/body.tex @@ -0,0 +1,474 @@ + +\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. +