\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
-% \usepackage{amssymb,amsmath}
\usepackage{hyperref}
-% \usepackage{picins}
\usepackage{color}
\usepackage{fancyvrb}
\usepackage[show]{ed}
-\definecolor{gray}{gray}{0.85}
-%\newcommand{\logo}[3]{
-%\parpic(0cm,0cm)(#2,#3)[l]{\includegraphics[width=#1]{whelp-bw}}
-%}
-
\newcommand{\component}{component}
\newcommand{\components}{components}
\newcommand{\SKIP}{\MATHTT{skip}}
\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
-\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
-\newcommand{\SCRIPT}[1]{\texttt{#1}}
+\newcommand{\FILE}[1]{\texttt{#1}}
+\newcommand{\NOTE}[1]{\ednote{#1}{}}
+\newcommand{\TODO}[1]{\textbf{TODO: #1}}
+
+\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\newenvironment{grafite}{\VerbatimEnvironment
\begin{SaveVerbatim}{boxtmp}}%
\fcolorbox{black}{gray}{\BUseVerbatim[boxwidth=0.9\linewidth]{boxtmp}}
\end{center}}
-\newcounter{example}
-\newenvironment{example}{\stepcounter{example}\vspace{0.5em}\noindent\emph{Example} \arabic{example}.}
- {}
-\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
-\newcommand{\FILE}[1]{\texttt{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{}}
-\newcommand{\TODO}[1]{\textbf{TODO: #1}}
-
\newcounter{pass}
\newcommand{\PASS}{\stepcounter{pass}\arabic{pass}}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\end{center}}
-\bibliographystyle{plain}
+\bibliographystyle{alpha}
\begin{document}
\begin{opening}
-
\title{The \MATITA{} Proof Assistant}
-\author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
-\author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
-\author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
-\author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
-\institute{Department of Computer Science, University of Bologna\\
- Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
-
-\runningtitle{The \MATITA{} proof assistant}
-\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
+ \author{Andrea \surname{Asperti} \email{asperti@cs.unibo.it}}
+ \author{Claudio \surname{Sacerdoti Coen} \email{sacerdot@cs.unibo.it}}
+ \author{Enrico \surname{Tassi} \email{tassi@cs.unibo.it}}
+ \author{Stefano \surname{Zacchiroli} \email{zacchiro@cs.unibo.it}}
-% \date{data}
+ \institute{Department of Computer Science, University of Bologna\\
+ Mura Anteo Zamboni, 7 --- 40127 Bologna, ITALY}
-\begin{motto}
-``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
-\end{motto}
+ \runningtitle{The \MATITA{} proof assistant}
+ \runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
-\begin{abstract}
- abstract qui
-\end{abstract}
+ \begin{motto}
+ ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
+ \end{motto}
-\keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
-Digital Libraries}
+ \begin{abstract}
+ \TODO{scrivere abstract}
+ \end{abstract}
+ \keywords{Proof Assistant, Mathematical Knowledge Management, XML, Authoring,
+ Digital Libraries}
\end{opening}
% toc & co: to be removed in the final paper version
\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
+
+\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.
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
+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
+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
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};
+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),
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};
+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};
+language~\cite{remathematization};
\item an innovative, \MATHML-compliant rendering widget for the GTK
-graphical environment\cite{padovani}, supporting
+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
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.
-TODO
+\TODO{item che seguono:}
\begin{itemize}
\item sistema indipendente (da \COQ)
\item compatibilit\`a con sistemi legacy
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
+system whose development started 20 years ago.
+\NOTE{Zack: verificato su Coq'Art, \`e iniziato nel 1985-86}
+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
content level terms; presentation level terms.
\subsection{Fully specified terms}
-\label{sec:fullyspec}
+\label{sec:fullyintro}
\emph{Fully specified terms} are CIC terms where no information is
missing or left implicit. A fully specified term should be well-typed.
in Sect.~\ref{sec:libmanagement}.
\subsection{Partially specified terms}
-\label{sec:partspec}
+\label{sec:partiallyintro}
\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
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
+In Sect.~\ref{sec:partiallyintro} 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
the context dependent meaning of the exponent in the previous example).
\subsection{Presentation level terms}
+\label{sec:presentationintro}
Content level terms are a sort of abstract syntax trees for mathematical
formulae and proofs. The concrete syntax given to these abstract trees
presentation
level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
\GTKMATHVIEW{}
-widget developed by Luca Padovani \cite{padovani}. The widget is
+widget developed by Luca Padovani~\cite{padovani}. The widget is
particularly interesting since it allows to implement \emph{semantic
selection}.
\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}}
-
+browser.\NOTE{\TODO{manca la passata verso HTML}}
The \components{} not yet described (\texttt{extlib}, \texttt{xml},
\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
%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}
\forall x, y, z. x < y \to y < z \to x < z.
\end{grafite}
-The symbol ``\texttt{<}'' is likely to be overloaded in the library
+The symbol \OP{<} is likely to be overloaded in the library
(at least over natural numbers).
Thus, according to the disambiguation algorithm, two different
refinable partially specified terms could be associated to it.
\end{grafite}
The ``alias'' command in the example sets the preferred alias for the
-``\texttt{lt}'' symbol.
+\OP{lt} symbol.
Implicit preferences for new concepts are set since a concept just defined is
likely to be the preferred one in the rest of the script. Implicit preferences
reducing the search space.
Disambiguation preferences are included in the lexicon status
-(see Sect.~\ref{???}) that is part of the authoring interface status.
-Unlike aliases, they are not part of the library.
+(see Sect.~\ref{sec:presentationintro} that is part of the authoring interface
+status. Unlike aliases, they are not part of the library.
When starting a new authoring session the set of disambiguation preferences
is empty. Until it contains a preference for each overloaded symbol to be
at the end of the execution of a given script.
Preferences can be changed. For instance, at the start of the development
-of integer numbers the preference for the symbol ``\texttt{<}'' is likely
+of integer numbers the preference for the symbol \OP{<} is likely
to be the one over natural numbers; sooner or later it will be set to the one
over integer numbers.
we consider every alias corresponding to a current or past preference.
For instance, in the example above disambiguation succeeds in the
multi-preference pass
-TODO: CAMBIATO SOLO FINO A QUI
+\TODO{Disambiguazione: cambiato solo FINQUI}
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
fail quickly) and degree of ambiguity supported for presentation level terms.
\subsubsection{Operator instances}
+\label{sec:disambinstances}
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
script.
\subsubsection{Implicit coercions}
+\label{sec:disambcoercions}
Let us now consider a theorem about derivation:
attempting passes with implicit coercions.
\subsubsection{Disambiguation passes}
+\label{sec:disambpasses}
According to the criteria described above in \MATITA{} we choose to perform the
sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
\end{center}
\end{table}
-
-
\subsection{Generation and Invalidation}
\label{sec:libmanagement}
using the \WHELP{} technology, in response to the user alteration or
removal of mathematical objects.
-As already sketched in Sect.~\ref{sec:fullyspec} what we generate
+As already sketched in Sect.~\ref{sec:fullyintro} 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
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
+described in~\cite{zack-master} and really depends on a relational
database.
The latter is a fall-back in case the database is not
\subsection{Automation}
\label{sec:automation}
+\TODO{sezione sull'automazione}
+
\subsection{Naming convention}
+\label{sec:naming}
+
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.
``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
+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
features of the \MATITA{} authoring interface.
\subsection{Direct manipulation of terms}
+\label{sec:directmanip}
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
\end{center}
\end{figure}
-TODO: referenziarli e spostarli nella parte sulla libreria?
+\TODO{referenziarli e spostarli nella parte sulla libreria?}
+
\begin{figure}[!ht]
\begin{center}
\includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
\end{figure}
\subsection{Patterns}
+\label{sec:patterns}
In several situations working with direct manipulation of terms is
simpler and faster than typing the corresponding textual
\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{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
with $?$ and selecting the interesting parts with the placeholder
\noindent
\subsubsection{Tactics supporting patterns}
-MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
-INTERFACCIA OCMUNE PER LE TATTICHE
+
+\TODO{mergiare con il successivo facendo notare che i patterns sono una
+interfaccia comune 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,
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with \COQ{}}
+
\COQ{} has two different ways of restricting the application of tactics to
subterms of the sequent, both relaying on the same special syntax to identify
a term occurrence.
write it and say that we want, for example, the third and the fifth
occurrences of it (counting from left to right). In our previous example,
to change only the left part of the equivalence, the correct command
-is
+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
+command:
\begin{grafite}
pattern n at 2 in H
\end{grafite}
-\noindent
-would have resulted in this sequent
+
+would have resulted in this sequent:
+
\begin{grafite}
n : nat
m : nat
============================
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
adopting a method for restricting tactics application domain that discourages
using heavy math notation, would definitively be a bad choice.
-
\subsection{Tacticals}
+\label{sec:tinycals}
+
There are mainly two kinds of languages used by proof assistants to recorder
proofs: tactic based and declarative. We will not investigate the philosophy
around the choice that many proof assistant made, \MATITA{} included, and we
\hrule
\end{table}
-\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
+\MATITA{} tacticals syntax is reported in Tab.~\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
\begin{table}[ht]
\begin{tabular}{lll}
- \SCRIPT{nat.ma} & \SCRIPT{plus.ma} & \SCRIPT{times.ma} \\
- \SCRIPT{minus.ma} & \SCRIPT{exp.ma} & \SCRIPT{compare.ma} \\
- \SCRIPT{orders.ma} & \SCRIPT{le\_arith.ma} & \SCRIPT{lt\_arith.ma} \\
- \SCRIPT{factorial.ma} & \SCRIPT{sigma\_and\_pi.ma} & \SCRIPT{minimization.ma} \\
- \SCRIPT{div\_and\_mod.ma} & \SCRIPT{gcd.ma} & \SCRIPT{congruence.ma} \\
- \SCRIPT{primes.ma} & \SCRIPT{nth\_prime.ma} & \SCRIPT{ord.ma} \\
- \SCRIPT{count.ma} & \SCRIPT{relevant\_equations.ma} & \SCRIPT{permutation.ma} \\
- \SCRIPT{factorization.ma} & \SCRIPT{chinese\_reminder.ma} &
- \SCRIPT{fermat\_little\_th.ma} \\
- \SCRIPT{totient.ma} & & \\
+ \FILE{nat.ma} & \FILE{plus.ma} & \FILE{times.ma} \\
+ \FILE{minus.ma} & \FILE{exp.ma} & \FILE{compare.ma} \\
+ \FILE{orders.ma} & \FILE{le\_arith.ma} & \FILE{lt\_arith.ma} \\
+ \FILE{factorial.ma} & \FILE{sigma\_and\_pi.ma} & \FILE{minimization.ma} \\
+ \FILE{div\_and\_mod.ma} & \FILE{gcd.ma} & \FILE{congruence.ma} \\
+ \FILE{primes.ma} & \FILE{nth\_prime.ma} & \FILE{ord.ma} \\
+ \FILE{count.ma} & \FILE{relevant\_equations.ma} & \FILE{permutation.ma} \\
+ \FILE{factorization.ma} & \FILE{chinese\_reminder.ma} &
+ \FILE{fermat\_little\_th.ma} \\
+ \FILE{totient.ma} & & \\
\end{tabular}
\caption{\label{tab:scripts} Scripts on natural numbers in the standard library}
\end{table}
modify and elaborate previous contributions.
\section{Conclusions}
+\label{sec:conclusion}
+
+\TODO{conclusioni}
\acknowledgements
We would like to thank all the students that during the past
projects / helm.git / commitdiff