X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fmatita%2Fmatita.tex;h=636860a822ff4ae33ef12a57c7a307d48d7c8f2f;hb=c307d27343fe48aeeb2e1763a811f8122ac1c0df;hp=d0305c38167a1a76899cbdafb691a3f4f016c6ae;hpb=656cb59b98db21ef50afef7677ae03282bd8aad1;p=helm.git

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index d0305c381..636860a82 100644
--- a/helm/papers/matita/matita.tex
+++ b/helm/papers/matita/matita.tex
@@ -332,12 +332,99 @@ library as a whole will be logically inconsistent.
 Logical inconsistency has never been a problem in the daily work of a
 mathematician. The mathematician simply imposes himself a discipline to
 restrict himself to consistent subsets of the mathematical knowledge.
-However, in doing so he doesn't choose the subset in advance by forgetting
-the rest of his knowledge.
+However, in doing so he does not choose the subset in advance by forgetting
+the rest of his knowledge. On the contrary he may proceed with a sort of
+top-down strategy: he may always inspect or use part of his knowledge, but
+when he actually does so he should check recursively that inconsistencies are
+not exploited.
+
+Contrarily to the mathematical practice, the usual tendency in the world of
+assisted automation is that of building a logical environment (a consistent
+subset of the library) in a bottom up way, checking the consistency of a
+new axiom or theorem as soon as it is added to the environment. No lemma
+or definition outside the environment can be used until it is added to the
+library after every notion it depends on. Moreover, very often the logical
+environment is the only part of the library that can be inspected,
+that we can search lemmas in and that can be exploited by automatic tactics.
+
+Moving one by one notions from the library to the environment is a costly
+operation since it involves re-checking the correctness of the notion.
+As a consequence mathematical notions are packages into theories that must
+be added to the environment as a whole. However, the consistency problem is
+only raised at the level of theories: theories must be imported in a bottom
+up way and the system must check that no inconsistency arises.
+
+The practice of limiting the scope on the library to the logical environment
+is contrary to our commitment of being able to fully exploit as much as possible
+of the library at any given time. To reconcile consistency and visibility
+we have departed from the traditional implementation of an environment
+allowing environments to be built on demand in a top-down way. The new
+implementation is based on a modified meta-theory that changes the way
+convertibility, type checking, unification and refinement judgements.
+The modified meta-theory is fully described in \cite{libraryenvironments}.
+Here we just remark how a strong commitment on the way the user interacts
+with the library has lead to modifications to the logical core of the proof
+assistant. This is evidence that breakthroughs in the user interfaces
+and in the way the user interacts with the tools and with the library could
+be achieved only by means of strong architectural changes.
+
+\subsubsection{Accessibility}
+A large library that is completely in scope needs effective indexing and
+searching methods to make the user productive. Libraries of formal results
+are particularly critical since they hold a large percentage of technical
+lemmas that do not have a significative name and that must be retrieved
+using advanced methods based on matching, unification, generalization and
+instantiation.
+
+The efficiency of searching inside the library becomes a critical operation
+when automatic tactics exploit the library during the proof search. In this
+scenario the tactics must retrieve a set of candidates for backward or
+forward reasoning in a few milliseconds.
+
+The choice of several proof assistants is to use ad-hoc data structures,
+such as context trees, to index all the terms currently in scope. These
+data structures are expecially designed to quickly retrieve terms up
+to matching, instantiation and generalization. All these data structures
+try to maximize sharing of identical subterms so that matching can be
+reduced to a visit of the tree (or dag) that holds all the maximally shared
+terms together.
+
+Since the terms to be retrieved (or at least their initial prefix)
+are stored (actually ``melted'') in the data structure, these data structures
+must collect all the terms in a single location. In other words, adopting
+such data structures means centralizing the library.
+
+In the \MOWGLI{} project we have tried to follow an alternative approach
+that consists in keeping the library fully distributed and indexing it
+by means of spiders that collect metadata and store them in a database.
+The challenge is to be able to collect only a smaller as possible number
+of metadata that provide enough information to approximate the matching
+operation. A matching operation is then performed in two steps. The first
+step is a query to the remote search engine that stores the metadata in
+order to detect a (hopefully small) complete set of candidates that could
+match. Completeness means that no term that matches should be excluded from
+the set of candiates. The second step consists in retrieving from the
+distributed library all the candidates and attempt the actual matching.
+
+In the last we years we have progressively improved this technique.
+Our achievements can be found in \cite{query1,query2,query3}.
+
+The technique and tools already developed have been integrated in \MATITA{},
+that is able to contact a remote \WHELP{} search engine \cite{whelp} or that
+can be directly linked to the code of the \WHELP. In either case the database
+used to store the metadata can be local or remote.
+
+Our current challenge consists in the exploitation of \WHELP{} inside of
+\MATITA. In particular we are developing a set of tactics, for instance
+based on paramodulation \cite{paramodulation}, that perform queries to \WHELP{}
+to restrict the scope on the library to a set of interesting candidates,
+greatly reducing the search space. Moreover, queries to \WHELP{} are performed
+during parsing of user provided terms to disambiguate them.
+
+In Sect.~\ref{sec:metadata} we describe the technique adopted in \MATITA.
+
+\subsubsection{Library management}
 
-Contrarily to a mathematician, the usual tendency in the world of assisted
-automation is that of restricting in advance the part of the library that
-will be used later on, checking its consistency by construction.
 
 \subsection{ricerca e indicizzazione}
 \label{sec:metadata}
@@ -662,10 +749,37 @@ can be found in~\cite{disambiguation}, where a formulation without backtracking
 
 \subsubsection{Disambiguation stages}
 
-\subsection{notazione}
+\subsection{notation}
 \label{sec:notation}
 \ASSIGNEDTO{zack}
 
+Mathematical notation plays a fundamental role in mathematical practice: it
+helps expressing in a concise symbolic fashion concepts of arbitrary complexity.
+Its use in proof assistants like \MATITA{} is no exception. Formal mathematics
+indeed often impose to encode mathematical concepts at a very high level of
+details (e.g. Peano numbers, implicit arguments) having a restricted toolbox of
+syntactic constructions in the calculus.
+
+Consider for example one of the point reached while proving the distributivity
+of times over minus on natural numbers included in the \MATITA{} standards
+library. (Part of) the reached sequent can be seen in \MATITA{} both using the
+notation for various arithmetical and relational operator or without using it.
+The sequent rendered without using notation would be as follows:
+\sequent{
+\mathtt{H}: \mathtt{le} z y\\
+\mathtt{Hcut}: \mathtt{eq} \mathtt{nat} (\mathtt{plus} (\mathtt{times} x (\mathtt{minus}
+y z)) (\mathtt{times} x z))\\
+(\mathtt{plus} (\mathtt{minus} (\mathtt{times} x y) (\mathtt{times} x z))
+(\mathtt{times} x z))}{
+\mathtt{eq} \mathtt{nat} (\mathtt{times} x (\mathtt{minus} y z)) (\mathtt{minus}
+(\mathtt{times} x y) (\mathtt{times} x z))}
+while the corresponding sequent rendered with notation enabled would be:
+\sequent{
+H: z\leq y\\
+Hcut: x*(y-z)+x*z=x*y-x*z+x*z}{
+x*(y-z)=x*y-x*z}
+
+
 \subsection{mathml}
 \ASSIGNEDTO{zack}
 
@@ -673,7 +787,6 @@ can be found in~\cite{disambiguation}, where a formulation without backtracking
 \ASSIGNEDTO{zack}
 
 \subsection{pattern}
-\ASSIGNEDTO{gares}\\
 Patterns are the textual counterpart of the MathML widget graphical
 selection.
 
@@ -895,31 +1008,124 @@ using heavy math notation, would definitively be a bad choice.
 \ASSIGNEDTO{gares}\\
 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 first one and how \MATITA{} tries to solve them.
+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.
 
-For first we must highlight the fact that proof scripts made using tactis are
-particularly unreadable. This is not a big deal for the user while he iw
-constructing the proof, but is considerably a problem when he tries to reread
-what he did or whe he shows his work to someone else.
+\subsubsection{Tacticals overview}
 
-Another common issue for tactic based proof scripts is their mantenibility.
-Huge libraries have been developed, and backward compatibility is a really time
-consuming task. This problem is usually ameliorated with tacticals, that
-contibute structuring proofs, but rise one more difficulty for the user that
-want to read a proof, since they are executed in  an atomic way, making the
-user loose intermediate steps.
+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.
+\end{grafite}
 
-\MATITA{} uses a language of tactics and tacticals, but adopts a peculiar
-strategy to make this technique more user friendly without loosing in
-mantenibility or expressivity.
+The first is ``\texttt{;}'' that combines the tactic \texttt{split}
+with \texttt{intro}, applying the latter to each goal opened by the
+former. Then we have ``\texttt{[}'' that branches on the goals (here
+we have two goals, the two sides of the logic and).
+The first goal $B$ (with $A$ in the context)
+is proved by the first sequence of tactics
+\texttt{rewrite} and \texttt{assumption}. Then we move to the second
+goal with the separator ``\texttt{|}''. The last tactical we see here
+is ``\texttt{.}'' that is a sequential composition that selects the
+first goal opened for the following tactic (instead of applying it to
+them all like ``\texttt{;}''). Note that usually ``\texttt{.}'' is
+not considered a tactical, but a sentence terminator (i.e. the
+delimiter of commands the proof assistant executes).
+
+Giving serious examples here is rather difficult, since they are hard
+to read without the interactive tool. To help the reader in
+understanding the following considerations we just give few common
+usage examples without a proof context.
 
-\subsubsection{Tacticals overview}
-Before describing the peculiarities of \MATITA{} tacticals we briefly introduce what tacticals are and where they can be useful.
+\begin{grafite}
+  elim z; try assumption; [ ... | ... ].
+  elim z; first [ assumption | reflexivity | id ].
+\end{grafite}
 
-Tacticals first appered in LCF(cita qualcosa) and can be seen as programming constructs, like
-looping, branching, error recovery or sequential composition. 
+The first example goes by induction on a term \texttt{z} and applies
+the tactic \texttt{assumption} to each opened goal eventually recovering if
+\texttt{assumption} fails. Here we are asking the system to close all
+trivial cases and then we branch on the remaining with ``\texttt{[}''.
+The second example goes again by induction on \texttt{z} and tries to
+close each opened goal first with \texttt{assumption}, if it fails it
+tries \texttt{reflexivity} and finally \texttt{id}
+that is the tactic that leaves the goal untouched without failing. 
+
+Note that in the common implementation of tacticals both lines are
+compositions of tacticals and in particular they are a single
+statement (i.e. derived from the same non terminal entry of the
+grammar) ended with ``\texttt{.}''. As we will see later in \MATITA{}
+this is not true, since each atomic tactic or punctuation is considered 
+a single statement.
+
+\subsubsection{Common issues of tactic(als)-based proof languages}
+We will examine the two main problems of tactic(als)-based proof script:
+maintainability and readability. 
+
+Huge libraries of formal mathematics have been developed, and backward
+compatibility is a really time consuming task. \\
+A real-life example in the history of \MATITA{} was the reordering of
+goals opened by a tactic application. We noticed that some tactics
+were not opening goals in the expected order. In particular the
+\texttt{elim} tactic on a term of an inductive type with constructors
+$c_1, \ldots, c_n$ used to open goals in order $g_1, g_n, g_{n-1}
+\ldots, g_2$. The library of \MATITA{} was still in an embryonic state
+but some theorems about integers were there. The inductive type of
+$\mathcal{Z}$ has three constructors: $zero$, $pos$ and $neg$. All the
+induction proofs on this type where written without tacticals and,
+obviously, considering the three induction cases in the wrong order.
+Fixing the behavior of the tactic broke the library and two days of
+work were needed to make it compile again. The whole time was spent in
+finding the list of tactics used to prove the third induction case and
+swap it with the list of tactics used to prove the second case.  If
+the proofs was structured with the branch tactical this task could
+have been done automatically. 
+
+From this experience we learned that the use of tacticals for
+structuring proofs gives some help but may have some drawbacks in
+proof script readability. We must highlight that proof scripts
+readability is poor by itself, but in conjunction with tacticals it
+can be nearly impossible. The main cause is the fact that in proof
+scripts there is no trace of what you are working on. It is not rare
+for two different theorems to have the same proof script (while the
+proof is completely different).\\
+Bad readability is not a big deal for the user while he is
+constructing the proof, but is considerably a problem when he tries to
+reread what he did or when he shows his work to someone else.  The
+workaround commonly used to read a script is to execute it again
+step-by-step, so that you can see the proof goal changing and you can
+follow the proof steps. This works fine until you reach a tactical.  A
+compound statement, made by some basic tactics glued with tacticals,
+is executed in a single step, while it obviously performs lot of proof
+steps.  In the fist example of the previous section the whole branch
+over the two goals (respectively the left and right part of the logic
+and) result in a single step of execution. The workaround doesn't work
+anymore unless you de-structure on the fly the proof, putting some
+``\texttt{.}'' where you want the system to stop.\\
+
+Now we can understand the tradeoff between script readability and
+proof structuring with tacticals. Using tacticals helps in maintaining
+scripts, but makes it really hard to read them again, cause of the way
+they are executed.
+
+\MATITA{} uses a language of tactics and tacticals, but tries to avoid
+this tradeoff, alluring the user to write structured proof without
+making it impossible to read them again.
+
+\subsubsection{The \MATITA{} approach: Tinycals}
 
-\MATITA{} tacticals syntax is reported in table \ref{tab:tacsyn}.
 \begin{table}
  \caption{\label{tab:tacsyn} Concrete syntax of \MATITA{} tacticals.\strut}
 \hrule
@@ -938,37 +1144,54 @@ looping, branching, error recovery or sequential composition.
 \hrule
 \end{table}
 
-While one whould expect to find structured constructs like 
+\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{\MATITA{} Tinycals}
-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 execute as an atomic operation. This has two major benefits for the user, even being a so simple idea:
+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 easyer. Consider for example a proof by induction. After applying the
-  induction principle, with one step tacticals, you have to choose: structure
+  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
-  \verb+[+ and write tactics for all the cases and the close the tactical with
-  \verb+]+. You can replace most of the cases by the identity tactic just to
-  concentrate only on the first goal, but you will have to one step back and
-  one further every time you add something inside the tactical. And if you are
-  boared of doing so, you will finish in giving up structuring the proof and
-  write a plain list of tactics.
+  ``\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 baranches with a \verb+[+. This clearly subdivided all
-  the induction cases, but if the square brackets content is executed in one
-  single step you completely loose the possibility of rereading it. Again,
-  executing step-by-step is the way you whould like to review the
-  demonstration. Remember tha understandig 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 goning on.
+  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}
 
-
-
 \subsection{named variable e disambiguazione lazy}
 \ASSIGNEDTO{csc}