\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{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
-\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}
\newcommand{\MOWGLI}{MoWGLI}
+\newcommand{\MOWGLIIST}{IST-2001-33562}
\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
\newcommand{\OCAML}{OCaml}
\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
+\newcommand{\REWRITEHINT}{\textsc{RewriteHint}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\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]{\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{klunum}
\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.
-\subsection{Historical Perspective}
+\subsection{Historical perspective}
+
The origins of \MATITA{} go back to 1999. At the time we were mostly
interested to develop tools and techniques to enhance the accessibility
via Web of formal libraries of mathematics. Due to its dimension, the
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 \MOWGLIIST{} \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
(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
+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
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.
+On the contrary, the interface to interact with the library is rather
+innovative and directly inspired by the Web interfaces to our Web servers.
-\begin{itemize}
- \item scelta del sistema fondazional.
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
+\MATITA{} is backward compatible with the XML library of proof objects exported
+from \COQ{}, but, in order to test the actual usability of the system, we are
+also developing a new library of basic results from scratch.
\subsection{Relationship with \COQ{}}
However, the analogy essentially stops here and no code is shared by the
two systems.
-In a sense; we like to think of \MATITA{} as the way \COQ{} would
+In a sense, we like to think of \MATITA{} as the way \COQ{} would
look like if entirely rewritten from scratch: just to give an
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
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. 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
\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)}
+ codes (klocs)\strut}
\label{fig:libraries}
\end{center}
\end{figure}
Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
-depend on a restricted set of \components{}.
+depend on a restricted set of \components.
Only the proof assistant \MATITA{} and the \WHELP{} search engine are
applications meant to be used directly by the user. All the other applications
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.
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: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
The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
commands of the \MATITA{} proof assistant. Most of the commands are tactics.
Other commands are used to give definitions and axioms or to state theorems
-and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
+and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA.
It implements the semantics of each command in the grafite AST as a function
from status to status. It implements also an undo function to go back to
previous statuses.
The translation from partially specified terms to content level terms must
discriminate between terms used to represent proofs and terms used to represent
formulae. The firsts are translated to a content level representation of
-proof steps that can easily be rendered in natural language. The representation
+proof steps that can in turn easily be rendered in natural language
+using techniques inspired by~\cite{natural,YANNTHESIS}. The representation
adopted has greatly influenced the OMDoc~\cite{omdoc} proof format that is now
isomorphic to it. Terms that represent formulae are translated to \MATHML{}
Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
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
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 De Brujin
-indexes. In Coq variables can be bound either by name or by position. A term
+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
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.
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}
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{}.
+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.
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}).
+distributed) hypertext.
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-browsing}
+ \hspace{0.05\textwidth}
+ \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-query}
+ \caption{Browsing and searching the library\strut}
+ \label{fig:cicbrowser1}
+ \end{center}
+\end{figure}
+
+\begin{figure}[!ht]
+ \begin{center}
+ \includegraphics[width=0.70\textwidth]{pics/cicbrowser-screenshot-con}
+ \caption[Natural language rendering]{Natural language rendering of a theorem
+ from the library\strut}
+ \label{fig:cicbrowser2}
+ \end{center}
+\end{figure}
+
+Several useful operations can be implemented on the library only,
+regardless of the scripts. For instance, searching and browsing is
+implemented by the ``cicBrowser'' window available from the \MATITA{}
+GUI. Using it, the hierarchical structure of the library can be
+explored (on the left of Fig.~\ref{fig:cicbrowser1}), the natural
+language rendering of proofs can be inspected
+(Fig.~\ref{fig:cicbrowser2}), and content based searches on the
+library can be performed (on the right of Fig.~\ref{fig:cicbrowser1}).
+Available content based searches are described in
+Sect.~\ref{sec:indexing}. Other examples of library operations are
+disambiguation of content level terms (see
+Sect.~\ref{sec:disambiguation}) and 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
\subsection{Indexing and searching}
\label{sec:indexing}
+The \MATITA{} system is first of all an interface between the user and
+the mathematical library. For this reason, it is important to be
+able to search and retrieve mathematical concepts 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 mathematical concepts, based on a rich metadata set that has been
+tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
+set, and the searching facilites built on top of them --- collected
+in the so called \WHELP{} search 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 from 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 concept 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 search 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 theorem is stated, just before starting its proof,
+the library is searched
+to check that no other equivalent statement has been already proved
+(based on the pattern matching functionality of \WHELP); 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 useful \WHELP{} operation is \HINT; we may invoke this query
+at any moment during the authoring 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 (see Sect.~\ref{sec:naming}) that greatly simplifies the effort
+of recalling names, the naming discipline remains one of the most
+annoying aspects of formal developments, and \HINT{} provides
+a very friendly solution.
+In the near feature, we expect to extend the \HINT{} operation to
+a \REWRITEHINT, resulting in all equational statements that
+can be applied to rewrite the current goal.
+
\subsection{Disambiguation}
\label{sec:disambiguation}
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
+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}
-Let us 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 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):
+Consider the following command to state a theorem over integer numbers:
\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 implicitly 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
-chosen):
+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'".
\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 explicitly 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:
-
+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 lt_mono: \forall x, y, k. x < y \to x < y + k.
+theorem Zlt_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 chose to attempt \emph{multiple disambiguation passes}. A
-first pass attempts to disambiguate using the last available disambiguation
-aliases (\emph{mono aliases} pass); in case of failure the next pass tries
-disambiguation again 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.
+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.
+
+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}
-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
-we can read it in the \MATITA{} standard library) is:
-
+Consider now the following theorem:
\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}.
+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 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
+an alias for one instance 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 respected 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-dependent preferences are meaningful only for the term whose
disambiguation generated it. For this reason we call them \emph{one-shot
-aliases} and \MATITA{} does not use it to disambiguate further terms down in the
-script.
+preferences} and \MATITA{} does not use them to disambiguate further terms in
+the script.
\subsubsection{Implicit coercions}
+\label{sec:disambcoercions}
-Let us now consider a theorem about derivation:
-
+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 suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
-interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematicians 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
+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 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.
+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), 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.
+Motivated by this and similar examples 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
+According to the criteria described above, in \MATITA{} we perform the
+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{Sequence of disambiguation passes used in \MATITA.\strut}
+ \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{Disambiguation aliases}}
+ & \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 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
+ \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}
+\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 alteration or
-removal of mathematical objects.
-
-As already sketched in Sect.~\ref{sec:fullyspec} 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,
-while the latter is used to store all the metadata needed by
-\WHELP{}.
-
-While the consistency of the data store in the two media has
-nothing to do with the nature of
-the content of the library and is thus uninteresting (but really
-tedious to implement and keep bug-free), there is a deeper
-notion of mathematical consistency we need to provide. Each object
-must reference only defined object (i.e. each proof must use only
-already proved theorems).
-
-We will focus on how \MATITA{} ensures the interesting kind
-of consistency during the formalization of a mathematical theory,
+%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 alteration or
+%removal of mathematical objects.
+%
+%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,
+%while the latter is used to store all the metadata needed by
+%\WHELP.
+%
+%While the consistency of the data store in the two media has
+%nothing to do with the nature of
+%the content of the library and is thus uninteresting (but really
+%tedious to implement and keep bug-free), there is a deeper
+%notion of mathematical consistency we need to provide. Each object
+%must reference only defined object (i.e. each proof must use only
+%already proved theorems).
+
+In this section we will focus on how \MATITA{} ensures the library
+consistency during the formalization of a mathematical theory,
giving the user the freedom of adding, removing, modifying objects
without loosing the feeling of an always visible and browsable
library.
-\subsubsection{Compilation}
+\subsubsection{Invalidation}
+
+Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
+
+The first one is the calculation of all the concepts that recursively
+depend on the ones we are invalidating. The calculation of the
+reverse dependencies can be computed using the relational database
+that stores metadata.
+This technique is the same used by the \emph{Dependency Analyzer}
+and is described in~\cite{zack-master}.
+
+The second phase is the removal of all the results of the generation,
+metadata included.
-The typechecker component guarantees that if an object is well typed
-it depends only on well typed objects available in the library,
-that is exactly what we need to be sure that the logic consistency of
-the library is preserved. We have only to find the right order of
-compilation of the scripts that compose the user development.
+\subsubsection{Regeneration}
+
+%The typechecker component guarantees that if an object is well typed
+%it depends only on well typed objects available in the library,
+%that is exactly what we need to be sure that the logic consistency of
+%the library is preserved.
+
+To regenerate an invalidated part of the library \MATITA{} re-executes
+the script files that produced the invalidated concepts. The main
+problem is to find a suitable order of execution of the scripts.
For this purpose we provide a tool called \MATITADEP{}
-that takes in input the list of files that compose the development and
+that takes in input the list of scripts that compose the development and
outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
The user is not asked to run \MATITADEP{} by hand, but
simply to tell \MATITA{} the root directory of his development (where all
-script files can be found) and \MATITA{} will handle all the compilation
+script files can be found) and \MATITA{} will handle all the generation
related tasks, including dependencies calculation.
-To compute dependencies it is enough to look at the script files for
-inclusions of other parts of the development or for explicit
-references to other objects (i.e. with explicit aliases, see
-\ref{sec:disambaliases}).
-
-The output of the compilation is immediately available to the user
-trough the \WHELP{} technology, since all metadata are stored in a
-user-specific area of the database where the search engine has read
-access, and all the automated tactics that operates on the whole
-library, like \AUTO, have full visibility of the newly defined objects.
-
-Compilation is rather simple, and the only tricky case is when we want
-to compile again the same script, maybe after the removal of a
-theorem. Here the policy is simple: clean the output before recompiling.
-As we will see in the next section cleaning will ensure that
-there will be no theorems in the development that depends on the
-removed items.
-
-\subsubsection{Cleaning}
-
-With the term ``cleaning'' we mean the process of removing all the
-results of an object compilation. In order to keep the consistency of
-the library, cleaning an object requires the (recursive) cleaning
-of all the objects that depend on it (\emph{reverse dependencies}).
-
-The calculation of the reverse dependencies can be computed in two
-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
-database.
-The latter is a fall-back in case the database is not
-available.\footnote{Due to the complex deployment of a large piece of
-software like a database, it is a common practice for the \HELM{} team
-to use a shared remote database, that may be unavailable if the user
-workstation lacks network connectivity.} This facility has to be
-intended only as a fall-back, since the queries of the \WHELP{}
-technology depend require a working database.
+To compute dependencies it is enough to look at the script files for
+disambiguation preferences declared or imported from other scripts
+(see \ref{sec:disambaliases}).
-Cleaning guarantees that if an object is removed there are no dandling
-references to it, and that the part of the library still compiled is
-consistent. Since cleaning involves the removal of all the results of
-the compilation, metadata included, the library browsable trough the
-\WHELP{} technology is always kept up to date.
+Regenerating the content of a modified script file involves the preliminary
+invalidation of all its old content.
\subsubsection{Batch vs Interactive}
\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.
-
-While they share the same engine for compilation and cleaning, they
-provide different granularity. The batch compiler is only able to
-compile a whole script and similarly to clean only a whole script
-(together with all the other scripts that rely on an object defined in
-it). The interactive interface is able to execute single steps of
-compilation, that may include the definition of an object, and
-similarly to undo single steps. Note that in the latter case there is
-no risk of introducing dangling references since the \MATITA{} user
-interface inhibit undoing a step which is not the last executed.
+``compiler'' (\MATITAC).
+
+Only the former is intended to be used directly by the
+user, the latter is automatically invoked by \MATITA{}
+to try to regenerate parts of the library previously invalidated.
+
+While they share the same engine for generation and invalidation, they
+provide different granularity. \MATITAC{} is only able to reexecute a
+whole script and similarly to invalidate the whole content of a script
+(together with all the other scripts that rely on an concept defined
+in it).
\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.
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
+\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
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}.
+advantage of the whole bidimensional mathematical notation. The foreground
+window is an instance of the cicBrowser used to render the proof being
+developed.
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}
\includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
- \caption{\MATITA{} look and feel}
+ \caption{Authoring interface\strut}
\label{fig:screenshot}
\end{center}
\end{figure}
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
\includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
\hspace{0.05\textwidth}
\raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
- \caption{Semantic selection and hyperlinks}
+ \caption[Semantic selection and hyperlinks]{Semantic selection (on the left)
+ and hyperlinks (on the right)\strut}
\label{fig:directmanip}
\end{center}
\end{figure}
-\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}
- \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
\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
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@{}}
%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\\
H: m + n = n}{
m=O
}
-\noindent
+
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
+
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$.
\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 locates $n$.
\begin{grafite}
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
-\noindent
\subsubsection{Tactics supporting patterns}
-MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
-INTERFACCIA OCMUNE PER LE TATTICHE
+
+\TODO{Grazie ai pattern, rispetto a Coq noi abbiamo per esempio la possibilita' di fare riduzioni profonde!!!}
+
+\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
-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 techniques, and
adopting a method for restricting tactics application domain that discourages
using heavy math notation, would definitively be a bad choice.
-
\subsection{Tacticals}
-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
-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.
-
-\subsubsection{Tacticals overview}
-
-Tacticals first appeared in LCF and can be seen as programming
-constructs, like looping, branching, error recovery or sequential composition.
-The following simple example shows three tacticals in action
-\begin{grafite}
-theorem trivial:
- \forall A,B:Prop.
- A = B \to ((A \to B) \land (B \to A)).
- intros (A B H).
- split; intro;
- [ rewrite < H. assumption.
- | rewrite > H. assumption.
- ]
-qed.
-\end{grafite}
+\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
+%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.
+
+The procedural proof language implemented in \MATITA{} is pretty standard,
+with a notable exception for tacticals.
+
+%\subsubsection{Tacticals overview}
-The first is ``\texttt{;}'' that combines the tactic \texttt{split}
-with \texttt{intro}, applying the latter to each goal opened by the
-former. Then we have ``\texttt{[}'' that branches on the goals (here
-we have two goals, the two sides of the logic and).
-The first goal $B$ (with $A$ in the context)
-is proved by the first sequence of tactics
-\texttt{rewrite} and \texttt{assumption}. Then we move to the second
-goal with the separator ``\texttt{|}''. The last tactical we see here
-is ``\texttt{.}'' that is a sequential composition that selects the
-first goal opened for the following tactic (instead of applying it to
-them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
-not considered a tactical, but a sentence terminator (i.e. the
-delimiter of commands the proof assistant executes).
-
-Giving serious examples here is rather difficult, since they are hard
-to read without the interactive tool. To help the reader in
-understanding the following considerations we just give few common
-usage examples without a proof context.
+Tacticals first appeared in LCF as higher order tactics. They can be
+seen as control flow constructs, like looping, branching, error
+recovery or sequential composition.
+
+
+The following simple example
+shows a Coq script made of four dot-terminated commands
\begin{grafite}
- elim z; try assumption; [ ... | ... ].
- elim z; first [ assumption | reflexivity | id ].
+Theorem trivial:
+ forall A B:Prop,
+ A = B -> ((A -> B) /\ (B -> A)).
+ intros [A B H].
+ split; intro;
+ [ rewrite < H; assumption
+ | rewrite > H; assumption
+ ].
+Qed.
\end{grafite}
-The first example goes by induction on a term \texttt{z} and applies
-the tactic \texttt{assumption} to each opened goal eventually recovering if
-\texttt{assumption} fails. Here we are asking the system to close all
-trivial cases and then we branch on the remaining with ``\texttt{[}''.
-The second example goes again by induction on \texttt{z} and tries to
-close each opened goal first with \texttt{assumption}, if it fails it
-tries \texttt{reflexivity} and finally \texttt{id}
-that is the tactic that leaves the goal untouched without failing.
-
-Note that in the common implementation of tacticals both lines are
-compositions of tacticals and in particular they are a single
-statement (i.e. derived from the same non terminal entry of the
-grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
-this is not true, since each atomic tactic or punctuation is considered
-a single statement.
+The third command is an application of the sequencing tactical
+``$\ldots$\texttt{;}$\ldots$'', that combines the tactic
+\texttt{split} with the application of the branching tactical
+``$\ldots$\texttt{;[}$\ldots$\texttt{|}$\ldots$\texttt{|}$\ldots$\texttt{]}''
+to other tactics and tacticals.
+
+The usual implementation of tacticals executes them atomically as any
+other command. In \MATITA{} thi is not true since each punctuation is
+executed as a single command.
+
+%The latter is applied to all the goals opened by \texttt{split}
+%
+%(here we have two goals, the two sides of the logic and). The first
+%goal $B$ (with $A$ in the context) is proved by the first sequence of
+%tactics \texttt{rewrite} and \texttt{assumption}. Then we move to the
+%second goal with the separator ``\texttt{|}''.
+%
+%Giving serious examples here is rather difficult, since they are hard
+%to read without the interactive tool. To help the reader in
+%understanding the following considerations we just give few common
+%usage examples without a proof context.
+%
+%\begin{grafite}
+% elim z; try assumption; [ ... | ... ].
+% elim z; first [ assumption | reflexivity | id ].
+%\end{grafite}
+%
+%The first example goes by induction on a term \texttt{z} and applies
+%the tactic \texttt{assumption} to each opened goal eventually recovering if
+%\texttt{assumption} fails. Here we are asking the system to close all
+%trivial cases and then we branch on the remaining with ``\texttt{[}''.
+%The second example goes again by induction on \texttt{z} and tries to
+%close each opened goal first with \texttt{assumption}, if it fails it
+%tries \texttt{reflexivity} and finally \texttt{id}
+%that is the tactic that leaves the goal untouched without failing.
+%
+%Note that in the common implementation of tacticals both lines are
+%compositions of tacticals and in particular they are a single
+%statement (i.e. derived from the same non terminal entry of the
+%grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
+%this is not true, since each atomic tactic or punctuation is considered
+%a single statement.
\subsubsection{Common issues of tactic(als)-based proof languages}
We will examine the two main problems of tactic(als)-based proof script:
maintainability and readability.
-Huge libraries of formal mathematics have been developed, and backward
-compatibility is a really time consuming task. \\
-A real-life example in the history of \MATITA{} was the reordering of
-goals opened by a tactic application. We noticed that some tactics
-were not opening goals in the expected order. In particular the
-\texttt{elim} tactic on a term of an inductive type with constructors
-$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
-\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
-but some theorems about integers were there. The inductive type of
-$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
-induction proofs on this type where written without tacticals and,
-obviously, considering the three induction cases in the wrong order.
-Fixing the behavior of the tactic broke the library and two days of
-work were needed to make it compile again. The whole time was spent in
-finding the list of tactics used to prove the third induction case and
-swap it with the list of tactics used to prove the second case. If
-the proofs was structured with the branch tactical this task could
-have been done automatically.
-
-From this experience we learned that the use of tacticals for
-structuring proofs gives some help but may have some drawbacks in
-proof script readability. We must highlight that proof scripts
-readability is poor by itself, but in conjunction with tacticals it
-can be nearly impossible. The main cause is the fact that in proof
-scripts there is no trace of what you are working on. It is not rare
-for two different theorems to have the same proof script (while the
-proof is completely different).\\
-Bad readability is not a big deal for the user while he is
-constructing the proof, but is considerably a problem when he tries to
-reread what he did or when he shows his work to someone else. The
-workaround commonly used to read a script is to execute it again
-step-by-step, so that you can see the proof goal changing and you can
-follow the proof steps. This works fine until you reach a tactical. A
-compound statement, made by some basic tactics glued with tacticals,
-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 does not work
-anymore unless you de-structure on the fly the proof, putting some
-``\texttt{.}'' where you want the system to stop.\\
-
-Now we can understand the tradeoff between script readability and
-proof structuring with tacticals. Using tacticals helps in maintaining
-scripts, but makes it really hard to read them again, cause of the way
-they are executed.
-
-\MATITA{} uses a language of tactics and tacticals, but tries to avoid
-this tradeoff, alluring the user to write structured proof without
-making it impossible to read them again.
+%Huge libraries of formal mathematics have been developed, and backward
+%compatibility is a really time consuming task. \\
+%A real-life example in the history of \MATITA{} was the reordering of
+%goals opened by a tactic application. We noticed that some tactics
+%were not opening goals in the expected order. In particular the
+%\texttt{elim} tactic on a term of an inductive type with constructors
+%$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
+%\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
+%but some theorems about integers were there. The inductive type of
+%$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
+%induction proofs on this type where written without tacticals and,
+%obviously, considering the three induction cases in the wrong order.
+%Fixing the behavior of the tactic broke the library and two days of
+%work were needed to make it compile again. The whole time was spent in
+%finding the list of tactics used to prove the third induction case and
+%swap it with the list of tactics used to prove the second case. If
+%the proofs was structured with the branch tactical this task could
+%have been done automatically.
+%
+%From this experience we learned that the use of tacticals for
+%structuring proofs gives some help but may have some drawbacks in
+%proof script readability.
+
+Tacticals are not only used to make scripts shorter by factoring out
+common cases and repeating commands. They are a primary way of making
+scripts more mainteable. Moreover, they also have the well-known
+role of structuring the proof.
+
+However, authoring a proof structured with tacticals is annoying.
+Consider for example a proof by induction, and imagine you
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
+immediately structure the proof or postpone the structuring.
+If you decide for the former you have to apply the branching tactical and write
+at once tactics for all the cases. Since the user does not even know the
+generated goals yet, she can only replace all the cases with the identity
+tactic and execute the command, just to receive feedback on the first
+goal. Then she has to go one step back to replace the first identity
+tactic with the wanted one and repeat the process until all the
+branches are closed.
+
+One could imagine that a structured script is simpler to understand.
+This is not the case.
+A proof script, being not declarative, is not meant to be read.
+However, the user has the need of explaining it to others.
+This is achieved by interactively re-playing the script to show each
+intermediate proof status. Tacticals make this operation uncomfortable.
+Indeed, a tactical is executed atomically, while it is obvious that it
+performs lot of smaller steps we are interested in.
+To show the intermediate steps, the proof must be de-structured on the
+fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where
+possible.\\
+
+%Proof scripts
+%readability is poor by itself, but in conjunction with tacticals it
+%can be nearly impossible. The main cause is the fact that in proof
+%scripts there is no trace of what you are working on. It is not rare
+%for two different theorems to have the same proof script.\\
+%Bad readability is not a big deal for the user while he is
+%constructing the proof, but is considerably a problem when he tries to
+%reread what he did or when he shows his work to someone else. The
+%workaround commonly used to read a script is to execute it again
+%step-by-step, so that you can see the proof goal changing and you can
+%follow the proof steps. This works fine until you reach a tactical. A
+%compound statement, made by some basic tactics glued with tacticals,
+%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 does not work
+%anymore unless you de-structure on the fly the proof, putting some
+%``\texttt{.}'' where you want the system to stop.\\
+
+%Now we can understand the tradeoff between script readability and
+%proof structuring with tacticals. Using tacticals helps in maintaining
+%scripts, but makes it really hard to read them again, cause of the way
+%they are executed.
+
+\MATITA{} has a peculiar tacticals implementation that provides the
+same benefits as classical tacticals, while not burdening the user
+during proof authoring and re-playing.
+
+%\MATITA{} uses a language of tactics and tacticals, but tries to avoid
+%this tradeoff, alluring the user to write structured proof without
+%making it impossible to read them again.
\subsubsection{The \MATITA{} approach: Tinycals}
\begin{table}
- \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+ \caption{Concrete syntax of 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
+This is essential for the base idea behind \MATITA{} tacticals: step-by-step
execution.
The low-level tacticals implementation of \MATITA{} allows a step-by-step
execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
-not executed as an atomic operation. This has two major benefits for the user,
-even being a so simple idea:
-\begin{description}
-\item[Proof structuring]
- is much easier. Consider for example a proof by induction, and imagine you
- are using classical tacticals in one of the state of the
- art graphical interfaces for proof assistant like Proof General or \COQIDE.
- After applying the induction principle you have to choose: structure
- the proof or not. If you decide for the former you have to branch with
- ``\texttt{[}'' and write tactics for all the cases separated by
- ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
- You can replace most of the cases by the identity tactic just to
- concentrate only on the first goal, but you will have to go one step back and
- one further every time you add something inside the tactical. Again this is
- caused by the one step execution of tacticals and by the fact that to modify
- the already executed script you have to undo one step.
- And if you are board of doing so, you will finish in giving up structuring
- the proof and write a plain list of tactics.\\
- With step-by-step tacticals you can apply the induction principle, and just
- open the branching tactical ``\texttt{[}''. Then you can interact with the
- system reaching a proof of the first case, without having to specify any
- tactic for the other goals. When you have proved all the induction cases, you
- close the branching tactical with ``\texttt{]}'' and you are done with a
- structured proof. \\
- While \MATITA{} tacticals help in structuring proofs they allow you to
- choose the amount of structure you want. There are no constraints imposed by
- the system, and if the user wants he can even write completely plain proofs.
+not executed as an atomic operation. This has major benefits for the
+user during proof structuring and re-playing.
+
+For instance, reconsider the previous example of a proof by induction.
+With step-by-step tacticals the user can apply the induction principle, and just
+open the branching tactical ``\texttt{[}''. Then she can interact with the
+system until the proof of the first case is terminated. After that
+``\texttt{|}'' is used to move to the next goal, until all goals are
+closed. After the last goal, the user closes the branching tactical with
+``\texttt{]}'' and is done with a structured proof. \\
+While \MATITA{} tacticals help in structuring proofs they allow you to
+choose the amount of structure you want. There are no constraints imposed by
+the system, and if the user wants he can even write completely plain proofs.
-\item[Rereading]
- is possible. Going on step by step shows exactly what is going on. Consider
- again a proof by induction, that starts applying the induction principle and
- suddenly branches with a ``\texttt{[}''. This clearly separates all the
- induction cases, but if the square brackets content is executed in one single
- step you completely loose the possibility of rereading it and you have to
- temporary remove the branching tactical to execute in a satisfying way the
- branches. Again, executing step-by-step is the way you would like to review
- the demonstration. Remember that understanding the proof from the script is
- not easy, and only the execution of tactics (and the resulting transformed
- goal) gives you the feeling of what is going on.
-\end{description}
+Re-playing a proof is also made simpler. There is no longer any need
+to destructure the proof on the fly since \MATITA{} executes each
+tactical not atomically.
+
+%\item[Rereading]
+% is possible. Going on step by step shows exactly what is going on. Consider
+% again a proof by induction, that starts applying the induction principle and
+% suddenly branches with a ``\texttt{[}''. This clearly separates all the
+% induction cases, but if the square brackets content is executed in one single
+% step you completely loose the possibility of rereading it and you have to
+% temporary remove the branching tactical to execute in a satisfying way the
+% branches. Again, executing step-by-step is the way you would like to review
+% the demonstration. Remember that understanding the proof from the script is
+% not easy, and only the execution of tactics (and the resulting transformed
+% goal) gives you the feeling of what is going on.
+%\end{description}
\section{Standard library}
\label{sec:stdlib}
\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}
+ \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,
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
-five years collaborated in the \HELM{} project and contributed to
+We would like to thank all the people that during the past
+7 years collaborated in the \HELM{} project and contributed to
the development of \MATITA{}, and in particular
M.~Galat\`a, A.~Griggio, F.~Guidi, P.~Di~Lena, L.~Padovani, I.~Schena, M.~Selmi,
and V.~Tamburrelli.
\theendnotes
+\TODO{rivedere bibliografia, \'e un po' povera}
+
+\TODO{aggiungere entry per le coercion implicite}
+
\bibliography{matita}
\end{document}
-
projects / helm.git / blobdiff