+
+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).
+
+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.
+
+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.
+
+\subsubsection{Disambiguation passes}
+
+According to the criteria described above in \MATITA{} we choose to perform the
+sequence of disambiguation passes depicted in Tab.~\ref{tab:disambpasses}. In
+our experience that choice implements a good trade off among disambiguation time
+and admitted ambiguity in terms input by users.
+
+\begin{table}[ht]
+ \caption{Sequence of disambiguation passes used in \MATITA.\strut}
+ \label{tab:disambpasses}
+ \begin{center}
+ \begin{tabular}{c|c|c|c}
+ \multicolumn{1}{p{1.5cm}|}{\centering\raisebox{-1.5ex}{\textbf{Pass}}}
+ & \multicolumn{1}{p{3.1cm}|}{\centering\textbf{Disambiguation aliases}}
+ & \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
+ \end{tabular}
+ \end{center}
+\end{table}
+
+
+
+\subsection{Compilation and cleaning}
+\label{sec:libmanagement}
+
+%
+%goals: consentire sviluppo di una librearia mantenendo integrita' referenziale e usando le teconologie nostre (quindi con metadati, XML, libreria visibile)
+%\subsubsection{Composition}
+%scripts.ma, .moo, XML, metadata
+%\subsubsection{Compilation}
+%analogie con compilazione classica dso.\\
+%granularita' differenti per uso interattivo e non
+%\paragraph{Batch}
+%- granularita' .ma/buri \\
+%-- motivazioni\\
+%- come si calcolano le dipendenze\\
+%- quando la si usa\\
+%- metodi (cc e clean)\\
+%- garanzie
+%\paragraph{Interactive}
+%- granularita' fine\\
+%-- motivazioni
+%\label{sec:libmanagement}
+%consistenza: integrita' referenziale
+%Goals: mantenere consistente la rappresentazione della libreria su
+%memoria persistente consentendo di compilare e pulire le compilation
+%unit (.ma).\\
+%Vincoli: dipendenze oggetti-oggetti e metadati-oggetti\\
+%Due livelli di gestione libreria, uno e' solo in fase interattiva dove la compilazione e' passo passo: \\
+%--- granularita' oggetto per matita interactive\\
+%--- granularita' baseuri (compilation unit) per la libreria\\
+%In entrmbi i casi ora:\\
+%--- matitaSync: add, remove, timetravel(facility-macro tra 2 stati)[obj]\\
+%--- matitaCleanLib: clean\_baseuri (che poi usa matitaSync a sua volta)[comp1]\\
+%Vincoli di add: typecheck ( ==$>$ tutto quello che usa sta in lib)\\
+%Vincoli di remove: \\
+%--- la remove di mSync non li controlla (ma sa cosa cancellare per ogni uri)\\
+%--- la clean\_baseuri calcola le dipendenze con i metadati (o anche i moo direi) e li rispetta\\
+%Undo di matita garantisce la consistenza a patto che l'history che tiene sia ok\\
+%Undo della lib (mClean) garantisce la consistenza (usando moo o Db).\\
+
+The aim of this section is to describe the way \MATITA{}
+preserves the consistency and the availability of the library
+using the \WHELP{} technology, in response to the user addition or
+removal of mathematical objects.
+
+As already sketched in \ref{fully-spec} the output of the
+compilation of a script is split among two storage media, a
+classical filesystem and a relational database. The former is used to
+store the XML encoding of the objects defined in the script, the
+disambiguation aliases and the interpretation and notational convention defined,
+while the latter is used to store all the metadata needed by
+\WHELP{}.
+
+While the consistency of the data store in the two media has
+nothing to do with the nature of
+the content of the library and is thus uninteresting (but really
+tedious to implement and keep bug-free), there is a deeper
+notion of mathematical consistency we need to provide. Each object
+must reference only defined object (i.e. each proof must use only
+already proved theorems).
+
+We will focus on how \MATITA{} ensures the interesting kind
+of consistency during the formalization of a mathematical theory,
+giving the user the freedom of adding, removing, modifying objects
+without loosing the feeling of an always visible and browsable
+library.
+
+\subsubsection{Compilation}
+
+The typechecker component guarantees that if an object is well typed
+it depends only on well typed objects available in the library,
+that is exactly what we need to be sure that the logic consistency of
+the library is preserved. We have only to find the right order of
+compilation of the scripts that compose the user development.
+
+For this purpose we provide a tool called \MATITADEP{}
+that takes in input the list of files that compose the development and
+outputs their dependencies in a format suitable for the GNU \texttt{make} tool.
+The user is not asked to run \MATITADEP{} by hand, but
+simply to tell \MATITA{} the root directory of his development (where all
+script files can be found) and \MATITA{} will handle all the compilation
+related tasks, including dependencies calculation.
+To compute dependencies it is enough to look at the script files for
+inclusions of other parts of the development or for explicit
+references to other objects (i.e. with explicit aliases, see
+\ref{sec:disambaliases}).
+
+The output of the compilation is immediately available to the user
+trough the \WHELP{} technology, since all metadata are stored in a
+user-specific area of the database where the search engine has read
+access, and all the automated tactics that operates on the whole
+library, like \AUTO, have full visibility of the newly defined objects.
+
+Compilation is rather simple, and the only tricky case is when we want
+to compile again the same script, maybe after the removal of a
+theorem. Here the policy is simple: clean the output before recompiling.
+As we will see in the next section cleaning will ensure that
+there will be no theorems in the development that depends on the
+removed items.
+
+\subsubsection{Cleaning}
+
+With the term ``cleaning'' we mean the process of removing all the
+results of an object compilation. In order to keep the consistency of
+the library, cleaning an object requires the (recursive) cleaning
+of all the objects that depend on it (\emph{reverse dependencies}).
+
+The calculation of the reverse dependencies can be computed in two
+ways, using the relational database or using a simpler set of metadata
+that \MATITA{} saves in the filesystem as a result of compilation. The
+former technique is the same used by the \emph{Dependency Analyzer}
+described in \cite{zack-master} and really depends on a relational
+database.
+
+The latter is a fall-back in case the database is not
+available.\footnote{Due to the complex deployment of a large piece of
+software like a database, it is a common practice for the \HELM{} team
+to use a shared remote database, that may be unavailable if the user
+workstation lacks network connectivity.} This facility has to be
+intended only as a fall-back, since the queries of the \WHELP{}
+technology depend require a working database.
+
+Cleaning guarantees that if an object is removed there are no dandling
+references to it, and that the part of the library still compiled is
+consistent. Since cleaning involves the removal of all the results of
+the compilation, metadata included, the library browsable trough the
+\WHELP{} technology is always kept up to date.
+
+\subsubsection{Batch vs Interactive}
+
+\MATITA{} includes an interactive graphical interface and a batch
+compiler (\MATITAC). Only the former is intended to be used directly by the
+user, the latter is automatically invoked when a
+part of the user development is required (for example issuing an
+\texttt{include} command) but not yet compiled.
+
+While they share the same engine for compilation and cleaning, they
+provide different granularity. The batch compiler is only able to
+compile a whole script and similarly to clean only a whole script
+(together with all the other scripts that rely on an object defined in
+it). The interactive interface is able to execute single steps of
+compilation, that may include the definition of an object, and
+similarly to undo single steps. Note that in the latter case there is
+no risk of introducing dangling references since the \MATITA{} user
+interface inhibit undoing a step which is not the last executed.
+
+\subsection{Automation}
+
+\subsection{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{The authoring interface}
+
+\begin{figure}[t]
+ \begin{center}
+ \includegraphics[width=0.95\textwidth]{matita-screenshot}
+ \caption{\MATITA{} look and feel}
+ \label{fig:screenshot}
+ \end{center}
+\end{figure}
+
+\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.
+
+\subsection{Patterns}
+
+\subsubsection{Direct manipulation of terms}
+
+While terms are input as \TeX-like formulae in \MATITA, they're converted to a
+mixed \MATHML+\BOXML{} markup for output purposes and then rendered by
+\GTKMATHVIEW. This mixed choice~\cite{latexmathml} enables both high-quality
+bidimensional rendering of terms (including the use of fancy layout schemata
+like radicals and matrices~\cite{mathml}) and the use of a concise and
+widespread textual syntax.
+
+\begin{figure}[t]
+ \begin{center}
+ \includegraphics[width=0.40\textwidth]{matita-screenshot-selection}
+ \hspace{0.05\textwidth}
+ \raisebox{0.4cm}{\includegraphics[width=0.50\textwidth]{matita-screenshot-href}}
+ \caption{Semantic selection and hyperlinks}
+ \label{fig:directmanip}
+ \end{center}
+\end{figure}
+
+Keeping pointers from the presentations level terms down to the
+partially specified ones \MATITA{} enable direct manipulation of
+rendered (sub)terms in the form of hyperlinks and semantic selection.
+\emph{Hyperlinks} have anchors on the occurrences of constant and
+inductive type constructors and point to the corresponding definitions
+in the library. Anchors are available notwithstanding the use of
+user-defined mathematical notation: as can be seen on the right of
+Fig.~\ref{fig:directmanip}, where we clicked on $\not|$, symbols
+encoding complex notations retain all the hyperlinks of constants or
+constructors used in the notation.
+
+\emph{Semantic selection} enable the selection of mixed
+\MATHML+\BOXML{} markup, constraining the selection to markup
+representing meaningful CIC (sub)terms. In the example on the left of
+Fig.~\ref{fig:directmanip} is thus possible to select the subterm
+$\mathrm{prime}~n$, whereas it would not be possible to select
+$\forall~n:nat$ since the former denotes an application while the
+latter denotes an incomplete $\Pi$-binder. Once a (sub)term has been
+selected that way actions can be done on it like reductions or tactic
+applications.
+
+In our experience working with direct manipulation of terms is really
+effective and faster than retyping them. Nonetheless we need a way to
+encode term selections in scripts so that they can be batch compiled
+by \MATITAC. In \MATITA{} \emph{patterns} implement that encoding,
+being patterns the textual representations of \GTKMATHVIEW{} semantic
+selections. \NOTE{Zack:c'\`e scritto da qualche parte che l'utente
+non li deve necessariamente scrivere a mano, ma che pu\`o incollarli?
+Va scritto.}
+
+\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:pathsyn} Patterns concrete syntax.\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}
+% \]
+\[
+\begin{array}{@{}rcll@{}}
+ \NT{pattern} &
+ ::= & [~\verb+in+~\NT{sequent\_path}~]~[~\verb+match+~\NT{wanted}~] & \\
+ \NT{sequent\_path} &
+ ::= & \{~\NT{ident}~[~\verb+:+~\NT{multipath}~]~\}~
+ [~\verb+\vdash+~\NT{multipath}~] & \\
+ \NT{multipath} & ::= & \NT{term\_with\_placeholders} & \\
+ \NT{wanted} & ::= & \NT{term} & \\
+\end{array}
+\]
+\hrule
+\end{table}
+
+\subsubsection{Pattern concepts}
+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.
+
+ The first phase selects not only terms (roots of subterms) but also
+ their context that will be eventually used in the second phase.
+
+\item[Phase 2]
+ plays a role only if the $[~\verb+match+~\NT{wanted}~]$
+ part is specified. From the first phase we have some terms, that we
+ will see as subterm roots, and their context. For each of these
+ contexts the $\NT{wanted}$ term is disambiguated in it and the
+ corresponding root is searched for a subterm $\alpha$-equivalent to
+ $\NT{wanted}$. The result of this search is the selection the
+ pattern represents.
+
+\end{description}
+
+\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.
+
+\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)$