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