1 \documentclass[]{kluwer}
4 % \usepackage{amssymb,amsmath}
11 \definecolor{gray}{gray}{0.85}
12 %\newcommand{\logo}[3]{
13 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
16 \newcommand{\component}{component}
17 \newcommand{\components}{components}
19 \newcommand{\AUTO}{\textsc{Auto}}
20 \newcommand{\COQ}{Coq}
21 \newcommand{\ELIM}{\textsc{Elim}}
22 \newcommand{\GDOME}{Gdome}
23 \newcommand{\HELM}{Helm}
24 \newcommand{\HINT}{\textsc{Hint}}
25 \newcommand{\IN}{\ensuremath{\dN}}
26 \newcommand{\INSTANCE}{\textsc{Instance}}
27 \newcommand{\IR}{\ensuremath{\dR}}
28 \newcommand{\IZ}{\ensuremath{\dZ}}
29 \newcommand{\LIBXSLT}{LibXSLT}
30 \newcommand{\LOCATE}{\textsc{Locate}}
31 \newcommand{\MATCH}{\textsc{Match}}
32 \newcommand{\MATITA}{Matita}
33 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
34 \newcommand{\MOWGLI}{MoWGLI}
35 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
36 \newcommand{\NATIND}{\mathit{nat\_ind}}
37 \newcommand{\NUPRL}{NuPRL}
38 \newcommand{\OCAML}{OCaml}
39 \newcommand{\PROP}{\mathit{Prop}}
40 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
41 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
42 \newcommand{\UWOBO}{UWOBO}
43 \newcommand{\GETTER}{Getter}
44 \newcommand{\WHELP}{Whelp}
45 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
46 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
47 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
48 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
49 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
50 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
51 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
52 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
53 \newcommand{\SKIP}{\MATHTT{skip}}
54 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
56 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
57 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
58 \newcommand{\URI}[1]{\texttt{#1}}
59 \newcommand{\OP}[1]{``\texttt{#1}''}
61 %{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
62 \newenvironment{grafite}{\VerbatimEnvironment
63 \begin{SaveVerbatim}{boxtmp}}%
64 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
66 \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
70 \newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
72 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
73 \newcommand{\FILE}[1]{\texttt{#1}}
74 % \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
75 \newcommand{\NOTE}[1]{\ednote{#1}{foo}}
76 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
79 \newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
82 \newcommand{\sequent}[2]{
83 \savebox{\tmpxyz}[0.9\linewidth]{
84 \begin{minipage}{0.9\linewidth}
88 \end{minipage}}\setlength{\fboxsep}{3mm}%
90 \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
93 \bibliographystyle{plain}
99 \title{The \MATITA{} Proof Assistant}
101 \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
102 \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
103 \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
104 \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
105 \institute{Department of Computer Science, University of Bologna\\
106 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
108 \runningtitle{The Matita proof assistant}
109 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
114 ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
121 \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
126 \section{Introduction}
128 \MATITA{} is the Proof Assistant under development by the \HELM{} team
129 \cite{mkm-helm} at the University of Bologna, under the direction of
131 The paper describes the overall architecture of
132 the system, focusing on its most distintive and innovative
135 \subsection{Historical Perspective}
136 The origins of \MATITA{} go back to 1999. At the time we were mostly
137 interested to develop tools and techniques to enhance the accessibility
138 via Web of formal libraries of mathematics. Due to its dimension, the
139 library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
140 was choosed 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}.
143 The work, mostly performed in the framework of the recently concluded
144 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
147 \item exporting the information from the internal representation of
148 \COQ{} to a system and platform independent format. Since XML was at the
149 time an emerging standard, we naturally adopted this technology, fostering
150 a content-centric architecture\cite{content-centric} where the documents
151 of the library were the the main components around which everything else
153 \item developing indexing and searching techniques supporting semantic
154 queries to the library;
155 %these efforts gave birth to our \WHELP{}
156 %search engine, described in~\cite{whelp};
157 \item developing languages and tools for a high-quality notational
158 rendering of mathematical information\footnote{We have been
159 active in the MathML Working group since 1999.};
160 %and developed inside
161 %\HELM{} a MathML-compliant widget for the GTK graphical environment
162 %which can be integrated in any application.
165 According to our content-centric commitment, the library exported from
166 Coq was conceived as being distributed and most of the tools were developed
167 as Web services. The user could interact with the library and the tools by
168 means of a Web interface that orchestrates the Web services.
170 The Web services and the other tools have been implemented as front-ends
171 to a set of software libraries, collectively called the \HELM{} libraries.
172 At the end of the \MOWGLI{} project we already disposed of the following
173 tools and software libraries:
175 \item XML specifications for the Calculus of Inductive Constructions,
176 with libraries for parsing and saving mathematical objects in such a format
177 \cite{exportation-module};
178 \item metadata specifications with libraries for indexing and querying the
180 \item a proof checker library (i.e. the {\em kernel} of a proof assistant),
181 implemented to check that we exported form the \COQ{} library all the
182 logically relevant content;
183 \item a sophisticated parser (used by the search engine), able to deal
184 with potentially ambiguous and incomplete information, typical of the
185 mathematical notation \cite{disambiguation};
186 \item a {\em refiner} library, i.e. a type inference system, based on
187 partially specified terms, used by the disambiguating parser;
188 \item complex transformation algorithms for proof rendering in natural
189 language \cite{remathematization};
190 \item an innovative, MathML-compliant rendering widget for the GTK
191 graphical environment\cite{padovani}, supporting
192 high-quality bidimensional
193 rendering, and semantic selection, i.e. the possibility to select semantically
194 meaningful rendering expressions, and to past the respective content into
195 a different text area.
197 Starting from all this, developing our own proof assistant was not
198 too far away: essentially, we ``just'' had to
199 add an authoring interface, and a set of functionalities for the
200 overall management of the library, integrating everything into a
201 single system. \MATITA{} is the result of this effort.
203 \subsection{The System}
204 DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
207 \item scelta del sistema fondazionale
208 \item sistema indipendente (da Coq)
209 \item compatibilit\`a con sistemi legacy
212 \subsection{Relationship with \COQ{}}
214 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
215 more the effect of the circumstances of its creation described
216 above than the result of a deliberate design. In particular, we
217 (essentially) share the same foundational dialect of \COQ{} (the
218 Calculus of (Co)Inductive Constructions), the same implementative
219 language (\OCAML{}), and the same (script based) authoring philosophy.
220 However, the analogy essentially stops here and no code is shared by the
223 In a sense; we like to think of \MATITA{} as the way \COQ{} would
224 look like if entirely rewritten from scratch: just to give an
225 idea, although \MATITA{} currently supports almost all functionalities of
226 \COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
227 by \COQ{} (and we are convinced that, starting from scratch again,
228 we could furtherly reduce our code in sensible way).
230 Moreover, the complexity of the code of \MATITA{} is greatly reduced with
231 respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
232 989 functions, to be compared with the 4'286 functions of \COQ.
234 Finally, \MATITA{} has several innovatives features over \COQ{} that derive
235 from the integration of Mathematical Knowledge Management tools with proof
236 assistants. Among them, the advanced indexing tools over the library and
237 the parser for ambiguous mathematical notation.
239 The size and complexity improvements over \COQ{} must be understood
240 historically. \COQ{} is a quite old
241 system whose development started 15\NOTE{Verificare} years ago. Since then
242 several developers have took over the code and several new research ideas
243 that were not considered in the original architecture have been experimented
244 and integrated in the system. Moreover, there exists a lot of developments
245 for \COQ{} that require backward compatibility between each pair of releases;
246 since many central functionalities of a proof assistant are based on heuristics
247 or arbitrary choices to overcome undecidability (e.g. for higher order
248 unification), changing these functionalities mantaining backward compatibility
249 is very difficult. Finally, the code of \COQ{} has been greatly optimized
250 over the years; optimization reduces maintenability and rises the complexity
253 In writing \MATITA{} we have not been hindered by backward compatibility and
254 we have took advantage of the research results and experiences previously
255 developed by others, comprising the authors of \COQ. Moreover, starting from
256 scratch, we have designed in advance the architecture and we have splitted
257 the code in coherent minimally coupled libraries.
259 In the future we plan to exploit \MATITA{} as a test bench for new ideas and
260 extensions. Keeping the single libraries and the whole architecture as
261 simple as possible is thus crucial to foster future experiments and to
262 allow other developers to quickly understand our code and contribute.
264 %For direct experience of the authors, the learning curve to understand and
265 %be able to contribute to \COQ{}'s code is quite steep and requires direct
266 %and frequent interactions with \COQ{} developers.
270 \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
271 \caption{\MATITA{} libraries}
272 \label{fig:libraries}
276 \section{Overview of the Architecture}
277 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
278 (circle nodes) and \emph{applications} (squared nodes) developed in the HELM
281 Applications and \components{} depend over other \components{} forming a
282 directed acyclic graph (DAG). Each \component{} can be decomposed in
283 a a set of \emph{modules} also forming a DAG.
285 Modules and \components{} provide coherent sets of functionalities
286 at different scales. Applications that require only a few functionalities
287 depend on a restricted set of \components{}.
289 Only the proof assistant \MATITA{} and the \WHELP{} search engine are
290 applications meant to be used directly by the user. All the other applications
291 are Web services developed in the HELM and MoWGLI projects and already described
292 elsewhere. In particular:
294 \item The \emph{Getter} is a Web service to retrieve an (XML) document
295 from a physical location (URL) given its logical name (URI). The Getter is
296 responsible of updating a table that maps URIs to URLs. Thanks to the Getter
297 it is possible to work on a logically monolithic library that is physically
298 distributed on the network. More information on the Getter can be found
299 in~\cite{zack-master}.
300 \item \emph{Whelp} is a search engine to index and locate mathematical
301 notions (axioms, theorems, definitions) in the logical library managed
302 by the Getter. Typical examples of a query to Whelp are queries that search
303 for a theorem that generalize or instantiate a given formula, or that
304 can be immediately applied to prove a given goal. The output of Whelp is
305 an XML document that lists the URIs of a complete set of candidates that
306 are likely to satisfy the given query. The set is complete in the sense
307 that no notion that actually satisfies the query is thrown away. However,
308 the query is only approssimated in the sense that false matches can be
309 returned. Whelp has been described in~\cite{whelp}.
310 \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
311 notion in the distributed library, renders it according to the user provided
312 two dimensional mathematical notation. Uwobo may also embed the rendering
313 of mathematical notions into arbitrary documents before returning them.
314 The Getter is used by Uwobo to retrieve the document to be rendered.
315 Uwobo has been described in~\cite{zack-master}.
316 \item The \emph{Proof Checker} is a Web service that, given the URI of
317 notion in the distributed library, checks its correctness. Since the notion
318 is likely to depend in an acyclic way over other notions, the proof checker
319 is also responsible of building in a top-down way the DAG of all
320 dependencies, checking in turn every notion for correctness.
321 The proof checker has been described in~\cite{zack-master}.
322 \item The \emph{Dependency Analyzer} is a Web service that can produce
323 a textual or graphical representation of the dependecies of an object.
324 The dependency analyzer has been described in~\cite{zack-master}.
327 The dependency of a \component{} or application over another \component{} can
328 be satisfied by linking the \component{} in the same executable.
329 For those \components{} whose functionalities are also provided by the
330 aforementioned Web services, it is also possible to link stub code that
331 forwards the request to a remote Web service. For instance, the Getter
332 is just a wrapper to the \texttt{getter} \component{} that allows the
333 \component{} to be used as a Web service. \MATITA{} can directly link the code
334 of the \texttt{getter} \component, or it can use a stub library with the same
335 API that forwards every request to the Getter.
337 To better understand the architecture of \MATITA{} and the role of each
338 \component, we can focus on the representation of the mathematical information.
339 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
340 Constructions (CIC). In CIC terms are used to represent mathematical
341 expressions, types and proofs. \MATITA{} is able to handle terms at
342 four different levels of specification. On each level it is possible to provide
343 a different set of functionalities. The four different levels are:
344 fully specified terms; partially specified terms;
345 content level terms; presentation level terms.
347 \subsection{Fully specified terms}
348 \emph{Fully specified terms} are CIC terms where no information is
349 missing or left implicit. A fully specified term should be well-typed.
350 The mathematical notions (axioms, definitions, theorems) that are stored
351 in our mathematical library are fully specified and well-typed terms.
352 Fully specified terms are extremely verbose (to make type-checking
353 decidable). Their syntax is fixed and does not resemble the usual
354 extendible mathematical notation. They are not meant for direct user
357 The \texttt{cic} \component{} defines the data type that represents CIC terms
358 and provides a parser for terms stored in an XML format.
360 The most important \component{} that deals with fully specified terms is
361 \texttt{cic\_proof\_checking}. It implements the procedure that verifies
362 if a fully specified term is well-typed. It also implements the
363 \emph{conversion} judgement that verifies if two given terms are
364 computationally equivalent (i.e. they share the same normal form).
366 Terms may reference other mathematical notions in the library.
367 One commitment of our project is that the library should be physically
368 distributed. The \texttt{getter} \component{} manages the distribution,
369 providing a mapping from logical names (URIs) to the physical location
370 of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
371 data type and several utility functions over URIs. The
372 \texttt{cic\_proof\_checking} \component{} calls the \texttt{getter}
373 \component{} every time it needs to retrieve the definition of a mathematical
374 notion referenced by a term that is being type-checked.
376 The Proof Checker is the Web service that provides an interface
377 to the \texttt{cic\_proof\_checking} \component.
379 We use metadata and a sort of crawler to index the mathematical notions
380 in the distributed library. We are interested in retrieving a notion
381 by matching, instantiation or generalization of a user or system provided
382 mathematical expression. Thus we need to collect metadata over the fully
383 specified terms and to store the metadata in some kind of (relational)
384 database for later usage. The \texttt{hmysql} \component{} provides
386 interface to a (possibly remote) MySql database system used to store the
387 metadata. The \texttt{metadata} \component{} defines the data type of the
389 we are collecting and the functions that extracts the metadata from the
390 mathematical notions (the main functionality of the crawler).
391 The \texttt{whelp} \component{} implements a search engine that performs
392 approximated queries by matching/instantiation/generalization. The queries
393 operate only on the metadata and do not involve any actual matching
394 (that will be described later on and that is implemented in the
395 \texttt{cic\_unification} \component). Not performing any actual matching
396 the query only returns a complete and hopefully small set of matching
397 candidates. The process that has issued the query is responsible of
398 actually retrieving from the distributed library the candidates to prune
399 out false matches if interested in doing so.
401 The Whelp search engine is the Web service that provides an interface to
402 the \texttt{whelp} \component.
404 According to our vision, the library is developed collaboratively so that
405 changing or removing a notion can invalidate other notions in the library.
406 Moreover, changing or removing a notion requires a corresponding change
407 in the metadata database. The \texttt{library} \component{} is responsible
408 of preserving the coherence of the library and the database. For instance,
409 when a notion is removed, all the notions that depend on it and their
410 metadata are removed from the library. This aspect will be better detailed
411 in Sect.~\ref{decompilazione}.
413 \subsection{Partially specified terms}
414 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
415 Omitted subterms can bear no information at all or they may be associated to
416 a sequent. The formers are called \emph{implicit terms} and they occur only
417 linearly. The latters may occur multiple times and are called
418 \emph{metavariables}. An \emph{explicit substitution} is applied to each
419 occurrence of a metavariable. A metavariable stand for a term whose type is
420 given by the conclusion of the sequent. The term must be closed in the
421 context that is given by the ordered list of hypotheses of the sequent.
422 The explicit substitution instantiates every hypothesis with an actual
423 value for the term bound by the hypothesis.
425 Partially specified terms are not required to be well-typed. However a
426 partially specified term should be \emph{refinable}. A \emph{refiner} is
427 a type-inference procedure that can instantiate implicit terms and
428 metavariables and that can introduce \emph{implicit coercions} to make a
429 partially specified term be well-typed. The refiner of \MATITA{} is implemented
430 in the \texttt{cic\_unification} \component. As the type checker is based on
431 the conversion check, the refiner is based on \emph{unification} that is
432 a procedure that makes two partially specified term convertible by instantiating
433 as few as possible metavariables that occur in them.
435 Since terms are used in CIC to represent proofs, correct incomplete
436 proofs are represented by refinable partially specified terms. The metavariables
437 that occur in the proof correspond to the conjectures still to be proved.
438 The sequent associated to the metavariable is the conjecture the user needs to
441 \emph{Tactics} are the procedures that the user can apply to progress in the
442 proof. A tactic proves a conjecture possibly creating new (and hopefully
443 simpler) conjectures. The implementation of tactics is given in the
444 \texttt{tactics} \component. It is heavily based on the refinement and
445 unification procedures of the \texttt{cic\_unification} \component.
447 The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
448 commands of the \MATITA{} proof assistant. Most of the commands are tactics.
449 Other commands are used to give definitions and axioms or to state theorems
450 and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
451 It implements the semantics of each command in the grafite AST as a function
452 from status to status. It implements also an undo function to go back to
453 previous statuses. \TODO{parlare di disambiguazione lazy \& co?}
455 As fully specified terms, partially specified terms are not well suited
456 for user consumption since their syntax is not extendible and it is not
457 possible to adopt the usual mathematical notation. However they are already
458 an improvement over fully specified terms since they allow to omit redundant
459 information that can be inferred by the refiner.
461 \subsection{Content level terms}
462 \label{sec:contentintro}
464 The language used to communicate proofs and expecially expressions with the
465 user does not only needs to be extendible and accomodate the usual mathematical
466 notation. It must also reflect the comfortable degree of imprecision and
467 ambiguity that the mathematical language provides.
469 For instance, it is common practice in mathematics to speak of a generic
470 equality that can be used to compare any two terms. However, it is well known
471 that several equalities can be distinguished as soon as we care for decidability
472 or for their computational properties. For instance equality over real
473 numbers is well known to be undecidable, whereas it is decidable over
476 Similarly, we usually speak of natural numbers and their operations and
477 properties without caring about their representation. However the computational
478 properties of addition over the binary representation are very different from
479 those of addition over the unary representation. And addition over two natural
480 numbers is definitely different from addition over two real numbers.
482 Formal mathematics cannot hide these differences and obliges the user to be
483 very precise on the types he is using and their representation. However,
484 to communicate formulae with the user and with external tools, it seems good
485 practice to stick to the usual imprecise mathematical ontology. In the
486 Mathematical Knowledge Management community this imprecise language is called
487 the \emph{content level} representation of expressions.
489 In \MATITA{} we provide two translations: from partially specified terms
490 to content level terms and the other way around. The first translation can also
491 be applied to fully specified terms since a fully specified term is a special
492 case of partially specified term where no metavariable or implicit term occurs.
494 The translation from partially specified terms to content level terms must
495 discriminate between terms used to represent proofs and terms used to represent
496 expressions. The firsts are translated to a content level representation of
497 proof steps that can easily be rendered in natural language. The latters
498 are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C
500 for the representation of content level expressions in an XML extensible format.
502 The translation to content level is implemented in the
503 \texttt{acic\_content} \component. Its input are \emph{annotated partially
504 specified terms}, that are maximally unshared
505 partially specified terms enriched with additional typing information for each
506 subterm. This information is used to discriminate between terms that represent
507 proofs and terms that represent expressions. Part of it is also stored at the
508 content level since it is required to generate the natural language rendering
509 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
510 and not a DAG). The reason is that to the occurrences of a subterm in
511 two different positions we need to associate different typing informations.
512 This association is made easier when the term is represented as a tree since
513 it is possible to label each node with an unique identifier and associate
514 the typing information using a map on the identifiers.
515 The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
516 by the \texttt{library} \component{} since fully specified terms are stored
517 in the library in their annotated form.
519 We do not provide yet a reverse translation from content level proofs to
520 partially specified terms. But in \texttt{cic\_disambiguation} we do provide
521 the reverse translation for expressions. The mapping from
522 content level expressions to partially specified terms is not unique due to
523 the ambiguity of the content level. As a consequence the translation
524 is guided by an \emph{interpretation}, that is a function that chooses for
525 every ambiguous expression one partially specified term. The
526 \texttt{cic\_disambiguation} \component{} implements the
527 disambiguation algorithm we presented in~\cite{disambiguation} that is
528 responsible of building in an efficicent way the set of all ``correct''
529 interpretations. An interpretation is correct if the partially specified term
530 obtained using the interpretation is refinable.
532 \subsection{Presentation level terms}
534 Content level terms are a sort of abstract syntax trees for mathematical
535 expressions and proofs. The concrete syntax given to these abstract trees
536 is called \emph{presentation level}.
538 The main important difference between the content level language and the
539 presentation level language is that only the former is extendible. Indeed,
540 the presentation level language is a finite language that comprises all
541 the usual mathematical symbols. Mathematicians invent new notions every
542 single day, but they stick to a set of symbols that is more or less fixed.
544 The fact that the presentation language is finite allows the definition of
545 standard languages. In particular, for formulae we have adopt MathML
546 Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
548 represent proofs it is enough to embed formulae in plain text enriched with
549 formatting boxes. Since the language of formatting boxes is very simple,
550 many equivalent specifications exist and we have adopted our own, called
553 The \texttt{content\_pres} \component{} contains the implementation of the
554 translation from content level terms to presentation level terms. The
555 rendering of presentation level terms is left to the application that uses
556 the \component. However, in the \texttt{hgdome} \component{} we provide a few
557 utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
559 level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
560 widget developed by Luca Padovani \cite{padovani}. The widget is
561 particularly interesting since it allows to implement \emph{semantic
564 Semantic selection is a technique that consists in enriching the presentation
565 level terms with pointers to the content level terms and to the partially
566 specified terms they correspond to. Highlight of formulae in the widget is
567 constrained to selection of meaningful expressions, i.e. expressions that
568 correspond to a lower level term, that is a content term or a partially or
569 fully specified term.
570 Once the rendering of a lower level term is
571 selected it is possible for the application to retrieve the pointer to the
572 lower level term. An example of applications of semantic selection is
573 \emph{semantic cut\&paste}: the user can select an expression and paste it
574 elsewhere preserving its semantics (i.e. the partially specified term),
575 possibly performing some semantic transformation over it (e.g. renaming
576 variables that would be captured or lambda-lifting free variables).
578 The reverse translation from presentation level terms to content level terms
579 is implemented by a parser that is also found in \texttt{content\_pres}.
580 Differently from the translation from content level terms to partially
581 refined terms, this translation is not ambiguous. The reason is that the
582 parsing tool we have adopted (CamlP4) is not able to parse ambiguous
583 grammars. Thus we require the mapping from presentation level terms
584 (concrete syntax) to content level terms (abstract syntax) to be unique.
585 This means that the user must fix once and for all the associativity and
586 precedence level of every operator he is using. In practice this limitation
587 does not seem too strong. The reason is that the target of the
588 translation is an ambiguous language and the user is free to associate
589 to every content level term several different interpretations (as a
590 partially specified term).
592 Both the direct and reverse translation from presentation to content level
593 terms are parameterized over the user provided mathematical notation.
594 The \texttt{lexicon} \component{} is responsible of managing the lexicon,
595 that is the set of active notations. It defines an abstract syntax tree
596 of commands to declare and activate new notations and it implements the
597 semantics of these commands. It also implements undoing of the semantic
598 actions. Among the commands there are hints to the
599 disambiguation algorithm that are used to control and speed up disambiguation.
600 These mechanisms will be further discussed in Sect.~\ref{disambiguazione}.
602 Finally, the \texttt{grafite\_parser} \component{} implements a parser for
603 the concrete syntax of the commands of \MATITA. The parser process a stream
604 of characters and returns a stream of abstract syntax trees (the ones
605 defined by the \texttt{grafite} component and whose semantics is given
606 by \texttt{grafite\_engine}). When the parser meets a command that changes
607 the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
608 process the command. When the parser needs to parse a term at the presentation
609 level, it invokes the already described parser for terms contained in
610 \texttt{content\_pres}.
612 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
613 against the \texttt{grafite\_parser} \components{}
614 since they provide an interface to the user. In both cases the formulae
615 written by the user are parsed using the \texttt{content\_pres} \component{} and
616 then disambiguated using the \texttt{cic\_disambiguation} \component.
617 However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
618 \texttt{tactics} components since \WHELP{} can only execute those ASTs that
619 correspond to queries (implemented in the \texttt{whelp} component).
621 The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
622 providing a rendering service for the documents in the distributed library.
623 To render a document given its URI, \UWOBO{} retrieves it using the
624 \GETTER{} obtaining a document with fully specified terms. Then it translates
625 it to the presentation level passing through the content level. Finally
626 it returns the result document to be rendered by the user's
627 browser.\footnote{\TODO{manca la passata verso HTML}}
630 The \components{} not yet described (\texttt{extlib}, \texttt{xml},
631 \texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
632 minor \components{} that provide a core of useful functions and basic
633 services missing from the standard library of the programming language.
634 In particular, the \texttt{xml} \component{} is used
635 to easily represent, parse and pretty-print XML files.
637 \section{Partially specified terms}
638 --- il mondo delle tattiche e dintorni ---
639 serve una intro che almeno cita il widget (per i patterns) e che fa
640 il resoconto delle cose che abbiamo e che non descriviamo,
641 sottolineando che abbiamo qualcosa da dire sui pattern e sui
646 \subsection{Patterns}
647 Patterns are the textual counterpart of the MathML widget graphical
650 Matita benefits of a graphical interface and a powerful MathML rendering
651 widget that allows the user to select pieces of the sequent he is working
652 on. While this is an extremely intuitive way for the user to
653 restrict the application of tactics, for example, to some subterms of the
654 conclusion or some hypothesis, the way this action is recorded to the text
655 script is not obvious.\\
656 In \MATITA{} this issue is addressed by patterns.
658 \subsubsection{Pattern syntax}
659 A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
661 The former mocks-up a sequent, discharging unwanted subterms with $?$ and
662 selecting the interesting parts with the placeholder $\%$.
663 The latter is a term that lives in the context of the placeholders.
665 The concrete syntax is reported in table \ref{tab:pathsyn}
666 \NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
668 \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
671 \begin{array}{@{}rcll@{}}
673 ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
675 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
676 [~\verb+\vdash+~\NT{multipath}~] & \\
677 \NT{wanted} & ::= & \NT{term} & \\
678 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
684 \subsubsection{How patterns work}
685 Patterns mimic the user's selection in two steps. The first one
686 selects roots (subterms) of the sequent, using the
687 $\NT{sequent\_path}$, while the second
688 one searches the $\NT{wanted}$ term starting from these roots. Both are
689 optional steps, and by convention the empty pattern selects the whole
694 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
695 part of the syntax. $\NT{ident}$ is an hypothesis name and
696 selects the assumption where the following optional $\NT{multipath}$
697 will operate. \verb+\vdash+ can be considered the name for the goal.
698 If the whole pattern is omitted, the whole goal will be selected.
699 If one or more hypotheses names are given the selection is restricted to
700 these assumptions. If a $\NT{multipath}$ is omitted the whole
701 assumption is selected. Remember that the user can be mostly
702 unaware of this syntax, since the system is able to write down a
703 $\NT{sequent\_path}$ starting from a visual selection.
704 \NOTE{Questo ancora non va in matita}
706 A $\NT{multipath}$ is a CiC term in which a special constant $\%$
708 The roots of discharged subterms are marked with $?$, while $\%$
709 is used to select roots. The default $\NT{multipath}$, the one that
710 selects the whole term, is simply $\%$.
711 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
712 that respectively select the first argument of an application or
713 the source of an arrow and the head of the application that is
714 found in the arrow target.
716 The first phase selects not only terms (roots of subterms) but also
717 their context that will be eventually used in the second phase.
720 plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
721 part is specified. From the first phase we have some terms, that we
722 will see as subterm roots, and their context. For each of these
723 contexts the $\NT{wanted}$ term is disambiguated in it and the
724 corresponding root is searched for a subterm $\alpha$-equivalent to
725 $\NT{wanted}$. The result of this search is the selection the
731 Since the first step is equipotent to the composition of the two
732 steps, the system uses it to represent each visual selection.
733 The second step is only meant for the
734 experienced user that writes patterns by hand, since it really
735 helps in writing concise patterns as we will see in the
738 \subsubsection{Examples}
739 To explain how the first step works let's give an example. Consider
740 you want to prove the uniqueness of the identity element $0$ for natural
741 sum, and that you can relay on the previously demonstrated left
742 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
745 theorem valid_name: \forall n,m. m + n = n \to m = O.
749 leads you to the following sequent
757 where you want to change the right part of the equivalence of the $H$
758 hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
760 change in H:(? ? ? %) with (O + n).
763 This pattern, that is a simple instance of the $\NT{sequent\_path}$
764 grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
765 and discharges the head of the application and the first two arguments with a
766 $?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
767 but the user can simply select with the mouse the right part of the equivalence
768 and left to the system the burden of writing down in the script file the
769 corresponding pattern with $?$ and $\%$ in the right place (that is not
770 trivial, expecially where implicit arguments are hidden by the notation, like
771 the type $nat$ in this example).
773 Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
774 works too and can be done, by the experienced user, writing directly
775 a simpler pattern that uses the second phase.
777 change in match n in H with (O + n).
780 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
781 the second phase searches the wanted $n$ inside it by
782 $\alpha$-equivalence. The resulting
783 equivalence will be $m+(O+n)=O+n$ since the second phase found two
784 occurrences of $n$ in $H$ and the tactic changed both.
786 Just for completeness the second pattern is equivalent to the
787 following one, that is less readable but uses only the first phase.
789 change in H:(? ? (? ? %) %) with (O + n).
793 \subsubsection{Tactics supporting patterns}
794 In \MATITA{} all the tactics that can be restricted to subterm of the working
795 sequent accept the pattern syntax. In particular these tactics are: simplify,
796 change, fold, unfold, generalize, replace and rewrite.
798 \NOTE{attualmente rewrite e fold non supportano phase 2. per
799 supportarlo bisogna far loro trasformare il pattern phase1+phase2
800 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
801 con una pattern\_of(select(pattern))}
803 \subsubsection{Comparison with Coq}
804 Coq has a two diffrent ways of restricting the application of tactis to
805 subterms of the sequent, both relaying on the same special syntax to identify
808 The first way is to use this special syntax to specify directly to the
809 tactic the occurrnces of a wanted term that should be affected, while
810 the second is to prepare the sequent with another tactic called
811 pattern and the apply the real tactic. Note that the choice is not
812 left to the user, since some tactics needs the sequent to be prepared
813 with pattern and do not accept directly this special syntax.
815 The base idea is that to identify a subterm of the sequent we can
816 write it and say that we want, for example, the third and the fifth
817 occurce of it (counting from left to right). In our previous example,
818 to change only the left part of the equivalence, the correct command
821 change n at 2 in H with (O + n)
824 meaning that in the hypothesis $H$ the $n$ we want to change is the
825 second we encounter proceeding from left toright.
827 The tactic pattern computes a
828 $\beta$-expansion of a part of the sequent with respect to some
829 occurrences of the given term. In the previous example the following
835 would have resulted in this sequent
839 H : (fun n0 : nat => m + n = n0) n
840 ============================
844 where $H$ is $\beta$-expanded over the second $n$
845 occurrence. This is a trick to make the unification algorithm ignore
846 the head of the application (since the unification is essentially
847 first-order) but normally operate on the arguments.
848 This works for some tactics, like rewrite and replace,
849 but for example not for change and other tactics that do not relay on
852 The idea behind this way of identifying subterms in not really far
853 from the idea behind patterns, but really fails in extending to
854 complex notation, since it relays on a mono-dimensional sequent representation.
855 Real math notation places arguments upside-down (like in indexed sums or
856 integrations) or even puts them inside a bidimensional matrix.
857 In these cases using the mouse to select the wanted term is probably the
858 only way to tell the system exactly what you want to do.
860 One of the goals of \MATITA{} is to use modern publishing techiques, and
861 adopting a method for restricting tactics application domain that discourages
862 using heavy math notation, would definitively be a bad choice.
864 \subsection{Tacticals}
865 There are mainly two kinds of languages used by proof assistants to recorder
866 proofs: tactic based and declarative. We will not investigate the philosophy
867 aroud the choice that many proof assistant made, \MATITA{} included, and we
868 will not compare the two diffrent approaches. We will describe the common
869 issues of the tactic-based language approach and how \MATITA{} tries to solve
872 \subsubsection{Tacticals overview}
874 Tacticals first appeared in LCF and can be seen as programming
875 constructs, like looping, branching, error recovery or sequential composition.
876 The following simple example shows three tacticals in action
880 A = B \to ((A \to B) \land (B \to A)).
883 [ rewrite < H. assumption.
884 | rewrite > H. assumption.
889 The first is ``\texttt{;}'' that combines the tactic \texttt{split}
890 with \texttt{intro}, applying the latter to each goal opened by the
891 former. Then we have ``\texttt{[}'' that branches on the goals (here
892 we have two goals, the two sides of the logic and).
893 The first goal $B$ (with $A$ in the context)
894 is proved by the first sequence of tactics
895 \texttt{rewrite} and \texttt{assumption}. Then we move to the second
896 goal with the separator ``\texttt{|}''. The last tactical we see here
897 is ``\texttt{.}'' that is a sequential composition that selects the
898 first goal opened for the following tactic (instead of applying it to
899 them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
900 not considered a tactical, but a sentence terminator (i.e. the
901 delimiter of commands the proof assistant executes).
903 Giving serious examples here is rather difficult, since they are hard
904 to read without the interactive tool. To help the reader in
905 understanding the following considerations we just give few common
906 usage examples without a proof context.
909 elim z; try assumption; [ ... | ... ].
910 elim z; first [ assumption | reflexivity | id ].
913 The first example goes by induction on a term \texttt{z} and applies
914 the tactic \texttt{assumption} to each opened goal eventually recovering if
915 \texttt{assumption} fails. Here we are asking the system to close all
916 trivial cases and then we branch on the remaining with ``\texttt{[}''.
917 The second example goes again by induction on \texttt{z} and tries to
918 close each opened goal first with \texttt{assumption}, if it fails it
919 tries \texttt{reflexivity} and finally \texttt{id}
920 that is the tactic that leaves the goal untouched without failing.
922 Note that in the common implementation of tacticals both lines are
923 compositions of tacticals and in particular they are a single
924 statement (i.e. derived from the same non terminal entry of the
925 grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
926 this is not true, since each atomic tactic or punctuation is considered
929 \subsubsection{Common issues of tactic(als)-based proof languages}
930 We will examine the two main problems of tactic(als)-based proof script:
931 maintainability and readability.
933 Huge libraries of formal mathematics have been developed, and backward
934 compatibility is a really time consuming task. \\
935 A real-life example in the history of \MATITA{} was the reordering of
936 goals opened by a tactic application. We noticed that some tactics
937 were not opening goals in the expected order. In particular the
938 \texttt{elim} tactic on a term of an inductive type with constructors
939 $c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
940 \ldots, g_2$. The library of \MATITA{} was still in an embryonic state
941 but some theorems about integers were there. The inductive type of
942 $\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
943 induction proofs on this type where written without tacticals and,
944 obviously, considering the three induction cases in the wrong order.
945 Fixing the behavior of the tactic broke the library and two days of
946 work were needed to make it compile again. The whole time was spent in
947 finding the list of tactics used to prove the third induction case and
948 swap it with the list of tactics used to prove the second case. If
949 the proofs was structured with the branch tactical this task could
950 have been done automatically.
952 From this experience we learned that the use of tacticals for
953 structuring proofs gives some help but may have some drawbacks in
954 proof script readability. We must highlight that proof scripts
955 readability is poor by itself, but in conjunction with tacticals it
956 can be nearly impossible. The main cause is the fact that in proof
957 scripts there is no trace of what you are working on. It is not rare
958 for two different theorems to have the same proof script (while the
959 proof is completely different).\\
960 Bad readability is not a big deal for the user while he is
961 constructing the proof, but is considerably a problem when he tries to
962 reread what he did or when he shows his work to someone else. The
963 workaround commonly used to read a script is to execute it again
964 step-by-step, so that you can see the proof goal changing and you can
965 follow the proof steps. This works fine until you reach a tactical. A
966 compound statement, made by some basic tactics glued with tacticals,
967 is executed in a single step, while it obviously performs lot of proof
968 steps. In the fist example of the previous section the whole branch
969 over the two goals (respectively the left and right part of the logic
970 and) result in a single step of execution. The workaround doesn't work
971 anymore unless you de-structure on the fly the proof, putting some
972 ``\texttt{.}'' where you want the system to stop.\\
974 Now we can understand the tradeoff between script readability and
975 proof structuring with tacticals. Using tacticals helps in maintaining
976 scripts, but makes it really hard to read them again, cause of the way
979 \MATITA{} uses a language of tactics and tacticals, but tries to avoid
980 this tradeoff, alluring the user to write structured proof without
981 making it impossible to read them again.
983 \subsubsection{The \MATITA{} approach: Tinycals}
986 \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
989 \begin{array}{@{}rcll@{}}
991 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
993 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
994 \NT{block\_delimiter} &
995 ::= & \verb+begin+ ~|~ \verb+end+ & \\
997 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
1003 \MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
1004 While one would expect to find structured constructs like
1005 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
1006 This is essential for base idea behind matita tacticals: step-by-step execution.
1008 The low-level tacticals implementation of \MATITA{} allows a step-by-step
1009 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
1010 not executed as an atomic operation. This has two major benefits for the user,
1011 even being a so simple idea:
1013 \item[Proof structuring]
1014 is much easier. Consider for example a proof by induction, and imagine you
1015 are using classical tacticals in one of the state of the
1016 art graphical interfaces for proof assistant like Proof General or Coq Ide.
1017 After applying the induction principle you have to choose: structure
1018 the proof or not. If you decide for the former you have to branch with
1019 ``\texttt{[}'' and write tactics for all the cases separated by
1020 ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
1021 You can replace most of the cases by the identity tactic just to
1022 concentrate only on the first goal, but you will have to go one step back and
1023 one further every time you add something inside the tactical. Again this is
1024 caused by the one step execution of tacticals and by the fact that to modify
1025 the already executed script you have to undo one step.
1026 And if you are board of doing so, you will finish in giving up structuring
1027 the proof and write a plain list of tactics.\\
1028 With step-by-step tacticals you can apply the induction principle, and just
1029 open the branching tactical ``\texttt{[}''. Then you can interact with the
1030 system reaching a proof of the first case, without having to specify any
1031 tactic for the other goals. When you have proved all the induction cases, you
1032 close the branching tactical with ``\texttt{]}'' and you are done with a
1033 structured proof. \\
1034 While \MATITA{} tacticals help in structuring proofs they allow you to
1035 choose the amount of structure you want. There are no constraints imposed by
1036 the system, and if the user wants he can even write completely plain proofs.
1039 is possible. Going on step by step shows exactly what is going on. Consider
1040 again a proof by induction, that starts applying the induction principle and
1041 suddenly branches with a ``\texttt{[}''. This clearly separates all the
1042 induction cases, but if the square brackets content is executed in one single
1043 step you completely loose the possibility of rereading it and you have to
1044 temporary remove the branching tactical to execute in a satisfying way the
1045 branches. Again, executing step-by-step is the way you would like to review
1046 the demonstration. Remember that understanding the proof from the script is
1047 not easy, and only the execution of tactics (and the resulting transformed
1048 goal) gives you the feeling of what is going on.
1051 \section{Content level terms}
1053 \subsection{Disambiguation}
1055 Software applications that involve input of mathematical content should strive
1056 to require the user as less drift from informal mathematics as possible. We
1057 believe this to be a fundamental aspect of such applications user interfaces.
1058 Being that drift in general very large when inputing
1059 proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
1060 mathematical formulae which can be input using a \TeX-like encoding (the
1061 concrete syntax corresponding to presentation level terms) and are then
1062 translated (in multiple steps) to partially specified terms as sketched in
1063 Sect.~\ref{sec:contentintro}.
1065 The key component of the translation is the generic disambiguation algorithm
1066 implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
1067 and presented in~\cite{disambiguation}. In this section we present how to use
1068 such an algorithm in the context of the development of a library of formalized
1069 mathematics. We will see that using multiple passes of the algorithm, varying
1070 some of its parameters, helps in keeping the input terse without sacrificing
1073 \subsubsection{Disambiguation aliases}
1075 Let's start with the definition of the ``strictly greater then'' notion over
1076 (Peano) natural numbers.
1079 include "nat/nat.ma".
1081 definition gt: nat \to nat \to Prop \def
1082 \lambda n, m. m < n.
1085 The \texttt{include} statement adds the requirement that the part of the library
1086 defining the notion of natural numbers should be defined before
1087 processing the following definition. Note indeed that the algorithm presented
1088 in~\cite{disambiguation} does not describe where interpretations for ambiguous
1089 expressions come from, since it is application-specific. As a first
1090 approximation, we will assume that in \MATITA{} they come from the library (i.e.
1091 all interpretations available in the library are used) and the \texttt{include}
1092 statements are used to ensure the availability of required library slices (see
1093 Sect.~\ref{sec:libmanagement}).
1095 While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
1096 terms: its type and its body. Being available in the required library only one
1097 interpretation both for the unbound identifier \texttt{nat} and for the
1098 \OP{<} operator, and being the resulting partially specified term refinable,
1099 both type and body are easily disambiguated.
1101 Now suppose we have defined integers as signed natural numbers, and that we want
1102 to prove a theorem about an order relationship already defined on them (which of
1103 course overload the \OP{<} operator):
1109 \forall x, y, z. x < y \to y < z \to x < z.
1112 Since integers are defined on top of natural numbers, the part of the library
1113 concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
1114 type. Thus, according to the disambiguation algorithm, two different partially
1115 specified terms could be associated to it. At first, this might not be seen as a
1116 problem, since the user is asked and can choose interactively which of the two
1117 she had in mind. However in the long run it has the drawbacks of inhibiting
1118 batch compilation of the library (a technique used in \MATITA{} for behind the
1119 scene compilation when needed, e.g. when an \texttt{include} is issued) and
1120 yields to poor user interaction (imagine how tedious would be to be asked for a
1121 choice each time you re-evaluate \texttt{Zlt\_compat}!).
1123 For this reason we added to \MATITA{} the concept of \emph{disambiguation
1124 aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
1125 expressions to partially specified terms, which are part of the runtime status
1126 of \MATITA. They can be provided by users with the \texttt{alias} statement, but
1127 are usually automatically added when evaluating \texttt{include} statements
1128 (\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
1129 are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
1130 which require interactive choice are saved in batch compilable format. Thus,
1131 after evaluating the above theorem the script will be changed to the following
1132 snippet (assuming that the interpretation of \OP{<} over integers has been
1136 alias symbol "lt" = "integer 'less than'".
1138 \forall x, y, z. x < y \to y < z \to x < z.
1141 But how are disambiguation aliases used? Since they come from the parts of the
1142 library explicitely included we may be tempted of using them as the only
1143 available interpretations. This would speed up the disambiguation, but may fail.
1144 Consider for example:
1147 theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
1150 and suppose that the \OP{+} operator is defined only on natural numbers. If
1151 the alias for \OP{<} points to the integer version of the operator, no
1152 refinable partially specified term matching the term could be found.
1154 For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
1155 first pass attempt to disambiguate using the last available disambiguation
1156 aliases (\emph{mono aliases} pass), in case of failure the next pass try again
1157 the disambiguation forgetting the aliases and using the whole library to
1158 retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
1159 Since the latter pass may lead to too many choices we intertwined an additional
1160 pass among the two which use as interpretations all the aliases coming for
1161 included parts of the library (\emph{multi aliases} phase). This is the reason
1162 why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
1163 turned out to be a well-balanced trade-off among performances (earlier passes
1164 fail quickly) and degree of ambiguity supported for presentation level terms.
1166 \subsubsection{Operator instances}
1168 Let's suppose now we want to define a theorem relating ordering relations on
1169 natural and integer numbers. The way we would like to write such a theorem (as
1170 we can read it in the \MATITA{} standard library) is:
1174 include "nat/orders.ma".
1176 theorem lt_to_Zlt_pos_pos:
1177 \forall n, m: nat. n < m \to pos n < pos m.
1180 Unfortunately, none of the passes described above is able to disambiguate its
1181 type, no matter how aliases are defined. This is because the \OP{<} operator
1182 occurs twice in the content level term (it has two \emph{instances}) and two
1183 different interpretation for it have to be used in order to obtain a refinable
1184 partially specified term. To address this issue, we have the ability to consider
1185 each instance of a single symbol as a different ambiguous expression in the
1186 content level term, and thus we can assign a different interpretation to each of
1187 them. A disambiguation pass which exploit this feature is said to be using
1188 \emph{fresh instances}.
1190 Fresh instances lead to a non negligible performance loss (since the choice of
1191 an interpretation for one instances does not constraint the choice for the
1192 others). For this reason we always attempt a fresh instances pass only after
1193 attempting a non-fresh one.
1195 \subsubsection{Implicit coercions}
1197 Let's now consider a (rather hypothetical) theorem about derivation:
1200 theorem power_deriv:
1201 \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
1204 and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
1205 interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
1206 Mathematichians would write the term that way since it is well known that the
1207 natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
1208 number for the purpose of real multiplication. The refiner of \MATITA{} supports
1209 \emph{implicit coercions} for this reason: given as input the above content
1210 level term, it will return a partially specified term where in place of
1211 \texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
1212 (assuming it has been defined as such of course).
1214 Nonetheless coercions are not always desirable. For example, in disambiguating
1215 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
1216 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
1217 among the possible partially specified term choices. For this reason in
1218 \MATITA{} we always try first a disambiguation pass which require the refiner
1219 not to use the coercions and only in case of failure we attempt a
1220 coercion-enabled pass.
1222 It is interesting to observe also the relationship among operator instances and
1223 implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
1224 which \MATITA{} disambiguated using fresh instances. In case there exists a
1225 coercion from natural numbers to (positive) integers (which indeed does, it is
1226 the \texttt{pos} constructor itself), the theorem can be disambiguated using
1227 twice that coercion on the left hand side of the implication. The obtained
1228 partially specified term however would not probably be the expected one, being a
1229 theorem which prove a trivial implication. For this reason we choose to always
1230 prefer fresh instances over implicit coercion, i.e. we always attempt
1231 disambiguation passes with fresh instances before attempting passes with
1234 \subsubsection{Disambiguation passes}
1236 \TODO{spiegazione della tabella}
1239 \begin{tabular}{c|c|c|c}
1240 \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
1241 & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
1242 & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
1243 & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
1245 \PASS & Normal & Mono & Disabled \\
1246 \PASS & Normal & Multi & Disabled \\
1247 \PASS & Fresh & Mono & Disabled \\
1248 \PASS & Fresh & Multi & Disabled \\
1249 \PASS & Fresh & Mono & Enabled \\
1250 \PASS & Fresh & Multi & Enabled \\
1251 \PASS & Fresh & Library & Enabled
1255 \TODO{alias one shot}
1257 \section{The logical library}
1258 Matita is Coq compatible, in the sense that every theorem of Coq
1259 can be read, checked and referenced in further developments.
1260 However, in order to test the actual usability of the system, a
1261 new library of results has been started from scratch. In this case,
1262 of course, we wrote (and offer) the source script files,
1263 while, in the case of Coq, Matita may only rely on XML files of
1265 The current library just comprises about one thousand theorems in
1266 elementary aspects of arithmetics up to the multiplicative property for
1267 Eulers' totient function $\phi$.
1268 The library is organized in five main directories: $logic$ (connectives,
1269 quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type
1270 constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
1271 The most complex development is $nat$, organized in 25 scripts, listed
1272 in Figure\ref{scripts}
1275 nat.ma & plus.ma & times.ma \\
1276 minus.ma & exp.ma & compare.ma \\
1277 orders.ma & le\_arith.ma & lt\_arith.ma \\
1278 factorial.ma & sigma\_and\_pi.ma & minimization.ma \\
1279 div\_and\_mod.ma & gcd.ma & congruence.ma \\
1280 primes.ma & nth\_prime.ma & ord.ma\\
1281 count.ma & relevant\_equations.ma & permutation.ma \\
1282 factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\
1285 \caption{\label{scripts}Matita scripts on natural numbers}
1288 We do not plan to maintain the library in a centralized way,
1289 as most of the systems do. On the contary we are currently
1290 developing wiki-technologies to support a collaborative
1291 development of the library, encouraging people to expand,
1292 modify and elaborate previous contributions.
1294 \subsection{Matita's naming convention}
1295 A minor but not entirely negligible aspect of Matita is that of
1296 adopting a (semi)-rigid naming convention for identifiers, derived by
1297 our studies about metadata for statements.
1298 The convention is only applied to identifiers for theorems
1299 (not definitions), and relates the name of a proof to its statement.
1300 The basic rules are the following:
1302 \item each identifier is composed by an ordered list of (short)
1303 names occurring in a left to right traversal of the statement;
1304 \item all identifiers should (but this is not strictly compulsory)
1305 separated by an underscore,
1306 \item identifiers in two different hypothesis, or in an hypothesis
1307 and in the conlcusion must be separated by the string ``\verb+_to_+'';
1308 \item the identifier may be followed by a numerical suffix, or a
1309 single or duoble apostrophe.
1312 Take for instance the theorem
1313 \[\forall n:nat. n = plus \; n\; O\]
1314 Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
1315 \verb+eq_n_plus_n_O+ and so on.
1316 Similarly, consider the theorem
1317 \[\forall n,m:nat. n<m \to n \leq m\]
1318 In this case \verb+lt_to_le+ is a legal name,
1319 while \verb+lt_le+ is not.\\
1320 But what about, say, the symmetric law of equality? Probably you would like
1321 to name such a theorem with something explicitly recalling symmetry.
1322 The correct approach,
1323 in this case, is the following. You should start with defining the
1324 symmetric property for relations
1326 \[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
1328 Then, you may state the symmetry of equality as
1329 \[ \forall A:Type. symmetric \;A\;(eq \; A)\]
1330 and \verb+symmetric_eq+ is valid Matita name for such a theorem.
1331 So, somehow unexpectedly, the introduction of semi-rigid naming convention
1332 has an important benefical effect on the global organization of the library,
1333 forcing the user to define abstract notions and properties before
1334 using them (and formalizing such use).
1336 Two cases have a special treatment. The first one concerns theorems whose
1337 conclusion is a (universally quantified) predicate variable, i.e.
1338 theorems of the shape
1339 $\forall P,\dots.P(t)$.
1340 In this case you may replace the conclusion with the word
1341 ``elim'' or ``case''.
1342 For instance the name \verb+nat_elim2+ is a legal name for the double
1343 induction principle.
1345 The other special case is that of statements whose conclusion is a
1347 A typical example is the following
1350 match (eqb n m) with
1351 [ true \Rightarrow n = m
1352 | false \Rightarrow n \neq m]
1354 where $eqb$ is boolean equality.
1355 In this cases, the name can be build starting from the matched
1356 expression and the suffix \verb+_to_Prop+. In the above example,
1357 \verb+eqb_to_Prop+ is accepted.
1360 \section{Conclusions}
1363 We would like to thank all the students that during the past
1364 five years collaborated in the \HELM{} project and contributed to
1365 the development of Matita, and in particular
1366 M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
1371 \bibliography{matita}