]> matita.cs.unibo.it Git - helm.git/blob - helm/papers/matita/matita2.tex
/me reviewed up to section 2 (included)
[helm.git] / helm / papers / matita / matita2.tex
1 \documentclass[]{kluwer}
2 \usepackage{color}
3 \usepackage{graphicx}
4 \usepackage{hyperref}
5 \usepackage{color}
6 \usepackage{fancyvrb}
7 \usepackage[show]{ed}
8
9 \newcommand{\component}{component}
10 \newcommand{\components}{components}
11
12 \newcommand{\AUTO}{\textsc{Auto}}
13 \newcommand{\BOXML}{BoxML}
14 \newcommand{\COQ}{Coq}
15 \newcommand{\COQIDE}{CoqIde}
16 \newcommand{\ELIM}{\textsc{Elim}}
17 \newcommand{\GDOME}{Gdome}
18 \newcommand{\GTK}{GTK+}
19 \newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
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{\LEGO}{Lego}
28 \newcommand{\LOCATE}{\textsc{Locate}}
29 \newcommand{\MATCH}{\textsc{Match}}
30 \newcommand{\MATHML}{MathML}
31 \newcommand{\MATITA}{Matita}
32 \newcommand{\MATITAC}{\texttt{matitac}}
33 \newcommand{\MATITADEP}{\texttt{matitadep}}
34 \newcommand{\MOWGLI}{MoWGLI}
35 \newcommand{\MOWGLIIST}{IST-2001-33562}
36 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
37 \newcommand{\NATIND}{\mathit{nat\_ind}}
38 \newcommand{\NUPRL}{NuPRL}
39 \newcommand{\OCAML}{OCaml}
40 \newcommand{\PROP}{\mathit{Prop}}
41 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
42 \newcommand{\REWRITEHINT}{\textsc{RewriteHint}}
43 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
44 \newcommand{\UWOBO}{UWOBO}
45 \newcommand{\GETTER}{Getter}
46 \newcommand{\WHELP}{Whelp}
47
48 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
49 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
50 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
51 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
52 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
53 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
54 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
55 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
56 \newcommand{\SKIP}{\MATHTT{skip}}
57 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
58
59 \newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
60 \newcommand{\URI}[1]{\texttt{#1}}
61 \newcommand{\OP}[1]{``\texttt{#1}''}
62 \newcommand{\FILE}[1]{\texttt{#1}}
63 \newcommand{\NOTE}[1]{\ednote{#1}{}}
64 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
65
66 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
67
68 \newenvironment{grafite}{\VerbatimEnvironment
69  \begin{SaveVerbatim}{boxtmp}}%
70  {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
71   \begin{center}
72    \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
73   \end{center}}
74
75 \newcounter{pass}
76 \newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
77
78 \newsavebox{\tmpxyz}
79 \newcommand{\sequent}[2]{
80   \savebox{\tmpxyz}[0.9\linewidth]{
81     \begin{minipage}{0.9\linewidth}
82       \ensuremath{#1} \\
83       \rule{3cm}{0.03cm}\\
84       \ensuremath{#2}
85     \end{minipage}}\setlength{\fboxsep}{3mm}%
86   \begin{center}
87    \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
88   \end{center}}
89
90 \bibliographystyle{klunum}
91
92 \begin{document}
93
94 \begin{opening}
95  \title{The \MATITA{} Proof Assistant}
96
97  \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
98  \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
99  \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
100  \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
101
102  \institute{Department of Computer Science, University of Bologna\\
103  Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
104
105  \runningtitle{The \MATITA{} proof assistant}
106  \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
107
108  \begin{motto}
109   ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
110  \end{motto}
111
112  \begin{abstract}
113   \TODO{scrivere abstract}
114  \end{abstract}
115
116  \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
117  Digital Libraries}
118 \end{opening}
119
120 % toc & co: to be removed in the final paper version
121 \tableofcontents
122 \listoffigures
123 \listoftables
124
125 \section{Introduction}
126 \label{sec:intro}
127
128 \MATITA{} is the Proof Assistant under development by the \HELM{}
129 team~\cite{mkm-helm} at the University of Bologna, under the direction of
130 Prof.~Asperti. This paper describes the overall architecture of
131 the system, focusing on its most distinctive and innovative 
132 features.
133
134 \subsection{Historical perspective}
135
136 The origins of \MATITA{} go back to 1999. At the time we were mostly 
137 interested to develop tools and techniques to enhance the accessibility
138 via Web of libraries of formal mathematics. Due to its dimension, the
139 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems) 
140 was chosen as a privileged test bench for our work, although experiments
141 have been also conducted with other systems, and notably 
142 with \NUPRL~\cite{nuprl-book}.\TODO{citare la tesi di vincenzo(?)}
143 The work, mostly performed in the framework of the recently concluded 
144 European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the 
145 following steps:
146 \begin{enumerate}
147
148  \item exporting the information from the internal representation of
149   \COQ{} to a system and platform independent format. Since XML was at
150   the time an emerging standard, we naturally adopted that technology,
151   fostering a content-centric architecture~\cite{content-centric} where
152   the documents of the library were the the main components around which
153   everything else has to be build;
154
155  \item developing indexing and searching techniques supporting semantic
156   queries to the library; 
157
158  \item developing languages and tools for a high-quality notational
159   rendering of mathematical information.\footnote{We have been active in
160   the \MATHML{} Working group since 1999.} 
161
162 \end{enumerate}
163
164 According to our content-centric commitment, the library exported from
165 \COQ{} was conceived as being distributed and most of the tools were developed
166 as Web services. The user can interact with the library and the tools by
167 means of a Web interface that orchestrates the Web services.
168
169 Web services and other tools have been implemented as front-ends
170 to a set of software components, collectively called the \HELM{} components.
171 At the end of the \MOWGLI{} project we already disposed of the following
172 tools and software components:
173 \begin{itemize}
174
175  \item XML specifications for the Calculus of Inductive Constructions,
176   with components for parsing and saving mathematical objects in such a
177   format~\cite{exportation-module};
178
179  \item metadata specifications with components for indexing and querying the
180   XML knowledge base;
181
182  \item a proof checker (i.e. the \emph{kernel} of a proof assistant), 
183   implemented to check that we exported from the \COQ{} library all the 
184   logically relevant content;
185
186  \item a sophisticated term parser (used by the search engine), able to deal 
187   with potentially ambiguous and incomplete information, typical of the 
188   mathematical notation~\cite{disambiguation};
189
190  \item a \emph{refiner} component, i.e. a type inference system, based on
191   partially specified terms, used by the disambiguating parser;
192
193  \item complex transformation algorithms for proof rendering in natural
194   language~\cite{remathematization};
195
196  \item an innovative, \MATHML-compliant rendering widget~\cite{padovani}
197   for the \GTK{} graphical environment,\footnote{\url{http://www.gtk.org/}}
198   supporting high-quality bidimensional
199   rendering, and semantic selection, i.e. the possibility to select semantically
200   meaningful rendering expressions, and to paste the respective content into
201   a different text area.
202
203 \end{itemize}
204
205 Starting from all this, developing our own proof assistant was not
206 too far away: essentially, we ``just'' had to
207 add an authoring interface, and a set of functionalities for the
208 overall management of the library, integrating everything into a
209 single system. \MATITA{} is the result of this effort. 
210
211 \subsection{The system}
212
213 \MATITA{} is a proof assistant (also called interactive theorem prover).
214 It is based on the Calculus of (Co)Inductive Constructions
215 (CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
216 Church enriched with primitive inductive and co-inductive data types.
217 Via the Curry-Howard isomorphism, the calculus can be seen as a very
218 rich higher order logic and proofs can be simply represented and
219 stored as lambda-terms. \COQ{} and \LEGO~\cite{lego} are other systems
220 that adopt (variations of) CIC as their foundation.
221
222 The proof language of \MATITA{} is procedural, in the tradition of the LCF
223 theorem prover~\cite{lcf}. \COQ, \NUPRL, PVS, Isabelle are all examples of
224 others systems
225 whose proof language is procedural. Traditionally, in a procedural system
226 the user interacts only with the \emph{script}, while proof terms are internal
227 records kept by the system. On the contrary, in \MATITA{} proof terms are
228 praised as declarative versions of the proof. Playing that role, they are the
229 primary mean of communication of proofs (once rendered to natural language
230 for human audiences).
231
232 The user interfaces now adopted by all the proof assistants based on a
233 procedural proof language have been inspired by the CtCoq pioneering
234 system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
235 by CtCoq is the Proof General generic interface~\cite{proofgeneral},
236 that has set a sort of
237 standard way to interact with the system. Several procedural proof assistants
238 have either adopted or cloned Proof General as their main user interface.
239 The authoring interface of \MATITA{} is a clone of the Proof General interface.
240 On the contrary, the interface to interact with the library is rather
241 innovative and directly inspired by the Web interfaces to our Web servers.
242
243 \MATITA{} is backward compatible with the XML library of proof objects exported
244 from \COQ{}, but, in order to test the actual usability of the system, we are
245 also developing a new library of basic results from scratch.
246
247 \subsection{Relationship with \COQ{}}
248
249 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
250 more the effect of the circumstances of its creation described 
251 above than the result of a deliberate design. In particular, we
252 (essentially) share the same foundational dialect of \COQ{} (the
253 Calculus of (Co)Inductive Constructions), the same implementation
254 language (\OCAML\footnote{\url{http://caml.inria.fr/}}),
255 and the same (procedural, script based) authoring philosophy.
256 However, the analogy essentially stops here and no code is shared
257 between the two systems.
258
259 In a sense, we like to think of \MATITA{} as the way \COQ{} would 
260 look like if entirely rewritten from scratch: just to give an
261 idea, although \MATITA{} currently supports almost all functionalities of
262 \COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
263 by \COQ{} (and we are convinced that, starting from scratch again,
264 we could reduce our code even further in a sensible way).
265
266 Moreover, the complexity of the code of \MATITA{} is greatly reduced with
267 respect to \COQ. For instance, the API of the components of \MATITA{} comprise
268 989 functions, to be compared with the 4'286 functions of \COQ.
269
270 Finally, \MATITA{} has several innovative features over \COQ{} that derive
271 from the integration of Mathematical Knowledge Management tools with proof
272 assistants. Among them, the advanced indexing tools over the library and
273 the parser for ambiguous mathematical notation.
274
275 The size and complexity improvements over \COQ{} must be understood
276 historically. \COQ{} is a quite old
277 system whose development started 20 years ago. Since then,
278 several developers have took over the code and several new research ideas
279 that were not considered in the original architecture have been experimented
280 and integrated in the system. Moreover, there exists a lot of developments
281 for \COQ{} that require backward compatibility between each pair of releases;
282 since many central functionalities of a proof assistant are based on heuristics
283 or arbitrary choices to overcome undecidability (e.g. for higher order
284 unification), changing these functionalities maintaining backward compatibility
285 is very difficult. Finally, the code of \COQ{} has been greatly optimized
286 over the years; optimization reduces maintainability and rises the complexity
287 of the code.
288
289 In writing \MATITA{} we have not been hindered by backward compatibility and
290 we have took advantage of the research results and experiences previously
291 developed by others, comprising the authors of \COQ. Moreover, starting from
292 scratch, we have designed in advance the architecture and we have split
293 the code in coherent minimally coupled components.
294
295 In the future we plan to exploit \MATITA{} as a test bench for new ideas and
296 extensions. Keeping the single components and the whole architecture as
297 simple as possible is thus crucial to foster future experiments and to
298 allow other developers to quickly understand our code and contribute.
299
300 %For direct experience of the authors, the learning curve to understand and
301 %be able to contribute to \COQ{}'s code is quite steep and requires direct
302 %and frequent interactions with \COQ{} developers.
303
304 \section{Architecture}
305 \label{architettura}
306
307 \begin{figure}[!ht]
308  \begin{center}
309   \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
310   \caption[\MATITA{} components and related applications]{\MATITA{}
311    components and related applications, with thousands of line of
312    codes (klocs)\strut}
313   \label{fig:libraries}
314  \end{center}
315 \end{figure}
316
317 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
318 (circle nodes) and \emph{applications} (squared nodes) developed in the
319 \HELM{} project. Each node is annotated with the number of lines of
320 source code (comprising comments).
321
322 Applications and \components{} depend on other \components{} forming a
323 directed acyclic graph (DAG). Each \component{} can be decomposed in
324 a set of \emph{modules} also forming a DAG.
325
326 Modules and \components{} provide coherent sets of functionalities
327 at different scales. Applications that require only a few functionalities
328 depend on a restricted set of \components.
329
330 Only the proof assistant \MATITA{} and the \WHELP{} search engine are
331 applications meant to be used directly by the user. All the other applications
332 are Web services developed in the \HELM{} and \MOWGLI{} projects and already
333 described elsewhere. In particular:
334 \begin{itemize}
335
336  \item The \emph{\GETTER}~\cite{zack-master} is a Web service to
337   retrieve an (XML) document from a physical location (URL) given its
338   logical name (URI). The Getter is responsible of updating a table that
339   maps URIs to URLs. Thanks to the Getter it is possible to work on a
340   logically monolithic library that is physically distributed on the
341   network.
342
343  \item \emph{\WHELP}~\cite{whelp} is a search engine to index and
344   locate mathematical concepts (axioms, theorems, definitions) in the
345   logical library managed by the Getter. Typical examples of
346   \WHELP{} queries are those that search for a theorem that generalize or
347   instantiate a given formula, or that can be immediately applied to
348   prove a given goal. The output of Whelp is an XML document that lists
349   the URIs of a complete set of candidates that are likely to satisfy
350   the given query. The set is complete in the sense that no concept that
351   actually satisfies the query is thrown away. However, the query is
352   only approximated in the sense that false matches can be returned.
353
354  \item \emph{\UWOBO}~\cite{zack-master} is a Web service that, given the
355   URI of a mathematical concept in the distributed library, renders it
356   according to the user provided two dimensional mathematical notation.
357   \UWOBO{} may also inline the rendering of mathematical concepts into
358   arbitrary documents before returning them.  The Getter is used by
359   \UWOBO{} to retrieve the document to be rendered.
360
361  \item The \emph{Proof Checker}~\cite{zack-master} is a Web service
362   that, given the URI of a concept in the distributed library, checks its
363   correctness. Since the concept is likely to depend in an acyclic way
364   on other concepts, the proof checker is also responsible of building
365   in a top-down way the DAG of all dependencies, checking in turn every
366   concept for correctness.
367
368  \item The \emph{Dependency Analyzer}~\cite{zack-master} is a Web
369   service that can produce a textual or graphical representation of the
370   dependencies of a concept.
371
372 \end{itemize}
373
374 The dependency of a \component{} or application over another \component{} can
375 be satisfied by linking the \component{} in the same executable.
376 For those \components{} whose functionalities are also provided by the
377 aforementioned Web services, it is also possible to link stub code that
378 forwards the request to a remote Web service. For instance, the
379 \GETTER{} application is just a wrapper to the \GETTER{} \component{}
380 that allows it to be used as a Web service. \MATITA{} can directly link
381 the code of the \GETTER{} \component, or it can use a stub library with
382 the same API that forwards every request to the Web service.
383
384 To better understand the architecture of \MATITA{} and the role of each
385 \component, we can focus on the representation of the mathematical
386 information.  In CIC terms are used to represent mathematical formulae,
387 types and proofs. \MATITA{} is able to handle terms at four different
388 levels of specification. On each level it is possible to provide a
389 different set of functionalities. The four different levels are: fully
390 specified terms; partially specified terms; content level terms;
391 presentation level terms.
392
393 \subsection{Fully specified terms}
394 \label{sec:fullyintro}
395
396  \emph{Fully specified terms} are CIC terms where no information is
397    missing or left implicit. A fully specified term should be well-typed.
398    The mathematical concepts (axioms, definitions, theorems) that are stored
399    in our mathematical library are fully specified and well-typed terms.
400    Fully specified terms are extremely verbose (to make type-checking
401    decidable). Their syntax is fixed and does not resemble the usual
402    extendible mathematical notation. They are not meant for direct user
403    consumption.
404
405    The \texttt{cic} \component{} defines the data type that represents CIC terms
406    and provides a parser for terms stored in XML format.
407
408    The most important \component{} that deals with fully specified terms is
409    \texttt{cic\_proof\_checking}. It implements the procedure that verifies
410    if a fully specified term is well-typed. It also implements the
411    \emph{conversion} judgement that verifies if two given terms are
412    computationally equivalent (i.e. they share the same normal form).
413
414    Terms may reference other mathematical concepts in the library.
415    One commitment of our project is that the library should be physically
416    distributed. The \GETTER{} \component{} manages the distribution,
417    providing a mapping from logical names (URIs) to the physical location
418    of a concept (an URL). The \texttt{urimanager} \component{} provides the URI
419    data type and several utility functions over URIs. The
420    \texttt{cic\_proof\_checking} \component{} calls the \GETTER{}
421    \component{} every time it needs to retrieve the definition of a mathematical
422    concept referenced by a term that is being type-checked. 
423
424    The Proof Checker application is the Web service that provides an interface
425    to the \texttt{cic\_proof\_checking} \component.
426
427    We use metadata and a sort of crawler to index the mathematical concepts
428    in the distributed library. We are interested in retrieving a concept
429    by matching, instantiation or generalization of a user or system provided
430    mathematical formula. Thus we need to collect metadata over the fully
431    specified terms and to store the metadata in some kind of (relational)
432    database for later usage. The \texttt{hmysql} \component{} provides
433    a simplified
434    interface to a (possibly remote) MySQL\footnote{\url{http://www.mysql.com/}}
435    database system used to store the metadata.
436    The \texttt{metadata} \component{} defines the data type of the metadata
437    we are collecting and the functions that extracts the metadata from the
438    mathematical concepts (the main functionality of the crawler).
439    The \texttt{whelp} \component{} implements a search engine that performs
440    approximated queries by matching/instantiation/generalization. The queries
441    operate only on the metadata and do not involve any actual matching
442    (see the \texttt{cic\_unification} \component in
443    Sect.~\ref{sec:partiallyintro}). Not performing any actual matching
444    a query only returns a complete and hopefully small set of matching
445    candidates. The process that has issued the query is responsible of
446    actually retrieving from the distributed library the candidates to prune
447    out false matches if interested in doing so.
448
449    The \WHELP{} application is the Web service that provides an interface to
450    the \texttt{whelp} \component.
451
452    According to our vision, the library is developed collaboratively so that
453    changing or removing a concept can invalidate other concepts in the library.
454    Moreover, changing or removing a concept requires a corresponding change
455    in the metadata database. The \texttt{library} \component{} is responsible
456    of preserving the coherence of the library and the database. For instance,
457    when a concept is removed, all the concepts that depend on it and their
458    metadata are removed from the library. This aspect will be better detailed
459    in Sect.~\ref{sec:libmanagement}.
460    
461 \subsection{Partially specified terms}
462 \label{sec:partiallyintro}
463
464 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
465 Omitted subterms can bear no information at all or they may be associated to
466 a sequent. The formers are called \emph{implicit terms} and they occur only
467 linearly. The latters may occur multiple times and are called
468 \emph{metavariables}. An \emph{explicit substitution} is applied to each
469 occurrence of a metavariable. A metavariable stands for a term whose type is
470 given by the conclusion of the sequent. The term must be closed in the
471 context that is given by the ordered list of hypotheses of the sequent.
472 The explicit substitution instantiates every hypothesis with an actual
473 value for the variable bound by the hypothesis.
474
475 Partially specified terms are not required to be well-typed. However a
476 partially specified term should be \emph{refinable}. A \emph{refiner} is
477 a type-inference procedure that can instantiate implicit terms and
478 metavariables and that can introduce
479 \emph{implicit coercions}~\cite{barthe95implicit} to make a
480 partially specified term well-typed. The refiner of \MATITA{} is implemented
481 in the \texttt{cic\_unification} \component. As the type checker is based on
482 the conversion check, the refiner is based on \emph{unification} that is
483 a procedure that makes two partially specified term convertible by instantiating
484 as few as possible metavariables that occur in them.
485
486 Since terms are used in CIC to represent proofs, correct incomplete
487 proofs are represented by refinable partially specified terms. The metavariables
488 that occur in the proof correspond to the conjectures still to be proved.
489 The sequent associated to the metavariable is the conjecture the user needs to
490 prove.
491
492 \emph{Tactics} are the procedures that the user can apply to progress in the
493 proof. A tactic proves a conjecture possibly creating new (and hopefully
494 simpler) conjectures. The implementation of tactics is given in the
495 \texttt{tactics} \component. It is heavily based on the refinement and
496 unification procedures of the \texttt{cic\_unification} \component.
497
498 The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
499 commands of the \MATITA{} proof assistant. Most of the commands are tactics.
500 Other commands are used to give definitions and axioms or to state theorems
501 and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA.
502 It implements the semantics of each command in the grafite AST as a function
503 from status to status.  It implements also an undo function to go back to
504 previous statuses.
505
506 As fully specified terms, partially specified terms are not well suited
507 for user consumption since their syntax is not extendible and it is not
508 possible to adopt the usual mathematical notation. However they are already
509 an improvement over fully specified terms since they allow to omit redundant
510 information that can be inferred by the refiner.
511
512 \subsection{Content level terms}
513 \label{sec:contentintro}
514
515 The language used to communicate proofs and especially formulae with the
516 user does not only needs to be extendible and accommodate the usual mathematical
517 notation. It must also reflect the comfortable degree of imprecision and
518 ambiguity that the mathematical language provides.
519
520 For instance, it is common practice in mathematics to speak of a generic
521 equality that can be used to compare any two terms. However, it is well known
522 that several equalities can be distinguished as soon as we care for decidability
523 or for their computational properties. For instance equality over real
524 numbers is well known to be undecidable, whereas it is decidable over
525 rational numbers.
526
527 Similarly, we usually speak of natural numbers and their operations and
528 properties without caring about their representation. However the computational
529 properties of addition over the binary representation are very different from
530 those of addition over the unary representation. And addition over two natural
531 numbers is definitely different from addition over two real numbers.
532
533 Formal mathematics cannot hide these differences and obliges the user to be
534 very precise on the types he is using and their representation. However,
535 to communicate formulae with the user and with external tools, it seems good
536 practice to stick to the usual imprecise mathematical ontology. In the
537 Mathematical Knowledge Management community this imprecise language is called
538 the \emph{content level}~\cite{adams} representation of formulae.
539
540 In \MATITA{} we provide translations from partially specified terms
541 to content level terms and the other way around. The first translation can also
542 be applied to fully specified terms since a fully specified term is a special
543 case of partially specified term where no metavariable or implicit term occurs.
544
545 The translation from partially specified terms to content level terms must
546 discriminate between terms used to represent proofs and terms used to represent
547 formulae. The firsts are translated to a content level representation of
548 proof steps that can in turn easily be rendered in natural language
549 using techniques inspired by~\cite{natural,YANNTHESIS}. The representation
550 adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
551 isomorphic to it. Terms that represent formulae are translated to \MATHML{}
552 Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
553 for the representation of content level formulae in an extensible XML format.
554
555 The translation to content level is implemented in the
556 \texttt{acic\_content} \component. Its input are \emph{annotated partially
557 specified terms}, that are maximally unshared
558 partially specified terms enriched with additional typing information for each
559 subterm. This information is used to discriminate between terms that represent
560 proofs and terms that represent formulae. Part of it is also stored at the
561 content level since it is required to generate the natural language rendering
562 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
563 and not a DAG). The reason is that to different occurrences of a subterm
564 we need to associate different typing information.
565 This association is made easier when the term is represented as a tree since
566 it is possible to label each node with an unique identifier and associate
567 the typing information using a map on the identifiers.
568 The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
569 by the \texttt{library} \component{} since fully specified terms are stored
570 in the library in their annotated form.
571
572 We do not provide yet a reverse translation from content level proofs to
573 partially specified terms. But in \texttt{cic\_disambiguation} we do provide
574 the reverse translation for formulae. The mapping from
575 content level formulae to partially specified terms is not unique due to
576 the ambiguity of the content level. As a consequence the translation
577 is guided by an \emph{interpretation}, that is a function that chooses for
578 every ambiguous formula one partially specified term. The
579 \texttt{cic\_disambiguation} \component{} implements the
580 disambiguation algorithm presented in~\cite{disambiguation} that is
581 responsible of building in an efficient way the set of all correct
582 interpretations. An interpretation is correct if the partially specified term
583 obtained using the interpretation is refinable.
584
585 In Sect.~\ref{sec:partiallyintro} we described the semantics of
586 a command as a
587 function from status to status. We also hinted that the formulae in a
588 command are encoded as partially specified terms. However, consider the
589 command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
590 of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
591 replace $x$ in that context, its encoding as a term cannot be computed
592 until $x$ is located. In other words, $y^2$ must be disambiguated in the
593 context of the occurrence $x$ it must replace.
594
595 The elegant solution we have implemented consists in representing terms
596 in a command as functions from a context to a partially refined term. The
597 function is obtained by partially applying our disambiguation function to
598 the content level term to be disambiguated. Our solution should be compared with
599 the one adopted in the \COQ{} system, where ambiguity is only relative to
600 De Brujin indexes.
601 In \COQ, variables can be bound either by name or by position. A term
602 occurring in a command has all its variables bound by name to avoid the need of
603 a context during disambiguation.  This makes more complex every
604 operation over terms (i.e. according to our architecture every module that
605 depends on \texttt{cic}) since the code must deal consistently with both kinds
606 of binding. Moreover, this solution cannot cope with other forms of ambiguity
607 (as the context dependent meaning of the exponent in the previous example).
608
609 \subsection{Presentation level terms}
610 \label{sec:presentationintro}
611
612 Content level terms are a sort of abstract syntax trees for mathematical
613 formulae and proofs. The concrete syntax given to these abstract trees
614 is called \emph{presentation level}.
615
616 The main important difference between the content level language and the
617 presentation level language is that only the former is extendible. Indeed,
618 the presentation level language is a finite language that comprises all
619 the usual mathematical symbols. Mathematicians invent new notions every
620 single day, but they stick to a set of symbols that is more or less fixed.
621
622 The fact that the presentation language is finite allows the definition of
623 standard languages. In particular, for formulae we have adopt \MATHML{}
624 Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
625 visually
626 represent proofs it is enough to embed formulae in plain text enriched with
627 formatting boxes. Since the language of formatting boxes is very simple,
628 many equivalent specifications exist and we have adopted our own, called
629 \BOXML.
630
631 The \texttt{content\_pres} \component{} contains the implementation of the
632 translation from content level terms to presentation level terms. The
633 rendering of presentation level terms is left to the application that uses
634 the \component. However, in the \texttt{hgdome} \component{} we provide a few
635 utility functions to build a \GDOME~\cite{gdome2} \MATHML+\BOXML{} tree from our
636 presentation
637 level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
638 \GTKMATHVIEW{}
639 widget developed by Luca Padovani~\cite{padovani}. The widget is
640 particularly interesting since it allows the implementation of \emph{semantic
641 selection}.
642
643 Semantic selection is a technique that consists in enriching the presentation
644 level terms with pointers to the content level terms and to the partially
645 specified terms they correspond to. Highlight of formulae in the widget is
646 constrained to selection of meaningful expressions, i.e. expressions that
647 correspond to a lower level term, that is a content term or a partially or
648 fully specified term.
649 Once the rendering of a lower level term is
650 selected it is possible for the application to retrieve the pointer to the
651 lower level term. An example of applications of semantic selection is
652 \emph{semantic copy \& paste}: the user can select an expression and paste it
653 elsewhere preserving its semantics (i.e. the partially specified term),
654 possibly performing some semantic transformation over it (e.g. renaming
655 variables that would be captured or lambda-lifting free variables).
656
657 The reverse translation from presentation level terms to content level terms
658 is implemented by a parser that is also found in \texttt{content\_pres}.
659 Differently from the translation from content level terms to partially
660 refined terms, this translation is not ambiguous. The reason is that the
661 parsing tool we have adopted (CamlP4) is not able to parse ambiguous
662 grammars. Thus we require the mapping from presentation level terms
663 (concrete syntax) to content level terms (abstract syntax) to be unique.
664 This means that the user must fix once and for all the associativity and
665 precedence level of every operator he is using. In practice this limitation
666 does not seem too strong. The reason is that the target of the
667 translation is an ambiguous language and the user is free to associate
668 to every content level term several different interpretations (as a
669 partially specified term).
670
671 Both the direct and reverse translation from presentation to content level
672 terms are parameterized over the user provided mathematical notation. 
673 The \texttt{lexicon} \component{} is responsible of managing the lexicon,
674 that is the set of active notations. It defines an abstract syntax tree
675 of commands to declare and activate new notations and it implements the
676 semantics of these commands. It also implements undoing of the semantic
677 actions. Among the commands there are hints to the
678 disambiguation algorithm that are used to control and speed up disambiguation.
679 These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
680
681 Finally, the \texttt{grafite\_parser} \component{} implements a parser for
682 the concrete syntax of the commands of \MATITA. The parser process a stream
683 of characters and returns a stream of abstract syntax trees (the ones
684 defined by the \texttt{grafite} component and whose semantics is given
685 by \texttt{grafite\_engine}). When the parser meets a command that changes
686 the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
687 process the command. When the parser needs to parse a term at the presentation
688 level, it invokes the already described parser for terms contained in
689 \texttt{content\_pres}.
690
691 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
692 against the \texttt{grafite\_parser} \components{}
693 since they provide an interface to the user. In both cases the formulae
694 written by the user are parsed using the \texttt{content\_pres} \component{} and
695 then disambiguated using the \texttt{cic\_disambiguation} \component.  However,
696 only \MATITA{} is linked against the \texttt{grafite\_engine} and
697 \texttt{tactics} components (summing up to a total of 11'200 lines of code)
698 since \WHELP{} can only execute those ASTs that correspond to queries
699 (implemented in the \texttt{whelp} component).
700
701 The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
702 providing a rendering service for the documents in the distributed library.
703 To render a document given its URI, \UWOBO{} retrieves it using the
704 \GETTER{} obtaining a document with fully specified terms. Then it translates
705 it to the presentation level passing through the content level. Finally
706 it returns the result document to be rendered by the user's
707 browser.
708
709 The \components{} not yet described (\texttt{extlib}, \texttt{xml},
710 \texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are 
711 minor \components{} that provide a core of useful functions and basic
712 services missing from the standard library of the programming language.
713 %In particular, the \texttt{xml} \component{} is used to easily represent,
714 %parse and pretty-print XML files.
715
716 \section{The interface to the library}
717 \label{sec:library}
718
719 A proof assistant provides both an interface to interact with its library and
720 an \emph{authoring} interface to develop new proofs and theories. According
721 to its historical origins, \MATITA{} strives to provide innovative
722 functionalities for the interaction with the library. It is more traditional
723 in its script based authoring interface.
724
725 In the remaining part of the paper we focus on the user view of \MATITA.
726 This section is devoted to the aspects of the tool that arise from the
727 document centric approach to the library. Sect.~\ref{sec:authoring} describes
728 the peculiarities of the authoring interface.
729
730 The library of \MATITA{} comprises mathematical concepts (theorems,
731 axioms, definitions) and notation. The concepts are authored sequentially
732 using scripts that are (ordered) sequences of procedural commands.
733 However, once they are produced we store them independently in the library.
734 The only relation implicitly kept between the concepts are the logical,
735 acyclic dependencies among them. This way the library forms a global (and
736 distributed) hypertext.
737
738 \begin{figure}[!ht]
739  \begin{center}
740   \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-browsing}
741   \hspace{0.05\textwidth}
742   \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-query}
743   \caption{Browsing and searching the library\strut}
744   \label{fig:cicbrowser1}
745  \end{center}
746 \end{figure}
747
748 \begin{figure}[!ht]
749  \begin{center}
750   \includegraphics[width=0.70\textwidth]{pics/cicbrowser-screenshot-con}
751   \caption[Natural language rendering]{Natural language rendering of a theorem
752   from the library\strut}
753   \label{fig:cicbrowser2}
754  \end{center}
755 \end{figure}
756
757 Several useful operations can be implemented on the library only,
758 regardless of the scripts. For instance, searching and browsing is
759 implemented by the ``cicBrowser'' window available from the \MATITA{}
760 GUI. Using it, the hierarchical structure of the library can be
761 explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural
762 language rendering of proofs can be inspected
763 (Fig.~\ref{fig:cicbrowser2}), and content based searches on the
764 library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}).
765 Available content based searches are described in
766 Sect.~\ref{sec:indexing}.  Other examples of library operations are
767 disambiguation of content level terms (see
768 Sect.~\ref{sec:disambiguation}) and automatic proof searching (see
769 Sect.~\ref{sec:automation}).
770
771 The key requisite for the previous operations is that the library must
772 be fully accessible and in a logically consistent state. To preserve
773 consistency, a concept cannot be altered or removed unless the part of the
774 library that depends on it is modified accordingly. To allow incremental
775 changes and cooperative development, consistent revisions are necessary.
776 For instance, to modify a definition, the user could fork a new version
777 of the library where the definition is updated and all the concepts that
778 used to rely on it are absent. The user is then responsible to restore
779 the removed part in the new branch, merging the branch when the library is
780 fully restored.
781
782 To implement the proposed versioning system on top of a standard one
783 it is necessary to implement \emph{invalidation} first. Invalidation
784 is the operation that locates and removes from the library all the concepts
785 that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
786 a concept from the library also involves deleting its metadata from the
787 database.
788
789 For non collaborative development, full versioning can be avoided, but
790 invalidation is still required. Since nobody else is relying on the
791 user development, the user is free to change and invalidate part of the library
792 without branching. Invalidation is still necessary to avoid using a
793 concept that is no longer valid.
794 So far, in \MATITA{} we address only this non collaborative scenario
795 (see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
796 is still under design.
797
798 Scripts are not seen as constituents of the library. They are not published
799 and indexed, so they cannot be searched or browsed using \HELM{} tools.
800 However, they play a central role for the maintenance of the library.
801 Indeed, once a concept is invalidated, the only way to restore it is to
802 fix the possibly broken script that used to generate it.
803 Moreover, during the authoring phase, scripts are a natural way to
804 group concepts together. They also constitute a less fine grained clustering
805 of concepts for invalidation.
806
807 In the rest of this section we present in more details the functionalities of
808 \MATITA{} related to library management and exploitation.
809 Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
810 the \MATITA{} authoring interface.
811
812 \subsection{Indexing and searching}
813 \label{sec:indexing}
814
815 The \MATITA{} system is first of all an interface between the user and
816 the mathematical library. For this reason, it is important to be
817 able to search and retrieve mathematical concepts in a quick and 
818 effective way, assuming as little knowledge as possible about the 
819 library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
820 for mathematical concepts, based on a rich metadata set that has been 
821 tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
822 set, and the searching facilites built on top of them --- collected 
823 in the so called \WHELP{} search engine --- have been
824 extensively described in~\cite{whelp}. Let us just recall here that
825 the \WHELP{} metadata model is essentially based a single ternary relation 
826 \REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
827  given position $p$, where the position specify the place of the 
828 occurrence of $t$ inside $s$ (we currently work with a fixed set of 
829 positions, discriminating the hypothesis from the conclusion and
830 outermost form innermost occurrences). This approach is extremely 
831 flexible, since extending the set of positions 
832 we may improve the granularity and the precision of our indexing technique,
833 with no additional architectural impact.
834
835 Every time a new mathematical concept is created and saved by the user it gets 
836 indexed, and becomes immediately visible in the library. Several 
837 interesting and innovative features of \MATITA{} described in the following
838 sections rely in a direct or indirect way on its metadata system and
839 the search features. Here, we shall just recall some of its most
840 direct applications.
841
842 A first, very simple but not negligeable feature is the check for duplicates.
843 As soon as a theorem is stated, just before starting its proof, 
844 the library is searched 
845 to check that no other equivalent statement has been already proved
846 (based on the pattern matching functionality of \WHELP); if this is the case,
847 a warning is raised to the user. At present, the notion of equivalence 
848 adopted by \MATITA{} is convertibility, but we may imagine to weaken it 
849 in the future, covering for instance isomorphisms.    
850
851 Another useful \WHELP{} operation is \HINT; we may invoke this query
852 at any moment during the authoring of a proof, resulting in the list
853 of all theorems of the library which can be applied to the current
854 goal. In practice, this is mostly used not really to discover what theorems
855 can be applied to a given goal, but to actually retrieve a theorem that 
856 we wish to apply, but whose name we have forgotten.
857 In fact, even if \MATITA{} adopts a semi-rigid naming convention for 
858 statements (see Sect.~\ref{sec:naming}) that greatly simplifies the effort
859 of recalling names, the naming discipline remains one of the most
860 annoying aspects of formal developments, and \HINT{} provides
861 a very friendly solution.
862 In the near feature, we expect to extend the \HINT{} operation to
863 a \REWRITEHINT, resulting in all equational statements that
864 can be applied to rewrite the current goal.
865
866 \subsection{Disambiguation}
867 \label{sec:disambiguation}
868
869 Software applications that involve input of mathematical content should strive
870 to require the user as less drift from informal mathematics as possible. We
871 believe this to be a fundamental aspect of such applications user interfaces.
872 Being that drift in general very large when inputing
873 proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
874 mathematical formulae which can be input using a \TeX-like encoding (the
875 concrete syntax corresponding to presentation level terms) and are then
876 translated (in multiple steps) to partially specified terms as sketched in
877 Sect.~\ref{sec:contentintro}.
878
879 The key component of the translation is the generic disambiguation algorithm
880 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
881 and presented in~\cite{disambiguation}. In this section we present how to use
882 that algorithm in the context of the development of a library of formalized
883 mathematics. We will see that using multiple passes of the algorithm, varying
884 some of its parameters, helps in keeping the input terse without sacrificing
885 expressiveness.
886
887 \subsubsection{Disambiguation aliases}
888 \label{sec:disambaliases}
889
890 Consider the following command to state a theorem over integer numbers:
891
892 \begin{grafite}
893 theorem Zlt_compat:
894   \forall x, y, z. x < y \to y < z \to x < z.
895 \end{grafite}
896
897 The symbol \OP{<} is likely to be overloaded in the library
898 (at least over natural numbers). 
899 Thus, according to the disambiguation algorithm, two different
900 refinable partially specified terms could be associated to it.
901 \MATITA{} asks the user what interpretation he meant. However, to avoid
902 posing the same question in case of a future re-execution (e.g. undo/redo),
903 the choice must be recorded. Since scripts need to be re-executed after
904 invalidation, the choice record must be permanently stored somewhere. The most
905 natural place is in the script itself.
906
907 In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
908 They are mappings, stored in the library, from ambiguity sources
909 (identifiers, symbols and literal numbers at the content level) to partially
910 specified terms. In case of overloaded sources there exists multiple aliases
911 with the same source. It is possible to record \emph{disambiguation
912 preferences} to select one of the aliases of an overloaded source.
913
914 Preferences can be explicitely given in the script (using the
915 misleading \texttt{alias} commands), but
916 are also implicitly added when a new concept is introduced (\emph{implicit
917 preferences}) or after a sucessfull disambiguation that did not require
918 user interaction. Explicit preferences are added automatically by \MATITA{} to
919 record the disambiguation choices of the user. For instance, after the
920 disambiguation of the command above, the script is altered as follows:
921
922 \begin{grafite}
923 alias symbol "lt" = "integer 'less than'".
924 theorem Zlt_compat:
925   \forall x, y, z. x < y \to y < z \to x < z.
926 \end{grafite}
927
928 The ``alias'' command in the example sets the preferred alias for the
929 \OP{lt} symbol.
930
931 Implicit preferences for new concepts are set since a concept just defined is
932 likely to be the preferred one in the rest of the script. Implicit preferences
933 learned from disambiguation of previous commands grant the coherence of
934 the disambiguation in the rest of the script and speed up disambiguation
935 reducing the search space.
936
937 Disambiguation preferences are included in the lexicon status
938 (see Sect.~\ref{sec:presentationintro}) that is part of the authoring interface
939 status.  Unlike aliases, they are not part of the library.
940
941 When starting a new authoring session the set of disambiguation preferences
942 is empty. Until it contains a preference for each overloaded symbol to be
943 used in the script, the user can be faced with questions from the disambiguator.
944 To reduce the likelyhood of user interactions, we introduced
945 the \texttt{include} command. With \texttt{include} it is possible to import
946 at once in the current session the set of preferences that was in effect
947 at the end of the execution of a given script.
948
949 Preferences can be changed. For instance, at the start of the development
950 of integer numbers the preference for the symbol \OP{<} is likely
951 to be the one over natural numbers; sooner or later it will be set to the one
952 over integer numbers.
953
954 Nothing forbids the set of preferences to become incoherent. For this reason
955 the disambiguator cannot always respect the user preferences.
956 Consider, for example:
957 \begin{grafite}
958 theorem Zlt_mono:
959   \forall x, y, k. x < y \to x < y + k.
960 \end{grafite}
961
962 No refinable partially specified term corresponds to the preferences:
963 \OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
964 limitation we organized disambiguation in \emph{multiple passes}: when the
965 disambiguator fails, disambiguation is tried again with a less strict set of
966 preferences.
967
968 Several disambiguation parameters can vary among passes. With respect to
969 preference handling we implemented three passes.  In the first pass, called
970 \emph{mono-preferences}, we consider only the aliases corresponding to the
971 current preferences.  In the second pass, called \emph{multi-preferences}, we
972 consider every alias corresponding to a current or past preference.  For
973 instance, in the example above disambiguation succeeds in the multi-preference
974 pass. In the third pass, called \emph{library-preferences}, all aliases
975 available in the library are considered.
976
977 The rationale behind this choice is trying to respect user preferences in early
978 passes that complete quickly in case of failure; later passes are slower but
979 have more chances of success.
980
981 \subsubsection{Operator instances}
982 \label{sec:disambinstances}
983
984 Consider now the following theorem:
985 \begin{grafite}
986 theorem lt_to_Zlt_pos_pos:
987   \forall n, m: nat. n < m \to pos n < pos m. 
988 \end{grafite}
989 and assume that there exist in the library aliases for \OP{<} over natural
990 numbers and over integer numbers. None of the passes described above is able to
991 disambiguate \texttt{lt\_to\_Zlt\_pos\_pos}, no matter how preferences are set.
992 This is because the \OP{<} operator occurs twice in the content level term (it
993 has two \emph{instances}) and two different interpretations for it have to be
994 used in order to obtain a refinable partially specified term.
995
996 To address this issue, we have the ability to consider each instance of a single
997 symbol as a different ambiguous expression in the content level term, and thus
998 we can use a different alias for each of them. Exploiting or not this feature is
999 one of the disambiguation pass parameters. A disambiguation pass which exploit
1000 it is said to be using \emph{fresh instances} (opposed to a \emph{shared
1001 instances} pass).
1002
1003 Fresh instances lead to a non negligible performance loss (since the choice of
1004 an alias for one instance does not constraint the choice of the others). For
1005 this reason we always attempt a fresh instances pass only after attempting a
1006 non-fresh one.
1007
1008 \paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
1009 instance-independent. However, implicit preferences obtained as a result of a
1010 disambiguation pass which uses fresh instances ought to be instance-dependent.
1011 Informally, the set of preferences that can be respected by the disambiguator on
1012 the theorem above is: ``the first instance of the \OP{<} symbol is over natural
1013 numbers, while the second is on integer numbers''.
1014
1015 Instance-dependent preferences are meaningful only for the term whose
1016 disambiguation generated it. For this reason we call them \emph{one-shot
1017 preferences} and \MATITA{} does not use them to disambiguate further terms in
1018 the script.
1019
1020 \subsubsection{Implicit coercions}
1021 \label{sec:disambcoercions}
1022
1023 Consider the following theorem about derivation:
1024 \begin{grafite}
1025 theorem power_deriv:
1026   \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
1027 \end{grafite}
1028 and assume that in the library there is an alias mapping \OP{\^} to a partially
1029 specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
1030 order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
1031 right hand side of the equality need to be ``injected'' from \texttt{nat} to
1032 \texttt{R}.  The refiner of \MATITA{} supports \emph{implicit coercions} for
1033 this reason: given as input the above presentation level term, it will return a
1034 partially specified term where in place of \texttt{n} the application of a
1035 coercion from \texttt{nat} to \texttt{R} appears (assuming such a coercion has
1036 been defined in advance).
1037
1038 Coercions are not always desirable. For example, in disambiguating
1039 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
1040 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
1041 among the possible partially specified term choices. For this reason we always
1042 attempt a disambiguation pass which require the refiner not to use the coercions
1043 before attempting a coercion-enabled pass.
1044
1045 The choice of whether implicit coercions are enabled or not interact with the
1046 choice about operator instances. Indeed, consider again
1047 \texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
1048 instances. In case there exists a coercion from natural numbers to (positive)
1049 integers (which indeed does), the
1050 theorem can be disambiguated using twice that coercion on the left hand side of
1051 the implication. The obtained partially specified term however would not
1052 probably be the expected one, being a theorem which prove a trivial implication.
1053 Motivated by this and similar examples we choose to always prefer fresh
1054 instances over implicit coercions, i.e.  we always attempt disambiguation
1055 passes with fresh instances
1056 and no implicit coercions before attempting passes with implicit coercions.
1057
1058 \subsubsection{Disambiguation passes}
1059 \label{sec:disambpasses}
1060
1061 According to the criteria described above, in \MATITA{} we perform the
1062 disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
1063 our experience that choice gives reasonable performance and minimize the need of
1064 user interaction during the disambiguation.
1065
1066 \begin{table}[ht]
1067  \caption{Disambiguation passes sequence\strut}
1068  \label{tab:disambpasses} 
1069  \begin{center}
1070   \begin{tabular}{c|c|c|c}
1071    \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
1072    & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Preferences}}
1073    & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
1074    & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
1075    \hline
1076    \PASS & Mono-preferences     & Shared instances  & Disabled \\
1077    \PASS & Multi-preferences    & Shared instances  & Disabled \\
1078    \PASS & Mono-preferences     & Fresh instances   & Disabled \\
1079    \PASS & Multi-preferences    & Fresh instances   & Disabled \\
1080    \PASS & Mono-preferences     & Fresh instances   & Enabled  \\
1081    \PASS & Multi-preferences    & Fresh instances   & Enabled  \\
1082    \PASS & Library-preferences  & Fresh instances   & Enabled
1083   \end{tabular}
1084  \end{center}
1085 \end{table}
1086
1087 \subsection{Generation and invalidation}
1088 \label{sec:libmanagement}
1089
1090 %The aim of this section is to describe the way \MATITA{} 
1091 %preserves the consistency and the availability of the library
1092 %using the \WHELP{} technology, in response to the user alteration or 
1093 %removal of mathematical objects.
1094 %
1095 %As already sketched in Sect.~\ref{sec:fullyintro} what we generate 
1096 %from a script is split among two storage media, a
1097 %classical filesystem and a relational database. The former is used to
1098 %store the XML encoding of the objects defined in the script, the
1099 %disambiguation aliases and the interpretation and notational convention defined,
1100 %while the latter is used to store all the metadata needed by
1101 %\WHELP.
1102 %
1103 %While the consistency of the data store in the two media has
1104 %nothing to do with the nature of
1105 %the content of the library and is thus uninteresting (but really
1106 %tedious to implement and keep bug-free), there is a deeper
1107 %notion of mathematical consistency we need to provide. Each object
1108 %must reference only defined object (i.e. each proof must use only
1109 %already proved theorems). 
1110
1111 In this section we will focus on how \MATITA{} ensures the library 
1112 consistency during the formalization of a mathematical theory, 
1113 giving the user the freedom of adding, removing, modifying objects
1114 without loosing the feeling of an always visible and browsable
1115 library.
1116
1117 \subsubsection{Invalidation}
1118
1119 Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
1120
1121 The first one is the calculation of all the concepts that recursively
1122 depend on the ones we are invalidating.  The calculation of the
1123 reverse dependencies can be computed using the relational database
1124 that stores metadata.
1125 This technique is the same used by the \emph{Dependency Analyzer}
1126 and is described in~\cite{zack-master}.
1127
1128 The second phase is the removal of all the results of the generation,
1129 metadata included.
1130
1131 \subsubsection{Regeneration}
1132
1133 %The typechecker component guarantees that if an object is well typed
1134 %it depends only on well typed objects available in the library,
1135 %that is exactly what we need to be sure that the logic consistency of
1136 %the library is preserved.
1137
1138 To regenerate an invalidated part of the library \MATITA{} re-executes
1139 the script files that produced the invalidated concepts.  The main 
1140 problem is to find a suitable order of execution of the scripts.
1141
1142 For this purpose we provide a tool called \MATITADEP{}
1143 that takes in input the list of scripts that compose the development and
1144 outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
1145 The user is not asked to run \MATITADEP{} by hand, but
1146 simply to tell \MATITA{} the root directory of his development (where all
1147 script files can be found) and \MATITA{} will handle all the generation
1148 related tasks, including dependencies calculation.
1149
1150 To compute dependencies it is enough to look at the script files for
1151 disambiguation preferences declared or imported from other scripts
1152 (see \ref{sec:disambaliases}). 
1153
1154 Regenerating the content of a modified script file involves the preliminary
1155 invalidation of all its old content.
1156
1157 \subsubsection{Batch vs Interactive}
1158
1159 \MATITA{} includes an interactive authoring interface and a batch
1160 ``compiler'' (\MATITAC). 
1161
1162 Only the former is intended to be used directly by the
1163 user, the latter is automatically invoked by \MATITA{}
1164 to try to regenerate parts of the library previously invalidated.
1165
1166 While they share the same engine for generation and invalidation, they
1167 provide different granularity. \MATITAC{} is only able to reexecute a
1168 whole script and similarly to invalidate the whole content of a script
1169 (together with all the other scripts that rely on an concept defined
1170 in it). 
1171
1172 \subsection{Automation}
1173 \label{sec:automation}
1174
1175 \TODO{sezione sull'automazione}
1176
1177 \subsection{Naming convention}
1178 \label{sec:naming}
1179
1180 A minor but not entirely negligible aspect of \MATITA{} is that of
1181 adopting a (semi)-rigid naming convention for identifiers, derived by 
1182 our studies about metadata for statements. 
1183 The convention is only applied to identifiers for theorems 
1184 (not definitions), and relates the name of a proof to its statement.
1185 The basic rules are the following:
1186 \begin{itemize}
1187 \item each identifier is composed by an ordered list of (short)
1188 names occurring in a left to right traversal of the statement; 
1189 \item all identifiers should (but this is not strictly compulsory) 
1190 separated by an underscore,
1191 \item identifiers in two different hypothesis, or in an hypothesis
1192 and in the conclusion must be separated by the string ``\verb+_to_+'';
1193 \item the identifier may be followed by a numerical suffix, or a
1194 single or double apostrophe.
1195
1196 \end{itemize}
1197 Take for instance the theorem
1198 \[\forall n:nat. n = plus \; n\; O\]
1199 Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, 
1200 \verb+eq_n_plus_n_O+ and so on. 
1201 Similarly, consider the theorem 
1202 \[\forall n,m:nat. n<m \to n \leq m\]
1203 In this case \verb+lt_to_le+ is a legal name, 
1204 while \verb+lt_le+ is not.\\
1205 But what about, say, the symmetric law of equality? Probably you would like 
1206 to name such a theorem with something explicitly recalling symmetry.
1207 The correct approach, 
1208 in this case, is the following. You should start with defining the 
1209 symmetric property for relations
1210
1211 \[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
1212
1213 Then, you may state the symmetry of equality as
1214 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
1215 and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem. 
1216 So, somehow unexpectedly, the introduction of semi-rigid naming convention
1217 has an important beneficial effect on the global organization of the library, 
1218 forcing the user to define abstract notions and properties before 
1219 using them (and formalizing such use).
1220
1221 Two cases have a special treatment. The first one concerns theorems whose
1222 conclusion is a (universally quantified) predicate variable, i.e. 
1223 theorems of the shape
1224 $\forall P,\dots.P(t)$.
1225 In this case you may replace the conclusion with the word
1226 ``elim'' or ``case''.
1227 For instance the name \verb+nat_elim2+ is a legal name for the double
1228 induction principle.
1229
1230 The other special case is that of statements whose conclusion is a
1231 match expression. 
1232 A typical example is the following
1233 \begin{verbatim}
1234   \forall n,m:nat. 
1235       match (eqb n m) with
1236         [ true  \Rightarrow n = m 
1237         | false \Rightarrow n \neq m]
1238 \end{verbatim}
1239 where $eqb$ is boolean equality.
1240 In this cases, the name can be build starting from the matched
1241 expression and the suffix \verb+_to_Prop+. In the above example, 
1242 \verb+eqb_to_Prop+ is accepted. 
1243
1244 \section{The authoring interface}
1245 \label{sec:authoring}
1246
1247 The authoring interface of \MATITA{} is very similar to Proof General.  We
1248 chose not to build the \MATITA{} UI over Proof General for two reasons. First
1249 of all we wanted to integrate our XML-based rendering technologies, mainly
1250 \GTKMATHVIEW. At the time of writing Proof General supports only text based
1251 rendering.\footnote{This may change with the future release of Proof General
1252 based on Eclipse, but is not yet the case.} The second reason is that we wanted
1253 to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
1254 as \GTK{} is.
1255
1256 Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
1257 featuring two windows. The background one is very like to the Proof General
1258 interface. The main difference is that we use the \GTKMATHVIEW{} widget to
1259 render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
1260 advantage of the whole bidimensional mathematical notation. The foreground
1261 window is an instance of the cicBrowser used to render the proof being
1262 developed.
1263
1264 Note that the syntax used in the script view is \TeX-like, however Unicode is 
1265 fully supported so that mathematical glyphs can be input as such.
1266
1267 \begin{figure}[!ht]
1268  \begin{center}
1269   \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
1270   \caption{Authoring interface\strut}
1271   \label{fig:screenshot}
1272  \end{center}
1273 \end{figure}
1274
1275 Since the concepts of script based proof authoring are well-known, the
1276 remaining part of this section is dedicated to the distinguishing
1277 features of the \MATITA{} authoring interface.
1278
1279 \subsection{Direct manipulation of terms}
1280 \label{sec:directmanip}
1281
1282 While terms are input as \TeX-like formulae in \MATITA, they are converted to a
1283 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
1284 \GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
1285 high-quality bidimensional rendering of terms (including the use of fancy
1286 layout schemata like radicals and matrices) and the use of a
1287 concise and widespread textual syntax.
1288
1289 Keeping pointers from the presentations level terms down to the
1290 partially specified ones \MATITA{} enable direct manipulation of
1291 rendered (sub)terms in the form of hyperlinks and semantic selection.
1292
1293 \emph{Hyperlinks} have anchors on the occurrences of constant and
1294 inductive type constructors and point to the corresponding definitions
1295 in the library. Anchors are available notwithstanding the use of
1296 user-defined mathematical notation: as can be seen on the right of
1297 Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
1298 encoding complex notations retain all the hyperlinks of constants or
1299 constructors used in the notation.
1300
1301 \emph{Semantic selection} enables the selection of mixed
1302 \MATHML+\BOXML{} markup, constraining the selection to markup
1303 representing meaningful CIC (sub)terms. In the example on the left of
1304 Fig.~\ref{fig:directmanip} is thus possible to select the subterm
1305 $\mathrm{prime}~n$, whereas it would not be possible to select
1306 $\to n$ since the former denotes an application while the
1307 latter it not a subterm. Once a meaningful (sub)term has been
1308 selected actions can be done on it like reductions or tactic
1309 applications.
1310
1311 \begin{figure}[!ht]
1312  \begin{center}
1313   \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
1314   \hspace{0.05\textwidth}
1315   \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
1316   \caption[Semantic selection and hyperlinks]{Semantic selection (on the left)
1317   and hyperlinks (on the right)\strut}
1318   \label{fig:directmanip}
1319  \end{center}
1320 \end{figure}
1321
1322 \subsection{Patterns}
1323 \label{sec:patterns}
1324
1325 In several situations working with direct manipulation of terms is 
1326 simpler and faster than typing the corresponding textual 
1327 commands~\cite{proof-by-pointing}.
1328 Nonetheless we need to record actions and selections in scripts.
1329
1330 In \MATITA{} \emph{patterns} are textual representations of selections.
1331 Users can select using the GUI and then ask the system to paste the
1332 corresponding pattern in this script, but more often this process is
1333 transparent: once an action is performed on a selection, the corresponding
1334 textual command is computed and inserted in the script.
1335
1336 \subsubsection{Pattern syntax}
1337
1338 Patterns are composed of two parts: \NT{sequent\_path} and
1339 \NT{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
1340
1341 \NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
1342 with $?$ and selecting the interesting parts with the placeholder
1343 $\%$.  \NT{wanted} is a term that lives in the context of the
1344 placeholders.
1345
1346 Textual patterns produced from a graphical selection are made of the
1347 \NT{sequent\_path} only. Such patterns can represent every selection,
1348 but are quite verbose. The \NT{wanted} part of the syntax is meant to
1349 help the users in writing concise and elegant patterns by hand.
1350
1351 \begin{table}
1352  \caption{Patterns concrete syntax\strut}
1353  \label{tab:pathsyn}
1354 \hrule
1355 \[
1356 \begin{array}{@{}rcll@{}}
1357   \NT{pattern} & 
1358     ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
1359   \NT{sequent\_path} & 
1360     ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
1361       [~\verb+\vdash+~\NT{multipath}~] & \\
1362   \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
1363   \NT{wanted} & ::= & \NT{term} & \\
1364 \end{array}
1365 \]
1366 \hrule
1367 \end{table}
1368
1369 \subsubsection{Pattern evaluation}
1370
1371 Patterns are evaluated in two phases. The first selects roots
1372 (subterms) of the sequent, using the $\NT{sequent\_path}$,  while the
1373 second searches the $\NT{wanted}$ term starting from these roots.
1374 % Both are optional steps, and by convention the empty pattern selects
1375 % the whole conclusion.
1376
1377 \begin{description}
1378 \item[Phase 1]
1379   concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
1380   part of the syntax. $\NT{ident}$ is an hypothesis name and
1381   selects the assumption where the following optional $\NT{multipath}$
1382   will operate. \verb+\vdash+ can be considered the name for the goal.
1383   If the whole pattern is omitted, the whole goal will be selected.
1384   If one or more hypotheses names are given the selection is restricted to 
1385   these assumptions. If a $\NT{multipath}$ is omitted the whole
1386   assumption is selected. Remember that the user can be mostly
1387   unaware of this syntax, since the system is able to write down a 
1388   $\NT{sequent\_path}$ starting from a visual selection.
1389   \NOTE{Questo ancora non va in matita}
1390
1391   A $\NT{multipath}$ is a CIC term in which a special constant $\%$
1392   is allowed.
1393   The roots of discharged subterms are marked with $?$, while $\%$
1394   is used to select roots. The default $\NT{multipath}$, the one that
1395   selects the whole term, is simply $\%$.
1396   Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
1397   that respectively select the first argument of an application or
1398   the source of an arrow and the head of the application that is
1399   found in the arrow target.
1400
1401   The first phase not only selects terms (roots of subterms) but
1402   determines also their context that will be eventually used in the
1403   second phase.
1404
1405 \item[Phase 2] 
1406   plays a role only if the $[~\verb+match+~\NT{wanted}~]$
1407   part is specified. From the first phase we have some terms, that we
1408   will see as subterm roots, and their context. For each of these
1409   contexts the $\NT{wanted}$ term is disambiguated in it and the
1410   corresponding root is searched for a subterm that can be unified to
1411   $\NT{wanted}$. The result of this search is the selection the
1412   pattern represents.
1413
1414 \end{description}
1415
1416 \subsubsection{Examples}
1417 %To explain how the first phase works let us give an example. Consider
1418 %you want to prove the uniqueness of the identity element $0$ for natural
1419 %sum, and that you can rely on the previously demonstrated left
1420 %injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
1421 %Typing
1422 %\begin{grafite}
1423 %theorem valid_name: \forall n,m. m + n = n \to m = O.
1424 %  intros (n m H).
1425 %\end{grafite}
1426
1427 Consider the following sequent 
1428 \sequent{
1429 n:nat\\
1430 m:nat\\
1431 H: m + n = n}{
1432 m=O
1433 }
1434
1435 To change the right part of the equivalence of the $H$
1436 hypothesis with $O + n$ the user selects and pastes it as the pattern
1437 in the following statement.
1438 \begin{grafite}
1439   change in H:(? ? ? %) with (O + n).
1440 \end{grafite}
1441
1442 To understand the pattern (or produce it by hand) the user should be
1443 aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
1444 that the pattern selects only the third argument of $eq$.
1445
1446 The experienced user may also write by hand a concise pattern
1447 to change at once all the occurrences of $n$ in the hypothesis $H$:
1448 \begin{grafite}
1449   change in H match n with (O + n).
1450 \end{grafite}
1451
1452 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
1453 the second phase locates $n$.
1454
1455 The latter pattern is equivalent to the following one, that the system
1456 can automatically generate from the selection.
1457 \begin{grafite}
1458   change in H:(? ? (? ? %) %) with (O + n).
1459 \end{grafite}
1460
1461 \subsubsection{Tactics supporting patterns}
1462
1463 \TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
1464
1465 \TODO{mergiare con il successivo facendo notare che i patterns sono una
1466 interfaccia comune per le tattiche}
1467
1468 In \MATITA{} all the tactics that can be restricted to subterm of the working
1469 sequent accept the pattern syntax. In particular these tactics are: simplify,
1470 change, fold, unfold, generalize, replace and rewrite.
1471
1472 \NOTE{attualmente rewrite e fold non supportano phase 2. per
1473 supportarlo bisogna far loro trasformare il pattern phase1+phase2 
1474 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
1475 con una pattern\_of(select(pattern))}
1476
1477 \subsubsection{Comparison with \COQ{}}
1478
1479 \COQ{} has two different ways of restricting the application of tactics to
1480 subterms of the sequent, both relaying on the same special syntax to identify
1481 a term occurrence.
1482
1483 The first way is to use this special syntax to tell the
1484 tactic what occurrences of a wanted term should be affected.
1485 The second is to prepare the sequent with another tactic called
1486 pattern and then apply the real tactic. Note that the choice is not
1487 left to the user, since some tactics needs the sequent to be prepared
1488 with pattern and do not accept directly this special syntax.
1489
1490 The base idea is that to identify a subterm of the sequent we can
1491 write it and say that we want, for example, the third and the fifth
1492 occurrences of it (counting from left to right). In our previous example,
1493 to change only the left part of the equivalence, the correct command
1494 is:
1495
1496 \begin{grafite}
1497   change n at 2 in H with (O + n)
1498 \end{grafite} 
1499
1500 meaning that in the hypothesis $H$ the $n$ we want to change is the
1501 second we encounter proceeding from left to right.
1502
1503 The tactic pattern computes a
1504 $\beta$-expansion of a part of the sequent with respect to some
1505 occurrences of the given term. In the previous example the following
1506 command:
1507 \begin{grafite}
1508   pattern n at 2 in H
1509 \end{grafite}
1510
1511 would have resulted in this sequent:
1512
1513 \begin{grafite}
1514   n : nat
1515   m : nat
1516   H : (fun n0 : nat => m + n = n0) n
1517   ============================
1518    m = 0
1519 \end{grafite}
1520
1521 where $H$ is $\beta$-expanded over the second $n$
1522 occurrence. 
1523
1524 At this point, since \COQ{} unification algorithm is essentially
1525 first-order, the application of an elimination principle (of the
1526 form $\forall P.\forall x.(H~x)\to (P~x)$) will unify 
1527 $x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
1528
1529 Since rewriting, replacing and several other tactics boils down to
1530 the application of the equality elimination principle, the previous
1531 trick deals the expected behaviour.
1532
1533 The idea behind this way of identifying subterms in not really far
1534 from the idea behind patterns, but fails in extending to
1535 complex notation, since it relays on a mono-dimensional sequent representation.
1536 Real math notation places arguments upside-down (like in indexed sums or
1537 integrations) or even puts them inside a bidimensional matrix.  
1538 In these cases using the mouse to select the wanted term is probably the 
1539 more effective way to tell the system what to do. 
1540
1541 One of the goals of \MATITA{} is to use modern publishing techniques, and
1542 adopting a method for restricting tactics application domain that discourages 
1543 using heavy math notation, would definitively be a bad choice.
1544
1545 \subsection{Tacticals}
1546 \label{sec:tinycals}
1547
1548 %There are mainly two kinds of languages used by proof assistants to recorder
1549 %proofs: tactic based and declarative. We will not investigate the philosophy
1550 %around the choice that many proof assistant made, \MATITA{} included, and we
1551 %will not compare the two different approaches. We will describe the common
1552 %issues of the tactic-based language approach and how \MATITA{} tries to solve
1553 %them.
1554
1555 The procedural proof language implemented in \MATITA{} is pretty standard,
1556 with a notable exception for tacticals.
1557
1558 %\subsubsection{Tacticals overview}
1559
1560 Tacticals first appeared in LCF as higher order tactics.  They can be
1561 seen as control flow constructs, like looping, branching, error
1562 recovery or sequential composition. 
1563
1564
1565 The following simple example
1566 shows a Coq script made of four dot-terminated commands
1567
1568 \begin{grafite}
1569 Theorem trivial: 
1570   forall A B:Prop,
1571     A = B -> ((A -> B) /\ (B -> A)).
1572   intros [A B H].
1573   split; intro; 
1574     [ rewrite < H; assumption
1575     | rewrite > H; assumption
1576     ].
1577 Qed.
1578 \end{grafite}
1579
1580 The third command is an application of the sequencing tactical
1581 ``$\ldots$\texttt{;}$\ldots$'', that combines the tactic
1582 \texttt{split} with the application of the branching tactical
1583 ``$\ldots$\texttt{;[}$\ldots$\texttt{|}$\ldots$\texttt{|}$\ldots$\texttt{]}''
1584 to other tactics and tacticals.
1585
1586 The usual implementation of tacticals executes them atomically as any
1587 other command. In \MATITA{} thi is not true since each punctuation is
1588 executed as a single command.
1589
1590 %The latter is applied to all the goals opened by \texttt{split}
1591 %
1592 %(here we have two goals, the two sides of the logic and).  The first
1593 %goal $B$ (with $A$ in the context) is proved by the first sequence of
1594 %tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the
1595 %second goal with the separator ``\texttt{|}''. 
1596 %
1597 %Giving serious examples here is rather difficult, since they are hard
1598 %to read without the interactive tool. To help the reader in
1599 %understanding the following considerations we just give few common
1600 %usage examples without a proof context.
1601 %
1602 %\begin{grafite}
1603 %  elim z; try assumption; [ ... | ... ].
1604 %  elim z; first [ assumption | reflexivity | id ].
1605 %\end{grafite}
1606 %
1607 %The first example goes by induction on a term \texttt{z} and applies
1608 %the tactic \texttt{assumption} to each opened goal eventually recovering if
1609 %\texttt{assumption} fails. Here we are asking the system to close all
1610 %trivial cases and then we branch on the remaining with ``\texttt{[}''.
1611 %The second example goes again by induction on \texttt{z} and tries to
1612 %close each opened goal first with \texttt{assumption}, if it fails it
1613 %tries \texttt{reflexivity} and finally \texttt{id}
1614 %that is the tactic that leaves the goal untouched without failing. 
1615 %
1616 %Note that in the common implementation of tacticals both lines are
1617 %compositions of tacticals and in particular they are a single
1618 %statement (i.e. derived from the same non terminal entry of the
1619 %grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
1620 %this is not true, since each atomic tactic or punctuation is considered 
1621 %a single statement.
1622
1623 \subsubsection{Common issues of tactic(als)-based proof languages}
1624 We will examine the two main problems of tactic(als)-based proof script:
1625 maintainability and readability. 
1626
1627 %Huge libraries of formal mathematics have been developed, and backward
1628 %compatibility is a really time consuming task. \\
1629 %A real-life example in the history of \MATITA{} was the reordering of
1630 %goals opened by a tactic application. We noticed that some tactics
1631 %were not opening goals in the expected order. In particular the
1632 %\texttt{elim} tactic on a term of an inductive type with constructors
1633 %$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
1634 %\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
1635 %but some theorems about integers were there. The inductive type of
1636 %$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
1637 %induction proofs on this type where written without tacticals and,
1638 %obviously, considering the three induction cases in the wrong order.
1639 %Fixing the behavior of the tactic broke the library and two days of
1640 %work were needed to make it compile again. The whole time was spent in
1641 %finding the list of tactics used to prove the third induction case and
1642 %swap it with the list of tactics used to prove the second case.  If
1643 %the proofs was structured with the branch tactical this task could
1644 %have been done automatically. 
1645 %
1646 %From this experience we learned that the use of tacticals for
1647 %structuring proofs gives some help but may have some drawbacks in
1648 %proof script readability. 
1649
1650 Tacticals are not only used to make scripts shorter by factoring out
1651 common cases and repeating commands. They are a primary way of making
1652 scripts more mainteable. Moreover, they also have the well-known
1653 role of structuring the proof.
1654
1655 However, authoring a proof structured with tacticals is annoying.
1656 Consider for example a proof by induction, and imagine you
1657 are using one of the state of the art graphical interfaces for proof assistant
1658 like Proof General. After applying the induction principle you have to choose:
1659 immediately structure the proof or postpone the structuring.
1660 If you decide for the former you have to apply the branching tactical and write
1661 at once tactics for all the cases. Since the user does not even know the
1662 generated goals yet, he can only replace all the cases with the identity
1663 tactic and execute the command, just to receive feedback on the first
1664 goal. Then he has to go one step back to replace the first identity
1665 tactic with the wanted one and repeat the process until all the
1666 branches are closed.
1667
1668 One could imagine that a structured script is simpler to understand.
1669 This is not the case.
1670 A proof script, being not declarative, is not meant to be read.
1671 However, the user has the need of explaining it to others.
1672 This is achieved by interactively re-playing the script to show each
1673 intermediate proof status. Tacticals make this operation uncomfortable.
1674 Indeed, a tactical is executed atomically, while it is obvious that it
1675 performs lot of smaller steps we are interested in.
1676 To show the intermediate steps, the proof must be de-structured on the
1677 fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where
1678 possible.\\
1679
1680 %Proof scripts
1681 %readability is poor by itself, but in conjunction with tacticals it
1682 %can be nearly impossible. The main cause is the fact that in proof
1683 %scripts there is no trace of what you are working on. It is not rare
1684 %for two different theorems to have the same proof script.\\
1685 %Bad readability is not a big deal for the user while he is
1686 %constructing the proof, but is considerably a problem when he tries to
1687 %reread what he did or when he shows his work to someone else.  The
1688 %workaround commonly used to read a script is to execute it again
1689 %step-by-step, so that you can see the proof goal changing and you can
1690 %follow the proof steps. This works fine until you reach a tactical.  A
1691 %compound statement, made by some basic tactics glued with tacticals,
1692 %is executed in a single step, while it obviously performs lot of proof
1693 %steps.  In the fist example of the previous section the whole branch
1694 %over the two goals (respectively the left and right part of the logic
1695 %and) result in a single step of execution. The workaround does not work
1696 %anymore unless you de-structure on the fly the proof, putting some
1697 %``\texttt{.}'' where you want the system to stop.\\
1698
1699 %Now we can understand the tradeoff between script readability and
1700 %proof structuring with tacticals. Using tacticals helps in maintaining
1701 %scripts, but makes it really hard to read them again, cause of the way
1702 %they are executed.
1703
1704 \MATITA{} has a peculiar tacticals implementation that provides the
1705 same benefits as classical tacticals, while not burdening the user
1706 during proof authoring and re-playing.
1707
1708 %\MATITA{} uses a language of tactics and tacticals, but tries to avoid
1709 %this tradeoff, alluring the user to write structured proof without
1710 %making it impossible to read them again.
1711
1712 \subsubsection{The \MATITA{} approach: Tinycals}
1713
1714 \begin{table}
1715  \caption{Concrete syntax of tacticals\strut}
1716  \label{tab:tacsyn}
1717 \hrule
1718 \[
1719 \begin{array}{@{}rcll@{}}
1720   \NT{punctuation} & 
1721     ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
1722   \NT{block\_kind} & 
1723     ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
1724   \NT{block\_delimiter} & 
1725     ::= & \verb+begin+ ~|~ \verb+end+ & \\
1726   \NT{tactical} & 
1727     ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
1728 \end{array}
1729 \]
1730 \hrule
1731 \end{table}
1732
1733 \MATITA{} tacticals syntax is reported in Tab.~\ref{tab:tacsyn}.
1734 While one would expect to find structured constructs like 
1735 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
1736 This is essential for the base idea behind \MATITA{} tacticals: step-by-step
1737 execution.
1738
1739 The low-level tacticals implementation of \MATITA{} allows a step-by-step
1740 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
1741 not executed as an atomic operation. This has major benefits for the
1742 user during proof structuring and re-playing.
1743
1744 For instance, reconsider the previous example of a proof by induction.
1745 With step-by-step tacticals the user can apply the induction principle, and just
1746 open the branching tactical ``\texttt{[}''. Then he can interact with the
1747 system until the proof of the first case is terminated. After that
1748 ``\texttt{|}'' is used to move to the next goal, until all goals are
1749 closed. After the last goal, the user closes the branching tactical with
1750 ``\texttt{]}'' and is done with a structured proof. \\
1751 While \MATITA{} tacticals help in structuring proofs they allow you to 
1752 choose the amount of structure you want. There are no constraints imposed by
1753 the system, and if the user wants he can even write completely plain proofs.
1754   
1755 Re-playing a proof is also made simpler. There is no longer any need
1756 to destructure the proof on the fly since \MATITA{} executes each
1757 tactical not atomically.
1758
1759 %\item[Rereading]
1760 %  is possible. Going on step by step shows exactly what is going on.  Consider
1761 %  again a proof by induction, that starts applying the induction principle and
1762 %  suddenly branches with a ``\texttt{[}''. This clearly separates all the
1763 %  induction cases, but if the square brackets content is executed in one single
1764 %  step you completely loose the possibility of rereading it and you have to
1765 %  temporary remove the branching tactical to execute in a satisfying way the
1766 %  branches.  Again, executing step-by-step is the way you would like to review
1767 %  the demonstration. Remember that understanding the proof from the script is
1768 %  not easy, and only the execution of tactics (and the resulting transformed
1769 %  goal) gives you the feeling of what is going on.
1770 %\end{description}
1771
1772 \section{Standard library}
1773 \label{sec:stdlib}
1774
1775 \MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
1776 can be read, checked and referenced in further developments. 
1777 However, in order to test the actual usability of the system, a
1778 new library of results has been started from scratch. In this case, 
1779 of course, we wrote (and offer) the source script files, 
1780 while, in the case of \COQ, \MATITA{} may only rely on XML files of
1781 \COQ{} objects. 
1782 The current library just comprises about one thousand theorems in 
1783 elementary aspects of arithmetics up to the multiplicative property for 
1784 Eulers' totient function $\phi$.
1785 The library is organized in five main directories: \texttt{logic} (connectives,
1786 quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type 
1787 constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
1788 (rationals). The most complex development is \texttt{nat}, organized in 25
1789 scripts, listed in Tab.~\ref{tab:scripts}.
1790
1791 \begin{table}[ht]
1792  \begin{tabular}{lll}
1793   \FILE{nat.ma}    & \FILE{plus.ma} & \FILE{times.ma}  \\
1794   \FILE{minus.ma}  & \FILE{exp.ma}  & \FILE{compare.ma} \\
1795   \FILE{orders.ma} & \FILE{le\_arith.ma} &  \FILE{lt\_arith.ma} \\   
1796   \FILE{factorial.ma} & \FILE{sigma\_and\_pi.ma} & \FILE{minimization.ma}  \\
1797   \FILE{div\_and\_mod.ma} & \FILE{gcd.ma} & \FILE{congruence.ma} \\
1798   \FILE{primes.ma} & \FILE{nth\_prime.ma} & \FILE{ord.ma} \\
1799   \FILE{count.ma}  & \FILE{relevant\_equations.ma} & \FILE{permutation.ma} \\ 
1800   \FILE{factorization.ma} & \FILE{chinese\_reminder.ma} &
1801   \FILE{fermat\_little\_th.ma} \\     
1802   \FILE{totient.ma} & & \\
1803  \end{tabular}
1804  \caption{Scripts on natural numbers in the standard library\strut}
1805  \label{tab:scripts}
1806 \end{table}
1807
1808 We do not plan to maintain the library in a centralized way, 
1809 as most of the systems do. On the contrary we are currently
1810 developing wiki-technologies to support a collaborative 
1811 development of the library, encouraging people to expand, 
1812 modify and elaborate previous contributions.
1813
1814 \section{Conclusions}
1815 \label{sec:conclusion}
1816
1817 \TODO{conclusioni}
1818
1819 \acknowledgements
1820 We would like to thank all the people that during the past
1821 7 years collaborated in the \HELM{} project and contributed to 
1822 the development of \MATITA{}, and in particular
1823 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
1824 and V.~Tamburrelli.
1825
1826 \theendnotes
1827
1828 \TODO{rivedere bibliografia, \'e un po' povera}
1829
1830 \TODO{aggiungere entry per le coercion implicite}
1831
1832 \bibliography{matita}
1833
1834 \end{document}