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}}
53 \section{Introduction}
55 {\em Matita} is the proof assistant under development by the \HELM{} team
56 \cite{annals} at the University of Bologna, under the direction of
58 The origin of the system goes back to 1999. At the time we were mostly
59 interested to develop tools and techniques to enhance the accessibility
60 via web of formal libraries of mathematics. Due to its dimension, the
61 library of the \COQ{} proof assistant (of the order of 35'000 theorems)
62 was choosed as a privileged test bench for our work, although experiments
63 have been also conducted with other systems, and notably with \NUPRL{}.
64 The work, mostly performed in the framework of the recently concluded
65 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
68 \item exporting the information from the internal representation of
69 \COQ{} to a system and platform independent format. Since XML was at the
70 time an emerging standard, we naturally adopted this technology, fostering
71 a content-based architecture for future system, where the documents
72 of the library were the the main components around which everything else
74 \item developing indexing and searching techniques supporting semantic
75 queries to the library; these efforts gave birth to our \WHELP{}
76 search engine, described in~\cite{whelp};
77 \item developing languages and tools for a high-quality notational
78 rendering of mathematical information; in particular, we have been
79 active in the MathML Working group since 1999, and developed inside
80 \HELM{} a MathML-compliant widget for the GTK graphical environment
81 which can be integrated in any application.
83 The exportation issue, extensively discussed in \cite{exportation},
84 has several major implications worth to be discussed.
87 point concerns the kind of content information to be exported. In a
88 proof assistant like \COQ{}, proofs are represented in at least three clearly
89 distinguishable formats: \emph{scripts} (i.e. sequences of commands issued by the
90 user to the system during an interactive session of proof), \emph{proof objects}
91 (which is the low-level representation of proofs in the form of
92 lambda-terms readable to and checked by kernel) and \emph{proof-trees} (which
93 is a kind of intermediate representation, vaguely inspired by a sequent
94 like notation, that inherits most of the defects but essentially
95 none of the advantages of the previous representations).
96 Partially related to this problem, there is the
97 issue of the {\em granularity} of the library: scripts usually comprise
98 small developments with many definitions and theorems, while
99 proof objects correspond to individual mathemtical items.
101 In our case, the choice of the content encoding was eventually dictated
102 by the methodological assumption of offering the information in a
103 stable and system-independent format. The language of scripts is too
104 oriented to \COQ, and it changes too rapidly to be of any interest
105 to third parties. On the other side, the language of proof objects
107 the logical framework (the Calculus of Inductive Constructions, in
108 the case of \COQ), is grammatically simple, semantically clear and,
109 especially, is very stable (as kernels of proof assistants
111 So the granularity of the library is at the level of individual
112 objects, that also justifies from another point of view the need
113 for efficient searching techniques for retrieving individual
114 logical items from the repository.
116 The main (possibly only) problem with proof objects is that they are
117 difficult to read and do not directly correspond to what the user typed
118 in. An analogy frequently made in the proof assistant community is that of
119 comparing the vernacular language of scripts to a high level source language
120 and lambda terms to the assembly language they are compiled in. We do not
121 share this view and prefer to look at scripts as an imperative language,
122 and to lambda terms as their denotational semantics; still, however,
123 denotational semantics is possibly more formal but surely not more readable
124 than the imperative source.
126 For all the previous reasons, a huge amount of work inside \MOWGLI{} has
127 been devoted to automatic reconstruction of proofs in natural language
128 from lambda terms. Since lambda terms are in close connection
129 with natural deduction
130 (that is still the most natural logical language discovered so far)
131 the work is not hopeless as it may seem, especially if rendering
132 is combined, as in our case, with dynamic features supporting
133 in-line expansions or contractions of subproofs. The final
134 rendering is probably not entirely satisfactory (see \cite{ida} for a
135 discussion), but surely
136 readable (the actual quality largely depends by the way the lambda
139 Summing up, we already disposed of the following tools/techniques:
141 \item XML specifications for the Calculus of Inductive Constructions,
142 with tools for parsing and saving mathematical objects in such a format;
143 \item metadata specifications and tools for indexing and querying the
145 \item a proof checker (i.e. the {\em kernel} of a proof assistant),
146 implemented to check that we exported form the \COQ{} library all the
147 logically relevant content;
148 \item a sophisticated parser (used by the search engine), able to deal
149 with potentially ambiguous and incomplete information, typical of the
150 mathematical notation \cite{};
151 \item a {\em refiner}, i.e. a type inference system, based on complex
152 existential variables, used by the disambiguating parser;
153 \item complex transformation algorithms for proof rendering in natural
155 \item an innovative rendering widget, supporting high-quality bidimensional
156 rendering, and semantic selection, i.e. the possibility to select semantically
157 meaningfull rendering expressions, and to past the respective content into
158 a different text area.
159 \NOTE{il widget\\ non ha sel\\ semantica}
161 Starting from all this, the further step of developing our own
162 proof assistant was too
163 small and too tempting to be neglected. Essentially, we ``just'' had to
164 add an authoring interface, and a set of functionalities for the
165 overall management of the library, integrating everything into a
166 single system. \MATITA{} is the result of this effort.
168 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
169 more the effect of the circumstances of its creation described
170 above than the result of a deliberate design. In particular, we
171 (essentially) share the same foundational dialect of \COQ{} (the
172 Calculus of Inductive Constructions), the same implementative
173 language (\OCAML{}), and the same (script based) authoring philosophy.
174 However, as we shall see, the analogy essentially stops here.
176 In a sense; we like to think of \MATITA{} as the way \COQ{} would
177 look like if entirely rerwritten from scratch: just to give an
178 idea, although \MATITA{} currently supports almost all functionalities of
179 \COQ{}, it links 60'000 lins of \OCAML{} code, against ... of \COQ{} (and
180 we are convinced that, starting from scratch againg, we could furtherly
181 reduce our code in sensible way).\NOTE{righe\\\COQ{}}
184 \item scelta del sistema fondazionale
185 \item sistema indipendente (da Coq)
187 \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
188 implementative, \dots)
189 \item compatibilit\`a con sistemi legacy
198 \subsection{metavariabili}
204 \subsection{tatticali}
207 \subsection{Disambiguation}
208 \label{sec:disambiguation}
212 \caption{\label{tab:termsyn} Concrete syntax of CIC terms in \MATITA{}.\strut}
215 \begin{array}{@{}rcll@{}}
216 \NT{term} & ::= & & \mbox{\bf terms} \\
217 & & x & \mbox{(identifier)} \\
218 & | & n & \mbox{(number)} \\
219 & | & s & \mbox{(symbol)} \\
220 & | & \mathrm{URI} & \mbox{(URI)} \\
221 & | & \verb+?+ & \mbox{(implicit)} \\
222 & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
223 & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
224 & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
225 & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
226 & | & \NT{term}~\NT{term} & \mbox{(application)} \\
227 & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
228 & | & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
229 & & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
230 ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
231 & & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
232 & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
233 & | & \verb+(+~\NT{term}~\verb+)+ \\
234 \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
235 & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
236 \NT{fun} & ::= & & \mbox{\bf functions} \\
237 & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
238 \NT{binder} & ::= & & \mbox{\bf binders} \\
239 & & \verb+\forall+ \mid \verb+\lambda+ \\
240 \NT{arg} & ::= & & \mbox{\bf single argument} \\
241 & & \verb+_+ \mid x \\
242 \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
244 & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
245 \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
247 & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
248 \NT{kind} & ::= & & \mbox{\bf induction kind} \\
249 & & \verb+rec+ \mid \verb+corec+ \\
250 \NT{rule} & ::= & & \mbox{\bf rules} \\
251 & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
260 The disambiguation phase builds CIC terms from ASTs of user inputs (also called
261 \emph{ambiguous terms}). Ambiguous terms may carry three different \emph{sources
262 of ambiguity}: unbound identifiers, literal numbers, and literal symbols.
263 \emph{Unbound identifiers} are sources of ambiguity since the same name
264 could have been used to represent different objects. For example, three
265 different theorems of the \COQ{} library share the name $\mathit{plus\_assoc}$
266 (locating them is an exercise for the interested reader. Hint: use \WHELP's
269 \emph{Numbers} are ambiguous since several different encodings of them could be
270 provided in logical systems. In the \COQ{} standard library for example we found
271 naturals (in their unary encoding), positives (binary encoding), integers
272 (signed positives), and reals. Finally, \emph{symbols} (instances of the
273 \emph{binop} and \emph{unop} syntactic categories of Table~\ref{tab:syntax}) are
274 ambiguous as well: infix \texttt{+} for example is overloaded to represent
275 addition over the four different kinds of numbers available in the \COQ{}
276 standard library. Note that given a term with more than one sources of
277 ambiguity, not all possible disambiguation choices are valid: for example, given
278 the input \texttt{1+1} we must choose an interpretation of \texttt{+} which is
279 typable in CIC according to the chosen interpretation for \texttt{1}; choosing
280 as \texttt{+} the addition over natural numbers and as \texttt{1} the real
281 number $1$ will lead to a type error.
283 A \emph{disambiguation algorithm} takes as input an ambiguous term and return a
284 fully determined CIC term. The \emph{naive disambiguation algorithm} takes as
285 input an ambiguous term $t$ and proceeds as follows:
289 \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(t)\}$, where
290 $\mathit{Dom}(t)$ is the set of ambiguity sources of $t$. Each $D_i$ is a set
293 \item Let $\Phi = \{\phi_i | {i\in\mathit{Dom}(t)},\phi_i\in D_i\}$
294 % such that $\forall i\in\mathit{Dom}(t),\exists\phi_j\in\Phi,i=j$
295 be an interpretation for $t$. Given $t$ and an interpretation $\Phi$, a CIC
296 term is fully determined. Iterate over all possible interpretations of $t$ and
297 type-check them, keep only typable interpretations (i.e. interpretations that
298 determine typable terms).
300 \item Let $n$ be the number of interpretations who survived step 2. If $n=0$
301 signal a type error. If $n=1$ we have found exactly one CIC term
302 corresponding to $t$, returns it as output of the disambiguation phase.
303 If $n>1$ let the user choose one of the $n$ interpretations and returns the
308 The above algorithm is highly inefficient since the number of possible
309 interpretations $\Phi$ grows exponentially with the number of ambiguity sources.
310 The actual algorithm used in \WHELP{} is far more efficient being, in the
311 average case, linear in the number of ambiguity sources.
313 The efficient algorithm can be applied if the logic can be extended with
314 metavariables and a refiner can be implemented. This is the case for CIC and
315 several other logics.
316 \emph{Metavariables}~\cite{munoz} are typed, non linear placeholders that can
317 occur in terms; $?_i$ usually denotes the $i$-th metavariable, while $?$ denotes
318 a freshly created metavariable. A \emph{refiner}~\cite{mcbride} is a
319 function whose input is a term with placeholders and whose output is either a
320 new term obtained instantiating some placeholder or $\epsilon$, meaning that no
321 well typed instantiation could be found for the placeholders occurring in
322 the term (type error).
324 The efficient algorithm starts with an interpretation $\Phi_0 = \{\phi_i |
325 \phi_i = ?, i\in\mathit{Dom}(t)\}$,
326 which associates a fresh metavariable to each
327 source of ambiguity. Then it iterates refining the current CIC term (i.e. the
328 term obtained interpreting $t$ with $\Phi_i$). If the refinement succeeds the
329 next interpretation $\Phi_{i+1}$ will be created \emph{making a choice}, that is
330 replacing a placeholder with one of the possible choice from the corresponding
331 disambiguation domain. The placeholder to be replaced is chosen following a
332 preorder visit of the ambiguous term. If the refinement fails the current set of
333 choices cannot lead to a well-typed term and backtracking is attempted.
334 Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does no
335 longer contain any placeholder), backtracking is attempted
336 anyway to find the other correct interpretations.
338 The intuition which explain why this algorithm is more efficient is that as soon
339 as a term containing placeholders is not typable, no further instantiation of
340 its placeholders could lead to a typable term. For example, during the
341 disambiguation of user input \texttt{\TEXMACRO{forall} x. x*0 = 0}, an
342 interpretation $\Phi_i$ is encountered which associates $?$ to the instance
343 of \texttt{0} on the right, the real number $0$ to the instance of \texttt{0} on
344 the left, and the multiplication over natural numbers (\texttt{mult} for short)
345 to \texttt{*}. The refiner will fail, since \texttt{mult} require a natural
346 argument, and no further instantiation of the placeholder will be tried.
348 If, at the end of the disambiguation, more than one possible interpretations are
349 possible, the user will be asked to choose the intended one (see
350 Fig.~\ref{fig:disambiguation}).
353 % \centerline{\includegraphics[width=0.9\textwidth]{disambiguation-1}}
354 \caption{\label{fig:disambiguation} Disambiguation: interpretation choice}
357 Details of the disambiguation algorithm of \WHELP{} can
358 be found in~\cite{disambiguation}, where an equivalent algorithm
359 that avoids backtracking is also presented.
361 \subsection{notazione}
364 \subsection{libreria tutta visibile}
367 \subsection{ricerca e indicizzazione}
373 \subsection{xml / gestione della libreria}
376 \subsection{named variable}
379 \subsection{assenza di proof tree / resa in linguaggio naturale}
382 \subsection{selezione semantica, cut paste, hyperlink}
385 \subsection{sostituzioni esplicite vs moduli}
388 \section{Drawbacks, missing, \dots}
396 \subsection{estrazione}
399 \subsection{localizzazione errori}
402 \textbf{Acknowledgements}
403 We would like to thank all the students that during the past
404 five years collaborated in the \HELM{} project and contributed to
405 the development of Matita, and in particular
406 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
410 \begin{thebibliography}{}
412 \bibitem{ida}A.Asperti, H.Geuvers, I.Loeb, L.E.Mamane, C.Sacerdoti Coen.
413 An Interactive Algebra Course with Formalised Proofs and Definitions.
414 Post-Proceedings of the Fourth International Conference on
415 Mathemtical Knowledge Management. Bremen, Germany, July 2005. LNCS,
418 \bibitem{annals} A.~Asperti, F.~Guidi, L.~Padovani, C.~Sacerdoti Coen,
419 I.~Schena. \emph{Mathematical Knowledge Management in HELM}. Annals of
420 Mathematics and Artificial Intelligence, 38(1): 27--46; May 2003.
422 \bibitem{whelp} A.~Asperti, F.~Guidi, C.~Sacerdoti Coen,
423 E.Tassi, S.Zacchiroli. \emph{A content based mathematical search
424 engine: whelp}. Post-proceedings of the Types 2004 International
425 Conference, Jouy-en-Josas, France, December 2004. LNCS (to appear).
427 \bibitem{metadata2} A. Asperti, M. Selmi. \emph{Efficient Retrieval of
428 Mathematical Statements}. In Proceeding of the Third International Conference
429 on Mathematical Knowledge Management, MKM 2004. Bialowieza, Poland. LNCS 3119.
430 \bibitem{pechino} A.Asperti, B.Wegner. \emph{An Approach to
431 Machine-Understandable Representation of the Mathematical Information in
432 Digital Documents}. In: Fengshai Bai and Bernd Wegner (eds.): Electronic
433 Information and Communication in Mathematics, LNCS vol. 2730,
436 \bibitem{coq} The Coq proof-assistant, \url{http://coq.inria.fr}
438 \bibitem{metadata1} F. Guidi, C. Sacerdoti Coen. \emph{Querying Distributed
439 Digital Libraries of Mathematics}. In Proceedings of Calculemus 2003, 11th
440 Symposium on the Integration of Symbolic Computation and Mechanized
441 Reasoning. Aracne Editrice.
443 \bibitem{exportation} C. Sacerdoti Coen. \emph{From Proof-Assistans to
444 Distributed Libraries of Mathematics: Tips and Pitfalls}.
445 In Proc. Mathematical Knowledge Management 2003, Lecture Notes in Computer
446 Science, Vol. 2594, pp. 30--44, Springer-Verlag.
448 \bibitem{disambiguation} C. Sacerdoti Coen, S. Zacchiroli. \emph{Efficient
449 Ambiguous Parsing of Mathematical Formulae}. In Proceedings of the Third
450 International Conference on Mathematical Knowledge Management, MKM 2004.
453 \end{thebibliography}