]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/tactics/doc/body.tex
abstracted pretty printers over inner pretty printing units (terms, lazy terms, and...
[helm.git] / helm / ocaml / tactics / doc / body.tex
1
2 \section{Tinycals: \MATITA{} tacticals}
3
4 \subsection{Introduction}
5
6 % outline:
7 % - script
8
9 Most of modern mainstream proof assistants enable input of proofs of
10 propositions using a textual language. Compilation units written in such
11 languages are sequence of textual \emph{statements} and are usually called
12 \emph{scripts} as a whole. Scripts are so entangled with proof assistants that
13 they drived the design of state of the art of their Graphical User Interfaces
14 (GUIs). Fig.~\ref{fig:proofgeneral} is a screenshot of Proof General, a generic
15 proof assistant interface based on Emacs widely used and compatible with systems
16 like Coq, Isabelle, PhoX, LEGO, and many more. Other system specific GUIs exist
17 but share the same design, understanding it and they way such GUIs are operated
18 is relevant to our discussion.
19
20 %\begin{figure}[ht]
21 % \begin{center}
22 %  \includegraphic{pics/pg-coq-screenshot}
23 %  \caption{Proof General: a generic interface for proof assistants}
24 %  \label{fig:proofgeneral}
25 % \end{center}
26 %\end{figure}
27
28 % - modo di lavorare
29
30 The paradigm behind such GUIs is quite simple. The window on the left is an
31 editable text area containing the script and split in two by an \emph{execution
32 point} (the point where background color changes). The part starting at the
33 beginning of the script and ending at the marker (distinguishable for having a
34 light blue background in the picture) contains the sequence of statements which
35 have already been fed into the system. We will call this former part
36 \emph{locked area} since the user is not free to change it as her willing. The
37 remaining part, which extends until the end of the script, is named
38 \emph{scratch area} and can be freely modified. The window on the right is
39 read-only for the user and includes at the top the current proof status, when
40 some proof is ongoing, and at the bottom a message area used for error messages
41 or other feedback from the system to the user. The user usually proceed
42 alternating editing of the scratch area and execution point movements (forward
43 to evaluate statements and backward to retract statements if she need to change
44 something in the locked area).
45
46 Execution point movements are not free, but constrained by the structure of the
47 script language used. The granularity is that of statements. In systems like Coq
48 or \MATITA{} examples of statements are: inductive definitions, theorems, and
49 tactics. \emph{Tactics} are the building blocks of proofs. For example, the
50 following script snippet contains a theorem about a relationship of natural
51 minus with natural plus, along with its proof (line numbers have been added for
52 the sake of presentation) as it can be found in the standard library of the
53 \MATITA{} proof assistant:
54
55 %\begin{example}
56 %\begin{Verbatim}
57 %theorem eq_minus_minus_minus_plus: \forall n,m,p:nat. (n-m)-p = n-(m+p).
58 % intros.
59 % cut (m+p \le n \or m+p \nleq n).
60 % elim Hcut.
61 % symmetry.
62 % apply plus_to_minus.
63 % rewrite > assoc_plus.
64 % rewrite > (sym_plus p).
65 % rewrite < plus_minus_m_m.
66 % rewrite > sym_plus.
67 % rewrite < plus_minus_m_m.
68 % reflexivity.
69 % apply (trans_le ? (m+p)).
70 % rewrite < sym_plus.
71 % apply le_plus_n.
72 % assumption.
73 % apply le_plus_to_minus_r.
74 % rewrite > sym_plus.
75 % assumption.   
76 % rewrite > (eq_minus_n_m_O n (m+p)).
77 % rewrite > (eq_minus_n_m_O (n-m) p).
78 % reflexivity.
79 % apply le_plus_to_minus.
80 % apply lt_to_le.
81 % rewrite < sym_plus.
82 % apply not_le_to_lt.
83 % assumption.
84 % apply lt_to_le.
85 % apply not_le_to_lt.
86 % assumption.          
87 % apply (decidable_le (m+p) n).
88 %qed.
89 %\end{Verbatim}
90 %\end{example}
91
92 The script snippet is made of 32 statements, one per line (but this is not a
93 requirement of the \MATITA{} script language, namely \emph{Grafite}). The first
94 statement is the assertion that the user want to prove a proposition with a
95 given type, specified after the ``\texttt{:}'', its execution will cause
96 \MATITA{} to enter the proof state showing to the user the list of goals that
97 still need to be proved to conclude the proof. The last statement (\texttt{Qed})
98 is an assertion that the proof is completed. All intertwining statements are
99 tactic applications.
100
101 Given the constraint we mentioned about execution point, while inserting (or
102 replaying) the above script, the user may position it at the end of any line,
103 having feedback about the status of the proof in that point. See for example
104 Fig.~\ref{fig:matita} where an intermediate proof status is shown.
105
106 %\begin{figure}[ht]
107 % \begin{center}
108 %  \includegraphic{matita_screenshot}
109 %  \caption{Matita: ongoing proof}
110 %  \label{fig:matita}
111 % \end{center}
112 %\end{figure}
113
114 % - script: sorgenti di un linguaggio imperativo, oggetti la loro semantica
115 % - script = sequenza di comandi
116
117 You can create an analogy among scripts and sources written in an imperative
118 programming language, seeing proofs as the denotational semantics of that
119 language. In such analogy the language used in the script of
120 Fig.~\ref{fig:matita} is rather poor offering as the only programming construct
121 the sequential composition of tactic application. What enables step by step
122 execution is the operational semantics of each tactic application (i.e. how it
123 changes the current proof status).
124
125 %  - pro: concisi
126
127 This kind of scripts have both advantages and drawbacks. Among advantages we can
128 for sure list the effectiveness of the language. In spite of being longer than
129 the corresponding informal text version of the proof (a gap hardly fillable with
130 proof assistants~\cite{debrujinfactor}), the script is fast to write in
131 interactive use, enable cut and paste approaches, and gives a lot of flexibility
132 (once the syntax is known of course) in tactic application via additional flags
133 that can be easily passed to them.
134
135 %  - cons: non strutturati, hanno senso solo via reply
136
137 Unfortunately, drawbacks are non negligible. Scripts like those of
138 Fig.~\ref{fig:matita} are completely unstructured and hardly can be assigned a
139 meaning simply looking at them. Even experienced users, that knows the details
140 of all involved tactics, can hardly figure what a script mean without replaying
141 the proof in their heads. This indeed is a key aspect of scripts: they are
142 meaningful via \emph{reply}. People interested in understanding a formal proof
143 written as a script usually start the preferred tool and execute it step by
144 step. A contrasting approach compared to what happens with high level
145 programming languages where looking at the code is usually enough to understand
146 its details.
147
148 %  - cons: poco robusti (wrt cambiamenti nelle tattiche, nello statement, ...)
149
150 Additionally, scripts are usually not robust against changes, intending with
151 that term both changes in the statement that need to be proved (e.g.
152 strenghtening of an inductive hypothesis) and changes in the implementation of
153 involved tactics. This drawback can force backward compatibility and slow down
154 systems development. A real-life example in the history of \MATITA{} was the
155 reordering of goals after tactic application; the total time needed to port the
156 (tiny at the time) standard library of no more that 30 scripts was 2 days work.
157 Having the scripts being structured the task could have been done in much less
158 time and even automated.
159
160 Tacticals are an attempt at solving this drawbacks.
161
162 \subsection{Tacticals}
163
164 % - script = sequenza di comandi + tatticali
165
166 \ldots descrizione dei tatticali \ldots
167
168 %  - pro: fattorizzazione
169
170 Tacticals as described above have several advantages with respect to plain
171 sequential application of tactics. First of all they enable a great amount of
172 factorization of proofs using the sequential composition ``;'' operator. Think
173 for example at proofs by induction on inductive types with several constructors,
174 which are so frequent when formalizing properties from the computer science
175 field. It is often the case that several, or even all, cases can be dealt with
176 uniform strategies, which can in turn by coded in a single script snipped which
177 can appear only once, at the right hand side of a ``;''.
178
179 %  - pro: robustezza
180
181 Scripts properly written using the tacticals above are even more robust with
182 respect to changes. The additional amount of flexibility is given by
183 ``conditional'' constructs like \texttt{try}, \texttt{solve}, and
184 \texttt{first}. Using them the scripts no longer contain a single way of
185 proceeding from one status of the proof to another, they can list more. The wise
186 proof coder may exploit this mechanism providing fallbacks in order to be more
187 robust to future changes in tactics implementation. Of course she is not
188 required to!
189
190 %  - pro: strutturazione delle prove (via branching)
191
192 Finally, the branching constructs \texttt{[}, \texttt{|}, and \texttt{]} enable
193 proof structuring. Consider for example an alternative, branching based, version
194 of the example above:
195
196 %\begin{example}
197 %\begin{Verbatim}
198 %...
199 %\end{Verbatim}
200 %\end{example}
201
202 Tactic applications are the same of the previous version of the script, but
203 branching tacticals are used. The above version is highly more readable and
204 without executing it key points of the proofs like induction cases can be
205 observed.
206
207 %  - tradeoff: utilizzo dei tatticali vs granularita' dell'esecuzione
208 %    (impossibile eseguire passo passo)
209
210 One can now wonder why thus all scripts are not written in a robust, concise and
211 structured fashion. The reason is the existence of an unfortunate tradeoff
212 between the need of using tacticals and the impossibility of executing step by
213 step \emph{inside} them. Indeed, trying to mimic the structured version of the
214 proof above in GUIs like Proof General or CoqIDE will result in a single macro
215 step that will bring you from the beginning of the proof directly at the end of
216 it!
217
218 Tinycals as implemented in \MATITA{} are a solution to this problem, preserving
219 the usual tacticals semantics, giving meaning to intermediate execution point
220 inside complex tacticals.
221
222 \subsection{Tinycals}
223
224 \subsection{Tinycals semantics}
225
226 \subsubsection{Language}
227
228 \[
229 \begin{array}{rcll}
230  S & ::= & & \mbox{(\textbf{continuationals})}\\
231    &     & \TACTIC{T} & \mbox{(tactic)}\\[2ex]
232    &  |  & \DOT & \mbox{(dot)} \\
233    &  |  & \SEMICOLON & \mbox{(semicolon)} \\
234    &  |  & \BRANCH & \mbox{(branch)} \\
235    &  |  & \SHIFT & \mbox{(shift)} \\
236    &  |  & \POS{i} & \mbox{(relative positioning)} \\
237    &  |  & \MERGE & \mbox{(merge)} \\[2ex]
238    &  |  & \FOCUS{g_1,\dots,g_n} & \mbox{(absolute positioning)} \\
239    &  |  & \UNFOCUS & \mbox{(unfocus)} \\[2ex]
240    &  |  & S ~ S & \mbox{(sequential composition)} \\[2ex]
241    T & : := & & \mbox{(\textbf{tactics})}\\
242      &   & \SKIP & \mbox{(skip)} \\
243      & | & \mathtt{reflexivity} & \\
244      & | & \mathtt{apply}~t & \\
245      & | & \dots &
246 \end{array}
247 \]
248
249 \subsubsection{Status}
250
251 \[
252 \begin{array}{rcll}
253  \xi & & & \mbox{(proof status)} \\
254  \mathit{goal} & & & \mbox{(proof goal)} \\[2ex]
255
256  \SWITCH & = & \OPEN~\mathit{goal} ~ | ~ \CLOSED~\mathit{goal} & \\
257  \mathit{locator} & = & \INT\times\SWITCH & \\
258  \mathit{tag} & = & \BRANCHTAG ~ | ~ \FOCUSTAG \\[2ex]
259
260  \Gamma & = & \mathit{locator}~\LIST & \mbox{(context)} \\
261  \tau & = & \mathit{locator}~\LIST & \mbox{(todo)} \\
262  \kappa & = & \mathit{locator}~\LIST & \mbox{(dot's future)} \\[2ex]
263
264  \mathit{stack} & = & (\Gamma\times\tau\times\kappa\times\mathit{tag})~\LIST
265  \\[2ex]
266
267  \mathit{status} & = & \xi\times\mathit{stack} \\
268 \end{array}
269 \]
270
271 \paragraph{Utilities}
272 \begin{itemize}
273  \item $\ZEROPOS([g_1;\cdots;g_n]) =
274   [\langle 0,\OPEN~g_1\rangle;\cdots;\langle 0,\OPEN~g_n\rangle]$
275  \item $\INITPOS([\langle i_1,s_1\rangle;\cdots;\langle i_n,s_n\rangle]) =
276   [\langle 1,s_1\rangle;\cdots;\langle n,s_n\rangle]$
277  \item $\ISFRESH(s) =
278   \left\{
279   \begin{array}{ll}
280    \mathit{true} & \mathrm{if} ~ s = \langle n, \OPEN~g\rangle\land n > 0 \\
281    \mathit{false} & \mathrm{otherwise} \\
282   \end{array}
283   \right.$
284  \item $\FILTEROPEN(\mathit{locs})=
285   \left\{
286   \begin{array}{ll}
287    [] & \mathrm{if}~\mathit{locs} = [] \\
288    \langle i,\OPEN~g\rangle :: \FILTEROPEN(\mathit{tl})
289    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl} \\
290    \FILTEROPEN(\mathit{tl})
291    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
292   \end{array}
293   \right.$
294  \item $\REMOVEGOALS(G,\mathit{locs}) =
295   \left\{
296   \begin{array}{ll}
297    [] & \mathrm{if}~\mathit{locs} = [] \\
298    \REMOVEGOALS(G,\mathit{tl})
299    & \mathrm{if}~\mathit{locs} = \langle i,\OPEN~g\rangle :: \mathit{tl}
300      \land g\in G\\
301    hd :: \REMOVEGOALS(G,\mathit{tl})
302    & \mathrm{if}~\mathit{locs} = \mathit{hd} :: \mathit{tl} \\
303   \end{array}
304   \right.$
305  \item $\DEEPCLOSE(G,S)$: (intuition) given a set of goals $G$ and a stack $S$
306   it returns a new stack $S'$ identical to the given one with the exceptions
307   that each locator whose goal is in $G$ is marked as closed in $\Gamma$ stack
308   components and removed from $\tau$ and $\kappa$ components.
309  \item $\GOALS(S)$: (inutition) return all goals appearing in whatever position
310   on a given stack $S$, appearing in an \OPEN{} switch.
311 \end{itemize}
312
313 \paragraph{Invariants}
314 \begin{itemize}
315  \item $\forall~\mathrm{entry}~\ENTRY{\Gamma}{\tau}{\kappa}{t}, \forall s
316   \in\tau\cup\kappa, \exists g, s = \OPEN~g$ (each locator on the stack in
317   $\tau$ and $\kappa$ components has an \OPEN~switch).
318  \item Unless \FOCUS{} is used the stack contains no duplicate goals.
319  \item $\forall~\mathrm{locator}~l\in\Gamma \mbox{(with the exception of the
320   top-level $\Gamma$)}, \ISFRESH(l)$.
321 \end{itemize}
322
323 \subsubsection{Semantics}
324
325 \[
326 \begin{array}{rcll}
327  \SEMOP{\cdot} & : & C -> \mathit{status} -> \mathit{status} &
328   \mbox{(continuationals semantics)} \\
329  \TSEMOP{\cdot} & : & T -> \xi -> \SWITCH ->
330   \xi\times\GOAL~\LIST\times\GOAL~\LIST & \mbox{(tactics semantics)} \\
331 \end{array}
332 \]
333
334 \[
335 \begin{array}{rcl}
336  \mathit{apply\_tac} & : & T -> \xi -> \GOAL ->
337   \xi\times\GOAL~\LIST\times\GOAL~\LIST
338 \end{array}
339 \]
340
341 \[
342 \begin{array}{rlcc}
343  \TSEM{T}{\xi}{\OPEN~g} & = & \mathit{apply\_tac}(T,\xi,n) & T\neq\SKIP\\
344  \TSEM{\SKIP}{\xi}{\CLOSED~g} & = & \langle \xi, [], [g]\rangle &
345 \end{array}
346 \]
347
348 \[
349 \begin{array}{rcl}
350
351  \SEM{\TACTIC{T}}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
352  & =
353  & \langle
354    \xi_n,
355    \ENTRY{\Gamma'}{\tau'}{\kappa'}{t}
356 %    \ENTRY{\ZEROPOS(G^o_n)}{\tau\setminus G^c_n}{\kappa\setminus G^o_n}{t}
357    :: \DEEPCLOSE(G^c_n,S)
358    \rangle
359  \\[1ex]
360  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{where} ~ n\geq 1}
361  \\[1ex]
362  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
363   \Gamma' = \ZEROPOS(G^o_n)
364   \land \tau' = \REMOVEGOALS(G^c_n,\tau)
365   \land \kappa' = \REMOVEGOALS(G^o_n,\kappa)
366  }
367  \\[1ex]
368  \multicolumn{3}{l}{\hspace{\sidecondlen}\mathit{and} ~
369  \left\{
370  \begin{array}{rcll}
371   \langle\xi_0, G^o_0, G^c_0\rangle & = & \langle\xi, [], []\rangle \\
372   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
373   & =
374   & \langle\xi_i, G^o_i, G^c_i\rangle
375   & l_{i+1}\in G^c_i \\
376   \langle\xi_{i+1}, G^o_{i+1}, G^c_{i+1}\rangle
377   & =
378   & \langle\xi, (G^o_i\setminus G^c)\cup G^o, G^c_i\cup G^c\rangle
379   & l_{i+1}\not\in G^c_i \\[1ex]
380   & & \mathit{where} ~ \langle\xi,G^o,G^c\rangle=\TSEM{T}{\xi_i}{l_{i+1}} \\
381  \end{array}
382  \right.
383  }
384  \\[6ex]
385
386  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{\kappa}{t}::S}
387  & =
388  & \langle \xi, \ENTRY{l_1}{\tau}{\GIN[2]\cup\kappa}{t}::S \rangle
389  \\[1ex]
390  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=\GIN \land n\geq 1
391  \\[2ex]
392
393  \SEM{~\DOT~}{\ENTRY{\Gamma}{\tau}{l::\kappa}{t}::S}
394  & =
395  & \langle \xi, \ENTRY{[l]}{\tau}{\kappa}{t}::S \rangle
396  \\[1ex]
397  & & \mathrm{where} ~ \FILTEROPEN(\Gamma)=[]
398  \\[2ex]
399
400  \SEM{~\SEMICOLON~}{S} & = & \langle \xi, S \rangle \\[1ex]
401
402  \SEM{~\BRANCH~}{\ENTRY{\GIN}{\tau}{\kappa}{t}::S}
403  \quad 
404  & =
405  & \langle\xi, \ENTRY{[l_1']}{[]}{[]}{\BRANCHTAG}
406    ::\ENTRY{[l_2';\cdots;l_n']}{\tau}{\kappa}{t}::S
407  \\[1ex]
408  & & \mathrm{where} ~ n\geq 2 ~ \land ~ \INITPOS(\GIN)=[l_1';\cdots;l_n']
409  \\[2ex]
410
411  \SEM{~\SHIFT~}
412   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\GIN}{\tau'}{\kappa'}{t'}
413   ::S}
414  & =
415  & \langle
416    \xi, \ENTRY{[l_1]}{\tau\cup\FILTEROPEN(\Gamma)}{[]}{\BRANCHTAG}
417         ::\ENTRY{\GIN[2]}{\tau'}{\kappa'}{t'}::S
418    \rangle
419  \\[1ex]
420  & & \mathrm{where} ~ n\geq 1
421  \\[2ex]
422
423  \SEM{~\POS{i}~}
424   {\ENTRY{[l]}{[]}{[]}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
425  & =
426  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
427    ::\ENTRY{l :: (\Gamma'\setminus [l_i])}{\tau'}{\kappa'}{t'}::S \rangle
428  \\[1ex]
429  & & \mathrm{where} ~ \langle i,l'\rangle = l_i\in \Gamma'~\land~\ISFRESH(l)
430  \\[2ex]
431
432  \SEM{~\POS{i}~}
433   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}
434   ::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}::S}
435  & =
436  & \langle \xi, \ENTRY{[l_i]}{[]}{[]}{\BRANCHTAG}
437  ::\ENTRY{\Gamma'\setminus [l_i]}{\tau'\cup\FILTEROPEN(\Gamma)}{\kappa'}{t'}::S
438    \rangle
439  \\[1ex]
440  & & \mathrm{where} ~ \langle i, l'\rangle = l_i\in \Gamma'
441  \\[2ex]
442
443  \SEM{~\MERGE~}
444   {\ENTRY{\Gamma}{\tau}{\kappa}{\BRANCHTAG}::\ENTRY{\Gamma'}{\tau'}{\kappa'}{t'}
445   ::S}
446  & =
447  & \langle \xi,
448    \ENTRY{\tau\cup\FILTEROPEN(\Gamma)\cup\Gamma'\cup\kappa}{\tau'}{\kappa'}{t'}
449    :: S
450    \rangle
451  \\[2ex]
452
453  \SEM{\FOCUS{g_1,\dots,g_n}}{S}
454  & = 
455  & \langle \xi, \ENTRY{\ZEROPOS([g_1;\cdots;g_n])}{[]}{[]}{\FOCUSTAG}
456    ::\DEEPCLOSE(S)
457    \rangle
458  \\[1ex]
459  & & \mathrm{where} ~
460  \forall i=1,\dots,n,~g_i\in\GOALS(S)
461  \\[2ex]
462
463  \SEM{\UNFOCUS}{\ENTRY{[]}{[]}{[]}{\FOCUSTAG}::S}
464  & = 
465  & \langle \xi, S\rangle \\[2ex]
466
467 \end{array}
468 \]
469
470 \subsection{Related works}
471
472 In~\cite{fk:strata2003}, Kirchner described a small step semantics for Coq
473 tacticals and PVS strategies.
474