1 \documentclass[]{kluwer}
4 % \usepackage{amssymb,amsmath}
11 \definecolor{gray}{gray}{0.85}
12 %\newcommand{\logo}[3]{
13 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
16 \newcommand{\component}{component}
17 \newcommand{\components}{components}
19 \newcommand{\AUTO}{\textsc{Auto}}
20 \newcommand{\BOXML}{BoxML}
21 \newcommand{\COQ}{Coq}
22 \newcommand{\COQIDE}{CoqIde}
23 \newcommand{\ELIM}{\textsc{Elim}}
24 \newcommand{\GDOME}{Gdome}
25 \newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
26 \newcommand{\HELM}{Helm}
27 \newcommand{\HINT}{\textsc{Hint}}
28 \newcommand{\IN}{\ensuremath{\dN}}
29 \newcommand{\INSTANCE}{\textsc{Instance}}
30 \newcommand{\IR}{\ensuremath{\dR}}
31 \newcommand{\IZ}{\ensuremath{\dZ}}
32 \newcommand{\LIBXSLT}{LibXSLT}
33 \newcommand{\LOCATE}{\textsc{Locate}}
34 \newcommand{\MATCH}{\textsc{Match}}
35 \newcommand{\MATHML}{MathML}
36 \newcommand{\MATITA}{Matita}
37 \newcommand{\MATITAC}{\texttt{matitac}}
38 \newcommand{\MATITADEP}{\texttt{matitadep}}
39 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
40 \newcommand{\MOWGLI}{MoWGLI}
41 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
42 \newcommand{\NATIND}{\mathit{nat\_ind}}
43 \newcommand{\NUPRL}{NuPRL}
44 \newcommand{\OCAML}{OCaml}
45 \newcommand{\PROP}{\mathit{Prop}}
46 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
47 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
48 \newcommand{\UWOBO}{UWOBO}
49 \newcommand{\GETTER}{Getter}
50 \newcommand{\WHELP}{Whelp}
51 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
52 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
53 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
54 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
55 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
56 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
57 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
58 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
59 \newcommand{\SKIP}{\MATHTT{skip}}
60 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
62 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
63 \newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
64 \newcommand{\URI}[1]{\texttt{#1}}
65 \newcommand{\OP}[1]{``\texttt{#1}''}
66 \newcommand{\SCRIPT}[1]{\texttt{#1}}
68 \newenvironment{grafite}{\VerbatimEnvironment
69 \begin{SaveVerbatim}{boxtmp}}%
70 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
72 \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
76 \newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
78 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
79 \newcommand{\FILE}[1]{\texttt{#1}}
80 \newcommand{\NOTE}[1]{\ednote{#1}{}}
81 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
84 \newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
87 \newcommand{\sequent}[2]{
88 \savebox{\tmpxyz}[0.9\linewidth]{
89 \begin{minipage}{0.9\linewidth}
93 \end{minipage}}\setlength{\fboxsep}{3mm}%
95 \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
98 \bibliographystyle{plain}
104 \title{The \MATITA{} Proof Assistant}
106 \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
107 \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
108 \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
109 \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
110 \institute{Department of Computer Science, University of Bologna\\
111 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
113 \runningtitle{The \MATITA{} proof assistant}
114 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
119 ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
126 \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
131 % toc & co: to be removed in the final paper version
136 \section{Introduction}
138 \MATITA{} is the Proof Assistant under development by the \HELM{} team
139 \cite{mkm-helm} at the University of Bologna, under the direction of
141 The paper describes the overall architecture of
142 the system, focusing on its most distinctive and innovative
145 \subsection{Historical Perspective}
146 The origins of \MATITA{} go back to 1999. At the time we were mostly
147 interested to develop tools and techniques to enhance the accessibility
148 via Web of formal libraries of mathematics. Due to its dimension, the
149 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
150 was chosen as a privileged test bench for our work, although experiments
151 have been also conducted with other systems, and notably
152 with \NUPRL~\cite{nuprl-book}.
153 The work, mostly performed in the framework of the recently concluded
154 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
157 \item exporting the information from the internal representation of
158 \COQ{} to a system and platform independent format. Since XML was at the
159 time an emerging standard, we naturally adopted this technology, fostering
160 a content-centric architecture\cite{content-centric} where the documents
161 of the library were the the main components around which everything else
163 \item developing indexing and searching techniques supporting semantic
164 queries to the library;
165 \item developing languages and tools for a high-quality notational
166 rendering of mathematical information\footnote{We have been
167 active in the \MATHML{} Working group since 1999.};
170 According to our content-centric commitment, the library exported from
171 \COQ{} was conceived as being distributed and most of the tools were developed
172 as Web services. The user could interact with the library and the tools by
173 means of a Web interface that orchestrates the Web services.
175 The Web services and the other tools have been implemented as front-ends
176 to a set of software components, collectively called the \HELM{} components.
177 At the end of the \MOWGLI{} project we already disposed of the following
178 tools and software components:
180 \item XML specifications for the Calculus of Inductive Constructions,
181 with components for parsing and saving mathematical objects in such a format
182 \cite{exportation-module};
183 \item metadata specifications with components for indexing and querying the
185 \item a proof checker library (i.e. the {\em kernel} of a proof assistant),
186 implemented to check that we exported from the \COQ{} library all the
187 logically relevant content;
188 \item a sophisticated parser (used by the search engine), able to deal
189 with potentially ambiguous and incomplete information, typical of the
190 mathematical notation \cite{disambiguation};
191 \item a {\em refiner} library, i.e. a type inference system, based on
192 partially specified terms, used by the disambiguating parser;
193 \item complex transformation algorithms for proof rendering in natural
194 language \cite{remathematization};
195 \item an innovative, \MATHML-compliant rendering widget for the GTK
196 graphical environment\cite{padovani}, supporting
197 high-quality bidimensional
198 rendering, and semantic selection, i.e. the possibility to select semantically
199 meaningful rendering expressions, and to paste the respective content into
200 a different text area.
202 Starting from all this, developing our own proof assistant was not
203 too far away: essentially, we ``just'' had to
204 add an authoring interface, and a set of functionalities for the
205 overall management of the library, integrating everything into a
206 single system. \MATITA{} is the result of this effort.
208 \subsection{The system}
210 \MATITA{} is a proof assistant (also called interactive theorem prover).
211 It is based on the Calculus of (Co)Inductive Constructions
212 (CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
213 Church enriched with primitive inductive and co-inductive data types.
214 Via the Curry-Howard isomorphism, the calculus can be seen as a very
215 rich higher order logic and proofs can be simply represented and
216 stored as lambda-terms. \COQ{} and Lego are other systems that adopt
217 (variations of) CIC as their foundation.
219 The proof language of \MATITA{} is procedural, in the tradition of the LCF
220 theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
221 whose proof language is procedural. Traditionally, in a procedural system
222 the user interacts only with the \emph{script}, while proof terms are internal
223 records kept by the system. On the contrary, in \MATITA{} proof terms are
224 praised as declarative versions of the proof. With this role, they are the
225 primary mean of communication of proofs (once rendered to natural language
226 for human audiences).
228 The user interfaces now adopted by all the proof assistants based on a
229 procedural proof language have been inspired by the CtCoq pioneering
230 system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
231 by CtCoq is the Proof General generic interface~\cite{proofgeneral},
232 that has set a sort of
233 standard way to interact with the system. Several procedural proof assistants
234 have either adopted or cloned Proof General as their main user interface.
235 The authoring interface of \MATITA{} is a clone of the Proof General interface.
238 \item scelta del sistema fondazional.
239 \item sistema indipendente (da \COQ)
240 \item compatibilit\`a con sistemi legacy
243 \subsection{Relationship with \COQ{}}
245 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
246 more the effect of the circumstances of its creation described
247 above than the result of a deliberate design. In particular, we
248 (essentially) share the same foundational dialect of \COQ{} (the
249 Calculus of (Co)Inductive Constructions), the same implementation
250 language (\OCAML{}), and the same (script based) authoring philosophy.
251 However, the analogy essentially stops here and no code is shared by the
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 sensible way).
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.
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.
270 The size and complexity improvements over \COQ{} must be understood
271 historically. \COQ{} is a quite old
272 system whose development started 15\NOTE{Verificare} years ago. Since then
273 several developers have took over the code and several new research ideas
274 that were not considered in the original architecture have been experimented
275 and integrated in the system. Moreover, there exists a lot of developments
276 for \COQ{} that require backward compatibility between each pair of releases;
277 since many central functionalities of a proof assistant are based on heuristics
278 or arbitrary choices to overcome undecidability (e.g. for higher order
279 unification), changing these functionalities maintaining backward compatibility
280 is very difficult. Finally, the code of \COQ{} has been greatly optimized
281 over the years; optimization reduces maintainability and rises the complexity
284 In writing \MATITA{} we have not been hindered by backward compatibility and
285 we have took advantage of the research results and experiences previously
286 developed by others, comprising the authors of \COQ. Moreover, starting from
287 scratch, we have designed in advance the architecture and we have split
288 the code in coherent minimally coupled components.
290 In the future we plan to exploit \MATITA{} as a test bench for new ideas and
291 extensions. Keeping the single components and the whole architecture as
292 simple as possible is thus crucial to foster future experiments and to
293 allow other developers to quickly understand our code and contribute.
295 %For direct experience of the authors, the learning curve to understand and
296 %be able to contribute to \COQ{}'s code is quite steep and requires direct
297 %and frequent interactions with \COQ{} developers.
299 \section{Architecture}
304 \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
305 \caption[\MATITA{} components and related applications]{\MATITA{}
306 components and related applications, with thousands of line of
308 \label{fig:libraries}
312 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
313 (circle nodes) and \emph{applications} (squared nodes) developed in the HELM
314 project. Each node is annotated with the number of lines of source code
315 (comprising comments).
317 Applications and \components{} depend over other \components{} forming a
318 directed acyclic graph (DAG). Each \component{} can be decomposed in
319 a a set of \emph{modules} also forming a DAG.
321 Modules and \components{} provide coherent sets of functionalities
322 at different scales. Applications that require only a few functionalities
323 depend on a restricted set of \components{}.
325 Only the proof assistant \MATITA{} and the \WHELP{} search engine are
326 applications meant to be used directly by the user. All the other applications
327 are Web services developed in the HELM and MoWGLI projects and already described
328 elsewhere. In particular:
330 \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
331 from a physical location (URL) given its logical name (URI). The Getter is
332 responsible of updating a table that maps URIs to URLs. Thanks to the Getter
333 it is possible to work on a logically monolithic library that is physically
334 distributed on the network. More information on the Getter can be found
335 in~\cite{zack-master}.
336 \item \emph{\WHELP} is a search engine to index and locate mathematical
337 notions (axioms, theorems, definitions) in the logical library managed
338 by the Getter. Typical examples of a query to Whelp are queries that search
339 for a theorem that generalize or instantiate a given formula, or that
340 can be immediately applied to prove a given goal. The output of Whelp is
341 an XML document that lists the URIs of a complete set of candidates that
342 are likely to satisfy the given query. The set is complete in the sense
343 that no notion that actually satisfies the query is thrown away. However,
344 the query is only approximated in the sense that false matches can be
345 returned. Whelp has been described in~\cite{whelp}.
346 \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
347 notion in the distributed library, renders it according to the user provided
348 two dimensional mathematical notation. \UWOBO{} may also embed the rendering
349 of mathematical notions into arbitrary documents before returning them.
350 The Getter is used by \UWOBO{} to retrieve the document to be rendered.
351 \UWOBO{} has been described in~\cite{zack-master}.
352 \item The \emph{Proof Checker} is a Web service that, given the URI of
353 notion in the distributed library, checks its correctness. Since the notion
354 is likely to depend in an acyclic way over other notions, the proof checker
355 is also responsible of building in a top-down way the DAG of all
356 dependencies, checking in turn every notion for correctness.
357 The proof checker has been described in~\cite{zack-master}.
358 \item The \emph{Dependency Analyzer} is a Web service that can produce
359 a textual or graphical representation of the dependencies of an object.
360 The dependency analyzer has been described in~\cite{zack-master}.
363 The dependency of a \component{} or application over another \component{} can
364 be satisfied by linking the \component{} in the same executable.
365 For those \components{} whose functionalities are also provided by the
366 aforementioned Web services, it is also possible to link stub code that
367 forwards the request to a remote Web service. For instance, the Getter
368 is just a wrapper to the \GETTER{} \component{} that allows the
369 \component{} to be used as a Web service. \MATITA{} can directly link the code
370 of the \GETTER{} \component, or it can use a stub library with the same
371 API that forwards every request to the Getter.
373 To better understand the architecture of \MATITA{} and the role of each
374 \component, we can focus on the representation of the mathematical information.
375 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
376 Constructions (CIC). In CIC terms are used to represent mathematical
377 formulae, types and proofs. \MATITA{} is able to handle terms at
378 four different levels of specification. On each level it is possible to provide
379 a different set of functionalities. The four different levels are:
380 fully specified terms; partially specified terms;
381 content level terms; presentation level terms.
383 \subsection{Fully specified terms}
384 \label{sec:fullyspec}
386 \emph{Fully specified terms} are CIC terms where no information is
387 missing or left implicit. A fully specified term should be well-typed.
388 The mathematical notions (axioms, definitions, theorems) that are stored
389 in our mathematical library are fully specified and well-typed terms.
390 Fully specified terms are extremely verbose (to make type-checking
391 decidable). Their syntax is fixed and does not resemble the usual
392 extendible mathematical notation. They are not meant for direct user
395 The \texttt{cic} \component{} defines the data type that represents CIC terms
396 and provides a parser for terms stored in an XML format.
398 The most important \component{} that deals with fully specified terms is
399 \texttt{cic\_proof\_checking}. It implements the procedure that verifies
400 if a fully specified term is well-typed. It also implements the
401 \emph{conversion} judgement that verifies if two given terms are
402 computationally equivalent (i.e. they share the same normal form).
404 Terms may reference other mathematical notions in the library.
405 One commitment of our project is that the library should be physically
406 distributed. The \GETTER{} \component{} manages the distribution,
407 providing a mapping from logical names (URIs) to the physical location
408 of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
409 data type and several utility functions over URIs. The
410 \texttt{cic\_proof\_checking} \component{} calls the \GETTER
411 \component{} every time it needs to retrieve the definition of a mathematical
412 notion referenced by a term that is being type-checked.
414 The Proof Checker is the Web service that provides an interface
415 to the \texttt{cic\_proof\_checking} \component.
417 We use metadata and a sort of crawler to index the mathematical notions
418 in the distributed library. We are interested in retrieving a notion
419 by matching, instantiation or generalization of a user or system provided
420 mathematical formula. Thus we need to collect metadata over the fully
421 specified terms and to store the metadata in some kind of (relational)
422 database for later usage. The \texttt{hmysql} \component{} provides
424 interface to a (possibly remote) MySql database system used to store the
425 metadata. The \texttt{metadata} \component{} defines the data type of the
427 we are collecting and the functions that extracts the metadata from the
428 mathematical notions (the main functionality of the crawler).
429 The \texttt{whelp} \component{} implements a search engine that performs
430 approximated queries by matching/instantiation/generalization. The queries
431 operate only on the metadata and do not involve any actual matching
432 (that will be described later on and that is implemented in the
433 \texttt{cic\_unification} \component). Not performing any actual matching
434 the query only returns a complete and hopefully small set of matching
435 candidates. The process that has issued the query is responsible of
436 actually retrieving from the distributed library the candidates to prune
437 out false matches if interested in doing so.
439 The Whelp search engine is the Web service that provides an interface to
440 the \texttt{whelp} \component.
442 According to our vision, the library is developed collaboratively so that
443 changing or removing a notion can invalidate other notions in the library.
444 Moreover, changing or removing a notion requires a corresponding change
445 in the metadata database. The \texttt{library} \component{} is responsible
446 of preserving the coherence of the library and the database. For instance,
447 when a notion is removed, all the notions that depend on it and their
448 metadata are removed from the library. This aspect will be better detailed
449 in Sect.~\ref{sec:libmanagement}.
451 \subsection{Partially specified terms}
454 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
455 Omitted subterms can bear no information at all or they may be associated to
456 a sequent. The formers are called \emph{implicit terms} and they occur only
457 linearly. The latters may occur multiple times and are called
458 \emph{metavariables}. An \emph{explicit substitution} is applied to each
459 occurrence of a metavariable. A metavariable stand for a term whose type is
460 given by the conclusion of the sequent. The term must be closed in the
461 context that is given by the ordered list of hypotheses of the sequent.
462 The explicit substitution instantiates every hypothesis with an actual
463 value for the variable bound by the hypothesis.
465 Partially specified terms are not required to be well-typed. However a
466 partially specified term should be \emph{refinable}. A \emph{refiner} is
467 a type-inference procedure that can instantiate implicit terms and
468 metavariables and that can introduce \emph{implicit coercions} to make a
469 partially specified term well-typed. The refiner of \MATITA{} is implemented
470 in the \texttt{cic\_unification} \component. As the type checker is based on
471 the conversion check, the refiner is based on \emph{unification} that is
472 a procedure that makes two partially specified term convertible by instantiating
473 as few as possible metavariables that occur in them.
475 Since terms are used in CIC to represent proofs, correct incomplete
476 proofs are represented by refinable partially specified terms. The metavariables
477 that occur in the proof correspond to the conjectures still to be proved.
478 The sequent associated to the metavariable is the conjecture the user needs to
481 \emph{Tactics} are the procedures that the user can apply to progress in the
482 proof. A tactic proves a conjecture possibly creating new (and hopefully
483 simpler) conjectures. The implementation of tactics is given in the
484 \texttt{tactics} \component. It is heavily based on the refinement and
485 unification procedures of the \texttt{cic\_unification} \component.
487 The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
488 commands of the \MATITA{} proof assistant. Most of the commands are tactics.
489 Other commands are used to give definitions and axioms or to state theorems
490 and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
491 It implements the semantics of each command in the grafite AST as a function
492 from status to status. It implements also an undo function to go back to
495 As fully specified terms, partially specified terms are not well suited
496 for user consumption since their syntax is not extendible and it is not
497 possible to adopt the usual mathematical notation. However they are already
498 an improvement over fully specified terms since they allow to omit redundant
499 information that can be inferred by the refiner.
501 \subsection{Content level terms}
502 \label{sec:contentintro}
504 The language used to communicate proofs and especially formulae with the
505 user does not only needs to be extendible and accommodate the usual mathematical
506 notation. It must also reflect the comfortable degree of imprecision and
507 ambiguity that the mathematical language provides.
509 For instance, it is common practice in mathematics to speak of a generic
510 equality that can be used to compare any two terms. However, it is well known
511 that several equalities can be distinguished as soon as we care for decidability
512 or for their computational properties. For instance equality over real
513 numbers is well known to be undecidable, whereas it is decidable over
516 Similarly, we usually speak of natural numbers and their operations and
517 properties without caring about their representation. However the computational
518 properties of addition over the binary representation are very different from
519 those of addition over the unary representation. And addition over two natural
520 numbers is definitely different from addition over two real numbers.
522 Formal mathematics cannot hide these differences and obliges the user to be
523 very precise on the types he is using and their representation. However,
524 to communicate formulae with the user and with external tools, it seems good
525 practice to stick to the usual imprecise mathematical ontology. In the
526 Mathematical Knowledge Management community this imprecise language is called
527 the \emph{content level} representation of formulae.
529 In \MATITA{} we provide two translations: from partially specified terms
530 to content level terms and the other way around. The first translation can also
531 be applied to fully specified terms since a fully specified term is a special
532 case of partially specified term where no metavariable or implicit term occurs.
534 The translation from partially specified terms to content level terms must
535 discriminate between terms used to represent proofs and terms used to represent
536 formulae. The firsts are translated to a content level representation of
537 proof steps that can easily be rendered in natural language. The representation
538 adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
539 isomorphic to it. Terms that represent formulae are translated to \MATHML{}
540 Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
541 for the representation of content level formulae in an XML extensible format.
543 The translation to content level is implemented in the
544 \texttt{acic\_content} \component. Its input are \emph{annotated partially
545 specified terms}, that are maximally unshared
546 partially specified terms enriched with additional typing information for each
547 subterm. This information is used to discriminate between terms that represent
548 proofs and terms that represent formulae. Part of it is also stored at the
549 content level since it is required to generate the natural language rendering
550 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
551 and not a DAG). The reason is that to the occurrences of a subterm in
552 two different positions we need to associate different typing informations.
553 This association is made easier when the term is represented as a tree since
554 it is possible to label each node with an unique identifier and associate
555 the typing information using a map on the identifiers.
556 The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
557 by the \texttt{library} \component{} since fully specified terms are stored
558 in the library in their annotated form.
560 We do not provide yet a reverse translation from content level proofs to
561 partially specified terms. But in \texttt{cic\_disambiguation} we do provide
562 the reverse translation for formulae. The mapping from
563 content level formulae to partially specified terms is not unique due to
564 the ambiguity of the content level. As a consequence the translation
565 is guided by an \emph{interpretation}, that is a function that chooses for
566 every ambiguous formula one partially specified term. The
567 \texttt{cic\_disambiguation} \component{} implements the
568 disambiguation algorithm we presented in~\cite{disambiguation} that is
569 responsible of building in an efficient way the set of all ``correct''
570 interpretations. An interpretation is correct if the partially specified term
571 obtained using the interpretation is refinable.
573 In Sect.~\ref{sec:partspec} the last section we described the semantics of a
575 function from status to status. We also suggested that the formulae in a
576 command are encoded as partially specified terms. However, consider the
577 command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
578 of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
579 replace $x$ in that context, its encoding as a term cannot be computed
580 until $x$ is located. In other words, $y^2$ must be disambiguated in the
581 context of the occurrence $x$ it must replace.
583 The elegant solution we have implemented consists in representing terms
584 in a command as functions from a context to a partially refined term. The
585 function is obtained by partially applying our disambiguation function to
586 the content term to be disambiguated. Our solution should be compared with
587 the one adopted in the Coq system, where ambiguity is only relative to De Brujin
588 indexes. In Coq variables can be bound either by name or by position. A term
589 occurring in a command has all its variables bound by name to avoid the need of
590 a context during disambiguation. Moreover, this makes more complex every
591 operation over terms (i.e. according to our architecture every module that
592 depends on \texttt{cic}) since the code must deal consistently with both kinds
593 of binding. Also, this solution cannot cope with other forms of ambiguity (as
594 the context dependent meaning of the exponent in the previous example).
596 \subsection{Presentation level terms}
598 Content level terms are a sort of abstract syntax trees for mathematical
599 formulae and proofs. The concrete syntax given to these abstract trees
600 is called \emph{presentation level}.
602 The main important difference between the content level language and the
603 presentation level language is that only the former is extendible. Indeed,
604 the presentation level language is a finite language that comprises all
605 the usual mathematical symbols. Mathematicians invent new notions every
606 single day, but they stick to a set of symbols that is more or less fixed.
608 The fact that the presentation language is finite allows the definition of
609 standard languages. In particular, for formulae we have adopt \MATHML{}
610 Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
612 represent proofs it is enough to embed formulae in plain text enriched with
613 formatting boxes. Since the language of formatting boxes is very simple,
614 many equivalent specifications exist and we have adopted our own, called
617 The \texttt{content\_pres} \component{} contains the implementation of the
618 translation from content level terms to presentation level terms. The
619 rendering of presentation level terms is left to the application that uses
620 the \component. However, in the \texttt{hgdome} \component{} we provide a few
621 utility functions to build a \GDOME~\cite{gdome2} \MATHML+\BOXML{} tree from our
623 level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
625 widget developed by Luca Padovani \cite{padovani}. The widget is
626 particularly interesting since it allows to implement \emph{semantic
629 Semantic selection is a technique that consists in enriching the presentation
630 level terms with pointers to the content level terms and to the partially
631 specified terms they correspond to. Highlight of formulae in the widget is
632 constrained to selection of meaningful expressions, i.e. expressions that
633 correspond to a lower level term, that is a content term or a partially or
634 fully specified term.
635 Once the rendering of a lower level term is
636 selected it is possible for the application to retrieve the pointer to the
637 lower level term. An example of applications of semantic selection is
638 \emph{semantic cut\&paste}: the user can select an expression and paste it
639 elsewhere preserving its semantics (i.e. the partially specified term),
640 possibly performing some semantic transformation over it (e.g. renaming
641 variables that would be captured or lambda-lifting free variables).
643 The reverse translation from presentation level terms to content level terms
644 is implemented by a parser that is also found in \texttt{content\_pres}.
645 Differently from the translation from content level terms to partially
646 refined terms, this translation is not ambiguous. The reason is that the
647 parsing tool we have adopted (CamlP4) is not able to parse ambiguous
648 grammars. Thus we require the mapping from presentation level terms
649 (concrete syntax) to content level terms (abstract syntax) to be unique.
650 This means that the user must fix once and for all the associativity and
651 precedence level of every operator he is using. In practice this limitation
652 does not seem too strong. The reason is that the target of the
653 translation is an ambiguous language and the user is free to associate
654 to every content level term several different interpretations (as a
655 partially specified term).
657 Both the direct and reverse translation from presentation to content level
658 terms are parameterized over the user provided mathematical notation.
659 The \texttt{lexicon} \component{} is responsible of managing the lexicon,
660 that is the set of active notations. It defines an abstract syntax tree
661 of commands to declare and activate new notations and it implements the
662 semantics of these commands. It also implements undoing of the semantic
663 actions. Among the commands there are hints to the
664 disambiguation algorithm that are used to control and speed up disambiguation.
665 These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
667 Finally, the \texttt{grafite\_parser} \component{} implements a parser for
668 the concrete syntax of the commands of \MATITA. The parser process a stream
669 of characters and returns a stream of abstract syntax trees (the ones
670 defined by the \texttt{grafite} component and whose semantics is given
671 by \texttt{grafite\_engine}). When the parser meets a command that changes
672 the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
673 process the command. When the parser needs to parse a term at the presentation
674 level, it invokes the already described parser for terms contained in
675 \texttt{content\_pres}.
677 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
678 against the \texttt{grafite\_parser} \components{}
679 since they provide an interface to the user. In both cases the formulae
680 written by the user are parsed using the \texttt{content\_pres} \component{} and
681 then disambiguated using the \texttt{cic\_disambiguation} \component. However,
682 only \MATITA{} is linked against the \texttt{grafite\_engine} and
683 \texttt{tactics} components (summing up to a total of 11'200 lines of code)
684 since \WHELP{} can only execute those ASTs that correspond to queries
685 (implemented in the \texttt{whelp} component).
687 The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
688 providing a rendering service for the documents in the distributed library.
689 To render a document given its URI, \UWOBO{} retrieves it using the
690 \GETTER{} obtaining a document with fully specified terms. Then it translates
691 it to the presentation level passing through the content level. Finally
692 it returns the result document to be rendered by the user's
693 browser.\footnote{\TODO{manca la passata verso HTML}}
696 The \components{} not yet described (\texttt{extlib}, \texttt{xml},
697 \texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
698 minor \components{} that provide a core of useful functions and basic
699 services missing from the standard library of the programming language.
700 %In particular, the \texttt{xml} \component{} is used to easily represent,
701 %parse and pretty-print XML files.
704 \section{The interface to the library}
707 A proof assistant provides both an interface to interact with its library and
708 an \emph{authoring} interface to develop new proofs and theories. According
709 to its historical origins, \MATITA{} strives to provide innovative
710 functionalities for the interaction with the library. It is more traditional
711 in its script based authoring interface.
713 In the remaining part of the paper we focus on the user view of \MATITA{}.
714 This section is devoted to the aspects of the tool that arise from the
715 document centric approach to the library. Sect.~\ref{sec:authoring} describes
716 the peculiarities of the authoring interface.
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 However, once they are produced we store them independently in the library.
722 The only relation implicitly kept between the notions are the logical,
723 acyclic dependencies among them. This way the library forms a global (and
724 distributed) hypertext. Several useful operations can be implemented on the
725 library only, regardless of the scripts. Examples of such operations
726 implemented in \MATITA{} are: searching and browsing (see Sect.~\ref{sec:indexing});
727 disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
728 automatic proof searching (see Sect.~\ref{sec:automation}).
730 The key requisite for the previous operations is that the library must
731 be fully accessible and in a logically consistent state. To preserve
732 consistency, a concept cannot be altered or removed unless the part of the
733 library that depends on it is modified accordingly. To allow incremental
734 changes and cooperative development, consistent revisions are necessary.
735 For instance, to modify a definition, the user could fork a new version
736 of the library where the definition is updated and all the concepts that
737 used to rely on it are absent. The user is then responsible to restore
738 the removed part in the new branch, merging the branch when the library is
741 To implement the proposed versioning system on top of a standard one
742 it is necessary to implement \emph{invalidation} first. Invalidation
743 is the operation that locates and removes from the library all the concepts
744 that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
745 a concept from the library also involves deleting its metadata from the
748 For non collaborative development, full versioning can be avoided, but
749 invalidation is still required. Since nobody else is relying on the
750 user development, the user is free to change and invalidate part of the library
751 without branching. Invalidation is still necessary to avoid using a
752 concept that is no longer valid.
753 So far, in \MATITA{} we address only this non collaborative scenario
754 (see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
755 is still under design.
757 Scripts are not seen as constituents of the library. They are not published
758 and indexed, so they cannot be searched or browsed using \HELM{} tools.
759 However, they play a central role for the maintenance of the library.
760 Indeed, once a notion is invalidated, the only way to restore it is to
761 fix the possibly broken script that used to generate it.
762 Moreover, during the authoring phase, scripts are a natural way to
763 group notions together. They also constitute a less fine grained clustering
764 of notions for invalidation.
766 In the rest of this section we present in more details the functionalities of
767 \MATITA{} related to library management and exploitation.
768 Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
769 the \MATITA{} authoring interface.
771 \subsection{Indexing and searching}
774 \subsection{Disambiguation}
775 \label{sec:disambiguation}
777 Software applications that involve input of mathematical content should strive
778 to require the user as less drift from informal mathematics as possible. We
779 believe this to be a fundamental aspect of such applications user interfaces.
780 Being that drift in general very large when inputing
781 proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
782 mathematical formulae which can be input using a \TeX-like encoding (the
783 concrete syntax corresponding to presentation level terms) and are then
784 translated (in multiple steps) to partially specified terms as sketched in
785 Sect.~\ref{sec:contentintro}.
787 The key component of the translation is the generic disambiguation algorithm
788 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
789 and presented in~\cite{disambiguation}. In this section we present how to use
790 such an algorithm in the context of the development of a library of formalized
791 mathematics. We will see that using multiple passes of the algorithm, varying
792 some of its parameters, helps in keeping the input terse without sacrificing
795 \subsubsection{Disambiguation aliases}
796 \label{sec:disambaliases}
797 Let us start with the definition of the ``strictly greater then'' notion over
798 (Peano) natural numbers.
801 include "nat/nat.ma".
803 definition gt: nat \to nat \to Prop \def
807 The \texttt{include} statement adds the requirement that the part of the library
808 defining the notion of natural numbers should be defined before
809 processing what follows. Note indeed that the algorithm presented
810 in~\cite{disambiguation} does not describe where interpretations for ambiguous
811 expressions come from, since it is application-specific. As a first
812 approximation, we will assume that in \MATITA{} they come from the library (i.e.
813 all interpretations available in the library are used) and the \texttt{include}
814 statements are used to ensure the availability of required library slices (see
815 Sect.~\ref{sec:libmanagement}).
817 While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
818 terms: its type and its body. Being available in the required library only one
819 interpretation both for the unbound identifier \texttt{nat} and for the
820 \OP{<} operator, and being the resulting partially specified term refinable,
821 both type and body are easily disambiguated.
823 Now suppose we have defined integers as signed natural numbers, and that we want
824 to prove a theorem about an order relationship already defined on them (which of
825 course overload the \OP{<} operator):
831 \forall x, y, z. x < y \to y < z \to x < z.
834 Since integers are defined on top of natural numbers, the part of the library
835 concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
836 type. Thus, according to the disambiguation algorithm, two different partially
837 specified terms could be associated to it. At first, this might not be seen as a
838 problem, since the user is asked and can choose interactively which of the two
839 she had in mind. However in the long run it has the drawbacks of inhibiting
840 batch compilation of the library (a technique used in \MATITA{} for behind the
841 scene compilation when needed, e.g. when an \texttt{include} is issued) and
842 yields to poor user interaction (imagine how tedious would be to be asked for a
843 choice each time you re-evaluate \texttt{Zlt\_compat}!).
845 For this reason we added to \MATITA{} the concept of \emph{disambiguation
846 aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
847 expressions to partially specified terms, which are part of the runtime status
848 of \MATITA. They can be provided by users with the \texttt{alias} statement, but
849 are usually automatically added when evaluating \texttt{include} statements
850 (\emph{implicit aliases}). Aliases implicitly inferred during disambiguation
851 are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
852 which require interactive choice are saved in batch compilable format. Thus,
853 after evaluating the above theorem the script will be changed to the following
854 snippet (assuming that the interpretation of \OP{<} over integers has been
858 alias symbol "lt" = "integer 'less than'".
860 \forall x, y, z. x < y \to y < z \to x < z.
863 But how are disambiguation aliases used? Since they come from the parts of the
864 library explicitly included we may be tempted of using them as the only
865 available interpretations. This would speed up the disambiguation, but may fail.
866 Consider for example:
869 theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
872 and suppose that the \OP{+} operator is defined only on natural numbers. If
873 the alias for \OP{<} points to the integer version of the operator, no
874 refinable partially specified term matching the term could be found.
876 For this reason we chose to attempt \emph{multiple disambiguation passes}. A
877 first pass attempts to disambiguate using the last available disambiguation
878 aliases (\emph{mono aliases} pass); in case of failure the next pass tries
879 disambiguation again forgetting the aliases and using the whole library to
880 retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
881 Since the latter pass may lead to too many choices we intertwined an additional
882 pass among the two which use as interpretations all the aliases coming for
883 included parts of the library (\emph{multi aliases} phase). This is the reason
884 why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
885 turned out to be a well-balanced trade-off among performances (earlier passes
886 fail quickly) and degree of ambiguity supported for presentation level terms.
888 \subsubsection{Operator instances}
890 Let us suppose now we want to define a theorem relating ordering relations on
891 natural and integer numbers. The way we would like to write such a theorem (as
892 we can read it in the \MATITA{} standard library) is:
896 include "nat/orders.ma".
898 theorem lt_to_Zlt_pos_pos:
899 \forall n, m: nat. n < m \to pos n < pos m.
902 Unfortunately, none of the passes described above is able to disambiguate its
903 type, no matter how aliases are defined. This is because the \OP{<} operator
904 occurs twice in the content level term (it has two \emph{instances}) and two
905 different interpretations for it have to be used in order to obtain a refinable
906 partially specified term. To address this issue, we have the ability to consider
907 each instance of a single symbol as a different ambiguous expression in the
908 content level term, and thus we can assign a different interpretation to each of
909 them. A disambiguation pass which exploit this feature is said to be using
910 \emph{fresh instances}.
912 Fresh instances lead to a non negligible performance loss (since the choice of
913 an interpretation for one instances does not constraint the choice for the
914 others). For this reason we always attempt a fresh instances pass only after
915 attempting a non-fresh one.
917 \paragraph{One-shot aliases} Disambiguation aliases as seen so far are
918 instance-independent. However, aliases obtained as a result of a disambiguation
919 pass which uses fresh instances ought to be instance-dependent, that is: to
920 ensure a term can be disambiguated in a batch fashion we may need to state that
921 an \emph{i}-th instance of a symbol should be mapped to a given partially
922 specified term. Instance-depend aliases are meaningful only for the term whose
923 disambiguation generated it. For this reason we call them \emph{one-shot
924 aliases} and \MATITA{} does not use it to disambiguate further terms down in the
927 \subsubsection{Implicit coercions}
929 Let us now consider a theorem about derivation:
933 \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
936 and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
937 interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
938 Mathematicians would write the term that way since it is well known that the
939 natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
940 number for the purpose of real multiplication. The refiner of \MATITA{} supports
941 \emph{implicit coercions} for this reason: given as input the above content
942 level term, it will return a partially specified term where in place of
943 \texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
944 (assuming it has been defined as such of course).
946 Nonetheless coercions are not always desirable. For example, in disambiguating
947 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
948 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
949 among the possible partially specified term choices. For this reason in
950 \MATITA{} we always try first a disambiguation pass which require the refiner
951 not to use the coercions and only in case of failure we attempt a
952 coercion-enabled pass.
954 It is interesting to observe also the relationship among operator instances and
955 implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
956 which \MATITA{} disambiguated using fresh instances. In case there exists a
957 coercion from natural numbers to (positive) integers (which indeed does, it is
958 the \texttt{pos} constructor itself), the theorem can be disambiguated using
959 twice that coercion on the left hand side of the implication. The obtained
960 partially specified term however would not probably be the expected one, being a
961 theorem which prove a trivial implication. For this reason we choose to always
962 prefer fresh instances over implicit coercions, i.e. we always attempt
963 disambiguation passes with fresh instances and no implicit coercions before
964 attempting passes with implicit coercions.
966 \subsubsection{Disambiguation passes}
968 According to the criteria described above in \MATITA{} we choose to perform the
969 sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
970 our experience that choice gives reasonable performance and minimize the need of
971 user interaction during the disambiguation.
974 \caption{Sequence of disambiguation passes used in \MATITA.\strut}
975 \label{tab:disambpasses}
977 \begin{tabular}{c|c|c|c}
978 \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
979 & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
980 & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
981 & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
983 \PASS & Mono aliases & Shared & Disabled \\
984 \PASS & Multi aliases & Shared & Disabled \\
985 \PASS & Mono aliases & Fresh instances & Disabled \\
986 \PASS & Multi aliases & Fresh instances & Disabled \\
987 \PASS & Mono aliases & Fresh instances & Enabled \\
988 \PASS & Multi aliases & Fresh instances & Enabled \\
989 \PASS & Library aliases& Fresh instances & Enabled
996 \subsection{Generation and Invalidation}
997 \label{sec:libmanagement}
999 The aim of this section is to describe the way \MATITA{}
1000 preserves the consistency and the availability of the library
1001 using the \WHELP{} technology, in response to the user alteration or
1002 removal of mathematical objects.
1004 As already sketched in Sect.~\ref{sec:fullyspec} what we generate
1005 from a script is split among two storage media, a
1006 classical filesystem and a relational database. The former is used to
1007 store the XML encoding of the objects defined in the script, the
1008 disambiguation aliases and the interpretation and notational convention defined,
1009 while the latter is used to store all the metadata needed by
1012 While the consistency of the data store in the two media has
1013 nothing to do with the nature of
1014 the content of the library and is thus uninteresting (but really
1015 tedious to implement and keep bug-free), there is a deeper
1016 notion of mathematical consistency we need to provide. Each object
1017 must reference only defined object (i.e. each proof must use only
1018 already proved theorems).
1020 We will focus on how \MATITA{} ensures the interesting kind
1021 of consistency during the formalization of a mathematical theory,
1022 giving the user the freedom of adding, removing, modifying objects
1023 without loosing the feeling of an always visible and browsable
1026 \subsubsection{Compilation}
1028 The typechecker component guarantees that if an object is well typed
1029 it depends only on well typed objects available in the library,
1030 that is exactly what we need to be sure that the logic consistency of
1031 the library is preserved. We have only to find the right order of
1032 compilation of the scripts that compose the user development.
1034 For this purpose we provide a tool called \MATITADEP{}
1035 that takes in input the list of files that compose the development and
1036 outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
1037 The user is not asked to run \MATITADEP{} by hand, but
1038 simply to tell \MATITA{} the root directory of his development (where all
1039 script files can be found) and \MATITA{} will handle all the compilation
1040 related tasks, including dependencies calculation.
1041 To compute dependencies it is enough to look at the script files for
1042 inclusions of other parts of the development or for explicit
1043 references to other objects (i.e. with explicit aliases, see
1044 \ref{sec:disambaliases}).
1046 The output of the compilation is immediately available to the user
1047 trough the \WHELP{} technology, since all metadata are stored in a
1048 user-specific area of the database where the search engine has read
1049 access, and all the automated tactics that operates on the whole
1050 library, like \AUTO, have full visibility of the newly defined objects.
1052 Compilation is rather simple, and the only tricky case is when we want
1053 to compile again the same script, maybe after the removal of a
1054 theorem. Here the policy is simple: clean the output before recompiling.
1055 As we will see in the next section cleaning will ensure that
1056 there will be no theorems in the development that depends on the
1059 \subsubsection{Cleaning}
1061 With the term ``cleaning'' we mean the process of removing all the
1062 results of an object compilation. In order to keep the consistency of
1063 the library, cleaning an object requires the (recursive) cleaning
1064 of all the objects that depend on it (\emph{reverse dependencies}).
1066 The calculation of the reverse dependencies can be computed in two
1067 ways, using the relational database or using a simpler set of metadata
1068 that \MATITA{} saves in the filesystem as a result of compilation. The
1069 former technique is the same used by the \emph{Dependency Analyzer}
1070 described in \cite{zack-master} and really depends on a relational
1073 The latter is a fall-back in case the database is not
1074 available.\footnote{Due to the complex deployment of a large piece of
1075 software like a database, it is a common practice for the \HELM{} team
1076 to use a shared remote database, that may be unavailable if the user
1077 workstation lacks network connectivity.} This facility has to be
1078 intended only as a fall-back, since the queries of the \WHELP{}
1079 technology depend require a working database.
1081 Cleaning guarantees that if an object is removed there are no dandling
1082 references to it, and that the part of the library still compiled is
1083 consistent. Since cleaning involves the removal of all the results of
1084 the compilation, metadata included, the library browsable trough the
1085 \WHELP{} technology is always kept up to date.
1087 \subsubsection{Batch vs Interactive}
1089 \MATITA{} includes an interactive authoring interface and a batch
1090 ``compiler'' (\MATITAC). Only the former is intended to be used directly by the
1091 user, the latter is automatically invoked when a
1092 part of the user development is required (for example issuing an
1093 \texttt{include} command) but not yet compiled.
1095 While they share the same engine for compilation and cleaning, they
1096 provide different granularity. The batch compiler is only able to
1097 compile a whole script and similarly to clean only a whole script
1098 (together with all the other scripts that rely on an object defined in
1099 it). The interactive interface is able to execute single steps of
1100 compilation, that may include the definition of an object, and
1101 similarly to undo single steps. Note that in the latter case there is
1102 no risk of introducing dangling references since the \MATITA{} user
1103 interface inhibit undoing a step which is not the last executed.
1105 \subsection{Automation}
1106 \label{sec:automation}
1108 \subsection{Naming convention}
1109 A minor but not entirely negligible aspect of \MATITA{} is that of
1110 adopting a (semi)-rigid naming convention for identifiers, derived by
1111 our studies about metadata for statements.
1112 The convention is only applied to identifiers for theorems
1113 (not definitions), and relates the name of a proof to its statement.
1114 The basic rules are the following:
1116 \item each identifier is composed by an ordered list of (short)
1117 names occurring in a left to right traversal of the statement;
1118 \item all identifiers should (but this is not strictly compulsory)
1119 separated by an underscore,
1120 \item identifiers in two different hypothesis, or in an hypothesis
1121 and in the conclusion must be separated by the string ``\verb+_to_+'';
1122 \item the identifier may be followed by a numerical suffix, or a
1123 single or double apostrophe.
1126 Take for instance the theorem
1127 \[\forall n:nat. n = plus \; n\; O\]
1128 Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
1129 \verb+eq_n_plus_n_O+ and so on.
1130 Similarly, consider the theorem
1131 \[\forall n,m:nat. n<m \to n \leq m\]
1132 In this case \verb+lt_to_le+ is a legal name,
1133 while \verb+lt_le+ is not.\\
1134 But what about, say, the symmetric law of equality? Probably you would like
1135 to name such a theorem with something explicitly recalling symmetry.
1136 The correct approach,
1137 in this case, is the following. You should start with defining the
1138 symmetric property for relations
1140 \[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
1142 Then, you may state the symmetry of equality as
1143 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
1144 and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
1145 So, somehow unexpectedly, the introduction of semi-rigid naming convention
1146 has an important beneficial effect on the global organization of the library,
1147 forcing the user to define abstract notions and properties before
1148 using them (and formalizing such use).
1150 Two cases have a special treatment. The first one concerns theorems whose
1151 conclusion is a (universally quantified) predicate variable, i.e.
1152 theorems of the shape
1153 $\forall P,\dots.P(t)$.
1154 In this case you may replace the conclusion with the word
1155 ``elim'' or ``case''.
1156 For instance the name \verb+nat_elim2+ is a legal name for the double
1157 induction principle.
1159 The other special case is that of statements whose conclusion is a
1161 A typical example is the following
1164 match (eqb n m) with
1165 [ true \Rightarrow n = m
1166 | false \Rightarrow n \neq m]
1168 where $eqb$ is boolean equality.
1169 In this cases, the name can be build starting from the matched
1170 expression and the suffix \verb+_to_Prop+. In the above example,
1171 \verb+eqb_to_Prop+ is accepted.
1173 \section{The authoring interface}
1174 \label{sec:authoring}
1176 The authoring interface of \MATITA{} is very similar to Proof General. We
1177 chose not to build the \MATITA{} UI over Proof General for two reasons. First
1178 of all we wanted to integrate our XML-based rendering technologies, mainly
1179 \GTKMATHVIEW{}. At the time of writing Proof General supports only text based
1180 rendering.\footnote{This may change with the future release of Proof General
1181 based on Eclipse, but is not yet the case.} The second reason is that we wanted
1182 to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
1185 Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
1186 featuring two windows. The background one is very like to the Proof General
1187 interface. The main difference is that we use the \GTKMATHVIEW{} widget to
1188 render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
1189 advantage of the whole bidimensional mathematical notation.
1191 The foreground window, also implemented around \GTKMATHVIEW, is called
1192 ``cicBrowser''. It is used to browse the library, including the proof being
1193 developed, and enable content based search over it. Proofs are rendered in
1194 natural language, automatically generated from the low-level lambda-terms,
1195 using techniques inspired by \cite{natural,YANNTHESIS} and already described
1196 in~\cite{remathematization}.
1198 Note that the syntax used in the script view is \TeX-like, however Unicode is
1199 fully supported so that mathematical glyphs can be input as such.
1203 \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
1204 \caption{\MATITA{} look and feel}
1205 \label{fig:screenshot}
1209 Since the concepts of script based proof authoring are well-known, the
1210 remaining part of this section is dedicated to the distinguishing
1211 features of the \MATITA{} authoring interface.
1213 \subsection{Direct manipulation of terms}
1215 While terms are input as \TeX-like formulae in \MATITA, they are converted to a
1216 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
1217 \GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
1218 high-quality bidimensional rendering of terms (including the use of fancy
1219 layout schemata like radicals and matrices) and the use of a
1220 concise and widespread textual syntax.
1222 Keeping pointers from the presentations level terms down to the
1223 partially specified ones \MATITA{} enable direct manipulation of
1224 rendered (sub)terms in the form of hyperlinks and semantic selection.
1226 \emph{Hyperlinks} have anchors on the occurrences of constant and
1227 inductive type constructors and point to the corresponding definitions
1228 in the library. Anchors are available notwithstanding the use of
1229 user-defined mathematical notation: as can be seen on the right of
1230 Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
1231 encoding complex notations retain all the hyperlinks of constants or
1232 constructors used in the notation.
1234 \emph{Semantic selection} enables the selection of mixed
1235 \MATHML+\BOXML{} markup, constraining the selection to markup
1236 representing meaningful CIC (sub)terms. In the example on the left of
1237 Fig.~\ref{fig:directmanip} is thus possible to select the subterm
1238 $\mathrm{prime}~n$, whereas it would not be possible to select
1239 $\to n$ since the former denotes an application while the
1240 latter it not a subterm. Once a meaningful (sub)term has been
1241 selected actions can be done on it like reductions or tactic
1246 \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
1247 \hspace{0.05\textwidth}
1248 \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
1249 \caption{Semantic selection and hyperlinks}
1250 \label{fig:directmanip}
1256 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
1257 \hspace{0.02\textwidth}
1258 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
1259 \hspace{0.02\textwidth}
1260 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}
1261 \caption{Browsing and searching the library}
1262 \label{fig:cicbrowser}
1266 \subsection{Patterns}
1268 In several situations working with direct manipulation of terms is
1269 simpler and faster than typing the corresponding textual
1270 commands~\cite{proof-by-pointing}.
1271 Nonetheless we need to record actions and selections in scripts.
1273 In \MATITA{} \emph{patterns} are textual representations of selections.
1274 Users can select using the GUI and then ask the system to paste the
1275 corresponding pattern in this script, but more often this process is
1276 transparent: once an action is performed on a selection, the corresponding
1277 textual command is computed and inserted in the script.
1279 \subsubsection{Pattern syntax}
1281 Patterns are composed of two parts: \NT{sequent\_path} and
1282 \NT{wanted}; their concrete syntax is reported in table
1285 \NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
1286 with $?$ and selecting the interesting parts with the placeholder
1287 $\%$. \NT{wanted} is a term that lives in the context of the
1290 Textual patterns produced from a graphical selection are made of the
1291 \NT{sequent\_path} only. Such patterns can represent every selection,
1292 but are quite verbose. The \NT{wanted} part of the syntax is meant to
1293 help the users in writing concise and elegant patterns by hand.
1296 \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
1299 \begin{array}{@{}rcll@{}}
1301 ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
1302 \NT{sequent\_path} &
1303 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
1304 [~\verb+\vdash+~\NT{multipath}~] & \\
1305 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
1306 \NT{wanted} & ::= & \NT{term} & \\
1312 \subsubsection{Pattern evaluation}
1314 Patterns are evaluated in two phases. The first selects roots
1315 (subterms) of the sequent, using the $\NT{sequent\_path}$, while the
1316 second searches the $\NT{wanted}$ term starting from these roots.
1317 % Both are optional steps, and by convention the empty pattern selects
1318 % the whole conclusion.
1322 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
1323 part of the syntax. $\NT{ident}$ is an hypothesis name and
1324 selects the assumption where the following optional $\NT{multipath}$
1325 will operate. \verb+\vdash+ can be considered the name for the goal.
1326 If the whole pattern is omitted, the whole goal will be selected.
1327 If one or more hypotheses names are given the selection is restricted to
1328 these assumptions. If a $\NT{multipath}$ is omitted the whole
1329 assumption is selected. Remember that the user can be mostly
1330 unaware of this syntax, since the system is able to write down a
1331 $\NT{sequent\_path}$ starting from a visual selection.
1332 \NOTE{Questo ancora non va in matita}
1334 A $\NT{multipath}$ is a CIC term in which a special constant $\%$
1336 The roots of discharged subterms are marked with $?$, while $\%$
1337 is used to select roots. The default $\NT{multipath}$, the one that
1338 selects the whole term, is simply $\%$.
1339 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
1340 that respectively select the first argument of an application or
1341 the source of an arrow and the head of the application that is
1342 found in the arrow target.
1344 The first phase not only selects terms (roots of subterms) but
1345 determines also their context that will be eventually used in the
1349 plays a role only if the $[~\verb+match+~\NT{wanted}~]$
1350 part is specified. From the first phase we have some terms, that we
1351 will see as subterm roots, and their context. For each of these
1352 contexts the $\NT{wanted}$ term is disambiguated in it and the
1353 corresponding root is searched for a subterm that can be unified to
1354 $\NT{wanted}$. The result of this search is the selection the
1359 \subsubsection{Examples}
1360 %To explain how the first phase works let us give an example. Consider
1361 %you want to prove the uniqueness of the identity element $0$ for natural
1362 %sum, and that you can rely on the previously demonstrated left
1363 %injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
1366 %theorem valid_name: \forall n,m. m + n = n \to m = O.
1370 Consider the following sequent
1378 To change the right part of the equivalence of the $H$
1379 hypothesis with $O + n$ the user selects and pastes it as the pattern
1380 in the following statement.
1382 change in H:(? ? ? %) with (O + n).
1385 To understand the pattern (or produce it by hand) the user should be
1386 aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
1387 that the pattern selects only the third argument of $eq$.
1389 The experienced user may also write by hand a concise pattern
1390 to change at once all the occurrences of $n$ in the hypothesis $H$:
1392 change in H match n with (O + n).
1395 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
1396 the second phase locates $n$.
1398 The latter pattern is equivalent to the following one, that the system
1399 can automatically generate from the selection.
1401 change in H:(? ? (? ? %) %) with (O + n).
1405 \subsubsection{Tactics supporting patterns}
1406 MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
1407 INTERFACCIA OCMUNE PER LE TATTICHE
1409 In \MATITA{} all the tactics that can be restricted to subterm of the working
1410 sequent accept the pattern syntax. In particular these tactics are: simplify,
1411 change, fold, unfold, generalize, replace and rewrite.
1413 \NOTE{attualmente rewrite e fold non supportano phase 2. per
1414 supportarlo bisogna far loro trasformare il pattern phase1+phase2
1415 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
1416 con una pattern\_of(select(pattern))}
1418 \subsubsection{Comparison with \COQ{}}
1419 \COQ{} has two different ways of restricting the application of tactics to
1420 subterms of the sequent, both relaying on the same special syntax to identify
1423 The first way is to use this special syntax to tell the
1424 tactic what occurrences of a wanted term should be affected.
1425 The second is to prepare the sequent with another tactic called
1426 pattern and then apply the real tactic. Note that the choice is not
1427 left to the user, since some tactics needs the sequent to be prepared
1428 with pattern and do not accept directly this special syntax.
1430 The base idea is that to identify a subterm of the sequent we can
1431 write it and say that we want, for example, the third and the fifth
1432 occurrences of it (counting from left to right). In our previous example,
1433 to change only the left part of the equivalence, the correct command
1436 change n at 2 in H with (O + n)
1439 meaning that in the hypothesis $H$ the $n$ we want to change is the
1440 second we encounter proceeding from left to right.
1442 The tactic pattern computes a
1443 $\beta$-expansion of a part of the sequent with respect to some
1444 occurrences of the given term. In the previous example the following
1450 would have resulted in this sequent
1454 H : (fun n0 : nat => m + n = n0) n
1455 ============================
1459 where $H$ is $\beta$-expanded over the second $n$
1460 occurrence. This is a trick to make the unification algorithm ignore
1461 the head of the application (since the unification is essentially
1462 first-order) but normally operate on the arguments.
1463 This works for some tactics, like rewrite and replace,
1464 but for example not for change and other tactics that do not relay on
1467 The idea behind this way of identifying subterms in not really far
1468 from the idea behind patterns, but really fails in extending to
1469 complex notation, since it relays on a mono-dimensional sequent representation.
1470 Real math notation places arguments upside-down (like in indexed sums or
1471 integrations) or even puts them inside a bidimensional matrix.
1472 In these cases using the mouse to select the wanted term is probably the
1473 only way to tell the system exactly what you want to do.
1475 One of the goals of \MATITA{} is to use modern publishing techniques, and
1476 adopting a method for restricting tactics application domain that discourages
1477 using heavy math notation, would definitively be a bad choice.
1480 \subsection{Tacticals}
1481 There are mainly two kinds of languages used by proof assistants to recorder
1482 proofs: tactic based and declarative. We will not investigate the philosophy
1483 around the choice that many proof assistant made, \MATITA{} included, and we
1484 will not compare the two different approaches. We will describe the common
1485 issues of the tactic-based language approach and how \MATITA{} tries to solve
1488 \subsubsection{Tacticals overview}
1490 Tacticals first appeared in LCF and can be seen as programming
1491 constructs, like looping, branching, error recovery or sequential composition.
1492 The following simple example shows three tacticals in action
1496 A = B \to ((A \to B) \land (B \to A)).
1499 [ rewrite < H. assumption.
1500 | rewrite > H. assumption.
1505 The first is ``\texttt{;}'' that combines the tactic \texttt{split}
1506 with \texttt{intro}, applying the latter to each goal opened by the
1507 former. Then we have ``\texttt{[}'' that branches on the goals (here
1508 we have two goals, the two sides of the logic and).
1509 The first goal $B$ (with $A$ in the context)
1510 is proved by the first sequence of tactics
1511 \texttt{rewrite} and \texttt{assumption}. Then we move to the second
1512 goal with the separator ``\texttt{|}''. The last tactical we see here
1513 is ``\texttt{.}'' that is a sequential composition that selects the
1514 first goal opened for the following tactic (instead of applying it to
1515 them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
1516 not considered a tactical, but a sentence terminator (i.e. the
1517 delimiter of commands the proof assistant executes).
1519 Giving serious examples here is rather difficult, since they are hard
1520 to read without the interactive tool. To help the reader in
1521 understanding the following considerations we just give few common
1522 usage examples without a proof context.
1525 elim z; try assumption; [ ... | ... ].
1526 elim z; first [ assumption | reflexivity | id ].
1529 The first example goes by induction on a term \texttt{z} and applies
1530 the tactic \texttt{assumption} to each opened goal eventually recovering if
1531 \texttt{assumption} fails. Here we are asking the system to close all
1532 trivial cases and then we branch on the remaining with ``\texttt{[}''.
1533 The second example goes again by induction on \texttt{z} and tries to
1534 close each opened goal first with \texttt{assumption}, if it fails it
1535 tries \texttt{reflexivity} and finally \texttt{id}
1536 that is the tactic that leaves the goal untouched without failing.
1538 Note that in the common implementation of tacticals both lines are
1539 compositions of tacticals and in particular they are a single
1540 statement (i.e. derived from the same non terminal entry of the
1541 grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
1542 this is not true, since each atomic tactic or punctuation is considered
1545 \subsubsection{Common issues of tactic(als)-based proof languages}
1546 We will examine the two main problems of tactic(als)-based proof script:
1547 maintainability and readability.
1549 Huge libraries of formal mathematics have been developed, and backward
1550 compatibility is a really time consuming task. \\
1551 A real-life example in the history of \MATITA{} was the reordering of
1552 goals opened by a tactic application. We noticed that some tactics
1553 were not opening goals in the expected order. In particular the
1554 \texttt{elim} tactic on a term of an inductive type with constructors
1555 $c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
1556 \ldots, g_2$. The library of \MATITA{} was still in an embryonic state
1557 but some theorems about integers were there. The inductive type of
1558 $\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
1559 induction proofs on this type where written without tacticals and,
1560 obviously, considering the three induction cases in the wrong order.
1561 Fixing the behavior of the tactic broke the library and two days of
1562 work were needed to make it compile again. The whole time was spent in
1563 finding the list of tactics used to prove the third induction case and
1564 swap it with the list of tactics used to prove the second case. If
1565 the proofs was structured with the branch tactical this task could
1566 have been done automatically.
1568 From this experience we learned that the use of tacticals for
1569 structuring proofs gives some help but may have some drawbacks in
1570 proof script readability. We must highlight that proof scripts
1571 readability is poor by itself, but in conjunction with tacticals it
1572 can be nearly impossible. The main cause is the fact that in proof
1573 scripts there is no trace of what you are working on. It is not rare
1574 for two different theorems to have the same proof script (while the
1575 proof is completely different).\\
1576 Bad readability is not a big deal for the user while he is
1577 constructing the proof, but is considerably a problem when he tries to
1578 reread what he did or when he shows his work to someone else. The
1579 workaround commonly used to read a script is to execute it again
1580 step-by-step, so that you can see the proof goal changing and you can
1581 follow the proof steps. This works fine until you reach a tactical. A
1582 compound statement, made by some basic tactics glued with tacticals,
1583 is executed in a single step, while it obviously performs lot of proof
1584 steps. In the fist example of the previous section the whole branch
1585 over the two goals (respectively the left and right part of the logic
1586 and) result in a single step of execution. The workaround does not work
1587 anymore unless you de-structure on the fly the proof, putting some
1588 ``\texttt{.}'' where you want the system to stop.\\
1590 Now we can understand the tradeoff between script readability and
1591 proof structuring with tacticals. Using tacticals helps in maintaining
1592 scripts, but makes it really hard to read them again, cause of the way
1595 \MATITA{} uses a language of tactics and tacticals, but tries to avoid
1596 this tradeoff, alluring the user to write structured proof without
1597 making it impossible to read them again.
1599 \subsubsection{The \MATITA{} approach: Tinycals}
1602 \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
1605 \begin{array}{@{}rcll@{}}
1607 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
1609 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
1610 \NT{block\_delimiter} &
1611 ::= & \verb+begin+ ~|~ \verb+end+ & \\
1613 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
1619 \MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
1620 While one would expect to find structured constructs like
1621 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
1622 This is essential for base idea behind \MATITA{} tacticals: step-by-step
1625 The low-level tacticals implementation of \MATITA{} allows a step-by-step
1626 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
1627 not executed as an atomic operation. This has two major benefits for the user,
1628 even being a so simple idea:
1630 \item[Proof structuring]
1631 is much easier. Consider for example a proof by induction, and imagine you
1632 are using classical tacticals in one of the state of the
1633 art graphical interfaces for proof assistant like Proof General or \COQIDE.
1634 After applying the induction principle you have to choose: structure
1635 the proof or not. If you decide for the former you have to branch with
1636 ``\texttt{[}'' and write tactics for all the cases separated by
1637 ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
1638 You can replace most of the cases by the identity tactic just to
1639 concentrate only on the first goal, but you will have to go one step back and
1640 one further every time you add something inside the tactical. Again this is
1641 caused by the one step execution of tacticals and by the fact that to modify
1642 the already executed script you have to undo one step.
1643 And if you are board of doing so, you will finish in giving up structuring
1644 the proof and write a plain list of tactics.\\
1645 With step-by-step tacticals you can apply the induction principle, and just
1646 open the branching tactical ``\texttt{[}''. Then you can interact with the
1647 system reaching a proof of the first case, without having to specify any
1648 tactic for the other goals. When you have proved all the induction cases, you
1649 close the branching tactical with ``\texttt{]}'' and you are done with a
1650 structured proof. \\
1651 While \MATITA{} tacticals help in structuring proofs they allow you to
1652 choose the amount of structure you want. There are no constraints imposed by
1653 the system, and if the user wants he can even write completely plain proofs.
1656 is possible. Going on step by step shows exactly what is going on. Consider
1657 again a proof by induction, that starts applying the induction principle and
1658 suddenly branches with a ``\texttt{[}''. This clearly separates all the
1659 induction cases, but if the square brackets content is executed in one single
1660 step you completely loose the possibility of rereading it and you have to
1661 temporary remove the branching tactical to execute in a satisfying way the
1662 branches. Again, executing step-by-step is the way you would like to review
1663 the demonstration. Remember that understanding the proof from the script is
1664 not easy, and only the execution of tactics (and the resulting transformed
1665 goal) gives you the feeling of what is going on.
1668 \section{Standard library}
1671 \MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
1672 can be read, checked and referenced in further developments.
1673 However, in order to test the actual usability of the system, a
1674 new library of results has been started from scratch. In this case,
1675 of course, we wrote (and offer) the source script files,
1676 while, in the case of \COQ, \MATITA{} may only rely on XML files of
1678 The current library just comprises about one thousand theorems in
1679 elementary aspects of arithmetics up to the multiplicative property for
1680 Eulers' totient function $\phi$.
1681 The library is organized in five main directories: \texttt{logic} (connectives,
1682 quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
1683 constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
1684 (rationals). The most complex development is \texttt{nat}, organized in 25
1685 scripts, listed in Tab.~\ref{tab:scripts}.
1688 \begin{tabular}{lll}
1689 \SCRIPT{nat.ma} & \SCRIPT{plus.ma} & \SCRIPT{times.ma} \\
1690 \SCRIPT{minus.ma} & \SCRIPT{exp.ma} & \SCRIPT{compare.ma} \\
1691 \SCRIPT{orders.ma} & \SCRIPT{le\_arith.ma} & \SCRIPT{lt\_arith.ma} \\
1692 \SCRIPT{factorial.ma} & \SCRIPT{sigma\_and\_pi.ma} & \SCRIPT{minimization.ma} \\
1693 \SCRIPT{div\_and\_mod.ma} & \SCRIPT{gcd.ma} & \SCRIPT{congruence.ma} \\
1694 \SCRIPT{primes.ma} & \SCRIPT{nth\_prime.ma} & \SCRIPT{ord.ma} \\
1695 \SCRIPT{count.ma} & \SCRIPT{relevant\_equations.ma} & \SCRIPT{permutation.ma} \\
1696 \SCRIPT{factorization.ma} & \SCRIPT{chinese\_reminder.ma} &
1697 \SCRIPT{fermat\_little\_th.ma} \\
1698 \SCRIPT{totient.ma} & & \\
1700 \caption{\label{tab:scripts} Scripts on natural numbers in the standard library}
1703 We do not plan to maintain the library in a centralized way,
1704 as most of the systems do. On the contrary we are currently
1705 developing wiki-technologies to support a collaborative
1706 development of the library, encouraging people to expand,
1707 modify and elaborate previous contributions.
1709 \section{Conclusions}
1712 We would like to thank all the students that during the past
1713 five years collaborated in the \HELM{} project and contributed to
1714 the development of \MATITA{}, and in particular
1715 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
1720 \bibliography{matita}