X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=c5c0fff05b9e433c444bd921cf1ed71982c5904f;hb=114ee592d3da9b49abfd4c1b186cba1e170075dc;hp=b3842fbd3f3cd7bb0e6cc2959c7cc4fd36637c29;hpb=04f700d0ce01c1cc5bce8a6013e28bf38a25cf56;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index b3842fbd3..c5c0fff05 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1,4 +1,4 @@
-\documentclass[draft]{kluwer}
+\documentclass[]{kluwer}
 \usepackage{color}
 \usepackage{graphicx}
 % \usepackage{amssymb,amsmath}
@@ -139,22 +139,24 @@ 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 teps:
+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 for future system, where the documents
+a content-centric architecture\cite{content-centric} where the documents
 of the library were the the main components around which everything else 
 has to be build;
 \item developing indexing and searching techniques supporting semantic
- queries to the library; these efforts gave birth to our \WHELP{}
-search engine, described in~\cite{whelp};
+ queries to the library; 
+%these efforts gave birth to our \WHELP{}
+%search engine, described in~\cite{whelp};
 \item developing languages and tools for a high-quality notational 
-rendering of mathematical information; in particular, we have been 
-active in the MathML Working group since 1999, and developed inside
-\HELM{} a MathML-compliant widget for the GTK graphical environment
-which can be integrated in any application.
+rendering of mathematical information\footnote{We have been 
+active in the MathML Working group since 1999.}; 
+%and developed inside
+%\HELM{} a MathML-compliant widget for the GTK graphical environment
+%which can be integrated in any application.
 \end{itemize}
 
 According to our content-centric commitment, the library exported from
@@ -163,9 +165,9 @@ 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 libraries, collectively called the \HELM{} libraries.
+to a set of software libraries, collectively called the \HELM{} libraries.
 At the end of the \MOWGLI{} project we already disposed of the following
-techniques and libraries:
+tools and software libraries:
 \begin{itemize}
 \item XML specifications for the Calculus of Inductive Constructions,
 with libraries for parsing and saving mathematical objects in such a format
@@ -182,15 +184,15 @@ mathematical notation \cite{disambiguation};
 partially specified terms, used by the disambiguating parser;
 \item complex transformation algorithms for proof rendering in natural
 language \cite{remathematization};
-\item an innovative rendering widget \cite{padovani}, supporting 
+\item an innovative, MathML-compliant rendering widget for the GTK 
+graphical environment\cite{padovani}, supporting 
 high-quality bidimensional
 rendering, and semantic selection, i.e. the possibility to select semantically
 meaningful rendering expressions, and to past the respective content into
 a different text area.
 \end{itemize}
-Starting from all this, the further step of developing our own 
-proof assistant was too
-small and too tempting to be neglected. Essentially, we ``just'' had to
+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. 
@@ -268,6 +270,14 @@ allow other developers to quickly understand our code and contribute.
  \end{center}
 \end{figure}
 
+\begin{figure}[t]
+ \begin{center}
+  \includegraphics[width=0.9\textwidth]{libraries.ps}
+  \caption{\MATITA{} libraries}
+  \label{fig:libraries}
+ \end{center}
+\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.
@@ -1212,11 +1222,116 @@ implicit coercions.
 
 \TODO{alias one shot}
 
+\section{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.
+
+\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{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, 
+M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
 and V.~Tamburrelli.
 
 \theendnotes