\newcommand{\sequent}[2]{
\savebox{\tmpxyz}[0.9\linewidth]{
\begin{minipage}{0.9\linewidth}
- \ensuremath{#1} \\
+ \texttt{#1} \\
\rule{3cm}{0.03cm}\\
- \ensuremath{#2}
+ \texttt{#2}
\end{minipage}}\setlength{\fboxsep}{3mm}%
\begin{center}
\fcolorbox{black}{gray}{\usebox{\tmpxyz}}
\listoffigures
\listoftables
+\TODO{rivedere tutti gli usi di \TEXMACRO{NOTE}}
+
\section{Introduction}
\label{sec:intro}
The origins of \MATITA{} go back to 1999. At the time we were mostly
interested in developing tools and techniques to enhance the accessibility
via Web of libraries of formalized mathematics. Due to its dimension, the
-library of the \COQ~\cite{CoqManual} proof assistant (of the order of 35'000 theorems)
+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}.\TODO{citare la tesi di vincenzo(?)}
preferences.
Several disambiguation parameters can vary among passes. With respect to
-preference handling we implemented 3 passes. In the first pass, called
+preference handling we implemented three passes. In the first pass, called
\emph{mono-preferences}, we consider only the aliases corresponding to the
current set of preferences. In the second pass, called
\emph{multi-preferences}, we
\subsubsection{Invalidation}
-Invalidation (see Sect.~\ref{sec:library}) is implemented in 2 phases.
+Invalidation (see Sect.~\ref{sec:library}) is implemented in two phases.
The first one is the calculation of all the concepts that recursively
depend on the ones we are invalidating. It can be performed
\label{sec:automation}
In the long run, one would expect to work with a proof assistant
-like \MATITA, using only 3 basic tactics: \TAC{intro}, \TAC{elim},
+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
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 2
+(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
\item all names should (but this is not strictly compulsory)
separated by an underscore;
- \item names occurring in 2 different hypotheses, or in an hypothesis
+ \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
\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}
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.\NOTE{Questo ancora non va in matita}
+
+ 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}
% intros (n m H).
%\end{grafite}
-Consider the following sequent
-\sequent{
-n:nat\\
-m:nat\\
-H: m + n = n}{
-m=O
-}
+Consider the following sequent:
+\sequent{n: nat\\m: nat\\H: m + n = n}{m = O}
-To change the right part of the equivalence of the $H$
-hypothesis with $O + n$ the user selects and pastes it as the pattern
+To change the right part of the equality of the \texttt{H}
+hypothesis with \texttt{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}
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$.
+aware that the notation \texttt{m + n = n} hides the term
+\texttt{eq nat (m + n) n}, so
+that the pattern selects only the third argument of \texttt{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 change at once all the occurrences of \texttt{n} in the hypothesis
+\texttt{H}:
\begin{grafite}
change in H match n with (O + n).
\end{grafite}
-In this case the $\NT{sequent\_path}$ selects the whole $H$, while
-the second phase locates $n$.
+In this case the \NT{sequent\_path} selects the whole \texttt{H}, while
+the second phase locates \texttt{n}.
The latter pattern is equivalent to the following one, that the system
can automatically generate from the selection.
\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.
+In \MATITA{} all the tactics that can be restricted to subterms of the current
+sequent accept the pattern syntax. These tactics are:
+\TAC{simplify}, \TAC{change}, \TAC{fold}, \TAC{unfold}, \TAC{generalize},
+\TAC{replace} and \TAC{rewrite}.
-\NOTE{attualmente rewrite e fold non supportano phase 2. per
+\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))}
\subsubsection{Comparison with \COQ{}}
\COQ{} has two different ways of restricting the application of tactics to
-subterms of the sequent, both relaying on the same special syntax to identify
-a term occurrence.
+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$
+\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 behaviour.
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.
\subsection{Tacticals}
\label{sec:tinycals}
%\subsubsection{Tacticals overview}
-Tacticals first appeared in LCF as higher order tactics. They can be
-seen as control flow constructs, like looping, branching, error
-recovery or sequential composition.
-
-
-The following simple example
-shows a Coq script made of four dot-terminated commands
+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.
+The following simple example shows a \COQ{} script made of four dot-terminated
+commands:
\begin{grafite}
Theorem trivial:
forall A B:Prop,
Qed.
\end{grafite}
-The third command is an application of the sequencing tactical
-``$\ldots$\texttt{;}$\ldots$'', that combines the tactic
-\texttt{split} with the application of the branching tactical
-``$\ldots$\texttt{;[}$\ldots$\texttt{|}$\ldots$\texttt{|}$\ldots$\texttt{]}''
-to other tactics and tacticals.
+The third command is an application of the sequencing tactical \OP{..~;~..},
+that combines the tactic \TAC{split} with the application of the branching
+tactical \OP{..~;[~..~|~..~|~..~]} to other tactics or tacticals.
The usual implementation of tacticals executes them atomically as any
-other command. In \MATITA{} thi is not true since each punctuation is
-executed as a single command.
+other command. In \MATITA{} this is not the case: each punctuation
+symbol is executed as a single command.
%The latter is applied to all the goals opened by \texttt{split}
%
%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 tactic-based proof languages}
+We will examine the two main problems of tactic-based proof scripts:
maintainability and readability.
%Huge libraries of formal mathematics have been developed, and backward
%proof script readability.
Tacticals are not only used to make scripts shorter by factoring out
-common cases and repeating commands. They are a primary way of making
-scripts more mainteable. Moreover, they also have the well-known
-role of structuring the proof.
+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:
+are using one of the state of the art graphical interfaces for proof assistant:
+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
Indeed, a tactical is executed atomically, while it is obvious that it
performs lot of smaller steps we are interested in.
To show the intermediate steps, the proof must be de-structured on the
-fly, for example replacing ``\texttt{;}'' with ``\texttt{.}'' where
-possible.\\
+fly, for example replacing \OP{;} with \OP{.} where possible.
%Proof scripts
%readability is poor by itself, but in conjunction with tacticals it
%this tradeoff, alluring the user to write structured proof without
%making it impossible to read them again.
-\subsubsection{The \MATITA{} approach: Tinycals}
+\subsubsection{The \MATITA{} approach}
\begin{table}
\caption{Concrete syntax of tacticals\strut}
\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 the base idea behind \MATITA{} tacticals: step-by-step
+This is essential the base idea of \MATITA{} tacticals: step-by-step
execution.
The low-level tacticals implementation of \MATITA{} allows a step-by-step
For instance, reconsider the previous example of a proof by induction.
With step-by-step tacticals the user can apply the induction principle, and just
-open the branching tactical ``\texttt{[}''. Then he can interact with the
+open the branching tactical \OP{[}. Then he can interact with the
system until the proof of the first case is terminated. After that
-``\texttt{|}'' is used to move to the next goal, until all goals are
+\OP{|} is used to move to the next goal, until all goals are
closed. After the last goal, the user closes the branching tactical with
-``\texttt{]}'' and is done with a structured proof. \\
+\OP{]} and he just finished 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.
+the system, and if the user wants he can even write completely un-structured
+proofs.
Re-playing a proof is also made simpler. There is no longer any need
to destructure the proof on the fly since \MATITA{} executes each
\TODO{rivedere bibliografia, \'e un po' povera}
-\TODO{aggiungere entry per le coercion implicite}
-
\bibliography{matita}
\end{document}
projects / helm.git / commitdiff