-\documentclass[draft]{kluwer}
+\documentclass[]{kluwer}
\usepackage{color}
\usepackage{graphicx}
% \usepackage{amssymb,amsmath}
\newcommand{\components}{components}
\newcommand{\AUTO}{\textsc{Auto}}
+\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
\newcommand{\COQIDE}{CoqIde}
\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
+\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
\newcommand{\IN}{\ensuremath{\dN}}
\newcommand{\LIBXSLT}{LibXSLT}
\newcommand{\LOCATE}{\textsc{Locate}}
\newcommand{\MATCH}{\textsc{Match}}
+\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
-%{\end{SaveVerbatim}\setlength{\fboxrule}{.5mm}\setlength{\fboxsep}{2mm}%
\newenvironment{grafite}{\VerbatimEnvironment
\begin{SaveVerbatim}{boxtmp}}%
{\end{SaveVerbatim}\setlength{\fboxsep}{3mm}%
{}
\newcommand{\ASSIGNEDTO}[1]{\textbf{Assigned to:} #1}
\newcommand{\FILE}[1]{\texttt{#1}}
-% \newcommand{\NOTE}[1]{\ifodd \arabic{page} \else \hspace{-2cm}\fi\ednote{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{foo}}
+\newcommand{\NOTE}[1]{\ednote{#1}{}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\newcounter{pass}
%search engine, described in~\cite{whelp};
\item developing languages and tools for a high-quality notational
rendering of mathematical information\footnote{We have been
-active in the MathML Working group since 1999.};
+active in the \MATHML{} Working group since 1999.};
%and developed inside
-%\HELM{} a MathML-compliant widget for the GTK graphical environment
+%\HELM{} a \MATHML-compliant widget for the GTK graphical environment
%which can be integrated in any application.
\end{itemize}
means of a Web interface that orchestrates the Web services.
The Web services and the other tools have been implemented as front-ends
-to a set of software libraries, collectively called the \HELM{} libraries.
+to a set of software components, collectively called the \HELM{} components.
At the end of the \MOWGLI{} project we already disposed of the following
-tools and software libraries:
+tools and software components:
\begin{itemize}
\item XML specifications for the Calculus of Inductive Constructions,
-with libraries for parsing and saving mathematical objects in such a format
+with components for parsing and saving mathematical objects in such a format
\cite{exportation-module};
-\item metadata specifications with libraries for indexing and querying the
+\item metadata specifications with components for indexing and querying the
XML knowledge base;
\item a proof checker library (i.e. the {\em kernel} of a proof assistant),
-implemented to check that we exported form the \COQ{} library all the
+implemented to check that we exported from the \COQ{} library all the
logically relevant content;
\item a sophisticated parser (used by the search engine), able to deal
with potentially ambiguous and incomplete information, typical of the
partially specified terms, used by the disambiguating parser;
\item complex transformation algorithms for proof rendering in natural
language \cite{remathematization};
-\item an innovative, MathML-compliant rendering widget for the GTK
+\item an innovative, \MATHML-compliant rendering widget for the GTK
graphical environment\cite{padovani}, supporting
high-quality bidimensional
rendering, and semantic selection, i.e. the possibility to select semantically
-meaningful rendering expressions, and to past the respective content into
+meaningful rendering expressions, and to paste the respective content into
a different text area.
\end{itemize}
Starting from all this, developing our own proof assistant was not
overall management of the library, integrating everything into a
single system. \MATITA{} is the result of this effort.
-\subsection{The System}
-DESCRIZIONE DEL SISTEMA DAL PUNTO DI VISTA ``UTENTE''
+\subsection{The system}
+
+\MATITA{} is a proof assistant (also called interactive theorem prover).
+It is based on the Calculus of (Co)Inductive Constructions (CIC) that
+is a dependently typed lambda-calculus \`a la Church enriched with primitive
+inductive and co-indutive data types. Via the Curry-Howard isomorphism, the
+calculus can be seen as a very rich higher order logic and proofs can be
+simply represented and stored as lambda-terms. Coq and Lego are other systems
+that adopt (variations of) CIC as their foundation.
+
+The proof language of \MATITA{} is procedural, in the tradition of the LCF
+theorem prover. Coq, NuPRL, PVS, Isabelle are all examples of others systems
+whose proof language is procedural. Traditionally, in a procedural system
+the user interacts only with the \emph{script}, while proof terms are internal
+records kept by the system. On the contrary, in \MATITA{} proof terms are
+praised as declarative versions of the proof. With this role, they are the
+primary mean of communication of proofs (once rendered to natural language
+for human audiences).
+
+The user interfaces now adopted by all the proof assistants that adopt a
+procedural proof language have been inspired by the CtCoq pioneering
+system~\cite{ctcoq}. One succesfull incarnation of the ideas introduced
+by CtCoq is the Proof General generic interface, that has set a sort of
+standard way to interact with the system. Several procedural proof assistants
+have either adopted or cloned Proof General as their main user interface.
+\MATITA{} has also cloned the Proof General interface,
\begin{itemize}
\item scelta del sistema fondazionale
we could furtherly reduce our code in sensible way).
Moreover, the complexity of the code of \MATITA{} is greatly reduced with
-respect to \COQ. For instance, the API of the libraries of \MATITA{} comprise
+respect to \COQ. For instance, the API of the components of \MATITA{} comprise
989 functions, to be compared with the 4'286 functions of \COQ.
Finally, \MATITA{} has several innovatives features over \COQ{} that derive
we have took advantage of the research results and experiences previously
developed by others, comprising the authors of \COQ. Moreover, starting from
scratch, we have designed in advance the architecture and we have splitted
-the code in coherent minimally coupled libraries.
+the code in coherent minimally coupled components.
In the future we plan to exploit \MATITA{} as a test bench for new ideas and
-extensions. Keeping the single libraries and the whole architecture as
+extensions. Keeping the single components and the whole architecture as
simple as possible is thus crucial to foster future experiments and to
allow other developers to quickly understand our code and contribute.
%be able to contribute to \COQ{}'s code is quite steep and requires direct
%and frequent interactions with \COQ{} developers.
-\begin{figure}[t]
+\section{Architecture}
+\label{architettura}
+
+\begin{figure}[ht]
\begin{center}
\includegraphics[width=0.9\textwidth]{librariesCluster.ps}
- \caption{\MATITA{} libraries}
+ \caption{\MATITA{} components}
\label{fig:libraries}
\end{center}
\end{figure}
-\section{Architecture}
-\label{architettura}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
project.
formulae. The firsts are translated to a content level representation of
proof steps that can easily be rendered in natural language. 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
+isomorphic to it. Terms that represent formulae are translated to \MATHML{}
+Content formulae. \MATHML{} Content~\cite{mathml} is a W3C standard
for the representation of content level formulae in an XML extensible format.
The translation to content level is implemented in the
single day, but they stick to a set of symbols that is more or less fixed.
The fact that the presentation language is finite allows the definition of
-standard languages. In particular, for formulae we have adopt MathML
+standard languages. In particular, for formulae we have adopt \MATHML{}
Presentation~\cite{mathml} that is an XML dialect standardized by the W3C. To
visually
represent proofs it is enough to embed formulae in plain text enriched with
formatting boxes. Since the language of formatting boxes is very simple,
many equivalent specifications exist and we have adopted our own, called
-BoxML.
+\BOXML.
The \texttt{content\_pres} \component{} contains the implementation of the
translation from content level terms to presentation level terms. The
rendering of presentation level terms is left to the application that uses
the \component. However, in the \texttt{hgdome} \component{} we provide a few
-utility functions to build a \GDOME~\cite{gdome2} MathML+BoxML tree from our
+utility functions to build a \GDOME~\cite{gdome2} \MATHML+\BOXML{} tree from our
presentation
-level terms. \GDOME{} MathML+BoxML trees can be rendered by the GtkMathView
+level terms. \GDOME{} \MATHML+\BOXML{} trees can be rendered by the
+\GTKMATHVIEW{}
widget developed by Luca Padovani \cite{padovani}. The widget is
particularly interesting since it allows to implement \emph{semantic
selection}.
%In particular, the \texttt{xml} \component{} is used to easily represent,
%parse and pretty-print XML files.
-\section{Using \MATITA (boh \ldots cambiare titolo)}
-\begin{figure}[t]
- \begin{center}
-% \includegraphics[width=0.9\textwidth]{a.eps}
- \caption{\MATITA{} screenshot}
- \label{fig:screenshot}
- \end{center}
-\end{figure}
+\section{The interface to the library}
+
+A proof assistant provides both an interface to interact with its library and
+an \emph{authoring} interface to develop new proofs and theories. According
+to its historical origins, \MATITA{} strives to provide innovative
+functionalities for the interaction with the library. It is more traditional
+in its script based authoring interface.
+
+In the remaining part of the paper we focus on the user view of \MATITA{}.
+This section is devoted to the aspects of the tool that arise from the
+document centric approach to the library. Sect.~\ref{authoring} describes
+the peculiarities of the authoring interface.
+
+
+The library of \MATITA{} comprises mathematical concepts (theorems,
+axioms, definitions) and notation. The concepts are authored sequentially
+using scripts that are (ordered) sequences of procedural commands.
+However, once they are produced we store them independently in the library.
+The only relation implicitly kept between the notions are the logical,
+acyclic dependencies among them. This way the library forms a global (and
+distributed) hypertext. Several useful operations can be implemented on the
+library only, regardless of the scripts. Examples of such operations
+implemented in \MATITA{} are: searching and browing (see Sect.~\ref{sec:index});
+disambiguation of content level terms (see Sect.~\ref{sec:disambiguation});
+automatic proof searching (see Sect.~\ref{sec:automation}).
+
+A requisite for the previous operations is that the library must
+be fully accessible and in a logically consistent state. To preserve
+consistency, a concept cannot be altered or removed unless the part of the
+library that depends on it is modified accordingly. To allow incremental
+changes and cooperative development, consistent revisions are necessary.
+For instance, to modify a definition, the user could fork a new version
+of the library where the definition is updated and all the concepts that
+used to rely on it are absent. The user is then responsible to restore
+the removed part in the new branch, merging the branch when the library is
+fully restored.
+
+To implement the proposed versioning system on top of a standard one
+it is necessary to implement \emph{invalidation} first. Invalidation
+is the operation that locates and removes from the library all the concepts
+that depend on a given one. As described in Sect.~\ref{sec:...}, removing
+a concept from the library also involves deleting its metadata from the
+database.
-\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
-split in two main windows: on the left a textual widget is used to edit the
-script, on the right the list of open goal is shown using a MathML rendering
-widget. A distinguished part of the script (shaded in the screenshot) represent
-the commands already executed and can't be edited without undoing them. The
-remaining part can be freely edited and commands from that part can be executed
-moving down the execution point. An additional window --- the ``cicBrowser'' ---
-can be used to browse the library, including the proof being developed, and
-enable content based search on it. In the cicBrowser proofs are rendered in
-natural language, automatically generated from the low-level $\lambda$-terms
-using techniques inspired by \cite{natural,YANNTHESIS}.
+For non collaborative development, full versioning can be avoided, but
+invalidation is still required. Since nobody else is relying on your
+development, you are free to change and invalidate part of the library
+without branching. Invalidation is still necessary to avoid using a
+concept that is no longer valid.
+So far, in \MATITA{} we address only this non collaborative scenario
+(see Sect.~\ref{sec:decompilazione}). Collaborative development and versioning
+is still under design.
-In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
-only seen as a convenient way to create mathematical objects. The universe of
-all these objects makes up the \HELM{} library, which is always completely
-visible to the user. The mathematical library is thus conceived as a global
-hypertext, where objects may freely reference each other. It is a duty of
-the system to guide the user through the relevant parts of the library.
+Scripts are not seen as constituents of the library. They are not published
+and indexed, so they cannot be searched or browsed using \HELM{} tools.
+However, they play a central role for the mainteinance of the library.
+Indeed, once a notion is invalidated, the only way to restore it is to
+fix the possibly broken script that used to generate it.
+Moreover, during the authoring phase, scripts are a natural way to
+group notions together. They also constitute a less fine grained clustering
+of notions for invalidation.
-This methodological assumption has many important consequences
-which will be discussed in the next section.
+In the following sections we present in more details the functionalities
+of \MATITA{} related to library management and exploitation.
-%on one side
-%it requires functionalities for the overall management of the library,
-%%%%%comprising efficient indexing techniques to retrieve and filter the
-%information;
-%on the other it introduces overloading in the use of
-%identifiers and mathematical notation, requiring sophisticated disambiguation
-%techniques for interpreting the user inputs.
-%In the next two sections we shall separately discuss the two previous
-%points.
-%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
-%organized in components which work on data in this format. For instance the
-%rendering engine, which transform $\lambda$-terms encoded as XML document to
-%MathML Presentation documents, can be used apart from \MATITA{} to print ...
-%FINIRE
-A final section is devoted to some innovative aspects
-of the authoring system, such as a step by step tactical execution,
-content selection and copy-paste.
+\subsection{Indexing and searching}
-\section{Library Management}
+\subsection{Disambiguation}
+\label{sec:disambiguation}
+
+Software applications that involve input of mathematical content should strive
+to require the user as less drift from informal mathematics as possible. We
+believe this to be a fundamental aspect of such applications user interfaces.
+Being that drift in general very large when inputing
+proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
+mathematical formulae which can be input using a \TeX-like encoding (the
+concrete syntax corresponding to presentation level terms) and are then
+translated (in multiple steps) to partially specified terms as sketched in
+Sect.~\ref{sec:contentintro}.
+
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+such an algorithm in the context of the development of a library of formalized
+mathematics. We will see that using multiple passes of the algorithm, varying
+some of its parameters, helps in keeping the input terse without sacrificing
+expressiveness.
+
+\subsubsection{Disambiguation aliases}
+\label{sec:disambaliases}
+Let's start with the definition of the ``strictly greater then'' notion over
+(Peano) natural numbers.
+
+\begin{grafite}
+include "nat/nat.ma".
+..
+definition gt: nat \to nat \to Prop \def
+ \lambda n, m. m < n.
+\end{grafite}
+
+The \texttt{include} statement adds the requirement that the part of the library
+defining the notion of natural numbers should be defined before
+processing the what follows. Note indeed that the algorithm presented
+in~\cite{disambiguation} does not describe where interpretations for ambiguous
+expressions come from, since it is application-specific. As a first
+approximation, we will assume that in \MATITA{} they come from the library (i.e.
+all interpretations available in the library are used) and the \texttt{include}
+statements are used to ensure the availability of required library slices (see
+Sect.~\ref{sec:libmanagement}).
+
+While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
+terms: its type and its body. Being available in the required library only one
+interpretation both for the unbound identifier \texttt{nat} and for the
+\OP{<} operator, and being the resulting partially specified term refinable,
+both type and body are easily disambiguated.
+
+Now suppose we have defined integers as signed natural numbers, and that we want
+to prove a theorem about an order relationship already defined on them (which of
+course overload the \OP{<} operator):
+
+\begin{grafite}
+include "Z/z.ma".
+..
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+Since integers are defined on top of natural numbers, the part of the library
+concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
+type. Thus, according to the disambiguation algorithm, two different partially
+specified terms could be associated to it. At first, this might not be seen as a
+problem, since the user is asked and can choose interactively which of the two
+she had in mind. However in the long run it has the drawbacks of inhibiting
+batch compilation of the library (a technique used in \MATITA{} for behind the
+scene compilation when needed, e.g. when an \texttt{include} is issued) and
+yields to poor user interaction (imagine how tedious would be to be asked for a
+choice each time you re-evaluate \texttt{Zlt\_compat}!).
+
+For this reason we added to \MATITA{} the concept of \emph{disambiguation
+aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
+expressions to partially specified terms, which are part of the runtime status
+of \MATITA. They can be provided by users with the \texttt{alias} statement, but
+are usually automatically added when evaluating \texttt{include} statements
+(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
+are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
+which require interactive choice are saved in batch compilable format. Thus,
+after evaluating the above theorem the script will be changed to the following
+snippet (assuming that the interpretation of \OP{<} over integers has been
+choosed):
+
+\begin{grafite}
+alias symbol "lt" = "integer 'less than'".
+theorem Zlt_compat:
+ \forall x, y, z. x < y \to y < z \to x < z.
+\end{grafite}
+
+But how are disambiguation aliases used? Since they come from the parts of the
+library explicitely included we may be tempted of using them as the only
+available interpretations. This would speed up the disambiguation, but may fail.
+Consider for example:
+
+\begin{grafite}
+theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+\end{grafite}
+
+and suppose that the \OP{+} operator is defined only on natural numbers. If
+the alias for \OP{<} points to the integer version of the operator, no
+refinable partially specified term matching the term could be found.
+
+For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
+first pass attempt to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass), in case of failure the next pass try again
+the disambiguation forgetting the aliases and using the whole library to
+retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
+Since the latter pass may lead to too many choices we intertwined an additional
+pass among the two which use as interpretations all the aliases coming for
+included parts of the library (\emph{multi aliases} phase). This is the reason
+why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
+turned out to be a well-balanced trade-off among performances (earlier passes
+fail quickly) and degree of ambiguity supported for presentation level terms.
+
+\subsubsection{Operator instances}
+
+Let's suppose now we want to define a theorem relating ordering relations on
+natural and integer numbers. The way we would like to write such a theorem (as
+we can read it in the \MATITA{} standard library) is:
+
+\begin{grafite}
+include "Z/z.ma".
+include "nat/orders.ma".
+..
+theorem lt_to_Zlt_pos_pos:
+ \forall n, m: nat. n < m \to pos n < pos m.
+\end{grafite}
+
+Unfortunately, none of the passes described above is able to disambiguate its
+type, no matter how aliases are defined. This is because the \OP{<} operator
+occurs twice in the content level term (it has two \emph{instances}) and two
+different interpretations for it have to be used in order to obtain a refinable
+partially specified term. To address this issue, we have the ability to consider
+each instance of a single symbol as a different ambiguous expression in the
+content level term, and thus we can assign a different interpretation to each of
+them. A disambiguation pass which exploit this feature is said to be using
+\emph{fresh instances}.
+
+Fresh instances lead to a non negligible performance loss (since the choice of
+an interpretation for one instances does not constraint the choice for the
+others). For this reason we always attempt a fresh instances pass only after
+attempting a non-fresh one.
+
+\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
+instance-independent. However, aliases obtained as a result of a disambiguation
+pass which uses fresh instances ought to be instance-dependent, that is: to
+ensure a term can be disambiguated in a batch fashion we may need to state that
+an \emph{i}-th instance of a symbol should be mapped to a given partially
+specified term. Instance-depend aliases are meaningful only for the term whose
+disambiguation generated it. For this reason we call them \emph{one-shot
+aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
+script.
+
+\subsubsection{Implicit coercions}
+
+Let's now consider a (rather hypothetical) theorem about derivation:
+
+\begin{grafite}
+theorem power_deriv:
+ \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+\end{grafite}
+
+and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
+interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
+Mathematichians would write the term that way since it is well known that the
+natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
+number for the purpose of real multiplication. The refiner of \MATITA{} supports
+\emph{implicit coercions} for this reason: given as input the above content
+level term, it will return a partially specified term where in place of
+\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
+(assuming it has been defined as such of course).
+
+Nonetheless coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
+among the possible partially specified term choices. For this reason in
+\MATITA{} we always try first a disambiguation pass which require the refiner
+not to use the coercions and only in case of failure we attempt a
+coercion-enabled pass.
+
+It is interesting to observe also the relationship among operator instances and
+implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
+which \MATITA{} disambiguated using fresh instances. In case there exists a
+coercion from natural numbers to (positive) integers (which indeed does, it is
+the \texttt{pos} constructor itself), the theorem can be disambiguated using
+twice that coercion on the left hand side of the implication. The obtained
+partially specified term however would not probably be the expected one, being a
+theorem which prove a trivial implication. For this reason we choose to always
+prefer fresh instances over implicit coercions, i.e. we always attempt
+disambiguation passes with fresh instances and no implicit coercions before
+attempting passes with implicit coercions.
+
+\subsubsection{Disambiguation passes}
+
+According to the criteria described above in \MATITA{} we choose to perform the
+sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+our experience that choice implements a good trade off among disambiguation time
+and admitted ambiguity in terms input by users.
+
+\begin{table}[ht]
+ \caption{Sequence of disambiguation passes used in \MATITA.\strut}
+ \label{tab:disambpasses}
+ \begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+ & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+ & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+ \hline
+ \PASS & Mono aliases & Shared & Disabled \\
+ \PASS & Multi aliases & Shared & Disabled \\
+ \PASS & Mono aliases & Fresh instances & Disabled \\
+ \PASS & Multi aliases & Fresh instances & Disabled \\
+ \PASS & Mono aliases & Fresh instances & Enabled \\
+ \PASS & Multi aliases & Fresh instances & Enabled \\
+ \PASS & Library aliases& Fresh instances & Enabled
+ \end{tabular}
+ \end{center}
+\end{table}
-\subsection{Indexing and searching}
\subsection{Compilation and cleaning}
\subsection{Automation}
-\subsection{\MATITA's naming convention}
+\subsection{Naming convention}
A minor but not entirely negligible aspect of \MATITA{} is that of
adopting a (semi)-rigid naming convention for identifiers, derived by
our studies about metadata for statements.
expression and the suffix \verb+_to_Prop+. In the above example,
\verb+eqb_to_Prop+ is accepted.
-\section{The \MATITA{} user interface}
-
-\subsection{Disambiguation}
-\label{sec:disambiguation}
-
-Software applications that involve input of mathematical content should strive
-to require the user as less drift from informal mathematics as possible. We
-believe this to be a fundamental aspect of such applications user interfaces.
-Being that drift in general very large when inputing
-proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
-mathematical formulae which can be input using a \TeX-like encoding (the
-concrete syntax corresponding to presentation level terms) and are then
-translated (in multiple steps) to partially specified terms as sketched in
-Sect.~\ref{sec:contentintro}.
-
-The key component of the translation is the generic disambiguation algorithm
-implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
-and presented in~\cite{disambiguation}. In this section we present how to use
-such an algorithm in the context of the development of a library of formalized
-mathematics. We will see that using multiple passes of the algorithm, varying
-some of its parameters, helps in keeping the input terse without sacrificing
-expressiveness.
-
-\subsubsection{Disambiguation aliases}
-\label{sec:disambaliases}
-Let's start with the definition of the ``strictly greater then'' notion over
-(Peano) natural numbers.
-
-\begin{grafite}
-include "nat/nat.ma".
-..
-definition gt: nat \to nat \to Prop \def
- \lambda n, m. m < n.
-\end{grafite}
-
-The \texttt{include} statement adds the requirement that the part of the library
-defining the notion of natural numbers should be defined before
-processing the what follows. Note indeed that the algorithm presented
-in~\cite{disambiguation} does not describe where interpretations for ambiguous
-expressions come from, since it is application-specific. As a first
-approximation, we will assume that in \MATITA{} they come from the library (i.e.
-all interpretations available in the library are used) and the \texttt{include}
-statements are used to ensure the availability of required library slices (see
-Sect.~\ref{sec:libmanagement}).
-
-While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
-terms: its type and its body. Being available in the required library only one
-interpretation both for the unbound identifier \texttt{nat} and for the
-\OP{<} operator, and being the resulting partially specified term refinable,
-both type and body are easily disambiguated.
-
-Now suppose we have defined integers as signed natural numbers, and that we want
-to prove a theorem about an order relationship already defined on them (which of
-course overload the \OP{<} operator):
+\section{The authoring interface}
-\begin{grafite}
-include "Z/z.ma".
-..
-theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
-\end{grafite}
-
-Since integers are defined on top of natural numbers, the part of the library
-concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
-type. Thus, according to the disambiguation algorithm, two different partially
-specified terms could be associated to it. At first, this might not be seen as a
-problem, since the user is asked and can choose interactively which of the two
-she had in mind. However in the long run it has the drawbacks of inhibiting
-batch compilation of the library (a technique used in \MATITA{} for behind the
-scene compilation when needed, e.g. when an \texttt{include} is issued) and
-yields to poor user interaction (imagine how tedious would be to be asked for a
-choice each time you re-evaluate \texttt{Zlt\_compat}!).
-
-For this reason we added to \MATITA{} the concept of \emph{disambiguation
-aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
-expressions to partially specified terms, which are part of the runtime status
-of \MATITA. They can be provided by users with the \texttt{alias} statement, but
-are usually automatically added when evaluating \texttt{include} statements
-(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
-are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
-which require interactive choice are saved in batch compilable format. Thus,
-after evaluating the above theorem the script will be changed to the following
-snippet (assuming that the interpretation of \OP{<} over integers has been
-choosed):
-
-\begin{grafite}
-alias symbol "lt" = "integer 'less than'".
-theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
-\end{grafite}
-
-But how are disambiguation aliases used? Since they come from the parts of the
-library explicitely included we may be tempted of using them as the only
-available interpretations. This would speed up the disambiguation, but may fail.
-Consider for example:
-
-\begin{grafite}
-theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
-\end{grafite}
-
-and suppose that the \OP{+} operator is defined only on natural numbers. If
-the alias for \OP{<} points to the integer version of the operator, no
-refinable partially specified term matching the term could be found.
-
-For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
-first pass attempt to disambiguate using the last available disambiguation
-aliases (\emph{mono aliases} pass), in case of failure the next pass try again
-the disambiguation forgetting the aliases and using the whole library to
-retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
-Since the latter pass may lead to too many choices we intertwined an additional
-pass among the two which use as interpretations all the aliases coming for
-included parts of the library (\emph{multi aliases} phase). This is the reason
-why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
-turned out to be a well-balanced trade-off among performances (earlier passes
-fail quickly) and degree of ambiguity supported for presentation level terms.
-
-\subsubsection{Operator instances}
-
-Let's suppose now we want to define a theorem relating ordering relations on
-natural and integer numbers. The way we would like to write such a theorem (as
-we can read it in the \MATITA{} standard library) is:
-
-\begin{grafite}
-include "Z/z.ma".
-include "nat/orders.ma".
-..
-theorem lt_to_Zlt_pos_pos:
- \forall n, m: nat. n < m \to pos n < pos m.
-\end{grafite}
-
-Unfortunately, none of the passes described above is able to disambiguate its
-type, no matter how aliases are defined. This is because the \OP{<} operator
-occurs twice in the content level term (it has two \emph{instances}) and two
-different interpretations for it have to be used in order to obtain a refinable
-partially specified term. To address this issue, we have the ability to consider
-each instance of a single symbol as a different ambiguous expression in the
-content level term, and thus we can assign a different interpretation to each of
-them. A disambiguation pass which exploit this feature is said to be using
-\emph{fresh instances}.
-
-Fresh instances lead to a non negligible performance loss (since the choice of
-an interpretation for one instances does not constraint the choice for the
-others). For this reason we always attempt a fresh instances pass only after
-attempting a non-fresh one.
+\begin{figure}[t]
+ \begin{center}
+ \includegraphics[width=0.95\textwidth]{matita-screenshot}
+ \caption{\MATITA{} look and feel}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
-\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
-instance-independent. However, aliases obtained as a result of a disambiguation
-pass which uses fresh instances ought to be instance-dependent, that is: to
-ensure a term can be disambiguated in a batch fashion we may need to state that
-an \emph{i}-th instance of a symbol should be mapped to a given partially
-specified term. Instance-depend aliases are meaningful only for the term whose
-disambiguation generated it. For this reason we call them \emph{one-shot
-aliases} and \MATITA{} doesn't use it to disambiguate further terms down in the
-script.
+\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
+split in two main windows: on the left a textual widget is used to edit the
+script, on the right the list of open goal is shown using a \MATHML{} rendering
+widget. A distinguished part of the script (shaded in the screenshot) represent
+the commands already executed and can't be edited without undoing them. The
+remaining part can be freely edited and commands from that part can be executed
+moving down the execution point. An additional window --- the ``cicBrowser'' ---
+can be used to browse the library, including the proof being developed, and
+enable content based search on it. In the cicBrowser proofs are rendered in
+natural language, automatically generated from the low-level $\lambda$-terms
+using techniques inspired by \cite{natural,YANNTHESIS}.
-\subsubsection{Implicit coercions}
+%In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
+%only seen as a convenient way to create mathematical objects. The universe of
+%all these objects makes up the \HELM{} library, which is always completely
+%visible to the user. The mathematical library is thus conceived as a global
+%hypertext, where objects may freely reference each other. It is a duty of
+%the system to guide the user through the relevant parts of the library.
-Let's now consider a (rather hypothetical) theorem about derivation:
+%This methodological assumption has many important consequences
+%which will be discussed in the next section.
-\begin{grafite}
-theorem power_deriv:
- \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
-\end{grafite}
+%on one side
+%it requires functionalities for the overall management of the library,
+%%%%%comprising efficient indexing techniques to retrieve and filter the
+%information;
+%on the other it introduces overloading in the use of
+%identifiers and mathematical notation, requiring sophisticated disambiguation
+%techniques for interpreting the user inputs.
+%In the next two sections we shall separately discuss the two previous
+%points.
-and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
-interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematichians would write the term that way since it is well known that the
-natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
-number for the purpose of real multiplication. The refiner of \MATITA{} supports
-\emph{implicit coercions} for this reason: given as input the above content
-level term, it will return a partially specified term where in place of
-\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
-(assuming it has been defined as such of course).
+%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
+%organized in components which work on data in this format. For instance the
+%rendering engine, which transform $\lambda$-terms encoded as XML document to
+%\MATHML{} Presentation documents, can be used apart from \MATITA{} to print ...
+%FINIRE
-Nonetheless coercions are not always desirable. For example, in disambiguating
-\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
-two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
-among the possible partially specified term choices. For this reason in
-\MATITA{} we always try first a disambiguation pass which require the refiner
-not to use the coercions and only in case of failure we attempt a
-coercion-enabled pass.
+A final section is devoted to some innovative aspects
+of the authoring system, such as a step by step tactical execution,
+content selection and copy-paste.
-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.
+\subsection{Patterns}
-\subsubsection{Disambiguation passes}
+\subsubsection{Direct manipulation of terms}
-According to the criteria described above in \MATITA{} we choose to perform the
-sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
-our experience that choice implements a good trade off among disambiguation time
-and admitted ambiguity in terms input by users.
+While terms are input as \TeX-like formulae in \MATITA, they're converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. This mixed choice~\cite{latexmathml} enables both high-quality
+bidimensional rendering of terms (including the use of fancy layout schemata
+like radicals and matrices~\cite{mathml}) and the use of a concise and
+widespread textual syntax.
-\begin{table}[ht]
- \caption{Sequence of disambiguation passes used in \MATITA.\strut}
- \label{tab:disambpasses}
+\begin{figure}[t]
\begin{center}
- \begin{tabular}{c|c|c|c}
- \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
- & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
- & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
- & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
- \hline
- \PASS & Mono aliases & Shared & Disabled \\
- \PASS & Multi aliases & Shared & Disabled \\
- \PASS & Mono aliases & Fresh instances & Disabled \\
- \PASS & Multi aliases & Fresh instances & Disabled \\
- \PASS & Mono aliases & Fresh instances & Enabled \\
- \PASS & Multi aliases & Fresh instances & Enabled \\
- \PASS & Library aliases& Fresh instances & Enabled
- \end{tabular}
+ \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+ \hspace{0.05\textwidth}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
+ \caption{Semantic selection and hyperlinks}
+ \label{fig:directmanip}
\end{center}
-\end{table}
-
-\subsection{Patterns}
-
-serve una intro che almeno cita il widget (per i patterns) e che fa
-il resoconto delle cose che abbiamo e che non descriviamo,
-sottolineando che abbiamo qualcosa da dire sui pattern e sui
-tattichini.\\
-
-Patterns are the textual counterpart of the MathML widget graphical
-selection.
+\end{figure}
-\MATITA{} benefits of a graphical interface and a powerful MathML rendering
-widget that allows the user to select pieces of the sequent he is working
-on. While this is an extremely intuitive way for the user to
-restrict the application of tactics, for example, to some subterms of the
-conclusion or some hypothesis, the way this action is recorded to the text
-script is not obvious.\\
-In \MATITA{} this issue is addressed by patterns.
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enable the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\forall~n:nat$ since the former denotes an application while the
+latter denotes an incomplete $\Pi$-binder. Once a (sub)term has been
+selected that way actions can be done on it like reductions or tactic
+applications.
+
+In our experience working with direct manipulation of terms is really
+effective and faster than retyping them. Nonetheless we need a way to
+encode term selections in scripts so that they can be batch compiled
+by \MATITAC. In \MATITA{} \emph{patterns} implement that encoding,
+being patterns the textual representations of \GTKMATHVIEW{} semantic
+selections. \NOTE{Zack:c'\`e scritto da qualche parte che l'utente
+non li deve necessariamente scrivere a mano, ma che pu\`o incollarli?
+Va scritto.}
\subsubsection{Pattern syntax}
A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
The concrete syntax is reported in table \ref{tab:pathsyn}
\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
\begin{table}
- \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
+ \caption{\label{tab:pathsyn} Patterns concrete syntax.\strut}
\hrule
+% \[
+% \begin{array}{@{}rcll@{}}
+% \NT{pattern} &
+% ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
+% \NT{sequent\_path} &
+% ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+% [~\verb+\vdash+~\NT{multipath}~] & \\
+% \NT{wanted} & ::= & \NT{term} & \\
+% \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+% \end{array}
+% \]
\[
\begin{array}{@{}rcll@{}}
\NT{pattern} &
- ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
+ ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
\NT{sequent\_path} &
::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
[~\verb+\vdash+~\NT{multipath}~] & \\
- \NT{wanted} & ::= & \NT{term} & \\
\NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+ \NT{wanted} & ::= & \NT{term} & \\
\end{array}
\]
\hrule
\end{table}
-\subsubsection{How patterns work}
+\subsubsection{Pattern concepts}
Patterns mimic the user's selection in two steps. The first one
selects roots (subterms) of the sequent, using the
$\NT{sequent\_path}$, while the second
their context that will be eventually used in the second phase.
\item[Phase 2]
- plays a role only if the $[~\verb+in match+~\NT{wanted}~]$
+ plays a role only if the $[~\verb+match+~\NT{wanted}~]$
part is specified. From the first phase we have some terms, that we
will see as subterm roots, and their context. For each of these
contexts the $\NT{wanted}$ term is disambiguated in it and the
works too and can be done, by the experienced user, writing directly
a simpler pattern that uses the second phase.
\begin{grafite}
- change in match n in H with (O + n).
+ change in H match n with (O + n).
\end{grafite}
\noindent
In this case the $\NT{sequent\_path}$ selects the whole $H$, while
goal) gives you the feeling of what is going on.
\end{description}
-\section{The \MATITA{} library}
+\section{Standard library}
\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
can be read, checked and referenced in further developments.
projects / helm.git / blobdiff