X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fpapers%2Fmatita%2Fmatita2.tex;h=f2e411d4a6b097227b4a315698d3993d97caa0fb;hb=6db12650bceb071d9b5ea8f882613a98bd6df79b;hp=7c8e2fa45252e3ccc7275cfb79cd302dcab20984;hpb=0934df282c5a661213df1962e678d9b9b95fee50;p=helm.git

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 7c8e2fa45..f2e411d4a 100644
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -123,6 +123,7 @@ Digital Libraries}
 
 \end{opening}
 
+
 \section{Introduction}
 \label{sec:intro}
 \MATITA{} is the Proof Assistant under development by the \HELM{} team
@@ -273,7 +274,7 @@ allow other developers to quickly understand our code and contribute.
  \end{center}
 \end{figure}
 
-\section{Overview of the Architecture}
+\section{Architecture}
 Fig.~\ref{fig:libraries} shows the architecture of the \emph{\components}
 (circle nodes) and \emph{applications} (squared nodes) developed in the HELM
 project.
@@ -401,6 +402,15 @@ content level terms; presentation level terms.
    The Whelp search engine 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
+   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
+   metadata are removed from the library. This aspect will be better detailed
+   in Sect.~\ref{decompilazione}.
+   
 \subsection{Partially specified terms}
 \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
@@ -432,9 +442,16 @@ prove.
 \emph{Tactics} are the procedures that the user can apply to progress in the
 proof. A tactic proves a conjecture possibly creating new (and hopefully
 simpler) conjectures. The implementation of tactics is given in the
-\texttt{tactics} \component. It is heavily based on the refinement and unification
-procedures of the \texttt{cic\_unification} \component. \TODO{citare paramodulation
-da qualche part o toglierla dal grafo}
+\texttt{tactics} \component. It is heavily based on the refinement and
+unification procedures of the \texttt{cic\_unification} \component.
+
+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{}.
+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. \TODO{parlare di disambiguazione lazy \& co?}
 
 As fully specified terms, partially specified terms are not well suited
 for user consumption since their syntax is not extendible and it is not
@@ -496,16 +513,18 @@ 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 annotates partially specified terms.
+The \texttt{cic\_acic} \component{} unshares and annotates terms. It is used
+by the \texttt{library} \component{} since fully specified terms are stored
+in the library in their annotated form.
 
 We do not provide yet a reverse translation from content level proofs to
-partially specified terms. But in \texttt{disambiguation} we do provide
+partially specified terms. But in \texttt{cic\_disambiguation} we do provide
 the reverse translation for expressions. The mapping from
 content level expressions to partially specified terms is not unique due to
 the ambiguity of the content level. As a consequence the translation
 is guided by an \emph{interpretation}, that is a function that chooses for
 every ambiguous expression one partially specified term. The
-\texttt{disambiguation} \component{} contains the implementation of the
+\texttt{cic\_disambiguation} \component{} implements the
 disambiguation algorithm we presented in~\cite{disambiguation} that is
 responsible of building in an efficicent way the set of all ``correct''
 interpretations. An interpretation is correct if the partially specified term
@@ -547,7 +566,9 @@ Semantic selection is a technique that consists in enriching the presentation
 level terms with pointers to the content level terms and to the partially
 specified terms they correspond to. Highlight of formulae in the widget is
 constrained to selection of meaningful expressions, i.e. expressions that
-correspond to a lower\footnote{\TODO{non abbiamo parlato di ``ordine''}} level term. Once the rendering of a lower level term is
+correspond to a lower level term, that is a content term or a partially or
+fully specified term.
+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
@@ -563,17 +584,40 @@ parsing tool we have adopted (CamlP4) is not able to parse ambiguous
 grammars. Thus we require the mapping from presentation level terms
 (concrete syntax) to content level terms (abstract syntax) to be unique.
 This means that the user must fix once and for all the associativity and
-precedence level of every operator he is using. In prctice this limitation
+precedence level of every operator he is using. In practice this limitation
 does not seem too strong. The reason is that the target of the
 translation is an ambiguous language and the user is free to associate
 to every content level term several different interpretations (as a
 partially specified term).
 
+Both the direct and reverse translation from presentation to content level
+terms are parameterized over the user provided mathematical notation. 
+The \texttt{lexicon} \component{} is responsible of managing the lexicon,
+that is the set of active notations. It defines an abstract syntax tree
+of commands to declare and activate new notations and it implements the
+semantics of these commands. It also implements undoing of the semantic
+actions. Among the commands there are hints to the
+disambiguation algorithm that are used to control and speed up disambiguation.
+These mechanisms will be further discussed in Sect.~\ref{disambiguazione}.
+
+Finally, the \texttt{grafite\_parser} \component{} implements a parser for
+the concrete syntax of the commands of \MATITA. The parser process 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
+the lexicon, it invokes the \texttt{lexicon} \component{} to immediately
+process the command. When the parser needs to parse a term at the presentation
+level, it invokes the already described parser for terms contained in
+\texttt{content\_pres}.
+
 The \MATITA{} proof assistant and the \WHELP{} search engine are both linked
-against the \texttt{cic\_disambiguation} and \texttt{content\_pres} \components{}
+against the \texttt{grafite\_parser} \components{}
 since they provide an interface to the user. In both cases the formulae
 written by the user are parsed using the \texttt{content\_pres} \component{} and
 then disambiguated using the \texttt{cic\_disambiguation} \component.
+However, only \MATITA{} is linked against the \texttt{grafite\_engine} and
+\texttt{tactics} components since \WHELP{} can only execute those ASTs that
+correspond to queries (implemented in the \texttt{whelp} component).
 
 The \UWOBO{} Web service wraps the \texttt{content\_pres} \component,
 providing a rendering service for the documents in the distributed library.
@@ -583,644 +627,767 @@ it to the presentation level passing through the content level. Finally
 it returns the result document to be rendered by the user's
 browser.\footnote{\TODO{manca la passata verso HTML}}
 
-\hrule
 
-At the bottom of the DAG we have a few \components{} (\texttt{extlib},
-\texttt{xml} and the \texttt{registry}) that provide a core of
-useful functions used everywhere else. In particular, the \texttt{xml} \component{}
-to easily represent, parse and pretty-print XML files is a central component
-since in HELM every piece of information is stored in \ldots. [FINIRE]
-The other basic \components{} provide often needed operations over generic
-data structures (\texttt{extlib}) and central storage for configuration options
-(the \texttt{registry}).
+The \components{} not yet described (\texttt{extlib}, \texttt{xml},
+\texttt{logger}, \texttt{registry} and \texttt{utf8\_macros}) are 
+minor \components{} that provide a core of useful functions and basic
+services missing from the standard library of the programming language.
+In particular, the \texttt{xml} \component{} is used
+to easily represent, parse and pretty-print XML files.
 
-\texttt{urimanager}
+\section{Using \MATITA (boh \ldots cambiare titolo)}
 
-\texttt{getter}
+\begin{figure}[t]
+ \begin{center}
+%   \includegraphics[width=0.9\textwidth]{a.eps}
+  \caption{\MATITA{} screenshot}
+  \label{fig:screenshot}
+ \end{center}
+\end{figure}
 
-\texttt{cic}
+\MATITA{} has a script based user interface. As can be seen in Fig.~... it is
+split in two main windows: on the left a textual widget is used to edit the
+script, on the right the list of open goal is shown using a MathML rendering
+widget. A distinguished part of the script (shaded in the screenshot) represent
+the commands already executed and can't be edited without undoing them. The
+remaining part can be freely edited and commands from that part can be executed
+moving down the execution point. An additional window --- the ``cicBrowser'' ---
+can be used to browse the library, including the proof being developed, and
+enable content based search on it. In the cicBrowser proofs are rendered in
+natural language, automatically generated from the low-level $\lambda$-terms
+using techniques inspired by \cite{natural,YANNTHESIS}.
+
+In the \MATITA{} philosophy the script is not relevant \emph{per se}, but is
+only seen as a convenient way to create mathematical objects. The universe of
+all these objects makes up the \HELM{} library, which is always completely
+visible to the user. The mathematical library is thus conceived as a global 
+hypertext, where objects may freely reference each other. It is a duty of
+the system to guide the user through the relevant parts of the library. 
+
+This methodological assumption has many important consequences
+which will be discussed in the next section.
+
+%on one side
+%it requires functionalities for the overall management of the library, 
+%%%%%comprising efficient indexing techniques to retrieve and filter the 
+%information; 
+%on the other it introduces overloading in the use of 
+%identifiers and mathematical notation, requiring sophisticated disambiguation
+%techniques for interpreting the user inputs.  
+%In the next two sections we shall separately discuss the two previous 
+%points. 
+
+%In order to maximize accessibility mathematical objects are encoded in XML. (As%discussed in the introduction,) the modular architecture of \MATITA{} is
+%organized in components which work on data in this format. For instance the
+%rendering engine, which transform $\lambda$-terms encoded as XML document to
+%MathML Presentation documents, can be used apart from \MATITA{} to print  ...
+%FINIRE
+
+A final section is devoted to some innovative aspects
+of the authoring system, such as a step by step tactical execution, 
+content selection and copy-paste. 
+
+\section{Library Management}
+
+\subsection{Indexing and searching}
+
+\subsection{Developments}
+
+\subsection{Automation}
 
-\section{Partially specified terms}
---- il mondo delle tattiche e dintorni ---
-serve una intro che almeno cita il widget (per i patterns) e che fa
-il resoconto delle cose che abbiamo e che non descriviamo,
-sottolineando che abbiamo qualcosa da dire sui pattern e sui
-tattichini.\\
+\subsection{Matita's naming convention}
+A minor but not entirely negligible aspect of Matita is that of
+adopting a (semi)-rigid naming convention for identifiers, derived by 
+our studies about metadata for statements. 
+The convention is only applied to identifiers for theorems 
+(not definitions), and relates the name of a proof to its statement.
+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 conlcusion must be separated by the string ``\verb+_to_+'';
+\item the identifier may be followed by a numerical suffix, or a
+single or duoble 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.\\
+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 \]
 
-\subsection{Patterns}
-Patterns are the textual counterpart of the MathML widget graphical
-selection.
+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 benefical effect on the global organization of the library, 
+forcing the user to define abstract notions and properties before 
+using them (and formalizing such use).
 
-Matita benefits of a graphical interface and a powerful MathML rendering
-widget that allows the user to select pieces of the sequent he is working
-on. While this is an extremely intuitive way for the user to
-restrict the application of tactics, for example, to some subterms of the
-conclusion or some hypothesis, the way this action is recorded to the text
-script is not obvious.\\
-In \MATITA{} this issue is addressed by patterns.
+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
+induction principle.
 
-\subsubsection{Pattern syntax}
-A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
-$\NT{wanted}$.
-The former mocks-up a sequent, discharging unwanted subterms with $?$ and
-selecting the interesting parts with the placeholder $\%$. 
-The latter is a term that lives in the context of the placeholders.
+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.
+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. 
 
-The concrete syntax is reported in table \ref{tab:pathsyn}
-\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
-\begin{table}
- \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
-\hrule
-\[
-\begin{array}{@{}rcll@{}}
-  \NT{pattern} & 
-    ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
-  \NT{sequent\_path} & 
-    ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
-      [~\verb+\vdash+~\NT{multipath}~] & \\
-  \NT{wanted} & ::= & \NT{term} & \\
-  \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
-\end{array}
-\]
-\hrule
-\end{table}
+\section{The \MATITA{} user interface}
 
-\subsubsection{How patterns work}
-Patterns mimic the user's selection in two steps. The first one
-selects roots (subterms) of the sequent, using the
-$\NT{sequent\_path}$,  while the second 
-one searches the $\NT{wanted}$ term starting from these 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.
+\subsection{Disambiguation}
 
-  The first phase selects not only terms (roots of subterms) but also 
-  their context that will be eventually used in the second phase.
+Software applications that involve input of mathematical content should strive
+to require the user as less drift from informal mathematics as possible. We
+believe this to be a fundamental aspect of such applications user interfaces.
+Being that drift in general very large when inputing
+proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
+mathematical formulae which can be input using a \TeX-like encoding (the
+concrete syntax corresponding to presentation level terms) and are then
+translated (in multiple steps) to partially specified terms as sketched in
+Sect.~\ref{sec:contentintro}.
 
-\item[Phase 2] 
-  plays a role only if the $[~\verb+in 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 $\alpha$-equivalent to
-  $\NT{wanted}$. The result of this search is the selection the
-  pattern represents.
+The key component of the translation is the generic disambiguation algorithm
+implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
+and presented in~\cite{disambiguation}. In this section we present how to use
+such an algorithm in the context of the development of a library of formalized
+mathematics. We will see that using multiple passes of the algorithm, varying
+some of its parameters, helps in keeping the input terse without sacrificing
+expressiveness.
 
-\end{description}
+\subsubsection{Disambiguation aliases}
 
-\noindent
-Since the first step is equipotent to the composition of the two
-steps, the system uses it to represent each visual selection.
-The second step is only meant for the
-experienced user that writes patterns by hand, since it really
-helps in writing concise patterns as we will see in the
-following examples.
+Let's start with the definition of the ``strictly greater then'' notion over
+(Peano) natural numbers.
 
-\subsubsection{Examples}
-To explain how the first step works let's give an example. Consider
-you want to prove the uniqueness of the identity element $0$ for natural
-sum, and that you can relay 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
-leads you to the following sequent 
-\sequent{
-n:nat\\
-m:nat\\
-H: m + n = n}{
-m=O
-}
-\noindent
-where you want to change the right part of the equivalence of the $H$
-hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
 \begin{grafite}
-  change in H:(? ? ? %) with (O + n).
+include "nat/nat.ma".
+..
+definition gt: nat \to nat \to Prop \def
+  \lambda n, m. m < n.
 \end{grafite}
-\noindent
-This pattern, that is a simple instance of the $\NT{sequent\_path}$
-grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
-and discharges the head of the application and the first two arguments with a
-$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
-but the user can simply select with the mouse the right part of the equivalence
-and left to the system the burden of writing down in the script file the
-corresponding pattern with $?$ and $\%$ in the right place (that is not
-trivial, expecially where implicit arguments are hidden by the notation, like
-the type $nat$ in this example).
 
-Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ 
-works too and can be done, by the experienced user, writing directly
-a simpler pattern that uses the second phase.
-\begin{grafite}
-  change in match n in H with (O + n).
-\end{grafite}
-\noindent
-In this case the $\NT{sequent\_path}$ selects the whole $H$, while
-the second phase searches the wanted $n$ inside it by
-$\alpha$-equivalence. The resulting
-equivalence will be $m+(O+n)=O+n$ since the second phase found two
-occurrences of $n$ in $H$ and the tactic changed both.
+The \texttt{include} statement adds the requirement that the part of the library
+defining the notion of natural numbers should be defined before
+processing the following definition. Note indeed that the algorithm presented
+in~\cite{disambiguation} does not describe where interpretations for ambiguous
+expressions come from, since it is application-specific. As a first
+approximation, we will assume that in \MATITA{} they come from the library (i.e.
+all interpretations available in the library are used) and the \texttt{include}
+statements are used to ensure the availability of required library slices (see
+Sect.~\ref{sec:libmanagement}).
+
+While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
+terms: its type and its body. Being available in the required library only one
+interpretation both for the unbound identifier \texttt{nat} and for the
+\OP{<} operator, and being the resulting partially specified term refinable,
+both type and body are easily disambiguated.
+
+Now suppose we have defined integers as signed natural numbers, and that we want
+to prove a theorem about an order relationship already defined on them (which of
+course overload the \OP{<} operator):
 
-Just for completeness the second pattern is equivalent to the
-following one, that is less readable but uses only the first phase.
 \begin{grafite}
-  change in H:(? ? (? ? %) %) with (O + n).
+include "Z/z.ma".
+..
+theorem Zlt_compat:
+  \forall x, y, z. x < y \to y < z \to x < z.
 \end{grafite}
-\noindent
-
-\subsubsection{Tactics supporting patterns}
-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.
 
-\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))}
-
-\subsubsection{Comparison with Coq}
-Coq has a two diffrent ways of restricting the application of tactis to
-subterms of the sequent, both relaying on the same special syntax to identify
-a term occurrence.
-
-The first way is to use this special syntax to specify directly to the
-tactic the occurrnces of a wanted term that should be affected, while
-the second is to prepare the sequent with another tactic called
-pattern and the 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.
+Since integers are defined on top of natural numbers, the part of the library
+concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
+type. Thus, according to the disambiguation algorithm, two different partially
+specified terms could be associated to it. At first, this might not be seen as a
+problem, since the user is asked and can choose interactively which of the two
+she had in mind. However in the long run it has the drawbacks of inhibiting
+batch compilation of the library (a technique used in \MATITA{} for behind the
+scene compilation when needed, e.g. when an \texttt{include} is issued) and
+yields to poor user interaction (imagine how tedious would be to be asked for a
+choice each time you re-evaluate \texttt{Zlt\_compat}!).
 
-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
-occurce of it (counting from left to right). In our previous example,
-to change only the left part of the equivalence, the correct command
-is
-\begin{grafite}
-  change n at 2 in H with (O + n)
-\end{grafite} 
-\noindent
-meaning that in the hypothesis $H$ the $n$ we want to change is the
-second we encounter proceeding from left toright.
+For this reason we added to \MATITA{} the concept of \emph{disambiguation
+aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
+expressions to partially specified terms, which are part of the runtime status
+of \MATITA. They can be provided by users with the \texttt{alias} statement, but
+are usually automatically added when evaluating \texttt{include} statements
+(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
+are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
+which require interactive choice are saved in batch compilable format. Thus,
+after evaluating the above theorem the script will be changed to the following
+snippet (assuming that the interpretation of \OP{<} over integers has been
+choosed):
 
-The tactic pattern computes a
-$\beta$-expansion of a part of the sequent with respect to some
-occurrences of the given term. In the previous example the following
-command
 \begin{grafite}
-  pattern n at 2 in H
+alias symbol "lt" = "integer 'less than'".
+theorem Zlt_compat:
+  \forall x, y, z. x < y \to y < z \to x < z.
 \end{grafite}
-\noindent
-would have resulted in this sequent
+
+But how are disambiguation aliases used? Since they come from the parts of the
+library explicitely included we may be tempted of using them as the only
+available interpretations. This would speed up the disambiguation, but may fail.
+Consider for example:
+
 \begin{grafite}
-  n : nat
-  m : nat
-  H : (fun n0 : nat => m + n = n0) n
-  ============================
-   m = 0
+theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
 \end{grafite}
-\noindent
-where $H$ is $\beta$-expanded over the second $n$
-occurrence. This is a trick to make the unification algorithm ignore
-the head of the application (since the unification is essentially
-first-order) but normally operate on the arguments. 
-This works for some tactics, like rewrite and replace,
-but for example not for change and other tactics that do not relay on
-unification. 
 
-The idea behind this way of identifying subterms in not really far
-from the idea behind patterns, but really fails in extending to
-complex notation, since it relays on a mono-dimensional sequent representation.
-Real math notation places arguments upside-down (like in indexed sums or
-integrations) or even puts them inside a bidimensional matrix.  
-In these cases using the mouse to select the wanted term is probably the 
-only way to tell the system exactly what you want to do. 
+and suppose that the \OP{+} operator is defined only on natural numbers. If
+the alias for \OP{<} points to the integer version of the operator, no
+refinable partially specified term matching the term could be found.
 
-One of the goals of \MATITA{} is to use modern publishing techiques, and
-adopting a method for restricting tactics application domain that discourages 
-using heavy math notation, would definitively be a bad choice.
+For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
+first pass attempt to disambiguate using the last available disambiguation
+aliases (\emph{mono aliases} pass), in case of failure the next pass try again
+the disambiguation forgetting the aliases and using the whole library to
+retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
+Since the latter pass may lead to too many choices we intertwined an additional
+pass among the two which use as interpretations all the aliases coming for
+included parts of the library (\emph{multi aliases} phase). This is the reason
+why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
+turned out to be a well-balanced trade-off among performances (earlier passes
+fail quickly) and degree of ambiguity supported for presentation level terms.
 
-\subsection{Tacticals}
-There are mainly two kinds of languages used by proof assistants to recorder
-proofs: tactic based and declarative. We will not investigate the philosophy
-aroud the choice that many proof assistant made, \MATITA{} included, and we
-will not compare the two diffrent approaches. We will describe the common
-issues of the tactic-based language approach and how \MATITA{} tries to solve
-them.
+\subsubsection{Operator instances}
 
-\subsubsection{Tacticals overview}
+Let's suppose now we want to define a theorem relating ordering relations on
+natural and integer numbers. The way we would like to write such a theorem (as
+we can read it in the \MATITA{} standard library) is:
 
-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
 \begin{grafite}
-theorem trivial: 
-  \forall A,B:Prop. 
-    A = B \to ((A \to B) \land (B \to A)).
-  intros (A B H).
-  split; intro; 
-    [ rewrite < H. assumption.
-    | rewrite > H. assumption.
-    ]
-qed.
+include "Z/z.ma".
+include "nat/orders.ma".
+..
+theorem lt_to_Zlt_pos_pos:
+  \forall n, m: nat. n < m \to pos n < pos m. 
 \end{grafite}
 
-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).
+Unfortunately, none of the passes described above is able to disambiguate its
+type, no matter how aliases are defined. This is because the \OP{<} operator
+occurs twice in the content level term (it has two \emph{instances}) and two
+different interpretation for it have to be used in order to obtain a refinable
+partially specified term. To address this issue, we have the ability to consider
+each instance of a single symbol as a different ambiguous expression in the
+content level term, and thus we can assign a different interpretation to each of
+them. A disambiguation pass which exploit this feature is said to be using
+\emph{fresh instances}.
 
-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.
+Fresh instances lead to a non negligible performance loss (since the choice of
+an interpretation for one instances does not constraint the choice for the
+others). For this reason we always attempt a fresh instances pass only after
+attempting a non-fresh one.
+
+\subsubsection{Implicit coercions}
+
+Let's now consider a (rather hypothetical) theorem about derivation:
 
 \begin{grafite}
-  elim z; try assumption; [ ... | ... ].
-  elim z; first [ assumption | reflexivity | id ].
+theorem power_deriv:
+  \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
 \end{grafite}
 
-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. 
+and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
+interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
+Mathematichians would write the term that way since it is well known that the
+natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
+number for the purpose of real multiplication. The refiner of \MATITA{} supports
+\emph{implicit coercions} for this reason: given as input the above content
+level term, it will return a partially specified term where in place of
+\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
+(assuming it has been defined as such of course).
 
-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.
+Nonetheless coercions are not always desirable. For example, in disambiguating
+\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
+two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
+among the possible partially specified term choices. For this reason in
+\MATITA{} we always try first a disambiguation pass which require the refiner
+not to use the coercions and only in case of failure we attempt a
+coercion-enabled pass.
 
-\subsubsection{Common issues of tactic(als)-based proof languages}
-We will examine the two main problems of tactic(als)-based proof script:
-maintainability and readability. 
+It is interesting to observe also the relationship among operator instances and
+implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
+which \MATITA{} disambiguated using fresh instances. In case there exists a
+coercion from natural numbers to (positive) integers (which indeed does, it is
+the \texttt{pos} constructor itself), the theorem can be disambiguated using
+twice that coercion on the left hand side of the implication. The obtained
+partially specified term however would not probably be the expected one, being a
+theorem which prove a trivial implication. For this reason we choose to always
+prefer fresh instances over implicit coercion, i.e. we always attempt
+disambiguation passes with fresh instances before attempting passes with
+implicit coercions.
 
-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. 
+\subsubsection{Disambiguation passes}
 
-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 doesn't work
-anymore unless you de-structure on the fly the proof, putting some
-``\texttt{.}'' where you want the system to stop.\\
+\TODO{spiegazione della tabella}
 
-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.
+\begin{center}
+ \begin{tabular}{c|c|c|c}
+  \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+  & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
+  & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+  & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
+  \hline
+  \PASS & Normal & Mono & Disabled \\
+  \PASS & Normal & Multi & Disabled \\
+  \PASS & Fresh & Mono & Disabled \\
+  \PASS & Fresh & Multi & Disabled \\
+  \PASS & Fresh & Mono & Enabled \\
+  \PASS & Fresh & Multi & Enabled \\
+  \PASS & Fresh & Library & Enabled
+ \end{tabular}
+\end{center}
 
-\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.
+\TODO{alias one shot}
 
-\subsubsection{The \MATITA{} approach: Tinycals}
 
+
+
+
+
+
+\subsection{Patterns}
+
+serve una intro che almeno cita il widget (per i patterns) e che fa
+il resoconto delle cose che abbiamo e che non descriviamo,
+sottolineando che abbiamo qualcosa da dire sui pattern e sui
+tattichini.\\
+
+Patterns are the textual counterpart of the MathML widget graphical
+selection.
+
+Matita benefits of a graphical interface and a powerful MathML rendering
+widget that allows the user to select pieces of the sequent he is working
+on. While this is an extremely intuitive way for the user to
+restrict the application of tactics, for example, to some subterms of the
+conclusion or some hypothesis, the way this action is recorded to the text
+script is not obvious.\\
+In \MATITA{} this issue is addressed by patterns.
+
+\subsubsection{Pattern syntax}
+A pattern is composed of two terms: a $\NT{sequent\_path}$ and a
+$\NT{wanted}$.
+The former mocks-up a sequent, discharging unwanted subterms with $?$ and
+selecting the interesting parts with the placeholder $\%$. 
+The latter is a term that lives in the context of the placeholders.
+
+The concrete syntax is reported in table \ref{tab:pathsyn}
+\NOTE{uso nomi diversi dalla grammatica ma che hanno + senso}
 \begin{table}
- \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+ \caption{\label{tab:pathsyn} Concrete syntax of \MATITA{} patterns.\strut}
 \hrule
 \[
 \begin{array}{@{}rcll@{}}
-  \NT{punctuation} & 
-    ::= & \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} & 
-    ::= & \verb+begin+ ~|~ \verb+end+ & \\
-  \NT{tactical} & 
-    ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+  \NT{pattern} & 
+    ::= & [~\verb+in match+~\NT{wanted}~]~[~\verb+in+~\NT{sequent\_path}~] & \\
+  \NT{sequent\_path} & 
+    ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+      [~\verb+\vdash+~\NT{multipath}~] & \\
+  \NT{wanted} & ::= & \NT{term} & \\
+  \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
 \end{array}
 \]
 \hrule
 \end{table}
 
-\MATITA{} tacticals syntax is reported in table \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.
+\subsubsection{How patterns work}
+Patterns mimic the user's selection in two steps. The first one
+selects roots (subterms) of the sequent, using the
+$\NT{sequent\_path}$,  while the second 
+one searches the $\NT{wanted}$ term starting from these roots. Both are
+optional steps, and by convention the empty pattern selects the whole
+conclusion.
 
-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 Coq Ide.
-  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}
+\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}
 
-\section{Content level terms}
+  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.
 
-\subsection{Disambiguation}
+  The first phase selects not only terms (roots of subterms) but also 
+  their context that will be eventually used in the second phase.
 
-Software applications that involve input of mathematical content should strive
-to require the user as less drift from informal mathematics as possible. We
-believe this to be a fundamental aspect of such applications user interfaces.
-Being that drift in general very large when inputing
-proofs~\cite{debrujinfactor}, in \MATITA{} we achieved good results for
-mathematical formulae which can be input using a \TeX-like encoding (the
-concrete syntax corresponding to presentation level terms) and are then
-translated (in multiple steps) to partially specified terms as sketched in
-Sect.~\ref{sec:contentintro}.
+\item[Phase 2] 
+  plays a role only if the $[~\verb+in 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 $\alpha$-equivalent to
+  $\NT{wanted}$. The result of this search is the selection the
+  pattern represents.
 
-The key component of the translation is the generic disambiguation algorithm
-implemented in the \texttt{disambiguation} library of Fig.~\ref{fig:libraries}
-and presented in~\cite{disambiguation}. In this section we present how to use
-such an algorithm in the context of the development of a library of formalized
-mathematics. We will see that using multiple passes of the algorithm, varying
-some of its parameters, helps in keeping the input terse without sacrificing
-expressiveness.
+\end{description}
 
-\subsubsection{Disambiguation aliases}
+\noindent
+Since the first step is equipotent to the composition of the two
+steps, the system uses it to represent each visual selection.
+The second step is only meant for the
+experienced user that writes patterns by hand, since it really
+helps in writing concise patterns as we will see in the
+following examples.
 
-Let's start with the definition of the ``strictly greater then'' notion over
-(Peano) natural numbers.
+\subsubsection{Examples}
+To explain how the first step works let's give an example. Consider
+you want to prove the uniqueness of the identity element $0$ for natural
+sum, and that you can relay 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
+leads you to the following sequent 
+\sequent{
+n:nat\\
+m:nat\\
+H: m + n = n}{
+m=O
+}
+\noindent
+where you want to change the right part of the equivalence of the $H$
+hypothesis with $O + n$ and then use $inj\_plus\_l$ to prove $m=O$.
+\begin{grafite}
+  change in H:(? ? ? %) with (O + n).
+\end{grafite}
+\noindent
+This pattern, that is a simple instance of the $\NT{sequent\_path}$
+grammar entry, acts on $H$ that has type (without notation) $(eq~nat~(m+n)~n)$
+and discharges the head of the application and the first two arguments with a
+$?$ and selects the last argument with $\%$. The syntax may seem uncomfortable,
+but the user can simply select with the mouse the right part of the equivalence
+and left to the system the burden of writing down in the script file the
+corresponding pattern with $?$ and $\%$ in the right place (that is not
+trivial, expecially where implicit arguments are hidden by the notation, like
+the type $nat$ in this example).
 
+Changing all the occurrences of $n$ in the hypothesis $H$ with $O+n$ 
+works too and can be done, by the experienced user, writing directly
+a simpler pattern that uses the second phase.
 \begin{grafite}
-include "nat/nat.ma".
-..
-definition gt: nat \to nat \to Prop \def
-  \lambda n, m. m < n.
+  change in match n in H with (O + n).
 \end{grafite}
+\noindent
+In this case the $\NT{sequent\_path}$ selects the whole $H$, while
+the second phase searches the wanted $n$ inside it by
+$\alpha$-equivalence. The resulting
+equivalence will be $m+(O+n)=O+n$ since the second phase found two
+occurrences of $n$ in $H$ and the tactic changed both.
 
-The \texttt{include} statement adds the requirement that the part of the library
-defining the notion of natural numbers should be defined before
-processing the following definition. Note indeed that the algorithm presented
-in~\cite{disambiguation} does not describe where interpretations for ambiguous
-expressions come from, since it is application-specific. As a first
-approximation, we will assume that in \MATITA{} they come from the library (i.e.
-all interpretations available in the library are used) and the \texttt{include}
-statements are used to ensure the availability of required library slices (see
-Sect.~\ref{sec:libmanagement}).
+Just for completeness the second pattern is equivalent to the
+following one, that is less readable but uses only the first phase.
+\begin{grafite}
+  change in H:(? ? (? ? %) %) with (O + n).
+\end{grafite}
+\noindent
 
-While processing the \texttt{gt} definition, \MATITA{} has to disambiguate two
-terms: its type and its body. Being available in the required library only one
-interpretation both for the unbound identifier \texttt{nat} and for the
-\OP{<} operator, and being the resulting partially specified term refinable,
-both type and body are easily disambiguated.
+\subsubsection{Tactics supporting patterns}
+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.
 
-Now suppose we have defined integers as signed natural numbers, and that we want
-to prove a theorem about an order relationship already defined on them (which of
-course overload the \OP{<} operator):
+\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))}
 
-\begin{grafite}
-include "Z/z.ma".
-..
-theorem Zlt_compat:
-  \forall x, y, z. x < y \to y < z \to x < z.
-\end{grafite}
+\subsubsection{Comparison with Coq}
+Coq has a two diffrent ways of restricting the application of tactis to
+subterms of the sequent, both relaying on the same special syntax to identify
+a term occurrence.
 
-Since integers are defined on top of natural numbers, the part of the library
-concerning the latters is available when disambiguating \texttt{Zlt\_compat}'s
-type. Thus, according to the disambiguation algorithm, two different partially
-specified terms could be associated to it. At first, this might not be seen as a
-problem, since the user is asked and can choose interactively which of the two
-she had in mind. However in the long run it has the drawbacks of inhibiting
-batch compilation of the library (a technique used in \MATITA{} for behind the
-scene compilation when needed, e.g. when an \texttt{include} is issued) and
-yields to poor user interaction (imagine how tedious would be to be asked for a
-choice each time you re-evaluate \texttt{Zlt\_compat}!).
+The first way is to use this special syntax to specify directly to the
+tactic the occurrnces of a wanted term that should be affected, while
+the second is to prepare the sequent with another tactic called
+pattern and the 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.
 
-For this reason we added to \MATITA{} the concept of \emph{disambiguation
-aliases}. Disambiguation aliases are one-to-many mappings from ambiguous
-expressions to partially specified terms, which are part of the runtime status
-of \MATITA. They can be provided by users with the \texttt{alias} statement, but
-are usually automatically added when evaluating \texttt{include} statements
-(\emph{implicit aliases}). Aliases implicitely inferred during disambiguation
-are remembered as well. Moreover, \MATITA{} does it best to ensure that terms
-which require interactive choice are saved in batch compilable format. Thus,
-after evaluating the above theorem the script will be changed to the following
-snippet (assuming that the interpretation of \OP{<} over integers has been
-choosed):
+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
+occurce of it (counting from left to right). In our previous example,
+to change only the left part of the equivalence, the correct command
+is
+\begin{grafite}
+  change n at 2 in H with (O + n)
+\end{grafite} 
+\noindent
+meaning that in the hypothesis $H$ the $n$ we want to change is the
+second we encounter proceeding from left toright.
 
+The tactic pattern computes a
+$\beta$-expansion of a part of the sequent with respect to some
+occurrences of the given term. In the previous example the following
+command
 \begin{grafite}
-alias symbol "lt" = "integer 'less than'".
-theorem Zlt_compat:
-  \forall x, y, z. x < y \to y < z \to x < z.
+  pattern n at 2 in H
 \end{grafite}
-
-But how are disambiguation aliases used? Since they come from the parts of the
-library explicitely included we may be tempted of using them as the only
-available interpretations. This would speed up the disambiguation, but may fail.
-Consider for example:
-
+\noindent
+would have resulted in this sequent
 \begin{grafite}
-theorem lt_mono: \forall x, y, k. x < y \to x < y + k.
+  n : nat
+  m : nat
+  H : (fun n0 : nat => m + n = n0) n
+  ============================
+   m = 0
 \end{grafite}
+\noindent
+where $H$ is $\beta$-expanded over the second $n$
+occurrence. This is a trick to make the unification algorithm ignore
+the head of the application (since the unification is essentially
+first-order) but normally operate on the arguments. 
+This works for some tactics, like rewrite and replace,
+but for example not for change and other tactics that do not relay on
+unification. 
 
-and suppose that the \OP{+} operator is defined only on natural numbers. If
-the alias for \OP{<} points to the integer version of the operator, no
-refinable partially specified term matching the term could be found.
+The idea behind this way of identifying subterms in not really far
+from the idea behind patterns, but really fails in extending to
+complex notation, since it relays on a mono-dimensional sequent representation.
+Real math notation places arguments upside-down (like in indexed sums or
+integrations) or even puts them inside a bidimensional matrix.  
+In these cases using the mouse to select the wanted term is probably the 
+only way to tell the system exactly what you want to do. 
 
-For this reason we choosed to attempt \emph{multiple disambiguation passes}. A
-first pass attempt to disambiguate using the last available disambiguation
-aliases (\emph{mono aliases} pass), in case of failure the next pass try again
-the disambiguation forgetting the aliases and using the whole library to
-retrieve interpretation for ambiguous expressions (\emph{library aliases} pass).
-Since the latter pass may lead to too many choices we intertwined an additional
-pass among the two which use as interpretations all the aliases coming for
-included parts of the library (\emph{multi aliases} phase). This is the reason
-why aliases are \emph{one-to-many} mappings instead of one-to-one. This choice
-turned out to be a well-balanced trade-off among performances (earlier passes
-fail quickly) and degree of ambiguity supported for presentation level terms.
+One of the goals of \MATITA{} is to use modern publishing techiques, and
+adopting a method for restricting tactics application domain that discourages 
+using heavy math notation, would definitively be a bad choice.
 
-\subsubsection{Operator instances}
 
-Let's suppose now we want to define a theorem relating ordering relations on
-natural and integer numbers. The way we would like to write such a theorem (as
-we can read it in the \MATITA{} standard library) is:
+\subsection{Tacticals}
+There are mainly two kinds of languages used by proof assistants to recorder
+proofs: tactic based and declarative. We will not investigate the philosophy
+aroud the choice that many proof assistant made, \MATITA{} included, and we
+will not compare the two diffrent approaches. We will describe the common
+issues of the tactic-based language approach and how \MATITA{} tries to solve
+them.
+
+\subsubsection{Tacticals overview}
 
+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
 \begin{grafite}
-include "Z/z.ma".
-include "nat/orders.ma".
-..
-theorem lt_to_Zlt_pos_pos:
-  \forall n, m: nat. n < m \to pos n < pos m. 
+theorem trivial: 
+  \forall A,B:Prop. 
+    A = B \to ((A \to B) \land (B \to A)).
+  intros (A B H).
+  split; intro; 
+    [ rewrite < H. assumption.
+    | rewrite > H. assumption.
+    ]
+qed.
 \end{grafite}
 
-Unfortunately, none of the passes described above is able to disambiguate its
-type, no matter how aliases are defined. This is because the \OP{<} operator
-occurs twice in the content level term (it has two \emph{instances}) and two
-different interpretation for it have to be used in order to obtain a refinable
-partially specified term. To address this issue, we have the ability to consider
-each instance of a single symbol as a different ambiguous expression in the
-content level term, and thus we can assign a different interpretation to each of
-them. A disambiguation pass which exploit this feature is said to be using
-\emph{fresh instances}.
-
-Fresh instances lead to a non negligible performance loss (since the choice of
-an interpretation for one instances does not constraint the choice for the
-others). For this reason we always attempt a fresh instances pass only after
-attempting a non-fresh one.
-
-\subsubsection{Implicit coercions}
+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).
 
-Let's now consider a (rather hypothetical) theorem about derivation:
+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.
 
 \begin{grafite}
-theorem power_deriv:
-  \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
+  elim z; try assumption; [ ... | ... ].
+  elim z; first [ assumption | reflexivity | id ].
 \end{grafite}
 
-and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
-interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematichians would write the term that way since it is well known that the
-natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
-number for the purpose of real multiplication. The refiner of \MATITA{} supports
-\emph{implicit coercions} for this reason: given as input the above content
-level term, it will return a partially specified term where in place of
-\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
-(assuming it has been defined as such of course).
+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. 
 
-Nonetheless coercions are not always desirable. For example, in disambiguating
-\texttt{\TEXMACRO{forall} x: nat. n < n + 1} we don't want the term which uses
-two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
-among the possible partially specified term choices. For this reason in
-\MATITA{} we always try first a disambiguation pass which require the refiner
-not to use the coercions and only in case of failure we attempt a
-coercion-enabled pass.
+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.
 
-It is interesting to observe also the relationship among operator instances and
-implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
-which \MATITA{} disambiguated using fresh instances. In case there exists a
-coercion from natural numbers to (positive) integers (which indeed does, it is
-the \texttt{pos} constructor itself), the theorem can be disambiguated using
-twice that coercion on the left hand side of the implication. The obtained
-partially specified term however would not probably be the expected one, being a
-theorem which prove a trivial implication. For this reason we choose to always
-prefer fresh instances over implicit coercion, i.e. we always attempt
-disambiguation passes with fresh instances before attempting passes with
-implicit coercions.
+\subsubsection{Common issues of tactic(als)-based proof languages}
+We will examine the two main problems of tactic(als)-based proof script:
+maintainability and readability. 
 
-\subsubsection{Disambiguation passes}
+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. 
 
-\TODO{spiegazione della tabella}
+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 doesn't work
+anymore unless you de-structure on the fly the proof, putting some
+``\texttt{.}'' where you want the system to stop.\\
 
-\begin{center}
- \begin{tabular}{c|c|c|c}
-  \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
-  & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
-  & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
-  & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
-  \hline
-  \PASS & Normal & Mono & Disabled \\
-  \PASS & Normal & Multi & Disabled \\
-  \PASS & Fresh & Mono & Disabled \\
-  \PASS & Fresh & Multi & Disabled \\
-  \PASS & Fresh & Mono & Enabled \\
-  \PASS & Fresh & Multi & Enabled \\
-  \PASS & Fresh & Library & Enabled
- \end{tabular}
-\end{center}
+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.
 
-\TODO{alias one shot}
+\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}
+
+\begin{table}
+ \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
+\hrule
+\[
+\begin{array}{@{}rcll@{}}
+  \NT{punctuation} & 
+    ::= & \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} & 
+    ::= & \verb+begin+ ~|~ \verb+end+ & \\
+  \NT{tactical} & 
+    ::= & \verb+skip+ ~|~ \NT{tactic} ~|~ \NT{block\_delimiter} ~|~ \NT{block\_kind} ~|~ \NT{punctuation} ~|~& \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\MATITA{} tacticals syntax is reported in table \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 Coq Ide.
+  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}
+
+\section{The Matita library}
 
-\section{The logical library}
 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
@@ -1257,72 +1424,6 @@ developing wiki-technologies to support a collaborative
 development of the library, encouraging people to expand, 
 modify and elaborate previous contributions.
 
-\subsection{Matita's naming convention}
-A minor but not entirely negligible aspect of Matita is that of
-adopting a (semi)-rigid naming convention for identifiers, derived by 
-our studies about metadata for statements. 
-The convention is only applied to identifiers for theorems 
-(not definitions), and relates the name of a proof to its statement.
-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 conlcusion must be separated by the string ``\verb+_to_+'';
-\item the identifier may be followed by a numerical suffix, or a
-single or duoble 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.\\
-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 \]
-
-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 benefical effect on the global organization of the library, 
-forcing the user to define abstract notions 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
-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.
-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. 
-
-
 \section{Conclusions}
 
 \acknowledgements