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