\newcommand{\component}{component}
\newcommand{\components}{components}
-\newcommand{\AUTO}{\textsc{Auto}}
\newcommand{\BOXML}{BoxML}
\newcommand{\COQ}{Coq}
-\newcommand{\COQIDE}{CoqIde}
-\newcommand{\ELIM}{\textsc{Elim}}
\newcommand{\GDOME}{Gdome}
+\newcommand{\GTK}{GTK+}
\newcommand{\GTKMATHVIEW}{\textsc{GtkMathView}}
\newcommand{\HELM}{Helm}
\newcommand{\HINT}{\textsc{Hint}}
-\newcommand{\IN}{\ensuremath{\dN}}
-\newcommand{\INSTANCE}{\textsc{Instance}}
-\newcommand{\IR}{\ensuremath{\dR}}
-\newcommand{\IZ}{\ensuremath{\dZ}}
-\newcommand{\LIBXSLT}{LibXSLT}
-\newcommand{\LOCATE}{\textsc{Locate}}
-\newcommand{\MATCH}{\textsc{Match}}
+% \newcommand{\IN}{\ensuremath{\dN}}
+\newcommand{\LEGO}{Lego}
\newcommand{\MATHML}{MathML}
\newcommand{\MATITA}{Matita}
\newcommand{\MATITAC}{\texttt{matitac}}
\newcommand{\MATITADEP}{\texttt{matitadep}}
\newcommand{\MOWGLI}{MoWGLI}
\newcommand{\MOWGLIIST}{IST-2001-33562}
-\newcommand{\NAT}{\ensuremath{\mathit{nat}}}
-\newcommand{\NATIND}{\mathit{nat\_ind}}
\newcommand{\NUPRL}{NuPRL}
\newcommand{\OCAML}{OCaml}
-\newcommand{\PROP}{\mathit{Prop}}
\newcommand{\REF}[3]{\ensuremath{\mathit{Ref}_{#1}(#2,#3)}}
\newcommand{\REWRITEHINT}{\textsc{RewriteHint}}
\newcommand{\TEXMACRO}[1]{\texttt{\char92 #1}}
\newcommand{\URI}[1]{\texttt{#1}}
\newcommand{\OP}[1]{``\texttt{#1}''}
\newcommand{\FILE}[1]{\texttt{#1}}
-\newcommand{\NOTE}[1]{\ednote{#1}{}}
+\newcommand{\TAC}[1]{\texttt{#1}}
\newcommand{\TODO}[1]{\textbf{TODO: #1}}
\definecolor{gray}{gray}{0.85} % 1 -> white; 0 -> black
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\end{center}}
-\bibliographystyle{alpha}
+\bibliographystyle{klunum}
\begin{document}
\runningtitle{The \MATITA{} proof assistant}
\runningauthor{Asperti, Sacerdoti Coen, Tassi, Zacchiroli}
- \begin{motto}
- ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
- \end{motto}
+%\begin{motto}
+% ``We are nearly bug-free'' -- \emph{CSC, Oct 2005}
+% \end{motto}
\begin{abstract}
\TODO{scrivere abstract}
\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
+Prof.~Asperti. This paper describes the overall architecture of
the system, focusing on its most distinctive and innovative
features.
\subsection{Historical perspective}
The origins of \MATITA{} go back to 1999. At the time we were mostly
-interested to develop tools and techniques to enhance the accessibility
-via Web of formal libraries of mathematics. Due to its dimension, the
-library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
+interested in developing tools and techniques to enhance the accessibility
+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
with \NUPRL~\cite{nuprl-book}.
The work, mostly performed in the framework of the recently concluded
European project \MOWGLIIST{} \MOWGLI~\cite{pechino}, mainly consisted in the
following steps:
-\begin{itemize}
-\item exporting the information from the internal representation of
- \COQ{} to a system and platform independent format. Since XML was at the
-time an emerging standard, we naturally adopted this technology, fostering
-a content-centric architecture~\cite{content-centric} where the documents
-of the library were the the main components around which everything else
-has to be build;
-\item developing indexing and searching techniques supporting semantic
- queries to the library;
-\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.};
-\end{itemize}
+\begin{enumerate}
+
+ \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 that technology,
+ fostering 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 built;
+
+ \item developing indexing and searching techniques supporting semantic
+ queries to the library;
+
+ \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.}
+
+\end{enumerate}
According to our content-centric commitment, the library exported from
\COQ{} was conceived as being distributed and most of the tools were developed
-as Web services. The user could interact with the library and the tools by
+as Web services. The user can interact with the library and the tools by
means of a Web interface that orchestrates the Web services.
-The Web services and the other tools have been implemented as front-ends
+Web services and other tools have been implemented as front-ends
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 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};
-\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 from the \COQ{} library all the
-logically relevant content;
-\item a sophisticated parser (used by the search engine), able to deal
-with potentially ambiguous and incomplete information, typical of the
-mathematical notation~\cite{disambiguation};
-\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};
-\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 paste the respective content into
-a different text area.
+
+ \item XML specifications for the Calculus of Inductive Constructions,
+ 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 (i.e. the \emph{kernel} of a proof assistant),
+ implemented to check that we exported from the \COQ{} library all the
+ logically relevant content;
+
+ \item a sophisticated term parser (used by the search engine), able to deal
+ with potentially ambiguous and incomplete information, typical of the
+ mathematical notation~\cite{disambiguation};
+
+ \item a \emph{refiner} component, 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};
+
+ \item an innovative, \MATHML-compliant rendering widget~\cite{padovani}
+ for the \GTK{}\footnote{\url{http://www.gtk.org}} graphical environment,
+ 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
+ a different text area.
+
\end{itemize}
+
Starting from all this, developing our own proof assistant was not
too far away: essentially, we ``just'' had to
add an authoring interface, and a set of functionalities for the
Church enriched with primitive inductive and co-inductive data types.
Via the Curry-Howard isomorphism, the calculus can be seen as a very
rich higher order logic and proofs can be simply represented and
-stored as lambda-terms. \COQ{} and Lego are other systems that adopt
-(variations of) CIC as their foundation.
+stored as lambda-terms. \COQ{} and \LEGO~\cite{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
+theorem prover~\cite{lcf}. \COQ, \NUPRL, PVS, Isabelle are all examples of
+others systems
whose proof language is procedural. Traditionally, in a procedural system
the user interacts only with the \emph{script}, while proof terms are internal
-records kept by the system. On the contrary, in \MATITA{} proof terms are
-praised as declarative versions of the proof. With this role, they are the
-primary mean of communication of proofs (once rendered to natural language
-for human audiences).
-
-The user interfaces now adopted by all the proof assistants based on a
-procedural proof language have been inspired by the CtCoq pioneering
+records kept by the system.
+In \MATITA{}, which has been conceived for a potentially distributed
+library, proof terms are also meant as the primary representation for
+storage and communication with other systems (e.g. \COQ).
+%On the contrary, in \MATITA{} proof terms are
+%praised as declarative versions of the proof. Playing that role, they are the
+%primary mean of communication of proofs (once rendered to natural language
+%for human audiences).
+
+All the user interfaces currently adopted by proof assistants based on a
+procedural proof language have been influenced by the CtCoq pioneering
system~\cite{ctcoq1}. One successful incarnation of the ideas introduced
by CtCoq is the Proof General generic interface~\cite{proofgeneral},
that has set a sort of
-standard way to interact with the system. Several procedural proof assistants
-have either adopted or cloned Proof General as their main user interface.
-The authoring interface of \MATITA{} is a clone of the Proof General interface.
-
-\TODO{item che seguono:}
-\begin{itemize}
- \item sistema indipendente (da \COQ)
- \item compatibilit\`a con sistemi legacy
-\end{itemize}
+standard way to interact with the system.
+%Several procedural proof assistants
+%have either adopted or cloned Proof General as their main user interface.
+The authoring interface of \MATITA{} essentially offers the same
+functionalities of the Proof General interface or CoqIde.
+On the contrary, the interface to interact with the library is rather
+innovative and directly inspired by the Web interfaces to our Web servers.
+
+\MATITA{} is backward compatible with the XML library of proof objects exported
+from \COQ{}, but, in order to test the actual usability of the system, we are
+also developing a new library of basic results from scratch.
\subsection{Relationship with \COQ{}}
above than the result of a deliberate design. In particular, we
(essentially) share the same foundational dialect of \COQ{} (the
Calculus of (Co)Inductive Constructions), the same implementation
-language (\OCAML{}), and the same (script based) authoring philosophy.
-However, the analogy essentially stops here and no code is shared by the
-two systems.
+language (\OCAML\footnote{\url{http://caml.inria.fr/}}),
+and the same (procedural, script based) authoring philosophy.
+However, the analogy essentially stops here; in particular, no code is shared
+between the two systems and the algorithms are often different.
In a sense, we like to think of \MATITA{} as the way \COQ{} would
look like if entirely rewritten from scratch: just to give an
idea, although \MATITA{} currently supports almost all functionalities of
\COQ{}, it links 60'000 lines of \OCAML{} code, against the 166'000 lines linked
by \COQ{} (and we are convinced that, starting from scratch again,
-we could reduce our code even further in sensible way).
+we could reduce our code even further in a sensible way).
Moreover, the complexity of the code of \MATITA{} is greatly reduced with
respect to \COQ. For instance, the API of the components of \MATITA{} comprise
the parser for ambiguous mathematical notation.
The size and complexity improvements over \COQ{} must be understood
-historically. \COQ{} is a quite old
-system whose development started 20 years ago. Since then
+historically. \COQ~\cite{CoqArt} is a quite old
+system whose development started 20 years ago. Since then,
several developers have took over the code and several new research ideas
-that were not considered in the original architecture have been experimented
+and optimizations that were not considered in the original architecture
+have been experimented
and integrated in the system. Moreover, there exists a lot of developments
for \COQ{} that require backward compatibility between each pair of releases;
since many central functionalities of a proof assistant are based on heuristics
or arbitrary choices to overcome undecidability (e.g. for higher order
unification), changing these functionalities maintaining backward compatibility
-is very difficult. Finally, the code of \COQ{} has been greatly optimized
-over the years; optimization reduces maintainability and rises the complexity
-of the code.
+is very difficult.
+%Finally, the code of \COQ{} has been greatly optimized
+%over the years; optimization reduces maintainability and rises the complexity
+%of the code.
In writing \MATITA{} we have not been hindered by backward compatibility and
we have took advantage of the research results and experiences previously
\end{figure}
Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
-(circle nodes) and \emph{applications} (squared nodes) developed in the HELM
-project. Each node is annotated with the number of lines of source code
-(comprising comments).
+(circle nodes) and \emph{applications} (squared nodes) developed in the
+\HELM{} project. Each node is annotated with the number of lines of
+source code (comprising comments).
-Applications and \components{} depend over other \components{} forming a
+Applications and \components{} depend on other \components{} forming a
directed acyclic graph (DAG). Each \component{} can be decomposed in
-a a set of \emph{modules} also forming a DAG.
+a set of \emph{modules} also forming a DAG.
Modules and \components{} provide coherent sets of functionalities
at different scales. Applications that require only a few functionalities
-depend on a restricted set of \components{}.
+depend on a restricted set of \components.
Only the proof assistant \MATITA{} and the \WHELP{} search engine are
-applications meant to be used directly by the user. All the other applications
-are Web services developed in the HELM and MoWGLI projects and already described
-elsewhere. In particular:
+applications meant to be used directly by the user; all the other applications
+are Web services developed in the \HELM{} and \MOWGLI{} projects. The
+following applications have already been described elsewhere:
\begin{itemize}
- \item The \emph{\GETTER} is a Web service to retrieve an (XML) document
- from a physical location (URL) given its logical name (URI). The Getter is
- responsible of updating a table that maps URIs to URLs. Thanks to the Getter
- it is possible to work on a logically monolithic library that is physically
- distributed on the network. More information on the Getter can be found
- in~\cite{zack-master}.
- \item \emph{\WHELP} is a search engine to index and locate mathematical
- notions (axioms, theorems, definitions) in the logical library managed
- by the Getter. Typical examples of a query to Whelp are queries that search
- for a theorem that generalize or instantiate a given formula, or that
- can be immediately applied to prove a given goal. The output of Whelp is
- an XML document that lists the URIs of a complete set of candidates that
- are likely to satisfy the given query. The set is complete in the sense
- that no notion that actually satisfies the query is thrown away. However,
- the query is only approximated in the sense that false matches can be
- returned. Whelp has been described in~\cite{whelp}.
- \item \emph{\UWOBO} is a Web service that, given the URI of a mathematical
- notion in the distributed library, renders it according to the user provided
- two dimensional mathematical notation. \UWOBO{} may also embed the rendering
- of mathematical notions into arbitrary documents before returning them.
- The Getter is used by \UWOBO{} to retrieve the document to be rendered.
- \UWOBO{} has been described in~\cite{zack-master}.
- \item The \emph{Proof Checker} is a Web service that, given the URI of
- notion in the distributed library, checks its correctness. Since the notion
- is likely to depend in an acyclic way over other notions, the proof checker
- is also responsible of building in a top-down way the DAG of all
- dependencies, checking in turn every notion for correctness.
- The proof checker has been described in~\cite{zack-master}.
- \item The \emph{Dependency Analyzer} is a Web service that can produce
- a textual or graphical representation of the dependencies of an object.
- The dependency analyzer has been described in~\cite{zack-master}.
+
+ \item The \emph{\GETTER}~\cite{zack-master} is a Web service to
+ retrieve an (XML) document from a physical location (URL) given its
+ logical name (URI). The Getter is responsible of updating a table that
+ maps URIs to URLs. Thanks to the Getter it is possible to work on a
+ logically monolithic library that is physically distributed on the
+ network.
+
+ \item \emph{\WHELP}~\cite{whelp} is a search engine to index and
+ locate mathematical concepts (axioms, theorems, definitions) in the
+ logical library managed by the Getter. Typical examples of
+ \WHELP{} queries are those that search for a theorem that generalize or
+ instantiate a given formula, or that can be immediately applied to
+ prove a given goal. The output of Whelp is an XML document that lists
+ the URIs of a complete set of candidates that are likely to satisfy
+ the given query. The set is complete in the sense that no concept that
+ actually satisfies the query is thrown away. However, the query is
+ only approximated in the sense that false matches can be returned.
+
+ \item \emph{\UWOBO}~\cite{zack-master} is a Web service that, given the
+ URI of a mathematical concept in the distributed library, renders it
+ according to the user provided two dimensional mathematical notation.
+ \UWOBO{} may also inline the rendering of mathematical concepts into
+ arbitrary documents before returning them. The Getter is used by
+ \UWOBO{} to retrieve the document to be rendered.
+
+ \item The \emph{Proof Checker}~\cite{zack-master} is a Web service
+ that, given the URI of a concept in the distributed library, checks its
+ correctness. Since the concept is likely to depend in an acyclic way
+ on other concepts, the proof checker is also responsible of building
+ in a top-down way the DAG of all dependencies, checking in turn every
+ concept for correctness.
+
+ \item The \emph{Dependency Analyzer}~\cite{zack-master} is a Web
+ service that can produce a textual or graphical representation of the
+ dependencies of a concept.
+
\end{itemize}
The dependency of a \component{} or application over another \component{} can
be satisfied by linking the \component{} in the same executable.
For those \components{} whose functionalities are also provided by the
aforementioned Web services, it is also possible to link stub code that
-forwards the request to a remote Web service. For instance, the Getter
-is just a wrapper to the \GETTER{} \component{} that allows the
-\component{} to be used as a Web service. \MATITA{} can directly link the code
-of the \GETTER{} \component, or it can use a stub library with the same
-API that forwards every request to the Getter.
+forwards the request to a remote Web service. For instance, the
+\GETTER{} application is just a wrapper to the \GETTER{} \component{}
+that allows it to be used as a Web service. \MATITA{} can directly link
+the code of the \GETTER{} \component, or it can use a stub library with
+the same API that forwards every request to the Web service.
To better understand the architecture of \MATITA{} and the role of each
-\component, we can focus on the representation of the mathematical information.
-\MATITA{} is based on (a variant of) the Calculus of (Co)Inductive
-Constructions (CIC). In CIC terms are used to represent mathematical
-formulae, types and proofs. \MATITA{} is able to handle terms at
-four different levels of specification. On each level it is possible to provide
-a different set of functionalities. The four different levels are:
-fully specified terms; partially specified terms;
-content level terms; presentation level terms.
+\component, we can focus on the representation of the mathematical
+information. In CIC terms are used to represent mathematical formulae,
+types and proofs. \MATITA{} is able to handle terms at four different
+levels of specification. On each level it is possible to provide a
+different set of functionalities. The four different levels are: fully
+specified terms; partially specified terms; content level terms;
+presentation level terms.
\subsection{Fully specified terms}
\label{sec:fullyintro}
\emph{Fully specified terms} are CIC terms where no information is
missing or left implicit. A fully specified term should be well-typed.
- The mathematical notions (axioms, definitions, theorems) that are stored
+ The mathematical concepts (axioms, definitions, theorems) that are stored
in our mathematical library are fully specified and well-typed terms.
Fully specified terms are extremely verbose (to make type-checking
decidable). Their syntax is fixed and does not resemble the usual
consumption.
The \texttt{cic} \component{} defines the data type that represents CIC terms
- and provides a parser for terms stored in an XML format.
+ and provides a parser for terms stored in XML format.
The most important \component{} that deals with fully specified terms is
\texttt{cic\_proof\_checking}. It implements the procedure that verifies
\emph{conversion} judgement that verifies if two given terms are
computationally equivalent (i.e. they share the same normal form).
- Terms may reference other mathematical notions in the library.
+ Terms may reference other mathematical concepts in the library.
One commitment of our project is that the library should be physically
distributed. The \GETTER{} \component{} manages the distribution,
providing a mapping from logical names (URIs) to the physical location
- of a notion (an URL). The \texttt{urimanager} \component{} provides the URI
+ of a concept (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{}
\component{} every time it needs to retrieve the definition of a mathematical
- notion referenced by a term that is being type-checked.
+ concept referenced by a term that is being type-checked.
- The Proof Checker is the Web service that provides an interface
+ The Proof Checker application is the Web service that provides an interface
to the \texttt{cic\_proof\_checking} \component.
- We use metadata and a sort of crawler to index the mathematical notions
- in the distributed library. We are interested in retrieving a notion
+ We use metadata to index the mathematical concepts
+ in the distributed library. We are interested in retrieving a concept
by matching, instantiation or generalization of a user or system provided
mathematical formula. Thus we need to collect metadata over the fully
specified terms and to store the metadata in some kind of (relational)
database for later usage. The \texttt{hmysql} \component{} provides
a simplified
- interface to a (possibly remote) MySql database system used to store the
- metadata. The \texttt{metadata} \component{} defines the data type of the
- metadata
+ interface to a (possibly remote) MySQL\footnote{\url{http://www.mysql.com/}}
+ database system used to store the metadata.
+ The \texttt{metadata} \component{} defines the data type of the metadata
we are collecting and the functions that extracts the metadata from the
- mathematical notions (the main functionality of the crawler).
+ mathematical concepts (the main functionality of the crawler).
The \texttt{whelp} \component{} implements a search engine that performs
approximated queries by matching/instantiation/generalization. The queries
operate only on the metadata and do not involve any actual matching
- (that will be described later on and that is implemented in the
- \texttt{cic\_unification} \component). Not performing any actual matching
- the query only returns a complete and hopefully small set of matching
+ (see the \texttt{cic\_unification} \component{} in
+ Sect.~\ref{sec:partiallyintro}). Not performing any actual matching
+ a query only returns a complete and hopefully small set of matching
candidates. The process that has issued the query is responsible of
actually retrieving from the distributed library the candidates to prune
out false matches if interested in doing so.
- The Whelp search engine is the Web service that provides an interface to
+ The \WHELP{} application is the Web service that provides an interface to
the \texttt{whelp} \component.
According to our vision, the library is developed collaboratively so that
- changing or removing a notion can invalidate other notions in the library.
- Moreover, changing or removing a notion requires a corresponding change
+ changing or removing a concept can invalidate other concepts in the library.
+ Moreover, changing or removing a concept requires a corresponding change
in the metadata database. The \texttt{library} \component{} is responsible
of preserving the coherence of the library and the database. For instance,
- when a notion is removed, all the notions that depend on it and their
+ when a concept is removed, all the concepts that depend on it and their
metadata are removed from the library. This aspect will be better detailed
in Sect.~\ref{sec:libmanagement}.
\label{sec:partiallyintro}
\emph{Partially specified terms} are CIC terms where subterms can be omitted.
-Omitted subterms can bear no information at all or they may be associated to
-a sequent. The formers are called \emph{implicit terms} and they occur only
-linearly. The latters may occur multiple times and are called
-\emph{metavariables}. An \emph{explicit substitution} is applied to each
-occurrence of a metavariable. A metavariable stand for a term whose type is
+Omitted subterms come in two flavours:
+\emph{implicit terms} that do not require a declaration, but can only occur
+linearly; and \emph{metavariables}~\cite{geuvers-jojgov,munoz} whose declaration
+associates with them a sequent and whose occurrences are coupled with an
+explicit substitution.
+A metavariable stands for a term whose type is
given by the conclusion of the sequent. The term must be closed in the
context that is given by the ordered list of hypotheses of the sequent.
The explicit substitution instantiates every hypothesis with an actual
Partially specified terms are not required to be well-typed. However a
partially specified term should be \emph{refinable}. A \emph{refiner} is
a type-inference procedure that can instantiate implicit terms and
-metavariables and that can introduce \emph{implicit coercions} to make a
+metavariables and that can introduce
+\emph{implicit coercions}~\cite{barthe95implicit} to make a
partially specified term well-typed. The refiner of \MATITA{} is implemented
-in the \texttt{cic\_unification} \component. As the type checker is based on
-the conversion check, the refiner is based on \emph{unification} that is
-a procedure that makes two partially specified term convertible by instantiating
-as few as possible metavariables that occur in them.
+in the \texttt{cic\_unification} \component. In the same way as the
+type checker is based on
+convertibility, the refiner is based on \emph{unification}~\cite{strecker}
+that is a procedure that makes two partially specified term convertible by
+instantiating as few metavariables as possible that occur in them.
Since terms are used in CIC to represent proofs, correct incomplete
proofs are represented by refinable partially specified terms. The metavariables
The \texttt{grafite} \component{} defines the abstract syntax tree (AST) for the
commands of the \MATITA{} proof assistant. Most of the commands are tactics.
Other commands are used to give definitions and axioms or to state theorems
-and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA{}.
+and lemmas. The \texttt{grafite\_engine} \component{} is the core of \MATITA.
It implements the semantics of each command in the grafite AST as a function
from status to status. It implements also an undo function to go back to
previous statuses.
\label{sec:contentintro}
The language used to communicate proofs and especially formulae with the
-user does not only needs to be extendible and accommodate the usual mathematical
-notation. It must also reflect the comfortable degree of imprecision and
-ambiguity that the mathematical language provides.
+user does not only need to be extendible and accommodate the usual mathematical
+notation. It must also reflect the comfortable and suggestive degree of
+notational abuse so typical of the mathematical language.
For instance, it is common practice in mathematics to speak of a generic
equality that can be used to compare any two terms. However, it is well known
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 forces 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
Mathematical Knowledge Management community this imprecise language is called
-the \emph{content level} representation of formulae.
+the \emph{content level}~\cite{adams} representation of formulae.
-In \MATITA{} we provide two translations: from partially specified terms
-to content level terms and the other way around. The first translation can also
-be applied to fully specified terms since a fully specified term is a special
-case of partially specified term where no metavariable or implicit term occurs.
-
-The translation from partially specified terms to content level terms must
+In \MATITA{} we provide translations from partially specified terms
+to content level terms and the other way around.
+The former translation must
discriminate between terms used to represent proofs and terms used to represent
-formulae. The firsts are translated to a content level representation of
-proof steps that can in turn easily be rendered in natural language
-using techniques inspired by~\cite{natural,YANNTHESIS}. The representation
+formulae. Using techniques inspired by~\cite{natural,YANNTHESIS}, the firsts
+are translated to a content level representation of
+proof steps that can in turn 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
-for the representation of content level formulae in an XML extensible format.
+for the representation of content level formulae in an extensible XML format.
The translation to content level is implemented in the
\texttt{acic\_content} \component. Its input are \emph{annotated partially
-specified terms}, that are maximally unshared
+specified terms}, that are
partially specified terms enriched with additional typing information for each
subterm. This information is used to discriminate between terms that represent
proofs and terms that represent formulae. Part of it is also stored at the
content level since it is required to generate the natural language rendering
-of proofs. The terms need to be maximally unshared (i.e. they must be a tree
-and not a DAG). The reason is that to the occurrences of a subterm in
-two different positions we need to associate different typing informations.
-This association is made easier when the term is represented as a tree since
-it is possible to label each node with an unique identifier and associate
-the typing information using a map on the identifiers.
-The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
+of proofs.
+The \texttt{cic\_acic} \component{} annotates terms. It is used
by the \texttt{library} \component{} since fully specified terms are stored
in the library in their annotated form.
is guided by an \emph{interpretation}, that is a function that chooses for
every ambiguous formula one partially specified term. The
\texttt{cic\_disambiguation} \component{} implements the
-disambiguation algorithm we presented in~\cite{disambiguation} that is
-responsible of building in an efficient way the set of all ``correct''
+disambiguation algorithm presented in~\cite{disambiguation} that is
+responsible of building in an efficient way the set of all correct
interpretations. An interpretation is correct if the partially specified term
obtained using the interpretation is refinable.
-In Sect.~\ref{sec:partiallyintro} the last section we described the semantics of
+In Sect.~\ref{sec:partiallyintro} we described the semantics of
a command as a
-function from status to status. We also suggested that the formulae in a
+function from status to status. We also hinted 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
of $x$ to be replaced is located, its context is unknown. Since $y^2$ must
The elegant solution we have implemented consists in representing terms
in a command as functions from a context to a partially refined term. The
function is obtained by partially applying our disambiguation function to
-the content term to be disambiguated. Our solution should be compared with
-the one adopted in the \COQ{} system, where ambiguity is only relative to
-De Brujin indexes.
-In \COQ{} variables can be bound either by name or by position. A term
+the content level term to be disambiguated. Our solution should be compared with
+the one adopted in the \COQ{} system (where ambiguity is only relative to
+De Bruijn indexes).
+In \COQ, variables can be bound either by name or by position. A term
occurring in a command has all its variables bound by name to avoid the need of
-a context during disambiguation. Moreover, this makes more complex every
+a context during disambiguation. This makes more complex every
operation over terms (i.e. according to our architecture every module that
depends on \texttt{cic}) since the code must deal consistently with both kinds
-of binding. Also, this solution cannot cope with other forms of ambiguity (as
-the context dependent meaning of the exponent in the previous example).
+of binding. Moreover, this solution cannot cope with other forms of ambiguity
+(as the context dependent meaning of the exponent in the previous example).
\subsection{Presentation level terms}
\label{sec:presentationintro}
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
+particularly interesting since it allows the implementation of \emph{semantic
selection}.
Semantic selection is a technique that consists in enriching the presentation
Once the rendering of a lower level term is
selected it is possible for the application to retrieve the pointer to the
lower level term. An example of applications of semantic selection is
-\emph{semantic cut\&paste}: the user can select an expression and paste it
+\emph{semantic copy \& paste}: the user can select an expression and paste it
elsewhere preserving its semantics (i.e. the partially specified term),
possibly performing some semantic transformation over it (e.g. renaming
variables that would be captured or lambda-lifting free variables).
These mechanisms will be further discussed in Sect.~\ref{sec:disambiguation}.
Finally, the \texttt{grafite\_parser} \component{} implements a parser for
-the concrete syntax of the commands of \MATITA. The parser process a stream
+the concrete syntax of the commands of \MATITA. The parser processes a stream
of characters and returns a stream of abstract syntax trees (the ones
defined by the \texttt{grafite} component and whose semantics is given
by \texttt{grafite\_engine}). When the parser meets a command that changes
\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.\NOTE{\TODO{manca la passata verso HTML}}
+browser.
The \components{} not yet described (\texttt{extlib}, \texttt{xml},
\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are
\label{sec:library}
A proof assistant provides both an interface to interact with its library and
-an \emph{authoring} interface to develop new proofs and theories. According
+an 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.
-The only relation implicitly kept between the notions are the logical,
+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
Scripts are not seen as constituents of the library. They are not published
and indexed, so they cannot be searched or browsed using \HELM{} tools.
However, they play a central role for the maintenance of the library.
-Indeed, once a notion is invalidated, the only way to restore it is to
+Indeed, once a concept 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.
+group concepts together. They also constitute a less fine grained clustering
+of concepts for invalidation.
In the rest of this section we present in more details the functionalities of
\MATITA{} related to library management and exploitation.
library. To this aim, \MATITA{} uses a sophisticated indexing mechanism
for mathematical concepts, based on a rich metadata set that has been
tuned along the European project \MOWGLIIST{} \MOWGLI. The metadata
-set, and the searching facilites built on top of them --- collected
+set, and the searching facilities built on top of them --- collected
in the so called \WHELP{} search engine --- have been
extensively described in~\cite{whelp}. Let us just recall here that
-the \WHELP{} metadata model is essentially based a single ternary relation
-\REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
- given position $p$, where the position specify the place of the
+the \WHELP{} metadata model is essentially based on a single ternary relation
+\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
indexed, and becomes immediately visible in the library. Several
interesting and innovative features of \MATITA{} described in the following
sections rely in a direct or indirect way on its metadata system and
-the search features. Here, we shall just recall some of its most
+the search functionalities. 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 negligible 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
(based on the pattern matching functionality of \WHELP); if this is the case,
a warning is raised to the user. At present, the notion of equivalence
adopted by \MATITA{} is convertibility, but we may imagine to weaken it
-in the future, covering for instance isomorphisms.
+in the future, covering for instance isomorphisms~\cite{delahaye}.
Another useful \WHELP{} operation is \HINT; we may invoke this query
at any moment during the authoring of a proof, resulting in the list
of 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.
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
+The drift is still very large for
+proofs~\cite{debrujinfactor}, while better results may be achieved for
+mathematical formulae. In \MATITA{} formulae can be written using a
+\TeX-like 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
+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
expressiveness.
-\subsubsection{Disambiguation aliases}
+\subsubsection{Disambiguation preferences}
\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:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The symbol \OP{<} is likely to be overloaded in the library
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
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
+Preferences can be explicitly given in the script (using the \texttt{alias}
+command), but
are also implicitly added when a new concept is introduced (\emph{implicit
-preferences}) or after a sucessfull disambiguation that did not require
+preferences}) or after a successful disambiguation that did not require
user interaction. Explicit preferences are added automatically by \MATITA{} to
record the disambiguation choices of the user. For instance, after the
disambiguation of the command above, the script is altered as follows:
\begin{grafite}
alias symbol "lt" = "integer 'less than'".
theorem Zlt_compat:
- \forall x, y, z. x < y \to y < z \to x < z.
+ \forall x,y,z. x < y \to y < z \to x < z.
\end{grafite}
The ``alias'' command in the example sets the preferred alias for the
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
+To reduce the likelihood 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.
+The inclusion mechanism is thus sensibly different from that of other systems
+where concepts are effectively loaded and made visibible by inclusion; in \MATITA{}
+all concepts are always visible, and inclusion, that is optional, is only used
+to set up preferences.
-Preferences can be changed. For instance, at the start of the development
+Preferences can be changed. For instance, at the beginning 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.
Consider, for example:
\begin{grafite}
theorem Zlt_mono:
- \forall x, y, k. x < y \to x < y + k.
+ \forall x,y,k. x < y \to x < y + k.
\end{grafite}
No refinable partially specified term corresponds to the preferences:
\OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
limitation we organized disambiguation in \emph{multiple passes}: when the
-disambiguator fails, disambiguation is tried again with a less strict set of
+disambiguator fails, disambiguation is tried again with a less restrictive 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
+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
available in the library are considered.
-\TODO{rivedere questo periodo\ldots}
The rationale behind this choice is trying to respect user preferences in early
passes that complete quickly in case of failure; later passes are slower but
have more chances of success.
\subsubsection{Operator instances}
\label{sec:disambinstances}
-Consider now the following theorem:
+Consider now the following theorem, where \texttt{pos} injects natural numbers
+into positive integers:
+
\begin{grafite}
theorem lt_to_Zlt_pos_pos:
- \forall n, m: nat. n < m \to pos n < pos m.
+ \forall n,m: nat. n < m \to pos n < pos m.
\end{grafite}
and assume that there exist in the library aliases for \OP{<} over natural
numbers and over integer numbers. None of the passes described above is able to
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 instances does not constraint the choice of the others). For
+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
-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''.
+%\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
+%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
+Instance-dependent preferences are meaningful only for the term whose
+disambiguation generated them. For this reason we call them \emph{one-shot
preferences} and \MATITA{} does not use them to disambiguate further terms in
the script.
Consider the following theorem about derivation:
\begin{grafite}
theorem power_deriv:
- \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+ \forall n: nat, x: R. d x^n dx = n * x^(n - 1).
\end{grafite}
and assume that in the library there is an alias mapping \OP{\^} to a partially
specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
right hand side of the equality need to be ``injected'' from \texttt{nat} to
-\texttt{R}. The refiner of \MATITA{} supports \emph{implicit coercions} for
+\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
-\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
-two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
-among the possible partially specified term choices. For this reason we always
-attempt a disambiguation pass which require the refiner not to use the coercions
-before attempting a coercion-enabled pass.
-
-The choice of whether implicit coercions are enabled or not interact with the
+Implicit coercions are not always desirable. For example, consider the term
+\texttt{\TEXMACRO{forall} x. x < x + 1} and assume that the preferences for \OP{<}
+and \OP{+} are over real numbers. The expected interpretation assignes the
+type \texttt{R} to \texttt{x}.
+However, if we had a coercion from natural to real numbers an alternative
+interpretation is to assign the type \texttt{nat} to \texttt{x} inserting the coercion
+as needed. Clearly, the latter interpretation looks artificial and
+for this reason we enable coercions only in case of failure of previous
+attempts.
+
+The choice of whether implicit coercions are enabled or not interacts 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.
+instances. In case there exists a coercion from natural numbers to positive
+integers ({\texttt{pos} itself), the command
+can be disambiguated as
+\texttt{\TEXMACRO{forall} n,m: nat. pos n < pos m \TEXMACRO{to} pos n < pos m}.
+This is not the expected interpretation;
+by this and similar examples we choose to always prefer fresh
+instances over implicit coercions.
\subsubsection{Disambiguation passes}
\label{sec:disambpasses}
-According to the criteria described above in \MATITA{} we choose to perform the
-sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
-our experience that choice gives reasonable performance and minimize the need of
-user interaction during the disambiguation.
+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 reduces the need
+of user interaction during the disambiguation.
\begin{table}[ht]
- \caption{Disambiguation passes sequence\strut}
- \label{tab:disambpasses}
\begin{center}
\begin{tabular}{c|c|c|c}
\multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
- & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Preferences}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\raisebox{-1.5ex}{\textbf{Preferences}}}
& \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
& \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
\hline
\PASS & Library-preferences & Fresh instances & Enabled
\end{tabular}
\end{center}
+ \caption{Disambiguation passes sequence\strut}
+ \label{tab:disambpasses}
\end{table}
-\subsection{Generation and invalidation}
+\subsection{Invalidation and regeneration}
\label{sec:libmanagement}
-The aim of this section is to describe the way \MATITA{}
-preserves the consistency and the availability of the library
-using the \WHELP{} technology, in response to the user alteration or
-removal of mathematical objects.
-
-As already sketched in Sect.~\ref{sec:fullyintro} what we generate
-from a script is split among two storage media, a
-classical filesystem and a relational database. The former is used to
-store the XML encoding of the objects defined in the script, the
-disambiguation aliases and the interpretation and notational convention defined,
-while the latter is used to store all the metadata needed by
-\WHELP{}.
-
-While the consistency of the data store in the two media has
-nothing to do with the nature of
-the content of the library and is thus uninteresting (but really
-tedious to implement and keep bug-free), there is a deeper
-notion of mathematical consistency we need to provide. Each object
-must reference only defined object (i.e. each proof must use only
-already proved theorems).
-
-We will focus on how \MATITA{} ensures the interesting kind
-of consistency during the formalization of a mathematical theory,
+%The aim of this section is to describe the way \MATITA{}
+%preserves the consistency and the availability of the library
+%using the \WHELP{} technology, in response to the user alteration or
+%removal of mathematical objects.
+%
+%As already sketched in Sect.~\ref{sec:fullyintro} what we generate
+%from a script is split among two storage media, a
+%classical filesystem and a relational database. The former is used to
+%store the XML encoding of the objects defined in the script, the
+%disambiguation aliases and the interpretation and notational convention defined,
+%while the latter is used to store all the metadata needed by
+%\WHELP.
+%
+%While the consistency of the data store in the two media has
+%nothing to do with the nature of
+%the content of the library and is thus uninteresting (but really
+%tedious to implement and keep bug-free), there is a deeper
+%notion of mathematical consistency we need to provide. Each object
+%must reference only defined object (i.e. each proof must use only
+%already proved theorems).
+
+In this section we will focus on how \MATITA{} ensures the library
+consistency during the formalization of a mathematical theory,
giving the user the freedom of adding, removing, modifying objects
without loosing the feeling of an always visible and browsable
library.
-\subsubsection{Compilation}
+\subsubsection{Invalidation}
+
+Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
-The typechecker component guarantees that if an object is well typed
-it depends only on well typed objects available in the library,
-that is exactly what we need to be sure that the logic consistency of
-the library is preserved. We have only to find the right order of
-compilation of the scripts that compose the user development.
+The first one is the computation of all the concepts that recursively
+depend on the ones we are invalidating. It can be performed
+from the metadata stored in the relational database.
+This technique is the same used by the \emph{Dependency Analyzer}
+and is described in~\cite{zack-master}.
+
+The second phase is the removal of all the results of the generation,
+metadata included.
+
+\subsubsection{Regeneration}
+
+%The typechecker component guarantees that if an object is well typed
+%it depends only on well typed objects available in the library,
+%that is exactly what we need to be sure that the logic consistency of
+%the library is preserved.
+
+To regenerate an invalidated part of the library \MATITA{} re-executes
+the 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 files that compose the development and
-outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+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.\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 compilation
+script files can be found) and \MATITA{} will handle all the generation
related tasks, including dependencies calculation.
-To compute dependencies it is enough to look at the script files for
-inclusions of other parts of the development or for explicit
-references to other objects (i.e. with explicit aliases, see
-\ref{sec:disambaliases}).
-
-The output of the compilation is immediately available to the user
-trough the \WHELP{} technology, since all metadata are stored in a
-user-specific area of the database where the search engine has read
-access, and all the automated tactics that operates on the whole
-library, like \AUTO, have full visibility of the newly defined objects.
-
-Compilation is rather simple, and the only tricky case is when we want
-to compile again the same script, maybe after the removal of a
-theorem. Here the policy is simple: clean the output before recompiling.
-As we will see in the next section cleaning will ensure that
-there will be no theorems in the development that depends on the
-removed items.
-
-\subsubsection{Cleaning}
-
-With the term ``cleaning'' we mean the process of removing all the
-results of an object compilation. In order to keep the consistency of
-the library, cleaning an object requires the (recursive) cleaning
-of all the objects that depend on it (\emph{reverse dependencies}).
-
-The calculation of the reverse dependencies can be computed in two
-ways, using the relational database or using a simpler set of metadata
-that \MATITA{} saves in the filesystem as a result of compilation. The
-former technique is the same used by the \emph{Dependency Analyzer}
-described in~\cite{zack-master} and really depends on a relational
-database.
-The latter is a fall-back in case the database is not
-available.\footnote{Due to the complex deployment of a large piece of
-software like a database, it is a common practice for the \HELM{} team
-to use a shared remote database, that may be unavailable if the user
-workstation lacks network connectivity.} This facility has to be
-intended only as a fall-back, since the queries of the \WHELP{}
-technology depend require a working database.
+To compute dependencies it is enough to look at the script files for
+literal of included explicit disambiguation preferences
+(see Sect.~\ref{sec:disambaliases}).
-Cleaning guarantees that if an object is removed there are no dandling
-references to it, and that the part of the library still compiled is
-consistent. Since cleaning involves the removal of all the results of
-the compilation, metadata included, the library browsable trough the
-\WHELP{} technology is always kept up to date.
+The re-execution of a script to regenerate part of the library
+requires the preliminary invalidation of the concepts generated by the
+script.
\subsubsection{Batch vs Interactive}
\MATITA{} includes an interactive authoring interface and a batch
-``compiler'' (\MATITAC). Only the former is intended to be used directly by the
-user, the latter is automatically invoked when a
-part of the user development is required (for example issuing an
-\texttt{include} command) but not yet compiled.
-
-While they share the same engine for compilation and cleaning, they
-provide different granularity. The batch compiler is only able to
-compile a whole script and similarly to clean only a whole script
-(together with all the other scripts that rely on an object defined in
-it). The interactive interface is able to execute single steps of
-compilation, that may include the definition of an object, and
-similarly to undo single steps. Note that in the latter case there is
-no risk of introducing dangling references since the \MATITA{} user
-interface inhibit undoing a step which is not the last executed.
+``compiler'' (\MATITAC).
+
+Only the former is intended to be used directly by the
+user, the latter is automatically invoked by \MATITA{}
+to regenerate parts of the library previously invalidated.
+
+While they share the same engine for generation and invalidation, they
+provide different granularity. \MATITAC{} is only able to re-execute a
+whole script and similarly to invalidate all the concepts generated
+by a script (together with all the other scripts that rely on a concept defined
+in it).
\subsection{Automation}
\label{sec:automation}
-\TODO{sezione sull'automazione}
+In the long run, one would expect to work with a proof assistant
+like \MATITA, using only three basic tactics: \TAC{intro}, \TAC{elim},
+and \TAC{auto}
+(possibly integrated by a moderate use of \TAC{cut}). The state of the art
+in automated deduction is still far away from this goal, but
+this is one of the main development direction of \MATITA.
+
+Even in this field, the underlying philosophy of \MATITA{} is to
+free the user from any burden relative to the overall management
+of the library. For instance, in \COQ, the user is responsible to
+define small collections of theorems to be used as a parameter
+by the \TAC{auto} tactic;
+in \MATITA, it is the system itself that automatically retrieves, from
+the whole library, a subset of theorems worth to be considered
+according to the signature of the current goal and context.
+
+The basic tactic merely iterates the use of the \TAC{apply} tactic
+(with no \TAC{intro}). The search tree may be pruned according to two
+main parameters: the \emph{depth} (whit the obvious meaning), and the
+\emph{width} that is the maximum number of (new) open goals allowed at
+any instant. \MATITA{} has only one notion of metavariable, corresponding
+to the so called existential variables of \COQ; so, \MATITA's \TAC{auto}
+tactic should be compared with \COQ's \TAC{EAuto} tactic.
+
+Recently we have extended automation with paramodulation based
+techniques. At present, the system works reasonably well with
+equational rewriting, where the notion of equality is parametric
+and can be specified by the user: the system only requires
+a proof of {\em reflexivity} and {\em paramodulation} (or rewriting,
+as it is usually called in the proof assistant community).
+
+Given an equational goal, \MATITA{} recovers all known equational facts
+from the library (and the local context), applying a variant of
+the so called {\em given-clause algorithm}~\cite{paramodulation},
+that is the the procedure currently used by the majority of modern
+automatic theorem provers.
+
+The given-clause algorithm is essentially composed by an alternation
+of a \emph{saturation} phase and a \emph{demodulation} phase.
+The former derives new facts by a set of active
+facts and a new \emph{given} clause suitably selected from a set of passive
+equations. The latter tries to simplify the equations
+orienting them according to a suitable weight associated to terms.
+\MATITA{} currently supports several different weighting functions
+comprising Knuth-Bendix ordering (kbo) and recursive path ordering (rpo),
+that integrates particularly well with normalization.
+
+Demodulation alone is already a quite powerful technique, and
+it has been turned into a tactic by itself: the \TAC{demodulate}
+tactic, which can be seen as a kind of generalization of \TAC{simplify}.
+The following portion of script describes two
+interesting cases of application of this tactic (both of them relying
+on elementary arithmetic equations):
+
+\begin{grafite}
+theorem example1:
+ \forall x: nat. (x+1)*(x-1) = x*x - 1.
+intro.
+apply (nat_case x);
+ [ simplify; reflexivity
+ | intro; demodulate; reflexivity ]
+qed.
+\end{grafite}
+
+\begin{grafite}
+theorem example2:
+ \forall x,y: nat. (x+y)*(x+y) = x*x + 2*x*y + y*y.
+intros; demodulate; reflexivity
+qed.
+\end{grafite}
+
+In the future we expect to integrate applicative and equational
+rewriting. In particular, the overall idea would be to integrate
+applicative rewriting with demodulation, treating saturation as an
+operation to be performed in batch mode, e.g. during the night.
\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
+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 two 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 statement
+\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 \def
+ \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}
-The authoring interface of \MATITA{} is very similar to Proof General. We
+The authoring interface of \MATITA{} is very similar to Proof
+General~\cite{proofgeneral}. We
chose not to build the \MATITA{} UI over Proof General for two reasons. First
of all we wanted to integrate our XML-based rendering technologies, mainly
-\GTKMATHVIEW{}. At the time of writing Proof General supports only text based
-rendering.\footnote{This may change with the future release of Proof General
-based on Eclipse, but is not yet the case.} The second reason is that we wanted
-to build the \MATITA{} UI on top of a state-of-the-art and widespread toolkit
-as GTK is.
+\GTKMATHVIEW, in the UI.
+At the time of writing Proof General supports only text based
+rendering.\footnote{This may change with future releases of Proof General
+based on Eclipse (\url{http://www.eclipse.org/}), but is not yet the
+case.} The second reason is that we wanted
+to build the \MATITA{} UI on top of a state-of-the-art and widespread graphical
+toolkit as \GTK{} is.
Fig.~\ref{fig:screenshot} is a screenshot of the \MATITA{} authoring interface,
featuring two windows. The background one is very like to the Proof General
interface. The main difference is that we use the \GTKMATHVIEW{} widget to
render sequents. Since \GTKMATHVIEW{} renders \MATHML{} markup we take
advantage of the whole bidimensional mathematical notation. The foreground
-window is an instance of the cicBrowser used to render the proof being
-developed.
+window is an instance of the cicBrowser (see Sect.~\ref{sec:library}) used to
+render in natural language the proof being developed.
-Note that the syntax used in the script view is \TeX-like, however Unicode is
-fully supported so that mathematical glyphs can be input as such.
+Note that the syntax used in the script view is \TeX-like, but
+Unicode\footnote{\url{http://www.unicode.org/}} is
+also fully supported so that mathematical glyphs can be input as such.
\begin{figure}[!ht]
\begin{center}
\includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
- \caption{\MATITA{} look and feel\strut}
+ \caption{Authoring interface\strut}
\label{fig:screenshot}
\end{center}
\end{figure}
concise and widespread textual syntax.
Keeping pointers from the presentations level terms down to the
-partially specified ones \MATITA{} enable direct manipulation of
+partially specified ones, \MATITA{} enables 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
+Fig.~\ref{fig:directmanip}, where we clicked on $\nmid$, symbols
encoding complex notations retain all the hyperlinks of constants or
constructors used in the notation.
Fig.~\ref{fig:directmanip} is thus possible to select the subterm
$\mathrm{prime}~n$, whereas it would not be possible to select
$\to n$ since the former denotes an application while the
-latter it not a subterm. Once a meaningful (sub)term has been
-selected actions can be done on it like reductions or tactic
-applications.
+latter is not a subterm. Once a meaningful (sub)term has been
+selected actions like reductions or tactic applications can be performed on it.
\begin{figure}[!ht]
\begin{center}
In \MATITA{} \emph{patterns} are textual representations of selections.
Users can select using the GUI and then ask the system to paste the
-corresponding pattern in this script, but more often this process is
-transparent: once an action is performed on a selection, the corresponding
+corresponding pattern in this script. More often this process is
+transparent to the user: once an action is performed on a selection,
+the corresponding
textual command is computed and inserted in the script.
\subsubsection{Pattern syntax}
\NT{wanted}; their concrete syntax is reported in Tab.~\ref{tab:pathsyn}.
\NT{sequent\_path} mocks-up a sequent, discharging unwanted subterms
-with $?$ and selecting the interesting parts with the placeholder
-$\%$. \NT{wanted} is a term that lives in the context of the
+with \OP{?} and selecting the interesting parts with the placeholder
+\OP{\%}. \NT{wanted} is a term that lives in the context of the
placeholders.
Textual patterns produced from a graphical selection are made of the
\subsubsection{Pattern evaluation}
Patterns are evaluated in two phases. The first selects roots
-(subterms) of the sequent, using the $\NT{sequent\_path}$, while the
-second searches the $\NT{wanted}$ term starting from these roots.
+(subterms) of the sequent, using the \NT{sequent\_path}, while the
+second searches the \NT{wanted} term starting from that roots.
% Both are optional steps, and by convention the empty pattern selects
% the whole conclusion.
\begin{description}
\item[Phase 1]
- concerns only the $[~\verb+in+~\NT{sequent\_path}~]$
- part of the syntax. $\NT{ident}$ is an hypothesis name and
- selects the assumption where the following optional $\NT{multipath}$
- will operate. \verb+\vdash+ can be considered the name for the goal.
- If the whole pattern is omitted, the whole goal will be selected.
- If one or more hypotheses names are given the selection is restricted to
- these assumptions. If a $\NT{multipath}$ is omitted the whole
- assumption is selected. Remember that the user can be mostly
- unaware of this syntax, since the system is able to write down a
- $\NT{sequent\_path}$ starting from a visual selection.
- \NOTE{Questo ancora non va in matita}
-
- A $\NT{multipath}$ is a CIC term in which a special constant $\%$
- is allowed.
- The roots of discharged subterms are marked with $?$, while $\%$
- is used to select roots. The default $\NT{multipath}$, the one that
- selects the whole term, is simply $\%$.
- Valid $\NT{multipath}$ are, for example, $(?~\%~?)$ or $\%~\verb+\to+~(\%~?)$
- that respectively select the first argument of an application or
- the source of an arrow and the head of the application that is
- found in the arrow target.
-
- The first phase not only selects terms (roots of subterms) but
- determines also their context that will be eventually used in the
- second phase.
+ concerns only \NT{sequent\_path}. \NT{ident} is an hypothesis name and selects
+ the assumption where the following optional \NT{multipath} will operate.
+ \verb+\vdash+ can be considered the name for the goal. If the whole pattern
+ is omitted, the whole goal will be selected. If one or more hypothesis names
+ are given, the selection is restricted to that assumptions. If a
+ $\NT{multipath}$ is omitted the whole assumption is selected. Remember that
+ the user can be mostly unaware of patterns concrete syntax, since the system
+ is able to write down a \NT{sequent\_path} starting from a graphical
+ selection.
+
+ A \NT{multipath} is a CIC term in which a special constant \OP{\%} is allowed.
+ The roots of discharged subterms are marked with \OP{?}, while \OP{\%} is used
+ to select roots. The default \NT{multipath}, the one that selects the whole
+ term, is simply \OP{\%}. Valid \NT{multipath} are, for example, \texttt{(? \%
+ ?)} or \texttt{\% \TEXMACRO{to} (\% ?)} that respectively select the first
+ argument of an application or the source of an arrow and the head of the
+ application that is found in the arrow target.
+
+ This phase not only selects terms (roots of subterms) but determines also
+ their context that will be possibly used in the next phase.
\item[Phase 2]
- plays a role only if the $[~\verb+match+~\NT{wanted}~]$
- part is specified. From the first phase we have some terms, that we
- will see as subterm roots, and their context. For each of these
- contexts the $\NT{wanted}$ term is disambiguated in it and the
- corresponding root is searched for a subterm that can be unified to
- $\NT{wanted}$. The result of this search is the selection the
+ plays a role only if \NT{wanted} is specified. From the first phase we
+ have some terms, that we will use as roots, and their context.
+ For each of these contexts the \NT{wanted} term is disambiguated in it
+ and the corresponding root is searched for a subterm that can be unified to
+ \NT{wanted}. The result of this search is the selection the
pattern represents.
\end{description}
\subsubsection{Examples}
-%To explain how the first phase works let us give an example. Consider
-%you want to prove the uniqueness of the identity element $0$ for natural
-%sum, and that you can rely on the previously demonstrated left
-%injectivity of the sum, that is $inj\_plus\_l:\forall x,y,z.x+y=z+y \to x =z$.
-%Typing
-%\begin{grafite}
-%theorem valid_name: \forall n,m. m + n = n \to m = O.
-% intros (n m H).
-%\end{grafite}
-%\noindent
-Consider the following sequent
-\sequent{
-n:nat\\
-m:nat\\
-H: m + n = n}{
-m=O
-}
-\noindent
-To change the right part of the equivalence of the $H$
-hypothesis with $O + n$ the user selects and pastes it as the pattern
+
+Consider the following sequent:
+\sequent{n: nat\\m: nat\\H: m + n = n}{m = O}
+
+To change the right part of the equality of the $H$
+hypothesis with $O + n$, the user selects and pastes it as the pattern
in the following statement.
\begin{grafite}
change in H:(? ? ? %) with (O + n).
\end{grafite}
-\noindent
-To understand the pattern (or produce it by hand) the user should be
-aware that the notation $m+n=n$ hides the term $(eq~nat~(m+n)~n)$, so
-that the pattern selects only the third argument of $eq$.
-The experienced user may also write by hand a concise pattern
-to change at once all the occurrences of $n$ in the hypothesis $H$:
+To understand the pattern (or produce it by hand) the user should be aware that
+the notation $m + n = n$ hides the term $\mathrm{eq}~\mathrm{nat}~(m + n)~n$, so
+that the pattern selects only the third argument of $\mathrm{eq}$.
+
+The experienced user may also write by hand a concise pattern to change at once
+all the occurrences of $n$ in the hypothesis $H$:
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
-\noindent
-In this case the $\NT{sequent\_path}$ selects the whole $H$, while
+
+In this case the \NT{sequent\_path} selects the whole $H$, while
the second phase locates $n$.
The latter pattern is equivalent to the following one, that the system
\begin{grafite}
change in H:(? ? (? ? %) %) with (O + n).
\end{grafite}
-\noindent
-
-\subsubsection{Tactics supporting patterns}
-
-\TODO{mergiare con il successivo facendo notare che i patterns sono una
-interfaccia comune per le tattiche}
-In \MATITA{} all the tactics that can be restricted to subterm of the working
-sequent accept the pattern syntax. In particular these tactics are: simplify,
-change, fold, unfold, generalize, replace and rewrite.
+\subsubsection{Comparison with \COQ{}}
-\NOTE{attualmente rewrite e fold non supportano phase 2. per
-supportarlo bisogna far loro trasformare il pattern phase1+phase2
-in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
-con una pattern\_of(select(pattern))}
+In \MATITA{} all the tactics that act on subterms of the current sequent
+accept pattern arguments. Additional arguments can be disambiguated in the
+contexts of the terms selected by the pattern
+(\emph{context-dependent arguments}).
-\subsubsection{Comparison with \COQ{}}
+%\NOTE{attualmente rewrite e fold non supportano fase 2. per
+%supportarlo bisogna far loro trasformare il pattern phase1+phase2
+%in un pattern phase1only come faccio nell'ultimo esempio. lo si fa
+%con una pattern\_of(select(pattern))}
\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.
+subterms of the current sequent, both relying on the same special syntax to
+identify a term occurrence.
The first way is to use this special syntax to tell the
tactic what occurrences of a wanted term should be affected.
The second is to prepare the sequent with another tactic called
-pattern and then apply the real tactic. Note that the choice is not
+\TAC{pattern} and then apply the real tactic. Note that the choice is not
left to the user, since some tactics needs the sequent to be prepared
with pattern and do not accept directly this special syntax.
-The base idea is that to identify a subterm of the sequent we can
-write it and say that we want, for example, the third and the fifth
-occurrences of it (counting from left to right). In our previous example,
+The idea is that to identify a subterm of the sequent we can
+write it and say that we want, for example, its third and fifth
+occurrences (counting from left to right). In our previous example,
to change only the left part of the equivalence, the correct command
-is:
-
+would be:
\begin{grafite}
change n at 2 in H with (O + n)
\end{grafite}
+meaning that in the hypothesis \texttt{H} the \texttt{n} we want to change is
+the second we encounter proceeding from left to right.
-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
+The tactic \TAC{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:
\begin{grafite}
pattern n at 2 in H
\end{grafite}
-
-would have resulted in this sequent:
-
-\begin{grafite}
- n : nat
- m : nat
- H : (fun n0 : nat => m + n = n0) n
- ============================
- m = 0
-\end{grafite}
-
-where $H$ is $\beta$-expanded over the second $n$
+would have resulted in the sequent:
+\sequent{n: nat\\m : nat\\H: (fun n0: nat => m + n = n0) n}{m = 0}
+where \texttt{H} is $\beta$-expanded over the second \texttt{n}
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)}.
+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 \texttt{x} with \texttt{n} and \texttt{P} with
+\texttt{(fun n0: nat => m + n = n0)}.
-Since rewriting, replacing and several other tactics boils down to
+Since \TAC{rewrite}, \TAC{replace} and several other tactics boils down to
the application of the equality elimination principle, the previous
-trick deals the expected behaviour.
+trick implements the expected behavior.
The idea behind this way of identifying subterms in not really far
from the idea behind patterns, but fails in extending to
-complex notation, since it relays on a mono-dimensional sequent representation.
+complex notation, since it relies 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
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.
+using heavy math notation would have definitively been a bad choice.
+
+In \MATITA{}, tactics accepting pattern arguments can be more expressive than
+the equivalent tactics in \COQ{} since variables bound in the pattern context,
+can occur in context-dependent arguments. For example, consider the sequent:
+\sequent{n: nat\\x: nat\\H: \forall m. n + m*n = x + m}{m = O}
+In \MATITA{} the user can issue the command:
+\begin{grafite}
+change in H: \forall _. (? ? % ?) with (S m) * n.
+\end{grafite}
+to change $n+m*n$ with $(S~m)*n$. To achieve the same effect in \COQ, the
+user is obliged to change the whole hypothesis rewriting its right hand side
+as well.
\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
-will not compare the two different approaches. We will describe the common
-issues of the tactic-based language approach and how \MATITA{} tries to solve
-them.
+The procedural proof language implemented in \MATITA{} is pretty standard,
+with a notable exception for tacticals.
-\subsubsection{Tacticals overview}
+Tacticals first appeared in LCF~\cite{lcf} as higher order tactics.
+They can be seen as control flow constructs like looping, branching,
+error recovery and sequential composition.
-Tacticals first appeared in LCF and can be seen as programming
-constructs, like looping, branching, error recovery or sequential composition.
-The following simple example shows three tacticals in action
+The following simple example shows a \COQ{} script made of four dot-terminated
+commands:
\begin{grafite}
-theorem trivial:
- \forall A,B:Prop.
- A = B \to ((A \to B) \land (B \to A)).
- intros (A B H).
+Theorem trivial:
+ forall A B:Prop,
+ A = B -> ((A -> B) /\ (B -> A)).
+ intros [A B H].
split; intro;
- [ rewrite < H. assumption.
- | rewrite > H. assumption.
- ]
-qed.
+ [ rewrite < H; assumption
+ | rewrite > H; assumption
+ ].
+Qed.
\end{grafite}
-The first is ``\texttt{;}'' that combines the tactic \texttt{split}
-with \texttt{intro}, applying the latter to each goal opened by the
-former. Then we have ``\texttt{[}'' that branches on the goals (here
-we have two goals, the two sides of the logic and).
-The first goal $B$ (with $A$ in the context)
-is proved by the first sequence of tactics
-\texttt{rewrite} and \texttt{assumption}. Then we move to the second
-goal with the separator ``\texttt{|}''. The last tactical we see here
-is ``\texttt{.}'' that is a sequential composition that selects the
-first goal opened for the following tactic (instead of applying it to
-them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
-not considered a tactical, but a sentence terminator (i.e. the
-delimiter of commands the proof assistant executes).
-
-Giving serious examples here is rather difficult, since they are hard
-to read without the interactive tool. To help the reader in
-understanding the following considerations we just give few common
-usage examples without a proof context.
+The third command is an application of the sequencing tactical \OP{$\ldots$~;~$\ldots$},
+that combines the tactic \TAC{split} with the application of the branching
+tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]} to other tactics or tacticals.
-\begin{grafite}
- elim z; try assumption; [ ... | ... ].
- elim z; first [ assumption | reflexivity | id ].
-\end{grafite}
+The usual implementation of tacticals executes them atomically as any
+other command. In \MATITA{} this is not the case: each punctuation
+symbol is executed as a single command.
-The first example goes by induction on a term \texttt{z} and applies
-the tactic \texttt{assumption} to each opened goal eventually recovering if
-\texttt{assumption} fails. Here we are asking the system to close all
-trivial cases and then we branch on the remaining with ``\texttt{[}''.
-The second example goes again by induction on \texttt{z} and tries to
-close each opened goal first with \texttt{assumption}, if it fails it
-tries \texttt{reflexivity} and finally \texttt{id}
-that is the tactic that leaves the goal untouched without failing.
-
-Note that in the common implementation of tacticals both lines are
-compositions of tacticals and in particular they are a single
-statement (i.e. derived from the same non terminal entry of the
-grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
-this is not true, since each atomic tactic or punctuation is considered
-a single statement.
-
-\subsubsection{Common issues of tactic(als)-based proof languages}
-We will examine the two main problems of tactic(als)-based proof script:
+\subsubsection{Common issues of tacticals}
+We will examine the two main problems of procedural proof languages:
maintainability and readability.
-Huge libraries of formal mathematics have been developed, and backward
-compatibility is a really time consuming task. \\
-A real-life example in the history of \MATITA{} was the reordering of
-goals opened by a tactic application. We noticed that some tactics
-were not opening goals in the expected order. In particular the
-\texttt{elim} tactic on a term of an inductive type with constructors
-$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
-\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
-but some theorems about integers were there. The inductive type of
-$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
-induction proofs on this type where written without tacticals and,
-obviously, considering the three induction cases in the wrong order.
-Fixing the behavior of the tactic broke the library and two days of
-work were needed to make it compile again. The whole time was spent in
-finding the list of tactics used to prove the third induction case and
-swap it with the list of tactics used to prove the second case. If
-the proofs was structured with the branch tactical this task could
-have been done automatically.
-
-From this experience we learned that the use of tacticals for
-structuring proofs gives some help but may have some drawbacks in
-proof script readability. We must highlight that proof scripts
-readability is poor by itself, but in conjunction with tacticals it
-can be nearly impossible. The main cause is the fact that in proof
-scripts there is no trace of what you are working on. It is not rare
-for two different theorems to have the same proof script (while the
-proof is completely different).\\
-Bad readability is not a big deal for the user while he is
-constructing the proof, but is considerably a problem when he tries to
-reread what he did or when he shows his work to someone else. The
-workaround commonly used to read a script is to execute it again
-step-by-step, so that you can see the proof goal changing and you can
-follow the proof steps. This works fine until you reach a tactical. A
-compound statement, made by some basic tactics glued with tacticals,
-is executed in a single step, while it obviously performs lot of proof
-steps. In the fist example of the previous section the whole branch
-over the two goals (respectively the left and right part of the logic
-and) result in a single step of execution. The workaround does not work
-anymore unless you de-structure on the fly the proof, putting some
-``\texttt{.}'' where you want the system to stop.\\
-
-Now we can understand the tradeoff between script readability and
-proof structuring with tacticals. Using tacticals helps in maintaining
-scripts, but makes it really hard to read them again, cause of the way
-they are executed.
-
-\MATITA{} uses a language of tactics and tacticals, but tries to avoid
-this tradeoff, alluring the user to write structured proof without
-making it impossible to read them again.
-
-\subsubsection{The \MATITA{} approach: Tinycals}
+Tacticals are not only used to make scripts shorter by factoring out
+common cases and repeating commands. They are the primary way of making
+scripts more maintainable. They also have the well-known duty of
+structuring the proof using the branching tactical.
+
+However, authoring a proof structured with tacticals is annoying.
+Consider for example a proof by induction, and imagine you
+are using one of the state of the art graphical interfaces for proof assistant
+like Proof General. After applying the induction principle you have to choose:
+immediately structure the proof or postpone the structuring.
+If you decide for the former you have to apply the branching tactical and write
+at once tactics for all the cases. Since the user does not even know the
+generated goals yet, he can only replace all the cases with the identity
+tactic and execute the command, just to receive feedback on the first
+goal. Then he has to go one step back to replace the first identity
+tactic with the wanted one and repeat the process until all the
+branches are closed.
+
+One could imagine that a structured script is simpler to understand.
+This is not the case.
+A proof script, being not declarative, is not meant to be read.
+However, the user has the need of explaining it to others.
+This is achieved by interactively re-playing the script to show each
+intermediate proof status. Tacticals make this operation uncomfortable.
+Indeed, a tactical is executed atomically, while it is obvious that it
+performs lot of smaller steps we are interested in.
+To show the intermediate steps, the proof must be de-structured on the
+fly, for example replacing \OP{;} with \OP{.} where possible.
+
+\MATITA{} has a peculiar tacticals implementation that provides the
+same benefits as classical tacticals, while not burdening the user
+during proof authoring and re-playing.
+
+\subsubsection{The \MATITA{} approach}
\begin{table}
\caption{Concrete syntax of tacticals\strut}
::= & \SEMICOLON \quad|\quad \DOT \quad|\quad \SHIFT \quad|\quad \BRANCH \quad|\quad \MERGE \quad|\quad \POS{\mathrm{NUMBER}~} & \\
\NT{block\_kind} &
::= & \verb+focus+ ~|~ \verb+try+ ~|~ \verb+solve+ ~|~ \verb+first+ ~|~ \verb+repeat+ ~|~ \verb+do+~\mathrm{NUMBER} & \\
- \NT{block\_delimiter} &
+ \NT{block\_delim} &
::= & \verb+begin+ ~|~ \verb+end+ & \\
- \NT{tactical} &
- ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+ \NT{command} &
+ ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delim} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} \\
\end{array}
\]
\hrule
\end{table}
\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
-execution.
-
-The low-level tacticals implementation of \MATITA{} allows a step-by-step
-execution of a tactical, that substantially means that a $\NT{block\_kind}$ is
-not executed as an atomic operation. This has two major benefits for the user,
-even being a so simple idea:
-\begin{description}
-\item[Proof structuring]
- is much easier. Consider for example a proof by induction, and imagine you
- are using classical tacticals in one of the state of the
- art graphical interfaces for proof assistant like Proof General or \COQIDE.
- After applying the induction principle you have to choose: structure
- the proof or not. If you decide for the former you have to branch with
- ``\texttt{[}'' and write tactics for all the cases separated by
- ``\texttt{|}'' and then close the tactical with ``\texttt{]}''.
- You can replace most of the cases by the identity tactic just to
- concentrate only on the first goal, but you will have to go one step back and
- one further every time you add something inside the tactical. Again this is
- caused by the one step execution of tacticals and by the fact that to modify
- the already executed script you have to undo one step.
- And if you are board of doing so, you will finish in giving up structuring
- the proof and write a plain list of tactics.\\
- With step-by-step tacticals you can apply the induction principle, and just
- open the branching tactical ``\texttt{[}''. Then you can interact with the
- system reaching a proof of the first case, without having to specify any
- tactic for the other goals. When you have proved all the induction cases, you
- close the branching tactical with ``\texttt{]}'' and you are done with a
- structured proof. \\
- While \MATITA{} tacticals help in structuring proofs they allow you to
- choose the amount of structure you want. There are no constraints imposed by
- the system, and if the user wants he can even write completely plain proofs.
-
-\item[Rereading]
- is possible. Going on step by step shows exactly what is going on. Consider
- again a proof by induction, that starts applying the induction principle and
- suddenly branches with a ``\texttt{[}''. This clearly separates all the
- induction cases, but if the square brackets content is executed in one single
- step you completely loose the possibility of rereading it and you have to
- temporary remove the branching tactical to execute in a satisfying way the
- branches. Again, executing step-by-step is the way you would like to review
- the demonstration. Remember that understanding the proof from the script is
- not easy, and only the execution of tactics (and the resulting transformed
- goal) gives you the feeling of what is going on.
-\end{description}
+LCF tacticals have been replaced by unstructured more primitive commands;
+every LCF tactical is semantically equivalent to a sequential composition of
+them. As usual, each command is executed atomically, so that a sequence
+corresponding to an LCF tactical is now executed in multiple steps.
+
+For instance, reconsider the previous example of a proof by induction.
+In \MATITA{} the user can apply the induction principle, and just
+open the branching punctuation symbol \OP{[}. Then he can interact with the
+system (applying tactics and so forth) until he decides to move to the
+next branch using \OP{|}. After the last branch, the punctuation symbol
+\OP{]} must be used to collect goals possibly left open, accordingly to
+the semantics of the LCF branching tactical \OP{$\ldots$~;[~$\ldots$~|~$\ldots$~|~$\ldots$~]}. The result effortlessly obtained is a structured script.
+
+The user is not forced to fully structure his script. If he wants, he
+can even write completely unstructured proofs using only the \OP{.}
+punctuation symbol.
+
+Re-playing a proof is also straightforward since there is no longer any need
+to manually destructure the proof.
\section{Standard library}
\label{sec:stdlib}
-\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{}
-can be read, checked and referenced in further developments.
-However, in order to test the actual usability of the system, a
-new library of results has been started from scratch. In this case,
-of course, we wrote (and offer) the source script files,
-while, in the case of \COQ, \MATITA{} may only rely on XML files of
-\COQ{} objects.
+\MATITA{} is \COQ{} compatible, in the sense that every theorem of \COQ{} can be
+read, checked and referenced in further developments. However, in order to test
+the actual usability of the system, a new library of results has been started
+from scratch. In this case, of course, we wrote (and offer) the source scripts,
+while in the case of \COQ{} \MATITA{} may only rely on XML files of \COQ{}
+objects.
+
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: \texttt{logic} (connectives,
-quantifiers, equality, \ldots), \texttt{datatypes} (basic datatypes and type
+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}.
We do not plan to maintain the library in a centralized way,
as most of the systems do. On the contrary we are currently
-developing wiki-technologies to support a collaborative
+developing Wiki-technologies to support collaborative
development of the library, encouraging people to expand,
modify and elaborate previous contributions.
projects / helm.git / blobdiff