-\documentclass{kluwer}
+\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
%}
+\newcommand{\component}{component}
+\newcommand{\components}{components}
+
\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
+\newcommand{\COQIDE}{CoqIde}
\newcommand{\ELIM}{\textsc{Elim}}
+\newcommand{\GDOME}{Gdome}
+\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
+\newcommand{\MATITAC}{\texttt{matitac}}
+\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\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{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
-\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+\newcommand{\NT}[1]{\ensuremath{\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}%
{}
\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{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
+\newcounter{pass}
+\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
+
\newsavebox{\tmpxyz}
\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
\institute{Department of Computer Science, University of Bologna\\
Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
-\runningtitle{The Matita proof assistant}
+\runningtitle{The \MATITA{} proof assistant}
\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
% \date{data}
\end{opening}
-\begin{figure}[t]
+\tableofcontents
+\listoffigures
+
+\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 distinctive 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 chosen 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;
+\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.};
+\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 components, collectively called the \HELM{} components.
+At the end of the \MOWGLI{} project we already disposed of the following
+tools and software components:
+\begin{itemize}
+\item XML specifications for the Calculus of Inductive Constructions,
+with components for parsing and saving mathematical objects in such a format
+\cite{exportation-module};
+\item metadata specifications with components 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 from 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 paste 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}
+
+\MATITA{} is a proof assistant (also called interactive theorem prover).
+It is based on the Calculus of (Co)Inductive Constructions
+(CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
+Church enriched with primitive inductive and co-inductive data types.
+Via the Curry-Howard isomorphism, the calculus can be seen as a very
+rich higher order logic and proofs can be simply represented and
+stored as lambda-terms. \COQ{} and Lego are other systems that adopt
+(variations of) CIC as their foundation.
+
+The proof language of \MATITA{} is procedural, in the tradition of the LCF
+theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
+whose proof language is procedural. Traditionally, in a procedural system
+the user interacts only with the \emph{script}, while proof terms are internal
+records kept by the system. On the contrary, in \MATITA{} proof terms are
+praised as declarative versions of the proof. With this role, they are the
+primary mean of communication of proofs (once rendered to natural language
+for human audiences).
+
+The user interfaces now adopted by all the proof assistants based on a
+procedural proof language have been inspired by the CtCoq pioneering
+system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
+by CtCoq is the Proof General generic interface~\cite{proofgeneral},
+that has set a sort of
+standard way to interact with the system. Several procedural proof assistants
+have either adopted or cloned Proof General as their main user interface.
+The authoring interface of \MATITA{} is a clone of the Proof General interface.
+
+\begin{itemize}
+ \item scelta del sistema fondazional.
+ \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 implementation
+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 reduce our code even further in sensible way).
+
+Moreover, the complexity of the code of \MATITA{} is greatly reduced with
+respect to \COQ. For instance, the API of the components of \MATITA{} comprise
+989 functions, to be compared with the 4'286 functions of \COQ.
+
+FINQUI SPELL CHECKATO
+
+Finally, \MATITA{} has several innovative 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 components.
+
+In the future we plan to exploit \MATITA{} as a test bench for new ideas and
+extensions. Keeping the single components 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.
+
+\section{Architecture}
+\label{architettura}
+
+\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.9\textwidth]{libraries}
- \caption{\MATITA{} libraries}
+ \includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters}
+ \caption[\MATITA{} components and related applications]{\MATITA{}
+ components and related applications, with thousands of line of
+ codes (klocs)}
+ \label{fig:libraries}
\end{center}
- \label{fig:libraries}
\end{figure}
-\section{Overview of the Architecture}
-Fig.~\ref{fig:libraries} shows the architecture of the \emph{libraries} (circle nodes)
-and \emph{applications} (squared nodes) developed in the HELM project.
+Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
+(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
+project. Each node is annotated with the number of lines of source code
+(comprising comments).
-Applications and libraries depend over other libraries forming a
-directed acyclic graph (DAG). Each library can be decomposed in
+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 libraries provide coherent sets of functionalities
+Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
-depend on a restricted set of libraries. \MATITA, our most complex
-application, depends on every library.
+depend on a restricted set of \components{}.
-Only the proof assistant \MATITA{} is an application 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:
+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{getter}.
+ 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
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{uwobo}.
+ 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{proofchecker}.
+ 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{dependencyanalyzer}.
+ The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}
-The dependency of a library or application over another library can
-be satisfied by linking the library in the same executable.
-For those libraries whose functionalities are also provided by the
+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} library that allows the library
-to be used as a Web service. \MATITA{} can directly link the code of the
-\texttt{getter} library, or it can use a stub library with the same API
-that forwards every request to the Getter.
+is just a wrapper to the \GETTER{} \component{} that allows the
+\component{} to be used as a Web service. \MATITA{} can directly link the code
+of the \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
-library, we can focus on the rappresentation of the mathematical information.
+\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 refinement. On each level it is possible to provide a
-different set of functionalities. The four different levels are:
-fully specified terms; partially specified terms; terms
-at the content level; terms at the presentation level.
+formulae, 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}
+\label{sec:fullyspec}
+
\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
extendible mathematical notation. They are not meant for direct user
consumption.
- The \texttt{cic} library defines the data type that represents CIC terms
+ 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 library that deals with fully specified terms is
+ 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
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} library manages the distribution,
+ distributed. The \GETTER{} \component{} manages the distribution,
providing a mapping from logical names (URIs) to the physical location
- of a notion (an URL). The \texttt{urimanager} library provides the URI
+ 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} library calls the \texttt{getter} library
- every time it needs to retrieve the definition of a mathematical notion
- referenced by a term that is being type-checked.
+ \texttt{cic\_proof\_checking} \component{} calls the \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 HTTP interface
- to the \texttt{cic\_proof\_checking} library.
+ 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
+ mathematical formula. 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} library provides a simplified
+ 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} library defines the data type of the metadata
+ 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} library implements a search engine that performs
+ 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} library). Not performing any actual matching
+ \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} library.
+ 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{sec:libmanagement}.
+
\subsection{Partially specified terms}
+\label{sec:partspec}
+
\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
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.
+value for the variable 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} library. As the type checker is based on
+partially specified term 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 use in CIC to represent proofs, so far correct incomplete
+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
\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} library. It is heavily based on the refinement and unification
-procedures of the \texttt{cic\_unification} library.
+\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.
As fully specified terms, partially specified terms are not well suited
for user consumption since their syntax is not extendible and it is not
an improvement over fully specified terms since they allow to omit redundant
information that can be inferred by the refiner.
-\subsection{Terms at the content level}
+\subsection{Content level terms}
+\label{sec:contentintro}
+
+The language used to communicate proofs and expecially formulae 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 formulae.
+
+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
+formulae. The firsts are translated to a content level representation of
+proof steps that can easily be rendered in natural language. The representation
+adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
+isomorphic to it. Terms that represent formulae are translated to \MATHML{}
+Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
+for the representation of content level formulae 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 formulae. 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 formulae. The mapping from
+content level formulae 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 formula 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.
+
+In Sect.~\ref{sec:partspec} the last section we described the semantics of a
+command as a
+function from status to status. We also suggested that the formulae in a
+command are encoded as partially specified terms. However, consider the
+command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
+of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
+replace $x$ in that context, its encoding as a term cannot be computed
+until $x$ is located. In other words, $y^2$ must be disambiguated in the
+context of the occurrence $x$ it must replace.
+
+The elegant solution we have implemented consists in representing terms
+in a command as functions from a context to a partially refined term. The
+function is obtained by partially applying our disambiguation function to
+the content term to be disambiguated. Our solution should be compared with
+the one adopted in the Coq system, where ambiguity is only relative to De Brujin
+indexes. In Coq variables can be bound either by name or by position. A term
+occurring in a command has all its variables bound by name to avoid the need of
+a context during disambiguation. Moreover, this makes more complex every
+operation over terms (i.e. according to our architecture every module that
+depends on \texttt{cic}) since the code must deal consistently with both kinds
+of binding. Also, this solution cannot cope with other forms of ambiguity (as
+the context dependent meaning of the exponent in the previous example).
+
+\subsection{Presentation level terms}
+
+Content level terms are a sort of abstract syntax trees for mathematical
+formulae 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{sec:disambiguation}.
+
+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 (summing up to a total of 11'200 lines of code)
+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{The interface to the library}
+\label{sec:library}
+
+A proof assistant provides both an interface to interact with its library and
+an \emph{authoring} interface to develop new proofs and theories. According
+to its historical origins, \MATITA{} strives to provide innovative
+functionalities for the interaction with the library. It is more traditional
+in its script based authoring interface.
+
+In the remaining part of the paper we focus on the user view of \MATITA{}.
+This section is devoted to the aspects of the tool that arise from the
+document centric approach to the library. Sect.~\ref{sec:authoring} describes
+the peculiarities of the authoring interface.
+
+The library of \MATITA{} comprises mathematical concepts (theorems,
+axioms, definitions) and notation. The concepts are authored sequentially
+using scripts that are (ordered) sequences of procedural commands.
+However, once they are produced we store them independently in the library.
+The only relation implicitly kept between the notions are the logical,
+acyclic dependencies among them. This way the library forms a global (and
+distributed) hypertext. Several useful operations can be implemented on the
+library only, regardless of the scripts. Examples of such operations
+implemented in \MATITA{} are: searching and browsing (see Sect.~\ref{sec:indexing});
+disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
+automatic proof searching (see Sect.~\ref{sec:automation}).
+
+The key requisite for the previous operations is that the library must
+be fully accessible and in a logically consistent state. To preserve
+consistency, a concept cannot be altered or removed unless the part of the
+library that depends on it is modified accordingly. To allow incremental
+changes and cooperative development, consistent revisions are necessary.
+For instance, to modify a definition, the user could fork a new version
+of the library where the definition is updated and all the concepts that
+used to rely on it are absent. The user is then responsible to restore
+the removed part in the new branch, merging the branch when the library is
+fully restored.
+
+To implement the proposed versioning system on top of a standard one
+it is necessary to implement \emph{invalidation} first. Invalidation
+is the operation that locates and removes from the library all the concepts
+that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
+a concept from the library also involves deleting its metadata from the
+database.
+
+For non collaborative development, full versioning can be avoided, but
+invalidation is still required. Since nobody else is relying on the
+user development, the user is free to change and invalidate part of the library
+without branching. Invalidation is still necessary to avoid using a
+concept that is no longer valid.
+So far, in \MATITA{} we address only this non collaborative scenario
+(see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
+is still under design.
+
+Scripts are not seen as constituents of the library. They are not published
+and indexed, so they cannot be searched or browsed using \HELM{} tools.
+However, they play a central role for the mainteinance of the library.
+Indeed, once a notion is invalidated, the only way to restore it is to
+fix the possibly broken script that used to generate it.
+Moreover, during the authoring phase, scripts are a natural way to
+group notions together. They also constitute a less fine grained clustering
+of notions for invalidation.
+
+In the rest of this section we present in more details the functionalities of
+\MATITA{} related to library management and exploitation.
+Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
+the \MATITA{} authoring interface.
+
+\subsection{Indexing and searching}
+\label{sec:indexing}
+
+\subsection{Disambiguation}
+\label{sec: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} component 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}
+\label{sec:disambaliases}
+Let us 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 what follows. 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 chose to attempt \emph{multiple disambiguation passes}. A
+first pass attempts to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass); in case of failure the next pass tries
+disambiguation again 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 us 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 interpretations 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.
+
+\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
+instance-independent. However, aliases obtained as a result of a disambiguation
+pass which uses fresh instances ought to be instance-dependent, that is: to
+ensure a term can be disambiguated in a batch fashion we may need to state that
+an \emph{i}-th instance of a symbol should be mapped to a given partially
+specified term. Instance-depend aliases are meaningful only for the term whose
+disambiguation generated it. For this reason we call them \emph{one-shot
+aliases} and \MATITA{} does not use it to disambiguate further terms down in the
+script.
+
+\subsubsection{Implicit coercions}
+
+Let us now consider a 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{*}.
+Mathematichans 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 do not 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 coercions, i.e. we always attempt
+disambiguation passes with fresh instances and no implicit coercions before
+attempting passes with implicit coercions.
+
+\subsubsection{Disambiguation passes}
+
+According to the criteria described above in \MATITA{} we choose to perform the
+sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+our experience that choice gives reasonable performance and minimize the need of
+user interaction during the disambiguation.
+
+\begin{table}[ht]
+ \caption{Sequence of disambiguation passes used in \MATITA.\strut}
+ \label{tab:disambpasses}
+ \begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Mono aliases & Shared & Disabled \\
+ \PASS & Multi aliases & Shared & Disabled \\
+ \PASS & Mono aliases & Fresh instances & Disabled \\
+ \PASS & Multi aliases & Fresh instances & Disabled \\
+ \PASS & Mono aliases & Fresh instances & Enabled \\
+ \PASS & Multi aliases & Fresh instances & Enabled \\
+ \PASS & Library aliases& Fresh instances & Enabled
+ \end{tabular}
+ \end{center}
+\end{table}
-\subsection{Terms at the presentation level}
+
+\subsection{Generation and Invalidation}
+\label{sec:libmanagement}
+
+The aim of this section is to describe the way \MATITA{}
+preserves the consistency and the availability of the library
+using the \WHELP{} technology, in response to the user alteration or
+removal of mathematical objects.
+
+As already sketched in Sec.~\ref{sec:fullyspec} what we generate
+from a script is split among two storage media, a
+classical filesystem and a relational database. The former is used to
+store the XML encoding of the objects defined in the script, the
+disambiguation aliases and the interpretation and notational convention defined,
+while the latter is used to store all the metadata needed by
+\WHELP{}.
+
+While the consistency of the data store in the two media has
+nothing to do with the nature of
+the content of the library and is thus uninteresting (but really
+tedious to implement and keep bug-free), there is a deeper
+notion of mathematical consistency we need to provide. Each object
+must reference only defined object (i.e. each proof must use only
+already proved theorems).
+
+We will focus on how \MATITA{} ensures the interesting kind
+of consistency during the formalization of a mathematical theory,
+giving the user the freedom of adding, removing, modifying objects
+without loosing the feeling of an always visible and browsable
+library.
+
+\subsubsection{Compilation}
+
+The typechecker component guarantees that if an object is well typed
+it depends only on well typed objects available in the library,
+that is exactly what we need to be sure that the logic consistency of
+the library is preserved. We have only to find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we provide a tool called \MATITADEP{}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+The user is not asked to run \MATITADEP{} by hand, but
+simply to tell \MATITA{} the root directory of his development (where all
+script files can be found) and \MATITA{} will handle all the compilation
+related tasks, including dependencies calculation.
+To compute dependencies it is enough to look at the script files for
+inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{sec:disambaliases}).
+
+The output of the compilation is immediately available to the user
+trough the \WHELP{} technology, since all metadata are stored in a
+user-specific area of the database where the search engine has read
+access, and all the automated tactics that operates on the whole
+library, like \AUTO, have full visibility of the newly defined objects.
+
+Compilation is rather simple, and the only tricky case is when we want
+to compile again the same script, maybe after the removal of a
+theorem. Here the policy is simple: clean the output before recompiling.
+As we will see in the next section cleaning will ensure that
+there will be no theorems in the development that depends on the
+removed items.
+
+\subsubsection{Cleaning}
+
+With the term ``cleaning'' we mean the process of removing all the
+results of an object compilation. In order to keep the consistency of
+the library, cleaning an object requires the (recursive) cleaning
+of all the objects that depend on it (\emph{reverse dependencies}).
+
+The calculation of the reverse dependencies can be computed in two
+ways, using the relational database or using a simpler set of metadata
+that \MATITA{} saves in the filesystem as a result of compilation. The
+former technique is the same used by the \emph{Dependency Analyzer}
+described in \cite{zack-master} and really depends on a relational
+database.
+
+The latter is a fall-back in case the database is not
+available.\footnote{Due to the complex deployment of a large piece of
+software like a database, it is a common practice for the \HELM{} team
+to use a shared remote database, that may be unavailable if the user
+workstation lacks network connectivity.} This facility has to be
+intended only as a fall-back, since the queries of the \WHELP{}
+technology depend require a working database.
+
+Cleaning guarantees that if an object is removed there are no dandling
+references to it, and that the part of the library still compiled is
+consistent. Since cleaning involves the removal of all the results of
+the compilation, metadata included, the library browsable trough the
+\WHELP{} technology is always kept up to date.
+
+\subsubsection{Batch vs Interactive}
+
+\MATITA{} includes an interactive authoring interface and a batch
+``compiler'' (\MATITAC). Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a
+part of the user development is required (for example issuing an
+\texttt{include} command) but not yet compiled.
+
+While they share the same engine for compilation and cleaning, they
+provide different granularity. The batch compiler is only able to
+compile a whole script and similarly to clean only a whole script
+(together with all the other scripts that rely on an object defined in
+it). The interactive interface is able to execute single steps of
+compilation, that may include the definition of an object, and
+similarly to undo single steps. Note that in the latter case there is
+no risk of introducing dangling references since the \MATITA{} user
+interface inhibit undoing a step which is not the last executed.
+
+\subsection{Automation}
+\label{sec:automation}
+
+\subsection{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 authoring interface}
+\label{sec:authoring}
+
+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}. At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof General
+based on Eclipse, but is not yet the case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation.
+
+The foreground window, also implemented around \GTKMATHVIEW, is called
+``cicBrowser''. It is used to browse the library, including the proof being
+developed, and enable content based search over it. Proofs are rendered in
+natural language, automatically generated from the low-level lambda-terms,
+using techniques inspired by \cite{natural,YANNTHESIS} and already described
+in~\cite{remathematization}.
+
+Note that the syntax used in the script view is \TeX-like, however unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.95\textwidth]{matita-screenshot}
+ \caption{\MATITA{} look and feel}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
+
+\subsection{Direct manipulation of terms}
+
+While terms are input as \TeX-like formulae in \MATITA, they are converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
+high-quality bidimensional rendering of terms (including the use of fancy
+layout schemata like radicals and matrices) and the use of a
+concise and widespread textual syntax.
+
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enables the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\to n$ since the former denotes an application while the
+latter it not a subterm. Once a meaningful (sub)term has been
+selected actions can be done on it like reductions or tactic
+applications.
+
+\begin{figure}[t]
+ \begin{center}
+ \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+ \hspace{0.05\textwidth}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
+ \caption{Semantic selection and hyperlinks}
+ \label{fig:directmanip}
+ \end{center}
+\end{figure}
+
+
+
+\subsection{Patterns}
+
+In several situations working with direct manipulation of terms is
+simpler and faster than typing the corresponding textual
+commands~\cite{proof-by-pointing}.
+Nonetheless we need to record actions and selections in scripts.
+
+In \MATITA{} \emph{patterns} are textual representations of selections.
+Users can select using the GUI and then ask the system to paste the
+corresponding pattern in this script, but more often this process is
+transparent: once an action is performed on a selection, the corresponding
+textual command is computed and inserted in the script.
+
+\subsubsection{Pattern syntax}
+
+Patterns are composed of two parts: \NT{sequent\_path} and
+\NT{wanted}; their concrete syntax is reported in table
+\ref{tab:pathsyn}.
+
+\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
+with $?$ and selecting the interesting parts with the placeholder
+$\%$. \NT{wanted} is a term that lives in the context of the
+placeholders.
+
+Textual patterns produced from a graphical selection are made of the
+\NT{sequent\_path} only. Such patterns can represent every selection,
+but are quite verbose. The \NT{wanted} part of the syntax is meant to
+help the users in writing concise and elegant patterns by hand.
+
+\begin{table}
+ \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
\hrule
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{pattern} &
+ ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
+ \NT{sequent\_path} &
+ ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+ [~\verb+\vdash+~\NT{multipath}~] & \\
+ \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+ \NT{wanted} & ::= & \NT{term} & \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\subsubsection{Pattern evaluation}
+
+Patterns are evaluated in two phases. The first selects roots
+(subterms) of the sequent, using the $\NT{sequent\_path}$, while the
+second 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 not only selects terms (roots of subterms) but
+ determines also their context that will be eventually used in the
+ second phase.
+
+\item[Phase 2]
+ plays a role only if the $[~\verb+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 that can be unified to
+ $\NT{wanted}$. The result of this search is the selection the
+ pattern represents.
+
+\end{description}
+
+\subsubsection{Examples}
+%To explain how the first phase works let us give an example. Consider
+%you want to prove the uniqueness of the identity element $0$ for natural
+%sum, and that you can rely 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
+Consider the following sequent
+\sequent{
+n:nat\\
+m:nat\\
+H: m + n = n}{
+m=O
+}
+\noindent
+To change the right part of the equivalence of the $H$
+hypothesis with $O + n$ the user selects and pastes it as the pattern
+in the following statement.
+\begin{grafite}
+ change in H:(? ? ? %) with (O + n).
+\end{grafite}
+\noindent
+To understand the pattern (or produce it by hand) the user should be
+aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
+that the pattern selects only the third argument of $eq$.
+
+The experienced user may also write by hand a concise pattern
+to change at once all the occcurrences of $n$ in the hypothesis $H$:
+\begin{grafite}
+ change in H match n with (O + n).
+\end{grafite}
+\noindent
+In this case the $\NT{sequent\_path}$ selects the whole $H$, while
+the second phase locates $n$.
+
+The latter pattern is equivalent to the following one, that the system
+can automatically generate from the selection.
+\begin{grafite}
+ change in H:(? ? (? ? %) %) with (O + n).
+\end{grafite}
+\noindent
+
+\subsubsection{Tactics supporting patterns}
+MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
+INTERFACCIA OCMUNE PER LE TATTICHE
+
+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 different 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 tell the
+tactic what occurrences of a wanted term should be affected.
+The second is to prepare the sequent with another tactic called
+pattern and then 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 to right.
+
+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.
-At the bottom of the DAG we have a few libraries (\texttt{extlib},
-\texttt{xml} and the \texttt{registry}) that provide a core of
-useful functions used everywhere else. In particular, the \texttt{xml} library
-to easily represent, parse and pretty-print XML files is a central component
-since in HELM every piece of information is stored in \ldots. [FINIRE]
-The other basic libraries provide often needed operations over generic
-data structures (\texttt{extlib}) and central storage for configuration options
-(the \texttt{registry}).
+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.
-\texttt{urimanager}
+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.
-\texttt{getter}
-\texttt{cic}
+\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 does not 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 \COQIDE.
+ 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{Standard library}
+\label{sec:stdlib}
+
+\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
-A.Griggio, F.Guidi, P. Di Lena, L.Padovani, I.Schena, M.Selmi,
-V.Tamburrelli.
+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}
projects / helm.git / blobdiff