X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=84c98b48406b0155959e8779257e5a82ef2bc746;hb=6c43a7f440daf19e2475b7eabd20456bdb0e9f76;hp=3cc2faf039f4826469b0f8e1a0e31ca8a50ac6a0;hpb=c2e705d92a743db375539b8face34e5ee114e909;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 3cc2faf03..84c98b484 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1,4 +1,4 @@
-\documentclass[]{kluwer}
+\documentclass[draft]{kluwer}
 \usepackage{color}
 \usepackage{graphicx}
 % \usepackage{amssymb,amsmath}
@@ -18,6 +18,7 @@
 
 \newcommand{\AUTO}{\textsc{Auto}}
 \newcommand{\COQ}{Coq}
+\newcommand{\COQIDE}{CoqIde}
 \newcommand{\ELIM}{\textsc{Elim}}
 \newcommand{\GDOME}{Gdome}
 \newcommand{\HELM}{Helm}
@@ -105,7 +106,7 @@
 \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}
@@ -123,6 +124,7 @@ Digital Libraries}
 
 \end{opening}
 
+
 \section{Introduction}
 \label{sec:intro}
 \MATITA{} is the Proof Assistant under development by the \HELM{} team
@@ -163,7 +165,7 @@ 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
+\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.
 
@@ -205,7 +207,7 @@ DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
 
 \begin{itemize}
  \item scelta del sistema fondazionale
- \item sistema indipendente (da Coq)
+ \item sistema indipendente (da \COQ)
  \item compatibilit\`a con sistemi legacy
 \end{itemize}
 
@@ -274,6 +276,7 @@ allow other developers to quickly understand our code and contribute.
 \end{figure}
 
 \section{Architecture}
+\label{architettura}
 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
 (circle nodes) and \emph{applications} (squared nodes) developed in the HELM
 project.
@@ -329,9 +332,9 @@ 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
+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 \texttt{getter} \component, or it can use a stub library with the same
+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
@@ -345,6 +348,7 @@ fully specified terms; partially specified terms;
 content level terms; presentation level terms.
 
 \subsection{Fully specified terms}
+\label{fully-spec}
  \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
@@ -365,11 +369,11 @@ content level terms; presentation level terms.
 
    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,
+   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} \component{} provides the URI
    data type and several utility functions over URIs. The
-   \texttt{cic\_proof\_checking} \component{} calls the \texttt{getter}
+   \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. 
 
@@ -408,7 +412,7 @@ content level terms; presentation level terms.
    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}.
+   in Sect.~\ref{sec:libmanagement}.
    
 \subsection{Partially specified terms}
 \emph{Partially specified terms} are CIC terms where subterms can be omitted.
@@ -597,7 +601,7 @@ 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}.
+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
@@ -690,14 +694,212 @@ content selection and copy-paste.
 
 \subsection{Indexing and searching}
 
-\subsection{Developments}
+
+\subsection{Compilation and decompilation}
+\label{sec:libmanagement}
+
+The aim of this section is to describe the way matita 
+preserves the consistency and the availability of the library
+trough the \WHELP{} technology, in response to the user addition or 
+deletion of mathematical objects.
+
+As already sketched in \ref{fully-spec} the output of the
+compilation of 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{}. In addition the \GETTER component
+should be updated with the the new mapping between the logical URI
+and the physical path of objects.
+
+While this kind of consistency has nothing to do with the nature of
+the content of the library and is thus of poor interest (but really
+tedious to implement and keep bug-free), there is a more deep
+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, deleting, 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 defined 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 find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we developed a low level tool called \emph{matitadep}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the make utility.
+The user is not asked to run \emph{matitadep} nor make 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
+tasks.\\
+To calculate dependencies it is enough to look at the script file for
+its inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{aliases}). 
+
+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 deletion of a
+theorem. Here the policy is simple: decompile it before recompiling.
+As we will see in the next section decompilation will ensure that
+there will be no theorems in the development that depends on the
+removed item.
+
+\subsubsection{Decompilation}
+Decompiling an object involves,
+recursively, the decompilation of all the objects that depend on it.
+
+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. Due to
+the complex deployment of a complex peace of software like a database,
+it is a common usage for the \HELM{} team to use a single and remote
+database, that may result unavailable if the user workstation lacks
+connectivity.  This facility has to be intended only as a fall-back,
+since the whole \WHELP{} technology depends on the database.
+
+Decompilation guarantees that if an object is removed there are no
+dandling references to it, and that the part of the library still
+compiled is logically consistent. Since decompilation involves the
+deletion of all the outputs of the compilation, metadata included, the
+library browsable trough the \WHELP{} technology is always up to date.
+
+\subsubsection{Interactive and batch (de)compilation}
+\MATITA{} includes an interactive graphical interface and a batch
+compiler. Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a not yet compiled
+part of the user development is required.
+
+While they share the same engine for compilation and decompilation,
+they provide different granularity. The batch compiler is only able to
+compile a whole script file and reciprocally it can decompile only a whole
+script, and consequently 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
+symmetrically to undo single steps, thus removing single objects.
+
+%
+%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
+%\subsubsection{Composition}
+%scripts.ma, .moo, XML, metadata
+%\subsubsection{Compilation}
+%analogie con compilazione classica dso.\\
+%granularita' differenti per uso interattivo e non
+%\paragraph{Batch}
+%- granularita' .ma/buri \\
+%-- motivazioni\\
+%- come si calcolano le dipendenze\\
+%- quando la si usa\\
+%- metodi (cc e clean)\\
+%- garanzie
+%\paragraph{Interactive}
+%- granularita' fine\\
+%-- motivazioni
+%\label{sec:libmanagement}
+%consistenza: integrita' referenziale
+%Goals: mantenere consistente la rappresentazione della libreria su memoria persistente consentendo di compilare e decompilare le compilation unit (.ma).\\
+%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
+%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
+%--- granularita' oggetto per matita interactive\\
+%--- granularita' baseuri (compilation unit) per la libreria\\
+%In entrmbi i casi ora:\\
+%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
+%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
+%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
+%Vincoli di remove: \\
+%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
+%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
+%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
+%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
 
 \subsection{Automation}
 
-\subsection{Naming}
+\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}
+\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
@@ -710,7 +912,7 @@ 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}
+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
@@ -718,7 +920,7 @@ some of its parameters, helps in keeping the input terse without sacrificing
 expressiveness.
 
 \subsubsection{Disambiguation aliases}
-
+\label{aliases}
 Let's start with the definition of the ``strictly greater then'' notion over
 (Peano) natural numbers.
 
@@ -731,7 +933,7 @@ definition gt: nat \to nat \to Prop \def
 
 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
+processing the 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.
@@ -827,7 +1029,7 @@ theorem lt_to_Zlt_pos_pos:
 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
+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
@@ -874,30 +1076,42 @@ 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.
+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}
 
+Summarizing, we perform multiple disambiguation passes for each presentation
+level term and in each of them we have 3 degree of freedom: disambiguation
+aliases (mono/multi/library), operator instances (shared/fresh), and implicit
+coercions (enabled/disabled). This would lead to up to 12 different
+disambiguation passes with ordering to be decided upon. Our choice in \MATITA{}
+is depicted in Tab.~\ref{tab:disambpasses}.
+
 \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}
+\begin{table}
+ \caption{Disambiguation passes.\strut}
+ \label{tab:disambpasses} 
+ \footnotesize
+ \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}
 
 \TODO{alias one shot}
 
@@ -906,111 +1120,6 @@ implicit coercions.
 
 
 
-\subsection{The logical 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.
-
-\subsubsection{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{Patterns}
 
@@ -1022,7 +1131,7 @@ tattichini.\\
 Patterns are the textual counterpart of the MathML widget graphical
 selection.
 
-Matita benefits of a graphical interface and a powerful MathML rendering
+\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
@@ -1175,8 +1284,8 @@ 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
+\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.
 
@@ -1389,7 +1498,7 @@ even being a so simple idea:
 \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.
+  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 
@@ -1424,12 +1533,50 @@ even being a so simple idea:
   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
+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.