restructuring

[helm.git] / helm / papers / matita / matita2.tex

\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\usepackage{hyperref}
% \usepackage{picins}
\usepackage{color}
\usepackage{fancyvrb}
\usepackage[show]{ed}

\definecolor{gray}{gray}{0.85}
%\newcommand{\logo}[3]{
%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}

\newcommand{\component}{component}
\newcommand{\components}{components}

\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\COQ}{Coq}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\INSTANCE}{\textsc{Instance}}
\newcommand{\IR}{\ensuremath{\dR}}
\newcommand{\IZ}{\ensuremath{\dZ}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
\newcommand{\MATITA}{Matita}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
\newcommand{\OCAML}{OCaml}
\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\UWOBO}{UWOBO}
\newcommand{\GETTER}{Getter}
\newcommand{\WHELP}{Whelp}
\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
\newcommand{\SHIFT}{\ensuremath{\mbox{\textbf{\textbar}}}}
\newcommand{\POS}[1]{\ensuremath{#1\mbox{\textbf{:}}}}
\newcommand{\MERGE}{\ensuremath{\mbox{\textbf{]}}}}
\newcommand{\FOCUS}[1]{\ensuremath{\mathtt{focus}~#1}}
\newcommand{\UNFOCUS}{\ensuremath{\mathtt{unfocus}}}
\newcommand{\SKIP}{\MATHTT{skip}}
\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}

\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}

%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
 \begin{SaveVerbatim}{boxtmp}}%
 {\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
  \begin{center}
   \fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
  \end{center}}

\newcounter{example}
\newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
 {}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}

\newcounter{pass}
\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}

\newsavebox{\tmpxyz}
\newcommand{\sequent}[2]{
  \savebox{\tmpxyz}[0.9\linewidth]{
    \begin{minipage}{0.9\linewidth}
      \ensuremath{#1} \\
      \rule{3cm}{0.03cm}\\
      \ensuremath{#2}
    \end{minipage}}\setlength{\fboxsep}{3mm}%
  \begin{center}
   \fcolorbox{black}{gray}{\usebox{\tmpxyz}}
  \end{center}}

\bibliographystyle{plain}

\begin{document}

\begin{opening}

 \title{The \MATITA{} Proof Assistant}

\author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
\author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
\author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
\author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
\institute{Department of Computer Science, University of Bologna\\
 Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}

\runningtitle{The Matita proof assistant}
\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}

% \date{data}

\begin{motto}
``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
\end{motto}

\begin{abstract}
 abstract qui
\end{abstract}

\keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
Digital Libraries}

\end{opening}


\section{Introduction}
\label{sec:intro}
\MATITA{} is the Proof Assistant under development by the \HELM{} team
\cite{mkm-helm} at the University of Bologna, under the direction of 
Prof.~Asperti. \\
The paper describes the overall architecture of
the system, focusing on its most distintive and innovative 
features.

\subsection{Historical Perspective}
The origins of \MATITA{} go back to 1999. At the time we were mostly 
interested to develop tools and techniques to enhance the accessibility
via Web of formal libraries of mathematics. Due to its dimension, the
library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems) 
was choosed as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably 
with \NUPRL{}\cite{nuprl-book}.
The work, mostly performed in the framework of the recently concluded 
European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the 
following steps:
\begin{itemize}
\item exporting the information from the internal representation of
 \COQ{} to a system and platform independent format. Since XML was at the 
time an emerging standard, we naturally adopted this technology, fostering
a content-centric architecture\cite{content-centric} where the documents
of the library were the the main components around which everything else 
has to be build;
\item developing indexing and searching techniques supporting semantic
 queries to the library; 
%these efforts gave birth to our \WHELP{}
%search engine, described in~\cite{whelp};
\item developing languages and tools for a high-quality notational 
rendering of mathematical information\footnote{We have been 
active in the MathML Working group since 1999.}; 
%and developed inside
%\HELM{} a MathML-compliant widget for the GTK graphical environment
%which can be integrated in any application.
\end{itemize}

According to our content-centric commitment, the library exported from
Coq was conceived as being distributed and most of the tools were developed
as Web services. The user could interact with the library and the tools by
means of a Web interface that orchestrates the Web services.

The Web services and the other tools have been implemented as front-ends
to a set of software libraries, collectively called the \HELM{} libraries.
At the end of the \MOWGLI{} project we already disposed of the following
tools and software libraries:
\begin{itemize}
\item XML specifications for the Calculus of Inductive Constructions,
with libraries for parsing and saving mathematical objects in such a format
\cite{exportation-module};
\item metadata specifications with libraries for indexing and querying the
XML knowledge base;
\item a proof checker library (i.e. the {\em kernel} of a proof assistant), 
implemented to check that we exported form the \COQ{} library all the 
logically relevant content;
\item a sophisticated parser (used by the search engine), able to deal 
with potentially ambiguous and incomplete information, typical of the 
mathematical notation \cite{disambiguation};
\item a {\em refiner} library, i.e. a type inference system, based on
partially specified terms, used by the disambiguating parser;
\item complex transformation algorithms for proof rendering in natural
language \cite{remathematization};
\item an innovative, MathML-compliant rendering widget for the GTK 
graphical environment\cite{padovani}, supporting 
high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
meaningful rendering expressions, and to past the respective content into
a different text area.
\end{itemize}
Starting from all this, developing our own proof assistant was not
too far away: essentially, we ``just'' had to
add an authoring interface, and a set of functionalities for the
overall management of the library, integrating everything into a
single system. \MATITA{} is the result of this effort. 

\subsection{The System}
DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''

\begin{itemize}
 \item scelta del sistema fondazionale
 \item sistema indipendente (da Coq)
 \item compatibilit\`a con sistemi legacy
\end{itemize}

\subsection{Relationship with \COQ{}}

At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
more the effect of the circumstances of its creation described 
above than the result of a deliberate design. In particular, we
(essentially) share the same foundational dialect of \COQ{} (the
Calculus of (Co)Inductive Constructions), the same implementative
language (\OCAML{}), and the same (script based) authoring philosophy.
However, the analogy essentially stops here and no code is shared by the
two systems.

In a sense; we like to think of \MATITA{} as the way \COQ{} would 
look like if entirely rewritten from scratch: just to give an
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
by \COQ{} (and we are convinced that, starting from scratch again,
we could furtherly reduce our code in sensible way).

Moreover, the complexity of the code of \MATITA{} is greatly reduced with
respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
989 functions, to be compared with the 4'286 functions of \COQ.

Finally, \MATITA{} has several innovatives features over \COQ{} that derive
from the integration of Mathematical Knowledge Management tools with proof
assistants. Among them, the advanced indexing tools over the library and
the parser for ambiguous mathematical notation.

The size and complexity improvements over \COQ{} must be understood
historically. \COQ{} is a quite old
system whose development started 15\NOTE{Verificare} years ago. Since then
several developers have took over the code and several new research ideas
that were not considered in the original architecture have been experimented
and integrated in the system. Moreover, there exists a lot of developments
for \COQ{} that require backward compatibility between each pair of releases;
since many central functionalities of a proof assistant are based on heuristics
or arbitrary choices to overcome undecidability (e.g. for higher order
unification), changing these functionalities mantaining backward compatibility
is very difficult. Finally, the code of \COQ{} has been greatly optimized
over the years; optimization reduces maintenability and rises the complexity
of the code.

In writing \MATITA{} we have not been hindered by backward compatibility and
we have took advantage of the research results and experiences previously
developed by others, comprising the authors of \COQ. Moreover, starting from
scratch, we have designed in advance the architecture and we have splitted
the code in coherent minimally coupled libraries.

In the future we plan to exploit \MATITA{} as a test bench for new ideas and
extensions. Keeping the single libraries and the whole architecture as
simple as possible is thus crucial to foster future experiments and to
allow other developers to quickly understand our code and contribute.

%For direct experience of the authors, the learning curve to understand and
%be able to contribute to \COQ{}'s code is quite steep and requires direct
%and frequent interactions with \COQ{} developers.

\begin{figure}[t]
 \begin{center}
  \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
  \caption{\MATITA{} libraries}
  \label{fig:libraries}
 \end{center}
\end{figure}

\section{Architecture}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
project.

Applications and \components{} depend over other \components{} forming a
directed acyclic graph (DAG). Each \component{} can be decomposed in
a a set of \emph{modules} also forming a DAG.

Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
depend on a restricted set of \components{}.

Only the proof assistant \MATITA{} and the \WHELP{} search engine are
applications meant to be used directly by the user. All the other applications
are Web services developed in the HELM and MoWGLI projects and already described
elsewhere. In particular:
\begin{itemize}
 \item The \emph{Getter} is a Web service to retrieve an (XML) document
   from a physical location (URL) given its logical name (URI). The Getter is
   responsible of updating a table that maps URIs to URLs. Thanks to the Getter
   it is possible to work on a logically monolithic library that is physically
   distributed on the network. More information on the Getter can be found
   in~\cite{zack-master}.
 \item \emph{Whelp} is a search engine to index and locate mathematical
   notions (axioms, theorems, definitions) in the logical library managed
   by the Getter. Typical examples of a query to Whelp are queries that search
   for a theorem that generalize or instantiate a given formula, or that
   can be immediately applied to prove a given goal. The output of Whelp is
   an XML document that lists the URIs of a complete set of candidates that
   are likely to satisfy the given query. The set is complete in the sense
   that no notion that actually satisfies the query is thrown away. However,
   the query is only approssimated in the sense that false matches can be
   returned. Whelp has been described in~\cite{whelp}.
 \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
   notion in the distributed library, renders it according to the user provided
   two dimensional mathematical notation. Uwobo may also embed the rendering
   of mathematical notions into arbitrary documents before returning them.
   The Getter is used by Uwobo to retrieve the document to be rendered.
   Uwobo has been described in~\cite{zack-master}.
 \item The \emph{Proof Checker} is a Web service that, given the URI of
   notion in the distributed library, checks its correctness. Since the notion
   is likely to depend in an acyclic way over other notions, the proof checker
   is also responsible of building in a top-down way the DAG of all
   dependencies, checking in turn every notion for correctness.
   The proof checker has been described in~\cite{zack-master}.
 \item The \emph{Dependency Analyzer} is a Web service that can produce
   a textual or graphical representation of the dependecies of an object.
   The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}

The dependency of a \component{} or application over another \component{} can
be satisfied by linking the \component{} in the same executable.
For those \components{} whose functionalities are also provided by the
aforementioned Web services, it is also possible to link stub code that
forwards the request to a remote Web service. For instance, the Getter
is just a wrapper to the \texttt{getter} \component{} that allows the
\component{} to be used as a Web service. \MATITA{} can directly link the code
of the \texttt{getter} \component, or it can use a stub library with the same
API that forwards every request to the Getter.

To better understand the architecture of \MATITA{} and the role of each
\component, we can focus on the representation of the mathematical information.
\MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
Constructions (CIC). In CIC terms are used to represent mathematical
expressions, types and proofs. \MATITA{} is able to handle terms at
four different levels of specification. On each level it is possible to provide
a different set of functionalities. The four different levels are:
fully specified terms; partially specified terms; 
content level terms; presentation level terms.

\subsection{Fully specified terms}
 \emph{Fully specified terms} are CIC terms where no information is
   missing or left implicit. A fully specified term should be well-typed.
   The mathematical notions (axioms, definitions, theorems) that are stored
   in our mathematical library are fully specified and well-typed terms.
   Fully specified terms are extremely verbose (to make type-checking
   decidable). Their syntax is fixed and does not resemble the usual
   extendible mathematical notation. They are not meant for direct user
   consumption.

   The \texttt{cic} \component{} defines the data type that represents CIC terms
   and provides a parser for terms stored in an XML format.

   The most important \component{} that deals with fully specified terms is
   \texttt{cic\_proof\_checking}. It implements the procedure that verifies
   if a fully specified term is well-typed. It also implements the
   \emph{conversion} judgement that verifies if two given terms are
   computationally equivalent (i.e. they share the same normal form).

   Terms may reference other mathematical notions in the library.
   One commitment of our project is that the library should be physically
   distributed. The \texttt{getter} \component{} manages the distribution,
   providing a mapping from logical names (URIs) to the physical location
   of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
   data type and several utility functions over URIs. The
   \texttt{cic\_proof\_checking} \component{} calls the \texttt{getter}
   \component{} every time it needs to retrieve the definition of a mathematical
   notion referenced by a term that is being type-checked. 

   The Proof Checker is the Web service that provides an interface
   to the \texttt{cic\_proof\_checking} \component.

   We use metadata and a sort of crawler to index the mathematical notions
   in the distributed library. We are interested in retrieving a notion
   by matching, instantiation or generalization of a user or system provided
   mathematical expression. Thus we need to collect metadata over the fully
   specified terms and to store the metadata in some kind of (relational)
   database for later usage. The \texttt{hmysql} \component{} provides
   a simplified
   interface to a (possibly remote) MySql database system used to store the
   metadata. The \texttt{metadata} \component{} defines the data type of the
   metadata
   we are collecting and the functions that extracts the metadata from the
   mathematical notions (the main functionality of the crawler).
   The \texttt{whelp} \component{} implements a search engine that performs
   approximated queries by matching/instantiation/generalization. The queries
   operate only on the metadata and do not involve any actual matching
   (that will be described later on and that is implemented in the
    \texttt{cic\_unification} \component). Not performing any actual matching
   the query only returns a complete and hopefully small set of matching
   candidates. The process that has issued the query is responsible of
   actually retrieving from the distributed library the candidates to prune
   out false matches if interested in doing so.

   The Whelp search engine is the Web service that provides an interface to
   the \texttt{whelp} \component.

   According to our vision, the library is developed collaboratively so that
   changing or removing a notion can invalidate other notions in the library.
   Moreover, changing or removing a notion requires a corresponding change
   in the metadata database. The \texttt{library} \component{} is responsible
   of preserving the coherence of the library and the database. For instance,
   when a notion is removed, all the notions that depend on it and their
   metadata are removed from the library. This aspect will be better detailed
   in Sect.~\ref{decompilazione}.
   
\subsection{Partially specified terms}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
Omitted subterms can bear no information at all or they may be associated to
a sequent. The formers are called \emph{implicit terms} and they occur only
linearly. The latters may occur multiple times and are called
\emph{metavariables}. An \emph{explicit substitution} is applied to each
occurrence of a metavariable. A metavariable stand for a term whose type is
given by the conclusion of the sequent. The term must be closed in the
context that is given by the ordered list of hypotheses of the sequent.
The explicit substitution instantiates every hypothesis with an actual
value for the term bound by the hypothesis.

Partially specified terms are not required to be well-typed. However a
partially specified term should be \emph{refinable}. A \emph{refiner} is
a type-inference procedure that can instantiate implicit terms and
metavariables and that can introduce \emph{implicit coercions} to make a
partially specified term be well-typed. The refiner of \MATITA{} is implemented
in the \texttt{cic\_unification} \component. As the type checker is based on
the conversion check, the refiner is based on \emph{unification} that is
a procedure that makes two partially specified term convertible by instantiating
as few as possible metavariables that occur in them.

Since terms are used in CIC to represent proofs, correct incomplete
proofs are represented by refinable partially specified terms. The metavariables
that occur in the proof correspond to the conjectures still to be proved.
The sequent associated to the metavariable is the conjecture the user needs to
prove.

\emph{Tactics} are the procedures that the user can apply to progress in the
proof. A tactic proves a conjecture possibly creating new (and hopefully
simpler) conjectures. The implementation of tactics is given in the
\texttt{tactics} \component. It is heavily based on the refinement and
unification procedures of the \texttt{cic\_unification} \component.

The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
commands of the \MATITA{} proof assistant. Most of the commands are tactics.
Other commands are used to give definitions and axioms or to state theorems
and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
It implements the semantics of each command in the grafite AST as a function
from status to status.  It implements also an undo function to go back to
previous statuses. \TODO{parlare di disambiguazione lazy \& co?}

As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
possible to adopt the usual mathematical notation. However they are already
an improvement over fully specified terms since they allow to omit redundant
information that can be inferred by the refiner.

\subsection{Content level terms}
\label{sec:contentintro}

The language used to communicate proofs and expecially expressions with the
user does not only needs to be extendible and accomodate the usual mathematical
notation. It must also reflect the comfortable degree of imprecision and
ambiguity that the mathematical language provides.

For instance, it is common practice in mathematics to speak of a generic
equality that can be used to compare any two terms. However, it is well known
that several equalities can be distinguished as soon as we care for decidability
or for their computational properties. For instance equality over real
numbers is well known to be undecidable, whereas it is decidable over
rational numbers.

Similarly, we usually speak of natural numbers and their operations and
properties without caring about their representation. However the computational
properties of addition over the binary representation are very different from
those of addition over the unary representation. And addition over two natural
numbers is definitely different from addition over two real numbers.

Formal mathematics cannot hide these differences and obliges the user to be
very precise on the types he is using and their representation. However,
to communicate formulae with the user and with external tools, it seems good
practice to stick to the usual imprecise mathematical ontology. In the
Mathematical Knowledge Management community this imprecise language is called
the \emph{content level} representation of expressions.

In \MATITA{} we provide two translations: from partially specified terms
to content level terms and the other way around. The first translation can also
be applied to fully specified terms since a fully specified term is a special
case of partially specified term where no metavariable or implicit term occurs.

The translation from partially specified terms to content level terms must
discriminate between terms used to represent proofs and terms used to represent
expressions. The firsts are translated to a content level representation of
proof steps that can easily be rendered in natural language. The latters
are translated to MathML Content formulae. MathML Content~\cite{mathml} is a W3C
standard
for the representation of content level expressions in an XML extensible format.

The translation to content level is implemented in the
\texttt{acic\_content} \component. Its input are \emph{annotated partially
specified terms}, that are maximally unshared
partially specified terms enriched with additional typing information for each
subterm. This information is used to discriminate between terms that represent
proofs and terms that represent expressions. Part of it is also stored at the
content level since it is required to generate the natural language rendering
of proofs. The terms need to be maximally unshared (i.e. they must be a tree
and not a DAG). The reason is that to the occurrences of a subterm in
two different positions we need to associate different typing informations.
This association is made easier when the term is represented as a tree since
it is possible to label each node with an unique identifier and associate
the typing information using a map on the identifiers.
The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
by the \texttt{library} \component{} since fully specified terms are stored
in the library in their annotated form.

We do not provide yet a reverse translation from content level proofs to
partially specified terms. But in \texttt{cic\_disambiguation} we do provide
the reverse translation for expressions. The mapping from
content level expressions to partially specified terms is not unique due to
the ambiguity of the content level. As a consequence the translation
is guided by an \emph{interpretation}, that is a function that chooses for
every ambiguous expression one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
disambiguation algorithm we presented in~\cite{disambiguation} that is
responsible of building in an efficicent way the set of all ``correct''
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.

\subsection{Presentation level terms}

Content level terms are a sort of abstract syntax trees for mathematical
expressions and proofs. The concrete syntax given to these abstract trees
is called \emph{presentation level}.

The main important difference between the content level language and the
presentation level language is that only the former is extendible. Indeed,
the presentation level language is a finite language that comprises all
the usual mathematical symbols. Mathematicians invent new notions every
single day, but they stick to a set of symbols that is more or less fixed.

The fact that the presentation language is finite allows the definition of
standard languages. In particular, for formulae we have adopt MathML
Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
visually
represent proofs it is enough to embed formulae in plain text enriched with
formatting boxes. Since the language of formatting boxes is very simple,
many equivalent specifications exist and we have adopted our own, called
BoxML.

The \texttt{content\_pres} \component{} contains the implementation of the
translation from content level terms to presentation level terms. The
rendering of presentation level terms is left to the application that uses
the \component. However, in the \texttt{hgdome} \component{} we provide a few
utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
presentation
level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
widget developed by Luca Padovani \cite{padovani}. The widget is
particularly interesting since it allows to implement \emph{semantic
selection}.

Semantic selection is a technique that consists in enriching the presentation
level terms with pointers to the content level terms and to the partially
specified terms they correspond to. Highlight of formulae in the widget is
constrained to selection of meaningful expressions, i.e. expressions that
correspond to a lower level term, that is a content term or a partially or
fully specified term.
Once the rendering of a lower level term is
selected it is possible for the application to retrieve the pointer to the
lower level term. An example of applications of semantic selection is
\emph{semantic cut\&paste}: the user can select an expression and paste it
elsewhere preserving its semantics (i.e. the partially specified term),
possibly performing some semantic transformation over it (e.g. renaming
variables that would be captured or lambda-lifting free variables).

The reverse translation from presentation level terms to content level terms
is implemented by a parser that is also found in \texttt{content\_pres}.
Differently from the translation from content level terms to partially
refined terms, this translation is not ambiguous. The reason is that the
parsing tool we have adopted (CamlP4) is not able to parse ambiguous
grammars. Thus we require the mapping from presentation level terms
(concrete syntax) to content level terms (abstract syntax) to be unique.
This means that the user must fix once and for all the associativity and
precedence level of every operator he is using. In practice this limitation
does not seem too strong. The reason is that the target of the
translation is an ambiguous language and the user is free to associate
to every content level term several different interpretations (as a
partially specified term).

Both the direct and reverse translation from presentation to content level
terms are parameterized over the user provided mathematical notation. 
The \texttt{lexicon} \component{} is responsible of managing the lexicon,
that is the set of active notations. It defines an abstract syntax tree
of commands to declare and activate new notations and it implements the
semantics of these commands. It also implements undoing of the semantic
actions. Among the commands there are hints to the
disambiguation algorithm that are used to control and speed up disambiguation.
These mechanisms will be further discussed in Sect.~\ref{disambiguazione}.

Finally, the \texttt{grafite\_parser} \component{} implements a parser for
the concrete syntax of the commands of \MATITA. The parser process a stream
of characters and returns a stream of abstract syntax trees (the ones
defined by the \texttt{grafite} component and whose semantics is given
by \texttt{grafite\_engine}). When the parser meets a command that changes
the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
process the command. When the parser needs to parse a term at the presentation
level, it invokes the already described parser for terms contained in
\texttt{content\_pres}.

The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
against the \texttt{grafite\_parser} \components{}
since they provide an interface to the user. In both cases the formulae
written by the user are parsed using the \texttt{content\_pres} \component{} and
then disambiguated using the \texttt{cic\_disambiguation} \component.
However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
\texttt{tactics} components since \WHELP{} can only execute those ASTs that
correspond to queries (implemented in the \texttt{whelp} component).

The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
providing a rendering service for the documents in the distributed library.
To render a document given its URI, \UWOBO{} retrieves it using the
\GETTER{} obtaining a document with fully specified terms. Then it translates
it to the presentation level passing through the content level. Finally
it returns the result document to be rendered by the user's
browser.\footnote{\TODO{manca la passata verso HTML}}


The \components{} not yet described (\texttt{extlib}, \texttt{xml},
\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are 
minor \components{} that provide a core of useful functions and basic
services missing from the standard library of the programming language.
In particular, the \texttt{xml} \component{} is used
to easily represent, parse and pretty-print XML files.

\section{Using \MATITA (boh \ldots cambiare titolo)}

\begin{figure}[t]
 \begin{center}
%   \includegraphics[width=0.9\textwidth]{a.eps}
  \caption{\MATITA{} screenshot}
  \label{fig:screenshot}
 \end{center}
\end{figure}

\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
split in two main windows: on the left a textual widget is used to edit the
script, on the right the list of open goal is shown using a MathML rendering
widget. A distinguished part of the script (shaded in the screenshot) represent
the commands already executed and can't be edited without undoing them. The
remaining part can be freely edited and commands from that part can be executed
moving down the execution point. An additional window --- the ``cicBrowser'' ---
can be used to browse the library, including the proof being developed, and
enable content based search on it. In the cicBrowser proofs are rendered in
natural language, automatically generated from the low-level $\lambda$-terms
using techniques inspired by \cite{natural,YANNTHESIS}.

In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
only seen as a convenient way to create mathematical objects. The universe of
all these objects makes up the \HELM{} library, which is always completely
visible to the user. The mathematical library is thus conceived as a global 
hypertext, where objects may freely reference each other. It is a duty of
the system to guide the user through the relevant parts of the library. 

This methodological assumption has many important consequences
which will be discussed in the next section.

%on one side
%it requires functionalities for the overall management of the library, 
%%%%%comprising efficient indexing techniques to retrieve and filter the 
%information; 
%on the other it introduces overloading in the use of 
%identifiers and mathematical notation, requiring sophisticated disambiguation
%techniques for interpreting the user inputs.  
%In the next two sections we shall separately discuss the two previous 
%points. 

%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
%organized in components which work on data in this format. For instance the
%rendering engine, which transform $\lambda$-terms encoded as XML document to
%MathML Presentation documents, can be used apart from \MATITA{} to print  ...
%FINIRE

A final section is devoted to some innovative aspects
of the authoring system, such as a step by step tactical execution, 
content selection and copy-paste. 

\section{Library Management}

\subsection{Indexing and searching}

\subsection{Developments}

\subsection{Automation}

\subsection{Matita's naming convention}
A minor but not entirely negligible aspect of Matita is that of
adopting a (semi)-rigid naming convention for identifiers, derived by 
our studies about metadata for statements. 
The convention is only applied to identifiers for theorems 
(not definitions), and relates the name of a proof to its statement.
The basic rules are the following:
\begin{itemize}
\item each identifier is composed by an ordered list of (short)
names occurring in a left to right traversal of the statement; 
\item all identifiers should (but this is not strictly compulsory) 
separated by an underscore,
\item identifiers in two different hypothesis, or in an hypothesis
and in the conlcusion must be separated by the string ``\verb+_to_+'';
\item the identifier may be followed by a numerical suffix, or a
single or duoble apostrophe.

\end{itemize}
Take for instance the theorem
\[\forall n:nat. n = plus \; n\; O\]
Possible legal names are: \verb+plus_n_O+, \verb+plus_O+, 
\verb+eq_n_plus_n_O+ and so on. 
Similarly, consider the theorem 
\[\forall n,m:nat. n<m \to n \leq m\]
In this case \verb+lt_to_le+ is a legal name, 
while \verb+lt_le+ is not.\\
But what about, say, the symmetric law of equality? Probably you would like 
to name such a theorem with something explicitly recalling symmetry.
The correct approach, 
in this case, is the following. You should start with defining the 
symmetric property for relations

\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]

Then, you may state the symmetry of equality as
\[ \forall A:Type. symmetric \;A\;(eq \; A)\]
and \verb+symmetric_eq+ is valid Matita name for such a theorem. 
So, somehow unexpectedly, the introduction of semi-rigid naming convention
has an important benefical effect on the global organization of the library, 
forcing the user to define abstract notions and properties before 
using them (and formalizing such use).

Two cases have a special treatment. The first one concerns theorems whose
conclusion is a (universally quantified) predicate variable, i.e. 
theorems of the shape
$\forall P,\dots.P(t)$.
In this case you may replace the conclusion with the word
``elim'' or ``case''.
For instance the name \verb+nat_elim2+ is a legal name for the double
induction principle.

The other special case is that of statements whose conclusion is a
match expression. 
A typical example is the following
\begin{verbatim}
  \forall n,m:nat. 
      match (eqb n m) with
        [ true  \Rightarrow n = m 
        | false \Rightarrow n \neq m]
\end{verbatim}
where $eqb$ is boolean equality.
In this cases, the name can be build starting from the matched
expression and the suffix \verb+_to_Prop+. In the above example, 
\verb+eqb_to_Prop+ is accepted. 

\section{The \MATITA{} user interface}



\subsection{Disambiguation}

Software applications that involve input of mathematical content should strive
to require the user as less drift from informal mathematics as possible. We
believe this to be a fundamental aspect of such applications user interfaces.
Being that drift in general very large when inputing
proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
mathematical formulae which can be input using a \TeX-like encoding (the
concrete syntax corresponding to presentation level terms) and are then
translated (in multiple steps) to partially specified terms as sketched in
Sect.~\ref{sec:contentintro}.

The key component of the translation is the generic disambiguation algorithm
implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
and presented in~\cite{disambiguation}. In this section we present how to use
such an algorithm in the context of the development of a library of formalized
mathematics. We will see that using multiple passes of the algorithm, varying
some of its parameters, helps in keeping the input terse without sacrificing
expressiveness.

\subsubsection{Disambiguation aliases}

Let's start with the definition of the ``strictly greater then'' notion over
(Peano) natural numbers.

\begin{grafite}
include "nat/nat.ma".
..
definition gt: nat \to nat \to Prop \def
  \lambda n, m. m < n.
\end{grafite}

The \texttt{include} statement adds the requirement that the part of the library
defining the notion of natural numbers should be defined before
processing the following definition. Note indeed that the algorithm presented
in~\cite{disambiguation} does not describe where interpretations for ambiguous
expressions come from, since it is application-specific. As a first
approximation, we will assume that in \MATITA{} they come from the library (i.e.
all interpretations available in the library are used) and the \texttt{include}
statements are used to ensure the availability of required library slices (see
Sect.~\ref{sec:libmanagement}).

While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
terms: its type and its body. Being available in the required library only one
interpretation both for the unbound identifier \texttt{nat} and for the
\OP{<} operator, and being the resulting partially specified term refinable,
both type and body are easily disambiguated.

Now suppose we have defined integers as signed natural numbers, and that we want
to prove a theorem about an order relationship already defined on them (which of
course overload the \OP{<} operator):

\begin{grafite}
include "Z/z.ma".
..
theorem Zlt_compat:
  \forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}

Since integers are defined on top of natural numbers, the part of the library
concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
type. Thus, according to the disambiguation algorithm, two different partially
specified terms could be associated to it. At first, this might not be seen as a
problem, since the user is asked and can choose interactively which of the two
she had in mind. However in the long run it has the drawbacks of inhibiting
batch compilation of the library (a technique used in \MATITA{} for behind the
scene compilation when needed, e.g. when an \texttt{include} is issued) and
yields to poor user interaction (imagine how tedious would be to be asked for a
choice each time you re-evaluate \texttt{Zlt\_compat}!).

For this reason we added to \MATITA{} the concept of \emph{disambiguation
aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
expressions to partially specified terms, which are part of the runtime status
of \MATITA. They can be provided by users with the \texttt{alias} statement, but
are usually automatically added when evaluating \texttt{include} statements
(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
which require interactive choice are saved in batch compilable format. Thus,
after evaluating the above theorem the script will be changed to the following
snippet (assuming that the interpretation of \OP{<} over integers has been
choosed):

\begin{grafite}
alias symbol "lt" = "integer 'less than'".
theorem Zlt_compat:
  \forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}

But how are disambiguation aliases used? Since they come from the parts of the
library explicitely included we may be tempted of using them as the only
available interpretations. This would speed up the disambiguation, but may fail.
Consider for example:

\begin{grafite}
theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
\end{grafite}

and suppose that the \OP{+} operator is defined only on natural numbers. If
the alias for \OP{<} points to the integer version of the operator, no
refinable partially specified term matching the term could be found.

For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
first pass attempt to disambiguate using the last available disambiguation
aliases (\emph{mono aliases} pass), in case of failure the next pass try again
the disambiguation forgetting the aliases and using the whole library to
retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
Since the latter pass may lead to too many choices we intertwined an additional
pass among the two which use as interpretations all the aliases coming for
included parts of the library (\emph{multi aliases} phase). This is the reason
why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
turned out to be a well-balanced trade-off among performances (earlier passes
fail quickly) and degree of ambiguity supported for presentation level terms.

\subsubsection{Operator instances}

Let's suppose now we want to define a theorem relating ordering relations on
natural and integer numbers. The way we would like to write such a theorem (as
we can read it in the \MATITA{} standard library) is:

\begin{grafite}
include "Z/z.ma".
include "nat/orders.ma".
..
theorem lt_to_Zlt_pos_pos:
  \forall n, m: nat. n < m \to pos n < pos m. 
\end{grafite}

Unfortunately, none of the passes described above is able to disambiguate its
type, no matter how aliases are defined. This is because the \OP{<} operator
occurs twice in the content level term (it has two \emph{instances}) and two
different interpretation for it have to be used in order to obtain a refinable
partially specified term. To address this issue, we have the ability to consider
each instance of a single symbol as a different ambiguous expression in the
content level term, and thus we can assign a different interpretation to each of
them. A disambiguation pass which exploit this feature is said to be using
\emph{fresh instances}.

Fresh instances lead to a non negligible performance loss (since the choice of
an interpretation for one instances does not constraint the choice for the
others). For this reason we always attempt a fresh instances pass only after
attempting a non-fresh one.

\subsubsection{Implicit coercions}

Let's now consider a (rather hypothetical) theorem about derivation:

\begin{grafite}
theorem power_deriv:
  \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
\end{grafite}

and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
Mathematichians would write the term that way since it is well known that the
natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
number for the purpose of real multiplication. The refiner of \MATITA{} supports
\emph{implicit coercions} for this reason: given as input the above content
level term, it will return a partially specified term where in place of
\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
(assuming it has been defined as such of course).

Nonetheless coercions are not always desirable. For example, in disambiguating
\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
among the possible partially specified term choices. For this reason in
\MATITA{} we always try first a disambiguation pass which require the refiner
not to use the coercions and only in case of failure we attempt a
coercion-enabled pass.

It is interesting to observe also the relationship among operator instances and
implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
which \MATITA{} disambiguated using fresh instances. In case there exists a
coercion from natural numbers to (positive) integers (which indeed does, it is
the \texttt{pos} constructor itself), the theorem can be disambiguated using
twice that coercion on the left hand side of the implication. The obtained
partially specified term however would not probably be the expected one, being a
theorem which prove a trivial implication. For this reason we choose to always
prefer fresh instances over implicit coercion, i.e. we always attempt
disambiguation passes with fresh instances before attempting passes with
implicit coercions.

\subsubsection{Disambiguation passes}

\TODO{spiegazione della tabella}

\begin{center}
 \begin{tabular}{c|c|c|c}
  \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
  & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
  & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
  & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
  \hline
  \PASS & Normal & Mono & Disabled \\
  \PASS & Normal & Multi & Disabled \\
  \PASS & Fresh & Mono & Disabled \\
  \PASS & Fresh & Multi & Disabled \\
  \PASS & Fresh & Mono & Enabled \\
  \PASS & Fresh & Multi & Enabled \\
  \PASS & Fresh & Library & Enabled
 \end{tabular}
\end{center}

\TODO{alias one shot}







\subsection{Patterns}

serve una intro che almeno cita il widget (per i patterns) e che fa
il resoconto delle cose che abbiamo e che non descriviamo,
sottolineando che abbiamo qualcosa da dire sui pattern e sui
tattichini.\\

Patterns are the textual counterpart of the MathML widget graphical
selection.

Matita benefits of a graphical interface and a powerful MathML rendering
widget that allows the user to select pieces of the sequent he is working
on. While this is an extremely intuitive way for the user to
restrict the application of tactics, for example, to some subterms of the
conclusion or some hypothesis, the way this action is recorded to the text
script is not obvious.\\
In \MATITA{} this issue is addressed by patterns.

\subsubsection{Pattern syntax}
A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
$\NT{wanted}$.
The former mocks-up a sequent, discharging unwanted subterms with $?$ and
selecting the interesting parts with the placeholder $\%$. 
The latter is a term that lives in the context of the placeholders.

The concrete syntax is reported in table \ref{tab:pathsyn}
\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
\begin{table}
 \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
\hrule
\[
\begin{array}{@{}rcll@{}}
  \NT{pattern} & 
    ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
  \NT{sequent\_path} & 
    ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
      [~\verb+\vdash+~\NT{multipath}~] & \\
  \NT{wanted} & ::= & \NT{term} & \\
  \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
\end{array}
\]
\hrule
\end{table}

\subsubsection{How patterns work}
Patterns mimic the user's selection in two steps. The first one
selects roots (subterms) of the sequent, using the
$\NT{sequent\_path}$,  while the second 
one searches the $\NT{wanted}$ term starting from these roots. Both are
optional steps, and by convention the empty pattern selects the whole
conclusion.

\begin{description}
\item[Phase 1]
  concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
  part of the syntax. $\NT{ident}$ is an hypothesis name and
  selects the assumption where the following optional $\NT{multipath}$
  will operate. \verb+\vdash+ can be considered the name for the goal.
  If the whole pattern is omitted, the whole goal will be selected.
  If one or more hypotheses names are given the selection is restricted to 
  these assumptions. If a $\NT{multipath}$ is omitted the whole
  assumption is selected. Remember that the user can be mostly
  unaware of this syntax, since the system is able to write down a 
  $\NT{sequent\_path}$ starting from a visual selection.
  \NOTE{Questo ancora non va in matita}

  A $\NT{multipath}$ is a CiC term in which a special constant $\%$
  is allowed.
  The roots of discharged subterms are marked with $?$, while $\%$
  is used to select roots. The default $\NT{multipath}$, the one that
  selects the whole term, is simply $\%$.
  Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
  that respectively select the first argument of an application or
  the source of an arrow and the head of the application that is
  found in the arrow target.

  The first phase selects not only terms (roots of subterms) but also 
  their context that will be eventually used in the second phase.

\item[Phase 2] 
  plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
  part is specified. From the first phase we have some terms, that we
  will see as subterm roots, and their context. For each of these
  contexts the $\NT{wanted}$ term is disambiguated in it and the
  corresponding root is searched for a subterm $\alpha$-equivalent to
  $\NT{wanted}$. The result of this search is the selection the
  pattern represents.

\end{description}

\noindent
Since the first step is equipotent to the composition of the two
steps, the system uses it to represent each visual selection.
The second step is only meant for the
experienced user that writes patterns by hand, since it really
helps in writing concise patterns as we will see in the
following examples.

\subsubsection{Examples}
To explain how the first step works let's give an example. Consider
you want to prove the uniqueness of the identity element $0$ for natural
sum, and that you can relay on the previously demonstrated left
injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
Typing
\begin{grafite}
theorem valid_name: \forall n,m. m + n = n \to m = O.
  intros (n m H).
\end{grafite}
\noindent
leads you to the following sequent 
\sequent{
n:nat\\
m:nat\\
H: m + n = n}{
m=O
}
\noindent
where you want to change the right part of the equivalence of the $H$
hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
\begin{grafite}
  change in H:(? ? ? %) with (O + n).
\end{grafite}
\noindent
This pattern, that is a simple instance of the $\NT{sequent\_path}$
grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
and discharges the head of the application and the first two arguments with a
$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
but the user can simply select with the mouse the right part of the equivalence
and left to the system the burden of writing down in the script file the
corresponding pattern with $?$ and $\%$ in the right place (that is not
trivial, expecially where implicit arguments are hidden by the notation, like
the type $nat$ in this example).

Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ 
works too and can be done, by the experienced user, writing directly
a simpler pattern that uses the second phase.
\begin{grafite}
  change in match n in H with (O + n).
\end{grafite}
\noindent
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
the second phase searches the wanted $n$ inside it by
$\alpha$-equivalence. The resulting
equivalence will be $m+(O+n)=O+n$ since the second phase found two
occurrences of $n$ in $H$ and the tactic changed both.

Just for completeness the second pattern is equivalent to the
following one, that is less readable but uses only the first phase.
\begin{grafite}
  change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
\noindent

\subsubsection{Tactics supporting patterns}
In \MATITA{} all the tactics that can be restricted to subterm of the working
sequent accept the pattern syntax. In particular these tactics are: simplify,
change, fold, unfold, generalize, replace and rewrite.

\NOTE{attualmente rewrite e fold non supportano phase 2. per
supportarlo bisogna far loro trasformare il pattern phase1+phase2 
in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
con una pattern\_of(select(pattern))}

\subsubsection{Comparison with Coq}
Coq has a two diffrent ways of restricting the application of tactis to
subterms of the sequent, both relaying on the same special syntax to identify
a term occurrence.

The first way is to use this special syntax to specify directly to the
tactic the occurrnces of a wanted term that should be affected, while
the second is to prepare the sequent with another tactic called
pattern and the apply the real tactic. Note that the choice is not
left to the user, since some tactics needs the sequent to be prepared
with pattern and do not accept directly this special syntax.

The base idea is that to identify a subterm of the sequent we can
write it and say that we want, for example, the third and the fifth
occurce of it (counting from left to right). In our previous example,
to change only the left part of the equivalence, the correct command
is
\begin{grafite}
  change n at 2 in H with (O + n)
\end{grafite} 
\noindent
meaning that in the hypothesis $H$ the $n$ we want to change is the
second we encounter proceeding from left toright.

The tactic pattern computes a
$\beta$-expansion of a part of the sequent with respect to some
occurrences of the given term. In the previous example the following
command
\begin{grafite}
  pattern n at 2 in H
\end{grafite}
\noindent
would have resulted in this sequent
\begin{grafite}
  n : nat
  m : nat
  H : (fun n0 : nat => m + n = n0) n
  ============================
   m = 0
\end{grafite}
\noindent
where $H$ is $\beta$-expanded over the second $n$
occurrence. This is a trick to make the unification algorithm ignore
the head of the application (since the unification is essentially
first-order) but normally operate on the arguments. 
This works for some tactics, like rewrite and replace,
but for example not for change and other tactics that do not relay on
unification. 

The idea behind this way of identifying subterms in not really far
from the idea behind patterns, but really fails in extending to
complex notation, since it relays on a mono-dimensional sequent representation.
Real math notation places arguments upside-down (like in indexed sums or
integrations) or even puts them inside a bidimensional matrix.  
In these cases using the mouse to select the wanted term is probably the 
only way to tell the system exactly what you want to do. 

One of the goals of \MATITA{} is to use modern publishing techiques, and
adopting a method for restricting tactics application domain that discourages 
using heavy math notation, would definitively be a bad choice.


\subsection{Tacticals}
There are mainly two kinds of languages used by proof assistants to recorder
proofs: tactic based and declarative. We will not investigate the philosophy
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 tactic-based language approach and how \MATITA{} tries to solve
them.

\subsubsection{Tacticals overview}

Tacticals first appeared in LCF and can be seen as programming
constructs, like looping, branching, error recovery or sequential composition.
The following simple example shows three tacticals in action
\begin{grafite}
theorem trivial: 
  \forall A,B:Prop. 
    A = B \to ((A \to B) \land (B \to A)).
  intros (A B H).
  split; intro; 
    [ rewrite < H. assumption.
    | rewrite > H. assumption.
    ]
qed.
\end{grafite}

The first is ``\texttt{;}'' that combines the tactic \texttt{split}
with \texttt{intro}, applying the latter to each goal opened by the
former. Then we have ``\texttt{[}'' that branches on the goals (here
we have two goals, the two sides of the logic and).
The first goal $B$ (with $A$ in the context)
is proved by the first sequence of tactics
\texttt{rewrite} and \texttt{assumption}. Then we move to the second
goal with the separator ``\texttt{|}''. The last tactical we see here
is ``\texttt{.}'' that is a sequential composition that selects the
first goal opened for the following tactic (instead of applying it to
them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
not considered a tactical, but a sentence terminator (i.e. the
delimiter of commands the proof assistant executes).

Giving serious examples here is rather difficult, since they are hard
to read without the interactive tool. To help the reader in
understanding the following considerations we just give few common
usage examples without a proof context.

\begin{grafite}
  elim z; try assumption; [ ... | ... ].
  elim z; first [ assumption | reflexivity | id ].
\end{grafite}

The first example goes by induction on a term \texttt{z} and applies
the tactic \texttt{assumption} to each opened goal eventually recovering if
\texttt{assumption} fails. Here we are asking the system to close all
trivial cases and then we branch on the remaining with ``\texttt{[}''.
The second example goes again by induction on \texttt{z} and tries to
close each opened goal first with \texttt{assumption}, if it fails it
tries \texttt{reflexivity} and finally \texttt{id}
that is the tactic that leaves the goal untouched without failing. 

Note that in the common implementation of tacticals both lines are
compositions of tacticals and in particular they are a single
statement (i.e. derived from the same non terminal entry of the
grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
this is not true, since each atomic tactic or punctuation is considered 
a single statement.

\subsubsection{Common issues of tactic(als)-based proof languages}
We will examine the two main problems of tactic(als)-based proof script:
maintainability and readability. 

Huge libraries of formal mathematics have been developed, and backward
compatibility is a really time consuming task. \\
A real-life example in the history of \MATITA{} was the reordering of
goals opened by a tactic application. We noticed that some tactics
were not opening goals in the expected order. In particular the
\texttt{elim} tactic on a term of an inductive type with constructors
$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
but some theorems about integers were there. The inductive type of
$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
induction proofs on this type where written without tacticals and,
obviously, considering the three induction cases in the wrong order.
Fixing the behavior of the tactic broke the library and two days of
work were needed to make it compile again. The whole time was spent in
finding the list of tactics used to prove the third induction case and
swap it with the list of tactics used to prove the second case.  If
the proofs was structured with the branch tactical this task could
have been done automatically. 

From this experience we learned that the use of tacticals for
structuring proofs gives some help but may have some drawbacks in
proof script readability. We must highlight that proof scripts
readability is poor by itself, but in conjunction with tacticals it
can be nearly impossible. The main cause is the fact that in proof
scripts there is no trace of what you are working on. It is not rare
for two different theorems to have the same proof script (while the
proof is completely different).\\
Bad readability is not a big deal for the user while he is
constructing the proof, but is considerably a problem when he tries to
reread what he did or when he shows his work to someone else.  The
workaround commonly used to read a script is to execute it again
step-by-step, so that you can see the proof goal changing and you can
follow the proof steps. This works fine until you reach a tactical.  A
compound statement, made by some basic tactics glued with tacticals,
is executed in a single step, while it obviously performs lot of proof
steps.  In the fist example of the previous section the whole branch
over the two goals (respectively the left and right part of the logic
and) result in a single step of execution. The workaround doesn't work
anymore unless you de-structure on the fly the proof, putting some
``\texttt{.}'' where you want the system to stop.\\

Now we can understand the tradeoff between script readability and
proof structuring with tacticals. Using tacticals helps in maintaining
scripts, but makes it really hard to read them again, cause of the way
they are executed.

\MATITA{} uses a language of tactics and tacticals, but tries to avoid
this tradeoff, alluring the user to write structured proof without
making it impossible to read them again.

\subsubsection{The \MATITA{} approach: Tinycals}

\begin{table}
 \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
\hrule
\[
\begin{array}{@{}rcll@{}}
  \NT{punctuation} & 
    ::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
  \NT{block\_kind} & 
    ::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
  \NT{block\_delimiter} & 
    ::= & \verb+begin+ ~|~ \verb+end+ & \\
  \NT{tactical} & 
    ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
\end{array}
\]
\hrule
\end{table}

\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
While one would expect to find structured constructs like 
$\verb+do+~n~\NT{tactic}$ the syntax allows pieces of tacticals to be written.
This is essential for base idea behind matita tacticals: step-by-step execution.

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 executed as an atomic operation. This has two major benefits for the user,
even being a so simple idea:
\begin{description}
\item[Proof structuring] 
  is much easier. Consider for example a proof by induction, and imagine you
  are using classical tacticals in one of the state of the
  art graphical interfaces for proof assistant like Proof General or Coq Ide.
  After applying the induction principle you have to choose: structure
  the proof or not. If you decide for the former you have to branch with
  ``\texttt{[}'' and write tactics for all the cases separated by 
  ``\texttt{|}'' and then close the tactical with ``\texttt{]}''. 
  You can replace most of the cases by the identity tactic just to
  concentrate only on the first goal, but you will have to go one step back and
  one further every time you add something inside the tactical. Again this is
  caused by the one step execution of tacticals and by the fact that to modify
  the already executed script you have to undo one step.
  And if you are board of doing so, you will finish in giving up structuring
  the proof and write a plain list of tactics.\\
  With step-by-step tacticals you can apply the induction principle, and just
  open the branching tactical ``\texttt{[}''. Then you can interact with the
  system reaching a proof of the first case, without having to specify any
  tactic for the other goals. When you have proved all the induction cases, you
  close the branching tactical with ``\texttt{]}'' and you are done with a 
  structured proof. \\
  While \MATITA{} tacticals help in structuring proofs they allow you to 
  choose the amount of structure you want. There are no constraints imposed by
  the system, and if the user wants he can even write completely plain proofs.
  
\item[Rereading]
  is possible. Going on step by step shows exactly what is going on.  Consider
  again a proof by induction, that starts applying the induction principle and
  suddenly branches with a ``\texttt{[}''. This clearly separates all the
  induction cases, but if the square brackets content is executed in one single
  step you completely loose the possibility of rereading it and you have to
  temporary remove the branching tactical to execute in a satisfying way the
  branches.  Again, executing step-by-step is the way you would like to review
  the demonstration. Remember that understanding the proof from the script is
  not easy, and only the execution of tactics (and the resulting transformed
  goal) gives you the feeling of what is going on.
\end{description}

\section{The Matita library}

Matita is Coq compatible, in the sense that every theorem of Coq
can be read, checked and referenced in further developments. 
However, in order to test the actual usability of the system, a
new library of results has been started from scratch. In this case, 
of course, we wrote (and offer) the source script files, 
while, in the case of Coq, Matita may only rely on XML files of
Coq objects. 
The current library just comprises about one thousand theorems in 
elementary aspects of arithmetics up to the multiplicative property for 
Eulers' totient function $\phi$.
The library is organized in five main directories: $logic$ (connectives,
quantifiers, equality, $\dots$), $datatypes$ (basic datatypes and type 
constructors), $nat$ (natural numbers), $Z$ (integers), $Q$ (rationals).
The most complex development is $nat$, organized in 25 scripts, listed
in Figure\ref{scripts}
\begin{figure}[htb]
$\begin{array}{lll}
nat.ma    & plus.ma & times.ma  \\
minus.ma  & exp.ma  & compare.ma \\
orders.ma & le\_arith.ma &  lt\_arith.ma \\   
factorial.ma & sigma\_and\_pi.ma & minimization.ma  \\
div\_and\_mod.ma & gcd.ma & congruence.ma \\
primes.ma & nth\_prime.ma & ord.ma\\
count.ma  & relevant\_equations.ma & permutation.ma \\ 
factorization.ma & chinese\_reminder.ma & fermat\_little\_th.ma \\     
totient.ma& & \\
\end{array}$
\caption{\label{scripts}Matita scripts on natural numbers}
\end{figure}

We do not plan to maintain the library in a centralized way, 
as most of the systems do. On the contary we are currently
developing wiki-technologies to support a collaborative 
development of the library, encouraging people to expand, 
modify and elaborate previous contributions.

\section{Conclusions}

\acknowledgements
We would like to thank all the students that during the past
five years collaborated in the \HELM{} project and contributed to 
the development of Matita, and in particular
M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
and V.~Tamburrelli.

\theendnotes

\bibliography{matita}

\end{document}