-\documentclass{kluwer}
+\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
\newcommand{\URI}[1]{\texttt{#1}}
+\newcommand{\OP}[1]{``\texttt{#1}''}
%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
+\newcounter{pass}
+\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
+
\newsavebox{\tmpxyz}
\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
\section{Introduction}
\label{sec:intro}
-In this paper we describe the architecture and a few distintive features of the
-\emph{\MATITA} proof assistant. \MATITA{} was not conceived out of the blue
-one single day; it has been the next natural step in the evolution of one
-line of research we started six years ago. Thus, to better understand the
-system, we start from its historical roots.
+\MATITA{} is the Proof Assistant under development by the \HELM{} team
+\cite{mkm-helm} at the University of Bologna, under the direction of
+Prof.~Asperti. \\
+The paper describes the overall architecture of
+the system, focusing on its most distintive and innovative
+features.
\subsection{Historical Perspective}
-\MATITA{} is under development by the \HELM{} team
-\cite{mkm-helm} at the University of Bologna, under the direction of
-Prof.~Asperti.
-The origin of the system goes back to 1999. At the time we were mostly
+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{} proof assistant (of the order of 35'000 theorems)
+library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
was choosed as a privileged test bench for our work, although experiments
-have been also conducted with other systems, and notably with \NUPRL{}.
+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
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;
+with libraries for parsing and saving mathematical objects in such a format
+\cite{exportation-module};
\item metadata specifications with libraries for indexing and querying the
XML knowledge base;
\item a proof checker library (i.e. the {\em kernel} of a proof assistant),
\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;
-\item an innovative rendering widget, supporting high-quality bidimensional
+language \cite{remathematization};
+\item an innovative, MathML-compliant rendering widget for the GTK
+graphical environment\cite{padovani}, supporting
+high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
meaningful rendering expressions, and to past the respective content into
a different text area.
\end{itemize}
-Starting from all this, 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.
\subsection{The System}
+DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
+
+\begin{itemize}
+ \item scelta del sistema fondazionale
+ \item sistema indipendente (da Coq)
+ \item compatibilit\`a con sistemi legacy
+\end{itemize}
+
+\subsection{Relationship with \COQ{}}
At first sight, \MATITA{} looks as (and partly is) a \COQ{} clone. This is
more the effect of the circumstances of its creation described
extensions. Keeping the single libraries and the whole architecture as
simple as possible is thus crucial to speed up future experiments and to
allow other developers to quickly understand our code and contribute.
-For direct experience of the authors, the learning curve to understand and
-be able to contribute to \COQ{}'s code is quite steep and requires direct
-and frequent interactions with \COQ{} developers.
-\begin{itemize}
- \item scelta del sistema fondazionale
- \item sistema indipendente (da Coq)
- \begin{itemize}
- \item possibilit\`a di sperimentare (soluzioni architetturali, logiche,
- implementative, \dots)
- \item compatibilit\`a con sistemi legacy
- \end{itemize}
-\end{itemize}
+%For direct experience of the authors, the learning curve to understand and
+%be able to contribute to \COQ{}'s code is quite steep and requires direct
+%and frequent interactions with \COQ{} developers.
\begin{figure}[t]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
- \caption{\label{fig:libraries}\MATITA{} libraries}
+ \caption{\MATITA{} libraries}
+ \label{fig:libraries}
+ \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}
information that can be inferred by the refiner.
\subsection{Content level terms}
+\label{sec:contentintro}
+
The language used to communicate proofs and expecially expressions with the
user does not only needs to be extendible and accomodate the usual mathematical
notation. It must also reflect the comfortable degree of imprecision and
is guided by an \emph{interpretation}, that is a function that chooses for
every ambiguous expression one partially specified term. The
\texttt{disambiguation} library contains the implementation of the
-disambiguation algorithm we presented in \cite{disambiguation} that is
+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.
goal) gives you the feeling of what is going on.
\end{description}
+\section{Content level terms}
+
+\subsection{Disambiguation}
+
+Software applications that involve input of mathematical content should strive
+to require the user as less drift from informal mathematics as possible. We
+believe this to be a fundamental aspect of such applications user interfaces.
+Being that drift in general very large when inputing
+proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
+mathematical formulae which can be input using a \TeX-like encoding (the
+concrete syntax corresponding to presentation level terms) and are then
+translated (in multiple steps) to partially specified terms as sketched in
+Sect.~\ref{sec:contentintro}.
+
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+such an algorithm in the context of the development of a library of formalized
+mathematics. We will see that using multiple passes of the algorithm, varying
+some of its parameters, helps in keeping the input terse without sacrificing
+expressiveness.
+
+\subsubsection{Disambiguation aliases}
+
+Let's start with the definition of the ``strictly greater then'' notion over
+(Peano) natural numbers.
+
+\begin{grafite}
+include "nat/nat.ma".
+..
+definition gt: nat \to nat \to Prop \def
+ \lambda n, m. m < n.
+\end{grafite}
+
+The \texttt{include} statement adds the requirement that the part of the library
+defining the notion of natural numbers should be defined before
+processing the following definition. Note indeed that the algorithm presented
+in~\cite{disambiguation} does not describe where interpretations for ambiguous
+expressions come from, since it is application-specific. As a first
+approximation, we will assume that in \MATITA{} they come from the library (i.e.
+all interpretations available in the library are used) and the \texttt{include}
+statements are used to ensure the availability of required library slices (see
+Sect.~\ref{sec:libmanagement}).
+
+While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
+terms: its type and its body. Being available in the required library only one
+interpretation both for the unbound identifier \texttt{nat} and for the
+\OP{<} operator, and being the resulting partially specified term refinable,
+both type and body are easily disambiguated.
+
+Now suppose we have defined integers as signed natural numbers, and that we want
+to prove a theorem about an order relationship already defined on them (which of
+course overload the \OP{<} operator):
+
+\begin{grafite}
+include "Z/z.ma".
+..
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+Since integers are defined on top of natural numbers, the part of the library
+concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
+type. Thus, according to the disambiguation algorithm, two different partially
+specified terms could be associated to it. At first, this might not be seen as a
+problem, since the user is asked and can choose interactively which of the two
+she had in mind. However in the long run it has the drawbacks of inhibiting
+batch compilation of the library (a technique used in \MATITA{} for behind the
+scene compilation when needed, e.g. when an \texttt{include} is issued) and
+yields to poor user interaction (imagine how tedious would be to be asked for a
+choice each time you re-evaluate \texttt{Zlt\_compat}!).
+
+For this reason we added to \MATITA{} the concept of \emph{disambiguation
+aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
+expressions to partially specified terms, which are part of the runtime status
+of \MATITA. They can be provided by users with the \texttt{alias} statement, but
+are usually automatically added when evaluating \texttt{include} statements
+(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
+are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
+which require interactive choice are saved in batch compilable format. Thus,
+after evaluating the above theorem the script will be changed to the following
+snippet (assuming that the interpretation of \OP{<} over integers has been
+choosed):
+
+\begin{grafite}
+alias symbol "lt" = "integer 'less than'".
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+But how are disambiguation aliases used? Since they come from the parts of the
+library explicitely included we may be tempted of using them as the only
+available interpretations. This would speed up the disambiguation, but may fail.
+Consider for example:
+
+\begin{grafite}
+theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+and suppose that the \OP{+} operator is defined only on natural numbers. If
+the alias for \OP{<} points to the integer version of the operator, no
+refinable partially specified term matching the term could be found.
+
+For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
+first pass attempt to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass), in case of failure the next pass try again
+the disambiguation forgetting the aliases and using the whole library to
+retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
+Since the latter pass may lead to too many choices we intertwined an additional
+pass among the two which use as interpretations all the aliases coming for
+included parts of the library (\emph{multi aliases} phase). This is the reason
+why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
+turned out to be a well-balanced trade-off among performances (earlier passes
+fail quickly) and degree of ambiguity supported for presentation level terms.
+
+\subsubsection{Operator instances}
+
+Let's suppose now we want to define a theorem relating ordering relations on
+natural and integer numbers. The way we would like to write such a theorem (as
+we can read it in the \MATITA{} standard library) is:
+
+\begin{grafite}
+include "Z/z.ma".
+include "nat/orders.ma".
+..
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+
+Unfortunately, none of the passes described above is able to disambiguate its
+type, no matter how aliases are defined. This is because the \OP{<} operator
+occurs twice in the content level term (it has two \emph{instances}) and two
+different interpretation for it have to be used in order to obtain a refinable
+partially specified term. To address this issue, we have the ability to consider
+each instance of a single symbol as a different ambiguous expression in the
+content level term, and thus we can assign a different interpretation to each of
+them. A disambiguation pass which exploit this feature is said to be using
+\emph{fresh instances}.
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+an interpretation for one instances does not constraint the choice for the
+others). For this reason we always attempt a fresh instances pass only after
+attempting a non-fresh one.
+
+\subsubsection{Implicit coercions}
+
+Let's now consider a (rather hypothetical) theorem about derivation:
+
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+\end{grafite}
+
+and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
+interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
+Mathematichians would write the term that way since it is well known that the
+natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
+number for the purpose of real multiplication. The refiner of \MATITA{} supports
+\emph{implicit coercions} for this reason: given as input the above content
+level term, it will return a partially specified term where in place of
+\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
+(assuming it has been defined as such of course).
+
+Nonetheless coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
+among the possible partially specified term choices. For this reason in
+\MATITA{} we always try first a disambiguation pass which require the refiner
+not to use the coercions and only in case of failure we attempt a
+coercion-enabled pass.
+
+It is interesting to observe also the relationship among operator instances and
+implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
+which \MATITA{} disambiguated using fresh instances. In case there exists a
+coercion from natural numbers to (positive) integers (which indeed does, it is
+the \texttt{pos} constructor itself), the theorem can be disambiguated using
+twice that coercion on the left hand side of the implication. The obtained
+partially specified term however would not probably be the expected one, being a
+theorem which prove a trivial implication. For this reason we choose to always
+prefer fresh instances over implicit coercion, i.e. we always attempt
+disambiguation passes with fresh instances before attempting passes with
+implicit coercions.
+
+\subsubsection{Disambiguation passes}
+
+\TODO{spiegazione della tabella}
+
+\begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Normal & Mono & Disabled \\
+ \PASS & Normal & Multi & Disabled \\
+ \PASS & Fresh & Mono & Disabled \\
+ \PASS & Fresh & Multi & Disabled \\
+ \PASS & Fresh & Mono & Enabled \\
+ \PASS & Fresh & Multi & Enabled \\
+ \PASS & Fresh & Library & Enabled
+ \end{tabular}
+\end{center}
+
+\TODO{alias one shot}
+
+\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,
-V.Tamburrelli.
+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