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