1 \documentclass[]{kluwer}
9 \newcommand{\component}{component}
10 \newcommand{\components}{components}
12 \newcommand{\AUTO}{\textsc{Auto}}
13 \newcommand{\BOXML}{BoxML}
14 \newcommand{\COQ}{Coq}
15 \newcommand{\COQIDE}{CoqIde}
16 \newcommand{\ELIM}{\textsc{Elim}}
17 \newcommand{\GDOME}{Gdome}
18 \newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
19 \newcommand{\HELM}{Helm}
20 \newcommand{\HINT}{\textsc{Hint}}
21 \newcommand{\IN}{\ensuremath{\dN}}
22 \newcommand{\INSTANCE}{\textsc{Instance}}
23 \newcommand{\IR}{\ensuremath{\dR}}
24 \newcommand{\IZ}{\ensuremath{\dZ}}
25 \newcommand{\LIBXSLT}{LibXSLT}
26 \newcommand{\LOCATE}{\textsc{Locate}}
27 \newcommand{\MATCH}{\textsc{Match}}
28 \newcommand{\MATHML}{MathML}
29 \newcommand{\MATITA}{Matita}
30 \newcommand{\MATITAC}{\texttt{matitac}}
31 \newcommand{\MATITADEP}{\texttt{matitadep}}
32 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
33 \newcommand{\MOWGLI}{MoWGLI}
34 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
35 \newcommand{\NATIND}{\mathit{nat\_ind}}
36 \newcommand{\NUPRL}{NuPRL}
37 \newcommand{\OCAML}{OCaml}
38 \newcommand{\PROP}{\mathit{Prop}}
39 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
40 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
41 \newcommand{\UWOBO}{UWOBO}
42 \newcommand{\GETTER}{Getter}
43 \newcommand{\WHELP}{Whelp}
44 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
45 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
46 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
47 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
48 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
49 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
50 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
51 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
52 \newcommand{\SKIP}{\MATHTT{skip}}
53 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
55 \newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
56 \newcommand{\URI}[1]{\texttt{#1}}
57 \newcommand{\OP}[1]{``\texttt{#1}''}
58 \newcommand{\FILE}[1]{\texttt{#1}}
59 \newcommand{\NOTE}[1]{\ednote{#1}{}}
60 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
62 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
64 \newenvironment{grafite}{\VerbatimEnvironment
65 \begin{SaveVerbatim}{boxtmp}}%
66 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
68 \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
72 \newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
75 \newcommand{\sequent}[2]{
76 \savebox{\tmpxyz}[0.9\linewidth]{
77 \begin{minipage}{0.9\linewidth}
81 \end{minipage}}\setlength{\fboxsep}{3mm}%
83 \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
86 \bibliographystyle{alpha}
91 \title{The \MATITA{} Proof Assistant}
93 \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
94 \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
95 \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
96 \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
98 \institute{Department of Computer Science, University of Bologna\\
99 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
101 \runningtitle{The \MATITA{} proof assistant}
102 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
105 ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
109 \TODO{scrivere abstract}
112 \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
116 % toc & co: to be removed in the final paper version
121 \section{Introduction}
124 \MATITA{} is the Proof Assistant under development by the \HELM{}
125 team~\cite{mkm-helm} at the University of Bologna, under the direction of
126 Prof.~Asperti. The paper describes the overall architecture of
127 the system, focusing on its most distinctive and innovative
130 \subsection{Historical Perspective}
131 The origins of \MATITA{} go back to 1999. At the time we were mostly
132 interested to develop tools and techniques to enhance the accessibility
133 via Web of formal libraries of mathematics. Due to its dimension, the
134 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
135 was chosen as a privileged test bench for our work, although experiments
136 have been also conducted with other systems, and notably
137 with \NUPRL~\cite{nuprl-book}.
138 The work, mostly performed in the framework of the recently concluded
139 European project IST-33562 \MOWGLI~\cite{pechino}, mainly consisted in the
142 \item exporting the information from the internal representation of
143 \COQ{} to a system and platform independent format. Since XML was at the
144 time an emerging standard, we naturally adopted this technology, fostering
145 a content-centric architecture~\cite{content-centric} where the documents
146 of the library were the the main components around which everything else
148 \item developing indexing and searching techniques supporting semantic
149 queries to the library;
150 \item developing languages and tools for a high-quality notational
151 rendering of mathematical information\footnote{We have been
152 active in the \MATHML{} Working group since 1999.};
155 According to our content-centric commitment, the library exported from
156 \COQ{} was conceived as being distributed and most of the tools were developed
157 as Web services. The user could interact with the library and the tools by
158 means of a Web interface that orchestrates the Web services.
160 The Web services and the other tools have been implemented as front-ends
161 to a set of software components, collectively called the \HELM{} components.
162 At the end of the \MOWGLI{} project we already disposed of the following
163 tools and software components:
165 \item XML specifications for the Calculus of Inductive Constructions,
166 with components for parsing and saving mathematical objects in such a
167 format~\cite{exportation-module};
168 \item metadata specifications with components for indexing and querying the
170 \item a proof checker library (i.e. the {\em kernel} of a proof assistant),
171 implemented to check that we exported from the \COQ{} library all the
172 logically relevant content;
173 \item a sophisticated parser (used by the search engine), able to deal
174 with potentially ambiguous and incomplete information, typical of the
175 mathematical notation~\cite{disambiguation};
176 \item a {\em refiner} library, i.e. a type inference system, based on
177 partially specified terms, used by the disambiguating parser;
178 \item complex transformation algorithms for proof rendering in natural
179 language~\cite{remathematization};
180 \item an innovative, \MATHML-compliant rendering widget for the GTK
181 graphical environment~\cite{padovani}, supporting
182 high-quality bidimensional
183 rendering, and semantic selection, i.e. the possibility to select semantically
184 meaningful rendering expressions, and to paste the respective content into
185 a different text area.
187 Starting from all this, developing our own proof assistant was not
188 too far away: essentially, we ``just'' had to
189 add an authoring interface, and a set of functionalities for the
190 overall management of the library, integrating everything into a
191 single system. \MATITA{} is the result of this effort.
193 \subsection{The system}
195 \MATITA{} is a proof assistant (also called interactive theorem prover).
196 It is based on the Calculus of (Co)Inductive Constructions
197 (CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
198 Church enriched with primitive inductive and co-inductive data types.
199 Via the Curry-Howard isomorphism, the calculus can be seen as a very
200 rich higher order logic and proofs can be simply represented and
201 stored as lambda-terms. \COQ{} and Lego are other systems that adopt
202 (variations of) CIC as their foundation.
204 The proof language of \MATITA{} is procedural, in the tradition of the LCF
205 theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
206 whose proof language is procedural. Traditionally, in a procedural system
207 the user interacts only with the \emph{script}, while proof terms are internal
208 records kept by the system. On the contrary, in \MATITA{} proof terms are
209 praised as declarative versions of the proof. With this role, they are the
210 primary mean of communication of proofs (once rendered to natural language
211 for human audiences).
213 The user interfaces now adopted by all the proof assistants based on a
214 procedural proof language have been inspired by the CtCoq pioneering
215 system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
216 by CtCoq is the Proof General generic interface~\cite{proofgeneral},
217 that has set a sort of
218 standard way to interact with the system. Several procedural proof assistants
219 have either adopted or cloned Proof General as their main user interface.
220 The authoring interface of \MATITA{} is a clone of the Proof General interface.
222 \TODO{item che seguono:}
224 \item sistema indipendente (da \COQ)
225 \item compatibilit\`a con sistemi legacy
228 \subsection{Relationship with \COQ{}}
230 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
231 more the effect of the circumstances of its creation described
232 above than the result of a deliberate design. In particular, we
233 (essentially) share the same foundational dialect of \COQ{} (the
234 Calculus of (Co)Inductive Constructions), the same implementation
235 language (\OCAML{}), and the same (script based) authoring philosophy.
236 However, the analogy essentially stops here and no code is shared by the
239 In a sense; we like to think of \MATITA{} as the way \COQ{} would
240 look like if entirely rewritten from scratch: just to give an
241 idea, although \MATITA{} currently supports almost all functionalities of
242 \COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
243 by \COQ{} (and we are convinced that, starting from scratch again,
244 we could reduce our code even further in sensible way).
246 Moreover, the complexity of the code of \MATITA{} is greatly reduced with
247 respect to \COQ. For instance, the API of the components of \MATITA{} comprise
248 989 functions, to be compared with the 4'286 functions of \COQ.
250 Finally, \MATITA{} has several innovative features over \COQ{} that derive
251 from the integration of Mathematical Knowledge Management tools with proof
252 assistants. Among them, the advanced indexing tools over the library and
253 the parser for ambiguous mathematical notation.
255 The size and complexity improvements over \COQ{} must be understood
256 historically. \COQ{} is a quite old
257 system whose development started 20 years ago.
258 \NOTE{Zack: verificato su Coq'Art, \`e iniziato nel 1985-86}
260 several developers have took over the code and several new research ideas
261 that were not considered in the original architecture have been experimented
262 and integrated in the system. Moreover, there exists a lot of developments
263 for \COQ{} that require backward compatibility between each pair of releases;
264 since many central functionalities of a proof assistant are based on heuristics
265 or arbitrary choices to overcome undecidability (e.g. for higher order
266 unification), changing these functionalities maintaining backward compatibility
267 is very difficult. Finally, the code of \COQ{} has been greatly optimized
268 over the years; optimization reduces maintainability and rises the complexity
271 In writing \MATITA{} we have not been hindered by backward compatibility and
272 we have took advantage of the research results and experiences previously
273 developed by others, comprising the authors of \COQ. Moreover, starting from
274 scratch, we have designed in advance the architecture and we have split
275 the code in coherent minimally coupled components.
277 In the future we plan to exploit \MATITA{} as a test bench for new ideas and
278 extensions. Keeping the single components and the whole architecture as
279 simple as possible is thus crucial to foster future experiments and to
280 allow other developers to quickly understand our code and contribute.
282 %For direct experience of the authors, the learning curve to understand and
283 %be able to contribute to \COQ{}'s code is quite steep and requires direct
284 %and frequent interactions with \COQ{} developers.
286 \section{Architecture}
291 \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
292 \caption[\MATITA{} components and related applications]{\MATITA{}
293 components and related applications, with thousands of line of
295 \label{fig:libraries}
299 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
300 (circle nodes) and \emph{applications} (squared nodes) developed in the HELM
301 project. Each node is annotated with the number of lines of source code
302 (comprising comments).
304 Applications and \components{} depend over other \components{} forming a
305 directed acyclic graph (DAG). Each \component{} can be decomposed in
306 a a set of \emph{modules} also forming a DAG.
308 Modules and \components{} provide coherent sets of functionalities
309 at different scales. Applications that require only a few functionalities
310 depend on a restricted set of \components{}.
312 Only the proof assistant \MATITA{} and the \WHELP{} search engine are
313 applications meant to be used directly by the user. All the other applications
314 are Web services developed in the HELM and MoWGLI projects and already described
315 elsewhere. In particular:
317 \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
318 from a physical location (URL) given its logical name (URI). The Getter is
319 responsible of updating a table that maps URIs to URLs. Thanks to the Getter
320 it is possible to work on a logically monolithic library that is physically
321 distributed on the network. More information on the Getter can be found
322 in~\cite{zack-master}.
323 \item \emph{\WHELP} is a search engine to index and locate mathematical
324 notions (axioms, theorems, definitions) in the logical library managed
325 by the Getter. Typical examples of a query to Whelp are queries that search
326 for a theorem that generalize or instantiate a given formula, or that
327 can be immediately applied to prove a given goal. The output of Whelp is
328 an XML document that lists the URIs of a complete set of candidates that
329 are likely to satisfy the given query. The set is complete in the sense
330 that no notion that actually satisfies the query is thrown away. However,
331 the query is only approximated in the sense that false matches can be
332 returned. Whelp has been described in~\cite{whelp}.
333 \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
334 notion in the distributed library, renders it according to the user provided
335 two dimensional mathematical notation. \UWOBO{} may also embed the rendering
336 of mathematical notions into arbitrary documents before returning them.
337 The Getter is used by \UWOBO{} to retrieve the document to be rendered.
338 \UWOBO{} has been described in~\cite{zack-master}.
339 \item The \emph{Proof Checker} is a Web service that, given the URI of
340 notion in the distributed library, checks its correctness. Since the notion
341 is likely to depend in an acyclic way over other notions, the proof checker
342 is also responsible of building in a top-down way the DAG of all
343 dependencies, checking in turn every notion for correctness.
344 The proof checker has been described in~\cite{zack-master}.
345 \item The \emph{Dependency Analyzer} is a Web service that can produce
346 a textual or graphical representation of the dependencies of an object.
347 The dependency analyzer has been described in~\cite{zack-master}.
350 The dependency of a \component{} or application over another \component{} can
351 be satisfied by linking the \component{} in the same executable.
352 For those \components{} whose functionalities are also provided by the
353 aforementioned Web services, it is also possible to link stub code that
354 forwards the request to a remote Web service. For instance, the Getter
355 is just a wrapper to the \GETTER{} \component{} that allows the
356 \component{} to be used as a Web service. \MATITA{} can directly link the code
357 of the \GETTER{} \component, or it can use a stub library with the same
358 API that forwards every request to the Getter.
360 To better understand the architecture of \MATITA{} and the role of each
361 \component, we can focus on the representation of the mathematical information.
362 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
363 Constructions (CIC). In CIC terms are used to represent mathematical
364 formulae, types and proofs. \MATITA{} is able to handle terms at
365 four different levels of specification. On each level it is possible to provide
366 a different set of functionalities. The four different levels are:
367 fully specified terms; partially specified terms;
368 content level terms; presentation level terms.
370 \subsection{Fully specified terms}
371 \label{sec:fullyintro}
373 \emph{Fully specified terms} are CIC terms where no information is
374 missing or left implicit. A fully specified term should be well-typed.
375 The mathematical notions (axioms, definitions, theorems) that are stored
376 in our mathematical library are fully specified and well-typed terms.
377 Fully specified terms are extremely verbose (to make type-checking
378 decidable). Their syntax is fixed and does not resemble the usual
379 extendible mathematical notation. They are not meant for direct user
382 The \texttt{cic} \component{} defines the data type that represents CIC terms
383 and provides a parser for terms stored in an XML format.
385 The most important \component{} that deals with fully specified terms is
386 \texttt{cic\_proof\_checking}. It implements the procedure that verifies
387 if a fully specified term is well-typed. It also implements the
388 \emph{conversion} judgement that verifies if two given terms are
389 computationally equivalent (i.e. they share the same normal form).
391 Terms may reference other mathematical notions in the library.
392 One commitment of our project is that the library should be physically
393 distributed. The \GETTER{} \component{} manages the distribution,
394 providing a mapping from logical names (URIs) to the physical location
395 of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
396 data type and several utility functions over URIs. The
397 \texttt{cic\_proof\_checking} \component{} calls the \GETTER{}
398 \component{} every time it needs to retrieve the definition of a mathematical
399 notion referenced by a term that is being type-checked.
401 The Proof Checker is the Web service that provides an interface
402 to the \texttt{cic\_proof\_checking} \component.
404 We use metadata and a sort of crawler to index the mathematical notions
405 in the distributed library. We are interested in retrieving a notion
406 by matching, instantiation or generalization of a user or system provided
407 mathematical formula. Thus we need to collect metadata over the fully
408 specified terms and to store the metadata in some kind of (relational)
409 database for later usage. The \texttt{hmysql} \component{} provides
411 interface to a (possibly remote) MySql database system used to store the
412 metadata. The \texttt{metadata} \component{} defines the data type of the
414 we are collecting and the functions that extracts the metadata from the
415 mathematical notions (the main functionality of the crawler).
416 The \texttt{whelp} \component{} implements a search engine that performs
417 approximated queries by matching/instantiation/generalization. The queries
418 operate only on the metadata and do not involve any actual matching
419 (that will be described later on and that is implemented in the
420 \texttt{cic\_unification} \component). Not performing any actual matching
421 the query only returns a complete and hopefully small set of matching
422 candidates. The process that has issued the query is responsible of
423 actually retrieving from the distributed library the candidates to prune
424 out false matches if interested in doing so.
426 The Whelp search engine is the Web service that provides an interface to
427 the \texttt{whelp} \component.
429 According to our vision, the library is developed collaboratively so that
430 changing or removing a notion can invalidate other notions in the library.
431 Moreover, changing or removing a notion requires a corresponding change
432 in the metadata database. The \texttt{library} \component{} is responsible
433 of preserving the coherence of the library and the database. For instance,
434 when a notion is removed, all the notions that depend on it and their
435 metadata are removed from the library. This aspect will be better detailed
436 in Sect.~\ref{sec:libmanagement}.
438 \subsection{Partially specified terms}
439 \label{sec:partiallyintro}
441 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
442 Omitted subterms can bear no information at all or they may be associated to
443 a sequent. The formers are called \emph{implicit terms} and they occur only
444 linearly. The latters may occur multiple times and are called
445 \emph{metavariables}. An \emph{explicit substitution} is applied to each
446 occurrence of a metavariable. A metavariable stand for a term whose type is
447 given by the conclusion of the sequent. The term must be closed in the
448 context that is given by the ordered list of hypotheses of the sequent.
449 The explicit substitution instantiates every hypothesis with an actual
450 value for the variable bound by the hypothesis.
452 Partially specified terms are not required to be well-typed. However a
453 partially specified term should be \emph{refinable}. A \emph{refiner} is
454 a type-inference procedure that can instantiate implicit terms and
455 metavariables and that can introduce \emph{implicit coercions} to make a
456 partially specified term well-typed. The refiner of \MATITA{} is implemented
457 in the \texttt{cic\_unification} \component. As the type checker is based on
458 the conversion check, the refiner is based on \emph{unification} that is
459 a procedure that makes two partially specified term convertible by instantiating
460 as few as possible metavariables that occur in them.
462 Since terms are used in CIC to represent proofs, correct incomplete
463 proofs are represented by refinable partially specified terms. The metavariables
464 that occur in the proof correspond to the conjectures still to be proved.
465 The sequent associated to the metavariable is the conjecture the user needs to
468 \emph{Tactics} are the procedures that the user can apply to progress in the
469 proof. A tactic proves a conjecture possibly creating new (and hopefully
470 simpler) conjectures. The implementation of tactics is given in the
471 \texttt{tactics} \component. It is heavily based on the refinement and
472 unification procedures of the \texttt{cic\_unification} \component.
474 The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
475 commands of the \MATITA{} proof assistant. Most of the commands are tactics.
476 Other commands are used to give definitions and axioms or to state theorems
477 and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
478 It implements the semantics of each command in the grafite AST as a function
479 from status to status. It implements also an undo function to go back to
482 As fully specified terms, partially specified terms are not well suited
483 for user consumption since their syntax is not extendible and it is not
484 possible to adopt the usual mathematical notation. However they are already
485 an improvement over fully specified terms since they allow to omit redundant
486 information that can be inferred by the refiner.
488 \subsection{Content level terms}
489 \label{sec:contentintro}
491 The language used to communicate proofs and especially formulae with the
492 user does not only needs to be extendible and accommodate the usual mathematical
493 notation. It must also reflect the comfortable degree of imprecision and
494 ambiguity that the mathematical language provides.
496 For instance, it is common practice in mathematics to speak of a generic
497 equality that can be used to compare any two terms. However, it is well known
498 that several equalities can be distinguished as soon as we care for decidability
499 or for their computational properties. For instance equality over real
500 numbers is well known to be undecidable, whereas it is decidable over
503 Similarly, we usually speak of natural numbers and their operations and
504 properties without caring about their representation. However the computational
505 properties of addition over the binary representation are very different from
506 those of addition over the unary representation. And addition over two natural
507 numbers is definitely different from addition over two real numbers.
509 Formal mathematics cannot hide these differences and obliges the user to be
510 very precise on the types he is using and their representation. However,
511 to communicate formulae with the user and with external tools, it seems good
512 practice to stick to the usual imprecise mathematical ontology. In the
513 Mathematical Knowledge Management community this imprecise language is called
514 the \emph{content level} representation of formulae.
516 In \MATITA{} we provide two translations: from partially specified terms
517 to content level terms and the other way around. The first translation can also
518 be applied to fully specified terms since a fully specified term is a special
519 case of partially specified term where no metavariable or implicit term occurs.
521 The translation from partially specified terms to content level terms must
522 discriminate between terms used to represent proofs and terms used to represent
523 formulae. The firsts are translated to a content level representation of
524 proof steps that can easily be rendered in natural language. The representation
525 adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
526 isomorphic to it. Terms that represent formulae are translated to \MATHML{}
527 Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
528 for the representation of content level formulae in an XML extensible format.
530 The translation to content level is implemented in the
531 \texttt{acic\_content} \component. Its input are \emph{annotated partially
532 specified terms}, that are maximally unshared
533 partially specified terms enriched with additional typing information for each
534 subterm. This information is used to discriminate between terms that represent
535 proofs and terms that represent formulae. Part of it is also stored at the
536 content level since it is required to generate the natural language rendering
537 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
538 and not a DAG). The reason is that to the occurrences of a subterm in
539 two different positions we need to associate different typing informations.
540 This association is made easier when the term is represented as a tree since
541 it is possible to label each node with an unique identifier and associate
542 the typing information using a map on the identifiers.
543 The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
544 by the \texttt{library} \component{} since fully specified terms are stored
545 in the library in their annotated form.
547 We do not provide yet a reverse translation from content level proofs to
548 partially specified terms. But in \texttt{cic\_disambiguation} we do provide
549 the reverse translation for formulae. The mapping from
550 content level formulae to partially specified terms is not unique due to
551 the ambiguity of the content level. As a consequence the translation
552 is guided by an \emph{interpretation}, that is a function that chooses for
553 every ambiguous formula one partially specified term. The
554 \texttt{cic\_disambiguation} \component{} implements the
555 disambiguation algorithm we presented in~\cite{disambiguation} that is
556 responsible of building in an efficient way the set of all ``correct''
557 interpretations. An interpretation is correct if the partially specified term
558 obtained using the interpretation is refinable.
560 In Sect.~\ref{sec:partiallyintro} the last section we described the semantics of
562 function from status to status. We also suggested that the formulae in a
563 command are encoded as partially specified terms. However, consider the
564 command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
565 of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
566 replace $x$ in that context, its encoding as a term cannot be computed
567 until $x$ is located. In other words, $y^2$ must be disambiguated in the
568 context of the occurrence $x$ it must replace.
570 The elegant solution we have implemented consists in representing terms
571 in a command as functions from a context to a partially refined term. The
572 function is obtained by partially applying our disambiguation function to
573 the content term to be disambiguated. Our solution should be compared with
574 the one adopted in the Coq system, where ambiguity is only relative to De Brujin
575 indexes. In Coq variables can be bound either by name or by position. A term
576 occurring in a command has all its variables bound by name to avoid the need of
577 a context during disambiguation. Moreover, this makes more complex every
578 operation over terms (i.e. according to our architecture every module that
579 depends on \texttt{cic}) since the code must deal consistently with both kinds
580 of binding. Also, this solution cannot cope with other forms of ambiguity (as
581 the context dependent meaning of the exponent in the previous example).
583 \subsection{Presentation level terms}
584 \label{sec:presentationintro}
586 Content level terms are a sort of abstract syntax trees for mathematical
587 formulae and proofs. The concrete syntax given to these abstract trees
588 is called \emph{presentation level}.
590 The main important difference between the content level language and the
591 presentation level language is that only the former is extendible. Indeed,
592 the presentation level language is a finite language that comprises all
593 the usual mathematical symbols. Mathematicians invent new notions every
594 single day, but they stick to a set of symbols that is more or less fixed.
596 The fact that the presentation language is finite allows the definition of
597 standard languages. In particular, for formulae we have adopt \MATHML{}
598 Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
600 represent proofs it is enough to embed formulae in plain text enriched with
601 formatting boxes. Since the language of formatting boxes is very simple,
602 many equivalent specifications exist and we have adopted our own, called
605 The \texttt{content\_pres} \component{} contains the implementation of the
606 translation from content level terms to presentation level terms. The
607 rendering of presentation level terms is left to the application that uses
608 the \component. However, in the \texttt{hgdome} \component{} we provide a few
609 utility functions to build a \GDOME~\cite{gdome2} \MATHML+\BOXML{} tree from our
611 level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
613 widget developed by Luca Padovani~\cite{padovani}. The widget is
614 particularly interesting since it allows to implement \emph{semantic
617 Semantic selection is a technique that consists in enriching the presentation
618 level terms with pointers to the content level terms and to the partially
619 specified terms they correspond to. Highlight of formulae in the widget is
620 constrained to selection of meaningful expressions, i.e. expressions that
621 correspond to a lower level term, that is a content term or a partially or
622 fully specified term.
623 Once the rendering of a lower level term is
624 selected it is possible for the application to retrieve the pointer to the
625 lower level term. An example of applications of semantic selection is
626 \emph{semantic cut\&paste}: the user can select an expression and paste it
627 elsewhere preserving its semantics (i.e. the partially specified term),
628 possibly performing some semantic transformation over it (e.g. renaming
629 variables that would be captured or lambda-lifting free variables).
631 The reverse translation from presentation level terms to content level terms
632 is implemented by a parser that is also found in \texttt{content\_pres}.
633 Differently from the translation from content level terms to partially
634 refined terms, this translation is not ambiguous. The reason is that the
635 parsing tool we have adopted (CamlP4) is not able to parse ambiguous
636 grammars. Thus we require the mapping from presentation level terms
637 (concrete syntax) to content level terms (abstract syntax) to be unique.
638 This means that the user must fix once and for all the associativity and
639 precedence level of every operator he is using. In practice this limitation
640 does not seem too strong. The reason is that the target of the
641 translation is an ambiguous language and the user is free to associate
642 to every content level term several different interpretations (as a
643 partially specified term).
645 Both the direct and reverse translation from presentation to content level
646 terms are parameterized over the user provided mathematical notation.
647 The \texttt{lexicon} \component{} is responsible of managing the lexicon,
648 that is the set of active notations. It defines an abstract syntax tree
649 of commands to declare and activate new notations and it implements the
650 semantics of these commands. It also implements undoing of the semantic
651 actions. Among the commands there are hints to the
652 disambiguation algorithm that are used to control and speed up disambiguation.
653 These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
655 Finally, the \texttt{grafite\_parser} \component{} implements a parser for
656 the concrete syntax of the commands of \MATITA. The parser process a stream
657 of characters and returns a stream of abstract syntax trees (the ones
658 defined by the \texttt{grafite} component and whose semantics is given
659 by \texttt{grafite\_engine}). When the parser meets a command that changes
660 the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
661 process the command. When the parser needs to parse a term at the presentation
662 level, it invokes the already described parser for terms contained in
663 \texttt{content\_pres}.
665 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
666 against the \texttt{grafite\_parser} \components{}
667 since they provide an interface to the user. In both cases the formulae
668 written by the user are parsed using the \texttt{content\_pres} \component{} and
669 then disambiguated using the \texttt{cic\_disambiguation} \component. However,
670 only \MATITA{} is linked against the \texttt{grafite\_engine} and
671 \texttt{tactics} components (summing up to a total of 11'200 lines of code)
672 since \WHELP{} can only execute those ASTs that correspond to queries
673 (implemented in the \texttt{whelp} component).
675 The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
676 providing a rendering service for the documents in the distributed library.
677 To render a document given its URI, \UWOBO{} retrieves it using the
678 \GETTER{} obtaining a document with fully specified terms. Then it translates
679 it to the presentation level passing through the content level. Finally
680 it returns the result document to be rendered by the user's
681 browser.\NOTE{\TODO{manca la passata verso HTML}}
683 The \components{} not yet described (\texttt{extlib}, \texttt{xml},
684 \texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
685 minor \components{} that provide a core of useful functions and basic
686 services missing from the standard library of the programming language.
687 %In particular, the \texttt{xml} \component{} is used to easily represent,
688 %parse and pretty-print XML files.
690 \section{The interface to the library}
693 A proof assistant provides both an interface to interact with its library and
694 an \emph{authoring} interface to develop new proofs and theories. According
695 to its historical origins, \MATITA{} strives to provide innovative
696 functionalities for the interaction with the library. It is more traditional
697 in its script based authoring interface.
699 In the remaining part of the paper we focus on the user view of \MATITA{}.
700 This section is devoted to the aspects of the tool that arise from the
701 document centric approach to the library. Sect.~\ref{sec:authoring} describes
702 the peculiarities of the authoring interface.
704 The library of \MATITA{} comprises mathematical concepts (theorems,
705 axioms, definitions) and notation. The concepts are authored sequentially
706 using scripts that are (ordered) sequences of procedural commands.
707 However, once they are produced we store them independently in the library.
708 The only relation implicitly kept between the notions are the logical,
709 acyclic dependencies among them. This way the library forms a global (and
710 distributed) hypertext. Several useful operations can be implemented on the
711 library only, regardless of the scripts. Examples of such operations
712 implemented in \MATITA{} are: searching and browsing (see Sect.~\ref{sec:indexing});
713 disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
714 automatic proof searching (see Sect.~\ref{sec:automation}).
716 The key requisite for the previous operations is that the library must
717 be fully accessible and in a logically consistent state. To preserve
718 consistency, a concept cannot be altered or removed unless the part of the
719 library that depends on it is modified accordingly. To allow incremental
720 changes and cooperative development, consistent revisions are necessary.
721 For instance, to modify a definition, the user could fork a new version
722 of the library where the definition is updated and all the concepts that
723 used to rely on it are absent. The user is then responsible to restore
724 the removed part in the new branch, merging the branch when the library is
727 To implement the proposed versioning system on top of a standard one
728 it is necessary to implement \emph{invalidation} first. Invalidation
729 is the operation that locates and removes from the library all the concepts
730 that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
731 a concept from the library also involves deleting its metadata from the
734 For non collaborative development, full versioning can be avoided, but
735 invalidation is still required. Since nobody else is relying on the
736 user development, the user is free to change and invalidate part of the library
737 without branching. Invalidation is still necessary to avoid using a
738 concept that is no longer valid.
739 So far, in \MATITA{} we address only this non collaborative scenario
740 (see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
741 is still under design.
743 Scripts are not seen as constituents of the library. They are not published
744 and indexed, so they cannot be searched or browsed using \HELM{} tools.
745 However, they play a central role for the maintenance of the library.
746 Indeed, once a notion is invalidated, the only way to restore it is to
747 fix the possibly broken script that used to generate it.
748 Moreover, during the authoring phase, scripts are a natural way to
749 group notions together. They also constitute a less fine grained clustering
750 of notions for invalidation.
752 In the rest of this section we present in more details the functionalities of
753 \MATITA{} related to library management and exploitation.
754 Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
755 the \MATITA{} authoring interface.
757 \subsection{Indexing and searching}
760 \subsection{Disambiguation}
761 \label{sec:disambiguation}
763 Software applications that involve input of mathematical content should strive
764 to require the user as less drift from informal mathematics as possible. We
765 believe this to be a fundamental aspect of such applications user interfaces.
766 Being that drift in general very large when inputing
767 proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
768 mathematical formulae which can be input using a \TeX-like encoding (the
769 concrete syntax corresponding to presentation level terms) and are then
770 translated (in multiple steps) to partially specified terms as sketched in
771 Sect.~\ref{sec:contentintro}.
773 The key component of the translation is the generic disambiguation algorithm
774 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
775 and presented in~\cite{disambiguation}. In this section we present how to use
776 such an algorithm in the context of the development of a library of formalized
777 mathematics. We will see that using multiple passes of the algorithm, varying
778 some of its parameters, helps in keeping the input terse without sacrificing
781 \subsubsection{Disambiguation aliases}
782 \label{sec:disambaliases}
784 Consider the following command to state a theorem over integer numbers.
788 \forall x, y, z. x < y \to y < z \to x < z.
791 The symbol \OP{<} is likely to be overloaded in the library
792 (at least over natural numbers).
793 Thus, according to the disambiguation algorithm, two different
794 refinable partially specified terms could be associated to it.
795 \MATITA{} asks the user what interpretation he meant. However, to avoid
796 posing the same question in case of a future re-execution (e.g. undo/redo),
797 the choice must be recorded. Scripts need to be re-executed after invalidation.
798 Therefore the choice record must be permanently stored somewhere. The most
799 natural place is in the script itself.
801 In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
802 They are mappings, stored in the library, from ambiguity sources
803 (identifiers, symbols and literal numbers at the content level) to partially
804 specified terms. In case of overloaded sources there exists multiple aliases
805 with the same source. It is possible to record \emph{disambiguation
806 preferences} to select one of the aliases of an overloaded source.
808 Preferences can be explicitely given in the script (using the
809 misleading \texttt{alias} commands), but
810 are also implicitly added when a new concept is introduced (\emph{implicit
811 preferences}) or after a sucessfull disambiguation that did not require
812 user interaction. Explicit preferences are added automatically by \MATITA{} to
813 record the disambiguation choices of the user. For instance, after the
814 disambiguation of the command above, the script is altered as follows:
817 alias symbol "lt" = "integer 'less than'".
819 \forall x, y, z. x < y \to y < z \to x < z.
822 The ``alias'' command in the example sets the preferred alias for the
825 Implicit preferences for new concepts are set since a concept just defined is
826 likely to be the preferred one in the rest of the script. Implicit preferences
827 learned from disambiguation of previous commands grant the coherence of
828 the disambiguation in the rest of the script and speed up disambiguation
829 reducing the search space.
831 Disambiguation preferences are included in the lexicon status
832 (see Sect.~\ref{sec:presentationintro} that is part of the authoring interface
833 status. Unlike aliases, they are not part of the library.
835 When starting a new authoring session the set of disambiguation preferences
836 is empty. Until it contains a preference for each overloaded symbol to be
837 used in the script, the user can be faced with questions from the disambiguator.
838 To reduce the likelyhood of user interactions, we introduced
839 the \texttt{include} command. With \texttt{include} it is possible to import
840 at once in the current session the set of preferences that was in effect
841 at the end of the execution of a given script.
843 Preferences can be changed. For instance, at the start of the development
844 of integer numbers the preference for the symbol \OP{<} is likely
845 to be the one over natural numbers; sooner or later it will be set to the one
846 over integer numbers.
848 Nothing forbids the set of preferences to become incoherent. For this reason
849 the disambiguator cannot always respect the user preferences.
850 For example consider:
853 theorem Zlt_mono: \forall x, y, k. x < y \to x < y + k.
856 No refinable partially specified term corresponds to the preferences:
857 \OP{+} over natural numbers, \OP{<} over integer numbers.
858 When the disambiguator fails, disambiguation is tried again with a less
859 strict set of preferences. Thus disambiguation is organized in
860 multiple \emph{passes}. In the first pass, called \emph{mono-preferences},
861 we consider only the aliases corresponding to the current preferences.
862 In the second pass, called \emph{multi-preferences},
863 we consider every alias corresponding to a current or past preference.
864 For instance, in the example above disambiguation succeeds in the
865 multi-preference pass
867 \TODO{Disambiguazione: cambiato solo FINQUI}
869 and suppose that the \OP{+} operator is defined only on natural numbers. If
870 the alias for \OP{<} points to the integer version of the operator, no
871 refinable partially specified term matching the term could be found.
873 For this reason we chose to attempt \emph{multiple disambiguation passes}. A
874 first pass attempts to disambiguate using the last available disambiguation
875 aliases (\emph{mono aliases} pass); in case of failure the next pass tries
876 disambiguation again forgetting the aliases and using the whole library to
877 retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
878 Since the latter pass may lead to too many choices we intertwined an additional
879 pass among the two which use as interpretations all the aliases coming for
880 included parts of the library (\emph{multi aliases} phase). This is the reason
881 why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
882 turned out to be a well-balanced trade-off among performances (earlier passes
883 fail quickly) and degree of ambiguity supported for presentation level terms.
885 \subsubsection{Operator instances}
886 \label{sec:disambinstances}
888 Let us suppose now we want to define a theorem relating ordering relations on
889 natural and integer numbers. The way we would like to write such a theorem (as
890 we can read it in the \MATITA{} standard library) is:
894 include "nat/orders.ma".
896 theorem lt_to_Zlt_pos_pos:
897 \forall n, m: nat. n < m \to pos n < pos m.
900 Unfortunately, none of the passes described above is able to disambiguate its
901 type, no matter how aliases are defined. This is because the \OP{<} operator
902 occurs twice in the content level term (it has two \emph{instances}) and two
903 different interpretations for it have to be used in order to obtain a refinable
904 partially specified term. To address this issue, we have the ability to consider
905 each instance of a single symbol as a different ambiguous expression in the
906 content level term, and thus we can assign a different interpretation to each of
907 them. A disambiguation pass which exploit this feature is said to be using
908 \emph{fresh instances}.
910 Fresh instances lead to a non negligible performance loss (since the choice of
911 an interpretation for one instances does not constraint the choice for the
912 others). For this reason we always attempt a fresh instances pass only after
913 attempting a non-fresh one.
915 \paragraph{One-shot aliases} Disambiguation aliases as seen so far are
916 instance-independent. However, aliases obtained as a result of a disambiguation
917 pass which uses fresh instances ought to be instance-dependent, that is: to
918 ensure a term can be disambiguated in a batch fashion we may need to state that
919 an \emph{i}-th instance of a symbol should be mapped to a given partially
920 specified term. Instance-depend aliases are meaningful only for the term whose
921 disambiguation generated it. For this reason we call them \emph{one-shot
922 aliases} and \MATITA{} does not use it to disambiguate further terms down in the
925 \subsubsection{Implicit coercions}
926 \label{sec:disambcoercions}
928 Let us now consider a theorem about derivation:
932 \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
935 and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
936 interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
937 Mathematicians would write the term that way since it is well known that the
938 natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
939 number for the purpose of real multiplication. The refiner of \MATITA{} supports
940 \emph{implicit coercions} for this reason: given as input the above content
941 level term, it will return a partially specified term where in place of
942 \texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
943 (assuming it has been defined as such of course).
945 Nonetheless coercions are not always desirable. For example, in disambiguating
946 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
947 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
948 among the possible partially specified term choices. For this reason in
949 \MATITA{} we always try first a disambiguation pass which require the refiner
950 not to use the coercions and only in case of failure we attempt a
951 coercion-enabled pass.
953 It is interesting to observe also the relationship among operator instances and
954 implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
955 which \MATITA{} disambiguated using fresh instances. In case there exists a
956 coercion from natural numbers to (positive) integers (which indeed does, it is
957 the \texttt{pos} constructor itself), the theorem can be disambiguated using
958 twice that coercion on the left hand side of the implication. The obtained
959 partially specified term however would not probably be the expected one, being a
960 theorem which prove a trivial implication. For this reason we choose to always
961 prefer fresh instances over implicit coercions, i.e. we always attempt
962 disambiguation passes with fresh instances and no implicit coercions before
963 attempting passes with implicit coercions.
965 \subsubsection{Disambiguation passes}
966 \label{sec:disambpasses}
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
994 \subsection{Generation and Invalidation}
995 \label{sec:libmanagement}
997 The aim of this section is to describe the way \MATITA{}
998 preserves the consistency and the availability of the library
999 using the \WHELP{} technology, in response to the user alteration or
1000 removal of mathematical objects.
1002 As already sketched in Sect.~\ref{sec:fullyintro} what we generate
1003 from a script is split among two storage media, a
1004 classical filesystem and a relational database. The former is used to
1005 store the XML encoding of the objects defined in the script, the
1006 disambiguation aliases and the interpretation and notational convention defined,
1007 while the latter is used to store all the metadata needed by
1010 While the consistency of the data store in the two media has
1011 nothing to do with the nature of
1012 the content of the library and is thus uninteresting (but really
1013 tedious to implement and keep bug-free), there is a deeper
1014 notion of mathematical consistency we need to provide. Each object
1015 must reference only defined object (i.e. each proof must use only
1016 already proved theorems).
1018 We will focus on how \MATITA{} ensures the interesting kind
1019 of consistency during the formalization of a mathematical theory,
1020 giving the user the freedom of adding, removing, modifying objects
1021 without loosing the feeling of an always visible and browsable
1024 \subsubsection{Compilation}
1026 The typechecker component guarantees that if an object is well typed
1027 it depends only on well typed objects available in the library,
1028 that is exactly what we need to be sure that the logic consistency of
1029 the library is preserved. We have only to find the right order of
1030 compilation of the scripts that compose the user development.
1032 For this purpose we provide a tool called \MATITADEP{}
1033 that takes in input the list of files that compose the development and
1034 outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
1035 The user is not asked to run \MATITADEP{} by hand, but
1036 simply to tell \MATITA{} the root directory of his development (where all
1037 script files can be found) and \MATITA{} will handle all the compilation
1038 related tasks, including dependencies calculation.
1039 To compute dependencies it is enough to look at the script files for
1040 inclusions of other parts of the development or for explicit
1041 references to other objects (i.e. with explicit aliases, see
1042 \ref{sec:disambaliases}).
1044 The output of the compilation is immediately available to the user
1045 trough the \WHELP{} technology, since all metadata are stored in a
1046 user-specific area of the database where the search engine has read
1047 access, and all the automated tactics that operates on the whole
1048 library, like \AUTO, have full visibility of the newly defined objects.
1050 Compilation is rather simple, and the only tricky case is when we want
1051 to compile again the same script, maybe after the removal of a
1052 theorem. Here the policy is simple: clean the output before recompiling.
1053 As we will see in the next section cleaning will ensure that
1054 there will be no theorems in the development that depends on the
1057 \subsubsection{Cleaning}
1059 With the term ``cleaning'' we mean the process of removing all the
1060 results of an object compilation. In order to keep the consistency of
1061 the library, cleaning an object requires the (recursive) cleaning
1062 of all the objects that depend on it (\emph{reverse dependencies}).
1064 The calculation of the reverse dependencies can be computed in two
1065 ways, using the relational database or using a simpler set of metadata
1066 that \MATITA{} saves in the filesystem as a result of compilation. The
1067 former technique is the same used by the \emph{Dependency Analyzer}
1068 described in~\cite{zack-master} and really depends on a relational
1071 The latter is a fall-back in case the database is not
1072 available.\footnote{Due to the complex deployment of a large piece of
1073 software like a database, it is a common practice for the \HELM{} team
1074 to use a shared remote database, that may be unavailable if the user
1075 workstation lacks network connectivity.} This facility has to be
1076 intended only as a fall-back, since the queries of the \WHELP{}
1077 technology depend require a working database.
1079 Cleaning guarantees that if an object is removed there are no dandling
1080 references to it, and that the part of the library still compiled is
1081 consistent. Since cleaning involves the removal of all the results of
1082 the compilation, metadata included, the library browsable trough the
1083 \WHELP{} technology is always kept up to date.
1085 \subsubsection{Batch vs Interactive}
1087 \MATITA{} includes an interactive authoring interface and a batch
1088 ``compiler'' (\MATITAC). Only the former is intended to be used directly by the
1089 user, the latter is automatically invoked when a
1090 part of the user development is required (for example issuing an
1091 \texttt{include} command) but not yet compiled.
1093 While they share the same engine for compilation and cleaning, they
1094 provide different granularity. The batch compiler is only able to
1095 compile a whole script and similarly to clean only a whole script
1096 (together with all the other scripts that rely on an object defined in
1097 it). The interactive interface is able to execute single steps of
1098 compilation, that may include the definition of an object, and
1099 similarly to undo single steps. Note that in the latter case there is
1100 no risk of introducing dangling references since the \MATITA{} user
1101 interface inhibit undoing a step which is not the last executed.
1103 \subsection{Automation}
1104 \label{sec:automation}
1106 \TODO{sezione sull'automazione}
1108 \subsection{Naming convention}
1111 A minor but not entirely negligible aspect of \MATITA{} is that of
1112 adopting a (semi)-rigid naming convention for identifiers, derived by
1113 our studies about metadata for statements.
1114 The convention is only applied to identifiers for theorems
1115 (not definitions), and relates the name of a proof to its statement.
1116 The basic rules are the following:
1118 \item each identifier is composed by an ordered list of (short)
1119 names occurring in a left to right traversal of the statement;
1120 \item all identifiers should (but this is not strictly compulsory)
1121 separated by an underscore,
1122 \item identifiers in two different hypothesis, or in an hypothesis
1123 and in the conclusion must be separated by the string ``\verb+_to_+'';
1124 \item the identifier may be followed by a numerical suffix, or a
1125 single or double apostrophe.
1128 Take for instance the theorem
1129 \[\forall n:nat. n = plus \; n\; O\]
1130 Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
1131 \verb+eq_n_plus_n_O+ and so on.
1132 Similarly, consider the theorem
1133 \[\forall n,m:nat. n<m \to n \leq m\]
1134 In this case \verb+lt_to_le+ is a legal name,
1135 while \verb+lt_le+ is not.\\
1136 But what about, say, the symmetric law of equality? Probably you would like
1137 to name such a theorem with something explicitly recalling symmetry.
1138 The correct approach,
1139 in this case, is the following. You should start with defining the
1140 symmetric property for relations
1142 \[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
1144 Then, you may state the symmetry of equality as
1145 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
1146 and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
1147 So, somehow unexpectedly, the introduction of semi-rigid naming convention
1148 has an important beneficial effect on the global organization of the library,
1149 forcing the user to define abstract notions and properties before
1150 using them (and formalizing such use).
1152 Two cases have a special treatment. The first one concerns theorems whose
1153 conclusion is a (universally quantified) predicate variable, i.e.
1154 theorems of the shape
1155 $\forall P,\dots.P(t)$.
1156 In this case you may replace the conclusion with the word
1157 ``elim'' or ``case''.
1158 For instance the name \verb+nat_elim2+ is a legal name for the double
1159 induction principle.
1161 The other special case is that of statements whose conclusion is a
1163 A typical example is the following
1166 match (eqb n m) with
1167 [ true \Rightarrow n = m
1168 | false \Rightarrow n \neq m]
1170 where $eqb$ is boolean equality.
1171 In this cases, the name can be build starting from the matched
1172 expression and the suffix \verb+_to_Prop+. In the above example,
1173 \verb+eqb_to_Prop+ is accepted.
1175 \section{The authoring interface}
1176 \label{sec:authoring}
1178 The authoring interface of \MATITA{} is very similar to Proof General. We
1179 chose not to build the \MATITA{} UI over Proof General for two reasons. First
1180 of all we wanted to integrate our XML-based rendering technologies, mainly
1181 \GTKMATHVIEW{}. At the time of writing Proof General supports only text based
1182 rendering.\footnote{This may change with the future release of Proof General
1183 based on Eclipse, but is not yet the case.} The second reason is that we wanted
1184 to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
1187 Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
1188 featuring two windows. The background one is very like to the Proof General
1189 interface. The main difference is that we use the \GTKMATHVIEW{} widget to
1190 render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
1191 advantage of the whole bidimensional mathematical notation.
1193 The foreground window, also implemented around \GTKMATHVIEW, is called
1194 ``cicBrowser''. It is used to browse the library, including the proof being
1195 developed, and enable content based search over it. Proofs are rendered in
1196 natural language, automatically generated from the low-level lambda-terms,
1197 using techniques inspired by~\cite{natural,YANNTHESIS} and already described
1198 in~\cite{remathematization}.
1200 Note that the syntax used in the script view is \TeX-like, however Unicode is
1201 fully supported so that mathematical glyphs can be input as such.
1205 \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
1206 \caption{\MATITA{} look and feel}
1207 \label{fig:screenshot}
1211 Since the concepts of script based proof authoring are well-known, the
1212 remaining part of this section is dedicated to the distinguishing
1213 features of the \MATITA{} authoring interface.
1215 \subsection{Direct manipulation of terms}
1216 \label{sec:directmanip}
1218 While terms are input as \TeX-like formulae in \MATITA, they are converted to a
1219 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
1220 \GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
1221 high-quality bidimensional rendering of terms (including the use of fancy
1222 layout schemata like radicals and matrices) and the use of a
1223 concise and widespread textual syntax.
1225 Keeping pointers from the presentations level terms down to the
1226 partially specified ones \MATITA{} enable direct manipulation of
1227 rendered (sub)terms in the form of hyperlinks and semantic selection.
1229 \emph{Hyperlinks} have anchors on the occurrences of constant and
1230 inductive type constructors and point to the corresponding definitions
1231 in the library. Anchors are available notwithstanding the use of
1232 user-defined mathematical notation: as can be seen on the right of
1233 Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
1234 encoding complex notations retain all the hyperlinks of constants or
1235 constructors used in the notation.
1237 \emph{Semantic selection} enables the selection of mixed
1238 \MATHML+\BOXML{} markup, constraining the selection to markup
1239 representing meaningful CIC (sub)terms. In the example on the left of
1240 Fig.~\ref{fig:directmanip} is thus possible to select the subterm
1241 $\mathrm{prime}~n$, whereas it would not be possible to select
1242 $\to n$ since the former denotes an application while the
1243 latter it not a subterm. Once a meaningful (sub)term has been
1244 selected actions can be done on it like reductions or tactic
1249 \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
1250 \hspace{0.05\textwidth}
1251 \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
1252 \caption{Semantic selection and hyperlinks}
1253 \label{fig:directmanip}
1257 \TODO{referenziarli e spostarli nella parte sulla libreria?}
1261 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
1262 \hspace{0.02\textwidth}
1263 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
1264 \hspace{0.02\textwidth}
1265 \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}
1266 \caption{Browsing and searching the library}
1267 \label{fig:cicbrowser}
1271 \subsection{Patterns}
1272 \label{sec:patterns}
1274 In several situations working with direct manipulation of terms is
1275 simpler and faster than typing the corresponding textual
1276 commands~\cite{proof-by-pointing}.
1277 Nonetheless we need to record actions and selections in scripts.
1279 In \MATITA{} \emph{patterns} are textual representations of selections.
1280 Users can select using the GUI and then ask the system to paste the
1281 corresponding pattern in this script, but more often this process is
1282 transparent: once an action is performed on a selection, the corresponding
1283 textual command is computed and inserted in the script.
1285 \subsubsection{Pattern syntax}
1287 Patterns are composed of two parts: \NT{sequent\_path} and
1288 \NT{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
1290 \NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
1291 with $?$ and selecting the interesting parts with the placeholder
1292 $\%$. \NT{wanted} is a term that lives in the context of the
1295 Textual patterns produced from a graphical selection are made of the
1296 \NT{sequent\_path} only. Such patterns can represent every selection,
1297 but are quite verbose. The \NT{wanted} part of the syntax is meant to
1298 help the users in writing concise and elegant patterns by hand.
1301 \caption{Patterns concrete syntax.\strut}
1305 \begin{array}{@{}rcll@{}}
1307 ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
1308 \NT{sequent\_path} &
1309 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
1310 [~\verb+\vdash+~\NT{multipath}~] & \\
1311 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
1312 \NT{wanted} & ::= & \NT{term} & \\
1318 \subsubsection{Pattern evaluation}
1320 Patterns are evaluated in two phases. The first selects roots
1321 (subterms) of the sequent, using the $\NT{sequent\_path}$, while the
1322 second searches the $\NT{wanted}$ term starting from these roots.
1323 % Both are optional steps, and by convention the empty pattern selects
1324 % the whole conclusion.
1328 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
1329 part of the syntax. $\NT{ident}$ is an hypothesis name and
1330 selects the assumption where the following optional $\NT{multipath}$
1331 will operate. \verb+\vdash+ can be considered the name for the goal.
1332 If the whole pattern is omitted, the whole goal will be selected.
1333 If one or more hypotheses names are given the selection is restricted to
1334 these assumptions. If a $\NT{multipath}$ is omitted the whole
1335 assumption is selected. Remember that the user can be mostly
1336 unaware of this syntax, since the system is able to write down a
1337 $\NT{sequent\_path}$ starting from a visual selection.
1338 \NOTE{Questo ancora non va in matita}
1340 A $\NT{multipath}$ is a CIC term in which a special constant $\%$
1342 The roots of discharged subterms are marked with $?$, while $\%$
1343 is used to select roots. The default $\NT{multipath}$, the one that
1344 selects the whole term, is simply $\%$.
1345 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
1346 that respectively select the first argument of an application or
1347 the source of an arrow and the head of the application that is
1348 found in the arrow target.
1350 The first phase not only selects terms (roots of subterms) but
1351 determines also their context that will be eventually used in the
1355 plays a role only if the $[~\verb+match+~\NT{wanted}~]$
1356 part is specified. From the first phase we have some terms, that we
1357 will see as subterm roots, and their context. For each of these
1358 contexts the $\NT{wanted}$ term is disambiguated in it and the
1359 corresponding root is searched for a subterm that can be unified to
1360 $\NT{wanted}$. The result of this search is the selection the
1365 \subsubsection{Examples}
1366 %To explain how the first phase works let us give an example. Consider
1367 %you want to prove the uniqueness of the identity element $0$ for natural
1368 %sum, and that you can rely on the previously demonstrated left
1369 %injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
1372 %theorem valid_name: \forall n,m. m + n = n \to m = O.
1376 Consider the following sequent
1384 To change the right part of the equivalence of the $H$
1385 hypothesis with $O + n$ the user selects and pastes it as the pattern
1386 in the following statement.
1388 change in H:(? ? ? %) with (O + n).
1391 To understand the pattern (or produce it by hand) the user should be
1392 aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
1393 that the pattern selects only the third argument of $eq$.
1395 The experienced user may also write by hand a concise pattern
1396 to change at once all the occurrences of $n$ in the hypothesis $H$:
1398 change in H match n with (O + n).
1401 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
1402 the second phase locates $n$.
1404 The latter pattern is equivalent to the following one, that the system
1405 can automatically generate from the selection.
1407 change in H:(? ? (? ? %) %) with (O + n).
1411 \subsubsection{Tactics supporting patterns}
1413 \TODO{mergiare con il successivo facendo notare che i patterns sono una
1414 interfaccia comune per le tattiche}
1416 In \MATITA{} all the tactics that can be restricted to subterm of the working
1417 sequent accept the pattern syntax. In particular these tactics are: simplify,
1418 change, fold, unfold, generalize, replace and rewrite.
1420 \NOTE{attualmente rewrite e fold non supportano phase 2. per
1421 supportarlo bisogna far loro trasformare il pattern phase1+phase2
1422 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
1423 con una pattern\_of(select(pattern))}
1425 \subsubsection{Comparison with \COQ{}}
1427 \COQ{} has two different ways of restricting the application of tactics to
1428 subterms of the sequent, both relaying on the same special syntax to identify
1431 The first way is to use this special syntax to tell the
1432 tactic what occurrences of a wanted term should be affected.
1433 The second is to prepare the sequent with another tactic called
1434 pattern and then apply the real tactic. Note that the choice is not
1435 left to the user, since some tactics needs the sequent to be prepared
1436 with pattern and do not accept directly this special syntax.
1438 The base idea is that to identify a subterm of the sequent we can
1439 write it and say that we want, for example, the third and the fifth
1440 occurrences of it (counting from left to right). In our previous example,
1441 to change only the left part of the equivalence, the correct command
1445 change n at 2 in H with (O + n)
1448 meaning that in the hypothesis $H$ the $n$ we want to change is the
1449 second we encounter proceeding from left to right.
1451 The tactic pattern computes a
1452 $\beta$-expansion of a part of the sequent with respect to some
1453 occurrences of the given term. In the previous example the following
1459 would have resulted in this sequent:
1464 H : (fun n0 : nat => m + n = n0) n
1465 ============================
1469 where $H$ is $\beta$-expanded over the second $n$
1472 At this point, since Coq unification algorithm is essentially
1473 first-order, the application of an elimination principle (of the
1474 form $\forall P.\forall x.(H~x)\to (P~x)$) will unify
1475 $x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
1477 Since rewriting, replacing and several other tactics boils down to
1478 the application of the equality elimination principle, the previous
1479 trick deals the expected behaviour.
1481 The idea behind this way of identifying subterms in not really far
1482 from the idea behind patterns, but fails in extending to
1483 complex notation, since it relays on a mono-dimensional sequent representation.
1484 Real math notation places arguments upside-down (like in indexed sums or
1485 integrations) or even puts them inside a bidimensional matrix.
1486 In these cases using the mouse to select the wanted term is probably the
1487 more effective way to tell the system what to do.
1489 One of the goals of \MATITA{} is to use modern publishing techniques, and
1490 adopting a method for restricting tactics application domain that discourages
1491 using heavy math notation, would definitively be a bad choice.
1493 \subsection{Tacticals}
1494 \label{sec:tinycals}
1496 There are mainly two kinds of languages used by proof assistants to recorder
1497 proofs: tactic based and declarative. We will not investigate the philosophy
1498 around the choice that many proof assistant made, \MATITA{} included, and we
1499 will not compare the two different approaches. We will describe the common
1500 issues of the tactic-based language approach and how \MATITA{} tries to solve
1503 \subsubsection{Tacticals overview}
1505 Tacticals first appeared in LCF and can be seen as programming
1506 constructs, like looping, branching, error recovery or sequential composition.
1507 The following simple example shows three tacticals in action
1511 A = B \to ((A \to B) \land (B \to A)).
1514 [ rewrite < H. assumption.
1515 | rewrite > H. assumption.
1520 The first is ``\texttt{;}'' that combines the tactic \texttt{split}
1521 with \texttt{intro}, applying the latter to each goal opened by the
1522 former. Then we have ``\texttt{[}'' that branches on the goals (here
1523 we have two goals, the two sides of the logic and).
1524 The first goal $B$ (with $A$ in the context)
1525 is proved by the first sequence of tactics
1526 \texttt{rewrite} and \texttt{assumption}. Then we move to the second
1527 goal with the separator ``\texttt{|}''. The last tactical we see here
1528 is ``\texttt{.}'' that is a sequential composition that selects the
1529 first goal opened for the following tactic (instead of applying it to
1530 them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
1531 not considered a tactical, but a sentence terminator (i.e. the
1532 delimiter of commands the proof assistant executes).
1534 Giving serious examples here is rather difficult, since they are hard
1535 to read without the interactive tool. To help the reader in
1536 understanding the following considerations we just give few common
1537 usage examples without a proof context.
1540 elim z; try assumption; [ ... | ... ].
1541 elim z; first [ assumption | reflexivity | id ].
1544 The first example goes by induction on a term \texttt{z} and applies
1545 the tactic \texttt{assumption} to each opened goal eventually recovering if
1546 \texttt{assumption} fails. Here we are asking the system to close all
1547 trivial cases and then we branch on the remaining with ``\texttt{[}''.
1548 The second example goes again by induction on \texttt{z} and tries to
1549 close each opened goal first with \texttt{assumption}, if it fails it
1550 tries \texttt{reflexivity} and finally \texttt{id}
1551 that is the tactic that leaves the goal untouched without failing.
1553 Note that in the common implementation of tacticals both lines are
1554 compositions of tacticals and in particular they are a single
1555 statement (i.e. derived from the same non terminal entry of the
1556 grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
1557 this is not true, since each atomic tactic or punctuation is considered
1560 \subsubsection{Common issues of tactic(als)-based proof languages}
1561 We will examine the two main problems of tactic(als)-based proof script:
1562 maintainability and readability.
1564 Huge libraries of formal mathematics have been developed, and backward
1565 compatibility is a really time consuming task. \\
1566 A real-life example in the history of \MATITA{} was the reordering of
1567 goals opened by a tactic application. We noticed that some tactics
1568 were not opening goals in the expected order. In particular the
1569 \texttt{elim} tactic on a term of an inductive type with constructors
1570 $c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
1571 \ldots, g_2$. The library of \MATITA{} was still in an embryonic state
1572 but some theorems about integers were there. The inductive type of
1573 $\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
1574 induction proofs on this type where written without tacticals and,
1575 obviously, considering the three induction cases in the wrong order.
1576 Fixing the behavior of the tactic broke the library and two days of
1577 work were needed to make it compile again. The whole time was spent in
1578 finding the list of tactics used to prove the third induction case and
1579 swap it with the list of tactics used to prove the second case. If
1580 the proofs was structured with the branch tactical this task could
1581 have been done automatically.
1583 From this experience we learned that the use of tacticals for
1584 structuring proofs gives some help but may have some drawbacks in
1585 proof script readability. We must highlight that proof scripts
1586 readability is poor by itself, but in conjunction with tacticals it
1587 can be nearly impossible. The main cause is the fact that in proof
1588 scripts there is no trace of what you are working on. It is not rare
1589 for two different theorems to have the same proof script (while the
1590 proof is completely different).\\
1591 Bad readability is not a big deal for the user while he is
1592 constructing the proof, but is considerably a problem when he tries to
1593 reread what he did or when he shows his work to someone else. The
1594 workaround commonly used to read a script is to execute it again
1595 step-by-step, so that you can see the proof goal changing and you can
1596 follow the proof steps. This works fine until you reach a tactical. A
1597 compound statement, made by some basic tactics glued with tacticals,
1598 is executed in a single step, while it obviously performs lot of proof
1599 steps. In the fist example of the previous section the whole branch
1600 over the two goals (respectively the left and right part of the logic
1601 and) result in a single step of execution. The workaround does not work
1602 anymore unless you de-structure on the fly the proof, putting some
1603 ``\texttt{.}'' where you want the system to stop.\\
1605 Now we can understand the tradeoff between script readability and
1606 proof structuring with tacticals. Using tacticals helps in maintaining
1607 scripts, but makes it really hard to read them again, cause of the way
1610 \MATITA{} uses a language of tactics and tacticals, but tries to avoid
1611 this tradeoff, alluring the user to write structured proof without
1612 making it impossible to read them again.
1614 \subsubsection{The \MATITA{} approach: Tinycals}
1617 \caption{Concrete syntax of \MATITA{} tacticals.\strut}
1621 \begin{array}{@{}rcll@{}}
1623 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
1625 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
1626 \NT{block\_delimiter} &
1627 ::= & \verb+begin+ ~|~ \verb+end+ & \\
1629 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
1635 \MATITA{} tacticals syntax is reported in Tab.~\ref{tab:tacsyn}.
1636 While one would expect to find structured constructs like
1637 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
1638 This is essential for base idea behind \MATITA{} tacticals: step-by-step
1641 The low-level tacticals implementation of \MATITA{} allows a step-by-step
1642 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
1643 not executed as an atomic operation. This has two major benefits for the user,
1644 even being a so simple idea:
1646 \item[Proof structuring]
1647 is much easier. Consider for example a proof by induction, and imagine you
1648 are using classical tacticals in one of the state of the
1649 art graphical interfaces for proof assistant like Proof General or \COQIDE.
1650 After applying the induction principle you have to choose: structure
1651 the proof or not. If you decide for the former you have to branch with
1652 ``\texttt{[}'' and write tactics for all the cases separated by
1653 ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
1654 You can replace most of the cases by the identity tactic just to
1655 concentrate only on the first goal, but you will have to go one step back and
1656 one further every time you add something inside the tactical. Again this is
1657 caused by the one step execution of tacticals and by the fact that to modify
1658 the already executed script you have to undo one step.
1659 And if you are board of doing so, you will finish in giving up structuring
1660 the proof and write a plain list of tactics.\\
1661 With step-by-step tacticals you can apply the induction principle, and just
1662 open the branching tactical ``\texttt{[}''. Then you can interact with the
1663 system reaching a proof of the first case, without having to specify any
1664 tactic for the other goals. When you have proved all the induction cases, you
1665 close the branching tactical with ``\texttt{]}'' and you are done with a
1666 structured proof. \\
1667 While \MATITA{} tacticals help in structuring proofs they allow you to
1668 choose the amount of structure you want. There are no constraints imposed by
1669 the system, and if the user wants he can even write completely plain proofs.
1672 is possible. Going on step by step shows exactly what is going on. Consider
1673 again a proof by induction, that starts applying the induction principle and
1674 suddenly branches with a ``\texttt{[}''. This clearly separates all the
1675 induction cases, but if the square brackets content is executed in one single
1676 step you completely loose the possibility of rereading it and you have to
1677 temporary remove the branching tactical to execute in a satisfying way the
1678 branches. Again, executing step-by-step is the way you would like to review
1679 the demonstration. Remember that understanding the proof from the script is
1680 not easy, and only the execution of tactics (and the resulting transformed
1681 goal) gives you the feeling of what is going on.
1684 \section{Standard library}
1687 \MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
1688 can be read, checked and referenced in further developments.
1689 However, in order to test the actual usability of the system, a
1690 new library of results has been started from scratch. In this case,
1691 of course, we wrote (and offer) the source script files,
1692 while, in the case of \COQ, \MATITA{} may only rely on XML files of
1694 The current library just comprises about one thousand theorems in
1695 elementary aspects of arithmetics up to the multiplicative property for
1696 Eulers' totient function $\phi$.
1697 The library is organized in five main directories: \texttt{logic} (connectives,
1698 quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
1699 constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
1700 (rationals). The most complex development is \texttt{nat}, organized in 25
1701 scripts, listed in Tab.~\ref{tab:scripts}.
1704 \begin{tabular}{lll}
1705 \FILE{nat.ma} & \FILE{plus.ma} & \FILE{times.ma} \\
1706 \FILE{minus.ma} & \FILE{exp.ma} & \FILE{compare.ma} \\
1707 \FILE{orders.ma} & \FILE{le\_arith.ma} & \FILE{lt\_arith.ma} \\
1708 \FILE{factorial.ma} & \FILE{sigma\_and\_pi.ma} & \FILE{minimization.ma} \\
1709 \FILE{div\_and\_mod.ma} & \FILE{gcd.ma} & \FILE{congruence.ma} \\
1710 \FILE{primes.ma} & \FILE{nth\_prime.ma} & \FILE{ord.ma} \\
1711 \FILE{count.ma} & \FILE{relevant\_equations.ma} & \FILE{permutation.ma} \\
1712 \FILE{factorization.ma} & \FILE{chinese\_reminder.ma} &
1713 \FILE{fermat\_little\_th.ma} \\
1714 \FILE{totient.ma} & & \\
1716 \caption{Scripts on natural numbers in the standard library}
1720 We do not plan to maintain the library in a centralized way,
1721 as most of the systems do. On the contrary we are currently
1722 developing wiki-technologies to support a collaborative
1723 development of the library, encouraging people to expand,
1724 modify and elaborate previous contributions.
1726 \section{Conclusions}
1727 \label{sec:conclusion}
1732 We would like to thank all the students that during the past
1733 five years collaborated in the \HELM{} project and contributed to
1734 the development of \MATITA{}, and in particular
1735 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
1740 \bibliography{matita}