Added a few bibliographic entries.

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

diff --git a/helm/papers/matita/matita.tex b/helm/papers/matita/matita.tex
index d0305c38167a1a76899cbdafb691a3f4f016c6ae..636860a822ff4ae33ef12a57c7a307d48d7c8f2f 100644 (file)
--- 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.
 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}
 
 \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}
 
 
 \subsubsection{Disambiguation stages}
 

-\subsection{notazione}
+\subsection{notation}

 \label{sec:notation}
 \ASSIGNEDTO{zack}
 
 \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}
 
 \subsection{mathml}
 \ASSIGNEDTO{zack}
 


@@ -673,7 +787,6 @@ can be found in~\cite{disambiguation}, where a formulation without backtracking
 \ASSIGNEDTO{zack}
 
 \subsection{pattern}
 \ASSIGNEDTO{zack}
 
 \subsection{pattern}

-\ASSIGNEDTO{gares}\\

 Patterns are the textual counterpart of the MathML widget graphical
 selection.
 
 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
 \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
 \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}
 
 \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.
 
 $\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] 
 \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
   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]
 \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}
 
 \end{description}
 

-
-

 \subsection{named variable e disambiguazione lazy}
 \ASSIGNEDTO{csc}
 
 \subsection{named variable e disambiguazione lazy}
 \ASSIGNEDTO{csc}