1 \documentclass[a4paper]{llncs}
4 \usepackage{amssymb,amsmath}
8 %\newcommand{\logo}[3]{
9 %\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
12 \newcommand{\AUTO}{\textsc{Auto}}
13 \newcommand{\COQ}{Coq}
14 \newcommand{\ELIM}{\textsc{Elim}}
15 \newcommand{\HELM}{Helm}
16 \newcommand{\HINT}{\textsc{Hint}}
17 \newcommand{\IN}{\ensuremath{\mathbb{N}}}
18 \newcommand{\INSTANCE}{\textsc{Instance}}
19 \newcommand{\IR}{\ensuremath{\mathbb{R}}}
20 \newcommand{\LIBXSLT}{LibXSLT}
21 \newcommand{\LOCATE}{\textsc{Locate}}
22 \newcommand{\MATCH}{\textsc{Match}}
23 \newcommand{\MATITA}{Matita}
24 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
25 \newcommand{\MOWGLI}{MoWGLI}
26 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
27 \newcommand{\NATIND}{\mathit{nat\_ind}}
28 \newcommand{\NUPRL}{NuPRL}
29 \newcommand{\OCAML}{OCaml}
30 \newcommand{\PROP}{\mathit{Prop}}
31 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
32 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
33 \newcommand{\UWOBO}{UWOBO}
34 \newcommand{\WHELP}{Whelp}
36 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
37 \newcommand{\NOTE}[1]{\marginpar{\scriptsize #1}}
38 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
40 \title{The Matita proof assistant}
41 \author{Andrea Asperti, Claudio Sacerdoti Coen, Enrico Tassi
42 and Stefano Zacchiroli}
43 \institute{Department of Computer Science, University of Bologna\\
44 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY\\
45 \email{$\{$asperti,sacerdot,tassi,zacchiro$\}$@cs.unibo.it}}
46 \bibliographystyle{plain}
54 \section{Introduction}
56 {\em Matita} is the proof assistant under development by the \HELM{} team
57 \cite{mkm-helm} at the University of Bologna, under the direction of
59 The origin of the system goes back to 1999. At the time we were mostly
60 interested to develop tools and techniques to enhance the accessibility
61 via web of formal libraries of mathematics. Due to its dimension, the
62 library of the \COQ{} proof assistant (of the order of 35'000 theorems)
63 was choosed as a privileged test bench for our work, although experiments
64 have been also conducted with other systems, and notably with \NUPRL{}.
65 The work, mostly performed in the framework of the recently concluded
66 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
69 \item exporting the information from the internal representation of
70 \COQ{} to a system and platform independent format. Since XML was at the
71 time an emerging standard, we naturally adopted this technology, fostering
72 a content-based architecture for future system, where the documents
73 of the library were the the main components around which everything else
75 \item developing indexing and searching techniques supporting semantic
76 queries to the library; these efforts gave birth to our \WHELP{}
77 search engine, described in~\cite{whelp};
78 \item developing languages and tools for a high-quality notational
79 rendering of mathematical information; in particular, we have been
80 active in the MathML Working group since 1999, and developed inside
81 \HELM{} a MathML-compliant widget for the GTK graphical environment
82 which can be integrated in any application.
84 The exportation issue, extensively discussed in \cite{exportation-module},
85 has several major implications worth to be discussed.
88 point concerns the kind of content information to be exported. In a
89 proof assistant like \COQ{}, proofs are represented in at least three clearly
90 distinguishable formats: \emph{scripts} (i.e. sequences of commands issued by the
91 user to the system during an interactive session of proof), \emph{proof objects}
92 (which is the low-level representation of proofs in the form of
93 lambda-terms readable to and checked by kernel) and \emph{proof-trees} (which
94 is a kind of intermediate representation, vaguely inspired by a sequent
95 like notation, that inherits most of the defects but essentially
96 none of the advantages of the previous representations).
97 Partially related to this problem, there is the
98 issue of the {\em granularity} of the library: scripts usually comprise
99 small developments with many definitions and theorems, while
100 proof objects correspond to individual mathemtical items.
102 In our case, the choice of the content encoding was eventually dictated
103 by the methodological assumption of offering the information in a
104 stable and system-independent format. The language of scripts is too
105 oriented to \COQ, and it changes too rapidly to be of any interest
106 to third parties. On the other side, the language of proof objects
108 the logical framework (the Calculus of Inductive Constructions, in
109 the case of \COQ), is grammatically simple, semantically clear and,
110 especially, is very stable (as kernels of proof assistants
112 So the granularity of the library is at the level of individual
113 objects, that also justifies from another point of view the need
114 for efficient searching techniques for retrieving individual
115 logical items from the repository.
117 The main (possibly only) problem with proof objects is that they are
118 difficult to read and do not directly correspond to what the user typed
119 in. An analogy frequently made in the proof assistant community is that of
120 comparing the vernacular language of scripts to a high level source language
121 and lambda terms to the assembly language they are compiled in. We do not
122 share this view and prefer to look at scripts as an imperative language,
123 and to lambda terms as their denotational semantics; still, however,
124 denotational semantics is possibly more formal but surely not more readable
125 than the imperative source.
127 For all the previous reasons, a huge amount of work inside \MOWGLI{} has
128 been devoted to automatic reconstruction of proofs in natural language
129 from lambda terms. Since lambda terms are in close connection
130 with natural deduction
131 (that is still the most natural logical language discovered so far)
132 the work is not hopeless as it may seem, especially if rendering
133 is combined, as in our case, with dynamic features supporting
134 in-line expansions or contractions of subproofs. The final
135 rendering is probably not entirely satisfactory (see \cite{ida} for a
136 discussion), but surely
137 readable (the actual quality largely depends by the way the lambda
140 Summing up, we already disposed of the following tools/techniques:
142 \item XML specifications for the Calculus of Inductive Constructions,
143 with tools for parsing and saving mathematical objects in such a format;
144 \item metadata specifications and tools for indexing and querying the
146 \item a proof checker (i.e. the {\em kernel} of a proof assistant),
147 implemented to check that we exported form the \COQ{} library all the
148 logically relevant content;
149 \item a sophisticated parser (used by the search engine), able to deal
150 with potentially ambiguous and incomplete information, typical of the
151 mathematical notation \cite{};
152 \item a {\em refiner}, i.e. a type inference system, based on complex
153 existential variables, used by the disambiguating parser;
154 \item complex transformation algorithms for proof rendering in natural
156 \item an innovative rendering widget, supporting high-quality bidimensional
157 rendering, and semantic selection, i.e. the possibility to select semantically
158 meaningfull rendering expressions, and to past the respective content into
159 a different text area.
160 \NOTE{il widget\\ non ha sel\\ semantica}
162 Starting from all this, the further step of developing our own
163 proof assistant was too
164 small and too tempting to be neglected. Essentially, we ``just'' had to
165 add an authoring interface, and a set of functionalities for the
166 overall management of the library, integrating everything into a
167 single system. \MATITA{} is the result of this effort.
169 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
170 more the effect of the circumstances of its creation described
171 above than the result of a deliberate design. In particular, we
172 (essentially) share the same foundational dialect of \COQ{} (the
173 Calculus of Inductive Constructions), the same implementative
174 language (\OCAML{}), and the same (script based) authoring philosophy.
175 However, as we shall see, the analogy essentially stops here.
177 In a sense; we like to think of \MATITA{} as the way \COQ{} would
178 look like if entirely rerwritten from scratch: just to give an
179 idea, although \MATITA{} currently supports almost all functionalities of
180 \COQ{}, it links 60'000 lins of \OCAML{} code, against ... of \COQ{} (and
181 we are convinced that, starting from scratch againg, we could furtherly
182 reduce our code in sensible way).\NOTE{righe\\\COQ{}}
185 \item scelta del sistema fondazionale
186 \item sistema indipendente (da Coq)
188 \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
189 implementative, \dots)
190 \item compatibilit\`a con sistemi legacy
199 \subsection{metavariabili}
205 \subsection{tatticali}
208 \subsection{Disambiguation}
209 \label{sec:disambiguation}
213 \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in notation\strut}
216 \begin{array}{@{}rcll@{}}
217 \NT{term} & ::= & & \mbox{\bf terms} \\
218 & & x & \mbox{(identifier)} \\
219 & | & n & \mbox{(number)} \\
220 & | & s & \mbox{(symbol)} \\
221 & | & \mathrm{URI} & \mbox{(URI)} \\
222 & | & \verb+?+ & \mbox{(implicit)} \\
223 & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
224 & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
225 & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
226 & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
227 & | & \NT{term}~\NT{term} & \mbox{(application)} \\
228 & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
229 & | & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
230 & & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
231 ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
232 & & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
233 & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
234 & | & \verb+(+~\NT{term}~\verb+)+ \\
235 \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
236 & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
237 \NT{fun} & ::= & & \mbox{\bf functions} \\
238 & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
239 \NT{binder} & ::= & & \mbox{\bf binders} \\
240 & & \verb+\forall+ \mid \verb+\lambda+ \\
241 \NT{arg} & ::= & & \mbox{\bf single argument} \\
242 & & \verb+_+ \mid x \\
243 \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
245 & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
246 \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
248 & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
249 \NT{kind} & ::= & & \mbox{\bf induction kind} \\
250 & & \verb+rec+ \mid \verb+corec+ \\
251 \NT{rule} & ::= & & \mbox{\bf rules} \\
252 & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
258 \subsubsection{Term input}
260 The primary form of user interaction employed by \MATITA{} is textual script
261 editing: the user can modifies it and evaluate step by step its composing
262 \emph{statements}. Examples of statements are inductive type definitions,
263 theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can
264 be used to ask the system to refine a given term and pretty print the result).
265 Since many statements refer to terms of the underlying calculus, \MATITA{} needs
266 a concrete syntax able to encode terms of the Calculus of Inductive
269 Two of the requirements in the design of such a syntax are apparently in
272 \item the syntax should be as close as possible to common mathematical practice
273 and implement widespread mathematical notions;
274 \item each term described by the syntax should be non-ambiguous meaning that it
275 should exists a function which associates to each term of the syntax a CIC
279 These two requirements are addressed in \MATITA{} by the mean of two mechanisms
280 which work together: \emph{term disambiguation} and \emph{extensible notation}.
281 Their interaction is visible in the architecture of the \MATITA{} input phase,
282 depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
283 pipline of three levels: the concrete syntax level (level 0) is the one the user
284 has to deal with when inserting CIC terms; the abstract syntax level (level 2)
285 is an internal representation which intuitively encodes mathematical formulae at
286 the content level~\cite{adams}~\cite{mkm-structure}; the formal mathematics
287 level (level 3) is the CIC encoding of terms.
289 Requirement (1) is addressed by a built-in concrete syntax for terms, described
290 in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a
291 way for extending available mathematical notations. Extensible notation, which
292 is also in charge of providing a parsing function mapping concrete syntax terms
293 to content level terms, is described in Sect.~\ref{sec:notation}. Requirement
294 (2) is addressed by the conjunct action of that parsing function and
295 disambiguation which provides a function from content level terms to CIC terms.
297 \subsubsection{Sources of ambiguity}
299 The translation from content level terms to CIC terms is not straightforward
300 because some nodes of the content encoding admit more that one CIC encoding,
301 invalidating requirement (2).
305 Consider the term \texttt{\TEXMACRO{forall} x. x + ln 1 = x}, the type of a
306 lemma the user may want to prove. Assuming that both \texttt{+} and \texttt{=}
307 are parsed as infix operators, all the following questions are legitimate and
308 must be answered before obtaining a CIC term from its content level encoding
309 (Fig.~\ref{fig:inputphase}(b)):
313 \item Since \texttt{ln} is an unbound identifier, which CIC constants does it
314 represent? Many different theorems in the library may share its (rather
317 \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for?
318 Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is
319 it an unary or a binary encoding?
321 \item Which kind of equality the ``='' node represents? Is it Leibniz's
322 polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots?
328 In \MATITA, three \emph{sources of ambiguity} are admitted for content level
329 terms: unbound identifiers, literal numbers, and literal symbols.
331 \emph{Unbound identifiers} (question 1) are sources of ambiguity since the same
332 name could have been used in the proof assistant library to represent different
333 objects. \emph{Numbers} (question 2) are ambiguous since several different
334 encodings of them could be provided in the calculus. Finally, \emph{symbols}
335 (question 3) are ambiguous as well, since they may be used in an overloaded
336 fashion to represent the application of different objects.
338 \textbf{FINQUI, il resto \`e copy and paste dal Whelp paper \dots}
340 Note that given a content level term with more than one sources of ambiguity,
341 not all possible disambiguation choices are valid: for example, given the input
342 \texttt{1+1} we must choose an interpretation of \texttt{+} which is typable in
343 CIC according to the chosen interpretation for \texttt{1}; choosing as
344 \texttt{+} the addition over natural numbers and as \texttt{1} the real number
345 $1$ will lead to a type error.
347 A \emph{disambiguation algorithm} takes as input an ambiguous term and return a
348 fully determined CIC term. The \emph{naive disambiguation algorithm} takes as
349 input an ambiguous term $t$ and proceeds as follows:
353 \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
354 $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
357 \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$
358 % such that $\forall i\in\mathit{Dom}(t),\exists\phi_j\in\Phi,i=j$
359 be an interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC
360 term is fully determined. Iterate over all possible interpretations of $t$ and
361 type-check them, keep only typable interpretations (i.e. interpretations that
362 determine typable terms).
364 \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
365 signal a type error. If $n=1$ we have found exactly one CIC term
366 corresponding to $t$, returns it as output of the disambiguation phase.
367 If $n>1$ let the user choose one of the $n$ interpretations and returns the
372 The above algorithm is highly inefficient since the number of possible
373 interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
374 The actual algorithm used in \WHELP{} is far more efficient being, in the
375 average case, linear in the number of ambiguity sources.
377 The efficient algorithm can be applied if the logic can be extended with
378 metavariables and a refiner can be implemented. This is the case for CIC and
379 several other logics.
380 \emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
381 occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
382 a freshly created metavariable. A \emph{refiner}~\cite{McBride} is a
383 function whose input is a term with placeholders and whose output is either a
384 new term obtained instantiating some placeholder or $\epsilon$, meaning that no
385 well typed instantiation could be found for the placeholders occurring in
386 the term (type error).
388 The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
389 \phi_i = ?, i\in\mathit{Dom}(t)\}$,
390 which associates a fresh metavariable to each
391 source of ambiguity. Then it iterates refining the current CIC term (i.e. the
392 term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
393 next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
394 replacing a placeholder with one of the possible choice from the corresponding
395 disambiguation domain. The placeholder to be replaced is chosen following a
396 preorder visit of the ambiguous term. If the refinement fails the current set of
397 choices cannot lead to a well-typed term and backtracking is attempted.
398 Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
399 longer contain any placeholder), backtracking is attempted
400 anyway to find the other correct interpretations.
402 The intuition which explain why this algorithm is more efficient is that as soon
403 as a term containing placeholders is not typable, no further instantiation of
404 its placeholders could lead to a typable term. For example, during the
405 disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
406 interpretation $\Phi_i$ is encountered which associates $?$ to the instance
407 of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
408 the left, and the multiplication over natural numbers (\texttt{mult} for short)
409 to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
410 argument, and no further instantiation of the placeholder will be tried.
412 If, at the end of the disambiguation, more than one possible interpretations are
413 possible, the user will be asked to choose the intended one (see
414 Fig.~\ref{fig:disambiguation}).
417 % \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
418 \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
421 Details of the disambiguation algorithm of \WHELP{} can
422 be found in~\cite{disambiguation}, where an equivalent algorithm
423 that avoids backtracking is also presented.
425 \subsection{notazione}
429 \subsection{libreria tutta visibile}
432 \subsection{ricerca e indicizzazione}
438 \subsection{xml / gestione della libreria}
441 \subsection{named variable}
444 \subsection{assenza di proof tree / resa in linguaggio naturale}
447 \subsection{selezione semantica, cut paste, hyperlink}
450 \subsection{sostituzioni esplicite vs moduli}
453 \section{Drawbacks, missing, \dots}
461 \subsection{estrazione}
464 \subsection{localizzazione errori}
467 \textbf{Acknowledgements}
468 We would like to thank all the students that during the past
469 five years collaborated in the \HELM{} project and contributed to
470 the development of Matita, and in particular
471 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
474 \bibliography{matita}