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