]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/matita/matita2.tex
e2af8870cba8fd4ecfd17cbb8da013a7e19d0177
[helm.git] / helm / papers / matita / matita2.tex
1 \documentclass{kluwer}
2 \usepackage{color}
3 \usepackage{graphicx}
4 % \usepackage{amssymb,amsmath}
5 \usepackage{hyperref}
6 % \usepackage{picins}
7 \usepackage{color}
8 \usepackage{fancyvrb}
9 \usepackage[show]{ed}
10
11 \definecolor{gray}{gray}{0.85}
12 %\newcommand{\logo}[3]{
13 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
14 %}
15
16 \newcommand{\AUTO}{\textsc{Auto}}
17 \newcommand{\COQ}{Coq}
18 \newcommand{\ELIM}{\textsc{Elim}}
19 \newcommand{\GDOME}{Gdome}
20 \newcommand{\HELM}{Helm}
21 \newcommand{\HINT}{\textsc{Hint}}
22 \newcommand{\IN}{\ensuremath{\dN}}
23 \newcommand{\INSTANCE}{\textsc{Instance}}
24 \newcommand{\IR}{\ensuremath{\dR}}
25 \newcommand{\IZ}{\ensuremath{\dZ}}
26 \newcommand{\LIBXSLT}{LibXSLT}
27 \newcommand{\LOCATE}{\textsc{Locate}}
28 \newcommand{\MATCH}{\textsc{Match}}
29 \newcommand{\MATITA}{Matita}
30 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
31 \newcommand{\MOWGLI}{MoWGLI}
32 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
33 \newcommand{\NATIND}{\mathit{nat\_ind}}
34 \newcommand{\NUPRL}{NuPRL}
35 \newcommand{\OCAML}{OCaml}
36 \newcommand{\PROP}{\mathit{Prop}}
37 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
38 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
39 \newcommand{\UWOBO}{UWOBO}
40 \newcommand{\GETTER}{Getter}
41 \newcommand{\WHELP}{Whelp}
42 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
43 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
44 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
45 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
46 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
47 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
48 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
49 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
50 \newcommand{\SKIP}{\MATHTT{skip}}
51 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
52
53 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
54 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
55 \newcommand{\URI}[1]{\texttt{#1}}
56
57 %{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
58 \newenvironment{grafite}{\VerbatimEnvironment
59  \begin{SaveVerbatim}{boxtmp}}%
60  {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
61   \begin{center}
62    \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
63   \end{center}}
64
65 \newcounter{example}
66 \newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
67  {}
68 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
69 \newcommand{\FILE}[1]{\texttt{#1}}
70 % \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
71 \newcommand{\NOTE}[1]{\ednote{#1}{foo}}
72 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
73
74 \newsavebox{\tmpxyz}
75 \newcommand{\sequent}[2]{
76   \savebox{\tmpxyz}[0.9\linewidth]{
77     \begin{minipage}{0.9\linewidth}
78       \ensuremath{#1} \\
79       \rule{3cm}{0.03cm}\\
80       \ensuremath{#2}
81     \end{minipage}}\setlength{\fboxsep}{3mm}%
82   \begin{center}
83    \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
84   \end{center}}
85
86 \bibliographystyle{plain}
87
88 \begin{document}
89
90 \begin{opening}
91
92  \title{The \MATITA{} Proof Assistant}
93
94 \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
95 \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
96 \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
97 \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
98 \institute{Department of Computer Science, University of Bologna\\
99  Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
100
101 \runningtitle{The Matita proof assistant}
102 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
103
104 % \date{data}
105
106 \begin{motto}
107 ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
108 \end{motto}
109
110 \begin{abstract}
111  abstract qui
112 \end{abstract}
113
114 \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
115 Digital Libraries}
116
117 \end{opening}
118
119 \section{Introduction}
120 \label{sec:intro}
121 In this paper we describe the architecture and a few distintive features of the
122 \emph{\MATITA} proof assistant. \MATITA{} was not conceived out of the blue
123 one single day; it has been the next natural step in the evolution of one
124 line of research we started six years ago. Thus, to better understand the
125 system, we start from its historical roots.
126
127 \subsection{Historical Perspective}
128 \MATITA{} is under development by the \HELM{} team
129 \cite{mkm-helm} at the University of Bologna, under the direction of 
130 Prof.~Asperti. 
131 The origin of the system goes back to 1999. At the time we were mostly 
132 interested to develop tools and techniques to enhance the accessibility
133 via Web of formal libraries of mathematics. Due to its dimension, the
134 library of the \COQ{} proof assistant (of the order of 35'000 theorems) 
135 was choosed as a privileged test bench for our work, although experiments
136 have been also conducted with other systems, and notably with \NUPRL{}.
137 The work, mostly performed in the framework of the recently concluded 
138 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the 
139 following teps:
140 \begin{itemize}
141 \item exporting the information from the internal representation of
142  \COQ{} to a system and platform independent format. Since XML was at the 
143 time an emerging standard, we naturally adopted this technology, fostering
144 a content-centric architecture for future system, where the documents
145 of the library were the the main components around which everything else 
146 has to be build;
147 \item developing indexing and searching techniques supporting semantic
148  queries to the library; these efforts gave birth to our \WHELP{}
149 search engine, described in~\cite{whelp};
150 \item developing languages and tools for a high-quality notational 
151 rendering of mathematical information; in particular, we have been 
152 active in the MathML Working group since 1999, and developed inside
153 \HELM{} a MathML-compliant widget for the GTK graphical environment
154 which can be integrated in any application.
155 \end{itemize}
156
157 According to our content-centric commitment, the library exported from
158 Coq was conceived as being distributed and most of the tools were developed
159 as Web services. The user could interact with the library and the tools by
160 means of a Web interface that orchestrates the Web services.
161
162 The Web services and the other tools have been implemented as front-ends
163 to a set of libraries, collectively called the \HELM{} libraries.
164 At the end of the \MOWGLI{} project we already disposed of the following
165 techniques and libraries:
166 \begin{itemize}
167 \item XML specifications for the Calculus of Inductive Constructions,
168 with libraries for parsing and saving mathematical objects in such a format;
169 \item metadata specifications with libraries for indexing and querying the
170 XML knowledge base;
171 \item a proof checker library (i.e. the {\em kernel} of a proof assistant), 
172 implemented to check that we exported form the \COQ{} library all the 
173 logically relevant content;
174 \item a sophisticated parser (used by the search engine), able to deal 
175 with potentially ambiguous and incomplete information, typical of the 
176 mathematical notation \cite{disambiguation};
177 \item a {\em refiner} library, i.e. a type inference system, based on
178 partially specified terms, used by the disambiguating parser;
179 \item complex transformation algorithms for proof rendering in natural
180 language;
181 \item an innovative rendering widget, supporting high-quality bidimensional
182 rendering, and semantic selection, i.e. the possibility to select semantically
183 meaningful rendering expressions, and to past the respective content into
184 a different text area.
185 \end{itemize}
186 Starting from all this, the further step of developing our own 
187 proof assistant was too
188 small and too tempting to be neglected. Essentially, we ``just'' had to
189 add an authoring interface, and a set of functionalities for the
190 overall management of the library, integrating everything into a
191 single system. \MATITA{} is the result of this effort. 
192
193 \subsection{The System}
194 DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
195
196 \begin{itemize}
197  \item scelta del sistema fondazionale
198  \item sistema indipendente (da Coq)
199  \item compatibilit\`a con sistemi legacy
200 \end{itemize}
201
202 \subsection{Relationship with \COQ{}}
203
204 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
205 more the effect of the circumstances of its creation described 
206 above than the result of a deliberate design. In particular, we
207 (essentially) share the same foundational dialect of \COQ{} (the
208 Calculus of (Co)Inductive Constructions), the same implementative
209 language (\OCAML{}), and the same (script based) authoring philosophy.
210 However, the analogy essentially stops here and no code is shared by the
211 two systems.
212
213 In a sense; we like to think of \MATITA{} as the way \COQ{} would 
214 look like if entirely rewritten from scratch: just to give an
215 idea, although \MATITA{} currently supports almost all functionalities of
216 \COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
217 by \COQ{} (and we are convinced that, starting from scratch again,
218 we could furtherly reduce our code in sensible way).
219
220 Moreover, the complexity of the code of \MATITA{} is greatly reduced with
221 respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
222 916 functions, to be compared with the 4'286 functions of \COQ.
223
224 Finally, \MATITA{} has several innovatives features over \COQ{} that derive
225 from the integration of Mathematical Knowledge Management tools with proof
226 assistants. Among them, the advanced indexing tools over the library and
227 the parser for ambiguous mathematical notation.
228
229 The size and complexity improvements over \COQ{} must be understood
230 historically. \COQ{} is a quite old
231 system whose development started 15\NOTE{Verificare} years ago. Since then
232 several developers have took over the code and several new research ideas
233 that were not considered in the original architecture have been experimented
234 and integrated in the system. Moreover, there exists a lot of developments
235 for \COQ{} that require backward compatibility between each pair of releases;
236 since many central functionalities of a proof assistant are based on heuristics
237 or arbitrary choices to overcome undecidability (e.g. for higher order
238 unification), changing these functionalities mantaining backward compatibility
239 is very difficult. Finally, the code of \COQ{} has been greatly optimized
240 over the years; optimization reduces maintenability and rises the complexity
241 of the code.
242
243 In writing \MATITA{} we have not been hindered by backward compatibility and
244 we have took advantage of the research results and experiences previously
245 developed by others, comprising the authors of \COQ. Moreover, starting from
246 scratch, we have designed in advance the architecture and we have splitted
247 the code in coherent minimally coupled libraries.
248
249 In the future we plan to exploit \MATITA{} as a test bench for new ideas and
250 extensions. Keeping the single libraries and the whole architecture as
251 simple as possible is thus crucial to speed up future experiments and to
252 allow other developers to quickly understand our code and contribute.
253 %For direct experience of the authors, the learning curve to understand and
254 %be able to contribute to \COQ{}'s code is quite steep and requires direct
255 %and frequent interactions with \COQ{} developers.
256
257 \begin{figure}[t]
258  \begin{center}
259   \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
260   \caption{\label{fig:libraries}\MATITA{} libraries}
261  \end{center}
262 \end{figure}
263
264 \section{Overview of the Architecture}
265 Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
266 and \emph{applications} (squared nodes) developed in the HELM project.
267
268 Applications and libraries depend over other libraries forming a
269 directed acyclic graph (DAG). Each library can be decomposed in
270 a a set of \emph{modules} also forming a DAG.
271
272 Modules and libraries provide coherent sets of functionalities
273 at different scales. Applications that require only a few functionalities
274 depend on a restricted set of libraries.
275
276 Only the proof assistant \MATITA{} and the \WHELP{} search engine are
277 applications meant to be used directly by the user. All the other applications
278 are Web services developed in the HELM and MoWGLI projects and already described
279 elsewhere. In particular:
280 \begin{itemize}
281  \item The \emph{Getter} is a Web service to retrieve an (XML) document
282    from a physical location (URL) given its logical name (URI). The Getter is
283    responsible of updating a table that maps URIs to URLs. Thanks to the Getter
284    it is possible to work on a logically monolithic library that is physically
285    distributed on the network. More information on the Getter can be found
286    in~\cite{zack-master}.
287  \item \emph{Whelp} is a search engine to index and locate mathematical
288    notions (axioms, theorems, definitions) in the logical library managed
289    by the Getter. Typical examples of a query to Whelp are queries that search
290    for a theorem that generalize or instantiate a given formula, or that
291    can be immediately applied to prove a given goal. The output of Whelp is
292    an XML document that lists the URIs of a complete set of candidates that
293    are likely to satisfy the given query. The set is complete in the sense
294    that no notion that actually satisfies the query is thrown away. However,
295    the query is only approssimated in the sense that false matches can be
296    returned. Whelp has been described in~\cite{whelp}.
297  \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
298    notion in the distributed library, renders it according to the user provided
299    two dimensional mathematical notation. Uwobo may also embed the rendering
300    of mathematical notions into arbitrary documents before returning them.
301    The Getter is used by Uwobo to retrieve the document to be rendered.
302    Uwobo has been described in~\cite{zack-master}.
303  \item The \emph{Proof Checker} is a Web service that, given the URI of
304    notion in the distributed library, checks its correctness. Since the notion
305    is likely to depend in an acyclic way over other notions, the proof checker
306    is also responsible of building in a top-down way the DAG of all
307    dependencies, checking in turn every notion for correctness.
308    The proof checker has been described in~\cite{zack-master}.
309  \item The \emph{Dependency Analyzer} is a Web service that can produce
310    a textual or graphical representation of the dependecies of an object.
311    The dependency analyzer has been described in~\cite{zack-master}.
312 \end{itemize}
313
314 The dependency of a library or application over another library can
315 be satisfied by linking the library in the same executable.
316 For those libraries whose functionalities are also provided by the
317 aforementioned Web services, it is also possible to link stub code that
318 forwards the request to a remote Web service. For instance, the Getter
319 is just a wrapper to the \texttt{getter} library that allows the library
320 to be used as a Web service. \MATITA{} can directly link the code of the
321 \texttt{getter} library, or it can use a stub library with the same API
322 that forwards every request to the Getter.
323
324 To better understand the architecture of \MATITA{} and the role of each
325 library, we can focus on the representation of the mathematical information.
326 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
327 Constructions (CIC). In CIC terms are used to represent mathematical
328 expressions, types and proofs. \MATITA{} is able to handle terms at
329 four different levels of specification. On each level it is possible to provide
330 a different set of functionalities. The four different levels are:
331 fully specified terms; partially specified terms; 
332 content level terms; presentation level terms.
333
334 \subsection{Fully specified terms}
335  \emph{Fully specified terms} are CIC terms where no information is
336    missing or left implicit. A fully specified term should be well-typed.
337    The mathematical notions (axioms, definitions, theorems) that are stored
338    in our mathematical library are fully specified and well-typed terms.
339    Fully specified terms are extremely verbose (to make type-checking
340    decidable). Their syntax is fixed and does not resemble the usual
341    extendible mathematical notation. They are not meant for direct user
342    consumption.
343
344    The \texttt{cic} library defines the data type that represents CIC terms
345    and provides a parser for terms stored in an XML format.
346
347    The most important library that deals with fully specified terms is
348    \texttt{cic\_proof\_checking}. It implements the procedure that verifies
349    if a fully specified term is well-typed. It also implements the
350    \emph{conversion} judgement that verifies if two given terms are
351    computationally equivalent (i.e. they share the same normal form).
352
353    Terms may reference other mathematical notions in the library.
354    One commitment of our project is that the library should be physically
355    distributed. The \texttt{getter} library manages the distribution,
356    providing a mapping from logical names (URIs) to the physical location
357    of a notion (an URL). The \texttt{urimanager} library provides the URI
358    data type and several utility functions over URIs. The
359    \texttt{cic\_proof\_checking} library calls the \texttt{getter} library
360    every time it needs to retrieve the definition of a mathematical notion
361    referenced by a term that is being type-checked. 
362
363    The Proof Checker is the Web service that provides an interface
364    to the \texttt{cic\_proof\_checking} library.
365
366    We use metadata and a sort of crawler to index the mathematical notions
367    in the distributed library. We are interested in retrieving a notion
368    by matching, instantiation or generalization of a user or system provided
369    mathematical expression. Thus we need to collect metadata over the fully
370    specified terms and to store the metadata in some kind of (relational)
371    database for later usage. The \texttt{hmysql} library provides a simplified
372    interface to a (possibly remote) MySql database system used to store the
373    metadata. The \texttt{metadata} library defines the data type of the metadata
374    we are collecting and the functions that extracts the metadata from the
375    mathematical notions (the main functionality of the crawler).
376    The \texttt{whelp} library implements a search engine that performs
377    approximated queries by matching/instantiation/generalization. The queries
378    operate only on the metadata and do not involve any actual matching
379    (that will be described later on and that is implemented in the
380     \texttt{cic\_unification} library). Not performing any actual matching
381    the query only returns a complete and hopefully small set of matching
382    candidates. The process that has issued the query is responsible of
383    actually retrieving from the distributed library the candidates to prune
384    out false matches if interested in doing so.
385
386    The Whelp search engine is the Web service that provides an interface to
387    the \texttt{whelp} library.
388
389 \subsection{Partially specified terms}
390 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
391 Omitted subterms can bear no information at all or they may be associated to
392 a sequent. The formers are called \emph{implicit terms} and they occur only
393 linearly. The latters may occur multiple times and are called
394 \emph{metavariables}. An \emph{explicit substitution} is applied to each
395 occurrence of a metavariable. A metavariable stand for a term whose type is
396 given by the conclusion of the sequent. The term must be closed in the
397 context that is given by the ordered list of hypotheses of the sequent.
398 The explicit substitution instantiates every hypothesis with an actual
399 value for the term bound by the hypothesis.
400
401 Partially specified terms are not required to be well-typed. However a
402 partially specified term should be \emph{refinable}. A \emph{refiner} is
403 a type-inference procedure that can instantiate implicit terms and
404 metavariables and that can introduce \emph{implicit coercions} to make a
405 partially specified term be well-typed. The refiner of \MATITA{} is implemented
406 in the \texttt{cic\_unification} library. As the type checker is based on
407 the conversion check, the refiner is based on \emph{unification} that is
408 a procedure that makes two partially specified term convertible by instantiating
409 as few as possible metavariables that occur in them.
410
411 Since terms are used in CIC to represent proofs, correct incomplete
412 proofs are represented by refinable partially specified terms. The metavariables
413 that occur in the proof correspond to the conjectures still to be proved.
414 The sequent associated to the metavariable is the conjecture the user needs to
415 prove.
416
417 \emph{Tactics} are the procedures that the user can apply to progress in the
418 proof. A tactic proves a conjecture possibly creating new (and hopefully
419 simpler) conjectures. The implementation of tactics is given in the
420 \texttt{tactics} library. It is heavily based on the refinement and unification
421 procedures of the \texttt{cic\_unification} library. \TODO{citare paramodulation
422 da qualche part o toglierla dal grafo}
423
424 As fully specified terms, partially specified terms are not well suited
425 for user consumption since their syntax is not extendible and it is not
426 possible to adopt the usual mathematical notation. However they are already
427 an improvement over fully specified terms since they allow to omit redundant
428 information that can be inferred by the refiner.
429
430 \subsection{Content level terms}
431 The language used to communicate proofs and expecially expressions with the
432 user does not only needs to be extendible and accomodate the usual mathematical
433 notation. It must also reflect the comfortable degree of imprecision and
434 ambiguity that the mathematical language provides.
435
436 For instance, it is common practice in mathematics to speak of a generic
437 equality that can be used to compare any two terms. However, it is well known
438 that several equalities can be distinguished as soon as we care for decidability
439 or for their computational properties. For instance equality over real
440 numbers is well known to be undecidable, whereas it is decidable over
441 rational numbers.
442
443 Similarly, we usually speak of natural numbers and their operations and
444 properties without caring about their representation. However the computational
445 properties of addition over the binary representation are very different from
446 those of addition over the unary representation. And addition over two natural
447 numbers is definitely different from addition over two real numbers.
448
449 Formal mathematics cannot hide these differences and obliges the user to be
450 very precise on the types he is using and their representation. However,
451 to communicate formulae with the user and with external tools, it seems good
452 practice to stick to the usual imprecise mathematical ontology. In the
453 Mathematical Knowledge Management community this imprecise language is called
454 the \emph{content level} representation of expressions.
455
456 In \MATITA{} we provide two translations: from partially specified terms
457 to content level terms and the other way around. The first translation can also
458 be applied to fully specified terms since a fully specified term is a special
459 case of partially specified term where no metavariable or implicit term occurs.
460
461 The translation from partially specified terms to content level terms must
462 discriminate between terms used to represent proofs and terms used to represent
463 expressions. The firsts are translated to a content level representation of
464 proof steps that can easily be rendered in natural language. The latters
465 are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C
466 standard
467 for the representation of content level expressions in an XML extensible format.
468
469 The translation to content level is implemented in the
470 \texttt{acic\_content} library. Its input are \emph{annotated partially
471 specified terms}, that are maximally unshared
472 partially specified terms enriched with additional typing information for each
473 subterm. This information is used to discriminate between terms that represent
474 proofs and terms that represent expressions. Part of it is also stored at the
475 content level since it is required to generate the natural language rendering
476 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
477 and not a DAG). The reason is that to the occurrences of a subterm in
478 two different positions we need to associate different typing informations.
479 This association is made easier when the term is represented as a tree since
480 it is possible to label each node with an unique identifier and associate
481 the typing information using a map on the identifiers.
482 The \texttt{cic\_acic} library annotates partially specified terms.
483
484 We do not provide yet a reverse translation from content level proofs to
485 partially specified terms. But in \texttt{disambiguation} we do provide
486 the reverse translation for expressions. The mapping from
487 content level expressions to partially specified terms is not unique due to
488 the ambiguity of the content level. As a consequence the translation
489 is guided by an \emph{interpretation}, that is a function that chooses for
490 every ambiguous expression one partially specified term. The
491 \texttt{disambiguation} library contains the implementation of the
492 disambiguation algorithm we presented in \cite{disambiguation} that is
493 responsible of building in an efficicent way the set of all ``correct''
494 interpretations. An interpretation is correct if the partially specified term
495 obtained using the interpretation is refinable.
496
497 \subsection{Presentation level terms}
498
499 Content level terms are a sort of abstract syntax trees for mathematical
500 expressions and proofs. The concrete syntax given to these abstract trees
501 is called \emph{presentation level}.
502
503 The main important difference between the content level language and the
504 presentation level language is that only the former is extendible. Indeed,
505 the presentation level language is a finite language that comprises all
506 the usual mathematical symbols. Mathematicians invent new notions every
507 single day, but they stick to a set of symbols that is more or less fixed.
508
509 The fact that the presentation language is finite allows the definition of
510 standard languages. In particular, for formulae we have adopt MathML
511 Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
512 visually
513 represent proofs it is enough to embed formulae in plain text enriched with
514 formatting boxes. Since the language of formatting boxes is very simple,
515 many equivalent specifications exist and we have adopted our own, called
516 BoxML.
517
518 The \texttt{content\_pres} library contains the implementation of the
519 translation from content level terms to presentation level terms. The
520 rendering of presentation level terms is left to the application that uses
521 the library. However, in the \texttt{hgdome} library we provide a few
522 utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
523 presentation
524 level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
525 widget developed by Luca Padovani \cite{padovani}. The widget is
526 particularly interesting since it allows to implement \emph{semantic
527 selection}.
528
529 Semantic selection is a technique that consists in enriching the presentation
530 level terms with pointers to the content level terms and to the partially
531 specified terms they correspond to. Highlight of formulae in the widget is
532 constrained to selection of meaningful expressions, i.e. expressions that
533 correspond to a lower\footnote{\TODO{non abbiamo parlato di ``ordine''}} level term. Once the rendering of a lower level term is
534 selected it is possible for the application to retrieve the pointer to the
535 lower level term. An example of applications of semantic selection is
536 \emph{semantic cut\&paste}: the user can select an expression and paste it
537 elsewhere preserving its semantics (i.e. the partially specified term),
538 possibly performing some semantic transformation over it (e.g. renaming
539 variables that would be captured or lambda-lifting free variables).
540
541 The reverse translation from presentation level terms to content level terms
542 is implemented by a parser that is also found in \texttt{content\_pres}.
543 Differently from the translation from content level terms to partially
544 refined terms, this translation is not ambiguous. The reason is that the
545 parsing library we have adopted (CamlP4) is not able to parse ambiguous
546 grammars. Thus we require the mapping from presentation level terms
547 (concrete syntax) to content level terms (abstract syntax) to be unique.
548 This means that the user must fix once and for all the associativity and
549 precedence level of every operator he is using. In prctice this limitation
550 does not seem too strong. The reason is that the target of the
551 translation is an ambiguous language and the user is free to associate
552 to every content level term several different interpretations (as a
553 partially specified term).
554
555 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
556 against the \texttt{cic\_disambiguation} and \texttt{content\_pres} libraries
557 since they provide an interface to the user. In both cases the formulae
558 written by the user are parsed using the \texttt{content\_pres} library and
559 then disambiguated using the \texttt{cic\_disambiguation} library.
560
561 The \UWOBO{} Web service wraps the \texttt{content\_pres} library,
562 providing a rendering service for the documents in the distributed library.
563 To render a document given its URI, \UWOBO{} retrieves it using the
564 \GETTER{} obtaining a document with fully specified terms. Then it translates
565 it to the presentation level passing through the content level. Finally
566 it returns the result document to be rendered by the user's
567 browser.\footnote{\TODO{manca la passata verso HTML}}
568
569 \hrule
570
571 At the bottom of the DAG we have a few libraries (\texttt{extlib},
572 \texttt{xml} and the \texttt{registry}) that provide a core of
573 useful functions used everywhere else. In particular, the \texttt{xml} library
574 to easily represent, parse and pretty-print XML files is a central component
575 since in HELM every piece of information is stored in \ldots. [FINIRE]
576 The other basic libraries provide often needed operations over generic
577 data structures (\texttt{extlib}) and central storage for configuration options
578 (the \texttt{registry}).
579
580 \texttt{urimanager}
581
582 \texttt{getter}
583
584 \texttt{cic}
585
586 \section{Partially specified terms}
587 --- il mondo delle tattiche e dintorni ---
588 serve una intro che almeno cita il widget (per i patterns) e che fa
589 il resoconto delle cose che abbiamo e che non descriviamo,
590 sottolineando che abbiamo qualcosa da dire sui pattern e sui
591 tattichini.\\
592
593
594
595 \subsection{Patterns}
596 Patterns are the textual counterpart of the MathML widget graphical
597 selection.
598
599 Matita benefits of a graphical interface and a powerful MathML rendering
600 widget that allows the user to select pieces of the sequent he is working
601 on. While this is an extremely intuitive way for the user to
602 restrict the application of tactics, for example, to some subterms of the
603 conclusion or some hypothesis, the way this action is recorded to the text
604 script is not obvious.\\
605 In \MATITA{} this issue is addressed by patterns.
606
607 \subsubsection{Pattern syntax}
608 A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
609 $\NT{wanted}$.
610 The former mocks-up a sequent, discharging unwanted subterms with $?$ and
611 selecting the interesting parts with the placeholder $\%$. 
612 The latter is a term that lives in the context of the placeholders.
613
614 The concrete syntax is reported in table \ref{tab:pathsyn}
615 \NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
616 \begin{table}
617  \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
618 \hrule
619 \[
620 \begin{array}{@{}rcll@{}}
621   \NT{pattern} & 
622     ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
623   \NT{sequent\_path} & 
624     ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
625       [~\verb+\vdash+~\NT{multipath}~] & \\
626   \NT{wanted} & ::= & \NT{term} & \\
627   \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
628 \end{array}
629 \]
630 \hrule
631 \end{table}
632
633 \subsubsection{How patterns work}
634 Patterns mimic the user's selection in two steps. The first one
635 selects roots (subterms) of the sequent, using the
636 $\NT{sequent\_path}$,  while the second 
637 one searches the $\NT{wanted}$ term starting from these roots. Both are
638 optional steps, and by convention the empty pattern selects the whole
639 conclusion.
640
641 \begin{description}
642 \item[Phase 1]
643   concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
644   part of the syntax. $\NT{ident}$ is an hypothesis name and
645   selects the assumption where the following optional $\NT{multipath}$
646   will operate. \verb+\vdash+ can be considered the name for the goal.
647   If the whole pattern is omitted, the whole goal will be selected.
648   If one or more hypotheses names are given the selection is restricted to 
649   these assumptions. If a $\NT{multipath}$ is omitted the whole
650   assumption is selected. Remember that the user can be mostly
651   unaware of this syntax, since the system is able to write down a 
652   $\NT{sequent\_path}$ starting from a visual selection.
653   \NOTE{Questo ancora non va in matita}
654
655   A $\NT{multipath}$ is a CiC term in which a special constant $\%$
656   is allowed.
657   The roots of discharged subterms are marked with $?$, while $\%$
658   is used to select roots. The default $\NT{multipath}$, the one that
659   selects the whole term, is simply $\%$.
660   Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
661   that respectively select the first argument of an application or
662   the source of an arrow and the head of the application that is
663   found in the arrow target.
664
665   The first phase selects not only terms (roots of subterms) but also 
666   their context that will be eventually used in the second phase.
667
668 \item[Phase 2] 
669   plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
670   part is specified. From the first phase we have some terms, that we
671   will see as subterm roots, and their context. For each of these
672   contexts the $\NT{wanted}$ term is disambiguated in it and the
673   corresponding root is searched for a subterm $\alpha$-equivalent to
674   $\NT{wanted}$. The result of this search is the selection the
675   pattern represents.
676
677 \end{description}
678
679 \noindent
680 Since the first step is equipotent to the composition of the two
681 steps, the system uses it to represent each visual selection.
682 The second step is only meant for the
683 experienced user that writes patterns by hand, since it really
684 helps in writing concise patterns as we will see in the
685 following examples.
686
687 \subsubsection{Examples}
688 To explain how the first step works let's give an example. Consider
689 you want to prove the uniqueness of the identity element $0$ for natural
690 sum, and that you can relay on the previously demonstrated left
691 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
692 Typing
693 \begin{grafite}
694 theorem valid_name: \forall n,m. m + n = n \to m = O.
695   intros (n m H).
696 \end{grafite}
697 \noindent
698 leads you to the following sequent 
699 \sequent{
700 n:nat\\
701 m:nat\\
702 H: m + n = n}{
703 m=O
704 }
705 \noindent
706 where you want to change the right part of the equivalence of the $H$
707 hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
708 \begin{grafite}
709   change in H:(? ? ? %) with (O + n).
710 \end{grafite}
711 \noindent
712 This pattern, that is a simple instance of the $\NT{sequent\_path}$
713 grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
714 and discharges the head of the application and the first two arguments with a
715 $?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
716 but the user can simply select with the mouse the right part of the equivalence
717 and left to the system the burden of writing down in the script file the
718 corresponding pattern with $?$ and $\%$ in the right place (that is not
719 trivial, expecially where implicit arguments are hidden by the notation, like
720 the type $nat$ in this example).
721
722 Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ 
723 works too and can be done, by the experienced user, writing directly
724 a simpler pattern that uses the second phase.
725 \begin{grafite}
726   change in match n in H with (O + n).
727 \end{grafite}
728 \noindent
729 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
730 the second phase searches the wanted $n$ inside it by
731 $\alpha$-equivalence. The resulting
732 equivalence will be $m+(O+n)=O+n$ since the second phase found two
733 occurrences of $n$ in $H$ and the tactic changed both.
734
735 Just for completeness the second pattern is equivalent to the
736 following one, that is less readable but uses only the first phase.
737 \begin{grafite}
738   change in H:(? ? (? ? %) %) with (O + n).
739 \end{grafite}
740 \noindent
741
742 \subsubsection{Tactics supporting patterns}
743 In \MATITA{} all the tactics that can be restricted to subterm of the working
744 sequent accept the pattern syntax. In particular these tactics are: simplify,
745 change, fold, unfold, generalize, replace and rewrite.
746
747 \NOTE{attualmente rewrite e fold non supportano phase 2. per
748 supportarlo bisogna far loro trasformare il pattern phase1+phase2 
749 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
750 con una pattern\_of(select(pattern))}
751
752 \subsubsection{Comparison with Coq}
753 Coq has a two diffrent ways of restricting the application of tactis to
754 subterms of the sequent, both relaying on the same special syntax to identify
755 a term occurrence.
756
757 The first way is to use this special syntax to specify directly to the
758 tactic the occurrnces of a wanted term that should be affected, while
759 the second is to prepare the sequent with another tactic called
760 pattern and the apply the real tactic. Note that the choice is not
761 left to the user, since some tactics needs the sequent to be prepared
762 with pattern and do not accept directly this special syntax.
763
764 The base idea is that to identify a subterm of the sequent we can
765 write it and say that we want, for example, the third and the fifth
766 occurce of it (counting from left to right). In our previous example,
767 to change only the left part of the equivalence, the correct command
768 is
769 \begin{grafite}
770   change n at 2 in H with (O + n)
771 \end{grafite} 
772 \noindent
773 meaning that in the hypothesis $H$ the $n$ we want to change is the
774 second we encounter proceeding from left toright.
775
776 The tactic pattern computes a
777 $\beta$-expansion of a part of the sequent with respect to some
778 occurrences of the given term. In the previous example the following
779 command
780 \begin{grafite}
781   pattern n at 2 in H
782 \end{grafite}
783 \noindent
784 would have resulted in this sequent
785 \begin{grafite}
786   n : nat
787   m : nat
788   H : (fun n0 : nat => m + n = n0) n
789   ============================
790    m = 0
791 \end{grafite}
792 \noindent
793 where $H$ is $\beta$-expanded over the second $n$
794 occurrence. This is a trick to make the unification algorithm ignore
795 the head of the application (since the unification is essentially
796 first-order) but normally operate on the arguments. 
797 This works for some tactics, like rewrite and replace,
798 but for example not for change and other tactics that do not relay on
799 unification. 
800
801 The idea behind this way of identifying subterms in not really far
802 from the idea behind patterns, but really fails in extending to
803 complex notation, since it relays on a mono-dimensional sequent representation.
804 Real math notation places arguments upside-down (like in indexed sums or
805 integrations) or even puts them inside a bidimensional matrix.  
806 In these cases using the mouse to select the wanted term is probably the 
807 only way to tell the system exactly what you want to do. 
808
809 One of the goals of \MATITA{} is to use modern publishing techiques, and
810 adopting a method for restricting tactics application domain that discourages 
811 using heavy math notation, would definitively be a bad choice.
812
813 \subsection{Tacticals}
814 There are mainly two kinds of languages used by proof assistants to recorder
815 proofs: tactic based and declarative. We will not investigate the philosophy
816 aroud the choice that many proof assistant made, \MATITA{} included, and we
817 will not compare the two diffrent approaches. We will describe the common
818 issues of the tactic-based language approach and how \MATITA{} tries to solve
819 them.
820
821 \subsubsection{Tacticals overview}
822
823 Tacticals first appeared in LCF and can be seen as programming
824 constructs, like looping, branching, error recovery or sequential composition.
825 The following simple example shows three tacticals in action
826 \begin{grafite}
827 theorem trivial: 
828   \forall A,B:Prop. 
829     A = B \to ((A \to B) \land (B \to A)).
830   intros (A B H).
831   split; intro; 
832     [ rewrite < H. assumption.
833     | rewrite > H. assumption.
834     ]
835 qed.
836 \end{grafite}
837
838 The first is ``\texttt{;}'' that combines the tactic \texttt{split}
839 with \texttt{intro}, applying the latter to each goal opened by the
840 former. Then we have ``\texttt{[}'' that branches on the goals (here
841 we have two goals, the two sides of the logic and).
842 The first goal $B$ (with $A$ in the context)
843 is proved by the first sequence of tactics
844 \texttt{rewrite} and \texttt{assumption}. Then we move to the second
845 goal with the separator ``\texttt{|}''. The last tactical we see here
846 is ``\texttt{.}'' that is a sequential composition that selects the
847 first goal opened for the following tactic (instead of applying it to
848 them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
849 not considered a tactical, but a sentence terminator (i.e. the
850 delimiter of commands the proof assistant executes).
851
852 Giving serious examples here is rather difficult, since they are hard
853 to read without the interactive tool. To help the reader in
854 understanding the following considerations we just give few common
855 usage examples without a proof context.
856
857 \begin{grafite}
858   elim z; try assumption; [ ... | ... ].
859   elim z; first [ assumption | reflexivity | id ].
860 \end{grafite}
861
862 The first example goes by induction on a term \texttt{z} and applies
863 the tactic \texttt{assumption} to each opened goal eventually recovering if
864 \texttt{assumption} fails. Here we are asking the system to close all
865 trivial cases and then we branch on the remaining with ``\texttt{[}''.
866 The second example goes again by induction on \texttt{z} and tries to
867 close each opened goal first with \texttt{assumption}, if it fails it
868 tries \texttt{reflexivity} and finally \texttt{id}
869 that is the tactic that leaves the goal untouched without failing. 
870
871 Note that in the common implementation of tacticals both lines are
872 compositions of tacticals and in particular they are a single
873 statement (i.e. derived from the same non terminal entry of the
874 grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
875 this is not true, since each atomic tactic or punctuation is considered 
876 a single statement.
877
878 \subsubsection{Common issues of tactic(als)-based proof languages}
879 We will examine the two main problems of tactic(als)-based proof script:
880 maintainability and readability. 
881
882 Huge libraries of formal mathematics have been developed, and backward
883 compatibility is a really time consuming task. \\
884 A real-life example in the history of \MATITA{} was the reordering of
885 goals opened by a tactic application. We noticed that some tactics
886 were not opening goals in the expected order. In particular the
887 \texttt{elim} tactic on a term of an inductive type with constructors
888 $c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
889 \ldots, g_2$. The library of \MATITA{} was still in an embryonic state
890 but some theorems about integers were there. The inductive type of
891 $\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
892 induction proofs on this type where written without tacticals and,
893 obviously, considering the three induction cases in the wrong order.
894 Fixing the behavior of the tactic broke the library and two days of
895 work were needed to make it compile again. The whole time was spent in
896 finding the list of tactics used to prove the third induction case and
897 swap it with the list of tactics used to prove the second case.  If
898 the proofs was structured with the branch tactical this task could
899 have been done automatically. 
900
901 From this experience we learned that the use of tacticals for
902 structuring proofs gives some help but may have some drawbacks in
903 proof script readability. We must highlight that proof scripts
904 readability is poor by itself, but in conjunction with tacticals it
905 can be nearly impossible. The main cause is the fact that in proof
906 scripts there is no trace of what you are working on. It is not rare
907 for two different theorems to have the same proof script (while the
908 proof is completely different).\\
909 Bad readability is not a big deal for the user while he is
910 constructing the proof, but is considerably a problem when he tries to
911 reread what he did or when he shows his work to someone else.  The
912 workaround commonly used to read a script is to execute it again
913 step-by-step, so that you can see the proof goal changing and you can
914 follow the proof steps. This works fine until you reach a tactical.  A
915 compound statement, made by some basic tactics glued with tacticals,
916 is executed in a single step, while it obviously performs lot of proof
917 steps.  In the fist example of the previous section the whole branch
918 over the two goals (respectively the left and right part of the logic
919 and) result in a single step of execution. The workaround doesn't work
920 anymore unless you de-structure on the fly the proof, putting some
921 ``\texttt{.}'' where you want the system to stop.\\
922
923 Now we can understand the tradeoff between script readability and
924 proof structuring with tacticals. Using tacticals helps in maintaining
925 scripts, but makes it really hard to read them again, cause of the way
926 they are executed.
927
928 \MATITA{} uses a language of tactics and tacticals, but tries to avoid
929 this tradeoff, alluring the user to write structured proof without
930 making it impossible to read them again.
931
932 \subsubsection{The \MATITA{} approach: Tinycals}
933
934 \begin{table}
935  \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
936 \hrule
937 \[
938 \begin{array}{@{}rcll@{}}
939   \NT{punctuation} & 
940     ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
941   \NT{block\_kind} & 
942     ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
943   \NT{block\_delimiter} & 
944     ::= & \verb+begin+ ~|~ \verb+end+ & \\
945   \NT{tactical} & 
946     ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
947 \end{array}
948 \]
949 \hrule
950 \end{table}
951
952 \MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
953 While one would expect to find structured constructs like 
954 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
955 This is essential for base idea behind matita tacticals: step-by-step execution.
956
957 The low-level tacticals implementation of \MATITA{} allows a step-by-step
958 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
959 not executed as an atomic operation. This has two major benefits for the user,
960 even being a so simple idea:
961 \begin{description}
962 \item[Proof structuring] 
963   is much easier. Consider for example a proof by induction, and imagine you
964   are using classical tacticals in one of the state of the
965   art graphical interfaces for proof assistant like Proof General or Coq Ide.
966   After applying the induction principle you have to choose: structure
967   the proof or not. If you decide for the former you have to branch with
968   ``\texttt{[}'' and write tactics for all the cases separated by 
969   ``\texttt{|}'' and then close the tactical with ``\texttt{]}''. 
970   You can replace most of the cases by the identity tactic just to
971   concentrate only on the first goal, but you will have to go one step back and
972   one further every time you add something inside the tactical. Again this is
973   caused by the one step execution of tacticals and by the fact that to modify
974   the already executed script you have to undo one step.
975   And if you are board of doing so, you will finish in giving up structuring
976   the proof and write a plain list of tactics.\\
977   With step-by-step tacticals you can apply the induction principle, and just
978   open the branching tactical ``\texttt{[}''. Then you can interact with the
979   system reaching a proof of the first case, without having to specify any
980   tactic for the other goals. When you have proved all the induction cases, you
981   close the branching tactical with ``\texttt{]}'' and you are done with a 
982   structured proof. \\
983   While \MATITA{} tacticals help in structuring proofs they allow you to 
984   choose the amount of structure you want. There are no constraints imposed by
985   the system, and if the user wants he can even write completely plain proofs.
986   
987 \item[Rereading]
988   is possible. Going on step by step shows exactly what is going on.  Consider
989   again a proof by induction, that starts applying the induction principle and
990   suddenly branches with a ``\texttt{[}''. This clearly separates all the
991   induction cases, but if the square brackets content is executed in one single
992   step you completely loose the possibility of rereading it and you have to
993   temporary remove the branching tactical to execute in a satisfying way the
994   branches.  Again, executing step-by-step is the way you would like to review
995   the demonstration. Remember that understanding the proof from the script is
996   not easy, and only the execution of tactics (and the resulting transformed
997   goal) gives you the feeling of what is going on.
998 \end{description}
999
1000
1001 \acknowledgements
1002 We would like to thank all the students that during the past
1003 five years collaborated in the \HELM{} project and contributed to 
1004 the development of Matita, and in particular
1005 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi, 
1006 V.Tamburrelli.
1007
1008 \theendnotes
1009
1010 \bibliography{matita}
1011
1012
1013 \end{document}
1014