The origins of \MATITA{} go back to 1999. At the time we were mostly
interested in developing tools and techniques to enhance the accessibility
-via Web of libraries of formal mathematics. Due to its dimension, the
+via Web of libraries of formalized mathematics. Due to its dimension, the
library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
was chosen as a privileged test bench for our work, although experiments
have been also conducted with other systems, and notably
those of addition over the unary representation. And addition over two natural
numbers is definitely different from addition over two real numbers.
-Formal mathematics cannot hide these differences and obliges the user to be
+Formalized mathematics cannot hide these differences and obliges the user to be
very precise on the types he is using and their representation. However,
to communicate formulae with the user and with external tools, it seems good
practice to stick to the usual imprecise mathematical ontology. In the
an \emph{authoring} interface to develop new proofs and theories. According
to its historical origins, \MATITA{} strives to provide innovative
functionalities for the interaction with the library. It is more traditional
-in its script based authoring interface.
-
-In the remaining part of the paper we focus on the user view of \MATITA.
-This section is devoted to the aspects of the tool that arise from the
-document centric approach to the library. Sect.~\ref{sec:authoring} describes
-the peculiarities of the authoring interface.
+in its script based authoring interface. In the remaining part of the paper we
+focus on the user view of \MATITA.
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.
+Once they are produced we store them independently in the library.
The only relation implicitly kept between the concepts are the logical,
acyclic dependencies among them. This way the library forms a global (and
distributed) hypertext.
\begin{figure}[!ht]
\begin{center}
- \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-browsing}
+ \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-browsing}
\hspace{0.05\textwidth}
- \includegraphics[width=0.40\textwidth]{pics/cicbrowser-screenshot-query}
+ \includegraphics[width=0.45\textwidth]{pics/cicbrowser-screenshot-query}
\caption{Browsing and searching the library\strut}
\label{fig:cicbrowser1}
\end{center}
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
+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
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
+\REF{p}{s}{t} stating that a concept $s$ refers a concept $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
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.
+A first, very simple but not negligeable feature is the \emph{duplicate check}.
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
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
+
+In the near future, we expect to extend the \HINT{} query to
a \REWRITEHINT, resulting in all equational statements that
can be applied to rewrite the current goal.
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
+The key ingredient 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
+and presented in~\cite{disambiguation}. In this section we detail how to use
that algorithm in the context of the development of a library of formalized
mathematics. We will see that using multiple passes of the algorithm, varying
some of its parameters, helps in keeping the input terse without sacrificing
\subsubsection{Disambiguation aliases}
\label{sec:disambaliases}
-Consider the following command to state a theorem over integer numbers:
+Consider the following command that states a theorem over integer numbers:
\begin{grafite}
theorem Zlt_compat:
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.
+natural place is the script itself.
In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
They are mappings, stored in the library, from ambiguity sources
preferences.
Several disambiguation parameters can vary among passes. With respect to
-preference handling we implemented three passes. In the first pass, called
+preference handling we implemented 3 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
+current set of 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
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
+symbol as a different ambiguous expression in the content level term,
+enabling the use of a different alias for each of them.
+Exploiting or not this feature is
one of the disambiguation pass parameters. A disambiguation pass which exploit
it is said to be using \emph{fresh instances} (opposed to a \emph{shared
instances} pass).
Fresh instances lead to a non negligible performance loss (since the choice of
an alias for one 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.
+shared instances pass.
-\paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
+\paragraph{One-shot preferences} Disambiguation preferences 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
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
+\texttt{R}. The refiner of \MATITA{} supports
+\emph{implicit coercions}~\cite{barthe95implicit} 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
+Implicitc 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
+2 coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
among the possible partially specified term choices. For this reason we always
attempt a disambiguation pass which require the refiner not to use the coercions
before attempting a coercion-enabled pass.
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.
+probably be the expected one, being a theorem which proves 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
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.
+our experience that choice gives reasonable performance and minimizes the need
+of user interaction during the disambiguation.
\begin{table}[ht]
\caption{Disambiguation passes sequence\strut}
\subsubsection{Invalidation}
-Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
+Invalidation (see Sect.~\ref{sec:library}) is implemented in 2 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.
+depend on the ones we are invalidating. It can be performed
+using the relational database that stores the metadata.
This technique is the same used by the \emph{Dependency Analyzer}
and is described in~\cite{zack-master}.
%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
+the scripts 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 scripts that compose the development and
-outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+outputs their dependencies in a format suitable for the GNU \texttt{make}
+tool.\footnote{\url{http://www.gnu.org/software/make/}}
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 generation
related tasks, including dependencies calculation.
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}).
+literal of included explicit disambiguation preferences
+(see Sect.~\ref{sec:disambaliases}).
+\TODO{da rivedere: da dove salta fuori ``regenerating content''?}
Regenerating the content of a modified script file involves the preliminary
invalidation of all its old content.
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.
+to regenerate parts of the library previously invalidated.
+\TODO{come sopra: ``content of a script''?}
While they share the same engine for generation and invalidation, they
-provide different granularity. \MATITAC{} is only able to reexecute a
+provide different granularity. \MATITAC{} is only able to re-execute 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
+(together with all the other scripts that rely on a concept defined
in it).
\subsection{Automation}
\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
+adopting a (semi)-rigid naming convention for concept names, derived by
our studies about metadata for statements.
-The convention is only applied to identifiers for theorems
-(not definitions), and relates the name of a proof to its statement.
+The convention is only applied to theorems
+(not definitions), and relates theorem names to their statements.
The basic rules are the following:
\begin{itemize}
-\item each identifier is composed by an ordered list of (short)
-names occurring in a left to right traversal of the statement;
-\item all identifiers should (but this is not strictly compulsory)
-separated by an underscore,
-\item identifiers in two different hypothesis, or in an hypothesis
-and in the conclusion must be separated by the string ``\verb+_to_+'';
-\item the identifier may be followed by a numerical suffix, or a
-single or double apostrophe.
+
+ \item each name is composed by an ordered list of (short)
+ identifiers occurring in a left to right traversal of the statement;
+
+ \item all names should (but this is not strictly compulsory)
+ separated by an underscore;
+
+ \item names occurring in 2 different hypotheses, or in an hypothesis
+ and in the conclusion must be separated by the string \texttt{\_to\_};
+
+ \item the identifier may be followed by a numerical suffix, or a
+ single or double apostrophe.
\end{itemize}
-Take for instance the theorem
-\[\forall n:nat. n = plus \; n\; O\]
-Possible legal names are: \verb+plus_n_O+, \verb+plus_O+,
-\verb+eq_n_plus_n_O+ and so on.
-Similarly, consider the theorem
-\[\forall n,m:nat. n<m \to n \leq m\]
-In this case \verb+lt_to_le+ is a legal name,
-while \verb+lt_le+ is not.\\
+
+Take for instance the statement:
+\begin{grafite}
+ \forall n: nat. n = plus n O
+\end{grafite}
+Possible legal names are: \texttt{plus\_n\_O}, \texttt{plus\_O},
+\texttt{eq\_n\_plus\_n\_O} and so on.
+
+Similarly, consider the theorem:
+\begin{grafite}
+ \forall n, m: nat. n < m to n \leq m
+\end{grafite}
+In this case \texttt{lt\_to\_le} is a legal name,
+while \texttt{lt\_le} is not.
+
But what about, say, the symmetric law of equality? Probably you would like
to name such a theorem with something explicitly recalling symmetry.
The correct approach,
in this case, is the following. You should start with defining the
-symmetric property for relations
-
-\[definition\;symmetric\;= \lambda A:Type.\lambda R.\forall x,y:A.R x y \to R y x \]
+symmetric property for relations:
+\begin{grafite}
+definition symmetric =
+ \lambda A: Type. \lambda R. \forall x, y: A.
+ R x y \to R y x
+\end{grafite}
+Then, you may state the symmetry of equality as:
+\begin{grafite}
+\forall A: Type. symmetric A (eq A)
+\end{grafite}
+and \texttt{symmetric\_eq} is a legal name for such a theorem.
-Then, you may state the symmetry of equality as
-\[ \forall A:Type. symmetric \;A\;(eq \; A)\]
-and \verb+symmetric_eq+ is valid \MATITA{} name for such a theorem.
So, somehow unexpectedly, the introduction of semi-rigid naming convention
has an important beneficial effect on the global organization of the library,
-forcing the user to define abstract notions and properties before
+forcing the user to define abstract concepts and properties before
using them (and formalizing such use).
Two cases have a special treatment. The first one concerns theorems whose
conclusion is a (universally quantified) predicate variable, i.e.
theorems of the shape
-$\forall P,\dots.P(t)$.
-In this case you may replace the conclusion with the word
-``elim'' or ``case''.
-For instance the name \verb+nat_elim2+ is a legal name for the double
+$\forall P,\dots,.P(t)$.
+In this case you may replace the conclusion with the string
+\texttt{elim} or \texttt{case}.
+For instance the name \texttt{nat\_elim2} is a legal name for the double
induction principle.
The other special case is that of statements whose conclusion is a
match expression.
-A typical example is the following
-\begin{verbatim}
- \forall n,m:nat.
- match (eqb n m) with
- [ true \Rightarrow n = m
- | false \Rightarrow n \neq m]
-\end{verbatim}
-where $eqb$ is boolean equality.
+A typical example is the following:
+\begin{grafite}
+\forall n,m:nat.
+ match (eqb n m) with
+ [ true \Rightarrow n = m
+ | false \Rightarrow n \neq m]
+\end{grafite}
+where \texttt{eqb} is boolean equality.
In this cases, the name can be build starting from the matched
-expression and the suffix \verb+_to_Prop+. In the above example,
-\verb+eqb_to_Prop+ is accepted.
+expression and the suffix \texttt{\_to\_Prop}. In the above example,
+\texttt{eqb\_to\_Prop} is accepted.
\section{The authoring interface}
\label{sec:authoring}
projects / helm.git / commitdiff