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 formal 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 Formal 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.
725 In the remaining part of the paper we focus on the user view of \MATITA.
726 This section is devoted to the aspects of the tool that arise from the
727 document centric approach to the library. Sect.~\ref{sec:authoring} describes
728 the peculiarities of the authoring interface.
730 The library of \MATITA{} comprises mathematical concepts (theorems,
731 axioms, definitions) and notation. The concepts are authored sequentially
732 using scripts that are (ordered) sequences of procedural commands.
733 However, once they are produced we store them independently in the library.
734 The only relation implicitly kept between the concepts are the logical,
735 acyclic dependencies among them. This way the library forms a global (and
736 distributed) hypertext.
740 \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-browsing}
741 \hspace{0.05\textwidth}
742 \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-query}
743 \caption{Browsing and searching the library\strut}
744 \label{fig:cicbrowser1}
750 \includegraphics[width=0.70\textwidth]{pics/cicbrowser-screenshot-con}
751 \caption[Natural language rendering]{Natural language rendering of a theorem
752 from the library\strut}
753 \label{fig:cicbrowser2}
757 Several useful operations can be implemented on the library only,
758 regardless of the scripts. For instance, searching and browsing is
759 implemented by the ``cicBrowser'' window available from the \MATITA{}
760 GUI. Using it, the hierarchical structure of the library can be
761 explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural
762 language rendering of proofs can be inspected
763 (Fig.~\ref{fig:cicbrowser2}), and content based searches on the
764 library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}).
765 Available content based searches are described in
766 Sect.~\ref{sec:indexing}. Other examples of library operations are
767 disambiguation of content level terms (see
768 Sect.~\ref{sec:disambiguation}) and automatic proof searching (see
769 Sect.~\ref{sec:automation}).
771 The key requisite for the previous operations is that the library must
772 be fully accessible and in a logically consistent state. To preserve
773 consistency, a concept cannot be altered or removed unless the part of the
774 library that depends on it is modified accordingly. To allow incremental
775 changes and cooperative development, consistent revisions are necessary.
776 For instance, to modify a definition, the user could fork a new version
777 of the library where the definition is updated and all the concepts that
778 used to rely on it are absent. The user is then responsible to restore
779 the removed part in the new branch, merging the branch when the library is
782 To implement the proposed versioning system on top of a standard one
783 it is necessary to implement \emph{invalidation} first. Invalidation
784 is the operation that locates and removes from the library all the concepts
785 that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
786 a concept from the library also involves deleting its metadata from the
789 For non collaborative development, full versioning can be avoided, but
790 invalidation is still required. Since nobody else is relying on the
791 user development, the user is free to change and invalidate part of the library
792 without branching. Invalidation is still necessary to avoid using a
793 concept that is no longer valid.
794 So far, in \MATITA{} we address only this non collaborative scenario
795 (see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
796 is still under design.
798 Scripts are not seen as constituents of the library. They are not published
799 and indexed, so they cannot be searched or browsed using \HELM{} tools.
800 However, they play a central role for the maintenance of the library.
801 Indeed, once a concept is invalidated, the only way to restore it is to
802 fix the possibly broken script that used to generate it.
803 Moreover, during the authoring phase, scripts are a natural way to
804 group concepts together. They also constitute a less fine grained clustering
805 of concepts for invalidation.
807 In the rest of this section we present in more details the functionalities of
808 \MATITA{} related to library management and exploitation.
809 Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
810 the \MATITA{} authoring interface.
812 \subsection{Indexing and searching}
815 The \MATITA{} system is first of all an interface between the user and
816 the mathematical library. For this reason, it is important to be
817 able to search and retrieve mathematical concepts in a quick and
818 effective way, assuming as little knowledge as possible about the
819 library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
820 for mathematical concepts, based on a rich metadata set that has been
821 tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
822 set, and the searching facilites built on top of them --- collected
823 in the so called \WHELP{} search engine --- have been
824 extensively described in~\cite{whelp}. Let us just recall here that
825 the \WHELP{} metadata model is essentially based a single ternary relation
826 \REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
827 given position $p$, where the position specify the place of the
828 occurrence of $t$ inside $s$ (we currently work with a fixed set of
829 positions, discriminating the hypothesis from the conclusion and
830 outermost form innermost occurrences). This approach is extremely
831 flexible, since extending the set of positions
832 we may improve the granularity and the precision of our indexing technique,
833 with no additional architectural impact.
835 Every time a new mathematical concept is created and saved by the user it gets
836 indexed, and becomes immediately visible in the library. Several
837 interesting and innovative features of \MATITA{} described in the following
838 sections rely in a direct or indirect way on its metadata system and
839 the search features. Here, we shall just recall some of its most
842 A first, very simple but not negligeable feature is the check for duplicates.
843 As soon as a theorem is stated, just before starting its proof,
844 the library is searched
845 to check that no other equivalent statement has been already proved
846 (based on the pattern matching functionality of \WHELP); if this is the case,
847 a warning is raised to the user. At present, the notion of equivalence
848 adopted by \MATITA{} is convertibility, but we may imagine to weaken it
849 in the future, covering for instance isomorphisms.
851 Another useful \WHELP{} operation is \HINT; we may invoke this query
852 at any moment during the authoring of a proof, resulting in the list
853 of all theorems of the library which can be applied to the current
854 goal. In practice, this is mostly used not really to discover what theorems
855 can be applied to a given goal, but to actually retrieve a theorem that
856 we wish to apply, but whose name we have forgotten.
857 In fact, even if \MATITA{} adopts a semi-rigid naming convention for
858 statements (see Sect.~\ref{sec:naming}) that greatly simplifies the effort
859 of recalling names, the naming discipline remains one of the most
860 annoying aspects of formal developments, and \HINT{} provides
861 a very friendly solution.
862 In the near feature, we expect to extend the \HINT{} operation to
863 a \REWRITEHINT, resulting in all equational statements that
864 can be applied to rewrite the current goal.
866 \subsection{Disambiguation}
867 \label{sec:disambiguation}
869 Software applications that involve input of mathematical content should strive
870 to require the user as less drift from informal mathematics as possible. We
871 believe this to be a fundamental aspect of such applications user interfaces.
872 Being that drift in general very large when inputing
873 proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
874 mathematical formulae which can be input using a \TeX-like encoding (the
875 concrete syntax corresponding to presentation level terms) and are then
876 translated (in multiple steps) to partially specified terms as sketched in
877 Sect.~\ref{sec:contentintro}.
879 The key component of the translation is the generic disambiguation algorithm
880 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
881 and presented in~\cite{disambiguation}. In this section we present how to use
882 that algorithm in the context of the development of a library of formalized
883 mathematics. We will see that using multiple passes of the algorithm, varying
884 some of its parameters, helps in keeping the input terse without sacrificing
887 \subsubsection{Disambiguation aliases}
888 \label{sec:disambaliases}
890 Consider the following command to state a theorem over integer numbers:
894 \forall x, y, z. x < y \to y < z \to x < z.
897 The symbol \OP{<} is likely to be overloaded in the library
898 (at least over natural numbers).
899 Thus, according to the disambiguation algorithm, two different
900 refinable partially specified terms could be associated to it.
901 \MATITA{} asks the user what interpretation he meant. However, to avoid
902 posing the same question in case of a future re-execution (e.g. undo/redo),
903 the choice must be recorded. Since scripts need to be re-executed after
904 invalidation, the choice record must be permanently stored somewhere. The most
905 natural place is in the script itself.
907 In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
908 They are mappings, stored in the library, from ambiguity sources
909 (identifiers, symbols and literal numbers at the content level) to partially
910 specified terms. In case of overloaded sources there exists multiple aliases
911 with the same source. It is possible to record \emph{disambiguation
912 preferences} to select one of the aliases of an overloaded source.
914 Preferences can be explicitely given in the script (using the
915 misleading \texttt{alias} commands), but
916 are also implicitly added when a new concept is introduced (\emph{implicit
917 preferences}) or after a sucessfull disambiguation that did not require
918 user interaction. Explicit preferences are added automatically by \MATITA{} to
919 record the disambiguation choices of the user. For instance, after the
920 disambiguation of the command above, the script is altered as follows:
923 alias symbol "lt" = "integer 'less than'".
925 \forall x, y, z. x < y \to y < z \to x < z.
928 The ``alias'' command in the example sets the preferred alias for the
931 Implicit preferences for new concepts are set since a concept just defined is
932 likely to be the preferred one in the rest of the script. Implicit preferences
933 learned from disambiguation of previous commands grant the coherence of
934 the disambiguation in the rest of the script and speed up disambiguation
935 reducing the search space.
937 Disambiguation preferences are included in the lexicon status
938 (see Sect.~\ref{sec:presentationintro}) that is part of the authoring interface
939 status. Unlike aliases, they are not part of the library.
941 When starting a new authoring session the set of disambiguation preferences
942 is empty. Until it contains a preference for each overloaded symbol to be
943 used in the script, the user can be faced with questions from the disambiguator.
944 To reduce the likelyhood of user interactions, we introduced
945 the \texttt{include} command. With \texttt{include} it is possible to import
946 at once in the current session the set of preferences that was in effect
947 at the end of the execution of a given script.
949 Preferences can be changed. For instance, at the start of the development
950 of integer numbers the preference for the symbol \OP{<} is likely
951 to be the one over natural numbers; sooner or later it will be set to the one
952 over integer numbers.
954 Nothing forbids the set of preferences to become incoherent. For this reason
955 the disambiguator cannot always respect the user preferences.
956 Consider, for example:
959 \forall x, y, k. x < y \to x < y + k.
962 No refinable partially specified term corresponds to the preferences:
963 \OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
964 limitation we organized disambiguation in \emph{multiple passes}: when the
965 disambiguator fails, disambiguation is tried again with a less strict set of
968 Several disambiguation parameters can vary among passes. With respect to
969 preference handling we implemented three passes. In the first pass, called
970 \emph{mono-preferences}, we consider only the aliases corresponding to the
971 current preferences. In the second pass, called \emph{multi-preferences}, we
972 consider every alias corresponding to a current or past preference. For
973 instance, in the example above disambiguation succeeds in the multi-preference
974 pass. In the third pass, called \emph{library-preferences}, all aliases
975 available in the library are considered.
977 The rationale behind this choice is trying to respect user preferences in early
978 passes that complete quickly in case of failure; later passes are slower but
979 have more chances of success.
981 \subsubsection{Operator instances}
982 \label{sec:disambinstances}
984 Consider now the following theorem:
986 theorem lt_to_Zlt_pos_pos:
987 \forall n, m: nat. n < m \to pos n < pos m.
989 and assume that there exist in the library aliases for \OP{<} over natural
990 numbers and over integer numbers. None of the passes described above is able to
991 disambiguate \texttt{lt\_to\_Zlt\_pos\_pos}, no matter how preferences are set.
992 This is because the \OP{<} operator occurs twice in the content level term (it
993 has two \emph{instances}) and two different interpretations for it have to be
994 used in order to obtain a refinable partially specified term.
996 To address this issue, we have the ability to consider each instance of a single
997 symbol as a different ambiguous expression in the content level term, and thus
998 we can use a different alias for each of them. Exploiting or not this feature is
999 one of the disambiguation pass parameters. A disambiguation pass which exploit
1000 it is said to be using \emph{fresh instances} (opposed to a \emph{shared
1003 Fresh instances lead to a non negligible performance loss (since the choice of
1004 an alias for one instance does not constraint the choice of the others). For
1005 this reason we always attempt a fresh instances pass only after attempting a
1008 \paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
1009 instance-independent. However, implicit preferences obtained as a result of a
1010 disambiguation pass which uses fresh instances ought to be instance-dependent.
1011 Informally, the set of preferences that can be respected by the disambiguator on
1012 the theorem above is: ``the first instance of the \OP{<} symbol is over natural
1013 numbers, while the second is on integer numbers''.
1015 Instance-dependent preferences are meaningful only for the term whose
1016 disambiguation generated it. For this reason we call them \emph{one-shot
1017 preferences} and \MATITA{} does not use them to disambiguate further terms in
1020 \subsubsection{Implicit coercions}
1021 \label{sec:disambcoercions}
1023 Consider the following theorem about derivation:
1025 theorem power_deriv:
1026 \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
1028 and assume that in the library there is an alias mapping \OP{\^} to a partially
1029 specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
1030 order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
1031 right hand side of the equality need to be ``injected'' from \texttt{nat} to
1032 \texttt{R}. The refiner of \MATITA{} supports \emph{implicit coercions} 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 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 two 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 prove a trivial implication.
1053 Motivated by this and similar examples we choose to always prefer fresh
1054 instances over implicit coercions, i.e. we always attempt disambiguation
1055 passes with fresh instances
1056 and no implicit coercions before attempting passes with implicit coercions.
1058 \subsubsection{Disambiguation passes}
1059 \label{sec:disambpasses}
1061 According to the criteria described above, in \MATITA{} we perform the
1062 disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
1063 our experience that choice gives reasonable performance and minimize the need of
1064 user interaction during the disambiguation.
1067 \caption{Disambiguation passes sequence\strut}
1068 \label{tab:disambpasses}
1070 \begin{tabular}{c|c|c|c}
1071 \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
1072 & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Preferences}}
1073 & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
1074 & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
1076 \PASS & Mono-preferences & Shared instances & Disabled \\
1077 \PASS & Multi-preferences & Shared instances & Disabled \\
1078 \PASS & Mono-preferences & Fresh instances & Disabled \\
1079 \PASS & Multi-preferences & Fresh instances & Disabled \\
1080 \PASS & Mono-preferences & Fresh instances & Enabled \\
1081 \PASS & Multi-preferences & Fresh instances & Enabled \\
1082 \PASS & Library-preferences & Fresh instances & Enabled
1087 \subsection{Generation and invalidation}
1088 \label{sec:libmanagement}
1090 %The aim of this section is to describe the way \MATITA{}
1091 %preserves the consistency and the availability of the library
1092 %using the \WHELP{} technology, in response to the user alteration or
1093 %removal of mathematical objects.
1095 %As already sketched in Sect.~\ref{sec:fullyintro} what we generate
1096 %from a script is split among two storage media, a
1097 %classical filesystem and a relational database. The former is used to
1098 %store the XML encoding of the objects defined in the script, the
1099 %disambiguation aliases and the interpretation and notational convention defined,
1100 %while the latter is used to store all the metadata needed by
1103 %While the consistency of the data store in the two media has
1104 %nothing to do with the nature of
1105 %the content of the library and is thus uninteresting (but really
1106 %tedious to implement and keep bug-free), there is a deeper
1107 %notion of mathematical consistency we need to provide. Each object
1108 %must reference only defined object (i.e. each proof must use only
1109 %already proved theorems).
1111 In this section we will focus on how \MATITA{} ensures the library
1112 consistency during the formalization of a mathematical theory,
1113 giving the user the freedom of adding, removing, modifying objects
1114 without loosing the feeling of an always visible and browsable
1117 \subsubsection{Invalidation}
1119 Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
1121 The first one is the calculation of all the concepts that recursively
1122 depend on the ones we are invalidating. The calculation of the
1123 reverse dependencies can be computed using the relational database
1124 that stores 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 script files 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} tool.
1145 The user is not asked to run \MATITADEP{} by hand, but
1146 simply to tell \MATITA{} the root directory of his development (where all
1147 script files can be found) and \MATITA{} will handle all the generation
1148 related tasks, including dependencies calculation.
1150 To compute dependencies it is enough to look at the script files for
1151 disambiguation preferences declared or imported from other scripts
1152 (see \ref{sec:disambaliases}).
1154 Regenerating the content of a modified script file involves the preliminary
1155 invalidation of all its old content.
1157 \subsubsection{Batch vs Interactive}
1159 \MATITA{} includes an interactive authoring interface and a batch
1160 ``compiler'' (\MATITAC).
1162 Only the former is intended to be used directly by the
1163 user, the latter is automatically invoked by \MATITA{}
1164 to try to regenerate parts of the library previously invalidated.
1166 While they share the same engine for generation and invalidation, they
1167 provide different granularity. \MATITAC{} is only able to reexecute a
1168 whole script and similarly to invalidate the whole content of a script
1169 (together with all the other scripts that rely on an concept defined
1172 \subsection{Automation}
1173 \label{sec:automation}
1174 In the long run, one would expect to work with a Proof Assistant
1175 like Matita, using only three basic tactics: Intro, Elim, and Auto
1176 (possibly integrated by a moderate use of Cut). The state of the art
1177 in automated deduction is still far away from this goal, but
1178 this is one of the main development direction of Matita.
1180 Even in this field, the underlying phisolophy of Matita is to
1181 free the user from any burden relative to the overall management
1182 of the library. For instance, in Coq, the user is responsible to
1183 define small collections of theorems to be used as a parameter
1185 in Matita, it is the system itself that authomatically retrieves, from
1186 the whole library, a subset of theorems worth to be considered
1187 according to the signature of the current goal and context.
1189 The basic tactic merely performs an iterated use of the Apply tactic
1190 (with no Intro). The research tree may be pruned according to two
1191 main parameters: the {\em depth} (whit the obvious meaning), and the
1192 {\em width} that is the maximum number of (new) open goals allowed at
1193 any instant. Matita has only one notion of metavariable, corresponding
1194 to the so called existential variables of Coq; so, Matita's Auto tactic
1195 should be compared with Coq's EAuto.
1197 Recently we have extended automation with paramodulation based
1198 techniques. At present, the system works reasonably well with
1199 equational rewriting, where the notion of equality is parametric
1200 and can be specified by the user: the system only requires
1201 a proof of {\em reflexivity} and {\em paramodulation} (or rewriting,
1202 as it is usually called in the proof assistant community).
1204 Given an equational goal, Matita recovers all known equational facts
1205 from the library (and the local context), applying a variant of
1206 the so called {\em given-clause algorithm} \cite{paramodulation},
1207 that is the the procedure currently used by the majority of modern theorem
1210 The given-clause algorithm is essentially composed by an alternation
1211 of a {\em saturation} phase, deriving new facts by a set of active
1212 facts and a new {\em given} clause suitably selected from a set of passive
1214 and a {\em demodulation} phase that tries to simplify the equations
1215 orienting them according to a suitable weight associated with terms.
1216 Matita currently supports several different weigthing functions
1217 comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
1218 that integrates particualry well with normalization.
1220 Demodulation alone is already a quite powerful technique, and
1221 it has been turned into a tactic by itself: the {\em demodulate}
1222 tactic, which can be seen as a kind of generalization of {\em simplify}.
1223 The following portion of script describes two
1224 interesting cases of application of this tactic (both of them relying
1225 on elementary arithmetic equations):
1229 \forall x:nat. (x+1)*(x-1)=x*x - 1.
1232 [simplify;reflexivity
1233 |intro;demodulate;reflexivity]
1237 \forall x,y:nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
1238 intros;demodulate;reflexivity.
1242 In the future we expect to integrate applicative and equational
1243 rewriting. In particular, the overall idea would be to integrate
1244 applicative rewriting with demodulation, treating saturation as an
1245 operation to be performed in batch mode, e.g. during the night.
1249 \subsection{Naming convention}
1252 A minor but not entirely negligible aspect of \MATITA{} is that of
1253 adopting a (semi)-rigid naming convention for identifiers, derived by
1254 our studies about metadata for statements.
1255 The convention is only applied to identifiers for theorems
1256 (not definitions), and relates the name of a proof to its statement.
1257 The basic rules are the following:
1259 \item each identifier is composed by an ordered list of (short)
1260 names occurring in a left to right traversal of the statement;
1261 \item all identifiers should (but this is not strictly compulsory)
1262 separated by an underscore,
1263 \item identifiers in two different hypothesis, or in an hypothesis
1264 and in the conclusion must be separated by the string ``\verb+_to_+'';
1265 \item the identifier may be followed by a numerical suffix, or a
1266 single or double apostrophe.
1269 Take for instance the theorem
1270 \[\forall n:nat. n = plus \; n\; O\]
1271 Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
1272 \verb+eq_n_plus_n_O+ and so on.
1273 Similarly, consider the theorem
1274 \[\forall n,m:nat. n<m \to n \leq m\]
1275 In this case \verb+lt_to_le+ is a legal name,
1276 while \verb+lt_le+ is not.\\
1277 But what about, say, the symmetric law of equality? Probably you would like
1278 to name such a theorem with something explicitly recalling symmetry.
1279 The correct approach,
1280 in this case, is the following. You should start with defining the
1281 symmetric property for relations
1283 \[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
1285 Then, you may state the symmetry of equality as
1286 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
1287 and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
1288 So, somehow unexpectedly, the introduction of semi-rigid naming convention
1289 has an important beneficial effect on the global organization of the library,
1290 forcing the user to define abstract notions and properties before
1291 using them (and formalizing such use).
1293 Two cases have a special treatment. The first one concerns theorems whose
1294 conclusion is a (universally quantified) predicate variable, i.e.
1295 theorems of the shape
1296 $\forall P,\dots.P(t)$.
1297 In this case you may replace the conclusion with the word
1298 ``elim'' or ``case''.
1299 For instance the name \verb+nat_elim2+ is a legal name for the double
1300 induction principle.
1302 The other special case is that of statements whose conclusion is a
1304 A typical example is the following
1307 match (eqb n m) with
1308 [ true \Rightarrow n = m
1309 | false \Rightarrow n \neq m]
1311 where $eqb$ is boolean equality.
1312 In this cases, the name can be build starting from the matched
1313 expression and the suffix \verb+_to_Prop+. In the above example,
1314 \verb+eqb_to_Prop+ is accepted.
1316 \section{The authoring interface}
1317 \label{sec:authoring}
1319 The authoring interface of \MATITA{} is very similar to Proof General. We
1320 chose not to build the \MATITA{} UI over Proof General for two reasons. First
1321 of all we wanted to integrate our XML-based rendering technologies, mainly
1322 \GTKMATHVIEW. At the time of writing Proof General supports only text based
1323 rendering.\footnote{This may change with the future release of Proof General
1324 based on Eclipse, but is not yet the case.} The second reason is that we wanted
1325 to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
1328 Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
1329 featuring two windows. The background one is very like to the Proof General
1330 interface. The main difference is that we use the \GTKMATHVIEW{} widget to
1331 render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
1332 advantage of the whole bidimensional mathematical notation. The foreground
1333 window is an instance of the cicBrowser used to render the proof being
1336 Note that the syntax used in the script view is \TeX-like, however Unicode is
1337 fully supported so that mathematical glyphs can be input as such.
1341 \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
1342 \caption{Authoring interface\strut}
1343 \label{fig:screenshot}
1347 Since the concepts of script based proof authoring are well-known, the
1348 remaining part of this section is dedicated to the distinguishing
1349 features of the \MATITA{} authoring interface.
1351 \subsection{Direct manipulation of terms}
1352 \label{sec:directmanip}
1354 While terms are input as \TeX-like formulae in \MATITA, they are converted to a
1355 mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
1356 \GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
1357 high-quality bidimensional rendering of terms (including the use of fancy
1358 layout schemata like radicals and matrices) and the use of a
1359 concise and widespread textual syntax.
1361 Keeping pointers from the presentations level terms down to the
1362 partially specified ones \MATITA{} enable direct manipulation of
1363 rendered (sub)terms in the form of hyperlinks and semantic selection.
1365 \emph{Hyperlinks} have anchors on the occurrences of constant and
1366 inductive type constructors and point to the corresponding definitions
1367 in the library. Anchors are available notwithstanding the use of
1368 user-defined mathematical notation: as can be seen on the right of
1369 Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
1370 encoding complex notations retain all the hyperlinks of constants or
1371 constructors used in the notation.
1373 \emph{Semantic selection} enables the selection of mixed
1374 \MATHML+\BOXML{} markup, constraining the selection to markup
1375 representing meaningful CIC (sub)terms. In the example on the left of
1376 Fig.~\ref{fig:directmanip} is thus possible to select the subterm
1377 $\mathrm{prime}~n$, whereas it would not be possible to select
1378 $\to n$ since the former denotes an application while the
1379 latter it not a subterm. Once a meaningful (sub)term has been
1380 selected actions can be done on it like reductions or tactic
1385 \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
1386 \hspace{0.05\textwidth}
1387 \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
1388 \caption[Semantic selection and hyperlinks]{Semantic selection (on the left)
1389 and hyperlinks (on the right)\strut}
1390 \label{fig:directmanip}
1394 \subsection{Patterns}
1395 \label{sec:patterns}
1397 In several situations working with direct manipulation of terms is
1398 simpler and faster than typing the corresponding textual
1399 commands~\cite{proof-by-pointing}.
1400 Nonetheless we need to record actions and selections in scripts.
1402 In \MATITA{} \emph{patterns} are textual representations of selections.
1403 Users can select using the GUI and then ask the system to paste the
1404 corresponding pattern in this script, but more often this process is
1405 transparent: once an action is performed on a selection, the corresponding
1406 textual command is computed and inserted in the script.
1408 \subsubsection{Pattern syntax}
1410 Patterns are composed of two parts: \NT{sequent\_path} and
1411 \NT{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
1413 \NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
1414 with $?$ and selecting the interesting parts with the placeholder
1415 $\%$. \NT{wanted} is a term that lives in the context of the
1418 Textual patterns produced from a graphical selection are made of the
1419 \NT{sequent\_path} only. Such patterns can represent every selection,
1420 but are quite verbose. The \NT{wanted} part of the syntax is meant to
1421 help the users in writing concise and elegant patterns by hand.
1424 \caption{Patterns concrete syntax\strut}
1428 \begin{array}{@{}rcll@{}}
1430 ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
1431 \NT{sequent\_path} &
1432 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
1433 [~\verb+\vdash+~\NT{multipath}~] & \\
1434 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
1435 \NT{wanted} & ::= & \NT{term} & \\
1441 \subsubsection{Pattern evaluation}
1443 Patterns are evaluated in two phases. The first selects roots
1444 (subterms) of the sequent, using the $\NT{sequent\_path}$, while the
1445 second searches the $\NT{wanted}$ term starting from these roots.
1446 % Both are optional steps, and by convention the empty pattern selects
1447 % the whole conclusion.
1451 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
1452 part of the syntax. $\NT{ident}$ is an hypothesis name and
1453 selects the assumption where the following optional $\NT{multipath}$
1454 will operate. \verb+\vdash+ can be considered the name for the goal.
1455 If the whole pattern is omitted, the whole goal will be selected.
1456 If one or more hypotheses names are given the selection is restricted to
1457 these assumptions. If a $\NT{multipath}$ is omitted the whole
1458 assumption is selected. Remember that the user can be mostly
1459 unaware of this syntax, since the system is able to write down a
1460 $\NT{sequent\_path}$ starting from a visual selection.
1461 \NOTE{Questo ancora non va in matita}
1463 A $\NT{multipath}$ is a CIC term in which a special constant $\%$
1465 The roots of discharged subterms are marked with $?$, while $\%$
1466 is used to select roots. The default $\NT{multipath}$, the one that
1467 selects the whole term, is simply $\%$.
1468 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
1469 that respectively select the first argument of an application or
1470 the source of an arrow and the head of the application that is
1471 found in the arrow target.
1473 The first phase not only selects terms (roots of subterms) but
1474 determines also their context that will be eventually used in the
1478 plays a role only if the $[~\verb+match+~\NT{wanted}~]$
1479 part is specified. From the first phase we have some terms, that we
1480 will see as subterm roots, and their context. For each of these
1481 contexts the $\NT{wanted}$ term is disambiguated in it and the
1482 corresponding root is searched for a subterm that can be unified to
1483 $\NT{wanted}$. The result of this search is the selection the
1488 \subsubsection{Examples}
1489 %To explain how the first phase works let us give an example. Consider
1490 %you want to prove the uniqueness of the identity element $0$ for natural
1491 %sum, and that you can rely on the previously demonstrated left
1492 %injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
1495 %theorem valid_name: \forall n,m. m + n = n \to m = O.
1499 Consider the following sequent
1507 To change the right part of the equivalence of the $H$
1508 hypothesis with $O + n$ the user selects and pastes it as the pattern
1509 in the following statement.
1511 change in H:(? ? ? %) with (O + n).
1514 To understand the pattern (or produce it by hand) the user should be
1515 aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
1516 that the pattern selects only the third argument of $eq$.
1518 The experienced user may also write by hand a concise pattern
1519 to change at once all the occurrences of $n$ in the hypothesis $H$:
1521 change in H match n with (O + n).
1524 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
1525 the second phase locates $n$.
1527 The latter pattern is equivalent to the following one, that the system
1528 can automatically generate from the selection.
1530 change in H:(? ? (? ? %) %) with (O + n).
1533 \subsubsection{Tactics supporting patterns}
1535 \TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
1537 \TODO{mergiare con il successivo facendo notare che i patterns sono una
1538 interfaccia comune per le tattiche}
1540 In \MATITA{} all the tactics that can be restricted to subterm of the working
1541 sequent accept the pattern syntax. In particular these tactics are: simplify,
1542 change, fold, unfold, generalize, replace and rewrite.
1544 \NOTE{attualmente rewrite e fold non supportano phase 2. per
1545 supportarlo bisogna far loro trasformare il pattern phase1+phase2
1546 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
1547 con una pattern\_of(select(pattern))}
1549 \subsubsection{Comparison with \COQ{}}
1551 \COQ{} has two different ways of restricting the application of tactics to
1552 subterms of the sequent, both relaying on the same special syntax to identify
1555 The first way is to use this special syntax to tell the
1556 tactic what occurrences of a wanted term should be affected.
1557 The second is to prepare the sequent with another tactic called
1558 pattern and then apply the real tactic. Note that the choice is not
1559 left to the user, since some tactics needs the sequent to be prepared
1560 with pattern and do not accept directly this special syntax.
1562 The base idea is that to identify a subterm of the sequent we can
1563 write it and say that we want, for example, the third and the fifth
1564 occurrences of it (counting from left to right). In our previous example,
1565 to change only the left part of the equivalence, the correct command
1569 change n at 2 in H with (O + n)
1572 meaning that in the hypothesis $H$ the $n$ we want to change is the
1573 second we encounter proceeding from left to right.
1575 The tactic pattern computes a
1576 $\beta$-expansion of a part of the sequent with respect to some
1577 occurrences of the given term. In the previous example the following
1583 would have resulted in this sequent:
1588 H : (fun n0 : nat => m + n = n0) n
1589 ============================
1593 where $H$ is $\beta$-expanded over the second $n$
1596 At this point, since \COQ{} unification algorithm is essentially
1597 first-order, the application of an elimination principle (of the
1598 form $\forall P.\forall x.(H~x)\to (P~x)$) will unify
1599 $x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
1601 Since rewriting, replacing and several other tactics boils down to
1602 the application of the equality elimination principle, the previous
1603 trick deals the expected behaviour.
1605 The idea behind this way of identifying subterms in not really far
1606 from the idea behind patterns, but fails in extending to
1607 complex notation, since it relays on a mono-dimensional sequent representation.
1608 Real math notation places arguments upside-down (like in indexed sums or
1609 integrations) or even puts them inside a bidimensional matrix.
1610 In these cases using the mouse to select the wanted term is probably the
1611 more effective way to tell the system what to do.
1613 One of the goals of \MATITA{} is to use modern publishing techniques, and
1614 adopting a method for restricting tactics application domain that discourages
1615 using heavy math notation, would definitively be a bad choice.
1617 \subsection{Tacticals}
1618 \label{sec:tinycals}
1620 %There are mainly two kinds of languages used by proof assistants to recorder
1621 %proofs: tactic based and declarative. We will not investigate the philosophy
1622 %around the choice that many proof assistant made, \MATITA{} included, and we
1623 %will not compare the two different approaches. We will describe the common
1624 %issues of the tactic-based language approach and how \MATITA{} tries to solve
1627 The procedural proof language implemented in \MATITA{} is pretty standard,
1628 with a notable exception for tacticals.
1630 %\subsubsection{Tacticals overview}
1632 Tacticals first appeared in LCF as higher order tactics. They can be
1633 seen as control flow constructs, like looping, branching, error
1634 recovery or sequential composition.
1637 The following simple example
1638 shows a Coq script made of four dot-terminated commands
1643 A = B -> ((A -> B) /\ (B -> A)).
1646 [ rewrite < H; assumption
1647 | rewrite > H; assumption
1652 The third command is an application of the sequencing tactical
1653 ``$\ldots$\texttt{;}$\ldots$'', that combines the tactic
1654 \texttt{split} with the application of the branching tactical
1655 ``$\ldots$\texttt{;[}$\ldots$\texttt{|}$\ldots$\texttt{|}$\ldots$\texttt{]}''
1656 to other tactics and tacticals.
1658 The usual implementation of tacticals executes them atomically as any
1659 other command. In \MATITA{} thi is not true since each punctuation is
1660 executed as a single command.
1662 %The latter is applied to all the goals opened by \texttt{split}
1664 %(here we have two goals, the two sides of the logic and). The first
1665 %goal $B$ (with $A$ in the context) is proved by the first sequence of
1666 %tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the
1667 %second goal with the separator ``\texttt{|}''.
1669 %Giving serious examples here is rather difficult, since they are hard
1670 %to read without the interactive tool. To help the reader in
1671 %understanding the following considerations we just give few common
1672 %usage examples without a proof context.
1675 % elim z; try assumption; [ ... | ... ].
1676 % elim z; first [ assumption | reflexivity | id ].
1679 %The first example goes by induction on a term \texttt{z} and applies
1680 %the tactic \texttt{assumption} to each opened goal eventually recovering if
1681 %\texttt{assumption} fails. Here we are asking the system to close all
1682 %trivial cases and then we branch on the remaining with ``\texttt{[}''.
1683 %The second example goes again by induction on \texttt{z} and tries to
1684 %close each opened goal first with \texttt{assumption}, if it fails it
1685 %tries \texttt{reflexivity} and finally \texttt{id}
1686 %that is the tactic that leaves the goal untouched without failing.
1688 %Note that in the common implementation of tacticals both lines are
1689 %compositions of tacticals and in particular they are a single
1690 %statement (i.e. derived from the same non terminal entry of the
1691 %grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
1692 %this is not true, since each atomic tactic or punctuation is considered
1693 %a single statement.
1695 \subsubsection{Common issues of tactic(als)-based proof languages}
1696 We will examine the two main problems of tactic(als)-based proof script:
1697 maintainability and readability.
1699 %Huge libraries of formal mathematics have been developed, and backward
1700 %compatibility is a really time consuming task. \\
1701 %A real-life example in the history of \MATITA{} was the reordering of
1702 %goals opened by a tactic application. We noticed that some tactics
1703 %were not opening goals in the expected order. In particular the
1704 %\texttt{elim} tactic on a term of an inductive type with constructors
1705 %$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
1706 %\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
1707 %but some theorems about integers were there. The inductive type of
1708 %$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
1709 %induction proofs on this type where written without tacticals and,
1710 %obviously, considering the three induction cases in the wrong order.
1711 %Fixing the behavior of the tactic broke the library and two days of
1712 %work were needed to make it compile again. The whole time was spent in
1713 %finding the list of tactics used to prove the third induction case and
1714 %swap it with the list of tactics used to prove the second case. If
1715 %the proofs was structured with the branch tactical this task could
1716 %have been done automatically.
1718 %From this experience we learned that the use of tacticals for
1719 %structuring proofs gives some help but may have some drawbacks in
1720 %proof script readability.
1722 Tacticals are not only used to make scripts shorter by factoring out
1723 common cases and repeating commands. They are a primary way of making
1724 scripts more mainteable. Moreover, they also have the well-known
1725 role of structuring the proof.
1727 However, authoring a proof structured with tacticals is annoying.
1728 Consider for example a proof by induction, and imagine you
1729 are using one of the state of the art graphical interfaces for proof assistant
1730 like Proof General. After applying the induction principle you have to choose:
1731 immediately structure the proof or postpone the structuring.
1732 If you decide for the former you have to apply the branching tactical and write
1733 at once tactics for all the cases. Since the user does not even know the
1734 generated goals yet, he can only replace all the cases with the identity
1735 tactic and execute the command, just to receive feedback on the first
1736 goal. Then he has to go one step back to replace the first identity
1737 tactic with the wanted one and repeat the process until all the
1738 branches are closed.
1740 One could imagine that a structured script is simpler to understand.
1741 This is not the case.
1742 A proof script, being not declarative, is not meant to be read.
1743 However, the user has the need of explaining it to others.
1744 This is achieved by interactively re-playing the script to show each
1745 intermediate proof status. Tacticals make this operation uncomfortable.
1746 Indeed, a tactical is executed atomically, while it is obvious that it
1747 performs lot of smaller steps we are interested in.
1748 To show the intermediate steps, the proof must be de-structured on the
1749 fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where
1753 %readability is poor by itself, but in conjunction with tacticals it
1754 %can be nearly impossible. The main cause is the fact that in proof
1755 %scripts there is no trace of what you are working on. It is not rare
1756 %for two different theorems to have the same proof script.\\
1757 %Bad readability is not a big deal for the user while he is
1758 %constructing the proof, but is considerably a problem when he tries to
1759 %reread what he did or when he shows his work to someone else. The
1760 %workaround commonly used to read a script is to execute it again
1761 %step-by-step, so that you can see the proof goal changing and you can
1762 %follow the proof steps. This works fine until you reach a tactical. A
1763 %compound statement, made by some basic tactics glued with tacticals,
1764 %is executed in a single step, while it obviously performs lot of proof
1765 %steps. In the fist example of the previous section the whole branch
1766 %over the two goals (respectively the left and right part of the logic
1767 %and) result in a single step of execution. The workaround does not work
1768 %anymore unless you de-structure on the fly the proof, putting some
1769 %``\texttt{.}'' where you want the system to stop.\\
1771 %Now we can understand the tradeoff between script readability and
1772 %proof structuring with tacticals. Using tacticals helps in maintaining
1773 %scripts, but makes it really hard to read them again, cause of the way
1776 \MATITA{} has a peculiar tacticals implementation that provides the
1777 same benefits as classical tacticals, while not burdening the user
1778 during proof authoring and re-playing.
1780 %\MATITA{} uses a language of tactics and tacticals, but tries to avoid
1781 %this tradeoff, alluring the user to write structured proof without
1782 %making it impossible to read them again.
1784 \subsubsection{The \MATITA{} approach: Tinycals}
1787 \caption{Concrete syntax of tacticals\strut}
1791 \begin{array}{@{}rcll@{}}
1793 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
1795 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
1796 \NT{block\_delimiter} &
1797 ::= & \verb+begin+ ~|~ \verb+end+ & \\
1799 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
1805 \MATITA{} tacticals syntax is reported in Tab.~\ref{tab:tacsyn}.
1806 While one would expect to find structured constructs like
1807 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
1808 This is essential for the base idea behind \MATITA{} tacticals: step-by-step
1811 The low-level tacticals implementation of \MATITA{} allows a step-by-step
1812 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
1813 not executed as an atomic operation. This has major benefits for the
1814 user during proof structuring and re-playing.
1816 For instance, reconsider the previous example of a proof by induction.
1817 With step-by-step tacticals the user can apply the induction principle, and just
1818 open the branching tactical ``\texttt{[}''. Then he can interact with the
1819 system until the proof of the first case is terminated. After that
1820 ``\texttt{|}'' is used to move to the next goal, until all goals are
1821 closed. After the last goal, the user closes the branching tactical with
1822 ``\texttt{]}'' and is done with a structured proof. \\
1823 While \MATITA{} tacticals help in structuring proofs they allow you to
1824 choose the amount of structure you want. There are no constraints imposed by
1825 the system, and if the user wants he can even write completely plain proofs.
1827 Re-playing a proof is also made simpler. There is no longer any need
1828 to destructure the proof on the fly since \MATITA{} executes each
1829 tactical not atomically.
1832 % is possible. Going on step by step shows exactly what is going on. Consider
1833 % again a proof by induction, that starts applying the induction principle and
1834 % suddenly branches with a ``\texttt{[}''. This clearly separates all the
1835 % induction cases, but if the square brackets content is executed in one single
1836 % step you completely loose the possibility of rereading it and you have to
1837 % temporary remove the branching tactical to execute in a satisfying way the
1838 % branches. Again, executing step-by-step is the way you would like to review
1839 % the demonstration. Remember that understanding the proof from the script is
1840 % not easy, and only the execution of tactics (and the resulting transformed
1841 % goal) gives you the feeling of what is going on.
1844 \section{Standard library}
1847 \MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
1848 can be read, checked and referenced in further developments.
1849 However, in order to test the actual usability of the system, a
1850 new library of results has been started from scratch. In this case,
1851 of course, we wrote (and offer) the source script files,
1852 while, in the case of \COQ, \MATITA{} may only rely on XML files of
1854 The current library just comprises about one thousand theorems in
1855 elementary aspects of arithmetics up to the multiplicative property for
1856 Eulers' totient function $\phi$.
1857 The library is organized in five main directories: \texttt{logic} (connectives,
1858 quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
1859 constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
1860 (rationals). The most complex development is \texttt{nat}, organized in 25
1861 scripts, listed in Tab.~\ref{tab:scripts}.
1864 \begin{tabular}{lll}
1865 \FILE{nat.ma} & \FILE{plus.ma} & \FILE{times.ma} \\
1866 \FILE{minus.ma} & \FILE{exp.ma} & \FILE{compare.ma} \\
1867 \FILE{orders.ma} & \FILE{le\_arith.ma} & \FILE{lt\_arith.ma} \\
1868 \FILE{factorial.ma} & \FILE{sigma\_and\_pi.ma} & \FILE{minimization.ma} \\
1869 \FILE{div\_and\_mod.ma} & \FILE{gcd.ma} & \FILE{congruence.ma} \\
1870 \FILE{primes.ma} & \FILE{nth\_prime.ma} & \FILE{ord.ma} \\
1871 \FILE{count.ma} & \FILE{relevant\_equations.ma} & \FILE{permutation.ma} \\
1872 \FILE{factorization.ma} & \FILE{chinese\_reminder.ma} &
1873 \FILE{fermat\_little\_th.ma} \\
1874 \FILE{totient.ma} & & \\
1876 \caption{Scripts on natural numbers in the standard library\strut}
1880 We do not plan to maintain the library in a centralized way,
1881 as most of the systems do. On the contrary we are currently
1882 developing wiki-technologies to support a collaborative
1883 development of the library, encouraging people to expand,
1884 modify and elaborate previous contributions.
1886 \section{Conclusions}
1887 \label{sec:conclusion}
1892 We would like to thank all the people that during the past
1893 7 years collaborated in the \HELM{} project and contributed to
1894 the development of \MATITA{}, and in particular
1895 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
1900 \TODO{rivedere bibliografia, \'e un po' povera}
1902 \TODO{aggiungere entry per le coercion implicite}
1904 \bibliography{matita}