-\documentclass[]{kluwer}
+\documentclass[draft]{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{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
-\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\UWOBO}{UWOBO}
\newcommand{\GETTER}{Getter}
\newcommand{\WHELP}{Whelp}
+
\newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
\newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
\newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
\newcommand{\SKIP}{\MATHTT{skip}}
\newcommand{\TACTIC}[1]{\ensuremath{\mathtt{tactic}~#1}}
-\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
-\newcommand{\NT}[1]{\langle\mathit{#1}\rangle}
+\newcommand{\NT}[1]{\ensuremath{\langle\mathit{#1}\rangle}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[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
\tableofcontents
+\listoffigures
+\listoftables
\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
-the system, focusing on its most distintive and innovative
+
+\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.
\subsection{Historical Perspective}
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~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
-was choosed as a privileged test bench for our work, although experiments
+was chosen as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
-with \NUPRL{}\cite{nuprl-book}.
+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
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\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 software libraries, collectively called the \HELM{} libraries.
+to a set of software components, collectively called the \HELM{} components.
At the end of the \MOWGLI{} project we already disposed of the following
-tools and software libraries:
+tools and software components:
\begin{itemize}
\item XML specifications for the Calculus of Inductive Constructions,
-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
+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),
-implemented to check that we exported form the \COQ{} library all the
+implemented to check that we exported from the \COQ{} library all the
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 past the respective content into
+meaningful rendering expressions, and to paste the respective content into
a different text area.
\end{itemize}
Starting from all this, developing our own proof assistant was not
overall management of the library, integrating everything into a
single system. \MATITA{} is the result of this effort.
+\subsection{The system}
+
+\MATITA{} is a proof assistant (also called interactive theorem prover).
+It is based on the Calculus of (Co)Inductive Constructions
+(CIC)~\cite{Werner} that is a dependently typed lambda-calculus \`a la
+Church enriched with primitive inductive and co-inductive data types.
+Via the Curry-Howard isomorphism, the calculus can be seen as a very
+rich higher order logic and proofs can be simply represented and
+stored as lambda-terms. \COQ{} and Lego are other systems that adopt
+(variations of) CIC as their foundation.
+
+The proof language of \MATITA{} is procedural, in the tradition of the LCF
+theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
+whose proof language is procedural. Traditionally, in a procedural system
+the user interacts only with the \emph{script}, while proof terms are internal
+records kept by the system. On the contrary, in \MATITA{} proof terms are
+praised as declarative versions of the proof. With this role, they are the
+primary mean of communication of proofs (once rendered to natural language
+for human audiences).
+
+The user interfaces now adopted by all the proof assistants based on a
+procedural proof language have been inspired by the CtCoq pioneering
+system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
+by CtCoq is the Proof General generic interface~\cite{proofgeneral},
+that has set a sort of
+standard way to interact with the system. Several procedural proof assistants
+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{item che seguono:}
+\begin{itemize}
+ \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
above than the result of a deliberate design. In particular, we
(essentially) share the same foundational dialect of \COQ{} (the
-Calculus of (Co)Inductive Constructions), the same implementative
+Calculus of (Co)Inductive Constructions), the same implementation
language (\OCAML{}), and the same (script based) authoring philosophy.
However, the analogy essentially stops here and no code is shared by the
two systems.
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
by \COQ{} (and we are convinced that, starting from scratch again,
-we could furtherly reduce our code in sensible way).
+we could reduce our code even further in sensible way).
Moreover, the complexity of the code of \MATITA{} is greatly reduced with
-respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
+respect to \COQ. For instance, the API of the components of \MATITA{} comprise
989 functions, to be compared with the 4'286 functions of \COQ.
-Finally, \MATITA{} has several innovatives features over \COQ{} that derive
+Finally, \MATITA{} has several innovative features over \COQ{} that derive
from the integration of Mathematical Knowledge Management tools with proof
assistants. Among them, the advanced indexing tools over the library and
the parser for ambiguous mathematical notation.
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
for \COQ{} that require backward compatibility between each pair of releases;
since many central functionalities of a proof assistant are based on heuristics
or arbitrary choices to overcome undecidability (e.g. for higher order
-unification), changing these functionalities mantaining backward compatibility
+unification), changing these functionalities maintaining backward compatibility
is very difficult. Finally, the code of \COQ{} has been greatly optimized
-over the years; optimization reduces maintenability and rises the complexity
+over the years; optimization reduces maintainability and rises the complexity
of the code.
In writing \MATITA{} we have not been hindered by backward compatibility and
we have took advantage of the research results and experiences previously
developed by others, comprising the authors of \COQ. Moreover, starting from
-scratch, we have designed in advance the architecture and we have splitted
-the code in coherent minimally coupled libraries.
+scratch, we have designed in advance the architecture and we have split
+the code in coherent minimally coupled components.
In the future we plan to exploit \MATITA{} as a test bench for new ideas and
-extensions. Keeping the single libraries and the whole architecture as
+extensions. Keeping the single components and the whole architecture as
simple as possible is thus crucial to foster future experiments and to
allow other developers to quickly understand our code and contribute.
%be able to contribute to \COQ{}'s code is quite steep and requires direct
%and frequent interactions with \COQ{} developers.
-\subsection{The system}
-
-DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''\\
-ROBA CHE MANCA:
-\begin{itemize}
- \item scelta del sistema fondazionale
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
-
-\begin{figure}[t]
- \begin{center}
- \includegraphics[width=0.95\textwidth]{matita-screenshot}
- \caption{\MATITA{} look and feel}
- \label{fig:screenshot}
- \end{center}
-\end{figure}
-
-\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
-split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a \MATHML{} rendering
-widget. A distinguished part of the script (shaded in the screenshot) represent
-the commands already executed and can't be edited without undoing them. The
-remaining part can be freely edited and commands from that part can be executed
-moving down the execution point. An additional window --- the ``cicBrowser'' ---
-can be used to browse the library, including the proof being developed, and
-enable content based search on it. In the cicBrowser proofs are rendered in
-natural language, automatically generated from the low-level $\lambda$-terms
-using techniques inspired by \cite{natural,YANNTHESIS}.
-
-In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
-only seen as a convenient way to create mathematical objects. The universe of
-all these objects makes up the \HELM{} library, which is always completely
-visible to the user. The mathematical library is thus conceived as a global
-hypertext, where objects may freely reference each other. It is a duty of
-the system to guide the user through the relevant parts of the library.
-
-This methodological assumption has many important consequences
-which will be discussed in the next section.
-
-%on one side
-%it requires functionalities for the overall management of the library,
-%%%%%comprising efficient indexing techniques to retrieve and filter the
-%information;
-%on the other it introduces overloading in the use of
-%identifiers and mathematical notation, requiring sophisticated disambiguation
-%techniques for interpreting the user inputs.
-%In the next two sections we shall separately discuss the two previous
-%points.
-
-%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
-%organized in components which work on data in this format. For instance the
-%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%\MATHML{} Presentation documents, can be used apart from \MATITA{} to print ...
-%FINIRE
-
-A final section is devoted to some innovative aspects
-of the authoring system, such as a step by step tactical execution,
-content selection and copy-paste.
-
\section{Architecture}
\label{architettura}
-\begin{figure}[ht]
+\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.9\textwidth]{librariesCluster.ps}
- \caption{\MATITA{} libraries}
+ \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
+ \caption[\MATITA{} components and related applications]{\MATITA{}
+ components and related applications, with thousands of line of
+ codes (klocs).\strut}
\label{fig:libraries}
\end{center}
\end{figure}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
-project.
+project. Each node is annotated with the number of lines of source code
+(comprising comments).
Applications and \components{} depend over other \components{} forming a
directed acyclic graph (DAG). Each \component{} can be decomposed in
are Web services developed in the HELM and MoWGLI projects and already described
elsewhere. In particular:
\begin{itemize}
- \item The \emph{Getter} is a Web service to retrieve an (XML) document
+ \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
from a physical location (URL) given its logical name (URI). The Getter is
responsible of updating a table that maps URIs to URLs. Thanks to the Getter
it is possible to work on a logically monolithic library that is physically
distributed on the network. More information on the Getter can be found
in~\cite{zack-master}.
- \item \emph{Whelp} is a search engine to index and locate mathematical
+ \item \emph{\WHELP} is a search engine to index and locate mathematical
notions (axioms, theorems, definitions) in the logical library managed
by the Getter. Typical examples of a query to Whelp are queries that search
for a theorem that generalize or instantiate a given formula, or that
an XML document that lists the URIs of a complete set of candidates that
are likely to satisfy the given query. The set is complete in the sense
that no notion that actually satisfies the query is thrown away. However,
- the query is only approssimated in the sense that false matches can be
+ the query is only approximated in the sense that false matches can be
returned. Whelp has been described in~\cite{whelp}.
- \item \emph{Uwobo} is a Web service that, given the URI of a mathematical
+ \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
notion in the distributed library, renders it according to the user provided
- two dimensional mathematical notation. Uwobo may also embed the rendering
+ two dimensional mathematical notation. \UWOBO{} may also embed the rendering
of mathematical notions into arbitrary documents before returning them.
- The Getter is used by Uwobo to retrieve the document to be rendered.
- Uwobo has been described in~\cite{zack-master}.
+ The Getter is used by \UWOBO{} to retrieve the document to be rendered.
+ \UWOBO{} has been described in~\cite{zack-master}.
\item The \emph{Proof Checker} is a Web service that, given the URI of
notion in the distributed library, checks its correctness. Since the notion
is likely to depend in an acyclic way over other notions, the proof checker
dependencies, checking in turn every notion for correctness.
The proof checker has been described in~\cite{zack-master}.
\item The \emph{Dependency Analyzer} is a Web service that can produce
- a textual or graphical representation of the dependecies of an object.
+ a textual or graphical representation of the dependencies of an object.
The dependency analyzer has been described in~\cite{zack-master}.
\end{itemize}
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 \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 \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
content level terms; presentation level terms.
\subsection{Fully specified terms}
-\label{fully-spec}
+\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.
The mathematical notions (axioms, definitions, theorems) that are stored
Terms may reference other mathematical notions in the library.
One commitment of our project is that the library should be physically
- distributed. The \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 \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.
in Sect.~\ref{sec:libmanagement}.
\subsection{Partially specified terms}
+\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
a sequent. The formers are called \emph{implicit terms} and they occur only
\subsection{Content level terms}
\label{sec:contentintro}
-The language used to communicate proofs and expecially formulae with the
-user does not only needs to be extendible and accomodate the usual mathematical
+The language used to communicate proofs and especially formulae with the
+user does not only needs to be extendible and accommodate the usual mathematical
notation. It must also reflect the comfortable degree of imprecision and
ambiguity that the mathematical language provides.
every ambiguous formula one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
disambiguation algorithm we presented in~\cite{disambiguation} that is
-responsible of building in an efficicent way the set of all ``correct''
+responsible of building in an efficient way the set of all ``correct''
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
-In the last section we have 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
context of the occurrence $x$ it must replace.
The elegant solution we have implemented consists in representing terms
-in a command as function from a context to a partially refined term. The
+in a command as functions from a context to a partially refined term. The
function is obtained by partially applying our disambiguation function to
the content term to be disambiguated. Our solution should be compared with
-the one adopted in the Coq system (where ambiguity is only relative to
-DeBrujin indexes). In Coq variables can be bound either by name or by
-position. This makes more complex every operation over terms (i.e. according
-to our architecture every module that depends on \texttt{cic}). Moreover,
-this solution cannot cope with other forms of ambiguity (as the meaning
-of the $~^2$ exponent in the previous example that depends on the context).
+the one adopted in the Coq system, where ambiguity is only relative to De Brujin
+indexes. In Coq variables can be bound either by name or by position. A term
+occurring in a command has all its variables bound by name to avoid the need of
+a context during disambiguation. Moreover, this makes more complex every
+operation over terms (i.e. according to our architecture every module that
+depends on \texttt{cic}) since the code must deal consistently with both kinds
+of binding. Also, this solution cannot cope with other forms of ambiguity (as
+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}.
against the \texttt{grafite\_parser} \components{}
since they provide an interface to the user. In both cases the formulae
written by the user are parsed using the \texttt{content\_pres} \component{} and
-then disambiguated using the \texttt{cic\_disambiguation} \component.
-However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
-\texttt{tactics} components since \WHELP{} can only execute those ASTs that
-correspond to queries (implemented in the \texttt{whelp} component).
+then disambiguated using the \texttt{cic\_disambiguation} \component. However,
+only \MATITA{} is linked against the \texttt{grafite\_engine} and
+\texttt{tactics} components (summing up to a total of 11'200 lines of code)
+since \WHELP{} can only execute those ASTs that correspond to queries
+(implemented in the \texttt{whelp} component).
The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
providing a rendering service for the documents in the distributed library.
\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{Library Management}
+\section{The interface to the library}
+\label{sec:library}
+
+A proof assistant provides both an interface to interact with its library and
+an \emph{authoring} interface to develop new proofs and theories. According
+to its historical origins, \MATITA{} strives to provide innovative
+functionalities for the interaction with the library. It is more traditional
+in its script based authoring interface.
+
+In the remaining part of the paper we focus on the user view of \MATITA{}.
+This section is devoted to the aspects of the tool that arise from the
+document centric approach to the library. Sect.~\ref{sec:authoring} describes
+the peculiarities of the authoring interface.
+
+The library of \MATITA{} comprises mathematical concepts (theorems,
+axioms, definitions) and notation. The concepts are authored sequentially
+using scripts that are (ordered) sequences of procedural commands.
+However, once they are produced we store them independently in the library.
+The only relation implicitly kept between the notions are the logical,
+acyclic dependencies among them. This way the library forms a global (and
+distributed) hypertext. Several useful operations can be implemented on the
+library only, regardless of the scripts. Examples of such operations
+implemented in \MATITA{} are: searching and browsing (see Sect.~\ref{sec:indexing});
+disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
+automatic proof searching (see Sect.~\ref{sec:automation}).
+
+The key requisite for the previous operations is that the library must
+be fully accessible and in a logically consistent state. To preserve
+consistency, a concept cannot be altered or removed unless the part of the
+library that depends on it is modified accordingly. To allow incremental
+changes and cooperative development, consistent revisions are necessary.
+For instance, to modify a definition, the user could fork a new version
+of the library where the definition is updated and all the concepts that
+used to rely on it are absent. The user is then responsible to restore
+the removed part in the new branch, merging the branch when the library is
+fully restored.
+
+To implement the proposed versioning system on top of a standard one
+it is necessary to implement \emph{invalidation} first. Invalidation
+is the operation that locates and removes from the library all the concepts
+that depend on a given one. As described in Sect.~\ref{sec:libmanagement} removing
+a concept from the library also involves deleting its metadata from the
+database.
+
+For non collaborative development, full versioning can be avoided, but
+invalidation is still required. Since nobody else is relying on the
+user development, the user is free to change and invalidate part of the library
+without branching. Invalidation is still necessary to avoid using a
+concept that is no longer valid.
+So far, in \MATITA{} we address only this non collaborative scenario
+(see Sect.~\ref{sec:libmanagement}). Collaborative development and versioning
+is still under design.
+
+Scripts are not seen as constituents of the library. They are not published
+and indexed, so they cannot be searched or browsed using \HELM{} tools.
+However, they play a central role for the maintenance of the library.
+Indeed, once a notion is invalidated, the only way to restore it is to
+fix the possibly broken script that used to generate it.
+Moreover, during the authoring phase, scripts are a natural way to
+group notions together. They also constitute a less fine grained clustering
+of notions for invalidation.
+
+In the rest of this section we present in more details the functionalities of
+\MATITA{} related to library management and exploitation.
+Sect.~\ref{sec:authoring} is devoted to the description of the peculiarities of
+the \MATITA{} authoring interface.
\subsection{Indexing and searching}
+\label{sec:indexing}
+The Matita system is first of all an interface between the user and
+the mathematical repository. For this reason, it is important to be
+able to search and retrieve mathematical notions in a quick and
+effective way, assuming as little knowledge as possible about the
+library. To this aim, Matita uses a sophisticated indexing mechanism
+for mathemtical items, based on a reach metadata set that has been
+tuned along the European Project IST-2001-33562 MoWGLI. The metadata
+set, and the searching facilites built on top of them - collected
+in the so called \whelp seach engine - have been
+extensively described in \cite{whelp}. Let us just recall here that
+the whelp metadata model is essentially based a single ternary relation
+\REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
+ given position $p$, where the position specify the place of the
+occurrence of $t$ inside $s$ (we currently work with a fixed set of
+positions, discriminating, the hypothesis form the conclusion and
+outermost form innermost occurrences). This approach is extremely
+flexible, since extending the set of positions
+we may improve the granularity and the precision of our indexing technique,
+with no additional architectural impact.
+
+Every time a new mathematical object is created and saved by the user it gets
+indexed, and becomes immediately visible in the library. Several
+interesting and innovative features of Matita described in the following
+sections rely in a direct or indirect way on its metadata system and
+the searching features. Here, we shall just recall some of its most
+direct applications.
+
+A first, very simple but not negligeable feature is the check for duplicates.
+As soon as a new statement is defined, and before proving it,
+the library is searched
+to check that no other equivalent statement has been already proved
+(based on the \whelp{} pattern matching functionality); if this is the case,
+a warning is raised to the user. At present, the notion of equivalence
+adopted by Matita is convertibility, but we may imagine to weaken it
+in the future, covering for instance isomorphisms.
+
+Another usefull \whelp{} operation is {\em hint}; we may invoke this query
+at any moment during the development of a proof, resulting in the list
+of all theorems of the library which can be applied to the current
+goal. In practice, this is mostly used not really to discover what theorems
+can be applied to a given goal, but to actually retrieve a theorem that
+we wish to apply, but whose name we have forgotten.
+In fact, even if \Matita adopts a semi-rigid naming convention for
+statements \ref{naming} that greatly simplifies the effort of recalling
+names, the naming discipline remains one of the most
+annoying aspects of formal developments, and the hint feature provides
+a very friendly solution.
+In the near feature, we expect to extend the {\em hint} operation to
+a {\em rewrite-hint}, resulting in all equational statements that
+can be applied to {\em rewrite} the current goal.
-\subsection{Compilation and cleaning}
-\label{sec:libmanagement}
+\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
+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}.
-%
-%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 pulire 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).\\
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+that 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}
+\label{sec:disambaliases}
+
+Consider the following command to state a theorem over integer numbers:
+
+\begin{grafite}
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+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.
+\MATITA{} asks the user what interpretation he meant. However, to avoid
+posing the same question in case of a future re-execution (e.g. undo/redo),
+the choice must be recorded. Since scripts need to be re-executed after
+invalidation, the choice record must be permanently stored somewhere. The most
+natural place is in the script itself.
+
+In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
+They are mappings, stored in the library, from ambiguity sources
+(identifiers, symbols and literal numbers at the content level) to partially
+specified terms. In case of overloaded sources there exists multiple aliases
+with the same source. It is possible to record \emph{disambiguation
+preferences} to select one of the aliases of an overloaded source.
+
+Preferences can be explicitely given in the script (using the
+misleading \texttt{alias} commands), but
+are also implicitly added when a new concept is introduced (\emph{implicit
+preferences}) or after a sucessfull disambiguation that did not require
+user interaction. Explicit preferences are added automatically by \MATITA{} to
+record the disambiguation choices of the user. For instance, after the
+disambiguation of the command above, the script is altered as follows:
+
+\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}
+
+The ``alias'' command in the example sets the preferred alias for the
+\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
+learned from disambiguation of previous commands grant the coherence of
+the disambiguation in the rest of the script and speed up disambiguation
+reducing the search space.
+
+Disambiguation preferences are included in the lexicon status
+(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
+used in the script, the user can be faced with questions from the disambiguator.
+To reduce the likelyhood of user interactions, we introduced
+the \texttt{include} command. With \texttt{include} it is possible to import
+at once in the current session the set of preferences that was in effect
+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 \OP{<} is likely
+to be the one over natural numbers; sooner or later it will be set to the one
+over integer numbers.
+
+Nothing forbids the set of preferences to become incoherent. For this reason
+the disambiguator cannot always respect the user preferences.
+Consider, for example:
+\begin{grafite}
+theorem Zlt_mono:
+ \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+No refinable partially specified term corresponds to the preferences:
+\OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
+limitation we organized disambiguation in \emph{multiple passes}: when the
+disambiguator fails, disambiguation is tried again with a less strict set of
+preferences.
+
+Several disambiguation parameters can vary among passes. With respect to
+preference handling we implemented three passes. In the first pass, called
+\emph{mono-preferences}, we consider only the aliases corresponding to the
+current preferences. In the second pass, called \emph{multi-preferences}, we
+consider every alias corresponding to a current or past preference. For
+instance, in the example above disambiguation succeeds in the multi-preference
+pass. In the third pass, called \emph{library-preferences}, all aliases
+available in the library are considered.
+
+\TODO{rivedere questo periodo\ldots}
+The rationale behind this choice is trying to respect user preferences in early
+passes that complete quickly in case of failure; later passes are slower but
+have more chances of success.
+
+\subsubsection{Operator instances}
+\label{sec:disambinstances}
+
+Consider now the following theorem:
+\begin{grafite}
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+and assume that there exist in the library aliases for \OP{<} over natural
+numbers and over integer numbers. None of the passes described above is able to
+disambiguate \texttt{lt\_to\_Zlt\_pos\_pos}, no matter how preferences are set.
+This is because the \OP{<} operator occurs twice in the content level term (it
+has two \emph{instances}) and two 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 use a different alias for each of them. Exploiting or not this feature is
+one of the disambiguation pass parameters. A disambiguation pass which exploit
+it is said to be using \emph{fresh instances} (opposed to a \emph{shared
+instances} pass).
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+an alias for one instances does not constraint the choice of the others). For
+this reason we always attempt a fresh instances pass only after attempting a
+non-fresh one.
+
+\paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
+instance-independent. However, implicit preferences obtained as a result of a
+disambiguation pass which uses fresh instances ought to be instance-dependent.
+Informally, the set of preferences that can be satisfied by the disambiguator on
+the theorem above is: ``the first instance of the \OP{<} symbol is over natural
+numbers, while the second is on integer numbers''.
+
+Instance-depend preferences are meaningful only for the term whose
+disambiguation generated it. For this reason we call them \emph{one-shot
+preferences} and \MATITA{} does not use them to disambiguate further terms in
+the script.
+
+\subsubsection{Implicit coercions}
+\label{sec:disambcoercions}
+
+Consider the following theorem about derivation:
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+\end{grafite}
+and assume that in the library there is an alias mapping \OP{\^} to a partially
+specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
+order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
+right hand side of the equality need to be ``injected'' from \texttt{nat} to
+\texttt{R}. The refiner of \MATITA{} supports \emph{implicit coercions} for
+this reason: given as input the above presentation 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 such a coercion has
+been defined in advance).
+
+Coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not 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 we always
+attempt a disambiguation pass which require the refiner not to use the coercions
+before attempting a coercion-enabled pass.
+
+The choice of whether implicit coercions are enabled or not interact with the
+choice about operator instances. Indeed, consider again
+\texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
+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
+coercions, i.e. we always attempt disambiguation passes with fresh instances
+and no implicit coercions before 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
+our experience that choice gives reasonable performance and minimize the need of
+user interaction during the disambiguation.
+
+\begin{table}[ht]
+ \caption{Disambiguation passes sequence.\strut}
+ \label{tab:disambpasses}
+ \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{Preferences}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Mono-preferences & Shared instances & Disabled \\
+ \PASS & Multi-preferences & Shared instances & Disabled \\
+ \PASS & Mono-preferences & Fresh instances & Disabled \\
+ \PASS & Multi-preferences & Fresh instances & Disabled \\
+ \PASS & Mono-preferences & Fresh instances & Enabled \\
+ \PASS & Multi-preferences & Fresh instances & Enabled \\
+ \PASS & Library-preferences & Fresh instances & Enabled
+ \end{tabular}
+ \end{center}
+\end{table}
+
+\subsection{Generation and Invalidation}
+\label{sec:libmanagement}
The aim of this section is to describe the way \MATITA{}
preserves the consistency and the availability of the library
-using the \WHELP{} technology, in response to the user addition or
+using the \WHELP{} technology, in response to the user alteration or
removal 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
+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
disambiguation aliases and the interpretation and notational convention defined,
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
\subsubsection{Batch vs Interactive}
-\MATITA{} includes an interactive graphical interface and a batch
-compiler (\MATITAC). Only the former is intended to be used directly by the
+\MATITA{} includes an interactive authoring interface and a batch
+``compiler'' (\MATITAC). Only the former is intended to be used directly by the
user, the latter is automatically invoked when a
part of the user development is required (for example issuing an
\texttt{include} command) but not yet compiled.
interface inhibit undoing a step which is not the last executed.
\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.
\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_+'';
+and in the conclusion must be separated by the string ``\verb+_to_+'';
\item the identifier may be followed by a numerical suffix, or a
-single or duoble apostrophe.
+single or double apostrophe.
\end{itemize}
Take for instance the theorem
\[ \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,
+has an important beneficial effect on the global organization of the library,
forcing the user to define abstract notions and properties before
using them (and formalizing such use).
expression and the suffix \verb+_to_Prop+. In the above example,
\verb+eqb_to_Prop+ is accepted.
-\section{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
-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} 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
-some of its parameters, helps in keeping the input terse without sacrificing
-expressiveness.
-
-\subsubsection{Disambiguation aliases}
-\label{sec:disambaliases}
-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 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.
-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 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
-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.
-
-\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
-instance-independent. However, aliases obtained as a result of a disambiguation
-pass which uses fresh instances ought to be instance-dependent, that is: to
-ensure a term can be disambiguated in a batch fashion we may need to state that
-an \emph{i}-th instance of a symbol should be mapped to a given partially
-specified term. Instance-depend aliases are meaningful only for the term whose
-disambiguation generated it. For this reason we call them \emph{one-shot
-aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
-script.
-
-\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 coercions, i.e. we always attempt
-disambiguation passes with fresh instances and no implicit coercions before
-attempting passes with implicit coercions.
-
-\subsubsection{Disambiguation passes}
-
-According to the criteria described above in \MATITA{} we choose to perform the
-sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
-our experience that choice implements a good trade off among disambiguation time
-and admitted ambiguity in terms input by users.
-
-\begin{table}[ht]
- \caption{Sequence of disambiguation passes used in \MATITA.\strut}
- \label{tab:disambpasses}
+\section{The authoring interface}
+\label{sec:authoring}
+
+The authoring interface of \MATITA{} is very similar to Proof General. We
+chose not to build the \MATITA{} UI over Proof General for two reasons. First
+of all we wanted to integrate our XML-based rendering technologies, mainly
+\GTKMATHVIEW{}. At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with the future release of Proof General
+based on Eclipse, but is not yet the case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
+as GTK is.
+
+Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
+featuring two windows. The background one is very like to the Proof General
+interface. The main difference is that we use the \GTKMATHVIEW{} widget to
+render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
+advantage of the whole bidimensional mathematical notation.
+
+The foreground window, also implemented around \GTKMATHVIEW, is called
+``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
+in~\cite{remathematization}.
+
+Note that the syntax used in the script view is \TeX-like, however Unicode is
+fully supported so that mathematical glyphs can be input as such.
+
+\begin{figure}[!ht]
\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}
+ \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
+ \caption{\MATITA{} look and feel.\strut}
+ \label{fig:screenshot}
\end{center}
-\end{table}
+\end{figure}
-\subsection{Patterns}
+Since the concepts of script based proof authoring are well-known, the
+remaining part of this section is dedicated to the distinguishing
+features of the \MATITA{} authoring interface.
-\subsubsection{Direct manipulation of terms}
+\subsection{Direct manipulation of terms}
+\label{sec:directmanip}
-While terms are input as \TeX-like formulae in \MATITA, they're converted to a
+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
-\GTKMATHVIEW. This mixed choice~\cite{latexmathml} enables both high-quality
-bidimensional rendering of terms (including the use of fancy layout schemata
-like radicals and matrices~\cite{mathml}) and the use of a concise and
-widespread textual syntax.
-
-\begin{figure}[t]
+\GTKMATHVIEW. As described in~\cite{latexmathml} this mixed choice enables both
+high-quality bidimensional rendering of terms (including the use of fancy
+layout schemata like radicals and matrices) and the use of a
+concise and widespread textual syntax.
+
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enables the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\to n$ since the former denotes an application while the
+latter it not a subterm. Once a meaningful (sub)term has been
+selected actions can be done on it like reductions or tactic
+applications.
+
+\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+ \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
\hspace{0.05\textwidth}
- \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
- \caption{Semantic selection and hyperlinks}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
+ \caption{Semantic selection and hyperlinks.\strut}
\label{fig:directmanip}
\end{center}
\end{figure}
-Keeping pointers from the presentations level terms down to the partially
-specified ones \MATITA{} enable direct manipulation of rendered (sub)terms in
-the form of hyperlinks and semantic selection. \emph{Hyperlinks} have anchors on
-the occurrences of constant and inductive type constructors and point to the
-corresponding definitions in the library. Anchors are available notwithstanding
-the use of user-defined mathematical notation: as can be seen on the right of
-Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols encoding
-complex notations retain all the hyperlinks of constants or constructors used in
-the notation.
-
-\emph{Semantic selection} enable the selection of mixed \MATHML+\BOXML{} markup,
-constraining the selection to markup representing meaningful CIC (sub)terms. In
-the example on the left of Fig.~\ref{fig:directmanip} is thus possible to select
-the subterm $\mathrm{prime}~n$, whereas it would not be possible to select
-$\forall~n:nat$ since the former denotes an application while the latter denotes
-an incomplete $\Pi$-binder. Once a (sub)term has been selected that way actions
-can be done on it like reductions or tactic applications.
-
-In our experience working with direct manipulation of terms is really effective
-and faster than retyping them. Nonetheless we need a way to encode term
-selections in scripts so that they can be batch compiled by \MATITAC. In
-\MATITA{} \emph{patterns} implement that encoding, being patterns the textual
-representations of \GTKMATHVIEW semantic selections.\NOTE{Zack:c'\`e scritto da
-qualche parte che l'utente non li deve necessariamente scrivere a mano, ma che
-pu\`o incollarli? Va scritto.}
+\TODO{referenziarli e spostarli nella parte sulla libreria?}
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-browsing}
+ \hspace{0.02\textwidth}
+ \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
+ \hspace{0.02\textwidth}
+ \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}
+ \caption{Browsing and searching the library.\strut}
+ \label{fig:cicbrowser}
+ \end{center}
+\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
+commands~\cite{proof-by-pointing}.
+Nonetheless we need to record actions and selections in scripts.
+
+In \MATITA{} \emph{patterns} are textual representations of selections.
+Users can select using the GUI and then ask the system to paste the
+corresponding pattern in this script, but more often this process is
+transparent: once an action is performed on a selection, the corresponding
+textual command is computed and inserted in the script.
\subsubsection{Pattern syntax}
-A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
-$\NT{wanted}$.
-The former mocks-up a sequent, discharging unwanted subterms with $?$ and
-selecting the interesting parts with the placeholder $\%$.
-The latter is a term that lives in the context of the placeholders.
-
-The concrete syntax is reported in table \ref{tab:pathsyn}
-\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
+
+Patterns are composed of two parts: \NT{sequent\_path} and
+\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
+$\%$. \NT{wanted} is a term that lives in the context of the
+placeholders.
+
+Textual patterns produced from a graphical selection are made of the
+\NT{sequent\_path} only. Such patterns can represent every selection,
+but are quite verbose. The \NT{wanted} part of the syntax is meant to
+help the users in writing concise and elegant patterns by hand.
+
\begin{table}
- \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
+ \caption{Patterns concrete syntax.\strut}
+ \label{tab:pathsyn}
\hrule
-% \[
-% \begin{array}{@{}rcll@{}}
-% \NT{pattern} &
-% ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
-% \NT{sequent\_path} &
-% ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
-% [~\verb+\vdash+~\NT{multipath}~] & \\
-% \NT{wanted} & ::= & \NT{term} & \\
-% \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
-% \end{array}
-% \]
\[
\begin{array}{@{}rcll@{}}
\NT{pattern} &
\hrule
\end{table}
-\subsubsection{Pattern concepts}
-Patterns mimic the user's selection in two steps. The first one
-selects roots (subterms) of the sequent, using the
-$\NT{sequent\_path}$, while the second
-one searches the $\NT{wanted}$ term starting from these roots. Both are
-optional steps, and by convention the empty pattern selects the whole
-conclusion.
+\subsubsection{Pattern evaluation}
+
+Patterns are evaluated in two phases. The first selects roots
+(subterms) of the sequent, using the $\NT{sequent\_path}$, while the
+second searches the $\NT{wanted}$ term starting from these roots.
+% Both are optional steps, and by convention the empty pattern selects
+% the whole conclusion.
\begin{description}
\item[Phase 1]
$\NT{sequent\_path}$ starting from a visual selection.
\NOTE{Questo ancora non va in matita}
- A $\NT{multipath}$ is a CiC term in which a special constant $\%$
+ A $\NT{multipath}$ is a CIC term in which a special constant $\%$
is allowed.
The roots of discharged subterms are marked with $?$, while $\%$
is used to select roots. The default $\NT{multipath}$, the one that
the source of an arrow and the head of the application that is
found in the arrow target.
- The first phase selects not only terms (roots of subterms) but also
- their context that will be eventually used in the second phase.
+ The first phase not only selects terms (roots of subterms) but
+ determines also their context that will be eventually used in the
+ second phase.
\item[Phase 2]
plays a role only if the $[~\verb+match+~\NT{wanted}~]$
part is specified. From the first phase we have some terms, that we
will see as subterm roots, and their context. For each of these
contexts the $\NT{wanted}$ term is disambiguated in it and the
- corresponding root is searched for a subterm $\alpha$-equivalent to
+ corresponding root is searched for a subterm that can be unified to
$\NT{wanted}$. The result of this search is the selection the
pattern represents.
\end{description}
-\noindent
-Since the first step is equipotent to the composition of the two
-steps, the system uses it to represent each visual selection.
-The second step is only meant for the
-experienced user that writes patterns by hand, since it really
-helps in writing concise patterns as we will see in the
-following examples.
-
\subsubsection{Examples}
-To explain how the first step works let's give an example. Consider
-you want to prove the uniqueness of the identity element $0$ for natural
-sum, and that you can relay on the previously demonstrated left
-injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
-Typing
-\begin{grafite}
-theorem valid_name: \forall n,m. m + n = n \to m = O.
- intros (n m H).
-\end{grafite}
-\noindent
-leads you to the following sequent
+%To explain how the first phase works let us give an example. Consider
+%you want to prove the uniqueness of the identity element $0$ for natural
+%sum, and that you can rely on the previously demonstrated left
+%injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
+%Typing
+%\begin{grafite}
+%theorem valid_name: \forall n,m. m + n = n \to m = O.
+% intros (n m H).
+%\end{grafite}
+%\noindent
+Consider the following sequent
\sequent{
n:nat\\
m:nat\\
m=O
}
\noindent
-where you want to change the right part of the equivalence of the $H$
-hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
+To change the right part of the equivalence of the $H$
+hypothesis with $O + n$ the user selects and pastes it as the pattern
+in the following statement.
\begin{grafite}
change in H:(? ? ? %) with (O + n).
\end{grafite}
\noindent
-This pattern, that is a simple instance of the $\NT{sequent\_path}$
-grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
-and discharges the head of the application and the first two arguments with a
-$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
-but the user can simply select with the mouse the right part of the equivalence
-and left to the system the burden of writing down in the script file the
-corresponding pattern with $?$ and $\%$ in the right place (that is not
-trivial, expecially where implicit arguments are hidden by the notation, like
-the type $nat$ in this example).
-
-Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$
-works too and can be done, by the experienced user, writing directly
-a simpler pattern that uses the second phase.
+To understand the pattern (or produce it by hand) the user should be
+aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
+that the pattern selects only the third argument of $eq$.
+
+The experienced user may also write by hand a concise pattern
+to change at once all the occurrences of $n$ in the hypothesis $H$:
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
\noindent
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
-the second phase searches the wanted $n$ inside it by
-$\alpha$-equivalence. The resulting
-equivalence will be $m+(O+n)=O+n$ since the second phase found two
-occurrences of $n$ in $H$ and the tactic changed both.
+the second phase locates $n$.
-Just for completeness the second pattern is equivalent to the
-following one, that is less readable but uses only the first phase.
+The latter pattern is equivalent to the following one, that the system
+can automatically generate from the selection.
\begin{grafite}
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
\noindent
\subsubsection{Tactics supporting patterns}
+
+\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,
change, fold, unfold, generalize, replace and rewrite.
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with \COQ{}}
-\COQ{} has a two diffrent ways of restricting the application of tactis to
+
+\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.
-The first way is to use this special syntax to specify directly to the
-tactic the occurrnces of a wanted term that should be affected, while
-the second is to prepare the sequent with another tactic called
-pattern and the apply the real tactic. Note that the choice is not
+The first way is to use this special syntax to tell the
+tactic what occurrences of a wanted term should be affected.
+The second is to prepare the sequent with another tactic called
+pattern and then apply the real tactic. Note that the choice is not
left to the user, since some tactics needs the sequent to be prepared
with pattern and do not accept directly this special syntax.
The base idea is that to identify a subterm of the sequent we can
write it and say that we want, for example, the third and the fifth
-occurce of it (counting from left to right). In our previous example,
+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 toright.
+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
-first-order) but normally operate on the arguments.
-This works for some tactics, like rewrite and replace,
-but for example not for change and other tactics that do not relay on
-unification.
+occurrence.
+
+At this point, since Coq unification algorithm is essentially
+first-order, the application of an elimination principle (of the
+form $\forall P.\forall x.(H~x)\to (P~x)$) will unify
+$x$ with \texttt{n} and $P$ with \texttt{(fun n0 : nat => m + n = n0)}.
+
+Since rewriting, replacing and several other tactics boils down to
+the application of the equality elimination principle, the previous
+trick deals the expected behaviour.
The idea behind this way of identifying subterms in not really far
-from the idea behind patterns, but really fails in extending to
+from the idea behind patterns, but fails in extending to
complex notation, since it relays on a mono-dimensional sequent representation.
Real math notation places arguments upside-down (like in indexed sums or
integrations) or even puts them inside a bidimensional matrix.
In these cases using the mouse to select the wanted term is probably the
-only way to tell the system exactly what you want to do.
+more effective way to tell the system what to do.
-One of the goals of \MATITA{} is to use modern publishing techiques, and
+One of the goals of \MATITA{} is to use modern publishing techniques, and
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
-aroud the choice that many proof assistant made, \MATITA{} included, and we
-will not compare the two diffrent approaches. We will describe the common
+around the choice that many proof assistant made, \MATITA{} included, and we
+will not compare the two different approaches. We will describe the common
issues of the tactic-based language approach and how \MATITA{} tries to solve
them.
is executed in a single step, while it obviously performs lot of proof
steps. In the fist example of the previous section the whole branch
over the two goals (respectively the left and right part of the logic
-and) result in a single step of execution. The workaround doesn't work
+and) result in a single step of execution. The workaround does not work
anymore unless you de-structure on the fly the proof, putting some
``\texttt{.}'' where you want the system to stop.\\
\subsubsection{The \MATITA{} approach: Tinycals}
\begin{table}
- \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+ \caption{Concrete syntax of \MATITA{} tacticals.\strut}
+ \label{tab:tacsyn}
\hrule
\[
\begin{array}{@{}rcll@{}}
\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
\end{description}
\section{Standard library}
+\label{sec:stdlib}
\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
can be read, checked and referenced in further developments.
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}
+The library is organized in five main directories: \texttt{logic} (connectives,
+quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
+constructors), \texttt{nat} (natural numbers), \texttt{Z} (integers), \texttt{Q}
+(rationals). The most complex development is \texttt{nat}, organized in 25
+scripts, listed in Tab.~\ref{tab:scripts}.
+
+\begin{table}[ht]
+ \begin{tabular}{lll}
+ \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{Scripts on natural numbers in the standard library.\strut}
+ \label{tab:scripts}
+\end{table}
We do not plan to maintain the library in a centralized way,
-as most of the systems do. On the contary we are currently
+as most of the systems do. On the contrary 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}
+\label{sec:conclusion}
+
+\TODO{conclusioni}
\acknowledgements
We would like to thank all the students that during the past
projects / helm.git / blobdiff