-\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]{\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
+
+\MATITA{} is the Proof Assistant under development by the \HELM{}
+team~\cite{mkm-helm} at the University of Bologna, under the direction of
+Prof.~Asperti. The paper describes the overall architecture of
the system, focusing on its most distinctive and innovative
features.
have been also conducted with other systems, and notably
with \NUPRL~\cite{nuprl-book}.
The work, mostly performed in the framework of the recently concluded
-European project IST-33562 \MOWGLI{}~\cite{pechino}, mainly consisted in the
+European project IST-33562 \MOWGLI~\cite{pechino}, mainly consisted in the
following steps:
\begin{itemize}
\item exporting the information from the internal representation of
\COQ{} to a system and platform independent format. Since XML was at the
time an emerging standard, we naturally adopted this technology, fostering
-a content-centric architecture\cite{content-centric} where the documents
+a content-centric architecture~\cite{content-centric} where the documents
of the library were the the main components around which everything else
has to be build;
\item developing indexing and searching techniques supporting semantic
tools and software components:
\begin{itemize}
\item XML specifications for the Calculus of Inductive Constructions,
-with components for parsing and saving mathematical objects in such a format
-\cite{exportation-module};
+with components for parsing and saving mathematical objects in such a
+format~\cite{exportation-module};
\item metadata specifications with components for indexing and querying the
XML knowledge base;
\item a proof checker library (i.e. the {\em kernel} of a proof assistant),
logically relevant content;
\item a sophisticated parser (used by the search engine), able to deal
with potentially ambiguous and incomplete information, typical of the
-mathematical notation \cite{disambiguation};
+mathematical notation~\cite{disambiguation};
\item a {\em refiner} library, i.e. a type inference system, based on
partially specified terms, used by the disambiguating parser;
\item complex transformation algorithms for proof rendering in natural
-language \cite{remathematization};
+language~\cite{remathematization};
\item an innovative, \MATHML-compliant rendering widget for the GTK
-graphical environment\cite{padovani}, supporting
+graphical environment~\cite{padovani}, supporting
high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
meaningful rendering expressions, and to paste the respective content into
have either adopted or cloned Proof General as their main user interface.
The authoring interface of \MATITA{} is a clone of the Proof General interface.
+\TODO{item che seguono:}
\begin{itemize}
- \item scelta del sistema fondazional.
\item sistema indipendente (da \COQ)
\item compatibilit\`a con sistemi legacy
\end{itemize}
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
\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.9\textwidth,height=0.8\textheight]{libraries-clusters}
+ \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}
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
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
-In Sect.~\ref{sec:partspec} the last section we described the semantics of a
-command as a
+In Sect.~\ref{sec:partiallyintro} the last section we described the semantics of
+a command as a
function from status to status. We also suggested that the formulae in a
command are encoded as partially specified terms. However, consider the
command ``\texttt{replace} $x$ \texttt{with} $y^2$''. Until the occurrence
the context dependent meaning of the exponent in the previous example).
\subsection{Presentation level terms}
+\label{sec:presentationintro}
Content level terms are a sort of abstract syntax trees for mathematical
formulae and proofs. The concrete syntax given to these abstract trees
presentation
level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
\GTKMATHVIEW{}
-widget developed by Luca Padovani \cite{padovani}. The widget is
+widget developed by Luca Padovani~\cite{padovani}. The widget is
particularly interesting since it allows to implement \emph{semantic
selection}.
\GETTER{} obtaining a document with fully specified terms. Then it translates
it to the presentation level passing through the content level. Finally
it returns the result document to be rendered by the user's
-browser.\footnote{\TODO{manca la passata verso HTML}}
-
+browser.\NOTE{\TODO{manca la passata verso HTML}}
The \components{} not yet described (\texttt{extlib}, \texttt{xml},
\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
%In particular, the \texttt{xml} \component{} is used to easily represent,
%parse and pretty-print XML files.
-
\section{The interface to the library}
\label{sec:library}
\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{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.
+
+\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}
-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 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
-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, 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
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}
\label{sec:libmanagement}
using the \WHELP{} technology, in response to the user alteration or
removal of mathematical objects.
-As already sketched in Sect.~\ref{sec:fullyspec} what we generate
+As already sketched in Sect.~\ref{sec:fullyintro} what we generate
from a script is split among two storage media, a
classical filesystem and a relational database. The former is used to
store the XML encoding of the objects defined in the script, the
ways, using the relational database or using a simpler set of metadata
that \MATITA{} saves in the filesystem as a result of compilation. The
former technique is the same used by the \emph{Dependency Analyzer}
-described in \cite{zack-master} and really depends on a relational
+described in~\cite{zack-master} and really depends on a relational
database.
The latter is a fall-back in case the database is not
\subsection{Automation}
\label{sec:automation}
+\TODO{sezione sull'automazione}
+
\subsection{Naming convention}
+\label{sec:naming}
+
A minor but not entirely negligible aspect of \MATITA{} is that of
adopting a (semi)-rigid naming convention for identifiers, derived by
our studies about metadata for statements.
``cicBrowser''. It is used to browse the library, including the proof being
developed, and enable content based search over it. Proofs are rendered in
natural language, automatically generated from the low-level lambda-terms,
-using techniques inspired by \cite{natural,YANNTHESIS} and already described
+using techniques inspired by~\cite{natural,YANNTHESIS} and already described
in~\cite{remathematization}.
Note that the syntax used in the script view is \TeX-like, however Unicode is
\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.95\textwidth]{matita-screenshot}
- \caption{\MATITA{} look and feel}
+ \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
+ \caption{\MATITA{} look and feel.\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
selected actions can be done on it like reductions or tactic
applications.
-\begin{figure}[t]
+\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}
+\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
\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@{}}
\noindent
\subsubsection{Tactics supporting patterns}
-MERGIARE CON IL SUCCESSIVO FACENDO NOTARE CHE I PATTERNS SONO UNA
-INTERFACCIA OCMUNE PER LE TATTICHE
+
+\TODO{mergiare con il successivo facendo notare che i patterns sono una
+interfaccia comune per le tattiche}
In \MATITA{} all the tactics that can be restricted to subterm of the working
sequent accept the pattern syntax. In particular these tactics are: simplify,
con una pattern\_of(select(pattern))}
\subsubsection{Comparison with \COQ{}}
+
\COQ{} has two different ways of restricting the application of tactics to
subterms of the sequent, both relaying on the same special syntax to identify
a term occurrence.
write it and say that we want, for example, the third and the fifth
occurrences of it (counting from left to right). In our previous example,
to change only the left part of the equivalence, the correct command
-is
+is:
+
\begin{grafite}
change n at 2 in H with (O + n)
\end{grafite}
-\noindent
+
meaning that in the hypothesis $H$ the $n$ we want to change is the
second we encounter proceeding from left to right.
The tactic pattern computes a
$\beta$-expansion of a part of the sequent with respect to some
occurrences of the given term. In the previous example the following
-command
+command:
\begin{grafite}
pattern n at 2 in H
\end{grafite}
-\noindent
-would have resulted in this sequent
+
+would have resulted in this sequent:
+
\begin{grafite}
n : nat
m : nat
============================
m = 0
\end{grafite}
-\noindent
+
where $H$ is $\beta$-expanded over the second $n$
-occurrence. This is a trick to make the unification algorithm ignore
-the head of the application (since the unification is essentially
-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}
+\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
\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
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 contrary we are currently
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