Draft of section Indexing and searching.

[helm.git] / helm / papers / matita / matita2.tex

diff --git a/helm/papers/matita/matita2.tex b/helm/papers/matita/matita2.tex
index 8500cfa2c2b76f88e662dfd0c70b8929100360ac..9dca4c67768a9c5db5fdef044a3186be63d3a28e 100644 (file)
--- a/helm/papers/matita/matita2.tex
+++ b/helm/papers/matita/matita2.tex
@@ -1,4 +1,4 @@
-\documentclass[]{kluwer}
+\documentclass[draft]{kluwer}

 \usepackage{color}
 \usepackage{graphicx}
 \usepackage{hyperref}
 \usepackage{color}
 \usepackage{graphicx}
 \usepackage{hyperref}


@@ -29,7 +29,6 @@
 \newcommand{\MATITA}{Matita}
 \newcommand{\MATITAC}{\texttt{matitac}}
 \newcommand{\MATITADEP}{\texttt{matitadep}}
 \newcommand{\MATITA}{Matita}
 \newcommand{\MATITAC}{\texttt{matitac}}
 \newcommand{\MATITADEP}{\texttt{matitadep}}

-\newcommand{\METAHEADING}{Symbol & Position \\ \hline\hline}

 \newcommand{\MOWGLI}{MoWGLI}
 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
 \newcommand{\NATIND}{\mathit{nat\_ind}}
 \newcommand{\MOWGLI}{MoWGLI}
 \newcommand{\NAT}{\ensuremath{\mathit{nat}}}
 \newcommand{\NATIND}{\mathit{nat\_ind}}


@@ -41,6 +40,7 @@
 \newcommand{\UWOBO}{UWOBO}
 \newcommand{\GETTER}{Getter}
 \newcommand{\WHELP}{Whelp}
 \newcommand{\UWOBO}{UWOBO}
 \newcommand{\GETTER}{Getter}
 \newcommand{\WHELP}{Whelp}

+

 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}
 \newcommand{\DOT}{\ensuremath{\mbox{\textbf{.}}}}
 \newcommand{\SEMICOLON}{\ensuremath{\mbox{\textbf{;}}}}
 \newcommand{\BRANCH}{\ensuremath{\mbox{\textbf{[}}}}


@@ -291,7 +291,7 @@ allow other developers to quickly understand our code and contribute.
   \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
   \caption[\MATITA{} components and related applications]{\MATITA{}
    components and related applications, with thousands of line of
   \includegraphics[width=0.9\textwidth,height=0.8\textheight]{pics/libraries-clusters}
   \caption[\MATITA{} components and related applications]{\MATITA{}
    components and related applications, with thousands of line of

-   codes (klocs)}
+   codes (klocs).\strut}

   \label{fig:libraries}
  \end{center}
 \end{figure}
   \label{fig:libraries}
  \end{center}
 \end{figure}


@@ -756,6 +756,57 @@ the \MATITA{} authoring interface.
 
 \subsection{Indexing and searching}
 \label{sec:indexing}
 
 \subsection{Indexing and searching}
 \label{sec:indexing}

+The Matita system is first of all an interface between the user and
+the mathematical repository. For this reason, it is important to be
+able to search and retrieve mathematical notions in a quick and 
+effective way, assuming as little knowledge as possible about the 
+library. To this aim, Matita uses a sophisticated indexing mechanism
+for mathemtical items, based on a reach metadata set that has been 
+tuned along the European Project IST-2001-33562 MoWGLI. The metadata
+set, and the searching facilites built on top of them - collected 
+in the so called \whelp seach engine - have been
+extensively described in \cite{whelp}. Let us just recall here that
+the whelp metadata model is essentially based a single ternary relation 
+\REF{p}{s}{t} stating that an object $s$ refers an object $t$ at a
+ given position $p$, where the position specify the place of the 
+occurrence of $t$ inside $s$ (we currently work with a fixed set of 
+positions, discriminating, the hypothesis form the conclusion and
+outermost form innermost occurrences). This approach is extremely 
+flexible, since extending the set of positions 
+we may improve the granularity and the precision of our indexing technique,
+with no additional architectural impact.
+
+Every time a new mathematical object is created and saved by the user it gets 
+indexed, and becomes immediately visible in the library. Several 
+interesting and innovative features of Matita described in the following
+sections rely in a direct or indirect way on its metadata system and
+the searching features. Here, we shall just recall some of its most
+direct applications.
+
+A first, very simple but not negligeable feature is the check for duplicates.
+As soon as a new statement is defined, and before proving it, 
+the library is searched 
+to check that no other equivalent statement has been already proved
+(based on the \whelp{} pattern matching functionality); if this is the case,
+a warning is raised to the user. At present, the notion of equivalence 
+adopted by Matita is convertibility, but we may imagine to weaken it 
+in the future, covering for instance isomorphisms.    
+
+Another usefull \whelp{} operation is {\em hint}; we may invoke this query
+at any moment during the development of a proof, resulting in the list
+of all theorems of the library which can be applied to the current
+goal. In practice, this is mostly used not really to discover what theorems
+can be applied to a given goal, but to actually retrieve a theorem that 
+we wish to apply, but whose name we have forgotten.
+In fact, even if \Matita adopts a semi-rigid naming convention for 
+statements \ref{naming} that greatly simplifies the effort of recalling
+names, the naming discipline remains one of the most
+annoying aspects of formal developments, and the hint feature provides
+a very friendly solution.
+In the near feature, we expect to extend the {\em hint} operation to
+a {\em rewrite-hint}, resulting in all equational statements that
+can be applied to {\em rewrite} the current goal.
+

 
 \subsection{Disambiguation}
 \label{sec:disambiguation}
 
 \subsection{Disambiguation}
 \label{sec:disambiguation}


@@ -773,7 +824,7 @@ Sect.~\ref{sec:contentintro}.
 The key component of the translation is the generic disambiguation algorithm
 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
 and presented in~\cite{disambiguation}. In this section we present how to use
 The key component of the translation is the generic disambiguation algorithm
 implemented in the \texttt{disambiguation} component of Fig.~\ref{fig:libraries}
 and presented in~\cite{disambiguation}. In this section we present how to use

-such an algorithm in the context of the development of a library of formalized
+that algorithm in the context of the development of a library of formalized

 mathematics. We will see that using multiple passes of the algorithm, varying
 some of its parameters, helps in keeping the input terse without sacrificing
 expressiveness.
 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.


@@ -781,7 +832,7 @@ expressiveness.
 \subsubsection{Disambiguation aliases}
 \label{sec:disambaliases}
 
 \subsubsection{Disambiguation aliases}
 \label{sec:disambaliases}
 

-Consider the following command to state a theorem over integer numbers.
+Consider the following command to state a theorem over integer numbers:

 
 \begin{grafite}
 theorem Zlt_compat:
 
 \begin{grafite}
 theorem Zlt_compat:


@@ -794,8 +845,8 @@ Thus, according to the disambiguation algorithm, two different
 refinable partially specified terms could be associated to it.
 \MATITA{} asks the user what interpretation he meant. However, to avoid
 posing the same question in case of a future re-execution (e.g. undo/redo),
 refinable partially specified terms could be associated to it.
 \MATITA{} asks the user what interpretation he meant. However, to avoid
 posing the same question in case of a future re-execution (e.g. undo/redo),

-the choice must be recorded. Scripts need to be re-executed after invalidation.
-Therefore the choice record must be permanently stored somewhere. The most
+the choice must be recorded. Since scripts need to be re-executed after
+invalidation, the choice record must be permanently stored somewhere. The most

 natural place is in the script itself.
 
 In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.
 natural place is in the script itself.
 
 In \MATITA{} disambiguation is governed by \emph{disambiguation aliases}.


@@ -829,7 +880,7 @@ the disambiguation in the rest of the script and speed up disambiguation
 reducing the search space.
 
 Disambiguation preferences are included in the lexicon status
 reducing the search space.
 
 Disambiguation preferences are included in the lexicon status

-(see Sect.~\ref{sec:presentationintro} that is part of the authoring interface
+(see Sect.~\ref{sec:presentationintro}) that is part of the authoring interface

 status.  Unlike aliases, they are not part of the library.
 
 When starting a new authoring session the set of disambiguation preferences
 status.  Unlike aliases, they are not part of the library.
 
 When starting a new authoring session the set of disambiguation preferences


@@ -847,120 +898,107 @@ over integer numbers.
 
 Nothing forbids the set of preferences to become incoherent. For this reason
 the disambiguator cannot always respect the user preferences.
 
 Nothing forbids the set of preferences to become incoherent. For this reason
 the disambiguator cannot always respect the user preferences.

-For example consider:
-
+Consider, for example:

 \begin{grafite}
 \begin{grafite}

-theorem Zlt_mono: \forall x, y, k. x < y \to x < y + k.
+theorem Zlt_mono:
+  \forall x, y, k. x < y \to x < y + k.

 \end{grafite}
 
 No refinable partially specified term corresponds to the preferences:
 \end{grafite}
 
 No refinable partially specified term corresponds to the preferences:

-\OP{+} over natural numbers, \OP{<} over integer numbers.
-When the disambiguator fails, disambiguation is tried again with a less
-strict set of preferences. Thus disambiguation is organized in
-multiple \emph{passes}. In the first pass, called \emph{mono-preferences},
-we consider only the aliases corresponding to the current preferences.
-In the second pass, called \emph{multi-preferences},
-we consider every alias corresponding to a current or past preference.
-For instance, in the example above disambiguation succeeds in the
-multi-preference pass 
-
-\TODO{Disambiguazione: cambiato solo FINQUI}
-
-and suppose that the \OP{+} operator is defined only on natural numbers. If
-the alias for \OP{<} points to the integer version of the operator, no
-refinable partially specified term matching the term could be found.
-
-For this reason we chose to attempt \emph{multiple disambiguation passes}. A
-first pass attempts to disambiguate using the last available disambiguation
-aliases (\emph{mono aliases} pass); in case of failure the next pass tries
-disambiguation again 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.
+\OP{+} over natural numbers, \OP{<} over integer numbers. To overcome this
+limitation we organized disambiguation in \emph{multiple passes}: when the
+disambiguator fails, disambiguation is tried again with a less strict set of
+preferences.
+
+Several disambiguation parameters can vary among passes. With respect to
+preference handling we implemented three passes.  In the first pass, called
+\emph{mono-preferences}, we consider only the aliases corresponding to the
+current preferences.  In the second pass, called \emph{multi-preferences}, we
+consider every alias corresponding to a current or past preference.  For
+instance, in the example above disambiguation succeeds in the multi-preference
+pass. In the third pass, called \emph{library-preferences}, all aliases
+available in the library are considered.
+
+\TODO{rivedere questo periodo\ldots}
+The rationale behind this choice is trying to respect user preferences in early
+passes that complete quickly in case of failure; later passes are slower but
+have more chances of success.

 
 \subsubsection{Operator instances}
 \label{sec:disambinstances}
 
 
 \subsubsection{Operator instances}
 \label{sec:disambinstances}
 

-Let us 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:
-
+Consider now the following theorem:

 \begin{grafite}
 \begin{grafite}

-include "Z/z.ma".
-include "nat/orders.ma".
-..

 theorem lt_to_Zlt_pos_pos:
   \forall n, m: nat. n < m \to pos n < pos m. 
 \end{grafite}
 theorem lt_to_Zlt_pos_pos:
   \forall n, m: nat. n < m \to pos n < pos m. 
 \end{grafite}

-
-Unfortunately, none of the passes described above is able to disambiguate its
-type, no matter how aliases are defined. This is because the \OP{<} operator
-occurs twice in the content level term (it has two \emph{instances}) and two
-different interpretations for it have to be used in order to obtain a refinable
-partially specified term. To address this issue, we have the ability to consider
-each instance of a single symbol as a different ambiguous expression in the
-content level term, and thus we can assign a different interpretation to each of
-them. A disambiguation pass which exploit this feature is said to be using
-\emph{fresh instances}.
+and assume that there exist in the library aliases for \OP{<} over natural
+numbers and over integer numbers. None of the passes described above is able to
+disambiguate \texttt{lt\_to\_Zlt\_pos\_pos}, no matter how preferences are set.
+This is because the \OP{<} operator occurs twice in the content level term (it
+has two \emph{instances}) and two different interpretations for it have to be
+used in order to obtain a refinable partially specified term.
+
+To address this issue, we have the ability to consider each instance of a single
+symbol as a different ambiguous expression in the content level term, and thus
+we can use a different alias for each of them. Exploiting or not this feature is
+one of the disambiguation pass parameters. A disambiguation pass which exploit
+it is said to be using \emph{fresh instances} (opposed to a \emph{shared
+instances} pass).

 
 Fresh instances lead to a non negligible performance loss (since the choice of
 
 Fresh instances lead to a non negligible performance loss (since the choice of

-an interpretation for one instances does not constraint the choice for the
-others). For this reason we always attempt a fresh instances pass only after
-attempting a non-fresh one.
-
-\paragraph{One-shot aliases} Disambiguation aliases as seen so far are
-instance-independent. However, aliases obtained as a result of a disambiguation
-pass which uses fresh instances ought to be instance-dependent, that is: to
-ensure a term can be disambiguated in a batch fashion we may need to state that
-an \emph{i}-th instance of a symbol should be mapped to a given partially
-specified term. Instance-depend aliases are meaningful only for the term whose
+an alias for one instances does not constraint the choice of the others). For
+this reason we always attempt a fresh instances pass only after attempting a
+non-fresh one.
+
+\paragraph{One-shot preferences} Disambiguation preferecens as seen so far are
+instance-independent. However, implicit preferences obtained as a result of a
+disambiguation pass which uses fresh instances ought to be instance-dependent.
+Informally, the set of preferences that can be satisfied by the disambiguator on
+the theorem above is: ``the first instance of the \OP{<} symbol is over natural
+numbers, while the second is on integer numbers''.
+
+Instance-depend preferences are meaningful only for the term whose

 disambiguation generated it. For this reason we call them \emph{one-shot
 disambiguation generated it. For this reason we call them \emph{one-shot

-aliases} and \MATITA{} does not use it to disambiguate further terms down in the
-script.
+preferences} and \MATITA{} does not use them to disambiguate further terms in
+the script.

 
 \subsubsection{Implicit coercions}
 \label{sec:disambcoercions}
 
 
 \subsubsection{Implicit coercions}
 \label{sec:disambcoercions}
 

-Let us now consider a theorem about derivation:
-
+Consider the following theorem about derivation:

 \begin{grafite}
 theorem power_deriv:
   \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
 \end{grafite}
 \begin{grafite}
 theorem power_deriv:
   \forall n: nat, x: R. d x ^ n dx = n * x ^ (n - 1).
 \end{grafite}

-
-and suppose there exists a \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}
-interpretation for \OP{\^}, and a real number interpretation for \OP{*}.
-Mathematicians would write the term that way since it is well known that the
-natural number \texttt{n} could be ``injected'' in \IR{} and considered a real
-number for the purpose of real multiplication. The refiner of \MATITA{} supports
-\emph{implicit coercions} for this reason: given as input the above content
-level term, it will return a partially specified term where in place of
-\texttt{n} the application of a coercion from \texttt{nat} to \texttt{R} appears
-(assuming it has been defined as such of course).
-
-Nonetheless coercions are not always desirable. For example, in disambiguating
+and assume that in the library there is an alias mapping \OP{\^} to a partially
+specified term having type: \texttt{R \TEXMACRO{to} nat \TEXMACRO{to} R}. In
+order to disambiguate \texttt{power\_deriv}, the occurrence of \texttt{n} on the
+right hand side of the equality need to be ``injected'' from \texttt{nat} to
+\texttt{R}.  The refiner of \MATITA{} supports \emph{implicit coercions} for
+this reason: given as input the above presentation level term, it will return a
+partially specified term where in place of \texttt{n} the application of a
+coercion from \texttt{nat} to \texttt{R} appears (assuming such a coercion has
+been defined in advance).
+
+Coercions are not always desirable. For example, in disambiguating

 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up
 \texttt{\TEXMACRO{forall} x: nat. n < n + 1} we do not want the term which uses
 two coercions from \texttt{nat} to \texttt{R} around \OP{<} arguments to show up

-among the possible partially specified term choices. For this reason in
-\MATITA{} we always try first a disambiguation pass which require the refiner
-not to use the coercions and only in case of failure we attempt a
-coercion-enabled pass.
-
-It is interesting to observe also the relationship among operator instances and
-implicit coercions. Consider again the theorem \texttt{lt\_to\_Zlt\_pos\_pos},
-which \MATITA{} disambiguated using fresh instances. In case there exists a
-coercion from natural numbers to (positive) integers (which indeed does, it is
-the \texttt{pos} constructor itself), the theorem can be disambiguated using
-twice that coercion on the left hand side of the implication. The obtained
-partially specified term however would not probably be the expected one, being a
-theorem which prove a trivial implication. For this reason we choose to always
-prefer fresh instances over implicit coercions, i.e. we always attempt
-disambiguation passes with fresh instances and no implicit coercions before
-attempting passes with implicit coercions.
+among the possible partially specified term choices. For this reason we always
+attempt a disambiguation pass which require the refiner not to use the coercions
+before attempting a coercion-enabled pass.
+
+The choice of whether implicit coercions are enabled or not interact with the
+choice about operator instances. Indeed, consider again
+\texttt{lt\_to\_Zlt\_pos\_pos}, which can be disambiguated using fresh operator
+instances. In case there exists a coercion from natural numbers to (positive)
+integers (which indeed does, it is the \texttt{pos} constructor itself), the
+theorem can be disambiguated using twice that coercion on the left hand side of
+the implication. The obtained partially specified term however would not
+probably be the expected one, being a theorem which prove a trivial implication.
+For this reason we choose to always prefer fresh instances over implicit
+coercions, i.e.  we always attempt disambiguation passes with fresh instances
+and no implicit coercions before attempting passes with implicit coercions.

 
 \subsubsection{Disambiguation passes}
 \label{sec:disambpasses}
 
 \subsubsection{Disambiguation passes}
 \label{sec:disambpasses}


@@ -971,22 +1009,22 @@ our experience that choice gives reasonable performance and minimize the need of
 user interaction during the disambiguation.
 
 \begin{table}[ht]
 user interaction during the disambiguation.
 
 \begin{table}[ht]

- \caption{Sequence of disambiguation passes used in \MATITA.\strut}
+ \caption{Disambiguation passes sequence.\strut}

  \label{tab:disambpasses} 
  \begin{center}
   \begin{tabular}{c|c|c|c}
    \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
  \label{tab:disambpasses} 
  \begin{center}
   \begin{tabular}{c|c|c|c}
    \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}

-   & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+   & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Preferences}}

    & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
    & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
    \hline
    & \multicolumn{1}{p{2.5cm}|}{\centering\textbf{Operator instances}}
    & \multicolumn{1}{p{2.5cm}}{\centering\textbf{Implicit coercions}} \\
    \hline

-   \PASS & Mono aliases   & Shared         & Disabled \\
-   \PASS & Multi aliases  & Shared         & Disabled \\
-   \PASS & Mono aliases   & Fresh instances & Disabled \\
-   \PASS & Multi aliases  & Fresh instances & Disabled \\
-   \PASS & Mono        aliases   & Fresh instances & Enabled  \\
-   \PASS & Multi aliases  & Fresh instances & Enabled  \\
-   \PASS & Library aliases& Fresh instances & Enabled
+   \PASS & Mono-preferences    & Shared instances  & Disabled \\
+   \PASS & Multi-preferences   & Shared instances  & Disabled \\
+   \PASS & Mono-preferences    & Fresh instances   & Disabled \\
+   \PASS & Multi-preferences   & Fresh instances   & Disabled \\
+   \PASS & Mono-preferences    & Fresh instances   & Enabled  \\
+   \PASS & Multi-preferences   & Fresh instances   & Enabled  \\
+   \PASS & Library-preferences  & Fresh instances   & Enabled

   \end{tabular}
  \end{center}
 \end{table}
   \end{tabular}
  \end{center}
 \end{table}


@@ -1203,7 +1241,7 @@ fully supported so that mathematical glyphs can be input as such.
 \begin{figure}[!ht]
  \begin{center}
   \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}
 \begin{figure}[!ht]
  \begin{center}
   \includegraphics[width=0.95\textwidth]{pics/matita-screenshot}

-  \caption{\MATITA{} look and feel}
+  \caption{\MATITA{} look and feel.\strut}

   \label{fig:screenshot}
  \end{center}
 \end{figure}
   \label{fig:screenshot}
  \end{center}
 \end{figure}


@@ -1249,7 +1287,7 @@ applications.
   \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
   \hspace{0.05\textwidth}
   \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}
   \includegraphics[width=0.40\textwidth]{pics/matita-screenshot-selection}
   \hspace{0.05\textwidth}
   \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{pics/matita-screenshot-href}}

-  \caption{Semantic selection and hyperlinks}
+  \caption{Semantic selection and hyperlinks.\strut}

   \label{fig:directmanip}
  \end{center}
 \end{figure}
   \label{fig:directmanip}
  \end{center}
 \end{figure}


@@ -1263,7 +1301,7 @@ applications.
   \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
   \hspace{0.02\textwidth}
   \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}
   \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-query}
   \hspace{0.02\textwidth}
   \includegraphics[width=0.30\textwidth]{pics/cicbrowser-screenshot-con}

-  \caption{Browsing and searching the library}
+  \caption{Browsing and searching the library.\strut}

   \label{fig:cicbrowser}
  \end{center}
 \end{figure}
   \label{fig:cicbrowser}
  \end{center}
 \end{figure}


@@ -1467,20 +1505,24 @@ would have resulted in this sequent:
 \end{grafite}
 
 where $H$ is $\beta$-expanded over the second $n$
 \end{grafite}
 
 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. 
+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)}.
+
+Since rewriting, replacing and several other tactics boils down to
+the application of the equality elimination principle, the previous
+trick deals the expected behaviour.

 
 The idea behind this way of identifying subterms in not really far
 
 The idea behind this way of identifying subterms in not really far

-from the idea behind patterns, but really fails in extending to
+from the idea behind patterns, but 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 
 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. 
+more effective way to tell the system what to do. 

 
 One of the goals of \MATITA{} is to use modern publishing techniques, and
 adopting a method for restricting tactics application domain that discourages 
 
 One of the goals of \MATITA{} is to use modern publishing techniques, and
 adopting a method for restricting tactics application domain that discourages 


@@ -1709,7 +1751,7 @@ scripts, listed in Tab.~\ref{tab:scripts}.
   \FILE{fermat\_little\_th.ma} \\     
   \FILE{totient.ma} & & \\
  \end{tabular}
   \FILE{fermat\_little\_th.ma} \\     
   \FILE{totient.ma} & & \\
  \end{tabular}

- \caption{Scripts on natural numbers in the standard library}
+ \caption{Scripts on natural numbers in the standard library.\strut}

  \label{tab:scripts}
 \end{table}
 
  \label{tab:scripts}
 \end{table}