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,
119 \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
120 \caption{\MATITA{} libraries}
122 \label{fig:libraries}
125 \section{Overview of the Architecture}
126 Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
127 and \emph{applications} (squared nodes) developed in the HELM project.
129 Applications and libraries depend over other libraries forming a
130 directed acyclic graph (DAG). Each library can be decomposed in
131 a a set of \emph{modules} also forming a DAG.
133 Modules and libraries provide coherent sets of functionalities
134 at different scales. Applications that require only a few functionalities
135 depend on a restricted set of libraries. \MATITA, our most complex
136 application, depends on every library.
138 Only the proof assistant \MATITA{} is an application meant to be used directly
139 by the user. All the other applications are Web services developed in the
140 HELM and MoWGLI projects and already described elsewhere. In particular:
142 \item The \emph{Getter} is a Web service to retrieve an (XML) document
143 from a physical location (URL) given its logical name (URI). The Getter is
144 responsible of updating a table that maps URIs to URLs. Thanks to the Getter
145 it is possible to work on a logically monolithic library that is physically
146 distributed on the network. More information on the Getter can be found
148 \item \emph{Whelp} is a search engine to index and locate mathematical
149 notions (axioms, theorems, definitions) in the logical library managed
150 by the Getter. Typical examples of a query to Whelp are queries that search
151 for a theorem that generalize or instantiate a given formula, or that
152 can be immediately applied to prove a given goal. The output of Whelp is
153 an XML document that lists the URIs of a complete set of candidates that
154 are likely to satisfy the given query. The set is complete in the sense
155 that no notion that actually satisfies the query is thrown away. However,
156 the query is only approssimated in the sense that false matches can be
157 returned. Whelp has been described in~\cite{whelp}.
158 \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
159 notion in the distributed library, renders it according to the user provided
160 two dimensional mathematical notation. Uwobo may also embed the rendering
161 of mathematical notions into arbitrary documents before returning them.
162 The Getter is used by Uwobo to retrieve the document to be rendered.
163 Uwobo has been described in~\cite{uwobo}.
164 \item The \emph{Proof Checker} is a Web service that, given the URI of
165 notion in the distributed library, checks its correctness. Since the notion
166 is likely to depend in an acyclic way over other notions, the proof checker
167 is also responsible of building in a top-down way the DAG of all
168 dependencies, checking in turn every notion for correctness.
169 The proof checker has been described in~\cite{proofchecker}.
170 \item The \emph{Dependency Analyzer} is a Web service that can produce
171 a textual or graphical representation of the dependecies of an object.
172 The dependency analyzer has been described in~\cite{dependencyanalyzer}.
175 The dependency of a library or application over another library can
176 be satisfied by linking the library in the same executable.
177 For those libraries whose functionalities are also provided by the
178 aforementioned Web services, it is also possible to link stub code that
179 forwards the request to a remote Web service. For instance, the Getter
180 is just a wrapper to the \texttt{getter} library that allows the library
181 to be used as a Web service. \MATITA{} can directly link the code of the
182 \texttt{getter} library, or it can use a stub library with the same API
183 that forwards every request to the Getter.
185 To better understand the architecture of \MATITA{} and the role of each
186 library, we can focus on the representation of the mathematical information.
187 \MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
188 Constructions (CIC). In CIC terms are used to represent mathematical
189 expressions, types and proofs. \MATITA{} is able to handle terms at
190 four different levels of refinement. On each level it is possible to provide a
191 different set of functionalities. The four different levels are:
192 fully specified terms; partially specified terms; terms
193 at the content level; terms at the presentation level.
195 \subsection{Fully specified terms}
196 \emph{Fully specified terms} are CIC terms where no information is
197 missing or left implicit. A fully specified term should be well-typed.
198 The mathematical notions (axioms, definitions, theorems) that are stored
199 in our mathematical library are fully specified and well-typed terms.
200 Fully specified terms are extremely verbose (to make type-checking
201 decidable). Their syntax is fixed and does not resemble the usual
202 extendible mathematical notation. They are not meant for direct user
205 The \texttt{cic} library defines the data type that represents CIC terms
206 and provides a parser for terms stored in an XML format.
208 The most important library that deals with fully specified terms is
209 \texttt{cic\_proof\_checking}. It implements the procedure that verifies
210 if a fully specified term is well-typed. It also implements the
211 \emph{conversion} judgement that verifies if two given terms are
212 computationally equivalent (i.e. they share the same normal form).
214 Terms may reference other mathematical notions in the library.
215 One commitment of our project is that the library should be physically
216 distributed. The \texttt{getter} library manages the distribution,
217 providing a mapping from logical names (URIs) to the physical location
218 of a notion (an URL). The \texttt{urimanager} library provides the URI
219 data type and several utility functions over URIs. The
220 \texttt{cic\_proof\_checking} library calls the \texttt{getter} library
221 every time it needs to retrieve the definition of a mathematical notion
222 referenced by a term that is being type-checked.
224 The Proof Checker is the Web service that provides an HTTP interface
225 to the \texttt{cic\_proof\_checking} library.
227 We use metadata and a sort of crawler to index the mathematical notions
228 in the distributed library. We are interested in retrieving a notion
229 by matching, instantiation or generalization of a user or system provided
230 mathematical expression. Thus we need to collect metadata over the fully
231 specified terms and to store the metadata in some kind of (relational)
232 database for later usage. The \texttt{hmysql} library provides a simplified
233 interface to a (possibly remote) MySql database system used to store the
234 metadata. The \texttt{metadata} library defines the data type of the metadata
235 we are collecting and the functions that extracts the metadata from the
236 mathematical notions (the main functionality of the crawler).
237 The \texttt{whelp} library implements a search engine that performs
238 approximated queries by matching/instantiation/generalization. The queries
239 operate only on the metadata and do not involve any actual matching
240 (that will be described later on and that is implemented in the
241 \texttt{cic\_unification} library). Not performing any actual matching
242 the query only returns a complete and hopefully small set of matching
243 candidates. The process that has issued the query is responsible of
244 actually retrieving from the distributed library the candidates to prune
245 out false matches if interested in doing so.
247 The Whelp search engine is the Web service that provides an interface to
248 the \texttt{whelp} library.
250 \subsection{Partially specified terms}
251 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
252 Omitted subterms can bear no information at all or they may be associated to
253 a sequent. The formers are called \emph{implicit terms} and they occur only
254 linearly. The latters may occur multiple times and are called
255 \emph{metavariables}. An \emph{explicit substitution} is applied to each
256 occurrence of a metavariable. A metavariable stand for a term whose type is
257 given by the conclusion of the sequent. The term must be closed in the
258 context that is given by the ordered list of hypotheses of the sequent.
259 The explicit substitution instantiates every hypothesis with an actual
260 value for the term bound by the hypothesis.
262 Partially specified terms are not required to be well-typed. However a
263 partially specified term should be \emph{refinable}. A \emph{refiner} is
264 a type-inference procedure that can instantiate implicit terms and
265 metavariables and that can introduce \emph{implicit coercions} to make a
266 partially specified term be well-typed. The refiner of \MATITA{} is implemented
267 in the \texttt{cic\_unification} library. As the type checker is based on
268 the conversion check, the refiner is based on \emph{unification} that is
269 a procedure that makes two partially specified term convertible by instantiating
270 as few as possible metavariables that occur in them.
272 Since terms are use in CIC to represent proofs, so far correct incomplete
273 proofs are represented by refinable partially specified terms. The metavariables
274 that occur in the proof correspond to the conjectures still to be proved.
275 The sequent associated to the metavariable is the conjecture the user needs to
278 \emph{Tactics} are the procedures that the user can apply to progress in the
279 proof. A tactic proves a conjecture possibly creating new (and hopefully
280 simpler) conjectures. The implementation of tactics is given in the
281 \texttt{tactics} library. It is heavily based on the refinement and unification
282 procedures of the \texttt{cic\_unification} library.
284 As fully specified terms, partially specified terms are not well suited
285 for user consumption since their syntax is not extendible and it is not
286 possible to adopt the usual mathematical notation. However they are already
287 an improvement over fully specified terms since they allow to omit redundant
288 information that can be inferred by the refiner.
290 \subsection{Terms at the content level}
291 The language used to communicate proofs and expecially expressions with the
292 user does not only needs to be extendible and accomodate the usual mathematical
293 notation. It must also reflect the comfortable degree of imprecision and
294 ambiguity that the mathematical language provides.
296 For instance, it is common practice in mathematics to speak of a generic
297 equality that can be used to compare any two terms. However, it is well known
298 that several equalities can be identified as soon as we care for decidability
299 or for their computational properties. For instance equality over real
300 numbers is well known to be undecidable, whereas it is decidable over
303 Similarly, we usually speak of natural numbers and their operations and
304 properties without caring about their representation. However the computational
305 properties of addition over the binary representation are very different from
306 those of addition over the unary representation. And addition over two natural
307 numbers is definitely different from addition over two real numbers.
309 Formal mathematics cannot hide these differences and obliges the user to be
310 very precise on the types he is using and their representation. However,
311 to communicate formulae with the user and with external tools, it seems good
312 practice to stick to the usual imprecise mathematical ontology. In the
313 Mathematical Knowledge Management community this imprecise language is called
314 the \emph{content level} representation of expressions.
316 In \MATITA{} we provide two translations from partially specified terms
317 to content level terms and the other way around. The first translation can also
318 be applied to fully specified terms since a fully specified term is a special
319 case of partially specified term where no metavariable or implicit term occurs.
321 The translation from partially specified terms to content level terms must
322 discriminate between terms used to represent proofs and terms used to represent
323 expressions. The firsts are translated to a content level representation of
324 proof steps that can easily be rendered in natural language. The latters
325 are translated to MathML Content formulae. MathML Content is a W3C standard
326 for the representation of content level expressions in an XML extensible format.
328 The translation to content level is implemented in the
329 \texttt{acic\_content} library. Its input are \emph{annotated partially
330 specified terms}. Annotated partially specified terms are maximally unshared
331 partially specified terms enriched with additional typing information for each
332 subterm. This information is used to discriminate between terms that represent
333 proofs and terms that represent expressions. Part of it is also stored at the
334 content level since it is required to generate the natural language rendering
335 of proofs. The terms need to be maximally unshared (i.e. they must be a tree
336 and not a DAG). The reason is that to the occurrences of a subterm in
337 two different positions we need to associate different typing informations.
338 This association is made easier when the term is represented as a tree since
339 it is possible to label each node with an unique identifier and associate
340 the typing information using a map on the identifiers.
341 The \texttt{cic\_acic} library annotates partially specified terms.
343 We do not provide yet a reverse translation from content level proofs to
344 partially specified terms. But in \texttt{disambiguation} we do provide
345 the reverse translation for expressions. The mapping from
346 content level expressions to partially specified terms is not unique due to
347 the ambiguity of the content level. As a consequence the translation
348 is guided by an \emph{interpretation}, that is a function that chooses for
349 every ambiguous expression one partially specified term. The
350 \texttt{disambiguation} library contains the implementation of the
351 disambiguation algorithm we presented in \cite{disambiguation} that is
352 responsible of building in an efficicent way the set of all ``correct''
353 interpretations. An interpretation is correct if the partially refined term
354 obtained using the interpretation is refinable.
356 \subsection{Terms at the presentation level}
358 Content level terms are a sort of abstract syntax trees for mathematical
359 expressions and proofs. The concrete syntax given to these abstract trees
360 is called \emph{presentation level}.
362 The main important difference between the content level language and the
363 presentation level language is that only the former is extendible. Indeed,
364 the presentation level language is a finite language that comprises all
365 the usual mathematical symbols. Mathematicians invent new notions every
366 single day, but they stick to a set of symbols that is more or less fixed.
368 The fact that the presentation language is finite allows the definition of
369 standard languages. In particular, for formulae we have adopt MathML
370 Presentation that is an XML dialect standardized by the W3C. To visually
371 represent proofs it is enough to embed formulae in plain text enriched with
372 formatting boxes. Since the language of formatting boxes is very simple,
373 many equivalent specifications exist and we have adopted our own, called
376 The \texttt{content\_pres} library contains the implementation of the
377 translation from content level terms to presentation level terms. The
378 rendering of presentation level terms is left to the application that uses
379 the library. However, in the \texttt{hgdome} library we provide a few
380 utility functions to build a GDOM MathML+BoxML tree from our presentation
381 level terms. GDOM MathML+BoxML trees can be rendered by the GtkMathView
382 widget developed by Luca Padovani \cite{gtkmathview}. The widget is
383 particularly interesting since it allows to implement \emph{semantic
386 Semantic selection is a technique that consists in enriching the presentation
387 level terms with pointers to the content level terms and to the partially
388 refined terms they correspond to. Highlight of formulae in the widget is
389 constrained to selection of meaningful expressions, i.e. expressions that
390 correspond to a lower level term. Once the rendering of a lower level term is
391 selected it is possible for the application to retrieve the pointer to the
392 lower level term. An example of applications of semantic selection is
393 \emph{semantic cut\&paste}: the user can select an expression and paste it
394 elsewhere preserving its semantics (i.e. the partially enriched term),
395 possibly performing some semantic transformation over it (e.g. renaming
396 variables that would be captured or lambda-lifting free variables).
398 The reverse translation from presentation level terms to content level terms
399 is implemented by a parser that is also found in \texttt{content\_pres}.
400 Differently from the translation from content level terms to partially
401 refined terms, this translation is not ambiguous. The reason is that the
402 parsing library we have adopted (CamlP4) is not able to parse ambiguous
403 grammars. Thus we require the mapping from presentation level terms
404 (concrete syntax) to content level terms (abstract syntax) to be unique.
405 This means that the user must fix once and for all the associativity and
406 precedence level of every operator is he using. In prctice this limitation
407 does not seem too strong. The reason is that the target of the
408 translation is an ambiguous language and the user is free to associate
409 to every content level term several different interpretations (as a
410 partially specified term).
414 At the bottom of the DAG we have a few libraries (\texttt{extlib},
415 \texttt{xml} and the \texttt{registry}) that provide a core of
416 useful functions used everywhere else. In particular, the \texttt{xml} library
417 to easily represent, parse and pretty-print XML files is a central component
418 since in HELM every piece of information is stored in \ldots. [FINIRE]
419 The other basic libraries provide often needed operations over generic
420 data structures (\texttt{extlib}) and central storage for configuration options
421 (the \texttt{registry}).
429 \section{Partially specified terms}
430 --- il mondo delle tattiche e dintorni ---
431 serve una intro che almeno cita il widget (per i patterns) e che fa
432 il resoconto delle cose che abbiamo e che non descriviamo,
433 sottolineando che abbiamo qualcosa da dire sui pattern e sui
438 \subsection{Patterns}
439 Patterns are the textual counterpart of the MathML widget graphical
442 Matita benefits of a graphical interface and a powerful MathML rendering
443 widget that allows the user to select pieces of the sequent he is working
444 on. While this is an extremely intuitive way for the user to
445 restrict the application of tactics, for example, to some subterms of the
446 conclusion or some hypothesis, the way this action is recorded to the text
447 script is not obvious.\\
448 In \MATITA{} this issue is addressed by patterns.
450 \subsubsection{Pattern syntax}
451 A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
453 The former mocks-up a sequent, discharging unwanted subterms with $?$ and
454 selecting the interesting parts with the placeholder $\%$.
455 The latter is a term that lives in the context of the placeholders.
457 The concrete syntax is reported in table \ref{tab:pathsyn}
458 \NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
460 \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
463 \begin{array}{@{}rcll@{}}
465 ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
467 ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
468 [~\verb+\vdash+~\NT{multipath}~] & \\
469 \NT{wanted} & ::= & \NT{term} & \\
470 \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
476 \subsubsection{How patterns work}
477 Patterns mimic the user's selection in two steps. The first one
478 selects roots (subterms) of the sequent, using the
479 $\NT{sequent\_path}$, while the second
480 one searches the $\NT{wanted}$ term starting from these roots. Both are
481 optional steps, and by convention the empty pattern selects the whole
486 concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
487 part of the syntax. $\NT{ident}$ is an hypothesis name and
488 selects the assumption where the following optional $\NT{multipath}$
489 will operate. \verb+\vdash+ can be considered the name for the goal.
490 If the whole pattern is omitted, the whole goal will be selected.
491 If one or more hypotheses names are given the selection is restricted to
492 these assumptions. If a $\NT{multipath}$ is omitted the whole
493 assumption is selected. Remember that the user can be mostly
494 unaware of this syntax, since the system is able to write down a
495 $\NT{sequent\_path}$ starting from a visual selection.
496 \NOTE{Questo ancora non va in matita}
498 A $\NT{multipath}$ is a CiC term in which a special constant $\%$
500 The roots of discharged subterms are marked with $?$, while $\%$
501 is used to select roots. The default $\NT{multipath}$, the one that
502 selects the whole term, is simply $\%$.
503 Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
504 that respectively select the first argument of an application or
505 the source of an arrow and the head of the application that is
506 found in the arrow target.
508 The first phase selects not only terms (roots of subterms) but also
509 their context that will be eventually used in the second phase.
512 plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
513 part is specified. From the first phase we have some terms, that we
514 will see as subterm roots, and their context. For each of these
515 contexts the $\NT{wanted}$ term is disambiguated in it and the
516 corresponding root is searched for a subterm $\alpha$-equivalent to
517 $\NT{wanted}$. The result of this search is the selection the
523 Since the first step is equipotent to the composition of the two
524 steps, the system uses it to represent each visual selection.
525 The second step is only meant for the
526 experienced user that writes patterns by hand, since it really
527 helps in writing concise patterns as we will see in the
530 \subsubsection{Examples}
531 To explain how the first step works let's give an example. Consider
532 you want to prove the uniqueness of the identity element $0$ for natural
533 sum, and that you can relay on the previously demonstrated left
534 injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
537 theorem valid_name: \forall n,m. m + n = n \to m = O.
541 leads you to the following sequent
549 where you want to change the right part of the equivalence of the $H$
550 hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
552 change in H:(? ? ? %) with (O + n).
555 This pattern, that is a simple instance of the $\NT{sequent\_path}$
556 grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
557 and discharges the head of the application and the first two arguments with a
558 $?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
559 but the user can simply select with the mouse the right part of the equivalence
560 and left to the system the burden of writing down in the script file the
561 corresponding pattern with $?$ and $\%$ in the right place (that is not
562 trivial, expecially where implicit arguments are hidden by the notation, like
563 the type $nat$ in this example).
565 Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
566 works too and can be done, by the experienced user, writing directly
567 a simpler pattern that uses the second phase.
569 change in match n in H with (O + n).
572 In this case the $\NT{sequent\_path}$ selects the whole $H$, while
573 the second phase searches the wanted $n$ inside it by
574 $\alpha$-equivalence. The resulting
575 equivalence will be $m+(O+n)=O+n$ since the second phase found two
576 occurrences of $n$ in $H$ and the tactic changed both.
578 Just for completeness the second pattern is equivalent to the
579 following one, that is less readable but uses only the first phase.
581 change in H:(? ? (? ? %) %) with (O + n).
585 \subsubsection{Tactics supporting patterns}
586 In \MATITA{} all the tactics that can be restricted to subterm of the working
587 sequent accept the pattern syntax. In particular these tactics are: simplify,
588 change, fold, unfold, generalize, replace and rewrite.
590 \NOTE{attualmente rewrite e fold non supportano phase 2. per
591 supportarlo bisogna far loro trasformare il pattern phase1+phase2
592 in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
593 con una pattern\_of(select(pattern))}
595 \subsubsection{Comparison with Coq}
596 Coq has a two diffrent ways of restricting the application of tactis to
597 subterms of the sequent, both relaying on the same special syntax to identify
600 The first way is to use this special syntax to specify directly to the
601 tactic the occurrnces of a wanted term that should be affected, while
602 the second is to prepare the sequent with another tactic called
603 pattern and the apply the real tactic. Note that the choice is not
604 left to the user, since some tactics needs the sequent to be prepared
605 with pattern and do not accept directly this special syntax.
607 The base idea is that to identify a subterm of the sequent we can
608 write it and say that we want, for example, the third and the fifth
609 occurce of it (counting from left to right). In our previous example,
610 to change only the left part of the equivalence, the correct command
613 change n at 2 in H with (O + n)
616 meaning that in the hypothesis $H$ the $n$ we want to change is the
617 second we encounter proceeding from left toright.
619 The tactic pattern computes a
620 $\beta$-expansion of a part of the sequent with respect to some
621 occurrences of the given term. In the previous example the following
627 would have resulted in this sequent
631 H : (fun n0 : nat => m + n = n0) n
632 ============================
636 where $H$ is $\beta$-expanded over the second $n$
637 occurrence. This is a trick to make the unification algorithm ignore
638 the head of the application (since the unification is essentially
639 first-order) but normally operate on the arguments.
640 This works for some tactics, like rewrite and replace,
641 but for example not for change and other tactics that do not relay on
644 The idea behind this way of identifying subterms in not really far
645 from the idea behind patterns, but really fails in extending to
646 complex notation, since it relays on a mono-dimensional sequent representation.
647 Real math notation places arguments upside-down (like in indexed sums or
648 integrations) or even puts them inside a bidimensional matrix.
649 In these cases using the mouse to select the wanted term is probably the
650 only way to tell the system exactly what you want to do.
652 One of the goals of \MATITA{} is to use modern publishing techiques, and
653 adopting a method for restricting tactics application domain that discourages
654 using heavy math notation, would definitively be a bad choice.
656 \subsection{Tacticals}
657 There are mainly two kinds of languages used by proof assistants to recorder
658 proofs: tactic based and declarative. We will not investigate the philosophy
659 aroud the choice that many proof assistant made, \MATITA{} included, and we
660 will not compare the two diffrent approaches. We will describe the common
661 issues of the tactic-based language approach and how \MATITA{} tries to solve
664 \subsubsection{Tacticals overview}
666 Tacticals first appeared in LCF and can be seen as programming
667 constructs, like looping, branching, error recovery or sequential composition.
668 The following simple example shows three tacticals in action
672 A = B \to ((A \to B) \land (B \to A)).
675 [ rewrite < H. assumption.
676 | rewrite > H. assumption.
681 The first is ``\texttt{;}'' that combines the tactic \texttt{split}
682 with \texttt{intro}, applying the latter to each goal opened by the
683 former. Then we have ``\texttt{[}'' that branches on the goals (here
684 we have two goals, the two sides of the logic and).
685 The first goal $B$ (with $A$ in the context)
686 is proved by the first sequence of tactics
687 \texttt{rewrite} and \texttt{assumption}. Then we move to the second
688 goal with the separator ``\texttt{|}''. The last tactical we see here
689 is ``\texttt{.}'' that is a sequential composition that selects the
690 first goal opened for the following tactic (instead of applying it to
691 them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
692 not considered a tactical, but a sentence terminator (i.e. the
693 delimiter of commands the proof assistant executes).
695 Giving serious examples here is rather difficult, since they are hard
696 to read without the interactive tool. To help the reader in
697 understanding the following considerations we just give few common
698 usage examples without a proof context.
701 elim z; try assumption; [ ... | ... ].
702 elim z; first [ assumption | reflexivity | id ].
705 The first example goes by induction on a term \texttt{z} and applies
706 the tactic \texttt{assumption} to each opened goal eventually recovering if
707 \texttt{assumption} fails. Here we are asking the system to close all
708 trivial cases and then we branch on the remaining with ``\texttt{[}''.
709 The second example goes again by induction on \texttt{z} and tries to
710 close each opened goal first with \texttt{assumption}, if it fails it
711 tries \texttt{reflexivity} and finally \texttt{id}
712 that is the tactic that leaves the goal untouched without failing.
714 Note that in the common implementation of tacticals both lines are
715 compositions of tacticals and in particular they are a single
716 statement (i.e. derived from the same non terminal entry of the
717 grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
718 this is not true, since each atomic tactic or punctuation is considered
721 \subsubsection{Common issues of tactic(als)-based proof languages}
722 We will examine the two main problems of tactic(als)-based proof script:
723 maintainability and readability.
725 Huge libraries of formal mathematics have been developed, and backward
726 compatibility is a really time consuming task. \\
727 A real-life example in the history of \MATITA{} was the reordering of
728 goals opened by a tactic application. We noticed that some tactics
729 were not opening goals in the expected order. In particular the
730 \texttt{elim} tactic on a term of an inductive type with constructors
731 $c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
732 \ldots, g_2$. The library of \MATITA{} was still in an embryonic state
733 but some theorems about integers were there. The inductive type of
734 $\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
735 induction proofs on this type where written without tacticals and,
736 obviously, considering the three induction cases in the wrong order.
737 Fixing the behavior of the tactic broke the library and two days of
738 work were needed to make it compile again. The whole time was spent in
739 finding the list of tactics used to prove the third induction case and
740 swap it with the list of tactics used to prove the second case. If
741 the proofs was structured with the branch tactical this task could
742 have been done automatically.
744 From this experience we learned that the use of tacticals for
745 structuring proofs gives some help but may have some drawbacks in
746 proof script readability. We must highlight that proof scripts
747 readability is poor by itself, but in conjunction with tacticals it
748 can be nearly impossible. The main cause is the fact that in proof
749 scripts there is no trace of what you are working on. It is not rare
750 for two different theorems to have the same proof script (while the
751 proof is completely different).\\
752 Bad readability is not a big deal for the user while he is
753 constructing the proof, but is considerably a problem when he tries to
754 reread what he did or when he shows his work to someone else. The
755 workaround commonly used to read a script is to execute it again
756 step-by-step, so that you can see the proof goal changing and you can
757 follow the proof steps. This works fine until you reach a tactical. A
758 compound statement, made by some basic tactics glued with tacticals,
759 is executed in a single step, while it obviously performs lot of proof
760 steps. In the fist example of the previous section the whole branch
761 over the two goals (respectively the left and right part of the logic
762 and) result in a single step of execution. The workaround doesn't work
763 anymore unless you de-structure on the fly the proof, putting some
764 ``\texttt{.}'' where you want the system to stop.\\
766 Now we can understand the tradeoff between script readability and
767 proof structuring with tacticals. Using tacticals helps in maintaining
768 scripts, but makes it really hard to read them again, cause of the way
771 \MATITA{} uses a language of tactics and tacticals, but tries to avoid
772 this tradeoff, alluring the user to write structured proof without
773 making it impossible to read them again.
775 \subsubsection{The \MATITA{} approach: Tinycals}
778 \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
781 \begin{array}{@{}rcll@{}}
783 ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
785 ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
786 \NT{block\_delimiter} &
787 ::= & \verb+begin+ ~|~ \verb+end+ & \\
789 ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
795 \MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
796 While one would expect to find structured constructs like
797 $\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
798 This is essential for base idea behind matita tacticals: step-by-step execution.
800 The low-level tacticals implementation of \MATITA{} allows a step-by-step
801 execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
802 not executed as an atomic operation. This has two major benefits for the user,
803 even being a so simple idea:
805 \item[Proof structuring]
806 is much easier. Consider for example a proof by induction, and imagine you
807 are using classical tacticals in one of the state of the
808 art graphical interfaces for proof assistant like Proof General or Coq Ide.
809 After applying the induction principle you have to choose: structure
810 the proof or not. If you decide for the former you have to branch with
811 ``\texttt{[}'' and write tactics for all the cases separated by
812 ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
813 You can replace most of the cases by the identity tactic just to
814 concentrate only on the first goal, but you will have to go one step back and
815 one further every time you add something inside the tactical. Again this is
816 caused by the one step execution of tacticals and by the fact that to modify
817 the already executed script you have to undo one step.
818 And if you are board of doing so, you will finish in giving up structuring
819 the proof and write a plain list of tactics.\\
820 With step-by-step tacticals you can apply the induction principle, and just
821 open the branching tactical ``\texttt{[}''. Then you can interact with the
822 system reaching a proof of the first case, without having to specify any
823 tactic for the other goals. When you have proved all the induction cases, you
824 close the branching tactical with ``\texttt{]}'' and you are done with a
826 While \MATITA{} tacticals help in structuring proofs they allow you to
827 choose the amount of structure you want. There are no constraints imposed by
828 the system, and if the user wants he can even write completely plain proofs.
831 is possible. Going on step by step shows exactly what is going on. Consider
832 again a proof by induction, that starts applying the induction principle and
833 suddenly branches with a ``\texttt{[}''. This clearly separates all the
834 induction cases, but if the square brackets content is executed in one single
835 step you completely loose the possibility of rereading it and you have to
836 temporary remove the branching tactical to execute in a satisfying way the
837 branches. Again, executing step-by-step is the way you would like to review
838 the demonstration. Remember that understanding the proof from the script is
839 not easy, and only the execution of tactics (and the resulting transformed
840 goal) gives you the feeling of what is going on.
845 We would like to thank all the students that during the past
846 five years collaborated in the \HELM{} project and contributed to
847 the development of Matita, and in particular
848 A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
853 \bibliography{matita}