-\documentclass[draft]{kluwer}
+\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\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.
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, the user may also dispose of the source script files,
-while in the case of Coq he may only rely on XML files of
+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. The most complex result proved
-so far in Matita (that however, at our knoweledge, has never been proved
-before in any other system) is the multiplicative property for Eulers'
-totient function $\phi$.
+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).
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
projects / helm.git / blobdiff