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