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{\AUTO}{\textsc{Auto}}
17 \newcommand{\COQ}{Coq}
18 \newcommand{\ELIM}{\textsc{Elim}}
19 \newcommand{\HELM}{Helm}
20 \newcommand{\HINT}{\textsc{Hint}}
21 \newcommand{\IN}{\ensuremath{\dN}}
22 \newcommand{\INSTANCE}{\textsc{Instance}}
23 \newcommand{\IR}{\ensuremath{\dR}}
24 \newcommand{\IZ}{\ensuremath{\dZ}}
25 \newcommand{\LIBXSLT}{LibXSLT}
26 \newcommand{\LOCATE}{\textsc{Locate}}
27 \newcommand{\MATCH}{\textsc{Match}}
28 \newcommand{\MATITA}{Matita}
29 \newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
30 \newcommand{\MOWGLI}{MoWGLI}
31 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
32 \newcommand{\NATIND}{\mathit{nat\_ind}}
33 \newcommand{\NUPRL}{NuPRL}
34 \newcommand{\OCAML}{OCaml}
35 \newcommand{\PROP}{\mathit{Prop}}
36 \newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
37 \newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
38 \newcommand{\UWOBO}{UWOBO}
39 \newcommand{\WHELP}{Whelp}
40 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
41 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
42 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
43 \newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
44 \newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
45 \newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
46 \newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
47 \newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
48 \newcommand{\SKIP}{\MATHTT{skip}}
49 \newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
51 \definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
52 \newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
53 \newcommand{\URI}[1]{\texttt{#1}}
55 %{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
56 \newenvironment{grafite}{\VerbatimEnvironment
57 \begin{SaveVerbatim}{boxtmp}}%
58 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
60 \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
64 \newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
66 \newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
67 \newcommand{\FILE}[1]{\texttt{#1}}
68 % \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
69 \newcommand{\NOTE}[1]{\ednote{#1}{foo}}
70 \newcommand{\TODO}[1]{\textbf{TODO: #1}}
73 \newcommand{\sequent}[2]{
74 \savebox{\tmpxyz}[0.9\linewidth]{
75 \begin{minipage}{0.9\linewidth}
79 \end{minipage}}\setlength{\fboxsep}{3mm}%
81 \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
84 \bibliographystyle{plain}
90 \title{The \MATITA{} Proof Assistant}
92 \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
93 \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
94 \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
95 \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
96 \institute{Department of Computer Science, University of Bologna\\
97 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
99 \runningtitle{The Matita proof assistant}
100 \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
105 ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
112 \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
117 \section{Introduction}
119 {\em Matita} is the proof assistant under development by the \HELM{} team
120 \cite{mkm-helm} at the University of Bologna, under the direction of
122 The origin of the system goes back to 1999. At the time we were mostly
123 interested to develop tools and techniques to enhance the accessibility
124 via web of formal libraries of mathematics. Due to its dimension, the
125 library of the \COQ{} proof assistant (of the order of 35'000 theorems)
126 was choosed as a privileged test bench for our work, although experiments
127 have been also conducted with other systems, and notably with \NUPRL{}.
128 The work, mostly performed in the framework of the recently concluded
129 European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
132 \item exporting the information from the internal representation of
133 \COQ{} to a system and platform independent format. Since XML was at the
134 time an emerging standard, we naturally adopted this technology, fostering
135 a content-based architecture for future system, where the documents
136 of the library were the the main components around which everything else
138 \item developing indexing and searching techniques supporting semantic
139 queries to the library; these efforts gave birth to our \WHELP{}
140 search engine, described in~\cite{whelp};
141 \item developing languages and tools for a high-quality notational
142 rendering of mathematical information; in particular, we have been
143 active in the MathML Working group since 1999, and developed inside
144 \HELM{} a MathML-compliant widget for the GTK graphical environment
145 which can be integrated in any application.
147 The exportation issue, extensively discussed in \cite{exportation-module},
148 has several major implications worth to be discussed.
151 point concerns the kind of content information to be exported. In a
152 proof assistant like \COQ{}, proofs are represented in at least three clearly
153 distinguishable formats: \emph{scripts} (i.e. sequences of commands issued by the
154 user to the system during an interactive session of proof), \emph{proof objects}
155 (which is the low-level representation of proofs in the form of
156 lambda-terms readable to and checked by kernel) and \emph{proof-trees} (which
157 is a kind of intermediate representation, vaguely inspired by a sequent
158 like notation, that inherits most of the defects but essentially
159 none of the advantages of the previous representations).
160 Partially related to this problem, there is the
161 issue of the {\em granularity} of the library: scripts usually comprise
162 small developments with many definitions and theorems, while
163 proof objects correspond to individual mathematical items.
165 In our case, the choice of the content encoding was eventually dictated
166 by the methodological assumption of offering the information in a
167 stable and system-independent format. The language of scripts is too
168 oriented to \COQ, and it changes too rapidly to be of any interest
169 to third parties. On the other side, the language of proof objects
171 the logical framework (the Calculus of Inductive Constructions, in
172 the case of \COQ), is grammatically simple, semantically clear and,
173 especially, is very stable (as kernels of proof assistants
175 So the granularity of the library is at the level of individual
176 objects, that also justifies from another point of view the need
177 for efficient searching techniques for retrieving individual
178 logical items from the repository.
180 The main (possibly only) problem with proof objects is that they are
181 difficult to read and do not directly correspond to what the user typed
182 in. An analogy frequently made in the proof assistant community is that of
183 comparing the vernacular language of scripts to a high level source language
184 and lambda terms to the assembly language they are compiled in. We do not
185 share this view and prefer to look at scripts as an imperative language,
186 and to lambda terms as their denotational semantics; still, however,
187 denotational semantics is possibly more formal but surely not more readable
188 than the imperative source.
190 For all the previous reasons, a huge amount of work inside \MOWGLI{} has
191 been devoted to automatic reconstruction of proofs in natural language
192 from lambda terms. Since lambda terms are in close connection
193 with natural deduction
194 (that is still the most natural logical language discovered so far)
195 the work is not hopeless as it may seem, especially if rendering
196 is combined, as in our case, with dynamic features supporting
197 in-line expansions or contractions of subproofs. The final
198 rendering is probably not entirely satisfactory (see \cite{ida} for a
199 discussion), but surely
200 readable (the actual quality largely depends by the way the lambda
203 Summing up, we already disposed of the following tools/techniques:
205 \item XML specifications for the Calculus of Inductive Constructions,
206 with tools for parsing and saving mathematical objects in such a format;
207 \item metadata specifications and tools for indexing and querying the
209 \item a proof checker (i.e. the {\em kernel} of a proof assistant),
210 implemented to check that we exported form the \COQ{} library all the
211 logically relevant content;
212 \item a sophisticated parser (used by the search engine), able to deal
213 with potentially ambiguous and incomplete information, typical of the
214 mathematical notation \cite{};
215 \item a {\em refiner}, i.e. a type inference system, based on complex
216 existential variables, used by the disambiguating parser;
217 \item complex transformation algorithms for proof rendering in natural
219 \item an innovative rendering widget, supporting high-quality bidimensional
220 rendering, and semantic selection, i.e. the possibility to select semantically
221 meaningful rendering expressions, and to past the respective content into
222 a different text area.
223 \NOTE{il widget non ha sel semantica}
225 Starting from all this, the further step of developing our own
226 proof assistant was too
227 small and too tempting to be neglected. Essentially, we ``just'' had to
228 add an authoring interface, and a set of functionalities for the
229 overall management of the library, integrating everything into a
230 single system. \MATITA{} is the result of this effort.
232 At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
233 more the effect of the circumstances of its creation described
234 above than the result of a deliberate design. In particular, we
235 (essentially) share the same foundational dialect of \COQ{} (the
236 Calculus of Inductive Constructions), the same implementative
237 language (\OCAML{}), and the same (script based) authoring philosophy.
238 However, as we shall see, the analogy essentially stops here.
240 In a sense; we like to think of \MATITA{} as the way \COQ{} would
241 look like if entirely rewritten from scratch: just to give an
242 idea, although \MATITA{} currently supports almost all functionalities of
243 \COQ{}, it links 60'000 lins of \OCAML{} code, against ... of \COQ{} (and
244 we are convinced that, starting from scratch again, we could furtherly
245 reduce our code in sensible way).\NOTE{righe \COQ{}}
248 \item scelta del sistema fondazionale
249 \item sistema indipendente (da Coq)
251 \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
252 implementative, \dots)
253 \item compatibilit\`a con sistemi legacy
257 \section{\HELM{} library(??)}
259 \subsection{libreria tutta visibile}
261 \NOTE{assumo che si sia gia' parlato di approccio content-centrico}
262 Our commitment to the content-centric view of the architecture of the system
263 has important consequences on the user's experience and on the functionalities
264 of several components of \MATITA. In the content-centric view the library
265 of mathematical knowledge is an already existent and completely autonomous
266 entity that we are allowed to exploit and augment using \MATITA. Thus, in
267 principle, when the user starts to prove a new theorem she has complete
268 visibility of the library and she can refer to every definition and lemma,
269 also using the mathematical notation already developed. In a similar way,
270 every form of automation of the system must be able to analyze and possibly
271 exploit every notion in the library.
273 The benefits of this approach highly justify the non neglectable price to pay
274 in the development of several components. We analyse now a few of the causes
275 of this additional complexity.
277 \subsubsection{Ambiguity}
278 A rich mathematical library includes equivalent definitions and representations
279 of the same notion. Moreover, mathematical notation inside a rich library is
280 surely highly overloaded. As a consequence every mathematical expression the
281 user provides is highly ambiguous since all the definitions,
282 representations and special notations are available at once to the user.
284 The usual solution to the problem, as adopted for instance in Coq, is to
285 restrict the user's scope to just one interpretation for each definition,
286 representation or notation. In this way much of the ambiguity is removed,
287 burdening the user that must someway declare what is in scope and that must
288 use special syntax when she needs to refer to something not in scope.
290 Even with this approach ambiguity cannot be completely removed since implicit
291 coercions can be arbitrarily inserted by the system to ``change the type''
292 of subterms that do not have the expected type. Usually implicit coercions
293 are used to overcome the absence of subtyping that should mimic the subset
294 relation found in set theory. For instance, the expression
295 $\forall n \in nat. 2 * n * \pi \equiv_\pi 0$ is correct in set theory since
296 the set of natural numbers is a subset of that of real numbers; the
297 corresponding expression $\forall n:nat. 2*n*\pi \equiv_\pi 0$ is not well typed
298 and requires the automatic insertion of the coercion $real_of_nat: nat \to R$
299 either around both 2 and $n$ (to make both products be on real numbers) or
300 around the product $2*n$. The usual approach consists in either rejecting the
301 ambiguous term or arbitrarily choosing one of the interpretations. For instance,
302 Coq rejects the declaration of coercions that have alternatives
303 (i.e. already declared coercions with the same domain and codomain)
304 or that are obtained composing other coercions in order to
305 avoid making several terms highly ambiguous by choosing to insert any one of the
306 alternative coercions. Coq also arbitrarily chooses how to insert coercions in
307 terms to make them well typed when there is more than one possibility (as in
308 the previous example).
310 The approach we are following is radically different. It consists in dealing
311 with ambiguous expressions instead of avoiding them. As a last resource,
312 when the system is unable to disambiguate the input, the user is interactively
313 required to provide more information that is recorded to avoid asking the
314 same question again in subsequent processing of the same input.
315 More details on our approach can be found in \ref{sec:disambiguation}.
317 \subsubsection{Consistency}
318 A large mathematical library is likely to be logically inconsistent.
319 It may contain incompatible axioms or alternative conjectures and it may
320 even use definitions in incompatible ways. To clarify this last point,
321 consider two identical definitions of a set of elements of a given type
322 (or of a category of objects of a given type). Let us call the two definitions
323 $A-Set$ and $B-Set$ (or $A-Category$ and $B-Category$).
324 It is perfectly legitimate to either form the $A-Set$ of every $B-Set$
325 or the $B-Set$ of every $A-Set$ (the same for categories). This just corresponds
326 to assuming that a $B-Set$ (respectively an $A-Set$) is a small set, whereas
327 an $A-Set$ (respectively a $B-Set$) is a big set (possibly of small sets).
328 However, if one part of the library assumes $A-Set$s to be the small ones
329 and another part of the library assumes $B-Set$s to be the small ones, the
330 library as a whole will be logically inconsistent.
332 Logical inconsistency has never been a problem in the daily work of a
333 mathematician. The mathematician simply imposes himself a discipline to
334 restrict himself to consistent subsets of the mathematical knowledge.
335 However, in doing so he doesn't choose the subset in advance by forgetting
336 the rest of his knowledge.
338 Contrarily to a mathematician, the usual tendency in the world of assisted
339 automation is that of restricting in advance the part of the library that
340 will be used later on, checking its consistency by construction.
342 \subsection{ricerca e indicizzazione}
349 \subsection{sostituzioni esplicite vs moduli}
352 \subsection{xml / gestione della libreria}
356 \section{User Interface (da cambiare)}
358 \subsection{assenza di proof tree / resa in linguaggio naturale}
361 \subsection{Disambiguation}
362 \label{sec:disambiguation}
366 \caption{\label{tab:termsyn} Concrete syntax of CIC terms: built-in
370 \begin{array}{@{}rcll@{}}
371 \NT{term} & ::= & & \mbox{\bf terms} \\
372 & & x & \mbox{(identifier)} \\
373 & | & n & \mbox{(number)} \\
374 & | & s & \mbox{(symbol)} \\
375 & | & \mathrm{URI} & \mbox{(URI)} \\
376 & | & \verb+_+ & \mbox{(implicit)}\TODO{sync} \\
377 & | & \verb+?+n~[\verb+[+~\{\NT{subst}\}~\verb+]+] & \mbox{(meta)} \\
378 & | & \verb+let+~\NT{ptname}~\verb+\def+~\NT{term}~\verb+in+~\NT{term} \\
379 & | & \verb+let+~\NT{kind}~\NT{defs}~\verb+in+~\NT{term} \\
380 & | & \NT{binder}~\{\NT{ptnames}\}^{+}~\verb+.+~\NT{term} \\
381 & | & \NT{term}~\NT{term} & \mbox{(application)} \\
382 & | & \verb+Prop+ \mid \verb+Set+ \mid \verb+Type+ \mid \verb+CProp+ & \mbox{(sort)} \\
383 & | & \verb+match+~\NT{term}~ & \mbox{(pattern matching)} \\
384 & & ~ ~ [\verb+[+~\verb+in+~x~\verb+]+]
385 ~ [\verb+[+~\verb+return+~\NT{term}~\verb+]+] \\
386 & & ~ ~ \verb+with [+~[\NT{rule}~\{\verb+|+~\NT{rule}\}]~\verb+]+ & \\
387 & | & \verb+(+~\NT{term}~\verb+:+~\NT{term}~\verb+)+ & \mbox{(cast)} \\
388 & | & \verb+(+~\NT{term}~\verb+)+ \\
389 \NT{defs} & ::= & & \mbox{\bf mutual definitions} \\
390 & & \NT{fun}~\{\verb+and+~\NT{fun}\} \\
391 \NT{fun} & ::= & & \mbox{\bf functions} \\
392 & & \NT{arg}~\{\NT{ptnames}\}^{+}~[\verb+on+~x]~\verb+\def+~\NT{term} \\
393 \NT{binder} & ::= & & \mbox{\bf binders} \\
394 & & \verb+\forall+ \mid \verb+\lambda+ \\
395 \NT{arg} & ::= & & \mbox{\bf single argument} \\
396 & & \verb+_+ \mid x \\
397 \NT{ptname} & ::= & & \mbox{\bf possibly typed name} \\
399 & | & \verb+(+~\NT{arg}~\verb+:+~\NT{term}~\verb+)+ \\
400 \NT{ptnames} & ::= & & \mbox{\bf bound variables} \\
402 & | & \verb+(+~\NT{arg}~\{\verb+,+~\NT{arg}\}~[\verb+:+~\NT{term}]~\verb+)+ \\
403 \NT{kind} & ::= & & \mbox{\bf induction kind} \\
404 & & \verb+rec+ \mid \verb+corec+ \\
405 \NT{rule} & ::= & & \mbox{\bf rules} \\
406 & & x~\{\NT{ptname}\}~\verb+\Rightarrow+~\NT{term}
413 \subsubsection{Term input}
415 The primary form of user interaction employed by \MATITA{} is textual script
416 editing: the user modifies it and evaluate step by step its composing
417 \emph{statements}. Examples of statements are inductive type definitions,
418 theorem declarations, LCF-style tacticals, and macros (e.g. \texttt{Check} can
419 be used to ask the system to refine a given term and pretty print the result).
420 Since many statements refer to terms of the underlying calculus, \MATITA{} needs
421 a concrete syntax able to encode terms of the Calculus of Inductive
424 Two of the requirements in the design of such a syntax are apparently in
427 \item the syntax should be as close as possible to common mathematical practice
428 and implement widespread mathematical notations;
429 \item each term described by the syntax should be non-ambiguous meaning that it
430 should exists a function which associates to it a CIC term.
433 These two requirements are addressed in \MATITA{} by the mean of two mechanisms
434 which work together: \emph{term disambiguation} and \emph{extensible notation}.
435 Their interaction is visible in the architecture of the \MATITA{} input phase,
436 depicted in Fig.~\ref{fig:inputphase}. The architecture is articulated as a
437 pipline of three levels: the concrete syntax level (level 0) is the one the user
438 has to deal with when inserting CIC terms; the abstract syntax level (level 2)
439 is an internal representation which intuitively encodes mathematical formulae at
440 the content level~\cite{adams}\cite{mkm-structure}; the last level is that of
445 \includegraphics[width=0.9\textwidth]{input_phase}
446 \caption{\MATITA{} input phase}
448 \label{fig:inputphase}
451 Requirement (1) is addressed by a built-in concrete syntax for terms, described
452 in Tab.~\ref{tab:termsyn}, and the extensible notation mechanisms which offers a
453 way for extending available mathematical notations. Extensible notation, which
454 is also in charge of providing a parsing function mapping concrete syntax terms
455 to content level terms, is described in Sect.~\ref{sec:notation}. Requirement
456 (2) is addressed by the conjunct action of that parsing function and
457 disambiguation which provides a function from content level terms to CIC terms.
459 \subsubsection{Sources of ambiguity}
461 The translation from content level terms to CIC terms is not straightforward
462 because some nodes of the content encoding admit more that one CIC encoding,
463 invalidating requirement (2).
466 \label{ex:disambiguation}
468 Consider the term at the concrete syntax level \texttt{\TEXMACRO{forall} x. x +
469 ln 1 = x} of Fig.~\ref{fig:inputphase}(a), it can be the type of a lemma the
470 user may want to prove. Assuming that both \texttt{+} and \texttt{=} are parsed
471 as infix operators, all the following questions are legitimate and must be
472 answered before obtaining a CIC term from its content level encoding
473 (Fig.~\ref{fig:inputphase}(b)):
477 \item Since \texttt{ln} is an unbound identifier, which CIC constants does it
478 represent? Many different theorems in the library may share its (rather
481 \item Which kind of number (\IN, \IR, \dots) the \texttt{1} literal stand for?
482 Which encoding is used in CIC to represent it? E.g., assuming $1\in\IN$, is
483 it an unary or a binary encoding?
485 \item Which kind of equality the ``='' node represents? Is it Leibniz's
486 polymorhpic equality? Is it a decidable equality over \IN, \IR, \dots?
492 In \MATITA, three \emph{sources of ambiguity} are admitted for content level
493 terms: unbound identifiers, literal numbers, and operators. Each instance of
494 ambiguity sources (ambiguous entity) occuring in a content level term is
495 associated to a \emph{disambiguation domain}. Intuitively a disambiguation
496 domain is a set of CIC terms which may be replaced for an ambiguous entity
497 during disambiguation. Each item of the domain is said to be an
498 \emph{interpretation} for the ambiguous entity.
500 \emph{Unbound identifiers} (question 1) are ambiguous entities since the
501 namespace of CIC objects is not flat and the same identifier may denote many
502 ofthem. For example the short name \texttt{plus\_assoc} in the \HELM{} library
503 is shared by three different theorems stating the associative property of
504 different additions. This kind of ambiguity is avoidable if the user is willing
505 to use long names (in form of URIs in the \texttt{cic://} scheme) in the
506 concrete syntax, with the obvious drawbacks of obtaining long and unreadable
509 Given an unbound identifier, the corresponding disambiguation domain is computed
510 querying the library for all constants, inductive types, and inductive type
511 constructors having it as their short name (see the \LOCATE{} query in
512 Sect.~\ref{sec:metadata}).
514 \emph{Literal numbers} (question 2) are ambiguous entities as well since
515 different kinds of numbers can be encoded in CIC (\IN, \IR, \IZ, \dots) using
516 different encodings. Considering the restricted example of natural numbers we
517 can for instance encode them in CIC using inductive datatypes with a number of
518 constructor equal to the encoding base plus 1, obtaining one encoding for each
521 For each possible way of mapping a literal number to a CIC term, \MATITA{} is
522 aware of a \emph{number intepretation function} which, when applied to the
523 natural number denoted by the literal\footnote{at the moment only literal
524 natural number are supported in the concrete syntax} returns a corresponding CIC
525 term. The disambiguation domain for a given literal number is built applying to
526 the literal all available number interpretation functions in turn.
528 Number interpretation functions can be defined in OCaml or directly using
529 \TODO{notazione per i numeri}.
531 \emph{Operators} (question 3) are intuitively head of applications, as such they
532 are always applied to a (possiblt empty) sequence of arguments. Their ambiguity
533 is a need since it is often the case that some notation is used in an overloaded
534 fashion to hide the use of different CIC constants which encodes similar
535 concepts. For example, in the standard library of \MATITA{} the infix \texttt{+}
536 notation is available building a binary \texttt{Op(+)} node, whose
537 disambiguation domain may refer to different constants like the addition over
538 natural numbers \URI{cic:/matita/nat/plus/plus.con} or that over real numbers of
539 the \COQ{} standard library \URI{cic:/Coq/Reals/Rdefinitions/Rplus.con}.
541 For each possible way of mapping an operator application to a CIC term,
542 \MATITA{} knows an \emph{operator interpretation function} which, when applied
543 to an operator and its arguments, returns a CIC term. The disambiguation domain
544 for a given operator is built applying to the operator and its arguments all
545 available operator interpretation functions in turn.
547 Operator interpretation functions could be added using the
548 \texttt{interpretation} statement. For example, among the first line of the
549 script \FILE{matita/library/logic/equality.ma} from the \MATITA{} standard
553 interpretation "leibnitz's equality"
555 (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
558 Evaluating it in \MATITA{} will add an operator interpretation function for the
559 binary operator \texttt{eq} which expands to the CIC term on the right hand side
560 of the statement. That CIC term can be written using only built-in concrete
561 syntax, can contain no ambiguity source; still, it can refer to operator
562 arguments bound on the left hand side and can contain implicit terms (denoted
563 with \texttt{\_}) which will be expanded to fresh metavariables. The latter
564 feature is used in the example above for the first argument of Leibniz's
565 polymorhpic equality.
567 \subsubsection{Disambiguation algorithm}
569 A \emph{disambiguation algorithm} takes as input a content level term and return
570 a fully determined CIC term. The key observation on which a disambiguation
571 algorithm is based is that given a content level term with more than one sources
572 of ambiguity, not all possible combination of interpretation lead to a typable
573 CIC term. In the term of Ex.~\ref{ex:disambiguation} for instance the
574 interpretation of \texttt{ln} as a function from \IR to \IR and the
575 interpretation of \texttt{1} as the Peano number $1$ can't coexists. The notion
576 of ``can't coexists'' in the disambiguation of \MATITA{} is defined on top of
577 the \emph{refiner} for CIC terms described in~\cite{csc-phd}.
579 Briefly, a refiner is a function whose input is an \emph{incomplete CIC term}
580 $t_1$ --- i.e. a term where metavariables occur (Sect.~\ref{sec:metavariables}
581 --- and whose output is either:\NOTE{descrizione sommaria del refiner, pu\'o
582 essere spostata altrove}
586 \item an incomplete CIC term $t_2$ where $t_2$ is a well-typed term obtained
587 assigning a type to each metavariable in $t_1$ (in case of dependent types,
588 instantiation of some of the metavariable occurring in $t_1$ may occur as
591 \item $\epsilon$, meaning that no well-typed term could be obtained via
592 assignment of type to metavariable in $t_1$ and their instantiation;
594 \item $\bot$, meaning that the refiner is unable to decide whether of the two
595 cases above apply (refinement is semi-decidable).
599 On top of a CIC refiner \MATITA{} implement an efficient disambiguation
600 algorithm, which is outlined below. It takes as input a content level term $c$
601 and proceeds as follows:
605 \item Create disambiguation domains $\{D_i | i\in\mathit{Dom}(c)\}$, where
606 $\mathit{Dom}(c)$ is the set of ambiguity sources of $c$. Each $D_i$ is a set
607 of CIC terms and can be built as described above.
609 \item An \emph{interpretation} $\Phi$ for $c$ is a map associating an
610 incomplete CIC term to each ambiguity source of $c$. Given $c$ and one of its
611 interpretations an incomplete CIC term is fully determined replacing each
612 ambiguity source of $c$ with its mapping in the interpretation and injecting
613 the remaining structure of the content level in the CIC level (e.g. replacing
614 the application of the content level with the application of the CIC level).
615 This operation is informally called ``interpreting $c$ with $\Phi$''.
617 Create an initial interpretation $\Phi_0 = \{\phi_i | \phi_i = \_,
618 i\in\mathit{Dom}(c)\}$, which associates a fresh metavariable to each source
619 of ambiguity of $c$. During this step, implicit terms are expanded to fresh
620 metavariables as well.
622 \item Refine the current incomplete CIC term (i.e. the term obtained
623 interpreting $t$ with $\Phi_i$).
625 If the refinement succeeds or is undetermined the next interpretation
626 $\Phi_{i+1}$ will be created \emph{making a choice}, that is replacing in the
627 current interpretation one of the metavariable appearing in $\Phi_i$ with one
628 of the possible choice from the corresponding disambiguation domain. The
629 metavariable to be replaced is chosen following a preorder visit of the
630 ambiguous term. Then, step 3 is attempted again with the new interpretation.
632 If the refinement fails the current set of choices cannot lead to a well-typed
633 term and backtracking of the current interpretation is attempted.
635 \item Once an unambiguous correct interpretation is found (i.e. $\Phi_i$ does
636 no longer contain any placeholder), backtracking is attempted anyway to find
637 the other correct interpretations.
639 \item Let $n$ be the number of interpretations who survived step 4. If $n=0$
640 signal a type error. If $n=1$ we have found exactly one (incomplete) CIC term
641 corresponding to the content level term $c$, returns it as output of the
642 disambiguation phase. If $n>1$ we have found many different (incomplete) CIC
643 terms which can correspond to the content level term, let the user choose one
644 of the $n$ interpretations and returns the corresponding term.
648 The efficiency of this algorithm resides in the fact that as soon as an
649 incomplete CIC term is not typable, no further instantiation of the
650 metavariables of the corresponding interpretation is attemped.
651 % For example, during the disambiguation of the user input
652 % \texttt{\TEXMACRO{forall} x. x*0 = 0}, an interpretation $\Phi_i$ is
653 % encountered which associates $?$ to the instance of \texttt{0} on the right,
654 % the real number $0$ to the instance of \texttt{0} on the left, and the
655 % multiplication over natural numbers (\texttt{mult} for short) to \texttt{*}.
656 % The refiner will fail, since \texttt{mult} require a natural argument, and no
657 % further instantiation of the placeholder will be tried.
659 Details of the disambiguation algorithm along with an analysis of its complexity
660 can be found in~\cite{disambiguation}, where a formulation without backtracking
661 (corresponding to the actual \MATITA{} implementation) is also presented.
663 \subsubsection{Disambiguation stages}
665 \subsection{notazione}
672 \subsection{selezione semantica, cut paste, hyperlink}
677 Patterns are the textual counterpart of the MathML widget graphical
680 Matita benefits of a graphical interface and a powerful MathML rendering
681 widget that allows the user to select pieces of the sequent he is working
682 on. While this is an extremely intuitive way for the user to
683 restrict the application of tactics, for example, to some subterms of the
684 conclusion or some hypothesis, the way this action is recorded to the text
685 script is not obvious.\\
686 In \MATITA{} this issue is addressed by patterns.
688 \subsubsection{Pattern syntax}
689 A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
691 The former mocks-up a sequent, discharging unwanted subterms with $?$ and
692 selecting the interesting parts with the placeholder $\%$.
693 The latter is a term that lives in the context of the placeholders.
695 The concrete syntax is reported in table \ref{tab:pathsyn}
696 \NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
698 \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
701 \begin{array}{@{}rcll@{}}
703 ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
705 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
706 [~\verb+\vdash+~\NT{multipath}~] & \\
707 \NT{wanted} & ::= & \NT{term} & \\
708 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
714 \subsubsection{How patterns work}
715 Patterns mimic the user's selection in two steps. The first one
716 selects roots (subterms) of the sequent, using the
717 $\NT{sequent\_path}$, while the second
718 one searches the $\NT{wanted}$ term starting from these roots. Both are
719 optional steps, and by convention the empty pattern selects the whole
724 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
725 part of the syntax. $\NT{ident}$ is an hypothesis name and
726 selects the assumption where the following optional $\NT{multipath}$
727 will operate. \verb+\vdash+ can be considered the name for the goal.
728 If the whole pattern is omitted, the whole goal will be selected.
729 If one or more hypotheses names are given the selection is restricted to
730 these assumptions. If a $\NT{multipath}$ is omitted the whole
731 assumption is selected. Remember that the user can be mostly
732 unaware of this syntax, since the system is able to write down a
733 $\NT{sequent\_path}$ starting from a visual selection.
734 \NOTE{Questo ancora non va in matita}
736 A $\NT{multipath}$ is a CiC term in which a special constant $\%$
738 The roots of discharged subterms are marked with $?$, while $\%$
739 is used to select roots. The default $\NT{multipath}$, the one that
740 selects the whole term, is simply $\%$.
741 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
742 that respectively select the first argument of an application or
743 the source of an arrow and the head of the application that is
744 found in the arrow target.
746 The first phase selects not only terms (roots of subterms) but also
747 their context that will be eventually used in the second phase.
750 plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
751 part is specified. From the first phase we have some terms, that we
752 will see as subterm roots, and their context. For each of these
753 contexts the $\NT{wanted}$ term is disambiguated in it and the
754 corresponding root is searched for a subterm $\alpha$-equivalent to
755 $\NT{wanted}$. The result of this search is the selection the
761 Since the first step is equipotent to the composition of the two
762 steps, the system uses it to represent each visual selection.
763 The second step is only meant for the
764 experienced user that writes patterns by hand, since it really
765 helps in writing concise patterns as we will see in the
768 \subsubsection{Examples}
769 To explain how the first step works let's give an example. Consider
770 you want to prove the uniqueness of the identity element $0$ for natural
771 sum, and that you can relay on the previously demonstrated left
772 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
775 theorem valid_name: \forall n,m. m + n = n \to m = O.
779 leads you to the following sequent
787 where you want to change the right part of the equivalence of the $H$
788 hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
790 change in H:(? ? ? %) with (O + n).
793 This pattern, that is a simple instance of the $\NT{sequent\_path}$
794 grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
795 and discharges the head of the application and the first two arguments with a
796 $?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
797 but the user can simply select with the mouse the right part of the equivalence
798 and left to the system the burden of writing down in the script file the
799 corresponding pattern with $?$ and $\%$ in the right place (that is not
800 trivial, expecially where implicit arguments are hidden by the notation, like
801 the type $nat$ in this example).
803 Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
804 works too and can be done, by the experienced user, writing directly
805 a simpler pattern that uses the second phase.
807 change in match n in H with (O + n).
810 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
811 the second phase searches the wanted $n$ inside it by
812 $\alpha$-equivalence. The resulting
813 equivalence will be $m+(O+n)=O+n$ since the second phase found two
814 occurrences of $n$ in $H$ and the tactic changed both.
816 Just for completeness the second pattern is equivalent to the
817 following one, that is less readable but uses only the first phase.
819 change in H:(? ? (? ? %) %) with (O + n).
823 \subsubsection{Tactics supporting patterns}
824 In \MATITA{} all the tactics that can be restricted to subterm of the working
825 sequent accept the pattern syntax. In particular these tactics are: simplify,
826 change, fold, unfold, generalize, replace and rewrite.
828 \NOTE{attualmente rewrite e fold non supportano phase 2. per
829 supportarlo bisogna far loro trasformare il pattern phase1+phase2
830 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
831 con una pattern\_of(select(pattern))}
833 \subsubsection{Comparison with Coq}
834 Coq has a two diffrent ways of restricting the application of tactis to
835 subterms of the sequent, both relaying on the same special syntax to identify
838 The first way is to use this special syntax to specify directly to the
839 tactic the occurrnces of a wanted term that should be affected, while
840 the second is to prepare the sequent with another tactic called
841 pattern and the apply the real tactic. Note that the choice is not
842 left to the user, since some tactics needs the sequent to be prepared
843 with pattern and do not accept directly this special syntax.
845 The base idea is that to identify a subterm of the sequent we can
846 write it and say that we want, for example, the third and the fifth
847 occurce of it (counting from left to right). In our previous example,
848 to change only the left part of the equivalence, the correct command
851 change n at 2 in H with (O + n)
854 meaning that in the hypothesis $H$ the $n$ we want to change is the
855 second we encounter proceeding from left toright.
857 The tactic pattern computes a
858 $\beta$-expansion of a part of the sequent with respect to some
859 occurrences of the given term. In the previous example the following
865 would have resulted in this sequent
869 H : (fun n0 : nat => m + n = n0) n
870 ============================
874 where $H$ is $\beta$-expanded over the second $n$
875 occurrence. This is a trick to make the unification algorithm ignore
876 the head of the application (since the unification is essentially
877 first-order) but normally operate on the arguments.
878 This works for some tactics, like rewrite and replace,
879 but for example not for change and other tactics that do not relay on
882 The idea behind this way of identifying subterms in not really far
883 from the idea behind patterns, but really fails in extending to
884 complex notation, since it relays on a mono-dimensional sequent representation.
885 Real math notation places arguments upside-down (like in indexed sums or
886 integrations) or even puts them inside a bidimensional matrix.
887 In these cases using the mouse to select the wanted term is probably the
888 only way to tell the system exactly what you want to do.
890 One of the goals of \MATITA{} is to use modern publishing techiques, and
891 adopting a method for restricting tactics application domain that discourages
892 using heavy math notation, would definitively be a bad choice.
894 \subsection{Tacticals}
896 There are mainly two kinds of languages used by proof assistants to recorder
897 proofs: tactic based and declarative. We will not investigate the philosophy
898 aroud the choice that many proof assistant made, \MATITA{} included, and we will not compare the two diffrent approaches. We will describe the common issues of the first one and how \MATITA{} tries to solve them.
900 For first we must highlight the fact that proof scripts made using tactis are
901 particularly unreadable. This is not a big deal for the user while he iw
902 constructing the proof, but is considerably a problem when he tries to reread
903 what he did or whe he shows his work to someone else.
905 Another common issue for tactic based proof scripts is their mantenibility.
906 Huge libraries have been developed, and backward compatibility is a really time
907 consuming task. This problem is usually ameliorated with tacticals, that
908 contibute structuring proofs, but rise one more difficulty for the user that
909 want to read a proof, since they are executed in an atomic way, making the
910 user loose intermediate steps.
912 \MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
913 strategy to make this technique more user friendly without loosing in
914 mantenibility or expressivity.
916 \subsubsection{Tacticals overview}
917 Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
919 Tacticals first appered in LCF(cita qualcosa) and can be seen as programming constructs, like
920 looping, branching, error recovery or sequential composition.
922 \MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
924 \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
927 \begin{array}{@{}rcll@{}}
929 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
931 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
932 \NT{block\_delimiter} &
933 ::= & \verb+begin+ ~|~ \verb+end+ & \\
935 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
941 While one whould expect to find structured constructs like
942 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
943 This is essential for base idea behind matita tacticals: step-by-step execution.
945 \subsubsection{\MATITA{} Tinycals}
946 The low-level tacticals implementation of \MATITA{} allows a step-by-step execution of a tactical, that substantially means that a $\NT{block\_kind}$ is not execute as an atomic operation. This has two major benefits for the user, even being a so simple idea:
948 \item[Proof structuring]
949 is much easyer. Consider for example a proof by induction. After applying the
950 induction principle, with one step tacticals, you have to choose: structure
951 the proof or not. If you decide for the former you have to branch with
952 \verb+[+ and write tactics for all the cases and the close the tactical with
953 \verb+]+. You can replace most of the cases by the identity tactic just to
954 concentrate only on the first goal, but you will have to one step back and
955 one further every time you add something inside the tactical. And if you are
956 boared of doing so, you will finish in giving up structuring the proof and
957 write a plain list of tactics.
959 is possible. Going on step by step shows exactly what is going on.
960 Consider again a proof by induction, that starts applying the induction
961 principle and suddenly baranches with a \verb+[+. This clearly subdivided all
962 the induction cases, but if the square brackets content is executed in one
963 single step you completely loose the possibility of rereading it. Again,
964 executing step-by-step is the way you whould like to review the
965 demonstration. Remember tha understandig the proof from the script is not
966 easy, and only the execution of tactics (and the resulting transformed goal)
967 gives you the feeling of what is goning on.
972 \subsection{named variable e disambiguazione lazy}
975 \subsection{metavariabili}
976 \label{sec:metavariables}
983 \section{Drawbacks, missing, \dots}
991 \subsection{estrazione}
994 \subsection{localizzazione errori}
998 We would like to thank all the students that during the past
999 five years collaborated in the \HELM{} project and contributed to
1000 the development of Matita, and in particular
1001 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
1006 \bibliography{matita}